\r
import Unify ( tcMatchTy )\r
import Coercion\r
-import Type\r
+import Type hiding( substTyVarBndr, substTy, extendTvSubst )\r
import TypeRep\r
import TyCon\r
import Var\r
import StaticFlags ( opt_NoOptCoercion )\r
import Util\r
import Outputable\r
+import Unify\r
+import Pair\r
+import Maybes( allMaybes )\r
+import FastString\r
\end{code}\r
\r
%************************************************************************\r
mkCoPredTy in the ForAll case, where this note appears. \r
\r
\begin{code}\r
-optCoercion :: TvSubst -> Coercion -> NormalCo\r
+optCoercion :: CvSubst -> Coercion -> NormalCo\r
-- ^ optCoercion applies a substitution to a coercion, \r
-- *and* optimises it to reduce its size\r
optCoercion env co \r
- | opt_NoOptCoercion = substTy env co\r
+ | opt_NoOptCoercion = substCo env co\r
| otherwise = opt_co env False co\r
\r
type NormalCo = Coercion\r
\r
type NormalNonIdCo = NormalCo -- Extra invariant: not the identity\r
\r
-opt_co, opt_co' :: TvSubst\r
+opt_co, opt_co' :: CvSubst\r
-> Bool -- True <=> return (sym co)\r
-> Coercion\r
-> NormalCo \r
opt_co = opt_co'\r
-\r
-{- Debuggery \r
-opt_co env sym co \r
--- = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
--- co1 `seq` \r
--- pprTrace "opt_co done }" (ppr co1) \r
--- WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (s1,t1) \r
--- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
- = WARN( not (coreEqType co1 simple_result), \r
+{-\r
+opt_co env sym co\r
+ = pprTrace "opt_co {" (ppr sym <+> ppr co $$ ppr env) $\r
+ co1 `seq`\r
+ pprTrace "opt_co done }" (ppr co1) $\r
+ (WARN( not same_co_kind, ppr co <+> dcolon <+> pprEqPred (Pair s1 t1)\r
+ $$ ppr co1 <+> dcolon <+> pprEqPred (Pair s2 t2) )\r
+ WARN( not (coreEqCoercion co1 simple_result),\r
(text "env=" <+> ppr env) $$\r
(text "input=" <+> ppr co) $$\r
(text "simple=" <+> ppr simple_result) $$\r
(text "opt=" <+> ppr co1) )\r
- co1\r
+ co1)\r
where\r
co1 = opt_co' env sym co\r
- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
- (s,t) = coercionKind (substTy env co)\r
+ same_co_kind = s1 `eqType` s2 && t1 `eqType` t2\r
+ Pair s t = coercionKind (substCo env co)\r
(s1,t1) | sym = (t,s)\r
| otherwise = (s,t)\r
- (s2,t2) = coercionKind co1\r
+ Pair s2 t2 = coercionKind co1\r
\r
- simple_result | sym = mkSymCoercion (substTy env co)\r
- | otherwise = substTy env co\r
+ simple_result | sym = mkSymCo (substCo env co)\r
+ | otherwise = substCo env co\r
-}\r
\r
-opt_co' env sym (AppTy ty1 ty2) = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (FunTy ty1 ty2) = FunTy (opt_co env sym ty1) (opt_co env sym ty2)\r
-opt_co' env sym (PredTy (ClassP cls tys)) = PredTy (ClassP cls (map (opt_co env sym) tys))\r
-opt_co' env sym (PredTy (IParam n ty)) = PredTy (IParam n (opt_co env sym ty))\r
-opt_co' _ _ co@(PredTy (EqPred {})) = pprPanic "optCoercion" (ppr co)\r
-\r
-opt_co' env sym co@(TyVarTy tv)\r
- | Just ty <- lookupTyVar env tv = opt_co' (zapTvSubstEnv env) sym ty\r
- | not (isCoVar tv) = co -- Identity; does not mention a CoVar\r
- | ty1 `coreEqType` ty2 = ty1 -- Identity; ..ditto..\r
- | not sym = co\r
- | otherwise = mkSymCoercion co\r
+opt_co' env _ (Refl ty) = Refl (substTy env ty)\r
+opt_co' env sym (SymCo co) = opt_co env (not sym) co\r
+opt_co' env sym (TyConAppCo tc cos) = TyConAppCo tc (map (opt_co env sym) cos)\r
+opt_co' env sym (AppCo co1 co2) = mkAppCo (opt_co env sym co1) (opt_co env sym co2)\r
+opt_co' env sym (ForAllCo tv co) = case substTyVarBndr env tv of\r
+ (env', tv') -> ForAllCo tv' (opt_co env' sym co)\r
+opt_co' env sym (CoVarCo cv)\r
+ | Just co <- lookupCoVar env cv\r
+ = opt_co (zapCvSubstEnv env) sym co\r
+\r
+ | Just cv1 <- lookupInScope (getCvInScope env) cv\r
+ = ASSERT( isCoVar cv1 ) wrapSym sym (CoVarCo cv1)\r
+ -- cv1 might have a substituted kind!\r
+\r
+ | otherwise = WARN( True, ptext (sLit "opt_co: not in scope:") <+> ppr cv $$ ppr env)\r
+ ASSERT( isCoVar cv )\r
+ wrapSym sym (CoVarCo cv)\r
+\r
+opt_co' env sym (AxiomInstCo con cos)\r
+ -- Do *not* push sym inside top-level axioms\r
+ -- e.g. if g is a top-level axiom\r
+ -- g a : f a ~ a\r
+ -- then (sym (g ty)) /= g (sym ty) !!\r
+ = wrapSym sym $ AxiomInstCo con (map (opt_co env False) cos)\r
+ -- Note that the_co does *not* have sym pushed into it\r
+\r
+opt_co' env sym (UnsafeCo ty1 ty2)\r
+ | ty1' `eqType` ty2' = Refl ty1'\r
+ | sym = mkUnsafeCo ty2' ty1'\r
+ | otherwise = mkUnsafeCo ty1' ty2'\r
where\r
- (ty1,ty2) = coVarKind tv\r
-\r
-opt_co' env sym (ForAllTy tv cor) \r
- | isTyVar tv = case substTyVarBndr env tv of\r
- (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)\r
+ ty1' = substTy env ty1\r
+ ty2' = substTy env ty2\r
\r
-opt_co' env sym co@(ForAllTy co_var cor) \r
- | isCoVar co_var \r
- = WARN( co_var `elemVarSet` tyVarsOfType cor, ppr co )\r
- ForAllTy co_var' cor'\r
+opt_co' env sym (TransCo co1 co2)\r
+ | sym = opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
+ | otherwise = opt_trans opt_co1 opt_co2\r
where\r
- (co1,co2) = coVarKind co_var\r
- co1' = opt_co' env sym co1\r
- co2' = opt_co' env sym co2\r
- cor' = opt_co' env sym cor\r
- co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))\r
- -- See Note [Subtle shadowing in coercions]\r
-\r
-opt_co' env sym (TyConApp tc cos)\r
- | Just (arity, desc) <- isCoercionTyCon_maybe tc\r
- = mkAppTys (opt_co_tc_app env sym tc desc (take arity cos))\r
- (map (opt_co env sym) (drop arity cos))\r
- | otherwise\r
- = TyConApp tc (map (opt_co env sym) cos)\r
-\r
---------\r
-opt_co_tc_app :: TvSubst -> Bool -> TyCon -> CoTyConDesc -> [Coercion] -> NormalCo\r
--- Used for CoercionTyCons only\r
--- Arguments are *not* already simplified/substituted\r
-opt_co_tc_app env sym tc desc cos\r
- = case desc of\r
- CoAxiom {} -- Do *not* push sym inside top-level axioms\r
- -- e.g. if g is a top-level axiom\r
- -- g a : F a ~ a\r
- -- Then (sym (g ty)) /= g (sym ty) !!\r
- | sym -> mkSymCoercion the_co \r
- | otherwise -> the_co\r
- where\r
- the_co = TyConApp tc (map (opt_co env False) cos)\r
- -- Note that the_co does *not* have sym pushed into it\r
- \r
- CoTrans \r
- | sym -> opt_trans opt_co2 opt_co1 -- sym (g `o` h) = sym h `o` sym g\r
- | otherwise -> opt_trans opt_co1 opt_co2\r
-\r
- CoUnsafe\r
- | sym -> mkUnsafeCoercion ty2' ty1'\r
- | otherwise -> mkUnsafeCoercion ty1' ty2'\r
-\r
- CoSym -> opt_co env (not sym) co1\r
- CoLeft -> opt_lr fst\r
- CoRight -> opt_lr snd\r
- CoCsel1 -> opt_csel fstOf3\r
- CoCsel2 -> opt_csel sndOf3\r
- CoCselR -> opt_csel thirdOf3\r
-\r
- CoInst -- See if the first arg is already a forall\r
- -- ...then we can just extend the current substitution\r
- | Just (tv, co1_body) <- splitForAllTy_maybe co1\r
- -> opt_co (extendTvSubst env tv ty2') sym co1_body\r
-\r
- -- See if is *now* a forall\r
- | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1\r
- -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
-\r
- | otherwise\r
- -> TyConApp tc [opt_co1, ty2']\r
+ opt_co1 = opt_co env sym co1\r
+ opt_co2 = opt_co env sym co2\r
\r
+opt_co' env sym (NthCo n co)\r
+ | TyConAppCo tc cos <- co'\r
+ , isDecomposableTyCon tc -- Not synonym families\r
+ = ASSERT( n < length cos )\r
+ cos !! n\r
+ | otherwise\r
+ = NthCo n co'\r
where\r
- (co1 : cos1) = cos\r
- (co2 : _) = cos1\r
+ co' = opt_co env sym co\r
\r
- ty1' = substTy env co1\r
- ty2' = substTy env co2\r
+opt_co' env sym (InstCo co ty)\r
+ -- See if the first arg is already a forall\r
+ -- ...then we can just extend the current substitution\r
+ | Just (tv, co_body) <- splitForAllCo_maybe co\r
+ = opt_co (extendTvSubst env tv ty') sym co_body\r
\r
- -- These opt_cos have the sym pushed into them\r
- opt_co1 = opt_co env sym co1\r
- opt_co2 = opt_co env sym co2\r
+ -- See if it is a forall after optimization\r
+ | Just (tv, co'_body) <- splitForAllCo_maybe co'\r
+ = substCoWithTy tv ty' co'_body -- An inefficient one-variable substitution\r
\r
- the_unary_opt_co = TyConApp tc [opt_co1]\r
+ | otherwise = InstCo co' ty'\r
\r
- opt_lr sel = case splitAppTy_maybe opt_co1 of\r
- Nothing -> the_unary_opt_co \r
- Just lr -> sel lr\r
- opt_csel sel = case splitCoPredTy_maybe opt_co1 of\r
- Nothing -> the_unary_opt_co \r
- Just lr -> sel lr\r
+ where\r
+ co' = opt_co env sym co\r
+ ty' = substTy env ty\r
\r
-------------\r
-opt_transL :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
-opt_transL = zipWith opt_trans\r
+opt_transList :: [NormalCo] -> [NormalCo] -> [NormalCo]\r
+opt_transList = zipWith opt_trans\r
\r
opt_trans :: NormalCo -> NormalCo -> NormalCo\r
opt_trans co1 co2\r
- | isIdNormCo co1 = co2\r
- | otherwise = opt_trans1 co1 co2\r
+ | isReflCo co1 = co2\r
+ | otherwise = opt_trans1 co1 co2\r
\r
opt_trans1 :: NormalNonIdCo -> NormalCo -> NormalCo\r
-- First arg is not the identity\r
opt_trans1 co1 co2\r
- | isIdNormCo co2 = co1\r
- | otherwise = opt_trans2 co1 co2\r
+ | isReflCo co2 = co1\r
+ | otherwise = opt_trans2 co1 co2\r
\r
opt_trans2 :: NormalNonIdCo -> NormalNonIdCo -> NormalCo\r
-- Neither arg is the identity\r
-opt_trans2 (TyConApp tc [co1a,co1b]) co2\r
- | tc `hasKey` transCoercionTyConKey\r
- = opt_trans1 co1a (opt_trans2 co1b co2)\r
+opt_trans2 (TransCo co1a co1b) co2\r
+ -- Don't know whether the sub-coercions are the identity\r
+ = opt_trans co1a (opt_trans co1b co2) \r
\r
opt_trans2 co1 co2 \r
| Just co <- opt_trans_rule co1 co2\r
= co\r
\r
-opt_trans2 co1 (TyConApp tc [co2a,co2b])\r
- | tc `hasKey` transCoercionTyConKey\r
- , Just co1_2a <- opt_trans_rule co1 co2a\r
- = if isIdNormCo co1_2a\r
+opt_trans2 co1 (TransCo co2a co2b)\r
+ | Just co1_2a <- opt_trans_rule co1 co2a\r
+ = if isReflCo co1_2a\r
then co2b\r
- else opt_trans2 co1_2a co2b\r
+ else opt_trans1 co1_2a co2b\r
\r
opt_trans2 co1 co2\r
- = mkTransCoercion co1 co2\r
+ = mkTransCo co1 co2\r
\r
------\r
+-- Optimize coercions with a top-level use of transitivity.\r
opt_trans_rule :: NormalNonIdCo -> NormalNonIdCo -> Maybe NormalCo\r
-opt_trans_rule (TyConApp tc1 args1) (TyConApp tc2 args2)\r
- | tc1 == tc2\r
- = case isCoercionTyCon_maybe tc1 of\r
- Nothing \r
- -> Just (TyConApp tc1 (opt_transL args1 args2))\r
- Just (arity, desc) \r
- | arity == length args1\r
- -> opt_trans_rule_equal_tc desc args1 args2\r
- | otherwise\r
- -> case opt_trans_rule_equal_tc desc \r
- (take arity args1) \r
- (take arity args2) of\r
- Just co -> Just $ mkAppTys co $ \r
- opt_transL (drop arity args1) (drop arity args2)\r
- Nothing -> Nothing \r
- \r
--- Push transitivity inside apply\r
-opt_trans_rule co1 co2\r
- | Just (co1a, co1b) <- splitAppTy_maybe co1\r
- , Just (co2a, co2b) <- etaApp_maybe co2\r
- = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
\r
- | Just (co2a, co2b) <- splitAppTy_maybe co2\r
- , Just (co1a, co1b) <- etaApp_maybe co1\r
- = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
+-- push transitivity down through matching top-level constructors.\r
+opt_trans_rule in_co1@(TyConAppCo tc1 cos1) in_co2@(TyConAppCo tc2 cos2)\r
+ | tc1 == tc2 = fireTransRule "PushTyConApp" in_co1 in_co2 $\r
+ TyConAppCo tc1 (opt_transList cos1 cos2)\r
+\r
+-- push transitivity through matching destructors\r
+opt_trans_rule in_co1@(NthCo d1 co1) in_co2@(NthCo d2 co2)\r
+ | d1 == d2\r
+ , co1 `compatible_co` co2\r
+ = fireTransRule "PushNth" in_co1 in_co2 $\r
+ mkNthCo d1 (opt_trans co1 co2)\r
\r
+-- Push transitivity inside instantiation\r
+opt_trans_rule in_co1@(InstCo co1 ty1) in_co2@(InstCo co2 ty2)\r
+ | ty1 `eqType` ty2\r
+ , co1 `compatible_co` co2\r
+ = fireTransRule "TrPushInst" in_co1 in_co2 $\r
+ mkInstCo (opt_trans co1 co2) ty1\r
+ \r
+-- Push transitivity inside apply\r
+opt_trans_rule in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)\r
+ = fireTransRule "TrPushApp" in_co1 in_co2 $\r
+ mkAppCo (opt_trans co1a co2a) (opt_trans co1b co2b)\r
+\r
+-- Push transitivity inside PredCos\r
+opt_trans_rule in_co1@(PredCo pco1) in_co2@(PredCo pco2)\r
+ | Just pco' <- opt_trans_pred pco1 pco2\r
+ = fireTransRule "TrPushPrd" in_co1 in_co2 $\r
+ mkPredCo pco'\r
+\r
+opt_trans_rule co1@(TyConAppCo tc cos1) co2\r
+ | Just cos2 <- etaTyConAppCo_maybe tc co2\r
+ = ASSERT( length cos1 == length cos2 )\r
+ fireTransRule "EtaCompL" co1 co2 $\r
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)\r
+\r
+opt_trans_rule co1 co2@(TyConAppCo tc cos2)\r
+ | Just cos1 <- etaTyConAppCo_maybe tc co1\r
+ = ASSERT( length cos1 == length cos2 )\r
+ fireTransRule "EtaCompR" co1 co2 $\r
+ TyConAppCo tc (zipWith opt_trans cos1 cos2)\r
+\r
+\r
+{- BAY: think harder about this. do we still need it?\r
-- Push transitivity inside (s~t)=>r\r
-- We re-use the CoVar rather than using mkCoPredTy\r
-- See Note [Subtle shadowing in coercions]\r
, isCoVar cv1\r
, Just (s1,t1) <- coVarKind_maybe cv1\r
, Just (s2,t2,r2) <- etaCoPred_maybe co2\r
- = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
+ = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoType (opt_trans s1 s2) (opt_trans t1 t2)))\r
(opt_trans r1 r2))\r
\r
| Just (cv2,r2) <- splitForAllTy_maybe co2\r
, isCoVar cv2\r
, Just (s2,t2) <- coVarKind_maybe cv2\r
, Just (s1,t1,r1) <- etaCoPred_maybe co1\r
- = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
+ = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoType (opt_trans s1 s2) (opt_trans t1 t2)))\r
(opt_trans r1 r2))\r
+-}\r
\r
-- Push transitivity inside forall\r
opt_trans_rule co1 co2\r
- | Just (tv1,r1) <- splitTypeForAll_maybe co1\r
- , Just (tv2,r2) <- etaForAll_maybe co2\r
- , let r2' = substTyWith [tv2] [TyVarTy tv1] r2\r
- = Just (ForAllTy tv1 (opt_trans2 r1 r2'))\r
-\r
- | Just (tv2,r2) <- splitTypeForAll_maybe co2\r
- , Just (tv1,r1) <- etaForAll_maybe co1\r
- , let r1' = substTyWith [tv1] [TyVarTy tv2] r1\r
- = Just (ForAllTy tv1 (opt_trans2 r1' r2))\r
-\r
+ | Just (tv1,r1) <- splitForAllCo_maybe co1\r
+ , Just (tv2,r2) <- etaForAllCo_maybe co2\r
+ , let r2' = substCoWithTy tv2 (mkTyVarTy tv1) r2\r
+ = fireTransRule "EtaAllL" co1 co2 $\r
+ mkForAllCo tv1 (opt_trans2 r1 r2')\r
+\r
+ | Just (tv2,r2) <- splitForAllCo_maybe co2\r
+ , Just (tv1,r1) <- etaForAllCo_maybe co1\r
+ , let r1' = substCoWithTy tv1 (mkTyVarTy tv2) r1\r
+ = fireTransRule "EtaAllR" co1 co2 $\r
+ mkForAllCo tv1 (opt_trans2 r1' r2)\r
+\r
+-- Push transitivity inside axioms\r
opt_trans_rule co1 co2\r
-{- Omitting for now, because unsound\r
- | Just (sym1, (ax_tc1, ax1_args, ax_tvs, ax_lhs, ax_rhs)) <- co1_is_axiom_maybe\r
- , Just (sym2, (ax_tc2, ax2_args, _, _, _)) <- co2_is_axiom_maybe\r
- , ax_tc1 == ax_tc2\r
- , sym1 /= sym2\r
- = Just $\r
- if sym1 \r
- then substTyWith ax_tvs (opt_transL (map mkSymCoercion ax1_args) ax2_args) ax_rhs\r
- else substTyWith ax_tvs (opt_transL ax1_args (map mkSymCoercion ax2_args)) ax_lhs\r
--}\r
\r
- | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- co1_is_axiom_maybe\r
- , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co2\r
- = Just $ \r
+ -- TrPushAxR/TrPushSymAxR\r
+ | Just (sym, con, cos1) <- co1_is_axiom_maybe\r
+ , Just cos2 <- matchAxiom sym con co2\r
+ = fireTransRule "TrPushAxR" co1 co2 $\r
if sym \r
- then mkSymCoercion $ TyConApp ax_tc (opt_transL (map mkSymCoercion cos) ax_args)\r
- else TyConApp ax_tc (opt_transL ax_args cos)\r
+ then SymCo $ AxiomInstCo con (opt_transList (map mkSymCo cos2) cos1)\r
+ else AxiomInstCo con (opt_transList cos1 cos2)\r
\r
- | Just (sym, (ax_tc, ax_args, ax_tvs, ax_lhs, _)) <- isAxiom_maybe co2\r
- , Just cos <- matchesAxiomLhs ax_tvs ax_lhs co1\r
- = Just $ \r
+ -- TrPushAxL/TrPushSymAxL\r
+ | Just (sym, con, cos2) <- co2_is_axiom_maybe\r
+ , Just cos1 <- matchAxiom (not sym) con co1\r
+ = fireTransRule "TrPushAxL" co1 co2 $\r
if sym \r
- then mkSymCoercion $ TyConApp ax_tc (opt_transL ax_args (map mkSymCoercion cos))\r
- else TyConApp ax_tc (opt_transL cos ax_args)\r
+ then SymCo $ AxiomInstCo con (opt_transList cos2 (map mkSymCo cos1))\r
+ else AxiomInstCo con (opt_transList cos1 cos2)\r
+\r
+ -- TrPushAxSym/TrPushSymAx\r
+ | Just (sym1, con1, cos1) <- co1_is_axiom_maybe\r
+ , Just (sym2, con2, cos2) <- co2_is_axiom_maybe\r
+ , con1 == con2\r
+ , sym1 == not sym2\r
+ , let qtvs = co_ax_tvs con1\r
+ lhs = co_ax_lhs con1 \r
+ rhs = co_ax_rhs con1 \r
+ pivot_tvs = exactTyVarsOfType (if sym2 then rhs else lhs)\r
+ , all (`elemVarSet` pivot_tvs) qtvs\r
+ = fireTransRule "TrPushAxSym" co1 co2 $\r
+ if sym2\r
+ then liftCoSubstWith qtvs (opt_transList cos1 (map mkSymCo cos2)) lhs -- TrPushAxSym\r
+ else liftCoSubstWith qtvs (opt_transList (map mkSymCo cos1) cos2) rhs -- TrPushSymAx\r
where\r
co1_is_axiom_maybe = isAxiom_maybe co1\r
co2_is_axiom_maybe = isAxiom_maybe co2\r
\r
opt_trans_rule co1 co2 -- Identity rule\r
- | (ty1,_) <- coercionKind co1\r
- , (_,ty2) <- coercionKind co2\r
- , ty1 `coreEqType` ty2\r
- = Just ty2\r
+ | Pair ty1 _ <- coercionKind co1\r
+ , Pair _ ty2 <- coercionKind co2\r
+ , ty1 `eqType` ty2\r
+ = fireTransRule "RedTypeDirRefl" co1 co2 $\r
+ Refl ty2\r
\r
opt_trans_rule _ _ = Nothing\r
\r
------------ \r
-isAxiom_maybe :: Coercion -> Maybe (Bool, (TyCon, [Coercion], [TyVar], Type, Type))\r
-isAxiom_maybe co\r
- | Just (tc, args) <- splitTyConApp_maybe co\r
- , Just (_, desc) <- isCoercionTyCon_maybe tc\r
- = case desc of\r
- CoAxiom { co_ax_tvs = tvs, co_ax_lhs = lhs, co_ax_rhs = rhs } \r
- -> Just (False, (tc, args, tvs, lhs, rhs))\r
- CoSym | (arg1:_) <- args \r
- -> case isAxiom_maybe arg1 of\r
- Nothing -> Nothing\r
- Just (sym, stuff) -> Just (not sym, stuff)\r
- _ -> Nothing\r
- | otherwise\r
- = Nothing\r
-\r
-matchesAxiomLhs :: [TyVar] -> Type -> Type -> Maybe [Type]\r
-matchesAxiomLhs tvs ty_tmpl ty \r
- = case tcMatchTy (mkVarSet tvs) ty_tmpl ty of\r
+opt_trans_pred :: Pred Coercion -> Pred Coercion -> Maybe (Pred Coercion)\r
+opt_trans_pred (EqPred co1a co1b) (EqPred co2a co2b)\r
+ = Just (EqPred (opt_trans co1a co2a) (opt_trans co1b co2b))\r
+opt_trans_pred (ClassP cls1 cos1) (ClassP cls2 cos2)\r
+ | cls1 == cls2\r
+ = Just (ClassP cls1 (opt_transList cos1 cos2))\r
+opt_trans_pred (IParam n1 co1) (IParam n2 co2)\r
+ | n1 == n2\r
+ = Just (IParam n1 (opt_trans co1 co2))\r
+opt_trans_pred _ _ = Nothing\r
+\r
+fireTransRule :: String -> Coercion -> Coercion -> Coercion -> Maybe Coercion\r
+fireTransRule rule co1 co2 res\r
+ = -- pprTrace ("Trans rule fired: " ++ rule) (vcat [ppr co1, ppr co2, ppr res]) $\r
+ Just res\r
+\r
+-----------\r
+wrapSym :: Bool -> Coercion -> Coercion\r
+wrapSym sym co | sym = SymCo co\r
+ | otherwise = co\r
+\r
+-----------\r
+isAxiom_maybe :: Coercion -> Maybe (Bool, CoAxiom, [Coercion])\r
+isAxiom_maybe (SymCo co) \r
+ | Just (sym, con, cos) <- isAxiom_maybe co\r
+ = Just (not sym, con, cos)\r
+isAxiom_maybe (AxiomInstCo con cos)\r
+ = Just (False, con, cos)\r
+isAxiom_maybe _ = Nothing\r
+\r
+matchAxiom :: Bool -- True = match LHS, False = match RHS\r
+ -> CoAxiom -> Coercion -> Maybe [Coercion]\r
+-- If we succeed in matching, then *all the quantified type variables are bound*\r
+-- E.g. if tvs = [a,b], lhs/rhs = [b], we'll fail\r
+matchAxiom sym (CoAxiom { co_ax_tvs = qtvs, co_ax_lhs = lhs, co_ax_rhs = rhs }) co\r
+ = case liftCoMatch (mkVarSet qtvs) (if sym then lhs else rhs) co of\r
Nothing -> Nothing\r
- Just subst -> Just (map (substTyVar subst) tvs)\r
-\r
------------ \r
-opt_trans_rule_equal_tc :: CoTyConDesc -> [Coercion] -> [Coercion] -> Maybe Coercion\r
--- Rules for Coercion TyCons only\r
-\r
--- Push transitivity inside instantiation\r
-opt_trans_rule_equal_tc desc [co1,ty1] [co2,ty2]\r
- | CoInst <- desc\r
- , ty1 `coreEqType` ty2\r
- , co1 `compatible_co` co2\r
- = Just (mkInstCoercion (opt_trans2 co1 co2) ty1) \r
-\r
-opt_trans_rule_equal_tc desc [co1] [co2]\r
- | CoLeft <- desc, is_compat = Just (mkLeftCoercion res_co)\r
- | CoRight <- desc, is_compat = Just (mkRightCoercion res_co)\r
- | CoCsel1 <- desc, is_compat = Just (mkCsel1Coercion res_co)\r
- | CoCsel2 <- desc, is_compat = Just (mkCsel2Coercion res_co)\r
- | CoCselR <- desc, is_compat = Just (mkCselRCoercion res_co)\r
- where\r
- is_compat = co1 `compatible_co` co2\r
- res_co = opt_trans2 co1 co2\r
-\r
-opt_trans_rule_equal_tc _ _ _ = Nothing\r
+ Just subst -> allMaybes (map (liftCoSubstTyVar subst) qtvs)\r
\r
-------------\r
compatible_co :: Coercion -> Coercion -> Bool\r
-- Check whether (co1 . co2) will be well-kinded\r
compatible_co co1 co2\r
- = x1 `coreEqType` x2 \r
+ = x1 `eqType` x2 \r
where\r
- (_,x1) = coercionKind co1\r
- (x2,_) = coercionKind co2\r
+ Pair _ x1 = coercionKind co1\r
+ Pair x2 _ = coercionKind co2\r
\r
-------------\r
-etaForAll_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
+etaForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion)\r
-- Try to make the coercion be of form (forall tv. co)\r
-etaForAll_maybe co\r
- | Just (tv, r) <- splitForAllTy_maybe co\r
- , not (isCoVar tv) -- Check it is a *type* forall, not a (t1~t2)=>co\r
+etaForAllCo_maybe co\r
+ | Just (tv, r) <- splitForAllCo_maybe co\r
= Just (tv, r)\r
\r
- | (ty1,ty2) <- coercionKind co\r
- , Just (tv1, _) <- splitTypeForAll_maybe ty1\r
- , Just (tv2, _) <- splitTypeForAll_maybe ty2\r
+ | Pair ty1 ty2 <- coercionKind co\r
+ , Just (tv1, _) <- splitForAllTy_maybe ty1\r
+ , Just (tv2, _) <- splitForAllTy_maybe ty2\r
, tyVarKind tv1 `eqKind` tyVarKind tv2\r
- = Just (tv1, mkInstCoercion co (mkTyVarTy tv1))\r
+ = Just (tv1, mkInstCo co (mkTyVarTy tv1))\r
\r
| otherwise\r
= Nothing\r
\r
-etaCoPred_maybe :: Coercion -> Maybe (Coercion, Coercion, Coercion)\r
-etaCoPred_maybe co \r
- | Just (s,t,r) <- splitCoPredTy_maybe co\r
- = Just (s,t,r)\r
- \r
- -- co :: (s1~t1)=>r1 ~ (s2~t2)=>r2\r
- | (ty1,ty2) <- coercionKind co -- We know ty1,ty2 have same kind\r
- , Just (s1,_,_) <- splitCoPredTy_maybe ty1\r
- , Just (s2,_,_) <- splitCoPredTy_maybe ty2\r
- , typeKind s1 `eqKind` typeKind s2 -- t1,t2 have same kinds\r
- = Just (mkCsel1Coercion co, mkCsel2Coercion co, mkCselRCoercion co)\r
- \r
- | otherwise\r
- = Nothing\r
-\r
-etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)\r
--- Split a coercion g :: t1a t1b ~ t2a t2b\r
--- into (left g, right g) if possible\r
-etaApp_maybe co\r
- | Just (co1, co2) <- splitAppTy_maybe co\r
- = Just (co1, co2)\r
-\r
- | (ty1,ty2) <- coercionKind co\r
- , Just (ty1a, _) <- splitAppTy_maybe ty1\r
- , Just (ty2a, _) <- splitAppTy_maybe ty2\r
- , typeKind ty1a `eqKind` typeKind ty2a\r
- = Just (mkLeftCoercion co, mkRightCoercion co)\r
-\r
- | otherwise\r
- = Nothing\r
-\r
--------------\r
-splitTypeForAll_maybe :: Type -> Maybe (TyVar, Type)\r
--- Returns Just only for a *type* forall, not a (t1~t2)=>co\r
-splitTypeForAll_maybe ty\r
- | Just (tv, rty) <- splitForAllTy_maybe ty\r
- , not (isCoVar tv)\r
- = Just (tv, rty)\r
+etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]\r
+-- If possible, split a coercion \r
+-- g :: T s1 .. sn ~ T t1 .. tn\r
+-- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ] \r
+etaTyConAppCo_maybe tc (TyConAppCo tc2 cos2)\r
+ = ASSERT( tc == tc2 ) Just cos2\r
+\r
+etaTyConAppCo_maybe tc co\r
+ | isDecomposableTyCon tc\r
+ , Pair ty1 ty2 <- coercionKind co\r
+ , Just (tc1, tys1) <- splitTyConApp_maybe ty1\r
+ , Just (tc2, tys2) <- splitTyConApp_maybe ty2\r
+ , tc1 == tc2\r
+ , let n = length tys1\r
+ = ASSERT( tc == tc1 ) \r
+ ASSERT( n == length tys2 )\r
+ Just (decomposeCo n co) \r
+ -- NB: n might be <> tyConArity tc\r
+ -- e.g. data family T a :: * -> *\r
+ -- g :: T a b ~ T c d\r
\r
| otherwise\r
= Nothing\r
-\r
--------------\r
-isIdNormCo :: NormalCo -> Bool\r
--- Cheap identity test: look for coercions with no coercion variables at all\r
--- So it'll return False for (sym g `trans` g)\r
-isIdNormCo ty = go ty\r
- where\r
- go (TyVarTy tv) = not (isCoVar tv)\r
- go (AppTy t1 t2) = go t1 && go t2\r
- go (FunTy t1 t2) = go t1 && go t2\r
- go (ForAllTy tv ty) = go (tyVarKind tv) && go ty\r
- go (TyConApp tc tys) = not (isCoercionTyCon tc) && all go tys\r
- go (PredTy (IParam _ ty)) = go ty\r
- go (PredTy (ClassP _ tys)) = all go tys\r
- go (PredTy (EqPred t1 t2)) = go t1 && go t2\r
\end{code} \r
projects / ghc-hetmet.git / blobdiff