{-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts, BangPatterns,
ScopedTypeVariables #-}
module GHC.Core.Coercion (
Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
UnivCoProvenance, CoercionHole(..), BlockSubstFlag(..),
coHoleCoVar, setCoHoleCoVar,
LeftOrRight(..),
Var, CoVar, TyCoVar,
Role(..), ltRole,
coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
coercionType, mkCoercionType,
coercionKind, coercionLKind, coercionRKind,coercionKinds,
coercionRole, coercionKindRole,
mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
mkCoVarCo, mkCoVarCos,
mkAxInstCo, mkUnbranchedAxInstCo,
mkAxInstRHS, mkUnbranchedAxInstRHS,
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkTransMCo,
mkNthCo, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo,
castCoercionKind, castCoercionKind1, castCoercionKind2,
mkFamilyTyConAppCo,
mkHeteroCoercionType,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
instNewTyCon_maybe,
NormaliseStepper, NormaliseStepResult(..), composeSteppers,
mapStepResult, unwrapNewTypeStepper,
topNormaliseNewType_maybe, topNormaliseTypeX,
decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
splitTyConAppCo_maybe,
splitAppCo_maybe,
splitFunCo_maybe,
splitForAllCo_maybe,
splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
pickLR,
isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
isReflCoVar_maybe, isGReflMCo, coToMCo,
mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
isCoVar_maybe,
tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
coercionSize,
CvSubstEnv, emptyCvSubstEnv,
lookupCoVar,
substCo, substCos, substCoVar, substCoVars, substCoWith,
substCoVarBndr,
extendTvSubstAndInScope, getCvSubstEnv,
liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
emptyLiftingContext, extendLiftingContext, extendLiftingContextAndInScope,
liftCoSubstVarBndrUsing, isMappedByLC,
mkSubstLiftingContext, zapLiftingContext,
substForAllCoBndrUsingLC, lcTCvSubst, lcInScopeSet,
LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
eqCoercion, eqCoercionX,
seqCo,
pprCo, pprParendCo,
pprCoAxiom, pprCoAxBranch, pprCoAxBranchLHS,
pprCoAxBranchUser, tidyCoAxBndrsForUser,
etaExpandCoAxBranch,
tidyCo, tidyCos,
promoteCoercion, buildCoercion,
multToCo,
simplifyArgsWorker,
badCoercionHole, badCoercionHoleCo
) where
#include "GhclibHsVersions.h"
import {-# SOURCE #-} GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs)
import GHC.Prelude
import GHC.Iface.Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Tidy
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import {-# SOURCE #-} GHC.Core.Utils ( mkFunctionType )
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Name hiding ( varName )
import GHC.Utils.Misc
import GHC.Types.Basic
import GHC.Utils.Outputable
import GHC.Types.Unique
import GHC.Data.Pair
import GHC.Types.SrcLoc
import GHC.Builtin.Names
import GHC.Builtin.Types.Prim
import GHC.Data.List.SetOps
import GHC.Data.Maybe
import GHC.Types.Unique.FM
import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
import Data.Char( isDigit )
import qualified Data.Monoid as Monoid
coVarName :: CoVar -> Name
coVarName :: CoVar -> Name
coVarName = CoVar -> Name
varName
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = CoVar -> Unique -> CoVar
setVarUnique
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName = CoVar -> Name -> CoVar
setVarName
etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
etaExpandCoAxBranch :: CoAxBranch -> ([CoVar], [Type], Type)
etaExpandCoAxBranch (CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
cab_tvs = [CoVar]
tvs
, cab_eta_tvs :: CoAxBranch -> [CoVar]
cab_eta_tvs = [CoVar]
eta_tvs
, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs
, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs })
= ([CoVar]
tvs [CoVar] -> [CoVar] -> [CoVar]
forall a. [a] -> [a] -> [a]
++ [CoVar]
eta_tvs, [Type]
lhs [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
++ [Type]
eta_tys, Type -> [Type] -> Type
mkAppTys Type
rhs [Type]
eta_tys)
where
eta_tys :: [Type]
eta_tys = [CoVar] -> [Type]
mkTyVarTys [CoVar]
eta_tvs
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax :: CoAxiom br
ax@(CoAxiom { co_ax_tc :: forall (br :: BranchFlag). CoAxiom br -> TyCon
co_ax_tc = TyCon
tc, co_ax_branches :: forall (br :: BranchFlag). CoAxiom br -> Branches br
co_ax_branches = Branches br
branches })
= SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"axiom" SDoc -> SDoc -> SDoc
<+> CoAxiom br -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoAxiom br
ax SDoc -> SDoc -> SDoc
<+> SDoc
dcolon)
Int
2 ([SDoc] -> SDoc
vcat ((CoAxBranch -> SDoc) -> [CoAxBranch] -> [SDoc]
forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
tc) (Branches br -> [CoAxBranch]
forall (br :: BranchFlag). Branches br -> [CoAxBranch]
fromBranches Branches br
branches)))
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
tc CoAxBranch
br
| TyCon -> Bool
isDataFamilyTyCon TyCon
tc = TyCon -> CoAxBranch -> SDoc
pprCoAxBranchLHS TyCon
tc CoAxBranch
br
| Bool
otherwise = TyCon -> CoAxBranch -> SDoc
pprCoAxBranch TyCon
tc CoAxBranch
br
pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchLHS = (TidyEnv -> Type -> SDoc) -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch TidyEnv -> Type -> SDoc
forall p p. p -> p -> SDoc
pp_rhs
where
pp_rhs :: p -> p -> SDoc
pp_rhs p
_ p
_ = SDoc
empty
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch = (TidyEnv -> Type -> SDoc) -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch TidyEnv -> Type -> SDoc
ppr_rhs
where
ppr_rhs :: TidyEnv -> Type -> SDoc
ppr_rhs TidyEnv
env Type
rhs = SDoc
equals SDoc -> SDoc -> SDoc
<+> TidyEnv -> PprPrec -> Type -> SDoc
pprPrecTypeX TidyEnv
env PprPrec
topPrec Type
rhs
ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
-> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc) -> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch TidyEnv -> Type -> SDoc
ppr_rhs TyCon
fam_tc CoAxBranch
branch
= (SDoc -> SDoc -> SDoc) -> [SDoc] -> SDoc
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ((SDoc -> Int -> SDoc -> SDoc) -> Int -> SDoc -> SDoc -> SDoc
forall a b c. (a -> b -> c) -> b -> a -> c
flip SDoc -> Int -> SDoc -> SDoc
hangNotEmpty Int
2)
[ [TyCoVarBinder] -> SDoc
pprUserForAll (ArgFlag -> [CoVar] -> [TyCoVarBinder]
forall vis. vis -> [CoVar] -> [VarBndr CoVar vis]
mkTyCoVarBinders ArgFlag
Inferred [CoVar]
bndrs')
, SDoc
pp_lhs SDoc -> SDoc -> SDoc
<+> TidyEnv -> Type -> SDoc
ppr_rhs TidyEnv
tidy_env Type
ee_rhs
, String -> SDoc
text String
"-- Defined" SDoc -> SDoc -> SDoc
<+> SDoc
pp_loc ]
where
loc :: SrcSpan
loc = CoAxBranch -> SrcSpan
coAxBranchSpan CoAxBranch
branch
pp_loc :: SDoc
pp_loc | SrcSpan -> Bool
isGoodSrcSpan SrcSpan
loc = String -> SDoc
text String
"at" SDoc -> SDoc -> SDoc
<+> SrcLoc -> SDoc
forall a. Outputable a => a -> SDoc
ppr (SrcSpan -> SrcLoc
srcSpanStart SrcSpan
loc)
| Bool
otherwise = String -> SDoc
text String
"in" SDoc -> SDoc -> SDoc
<+> SrcSpan -> SDoc
forall a. Outputable a => a -> SDoc
ppr SrcSpan
loc
([CoVar]
ee_tvs, [Type]
ee_lhs, Type
ee_rhs) = CoAxBranch -> ([CoVar], [Type], Type)
etaExpandCoAxBranch CoAxBranch
branch
pp_lhs :: SDoc
pp_lhs = PprPrec -> IfaceTyCon -> IfaceAppArgs -> SDoc
pprIfaceTypeApp PprPrec
topPrec (TyCon -> IfaceTyCon
toIfaceTyCon TyCon
fam_tc)
(TidyEnv -> TyCon -> [Type] -> IfaceAppArgs
tidyToIfaceTcArgs TidyEnv
tidy_env TyCon
fam_tc [Type]
ee_lhs)
(TidyEnv
tidy_env, [CoVar]
bndrs') = TidyEnv -> [CoVar] -> (TidyEnv, [CoVar])
tidyCoAxBndrsForUser TidyEnv
emptyTidyEnv [CoVar]
ee_tvs
tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
tidyCoAxBndrsForUser :: TidyEnv -> [CoVar] -> (TidyEnv, [CoVar])
tidyCoAxBndrsForUser TidyEnv
init_env [CoVar]
tcvs
= (TidyEnv
tidy_env, [CoVar] -> [CoVar]
forall a. [a] -> [a]
reverse [CoVar]
tidy_bndrs)
where
(TidyEnv
tidy_env, [CoVar]
tidy_bndrs) = ((TidyEnv, [CoVar]) -> CoVar -> (TidyEnv, [CoVar]))
-> (TidyEnv, [CoVar]) -> [CoVar] -> (TidyEnv, [CoVar])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (TidyEnv, [CoVar]) -> CoVar -> (TidyEnv, [CoVar])
tidy_one (TidyEnv
init_env, []) [CoVar]
tcvs
tidy_one :: (TidyEnv, [CoVar]) -> CoVar -> (TidyEnv, [CoVar])
tidy_one (env :: TidyEnv
env@(TidyOccEnv
occ_env, VarEnv CoVar
subst), [CoVar]
rev_bndrs') CoVar
bndr
| CoVar -> Bool
is_wildcard CoVar
bndr = (TidyEnv
env_wild, [CoVar]
rev_bndrs')
| Bool
otherwise = (TidyEnv
env', CoVar
bndr' CoVar -> [CoVar] -> [CoVar]
forall a. a -> [a] -> [a]
: [CoVar]
rev_bndrs')
where
(TidyEnv
env', CoVar
bndr') = TidyEnv -> CoVar -> (TidyEnv, CoVar)
tidyVarBndr TidyEnv
env CoVar
bndr
env_wild :: TidyEnv
env_wild = (TidyOccEnv
occ_env, VarEnv CoVar -> CoVar -> CoVar -> VarEnv CoVar
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv VarEnv CoVar
subst CoVar
bndr CoVar
wild_bndr)
wild_bndr :: CoVar
wild_bndr = CoVar -> Name -> CoVar
setVarName CoVar
bndr (Name -> CoVar) -> Name -> CoVar
forall a b. (a -> b) -> a -> b
$
Name -> OccName -> Name
tidyNameOcc (CoVar -> Name
varName CoVar
bndr) (String -> OccName
mkTyVarOcc String
"_")
is_wildcard :: Var -> Bool
is_wildcard :: CoVar -> Bool
is_wildcard CoVar
tv = case OccName -> String
occNameString (CoVar -> OccName
forall a. NamedThing a => a -> OccName
getOccName CoVar
tv) of
(Char
'_' : String
rest) -> (Char -> Bool) -> String -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
rest
String
_ -> Bool
False
decomposeCo :: Arity -> Coercion
-> [Role]
-> [Coercion]
decomposeCo :: Int -> Coercion -> [Role] -> [Coercion]
decomposeCo Int
arity Coercion
co [Role]
rs
= [HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
n Coercion
co | (Int
n,Role
r) <- [Int
0..(Int
arityInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)] [Int] -> [Role] -> [(Int, Role)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` [Role]
rs ]
decomposeFunCo :: HasDebugCallStack
=> Role
-> Coercion
-> (CoercionN, Coercion, Coercion)
decomposeFunCo :: Role -> Coercion -> (Coercion, Coercion, Coercion)
decomposeFunCo Role
r Coercion
co = ASSERT2( all_ok, ppr co )
(HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
0 Coercion
co, HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
3 Coercion
co, HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
4 Coercion
co)
where
Pair Type
s1t1 Type
s2t2 = Coercion -> Pair Type
coercionKind Coercion
co
all_ok :: Bool
all_ok = Type -> Bool
isFunTy Type
s1t1 Bool -> Bool -> Bool
&& Type -> Bool
isFunTy Type
s2t2
decomposePiCos :: HasDebugCallStack
=> CoercionN -> Pair Type
-> [Type]
-> ([CoercionN], CoercionN)
decomposePiCos :: Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
decomposePiCos Coercion
orig_co (Pair Type
orig_k1 Type
orig_k2) [Type]
orig_args
= [Coercion]
-> (TCvSubst, Type)
-> Coercion
-> (TCvSubst, Type)
-> [Type]
-> ([Coercion], Coercion)
go [] (TCvSubst
orig_subst,Type
orig_k1) Coercion
orig_co (TCvSubst
orig_subst,Type
orig_k2) [Type]
orig_args
where
orig_subst :: TCvSubst
orig_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
[Type] -> VarSet
tyCoVarsOfTypes [Type]
orig_args VarSet -> VarSet -> VarSet
`unionVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
orig_co
go :: [CoercionN]
-> (TCvSubst,Kind)
-> CoercionN
-> (TCvSubst,Kind)
-> [Type]
-> ([CoercionN], Coercion)
go :: [Coercion]
-> (TCvSubst, Type)
-> Coercion
-> (TCvSubst, Type)
-> [Type]
-> ([Coercion], Coercion)
go [Coercion]
acc_arg_cos (TCvSubst
subst1,Type
k1) Coercion
co (TCvSubst
subst2,Type
k2) (Type
ty:[Type]
tys)
| Just (CoVar
a, Type
t1) <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
k1
, Just (CoVar
b, Type
t2) <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
k2
= let arg_co :: Coercion
arg_co = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
0 (Coercion -> Coercion
mkSymCo Coercion
co)
res_co :: Coercion
res_co = Coercion -> Coercion -> Coercion
mkInstCo Coercion
co (Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
Nominal Type
ty Coercion
arg_co)
subst1' :: TCvSubst
subst1' = TCvSubst -> CoVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst1 CoVar
a (Type
ty Type -> Coercion -> Type
`CastTy` Coercion
arg_co)
subst2' :: TCvSubst
subst2' = TCvSubst -> CoVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst2 CoVar
b Type
ty
in
[Coercion]
-> (TCvSubst, Type)
-> Coercion
-> (TCvSubst, Type)
-> [Type]
-> ([Coercion], Coercion)
go (Coercion
arg_co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
acc_arg_cos) (TCvSubst
subst1', Type
t1) Coercion
res_co (TCvSubst
subst2', Type
t2) [Type]
tys
| Just (Type
_w1, Type
_s1, Type
t1) <- Type -> Maybe (Type, Type, Type)
splitFunTy_maybe Type
k1
, Just (Type
_w1, Type
_s2, Type
t2) <- Type -> Maybe (Type, Type, Type)
splitFunTy_maybe Type
k2
= let (Coercion
_, Coercion
sym_arg_co, Coercion
res_co) = HasDebugCallStack =>
Role -> Coercion -> (Coercion, Coercion, Coercion)
Role -> Coercion -> (Coercion, Coercion, Coercion)
decomposeFunCo Role
Nominal Coercion
co
arg_co :: Coercion
arg_co = Coercion -> Coercion
mkSymCo Coercion
sym_arg_co
in
[Coercion]
-> (TCvSubst, Type)
-> Coercion
-> (TCvSubst, Type)
-> [Type]
-> ([Coercion], Coercion)
go (Coercion
arg_co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
acc_arg_cos) (TCvSubst
subst1,Type
t1) Coercion
res_co (TCvSubst
subst2,Type
t2) [Type]
tys
| Bool -> Bool
not (TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst1) Bool -> Bool -> Bool
|| Bool -> Bool
not (TCvSubst -> Bool
isEmptyTCvSubst TCvSubst
subst2)
= [Coercion]
-> (TCvSubst, Type)
-> Coercion
-> (TCvSubst, Type)
-> [Type]
-> ([Coercion], Coercion)
go [Coercion]
acc_arg_cos (TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst1, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst1 Type
k1)
Coercion
co
(TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst2, HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst1 Type
k2)
(Type
tyType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
tys)
go [Coercion]
acc_arg_cos (TCvSubst, Type)
_ki1 Coercion
co (TCvSubst, Type)
_ki2 [Type]
_tys = ([Coercion] -> [Coercion]
forall a. [a] -> [a]
reverse [Coercion]
acc_arg_cos, Coercion
co)
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe (CoVarCo CoVar
cv) = CoVar -> Maybe CoVar
forall a. a -> Maybe a
Just CoVar
cv
getCoVar_maybe Coercion
_ = Maybe CoVar
forall a. Maybe a
Nothing
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
splitTyConAppCo_maybe Coercion
co
| Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
= do { (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
; let args :: [Coercion]
args = (Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo (Role -> TyCon -> [Role]
tyConRolesX Role
r TyCon
tc) [Type]
tys
; (TyCon, [Coercion]) -> Maybe (TyCon, [Coercion])
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon
tc, [Coercion]
args) }
splitTyConAppCo_maybe (TyConAppCo Role
_ TyCon
tc [Coercion]
cos) = (TyCon, [Coercion]) -> Maybe (TyCon, [Coercion])
forall a. a -> Maybe a
Just (TyCon
tc, [Coercion]
cos)
splitTyConAppCo_maybe (FunCo Role
_ Coercion
w Coercion
arg Coercion
res) = (TyCon, [Coercion]) -> Maybe (TyCon, [Coercion])
forall a. a -> Maybe a
Just (TyCon
funTyCon, [Coercion]
cos)
where cos :: [Coercion]
cos = [Coercion
w, HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkRuntimeRepCo Coercion
arg, HasDebugCallStack => Coercion -> Coercion
Coercion -> Coercion
mkRuntimeRepCo Coercion
res, Coercion
arg, Coercion
res]
splitTyConAppCo_maybe Coercion
_ = Maybe (TyCon, [Coercion])
forall a. Maybe a
Nothing
multToCo :: Mult -> Coercion
multToCo :: Type -> Coercion
multToCo Type
r = Type -> Coercion
mkNomReflCo Type
r
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe (AppCo Coercion
co Coercion
arg) = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Coercion
co, Coercion
arg)
splitAppCo_maybe (TyConAppCo Role
r TyCon
tc [Coercion]
args)
| [Coercion]
args [Coercion] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` TyCon -> Int
tyConArity TyCon
tc
, Just ([Coercion]
args', Coercion
arg') <- [Coercion] -> Maybe ([Coercion], Coercion)
forall a. [a] -> Maybe ([a], a)
snocView [Coercion]
args
= (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just ( HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
args', Coercion
arg' )
| Bool -> Bool
not (TyCon -> Bool
mustBeSaturated TyCon
tc)
, Just ([Coercion]
args', Coercion
arg') <- [Coercion] -> Maybe ([Coercion], Coercion)
forall a. [a] -> Maybe ([a], a)
snocView [Coercion]
args
, Just Coercion
arg'' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Role -> TyCon -> Int -> Role
nthRole Role
r TyCon
tc ([Coercion] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Coercion]
args')) Coercion
arg'
= (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just ( HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
args', Coercion
arg'' )
splitAppCo_maybe Coercion
co
| Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Just (Type
ty1, Type
ty2) <- Type -> Maybe (Type, Type)
splitAppTy_maybe Type
ty
= (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo Role
r Type
ty1, Type -> Coercion
mkNomReflCo Type
ty2)
splitAppCo_maybe Coercion
_ = Maybe (Coercion, Coercion)
forall a. Maybe a
Nothing
splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe (FunCo Role
_ Coercion
_ Coercion
arg Coercion
res) = (Coercion, Coercion) -> Maybe (Coercion, Coercion)
forall a. a -> Maybe a
Just (Coercion
arg, Coercion
res)
splitFunCo_maybe Coercion
_ = Maybe (Coercion, Coercion)
forall a. Maybe a
Nothing
splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
splitForAllCo_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_maybe (ForAllCo CoVar
tv Coercion
k_co Coercion
co) = (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
tv, Coercion
k_co, Coercion
co)
splitForAllCo_maybe Coercion
_ = Maybe (CoVar, Coercion, Coercion)
forall a. Maybe a
Nothing
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
splitForAllCo_ty_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_ty_maybe (ForAllCo CoVar
tv Coercion
k_co Coercion
co)
| CoVar -> Bool
isTyVar CoVar
tv = (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
tv, Coercion
k_co, Coercion
co)
splitForAllCo_ty_maybe Coercion
_ = Maybe (CoVar, Coercion, Coercion)
forall a. Maybe a
Nothing
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe (ForAllCo CoVar
cv Coercion
k_co Coercion
co)
| CoVar -> Bool
isCoVar CoVar
cv = (CoVar, Coercion, Coercion) -> Maybe (CoVar, Coercion, Coercion)
forall a. a -> Maybe a
Just (CoVar
cv, Coercion
k_co, Coercion
co)
splitForAllCo_co_maybe Coercion
_ = Maybe (CoVar, Coercion, Coercion)
forall a. Maybe a
Nothing
coVarLType, coVarRType :: HasDebugCallStack => CoVar -> Type
coVarLType :: CoVar -> Type
coVarLType CoVar
cv | (Type
_, Type
_, Type
ty1, Type
_, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv = Type
ty1
coVarRType :: CoVar -> Type
coVarRType CoVar
cv | (Type
_, Type
_, Type
_, Type
ty2, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv = Type
ty2
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes :: CoVar -> Pair Type
coVarTypes CoVar
cv
| (Type
_, Type
_, Type
ty1, Type
ty2, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv
= Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair Type
ty1 Type
ty2
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
coVarKindsTypesRole :: CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv
| Just (TyCon
tc, [Type
k1,Type
k2,Type
ty1,Type
ty2]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe (CoVar -> Type
varType CoVar
cv)
= (Type
k1, Type
k2, Type
ty1, Type
ty2, TyCon -> Role
eqTyConRole TyCon
tc)
| Bool
otherwise
= String -> SDoc -> (Type, Type, Type, Type, Role)
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coVarKindsTypesRole, non coercion variable"
(CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv SDoc -> SDoc -> SDoc
$$ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (CoVar -> Type
varType CoVar
cv))
coVarKind :: CoVar -> Type
coVarKind :: CoVar -> Type
coVarKind CoVar
cv
= ASSERT( isCoVar cv )
CoVar -> Type
varType CoVar
cv
coVarRole :: CoVar -> Role
coVarRole :: CoVar -> Role
coVarRole CoVar
cv
= TyCon -> Role
eqTyConRole (case Type -> Maybe TyCon
tyConAppTyCon_maybe (CoVar -> Type
varType CoVar
cv) of
Just TyCon
tc0 -> TyCon
tc0
Maybe TyCon
Nothing -> String -> SDoc -> TyCon
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coVarRole: not tyconapp" (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
cv))
eqTyConRole :: TyCon -> Role
eqTyConRole :: TyCon -> Role
eqTyConRole TyCon
tc
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey
= Role
Nominal
| TyCon
tc TyCon -> Unique -> Bool
forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
= Role
Representational
| Bool
otherwise
= String -> SDoc -> Role
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"eqTyConRole: unknown tycon" (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
tc)
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo :: Coercion -> Coercion
mkRuntimeRepCo Coercion
co
= HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
0 Coercion
kind_co
where
kind_co :: Coercion
kind_co = Coercion -> Coercion
mkKindCo Coercion
co
isReflCoVar_maybe :: Var -> Maybe Coercion
isReflCoVar_maybe :: CoVar -> Maybe Coercion
isReflCoVar_maybe CoVar
cv
| CoVar -> Bool
isCoVar CoVar
cv
, Pair Type
ty1 Type
ty2 <- HasDebugCallStack => CoVar -> Pair Type
CoVar -> Pair Type
coVarTypes CoVar
cv
, Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2
= Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo (CoVar -> Role
coVarRole CoVar
cv) Type
ty1)
| Bool
otherwise
= Maybe Coercion
forall a. Maybe a
Nothing
isGReflCo :: Coercion -> Bool
isGReflCo :: Coercion -> Bool
isGReflCo (GRefl{}) = Bool
True
isGReflCo (Refl{}) = Bool
True
isGReflCo Coercion
_ = Bool
False
isGReflMCo :: MCoercion -> Bool
isGReflMCo :: MCoercion -> Bool
isGReflMCo MCoercion
MRefl = Bool
True
isGReflMCo (MCo Coercion
co) | Coercion -> Bool
isGReflCo Coercion
co = Bool
True
isGReflMCo MCoercion
_ = Bool
False
isReflCo :: Coercion -> Bool
isReflCo :: Coercion -> Bool
isReflCo (Refl{}) = Bool
True
isReflCo (GRefl Role
_ Type
_ MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = Bool
True
isReflCo Coercion
_ = Bool
False
isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
isGReflCo_maybe (GRefl Role
r Type
ty MCoercion
_) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
r)
isGReflCo_maybe (Refl Type
ty) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isGReflCo_maybe Coercion
_ = Maybe (Type, Role)
forall a. Maybe a
Nothing
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl Type
ty) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isReflCo_maybe (GRefl Role
r Type
ty MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
r)
isReflCo_maybe Coercion
_ = Maybe (Type, Role)
forall a. Maybe a
Nothing
isReflexiveCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = Maybe (Type, Role) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Type, Role) -> Bool)
-> (Coercion -> Maybe (Type, Role)) -> Coercion -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl Type
ty) = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isReflexiveCo_maybe (GRefl Role
r Type
ty MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty, Role
r)
isReflexiveCo_maybe Coercion
co
| Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2
= (Type, Role) -> Maybe (Type, Role)
forall a. a -> Maybe a
Just (Type
ty1, Role
r)
| Bool
otherwise
= Maybe (Type, Role)
forall a. Maybe a
Nothing
where (Pair Type
ty1 Type
ty2, Role
r) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
coToMCo :: Coercion -> MCoercion
coToMCo :: Coercion -> MCoercion
coToMCo Coercion
c = if Coercion -> Bool
isReflCo Coercion
c
then MCoercion
MRefl
else Coercion -> MCoercion
MCo Coercion
c
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflCo :: Role -> Type -> MCoercion -> Coercion
mkGReflCo Role
r Type
ty MCoercion
mco
| MCoercion -> Bool
isGReflMCo MCoercion
mco = if Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal then Type -> Coercion
Refl Type
ty
else Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty MCoercion
MRefl
| Bool
otherwise = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty MCoercion
mco
mkReflCo :: Role -> Type -> Coercion
mkReflCo :: Role -> Type -> Coercion
mkReflCo Role
Nominal Type
ty = Type -> Coercion
Refl Type
ty
mkReflCo Role
r Type
ty = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty MCoercion
MRefl
mkRepReflCo :: Type -> Coercion
mkRepReflCo :: Type -> Coercion
mkRepReflCo Type
ty = Role -> Type -> MCoercion -> Coercion
GRefl Role
Representational Type
ty MCoercion
MRefl
mkNomReflCo :: Type -> Coercion
mkNomReflCo :: Type -> Coercion
mkNomReflCo = Type -> Coercion
Refl
mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc [Coercion]
cos
| [Coercion
w, Coercion
_rep1, Coercion
_rep2, Coercion
co1, Coercion
co2] <- [Coercion]
cos
, TyCon -> Bool
isFunTyCon TyCon
tc
=
Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r Coercion
w Coercion
co1 Coercion
co2
| Just ([(CoVar, Coercion)]
tv_co_prs, Type
rhs_ty, [Coercion]
leftover_cos) <- TyCon
-> [Coercion] -> Maybe ([(CoVar, Coercion)], Type, [Coercion])
forall tyco.
TyCon -> [tyco] -> Maybe ([(CoVar, tyco)], Type, [tyco])
expandSynTyCon_maybe TyCon
tc [Coercion]
cos
= Coercion -> [Coercion] -> Coercion
mkAppCos (HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r ([(CoVar, Coercion)] -> LiftingContext
mkLiftingContext [(CoVar, Coercion)]
tv_co_prs) Type
rhs_ty) [Coercion]
leftover_cos
| Just [(Type, Role)]
tys_roles <- (Coercion -> Maybe (Type, Role))
-> [Coercion] -> Maybe [(Type, Role)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Coercion -> Maybe (Type, Role)
isReflCo_maybe [Coercion]
cos
= Role -> Type -> Coercion
mkReflCo Role
r (TyCon -> [Type] -> Type
mkTyConApp TyCon
tc (((Type, Role) -> Type) -> [(Type, Role)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Type, Role) -> Type
forall a b. (a, b) -> a
fst [(Type, Role)]
tys_roles))
| Bool
otherwise = Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
r TyCon
tc [Coercion]
cos
mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
mkFunCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r Coercion
w Coercion
co1 Coercion
co2
| Just (Type
ty1, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co1
, Just (Type
ty2, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co2
, Just (Type
w, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
w
= Role -> Type -> Coercion
mkReflCo Role
r (Type -> Type -> Type -> Type
mkVisFunTy Type
w Type
ty1 Type
ty2)
| Bool
otherwise = Role -> Coercion -> Coercion -> Coercion -> Coercion
FunCo Role
r Coercion
w Coercion
co1 Coercion
co2
mkAppCo :: Coercion
-> Coercion
-> Coercion
mkAppCo :: Coercion -> Coercion -> Coercion
mkAppCo Coercion
co Coercion
arg
| Just (Type
ty1, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Just (Type
ty2, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
arg
= Role -> Type -> Coercion
mkReflCo Role
r (Type -> Type -> Type
mkAppTy Type
ty1 Type
ty2)
| Just (Type
ty1, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
= HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc ([Role] -> [Type] -> [Coercion]
zip_roles (Role -> TyCon -> [Role]
tyConRolesX Role
r TyCon
tc) [Type]
tys)
where
zip_roles :: [Role] -> [Type] -> [Coercion]
zip_roles (Role
r1:[Role]
_) [] = [Role -> Role -> Coercion -> Coercion
downgradeRole Role
r1 Role
Nominal Coercion
arg]
zip_roles (Role
r1:[Role]
rs) (Type
ty1:[Type]
tys) = Role -> Type -> Coercion
mkReflCo Role
r1 Type
ty1 Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Role] -> [Type] -> [Coercion]
zip_roles [Role]
rs [Type]
tys
zip_roles [Role]
_ [Type]
_ = String -> [Coercion]
forall a. String -> a
panic String
"zip_roles"
mkAppCo (TyConAppCo Role
r TyCon
tc [Coercion]
args) Coercion
arg
= case Role
r of
Role
Nominal -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc ([Coercion]
args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion
arg])
Role
Representational -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Representational TyCon
tc ([Coercion]
args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion
arg'])
where new_role :: Role
new_role = (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc) [Role] -> Int -> Role
forall a. [a] -> Int -> a
!! ([Coercion] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Coercion]
args)
arg' :: Coercion
arg' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
new_role Role
Nominal Coercion
arg
Role
Phantom -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Phantom TyCon
tc ([Coercion]
args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
++ [Coercion -> Coercion
toPhantomCo Coercion
arg])
mkAppCo Coercion
co Coercion
arg = Coercion -> Coercion -> Coercion
AppCo Coercion
co Coercion
arg
mkAppCos :: Coercion
-> [Coercion]
-> Coercion
mkAppCos :: Coercion -> [Coercion] -> Coercion
mkAppCos Coercion
co1 [Coercion]
cos = (Coercion -> Coercion -> Coercion)
-> Coercion -> [Coercion] -> Coercion
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' Coercion -> Coercion -> Coercion
mkAppCo Coercion
co1 [Coercion]
cos
mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
mkForAllCo :: CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
v Coercion
kind_co Coercion
co
| ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
, ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
, Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Coercion -> Bool
isGReflCo Coercion
kind_co
= Role -> Type -> Coercion
mkReflCo Role
r (CoVar -> Type -> Type
mkTyCoInvForAllTy CoVar
v Type
ty)
| Bool
otherwise
= CoVar -> Coercion -> Coercion -> Coercion
ForAllCo CoVar
v Coercion
kind_co Coercion
co
mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
mkForAllCo_NoRefl :: CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl CoVar
v Coercion
kind_co Coercion
co
| ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
, ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
, ASSERT( not (isReflCo co)) True
, CoVar -> Bool
isCoVar CoVar
v
, Bool -> Bool
not (CoVar
v CoVar -> VarSet -> Bool
`elemVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
= Role -> Coercion -> Coercion -> Coercion -> Coercion
FunCo (Coercion -> Role
coercionRole Coercion
co) (Type -> Coercion
multToCo Type
Many) Coercion
kind_co Coercion
co
| Bool
otherwise
= CoVar -> Coercion -> Coercion -> Coercion
ForAllCo CoVar
v Coercion
kind_co Coercion
co
mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
mkForAllCos :: [(CoVar, Coercion)] -> Coercion -> Coercion
mkForAllCos [(CoVar, Coercion)]
bndrs Coercion
co
| Just (Type
ty, Role
r ) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
= let ([(CoVar, Coercion)]
refls_rev'd, [(CoVar, Coercion)]
non_refls_rev'd) = ((CoVar, Coercion) -> Bool)
-> [(CoVar, Coercion)]
-> ([(CoVar, Coercion)], [(CoVar, Coercion)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Coercion -> Bool
isReflCo (Coercion -> Bool)
-> ((CoVar, Coercion) -> Coercion) -> (CoVar, Coercion) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CoVar, Coercion) -> Coercion
forall a b. (a, b) -> b
snd) ([(CoVar, Coercion)] -> [(CoVar, Coercion)]
forall a. [a] -> [a]
reverse [(CoVar, Coercion)]
bndrs) in
(Coercion -> (CoVar, Coercion) -> Coercion)
-> Coercion -> [(CoVar, Coercion)] -> Coercion
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (((CoVar, Coercion) -> Coercion -> Coercion)
-> Coercion -> (CoVar, Coercion) -> Coercion
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((CoVar, Coercion) -> Coercion -> Coercion)
-> Coercion -> (CoVar, Coercion) -> Coercion)
-> ((CoVar, Coercion) -> Coercion -> Coercion)
-> Coercion
-> (CoVar, Coercion)
-> Coercion
forall a b. (a -> b) -> a -> b
$ (CoVar -> Coercion -> Coercion -> Coercion)
-> (CoVar, Coercion) -> Coercion -> Coercion
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl)
(Role -> Type -> Coercion
mkReflCo Role
r ([CoVar] -> Type -> Type
mkTyCoInvForAllTys ([CoVar] -> [CoVar]
forall a. [a] -> [a]
reverse (((CoVar, Coercion) -> CoVar) -> [(CoVar, Coercion)] -> [CoVar]
forall a b. (a -> b) -> [a] -> [b]
map (CoVar, Coercion) -> CoVar
forall a b. (a, b) -> a
fst [(CoVar, Coercion)]
refls_rev'd)) Type
ty))
[(CoVar, Coercion)]
non_refls_rev'd
| Bool
otherwise
= ((CoVar, Coercion) -> Coercion -> Coercion)
-> Coercion -> [(CoVar, Coercion)] -> Coercion
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((CoVar -> Coercion -> Coercion -> Coercion)
-> (CoVar, Coercion) -> Coercion -> Coercion
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl) Coercion
co [(CoVar, Coercion)]
bndrs
mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
mkHomoForAllCos :: [CoVar] -> Coercion -> Coercion
mkHomoForAllCos [CoVar]
vs Coercion
co
| Just (Type
ty, Role
r) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
= Role -> Type -> Coercion
mkReflCo Role
r ([CoVar] -> Type -> Type
mkTyCoInvForAllTys [CoVar]
vs Type
ty)
| Bool
otherwise
= [CoVar] -> Coercion -> Coercion
mkHomoForAllCos_NoRefl [CoVar]
vs Coercion
co
mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
mkHomoForAllCos_NoRefl :: [CoVar] -> Coercion -> Coercion
mkHomoForAllCos_NoRefl [CoVar]
vs Coercion
orig_co
= ASSERT( not (isReflCo orig_co))
(CoVar -> Coercion -> Coercion) -> Coercion -> [CoVar] -> Coercion
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr CoVar -> Coercion -> Coercion
go Coercion
orig_co [CoVar]
vs
where
go :: CoVar -> Coercion -> Coercion
go CoVar
v Coercion
co = CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo_NoRefl CoVar
v (Type -> Coercion
mkNomReflCo (CoVar -> Type
varType CoVar
v)) Coercion
co
mkCoVarCo :: CoVar -> Coercion
mkCoVarCo :: CoVar -> Coercion
mkCoVarCo CoVar
cv = CoVar -> Coercion
CoVarCo CoVar
cv
mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos = (CoVar -> Coercion) -> [CoVar] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map CoVar -> Coercion
mkCoVarCo
isCoVar_maybe :: Coercion -> Maybe CoVar
isCoVar_maybe :: Coercion -> Maybe CoVar
isCoVar_maybe (CoVarCo CoVar
cv) = CoVar -> Maybe CoVar
forall a. a -> Maybe a
Just CoVar
cv
isCoVar_maybe Coercion
_ = Maybe CoVar
forall a. Maybe a
Nothing
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
-> Coercion
mkAxInstCo :: Role -> CoAxiom br -> Int -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role CoAxiom br
ax Int
index [Type]
tys [Coercion]
cos
| Int
arity Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n_tys = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
ax_role (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
CoAxiom Branched -> Int -> [Coercion] -> Coercion
mkAxiomInstCo CoAxiom Branched
ax_br Int
index ([Coercion]
rtys [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
`chkAppend` [Coercion]
cos)
| Bool
otherwise = ASSERT( arity < n_tys )
Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
ax_role (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
Coercion -> [Coercion] -> Coercion
mkAppCos (CoAxiom Branched -> Int -> [Coercion] -> Coercion
mkAxiomInstCo CoAxiom Branched
ax_br Int
index
([Coercion]
ax_args [Coercion] -> [Coercion] -> [Coercion]
forall a. [a] -> [a] -> [a]
`chkAppend` [Coercion]
cos))
[Coercion]
leftover_args
where
n_tys :: Int
n_tys = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys
ax_br :: CoAxiom Branched
ax_br = CoAxiom br -> CoAxiom Branched
forall (br :: BranchFlag). CoAxiom br -> CoAxiom Branched
toBranchedAxiom CoAxiom br
ax
branch :: CoAxBranch
branch = CoAxiom Branched -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom Branched
ax_br Int
index
tvs :: [CoVar]
tvs = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch
arity :: Int
arity = [CoVar] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [CoVar]
tvs
arg_roles :: [Role]
arg_roles = CoAxBranch -> [Role]
coAxBranchRoles CoAxBranch
branch
rtys :: [Coercion]
rtys = (Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo ([Role]
arg_roles [Role] -> [Role] -> [Role]
forall a. [a] -> [a] -> [a]
++ Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal) [Type]
tys
([Coercion]
ax_args, [Coercion]
leftover_args)
= Int -> [Coercion] -> ([Coercion], [Coercion])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
arity [Coercion]
rtys
ax_role :: Role
ax_role = CoAxiom br -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole CoAxiom br
ax
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkAxiomInstCo :: CoAxiom Branched -> Int -> [Coercion] -> Coercion
mkAxiomInstCo CoAxiom Branched
ax Int
index [Coercion]
args
= ASSERT( args `lengthIs` coAxiomArity ax index )
CoAxiom Branched -> Int -> [Coercion] -> Coercion
AxiomInstCo CoAxiom Branched
ax Int
index [Coercion]
args
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
-> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
role CoAxiom Unbranched
ax [Type]
tys [Coercion]
cos
= Role
-> CoAxiom Unbranched -> Int -> [Type] -> [Coercion] -> Coercion
forall (br :: BranchFlag).
Role -> CoAxiom br -> Int -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role CoAxiom Unbranched
ax Int
0 [Type]
tys [Coercion]
cos
mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstRHS :: CoAxiom br -> Int -> [Type] -> [Coercion] -> Type
mkAxInstRHS CoAxiom br
ax Int
index [Type]
tys [Coercion]
cos
= ASSERT( tvs `equalLength` tys1 )
Type -> [Type] -> Type
mkAppTys Type
rhs' [Type]
tys2
where
branch :: CoAxBranch
branch = CoAxiom br -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
index
tvs :: [CoVar]
tvs = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch
cvs :: [CoVar]
cvs = CoAxBranch -> [CoVar]
coAxBranchCoVars CoAxBranch
branch
([Type]
tys1, [Type]
tys2) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
rhs' :: Type
rhs' = HasCallStack => [CoVar] -> [Type] -> Type -> Type
[CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
CoAxBranch -> Type
coAxBranchRHS CoAxBranch
branch
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS CoAxiom Unbranched
ax = CoAxiom Unbranched -> Int -> [Type] -> [Coercion] -> Type
forall (br :: BranchFlag).
CoAxiom br -> Int -> [Type] -> [Coercion] -> Type
mkAxInstRHS CoAxiom Unbranched
ax Int
0
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstLHS :: CoAxiom br -> Int -> [Type] -> [Coercion] -> Type
mkAxInstLHS CoAxiom br
ax Int
index [Type]
tys [Coercion]
cos
= ASSERT( tvs `equalLength` tys1 )
TyCon -> [Type] -> Type
mkTyConApp TyCon
fam_tc ([Type]
lhs_tys [Type] -> [Type] -> [Type]
forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
tys2)
where
branch :: CoAxBranch
branch = CoAxiom br -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
index
tvs :: [CoVar]
tvs = CoAxBranch -> [CoVar]
coAxBranchTyVars CoAxBranch
branch
cvs :: [CoVar]
cvs = CoAxBranch -> [CoVar]
coAxBranchCoVars CoAxBranch
branch
([Type]
tys1, [Type]
tys2) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
lhs_tys :: [Type]
lhs_tys = [CoVar] -> [Type] -> [Type] -> [Type]
substTysWith [CoVar]
tvs [Type]
tys1 ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars [CoVar]
cvs [Coercion]
cos ([Type] -> [Type]) -> [Type] -> [Type]
forall a b. (a -> b) -> a -> b
$
CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch
fam_tc :: TyCon
fam_tc = CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS CoAxiom Unbranched
ax = CoAxiom Unbranched -> Int -> [Type] -> [Coercion] -> Type
forall (br :: BranchFlag).
CoAxiom br -> Int -> [Type] -> [Coercion] -> Type
mkAxInstLHS CoAxiom Unbranched
ax Int
0
mkHoleCo :: CoercionHole -> Coercion
mkHoleCo :: CoercionHole -> Coercion
mkHoleCo CoercionHole
h = CoercionHole -> Coercion
HoleCo CoercionHole
h
mkUnivCo :: UnivCoProvenance
-> Role
-> Type
-> Type
-> Coercion
mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo UnivCoProvenance
prov Role
role Type
ty1 Type
ty2
| Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2 = Role -> Type -> Coercion
mkReflCo Role
role Type
ty1
| Bool
otherwise = UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo UnivCoProvenance
prov Role
role Type
ty1 Type
ty2
mkSymCo :: Coercion -> Coercion
mkSymCo :: Coercion -> Coercion
mkSymCo Coercion
co | Coercion -> Bool
isReflCo Coercion
co = Coercion
co
mkSymCo (SymCo Coercion
co) = Coercion
co
mkSymCo (SubCo (SymCo Coercion
co)) = Coercion -> Coercion
SubCo Coercion
co
mkSymCo Coercion
co = Coercion -> Coercion
SymCo Coercion
co
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2 | Coercion -> Bool
isReflCo Coercion
co1 = Coercion
co2
| Coercion -> Bool
isReflCo Coercion
co2 = Coercion
co1
mkTransCo (GRefl Role
r Type
t1 (MCo Coercion
co1)) (GRefl Role
_ Type
_ (MCo Coercion
co2))
= Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
t1 (Coercion -> MCoercion
MCo (Coercion -> MCoercion) -> Coercion -> MCoercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)
mkTransCo Coercion
co1 Coercion
co2 = Coercion -> Coercion -> Coercion
TransCo Coercion
co1 Coercion
co2
mkTransMCo :: MCoercion -> MCoercion -> MCoercion
mkTransMCo :: MCoercion -> MCoercion -> MCoercion
mkTransMCo MCoercion
MRefl MCoercion
co2 = MCoercion
co2
mkTransMCo MCoercion
co1 MCoercion
MRefl = MCoercion
co1
mkTransMCo (MCo Coercion
co1) (MCo Coercion
co2) = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)
mkNthCo :: HasDebugCallStack
=> Role
-> Int
-> Coercion
-> Coercion
mkNthCo :: Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
n Coercion
co
= ASSERT2( good_call, bad_call_msg )
Role -> Int -> Coercion -> Coercion
go Role
r Int
n Coercion
co
where
Pair Type
ty1 Type
ty2 = Coercion -> Pair Type
coercionKind Coercion
co
go :: Role -> Int -> Coercion -> Coercion
go Role
r Int
0 Coercion
co
| Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Just (CoVar
tv, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
ty
=
ASSERT( r == Nominal )
Type -> Coercion
mkNomReflCo (CoVar -> Type
varType CoVar
tv)
go Role
r Int
n Coercion
co
| Just (Type
ty, Role
r0) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, let tc :: TyCon
tc = Type -> TyCon
tyConAppTyCon Type
ty
= ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
ASSERT( nthRole r0 tc n == r )
Role -> Type -> Coercion
mkReflCo Role
r (Int -> Type -> Type
tyConAppArgN Int
n Type
ty)
where ok_tc_app :: Type -> Int -> Bool
ok_tc_app :: Type -> Int -> Bool
ok_tc_app Type
ty Int
n
| Just (TyCon
_, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
= [Type]
tys [Type] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
n
| Type -> Bool
isForAllTy Type
ty
= Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
| Bool
otherwise
= Bool
False
go Role
r Int
0 (ForAllCo CoVar
_ Coercion
kind_co Coercion
_)
= ASSERT( r == Nominal )
Coercion
kind_co
go Role
r Int
n co :: Coercion
co@(FunCo Role
r0 Coercion
w Coercion
arg Coercion
res)
= case Int
n of
Int
0 -> ASSERT( r == Nominal ) w
Int
1 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
Int
2 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
Int
3 -> ASSERT( r == r0 ) arg
Int
4 -> ASSERT( r == r0 ) res
Int
_ -> String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkNthCo(FunCo)" (Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
$$ Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
go Role
r Int
n (TyConAppCo Role
r0 TyCon
tc [Coercion]
arg_cos) = ASSERT2( r == nthRole r0 tc n
, (vcat [ ppr tc
, ppr arg_cos
, ppr r0
, ppr n
, ppr r ]) )
[Coercion]
arg_cos [Coercion] -> Int -> Coercion
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n
go Role
r Int
n Coercion
co =
Role -> Int -> Coercion -> Coercion
NthCo Role
r Int
n Coercion
co
bad_call_msg :: SDoc
bad_call_msg = [SDoc] -> SDoc
vcat [ String -> SDoc
text String
"Coercion =" SDoc -> SDoc -> SDoc
<+> Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co
, String -> SDoc
text String
"LHS ty =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1
, String -> SDoc
text String
"RHS ty =" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2
, String -> SDoc
text String
"n =" SDoc -> SDoc -> SDoc
<+> Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
n, String -> SDoc
text String
"r =" SDoc -> SDoc -> SDoc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr Role
r
, String -> SDoc
text String
"coercion role =" SDoc -> SDoc -> SDoc
<+> Role -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Coercion -> Role
coercionRole Coercion
co) ]
good_call :: Bool
good_call
| Just (CoVar
_tv1, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
ty1
, Just (CoVar
_tv2, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
ty2
= Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal
| Just (TyCon
tc1, [Type]
tys1) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
, Just (TyCon
tc2, [Type]
tys2) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2
, TyCon
tc1 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= let len1 :: Int
len1 = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys1
len2 :: Int
len2 = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys2
good_role :: Bool
good_role = case Coercion -> Role
coercionRole Coercion
co of
Role
Nominal -> Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal
Role
Representational -> Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc1 [Role] -> Int -> Role
forall a. [a] -> Int -> a
!! Int
n)
Role
Phantom -> Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Phantom
in Int
len1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
len2 Bool -> Bool -> Bool
&& Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
len1 Bool -> Bool -> Bool
&& Bool
good_role
| Bool
otherwise
= Bool
True
nthCoRole :: Int -> Coercion -> Role
nthCoRole :: Int -> Coercion -> Role
nthCoRole Int
n Coercion
co
| Just (TyCon
tc, [Type]
_) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
lty
= Role -> TyCon -> Int -> Role
nthRole Role
r TyCon
tc Int
n
| Just (CoVar, Type)
_ <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
lty
= Role
Nominal
| Bool
otherwise
= String -> SDoc -> Role
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"nthCoRole" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
where
lty :: Type
lty = Coercion -> Type
coercionLKind Coercion
co
r :: Role
r = Coercion -> Role
coercionRole Coercion
co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo LeftOrRight
lr Coercion
co
| Just (Type
ty, Role
eq) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
= Role -> Type -> Coercion
mkReflCo Role
eq (LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type -> (Type, Type)
splitAppTy Type
ty))
| Bool
otherwise
= LeftOrRight -> Coercion -> Coercion
LRCo LeftOrRight
lr Coercion
co
mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo (ForAllCo CoVar
tcv Coercion
_kind_co Coercion
body_co) Coercion
co
| Just (Type
arg, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
= TCvSubst -> Coercion -> Coercion
substCoUnchecked ([CoVar] -> [Type] -> TCvSubst
HasDebugCallStack => [CoVar] -> [Type] -> TCvSubst
zipTCvSubst [CoVar
tcv] [Type
arg]) Coercion
body_co
mkInstCo Coercion
co Coercion
arg = Coercion -> Coercion -> Coercion
InstCo Coercion
co Coercion
arg
mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
mkGReflRightCo :: Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
r Type
ty Coercion
co
| Coercion -> Bool
isGReflCo Coercion
co = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
| Bool
otherwise = Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
mkGReflLeftCo :: Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
r Type
ty Coercion
co
| Coercion -> Bool
isGReflCo Coercion
co = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
| Bool
otherwise = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceLeftCo :: Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
r Type
ty Coercion
co Coercion
co2
| Coercion -> Bool
isGReflCo Coercion
co = Coercion
co2
| Bool
otherwise = (Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co2
mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceRightCo :: Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty Coercion
co Coercion
co2
| Coercion -> Bool
isGReflCo Coercion
co = Coercion
co2
| Bool
otherwise = Coercion
co2 Coercion -> Coercion -> Coercion
`mkTransCo` Role -> Type -> MCoercion -> Coercion
GRefl Role
r Type
ty (Coercion -> MCoercion
MCo Coercion
co)
mkKindCo :: Coercion -> Coercion
mkKindCo :: Coercion -> Coercion
mkKindCo Coercion
co | Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co = Type -> Coercion
Refl (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty)
mkKindCo (GRefl Role
_ Type
_ (MCo Coercion
co)) = Coercion
co
mkKindCo (UnivCo (PhantomProv Coercion
h) Role
_ Type
_ Type
_) = Coercion
h
mkKindCo (UnivCo (ProofIrrelProv Coercion
h) Role
_ Type
_ Type
_) = Coercion
h
mkKindCo Coercion
co
| Pair Type
ty1 Type
ty2 <- Coercion -> Pair Type
coercionKind Coercion
co
, let tk1 :: Type
tk1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
tk2 :: Type
tk2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
, Type
tk1 Type -> Type -> Bool
`eqType` Type
tk2
= Type -> Coercion
Refl Type
tk1
| Bool
otherwise
= Coercion -> Coercion
KindCo Coercion
co
mkSubCo :: Coercion -> Coercion
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Type
ty) = Role -> Type -> MCoercion -> Coercion
GRefl Role
Representational Type
ty MCoercion
MRefl
mkSubCo (GRefl Role
Nominal Type
ty MCoercion
co) = Role -> Type -> MCoercion -> Coercion
GRefl Role
Representational Type
ty MCoercion
co
mkSubCo (TyConAppCo Role
Nominal TyCon
tc [Coercion]
cos)
= Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
Representational TyCon
tc (TyCon -> [Coercion] -> [Coercion]
applyRoles TyCon
tc [Coercion]
cos)
mkSubCo (FunCo Role
Nominal Coercion
w Coercion
arg Coercion
res)
= Role -> Coercion -> Coercion -> Coercion -> Coercion
FunCo Role
Representational Coercion
w
(Role -> Role -> Coercion -> Coercion
downgradeRole Role
Representational Role
Nominal Coercion
arg)
(Role -> Role -> Coercion -> Coercion
downgradeRole Role
Representational Role
Nominal Coercion
res)
mkSubCo Coercion
co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
Coercion -> Coercion
SubCo Coercion
co
downgradeRole_maybe :: Role
-> Role
-> Coercion -> Maybe Coercion
downgradeRole_maybe :: Role -> Role -> Coercion -> Maybe Coercion
downgradeRole_maybe Role
Nominal Role
Nominal Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Nominal Role
_ Coercion
_ = Maybe Coercion
forall a. Maybe a
Nothing
downgradeRole_maybe Role
Representational Role
Nominal Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Coercion
mkSubCo Coercion
co)
downgradeRole_maybe Role
Representational Role
Representational Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Representational Role
Phantom Coercion
_ = Maybe Coercion
forall a. Maybe a
Nothing
downgradeRole_maybe Role
Phantom Role
Phantom Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Phantom Role
_ Coercion
co = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Coercion
toPhantomCo Coercion
co)
downgradeRole :: Role
-> Role
-> Coercion -> Coercion
downgradeRole :: Role -> Role -> Coercion -> Coercion
downgradeRole Role
r1 Role
r2 Coercion
co
= case Role -> Role -> Coercion -> Maybe Coercion
downgradeRole_maybe Role
r1 Role
r2 Coercion
co of
Just Coercion
co' -> Coercion
co'
Maybe Coercion
Nothing -> String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"downgradeRole" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
co)
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo = CoAxiomRule -> [Coercion] -> Coercion
AxiomRuleCo
mkProofIrrelCo :: Role
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkProofIrrelCo :: Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
r Coercion
co Coercion
g Coercion
_ | Coercion -> Bool
isGReflCo Coercion
co = Role -> Type -> Coercion
mkReflCo Role
r (Coercion -> Type
mkCoercionTy Coercion
g)
mkProofIrrelCo Role
r Coercion
kco Coercion
g1 Coercion
g2 = UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (Coercion -> UnivCoProvenance
ProofIrrelProv Coercion
kco) Role
r
(Coercion -> Type
mkCoercionTy Coercion
g1) (Coercion -> Type
mkCoercionTy Coercion
g2)
setNominalRole_maybe :: Role
-> Coercion -> Maybe Coercion
setNominalRole_maybe :: Role -> Coercion -> Maybe Coercion
setNominalRole_maybe Role
r Coercion
co
| Role
r Role -> Role -> Bool
forall a. Eq a => a -> a -> Bool
== Role
Nominal = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
| Bool
otherwise = Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co
where
setNominalRole_maybe_helper :: Coercion -> Maybe Coercion
setNominalRole_maybe_helper (SubCo Coercion
co) = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
setNominalRole_maybe_helper co :: Coercion
co@(Refl Type
_) = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just Coercion
co
setNominalRole_maybe_helper (GRefl Role
_ Type
ty MCoercion
co) = Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> MCoercion -> Coercion
GRefl Role
Nominal Type
ty MCoercion
co
setNominalRole_maybe_helper (TyConAppCo Role
Representational TyCon
tc [Coercion]
cos)
= do { [Coercion]
cos' <- (Role -> Coercion -> Maybe Coercion)
-> [Role] -> [Coercion] -> Maybe [Coercion]
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Role -> TyCon -> [Role]
tyConRolesX Role
Representational TyCon
tc) [Coercion]
cos
; Coercion -> Maybe Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Role -> TyCon -> [Coercion] -> Coercion
TyConAppCo Role
Nominal TyCon
tc [Coercion]
cos' }
setNominalRole_maybe_helper (FunCo Role
Representational Coercion
w Coercion
co1 Coercion
co2)
= do { Coercion
co1' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe Role
Representational Coercion
co1
; Coercion
co2' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe Role
Representational Coercion
co2
; Coercion -> Maybe Coercion
forall (m :: * -> *) a. Monad m => a -> m a
return (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Coercion -> Coercion -> Coercion -> Coercion
FunCo Role
Nominal Coercion
w Coercion
co1' Coercion
co2'
}
setNominalRole_maybe_helper (SymCo Coercion
co)
= Coercion -> Coercion
SymCo (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co
setNominalRole_maybe_helper (TransCo Coercion
co1 Coercion
co2)
= Coercion -> Coercion -> Coercion
TransCo (Coercion -> Coercion -> Coercion)
-> Maybe Coercion -> Maybe (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co1 Maybe (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co2
setNominalRole_maybe_helper (AppCo Coercion
co1 Coercion
co2)
= Coercion -> Coercion -> Coercion
AppCo (Coercion -> Coercion -> Coercion)
-> Maybe Coercion -> Maybe (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co1 Maybe (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> Maybe Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
co2
setNominalRole_maybe_helper (ForAllCo CoVar
tv Coercion
kind_co Coercion
co)
= CoVar -> Coercion -> Coercion -> Coercion
ForAllCo CoVar
tv Coercion
kind_co (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co
setNominalRole_maybe_helper (NthCo Role
_r Int
n Coercion
co)
= Role -> Int -> Coercion -> Coercion
NthCo Role
Nominal Int
n (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Coercion -> Role
coercionRole Coercion
co) Coercion
co
setNominalRole_maybe_helper (InstCo Coercion
co Coercion
arg)
= Coercion -> Coercion -> Coercion
InstCo (Coercion -> Coercion -> Coercion)
-> Maybe Coercion -> Maybe (Coercion -> Coercion)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co Maybe (Coercion -> Coercion) -> Maybe Coercion -> Maybe Coercion
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Coercion -> Maybe Coercion
forall (f :: * -> *) a. Applicative f => a -> f a
pure Coercion
arg
setNominalRole_maybe_helper (UnivCo UnivCoProvenance
prov Role
_ Type
co1 Type
co2)
| case UnivCoProvenance
prov of PhantomProv Coercion
_ -> Bool
False
ProofIrrelProv Coercion
_ -> Bool
True
PluginProv String
_ -> Bool
False
= Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ UnivCoProvenance -> Role -> Type -> Type -> Coercion
UnivCo UnivCoProvenance
prov Role
Nominal Type
co1 Type
co2
setNominalRole_maybe_helper Coercion
_ = Maybe Coercion
forall a. Maybe a
Nothing
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo Coercion
h Type
t1 Type
t2
= UnivCoProvenance -> Role -> Type -> Type -> Coercion
mkUnivCo (Coercion -> UnivCoProvenance
PhantomProv Coercion
h) Role
Phantom Type
t1 Type
t2
toPhantomCo :: Coercion -> Coercion
toPhantomCo :: Coercion -> Coercion
toPhantomCo Coercion
co
= Coercion -> Type -> Type -> Coercion
mkPhantomCo (Coercion -> Coercion
mkKindCo Coercion
co) Type
ty1 Type
ty2
where Pair Type
ty1 Type
ty2 = Coercion -> Pair Type
coercionKind Coercion
co
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles TyCon
tc [Coercion]
cos
= (Role -> Coercion -> Coercion)
-> [Role] -> [Coercion] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Role
r -> Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal) (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc) [Coercion]
cos
tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX Role
Representational TyCon
tc = TyCon -> [Role]
tyConRolesRepresentational TyCon
tc
tyConRolesX Role
role TyCon
_ = Role -> [Role]
forall a. a -> [a]
repeat Role
role
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational TyCon
tc = TyCon -> [Role]
tyConRoles TyCon
tc [Role] -> [Role] -> [Role]
forall a. [a] -> [a] -> [a]
++ Role -> [Role]
forall a. a -> [a]
repeat Role
Nominal
nthRole :: Role -> TyCon -> Int -> Role
nthRole :: Role -> TyCon -> Int -> Role
nthRole Role
Nominal TyCon
_ Int
_ = Role
Nominal
nthRole Role
Phantom TyCon
_ Int
_ = Role
Phantom
nthRole Role
Representational TyCon
tc Int
n
= (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc) [Role] -> Int -> Role
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n
ltRole :: Role -> Role -> Bool
ltRole :: Role -> Role -> Bool
ltRole Role
Phantom Role
_ = Bool
False
ltRole Role
Representational Role
Phantom = Bool
True
ltRole Role
Representational Role
_ = Bool
False
ltRole Role
Nominal Role
Nominal = Bool
False
ltRole Role
Nominal Role
_ = Bool
True
promoteCoercion :: Coercion -> CoercionN
promoteCoercion :: Coercion -> Coercion
promoteCoercion Coercion
co = case Coercion
co of
Coercion
_ | Type
ki1 Type -> Type -> Bool
`eqType` Type
ki2
-> Type -> Coercion
mkNomReflCo (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1)
Refl Type
_ -> ASSERT( False )
Type -> Coercion
mkNomReflCo Type
ki1
GRefl Role
_ Type
_ MCoercion
MRefl -> ASSERT( False )
Type -> Coercion
mkNomReflCo Type
ki1
GRefl Role
_ Type
_ (MCo Coercion
co) -> Coercion
co
TyConAppCo Role
_ TyCon
tc [Coercion]
args
| Just Coercion
co' <- Coercion -> [Coercion] -> Maybe Coercion
instCoercions (Type -> Coercion
mkNomReflCo (TyCon -> Type
tyConKind TyCon
tc)) [Coercion]
args
-> Coercion
co'
| Bool
otherwise
-> Coercion -> Coercion
mkKindCo Coercion
co
AppCo Coercion
co1 Coercion
arg
| Just Coercion
co' <- Pair Type -> Coercion -> Coercion -> Maybe Coercion
instCoercion (Coercion -> Pair Type
coercionKind (Coercion -> Coercion
mkKindCo Coercion
co1))
(Coercion -> Coercion
promoteCoercion Coercion
co1) Coercion
arg
-> Coercion
co'
| Bool
otherwise
-> Coercion -> Coercion
mkKindCo Coercion
co
ForAllCo CoVar
tv Coercion
_ Coercion
g
| CoVar -> Bool
isTyVar CoVar
tv
-> Coercion -> Coercion
promoteCoercion Coercion
g
ForAllCo CoVar
_ Coercion
_ Coercion
_
-> ASSERT( False )
Type -> Coercion
mkNomReflCo Type
liftedTypeKind
FunCo Role
_ Coercion
_ Coercion
_ Coercion
_
-> ASSERT( False )
Type -> Coercion
mkNomReflCo Type
liftedTypeKind
CoVarCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
HoleCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
AxiomInstCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
AxiomRuleCo {} -> Coercion -> Coercion
mkKindCo Coercion
co
UnivCo (PhantomProv Coercion
kco) Role
_ Type
_ Type
_ -> Coercion
kco
UnivCo (ProofIrrelProv Coercion
kco) Role
_ Type
_ Type
_ -> Coercion
kco
UnivCo (PluginProv String
_) Role
_ Type
_ Type
_ -> Coercion -> Coercion
mkKindCo Coercion
co
SymCo Coercion
g
-> Coercion -> Coercion
mkSymCo (Coercion -> Coercion
promoteCoercion Coercion
g)
TransCo Coercion
co1 Coercion
co2
-> Coercion -> Coercion -> Coercion
mkTransCo (Coercion -> Coercion
promoteCoercion Coercion
co1) (Coercion -> Coercion
promoteCoercion Coercion
co2)
NthCo Role
_ Int
n Coercion
co1
| Just (TyCon
_, [Coercion]
args) <- Coercion -> Maybe (TyCon, [Coercion])
splitTyConAppCo_maybe Coercion
co1
, [Coercion]
args [Coercion] -> Int -> Bool
forall a. [a] -> Int -> Bool
`lengthExceeds` Int
n
-> Coercion -> Coercion
promoteCoercion ([Coercion]
args [Coercion] -> Int -> Coercion
forall a. [a] -> Int -> a
!! Int
n)
| Just (CoVar, Coercion, Coercion)
_ <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_maybe Coercion
co
, Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
-> ASSERT( False ) mkNomReflCo liftedTypeKind
| Bool
otherwise
-> Coercion -> Coercion
mkKindCo Coercion
co
LRCo LeftOrRight
lr Coercion
co1
| Just (Coercion
lco, Coercion
rco) <- Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe Coercion
co1
-> case LeftOrRight
lr of
LeftOrRight
CLeft -> Coercion -> Coercion
promoteCoercion Coercion
lco
LeftOrRight
CRight -> Coercion -> Coercion
promoteCoercion Coercion
rco
| Bool
otherwise
-> Coercion -> Coercion
mkKindCo Coercion
co
InstCo Coercion
g Coercion
_
| Type -> Bool
isForAllTy_ty Type
ty1
-> ASSERT( isForAllTy_ty ty2 )
Coercion -> Coercion
promoteCoercion Coercion
g
| Bool
otherwise
-> ASSERT( False)
Type -> Coercion
mkNomReflCo Type
liftedTypeKind
KindCo Coercion
_
-> ASSERT( False )
Type -> Coercion
mkNomReflCo Type
liftedTypeKind
SubCo Coercion
g
-> Coercion -> Coercion
promoteCoercion Coercion
g
where
Pair Type
ty1 Type
ty2 = Coercion -> Pair Type
coercionKind Coercion
co
ki1 :: Type
ki1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
ki2 :: Type
ki2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
instCoercion :: Pair Type
-> CoercionN
-> Coercion
-> Maybe CoercionN
instCoercion :: Pair Type -> Coercion -> Coercion -> Maybe Coercion
instCoercion (Pair Type
lty Type
rty) Coercion
g Coercion
w
| (Type -> Bool
isForAllTy_ty Type
lty Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy_ty Type
rty)
Bool -> Bool -> Bool
|| (Type -> Bool
isForAllTy_co Type
lty Bool -> Bool -> Bool
&& Type -> Bool
isForAllTy_co Type
rty)
, Just Coercion
w' <- Role -> Coercion -> Maybe Coercion
setNominalRole_maybe (Coercion -> Role
coercionRole Coercion
w) Coercion
w
= Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion -> Coercion
mkInstCo Coercion
g Coercion
w'
| Type -> Bool
isFunTy Type
lty Bool -> Bool -> Bool
&& Type -> Bool
isFunTy Type
rty
= Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
4 Coercion
g
| Bool
otherwise
= Maybe Coercion
forall a. Maybe a
Nothing
instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
instCoercions :: Coercion -> [Coercion] -> Maybe Coercion
instCoercions Coercion
g [Coercion]
ws
= let arg_ty_pairs :: [Pair Type]
arg_ty_pairs = (Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Pair Type
coercionKind [Coercion]
ws in
(Pair Type, Coercion) -> Coercion
forall a b. (a, b) -> b
snd ((Pair Type, Coercion) -> Coercion)
-> Maybe (Pair Type, Coercion) -> Maybe Coercion
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Pair Type, Coercion)
-> (Pair Type, Coercion) -> Maybe (Pair Type, Coercion))
-> (Pair Type, Coercion)
-> [(Pair Type, Coercion)]
-> Maybe (Pair Type, Coercion)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (Pair Type, Coercion)
-> (Pair Type, Coercion) -> Maybe (Pair Type, Coercion)
go (Coercion -> Pair Type
coercionKind Coercion
g, Coercion
g) ([Pair Type] -> [Coercion] -> [(Pair Type, Coercion)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Pair Type]
arg_ty_pairs [Coercion]
ws)
where
go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
-> Maybe (Pair Type, Coercion)
go :: (Pair Type, Coercion)
-> (Pair Type, Coercion) -> Maybe (Pair Type, Coercion)
go (Pair Type
g_tys, Coercion
g) (Pair Type
w_tys, Coercion
w)
= do { Coercion
g' <- Pair Type -> Coercion -> Coercion -> Maybe Coercion
instCoercion Pair Type
g_tys Coercion
g Coercion
w
; (Pair Type, Coercion) -> Maybe (Pair Type, Coercion)
forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Type -> Type -> Type
Type -> Type -> Type
piResultTy (Type -> Type -> Type) -> Pair Type -> Pair (Type -> Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair Type
g_tys Pair (Type -> Type) -> Pair Type -> Pair Type
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Pair Type
w_tys, Coercion
g') }
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 :: 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 {} -> ASSERT( r == Nominal )
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
castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
castCoercionKind :: Coercion -> Coercion -> Coercion -> Coercion
castCoercionKind Coercion
g Coercion
h1 Coercion
h2
= Coercion
-> Role -> Type -> Type -> Coercion -> Coercion -> Coercion
castCoercionKind2 Coercion
g Role
r Type
t1 Type
t2 Coercion
h1 Coercion
h2
where
(Pair Type
t1 Type
t2, Role
r) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
g
mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
mkFamilyTyConAppCo :: TyCon -> [Coercion] -> Coercion
mkFamilyTyConAppCo TyCon
tc [Coercion]
cos
| Just (TyCon
fam_tc, [Type]
fam_tys) <- TyCon -> Maybe (TyCon, [Type])
tyConFamInst_maybe TyCon
tc
, let tvs :: [CoVar]
tvs = TyCon -> [CoVar]
tyConTyVars TyCon
tc
fam_cos :: [Coercion]
fam_cos = ASSERT2( tvs `equalLength` cos, ppr tc <+> ppr cos )
(Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (Role -> [CoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
Nominal [CoVar]
tvs [Coercion]
cos) [Type]
fam_tys
= HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
fam_tc [Coercion]
fam_cos
| Bool
otherwise
= HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc [Coercion]
cos
mkPiCos :: Role -> [Var] -> Coercion -> Coercion
mkPiCos :: Role -> [CoVar] -> Coercion -> Coercion
mkPiCos Role
r [CoVar]
vs Coercion
co = (CoVar -> Coercion -> Coercion) -> Coercion -> [CoVar] -> Coercion
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Role -> CoVar -> Coercion -> Coercion
mkPiCo Role
r) Coercion
co [CoVar]
vs
mkPiCo :: Role -> Var -> Coercion -> Coercion
mkPiCo :: Role -> CoVar -> Coercion -> Coercion
mkPiCo Role
r CoVar
v Coercion
co | CoVar -> Bool
isTyVar CoVar
v = [CoVar] -> Coercion -> Coercion
mkHomoForAllCos [CoVar
v] Coercion
co
| CoVar -> Bool
isCoVar CoVar
v = ASSERT( not (v `elemVarSet` tyCoVarsOfCo co) )
Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r (Type -> Coercion
multToCo (CoVar -> Type
varMult CoVar
v)) (Role -> Type -> Coercion
mkReflCo Role
r (CoVar -> Type
varType CoVar
v)) Coercion
co
| Bool
otherwise = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r (Type -> Coercion
multToCo (CoVar -> Type
varMult CoVar
v)) (Role -> Type -> Coercion
mkReflCo Role
r (CoVar -> Type
varType CoVar
v)) Coercion
co
mkCoCast :: Coercion -> CoercionR -> Coercion
mkCoCast :: Coercion -> Coercion -> Coercion
mkCoCast Coercion
c Coercion
g
| (Coercion
g2:Coercion
g1:[Coercion]
_) <- [Coercion] -> [Coercion]
forall a. [a] -> [a]
reverse [Coercion]
co_list
= Coercion -> Coercion
mkSymCo Coercion
g1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
c Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
g2
| Bool
otherwise
= String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkCoCast" (Coercion -> SDoc
forall a. Outputable a => a -> SDoc
ppr Coercion
g SDoc -> SDoc -> SDoc
$$ Pair Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Coercion -> Pair Type
coercionKind Coercion
g))
where
(TyCon
tc, [Type]
_) = Type -> (TyCon, [Type])
splitTyConApp (Coercion -> Type
coercionLKind Coercion
g)
co_list :: [Coercion]
co_list = Int -> Coercion -> [Role] -> [Coercion]
decomposeCo (TyCon -> Int
tyConArity TyCon
tc) Coercion
g (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc)
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
| Just ([CoVar]
tvs, Type
ty, CoAxiom Unbranched
co_tc) <- TyCon -> Maybe ([CoVar], Type, CoAxiom Unbranched)
unwrapNewTyConEtad_maybe TyCon
tc
, [CoVar]
tvs [CoVar] -> [Type] -> Bool
forall a b. [a] -> [b] -> Bool
`leLength` [Type]
tys
= (Type, Coercion) -> Maybe (Type, Coercion)
forall a. a -> Maybe a
Just ([CoVar] -> Type -> [Type] -> Type
applyTysX [CoVar]
tvs Type
ty [Type]
tys, Role -> CoAxiom Unbranched -> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo Role
Representational CoAxiom Unbranched
co_tc [Type]
tys [])
| Bool
otherwise
= Maybe (Type, Coercion)
forall a. Maybe a
Nothing
type NormaliseStepper ev = RecTcChecker
-> TyCon
-> [Type]
-> NormaliseStepResult ev
data NormaliseStepResult ev
= NS_Done
| NS_Abort
| NS_Step RecTcChecker Type ev
mapStepResult :: (ev1 -> ev2)
-> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult :: (ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult ev1 -> ev2
f (NS_Step RecTcChecker
rec_nts Type
ty ev1
ev) = RecTcChecker -> Type -> ev2 -> NormaliseStepResult ev2
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts Type
ty (ev1 -> ev2
f ev1
ev)
mapStepResult ev1 -> ev2
_ NormaliseStepResult ev1
NS_Done = NormaliseStepResult ev2
forall ev. NormaliseStepResult ev
NS_Done
mapStepResult ev1 -> ev2
_ NormaliseStepResult ev1
NS_Abort = NormaliseStepResult ev2
forall ev. NormaliseStepResult ev
NS_Abort
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
-> NormaliseStepper ev
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev -> NormaliseStepper ev
composeSteppers NormaliseStepper ev
step1 NormaliseStepper ev
step2 RecTcChecker
rec_nts TyCon
tc [Type]
tys
= case NormaliseStepper ev
step1 RecTcChecker
rec_nts TyCon
tc [Type]
tys of
success :: NormaliseStepResult ev
success@(NS_Step {}) -> NormaliseStepResult ev
success
NormaliseStepResult ev
NS_Done -> NormaliseStepper ev
step2 RecTcChecker
rec_nts TyCon
tc [Type]
tys
NormaliseStepResult ev
NS_Abort -> NormaliseStepResult ev
forall ev. NormaliseStepResult ev
NS_Abort
unwrapNewTypeStepper :: NormaliseStepper Coercion
unwrapNewTypeStepper :: NormaliseStepper Coercion
unwrapNewTypeStepper RecTcChecker
rec_nts TyCon
tc [Type]
tys
| Just (Type
ty', Coercion
co) <- TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe TyCon
tc [Type]
tys
= case RecTcChecker -> TyCon -> Maybe RecTcChecker
checkRecTc RecTcChecker
rec_nts TyCon
tc of
Just RecTcChecker
rec_nts' -> RecTcChecker -> Type -> Coercion -> NormaliseStepResult Coercion
forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' Coercion
co
Maybe RecTcChecker
Nothing -> NormaliseStepResult Coercion
forall ev. NormaliseStepResult ev
NS_Abort
| Bool
otherwise
= NormaliseStepResult Coercion
forall ev. NormaliseStepResult ev
NS_Done
topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev)
-> Type -> Maybe (ev, Type)
topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper ev
stepper ev -> ev -> ev
plus Type
ty
| Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
, NS_Step RecTcChecker
rec_nts Type
ty' ev
ev <- NormaliseStepper ev
stepper RecTcChecker
initRecTc TyCon
tc [Type]
tys
= RecTcChecker -> ev -> Type -> Maybe (ev, Type)
go RecTcChecker
rec_nts ev
ev Type
ty'
| Bool
otherwise
= Maybe (ev, Type)
forall a. Maybe a
Nothing
where
go :: RecTcChecker -> ev -> Type -> Maybe (ev, Type)
go RecTcChecker
rec_nts ev
ev Type
ty
| Just (TyCon
tc, [Type]
tys) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
= case NormaliseStepper ev
stepper RecTcChecker
rec_nts TyCon
tc [Type]
tys of
NS_Step RecTcChecker
rec_nts' Type
ty' ev
ev' -> RecTcChecker -> ev -> Type -> Maybe (ev, Type)
go RecTcChecker
rec_nts' (ev
ev ev -> ev -> ev
`plus` ev
ev') Type
ty'
NormaliseStepResult ev
NS_Done -> (ev, Type) -> Maybe (ev, Type)
forall a. a -> Maybe a
Just (ev
ev, Type
ty)
NormaliseStepResult ev
NS_Abort -> Maybe (ev, Type)
forall a. Maybe a
Nothing
| Bool
otherwise
= (ev, Type) -> Maybe (ev, Type)
forall a. a -> Maybe a
Just (ev
ev, Type
ty)
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
topNormaliseNewType_maybe Type
ty
= NormaliseStepper Coercion
-> (Coercion -> Coercion -> Coercion)
-> Type
-> Maybe (Coercion, Type)
forall ev.
NormaliseStepper ev -> (ev -> ev -> ev) -> Type -> Maybe (ev, Type)
topNormaliseTypeX NormaliseStepper Coercion
unwrapNewTypeStepper Coercion -> Coercion -> Coercion
mkTransCo Type
ty
eqCoercion :: Coercion -> Coercion -> Bool
eqCoercion :: Coercion -> Coercion -> Bool
eqCoercion = Type -> Type -> Bool
eqType (Type -> Type -> Bool)
-> (Coercion -> Type) -> Coercion -> Coercion -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Coercion -> Type
coercionType
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
eqCoercionX RnEnv2
env = RnEnv2 -> Type -> Type -> Bool
eqTypeX RnEnv2
env (Type -> Type -> Bool)
-> (Coercion -> Type) -> Coercion -> Coercion -> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Coercion -> Type
coercionType
data LiftingContext = LC TCvSubst LiftCoEnv
instance Outputable LiftingContext where
ppr :: LiftingContext -> SDoc
ppr (LC TCvSubst
_ LiftCoEnv
env) = SDoc -> Int -> SDoc -> SDoc
hang (String -> SDoc
text String
"LiftingContext:") Int
2 (LiftCoEnv -> SDoc
forall a. Outputable a => a -> SDoc
ppr LiftCoEnv
env)
type LiftCoEnv = VarEnv Coercion
liftCoSubstWithEx :: Role
-> [TyVar]
-> [Coercion]
-> [TyCoVar]
-> [Type]
-> (Type -> Coercion, [Type])
liftCoSubstWithEx :: Role
-> [CoVar]
-> [Coercion]
-> [CoVar]
-> [Type]
-> (Type -> Coercion, [Type])
liftCoSubstWithEx Role
role [CoVar]
univs [Coercion]
omegas [CoVar]
exs [Type]
rhos
= let theta :: LiftingContext
theta = [(CoVar, Coercion)] -> LiftingContext
mkLiftingContext (String -> [CoVar] -> [Coercion] -> [(CoVar, Coercion)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"liftCoSubstWithExU" [CoVar]
univs [Coercion]
omegas)
psi :: LiftingContext
psi = LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
theta (String -> [CoVar] -> [Type] -> [(CoVar, Type)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"liftCoSubstWithExX" [CoVar]
exs [Type]
rhos)
in (LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
psi Role
role, HasCallStack => TCvSubst -> [Type] -> [Type]
TCvSubst -> [Type] -> [Type]
substTys (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
psi) ([CoVar] -> [Type]
mkTyCoVarTys [CoVar]
exs))
liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith :: Role -> [CoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith Role
r [CoVar]
tvs [Coercion]
cos Type
ty
= HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r ([(CoVar, Coercion)] -> LiftingContext
mkLiftingContext ([(CoVar, Coercion)] -> LiftingContext)
-> [(CoVar, Coercion)] -> LiftingContext
forall a b. (a -> b) -> a -> b
$ String -> [CoVar] -> [Coercion] -> [(CoVar, Coercion)]
forall a b. String -> [a] -> [b] -> [(a, b)]
zipEqual String
"liftCoSubstWith" [CoVar]
tvs [Coercion]
cos) Type
ty
liftCoSubst :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
{-# INLINE liftCoSubst #-}
liftCoSubst :: Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r lc :: LiftingContext
lc@(LC TCvSubst
subst LiftCoEnv
env) Type
ty
| LiftCoEnv -> Bool
forall a. VarEnv a -> Bool
isEmptyVarEnv LiftCoEnv
env = Role -> Type -> Coercion
mkReflCo Role
r (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
ty)
| Bool
otherwise = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
r Type
ty
emptyLiftingContext :: InScopeSet -> LiftingContext
emptyLiftingContext :: InScopeSet -> LiftingContext
emptyLiftingContext InScopeSet
in_scope = TCvSubst -> LiftCoEnv -> LiftingContext
LC (InScopeSet -> TCvSubst
mkEmptyTCvSubst InScopeSet
in_scope) LiftCoEnv
forall a. VarEnv a
emptyVarEnv
mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
mkLiftingContext :: [(CoVar, Coercion)] -> LiftingContext
mkLiftingContext [(CoVar, Coercion)]
pairs
= TCvSubst -> LiftCoEnv -> LiftingContext
LC (InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ [Coercion] -> VarSet
tyCoVarsOfCos (((CoVar, Coercion) -> Coercion)
-> [(CoVar, Coercion)] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map (CoVar, Coercion) -> Coercion
forall a b. (a, b) -> b
snd [(CoVar, Coercion)]
pairs))
([(CoVar, Coercion)] -> LiftCoEnv
forall a. [(CoVar, a)] -> VarEnv a
mkVarEnv [(CoVar, Coercion)]
pairs)
mkSubstLiftingContext :: TCvSubst -> LiftingContext
mkSubstLiftingContext :: TCvSubst -> LiftingContext
mkSubstLiftingContext TCvSubst
subst = TCvSubst -> LiftCoEnv -> LiftingContext
LC TCvSubst
subst LiftCoEnv
forall a. VarEnv a
emptyVarEnv
extendLiftingContext :: LiftingContext
-> TyCoVar
-> Coercion
-> LiftingContext
extendLiftingContext :: LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext (LC TCvSubst
subst LiftCoEnv
env) CoVar
tv Coercion
arg
| Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
arg
= TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst -> CoVar -> Type -> TCvSubst
extendTCvSubst TCvSubst
subst CoVar
tv Type
ty) LiftCoEnv
env
| Bool
otherwise
= TCvSubst -> LiftCoEnv -> LiftingContext
LC TCvSubst
subst (LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
tv Coercion
arg)
extendLiftingContextAndInScope :: LiftingContext
-> TyCoVar
-> Coercion
-> LiftingContext
extendLiftingContextAndInScope :: LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContextAndInScope (LC TCvSubst
subst LiftCoEnv
env) CoVar
tv Coercion
co
= LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContext (TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst -> VarSet -> TCvSubst
extendTCvInScopeSet TCvSubst
subst (Coercion -> VarSet
tyCoVarsOfCo Coercion
co)) LiftCoEnv
env) CoVar
tv Coercion
co
extendLiftingContextEx :: LiftingContext
-> [(TyCoVar,Type)]
-> LiftingContext
extendLiftingContextEx :: LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
lc [] = LiftingContext
lc
extendLiftingContextEx lc :: LiftingContext
lc@(LC TCvSubst
subst LiftCoEnv
env) ((CoVar
v,Type
ty):[(CoVar, Type)]
rest)
| CoVar -> Bool
isTyVar CoVar
v
= let lc' :: LiftingContext
lc' = TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst
subst TCvSubst -> VarSet -> TCvSubst
`extendTCvInScopeSet` Type -> VarSet
tyCoVarsOfType Type
ty)
(LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
v (Coercion -> LiftCoEnv) -> Coercion -> LiftCoEnv
forall a b. (a -> b) -> a -> b
$
Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
Nominal
Type
ty
(LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
Nominal (CoVar -> Type
tyVarKind CoVar
v)))
in LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
lc' [(CoVar, Type)]
rest
| CoercionTy Coercion
co <- Type
ty
=
ASSERT( isCoVar v )
let (Type
_, Type
_, Type
s1, Type
s2, Role
r) = HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
v
lift_s1 :: Coercion
lift_s1 = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
r Type
s1
lift_s2 :: Coercion
lift_s2 = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc Role
r Type
s2
kco :: Coercion
kco = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal (Role -> TyCon
equalityTyCon Role
r)
[ Coercion -> Coercion
mkKindCo Coercion
lift_s1, Coercion -> Coercion
mkKindCo Coercion
lift_s2
, Coercion
lift_s1 , Coercion
lift_s2 ]
lc' :: LiftingContext
lc' = TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst
subst TCvSubst -> VarSet -> TCvSubst
`extendTCvInScopeSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
(LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
v
(Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kco Coercion
co (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
(Coercion -> Coercion
mkSymCo Coercion
lift_s1) Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
lift_s2))
in LiftingContext -> [(CoVar, Type)] -> LiftingContext
extendLiftingContextEx LiftingContext
lc' [(CoVar, Type)]
rest
| Bool
otherwise
= String -> SDoc -> LiftingContext
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendLiftingContextEx" (CoVar -> SDoc
forall a. Outputable a => a -> SDoc
ppr CoVar
v SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"|->" SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
zapLiftingContext :: LiftingContext -> LiftingContext
zapLiftingContext :: LiftingContext -> LiftingContext
zapLiftingContext (LC TCvSubst
subst LiftCoEnv
_) = TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst) LiftCoEnv
forall a. VarEnv a
emptyVarEnv
substForAllCoBndrUsingLC :: Bool
-> (Coercion -> Coercion)
-> LiftingContext -> TyCoVar -> Coercion
-> (LiftingContext, TyCoVar, Coercion)
substForAllCoBndrUsingLC :: Bool
-> (Coercion -> Coercion)
-> LiftingContext
-> CoVar
-> Coercion
-> (LiftingContext, CoVar, Coercion)
substForAllCoBndrUsingLC Bool
sym Coercion -> Coercion
sco (LC TCvSubst
subst LiftCoEnv
lc_env) CoVar
tv Coercion
co
= (TCvSubst -> LiftCoEnv -> LiftingContext
LC TCvSubst
subst' LiftCoEnv
lc_env, CoVar
tv', Coercion
co')
where
(TCvSubst
subst', CoVar
tv', Coercion
co') = Bool
-> (Coercion -> Coercion)
-> TCvSubst
-> CoVar
-> Coercion
-> (TCvSubst, CoVar, Coercion)
substForAllCoBndrUsing Bool
sym Coercion -> Coercion
sco TCvSubst
subst CoVar
tv Coercion
co
ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
ty_co_subst !LiftingContext
lc Role
role Type
ty
= Role -> Type -> Coercion
go Role
role Type
ty
where
go :: Role -> Type -> Coercion
go :: Role -> Type -> Coercion
go Role
r Type
ty | Just Type
ty' <- Type -> Maybe Type
coreView Type
ty
= Role -> Type -> Coercion
go Role
r Type
ty'
go Role
Phantom Type
ty = Type -> Coercion
lift_phantom Type
ty
go Role
r (TyVarTy CoVar
tv) = String -> Maybe Coercion -> Coercion
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"ty_co_subst bad roles" (Maybe Coercion -> Coercion) -> Maybe Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
LiftingContext -> Role -> CoVar -> Maybe Coercion
liftCoSubstTyVar LiftingContext
lc Role
r CoVar
tv
go Role
r (AppTy Type
ty1 Type
ty2) = Coercion -> Coercion -> Coercion
mkAppCo (Role -> Type -> Coercion
go Role
r Type
ty1) (Role -> Type -> Coercion
go Role
Nominal Type
ty2)
go Role
r (TyConApp TyCon
tc [Type]
tys) = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
r TyCon
tc ((Role -> Type -> Coercion) -> [Role] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
go (Role -> TyCon -> [Role]
tyConRolesX Role
r TyCon
tc) [Type]
tys)
go Role
r (FunTy AnonArgFlag
_ Type
w Type
ty1 Type
ty2) = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
r (Role -> Type -> Coercion
go Role
Nominal Type
w) (Role -> Type -> Coercion
go Role
r Type
ty1) (Role -> Type -> Coercion
go Role
r Type
ty2)
go Role
r t :: Type
t@(ForAllTy (Bndr CoVar
v ArgFlag
_) Type
ty)
= let (LiftingContext
lc', CoVar
v', Coercion
h) = LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion)
liftCoSubstVarBndr LiftingContext
lc CoVar
v
body_co :: Coercion
body_co = LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc' Role
r Type
ty in
if CoVar -> Bool
isTyVar CoVar
v' Bool -> Bool -> Bool
|| CoVar -> Coercion -> Bool
almostDevoidCoVarOfCo CoVar
v' Coercion
body_co
then CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
v' Coercion
h Coercion
body_co
else String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"ty_co_subst: covar is not almost devoid" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
t)
go Role
r ty :: Type
ty@(LitTy {}) = ASSERT( r == Nominal )
Type -> Coercion
mkNomReflCo Type
ty
go Role
r (CastTy Type
ty Coercion
co) = Coercion -> Coercion -> Coercion -> Coercion
castCoercionKind (Role -> Type -> Coercion
go Role
r Type
ty) (LiftingContext -> Coercion -> Coercion
substLeftCo LiftingContext
lc Coercion
co)
(LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co)
go Role
r (CoercionTy Coercion
co) = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
r Coercion
kco (LiftingContext -> Coercion -> Coercion
substLeftCo LiftingContext
lc Coercion
co)
(LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co)
where kco :: Coercion
kco = Role -> Type -> Coercion
go Role
Nominal (Coercion -> Type
coercionType Coercion
co)
lift_phantom :: Type -> Coercion
lift_phantom Type
ty = Coercion -> Type -> Type -> Coercion
mkPhantomCo (Role -> Type -> Coercion
go Role
Nominal (HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty))
(HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
lc) Type
ty)
(HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
lc) Type
ty)
liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar :: LiftingContext -> Role -> CoVar -> Maybe Coercion
liftCoSubstTyVar (LC TCvSubst
subst LiftCoEnv
env) Role
r CoVar
v
| Just Coercion
co_arg <- LiftCoEnv -> CoVar -> Maybe Coercion
forall a. VarEnv a -> CoVar -> Maybe a
lookupVarEnv LiftCoEnv
env CoVar
v
= Role -> Role -> Coercion -> Maybe Coercion
downgradeRole_maybe Role
r (Coercion -> Role
coercionRole Coercion
co_arg) Coercion
co_arg
| Bool
otherwise
= Coercion -> Maybe Coercion
forall a. a -> Maybe a
Just (Coercion -> Maybe Coercion) -> Coercion -> Maybe Coercion
forall a b. (a -> b) -> a -> b
$ Role -> Type -> Coercion
mkReflCo Role
r (TCvSubst -> CoVar -> Type
substTyVar TCvSubst
subst CoVar
v)
liftCoSubstVarBndr :: LiftingContext -> TyCoVar
-> (LiftingContext, TyCoVar, Coercion)
liftCoSubstVarBndr :: LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion)
liftCoSubstVarBndr LiftingContext
lc CoVar
tv
= let (LiftingContext
lc', CoVar
tv', Coercion
h, ()
_) = (LiftingContext -> Type -> (Coercion, ()))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, ())
forall a.
(LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
liftCoSubstVarBndrUsing LiftingContext -> Type -> (Coercion, ())
callback LiftingContext
lc CoVar
tv in
(LiftingContext
lc', CoVar
tv', Coercion
h)
where
callback :: LiftingContext -> Type -> (Coercion, ())
callback LiftingContext
lc' Type
ty' = (LiftingContext -> Role -> Type -> Coercion
ty_co_subst LiftingContext
lc' Role
Nominal Type
ty', ())
liftCoSubstVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-> LiftingContext -> TyCoVar
-> (LiftingContext, TyCoVar, CoercionN, a)
liftCoSubstVarBndrUsing :: (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
liftCoSubstVarBndrUsing LiftingContext -> Type -> (Coercion, a)
fun LiftingContext
lc CoVar
old_var
| CoVar -> Bool
isTyVar CoVar
old_var
= (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
forall a.
(LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
liftCoSubstTyVarBndrUsing LiftingContext -> Type -> (Coercion, a)
fun LiftingContext
lc CoVar
old_var
| Bool
otherwise
= (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
forall a.
(LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
liftCoSubstCoVarBndrUsing LiftingContext -> Type -> (Coercion, a)
fun LiftingContext
lc CoVar
old_var
liftCoSubstTyVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-> LiftingContext -> TyVar
-> (LiftingContext, TyVar, CoercionN, a)
liftCoSubstTyVarBndrUsing :: (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
liftCoSubstTyVarBndrUsing LiftingContext -> Type -> (Coercion, a)
fun lc :: LiftingContext
lc@(LC TCvSubst
subst LiftCoEnv
cenv) CoVar
old_var
= ASSERT( isTyVar old_var )
( TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst
subst TCvSubst -> CoVar -> TCvSubst
`extendTCvInScope` CoVar
new_var) LiftCoEnv
new_cenv
, CoVar
new_var, Coercion
eta, a
stuff )
where
old_kind :: Type
old_kind = CoVar -> Type
tyVarKind CoVar
old_var
(Coercion
eta, a
stuff) = LiftingContext -> Type -> (Coercion, a)
fun LiftingContext
lc Type
old_kind
k1 :: Type
k1 = Coercion -> Type
coercionLKind Coercion
eta
new_var :: CoVar
new_var = InScopeSet -> CoVar -> CoVar
uniqAway (TCvSubst -> InScopeSet
getTCvInScope TCvSubst
subst) (CoVar -> Type -> CoVar
setVarType CoVar
old_var Type
k1)
lifted :: Coercion
lifted = Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
Nominal (CoVar -> Type
TyVarTy CoVar
new_var) Coercion
eta
new_cenv :: LiftCoEnv
new_cenv = LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
cenv CoVar
old_var Coercion
lifted
liftCoSubstCoVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-> LiftingContext -> CoVar
-> (LiftingContext, CoVar, CoercionN, a)
liftCoSubstCoVarBndrUsing :: (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> CoVar -> (LiftingContext, CoVar, Coercion, a)
liftCoSubstCoVarBndrUsing LiftingContext -> Type -> (Coercion, a)
fun lc :: LiftingContext
lc@(LC TCvSubst
subst LiftCoEnv
cenv) CoVar
old_var
= ASSERT( isCoVar old_var )
( TCvSubst -> LiftCoEnv -> LiftingContext
LC (TCvSubst
subst TCvSubst -> CoVar -> TCvSubst
`extendTCvInScope` CoVar
new_var) LiftCoEnv
new_cenv
, CoVar
new_var, Coercion
kind_co, a
stuff )
where
old_kind :: Type
old_kind = CoVar -> Type
coVarKind CoVar
old_var
(Coercion
eta, a
stuff) = LiftingContext -> Type -> (Coercion, a)
fun LiftingContext
lc Type
old_kind
k1 :: Type
k1 = Coercion -> Type
coercionLKind Coercion
eta
new_var :: CoVar
new_var = InScopeSet -> CoVar -> CoVar
uniqAway (TCvSubst -> InScopeSet
getTCvInScope TCvSubst
subst) (CoVar -> Type -> CoVar
setVarType CoVar
old_var Type
k1)
role :: Role
role = CoVar -> Role
coVarRole CoVar
old_var
eta' :: Coercion
eta' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
Nominal Coercion
eta
eta1 :: Coercion
eta1 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
role Int
2 Coercion
eta'
eta2 :: Coercion
eta2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
role Int
3 Coercion
eta'
co1 :: Coercion
co1 = CoVar -> Coercion
mkCoVarCo CoVar
new_var
co2 :: Coercion
co2 = Coercion -> Coercion
mkSymCo Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
co1 Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
eta2
kind_co :: Coercion
kind_co = HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal (Role -> TyCon
equalityTyCon Role
role)
[ Coercion -> Coercion
mkKindCo Coercion
co1, Coercion -> Coercion
mkKindCo Coercion
co2
, Coercion
co1 , Coercion
co2 ]
lifted :: Coercion
lifted = Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kind_co Coercion
co1 Coercion
co2
new_cenv :: LiftCoEnv
new_cenv = LiftCoEnv -> CoVar -> Coercion -> LiftCoEnv
forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
cenv CoVar
old_var Coercion
lifted
isMappedByLC :: TyCoVar -> LiftingContext -> Bool
isMappedByLC :: CoVar -> LiftingContext -> Bool
isMappedByLC CoVar
tv (LC TCvSubst
_ LiftCoEnv
env) = CoVar
tv CoVar -> LiftCoEnv -> Bool
forall a. CoVar -> VarEnv a -> Bool
`elemVarEnv` LiftCoEnv
env
substLeftCo :: LiftingContext -> Coercion -> Coercion
substLeftCo :: LiftingContext -> Coercion -> Coercion
substLeftCo LiftingContext
lc Coercion
co
= HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
lc) Coercion
co
substRightCo :: LiftingContext -> Coercion -> Coercion
substRightCo :: LiftingContext -> Coercion -> Coercion
substRightCo LiftingContext
lc Coercion
co
= HasCallStack => TCvSubst -> Coercion -> Coercion
TCvSubst -> Coercion -> Coercion
substCo (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
lc) Coercion
co
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv = (Coercion -> Coercion) -> LiftCoEnv -> LiftCoEnv
forall a b. (a -> b) -> VarEnv a -> VarEnv b
mapVarEnv Coercion -> Coercion
mkSymCo
lcSubstLeft :: LiftingContext -> TCvSubst
lcSubstLeft :: LiftingContext -> TCvSubst
lcSubstLeft (LC TCvSubst
subst LiftCoEnv
lc_env) = TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstLeft TCvSubst
subst LiftCoEnv
lc_env
lcSubstRight :: LiftingContext -> TCvSubst
lcSubstRight :: LiftingContext -> TCvSubst
lcSubstRight (LC TCvSubst
subst LiftCoEnv
lc_env) = TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstRight TCvSubst
subst LiftCoEnv
lc_env
liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstLeft = (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubst forall a. Pair a -> a
pFst
liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstRight = (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubst forall a. Pair a -> a
pSnd
liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubst forall a. Pair a -> a
selector TCvSubst
subst LiftCoEnv
lc_env
= TCvSubst -> TCvSubst -> TCvSubst
composeTCvSubst (InScopeSet -> TvSubstEnv -> LiftCoEnv -> TCvSubst
TCvSubst InScopeSet
emptyInScopeSet TvSubstEnv
tenv LiftCoEnv
cenv) TCvSubst
subst
where
pairs :: [(Unique, Coercion)]
pairs = LiftCoEnv -> [(Unique, Coercion)]
forall key elt. UniqFM key elt -> [(Unique, elt)]
nonDetUFMToList LiftCoEnv
lc_env
([(Unique, Type)]
tpairs, [(Unique, Coercion)]
cpairs) = ((Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion))
-> [(Unique, Coercion)] -> ([(Unique, Type)], [(Unique, Coercion)])
forall a b c. (a -> Either b c) -> [a] -> ([b], [c])
partitionWith (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
ty_or_co [(Unique, Coercion)]
pairs
tenv :: TvSubstEnv
tenv = [(Unique, Type)] -> TvSubstEnv
forall a. [(Unique, a)] -> VarEnv a
mkVarEnv_Directly [(Unique, Type)]
tpairs
cenv :: LiftCoEnv
cenv = [(Unique, Coercion)] -> LiftCoEnv
forall a. [(Unique, a)] -> VarEnv a
mkVarEnv_Directly [(Unique, Coercion)]
cpairs
ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
ty_or_co (Unique
u, Coercion
co)
| Just Coercion
equality_co <- Type -> Maybe Coercion
isCoercionTy_maybe Type
equality_ty
= (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
forall a b. b -> Either a b
Right (Unique
u, Coercion
equality_co)
| Bool
otherwise
= (Unique, Type) -> Either (Unique, Type) (Unique, Coercion)
forall a b. a -> Either a b
Left (Unique
u, Type
equality_ty)
where
equality_ty :: Type
equality_ty = Pair Type -> Type
forall a. Pair a -> a
selector (Coercion -> Pair Type
coercionKind Coercion
co)
lcTCvSubst :: LiftingContext -> TCvSubst
lcTCvSubst :: LiftingContext -> TCvSubst
lcTCvSubst (LC TCvSubst
subst LiftCoEnv
_) = TCvSubst
subst
lcInScopeSet :: LiftingContext -> InScopeSet
lcInScopeSet :: LiftingContext -> InScopeSet
lcInScopeSet (LC TCvSubst
subst LiftCoEnv
_) = TCvSubst -> InScopeSet
getTCvInScope TCvSubst
subst
seqMCo :: MCoercion -> ()
seqMCo :: MCoercion -> ()
seqMCo MCoercion
MRefl = ()
seqMCo (MCo Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqCo :: Coercion -> ()
seqCo :: Coercion -> ()
seqCo (Refl Type
ty) = Type -> ()
seqType Type
ty
seqCo (GRefl Role
r Type
ty MCoercion
mco) = Role
r Role -> () -> ()
`seq` Type -> ()
seqType Type
ty () -> () -> ()
`seq` MCoercion -> ()
seqMCo MCoercion
mco
seqCo (TyConAppCo Role
r TyCon
tc [Coercion]
cos) = Role
r Role -> () -> ()
`seq` TyCon
tc TyCon -> () -> ()
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
seqCo (AppCo Coercion
co1 Coercion
co2) = Coercion -> ()
seqCo Coercion
co1 () -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (ForAllCo CoVar
tv Coercion
k Coercion
co) = Type -> ()
seqType (CoVar -> Type
varType CoVar
tv) () -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
k
() -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (FunCo Role
r Coercion
w Coercion
co1 Coercion
co2) = Role
r Role -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
w () -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co1 () -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (CoVarCo CoVar
cv) = CoVar
cv CoVar -> () -> ()
`seq` ()
seqCo (HoleCo CoercionHole
h) = CoercionHole -> CoVar
coHoleCoVar CoercionHole
h CoVar -> () -> ()
`seq` ()
seqCo (AxiomInstCo CoAxiom Branched
con Int
ind [Coercion]
cos) = CoAxiom Branched
con CoAxiom Branched -> () -> ()
`seq` Int
ind Int -> () -> ()
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
seqCo (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2)
= UnivCoProvenance -> ()
seqProv UnivCoProvenance
p () -> () -> ()
`seq` Role
r Role -> () -> ()
`seq` Type -> ()
seqType Type
t1 () -> () -> ()
`seq` Type -> ()
seqType Type
t2
seqCo (SymCo Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqCo (TransCo Coercion
co1 Coercion
co2) = Coercion -> ()
seqCo Coercion
co1 () -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (NthCo Role
r Int
n Coercion
co) = Role
r Role -> () -> ()
`seq` Int
n Int -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (LRCo LeftOrRight
lr Coercion
co) = LeftOrRight
lr LeftOrRight -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (InstCo Coercion
co Coercion
arg) = Coercion -> ()
seqCo Coercion
co () -> () -> ()
`seq` Coercion -> ()
seqCo Coercion
arg
seqCo (KindCo Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqCo (SubCo Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqCo (AxiomRuleCo CoAxiomRule
_ [Coercion]
cs) = [Coercion] -> ()
seqCos [Coercion]
cs
seqProv :: UnivCoProvenance -> ()
seqProv :: UnivCoProvenance -> ()
seqProv (PhantomProv Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqProv (ProofIrrelProv Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqProv (PluginProv String
_) = ()
seqCos :: [Coercion] -> ()
seqCos :: [Coercion] -> ()
seqCos [] = ()
seqCos (Coercion
co:[Coercion]
cos) = Coercion -> ()
seqCo Coercion
co () -> () -> ()
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds [Coercion]
tys = [Pair Type] -> Pair [Type]
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA ([Pair Type] -> Pair [Type]) -> [Pair Type] -> Pair [Type]
forall a b. (a -> b) -> a -> b
$ (Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Pair Type
coercionKind [Coercion]
tys
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co = (Coercion -> Pair Type
coercionKind Coercion
co, Coercion -> Role
coercionRole Coercion
co)
coercionType :: Coercion -> Type
coercionType :: Coercion -> Type
coercionType Coercion
co = case Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co of
(Pair Type
ty1 Type
ty2, Role
r) -> Role -> Type -> Type -> Type
mkCoercionType Role
r Type
ty1 Type
ty2
coercionKind :: Coercion -> Pair Type
coercionKind :: Coercion -> Pair Type
coercionKind Coercion
co = Type -> Type -> Pair Type
forall a. a -> a -> Pair a
Pair (Coercion -> Type
coercionLKind Coercion
co) (Coercion -> Type
coercionRKind Coercion
co)
coercionLKind :: Coercion -> Type
coercionLKind :: Coercion -> Type
coercionLKind Coercion
co
= Coercion -> Type
go Coercion
co
where
go :: Coercion -> Type
go (Refl Type
ty) = Type
ty
go (GRefl Role
_ Type
ty MCoercion
_) = Type
ty
go (TyConAppCo Role
_ TyCon
tc [Coercion]
cos) = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
go (AppCo Coercion
co1 Coercion
co2) = Type -> Type -> Type
mkAppTy (Coercion -> Type
go Coercion
co1) (Coercion -> Type
go Coercion
co2)
go (ForAllCo CoVar
tv1 Coercion
_ Coercion
co1) = CoVar -> Type -> Type
mkTyCoInvForAllTy CoVar
tv1 (Coercion -> Type
go Coercion
co1)
go (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) = Type -> Type -> Type -> Type
mkFunctionType (Coercion -> Type
go Coercion
w) (Coercion -> Type
go Coercion
co1) (Coercion -> Type
go Coercion
co2)
go (CoVarCo CoVar
cv) = HasDebugCallStack => CoVar -> Type
CoVar -> Type
coVarLType CoVar
cv
go (HoleCo CoercionHole
h) = HasDebugCallStack => CoVar -> Type
CoVar -> Type
coVarLType (CoercionHole -> CoVar
coHoleCoVar CoercionHole
h)
go (UnivCo UnivCoProvenance
_ Role
_ Type
ty1 Type
_) = Type
ty1
go (SymCo Coercion
co) = Coercion -> Type
coercionRKind Coercion
co
go (TransCo Coercion
co1 Coercion
_) = Coercion -> Type
go Coercion
co1
go (LRCo LeftOrRight
lr Coercion
co) = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type -> (Type, Type)
splitAppTy (Coercion -> Type
go Coercion
co))
go (InstCo Coercion
aco Coercion
arg) = Coercion -> [Type] -> Type
go_app Coercion
aco [Coercion -> Type
go Coercion
arg]
go (KindCo Coercion
co) = HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Coercion -> Type
go Coercion
co)
go (SubCo Coercion
co) = Coercion -> Type
go Coercion
co
go (NthCo Role
_ Int
d Coercion
co) = Int -> Type -> Type
go_nth Int
d (Coercion -> Type
go Coercion
co)
go (AxiomInstCo CoAxiom Branched
ax Int
ind [Coercion]
cos) = CoAxiom Branched -> Int -> [Type] -> Type
forall (br :: BranchFlag). CoAxiom br -> Int -> [Type] -> Type
go_ax_inst CoAxiom Branched
ax Int
ind ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
go (AxiomRuleCo CoAxiomRule
ax [Coercion]
cos) = Pair Type -> Type
forall a. Pair a -> a
pFst (Pair Type -> Type) -> Pair Type -> Type
forall a b. (a -> b) -> a -> b
$ String -> Maybe (Pair Type) -> Pair Type
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"coercionKind" (Maybe (Pair Type) -> Pair Type) -> Maybe (Pair Type) -> Pair Type
forall a b. (a -> b) -> a -> b
$
CoAxiomRule -> [Pair Type] -> Maybe (Pair Type)
coaxrProves CoAxiomRule
ax ([Pair Type] -> Maybe (Pair Type))
-> [Pair Type] -> Maybe (Pair Type)
forall a b. (a -> b) -> a -> b
$ (Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Pair Type
coercionKind [Coercion]
cos
go_ax_inst :: CoAxiom br -> Int -> [Type] -> Type
go_ax_inst CoAxiom br
ax Int
ind [Type]
tys
| CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
cab_tvs = [CoVar]
tvs, cab_cvs :: CoAxBranch -> [CoVar]
cab_cvs = [CoVar]
cvs
, cab_lhs :: CoAxBranch -> [Type]
cab_lhs = [Type]
lhs } <- CoAxiom br -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
ind
, let ([Type]
tys1, [Type]
cotys1) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
cos1 :: [Coercion]
cos1 = (Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys1
= ASSERT( tys `equalLength` (tvs ++ cvs) )
HasCallStack => [CoVar] -> [Type] -> Type -> Type
[CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos1 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> Type
mkTyConApp (CoAxiom br -> TyCon
forall (br :: BranchFlag). CoAxiom br -> TyCon
coAxiomTyCon CoAxiom br
ax) [Type]
lhs
go_app :: Coercion -> [Type] -> Type
go_app :: Coercion -> [Type] -> Type
go_app (InstCo Coercion
co Coercion
arg) [Type]
args = Coercion -> [Type] -> Type
go_app Coercion
co (Coercion -> Type
go Coercion
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args)
go_app Coercion
co [Type]
args = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Coercion -> Type
go Coercion
co) [Type]
args
go_nth :: Int -> Type -> Type
go_nth :: Int -> Type -> Type
go_nth Int
d Type
ty
| Just [Type]
args <- Type -> Maybe [Type]
tyConAppArgs_maybe Type
ty
= ASSERT( args `lengthExceeds` d )
[Type]
args [Type] -> Int -> Type
forall a. Outputable a => [a] -> Int -> a
`getNth` Int
d
| Int
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
, Just (CoVar
tv,Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTy_maybe Type
ty
= CoVar -> Type
tyVarKind CoVar
tv
| Bool
otherwise
= String -> SDoc -> Type
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coercionLKind:nth" (Int -> SDoc
forall a. Outputable a => a -> SDoc
ppr Int
d SDoc -> SDoc -> SDoc
<+> Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
coercionRKind :: Coercion -> Type
coercionRKind :: Coercion -> Type
coercionRKind Coercion
co
= Coercion -> Type
go Coercion
co
where
go :: Coercion -> Type
go (Refl Type
ty) = Type
ty
go (GRefl Role
_ Type
ty MCoercion
MRefl) = Type
ty
go (GRefl Role
_ Type
ty (MCo Coercion
co1)) = Type -> Coercion -> Type
mkCastTy Type
ty Coercion
co1
go (TyConAppCo Role
_ TyCon
tc [Coercion]
cos) = TyCon -> [Type] -> Type
mkTyConApp TyCon
tc ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
go (AppCo Coercion
co1 Coercion
co2) = Type -> Type -> Type
mkAppTy (Coercion -> Type
go Coercion
co1) (Coercion -> Type
go Coercion
co2)
go (CoVarCo CoVar
cv) = HasDebugCallStack => CoVar -> Type
CoVar -> Type
coVarRType CoVar
cv
go (HoleCo CoercionHole
h) = HasDebugCallStack => CoVar -> Type
CoVar -> Type
coVarRType (CoercionHole -> CoVar
coHoleCoVar CoercionHole
h)
go (FunCo Role
_ Coercion
w Coercion
co1 Coercion
co2) = Type -> Type -> Type -> Type
mkFunctionType (Coercion -> Type
go Coercion
w) (Coercion -> Type
go Coercion
co1) (Coercion -> Type
go Coercion
co2)
go (UnivCo UnivCoProvenance
_ Role
_ Type
_ Type
ty2) = Type
ty2
go (SymCo Coercion
co) = Coercion -> Type
coercionLKind Coercion
co
go (TransCo Coercion
_ Coercion
co2) = Coercion -> Type
go Coercion
co2
go (LRCo LeftOrRight
lr Coercion
co) = LeftOrRight -> (Type, Type) -> Type
forall a. LeftOrRight -> (a, a) -> a
pickLR LeftOrRight
lr (Type -> (Type, Type)
splitAppTy (Coercion -> Type
go Coercion
co))
go (InstCo Coercion
aco Coercion
arg) = Coercion -> [Type] -> Type
go_app Coercion
aco [Coercion -> Type
go Coercion
arg]
go (KindCo Coercion
co) = HasDebugCallStack => Type -> Type
Type -> Type
typeKind (Coercion -> Type
go Coercion
co)
go (SubCo Coercion
co) = Coercion -> Type
go Coercion
co
go (NthCo Role
_ Int
d Coercion
co) = Int -> Type -> Type
go_nth Int
d (Coercion -> Type
go Coercion
co)
go (AxiomInstCo CoAxiom Branched
ax Int
ind [Coercion]
cos) = CoAxiom Branched -> Int -> [Type] -> Type
forall (br :: BranchFlag). CoAxiom br -> Int -> [Type] -> Type
go_ax_inst CoAxiom Branched
ax Int
ind ((Coercion -> Type) -> [Coercion] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
go (AxiomRuleCo CoAxiomRule
ax [Coercion]
cos) = Pair Type -> Type
forall a. Pair a -> a
pSnd (Pair Type -> Type) -> Pair Type -> Type
forall a b. (a -> b) -> a -> b
$ String -> Maybe (Pair Type) -> Pair Type
forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"coercionKind" (Maybe (Pair Type) -> Pair Type) -> Maybe (Pair Type) -> Pair Type
forall a b. (a -> b) -> a -> b
$
CoAxiomRule -> [Pair Type] -> Maybe (Pair Type)
coaxrProves CoAxiomRule
ax ([Pair Type] -> Maybe (Pair Type))
-> [Pair Type] -> Maybe (Pair Type)
forall a b. (a -> b) -> a -> b
$ (Coercion -> Pair Type) -> [Coercion] -> [Pair Type]
forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Pair Type
coercionKind [Coercion]
cos
go co :: Coercion
co@(ForAllCo CoVar
tv1 Coercion
k_co Coercion
co1)
| Coercion -> Bool
isGReflCo Coercion
k_co = CoVar -> Type -> Type
mkTyCoInvForAllTy CoVar
tv1 (Coercion -> Type
go Coercion
co1)
| Bool
otherwise = TCvSubst -> Coercion -> Type
go_forall TCvSubst
empty_subst Coercion
co
where
empty_subst :: TCvSubst
empty_subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ Coercion -> VarSet
tyCoVarsOfCo Coercion
co)
go_ax_inst :: CoAxiom br -> Int -> [Type] -> Type
go_ax_inst CoAxiom br
ax Int
ind [Type]
tys
| CoAxBranch { cab_tvs :: CoAxBranch -> [CoVar]
cab_tvs = [CoVar]
tvs, cab_cvs :: CoAxBranch -> [CoVar]
cab_cvs = [CoVar]
cvs
, cab_rhs :: CoAxBranch -> Type
cab_rhs = Type
rhs } <- CoAxiom br -> Int -> CoAxBranch
forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
ind
, let ([Type]
tys2, [Type]
cotys2) = [CoVar] -> [Type] -> ([Type], [Type])
forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
cos2 :: [Coercion]
cos2 = (Type -> Coercion) -> [Type] -> [Coercion]
forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys2
= ASSERT( tys `equalLength` (tvs ++ cvs) )
HasCallStack => [CoVar] -> [Type] -> Type -> Type
[CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys2 (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos2 Type
rhs
go_app :: Coercion -> [Type] -> Type
go_app :: Coercion -> [Type] -> Type
go_app (InstCo Coercion
co Coercion
arg) [Type]
args = Coercion -> [Type] -> Type
go_app Coercion
co (Coercion -> Type
go Coercion
argType -> [Type] -> [Type]
forall a. a -> [a] -> [a]
:[Type]
args)
go_app Coercion
co [Type]
args = HasDebugCallStack => Type -> [Type] -> Type
Type -> [Type] -> Type
piResultTys (Coercion -> Type
go Coercion
co) [Type]
args
go_forall :: TCvSubst -> Coercion -> Type
go_forall TCvSubst
subst (ForAllCo CoVar
tv1 Coercion
k_co Coercion
co)
| CoVar -> Bool
isTyVar CoVar
tv1
= CoVar -> Type -> Type
mkInfForAllTy CoVar
tv2 (TCvSubst -> Coercion -> Type
go_forall TCvSubst
subst' Coercion
co)
where
k2 :: Type
k2 = Coercion -> Type
coercionRKind Coercion
k_co
tv2 :: CoVar
tv2 = CoVar -> Type -> CoVar
setTyVarKind CoVar
tv1 (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
k2)
subst' :: TCvSubst
subst' | Coercion -> Bool
isGReflCo Coercion
k_co = TCvSubst -> CoVar -> TCvSubst
extendTCvInScope TCvSubst
subst CoVar
tv1
| Bool
otherwise = TCvSubst -> CoVar -> Type -> TCvSubst
extendTvSubst (TCvSubst -> CoVar -> TCvSubst
extendTCvInScope TCvSubst
subst CoVar
tv2) CoVar
tv1 (Type -> TCvSubst) -> Type -> TCvSubst
forall a b. (a -> b) -> a -> b
$
CoVar -> Type
TyVarTy CoVar
tv2 Type -> Coercion -> Type
`mkCastTy` Coercion -> Coercion
mkSymCo Coercion
k_co
go_forall TCvSubst
subst (ForAllCo CoVar
cv1 Coercion
k_co Coercion
co)
| CoVar -> Bool
isCoVar CoVar
cv1
= CoVar -> Type -> Type
mkTyCoInvForAllTy CoVar
cv2 (TCvSubst -> Coercion -> Type
go_forall TCvSubst
subst' Coercion
co)
where
k2 :: Type
k2 = Coercion -> Type
coercionRKind Coercion
k_co
r :: Role
r = CoVar -> Role
coVarRole CoVar
cv1
eta1 :: Coercion
eta1 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
2 (Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal Coercion
k_co)
eta2 :: Coercion
eta2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
3 (Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal Coercion
k_co)
cv2 :: CoVar
cv2 = CoVar -> Type -> CoVar
setVarType CoVar
cv1 (HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst Type
k2)
n_subst :: Coercion
n_subst = Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo` (CoVar -> Coercion
mkCoVarCo CoVar
cv2) Coercion -> Coercion -> Coercion
`mkTransCo` (Coercion -> Coercion
mkSymCo Coercion
eta2)
subst' :: TCvSubst
subst' | Coercion -> Bool
isReflCo Coercion
k_co = TCvSubst -> CoVar -> TCvSubst
extendTCvInScope TCvSubst
subst CoVar
cv1
| Bool
otherwise = TCvSubst -> CoVar -> Coercion -> TCvSubst
extendCvSubst (TCvSubst -> CoVar -> TCvSubst
extendTCvInScope TCvSubst
subst CoVar
cv2)
CoVar
cv1 Coercion
n_subst
go_forall TCvSubst
subst Coercion
other_co
= HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy TCvSubst
subst (Coercion -> Type
go Coercion
other_co)
coercionRole :: Coercion -> Role
coercionRole :: Coercion -> Role
coercionRole = Coercion -> Role
go
where
go :: Coercion -> Role
go (Refl Type
_) = Role
Nominal
go (GRefl Role
r Type
_ MCoercion
_) = Role
r
go (TyConAppCo Role
r TyCon
_ [Coercion]
_) = Role
r
go (AppCo Coercion
co1 Coercion
_) = Coercion -> Role
go Coercion
co1
go (ForAllCo CoVar
_ Coercion
_ Coercion
co) = Coercion -> Role
go Coercion
co
go (FunCo Role
r Coercion
_ Coercion
_ Coercion
_) = Role
r
go (CoVarCo CoVar
cv) = CoVar -> Role
coVarRole CoVar
cv
go (HoleCo CoercionHole
h) = CoVar -> Role
coVarRole (CoercionHole -> CoVar
coHoleCoVar CoercionHole
h)
go (AxiomInstCo CoAxiom Branched
ax Int
_ [Coercion]
_) = CoAxiom Branched -> Role
forall (br :: BranchFlag). CoAxiom br -> Role
coAxiomRole CoAxiom Branched
ax
go (UnivCo UnivCoProvenance
_ Role
r Type
_ Type
_) = Role
r
go (SymCo Coercion
co) = Coercion -> Role
go Coercion
co
go (TransCo Coercion
co1 Coercion
_co2) = Coercion -> Role
go Coercion
co1
go (NthCo Role
r Int
_d Coercion
_co) = Role
r
go (LRCo {}) = Role
Nominal
go (InstCo Coercion
co Coercion
_) = Coercion -> Role
go Coercion
co
go (KindCo {}) = Role
Nominal
go (SubCo Coercion
_) = Role
Representational
go (AxiomRuleCo CoAxiomRule
ax [Coercion]
_) = CoAxiomRule -> Role
coaxrRole CoAxiomRule
ax
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Role
Nominal = Type -> Type -> Type
mkPrimEqPred
mkCoercionType Role
Representational = Type -> Type -> Type
mkReprPrimEqPred
mkCoercionType Role
Phantom = \Type
ty1 Type
ty2 ->
let ki1 :: Type
ki1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
ki2 :: Type
ki2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
in
TyCon -> [Type] -> Type
TyConApp TyCon
eqPhantPrimTyCon [Type
ki1, Type
ki2, Type
ty1, Type
ty2]
mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
mkHeteroCoercionType :: Role -> Type -> Type -> Type -> Type -> Type
mkHeteroCoercionType Role
Nominal = Type -> Type -> Type -> Type -> Type
mkHeteroPrimEqPred
mkHeteroCoercionType Role
Representational = Type -> Type -> Type -> Type -> Type
mkHeteroReprPrimEqPred
mkHeteroCoercionType Role
Phantom = String -> Type -> Type -> Type -> Type -> Type
forall a. String -> a
panic String
"mkHeteroCoercionType"
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred Type
ty1 Type
ty2
= TyCon -> [Type] -> Type
mkTyConApp TyCon
eqPrimTyCon [Type
k1, Type
k2, Type
ty1, Type
ty2]
where
k1 :: Type
k1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
k2 :: Type
k2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
mkPrimEqPredRole :: Role -> Type -> Type -> PredType
mkPrimEqPredRole :: Role -> Type -> Type -> Type
mkPrimEqPredRole Role
Nominal = Type -> Type -> Type
mkPrimEqPred
mkPrimEqPredRole Role
Representational = Type -> Type -> Type
mkReprPrimEqPred
mkPrimEqPredRole Role
Phantom = String -> Type -> Type -> Type
forall a. String -> a
panic String
"mkPrimEqPredRole phantom"
mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
mkHeteroPrimEqPred :: Type -> Type -> Type -> Type -> Type
mkHeteroPrimEqPred Type
k1 Type
k2 Type
ty1 Type
ty2 = TyCon -> [Type] -> Type
mkTyConApp TyCon
eqPrimTyCon [Type
k1, Type
k2, Type
ty1, Type
ty2]
mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
mkHeteroReprPrimEqPred :: Type -> Type -> Type -> Type -> Type
mkHeteroReprPrimEqPred Type
k1 Type
k2 Type
ty1 Type
ty2
= TyCon -> [Type] -> Type
mkTyConApp TyCon
eqReprPrimTyCon [Type
k1, Type
k2, Type
ty1, Type
ty2]
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred Type
ty1 Type
ty2
= TyCon -> [Type] -> Type
mkTyConApp TyCon
eqReprPrimTyCon [Type
k1, Type
k2, Type
ty1, Type
ty2]
where
k1 :: Type
k1 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty1
k2 :: Type
k2 = HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty2
buildCoercion :: Type -> Type -> CoercionN
buildCoercion :: Type -> Type -> Coercion
buildCoercion Type
orig_ty1 Type
orig_ty2 = Type -> Type -> Coercion
go Type
orig_ty1 Type
orig_ty2
where
go :: Type -> Type -> Coercion
go Type
ty1 Type
ty2 | Just Type
ty1' <- Type -> Maybe Type
coreView Type
ty1 = Type -> Type -> Coercion
go Type
ty1' Type
ty2
| Just Type
ty2' <- Type -> Maybe Type
coreView Type
ty2 = Type -> Type -> Coercion
go Type
ty1 Type
ty2'
go (CastTy Type
ty1 Coercion
co) Type
ty2
= let co' :: Coercion
co' = Type -> Type -> Coercion
go Type
ty1 Type
ty2
r :: Role
r = Coercion -> Role
coercionRole Coercion
co'
in Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
r Type
ty1 Coercion
co Coercion
co'
go Type
ty1 (CastTy Type
ty2 Coercion
co)
= let co' :: Coercion
co' = Type -> Type -> Coercion
go Type
ty1 Type
ty2
r :: Role
r = Coercion -> Role
coercionRole Coercion
co'
in Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty2 Coercion
co Coercion
co'
go ty1 :: Type
ty1@(TyVarTy CoVar
tv1) Type
_tyvarty
= ASSERT( case _tyvarty of
{ TyVarTy tv2 -> tv1 == tv2
; _ -> False } )
Type -> Coercion
mkNomReflCo Type
ty1
go (FunTy { ft_mult :: Type -> Type
ft_mult = Type
w1, ft_arg :: Type -> Type
ft_arg = Type
arg1, ft_res :: Type -> Type
ft_res = Type
res1 })
(FunTy { ft_mult :: Type -> Type
ft_mult = Type
w2, ft_arg :: Type -> Type
ft_arg = Type
arg2, ft_res :: Type -> Type
ft_res = Type
res2 })
= Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
Nominal (Type -> Type -> Coercion
go Type
w1 Type
w2) (Type -> Type -> Coercion
go Type
arg1 Type
arg2) (Type -> Type -> Coercion
go Type
res1 Type
res2)
go (TyConApp TyCon
tc1 [Type]
args1) (TyConApp TyCon
tc2 [Type]
args2)
= ASSERT( tc1 == tc2 )
HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Nominal TyCon
tc1 ((Type -> Type -> Coercion) -> [Type] -> [Type] -> [Coercion]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Type -> Type -> Coercion
go [Type]
args1 [Type]
args2)
go (AppTy Type
ty1a Type
ty1b) Type
ty2
| Just (Type
ty2a, Type
ty2b) <- HasDebugCallStack => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
repSplitAppTy_maybe Type
ty2
= Coercion -> Coercion -> Coercion
mkAppCo (Type -> Type -> Coercion
go Type
ty1a Type
ty2a) (Type -> Type -> Coercion
go Type
ty1b Type
ty2b)
go Type
ty1 (AppTy Type
ty2a Type
ty2b)
| Just (Type
ty1a, Type
ty1b) <- HasDebugCallStack => Type -> Maybe (Type, Type)
Type -> Maybe (Type, Type)
repSplitAppTy_maybe Type
ty1
= Coercion -> Coercion -> Coercion
mkAppCo (Type -> Type -> Coercion
go Type
ty1a Type
ty2a) (Type -> Type -> Coercion
go Type
ty1b Type
ty2b)
go (ForAllTy (Bndr CoVar
tv1 ArgFlag
_flag1) Type
ty1) (ForAllTy (Bndr CoVar
tv2 ArgFlag
_flag2) Type
ty2)
| CoVar -> Bool
isTyVar CoVar
tv1
= ASSERT( isTyVar tv2 )
CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
tv1 Coercion
kind_co (Type -> Type -> Coercion
go Type
ty1 Type
ty2')
where kind_co :: Coercion
kind_co = Type -> Type -> Coercion
go (CoVar -> Type
tyVarKind CoVar
tv1) (CoVar -> Type
tyVarKind CoVar
tv2)
in_scope :: InScopeSet
in_scope = VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ Type -> VarSet
tyCoVarsOfType Type
ty2 VarSet -> VarSet -> VarSet
`unionVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
kind_co
ty2' :: Type
ty2' = InScopeSet -> [CoVar] -> [Type] -> Type -> Type
substTyWithInScope InScopeSet
in_scope [CoVar
tv2]
[CoVar -> Type
mkTyVarTy CoVar
tv1 Type -> Coercion -> Type
`mkCastTy` Coercion
kind_co]
Type
ty2
go (ForAllTy (Bndr CoVar
cv1 ArgFlag
_flag1) Type
ty1) (ForAllTy (Bndr CoVar
cv2 ArgFlag
_flag2) Type
ty2)
= ASSERT( isCoVar cv1 && isCoVar cv2 )
CoVar -> Coercion -> Coercion -> Coercion
mkForAllCo CoVar
cv1 Coercion
kind_co (Type -> Type -> Coercion
go Type
ty1 Type
ty2')
where s1 :: Type
s1 = CoVar -> Type
varType CoVar
cv1
s2 :: Type
s2 = CoVar -> Type
varType CoVar
cv2
kind_co :: Coercion
kind_co = Type -> Type -> Coercion
go Type
s1 Type
s2
r :: Role
r = CoVar -> Role
coVarRole CoVar
cv1
kind_co' :: Coercion
kind_co' = Role -> Role -> Coercion -> Coercion
downgradeRole Role
r Role
Nominal Coercion
kind_co
eta1 :: Coercion
eta1 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
2 Coercion
kind_co'
eta2 :: Coercion
eta2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
3 Coercion
kind_co'
subst :: TCvSubst
subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst (InScopeSet -> TCvSubst) -> InScopeSet -> TCvSubst
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$
Type -> VarSet
tyCoVarsOfType Type
ty2 VarSet -> VarSet -> VarSet
`unionVarSet` Coercion -> VarSet
tyCoVarsOfCo Coercion
kind_co
ty2' :: Type
ty2' = HasCallStack => TCvSubst -> Type -> Type
TCvSubst -> Type -> Type
substTy (TCvSubst -> CoVar -> Coercion -> TCvSubst
extendCvSubst TCvSubst
subst CoVar
cv2 (Coercion -> TCvSubst) -> Coercion -> TCvSubst
forall a b. (a -> b) -> a -> b
$ Coercion -> Coercion
mkSymCo Coercion
eta1 Coercion -> Coercion -> Coercion
`mkTransCo`
CoVar -> Coercion
mkCoVarCo CoVar
cv1 Coercion -> Coercion -> Coercion
`mkTransCo`
Coercion
eta2)
Type
ty2
go ty1 :: Type
ty1@(LitTy TyLit
lit1) Type
_lit2
= ASSERT( case _lit2 of
{ LitTy lit2 -> lit1 == lit2
; _ -> False } )
Type -> Coercion
mkNomReflCo Type
ty1
go (CoercionTy Coercion
co1) (CoercionTy Coercion
co2)
= Role -> Coercion -> Coercion -> Coercion -> Coercion
mkProofIrrelCo Role
Nominal Coercion
kind_co Coercion
co1 Coercion
co2
where
kind_co :: Coercion
kind_co = Type -> Type -> Coercion
go (Coercion -> Type
coercionType Coercion
co1) (Coercion -> Type
coercionType Coercion
co2)
go Type
ty1 Type
ty2
= String -> SDoc -> Coercion
forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"buildKindCoercion" ([SDoc] -> SDoc
vcat [ Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_ty1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
orig_ty2
, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty1, Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty2 ])
{-# INLINE simplifyArgsWorker #-}
simplifyArgsWorker :: [TyCoBinder] -> Kind
-> TyCoVarSet
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], CoercionN)
simplifyArgsWorker :: [TyCoBinder]
-> Type
-> VarSet
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], Coercion)
simplifyArgsWorker [TyCoBinder]
orig_ki_binders Type
orig_inner_ki VarSet
orig_fvs
[Role]
orig_roles [(Type, Coercion)]
orig_simplified_args
= [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Type
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], Coercion)
go [] [] LiftingContext
orig_lc [TyCoBinder]
orig_ki_binders Type
orig_inner_ki [Role]
orig_roles [(Type, Coercion)]
orig_simplified_args
where
orig_lc :: LiftingContext
orig_lc = InScopeSet -> LiftingContext
emptyLiftingContext (InScopeSet -> LiftingContext) -> InScopeSet -> LiftingContext
forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet (VarSet -> InScopeSet) -> VarSet -> InScopeSet
forall a b. (a -> b) -> a -> b
$ VarSet
orig_fvs
go :: [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Kind
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], CoercionN)
go :: [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Type
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], Coercion)
go [Type]
acc_xis [Coercion]
acc_cos !LiftingContext
lc [TyCoBinder]
binders Type
inner_ki [Role]
_ []
= ([Type] -> [Type]
forall a. [a] -> [a]
reverse [Type]
acc_xis, [Coercion] -> [Coercion]
forall a. [a] -> [a]
reverse [Coercion]
acc_cos, Coercion
kind_co)
where
final_kind :: Type
final_kind = [TyCoBinder] -> Type -> Type
mkPiTys [TyCoBinder]
binders Type
inner_ki
kind_co :: Coercion
kind_co = HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc Type
final_kind
go [Type]
acc_xis [Coercion]
acc_cos LiftingContext
lc (TyCoBinder
binder:[TyCoBinder]
binders) Type
inner_ki (Role
role:[Role]
roles) ((Type
xi,Coercion
co):[(Type, Coercion)]
args)
=
let !kind_co :: Coercion
kind_co = Coercion -> Coercion
mkSymCo (Coercion -> Coercion) -> Coercion -> Coercion
forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc (TyCoBinder -> Type
tyCoBinderType TyCoBinder
binder)
!casted_xi :: Type
casted_xi = Type
xi Type -> Coercion -> Type
`mkCastTy` Coercion
kind_co
casted_co :: Coercion
casted_co = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
role Type
xi Coercion
kind_co Coercion
co
!new_lc :: LiftingContext
new_lc | Just CoVar
tv <- TyCoBinder -> Maybe CoVar
tyCoBinderVar_maybe TyCoBinder
binder
= LiftingContext -> CoVar -> Coercion -> LiftingContext
extendLiftingContextAndInScope LiftingContext
lc CoVar
tv Coercion
casted_co
| Bool
otherwise
= LiftingContext
lc
in
[Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Type
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], Coercion)
go (Type
casted_xi Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
acc_xis)
(Coercion
casted_co Coercion -> [Coercion] -> [Coercion]
forall a. a -> [a] -> [a]
: [Coercion]
acc_cos)
LiftingContext
new_lc
[TyCoBinder]
binders
Type
inner_ki
[Role]
roles
[(Type, Coercion)]
args
go [Type]
acc_xis [Coercion]
acc_cos LiftingContext
lc [] Type
inner_ki [Role]
roles [(Type, Coercion)]
args
= 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
unflattened_tys :: [Type]
unflattened_tys = ((Type, Coercion) -> Type) -> [(Type, Coercion)] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Coercion -> Type
coercionRKind (Coercion -> Type)
-> ((Type, Coercion) -> Coercion) -> (Type, Coercion) -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Type, Coercion) -> Coercion
forall a b. (a, b) -> b
snd) [(Type, Coercion)]
args
([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]
unflattened_tys
casted_args :: [(Type, Coercion)]
casted_args = ASSERT2( equalLength args arg_cos
, ppr args $$ ppr arg_cos )
[ (Type
casted_xi, Coercion
casted_co)
| ((Type
xi, Coercion
co), Coercion
arg_co, Role
role) <- [(Type, Coercion)]
-> [Coercion] -> [Role] -> [((Type, Coercion), Coercion, Role)]
forall a b c. [a] -> [b] -> [c] -> [(a, b, c)]
zip3 [(Type, Coercion)]
args [Coercion]
arg_cos [Role]
roles
, let casted_xi :: Type
casted_xi = Type
xi Type -> Coercion -> Type
`mkCastTy` Coercion
arg_co
casted_co :: Coercion
casted_co = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceLeftCo Role
role Type
xi Coercion
arg_co Coercion
co ]
zapped_lc :: LiftingContext
zapped_lc = LiftingContext -> LiftingContext
zapLiftingContext LiftingContext
lc
Pair Type
flattened_kind Type
_ = Pair Type
co1_kind
([TyCoBinder]
bndrs, Type
new_inner) = Type -> ([TyCoBinder], Type)
splitPiTys Type
flattened_kind
([Type]
xis_out, [Coercion]
cos_out, Coercion
res_co_out)
= [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Type
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], Coercion)
go [Type]
acc_xis [Coercion]
acc_cos LiftingContext
zapped_lc [TyCoBinder]
bndrs Type
new_inner [Role]
roles [(Type, Coercion)]
casted_args
in
([Type]
xis_out, [Coercion]
cos_out, Coercion
res_co_out Coercion -> Coercion -> Coercion
`mkTransCo` Coercion
res_co)
go [Type]
_ [Coercion]
_ LiftingContext
_ [TyCoBinder]
_ Type
_ [Role]
_ [(Type, Coercion)]
_ = String -> ([Type], [Coercion], Coercion)
forall a. String -> a
panic
String
"simplifyArgsWorker wandered into deeper water than usual"
bad_co_hole_ty :: Type -> Monoid.Any
bad_co_hole_co :: Coercion -> Monoid.Any
(Type -> Any
bad_co_hole_ty, [Type] -> Any
_, Coercion -> Any
bad_co_hole_co, [Coercion] -> Any
_)
= TyCoFolder () Any
-> ()
-> (Type -> Any, [Type] -> Any, Coercion -> Any, [Coercion] -> Any)
forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder () Any
forall b. TyCoFolder b Any
folder ()
where
folder :: TyCoFolder b Any
folder = TyCoFolder :: forall env a.
(Type -> Maybe Type)
-> (env -> CoVar -> a)
-> (env -> CoVar -> a)
-> (env -> CoercionHole -> a)
-> (env -> CoVar -> ArgFlag -> env)
-> TyCoFolder env a
TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = Maybe Type -> Type -> Maybe Type
forall a b. a -> b -> a
const Maybe Type
forall a. Maybe a
Nothing
, tcf_tyvar :: b -> CoVar -> Any
tcf_tyvar = Any -> b -> CoVar -> Any
forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
, tcf_covar :: b -> CoVar -> Any
tcf_covar = Any -> b -> CoVar -> Any
forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
, tcf_hole :: b -> CoercionHole -> Any
tcf_hole = (CoercionHole -> Any) -> b -> CoercionHole -> Any
forall a b. a -> b -> a
const CoercionHole -> Any
hole
, tcf_tycobinder :: b -> CoVar -> ArgFlag -> b
tcf_tycobinder = b -> CoVar -> ArgFlag -> b
forall a b c. a -> b -> c -> a
const2
}
const2 :: a -> b -> c -> a
const2 :: a -> b -> c -> a
const2 a
x b
_ c
_ = a
x
hole :: CoercionHole -> Monoid.Any
hole :: CoercionHole -> Any
hole (CoercionHole { ch_blocker :: CoercionHole -> BlockSubstFlag
ch_blocker = BlockSubstFlag
YesBlockSubst }) = Bool -> Any
Monoid.Any Bool
True
hole CoercionHole
_ = Bool -> Any
Monoid.Any Bool
False
badCoercionHole :: Type -> Bool
badCoercionHole :: Type -> Bool
badCoercionHole = Any -> Bool
Monoid.getAny (Any -> Bool) -> (Type -> Any) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Any
bad_co_hole_ty
badCoercionHoleCo :: Coercion -> Bool
badCoercionHoleCo :: Coercion -> Bool
badCoercionHoleCo = Any -> Bool
Monoid.getAny (Any -> Bool) -> (Coercion -> Any) -> Coercion -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Any
bad_co_hole_co