module OptCoercion ( optCoercion, checkAxInstCo ) where
#include "HsVersions.h"
import GhcPrelude
import DynFlags
import TyCoRep
import TyCoSubst
import Coercion
import Type hiding( substTyVarBndr, substTy )
import TcType ( exactTyCoVarsOfType )
import TyCon
import CoAxiom
import VarSet
import VarEnv
import Outputable
import FamInstEnv ( flattenTys )
import Pair
import ListSetOps ( getNth )
import Util
import Unify
import InstEnv
import Control.Monad ( zipWithM )
optCoercion :: DynFlags -> TCvSubst -> Coercion -> NormalCo
optCoercion dflags env co
| hasNoOptCoercion dflags = substCo env co
| otherwise = optCoercion' env co
optCoercion' :: TCvSubst -> Coercion -> NormalCo
optCoercion' env co
| debugIsOn
= let out_co = opt_co1 lc False co
(Pair in_ty1 in_ty2, in_role) = coercionKindRole co
(Pair out_ty1 out_ty2, out_role) = coercionKindRole out_co
in
ASSERT2( substTyUnchecked env in_ty1 `eqType` out_ty1 &&
substTyUnchecked env in_ty2 `eqType` out_ty2 &&
in_role == out_role
, text "optCoercion changed types!"
$$ hang (text "in_co:") 2 (ppr co)
$$ hang (text "in_ty1:") 2 (ppr in_ty1)
$$ hang (text "in_ty2:") 2 (ppr in_ty2)
$$ hang (text "out_co:") 2 (ppr out_co)
$$ hang (text "out_ty1:") 2 (ppr out_ty1)
$$ hang (text "out_ty2:") 2 (ppr out_ty2)
$$ hang (text "subst:") 2 (ppr env) )
out_co
| otherwise = opt_co1 lc False co
where
lc = mkSubstLiftingContext env
type NormalCo = Coercion
type NormalNonIdCo = NormalCo
type SymFlag = Bool
type ReprFlag = Bool
opt_co1 :: LiftingContext
-> SymFlag
-> Coercion -> NormalCo
opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
opt_co2 :: LiftingContext
-> SymFlag
-> Role
-> Coercion -> NormalCo
opt_co2 env sym Phantom co = opt_phantom env sym co
opt_co2 env sym r co = opt_co3 env sym Nothing r co
opt_co3 :: LiftingContext -> SymFlag -> Maybe Role -> Role -> Coercion -> NormalCo
opt_co3 env sym (Just Phantom) _ co = opt_phantom env sym co
opt_co3 env sym (Just Representational) r co = opt_co4_wrap env sym True r co
opt_co3 env sym _ r co = opt_co4_wrap env sym False r co
opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
opt_co4_wrap = opt_co4
opt_co4 env _ rep r (Refl ty)
= ASSERT2( r == Nominal, text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr Nominal $$
text "Type:" <+> ppr ty )
liftCoSubst (chooseRole rep r) env ty
opt_co4 env _ rep r (GRefl _r ty MRefl)
= ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr _r $$
text "Type:" <+> ppr ty )
liftCoSubst (chooseRole rep r) env ty
opt_co4 env sym rep r (GRefl _r ty (MCo co))
= ASSERT2( r == _r, text "Expected role:" <+> ppr r $$
text "Found role:" <+> ppr _r $$
text "Type:" <+> ppr ty )
if isGReflCo co || isGReflCo co'
then liftCoSubst r' env ty
else wrapSym sym $ mkCoherenceRightCo r' ty' co' (liftCoSubst r' env ty)
where
r' = chooseRole rep r
ty' = substTy (lcSubstLeft env) ty
co' = opt_co4 env False False Nominal co
opt_co4 env sym rep r (SymCo co) = opt_co4_wrap env (not sym) rep r co
opt_co4 env sym rep r g@(TyConAppCo _r tc cos)
= ASSERT( r == _r )
case (rep, r) of
(True, Nominal) ->
mkTyConAppCo Representational tc
(zipWith3 (opt_co3 env sym)
(map Just (tyConRolesRepresentational tc))
(repeat Nominal)
cos)
(False, Nominal) ->
mkTyConAppCo Nominal tc (map (opt_co4_wrap env sym False Nominal) cos)
(_, Representational) ->
mkTyConAppCo r tc (zipWith (opt_co2 env sym)
(tyConRolesRepresentational tc)
cos)
(_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
opt_co4 env sym rep r (AppCo co1 co2)
= mkAppCo (opt_co4_wrap env sym rep r co1)
(opt_co4_wrap env sym False Nominal co2)
opt_co4 env sym rep r (ForAllCo tv k_co co)
= case optForAllCoBndr env sym tv k_co of
(env', tv', k_co') -> mkForAllCo tv' k_co' $
opt_co4_wrap env' sym rep r co
opt_co4 env sym rep r (FunCo _r co1 co2)
= ASSERT( r == _r )
if rep
then mkFunCo Representational co1' co2'
else mkFunCo r co1' co2'
where
co1' = opt_co4_wrap env sym rep r co1
co2' = opt_co4_wrap env sym rep r co2
opt_co4 env sym rep r (CoVarCo cv)
| Just co <- lookupCoVar (lcTCvSubst env) cv
= opt_co4_wrap (zapLiftingContext env) sym rep r co
| ty1 `eqType` ty2
= mkReflCo (chooseRole rep r) ty1
| otherwise
= ASSERT( isCoVar cv1 )
wrapRole rep r $ wrapSym sym $
CoVarCo cv1
where
Pair ty1 ty2 = coVarTypes cv1
cv1 = case lookupInScope (lcInScopeSet env) cv of
Just cv1 -> cv1
Nothing -> WARN( True, text "opt_co: not in scope:"
<+> ppr cv $$ ppr env)
cv
opt_co4 _ _ _ _ (HoleCo h)
= pprPanic "opt_univ fell into a hole" (ppr h)
opt_co4 env sym rep r (AxiomInstCo con ind cos)
= ASSERT( r == coAxiomRole con )
wrapRole rep (coAxiomRole con) $
wrapSym sym $
AxiomInstCo con ind (zipWith (opt_co2 env False)
(coAxBranchRoles (coAxiomNthBranch con ind))
cos)
opt_co4 env sym rep r (UnivCo prov _r t1 t2)
= ASSERT( r == _r )
opt_univ env sym prov (chooseRole rep r) t1 t2
opt_co4 env sym rep r (TransCo co1 co2)
| sym = opt_trans in_scope co2' co1'
| otherwise = opt_trans in_scope co1' co2'
where
co1' = opt_co4_wrap env sym rep r co1
co2' = opt_co4_wrap env sym rep r co2
in_scope = lcInScopeSet env
opt_co4 env _sym rep r (NthCo _r n co)
| Just (ty, _) <- isReflCo_maybe co
, Just (_tc, args) <- ASSERT( r == _r )
splitTyConApp_maybe ty
= liftCoSubst (chooseRole rep r) env (args `getNth` n)
| Just (ty, _) <- isReflCo_maybe co
, n == 0
, Just (tv, _) <- splitForAllTy_maybe ty
= liftCoSubst (chooseRole rep r) env (varType tv)
opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
= ASSERT( r == r1 )
opt_co4_wrap env sym rep r (cos `getNth` n)
opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
= ASSERT( r == _r )
ASSERT( n == 0 )
opt_co4_wrap env sym rep Nominal eta
opt_co4 env sym rep r (NthCo _r n co)
| TyConAppCo _ _ cos <- co'
, let nth_co = cos `getNth` n
= if rep && (r == Nominal)
then opt_co4_wrap (zapLiftingContext env) False True Nominal nth_co
else nth_co
| ForAllCo _ eta _ <- co'
= if rep
then opt_co4_wrap (zapLiftingContext env) False True Nominal eta
else eta
| otherwise
= wrapRole rep r $ NthCo r n co'
where
co' = opt_co1 env sym co
opt_co4 env sym rep r (LRCo lr co)
| Just pr_co <- splitAppCo_maybe co
= ASSERT( r == Nominal )
opt_co4_wrap env sym rep Nominal (pick_lr lr pr_co)
| Just pr_co <- splitAppCo_maybe co'
= ASSERT( r == Nominal )
if rep
then opt_co4_wrap (zapLiftingContext env) False True Nominal (pick_lr lr pr_co)
else pick_lr lr pr_co
| otherwise
= wrapRole rep Nominal $ LRCo lr co'
where
co' = opt_co4_wrap env sym False Nominal co
pick_lr CLeft (l, _) = l
pick_lr CRight (_, r) = r
opt_co4 env sym rep r (InstCo co1 arg)
| Just (tv, kind_co, co_body) <- splitForAllCo_ty_maybe co1
= opt_co4_wrap (extendLiftingContext env tv
(mkCoherenceRightCo Nominal t2 (mkSymCo kind_co) sym_arg))
sym rep r co_body
| Just (cv, kind_co, co_body) <- splitForAllCo_co_maybe co1
, CoercionTy h1 <- t1
, CoercionTy h2 <- t2
= let new_co = mk_new_co cv (opt_co4_wrap env sym False Nominal kind_co) h1 h2
in opt_co4_wrap (extendLiftingContext env cv new_co) sym rep r co_body
| Just (tv', kind_co', co_body') <- splitForAllCo_ty_maybe co1'
= opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
(mkCoherenceRightCo Nominal t2' (mkSymCo kind_co') arg'))
False False r' co_body'
| Just (cv', kind_co', co_body') <- splitForAllCo_co_maybe co1'
, CoercionTy h1' <- t1'
, CoercionTy h2' <- t2'
= let new_co = mk_new_co cv' kind_co' h1' h2'
in opt_co4_wrap (extendLiftingContext (zapLiftingContext env) cv' new_co)
False False r' co_body'
| otherwise = InstCo co1' arg'
where
co1' = opt_co4_wrap env sym rep r co1
r' = chooseRole rep r
arg' = opt_co4_wrap env sym False Nominal arg
sym_arg = wrapSym sym arg'
Pair t1 t2 = coercionKind sym_arg
Pair t1' t2' = coercionKind arg'
mk_new_co cv kind_co h1 h2
= let
r2 = coVarRole cv
kind_co' = downgradeRole r2 Nominal kind_co
n1 = mkNthCo r2 2 kind_co'
n2 = mkNthCo r2 3 kind_co'
in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
(n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
opt_co4 env sym _rep r (KindCo co)
= ASSERT( r == Nominal )
let kco' = promoteCoercion co in
case kco' of
KindCo co' -> promoteCoercion (opt_co1 env sym co')
_ -> opt_co4_wrap env sym False Nominal kco'
opt_co4 env sym _ r (SubCo co)
= ASSERT( r == Representational )
opt_co4_wrap env sym True Nominal co
opt_co4 env sym rep r (AxiomRuleCo co cs)
= ASSERT( r == coaxrRole co )
wrapRole rep r $
wrapSym sym $
AxiomRuleCo co (zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
opt_phantom :: LiftingContext -> SymFlag -> Coercion -> NormalCo
opt_phantom env sym co
= opt_univ env sym (PhantomProv (mkKindCo co)) Phantom ty1 ty2
where
Pair ty1 ty2 = coercionKind co
opt_univ :: LiftingContext -> SymFlag -> UnivCoProvenance -> Role
-> Type -> Type -> Coercion
opt_univ env sym (PhantomProv h) _r ty1 ty2
| sym = mkPhantomCo h' ty2' ty1'
| otherwise = mkPhantomCo h' ty1' ty2'
where
h' = opt_co4 env sym False Nominal h
ty1' = substTy (lcSubstLeft env) ty1
ty2' = substTy (lcSubstRight env) ty2
opt_univ env sym prov role oty1 oty2
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
, Just (tc2, tys2) <- splitTyConApp_maybe oty2
, tc1 == tc2
, equalLength tys1 tys2
= let roles = tyConRolesX role tc1
arg_cos = zipWith3 (mkUnivCo prov') roles tys1 tys2
arg_cos' = zipWith (opt_co4 env sym False) roles arg_cos
in
mkTyConAppCo role tc1 arg_cos'
| Just (tv1, ty1) <- splitForAllTy_ty_maybe oty1
, Just (tv2, ty2) <- splitForAllTy_ty_maybe oty2
= let k1 = tyVarKind tv1
k2 = tyVarKind tv2
eta = mkUnivCo prov' Nominal k1 k2
ty2' = substTyWith [tv2] [TyVarTy tv1 `mkCastTy` eta] ty2
(env', tv1', eta') = optForAllCoBndr env sym tv1 eta
in
mkForAllCo tv1' eta' (opt_univ env' sym prov' role ty1 ty2')
| Just (cv1, ty1) <- splitForAllTy_co_maybe oty1
, Just (cv2, ty2) <- splitForAllTy_co_maybe oty2
= let k1 = varType cv1
k2 = varType cv2
r' = coVarRole cv1
eta = mkUnivCo prov' Nominal k1 k2
eta_d = downgradeRole r' Nominal eta
n_co = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
(mkCoVarCo cv1) `mkTransCo`
(mkNthCo r' 3 eta_d)
ty2' = substTyWithCoVars [cv2] [n_co] ty2
(env', cv1', eta') = optForAllCoBndr env sym cv1 eta
in
mkForAllCo cv1' eta' (opt_univ env' sym prov' role ty1 ty2')
| otherwise
= let ty1 = substTyUnchecked (lcSubstLeft env) oty1
ty2 = substTyUnchecked (lcSubstRight env) oty2
(a, b) | sym = (ty2, ty1)
| otherwise = (ty1, ty2)
in
mkUnivCo prov' role a b
where
prov' = case prov of
UnsafeCoerceProv -> prov
PhantomProv kco -> PhantomProv $ opt_co4_wrap env sym False Nominal kco
ProofIrrelProv kco -> ProofIrrelProv $ opt_co4_wrap env sym False Nominal kco
PluginProv _ -> prov
opt_transList :: InScopeSet -> [NormalCo] -> [NormalCo] -> [NormalCo]
opt_transList is = zipWith (opt_trans is)
opt_trans :: InScopeSet -> NormalCo -> NormalCo -> NormalCo
opt_trans is co1 co2
| isReflCo co1 = co2
| otherwise = opt_trans1 is co1 co2
opt_trans1 :: InScopeSet -> NormalNonIdCo -> NormalCo -> NormalCo
opt_trans1 is co1 co2
| isReflCo co2 = co1
| otherwise = opt_trans2 is co1 co2
opt_trans2 :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> NormalCo
opt_trans2 is (TransCo co1a co1b) co2
= opt_trans is co1a (opt_trans is co1b co2)
opt_trans2 is co1 co2
| Just co <- opt_trans_rule is co1 co2
= co
opt_trans2 is co1 (TransCo co2a co2b)
| Just co1_2a <- opt_trans_rule is co1 co2a
= if isReflCo co1_2a
then co2b
else opt_trans1 is co1_2a co2b
opt_trans2 _ co1 co2
= mkTransCo co1 co2
opt_trans_rule :: InScopeSet -> NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo
opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
= ASSERT( r1 == r2 )
fireTransRule "GRefl" in_co1 in_co2 $
mkGReflRightCo r1 t1 (opt_trans is co1 co2)
opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
| d1 == d2
, coercionRole co1 == coercionRole co2
, co1 `compatible_co` co2
= ASSERT( r1 == r2 )
fireTransRule "PushNth" in_co1 in_co2 $
mkNthCo r1 d1 (opt_trans is co1 co2)
opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
| d1 == d2
, co1 `compatible_co` co2
= fireTransRule "PushLR" in_co1 in_co2 $
mkLRCo d1 (opt_trans is co1 co2)
opt_trans_rule is in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)
| ty1 `eqCoercion` ty2
, co1 `compatible_co` co2
= fireTransRule "TrPushInst" in_co1 in_co2 $
mkInstCo (opt_trans is co1 co2) ty1
opt_trans_rule is in_co1@(UnivCo p1 r1 tyl1 _tyr1)
in_co2@(UnivCo p2 r2 _tyl2 tyr2)
| Just prov' <- opt_trans_prov p1 p2
= ASSERT( r1 == r2 )
fireTransRule "UnivCo" in_co1 in_co2 $
mkUnivCo prov' r1 tyl1 tyr2
where
opt_trans_prov UnsafeCoerceProv UnsafeCoerceProv = Just UnsafeCoerceProv
opt_trans_prov (PhantomProv kco1) (PhantomProv kco2)
= Just $ PhantomProv $ opt_trans is kco1 kco2
opt_trans_prov (ProofIrrelProv kco1) (ProofIrrelProv kco2)
= Just $ ProofIrrelProv $ opt_trans is kco1 kco2
opt_trans_prov (PluginProv str1) (PluginProv str2) | str1 == str2 = Just p1
opt_trans_prov _ _ = Nothing
opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2)
| tc1 == tc2
= ASSERT( r1 == r2 )
fireTransRule "PushTyConApp" in_co1 in_co2 $
mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
opt_trans_rule is in_co1@(FunCo r1 co1a co1b) in_co2@(FunCo r2 co2a co2b)
= ASSERT( r1 == r2 )
fireTransRule "PushFun" in_co1 in_co2 $
mkFunCo r1 (opt_trans is co1a co2a) (opt_trans is co1b co2b)
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
= opt_trans_rule_app is in_co1 in_co2 co1a [co1b] co2a [co2b]
opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
| Just cos2 <- etaTyConAppCo_maybe tc co2
= ASSERT( cos1 `equalLength` cos2 )
fireTransRule "EtaCompL" co1 co2 $
mkTyConAppCo r tc (opt_transList is cos1 cos2)
opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
| Just cos1 <- etaTyConAppCo_maybe tc co1
= ASSERT( cos1 `equalLength` cos2 )
fireTransRule "EtaCompR" co1 co2 $
mkTyConAppCo r tc (opt_transList is cos1 cos2)
opt_trans_rule is co1@(AppCo co1a co1b) co2
| Just (co2a,co2b) <- etaAppCo_maybe co2
= opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
opt_trans_rule is co1 co2@(AppCo co2a co2b)
| Just (co1a,co1b) <- etaAppCo_maybe co1
= opt_trans_rule_app is co1 co2 co1a [co1b] co2a [co2b]
opt_trans_rule is co1 co2
| Just (tv1, eta1, r1) <- splitForAllCo_ty_maybe co1
, Just (tv2, eta2, r2) <- etaForAllCo_ty_maybe co2
= push_trans tv1 eta1 r1 tv2 eta2 r2
| Just (tv2, eta2, r2) <- splitForAllCo_ty_maybe co2
, Just (tv1, eta1, r1) <- etaForAllCo_ty_maybe co1
= push_trans tv1 eta1 r1 tv2 eta2 r2
where
push_trans tv1 eta1 r1 tv2 eta2 r2
= fireTransRule "EtaAllTy_ty" co1 co2 $
mkForAllCo tv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` tv1
r2' = substCoWithUnchecked [tv2] [mkCastTy (TyVarTy tv1) eta1] r2
opt_trans_rule is co1 co2
| Just (cv1, eta1, r1) <- splitForAllCo_co_maybe co1
, Just (cv2, eta2, r2) <- etaForAllCo_co_maybe co2
= push_trans cv1 eta1 r1 cv2 eta2 r2
| Just (cv2, eta2, r2) <- splitForAllCo_co_maybe co2
, Just (cv1, eta1, r1) <- etaForAllCo_co_maybe co1
= push_trans cv1 eta1 r1 cv2 eta2 r2
where
push_trans cv1 eta1 r1 cv2 eta2 r2
= fireTransRule "EtaAllTy_co" co1 co2 $
mkForAllCo cv1 (opt_trans is eta1 eta2) (opt_trans is' r1 r2')
where
is' = is `extendInScopeSet` cv1
role = coVarRole cv1
eta1' = downgradeRole role Nominal eta1
n1 = mkNthCo role 2 eta1'
n2 = mkNthCo role 3 eta1'
r2' = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
(mkCoVarCo cv1) `mkTransCo` n2])
r2
opt_trans_rule is co1 co2
| Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
, True <- sym
, Just cos2 <- matchAxiom sym con ind co2
, let newAxInst = AxiomInstCo con ind (opt_transList is (map mkSymCo cos2) cos1)
, Nothing <- checkAxInstCo newAxInst
= fireTransRule "TrPushSymAxR" co1 co2 $ SymCo newAxInst
| Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
, False <- sym
, Just cos2 <- matchAxiom sym con ind co2
, let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
, Nothing <- checkAxInstCo newAxInst
= fireTransRule "TrPushAxR" co1 co2 newAxInst
| Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
, True <- sym
, Just cos1 <- matchAxiom (not sym) con ind co1
, let newAxInst = AxiomInstCo con ind (opt_transList is cos2 (map mkSymCo cos1))
, Nothing <- checkAxInstCo newAxInst
= fireTransRule "TrPushSymAxL" co1 co2 $ SymCo newAxInst
| Just (sym, con, ind, cos2) <- co2_is_axiom_maybe
, False <- sym
, Just cos1 <- matchAxiom (not sym) con ind co1
, let newAxInst = AxiomInstCo con ind (opt_transList is cos1 cos2)
, Nothing <- checkAxInstCo newAxInst
= fireTransRule "TrPushAxL" co1 co2 newAxInst
| Just (sym1, con1, ind1, cos1) <- co1_is_axiom_maybe
, Just (sym2, con2, ind2, cos2) <- co2_is_axiom_maybe
, con1 == con2
, ind1 == ind2
, sym1 == not sym2
, let branch = coAxiomNthBranch con1 ind1
qtvs = coAxBranchTyVars branch ++ coAxBranchCoVars branch
lhs = coAxNthLHS con1 ind1
rhs = coAxBranchRHS branch
pivot_tvs = exactTyCoVarsOfType (if sym2 then rhs else lhs)
, all (`elemVarSet` pivot_tvs) qtvs
= fireTransRule "TrPushAxSym" co1 co2 $
if sym2
then liftCoSubstWith role qtvs (opt_transList is cos1 (map mkSymCo cos2)) lhs
else liftCoSubstWith role qtvs (opt_transList is (map mkSymCo cos1) cos2) rhs
where
co1_is_axiom_maybe = isAxiom_maybe co1
co2_is_axiom_maybe = isAxiom_maybe co2
role = coercionRole co1
opt_trans_rule _ co1 co2
| (Pair ty1 _, r) <- coercionKindRole co1
, Pair _ ty2 <- coercionKind co2
, ty1 `eqType` ty2
= fireTransRule "RedTypeDirRefl" co1 co2 $
mkReflCo r ty2
opt_trans_rule _ _ _ = Nothing
opt_trans_rule_app :: InScopeSet
-> Coercion
-> Coercion
-> Coercion
-> [Coercion]
-> Coercion
-> [Coercion]
-> Maybe Coercion
opt_trans_rule_app is orig_co1 orig_co2 co1a co1bs co2a co2bs
| AppCo co1aa co1ab <- co1a
, Just (co2aa, co2ab) <- etaAppCo_maybe co2a
= opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
| AppCo co2aa co2ab <- co2a
, Just (co1aa, co1ab) <- etaAppCo_maybe co1a
= opt_trans_rule_app is orig_co1 orig_co2 co1aa (co1ab:co1bs) co2aa (co2ab:co2bs)
| otherwise
= ASSERT( co1bs `equalLength` co2bs )
fireTransRule ("EtaApps:" ++ show (length co1bs)) orig_co1 orig_co2 $
let Pair _ rt1a = coercionKind co1a
(Pair lt2a _, rt2a) = coercionKindRole co2a
Pair _ rt1bs = traverse coercionKind co1bs
Pair lt2bs _ = traverse coercionKind co2bs
rt2bs = map coercionRole co2bs
kcoa = mkKindCo $ buildCoercion lt2a rt1a
kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
co2a' = mkCoherenceLeftCo rt2a lt2a kcoa co2a
co2bs' = zipWith3 mkGReflLeftCo rt2bs lt2bs kcobs
co2bs'' = zipWith mkTransCo co2bs' co2bs
in
mkAppCos (opt_trans is co1a co2a')
(zipWith (opt_trans is) co1bs co2bs'')
fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion
fireTransRule _rule _co1 _co2 res
= Just res
checkAxInstCo :: Coercion -> Maybe CoAxBranch
checkAxInstCo (AxiomInstCo ax ind cos)
= let branch = coAxiomNthBranch ax ind
tvs = coAxBranchTyVars branch
cvs = coAxBranchCoVars branch
incomps = coAxBranchIncomps branch
(tys, cotys) = splitAtList tvs (map (pFst . coercionKind) cos)
co_args = map stripCoercionTy cotys
subst = zipTvSubst tvs tys `composeTCvSubst`
zipCvSubst cvs co_args
target = Type.substTys subst (coAxBranchLHS branch)
in_scope = mkInScopeSet $
unionVarSets (map (tyCoVarsOfTypes . coAxBranchLHS) incomps)
flattened_target = flattenTys in_scope target in
check_no_conflict flattened_target incomps
where
check_no_conflict :: [Type] -> [CoAxBranch] -> Maybe CoAxBranch
check_no_conflict _ [] = Nothing
check_no_conflict flat (b@CoAxBranch { cab_lhs = lhs_incomp } : rest)
| SurelyApart <- tcUnifyTysFG instanceBindFun flat lhs_incomp
= check_no_conflict flat rest
| otherwise
= Just b
checkAxInstCo _ = Nothing
wrapSym :: SymFlag -> Coercion -> Coercion
wrapSym sym co | sym = mkSymCo co
| otherwise = co
wrapRole :: ReprFlag
-> Role
-> Coercion -> Coercion
wrapRole False _ = id
wrapRole True current = downgradeRole Representational current
chooseRole :: ReprFlag
-> Role
-> Role
chooseRole True _ = Representational
chooseRole _ r = r
isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom Branched, Int, [Coercion])
isAxiom_maybe (SymCo co)
| Just (sym, con, ind, cos) <- isAxiom_maybe co
= Just (not sym, con, ind, cos)
isAxiom_maybe (AxiomInstCo con ind cos)
= Just (False, con, ind, cos)
isAxiom_maybe _ = Nothing
matchAxiom :: Bool
-> CoAxiom br -> Int -> Coercion -> Maybe [Coercion]
matchAxiom sym ax@(CoAxiom { co_ax_tc = tc }) ind co
| CoAxBranch { cab_tvs = qtvs
, cab_cvs = []
, cab_roles = roles
, cab_lhs = lhs
, cab_rhs = rhs } <- coAxiomNthBranch ax ind
, Just subst <- liftCoMatch (mkVarSet qtvs)
(if sym then (mkTyConApp tc lhs) else rhs)
co
, all (`isMappedByLC` subst) qtvs
= zipWithM (liftCoSubstTyVar subst) roles qtvs
| otherwise
= Nothing
compatible_co :: Coercion -> Coercion -> Bool
compatible_co co1 co2
= x1 `eqType` x2
where
Pair _ x1 = coercionKind co1
Pair x2 _ = coercionKind co2
etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
etaForAllCo_ty_maybe co
| Just (tv, kind_co, r) <- splitForAllCo_ty_maybe co
= Just (tv, kind_co, r)
| Pair ty1 ty2 <- coercionKind co
, Just (tv1, _) <- splitForAllTy_ty_maybe ty1
, isForAllTy_ty ty2
, let kind_co = mkNthCo Nominal 0 co
= Just ( tv1, kind_co
, mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
| otherwise
= Nothing
etaForAllCo_co_maybe :: Coercion -> Maybe (CoVar, Coercion, Coercion)
etaForAllCo_co_maybe co
| Just (cv, kind_co, r) <- splitForAllCo_co_maybe co
= Just (cv, kind_co, r)
| Pair ty1 ty2 <- coercionKind co
, Just (cv1, _) <- splitForAllTy_co_maybe ty1
, isForAllTy_co ty2
= let kind_co = mkNthCo Nominal 0 co
r = coVarRole cv1
l_co = mkCoVarCo cv1
kind_co' = downgradeRole r Nominal kind_co
r_co = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
l_co `mkTransCo`
(mkNthCo r 3 kind_co')
in Just ( cv1, kind_co
, mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
| otherwise
= Nothing
etaAppCo_maybe :: Coercion -> Maybe (Coercion,Coercion)
etaAppCo_maybe co
| Just (co1,co2) <- splitAppCo_maybe co
= Just (co1,co2)
| (Pair ty1 ty2, Nominal) <- coercionKindRole co
, Just (_,t1) <- splitAppTy_maybe ty1
, Just (_,t2) <- splitAppTy_maybe ty2
, let isco1 = isCoercionTy t1
, let isco2 = isCoercionTy t2
, isco1 == isco2
= Just (LRCo CLeft co, LRCo CRight co)
| otherwise
= Nothing
etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
= ASSERT( tc == tc2 ) Just cos2
etaTyConAppCo_maybe tc co
| not (mustBeSaturated tc)
, (Pair ty1 ty2, r) <- coercionKindRole co
, Just (tc1, tys1) <- splitTyConApp_maybe ty1
, Just (tc2, tys2) <- splitTyConApp_maybe ty2
, tc1 == tc2
, isInjectiveTyCon tc r
, let n = length tys1
, tys2 `lengthIs` n
= ASSERT( tc == tc1 )
Just (decomposeCo n co (tyConRolesX r tc1))
| otherwise
= Nothing
optForAllCoBndr :: LiftingContext -> Bool
-> TyCoVar -> Coercion -> (LiftingContext, TyCoVar, Coercion)
optForAllCoBndr env sym
= substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env