X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypes%2FOptCoercion.lhs;h=0fff7abc5919910402010143b9494e43300a07ff;hb=9176377bf7d989919fe7d27cad1f56bd9c4e7b6b;hp=43de7d626e84176781e9250837943cb40b760382;hpb=b06d623b2e367a572de5daf06d6a0b12c2740471;p=ghc-hetmet.git

diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index 43de7d6..0fff7ab 100644
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -17,6 +17,7 @@ import TypeRep
 import TyCon
 import Var
 import VarSet
+import VarEnv
 import PrelNames
 import Util
 import Outputable
@@ -28,6 +29,23 @@ import Outputable
 %*                                                                      *
 %************************************************************************
 
+Note [Subtle shadowing in coercions]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Supose we optimising a coercion
+    optCoercion (forall (co_X5:t1~t2). ...co_B1...)
+The co_X5 is a wild-card; the bound variable of a coercion for-all
+should never appear in the body of the forall. Indeed we often
+write it like this
+    optCoercion ( (t1~t2) => ...co_B1... )
+
+Just because it's a wild-card doesn't mean we are free to choose
+whatever variable we like.  For example it'd be wrong for optCoercion
+to return
+   forall (co_B1:t1~t2). ...co_B1...
+because now the co_B1 (which is really free) has been captured, and
+subsequent substitutions will go wrong.  That's why we can't use
+mkCoPredTy in the ForAll case, where this note appears.  
+
 \begin{code}
 optCoercion :: TvSubst -> Coercion -> NormalCo
 -- ^ optCoercion applies a substitution to a coercion, 
@@ -48,19 +66,31 @@ opt_co, opt_co' :: TvSubst
        		-> Coercion
        		-> NormalCo	
 opt_co = opt_co'
--- opt_co sym co = pprTrace "opt_co {" (ppr sym <+> ppr co) $
---       	        co1 `seq` 
---                pprTrace "opt_co done }" (ppr co1) 
+
+{-    Debuggery 
+opt_co env sym co 
+-- = pprTrace "opt_co {" (ppr sym <+> ppr co) $
+--     	        co1 `seq` 
+--               pprTrace "opt_co done }" (ppr co1) 
 --               WARN( not same_co_kind, ppr co  <+> dcolon <+> pprEqPred (s1,t1) 
---                                     $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
---                co1
---  where
---    co1 = opt_co' sym co
---    same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
---    (s,t) = coercionKind co
---    (s1,t1) | sym = (t,s)
---            | otherwise = (s,t)
---    (s2,t2) = coercionKind co1
+--                                   $$ ppr co1 <+> dcolon <+> pprEqPred (s2,t2) )
+ =   WARN( not (coreEqType co1 simple_result), 
+           (text "env=" <+> ppr env) $$
+           (text "input=" <+> ppr co) $$
+           (text "simple=" <+> ppr simple_result) $$
+           (text "opt=" <+> ppr co1) )
+     co1
+ where
+   co1 = opt_co' env sym co
+   same_co_kind = s1 `coreEqType` s2 && t1 `coreEqType` t2
+   (s,t) = coercionKind (substTy env co)
+   (s1,t1) | sym = (t,s)
+           | otherwise = (s,t)
+   (s2,t2) = coercionKind co1
+
+   simple_result | sym = mkSymCoercion (substTy env co)
+                 | otherwise = substTy env co
+-}
 
 opt_co' env sym (AppTy ty1 ty2) 	  = mkAppTy (opt_co env sym ty1) (opt_co env sym ty2)
 opt_co' env sym (FunTy ty1 ty2) 	  = FunTy (opt_co env sym ty1) (opt_co env sym ty2)
@@ -78,11 +108,20 @@ opt_co' env sym co@(TyVarTy tv)
     (ty1,ty2) = coVarKind tv
 
 opt_co' env sym (ForAllTy tv cor) 
-  | isCoVar tv = mkCoPredTy (opt_co env sym co1) (opt_co env sym co2) (opt_co env sym cor)
-  | otherwise  = case substTyVarBndr env tv of
-                   (env', tv') -> ForAllTy tv' (opt_co env' sym cor)
+  | isTyVar tv  = case substTyVarBndr env tv of
+                   (env', tv') -> ForAllTy tv' (opt_co' env' sym cor)
+
+opt_co' env sym co@(ForAllTy co_var cor) 
+  | isCoVar co_var 
+  = WARN( co_var `elemVarSet` tyVarsOfType cor, ppr co )
+    ForAllTy co_var' cor'
   where
