module Coercion (
Coercion, CoercionN, CoercionR, CoercionP,
UnivCoProvenance, CoercionHole, LeftOrRight(..),
Var, CoVar, TyCoVar,
Role(..), ltRole,
coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
coercionType, coercionKind, coercionKinds,
mkCoercionType,
coercionRole, coercionKindRole,
mkReflCo, mkRepReflCo, mkNomReflCo,
mkCoVarCo, mkCoVarCos,
mkAxInstCo, mkUnbranchedAxInstCo,
mkAxInstRHS, mkUnbranchedAxInstRHS,
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkTransAppCo,
mkNthCo, mkNthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunCos,
mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
mkPhantomCo, mkHomoPhantomCo, toPhantomCo,
mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
downgradeRole, maybeSubCo, mkAxiomRuleCo,
mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo,
mkKindCo, castCoercionKind,
mkHeteroCoercionType,
instNewTyCon_maybe,
NormaliseStepper, NormaliseStepResult(..), composeSteppers,
modifyStepResultCo, unwrapNewTypeStepper,
topNormaliseNewType_maybe, topNormaliseTypeX_maybe,
decomposeCo, getCoVar_maybe,
splitTyConAppCo_maybe,
splitAppCo_maybe,
splitForAllCo_maybe,
nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
pickLR,
isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
mkCoVar, isCoVar, coVarName, setCoVarName, setCoVarUnique,
isCoVar_maybe,
tyCoVarsOfCo, tyCoVarsOfCos, coVarsOfCo,
tyCoVarsOfCoAcc, tyCoVarsOfCosAcc, tyCoVarsOfCoDSet,
coercionSize,
CvSubstEnv, emptyCvSubstEnv,
lookupCoVar,
substCo, substCos, substCoVar, substCoVars, substCoWith,
substCoVarBndr,
extendTvSubstAndInScope, getCvSubstEnv,
liftCoSubst, liftCoSubstTyVar, liftCoSubstWith, liftCoSubstWithEx,
emptyLiftingContext, extendLiftingContext,
liftCoSubstVarBndrCallback, isMappedByLC,
mkSubstLiftingContext, zapLiftingContext,
substForAllCoBndrCallbackLC, lcTCvSubst, lcInScopeSet,
LiftCoEnv, LiftingContext(..), liftEnvSubstLeft, liftEnvSubstRight,
substRightCo, substLeftCo, swapLiftCoEnv, lcSubstLeft, lcSubstRight,
eqCoercion, eqCoercionX,
seqCo,
pprCo, pprParendCo, pprCoBndr,
pprCoAxiom, pprCoAxBranch, pprCoAxBranchHdr,
tidyCo, tidyCos,
promoteCoercion
) where
#include "HsVersions.h"
import TyCoRep
import Type
import TyCon
import CoAxiom
import Var
import VarEnv
import Name hiding ( varName )
import Util
import BasicTypes
import Outputable
import Unique
import Pair
import SrcLoc
import PrelNames
import TysPrim ( eqPhantPrimTyCon )
import ListSetOps
import Maybes
#if __GLASGOW_HASKELL__ < 709
import Control.Applicative hiding ( empty )
import Prelude hiding ( and )
import Data.Traversable (traverse, sequenceA)
import Data.Foldable ( and )
#endif
import Control.Monad (foldM)
import Control.Arrow ( first )
import Data.Function ( on )
coVarName :: CoVar -> Name
coVarName = varName
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName = setVarName
coercionSize :: Coercion -> Int
coercionSize (Refl _ ty) = typeSize ty
coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (AppCo co arg) = coercionSize co + coercionSize arg
coercionSize (ForAllCo _ h co) = 1 + coercionSize co + coercionSize h
coercionSize (CoVarCo _) = 1
coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
coercionSize (UnivCo p _ t1 t2) = 1 + provSize p + typeSize t1 + typeSize t2
coercionSize (SymCo co) = 1 + coercionSize co
coercionSize (TransCo co1 co2) = 1 + coercionSize co1 + coercionSize co2
coercionSize (NthCo _ co) = 1 + coercionSize co
coercionSize (LRCo _ co) = 1 + coercionSize co
coercionSize (InstCo co arg) = 1 + coercionSize co + coercionSize arg
coercionSize (CoherenceCo c1 c2) = 1 + coercionSize c1 + coercionSize c2
coercionSize (KindCo co) = 1 + coercionSize co
coercionSize (SubCo co) = 1 + coercionSize co
coercionSize (AxiomRuleCo _ cs) = 1 + sum (map coercionSize cs)
provSize :: UnivCoProvenance -> Int
provSize UnsafeCoerceProv = 1
provSize (PhantomProv co) = 1 + coercionSize co
provSize (ProofIrrelProv co) = 1 + coercionSize co
provSize (PluginProv _) = 1
provSize (HoleProv h) = pprPanic "provSize hits a hole" (ppr h)
pprCo, pprParendCo :: Coercion -> SDoc
pprCo co = ppr_co TopPrec co
pprParendCo co = ppr_co TyConPrec co
ppr_co :: TyPrec -> Coercion -> SDoc
ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
ppr_co p co@(TyConAppCo _ tc [_,_])
| tc `hasKey` funTyConKey = ppr_fun_co p co
ppr_co _ (TyConAppCo r tc cos) = pprTcAppCo TyConPrec ppr_co tc cos <> ppr_role r
ppr_co p (AppCo co arg) = maybeParen p TyConPrec $
pprCo co <+> ppr_co TyConPrec arg
ppr_co p co@(ForAllCo {}) = ppr_forall_co p co
ppr_co _ (CoVarCo cv) = parenSymOcc (getOccName cv) (ppr cv)
ppr_co p (AxiomInstCo con index args)
= pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
(map (ppr_co TyConPrec) args)
ppr_co p co@(TransCo {}) = maybeParen p FunPrec $
case trans_co_list co [] of
[] -> panic "ppr_co"
(co:cos) -> sep ( ppr_co FunPrec co
: [ char ';' <+> ppr_co FunPrec co | co <- cos])
ppr_co p (InstCo co arg) = maybeParen p TyConPrec $
pprParendCo co <> text "@" <> ppr_co TopPrec arg
ppr_co p (UnivCo UnsafeCoerceProv r ty1 ty2)
= pprPrefixApp p (text "UnsafeCo" <+> ppr r)
[pprParendType ty1, pprParendType ty2]
ppr_co _ (UnivCo p r t1 t2)
= char 'U'
<> parens (ppr_prov <> comma <+> ppr t1 <> comma <+> ppr t2)
<> ppr_role r
where
ppr_prov = case p of
HoleProv h -> text "hole:" <> ppr h
PhantomProv kind_co -> text "phant:" <> ppr kind_co
ProofIrrelProv co -> text "irrel:" <> ppr co
PluginProv s -> text "plugin:" <> text s
UnsafeCoerceProv -> text "unsafe"
ppr_co p (SymCo co) = pprPrefixApp p (text "Sym") [pprParendCo co]
ppr_co p (NthCo n co) = pprPrefixApp p (text "Nth:" <> int n) [pprParendCo co]
ppr_co p (LRCo sel co) = pprPrefixApp p (ppr sel) [pprParendCo co]
ppr_co p (CoherenceCo c1 c2) = maybeParen p TyConPrec $
(ppr_co FunPrec c1) <+> (text "|>") <+>
(ppr_co FunPrec c2)
ppr_co p (KindCo co) = pprPrefixApp p (text "kind") [pprParendCo co]
ppr_co p (SubCo co) = pprPrefixApp p (text "Sub") [pprParendCo co]
ppr_co p (AxiomRuleCo co cs) = maybeParen p TopPrec $ ppr_axiom_rule_co co cs
ppr_axiom_rule_co :: CoAxiomRule -> [Coercion] -> SDoc
ppr_axiom_rule_co co ps = ppr (coaxrName co) <+> parens (interpp'SP ps)
ppr_role :: Role -> SDoc
ppr_role r = underscore <> pp_role
where pp_role = case r of
Nominal -> char 'N'
Representational -> char 'R'
Phantom -> char 'P'
trans_co_list :: Coercion -> [Coercion] -> [Coercion]
trans_co_list (TransCo co1 co2) cos = trans_co_list co1 (trans_co_list co2 cos)
trans_co_list co cos = co : cos
ppr_fun_co :: TyPrec -> Coercion -> SDoc
ppr_fun_co p co = pprArrowChain p (split co)
where
split :: Coercion -> [SDoc]
split (TyConAppCo _ f [arg, res])
| f `hasKey` funTyConKey
= ppr_co FunPrec arg : split res
split co = [ppr_co TopPrec co]
ppr_forall_co :: TyPrec -> Coercion -> SDoc
ppr_forall_co p (ForAllCo tv h co)
= maybeParen p FunPrec $
sep [pprCoBndr (tyVarName tv) h, ppr_co TopPrec co]
ppr_forall_co _ _ = panic "ppr_forall_co"
pprCoBndr :: Name -> Coercion -> SDoc
pprCoBndr name eta =
forAllLit <+> parens (ppr name <+> dcolon <+> ppr eta) <> dot
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
= hang (text "axiom" <+> ppr ax <+> dcolon)
2 (vcat (map (ppr_co_ax_branch (const ppr) ax) $ fromBranches branches))
pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch pprRhs
where
pprRhs fam_tc (TyConApp tycon _)
| isDataFamilyTyCon fam_tc
= pprDataCons tycon
pprRhs _ rhs = ppr rhs
pprCoAxBranchHdr :: CoAxiom br -> BranchIndex -> SDoc
pprCoAxBranchHdr ax index = pprCoAxBranch ax (coAxiomNthBranch ax index)
ppr_co_ax_branch :: (TyCon -> Type -> SDoc) -> CoAxiom br -> CoAxBranch -> SDoc
ppr_co_ax_branch ppr_rhs
(CoAxiom { co_ax_tc = fam_tc, co_ax_name = name })
(CoAxBranch { cab_tvs = tvs
, cab_cvs = cvs
, cab_lhs = lhs
, cab_rhs = rhs
, cab_loc = loc })
= foldr1 (flip hangNotEmpty 2)
[ pprUserForAll (mkNamedBinders Invisible (tvs ++ cvs))
, pprTypeApp fam_tc lhs <+> equals <+> ppr_rhs fam_tc rhs
, text "-- Defined" <+> pprLoc loc ]
where
pprLoc loc
| isGoodSrcSpan loc
= text "at" <+> ppr (srcSpanStart loc)
| otherwise
= text "in" <+>
quotes (ppr (nameModule name))
decomposeCo :: Arity -> Coercion -> [Coercion]
decomposeCo arity co
= [mkNthCo n co | n <- [0..(arity1)] ]
getCoVar_maybe :: Coercion -> Maybe CoVar
getCoVar_maybe (CoVarCo cv) = Just cv
getCoVar_maybe _ = Nothing
splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
splitTyConAppCo_maybe (Refl r ty)
= do { (tc, tys) <- splitTyConApp_maybe ty
; let args = zipWith mkReflCo (tyConRolesX r tc) tys
; return (tc, args) }
splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
splitTyConAppCo_maybe _ = Nothing
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe (AppCo co arg) = Just (co, arg)
splitAppCo_maybe (TyConAppCo r tc args)
| mightBeUnsaturatedTyCon tc || args `lengthExceeds` tyConArity tc
, Just (args', arg') <- snocView args
, Just arg'' <- setNominalRole_maybe arg'
= Just ( mkTyConAppCo r tc args', arg'' )
splitAppCo_maybe (Refl r ty)
| Just (ty1, ty2) <- splitAppTy_maybe ty
= Just (mkReflCo r ty1, mkNomReflCo ty2)
splitAppCo_maybe _ = Nothing
splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
splitForAllCo_maybe _ = Nothing
coVarTypes :: CoVar -> (Type,Type)
coVarTypes cv
| (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
= (ty1, ty2)
coVarKindsTypesRole :: CoVar -> (Kind,Kind,Type,Type,Role)
coVarKindsTypesRole cv
| Just (tc, [k1,k2,ty1,ty2]) <- splitTyConApp_maybe (varType cv)
= let role
| tc `hasKey` eqPrimTyConKey = Nominal
| tc `hasKey` eqReprPrimTyConKey = Representational
| otherwise = panic "coVarKindsTypesRole"
in (k1,k2,ty1,ty2,role)
| otherwise = pprPanic "coVarKindsTypesRole, non coercion variable"
(ppr cv $$ ppr (varType cv))
coVarKind :: CoVar -> Type
coVarKind cv
= ASSERT( isCoVar cv )
varType cv
coVarRole :: CoVar -> Role
coVarRole cv
| tc `hasKey` eqPrimTyConKey
= Nominal
| tc `hasKey` eqReprPrimTyConKey
= Representational
| otherwise
= pprPanic "coVarRole: unknown tycon" (ppr cv <+> dcolon <+> ppr (varType cv))
where
tc = case tyConAppTyCon_maybe (varType cv) of
Just tc0 -> tc0
Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv)
mkCoercionType :: Role -> Type -> Type -> Type
mkCoercionType Nominal = mkPrimEqPred
mkCoercionType Representational = mkReprPrimEqPred
mkCoercionType Phantom = \ty1 ty2 ->
let ki1 = typeKind ty1
ki2 = typeKind ty2
in
TyConApp eqPhantPrimTyCon [ki1, ki2, ty1, ty2]
mkHeteroCoercionType :: Role -> Kind -> Kind -> Type -> Type -> Type
mkHeteroCoercionType Nominal = mkHeteroPrimEqPred
mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
mkHeteroCoercionType Phantom = panic "mkHeteroCoercionType"
isReflCo :: Coercion -> Bool
isReflCo (Refl {}) = True
isReflCo _ = False
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl r ty) = Just (ty, r)
isReflCo_maybe _ = Nothing
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = isJust . isReflexiveCo_maybe
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl r ty) = Just (ty, r)
isReflexiveCo_maybe co
| ty1 `eqType` ty2
= Just (ty1, r)
| otherwise
= Nothing
where (Pair ty1 ty2, r) = coercionKindRole co
mkReflCo :: Role -> Type -> Coercion
mkReflCo r ty
= Refl r ty
mkRepReflCo :: Type -> Coercion
mkRepReflCo = mkReflCo Representational
mkNomReflCo :: Type -> Coercion
mkNomReflCo = mkReflCo Nominal
mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo r tc cos
| Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
= mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
| Just tys_roles <- traverse isReflCo_maybe cos
= Refl r (mkTyConApp tc (map fst tys_roles))
| otherwise = TyConAppCo r tc cos
mkFunCo :: Role -> Coercion -> Coercion -> Coercion
mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
mkFunCos r cos res_co = foldr (mkFunCo r) res_co cos
mkAppCo :: Coercion
-> Coercion
-> Coercion
mkAppCo (Refl r ty1) arg
| Just (ty2, _) <- isReflCo_maybe arg
= Refl r (mkAppTy ty1 ty2)
| Just (tc, tys) <- splitTyConApp_maybe ty1
= TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
where
zip_roles (r1:_) [] = [downgradeRole r1 Nominal arg]
zip_roles (r1:rs) (ty1:tys) = mkReflCo r1 ty1 : zip_roles rs tys
zip_roles _ _ = panic "zip_roles"
mkAppCo (TyConAppCo r tc args) arg
= case r of
Nominal -> TyConAppCo Nominal tc (args ++ [arg])
Representational -> TyConAppCo Representational tc (args ++ [arg'])
where new_role = (tyConRolesRepresentational tc) !! (length args)
arg' = downgradeRole new_role Nominal arg
Phantom -> TyConAppCo Phantom tc (args ++ [toPhantomCo arg])
mkAppCo co arg = AppCo co arg
mkAppCos :: Coercion
-> [Coercion]
-> Coercion
mkAppCos co1 cos = foldl mkAppCo co1 cos
mkTransAppCo :: Role
-> Coercion
-> Type
-> Type
-> Role
-> Coercion
-> Type
-> Type
-> Role
-> Coercion
mkTransAppCo r1 co1 ty1a ty1b r2 co2 ty2a ty2b r3
= case (r1, r2, r3) of
(_, _, Phantom)
-> mkPhantomCo kind_co (mkAppTy ty1a ty2a) (mkAppTy ty1b ty2b)
where
kind_co1 = mkKindCo co1
kind_co = mkNthCo 1 kind_co1
(_, _, Nominal)
-> ASSERT( r1 == Nominal && r2 == Nominal )
mkAppCo co1 co2
(Nominal, Nominal, Representational)
-> mkSubCo (mkAppCo co1 co2)
(_, Nominal, Representational)
-> ASSERT( r1 == Representational )
mkAppCo co1 co2
(Nominal, Representational, Representational)
-> go (mkSubCo co1)
(_ , _, Representational)
-> ASSERT( r1 == Representational && r2 == Representational )
go co1
where
go co1_repr
| Just (tc1b, tys1b) <- splitTyConApp_maybe ty1b
, nextRole ty1b == r2
= (mkAppCo co1_repr (mkNomReflCo ty2a)) `mkTransCo`
(mkTyConAppCo Representational tc1b
(zipWith mkReflCo (tyConRolesRepresentational tc1b) tys1b
++ [co2]))
| Just (tc1a, tys1a) <- splitTyConApp_maybe ty1a
, nextRole ty1a == r2
= (mkTyConAppCo Representational tc1a
(zipWith mkReflCo (tyConRolesRepresentational tc1a) tys1a
++ [co2]))
`mkTransCo`
(mkAppCo co1_repr (mkNomReflCo ty2b))
| otherwise
= pprPanic "mkTransAppCo" (vcat [ ppr r1, ppr co1, ppr ty1a, ppr ty1b
, ppr r2, ppr co2, ppr ty2a, ppr ty2b
, ppr r3 ])
mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
mkForAllCo tv kind_co co
| Refl r ty <- co
, Refl {} <- kind_co
= Refl r (mkNamedForAllTy tv Invisible ty)
| otherwise
= ForAllCo tv kind_co co
mkForAllCos :: [(TyVar, Coercion)] -> Coercion -> Coercion
mkForAllCos bndrs (Refl r ty)
= let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
foldl (flip $ uncurry ForAllCo)
(Refl r $ mkInvForAllTys (reverse (map fst refls_rev'd)) ty)
non_refls_rev'd
mkForAllCos bndrs co = foldr (uncurry ForAllCo) co bndrs
mkHomoForAllCos :: [TyVar] -> Coercion -> Coercion
mkHomoForAllCos tvs (Refl r ty)
= Refl r (mkInvForAllTys tvs ty)
mkHomoForAllCos tvs ty = mkHomoForAllCos_NoRefl tvs ty
mkHomoForAllCos_NoRefl :: [TyVar] -> Coercion -> Coercion
mkHomoForAllCos_NoRefl tvs orig_co = foldr go orig_co tvs
where
go tv co = ForAllCo tv (mkNomReflCo (tyVarKind tv)) co
mkCoVarCo :: CoVar -> Coercion
mkCoVarCo cv
| ty1 `eqType` ty2 = Refl (coVarRole cv) ty1
| otherwise = CoVarCo cv
where
(ty1, ty2) = coVarTypes cv
mkCoVarCos :: [CoVar] -> [Coercion]
mkCoVarCos = map mkCoVarCo
isCoVar_maybe :: Coercion -> Maybe CoVar
isCoVar_maybe (CoVarCo cv) = Just cv
isCoVar_maybe _ = Nothing
mkAxInstCo :: Role -> CoAxiom br -> BranchIndex -> [Type] -> [Coercion]
-> Coercion
mkAxInstCo role ax index tys cos
| arity == n_tys = downgradeRole role ax_role $
mkAxiomInstCo ax_br index (rtys `chkAppend` cos)
| otherwise = ASSERT( arity < n_tys )
downgradeRole role ax_role $
mkAppCos (mkAxiomInstCo ax_br index
(ax_args `chkAppend` cos))
leftover_args
where
n_tys = length tys
ax_br = toBranchedAxiom ax
branch = coAxiomNthBranch ax_br index
tvs = coAxBranchTyVars branch
arity = length tvs
arg_roles = coAxBranchRoles branch
rtys = zipWith mkReflCo (arg_roles ++ repeat Nominal) tys
(ax_args, leftover_args)
= splitAt arity rtys
ax_role = coAxiomRole ax
mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
mkAxiomInstCo ax index args
= ASSERT( coAxiomArity ax index == length args )
AxiomInstCo ax index args
mkUnbranchedAxInstCo :: Role -> CoAxiom Unbranched
-> [Type] -> [Coercion] -> Coercion
mkUnbranchedAxInstCo role ax tys cos
= mkAxInstCo role ax 0 tys cos
mkAxInstRHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstRHS ax index tys cos
= ASSERT( tvs `equalLength` tys1 )
mkAppTys rhs' tys2
where
branch = coAxiomNthBranch ax index
tvs = coAxBranchTyVars branch
cvs = coAxBranchCoVars branch
(tys1, tys2) = splitAtList tvs tys
rhs' = substTyWith tvs tys1 $
substTyWithCoVars cvs cos $
coAxBranchRHS branch
mkUnbranchedAxInstRHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstRHS ax = mkAxInstRHS ax 0
mkAxInstLHS :: CoAxiom br -> BranchIndex -> [Type] -> [Coercion] -> Type
mkAxInstLHS ax index tys cos
= ASSERT( tvs `equalLength` tys1 )
mkTyConApp fam_tc (lhs_tys `chkAppend` tys2)
where
branch = coAxiomNthBranch ax index
tvs = coAxBranchTyVars branch
cvs = coAxBranchCoVars branch
(tys1, tys2) = splitAtList tvs tys
lhs_tys = substTysWith tvs tys1 $
substTysWithCoVars cvs cos $
coAxBranchLHS branch
fam_tc = coAxiomTyCon ax
mkUnbranchedAxInstLHS :: CoAxiom Unbranched -> [Type] -> [Coercion] -> Type
mkUnbranchedAxInstLHS ax = mkAxInstLHS ax 0
mkUnsafeCo :: Role -> Type -> Type -> Coercion
mkUnsafeCo role ty1 ty2
= mkUnivCo UnsafeCoerceProv role ty1 ty2
mkHoleCo :: CoercionHole -> Role
-> Type -> Type -> Coercion
mkHoleCo h r t1 t2 = mkUnivCo (HoleProv h) r t1 t2
mkUnivCo :: UnivCoProvenance
-> Role
-> Type
-> Type
-> Coercion
mkUnivCo prov role ty1 ty2
| ty1 `eqType` ty2 = Refl role ty1
| otherwise = UnivCo prov role ty1 ty2
mkSymCo :: Coercion -> Coercion
mkSymCo co@(Refl {}) = co
mkSymCo (SymCo co) = co
mkSymCo (SubCo (SymCo co)) = SubCo co
mkSymCo co = SymCo co
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo co1 (Refl {}) = co1
mkTransCo (Refl {}) co2 = co2
mkTransCo co1 co2 = TransCo co1 co2
mkNthCoRole :: Role -> Int -> Coercion -> Coercion
mkNthCoRole role n co
= downgradeRole role nth_role $ nth_co
where
nth_co = mkNthCo n co
nth_role = coercionRole nth_co
mkNthCo :: Int -> Coercion -> Coercion
mkNthCo 0 (Refl _ ty)
| Just (tv, _) <- splitForAllTy_maybe ty
= Refl Nominal (tyVarKind tv)
mkNthCo n (Refl r ty)
= ASSERT( ok_tc_app ty n )
mkReflCo r' (tyConAppArgN n ty)
where tc = tyConAppTyCon ty
r' = nthRole r tc n
ok_tc_app :: Type -> Int -> Bool
ok_tc_app ty n
| Just (_, tys) <- splitTyConApp_maybe ty
= tys `lengthExceeds` n
| isForAllTy ty
= n == 0
| otherwise
= False
mkNthCo n (TyConAppCo _ _ cos) = cos `getNth` n
mkNthCo n co = NthCo n co
mkLRCo :: LeftOrRight -> Coercion -> Coercion
mkLRCo lr (Refl eq ty) = Refl eq (pickLR lr (splitAppTy ty))
mkLRCo lr co = LRCo lr co
mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo (ForAllCo tv _kind_co body_co) (Refl _ arg)
= substCoWithUnchecked [tv] [arg] body_co
mkInstCo co arg = InstCo co arg
mkCoherenceCo :: Coercion -> Coercion -> Coercion
mkCoherenceCo co1 (Refl {}) = co1
mkCoherenceCo (CoherenceCo co1 co2) co3
= CoherenceCo co1 (co2 `mkTransCo` co3)
mkCoherenceCo co1 co2 = CoherenceCo co1 co2
mkCoherenceRightCo :: Coercion -> Coercion -> Coercion
mkCoherenceRightCo c1 c2 = mkSymCo (mkCoherenceCo (mkSymCo c1) c2)
mkCoherenceLeftCo :: Coercion -> Coercion -> Coercion
mkCoherenceLeftCo = mkCoherenceCo
infixl 5 `mkCoherenceCo`
infixl 5 `mkCoherenceRightCo`
infixl 5 `mkCoherenceLeftCo`
mkKindCo :: Coercion -> Coercion
mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty)
mkKindCo (UnivCo (PhantomProv h) _ _ _) = h
mkKindCo (UnivCo (ProofIrrelProv h) _ _ _) = h
mkKindCo co
| Pair ty1 ty2 <- coercionKind co
, typeKind ty1 `eqType` typeKind ty2
= Refl Nominal (typeKind ty1)
| otherwise
= KindCo co
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl Nominal ty) = Refl Representational ty
mkSubCo (TyConAppCo Nominal tc cos)
= TyConAppCo Representational tc (applyRoles tc cos)
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
SubCo co
downgradeRole_maybe :: Role
-> Role
-> Coercion -> Maybe Coercion
downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
downgradeRole_maybe Nominal Representational _ = Nothing
downgradeRole_maybe Phantom Phantom co = Just co
downgradeRole_maybe Phantom _ co = Just (toPhantomCo co)
downgradeRole_maybe _ Phantom _ = Nothing
downgradeRole_maybe _ _ co = Just co
downgradeRole :: Role
-> Role
-> Coercion -> Coercion
downgradeRole r1 r2 co
= case downgradeRole_maybe r1 r2 co of
Just co' -> co'
Nothing -> pprPanic "downgradeRole" (ppr co)
maybeSubCo :: EqRel -> Coercion -> Coercion
maybeSubCo NomEq = id
maybeSubCo ReprEq = mkSubCo
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo
mkProofIrrelCo :: Role
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkProofIrrelCo r (Refl {}) g _ = Refl r (CoercionTy g)
mkProofIrrelCo r kco g1 g2 = mkUnivCo (ProofIrrelProv kco) r
(mkCoercionTy g1) (mkCoercionTy g2)
setNominalRole_maybe :: Coercion -> Maybe Coercion
setNominalRole_maybe co
| Nominal <- coercionRole co = Just co
setNominalRole_maybe (SubCo co) = Just co
setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
setNominalRole_maybe (TyConAppCo Representational tc cos)
= do { cos' <- mapM setNominalRole_maybe cos
; return $ TyConAppCo Nominal tc cos' }
setNominalRole_maybe (SymCo co)
= SymCo <$> setNominalRole_maybe co
setNominalRole_maybe (TransCo co1 co2)
= TransCo <$> setNominalRole_maybe co1 <*> setNominalRole_maybe co2
setNominalRole_maybe (AppCo co1 co2)
= AppCo <$> setNominalRole_maybe co1 <*> pure co2
setNominalRole_maybe (ForAllCo tv kind_co co)
= ForAllCo tv kind_co <$> setNominalRole_maybe co
setNominalRole_maybe (NthCo n co)
= NthCo n <$> setNominalRole_maybe co
setNominalRole_maybe (InstCo co arg)
= InstCo <$> setNominalRole_maybe co <*> pure arg
setNominalRole_maybe (CoherenceCo co1 co2)
= CoherenceCo <$> setNominalRole_maybe co1 <*> pure co2
setNominalRole_maybe (UnivCo prov _ co1 co2)
| case prov of UnsafeCoerceProv -> True
PhantomProv _ -> False
ProofIrrelProv _ -> True
PluginProv _ -> False
HoleProv _ -> False
= Just $ UnivCo prov Nominal co1 co2
setNominalRole_maybe _ = Nothing
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo h t1 t2
= mkUnivCo (PhantomProv h) Phantom t1 t2
mkHomoPhantomCo :: Type -> Type -> Coercion
mkHomoPhantomCo t1 t2
= ASSERT( k1 `eqType` typeKind t2 )
mkPhantomCo (mkNomReflCo k1) t1 t2
where
k1 = typeKind t1
toPhantomCo :: Coercion -> Coercion
toPhantomCo co
= mkPhantomCo (mkKindCo co) ty1 ty2
where Pair ty1 ty2 = coercionKind co
applyRoles :: TyCon -> [Coercion] -> [Coercion]
applyRoles tc cos
= zipWith (\r -> downgradeRole r Nominal) (tyConRolesRepresentational tc) cos
tyConRolesX :: Role -> TyCon -> [Role]
tyConRolesX Representational tc = tyConRolesRepresentational tc
tyConRolesX role _ = repeat role
tyConRolesRepresentational :: TyCon -> [Role]
tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
nthRole :: Role -> TyCon -> Int -> Role
nthRole Nominal _ _ = Nominal
nthRole Phantom _ _ = Phantom
nthRole Representational tc n
= (tyConRolesRepresentational tc) `getNth` n
ltRole :: Role -> Role -> Bool
ltRole Phantom _ = False
ltRole Representational Phantom = True
ltRole Representational _ = False
ltRole Nominal Nominal = False
ltRole Nominal _ = True
promoteCoercion :: Coercion -> Coercion
promoteCoercion co = case co of
_ | ki1 `eqType` ki2
-> mkNomReflCo (typeKind ty1)
Refl _ ty -> ASSERT( False )
mkNomReflCo (typeKind ty)
TyConAppCo _ tc args
| Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
-> co'
| otherwise
-> mkKindCo co
AppCo co1 arg
| Just co' <- instCoercion (coercionKind (mkKindCo co1))
(promoteCoercion co1) arg
-> co'
| otherwise
-> mkKindCo co
ForAllCo _ _ g
-> promoteCoercion g
CoVarCo {}
-> mkKindCo co
AxiomInstCo {}
-> mkKindCo co
UnivCo UnsafeCoerceProv _ t1 t2
-> mkUnsafeCo Nominal (typeKind t1) (typeKind t2)
UnivCo (PhantomProv kco) _ _ _
-> kco
UnivCo (ProofIrrelProv kco) _ _ _
-> kco
UnivCo (PluginProv _) _ _ _
-> mkKindCo co
UnivCo (HoleProv _) _ _ _
-> mkKindCo co
SymCo g
-> mkSymCo (promoteCoercion g)
TransCo co1 co2
-> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
NthCo n co1
| Just (_, args) <- splitTyConAppCo_maybe co1
, n < length args
-> promoteCoercion (args !! n)
| Just _ <- splitForAllCo_maybe co
, n == 0
-> ASSERT( False ) mkNomReflCo liftedTypeKind
| otherwise
-> mkKindCo co
LRCo lr co1
| Just (lco, rco) <- splitAppCo_maybe co1
-> case lr of
CLeft -> promoteCoercion lco
CRight -> promoteCoercion rco
| otherwise
-> mkKindCo co
InstCo g _
-> promoteCoercion g
CoherenceCo g h
-> mkSymCo h `mkTransCo` promoteCoercion g
KindCo _
-> ASSERT( False )
mkNomReflCo liftedTypeKind
SubCo g
-> promoteCoercion g
AxiomRuleCo {}
-> mkKindCo co
where
Pair ty1 ty2 = coercionKind co
ki1 = typeKind ty1
ki2 = typeKind ty2
instCoercion :: Pair Type
-> Coercion
-> Coercion
-> Maybe Coercion
instCoercion (Pair lty rty) g w
| isForAllTy lty && isForAllTy rty
, Just w' <- setNominalRole_maybe w
= Just $ mkInstCo g w'
| isFunTy lty && isFunTy rty
= Just $ mkNthCo 1 g
| otherwise
= Nothing
where
instCoercions :: Coercion -> [Coercion] -> Maybe Coercion
instCoercions g ws
= let arg_ty_pairs = map coercionKind ws in
snd <$> foldM go (coercionKind g, g) (zip arg_ty_pairs ws)
where
go :: (Pair Type, Coercion) -> (Pair Type, Coercion)
-> Maybe (Pair Type, Coercion)
go (g_tys, g) (w_tys, w)
= do { g' <- instCoercion g_tys g w
; return (piResultTy <$> g_tys <*> w_tys, g') }
castCoercionKind :: Coercion -> Coercion -> Coercion -> Coercion
castCoercionKind g h1 h2
= g `mkCoherenceLeftCo` h1 `mkCoherenceRightCo` h2
mkPiCos :: Role -> [Var] -> Coercion -> Coercion
mkPiCos r vs co = foldr (mkPiCo r) co vs
mkPiCo :: Role -> Var -> Coercion -> Coercion
mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
| otherwise = mkFunCo r (mkReflCo r (varType v)) co
mkCoCast :: Coercion -> Coercion -> Coercion
mkCoCast c g
= mkSymCo g1 `mkTransCo` c `mkTransCo` g2
where
(_, args) = splitTyConApp (pFst $ coercionKind g)
n_args = length args
co_list = decomposeCo n_args g
g1 = co_list `getNth` (n_args 2)
g2 = co_list `getNth` (n_args 1)
instNewTyCon_maybe :: TyCon -> [Type] -> Maybe (Type, Coercion)
instNewTyCon_maybe tc tys
| Just (tvs, ty, co_tc) <- unwrapNewTyConEtad_maybe tc
, tvs `leLength` tys
= Just (applyTysX tvs ty tys, mkUnbranchedAxInstCo Representational co_tc tys [])
| otherwise
= Nothing
type NormaliseStepper = RecTcChecker
-> TyCon
-> [Type]
-> NormaliseStepResult
data NormaliseStepResult
= NS_Done
| NS_Abort
| NS_Step RecTcChecker Type Coercion
modifyStepResultCo :: (Coercion -> Coercion)
-> NormaliseStepResult -> NormaliseStepResult
modifyStepResultCo f (NS_Step rec_nts ty co) = NS_Step rec_nts ty (f co)
modifyStepResultCo _ result = result
composeSteppers :: NormaliseStepper -> NormaliseStepper
-> NormaliseStepper
composeSteppers step1 step2 rec_nts tc tys
= case step1 rec_nts tc tys of
success@(NS_Step {}) -> success
NS_Done -> step2 rec_nts tc tys
NS_Abort -> NS_Abort
unwrapNewTypeStepper :: NormaliseStepper
unwrapNewTypeStepper rec_nts tc tys
| Just (ty', co) <- instNewTyCon_maybe tc tys
= case checkRecTc rec_nts tc of
Just rec_nts' -> NS_Step rec_nts' ty' co
Nothing -> NS_Abort
| otherwise
= NS_Done
topNormaliseTypeX_maybe :: NormaliseStepper -> Type -> Maybe (Coercion, Type)
topNormaliseTypeX_maybe stepper
= go initRecTc Nothing
where
go rec_nts mb_co1 ty
| Just (tc, tys) <- splitTyConApp_maybe ty
= case stepper rec_nts tc tys of
NS_Step rec_nts' ty' co2
-> go rec_nts' (mb_co1 `trans` co2) ty'
NS_Done -> all_done
NS_Abort -> Nothing
| otherwise
= all_done
where
all_done | Just co <- mb_co1 = Just (co, ty)
| otherwise = Nothing
Nothing `trans` co2 = Just co2
(Just co1) `trans` co2 = Just (co1 `mkTransCo` co2)
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
topNormaliseNewType_maybe ty
= topNormaliseTypeX_maybe unwrapNewTypeStepper ty
eqCoercion :: Coercion -> Coercion -> Bool
eqCoercion = eqType `on` coercionType
eqCoercionX :: RnEnv2 -> Coercion -> Coercion -> Bool
eqCoercionX env = eqTypeX env `on` coercionType
data LiftingContext = LC TCvSubst LiftCoEnv
instance Outputable LiftingContext where
ppr (LC _ env) = hang (text "LiftingContext:") 2 (ppr env)
type LiftCoEnv = VarEnv Coercion
liftCoSubstWithEx :: Role
-> [TyVar]
-> [Coercion]
-> [TyVar]
-> [Type]
-> (Type -> Coercion, [Type])
liftCoSubstWithEx role univs omegas exs rhos
= let theta = mkLiftingContext (zipEqual "liftCoSubstWithExU" univs omegas)
psi = extendLiftingContextEx theta (zipEqual "liftCoSubstWithExX" exs rhos)
in (ty_co_subst psi role, substTyVars (lcSubstRight psi) exs)
liftCoSubstWith :: Role -> [TyCoVar] -> [Coercion] -> Type -> Coercion
liftCoSubstWith r tvs cos ty
= liftCoSubst r (mkLiftingContext $ zipEqual "liftCoSubstWith" tvs cos) ty
liftCoSubst :: Role -> LiftingContext -> Type -> Coercion
liftCoSubst r lc@(LC subst env) ty
| isEmptyVarEnv env = Refl r (substTy subst ty)
| otherwise = ty_co_subst lc r ty
emptyLiftingContext :: InScopeSet -> LiftingContext
emptyLiftingContext in_scope = LC (mkEmptyTCvSubst in_scope) emptyVarEnv
mkLiftingContext :: [(TyCoVar,Coercion)] -> LiftingContext
mkLiftingContext pairs
= LC (mkEmptyTCvSubst $ mkInScopeSet $ tyCoVarsOfCos (map snd pairs))
(mkVarEnv pairs)
mkSubstLiftingContext :: TCvSubst -> LiftingContext
mkSubstLiftingContext subst = LC subst emptyVarEnv
extendLiftingContext :: LiftingContext
-> TyVar
-> Coercion
-> LiftingContext
extendLiftingContext (LC subst env) tv arg
= ASSERT( isTyVar tv )
LC subst (extendVarEnv env tv arg)
extendLiftingContextEx :: LiftingContext
-> [(TyVar,Type)]
-> LiftingContext
extendLiftingContextEx lc [] = lc
extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
= let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
(extendVarEnv env v (mkSymCo $ mkCoherenceCo
(mkNomReflCo ty)
(ty_co_subst lc Nominal (tyVarKind v))))
in extendLiftingContextEx lc' rest
zapLiftingContext :: LiftingContext -> LiftingContext
zapLiftingContext (LC subst _) = LC (zapTCvSubst subst) emptyVarEnv
substForAllCoBndrCallbackLC :: Bool
-> (Coercion -> Coercion)
-> LiftingContext -> TyVar -> Coercion
-> (LiftingContext, TyVar, Coercion)
substForAllCoBndrCallbackLC sym sco (LC subst lc_env) tv co
= (LC subst' lc_env, tv', co')
where
(subst', tv', co') = substForAllCoBndrCallback sym sco subst tv co
ty_co_subst :: LiftingContext -> Role -> Type -> Coercion
ty_co_subst lc role ty
= go role ty
where
go :: Role -> Type -> Coercion
go Phantom ty = lift_phantom ty
go r (TyVarTy tv) = expectJust "ty_co_subst bad roles" $
liftCoSubstTyVar lc r tv
go r (AppTy ty1 ty2) = mkAppCo (go r ty1) (go Nominal ty2)
go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
go r (ForAllTy (Anon ty1) ty2)
= mkFunCo r (go r ty1) (go r ty2)
go r (ForAllTy (Named v _) ty)
= let (lc', v', h) = liftCoSubstVarBndr lc v in
mkForAllCo v' h $! ty_co_subst lc' r ty
go r ty@(LitTy {}) = ASSERT( r == Nominal )
mkReflCo r ty
go r (CastTy ty co) = castCoercionKind (go r ty) (substLeftCo lc co)
(substRightCo lc co)
go r (CoercionTy co) = mkProofIrrelCo r kco (substLeftCo lc co)
(substRightCo lc co)
where kco = go Nominal (coercionType co)
lift_phantom ty = mkPhantomCo (go Nominal (typeKind ty))
(substTy (lcSubstLeft lc) ty)
(substTy (lcSubstRight lc) ty)
liftCoSubstTyVar :: LiftingContext -> Role -> TyVar -> Maybe Coercion
liftCoSubstTyVar (LC subst env) r v
| Just co_arg <- lookupVarEnv env v
= downgradeRole_maybe r (coercionRole co_arg) co_arg
| otherwise
= Just $ Refl r (substTyVar subst v)
liftCoSubstVarBndr :: LiftingContext -> TyVar
-> (LiftingContext, TyVar, Coercion)
liftCoSubstVarBndr lc tv
= let (lc', tv', h, _) = liftCoSubstVarBndrCallback callback lc tv in
(lc', tv', h)
where
callback lc' ty' = (ty_co_subst lc' Nominal ty', ())
liftCoSubstVarBndrCallback :: (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> TyVar
-> (LiftingContext, TyVar, Coercion, a)
liftCoSubstVarBndrCallback fun lc@(LC subst cenv) old_var
= ( LC (subst `extendTCvInScope` new_var) new_cenv
, new_var, eta, stuff )
where
old_kind = tyVarKind old_var
(eta, stuff) = fun lc old_kind
Pair k1 _ = coercionKind eta
new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
lifted = Refl Nominal (TyVarTy new_var)
new_cenv = extendVarEnv cenv old_var lifted
isMappedByLC :: TyCoVar -> LiftingContext -> Bool
isMappedByLC tv (LC _ env) = tv `elemVarEnv` env
substLeftCo :: LiftingContext -> Coercion -> Coercion
substLeftCo lc co
= substCo (lcSubstLeft lc) co
substRightCo :: LiftingContext -> Coercion -> Coercion
substRightCo lc co
= substCo (lcSubstRight lc) co
swapLiftCoEnv :: LiftCoEnv -> LiftCoEnv
swapLiftCoEnv = mapVarEnv mkSymCo
lcSubstLeft :: LiftingContext -> TCvSubst
lcSubstLeft (LC subst lc_env) = liftEnvSubstLeft subst lc_env
lcSubstRight :: LiftingContext -> TCvSubst
lcSubstRight (LC subst lc_env) = liftEnvSubstRight subst lc_env
liftEnvSubstLeft :: TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstLeft = liftEnvSubst pFst
liftEnvSubstRight :: TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubstRight = liftEnvSubst pSnd
liftEnvSubst :: (forall a. Pair a -> a) -> TCvSubst -> LiftCoEnv -> TCvSubst
liftEnvSubst selector subst lc_env
= composeTCvSubst (TCvSubst emptyInScopeSet tenv cenv) subst
where
pairs = varEnvToList lc_env
(tpairs, cpairs) = partitionWith ty_or_co pairs
tenv = mkVarEnv_Directly tpairs
cenv = mkVarEnv_Directly cpairs
ty_or_co :: (Unique, Coercion) -> Either (Unique, Type) (Unique, Coercion)
ty_or_co (u, co)
| Just equality_co <- isCoercionTy_maybe equality_ty
= Right (u, equality_co)
| otherwise
= Left (u, equality_ty)
where
equality_ty = selector (coercionKind co)
lcTCvSubst :: LiftingContext -> TCvSubst
lcTCvSubst (LC subst _) = subst
lcInScopeSet :: LiftingContext -> InScopeSet
lcInScopeSet (LC subst _) = getTCvInScope subst
seqCo :: Coercion -> ()
seqCo (Refl r ty) = r `seq` seqType ty
seqCo (TyConAppCo r tc cos) = r `seq` tc `seq` seqCos cos
seqCo (AppCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (ForAllCo tv k co) = seqType (tyVarKind tv) `seq` seqCo k
`seq` seqCo co
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
seqCo (UnivCo p r t1 t2)
= seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
seqCo (SymCo co) = seqCo co
seqCo (TransCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (NthCo n co) = n `seq` seqCo co
seqCo (LRCo lr co) = lr `seq` seqCo co
seqCo (InstCo co arg) = seqCo co `seq` seqCo arg
seqCo (CoherenceCo co1 co2) = seqCo co1 `seq` seqCo co2
seqCo (KindCo co) = seqCo co
seqCo (SubCo co) = seqCo co
seqCo (AxiomRuleCo _ cs) = seqCos cs
seqProv :: UnivCoProvenance -> ()
seqProv UnsafeCoerceProv = ()
seqProv (PhantomProv co) = seqCo co
seqProv (ProofIrrelProv co) = seqCo co
seqProv (PluginProv _) = ()
seqProv (HoleProv _) = ()
seqCos :: [Coercion] -> ()
seqCos [] = ()
seqCos (co:cos) = seqCo co `seq` seqCos cos
coercionType :: Coercion -> Type
coercionType co = case coercionKindRole co of
(Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
coercionKind :: Coercion -> Pair Type
coercionKind co = go co
where
go (Refl _ ty) = Pair ty ty
go (TyConAppCo _ tc cos)= mkTyConApp tc <$> (sequenceA $ map go cos)
go (AppCo co1 co2) = mkAppTy <$> go co1 <*> go co2
go (ForAllCo tv1 k_co co)
= let Pair _ k2 = go k_co
tv2 = setTyVarKind tv1 k2
Pair ty1 ty2 = go co
subst = zipTvSubst [tv1] [TyVarTy tv2 `mk_cast_ty` mkSymCo k_co]
ty2' = substTyAddInScope subst ty2 in
mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2'
go (CoVarCo cv) = toPair $ coVarTypes cv
go (AxiomInstCo ax ind cos)
| CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
, cab_lhs = lhs, cab_rhs = rhs } <- coAxiomNthBranch ax ind
, let Pair tycos1 tycos2 = sequenceA (map go cos)
(tys1, cotys1) = splitAtList tvs tycos1
(tys2, cotys2) = splitAtList tvs tycos2
cos1 = map stripCoercionTy cotys1
cos2 = map stripCoercionTy cotys2
= ASSERT( cos `equalLength` (tvs ++ cvs) )
Pair (substTyWith tvs tys1 $
substTyWithCoVars cvs cos1 $
mkTyConApp (coAxiomTyCon ax) lhs)
(substTyWith tvs tys2 $
substTyWithCoVars cvs cos2 rhs)
go (UnivCo _ _ ty1 ty2) = Pair ty1 ty2
go (SymCo co) = swap $ go co
go (TransCo co1 co2) = Pair (pFst $ go co1) (pSnd $ go co2)
go g@(NthCo d co)
| Just argss <- traverse tyConAppArgs_maybe tys
= ASSERT( and $ ((d <) . length) <$> argss )
(`getNth` d) <$> argss
| d == 0
, Just splits <- traverse splitForAllTy_maybe tys
= (tyVarKind . fst) <$> splits
| otherwise
= pprPanic "coercionKind" (ppr g)
where
tys = go co
go (LRCo lr co) = (pickLR lr . splitAppTy) <$> go co
go (InstCo aco arg) = go_app aco [arg]
go (CoherenceCo g h)
= let Pair ty1 ty2 = go g in
Pair (mkCastTy ty1 h) ty2
go (KindCo co) = typeKind <$> go co
go (SubCo co) = go co
go (AxiomRuleCo ax cos) = expectJust "coercionKind" $
coaxrProves ax (map go cos)
go_app :: Coercion -> [Coercion] -> Pair Type
go_app (InstCo co arg) args = go_app co (arg:args)
go_app co args = piResultTys <$> go co <*> (sequenceA $ map go args)
mk_cast_ty :: Type -> Coercion -> Type
mk_cast_ty ty (Refl {}) = ty
mk_cast_ty ty co = CastTy ty co
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds tys = sequenceA $ map coercionKind tys
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole = go
where
go (Refl r ty) = (Pair ty ty, r)
go (TyConAppCo r tc cos)
= (mkTyConApp tc <$> (sequenceA $ map coercionKind cos), r)
go (AppCo co1 co2)
= let (tys1, r1) = go co1 in
(mkAppTy <$> tys1 <*> coercionKind co2, r1)
go (ForAllCo tv1 k_co co)
= let Pair _ k2 = coercionKind k_co
tv2 = setTyVarKind tv1 k2
(Pair ty1 ty2, r) = go co
subst = zipTvSubst [tv1] [TyVarTy tv2 `mkCastTy` mkSymCo k_co]
ty2' = substTyAddInScope subst ty2 in
(mkNamedForAllTy <$> Pair tv1 tv2 <*> pure Invisible <*> Pair ty1 ty2', r)
go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
go (UnivCo _ r ty1 ty2) = (Pair ty1 ty2, r)
go (SymCo co) = first swap $ go co
go (TransCo co1 co2)
= let (tys1, r) = go co1 in
(Pair (pFst tys1) (pSnd $ coercionKind co2), r)
go (NthCo d co)
| Just (tv1, _) <- splitForAllTy_maybe ty1
= ASSERT( d == 0 )
let (tv2, _) = splitForAllTy ty2 in
(tyVarKind <$> Pair tv1 tv2, Nominal)
| otherwise
= let (tc1, args1) = splitTyConApp ty1
(_tc2, args2) = splitTyConApp ty2
in
ASSERT( tc1 == _tc2 )
((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
where
(Pair ty1 ty2, r) = go co
go co@(LRCo {}) = (coercionKind co, Nominal)
go (InstCo co arg) = go_app co [arg]
go (CoherenceCo co1 co2)
= let (Pair t1 t2, r) = go co1 in
(Pair (t1 `mkCastTy` co2) t2, r)
go co@(KindCo {}) = (coercionKind co, Nominal)
go (SubCo co) = (coercionKind co, Representational)
go co@(AxiomRuleCo ax _) = (coercionKind co, coaxrRole ax)
go_app :: Coercion -> [Coercion] -> (Pair Type, Role)
go_app (InstCo co arg) args = go_app co (arg:args)
go_app co args
= let (pair, r) = go co in
(piResultTys <$> pair <*> (sequenceA $ map coercionKind args), r)
coercionRole :: Coercion -> Role
coercionRole = snd . coercionKindRole