{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

module GHC.TcPlugin.API.Internal.Shim.Reduction where

-- base

import Prelude
  hiding (Floating(cos))

-- ghc

import GHC.Core.Class
  ( Class(classTyCon) )
import GHC.Core.Coercion
  ( Coercion, CoercionN, MCoercion(..)
  , Role(Nominal), LiftingContext
#if MIN_VERSION_ghc(9,0,0)
  , castCoercionKind1, castCoercionKind2
  , coercionLKind, coercionRKind
#else
  , mkCoherenceLeftCo, mkNomReflCo
#endif
  , coercionKind
#if MIN_VERSION_ghc(8,10,0)
  , coToMCo
#else
  , isReflCo
#endif
  , decomposePiCos, downgradeRole
  , liftCoSubst, emptyLiftingContext, extendLiftingContextAndInScope, zapLiftingContext
  , mkAppCo, mkAppCos
  , mkCoherenceRightCo
  , mkForAllCo, mkFunCo
  , mkGReflLeftCo, mkGReflRightCo
  , mkHomoForAllCos, mkProofIrrelCo
  , mkReflCo, mkSubCo, mkSymCo, mkTransCo, mkTyConAppCo
  )
import GHC.Core.Predicate
  ( mkClassPred )
import GHC.Core.TyCo.Rep
  ( TyCoBinder, mkFunTy
#if !MIN_VERSION_ghc(9,0,0)
  , Coercion(..)
#endif
  )
import GHC.Core.TyCon
  ( TyCon )
import GHC.Core.Type
  ( ArgFlag, Kind, Type, TyVar, TyVarBinder
#if MIN_VERSION_ghc(8,10,0)
  , AnonArgFlag
#endif
  , binderVars
  , mkAppTy, mkAppTys, mkCastTy, mkCoercionTy, mkForAllTy, mkForAllTys
  , mkTyConApp, mkPiTys
  , noFreeVarsOfType
  , splitPiTys, tyCoBinderType, tyCoBinderVar_maybe
  )
import GHC.Data.Pair
  ( Pair(Pair) )
import GHC.Types.Var
  ( setTyVarKind )
import GHC.Types.Var.Env
  ( mkInScopeSet )
import GHC.Types.Var.Set
  ( TyCoVarSet )
import GHC.Utils.Outputable
  ( Outputable(ppr), (<+>)
  , braces, text, vcat
  )

--------------------------------------------------------------------------------



-- | A 'Reduction' is the result of an operation that rewrites a type @ty_in@.

-- The 'Reduction' includes the rewritten type @ty_out@ and a 'Coercion' @co@

-- such that @co :: ty_in ~ ty_out@, where the role of the coercion is determined

-- by the context. That is, the LHS type of the coercion is the original type

-- @ty_in@, while its RHS type is the rewritten type @ty_out@.

--

-- A Reduction is always homogeneous, unless it is wrapped inside a 'HetReduction',

-- which separately stores the kind coercion.

data Reduction =
  Reduction
    { Reduction -> Coercion
reductionCoercion    :: Coercion
    , Reduction -> Type
reductionReducedType :: !Type
    }

-- | Stores a heterogeneous reduction.

--

-- The stored kind coercion must relate the kinds of the

-- stored reduction. That is, in @HetReduction (Reduction co xi) kco@,

-- we must have:

--

-- >  co :: ty ~ xi

-- > kco :: typeKind ty ~ typeKind xi

data HetReduction =
  HetReduction
    Reduction
    MCoercion

-- | Create a heterogeneous reduction.

--

-- Pre-condition: the provided kind coercion (second argument)

-- relates the kinds of the stored reduction.

-- That is, if the coercion stored in the 'Reduction' is of the form

--

-- > co :: ty ~ xi

--

-- Then the kind coercion supplied must be of the form:

--

-- > kco :: typeKind ty ~ typeKind xi

mkHetReduction :: Reduction  -- ^ heterogeneous reduction

               -> MCoercion  -- ^ kind coercion

               -> HetReduction
mkHetReduction :: Reduction -> MCoercion -> HetReduction
mkHetReduction Reduction
redn MCoercion
mco = Reduction -> MCoercion -> HetReduction
HetReduction Reduction
redn MCoercion
mco
{-# INLINE mkHetReduction #-}

-- | Homogenise a heterogeneous reduction.

--

-- Given @HetReduction (Reduction co xi) kco@, with

--

-- >  co :: ty ~ xi

-- > kco :: typeKind(ty) ~ typeKind(xi)

--

-- this returns the homogeneous reduction:

--

-- > hco :: ty ~ ( xi |> sym kco )

homogeniseHetRedn :: Role -> HetReduction -> Reduction
homogeniseHetRedn :: Role -> HetReduction -> Reduction
homogeniseHetRedn Role
role (HetReduction Reduction
redn MCoercion
kco)
  = Role -> Reduction -> MCoercion -> Reduction
mkCoherenceRightMRedn Role
role Reduction
redn (MCoercion -> MCoercion
mkSymMCo MCoercion
kco)
{-# INLINE homogeniseHetRedn #-}

-- | Create a 'Reduction' from a pair of a 'Coercion' and a 'Type.

--

-- Pre-condition: the RHS type of the coercion matches the provided type

-- (perhaps up to zonking).

--

-- Use 'coercionRedn' when you only have the coercion.

mkReduction :: Coercion -> Type -> Reduction
mkReduction :: Coercion -> Type -> Reduction
mkReduction Coercion
co Type
ty = Coercion -> Type -> Reduction
Reduction Coercion
co Type
ty
{-# INLINE mkReduction #-}

instance Outputable Reduction where
  ppr :: Reduction -> SDoc
ppr Reduction
redn =
    SDoc -> SDoc
braces (SDoc -> SDoc) -> SDoc -> SDoc
forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
      [ String -> SDoc
text String
"reductionOriginalType:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Reduction -> Type
reductionOriginalType Reduction
redn)
      , String -> SDoc
text String
" reductionReducedType:" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Reduction -> Type
reductionReducedType Reduction
redn)
      , String -> SDoc
text String
"    reductionCoercion:" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Reduction -> Coercion
reductionCoercion Reduction
redn)
      ]

-- | A 'Reduction' in which the 'Coercion' has 'Nominal' role.

type ReductionN = Reduction

-- | A 'Reduction' in which the 'Coercion' has 'Representational' role.

type ReductionR = Reduction

-- | Get the original, unreduced type corresponding to a 'Reduction'.

--

-- This is obtained by computing the LHS kind of the stored coercion,

-- which may be slow.

reductionOriginalType :: Reduction -> Type
reductionOriginalType :: Reduction -> Type
reductionOriginalType = Coercion -> Type
coercionLKind (Coercion -> Type) -> (Reduction -> Coercion) -> Reduction -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reduction -> Coercion
reductionCoercion
{-# INLINE reductionOriginalType #-}

-- | Turn a 'Coercion' into a 'Reduction'

-- by inspecting the RHS type of the coercion.

--

-- Prefer using 'mkReduction' when you already know

-- the RHS type of the coercion, to avoid computing it anew.

coercionRedn :: Coercion -> Reduction
coercionRedn :: Coercion -> Reduction
coercionRedn Coercion
co = Coercion -> Type -> Reduction
Reduction Coercion
co (Coercion -> Type
coercionRKind Coercion
co)
{-# INLINE coercionRedn #-}

-- | Downgrade the role of the coercion stored in the 'Reduction'.

downgradeRedn :: Role -- ^ desired role

              -> Role -- ^ current role

              -> Reduction
              -> Reduction
downgradeRedn :: Role -> Role -> Reduction -> Reduction
downgradeRedn Role
new_role Role
old_role redn :: Reduction
redn@(Reduction Coercion
co Type
_)
  = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = Role -> Role -> Coercion -> Coercion
downgradeRole Role
new_role Role
old_role Coercion
co }
{-# INLINE downgradeRedn #-}

-- | Downgrade the role of the coercion stored in the 'Reduction',

-- from 'Nominal' to 'Representational'.

mkSubRedn :: Reduction -> Reduction
mkSubRedn :: Reduction -> Reduction
mkSubRedn redn :: Reduction
redn@(Reduction Coercion
co Type
_) = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = Coercion -> Coercion
mkSubCo Coercion
co }
{-# INLINE mkSubRedn #-}

-- | Compose a reduction with a coercion on the left.

--

-- Pre-condition: the provided coercion's RHS type must match the LHS type

-- of the coercion that is stored in the reduction.

mkTransRedn :: Coercion -> Reduction -> Reduction
mkTransRedn :: Coercion -> Reduction -> Reduction
mkTransRedn Coercion
co1 redn :: Reduction
redn@(Reduction Coercion
co2 Type
_)
  = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = Coercion
co1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co2 }
{-# INLINE mkTransRedn #-}

-- | The reflexive reduction.

mkReflRedn :: Role -> Type -> Reduction
mkReflRedn :: Role -> Type -> Reduction
mkReflRedn Role
r Type
ty = Coercion -> Type -> Reduction
mkReduction (Role -> Type -> Coercion
mkReflCo Role
r Type
ty) Type
ty

-- | Create a 'Reduction' from a kind cast, in which

-- the casted type is the rewritten type.

--

-- Given @ty :: k1@, @mco :: k1 ~ k2@,

-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@

-- at the given 'Role'.

mkGReflRightRedn :: Role -> Type -> CoercionN -> Reduction
mkGReflRightRedn :: Role -> Type -> Coercion -> Reduction
mkGReflRightRedn Role
role Type
ty Coercion
co
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
role Type
ty Coercion
co)
      (Type -> Coercion -> Type
mkCastTy Type
ty Coercion
co)
{-# INLINE mkGReflRightRedn #-}

-- | Create a 'Reduction' from a kind cast, in which

-- the casted type is the rewritten type.

--

-- Given @ty :: k1@, @mco :: k1 ~ k2@,

-- produces the 'Reduction' @ty ~res_co~> (ty |> mco)@

-- at the given 'Role'.

mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflRightMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflRightMRedn Role
role Type
ty MCoercion
mco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo Role
role Type
ty MCoercion
mco)
      (Type -> MCoercion -> Type
mkCastTyMCo Type
ty MCoercion
mco)
{-# INLINE mkGReflRightMRedn #-}

-- | Create a 'Reduction' from a kind cast, in which

-- the casted type is the original (non-rewritten) type.

--

-- Given @ty :: k1@, @mco :: k1 ~ k2@,

-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@

-- at the given 'Role'.

mkGReflLeftRedn :: Role -> Type -> CoercionN -> Reduction
mkGReflLeftRedn :: Role -> Type -> Coercion -> Reduction
mkGReflLeftRedn Role
role Type
ty Coercion
co
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
role Type
ty Coercion
co)
      Type
ty
{-# INLINE mkGReflLeftRedn #-}

-- | Create a 'Reduction' from a kind cast, in which

-- the casted type is the original (non-rewritten) type.

--

-- Given @ty :: k1@, @mco :: k1 ~ k2@,

-- produces the 'Reduction' @(ty |> mco) ~res_co~> ty@

-- at the given 'Role'.

mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflLeftMRedn :: Role -> Type -> MCoercion -> Reduction
mkGReflLeftMRedn Role
role Type
ty MCoercion
mco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo Role
role Type
ty MCoercion
mco)
      Type
ty
{-# INLINE mkGReflLeftMRedn #-}

-- | Apply a cast to the result of a 'Reduction'.

--

-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @kco@

-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> kco )@

-- of the given 'Role' (which must match the role of the coercion stored

-- in the 'Reduction' argument).

mkCoherenceRightRedn :: Role -> Reduction -> CoercionN -> Reduction
mkCoherenceRightRedn :: Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
r (Reduction Coercion
co1 Type
ty2) Coercion
kco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty2 Coercion
kco Coercion
co1)
      (Type -> Coercion -> Type
mkCastTy Type
ty2 Coercion
kco)
{-# INLINE mkCoherenceRightRedn #-}

-- | Apply a cast to the result of a 'Reduction', using an 'MCoercionN'.

--

-- Given a 'Reduction' @ty1 ~co1~> (ty2 :: k2)@ and a kind coercion @mco@

-- with LHS kind @k2@, produce a new 'Reduction' @ty1 ~co2~> ( ty2 |> mco )@

-- of the given 'Role' (which must match the role of the coercion stored

-- in the 'Reduction' argument).

mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction
mkCoherenceRightMRedn :: Role -> Reduction -> MCoercion -> Reduction
mkCoherenceRightMRedn Role
r (Reduction Coercion
co1 Type
ty2) MCoercion
kco
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo Role
r Type
ty2 MCoercion
kco Coercion
co1)
      (Type -> MCoercion -> Type
mkCastTyMCo Type
ty2 MCoercion
kco)
{-# INLINE mkCoherenceRightMRedn #-}

-- | Apply a cast to a 'Reduction', casting both the original and the reduced type.

--

-- Given @cast_co@ and 'Reduction' @ty ~co~> xi@, this function returns

-- the 'Reduction' @(ty |> cast_co) ~return_co~> (xi |> cast_co)@

-- of the given 'Role' (which must match the role of the coercion stored

-- in the 'Reduction' argument).

--

-- Pre-condition: the 'Type' passed in is the same as the LHS type

-- of the coercion stored in the 'Reduction'.

mkCastRedn1 :: Role
            -> Type      -- ^ original type

            -> CoercionN -- ^ coercion to cast with

            -> Reduction -- ^ rewritten type, with rewriting coercion

            -> Reduction
mkCastRedn1 :: Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
r Type
ty Coercion
cast_co (Reduction Coercion
co Type
xi)
  -- co :: ty ~r ty'

  -- return_co :: (ty |> cast_co) ~r (ty' |> cast_co)

  = Coercion -> Type -> Reduction
mkReduction
      (Coercion -> Role -> Type -> Type -> Coercion -> Coercion
castCoercionKind1 Coercion
co Role
r Type
ty Type
xi Coercion
cast_co)
      (Type -> Coercion -> Type
mkCastTy Type
xi Coercion
cast_co)
{-# INLINE mkCastRedn1 #-}

-- | Apply casts on both sides of a 'Reduction' (of the given 'Role').

--

-- Use 'mkCastRedn1' when you want to cast both the original and reduced types

-- in a 'Reduction' using the same coercion.

--

-- Pre-condition: the 'Type' passed in is the same as the LHS type

-- of the coercion stored in the 'Reduction'.

mkCastRedn2 :: Role
            -> Type      -- ^ original type

            -> CoercionN -- ^ coercion to cast with on the left

            -> Reduction -- ^ rewritten type, with rewriting coercion

            -> CoercionN -- ^ coercion to cast with on the right

            -> Reduction
mkCastRedn2 :: Role -> Type -> Coercion -> Reduction -> Coercion -> Reduction
mkCastRedn2 Role
r Type
ty Coercion
cast_co (Reduction Coercion
nco Type
nty) Coercion
cast_co'
  = Coercion -> Type -> Reduction
mkReduction
      (Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
nco Role
r Type
ty Type
nty Coercion
cast_co Coercion
cast_co')
      (Type -> Coercion -> Type
mkCastTy Type
nty Coercion
cast_co')
{-# INLINE mkCastRedn2 #-}

-- | Apply one 'Reduction' to another.

--

-- Combines 'mkAppCo' and 'mkAppTy`.

mkAppRedn :: Reduction -> Reduction -> Reduction
mkAppRedn :: Reduction -> Reduction -> Reduction
mkAppRedn (Reduction Coercion
co1 Type
ty1) (Reduction Coercion
co2 Type
ty2)
  = Coercion -> Type -> Reduction
mkReduction (Coercion -> Coercion -> Coercion
mkAppCo Coercion
co1 Coercion
co2) (Type -> Type -> Type
mkAppTy Type
ty1 Type
ty2)
{-# INLINE mkAppRedn #-}

-- | Create a function 'Reduction'.

--

-- Combines 'mkFunCo' and 'mkFunTy'.

mkFunRedn :: Role
#if MIN_VERSION_ghc(8,10,0)
          -> AnonArgFlag
#endif
#if MIN_VERSION_ghc(9,0,0)
          -> ReductionN -- ^ multiplicity reduction

#endif
          -> Reduction  -- ^ argument reduction

          -> Reduction  -- ^ result reduction

          -> Reduction
mkFunRedn :: Role -> AnonArgFlag -> Reduction -> Reduction -> Reduction
mkFunRedn Role
r
#if MIN_VERSION_ghc(8,10,0)
  AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
  (Reduction w_co w_ty)
#endif
  (Reduction Coercion
arg_co Type
arg_ty)
  (Reduction Coercion
res_co Type
res_ty)
    = Coercion -> Type -> Reduction
mkReduction
        ( Role -> Coercion -> Coercion -> Coercion
mkFunCo
            Role
r
#if MIN_VERSION_ghc(9,0,0)
            w_co
#endif
            Coercion
arg_co
            Coercion
res_co
        )
        ( AnonArgFlag -> Type -> Type -> Type
mkFunTy
#if MIN_VERSION_ghc(8,10,0)
            AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
            w_ty
#endif
            Type
arg_ty
            Type
res_ty
        )
{-# INLINE mkFunRedn #-}

-- | Create a 'Reduction' associated to a Π type,

-- from a kind 'Reduction' and a body 'Reduction'.

--

-- Combines 'mkForAllCo' and 'mkForAllTy'.

mkForAllRedn :: ArgFlag
             -> TyVar
             -> ReductionN -- ^ kind reduction

             -> Reduction  -- ^ body reduction

             -> Reduction
mkForAllRedn :: ArgFlag -> TyVar -> Reduction -> Reduction -> Reduction
mkForAllRedn ArgFlag
vis TyVar
tv1 (Reduction Coercion
h Type
ki') (Reduction Coercion
co Type
ty)
  = Coercion -> Type -> Reduction
mkReduction
      (TyVar -> Coercion -> Coercion -> Coercion
mkForAllCo TyVar
tv1 Coercion
h Coercion
co)
      (TyVar -> ArgFlag -> Type -> Type
mkForAllTy TyVar
tv2 ArgFlag
vis Type
ty)
  where
    tv2 :: TyVar
tv2 = TyVar -> Type -> TyVar
setTyVarKind TyVar
tv1 Type
ki'
{-# INLINE mkForAllRedn #-}

-- | Create a 'Reduction' of a quantified type from a

-- 'Reduction' of the body.

--

-- Combines 'mkHomoForAllCos' and 'mkForAllTys'.

mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn [TyVarBinder]
bndrs (Reduction Coercion
co Type
ty)
  = Coercion -> Type -> Reduction
mkReduction
      ([TyVar] -> Coercion -> Coercion
mkHomoForAllCos ([TyVarBinder] -> [TyVar]
forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
bndrs) Coercion
co)
      ([TyVarBinder] -> Type -> Type
mkForAllTys [TyVarBinder]
bndrs Type
ty)
{-# INLINE mkHomoForAllRedn #-}

-- | Create a 'Reduction' from a coercion between coercions.

--

-- Combines 'mkProofIrrelCo' and 'mkCoercionTy'.

mkProofIrrelRedn :: Role      -- ^ role of the created coercion, "r"

                 -> CoercionN -- ^ co :: phi1 ~N phi2

                 -> Coercion  -- ^ g1 :: phi1

                 -> Coercion  -- ^ g2 :: phi2

                 -> Reduction -- ^ res_co :: g1 ~r g2

mkProofIrrelRedn :: Role -> Coercion -> Coercion -> Coercion -> Reduction
mkProofIrrelRedn Role
role Coercion
co Coercion
g1 Coercion
g2
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
role Coercion
co Coercion
g1 Coercion
g2)
      (Coercion -> Type
mkCoercionTy Coercion
g2)
{-# INLINE mkProofIrrelRedn #-}

-- | Create a reflexive 'Reduction' whose RHS is the given 'Coercion',

-- with the specified 'Role'.

mkReflCoRedn :: Role -> Coercion -> Reduction
mkReflCoRedn :: Role -> Coercion -> Reduction
mkReflCoRedn Role
role Coercion
co
  = Coercion -> Type -> Reduction
mkReduction
      (Role -> Type -> Coercion
mkReflCo Role
role Type
co_ty)
      Type
co_ty
  where
    co_ty :: Type
co_ty = Coercion -> Type
mkCoercionTy Coercion
co
{-# INLINE mkReflCoRedn #-}

-- | A collection of 'Reduction's where the coercions and the types are stored separately.

--

-- Use 'unzipRedns' to obtain 'Reductions' from a list of 'Reduction's.

--

-- This datatype is used in 'mkAppRedns', 'mkClassPredRedns' and 'mkTyConAppRedn',

-- which expect separate types and coercions.

--

-- Invariant: the two stored lists are of the same length,

-- and the RHS type of each coercion is the corresponding type.

data Reductions = Reductions [Coercion] [Type]

-- | Create 'Reductions' from individual lists of coercions and types.

--

-- The lists should be of the same length, and the RHS type of each coercion

-- should match the specified type in the other list.

mkReductions :: [Coercion] -> [Type] -> Reductions
mkReductions :: [Coercion] -> [Type] -> Reductions
mkReductions [Coercion]
cos [Type]
tys = [Coercion] -> [Type] -> Reductions
Reductions [Coercion]
cos [Type]
tys
{-# INLINE mkReductions #-}

-- | Combines 'mkAppCos' and 'mkAppTys'.

mkAppRedns :: Reduction -> Reductions -> Reduction
mkAppRedns :: Reduction -> Reductions -> Reduction
mkAppRedns (Reduction Coercion
co Type
ty) (Reductions [Coercion]
cos [Type]
tys)
  = Coercion -> Type -> Reduction
mkReduction (Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
co [Coercion]
cos) (Type -> [Type] -> Type
mkAppTys Type
ty [Type]
tys)
{-# INLINE mkAppRedns #-}

-- | 'TyConAppCo' for 'Reduction's: combines 'mkTyConAppCo' and `mkTyConApp`.

mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn :: Role -> TyCon -> Reductions -> Reduction
mkTyConAppRedn Role
role TyCon
tc (Reductions [Coercion]
cos [Type]
tys)
  = Coercion -> Type -> Reduction
mkReduction (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos) (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys)
{-# INLINE mkTyConAppRedn #-}

-- | Reduce the arguments of a 'Class' 'TyCon'.

mkClassPredRedn :: Class -> Reductions -> Reduction
mkClassPredRedn :: Class -> Reductions -> Reduction
mkClassPredRedn Class
cls (Reductions [Coercion]
cos [Type]
tys)
  = Coercion -> Type -> Reduction
mkReduction
      (HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal (Class -> TyCon
classTyCon Class
cls) [Coercion]
cos)
      (Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys)
{-# INLINE mkClassPredRedn #-}

-- | Obtain 'Reductions' from a list of 'Reduction's by unzipping.

unzipRedns :: [Reduction] -> Reductions
unzipRedns :: [Reduction] -> Reductions
unzipRedns = (Reduction -> Reductions -> Reductions)
-> Reductions -> [Reduction] -> Reductions
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Reduction -> Reductions -> Reductions
accRedn ([Coercion] -> [Type] -> Reductions
Reductions [] [])
  where
    accRedn :: Reduction -> Reductions -> Reductions
    accRedn :: Reduction -> Reductions -> Reductions
accRedn (Reduction Coercion
co Type
xi) (Reductions [Coercion]
cos [Type]
xis)
      = [Coercion] -> [Type] -> Reductions
Reductions (Coercion
coCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
cos) (Type
xiType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
xis)
{-# INLINE unzipRedns #-}

--------------------------------------------------------------------------------


data ArgsReductions =
  ArgsReductions
    {-# UNPACK #-} !Reductions
    !MCoercion

{-# INLINE simplifyArgsWorker #-}
simplifyArgsWorker :: [TyCoBinder] -> Kind -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker :: [TyCoBinder]
-> Type -> TyCoVarSet -> [Role] -> [Reduction] -> ArgsReductions
simplifyArgsWorker [TyCoBinder]
orig_ki_binders Type
orig_inner_ki TyCoVarSet
orig_fvs
                   [Role]
orig_roles [Reduction]
orig_simplified_args
  = LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go LiftingContext
orig_lc
       [TyCoBinder]
orig_ki_binders Type
orig_inner_ki
       [Role]
orig_roles [Reduction]
orig_simplified_args
  where
    orig_lc :: LiftingContext
orig_lc = InScopeSet -> LiftingContext
emptyLiftingContext (InScopeSet -> LiftingContext) -> InScopeSet -> LiftingContext
forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet (TyCoVarSet -> InScopeSet) -> TyCoVarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ TyCoVarSet
orig_fvs

    go :: LiftingContext -> [TyCoBinder] -> Kind -> [Role] -> [Reduction] -> ArgsReductions
    go :: LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go !LiftingContext
lc [TyCoBinder]
binders Type
inner_ki [Role]
_ []
      = Reductions -> MCoercion -> ArgsReductions
ArgsReductions
          ([Coercion] -> [Type] -> Reductions
mkReductions [] [])
          MCoercion
kind_co
      where
        final_kind :: Type
final_kind = [TyCoBinder] -> Type -> Type
mkPiTys [TyCoBinder]
binders Type
inner_ki
        kind_co :: MCoercion
kind_co | Type -> Bool
noFreeVarsOfType Type
final_kind = MCoercion
MRefl
                | Bool
otherwise                   = Coercion -> MCoercion
MCo (Coercion -> MCoercion) -> Coercion -> MCoercion
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc Type
final_kind

    go LiftingContext
lc (TyCoBinder
binder:[TyCoBinder]
binders) Type
inner_ki (Role
role:[Role]
roles) (Reduction
arg_redn:[Reduction]
arg_redns)
      =  let !kind_co :: Coercion
kind_co = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc (TyCoBinder -> Type
tyCoBinderType TyCoBinder
binder)
             !(Reduction Coercion
casted_co Type
casted_xi)
                      = Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn Role
role Reduction
arg_redn Coercion
kind_co
         -- now, extend the lifting context with the new binding

             !new_lc :: LiftingContext
new_lc | Just TyVar
tv <- TyCoBinder -> Maybe TyVar
tyCoBinderVar_maybe TyCoBinder
binder
                     = LiftingContext -> TyVar -> Coercion -> LiftingContext
extendLiftingContextAndInScope LiftingContext
lc TyVar
tv Coercion
casted_co
                     | Bool
otherwise
                     = LiftingContext
lc
             !(ArgsReductions (Reductions [Coercion]
cos [Type]
xis) MCoercion
final_kind_co)
               = LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go LiftingContext
new_lc [TyCoBinder]
binders Type
inner_ki [Role]
roles [Reduction]
arg_redns
         in Reductions -> MCoercion -> ArgsReductions
ArgsReductions
              ([Coercion] -> [Type] -> Reductions
Reductions (Coercion
casted_coCoercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
:[Coercion]
cos) (Type
casted_xiType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
xis))
              MCoercion
final_kind_co

    -- See Note [Last case in simplifyArgsWorker]

    go LiftingContext
lc [] Type
inner_ki [Role]
roles [Reduction]
arg_redns
      = let co1 :: Coercion
co1 = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc Type
inner_ki
            co1_kind :: Pair Type
co1_kind              = Coercion -> Pair Type
coercionKind Coercion
co1
            unrewritten_tys :: [Type]
unrewritten_tys       = (Reduction -> Type) -> [Reduction] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Reduction -> Type
reductionOriginalType [Reduction]
arg_redns
            ([Coercion]
arg_cos, Coercion
res_co)     = HasDebugCallStack =>
Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
decomposePiCos Coercion
co1 Pair Type
co1_kind [Type]
unrewritten_tys
            casted_args :: [Reduction]
casted_args           = (Role -> Reduction -> Coercion -> Reduction)
-> [Role] -> [Reduction] -> [Coercion] -> [Reduction]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 Role -> Reduction -> Coercion -> Reduction
mkCoherenceRightRedn [Role]
roles [Reduction]
arg_redns [Coercion]
arg_cos
            zapped_lc :: LiftingContext
zapped_lc             = LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
lc
            Pair Type
rewritten_kind Type
_ = Pair Type
co1_kind
            ([TyCoBinder]
bndrs, Type
new_inner)    = Type -> ([TyCoBinder], Type)
splitPiTys Type
rewritten_kind

            ArgsReductions Reductions
redns_out MCoercion
res_co_out
              = LiftingContext
-> [TyCoBinder] -> Type -> [Role] -> [Reduction] -> ArgsReductions
go LiftingContext
zapped_lc [TyCoBinder]
bndrs Type
new_inner [Role]
roles [Reduction]
casted_args
        in
          Reductions -> MCoercion -> ArgsReductions
ArgsReductions Reductions
redns_out (Coercion
res_co Coercion -> MCoercion -> MCoercion
`mkTransMCoR` MCoercion
res_co_out)

    go LiftingContext
_ [TyCoBinder]
_ Type
_ [Role]
_ [Reduction]
_ = String -> ArgsReductions
forall a. HasCallStack => String -> a
error String
"simplifyArgsWorker wandered into deeper water than usual"

--------------------------------------------------------------------------------


-- | Get the reverse of an 'MCoercion'

mkSymMCo :: MCoercion -> MCoercion
mkSymMCo :: MCoercion -> MCoercion
mkSymMCo MCoercion
MRefl    = MCoercion
MRefl
mkSymMCo (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
mkSymCo Coercion
co)

mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo Role
r Type
ty MCoercion
MRefl    = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
mkGReflLeftMCo Role
r Type
ty (MCo Coercion
co) = Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
r Type
ty Coercion
co

mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo Role
r Type
ty MCoercion
MRefl    = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
mkGReflRightMCo Role
r Type
ty (MCo Coercion
co) = Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
r Type
ty Coercion
co

-- | Cast a type by an 'MCoercion'

mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo Type
ty MCoercion
MRefl    = Type
ty
mkCastTyMCo Type
ty (MCo Coercion
co) = Type
ty Type -> Coercion -> Type
`mkCastTy` Coercion
co

-- | Like 'mkCoherenceRightCo', but with an 'MCoercion'

mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo Role
_ Type
_  MCoercion
MRefl    Coercion
co2 = Coercion
co2
mkCoherenceRightMCo Role
r Type
ty (MCo Coercion
co) Coercion
co2 = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty Coercion
co Coercion
co2

mkTransMCoR :: Coercion -> MCoercion -> MCoercion
mkTransMCoR :: Coercion -> MCoercion -> MCoercion
mkTransMCoR Coercion
co1 MCoercion
MRefl     = Coercion -> MCoercion
coToMCo Coercion
co1
mkTransMCoR Coercion
co1 (MCo Coercion
co2) = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)

--------------------------------------------------------------------------------


#if !MIN_VERSION_ghc(9,0,0)

coercionLKind, coercionRKind :: Coercion -> Type
coercionLKind :: Coercion -> Type
coercionLKind Coercion
co = case Coercion -> Pair Type
coercionKind Coercion
co of { Pair Type
lco Type
_ -> Type
lco }
coercionRKind :: Coercion -> Type
coercionRKind Coercion
co = case Coercion -> Pair Type
coercionKind Coercion
co of { Pair Type
_ Type
rco -> Type
rco }

-- | Creates a new coercion with both of its types casted by different casts

-- @castCoercionKind2 g r t1 t2 h1 h2@, where @g :: t1 ~r t2@,

-- has type @(t1 |> h1) ~r (t2 |> h2)@.

-- @h1@ and @h2@ must be nominal.

castCoercionKind2 :: Coercion -> Role -> Type -> Type
                 -> CoercionN -> CoercionN -> Coercion
castCoercionKind2 :: Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
g Role
r Type
t1 Type
t2 Coercion
h1 Coercion
h2
  = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
t2 Coercion
h2 (Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
r Type
t1 Coercion
h1 Coercion
g)

-- | @castCoercionKind1 g r t1 t2 h@ = @coercionKind g r t1 t2 h h@

-- That is, it's a specialised form of castCoercionKind, where the two

--          kind coercions are identical

-- @castCoercionKind1 g r t1 t2 h@, where @g :: t1 ~r t2@,

-- has type @(t1 |> h) ~r (t2 |> h)@.

-- @h@ must be nominal.

-- See Note [castCoercionKind1]

castCoercionKind1 :: Coercion -> Role -> Type -> Type
                  -> CoercionN -> Coercion
castCoercionKind1 :: Coercion -> Role -> Type -> Type -> Coercion -> Coercion
castCoercionKind1 Coercion
g Role
r Type
t1 Type
t2 Coercion
h
  = case Coercion
g of
      Refl {} -> Type -> Coercion
mkNomReflCo (Type -> Coercion -> Type
mkCastTy Type
t2 Coercion
h)
      GRefl Role
_ Type
_ MCoercion
mco -> case MCoercion
mco of
           MCoercion
MRefl       -> Role -> Type -> Coercion
mkReflCo Role
r (Type -> Coercion -> Type
mkCastTy Type
t2 Coercion
h)
           MCo Coercion
kind_co -> Role -> Type -> MCoercion -> Coercion
GRefl Role
r (Type -> Coercion -> Type
mkCastTy Type
t1 Coercion
h) (MCoercion -> Coercion) -> MCoercion -> Coercion
forall a b. (a -> b) -> a -> b
$
                          Coercion -> MCoercion
MCo (Coercion -> Coercion
mkSymCo Coercion
h Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
kind_co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
h)
      Coercion
_ -> Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
g Role
r Type
t1 Type
t2 Coercion
h Coercion
h
#endif

#if !MIN_VERSION_ghc(8,10,0)

coToMCo :: Coercion -> MCoercion
coToMCo co | isReflCo co = MRefl
           | otherwise   = MCo co

#endif