module OptCoercion ( optCoercion, checkAxInstCo ) where
#include "HsVersions.h"
import GhcPrelude
import DynFlags
import TyCoRep
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( substTy env in_ty1 `eqType` out_ty1 &&
substTy 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 _r ty)
= 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 (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
= Refl (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 (Refl _r2 ty))
| Just (_tc, args) <- ASSERT( r == _r )
splitTyConApp_maybe ty
= liftCoSubst (chooseRole rep r) env (args `getNth` n)
| n == 0
, Just (tv, _) <- splitForAllTy_maybe ty
= liftCoSubst (chooseRole rep r) env (tyVarKind 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_maybe co1
= opt_co4_wrap (extendLiftingContext env tv
(arg' `mkCoherenceRightCo` mkSymCo kind_co))
sym rep r co_body
| Just (tv', kind_co', co_body') <- splitForAllCo_maybe co1'
= opt_co4_wrap (extendLiftingContext (zapLiftingContext env) tv'
(arg' `mkCoherenceRightCo` mkSymCo kind_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
opt_co4 env sym rep r (CoherenceCo co1 co2)
| TransCo col1 cor1 <- co1
= opt_co4_wrap env sym rep r (mkTransCo (mkCoherenceCo col1 co2) cor1)
| TransCo col1' cor1' <- co1'
= if sym then opt_trans in_scope col1'
(optCoercion' (zapTCvSubst (lcTCvSubst env))
(mkCoherenceRightCo cor1' co2'))
else opt_trans in_scope (mkCoherenceCo col1' co2') cor1'
| otherwise
= wrapSym sym $ mkCoherenceCo (opt_co4_wrap env False rep r co1) co2'
where co1' = opt_co4_wrap env sym rep r co1
co2' = opt_co4_wrap env False False Nominal co2
in_scope = lcInScopeSet env
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_maybe oty1
, Just (tv2, ty2) <- splitForAllTy_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')
| 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@(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
| ForAllCo tv1 eta1 r1 <- co1
, Just (tv2,eta2,r2) <- etaForAllCo_maybe co2
= push_trans tv1 eta1 r1 tv2 eta2 r2
| ForAllCo tv2 eta2 r2 <- co2
, Just (tv1,eta1,r1) <- etaForAllCo_maybe co1
= push_trans tv1 eta1 r1 tv2 eta2 r2
where
push_trans tv1 eta1 r1 tv2 eta2 r2
= fireTransRule "EtaAllTy" 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 (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 is co1 co2
| Just (lco, lh) <- isCohRight_maybe co1
, Just (rco, rh) <- isCohLeft_maybe co2
, (coercionType lh) `eqType` (coercionType rh)
= opt_trans_rule is lco rco
opt_trans_rule _ co1 co2
| (Pair ty1 _, r) <- coercionKindRole co1
, Pair _ ty2 <- coercionKind co2
, ty1 `eqType` ty2
= fireTransRule "RedTypeDirRefl" co1 co2 $
Refl 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 _ = coercionKind co2a
Pair _ rt1bs = traverse coercionKind co1bs
Pair lt2bs _ = traverse coercionKind co2bs
kcoa = mkKindCo $ buildCoercion lt2a rt1a
kcobs = map mkKindCo $ zipWith buildCoercion lt2bs rt1bs
co2a' = mkCoherenceLeftCo co2a kcoa
co2bs' = zipWith mkCoherenceLeftCo co2bs kcobs
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
isCohLeft_maybe :: Coercion -> Maybe (Coercion, Coercion)
isCohLeft_maybe (CoherenceCo co1 co2) = Just (co1, co2)
isCohLeft_maybe _ = Nothing
isCohRight_maybe :: Coercion -> Maybe (Coercion, Coercion)
isCohRight_maybe (SymCo (CoherenceCo co1 co2)) = Just (mkSymCo co1, co2)
isCohRight_maybe _ = Nothing
compatible_co :: Coercion -> Coercion -> Bool
compatible_co co1 co2
= x1 `eqType` x2
where
Pair _ x1 = coercionKind co1
Pair x2 _ = coercionKind co2
etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
etaForAllCo_maybe co
| ForAllCo tv kind_co r <- co
= Just (tv, kind_co, r)
| Pair ty1 ty2 <- coercionKind co
, Just (tv1, _) <- splitForAllTy_maybe ty1
, isForAllTy ty2
, let kind_co = mkNthCo Nominal 0 co
= Just ( tv1, kind_co
, mkInstCo co (mkNomReflCo (TyVarTy tv1) `mkCoherenceRightCo` kind_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
| mightBeUnsaturatedTyCon 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
-> TyVar -> Coercion -> (LiftingContext, TyVar, Coercion)
optForAllCoBndr env sym
= substForAllCoBndrUsingLC sym (opt_co4_wrap env sym False Nominal) env