{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
module GHC.TcPlugin.API.Internal.Shim.Reduction where
import Prelude
hiding (Floating(cos))
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
)
data Reduction =
Reduction
{ Reduction -> Coercion
reductionCoercion :: Coercion
, Reduction -> Type
reductionReducedType :: !Type
}
data HetReduction =
HetReduction
Reduction
MCoercion
mkHetReduction :: Reduction
-> MCoercion
-> HetReduction
mkHetReduction :: Reduction -> MCoercion -> HetReduction
mkHetReduction Reduction
redn MCoercion
mco = Reduction -> MCoercion -> HetReduction
HetReduction Reduction
redn MCoercion
mco
{-# INLINE mkHetReduction #-}
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 #-}
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 forall a b. (a -> b) -> a -> b
$ [SDoc] -> SDoc
vcat
[ String -> SDoc
text String
"reductionOriginalType:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Reduction -> Type
reductionOriginalType Reduction
redn)
, String -> SDoc
text String
" reductionReducedType:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Reduction -> Type
reductionReducedType Reduction
redn)
, String -> SDoc
text String
" reductionCoercion:" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr (Reduction -> Coercion
reductionCoercion Reduction
redn)
]
type ReductionN = Reduction
type ReductionR = Reduction
reductionOriginalType :: Reduction -> Type
reductionOriginalType :: Reduction -> Type
reductionOriginalType = Coercion -> Type
coercionLKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. Reduction -> Coercion
reductionCoercion
{-# INLINE reductionOriginalType #-}
coercionRedn :: Coercion -> Reduction
coercionRedn :: Coercion -> Reduction
coercionRedn Coercion
co = Coercion -> Type -> Reduction
Reduction Coercion
co (Coercion -> Type
coercionRKind Coercion
co)
{-# INLINE coercionRedn #-}
downgradeRedn :: Role
-> 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 #-}
mkSubRedn :: Reduction -> Reduction
mkSubRedn :: Reduction -> Reduction
mkSubRedn redn :: Reduction
redn@(Reduction Coercion
co Type
_) = Reduction
redn { reductionCoercion :: Coercion
reductionCoercion = HasDebugCallStack => Coercion -> Coercion
mkSubCo Coercion
co }
{-# INLINE mkSubRedn #-}
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 #-}
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
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
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 #-}
mkCastRedn1 :: Role
-> Type
-> CoercionN
-> Reduction
-> Reduction
mkCastRedn1 :: Role -> Type -> Coercion -> Reduction -> Reduction
mkCastRedn1 Role
r Type
ty Coercion
cast_co (Reduction Coercion
co Type
xi)
= 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 #-}
mkCastRedn2 :: Role
-> Type
-> CoercionN
-> Reduction
-> CoercionN
-> 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 #-}
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 #-}
mkFunRedn :: Role
#if MIN_VERSION_ghc(8,10,0)
-> AnonArgFlag
#endif
#if MIN_VERSION_ghc(9,0,0)
-> ReductionN
#endif
-> Reduction
-> Reduction
-> Reduction
mkFunRedn :: Role
-> AnonArgFlag -> Reduction -> Reduction -> Reduction -> Reduction
mkFunRedn Role
r
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
(Reduction Coercion
w_co Type
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 -> Coercion
mkFunCo
Role
r
#if MIN_VERSION_ghc(9,0,0)
Coercion
w_co
#endif
Coercion
arg_co
Coercion
res_co
)
( AnonArgFlag -> Type -> Type -> Type -> Type
mkFunTy
#if MIN_VERSION_ghc(8,10,0)
AnonArgFlag
vis
#endif
#if MIN_VERSION_ghc(9,0,0)
Type
w_ty
#endif
Type
arg_ty
Type
res_ty
)
{-# INLINE mkFunRedn #-}
mkForAllRedn :: ArgFlag
-> TyVar
-> ReductionN
-> 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 #-}
mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn :: [TyVarBinder] -> Reduction -> Reduction
mkHomoForAllRedn [TyVarBinder]
bndrs (Reduction Coercion
co Type
ty)
= Coercion -> Type -> Reduction
mkReduction
([TyVar] -> Coercion -> Coercion
mkHomoForAllCos (forall tv argf. [VarBndr tv argf] -> [tv]
binderVars [TyVarBinder]
bndrs) Coercion
co)
([TyVarBinder] -> Type -> Type
mkForAllTys [TyVarBinder]
bndrs Type
ty)
{-# INLINE mkHomoForAllRedn #-}
mkProofIrrelRedn :: Role
-> CoercionN
-> Coercion
-> Coercion
-> Reduction
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 #-}
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 #-}
data Reductions = Reductions [Coercion] [Type]
mkReductions :: [Coercion] -> [Type] -> Reductions
mkReductions :: [Coercion] -> [Type] -> Reductions
mkReductions [Coercion]
cos [Type]
tys = [Coercion] -> [Type] -> Reductions
Reductions [Coercion]
cos [Type]
tys
{-# INLINE mkReductions #-}
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 #-}
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
mkTyConAppCo Role
role TyCon
tc [Coercion]
cos) (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc [Type]
tys)
{-# INLINE mkTyConAppRedn #-}
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
mkTyConAppCo Role
Nominal (Class -> TyCon
classTyCon Class
cls) [Coercion]
cos)
(Class -> [Type] -> Type
mkClassPred Class
cls [Type]
tys)
{-# INLINE mkClassPredRedn #-}
unzipRedns :: [Reduction] -> Reductions
unzipRedns :: [Reduction] -> Reductions
unzipRedns = 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
coforall a. a -> [a] -> [a]
:[Coercion]
cos) (Type
xiforall 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 forall a b. (a -> b) -> a -> b
$ TyCoVarSet -> InScopeSet
mkInScopeSet 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 forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => 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
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
!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_coforall a. a -> [a] -> [a]
:[Coercion]
cos) (Type
casted_xiforall a. a -> [a] -> [a]
:[Type]
xis))
MCoercion
final_kind_co
go LiftingContext
lc [] Type
inner_ki [Role]
roles [Reduction]
arg_redns
= let co1 :: Coercion
co1 = HasDebugCallStack => 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 = 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)
decomposePiCos Coercion
co1 Pair Type
co1_kind [Type]
unrewritten_tys
casted_args :: [Reduction]
casted_args = 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]
_ = forall a. HasCallStack => String -> a
error String
"simplifyArgsWorker wandered into deeper water than usual"
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
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
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 co = case coercionKind co of { Pair lco _ -> lco }
coercionRKind co = case coercionKind co of { Pair _ rco -> rco }
castCoercionKind2 :: Coercion -> Role -> Type -> Type
-> CoercionN -> CoercionN -> Coercion
castCoercionKind2 g r t1 t2 h1 h2
= mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
castCoercionKind1 :: Coercion -> Role -> Type -> Type
-> CoercionN -> Coercion
castCoercionKind1 g r t1 t2 h
= case g of
Refl {} -> mkNomReflCo (mkCastTy t2 h)
GRefl _ _ mco -> case mco of
MRefl -> mkReflCo r (mkCastTy t2 h)
MCo kind_co -> GRefl r (mkCastTy t1 h) $
MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)
_ -> castCoercionKind2 g r t1 t2 h h
#endif
#if !MIN_VERSION_ghc(8,10,0)
coToMCo :: Coercion -> MCoercion
coToMCo co | isReflCo co = MRefl
| otherwise = MCo co
#endif