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,
mkReflCo, mkRepReflCo, mkNomReflCo,
mkCoVarCo, mkCoVarCos,
mkAxInstCo, mkUnbranchedAxInstCo,
mkAxInstRHS, mkUnbranchedAxInstRHS,
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkTransAppCo,
mkNthCo, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos, mkHomoForAllCos_NoRefl,
mkPhantomCo,
mkUnsafeCo, mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
downgradeRole, maybeSubCo, mkAxiomRuleCo,
mkCoherenceCo, mkCoherenceRightCo, mkCoherenceLeftCo,
mkKindCo, castCoercionKind,
mkHeteroCoercionType,
instNewTyCon_maybe,
NormaliseStepper, NormaliseStepResult(..), composeSteppers,
mapStepResult, unwrapNewTypeStepper,
topNormaliseNewType_maybe, topNormaliseTypeX,
decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
splitTyConAppCo_maybe,
splitAppCo_maybe,
splitFunCo_maybe,
splitForAllCo_maybe,
nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
pickLR,
isReflCo, isReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
isReflCoVar_maybe,
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, pprCoAxBranchHdr,
tidyCo, tidyCos,
promoteCoercion, buildCoercion
) where
#include "HsVersions.h"
import GhcPrelude
import TyCoRep
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 ( eqPhantPrimTyCon )
import ListSetOps
import Maybes
import UniqFM
import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
coVarName :: CoVar -> Name
coVarName = varName
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName = setVarName
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_branches = branches })
= hang (text "axiom" <+> ppr ax <+> dcolon)
2 (vcat (map (ppr_co_ax_branch (\_ ty -> equals <+> pprType ty) ax) $
fromBranches branches))
pprCoAxBranch :: CoAxiom br -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch pprRhs
where
pprRhs fam_tc rhs
| isDataFamilyTyCon fam_tc
= empty
| otherwise
= equals <+> 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 (mkTyVarBinders Inferred (ee_tvs ++ cvs))
, pprTypeApp fam_tc ee_lhs <+> 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))
(ee_tvs, ee_lhs)
| Just (tycon, tc_args) <- splitTyConApp_maybe rhs
, isDataFamilyTyCon fam_tc
=
let tc_tvs = tyConTyVars tycon
etad_tvs = dropList tc_args tc_tvs
etad_tys = mkTyVarTys etad_tvs
eta_expanded_tvs = tvs `chkAppend` etad_tvs
eta_expanded_lhs = lhs `chkAppend` etad_tys
in (eta_expanded_tvs, eta_expanded_lhs)
| otherwise
= (tvs, lhs)
decomposeCo :: Arity -> Coercion
-> [Role]
-> [Coercion]
decomposeCo arity co rs
= [mkNthCo r n co | (n,r) <- [0..(arity1)] `zip` rs ]
decomposeFunCo :: HasDebugCallStack
=> Role
-> Coercion
-> (Coercion, Coercion)
decomposeFunCo r co = ASSERT2( all_ok, ppr co )
(mkNthCo r 2 co, mkNthCo r 3 co)
where
Pair s1t1 s2t2 = coercionKind co
all_ok = isFunTy s1t1 && isFunTy s2t2
decomposePiCos :: HasDebugCallStack
=> CoercionN -> Pair Type
-> [Type]
-> ([CoercionN], CoercionN)
decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
= go [] (orig_subst,orig_k1) orig_co (orig_subst,orig_k2) orig_args
where
orig_subst = mkEmptyTCvSubst $ mkInScopeSet $
tyCoVarsOfTypes orig_args `unionVarSet` tyCoVarsOfCo orig_co
go :: [CoercionN]
-> (TCvSubst,Kind)
-> CoercionN
-> (TCvSubst,Kind)
-> [Type]
-> ([CoercionN], Coercion)
go acc_arg_cos (subst1,k1) co (subst2,k2) (ty:tys)
| Just (a, t1) <- splitForAllTy_maybe k1
, Just (b, t2) <- splitForAllTy_maybe k2
= let arg_co = mkNthCo Nominal 0 (mkSymCo co)
res_co = mkInstCo co (mkNomReflCo ty `mkCoherenceLeftCo` arg_co)
subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
subst2' = extendTCvSubst subst2 b ty
in
go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
| Just (_s1, t1) <- splitFunTy_maybe k1
, Just (_s2, t2) <- splitFunTy_maybe k2
= let (sym_arg_co, res_co) = decomposeFunCo Nominal co
arg_co = mkSymCo sym_arg_co
in
go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
| not (isEmptyTCvSubst subst1) || not (isEmptyTCvSubst subst2)
= go acc_arg_cos (zapTCvSubst subst1, substTy subst1 k1)
co
(zapTCvSubst subst2, substTy subst1 k2)
(ty:tys)
go acc_arg_cos _ki1 co _ki2 _tys = (reverse acc_arg_cos, co)
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 (FunCo _ arg res) = Just (funTyCon, cos)
where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
splitTyConAppCo_maybe _ = Nothing
splitAppCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitAppCo_maybe (AppCo co arg) = Just (co, arg)
splitAppCo_maybe (TyConAppCo r tc args)
| args `lengthExceeds` tyConArity tc
, Just (args', arg') <- snocView args
= Just ( mkTyConAppCo r tc args', arg' )
| mightBeUnsaturatedTyCon tc
, Just (args', arg') <- snocView args
, Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) 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
splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
splitFunCo_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 :: HasDebugCallStack => CoVar -> Pair Type
coVarTypes cv
| (_, _, ty1, ty2, _) <- coVarKindsTypesRole cv
= Pair ty1 ty2
coVarKindsTypesRole :: HasDebugCallStack => 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"
mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
mkRuntimeRepCo co
= mkNthCo Nominal 0 kind_co
where
kind_co = mkKindCo co
isReflCoVar_maybe :: Var -> Maybe Coercion
isReflCoVar_maybe cv
| isCoVar cv
, Pair ty1 ty2 <- coVarTypes cv
, ty1 `eqType` ty2
= Just (Refl (coVarRole cv) ty1)
| otherwise
= Nothing
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 :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
mkTyConAppCo r tc cos
| tc `hasKey` funTyConKey
, [_rep1, _rep2, co1, co2] <- cos
=
mkFunCo r co1 co2
| 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
| Just (ty1, _) <- isReflCo_maybe co1
, Just (ty2, _) <- isReflCo_maybe co2
= Refl r (mkFunTy ty1 ty2)
| otherwise = FunCo r co1 co2
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
= mkTyConAppCo 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 -> mkTyConAppCo Nominal tc (args ++ [arg])
Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
where new_role = (tyConRolesRepresentational tc) !! (length args)
arg' = downgradeRole new_role Nominal arg
Phantom -> mkTyConAppCo 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 Nominal 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 (mkInvForAllTy tv 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 = CoVarCo 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( args `lengthIs` coAxiomArity ax index )
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 -> Coercion
mkHoleCo h = HoleCo h
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
mkNthCo :: HasDebugCallStack
=> Role
-> Int
-> Coercion
-> Coercion
mkNthCo r n co
= ASSERT2( good_call, bad_call_msg )
go r n co
where
Pair ty1 ty2 = coercionKind co
go r 0 (Refl _ ty)
| Just (tv, _) <- splitForAllTy_maybe ty
= ASSERT( r == Nominal )
Refl r (tyVarKind tv)
go r n (Refl r0 ty)
= ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
ASSERT( nthRole r0 tc n == r )
mkReflCo r (tyConAppArgN n ty)
where tc = tyConAppTyCon ty
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
go r 0 (ForAllCo _ kind_co _)
= ASSERT( r == Nominal )
kind_co
go r n co@(FunCo r0 arg res)
= case n of
0 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
1 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
2 -> ASSERT( r == r0 ) arg
3 -> ASSERT( r == r0 ) res
_ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
go r n (TyConAppCo r0 tc arg_cos) = ASSERT2( r == nthRole r0 tc n
, (vcat [ ppr tc
, ppr arg_cos
, ppr r0
, ppr n
, ppr r ]) )
arg_cos `getNth` n
go r n co =
NthCo r n co
bad_call_msg = vcat [ text "Coercion =" <+> ppr co
, text "LHS ty =" <+> ppr ty1
, text "RHS ty =" <+> ppr ty2
, text "n =" <+> ppr n, text "r =" <+> ppr r
, text "coercion role =" <+> ppr (coercionRole co) ]
good_call
| Just (_tv1, _) <- splitForAllTy_maybe ty1
, Just (_tv2, _) <- splitForAllTy_maybe ty2
= n == 0 && r == Nominal
| Just (tc1, tys1) <- splitTyConApp_maybe ty1
, Just (tc2, tys2) <- splitTyConApp_maybe ty2
, tc1 == tc2
= let len1 = length tys1
len2 = length tys2
good_role = case coercionRole co of
Nominal -> r == Nominal
Representational -> r == (tyConRolesRepresentational tc1 !! n)
Phantom -> r == Phantom
in len1 == len2 && n < len1 && good_role
| otherwise
= True
nthCoRole :: Int -> Coercion -> Role
nthCoRole n co
| Just (tc, _) <- splitTyConApp_maybe lty
= nthRole r tc n
| Just _ <- splitForAllTy_maybe lty
= Nominal
| otherwise
= pprPanic "nthCoRole" (ppr co)
where
(Pair lty _, r) = coercionKindRole 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
, let tk1 = typeKind ty1
tk2 = typeKind ty2
, tk1 `eqType` tk2
= Refl Nominal tk1
| 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 (FunCo Nominal arg res)
= FunCo Representational
(downgradeRole Representational Nominal arg)
(downgradeRole Representational Nominal res)
mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
SubCo co
downgradeRole_maybe :: Role
-> Role
-> Coercion -> Maybe Coercion
downgradeRole_maybe Nominal Nominal co = Just co
downgradeRole_maybe Nominal _ _ = Nothing
downgradeRole_maybe Representational Nominal co = Just (mkSubCo co)
downgradeRole_maybe Representational Representational co = Just co
downgradeRole_maybe Representational Phantom _ = Nothing
downgradeRole_maybe Phantom Phantom co = Just co
downgradeRole_maybe Phantom _ co = Just (toPhantomCo 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 :: Role
-> Coercion -> Maybe Coercion
setNominalRole_maybe r co
| r == Nominal = Just co
| otherwise = setNominalRole_maybe_helper co
where
setNominalRole_maybe_helper (SubCo co) = Just co
setNominalRole_maybe_helper (Refl _ ty) = Just $ Refl Nominal ty
setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
= do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
; return $ TyConAppCo Nominal tc cos' }
setNominalRole_maybe_helper (FunCo Representational co1 co2)
= do { co1' <- setNominalRole_maybe Representational co1
; co2' <- setNominalRole_maybe Representational co2
; return $ FunCo Nominal co1' co2'
}
setNominalRole_maybe_helper (SymCo co)
= SymCo <$> setNominalRole_maybe_helper co
setNominalRole_maybe_helper (TransCo co1 co2)
= TransCo <$> setNominalRole_maybe_helper co1 <*> setNominalRole_maybe_helper co2
setNominalRole_maybe_helper (AppCo co1 co2)
= AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
setNominalRole_maybe_helper (ForAllCo tv kind_co co)
= ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
setNominalRole_maybe_helper (NthCo _r n co)
= NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
setNominalRole_maybe_helper (InstCo co arg)
= InstCo <$> setNominalRole_maybe_helper co <*> pure arg
setNominalRole_maybe_helper (CoherenceCo co1 co2)
= CoherenceCo <$> setNominalRole_maybe_helper co1 <*> pure co2
setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
| case prov of UnsafeCoerceProv -> True
PhantomProv _ -> False
ProofIrrelProv _ -> True
PluginProv _ -> False
= Just $ UnivCo prov Nominal co1 co2
setNominalRole_maybe_helper _ = Nothing
mkPhantomCo :: Coercion -> Type -> Type -> Coercion
mkPhantomCo h t1 t2
= mkUnivCo (PhantomProv h) Phantom t1 t2
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 -> CoercionN
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
FunCo _ _ _
-> mkNomReflCo liftedTypeKind
CoVarCo {} -> mkKindCo co
HoleCo {} -> mkKindCo co
AxiomInstCo {} -> mkKindCo co
AxiomRuleCo {} -> mkKindCo co
UnivCo UnsafeCoerceProv _ t1 t2 -> mkUnsafeCo Nominal (typeKind t1) (typeKind t2)
UnivCo (PhantomProv kco) _ _ _ -> kco
UnivCo (ProofIrrelProv kco) _ _ _ -> kco
UnivCo (PluginProv _) _ _ _ -> mkKindCo co
SymCo g
-> mkSymCo (promoteCoercion g)
TransCo co1 co2
-> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
NthCo _ n co1
| Just (_, args) <- splitTyConAppCo_maybe co1
, args `lengthExceeds` n
-> 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
where
Pair ty1 ty2 = coercionKind co
ki1 = typeKind ty1
ki2 = typeKind ty2
instCoercion :: Pair Type
-> CoercionN
-> Coercion
-> Maybe CoercionN
instCoercion (Pair lty rty) g w
| isForAllTy lty && isForAllTy rty
, Just w' <- setNominalRole_maybe (coercionRole w) w
= Just $ mkInstCo g w'
| isFunTy lty && isFunTy rty
= Just $ mkNthCo Nominal 3 g
| otherwise
= Nothing
instCoercions :: CoercionN -> [Coercion] -> Maybe CoercionN
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 -> CoercionR -> Coercion
mkCoCast c g
| (g2:g1:_) <- reverse co_list
= mkSymCo g1 `mkTransCo` c `mkTransCo` g2
| otherwise
= pprPanic "mkCoCast" (ppr g $$ ppr (coercionKind g))
where
(tc, _) = splitTyConApp (pFst $ coercionKind g)
co_list = decomposeCo (tyConArity tc) g (tyConRolesRepresentational tc)
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 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 f (NS_Step rec_nts ty ev) = NS_Step rec_nts ty (f ev)
mapStepResult _ NS_Done = NS_Done
mapStepResult _ NS_Abort = NS_Abort
composeSteppers :: NormaliseStepper ev -> NormaliseStepper ev
-> NormaliseStepper ev
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 Coercion
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 :: NormaliseStepper ev -> (ev -> ev -> ev)
-> Type -> Maybe (ev, Type)
topNormaliseTypeX stepper plus ty
| Just (tc, tys) <- splitTyConApp_maybe ty
, NS_Step rec_nts ty' ev <- stepper initRecTc tc tys
= go rec_nts ev ty'
| otherwise
= Nothing
where
go rec_nts ev ty
| Just (tc, tys) <- splitTyConApp_maybe ty
= case stepper rec_nts tc tys of
NS_Step rec_nts' ty' ev' -> go rec_nts' (ev `plus` ev') ty'
NS_Done -> Just (ev, ty)
NS_Abort -> Nothing
| otherwise
= Just (ev, ty)
topNormaliseNewType_maybe :: Type -> Maybe (Coercion, Type)
topNormaliseNewType_maybe ty
= topNormaliseTypeX unwrapNewTypeStepper mkTransCo 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 :: HasDebugCallStack => 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 (Refl _ ty) = LC (extendTvSubst subst tv ty) env
extendLiftingContext (LC subst env) tv arg
= ASSERT( isTyVar tv )
LC subst (extendVarEnv env tv arg)
extendLiftingContextAndInScope :: LiftingContext
-> TyVar
-> Coercion
-> LiftingContext
extendLiftingContextAndInScope (LC subst env) tv co
= extendLiftingContext (LC (extendTCvInScopeSet subst (tyCoVarsOfCo co)) env) tv co
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
substForAllCoBndrUsingLC :: Bool
-> (Coercion -> Coercion)
-> LiftingContext -> TyVar -> Coercion
-> (LiftingContext, TyVar, Coercion)
substForAllCoBndrUsingLC sym sco (LC subst lc_env) tv co
= (LC subst' lc_env, tv', co')
where
(subst', tv', co') = substForAllCoBndrUsing 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 r ty | Just ty' <- coreView ty
= go r ty'
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 (FunTy ty1 ty2) = mkFunCo r (go r ty1) (go r ty2)
go r (ForAllTy (TvBndr 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, _) = liftCoSubstVarBndrUsing callback lc tv in
(lc', tv', h)
where
callback lc' ty' = (ty_co_subst lc' Nominal ty', ())
liftCoSubstVarBndrUsing :: (LiftingContext -> Type -> (Coercion, a))
-> LiftingContext -> TyVar
-> (LiftingContext, TyVar, Coercion, a)
liftCoSubstVarBndrUsing 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 = mkNomReflCo (TyVarTy new_var) `mkCoherenceRightCo` eta
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 = nonDetUFMToList 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 (FunCo r co1 co2) = r `seq` seqCo co1 `seq` seqCo co2
seqCo (CoVarCo cv) = cv `seq` ()
seqCo (HoleCo h) = coHoleCoVar h `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 r n co) = r `seq` 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 _) = ()
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 co@(ForAllCo tv1 k_co co1)
| isReflCo k_co = mkInvForAllTy tv1 <$> go co1
| otherwise = go_forall empty_subst co
where
empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
go (FunCo _ co1 co2) = mkFunTy <$> go co1 <*> go co2
go (CoVarCo cv) = coVarTypes cv
go (HoleCo h) = coVarTypes (coHoleCoVar h)
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 $ (`lengthExceeds` d) <$> 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)
go_forall subst (ForAllCo tv1 k_co co)
= mkInvForAllTy <$> Pair tv1 tv2 <*> go_forall subst' co
where
Pair _ k2 = go k_co
tv2 = setTyVarKind tv1 (substTy subst k2)
subst' | isReflCo k_co = extendTCvInScope subst tv1
| otherwise = extendTvSubst (extendTCvInScope subst tv2) tv1 $
TyVarTy tv2 `mkCastTy` mkSymCo k_co
go_forall subst other_co
= substTy subst `pLiftSnd` go other_co
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds tys = sequenceA $ map coercionKind tys
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole co = (coercionKind co, coercionRole co)
coercionRole :: Coercion -> Role
coercionRole = go
where
go (Refl r _) = r
go (TyConAppCo r _ _) = r
go (AppCo co1 _) = go co1
go (ForAllCo _ _ co) = go co
go (FunCo r _ _) = r
go (CoVarCo cv) = coVarRole cv
go (HoleCo h) = coVarRole (coHoleCoVar h)
go (AxiomInstCo ax _ _) = coAxiomRole ax
go (UnivCo _ r _ _) = r
go (SymCo co) = go co
go (TransCo co1 _co2) = go co1
go (NthCo r _d _co) = r
go (LRCo {}) = Nominal
go (InstCo co _) = go co
go (CoherenceCo co1 _) = go co1
go (KindCo {}) = Nominal
go (SubCo _) = Representational
go (AxiomRuleCo ax _) = coaxrRole ax
buildCoercion :: Type -> Type -> CoercionN
buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
where
go ty1 ty2 | Just ty1' <- coreView ty1 = go ty1' ty2
| Just ty2' <- coreView ty2 = go ty1 ty2'
go (CastTy ty1 co) ty2
= go ty1 ty2 `mkCoherenceLeftCo` co
go ty1 (CastTy ty2 co)
= go ty1 ty2 `mkCoherenceRightCo` co
go ty1@(TyVarTy tv1) _tyvarty
= ASSERT( case _tyvarty of
{ TyVarTy tv2 -> tv1 == tv2
; _ -> False } )
mkNomReflCo ty1
go (FunTy arg1 res1) (FunTy arg2 res2)
= mkFunCo Nominal (go arg1 arg2) (go res1 res2)
go (TyConApp tc1 args1) (TyConApp tc2 args2)
= ASSERT( tc1 == tc2 )
mkTyConAppCo Nominal tc1 (zipWith go args1 args2)
go (AppTy ty1a ty1b) ty2
| Just (ty2a, ty2b) <- repSplitAppTy_maybe ty2
= mkAppCo (go ty1a ty2a) (go ty1b ty2b)
go ty1 (AppTy ty2a ty2b)
| Just (ty1a, ty1b) <- repSplitAppTy_maybe ty1
= mkAppCo (go ty1a ty2a) (go ty1b ty2b)
go (ForAllTy (TvBndr tv1 _flag1) ty1) (ForAllTy (TvBndr tv2 _flag2) ty2)
= let kind_co = go (tyVarKind tv1) (tyVarKind tv2)
in_scope = mkInScopeSet $ tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
ty2' = substTyWithInScope in_scope [tv2]
[mkTyVarTy tv1 `mkCastTy` kind_co]
ty2
in
mkForAllCo tv1 kind_co (go ty1 ty2')
go ty1@(LitTy lit1) _lit2
= ASSERT( case _lit2 of
{ LitTy lit2 -> lit1 == lit2
; _ -> False } )
mkNomReflCo ty1
go (CoercionTy co1) (CoercionTy co2)
= mkProofIrrelCo Nominal kind_co co1 co2
where
kind_co = go (coercionType co1) (coercionType co2)
go ty1 ty2
= pprPanic "buildKindCoercion" (vcat [ ppr orig_ty1, ppr orig_ty2
, ppr ty1, ppr ty2 ])