Tighten up constraint solve order for RULES
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 14 Jan 2015 10:53:49 +0000 (10:53 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 14 Jan 2015 16:08:54 +0000 (16:08 +0000)
The main point is described in Note [Solve order for RULES].
I'm not sure if the potential bug described there could actually
happen, but I bet it could.  Anyway, this patch explicitly solves
LHS constraints and *then* RHS constraints (see the Note).

I also moved simplifyRule from TcSimplify (a large module) to
TcRules (a small one), which brings related code together.
It did mean I had to export runTcS from TcSimplify, but I think
that's a price worth paying.

compiler/typecheck/TcRules.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/typecheck/should_fail/T5853.stderr

index 17d548f..927eda5 100644 (file)
@@ -19,10 +19,13 @@ import TcEnv
 import TcEvidence( TcEvBinds(..) )
 import Type
 import Id
+import Var              ( EvVar )
 import Name
+import BasicTypes       ( RuleName )
 import SrcLoc
 import Outputable
 import FastString
+import Bag
 import Data.List( partition )
 
 {-
@@ -41,81 +44,6 @@ an example (test simplCore/should_compile/rule2.hs) produced by Roman:
    {-# RULES "foo/bar" foo = bar #-}
 
 He wanted the rule to typecheck.
-
-Note [Simplifying RULE constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-On the LHS of transformation rules we only simplify only equalities,
-but not dictionaries.  We want to keep dictionaries unsimplified, to
-serve as the available stuff for the RHS of the rule.  We *do* want to
-simplify equalities, however, to detect ill-typed rules that cannot be
-applied.
-
-Implementation: the TcSFlags carried by the TcSMonad controls the
-amount of simplification, so simplifyRuleLhs just sets the flag
-appropriately.
-
-Example.  Consider the following left-hand side of a rule
-        f (x == y) (y > z) = ...
-If we typecheck this expression we get constraints
-        d1 :: Ord a, d2 :: Eq a
-We do NOT want to "simplify" to the LHS
-        forall x::a, y::a, z::a, d1::Ord a.
-          f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
-Instead we want
-        forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
-          f ((==) d2 x y) ((>) d1 y z) = ...
-
-Here is another example:
-        fromIntegral :: (Integral a, Num b) => a -> b
-        {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
-In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
-we *dont* want to get
-        forall dIntegralInt.
-           fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
-because the scsel will mess up RULE matching.  Instead we want
-        forall dIntegralInt, dNumInt.
-          fromIntegral Int Int dIntegralInt dNumInt = id Int
-
-Even if we have
-        g (x == y) (y == z) = ..
-where the two dictionaries are *identical*, we do NOT WANT
-        forall x::a, y::a, z::a, d1::Eq a
-          f ((==) d1 x y) ((>) d1 y z) = ...
-because that will only match if the dict args are (visibly) equal.
-Instead we want to quantify over the dictionaries separately.
-
-In short, simplifyRuleLhs must *only* squash equalities, leaving
-all dicts unchanged, with absolutely no sharing.
-
-Also note that we can't solve the LHS constraints in isolation:
-Example   foo :: Ord a => a -> a
-          foo_spec :: Int -> Int
-          {-# RULE "foo"  foo = foo_spec #-}
-Here, it's the RHS that fixes the type variable
-
-HOWEVER, under a nested implication things are different
-Consider
-  f :: (forall a. Eq a => a->a) -> Bool -> ...
-  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
-       f b True = ...
-    #-}
-Here we *must* solve the wanted (Eq a) from the given (Eq a)
-resulting from skolemising the agument type of g.  So we
-revert to SimplCheck when going under an implication.
-
-
------------------------- So the plan is this -----------------------
-
-* Step 1: Simplify the LHS and RHS constraints all together in one bag
-          We do this to discover all unification equalities
-
-* Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
-          the ones we will quantify over, and the others
-
-* Step 3: Decide on the type variables to quantify over
-
-* Step 4: Simplify the LHS and RHS constraints separately, using the
-          quantified constraints as givens
 -}
 
 tcRules :: [LRuleDecl Name] -> TcM [LRuleDecl TcId]
@@ -132,7 +60,8 @@ tcRule (HsRule name act hs_bndrs lhs fv_lhs rhs fv_rhs)
        ; (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty)
             <- tcExtendTyVarEnv tv_bndrs $
                tcExtendIdEnv    id_bndrs $
-               do { ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
+               do { -- See Note [Solve order for RULES]
+                    ((lhs', rule_ty), lhs_wanted) <- captureConstraints (tcInferRho lhs)
                   ; (rhs', rhs_wanted) <- captureConstraints (tcMonoExpr rhs rule_ty)
                   ; return (lhs', lhs_wanted, rhs', rhs_wanted, rule_ty) }
 
@@ -223,3 +152,165 @@ tcRuleBndrs (L _ (RuleBndrSig (L _ name) rn_ty) : rule_bndrs)
 ruleCtxt :: FastString -> SDoc
 ruleCtxt name = ptext (sLit "When checking the transformation rule") <+>
                 doubleQuotes (ftext name)
+
+
+{-
+*********************************************************************************
+*                                                                                 *
+              Constraint simplification for rules
+*                                                                                 *
+***********************************************************************************
+
+Note [Simplifying RULE constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Example.  Consider the following left-hand side of a rule
+        f (x == y) (y > z) = ...
+If we typecheck this expression we get constraints
+        d1 :: Ord a, d2 :: Eq a
+We do NOT want to "simplify" to the LHS
+        forall x::a, y::a, z::a, d1::Ord a.
+          f ((==) (eqFromOrd d1) x y) ((>) d1 y z) = ...
+Instead we want
+        forall x::a, y::a, z::a, d1::Ord a, d2::Eq a.
+          f ((==) d2 x y) ((>) d1 y z) = ...
+
+Here is another example:
+        fromIntegral :: (Integral a, Num b) => a -> b
+        {-# RULES "foo"  fromIntegral = id :: Int -> Int #-}
+In the rule, a=b=Int, and Num Int is a superclass of Integral Int. But
+we *dont* want to get
+        forall dIntegralInt.
+           fromIntegral Int Int dIntegralInt (scsel dIntegralInt) = id Int
+because the scsel will mess up RULE matching.  Instead we want
+        forall dIntegralInt, dNumInt.
+          fromIntegral Int Int dIntegralInt dNumInt = id Int
+
+Even if we have
+        g (x == y) (y == z) = ..
+where the two dictionaries are *identical*, we do NOT WANT
+        forall x::a, y::a, z::a, d1::Eq a
+          f ((==) d1 x y) ((>) d1 y z) = ...
+because that will only match if the dict args are (visibly) equal.
+Instead we want to quantify over the dictionaries separately.
+
+In short, simplifyRuleLhs must *only* squash equalities, leaving
+all dicts unchanged, with absolutely no sharing.
+
+Also note that we can't solve the LHS constraints in isolation:
+Example   foo :: Ord a => a -> a
+          foo_spec :: Int -> Int
+          {-# RULE "foo"  foo = foo_spec #-}
+Here, it's the RHS that fixes the type variable
+
+HOWEVER, under a nested implication things are different
+Consider
+  f :: (forall a. Eq a => a->a) -> Bool -> ...
+  {-# RULES "foo" forall (v::forall b. Eq b => b->b).
+       f b True = ...
+    #-}
+Here we *must* solve the wanted (Eq a) from the given (Eq a)
+resulting from skolemising the agument type of g.  So we
+revert to SimplCheck when going under an implication.
+
+
+------------------------ So the plan is this -----------------------
+
+* Step 1: Simplify the LHS and RHS constraints all together in one bag
+          We do this to discover all unification equalities
+
+* Step 2: Zonk the ORIGINAL lhs constraints, and partition them into
+          the ones we will quantify over, and the others
+
+* Step 3: Decide on the type variables to quantify over
+
+* Step 4: Simplify the LHS and RHS constraints separately, using the
+          quantified constraints as givens
+
+Note [Solve order for RULES]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In step 1 above, we need to be a bit careful about solve order.
+Consider
+   f :: Int -> T Int
+   type instance T Int = Bool
+
+   RULE f 3 = True
+
+From the RULE we get
+   lhs-constraints:  T Int ~ alpha
+   rhs-constraints:  Bool ~ alpha
+where 'alpha' is the type that connects the two.  If we glom them
+all together, and solve the RHS constraint first, we might solve 
+with alpha := Bool.  But then we'd end up with a RULE like
+
+    RULE: f 3 |> (co :: T Int ~ Booo) = True
+
+which is terrible.  We want
+
+    RULE: f 3 = True |> (sym co :: Bool ~ T Int)
+
+So we are careful to solve the LHS constraints first, and *then* the
+RHS constraints.  Actually much of this is done by the on-the-fly
+constraint solving, so the same order must be observed in
+tcRule.
+
+
+Note [RULE quantification over equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Deciding which equalities to quantify over is tricky:
+ * We do not want to quantify over insoluble equalities (Int ~ Bool)
+    (a) because we prefer to report a LHS type error
+    (b) because if such things end up in 'givens' we get a bogus
+        "inaccessible code" error
+
+ * But we do want to quantify over things like (a ~ F b), where
+   F is a type function.
+
+The difficulty is that it's hard to tell what is insoluble!
+So we see whether the simplificaiotn step yielded any type errors,
+and if so refrain from quantifying over *any* equalities.
+-}
+
+simplifyRule :: RuleName
+             -> WantedConstraints       -- Constraints from LHS
+             -> WantedConstraints       -- Constraints from RHS
+             -> TcM ([EvVar], WantedConstraints)   -- LHS evidence variables
+-- See Note [Simplifying RULE constraints]
+--
+-- This function could be in TcSimplify, but that's a very big
+-- module and this is a small one.  Moreover, it's easier to
+-- understand tcRule when you can see simplifyRule too
+simplifyRule name lhs_wanted rhs_wanted
+  = do {         -- We allow ourselves to unify environment
+                 -- variables: runTcS runs with topTcLevel
+         (insoluble, _) <- runTcS $
+             do { -- First solve the LHS and *then* solve the RHS
+                  -- See Note [Solve order for RULES]
+                  lhs_resid <- solveWanteds lhs_wanted
+                ; rhs_resid <- solveWanteds rhs_wanted
+                ; return (insolubleWC lhs_resid || insolubleWC rhs_resid) }
+
+       ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
+       ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_simples
+             quantify_me  -- Note [RULE quantification over equalities]
+               | insoluble = quantify_insol
+               | otherwise = quantify_normal
+
+             quantify_insol ct = not (isEqPred (ctPred ct))
+
+             quantify_normal ct
+               | EqPred NomEq t1 t2 <- classifyPredType (ctPred ct)
+               = not (t1 `tcEqType` t2)
+               | otherwise
+               = True
+
+       ; traceTc "simplifyRule" $
+         vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
+              , text "lhs_wantd" <+> ppr lhs_wanted
+              , text "rhs_wantd" <+> ppr rhs_wanted
+              , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples
+              , text "q_cts"      <+> ppr q_cts
+              , text "non_q_cts"  <+> ppr non_q_cts ]
+
+       ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
+                , lhs_wanted { wc_simple = non_q_cts }) }
+
index 75abf0a..a29e1dc 100644 (file)
@@ -5,8 +5,11 @@ module TcSimplify(
        quantifyPred, growThetaTyVars,
        simplifyAmbiguityCheck,
        simplifyDefault,
-       simplifyRule, simplifyTop, simplifyInteractive,
-       solveWantedsTcM
+       simplifyTop, simplifyInteractive,
+       solveWantedsTcM,
+
+       -- For Rules we need these twoo
+       solveWanteds, runTcS
   ) where
 
 #include "HsVersions.h"
@@ -39,7 +42,6 @@ import PrelNames
 import Control.Monad    ( unless )
 import DynFlags         ( ExtensionFlag( Opt_AllowAmbiguousTypes ) )
 import Class            ( classKey )
-import BasicTypes       ( RuleName )
 import Maybes           ( isNothing )
 import Outputable
 import FastString
@@ -612,65 +614,6 @@ This only half-works, but then let-generalisation only half-works.
 
 *********************************************************************************
 *                                                                                 *
-*                             RULES                                               *
-*                                                                                 *
-***********************************************************************************
-
-See note [Simplifying RULE constraints] in TcRule
-
-Note [RULE quantification over equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Deciding which equalities to quantify over is tricky:
- * We do not want to quantify over insoluble equalities (Int ~ Bool)
-    (a) because we prefer to report a LHS type error
-    (b) because if such things end up in 'givens' we get a bogus
-        "inaccessible code" error
-
- * But we do want to quantify over things like (a ~ F b), where
-   F is a type function.
-
-The difficulty is that it's hard to tell what is insoluble!
-So we see whether the simplificaiotn step yielded any type errors,
-and if so refrain from quantifying over *any* equalites.
--}
-
-simplifyRule :: RuleName
-             -> WantedConstraints       -- Constraints from LHS
-             -> WantedConstraints       -- Constraints from RHS
-             -> TcM ([EvVar], WantedConstraints)   -- LHS evidence variables
--- See Note [Simplifying RULE constraints] in TcRule
-simplifyRule name lhs_wanted rhs_wanted
-  = do {         -- We allow ourselves to unify environment
-                 -- variables: runTcS runs with topTcLevel
-         (resid_wanted, _) <- solveWantedsTcM (lhs_wanted `andWC` rhs_wanted)
-                              -- Post: these are zonked and unflattened
-
-       ; zonked_lhs_simples <- TcM.zonkSimples (wc_simple lhs_wanted)
-       ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_simples
-             quantify_me  -- Note [RULE quantification over equalities]
-               | insolubleWC resid_wanted = quantify_insol
-               | otherwise                = quantify_normal
-
-             quantify_insol ct = not (isEqPred (ctPred ct))
-
-             quantify_normal ct
-               | EqPred NomEq t1 t2 <- classifyPredType (ctPred ct)
-               = not (t1 `tcEqType` t2)
-               | otherwise
-               = True
-
-       ; traceTc "simplifyRule" $
-         vcat [ ptext (sLit "LHS of rule") <+> doubleQuotes (ftext name)
-              , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples
-              , text "q_cts"      <+> ppr q_cts
-              , text "non_q_cts"  <+> ppr non_q_cts ]
-
-       ; return ( map (ctEvId . ctEvidence) (bagToList q_cts)
-                , lhs_wanted { wc_simple = non_q_cts }) }
-
-{-
-*********************************************************************************
-*                                                                                 *
 *                                 Main Simplifier                                 *
 *                                                                                 *
 ***********************************************************************************
index aa60ffe..3dc36ad 100644 (file)
@@ -1,20 +1,19 @@
-
-T5853.hs:15:52:
-    Could not deduce: fb ~ Subst (Subst fb a) (Elem fb)
-    from the context: (F (Subst (Subst fb a) b),
-                       Elem (Subst (Subst fb a) b) ~ b,
-                       Subst (Subst (Subst fb a) b) (Elem fb) ~ fb,
-                       Subst fb b ~ Subst (Subst fb a) b,
-                       F (Subst fb a),
-                       Elem (Subst fb a) ~ a,
-                       Elem (Subst (Subst fb a) b) ~ b,
-                       Subst (Subst (Subst fb a) b) a ~ Subst fb a)
-      bound by the RULE "map/map" at T5853.hs:15:2-57
-      ‘fb’ is a rigid type variable bound by
-           the RULE "map/map" at T5853.hs:15:2
-    Relevant bindings include
-      f :: b -> Elem fb (bound at T5853.hs:15:19)
-      g :: a -> b (bound at T5853.hs:15:21)
-      xs :: Subst fb a (bound at T5853.hs:15:23)
-    In the expression: (f . g) <$> xs
-    When checking the transformation rule "map/map"
+\r
+T5853.hs:15:52:\r
+    Could not deduce: fb ~ Subst (Subst (Subst fb b) a) (Elem fb)\r
+    from the context: (F (Subst fb b),\r
+                       Elem (Subst fb b) ~ b,\r
+                       Subst (Subst fb b) (Elem fb) ~ fb,\r
+                       F (Subst (Subst fb b) a),\r
+                       Elem (Subst (Subst fb b) a) ~ a,\r
+                       Elem (Subst fb b) ~ b,\r
+                       Subst (Subst (Subst fb b) a) b ~ Subst fb b)\r
+      bound by the RULE "map/map" at T5853.hs:15:2-57\r
+      ‘fb’ is a rigid type variable bound by\r
+           the RULE "map/map" at T5853.hs:15:2\r
+    Relevant bindings include\r
+      f :: b -> Elem fb (bound at T5853.hs:15:19)\r
+      g :: a -> b (bound at T5853.hs:15:21)\r
+      xs :: Subst (Subst fb b) a (bound at T5853.hs:15:23)\r
+    In the expression: (f . g) <$> xs\r
+    When checking the transformation rule "map/map"\r