-    (co1,co2) = coVarKind tv
+    (co1,co2) = coVarKind co_var
+    co1' = opt_co' env sym co1
+    co2' = opt_co' env sym co2
+    cor' = opt_co' env sym cor
+    co_var' = uniqAway (getTvInScope env) (mkWildCoVar (mkCoKind co1' co2'))
+    -- See Note [Subtle shadowing in coercions]
 
 opt_co' env sym (TyConApp tc cos)
   | Just (arity, desc) <- isCoercionTyCon_maybe tc
@@ -112,8 +151,8 @@ opt_co_tc_app env sym tc desc cos
         | otherwise -> opt_trans opt_co1 opt_co2
 
       CoUnsafe
-        | sym       -> TyConApp tc [opt_co2,opt_co1]
-        | otherwise -> TyConApp tc [opt_co1,opt_co2]
+        | sym       -> mkUnsafeCoercion ty2' ty1'
+        | otherwise -> mkUnsafeCoercion ty1' ty2'
 
       CoSym   -> opt_co env (not sym) co1
       CoLeft  -> opt_lr fst
@@ -125,21 +164,22 @@ opt_co_tc_app env sym tc desc cos
       CoInst        -- See if the first arg is already a forall
 		    -- ...then we can just extend the current substitution
         | Just (tv, co1_body) <- splitForAllTy_maybe co1
-        -> opt_co (extendTvSubst env tv ty') sym co1_body
+        -> opt_co (extendTvSubst env tv ty2') sym co1_body
 
                     -- See if is *now* a forall
         | Just (tv, opt_co1_body) <- splitForAllTy_maybe opt_co1
-        -> substTyWith [tv] [ty'] opt_co1_body	-- An inefficient one-variable substitution
+        -> substTyWith [tv] [ty2'] opt_co1_body	-- An inefficient one-variable substitution
 
         | otherwise
-        -> TyConApp tc [opt_co1, ty']
-        where
-          ty' = substTy env co2
+        -> TyConApp tc [opt_co1, ty2']
 
   where
     (co1 : cos1) = cos
     (co2 : _)    = cos1
 
+    ty1' = substTy env co1
+    ty2' = substTy env co2
+
 	-- These opt_cos have the sym pushed into them
     opt_co1 = opt_co env sym co1
     opt_co2 = opt_co env sym co2
@@ -217,14 +257,22 @@ opt_trans_rule co1 co2
   = Just (mkAppTy (opt_trans co1a co2a) (opt_trans co1b co2b))
 
 -- Push transitivity inside (s~t)=>r
+-- We re-use the CoVar rather than using mkCoPredTy
+-- See Note [Subtle shadowing in coercions]
 opt_trans_rule co1 co2
-  | Just (s1,t1,r1) <- splitCoPredTy_maybe co1
+  | Just (cv1,r1) <- splitForAllTy_maybe co1
+  , isCoVar cv1
+  , Just (s1,t1) <- coVarKind_maybe cv1
   , Just (s2,t2,r2) <- etaCoPred_maybe co2
-  = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))
+  = Just (ForAllTy (mkCoVar (coVarName cv1) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))
+                   (opt_trans r1 r2))
 
-  | Just (s2,t2,r2) <- splitCoPredTy_maybe co2
+  | Just (cv2,r2) <- splitForAllTy_maybe co2
+  , isCoVar cv2
+  , Just (s2,t2) <- coVarKind_maybe cv2
   , Just (s1,t1,r1) <- etaCoPred_maybe co1
-  = Just (mkCoPredTy (opt_trans s1 s2) (opt_trans t1 t2) (opt_trans r1 r2))
+  = Just (ForAllTy (mkCoVar (coVarName cv2) (mkCoKind (opt_trans s1 s2) (opt_trans t1 t2)))
+                   (opt_trans r1 r2))
 
 -- Push transitivity inside forall
 opt_trans_rule co1 co2
@@ -362,6 +410,8 @@ etaCoPred_maybe co
   = Nothing
 
 etaApp_maybe :: Coercion -> Maybe (Coercion, Coercion)
+-- Split a coercion g :: t1a t1b ~ t2a t2b
+-- into (left g, right g) if possible
 etaApp_maybe co
   | Just (co1, co2) <- splitAppTy_maybe co
   = Just (co1, co2)