{-# LANGUAGE CPP #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
module GHC.Core.Coercion (
Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionN, MCoercionR,
UnivCoProvenance, CoercionHole(..),
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,
mkNthCo, mkNthCoFunCo, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunResCo,
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, mkGReflLeftMCo, mkGReflRightMCo,
mkCoherenceRightMCo,
coToMCo, mkTransMCo, mkTransMCoL, mkTransMCoR, mkCastTyMCo, mkSymMCo,
mkHomoForAllMCo, mkFunResMCo, mkPiMCos, checkReflexiveMCo,
isReflMCo,
mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
isCoVar_maybe,
tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
tyCoFVsOfCo, tyCoFVsOfCos, tyCoVarsOfCoDSet,
coercionSize, anyFreeVarsOfCo,
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,
hasCoercionHoleTy, hasCoercionHoleCo,
HoleSet, coercionHolesOfType, coercionHolesOfCo
) where
#include "HsVersions.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.TyCon.RecWalk
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.Types.Basic
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 GHC.Types.Unique.Set
import GHC.Utils.Misc
import GHC.Utils.Outputable
import GHC.Utils.Panic
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 forall a. [a] -> [a] -> [a]
++ [CoVar]
eta_tvs, [Type]
lhs 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 :: forall (br :: BranchFlag). 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
<+> forall a. Outputable a => a -> SDoc
ppr CoAxiom br
ax SDoc -> SDoc -> SDoc
<+> SDoc
dcolon)
Int
2 ([SDoc] -> SDoc
vcat (forall a b. (a -> b) -> [a] -> [b]
map (TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser TyCon
tc) (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 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
= forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 (forall a b c. (a -> b -> c) -> b -> a -> c
flip SDoc -> Int -> SDoc -> SDoc
hangNotEmpty Int
2)
[ [TyCoVarBinder] -> SDoc
pprUserForAll (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
<+> forall a. Outputable a => a -> SDoc
ppr (SrcSpan -> SrcLoc
srcSpanStart SrcSpan
loc)
| Bool
otherwise = String -> SDoc
text String
"in" SDoc -> SDoc -> 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, forall a. [a] -> [a]
reverse [CoVar]
tidy_bndrs)
where
(TidyEnv
tidy_env, [CoVar]
tidy_bndrs) = 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' 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, 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 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 (forall a. NamedThing a => a -> OccName
getOccName CoVar
tv) of
(Char
'_' : String
rest) -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Char -> Bool
isDigit String
rest
String
_ -> Bool
False
coToMCo :: Coercion -> MCoercion
coToMCo :: Coercion -> MCoercion
coToMCo Coercion
co | Coercion -> Bool
isReflCo Coercion
co = MCoercion
MRefl
| Bool
otherwise = Coercion -> MCoercion
MCo Coercion
co
checkReflexiveMCo :: MCoercion -> MCoercion
checkReflexiveMCo :: MCoercion -> MCoercion
checkReflexiveMCo MCoercion
MRefl = MCoercion
MRefl
checkReflexiveMCo (MCo Coercion
co) | Coercion -> Bool
isReflexiveCo Coercion
co = MCoercion
MRefl
| Bool
otherwise = Coercion -> MCoercion
MCo Coercion
co
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
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 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
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)
mkTransMCoL :: MCoercion -> Coercion -> MCoercion
mkTransMCoL :: MCoercion -> Coercion -> MCoercion
mkTransMCoL MCoercion
MRefl Coercion
co2 = Coercion -> MCoercion
coToMCo Coercion
co2
mkTransMCoL (MCo Coercion
co1) Coercion
co2 = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)
mkTransMCoR :: Coercion -> MCoercion -> MCoercion
mkTransMCoR :: Coercion -> MCoercion -> MCoercion
mkTransMCoR Coercion
co1 MCoercion
MRefl = Coercion -> MCoercion
coToMCo Coercion
co1
mkTransMCoR Coercion
co1 (MCo Coercion
co2) = Coercion -> MCoercion
MCo (Coercion -> Coercion -> Coercion
mkTransCo Coercion
co1 Coercion
co2)
mkSymMCo :: MCoercion -> MCoercion
mkSymMCo :: MCoercion -> MCoercion
mkSymMCo MCoercion
MRefl = MCoercion
MRefl
mkSymMCo (MCo Coercion
co) = Coercion -> MCoercion
MCo (Coercion -> Coercion
mkSymCo Coercion
co)
mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo :: Type -> MCoercion -> Type
mkCastTyMCo Type
ty MCoercion
MRefl = Type
ty
mkCastTyMCo Type
ty (MCo Coercion
co) = Type
ty Type -> Coercion -> Type
`mkCastTy` Coercion
co
mkHomoForAllMCo :: TyCoVar -> MCoercion -> MCoercion
mkHomoForAllMCo :: CoVar -> MCoercion -> MCoercion
mkHomoForAllMCo CoVar
_ MCoercion
MRefl = MCoercion
MRefl
mkHomoForAllMCo CoVar
tcv (MCo Coercion
co) = Coercion -> MCoercion
MCo ([CoVar] -> Coercion -> Coercion
mkHomoForAllCos [CoVar
tcv] Coercion
co)
mkPiMCos :: [Var] -> MCoercion -> MCoercion
mkPiMCos :: [CoVar] -> MCoercion -> MCoercion
mkPiMCos [CoVar]
_ MCoercion
MRefl = MCoercion
MRefl
mkPiMCos [CoVar]
vs (MCo Coercion
co) = Coercion -> MCoercion
MCo (Role -> [CoVar] -> Coercion -> Coercion
mkPiCos Role
Representational [CoVar]
vs Coercion
co)
mkFunResMCo :: Scaled Type -> MCoercionR -> MCoercionR
mkFunResMCo :: Scaled Type -> MCoercion -> MCoercion
mkFunResMCo Scaled Type
_ MCoercion
MRefl = MCoercion
MRefl
mkFunResMCo Scaled Type
arg_ty (MCo Coercion
co) = Coercion -> MCoercion
MCo (Role -> Scaled Type -> Coercion -> Coercion
mkFunResCo Role
Representational Scaled Type
arg_ty Coercion
co)
mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflLeftMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflLeftMCo Role
r Type
ty MCoercion
MRefl = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
mkGReflLeftMCo Role
r Type
ty (MCo Coercion
co) = Role -> Type -> Coercion -> Coercion
mkGReflLeftCo Role
r Type
ty Coercion
co
mkGReflRightMCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflRightMCo :: Role -> Type -> MCoercion -> Coercion
mkGReflRightMCo Role
r Type
ty MCoercion
MRefl = Role -> Type -> Coercion
mkReflCo Role
r Type
ty
mkGReflRightMCo Role
r Type
ty (MCo Coercion
co) = Role -> Type -> Coercion -> Coercion
mkGReflRightCo Role
r Type
ty Coercion
co
mkCoherenceRightMCo :: Role -> Type -> MCoercionN -> Coercion -> Coercion
mkCoherenceRightMCo :: Role -> Type -> MCoercion -> Coercion -> Coercion
mkCoherenceRightMCo Role
_ Type
_ MCoercion
MRefl Coercion
co2 = Coercion
co2
mkCoherenceRightMCo Role
r Type
ty (MCo Coercion
co) Coercion
co2 = Role -> Type -> Coercion -> Coercion -> Coercion
mkCoherenceRightCo Role
r Type
ty Coercion
co Coercion
co2
isReflMCo :: MCoercion -> Bool
isReflMCo :: MCoercion -> Bool
isReflMCo MCoercion
MRefl = Bool
True
isReflMCo MCoercion
_ = Bool
False
decomposeCo :: Arity -> Coercion
-> [Role]
-> [Coercion]
decomposeCo :: Int -> Coercion -> [Role] -> [Coercion]
decomposeCo Int
arity Coercion
co [Role]
rs
= [HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
n Coercion
co | (Int
n,Role
r) <- [Int
0..(Int
arityforall a. Num a => a -> a -> a
-Int
1)] forall a b. [a] -> [b] -> [(a, b)]
`zip` [Role]
rs ]
decomposeFunCo :: HasDebugCallStack
=> Role
-> Coercion
-> (CoercionN, Coercion, Coercion)
decomposeFunCo :: HasDebugCallStack =>
Role -> Coercion -> (Coercion, Coercion, Coercion)
decomposeFunCo Role
r Coercion
co = ASSERT2( all_ok, ppr co )
(HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
0 Coercion
co, HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
3 Coercion
co, HasDebugCallStack => 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 :: HasDebugCallStack =>
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 forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet 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)
splitForAllTyCoVar_maybe Type
k1
, Just (CoVar
b, Type
t2) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
k2
= let arg_co :: Coercion
arg_co = HasDebugCallStack => 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 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)
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 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
substTy TCvSubst
subst1 Type
k1)
Coercion
co
(TCvSubst -> TCvSubst
zapTCvSubst TCvSubst
subst2, HasCallStack => TCvSubst -> Type -> Type
substTy TCvSubst
subst1 Type
k2)
(Type
tyforall a. a -> [a] -> [a]
:[Type]
tys)
go [Coercion]
acc_arg_cos (TCvSubst, Type)
_ki1 Coercion
co (TCvSubst, Type)
_ki2 [Type]
_tys = (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) = forall a. a -> Maybe a
Just CoVar
cv
getCoVar_maybe Coercion
_ = 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])
splitTyConApp_maybe Type
ty
; let args :: [Coercion]
args = 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
; forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon
tc, [Coercion]
args) }
splitTyConAppCo_maybe (TyConAppCo Role
_ TyCon
tc [Coercion]
cos) = forall a. a -> Maybe a
Just (TyCon
tc, [Coercion]
cos)
splitTyConAppCo_maybe (FunCo Role
_ Coercion
w Coercion
arg Coercion
res) = forall a. a -> Maybe a
Just (TyCon
funTyCon, [Coercion]
cos)
where cos :: [Coercion]
cos = [Coercion
w, HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo Coercion
arg, HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo Coercion
res, Coercion
arg, Coercion
res]
splitTyConAppCo_maybe 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) = forall a. a -> Maybe a
Just (Coercion
co, Coercion
arg)
splitAppCo_maybe (TyConAppCo Role
r TyCon
tc [Coercion]
args)
| [Coercion]
args forall a. [a] -> Int -> Bool
`lengthExceeds` TyCon -> Int
tyConArity TyCon
tc
, Just ([Coercion]
args', Coercion
arg') <- forall a. [a] -> Maybe ([a], a)
snocView [Coercion]
args
= forall a. a -> Maybe a
Just ( HasDebugCallStack => 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') <- 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 (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Coercion]
args')) Coercion
arg'
= forall a. a -> Maybe a
Just ( HasDebugCallStack => 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
= forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo Role
r Type
ty1, Type -> Coercion
mkNomReflCo Type
ty2)
splitAppCo_maybe 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) = forall a. a -> Maybe a
Just (Coercion
arg, Coercion
res)
splitFunCo_maybe 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) = forall a. a -> Maybe a
Just (CoVar
tv, Coercion
k_co, Coercion
co)
splitForAllCo_maybe 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 = forall a. a -> Maybe a
Just (CoVar
tv, Coercion
k_co, Coercion
co)
splitForAllCo_ty_maybe 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 = forall a. a -> Maybe a
Just (CoVar
cv, Coercion
k_co, Coercion
co)
splitForAllCo_co_maybe Coercion
_ = forall a. Maybe a
Nothing
coVarLType, coVarRType :: HasDebugCallStack => CoVar -> Type
coVarLType :: HasDebugCallStack => CoVar -> Type
coVarLType CoVar
cv | (Type
_, Type
_, Type
ty1, Type
_, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv = Type
ty1
coVarRType :: HasDebugCallStack => CoVar -> Type
coVarRType CoVar
cv | (Type
_, Type
_, Type
_, Type
ty2, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv = Type
ty2
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes CoVar
cv
| (Type
_, Type
_, Type
ty1, Type
ty2, Role
_) <- HasDebugCallStack => CoVar -> (Type, Type, Type, Type, Role)
coVarKindsTypesRole CoVar
cv
= forall a. a -> a -> Pair a
Pair Type
ty1 Type
ty2
coVarKindsTypesRole :: HasDebugCallStack => CoVar -> (Kind,Kind,Type,Type,Role)
coVarKindsTypesRole :: HasDebugCallStack => 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])
splitTyConApp_maybe (CoVar -> Type
varType CoVar
cv)
= (Type
k1, Type
k2, Type
ty1, Type
ty2, TyCon -> Role
eqTyConRole TyCon
tc)
| Bool
otherwise
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coVarKindsTypesRole, non coercion variable"
(forall a. Outputable a => a -> SDoc
ppr CoVar
cv SDoc -> SDoc -> 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 -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coVarRole: not tyconapp" (forall a. Outputable a => a -> SDoc
ppr CoVar
cv))
eqTyConRole :: TyCon -> Role
eqTyConRole :: TyCon -> Role
eqTyConRole TyCon
tc
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqPrimTyConKey
= Role
Nominal
| TyCon
tc forall a. Uniquable a => a -> Unique -> Bool
`hasKey` Unique
eqReprPrimTyConKey
= Role
Representational
| Bool
otherwise
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"eqTyConRole: unknown tycon" (forall a. Outputable a => a -> SDoc
ppr TyCon
tc)
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo Coercion
co
= HasDebugCallStack => 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
coVarTypes CoVar
cv
, Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2
= forall a. a -> Maybe a
Just (Role -> Type -> Coercion
mkReflCo (CoVar -> Role
coVarRole CoVar
cv) Type
ty1)
| Bool
otherwise
= forall a. Maybe a
Nothing
isGReflCo :: Coercion -> Bool
isGReflCo :: Coercion -> Bool
isGReflCo (GRefl{}) = Bool
True
isGReflCo (Refl{}) = Bool
True
isGReflCo Coercion
_ = 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
_) = forall a. a -> Maybe a
Just (Type
ty, Role
r)
isGReflCo_maybe (Refl Type
ty) = forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isGReflCo_maybe Coercion
_ = forall a. Maybe a
Nothing
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl Type
ty) = forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isReflCo_maybe (GRefl Role
r Type
ty MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = forall a. a -> Maybe a
Just (Type
ty, Role
r)
isReflCo_maybe Coercion
_ = forall a. Maybe a
Nothing
isReflexiveCo :: Coercion -> Bool
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = forall a. Maybe a -> Bool
isJust 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) = forall a. a -> Maybe a
Just (Type
ty, Role
Nominal)
isReflexiveCo_maybe (GRefl Role
r Type
ty MCoercion
mco) | MCoercion -> Bool
isGReflMCo MCoercion
mco = forall a. a -> Maybe a
Just (Type
ty, Role
r)
isReflexiveCo_maybe Coercion
co
| Type
ty1 Type -> Type -> Bool
`eqType` Type
ty2
= forall a. a -> Maybe a
Just (Type
ty1, Role
r)
| Bool
otherwise
= forall a. Maybe a
Nothing
where (Pair Type
ty1 Type
ty2, Role
r) = Coercion -> (Pair Type, Role)
coercionKindRole Coercion
co
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 :: HasDebugCallStack => 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) <- forall tyco.
TyCon -> [tyco] -> Maybe ([(CoVar, tyco)], Type, [tyco])
expandSynTyCon_maybe TyCon
tc [Coercion]
cos
= Coercion -> [Coercion] -> Coercion
mkAppCos (HasDebugCallStack => 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 <- 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 (forall a b. (a -> b) -> [a] -> [b]
map 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])
splitTyConApp_maybe Type
ty1
= HasDebugCallStack => 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 forall a. a -> [a] -> [a]
: [Role] -> [Type] -> [Coercion]
zip_roles [Role]
rs [Type]
tys
zip_roles [Role]
_ [Type]
_ = 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
mkTyConAppCo Role
Nominal TyCon
tc ([Coercion]
args forall a. [a] -> [a] -> [a]
++ [Coercion
arg])
Role
Representational -> HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo Role
Representational TyCon
tc ([Coercion]
args forall a. [a] -> [a] -> [a]
++ [Coercion
arg'])
where new_role :: Role
new_role = (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc) forall a. [a] -> Int -> a
!! (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
mkTyConAppCo Role
Phantom TyCon
tc ([Coercion]
args 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 = 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) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Coercion -> Bool
isReflCo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall a. [a] -> [a]
reverse [(CoVar, Coercion)]
bndrs) in
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. (a -> b) -> a -> b
$ 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 (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(CoVar, Coercion)]
refls_rev'd)) Type
ty))
[(CoVar, Coercion)]
non_refls_rev'd
| Bool
otherwise
= forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (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))
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 = 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) = forall a. a -> Maybe a
Just CoVar
cv
isCoVar_maybe Coercion
_ = forall a. Maybe a
Nothing
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
-> Coercion
mkAxInstCo :: forall (br :: BranchFlag).
Role -> CoAxiom br -> Int -> [Type] -> [Coercion] -> Coercion
mkAxInstCo Role
role CoAxiom br
ax Int
index [Type]
tys [Coercion]
cos
| Int
arity forall a. Eq a => a -> a -> Bool
== Int
n_tys = Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
ax_role forall a b. (a -> b) -> a -> b
$
CoAxiom Branched -> Int -> [Coercion] -> Coercion
mkAxiomInstCo CoAxiom Branched
ax_br Int
index ([Coercion]
rtys forall a. [a] -> [a] -> [a]
`chkAppend` [Coercion]
cos)
| Bool
otherwise = ASSERT( arity < n_tys )
Role -> Role -> Coercion -> Coercion
downgradeRole Role
role Role
ax_role 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 forall a. [a] -> [a] -> [a]
`chkAppend` [Coercion]
cos))
[Coercion]
leftover_args
where
n_tys :: Int
n_tys = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys
ax_br :: CoAxiom Branched
ax_br = forall (br :: BranchFlag). CoAxiom br -> CoAxiom Branched
toBranchedAxiom CoAxiom br
ax
branch :: CoAxBranch
branch = 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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [CoVar]
tvs
arg_roles :: [Role]
arg_roles = CoAxBranch -> [Role]
coAxBranchRoles CoAxBranch
branch
rtys :: [Coercion]
rtys = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Role -> Type -> Coercion
mkReflCo ([Role]
arg_roles forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Role
Nominal) [Type]
tys
([Coercion]
ax_args, [Coercion]
leftover_args)
= forall a. Int -> [a] -> ([a], [a])
splitAt Int
arity [Coercion]
rtys
ax_role :: Role
ax_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
= 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 :: forall (br :: BranchFlag).
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 = 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) = forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
rhs' :: Type
rhs' = HasCallStack => [CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys1 forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos 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 = forall (br :: BranchFlag).
CoAxiom br -> Int -> [Type] -> [Coercion] -> Type
mkAxInstRHS CoAxiom Unbranched
ax Int
0
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstLHS :: forall (br :: BranchFlag).
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 forall a. [a] -> [a] -> [a]
`chkAppend` [Type]
tys2)
where
branch :: CoAxBranch
branch = 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) = 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 forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> [Type] -> [Type]
substTysWithCoVars [CoVar]
cvs [Coercion]
cos forall a b. (a -> b) -> a -> b
$
CoAxBranch -> [Type]
coAxBranchLHS CoAxBranch
branch
fam_tc :: TyCon
fam_tc = 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 = 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 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
mkNthCo :: HasDebugCallStack
=> Role
-> Int
-> Coercion
-> Coercion
mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
n Coercion
co
= ASSERT2( good_call, bad_call_msg )
Int -> Coercion -> Coercion
go Int
n Coercion
co
where
Pair Type
ty1 Type
ty2 = Coercion -> Pair Type
coercionKind Coercion
co
go :: Int -> Coercion -> Coercion
go Int
0 Coercion
co
| Just (Type
ty, Role
_) <- Coercion -> Maybe (Type, Role)
isReflCo_maybe Coercion
co
, Just (CoVar
tv, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty
=
ASSERT( r == Nominal )
Type -> Coercion
mkNomReflCo (CoVar -> Type
varType CoVar
tv)
go 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])
splitTyConApp_maybe Type
ty
= [Type]
tys forall a. [a] -> Int -> Bool
`lengthExceeds` Int
n
| Type -> Bool
isForAllTy Type
ty
= Int
n forall a. Eq a => a -> a -> Bool
== Int
0
| Bool
otherwise
= Bool
False
go Int
0 (ForAllCo CoVar
_ Coercion
kind_co Coercion
_)
= ASSERT( r == Nominal )
Coercion
kind_co
go Int
n (FunCo Role
_ Coercion
w Coercion
arg Coercion
res)
= Int -> Coercion -> Coercion -> Coercion -> Coercion
mkNthCoFunCo Int
n Coercion
w Coercion
arg Coercion
res
go 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 forall a. Outputable a => [a] -> Int -> a
`getNth` Int
n
go Int
n (SymCo Coercion
co)
= Coercion -> Coercion
mkSymCo (Int -> Coercion -> Coercion
go Int
n Coercion
co)
go 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
<+> forall a. Outputable a => a -> SDoc
ppr Coercion
co
, String -> SDoc
text String
"LHS ty =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
ty1
, String -> SDoc
text String
"RHS ty =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Type
ty2
, String -> SDoc
text String
"n =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Int
n, String -> SDoc
text String
"r =" SDoc -> SDoc -> SDoc
<+> forall a. Outputable a => a -> SDoc
ppr Role
r
, String -> SDoc
text String
"coercion role =" SDoc -> SDoc -> 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)
splitForAllTyCoVar_maybe Type
ty1
, Just (CoVar
_tv2, Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty2
= Int
n forall a. Eq a => a -> a -> Bool
== Int
0 Bool -> Bool -> Bool
&& Role
r forall a. Eq a => a -> a -> Bool
== Role
Nominal
| Just (TyCon
tc1, [Type]
tys1) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty1
, Just (TyCon
tc2, [Type]
tys2) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty2
, TyCon
tc1 forall a. Eq a => a -> a -> Bool
== TyCon
tc2
= let len1 :: Int
len1 = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
tys1
len2 :: Int
len2 = 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 forall a. Eq a => a -> a -> Bool
== Role
Nominal
Role
Representational -> Role
r forall a. Eq a => a -> a -> Bool
== (TyCon -> [Role]
tyConRolesRepresentational TyCon
tc1 forall a. [a] -> Int -> a
!! Int
n)
Role
Phantom -> Role
r forall a. Eq a => a -> a -> Bool
== Role
Phantom
in Int
len1 forall a. Eq a => a -> a -> Bool
== Int
len2 Bool -> Bool -> Bool
&& Int
n forall a. Ord a => a -> a -> Bool
< Int
len1 Bool -> Bool -> Bool
&& Bool
good_role
| Bool
otherwise
= Bool
True
mkNthCoFunCo :: Int
-> CoercionN
-> Coercion
-> Coercion
-> Coercion
mkNthCoFunCo :: Int -> Coercion -> Coercion -> Coercion -> Coercion
mkNthCoFunCo Int
n Coercion
w Coercion
co1 Coercion
co2 = case Int
n of
Int
0 -> Coercion
w
Int
1 -> HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo Coercion
co1
Int
2 -> HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo Coercion
co2
Int
3 -> Coercion
co1
Int
4 -> Coercion
co2
Int
_ -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkNthCo(FunCo)" (forall a. Outputable a => a -> SDoc
ppr Int
n SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr Coercion
w SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr Coercion
co1 SDoc -> SDoc -> SDoc
$$ forall a. Outputable a => a -> SDoc
ppr Coercion
co2)
nthCoRole :: Int -> Coercion -> Role
nthCoRole :: Int -> Coercion -> Role
nthCoRole Int
n Coercion
co
| Just (TyCon
tc, [Type]
_) <- HasDebugCallStack => 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)
splitForAllTyCoVar_maybe Type
lty
= Role
Nominal
| Bool
otherwise
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"nthCoRole" (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 (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 (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 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 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
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
typeKind Type
ty1
tk2 :: Type
tk2 = HasDebugCallStack => 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 :: HasDebugCallStack => Coercion -> Coercion
mkSubCo :: HasDebugCallStack => 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 = forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Nominal Role
_ Coercion
_ = forall a. Maybe a
Nothing
downgradeRole_maybe Role
Representational Role
Nominal Coercion
co = forall a. a -> Maybe a
Just (HasDebugCallStack => Coercion -> Coercion
mkSubCo Coercion
co)
downgradeRole_maybe Role
Representational Role
Representational Coercion
co = forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Representational Role
Phantom Coercion
_ = forall a. Maybe a
Nothing
downgradeRole_maybe Role
Phantom Role
Phantom Coercion
co = forall a. a -> Maybe a
Just Coercion
co
downgradeRole_maybe Role
Phantom Role
_ Coercion
co = 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 -> forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"downgradeRole" (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 forall a. Eq a => a -> a -> Bool
== Role
Nominal = 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) = forall a. a -> Maybe a
Just Coercion
co
setNominalRole_maybe_helper co :: Coercion
co@(Refl Type
_) = forall a. a -> Maybe a
Just Coercion
co
setNominalRole_maybe_helper (GRefl Role
_ Type
ty MCoercion
co) = forall a. a -> Maybe a
Just 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' <- 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
; forall (m :: * -> *) a. Monad m => a -> m a
return 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
; forall (m :: * -> *) a. Monad m => a -> m a
return 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co1 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 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 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 forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Coercion -> Maybe Coercion
setNominalRole_maybe_helper Coercion
co forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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
CorePrepProv Bool
_ -> Bool
True
= forall a. a -> Maybe a
Just 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
_ = 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
= 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
_ = forall a. a -> [a]
repeat Role
role
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational TyCon
tc = TyCon -> [Role]
tyConRoles TyCon
tc forall a. [a] -> [a] -> [a]
++ 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) 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
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
UnivCo (CorePrepProv Bool
_) 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 forall a. [a] -> Int -> Bool
`lengthExceeds` Int
n
-> Coercion -> Coercion
promoteCoercion ([Coercion]
args forall a. [a] -> Int -> a
!! Int
n)
| Just (CoVar, Coercion, Coercion)
_ <- Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_maybe Coercion
co
, Int
n 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
typeKind Type
ty1
ki2 :: Type
ki2 = HasDebugCallStack => 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
= forall a. a -> Maybe a
Just 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
= forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkNthCo Role
Nominal Int
4 Coercion
g
| Bool
otherwise
= 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 = forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Pair Type
coercionKind [Coercion]
ws in
forall a b. (a, b) -> b
snd forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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) (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
; forall (m :: * -> *) a. Monad m => a -> m a
return (HasDebugCallStack => Type -> Type -> Type
piResultTy forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pair Type
g_tys 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) 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 )
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
mkTyConAppCo Role
Nominal TyCon
fam_tc [Coercion]
fam_cos
| Bool
otherwise
= HasDebugCallStack => 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 = 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 -> Scaled Type -> Coercion -> Coercion
mkFunResCo Role
r Scaled Type
scaled_ty Coercion
co
| Bool
otherwise = Role -> Scaled Type -> Coercion -> Coercion
mkFunResCo Role
r Scaled Type
scaled_ty Coercion
co
where
scaled_ty :: Scaled Type
scaled_ty = forall a. Type -> a -> Scaled a
Scaled (CoVar -> Type
varMult CoVar
v) (CoVar -> Type
varType CoVar
v)
mkFunResCo :: Role -> Scaled Type -> Coercion -> Coercion
mkFunResCo :: Role -> Scaled Type -> Coercion -> Coercion
mkFunResCo Role
role (Scaled Type
mult Type
arg_ty) Coercion
res_co
= Role -> Coercion -> Coercion -> Coercion -> Coercion
mkFunCo Role
role (Type -> Coercion
multToCo Type
mult) (Role -> Type -> Coercion
mkReflCo Role
role Type
arg_ty) Coercion
res_co
mkCoCast :: Coercion -> CoercionR -> Coercion
mkCoCast :: Coercion -> Coercion -> Coercion
mkCoCast Coercion
c Coercion
g
| (Coercion
g2:Coercion
g1:[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
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"mkCoCast" (forall a. Outputable a => a -> SDoc
ppr Coercion
g SDoc -> SDoc -> 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 forall a b. [a] -> [b] -> Bool
`leLength` [Type]
tys
= 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
= 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
instance Outputable ev => Outputable (NormaliseStepResult ev) where
ppr :: NormaliseStepResult ev -> SDoc
ppr NormaliseStepResult ev
NS_Done = String -> SDoc
text String
"NS_Done"
ppr NormaliseStepResult ev
NS_Abort = String -> SDoc
text String
"NS_Abort"
ppr (NS_Step RecTcChecker
_ Type
ty ev
ev) = [SDoc] -> SDoc
sep [String -> SDoc
text String
"NS_Step", forall a. Outputable a => a -> SDoc
ppr Type
ty, forall a. Outputable a => a -> SDoc
ppr ev
ev]
mapStepResult :: (ev1 -> ev2)
-> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult :: forall ev1 ev2.
(ev1 -> ev2) -> NormaliseStepResult ev1 -> NormaliseStepResult ev2
mapStepResult ev1 -> ev2
f (NS_Step RecTcChecker
rec_nts Type
ty ev1
ev) = 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 = forall ev. NormaliseStepResult ev
NS_Done
mapStepResult ev1 -> ev2
_ NormaliseStepResult ev1
NS_Abort = forall ev. NormaliseStepResult ev
NS_Abort
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
-> NormaliseStepper ev
composeSteppers :: forall ev.
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 -> 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' -> forall ev. RecTcChecker -> Type -> ev -> NormaliseStepResult ev
NS_Step RecTcChecker
rec_nts' Type
ty' Coercion
co
Maybe RecTcChecker
Nothing -> forall ev. NormaliseStepResult ev
NS_Abort
| Bool
otherwise
= forall ev. NormaliseStepResult ev
NS_Done
topNormaliseTypeX :: NormaliseStepper ev -> (ev -> ev -> ev)
-> Type -> Maybe (ev, Type)
topNormaliseTypeX :: forall ev.
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])
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
= 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])
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 -> forall a. a -> Maybe a
Just (ev
ev, Type
ty)
NormaliseStepResult ev
NS_Abort -> forall a. Maybe a
Nothing
| Bool
otherwise
= 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
= 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 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 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 (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 (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 (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]
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
liftCoSubst Role
r ([(CoVar, Coercion)] -> LiftingContext
mkLiftingContext forall a b. (a -> b) -> a -> b
$ 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 :: HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
r lc :: LiftingContext
lc@(LC TCvSubst
subst LiftCoEnv
env) Type
ty
| forall a. VarEnv a -> Bool
isEmptyVarEnv LiftCoEnv
env = Role -> Type -> Coercion
mkReflCo Role
r (HasCallStack => 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) forall a. VarEnv a
emptyVarEnv
mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
mkLiftingContext :: [(CoVar, Coercion)] -> LiftingContext
mkLiftingContext [(CoVar, Coercion)]
pairs
= TCvSubst -> LiftCoEnv -> LiftingContext
LC (InScopeSet -> TCvSubst
mkEmptyTCvSubst forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet forall a b. (a -> b) -> a -> b
$ [Coercion] -> VarSet
tyCoVarsOfCos (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(CoVar, Coercion)]
pairs))
(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 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 (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)
(forall a. VarEnv a -> CoVar -> a -> VarEnv a
extendVarEnv LiftCoEnv
env CoVar
v 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)
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
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)
(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 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
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"extendLiftingContextEx" (forall a. Outputable a => a -> SDoc
ppr CoVar
v SDoc -> SDoc -> SDoc
<+> String -> SDoc
text String
"|->" SDoc -> SDoc -> 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) 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) = forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"ty_co_subst bad roles" 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
mkTyConAppCo Role
r TyCon
tc (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 forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"ty_co_subst: covar is not almost devoid" (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
typeKind Type
ty))
(HasCallStack => TCvSubst -> Type -> Type
substTy (LiftingContext -> TCvSubst
lcSubstLeft LiftingContext
lc) Type
ty)
(HasCallStack => 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 <- 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
= forall a. a -> Maybe a
Just 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, ()
_) = 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 :: forall a.
(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
= 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
= 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 :: forall a.
(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 = 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 :: forall a.
(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
mkNthCo Role
role Int
2 Coercion
eta'
eta2 :: Coercion
eta2 = HasDebugCallStack => 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
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 = 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 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
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
substCo (LiftingContext -> TCvSubst
lcSubstRight LiftingContext
lc) Coercion
co
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv = 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 = forall key elt. UniqFM key elt -> [(Unique, elt)]
nonDetUFMToList LiftCoEnv
lc_env
([(Unique, Type)]
tpairs, [(Unique, Coercion)]
cpairs) = 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 = forall a. [(Unique, a)] -> VarEnv a
mkVarEnv_Directly [(Unique, Type)]
tpairs
cenv :: LiftCoEnv
cenv = 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
= forall a b. b -> Either a b
Right (Unique
u, Coercion
equality_co)
| Bool
otherwise
= forall a b. a -> Either a b
Left (Unique
u, Type
equality_ty)
where
equality_ty :: Type
equality_ty = 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 seq :: forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
ty seq :: forall a b. a -> b -> b
`seq` MCoercion -> ()
seqMCo MCoercion
mco
seqCo (TyConAppCo Role
r TyCon
tc [Coercion]
cos) = Role
r seq :: forall a b. a -> b -> b
`seq` TyCon
tc seq :: forall a b. a -> b -> b
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
seqCo (AppCo Coercion
co1 Coercion
co2) = Coercion -> ()
seqCo Coercion
co1 seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (ForAllCo CoVar
tv Coercion
k Coercion
co) = Type -> ()
seqType (CoVar -> Type
varType CoVar
tv) seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
k
seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (FunCo Role
r Coercion
w Coercion
co1 Coercion
co2) = Role
r seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
w seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co1 seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (CoVarCo CoVar
cv) = CoVar
cv seq :: forall a b. a -> b -> b
`seq` ()
seqCo (HoleCo CoercionHole
h) = CoercionHole -> CoVar
coHoleCoVar CoercionHole
h seq :: forall a b. a -> b -> b
`seq` ()
seqCo (AxiomInstCo CoAxiom Branched
con Int
ind [Coercion]
cos) = CoAxiom Branched
con seq :: forall a b. a -> b -> b
`seq` Int
ind seq :: forall a b. a -> b -> b
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
seqCo (UnivCo UnivCoProvenance
p Role
r Type
t1 Type
t2)
= UnivCoProvenance -> ()
seqProv UnivCoProvenance
p seq :: forall a b. a -> b -> b
`seq` Role
r seq :: forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t1 seq :: forall a b. a -> b -> b
`seq` Type -> ()
seqType Type
t2
seqCo (SymCo Coercion
co) = Coercion -> ()
seqCo Coercion
co
seqCo (TransCo Coercion
co1 Coercion
co2) = Coercion -> ()
seqCo Coercion
co1 seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co2
seqCo (NthCo Role
r Int
n Coercion
co) = Role
r seq :: forall a b. a -> b -> b
`seq` Int
n seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (LRCo LeftOrRight
lr Coercion
co) = LeftOrRight
lr seq :: forall a b. a -> b -> b
`seq` Coercion -> ()
seqCo Coercion
co
seqCo (InstCo Coercion
co Coercion
arg) = Coercion -> ()
seqCo Coercion
co seq :: forall a b. a -> b -> b
`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
_) = ()
seqProv (CorePrepProv Bool
_) = ()
seqCos :: [Coercion] -> ()
seqCos :: [Coercion] -> ()
seqCos [] = ()
seqCos (Coercion
co:[Coercion]
cos) = Coercion -> ()
seqCo Coercion
co seq :: forall a b. a -> b -> b
`seq` [Coercion] -> ()
seqCos [Coercion]
cos
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds [Coercion]
tys = forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
sequenceA forall a b. (a -> b) -> a -> b
$ 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 = 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 (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
coVarLType CoVar
cv
go (HoleCo CoercionHole
h) = HasDebugCallStack => 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) = 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
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) = forall {br :: BranchFlag}. CoAxiom br -> Int -> [Type] -> Type
go_ax_inst CoAxiom Branched
ax Int
ind (forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
go (AxiomRuleCo CoAxiomRule
ax [Coercion]
cos) = forall a. Pair a -> a
pFst forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"coercionKind" forall a b. (a -> b) -> a -> b
$
CoAxiomRule -> [Pair Type] -> Maybe (Pair Type)
coaxrProves CoAxiomRule
ax forall a b. (a -> b) -> a -> b
$ 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 } <- forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
ind
, let ([Type]
tys1, [Type]
cotys1) = forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
cos1 :: [Coercion]
cos1 = forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys1
= ASSERT( tys `equalLength` (tvs ++ cvs) )
HasCallStack => [CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys1 forall a b. (a -> b) -> a -> b
$
[CoVar] -> [Coercion] -> Type -> Type
substTyWithCoVars [CoVar]
cvs [Coercion]
cos1 forall a b. (a -> b) -> a -> b
$
TyCon -> [Type] -> Type
mkTyConApp (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
argforall a. a -> [a] -> [a]
:[Type]
args)
go_app Coercion
co [Type]
args = HasDebugCallStack => 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 forall a. Outputable a => [a] -> Int -> a
`getNth` Int
d
| Int
d forall a. Eq a => a -> a -> Bool
== Int
0
, Just (CoVar
tv,Type
_) <- Type -> Maybe (CoVar, Type)
splitForAllTyCoVar_maybe Type
ty
= CoVar -> Type
tyVarKind CoVar
tv
| Bool
otherwise
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"coercionLKind:nth" (forall a. Outputable a => a -> SDoc
ppr Int
d SDoc -> SDoc -> 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 (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
coVarRType CoVar
cv
go (HoleCo CoercionHole
h) = HasDebugCallStack => 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) = 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
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) = forall {br :: BranchFlag}. CoAxiom br -> Int -> [Type] -> Type
go_ax_inst CoAxiom Branched
ax Int
ind (forall a b. (a -> b) -> [a] -> [b]
map Coercion -> Type
go [Coercion]
cos)
go (AxiomRuleCo CoAxiomRule
ax [Coercion]
cos) = forall a. Pair a -> a
pSnd forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => String -> Maybe a -> a
expectJust String
"coercionKind" forall a b. (a -> b) -> a -> b
$
CoAxiomRule -> [Pair Type] -> Maybe (Pair Type)
coaxrProves CoAxiomRule
ax forall a b. (a -> b) -> a -> b
$ 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 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 } <- forall (br :: BranchFlag). CoAxiom br -> Int -> CoAxBranch
coAxiomNthBranch CoAxiom br
ax Int
ind
, let ([Type]
tys2, [Type]
cotys2) = forall b a. [b] -> [a] -> ([a], [a])
splitAtList [CoVar]
tvs [Type]
tys
cos2 :: [Coercion]
cos2 = forall a b. (a -> b) -> [a] -> [b]
map Type -> Coercion
stripCoercionTy [Type]
cotys2
= ASSERT( tys `equalLength` (tvs ++ cvs) )
HasCallStack => [CoVar] -> [Type] -> Type -> Type
substTyWith [CoVar]
tvs [Type]
tys2 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
argforall a. a -> [a] -> [a]
:[Type]
args)
go_app Coercion
co [Type]
args = HasDebugCallStack => 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
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 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
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
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
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
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]
_) = 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
typeKind Type
ty1
ki2 :: Type
ki2 = HasDebugCallStack => 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 = 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
typeKind Type
ty1
k2 :: Type
k2 = HasDebugCallStack => 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 = 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
typeKind Type
ty1
k2 :: Type
k2 = HasDebugCallStack => 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
mkTyConAppCo Role
Nominal TyCon
tc1 (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)
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)
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 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
mkNthCo Role
r Int
2 Coercion
kind_co'
eta2 :: Coercion
eta2 = HasDebugCallStack => Role -> Int -> Coercion -> Coercion
mkNthCo Role
r Int
3 Coercion
kind_co'
subst :: TCvSubst
subst = InScopeSet -> TCvSubst
mkEmptyTCvSubst forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet 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
substTy (TCvSubst -> CoVar -> Coercion -> TCvSubst
extendCvSubst TCvSubst
subst CoVar
cv2 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
= forall a. HasCallStack => String -> SDoc -> a
pprPanic String
"buildKindCoercion" ([SDoc] -> SDoc
vcat [ forall a. Outputable a => a -> SDoc
ppr Type
orig_ty1, forall a. Outputable a => a -> SDoc
ppr Type
orig_ty2
, forall a. Outputable a => a -> SDoc
ppr Type
ty1, forall a. Outputable a => a -> SDoc
ppr Type
ty2 ])
{-# INLINE simplifyArgsWorker #-}
simplifyArgsWorker :: [TyCoBinder] -> Kind
-> TyCoVarSet
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], MCoercionN)
simplifyArgsWorker :: [TyCoBinder]
-> Type
-> VarSet
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], MCoercion)
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], MCoercion)
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 forall a b. (a -> b) -> a -> b
$ VarSet -> InScopeSet
mkInScopeSet forall a b. (a -> b) -> a -> b
$ VarSet
orig_fvs
go :: [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Kind
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], MCoercionN)
go :: [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Type
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], MCoercion)
go [Type]
acc_xis [Coercion]
acc_cos !LiftingContext
lc [TyCoBinder]
binders Type
inner_ki [Role]
_ []
= (forall a. [a] -> [a]
reverse [Type]
acc_xis, forall a. [a] -> [a]
reverse [Coercion]
acc_cos, MCoercion
kind_co)
where
final_kind :: Type
final_kind = [TyCoBinder] -> Type -> Type
mkPiTys [TyCoBinder]
binders Type
inner_ki
kind_co :: MCoercion
kind_co | Type -> Bool
noFreeVarsOfType Type
final_kind = MCoercion
MRefl
| Bool
otherwise = Coercion -> MCoercion
MCo forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Role -> LiftingContext -> Type -> Coercion
liftCoSubst Role
Nominal LiftingContext
lc Type
final_kind
go [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 forall a b. (a -> b) -> a -> b
$
HasDebugCallStack => 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], MCoercion)
go (Type
casted_xi forall a. a -> [a] -> [a]
: [Type]
acc_xis)
(Coercion
casted_co 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
liftCoSubst Role
Nominal LiftingContext
lc Type
inner_ki
co1_kind :: Pair Type
co1_kind = Coercion -> Pair Type
coercionKind Coercion
co1
unrewritten_tys :: [Type]
unrewritten_tys = forall a b. (a -> b) -> [a] -> [b]
map (Coercion -> Type
coercionRKind forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Type, Coercion)]
args
([Coercion]
arg_cos, Coercion
res_co) = HasDebugCallStack =>
Coercion -> Pair Type -> [Type] -> ([Coercion], Coercion)
decomposePiCos Coercion
co1 Pair Type
co1_kind [Type]
unrewritten_tys
casted_args :: [(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) <- 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
rewritten_kind Type
_ = Pair Type
co1_kind
([TyCoBinder]
bndrs, Type
new_inner) = Type -> ([TyCoBinder], Type)
splitPiTys Type
rewritten_kind
([Type]
xis_out, [Coercion]
cos_out, MCoercion
res_co_out)
= [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Type
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], MCoercion)
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, MCoercion
res_co_out MCoercion -> Coercion -> MCoercion
`mkTransMCoL` Coercion
res_co)
go [Type]
_ [Coercion]
_ LiftingContext
_ [TyCoBinder]
_ Type
_ [Role]
_ [(Type, Coercion)]
_ = forall a. String -> a
panic
String
"simplifyArgsWorker wandered into deeper water than usual"
has_co_hole_ty :: Type -> Monoid.Any
has_co_hole_co :: Coercion -> Monoid.Any
(Type -> Any
has_co_hole_ty, [Type] -> Any
_, Coercion -> Any
has_co_hole_co, [Coercion] -> Any
_)
= forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo forall {env}. TyCoFolder env Any
folder ()
where
folder :: TyCoFolder env Any
folder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = forall a b. a -> b -> a
const forall a. Maybe a
Nothing
, tcf_tyvar :: env -> CoVar -> Any
tcf_tyvar = forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
, tcf_covar :: env -> CoVar -> Any
tcf_covar = forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
False)
, tcf_hole :: env -> CoercionHole -> Any
tcf_hole = forall a b c. a -> b -> c -> a
const2 (Bool -> Any
Monoid.Any Bool
True)
, tcf_tycobinder :: env -> CoVar -> ArgFlag -> env
tcf_tycobinder = forall a b c. a -> b -> c -> a
const2
}
const2 :: a -> b -> c -> a
const2 :: forall a b c. a -> b -> c -> a
const2 a
x b
_ c
_ = a
x
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy :: Type -> Bool
hasCoercionHoleTy = Any -> Bool
Monoid.getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Any
has_co_hole_ty
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo :: Coercion -> Bool
hasCoercionHoleCo = Any -> Bool
Monoid.getAny forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coercion -> Any
has_co_hole_co
type HoleSet = UniqSet CoercionHole
coercionHolesOfType :: Type -> UniqSet CoercionHole
coercionHolesOfCo :: Coercion -> UniqSet CoercionHole
(Type -> UniqSet CoercionHole
coercionHolesOfType, [Type] -> UniqSet CoercionHole
_, Coercion -> UniqSet CoercionHole
coercionHolesOfCo, [Coercion] -> UniqSet CoercionHole
_) = forall a env.
Monoid a =>
TyCoFolder env a
-> env -> (Type -> a, [Type] -> a, Coercion -> a, [Coercion] -> a)
foldTyCo TyCoFolder () (UniqSet CoercionHole)
folder ()
where
folder :: TyCoFolder () (UniqSet CoercionHole)
folder = TyCoFolder { tcf_view :: Type -> Maybe Type
tcf_view = forall a b. a -> b -> a
const forall a. Maybe a
Nothing
, tcf_tyvar :: () -> CoVar -> UniqSet CoercionHole
tcf_tyvar = \ ()
_ CoVar
_ -> forall a. Monoid a => a
mempty
, tcf_covar :: () -> CoVar -> UniqSet CoercionHole
tcf_covar = \ ()
_ CoVar
_ -> forall a. Monoid a => a
mempty
, tcf_hole :: () -> CoercionHole -> UniqSet CoercionHole
tcf_hole = forall a b. a -> b -> a
const forall a. Uniquable a => a -> UniqSet a
unitUniqSet
, tcf_tycobinder :: () -> CoVar -> ArgFlag -> ()
tcf_tycobinder = \ ()
_ CoVar
_ ArgFlag
_ -> ()
}