module GHC.Core.Coercion (
Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionR,
UnivCoProvenance, CoercionHole(..), BlockSubstFlag(..),
coHoleCoVar, setCoHoleCoVar,
LeftOrRight(..),
Var, CoVar, TyCoVar,
Role(..), ltRole,
coVarTypes, coVarKind, coVarKindsTypesRole, coVarRole,
coercionType, mkCoercionType,
coercionKind, coercionLKind, coercionRKind,coercionKinds,
coercionRole, coercionKindRole,
mkGReflCo, mkReflCo, mkRepReflCo, mkNomReflCo,
mkCoVarCo, mkCoVarCos,
mkAxInstCo, mkUnbranchedAxInstCo,
mkAxInstRHS, mkUnbranchedAxInstRHS,
mkAxInstLHS, mkUnbranchedAxInstLHS,
mkPiCo, mkPiCos, mkCoCast,
mkSymCo, mkTransCo, mkTransMCo,
mkNthCo, nthCoRole, mkLRCo,
mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo,
mkForAllCo, mkForAllCos, mkHomoForAllCos,
mkPhantomCo,
mkHoleCo, mkUnivCo, mkSubCo,
mkAxiomInstCo, mkProofIrrelCo,
downgradeRole, mkAxiomRuleCo,
mkGReflRightCo, mkGReflLeftCo, mkCoherenceLeftCo, mkCoherenceRightCo,
mkKindCo,
castCoercionKind, castCoercionKind1, castCoercionKind2,
mkFamilyTyConAppCo,
mkHeteroCoercionType,
mkPrimEqPred, mkReprPrimEqPred, mkPrimEqPredRole,
mkHeteroPrimEqPred, mkHeteroReprPrimEqPred,
instNewTyCon_maybe,
NormaliseStepper, NormaliseStepResult(..), composeSteppers,
mapStepResult, unwrapNewTypeStepper,
topNormaliseNewType_maybe, topNormaliseTypeX,
decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
splitTyConAppCo_maybe,
splitAppCo_maybe,
splitFunCo_maybe,
splitForAllCo_maybe,
splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
pickLR,
isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
isReflCoVar_maybe, isGReflMCo, 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,
multToCo,
simplifyArgsWorker,
badCoercionHole, badCoercionHoleCo
) where
#include "HsVersions.h"
import GHC.CoreToIface (toIfaceTyCon, tidyToIfaceTcArgs)
import GHC.Prelude
import GHC.Iface.Type
import GHC.Core.TyCo.Rep
import GHC.Core.TyCo.FVs
import GHC.Core.TyCo.Ppr
import GHC.Core.TyCo.Subst
import GHC.Core.TyCo.Tidy
import GHC.Core.Type
import GHC.Core.TyCon
import GHC.Core.Coercion.Axiom
import GHC.Core.Utils ( mkFunctionType )
import GHC.Types.Var
import GHC.Types.Var.Env
import GHC.Types.Var.Set
import GHC.Types.Name hiding ( varName )
import GHC.Utils.Misc
import GHC.Types.Basic
import GHC.Utils.Outputable
import GHC.Types.Unique
import GHC.Data.Pair
import GHC.Types.SrcLoc
import GHC.Builtin.Names
import GHC.Builtin.Types.Prim
import GHC.Data.List.SetOps
import GHC.Data.Maybe
import GHC.Types.Unique.FM
import Control.Monad (foldM, zipWithM)
import Data.Function ( on )
import Data.Char( isDigit )
import qualified Data.Monoid as Monoid
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..(arity1)] `zip` rs ]
decomposeFunCo :: HasDebugCallStack
=> Role
-> Coercion
-> (CoercionN, Coercion, Coercion)
decomposeFunCo r co = ASSERT2( all_ok, ppr co )
(mkNthCo Nominal 0 co, mkNthCo r 3 co, mkNthCo r 4 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 (_w1, _s1, t1) <- splitFunTy_maybe k1
, Just (_w1, _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 _ w arg res) = Just (funTyCon, cos)
where cos = [w, mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
splitTyConAppCo_maybe _ = Nothing
multToCo :: Mult -> Coercion
multToCo r = mkNomReflCo r
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
coVarLType, coVarRType :: HasDebugCallStack => CoVar -> Type
coVarLType cv | (_, _, ty1, _, _) <- coVarKindsTypesRole cv = ty1
coVarRType cv | (_, _, _, ty2, _) <- coVarKindsTypesRole cv = ty2
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)
= (k1, k2, ty1, ty2, eqTyConRole tc)
| 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
= eqTyConRole (case tyConAppTyCon_maybe (varType cv) of
Just tc0 -> tc0
Nothing -> pprPanic "coVarRole: not tyconapp" (ppr cv))
eqTyConRole :: TyCon -> Role
eqTyConRole tc
| tc `hasKey` eqPrimTyConKey
= Nominal
| tc `hasKey` eqReprPrimTyConKey
= Representational
| otherwise
= pprPanic "eqTyConRole: unknown tycon" (ppr tc)
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
| [w, _rep1, _rep2, co1, co2] <- cos
, isFunTyCon tc
=
mkFunCo r w 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 -> CoercionN -> Coercion -> Coercion -> Coercion
mkFunCo r w co1 co2
| Just (ty1, _) <- isReflCo_maybe co1
, Just (ty2, _) <- isReflCo_maybe co2
, Just (w, _) <- isReflCo_maybe w
= mkReflCo r (mkVisFunTy w ty1 ty2)
| otherwise = FunCo r w 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) (multToCo Many) 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
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 w arg res)
= case n of
0 -> ASSERT( r == Nominal ) w
1 -> ASSERT( r == Nominal ) mkRuntimeRepCo arg
2 -> ASSERT( r == Nominal ) mkRuntimeRepCo res
3 -> ASSERT( r == r0 ) arg
4 -> 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
lty = coercionLKind co
r = coercionRole 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 w arg res)
= FunCo Representational w
(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 w co1 co2)
= do { co1' <- setNominalRole_maybe Representational co1
; co2' <- setNominalRole_maybe Representational co2
; return $ FunCo Nominal w 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 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 (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 4 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') }
castCoercionKind2 :: Coercion -> Role -> Type -> Type
-> CoercionN -> CoercionN -> Coercion
castCoercionKind2 g r t1 t2 h1 h2
= mkCoherenceRightCo r t2 h2 (mkCoherenceLeftCo r t1 h1 g)
castCoercionKind1 :: Coercion -> Role -> Type -> Type
-> CoercionN -> Coercion
castCoercionKind1 g r t1 t2 h
= case g of
Refl {} -> ASSERT( r == Nominal )
mkNomReflCo (mkCastTy t2 h)
GRefl _ _ mco -> case mco of
MRefl -> mkReflCo r (mkCastTy t2 h)
MCo kind_co -> GRefl r (mkCastTy t1 h) $
MCo (mkSymCo h `mkTransCo` kind_co `mkTransCo` h)
_ -> castCoercionKind2 g r t1 t2 h h
castCoercionKind :: Coercion -> CoercionN -> CoercionN -> Coercion
castCoercionKind g h1 h2
= castCoercionKind2 g r t1 t2 h1 h2
where
(Pair t1 t2, r) = coercionKindRole g
mkFamilyTyConAppCo :: TyCon -> [CoercionN] -> CoercionN
mkFamilyTyConAppCo tc cos
| Just (fam_tc, fam_tys) <- tyConFamInst_maybe tc
, let tvs = tyConTyVars tc
fam_cos = ASSERT2( tvs `equalLength` cos, ppr tc <+> ppr cos )
map (liftCoSubstWith Nominal tvs cos) fam_tys
= mkTyConAppCo Nominal fam_tc fam_cos
| otherwise
= mkTyConAppCo Nominal tc cos
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 (multToCo (varMult v)) (mkReflCo r (varType v)) co
| otherwise = mkFunCo r (multToCo (varMult v)) (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 (coercionLKind 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 _ w ty1 ty2) = mkFunCo r (go Nominal w) (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) = 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 $ 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
k1 = coercionLKind 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
k1 = coercionLKind 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 w co1 co2) = r `seq` seqCo w `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 (PhantomProv co) = seqCo co
seqProv (ProofIrrelProv co) = seqCo co
seqProv (PluginProv _) = ()
seqCos :: [Coercion] -> ()
seqCos [] = ()
seqCos (co:cos) = seqCo co `seq` seqCos cos
coercionKinds :: [Coercion] -> Pair [Type]
coercionKinds tys = sequenceA $ map coercionKind tys
coercionKindRole :: Coercion -> (Pair Type, Role)
coercionKindRole co = (coercionKind co, coercionRole co)
coercionType :: Coercion -> Type
coercionType co = case coercionKindRole co of
(Pair ty1 ty2, r) -> mkCoercionType r ty1 ty2
coercionKind :: Coercion -> Pair Type
coercionKind co = Pair (coercionLKind co) (coercionRKind co)
coercionLKind :: Coercion -> Type
coercionLKind co
= go co
where
go (Refl ty) = ty
go (GRefl _ ty _) = ty
go (TyConAppCo _ tc cos) = mkTyConApp tc (map go cos)
go (AppCo co1 co2) = mkAppTy (go co1) (go co2)
go (ForAllCo tv1 _ co1) = mkTyCoInvForAllTy tv1 (go co1)
go (FunCo _ w co1 co2) = mkFunctionType (go w) (go co1) (go co2)
go (CoVarCo cv) = coVarLType cv
go (HoleCo h) = coVarLType (coHoleCoVar h)
go (UnivCo _ _ ty1 _) = ty1
go (SymCo co) = coercionRKind co
go (TransCo co1 _) = go co1
go (LRCo lr co) = pickLR lr (splitAppTy (go co))
go (InstCo aco arg) = go_app aco [go arg]
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
go (NthCo _ d co) = go_nth d (go co)
go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
go (AxiomRuleCo ax cos) = pFst $ expectJust "coercionKind" $
coaxrProves ax $ map coercionKind cos
go_ax_inst ax ind tys
| CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
, cab_lhs = lhs } <- coAxiomNthBranch ax ind
, let (tys1, cotys1) = splitAtList tvs tys
cos1 = map stripCoercionTy cotys1
= ASSERT( tys `equalLength` (tvs ++ cvs) )
substTyWith tvs tys1 $
substTyWithCoVars cvs cos1 $
mkTyConApp (coAxiomTyCon ax) lhs
go_app :: Coercion -> [Type] -> Type
go_app (InstCo co arg) args = go_app co (go arg:args)
go_app co args = piResultTys (go co) args
go_nth :: Int -> Type -> Type
go_nth d ty
| Just args <- tyConAppArgs_maybe ty
= ASSERT( args `lengthExceeds` d )
args `getNth` d
| d == 0
, Just (tv,_) <- splitForAllTy_maybe ty
= tyVarKind tv
| otherwise
= pprPanic "coercionLKind:nth" (ppr d <+> ppr ty)
coercionRKind :: Coercion -> Type
coercionRKind co
= go co
where
go (Refl ty) = ty
go (GRefl _ ty MRefl) = ty
go (GRefl _ ty (MCo co1)) = mkCastTy ty co1
go (TyConAppCo _ tc cos) = mkTyConApp tc (map go cos)
go (AppCo co1 co2) = mkAppTy (go co1) (go co2)
go (CoVarCo cv) = coVarRType cv
go (HoleCo h) = coVarRType (coHoleCoVar h)
go (FunCo _ w co1 co2) = mkFunctionType (go w) (go co1) (go co2)
go (UnivCo _ _ _ ty2) = ty2
go (SymCo co) = coercionLKind co
go (TransCo _ co2) = go co2
go (LRCo lr co) = pickLR lr (splitAppTy (go co))
go (InstCo aco arg) = go_app aco [go arg]
go (KindCo co) = typeKind (go co)
go (SubCo co) = go co
go (NthCo _ d co) = go_nth d (go co)
go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
go (AxiomRuleCo ax cos) = pSnd $ expectJust "coercionKind" $
coaxrProves ax $ map coercionKind cos
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_ax_inst ax ind tys
| CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
, cab_rhs = rhs } <- coAxiomNthBranch ax ind
, let (tys2, cotys2) = splitAtList tvs tys
cos2 = map stripCoercionTy cotys2
= ASSERT( tys `equalLength` (tvs ++ cvs) )
substTyWith tvs tys2 $
substTyWithCoVars cvs cos2 rhs
go_app :: Coercion -> [Type] -> Type
go_app (InstCo co arg) args = go_app co (go arg:args)
go_app co args = piResultTys (go co) args
go_forall subst (ForAllCo tv1 k_co co)
| isTyVar tv1
= mkInfForAllTy tv2 (go_forall subst' co)
where
k2 = coercionRKind 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 cv2 (go_forall subst' co)
where
k2 = coercionRKind 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 (go other_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_mult = w1, ft_arg = arg1, ft_res = res1 })
(FunTy { ft_mult = w2, ft_arg = arg2, ft_res = res2 })
= mkFunCo Nominal (go w1 w2) (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 ])
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 (coercionRKind . 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"
bad_co_hole_ty :: Type -> Monoid.Any
bad_co_hole_co :: Coercion -> Monoid.Any
(bad_co_hole_ty, _, bad_co_hole_co, _)
= foldTyCo folder ()
where
folder = TyCoFolder { tcf_view = const Nothing
, tcf_tyvar = const2 (Monoid.Any False)
, tcf_covar = const2 (Monoid.Any False)
, tcf_hole = const hole
, tcf_tycobinder = const2
}
const2 :: a -> b -> c -> a
const2 x _ _ = x
hole :: CoercionHole -> Monoid.Any
hole (CoercionHole { ch_blocker = YesBlockSubst }) = Monoid.Any True
hole _ = Monoid.Any False
badCoercionHole :: Type -> Bool
badCoercionHole = Monoid.getAny . bad_co_hole_ty
badCoercionHoleCo :: Coercion -> Bool
badCoercionHoleCo = Monoid.getAny . bad_co_hole_co