module OptCoercion ( optCoercion, checkAxInstCo ) where
#include "HsVersions.h"
import Coercion
import Type hiding( substTyVarBndr, substTy, extendTvSubst )
import TcType ( exactTyVarsOfType )
import TyCon
import CoAxiom
import Var
import VarSet
import FamInstEnv ( flattenTys )
import VarEnv
import StaticFlags ( opt_NoOptCoercion )
import Outputable
import Pair
import FastString
import Util
import Unify
import ListSetOps
import InstEnv
import Control.Monad ( zipWithM )
optCoercion :: CvSubst -> Coercion -> NormalCo
optCoercion env co
| opt_NoOptCoercion = substCo env co
| otherwise = opt_co1 env False co
type NormalCo = Coercion
type NormalNonIdCo = NormalCo
type SymFlag = Bool
type ReprFlag = Bool
opt_co1 :: CvSubst
-> SymFlag
-> Coercion -> NormalCo
opt_co1 env sym co = opt_co2 env sym (coercionRole co) co
opt_co2 :: CvSubst
-> 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 :: CvSubst -> 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 env sym True r co
opt_co3 env sym _ r co = opt_co4 env sym False r co
opt_co4 :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
opt_co4 env _ rep r (Refl _r ty)
= ASSERT( r == _r )
Refl (chooseRole rep r) (substTy env ty)
opt_co4 env sym rep r (SymCo co) = opt_co4 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 (tyConRolesX Representational tc))
(repeat Nominal)
cos)
(False, Nominal) ->
mkTyConAppCo Nominal tc (map (opt_co4 env sym False Nominal) cos)
(_, Representational) ->
mkTyConAppCo r tc (zipWith (opt_co2 env sym)
(tyConRolesX r tc)
cos)
(_, Phantom) -> pprPanic "opt_co4 sees a phantom!" (ppr g)
opt_co4 env sym rep r (AppCo co1 co2) = mkAppCo (opt_co4 env sym rep r co1)
(opt_co4 env sym False Nominal co2)
opt_co4 env sym rep r (ForAllCo tv co)
= case substTyVarBndr env tv of
(env', tv') -> mkForAllCo tv' (opt_co4 env' sym rep r co)
opt_co4 env sym rep r (CoVarCo cv)
| Just co <- lookupCoVar env cv
= opt_co4 (zapCvSubstEnv env) sym rep r co
| Just cv1 <- lookupInScope (getCvInScope env) cv
= ASSERT( isCoVar cv1 ) wrapRole rep r $ wrapSym sym (CoVarCo cv1)
| otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)
ASSERT( isCoVar cv )
wrapRole rep r $ wrapSym sym (CoVarCo cv)
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 s _r oty1 oty2)
= ASSERT( r == _r )
opt_univ env s (chooseRole rep r) a b
where
(a,b) = if sym then (oty2,oty1) else (oty1,oty2)
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 env sym rep r co1
co2' = opt_co4 env sym rep r co2
in_scope = getCvInScope env
opt_co4 env sym rep r co@(NthCo {}) = opt_nth_co env sym rep r co
opt_co4 env sym rep r (LRCo lr co)
| Just pr_co <- splitAppCo_maybe co
= ASSERT( r == Nominal )
opt_co4 env sym rep Nominal (pickLR lr pr_co)
| Just pr_co <- splitAppCo_maybe co'
= ASSERT( r == Nominal )
if rep
then opt_co4 (zapCvSubstEnv env) False True Nominal (pickLR lr pr_co)
else pickLR lr pr_co
| otherwise
= wrapRole rep Nominal $ LRCo lr co'
where
co' = opt_co4 env sym False Nominal co
opt_co4 env sym rep r (InstCo co ty)
| Just (tv, co_body) <- splitForAllCo_maybe co
= opt_co4 (extendTvSubst env tv ty') sym rep r co_body
| Just (tv, co'_body) <- splitForAllCo_maybe co'
= substCoWithTy (getCvInScope env) tv ty' co'_body
| otherwise = InstCo co' ty'
where
co' = opt_co4 env sym rep r co
ty' = substTy env ty
opt_co4 env sym _ r (SubCo co)
= ASSERT( r == Representational )
opt_co4 env sym True Nominal co
opt_co4 env sym rep r (AxiomRuleCo co ts cs)
= ASSERT( r == coaxrRole co )
wrapRole rep r $
wrapSym sym $
AxiomRuleCo co (map (substTy env) ts)
(zipWith (opt_co2 env False) (coaxrAsmpRoles co) cs)
opt_phantom :: CvSubst -> SymFlag -> Coercion -> NormalCo
opt_phantom env sym co
= if sym
then opt_univ env (fsLit "opt_phantom") Phantom ty2 ty1
else opt_univ env (fsLit "opt_phantom") Phantom ty1 ty2
where
Pair ty1 ty2 = coercionKind co
opt_univ :: CvSubst -> FastString -> Role -> Type -> Type -> Coercion
opt_univ env prov role oty1 oty2
| Just (tc1, tys1) <- splitTyConApp_maybe oty1
, Just (tc2, tys2) <- splitTyConApp_maybe oty2
, tc1 == tc2
= mkTyConAppCo role tc1 (zipWith3 (opt_univ env prov) (tyConRolesX role tc1) tys1 tys2)
| Just (l1, r1) <- splitAppTy_maybe oty1
, Just (l2, r2) <- splitAppTy_maybe oty2
, typeKind l1 `eqType` typeKind l2
= let role' = if role == Phantom then Phantom else Nominal in
mkAppCo (opt_univ env prov role l1 l2) (opt_univ env prov role' r1 r2)
| Just (tv1, ty1) <- splitForAllTy_maybe oty1
, Just (tv2, ty2) <- splitForAllTy_maybe oty2
, tyVarKind tv1 `eqType` tyVarKind tv2
= case substTyVarBndr2 env tv1 tv2 of { (env1, env2, tv') ->
let ty1' = substTy env1 ty1
ty2' = substTy env2 ty2 in
mkForAllCo tv' (opt_univ (zapCvSubstEnv2 env1 env2) prov role ty1' ty2') }
| otherwise
= mkUnivCo prov role (substTy env oty1) (substTy env oty2)
opt_nth_co :: CvSubst -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
opt_nth_co env sym rep r = go []
where
go ns (NthCo n co) = go (n:ns) co
go ns co
= opt_nths ns co
opt_nths [] co = opt_co4 env sym rep r co
opt_nths (n:ns) (TyConAppCo _ _ cos) = opt_nths ns (cos `getNth` n)
opt_nths ns co = opt_nths' ns (opt_co1 env sym co)
opt_nths' [] co
= if rep && (r == Nominal)
then opt_co4 (zapCvSubstEnv env) False True r co
else co
opt_nths' (n:ns) (TyConAppCo _ _ cos) = opt_nths' ns (cos `getNth` n)
opt_nths' ns co = wrapRole rep r (mk_nths ns co)
mk_nths [] co = co
mk_nths (n:ns) co = mk_nths ns (mkNthCo n co)
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 d1 co1) in_co2@(NthCo d2 co2)
| d1 == d2
, co1 `compatible_co` co2
= fireTransRule "PushNth" in_co1 in_co2 $
mkNthCo 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 `eqType` ty2
, co1 `compatible_co` co2
= fireTransRule "TrPushInst" in_co1 in_co2 $
mkInstCo (opt_trans is co1 co2) ty1
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 $
TyConAppCo r1 tc1 (opt_transList is cos1 cos2)
opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
= fireTransRule "TrPushApp" in_co1 in_co2 $
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
opt_trans_rule is co1@(TyConAppCo r tc cos1) co2
| Just cos2 <- etaTyConAppCo_maybe tc co2
= ASSERT( length cos1 == length cos2 )
fireTransRule "EtaCompL" co1 co2 $
TyConAppCo r tc (opt_transList is cos1 cos2)
opt_trans_rule is co1 co2@(TyConAppCo r tc cos2)
| Just cos1 <- etaTyConAppCo_maybe tc co1
= ASSERT( length cos1 == length cos2 )
fireTransRule "EtaCompR" co1 co2 $
TyConAppCo r tc (opt_transList is cos1 cos2)
opt_trans_rule is co1@(AppCo co1a co1b) co2
| Just (co2a,co2b) <- etaAppCo_maybe co2
= fireTransRule "EtaAppL" co1 co2 $
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
opt_trans_rule is co1 co2@(AppCo co2a co2b)
| Just (co1a,co1b) <- etaAppCo_maybe co1
= fireTransRule "EtaAppR" co1 co2 $
mkAppCo (opt_trans is co1a co2a) (opt_trans is co1b co2b)
opt_trans_rule is co1 co2
| Just (tv1,r1) <- splitForAllCo_maybe co1
, Just (tv2,r2) <- etaForAllCo_maybe co2
, let r2' = substCoWithTy is' tv2 (mkTyVarTy tv1) r2
is' = is `extendInScopeSet` tv1
= fireTransRule "EtaAllL" co1 co2 $
mkForAllCo tv1 (opt_trans2 is' r1 r2')
| Just (tv2,r2) <- splitForAllCo_maybe co2
, Just (tv1,r1) <- etaForAllCo_maybe co1
, let r1' = substCoWithTy is' tv1 (mkTyVarTy tv2) r1
is' = is `extendInScopeSet` tv2
= fireTransRule "EtaAllR" co1 co2 $
mkForAllCo tv1 (opt_trans2 is' r1' r2)
opt_trans_rule is co1 co2
| Just (sym, con, ind, cos1) <- co1_is_axiom_maybe
, Just cos2 <- matchAxiom sym con ind co2
, True <- sym
, 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
, Just cos2 <- matchAxiom sym con ind co2
, False <- sym
, 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
, Just cos1 <- matchAxiom (not sym) con ind co1
, True <- sym
, 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
, Just cos1 <- matchAxiom (not sym) con ind co1
, False <- sym
, 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
lhs = coAxNthLHS con1 ind1
rhs = coAxBranchRHS branch
pivot_tvs = exactTyVarsOfType (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 $
Refl r ty2
opt_trans_rule _ _ _ = Nothing
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
incomps = coAxBranchIncomps branch
tys = map (pFst . coercionKind) cos
subst = zipOpenTvSubst tvs tys
target = Type.substTys subst (coAxBranchLHS branch)
in_scope = mkInScopeSet $
unionVarSets (map (tyVarsOfTypes . 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 = SymCo 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
substTyVarBndr2 :: CvSubst -> TyVar -> TyVar
-> (CvSubst, CvSubst, TyVar)
substTyVarBndr2 env tv1 tv2
= case substTyVarBndr env tv1 of
(env1, tv1') -> (env1, extendTvSubstAndInScope env tv2 (mkTyVarTy tv1'), tv1')
zapCvSubstEnv2 :: CvSubst -> CvSubst -> CvSubst
zapCvSubstEnv2 env1 env2 = mkCvSubst (is1 `unionInScope` is2) []
where is1 = getCvInScope env1
is2 = getCvInScope env2
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
= let (CoAxBranch { cab_tvs = qtvs
, cab_roles = roles
, cab_lhs = lhs
, cab_rhs = rhs }) = coAxiomNthBranch ax ind in
case liftCoMatch (mkVarSet qtvs) (if sym then (mkTyConApp tc lhs) else rhs) co of
Nothing -> Nothing
Just subst -> zipWithM (liftCoSubstTyVar subst) roles qtvs
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)
etaForAllCo_maybe co
| Just (tv, r) <- splitForAllCo_maybe co
= Just (tv, r)
| Pair ty1 ty2 <- coercionKind co
, Just (tv1, _) <- splitForAllTy_maybe ty1
, Just (tv2, _) <- splitForAllTy_maybe ty2
, tyVarKind tv1 `eqKind` tyVarKind tv2
= Just (tv1, mkInstCo co (mkTyVarTy tv1))
| 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
, typeKind t1 `eqType` typeKind t2
= 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
| isDecomposableTyCon tc
, Pair ty1 ty2 <- coercionKind co
, Just (tc1, tys1) <- splitTyConApp_maybe ty1
, Just (tc2, tys2) <- splitTyConApp_maybe ty2
, tc1 == tc2
, let n = length tys1
= ASSERT( tc == tc1 )
ASSERT( n == length tys2 )
Just (decomposeCo n co)
| otherwise
= Nothing