{-# 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 "HsVersions.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 = varName
setCoVarUnique :: CoVar -> Unique -> CoVar
setCoVarUnique = setVarUnique
setCoVarName :: CoVar -> Name -> CoVar
setCoVarName = setVarName
etaExpandCoAxBranch :: CoAxBranch -> ([TyVar], [Type], Type)
etaExpandCoAxBranch (CoAxBranch { cab_tvs = tvs
, cab_eta_tvs = eta_tvs
, cab_lhs = lhs
, cab_rhs = rhs })
= (tvs ++ eta_tvs, lhs ++ eta_tys, mkAppTys rhs eta_tys)
where
eta_tys = mkTyVarTys eta_tvs
pprCoAxiom :: CoAxiom br -> SDoc
pprCoAxiom ax@(CoAxiom { co_ax_tc = tc, co_ax_branches = branches })
= hang (text "axiom" <+> ppr ax <+> dcolon)
2 (vcat (map (pprCoAxBranchUser tc) (fromBranches branches)))
pprCoAxBranchUser :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchUser tc br
| isDataFamilyTyCon tc = pprCoAxBranchLHS tc br
| otherwise = pprCoAxBranch tc br
pprCoAxBranchLHS :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranchLHS = ppr_co_ax_branch pp_rhs
where
pp_rhs _ _ = empty
pprCoAxBranch :: TyCon -> CoAxBranch -> SDoc
pprCoAxBranch = ppr_co_ax_branch ppr_rhs
where
ppr_rhs env rhs = equals <+> pprPrecTypeX env topPrec rhs
ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
-> TyCon -> CoAxBranch -> SDoc
ppr_co_ax_branch ppr_rhs fam_tc branch
= foldr1 (flip hangNotEmpty 2)
[ pprUserForAll (mkTyCoVarBinders Inferred bndrs')
, pp_lhs <+> ppr_rhs tidy_env ee_rhs
, text "-- Defined" <+> pp_loc ]
where
loc = coAxBranchSpan branch
pp_loc | isGoodSrcSpan loc = text "at" <+> ppr (srcSpanStart loc)
| otherwise = text "in" <+> ppr loc
(ee_tvs, ee_lhs, ee_rhs) = etaExpandCoAxBranch branch
pp_lhs = pprIfaceTypeApp topPrec (toIfaceTyCon fam_tc)
(tidyToIfaceTcArgs tidy_env fam_tc ee_lhs)
(tidy_env, bndrs') = tidyCoAxBndrsForUser emptyTidyEnv ee_tvs
tidyCoAxBndrsForUser :: TidyEnv -> [Var] -> (TidyEnv, [Var])
tidyCoAxBndrsForUser init_env tcvs
= (tidy_env, reverse tidy_bndrs)
where
(tidy_env, tidy_bndrs) = foldl tidy_one (init_env, []) tcvs
tidy_one (env@(occ_env, subst), rev_bndrs') bndr
| is_wildcard bndr = (env_wild, rev_bndrs')
| otherwise = (env', bndr' : rev_bndrs')
where
(env', bndr') = tidyVarBndr env bndr
env_wild = (occ_env, extendVarEnv subst bndr wild_bndr)
wild_bndr = setVarName bndr $
tidyNameOcc (varName bndr) (mkTyVarOcc "_")
is_wildcard :: Var -> Bool
is_wildcard tv = case occNameString (getOccName tv) of
('_' : rest) -> all isDigit rest
_ -> False
decomposeCo :: Arity -> Coercion
-> [Role]
-> [Coercion]
decomposeCo arity co rs
= [mkNthCo r n co | (n,r) <- [0..(arity-1)] `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 (mkGReflLeftCo Nominal ty 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 co
| Just (ty, r) <- isReflCo_maybe co
= 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' )
| not (mustBeSaturated tc)
, Just (args', arg') <- snocView args
, Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
= Just ( mkTyConAppCo r tc args', arg'' )
splitAppCo_maybe co
| Just (ty, r) <- isReflCo_maybe co
, 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 (TyCoVar, Coercion, Coercion)
splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
splitForAllCo_maybe _ = Nothing
splitForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
splitForAllCo_ty_maybe (ForAllCo tv k_co co)
| isTyVar tv = Just (tv, k_co, co)
splitForAllCo_ty_maybe _ = Nothing
splitForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
splitForAllCo_co_maybe (ForAllCo cv k_co co)
| isCoVar cv = Just (cv, k_co, co)
splitForAllCo_co_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)
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 (mkReflCo (coVarRole cv) ty1)
| otherwise
= Nothing
isGReflCo :: Coercion -> Bool
isGReflCo (GRefl{}) = True
isGReflCo (Refl{}) = True
isGReflCo _ = False
isGReflMCo :: MCoercion -> Bool
isGReflMCo MRefl = True
isGReflMCo (MCo co) | isGReflCo co = True
isGReflMCo _ = False
isReflCo :: Coercion -> Bool
isReflCo (Refl{}) = True
isReflCo (GRefl _ _ mco) | isGReflMCo mco = True
isReflCo _ = False
isGReflCo_maybe :: Coercion -> Maybe (Type, Role)
isGReflCo_maybe (GRefl r ty _) = Just (ty, r)
isGReflCo_maybe (Refl ty) = Just (ty, Nominal)
isGReflCo_maybe _ = Nothing
isReflCo_maybe :: Coercion -> Maybe (Type, Role)
isReflCo_maybe (Refl ty) = Just (ty, Nominal)
isReflCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
isReflCo_maybe _ = Nothing
isReflexiveCo :: Coercion -> Bool
isReflexiveCo = isJust . isReflexiveCo_maybe
isReflexiveCo_maybe :: Coercion -> Maybe (Type, Role)
isReflexiveCo_maybe (Refl ty) = Just (ty, Nominal)
isReflexiveCo_maybe (GRefl r ty mco) | isGReflMCo mco = Just (ty, r)
isReflexiveCo_maybe co
| ty1 `eqType` ty2
= Just (ty1, r)
| otherwise
= Nothing
where (Pair ty1 ty2, r) = coercionKindRole co
coToMCo :: Coercion -> MCoercion
coToMCo c = if isReflCo c
then MRefl
else MCo c
mkGReflCo :: Role -> Type -> MCoercionN -> Coercion
mkGReflCo r ty mco
| isGReflMCo mco = if r == Nominal then Refl ty
else GRefl r ty MRefl
| otherwise = GRefl r ty mco
mkReflCo :: Role -> Type -> Coercion
mkReflCo Nominal ty = Refl ty
mkReflCo r ty = GRefl r ty MRefl
mkRepReflCo :: Type -> Coercion
mkRepReflCo ty = GRefl Representational ty MRefl
mkNomReflCo :: Type -> Coercion
mkNomReflCo = Refl
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
= mkReflCo 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
= mkReflCo r (mkVisFunTy ty1 ty2)
| otherwise = FunCo r co1 co2
mkAppCo :: Coercion
-> Coercion
-> Coercion
mkAppCo co arg
| Just (ty1, r) <- isReflCo_maybe co
, Just (ty2, _) <- isReflCo_maybe arg
= mkReflCo r (mkAppTy ty1 ty2)
| Just (ty1, r) <- isReflCo_maybe co
, 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
mkForAllCo :: TyCoVar -> CoercionN -> Coercion -> Coercion
mkForAllCo v kind_co co
| ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
, ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
, Just (ty, r) <- isReflCo_maybe co
, isGReflCo kind_co
= mkReflCo r (mkTyCoInvForAllTy v ty)
| otherwise
= ForAllCo v kind_co co
mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
mkForAllCo_NoRefl v kind_co co
| ASSERT( varType v `eqType` (pFst $ coercionKind kind_co)) True
, ASSERT( isTyVar v || almostDevoidCoVarOfCo v co) True
, ASSERT( not (isReflCo co)) True
, isCoVar v
, not (v `elemVarSet` tyCoVarsOfCo co)
= FunCo (coercionRole co) kind_co co
| otherwise
= ForAllCo v kind_co co
mkForAllCos :: [(TyCoVar, CoercionN)] -> Coercion -> Coercion
mkForAllCos bndrs co
| Just (ty, r ) <- isReflCo_maybe co
= let (refls_rev'd, non_refls_rev'd) = span (isReflCo . snd) (reverse bndrs) in
foldl' (flip $ uncurry mkForAllCo_NoRefl)
(mkReflCo r (mkTyCoInvForAllTys (reverse (map fst refls_rev'd)) ty))
non_refls_rev'd
| otherwise
= foldr (uncurry mkForAllCo_NoRefl) co bndrs
mkHomoForAllCos :: [TyCoVar] -> Coercion -> Coercion
mkHomoForAllCos vs co
| Just (ty, r) <- isReflCo_maybe co
= mkReflCo r (mkTyCoInvForAllTys vs ty)
| otherwise
= mkHomoForAllCos_NoRefl vs co
mkHomoForAllCos_NoRefl :: [TyCoVar] -> Coercion -> Coercion
mkHomoForAllCos_NoRefl vs orig_co
= ASSERT( not (isReflCo orig_co))
foldr go orig_co vs
where
go v co = mkForAllCo_NoRefl v (mkNomReflCo (varType v)) 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 = mkReflCo role ty1
| otherwise = UnivCo prov role ty1 ty2
mkSymCo :: Coercion -> Coercion
mkSymCo co | isReflCo co = co
mkSymCo (SymCo co) = co
mkSymCo (SubCo (SymCo co)) = SubCo co
mkSymCo co = SymCo co
mkTransCo :: Coercion -> Coercion -> Coercion
mkTransCo co1 co2 | isReflCo co1 = co2
| isReflCo co2 = co1
mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
= GRefl r t1 (MCo $ mkTransCo co1 co2)
mkTransCo co1 co2 = TransCo co1 co2
mkTransMCo :: MCoercion -> MCoercion -> MCoercion
mkTransMCo MRefl co2 = co2
mkTransMCo co1 MRefl = co1
mkTransMCo (MCo co1) (MCo co2) = MCo (mkTransCo 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 co
| Just (ty, _) <- isReflCo_maybe co
, Just (tv, _) <- splitForAllTy_maybe ty
=
ASSERT( r == Nominal )
mkNomReflCo (varType tv)
go r n co
| Just (ty, r0) <- isReflCo_maybe co
, let tc = tyConAppTyCon ty
= ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
ASSERT( nthRole r0 tc n == r )
mkReflCo r (tyConAppArgN n ty)
where 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 co
| Just (ty, eq) <- isReflCo_maybe co
= mkReflCo eq (pickLR lr (splitAppTy ty))
| otherwise
= LRCo lr co
mkInstCo :: Coercion -> Coercion -> Coercion
mkInstCo (ForAllCo tcv _kind_co body_co) co
| Just (arg, _) <- isReflCo_maybe co
= substCoUnchecked (zipTCvSubst [tcv] [arg]) body_co
mkInstCo co arg = InstCo co arg
mkGReflRightCo :: Role -> Type -> CoercionN -> Coercion
mkGReflRightCo r ty co
| isGReflCo co = mkReflCo r ty
| otherwise = GRefl r ty (MCo co)
mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
mkGReflLeftCo r ty co
| isGReflCo co = mkReflCo r ty
| otherwise = mkSymCo $ GRefl r ty (MCo co)
mkCoherenceLeftCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceLeftCo r ty co co2
| isGReflCo co = co2
| otherwise = (mkSymCo $ GRefl r ty (MCo co)) `mkTransCo` co2
mkCoherenceRightCo :: Role -> Type -> CoercionN -> Coercion -> Coercion
mkCoherenceRightCo r ty co co2
| isGReflCo co = co2
| otherwise = co2 `mkTransCo` GRefl r ty (MCo co)
mkKindCo :: Coercion -> Coercion
mkKindCo co | Just (ty, _) <- isReflCo_maybe co = Refl (typeKind ty)
mkKindCo (GRefl _ _ (MCo co)) = co
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 tk1
| otherwise
= KindCo co
mkSubCo :: Coercion -> Coercion
mkSubCo (Refl ty) = GRefl Representational ty MRefl
mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
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)
mkAxiomRuleCo :: CoAxiomRule -> [Coercion] -> Coercion
mkAxiomRuleCo = AxiomRuleCo
mkProofIrrelCo :: Role
-> Coercion
-> Coercion
-> Coercion
-> Coercion
mkProofIrrelCo r co g _ | isGReflCo co = mkReflCo r (mkCoercionTy 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 co@(Refl _) = Just co
setNominalRole_maybe_helper (GRefl _ ty co) = Just $ GRefl Nominal ty co
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 (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 _ -> ASSERT( False )
mkNomReflCo ki1
GRefl _ _ MRefl -> ASSERT( False )
mkNomReflCo ki1
GRefl _ _ (MCo co) -> co
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 tv _ g
| isTyVar tv
-> promoteCoercion g
ForAllCo _ _ _
-> ASSERT( False )
mkNomReflCo liftedTypeKind
FunCo _ _ _
-> ASSERT( False )
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 _
| isForAllTy_ty ty1
-> ASSERT( isForAllTy_ty ty2 )
promoteCoercion g
| otherwise
-> ASSERT( False)
mkNomReflCo liftedTypeKind
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_ty lty && isForAllTy_ty rty)
|| (isForAllTy_co lty && isForAllTy_co 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 -> Role -> Type -> Type
-> CoercionN -> CoercionN -> Coercion
castCoercionKind g r t1 t2 h1 h2
= mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
castCoercionKindI :: Coercion -> CoercionN -> CoercionN -> Coercion
castCoercionKindI g h1 h2
= mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
where (Pair t1 t2, r) = coercionKindRole g
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
| isCoVar v = ASSERT( not (v `elemVarSet` tyCoVarsOfCo co) )
mkFunCo r (mkReflCo r (varType 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]
-> [TyCoVar]
-> [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, substTys (lcSubstRight psi) (mkTyCoVarTys 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 = mkReflCo 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
-> TyCoVar
-> Coercion
-> LiftingContext
extendLiftingContext (LC subst env) tv arg
| Just (ty, _) <- isReflCo_maybe arg
= LC (extendTCvSubst subst tv ty) env
| otherwise
= LC subst (extendVarEnv env tv arg)
extendLiftingContextAndInScope :: LiftingContext
-> TyCoVar
-> Coercion
-> LiftingContext
extendLiftingContextAndInScope (LC subst env) tv co
= extendLiftingContext (LC (extendTCvInScopeSet subst (tyCoVarsOfCo co)) env) tv co
extendLiftingContextEx :: LiftingContext
-> [(TyCoVar,Type)]
-> LiftingContext
extendLiftingContextEx lc [] = lc
extendLiftingContextEx lc@(LC subst env) ((v,ty):rest)
| isTyVar v
= let lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfType ty)
(extendVarEnv env v $
mkGReflRightCo Nominal
ty
(ty_co_subst lc Nominal (tyVarKind v)))
in extendLiftingContextEx lc' rest
| CoercionTy co <- ty
=
ASSERT( isCoVar v )
let (_, _, s1, s2, r) = coVarKindsTypesRole v
lift_s1 = ty_co_subst lc r s1
lift_s2 = ty_co_subst lc r s2
kco = mkTyConAppCo Nominal (equalityTyCon r)
[ mkKindCo lift_s1, mkKindCo lift_s2
, lift_s1 , lift_s2 ]
lc' = LC (subst `extendTCvInScopeSet` tyCoVarsOfCo co)
(extendVarEnv env v
(mkProofIrrelCo Nominal kco co $
(mkSymCo lift_s1) `mkTransCo` co `mkTransCo` lift_s2))
in extendLiftingContextEx lc' rest
| otherwise
= pprPanic "extendLiftingContextEx" (ppr v <+> text "|->" <+> ppr ty)
zapLiftingContext :: LiftingContext -> LiftingContext
zapLiftingContext (LC subst _) = LC (zapTCvSubst subst) emptyVarEnv
substForAllCoBndrUsingLC :: Bool
-> (Coercion -> Coercion)
-> LiftingContext -> TyCoVar -> Coercion
-> (LiftingContext, TyCoVar, 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 t@(ForAllTy (Bndr v _) ty)
= let (lc', v', h) = liftCoSubstVarBndr lc v
body_co = ty_co_subst lc' r ty in
if isTyVar v' || almostDevoidCoVarOfCo v' body_co
then mkForAllCo v' h body_co
else pprPanic "ty_co_subst: covar is not almost devoid" (ppr t)
go r ty@(LitTy {}) = ASSERT( r == Nominal )
mkNomReflCo ty
go r (CastTy ty co) = castCoercionKindI (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 $ mkReflCo r (substTyVar subst v)
liftCoSubstVarBndr :: LiftingContext -> TyCoVar
-> (LiftingContext, TyCoVar, 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 -> (CoercionN, a))
-> LiftingContext -> TyCoVar
-> (LiftingContext, TyCoVar, CoercionN, a)
liftCoSubstVarBndrUsing fun lc old_var
| isTyVar old_var
= liftCoSubstTyVarBndrUsing fun lc old_var
| otherwise
= liftCoSubstCoVarBndrUsing fun lc old_var
liftCoSubstTyVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-> LiftingContext -> TyVar
-> (LiftingContext, TyVar, CoercionN, a)
liftCoSubstTyVarBndrUsing fun lc@(LC subst cenv) old_var
= ASSERT( isTyVar 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 = mkGReflRightCo Nominal (TyVarTy new_var) eta
new_cenv = extendVarEnv cenv old_var lifted
liftCoSubstCoVarBndrUsing :: (LiftingContext -> Type -> (CoercionN, a))
-> LiftingContext -> CoVar
-> (LiftingContext, CoVar, CoercionN, a)
liftCoSubstCoVarBndrUsing fun lc@(LC subst cenv) old_var
= ASSERT( isCoVar old_var )
( LC (subst `extendTCvInScope` new_var) new_cenv
, new_var, kind_co, stuff )
where
old_kind = coVarKind old_var
(eta, stuff) = fun lc old_kind
Pair k1 _ = coercionKind eta
new_var = uniqAway (getTCvInScope subst) (setVarType old_var k1)
role = coVarRole old_var
eta' = downgradeRole role Nominal eta
eta1 = mkNthCo role 2 eta'
eta2 = mkNthCo role 3 eta'
co1 = mkCoVarCo new_var
co2 = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
kind_co = mkTyConAppCo Nominal (equalityTyCon role)
[ mkKindCo co1, mkKindCo co2
, co1 , co2 ]
lifted = mkProofIrrelCo Nominal kind_co co1 co2
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
seqMCo :: MCoercion -> ()
seqMCo MRefl = ()
seqMCo (MCo co) = seqCo co
seqCo :: Coercion -> ()
seqCo (Refl ty) = seqType ty
seqCo (GRefl r ty mco) = r `seq` seqType ty `seq` seqMCo mco
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 (varType 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 (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 (GRefl _ ty MRefl) = Pair ty ty
go (GRefl _ ty (MCo co1)) = Pair ty (mkCastTy ty co1)
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)
| isGReflCo k_co = mkTyCoInvForAllTy tv1 <$> go co1
| otherwise = go_forall empty_subst co
where
empty_subst = mkEmptyTCvSubst (mkInScopeSet $ tyCoVarsOfCo co)
go (FunCo _ co1 co2) = mkVisFunTy <$> 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 (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)
| isTyVar tv1
= mkInvForAllTy <$> Pair tv1 tv2 <*> go_forall subst' co
where
Pair _ k2 = go k_co
tv2 = setTyVarKind tv1 (substTy subst k2)
subst' | isGReflCo k_co = extendTCvInScope subst tv1
| otherwise = extendTvSubst (extendTCvInScope subst tv2) tv1 $
TyVarTy tv2 `mkCastTy` mkSymCo k_co
go_forall subst (ForAllCo cv1 k_co co)
| isCoVar cv1
= mkTyCoInvForAllTy <$> Pair cv1 cv2 <*> go_forall subst' co
where
Pair _ k2 = go k_co
r = coVarRole cv1
eta1 = mkNthCo r 2 (downgradeRole r Nominal k_co)
eta2 = mkNthCo r 3 (downgradeRole r Nominal k_co)
cv2 = setVarType cv1 (substTy subst k2)
n_subst = eta1 `mkTransCo` (mkCoVarCo cv2) `mkTransCo` (mkSymCo eta2)
subst' | isReflCo k_co = extendTCvInScope subst cv1
| otherwise = extendCvSubst (extendTCvInScope subst cv2)
cv1 n_subst
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 _) = Nominal
go (GRefl 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 (KindCo {}) = Nominal
go (SubCo _) = Representational
go (AxiomRuleCo ax _) = coaxrRole ax
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"
mkPrimEqPred :: Type -> Type -> Type
mkPrimEqPred ty1 ty2
= mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
where
k1 = typeKind ty1
k2 = typeKind ty2
mkPrimEqPredRole :: Role -> Type -> Type -> PredType
mkPrimEqPredRole Nominal = mkPrimEqPred
mkPrimEqPredRole Representational = mkReprPrimEqPred
mkPrimEqPredRole Phantom = panic "mkPrimEqPredRole phantom"
mkHeteroPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
mkHeteroPrimEqPred k1 k2 ty1 ty2 = mkTyConApp eqPrimTyCon [k1, k2, ty1, ty2]
mkHeteroReprPrimEqPred :: Kind -> Kind -> Type -> Type -> Type
mkHeteroReprPrimEqPred k1 k2 ty1 ty2
= mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
mkReprPrimEqPred :: Type -> Type -> Type
mkReprPrimEqPred ty1 ty2
= mkTyConApp eqReprPrimTyCon [k1, k2, ty1, ty2]
where
k1 = typeKind ty1
k2 = typeKind ty2
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
= let co' = go ty1 ty2
r = coercionRole co'
in mkCoherenceLeftCo r ty1 co co'
go ty1 (CastTy ty2 co)
= let co' = go ty1 ty2
r = coercionRole co'
in mkCoherenceRightCo r ty2 co co'
go ty1@(TyVarTy tv1) _tyvarty
= ASSERT( case _tyvarty of
{ TyVarTy tv2 -> tv1 == tv2
; _ -> False } )
mkNomReflCo ty1
go (FunTy { ft_arg = arg1, ft_res = res1 })
(FunTy { ft_arg = arg2, ft_res = 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 (Bndr tv1 _flag1) ty1) (ForAllTy (Bndr tv2 _flag2) ty2)
| isTyVar tv1
= ASSERT( isTyVar tv2 )
mkForAllCo tv1 kind_co (go ty1 ty2')
where 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
go (ForAllTy (Bndr cv1 _flag1) ty1) (ForAllTy (Bndr cv2 _flag2) ty2)
= ASSERT( isCoVar cv1 && isCoVar cv2 )
mkForAllCo cv1 kind_co (go ty1 ty2')
where s1 = varType cv1
s2 = varType cv2
kind_co = go s1 s2
r = coVarRole cv1
kind_co' = downgradeRole r Nominal kind_co
eta1 = mkNthCo r 2 kind_co'
eta2 = mkNthCo r 3 kind_co'
subst = mkEmptyTCvSubst $ mkInScopeSet $
tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co
ty2' = substTy (extendCvSubst subst cv2 $ mkSymCo eta1 `mkTransCo`
mkCoVarCo cv1 `mkTransCo`
eta2)
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 ])
{-# INLINE simplifyArgsWorker #-}
simplifyArgsWorker :: [TyCoBinder] -> Kind
-> TyCoVarSet
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], CoercionN)
simplifyArgsWorker orig_ki_binders orig_inner_ki orig_fvs
orig_roles orig_simplified_args
= go [] [] orig_lc orig_ki_binders orig_inner_ki orig_roles orig_simplified_args
where
orig_lc = emptyLiftingContext $ mkInScopeSet $ orig_fvs
go :: [Type]
-> [Coercion]
-> LiftingContext
-> [TyCoBinder]
-> Kind
-> [Role]
-> [(Type, Coercion)]
-> ([Type], [Coercion], CoercionN)
go acc_xis acc_cos lc binders inner_ki _ []
= (reverse acc_xis, reverse acc_cos, kind_co)
where
final_kind = mkPiTys binders inner_ki
kind_co = liftCoSubst Nominal lc final_kind
go acc_xis acc_cos lc (binder:binders) inner_ki (role:roles) ((xi,co):args)
=
let kind_co = mkSymCo $
liftCoSubst Nominal lc (tyCoBinderType binder)
!casted_xi = xi `mkCastTy` kind_co
casted_co = mkCoherenceLeftCo role xi kind_co co
!new_lc | Just tv <- tyCoBinderVar_maybe binder
= extendLiftingContextAndInScope lc tv casted_co
| otherwise
= lc
in
go (casted_xi : acc_xis)
(casted_co : acc_cos)
new_lc
binders
inner_ki
roles
args
go acc_xis acc_cos lc [] inner_ki roles args
= let co1 = liftCoSubst Nominal lc inner_ki
co1_kind = coercionKind co1
unflattened_tys = map (pSnd . coercionKind . snd) args
(arg_cos, res_co) = decomposePiCos co1 co1_kind unflattened_tys
casted_args = ASSERT2( equalLength args arg_cos
, ppr args $$ ppr arg_cos )
[ (casted_xi, casted_co)
| ((xi, co), arg_co, role) <- zip3 args arg_cos roles
, let casted_xi = xi `mkCastTy` arg_co
casted_co = mkCoherenceLeftCo role xi arg_co co ]
zapped_lc = zapLiftingContext lc
Pair flattened_kind _ = co1_kind
(bndrs, new_inner) = splitPiTys flattened_kind
(xis_out, cos_out, res_co_out)
= go acc_xis acc_cos zapped_lc bndrs new_inner roles casted_args
in
(xis_out, cos_out, res_co_out `mkTransCo` res_co)
go _ _ _ _ _ _ _ = panic
"simplifyArgsWorker wandered into deeper water than usual"