Fix a very subtle shadowing bug in optCoercion

See Note [Subtle shadowing in coercions]

This is what was going wrong in Trac 4160.

diff --git a/compiler/types/OptCoercion.lhs b/compiler/types/OptCoercion.lhs
index ecf93a0..0fff7ab 100644 (file)
--- a/compiler/types/OptCoercion.lhs
+++ b/compiler/types/OptCoercion.lhs
@@ -17,6 +17,7 @@ import TypeRep
 import TyCon\r
 import Var\r
 import VarSet\r
+import VarEnv\r
 import PrelNames\r
 import Util\r
 import Outputable\r
@@ -28,6 +29,23 @@ import Outputable
 %*                                                                      *\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
@@ -48,19 +66,31 @@ opt_co, opt_co' :: TvSubst
                        -> 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
@@ -78,11 +108,20 @@ opt_co' env sym co@(TyVarTy tv)
     (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
@@ -218,14 +257,22 @@ opt_trans_rule co1 co2
   = 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