import TyCon\r
import Var\r
import VarSet\r
+import VarEnv\r
import PrelNames\r
+import StaticFlags ( opt_NoOptCoercion )\r
import Util\r
import Outputable\r
\end{code}\r
%* *\r
%************************************************************************\r
\r
+Note [Subtle shadowing in coercions]\r
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~\r
+Supose we optimising a coercion\r
+ optCoercion (forall (co_X5:t1~t2). ...co_B1...)\r
+The co_X5 is a wild-card; the bound variable of a coercion for-all\r
+should never appear in the body of the forall. Indeed we often\r
+write it like this\r
+ optCoercion ( (t1~t2) => ...co_B1... )\r
+\r
+Just because it's a wild-card doesn't mean we are free to choose\r
+whatever variable we like. For example it'd be wrong for optCoercion\r
+to return\r
+ forall (co_B1:t1~t2). ...co_B1...\r
+because now the co_B1 (which is really free) has been captured, and\r
+subsequent substitutions will go wrong. That's why we can't use\r
+mkCoPredTy in the ForAll case, where this note appears. \r
+\r
\begin{code}\r
optCoercion :: TvSubst -> Coercion -> NormalCo\r
-- ^ optCoercion applies a substitution to a coercion, \r
-- *and* optimises it to reduce its size\r
-optCoercion env co = opt_co env False co\r
+optCoercion env co \r
+ | opt_NoOptCoercion = substTy env co\r
+ | otherwise = opt_co env False co\r
\r
type NormalCo = Coercion\r
-- Invariants: \r
-> Coercion\r
-> NormalCo \r
opt_co = opt_co'\r
--- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $\r
--- co1 `seq` \r
--- pprTrace "opt_co done }" (ppr co1) \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
--- co1\r
--- where\r
--- co1 = opt_co' sym co\r
--- same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2\r
--- (s,t) = coercionKind co\r
--- (s1,t1) | sym = (t,s)\r
--- | otherwise = (s,t)\r
--- (s2,t2) = coercionKind co1\r
+-- $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )\r
+ = WARN( not (coreEqType 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
+ 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
+ (s1,t1) | sym = (t,s)\r
+ | otherwise = (s,t)\r
+ (s2,t2) = coercionKind co1\r
+\r
+ simple_result | sym = mkSymCoercion (substTy env co)\r
+ | otherwise = substTy 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
(ty1,ty2) = coVarKind tv\r
\r
opt_co' env sym (ForAllTy tv cor) \r
- | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)\r
- | otherwise = case substTyVarBndr env tv of\r
- (env', tv') -> ForAllTy tv' (opt_co env' sym cor)\r
+ | isTyVar tv = case substTyVarBndr env tv of\r
+ (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)\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
where\r
- (co1,co2) = coVarKind tv\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
| otherwise -> opt_trans opt_co1 opt_co2\r
\r
CoUnsafe\r
- | sym -> TyConApp tc [opt_co2,opt_co1]\r
- | otherwise -> TyConApp tc [opt_co1,opt_co2]\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
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 ty') sym co1_body\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] [ty'] opt_co1_body -- An inefficient one-variable substitution\r
+ -> substTyWith [tv] [ty2'] opt_co1_body -- An inefficient one-variable substitution\r
\r
| otherwise\r
- -> TyConApp tc [opt_co1, ty']\r
- where\r
- ty' = substTy env co2\r
+ -> TyConApp tc [opt_co1, ty2']\r
\r
where\r
(co1 : cos1) = cos\r
(co2 : _) = cos1\r
\r
+ ty1' = substTy env co1\r
+ ty2' = substTy env co2\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
= Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))\r
\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
opt_trans_rule co1 co2\r
- | Just (s1,t1,r1) <- splitCoPredTy_maybe co1\r
+ | Just (cv1,r1) <- splitForAllTy_maybe co1\r
+ , isCoVar cv1\r
+ , Just (s1,t1) <- coVarKind_maybe cv1\r
, Just (s2,t2,r2) <- etaCoPred_maybe co2\r
- = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))\r
+ = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
+ (opt_trans r1 r2))\r
\r
- | Just (s2,t2,r2) <- splitCoPredTy_maybe co2\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 (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))\r
+ = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))\r
+ (opt_trans r1 r2))\r
\r
-- Push transitivity inside forall\r
opt_trans_rule co1 co2\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
projects / ghc-hetmet.git / blobdiff