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