Look inside implications in simplifyRule
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 31 Jan 2018 14:25:50 +0000 (14:25 +0000)
committerBen Gamari <ben@smart-cactus.org>
Thu, 1 Feb 2018 03:12:46 +0000 (22:12 -0500)
Trac #14732 was a perpelexing bug in which -fdefer-typed-holes
caused a mysterious type error in a RULE.  This turned out to
be because we are more aggressive about creating implications
when deferring (see TcUnify.implicationNeeded), and the rule
mechanism hadn't caught up.

This fixes it.

(cherry picked from commit e9ae0cae9eb6a340473b339b5711ae76c6bdd045)

compiler/typecheck/TcRules.hs
testsuite/tests/typecheck/should_compile/T14732.hs [new file with mode: 0644]
testsuite/tests/typecheck/should_compile/all.T

index fd7ce2f..75e4025 100644 (file)
@@ -25,8 +25,10 @@ import TcEnv
 import TcUnify( buildImplicationFor )
 import TcEvidence( mkTcCoVarCo )
 import Type
 import TcUnify( buildImplicationFor )
 import TcEvidence( mkTcCoVarCo )
 import Type
+import TyCon( isTypeFamilyTyCon )
 import Id
 import Var( EvVar )
 import Id
 import Var( EvVar )
+import VarSet
 import BasicTypes       ( RuleName )
 import SrcLoc
 import Outputable
 import BasicTypes       ( RuleName )
 import SrcLoc
 import Outputable
@@ -254,7 +256,7 @@ 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
 
 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
+    RULE: f 3 |> (co :: T Int ~ Bool) = True
 
 which is terrible.  We want
 
 
 which is terrible.  We want
 
@@ -310,52 +312,36 @@ simplifyRule :: RuleName
 -- NB: This consumes all simple constraints on the LHS, but not
 -- any LHS implication constraints.
 simplifyRule name lhs_wanted rhs_wanted
 -- NB: This consumes all simple constraints on the LHS, but not
 -- any LHS implication constraints.
 simplifyRule name lhs_wanted rhs_wanted
-  = do {         -- We allow ourselves to unify environment
-                 -- variables: runTcS runs with topTcLevel
-       ; lhs_clone <- cloneWC lhs_wanted
-       ; rhs_clone <- cloneWC rhs_wanted
-
+  = do {
        -- Note [The SimplifyRule Plan] step 1
        -- First solve the LHS and *then* solve the RHS
        -- Crucially, this performs unifications
        -- Note [The SimplifyRule Plan] step 1
        -- First solve the LHS and *then* solve the RHS
        -- Crucially, this performs unifications
-       -- See Note [Solve order for RULES]
-       -- See Note [Simplify cloned constraints]
-       ; insoluble <- runTcSDeriveds $
-             do { lhs_resid <- solveWanteds lhs_clone
-                ; rhs_resid <- solveWanteds rhs_clone
-                ; return ( insolubleWC lhs_resid ||
-                           insolubleWC rhs_resid ) }
+       -- Why clone?  See Note [Simplify cloned constraints]
+       ; lhs_clone <- cloneWC lhs_wanted
+       ; rhs_clone <- cloneWC rhs_wanted
+       ; runTcSDeriveds $
+             do { _ <- solveWanteds lhs_clone
+                ; _ <- solveWanteds rhs_clone
+                  -- Why do them separately?
+                  -- See Note [Solve order for RULES]
+                ; return () }
 
        -- Note [The SimplifyRule Plan] step 2
 
        -- Note [The SimplifyRule Plan] step 2
-       ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
+       ; lhs_wanted <- zonkWC lhs_wanted
+       ; let (quant_cts, residual_lhs_wanted) = getRuleQuantCts lhs_wanted
 
        -- Note [The SimplifyRule Plan] step 3
 
        -- Note [The SimplifyRule Plan] step 3
-       ; let quantify_ct :: Ct -> Bool
-             quantify_ct ct
-                | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
-                = not (insoluble || t1 `tcEqType` t2)
-                  -- Note [RULE quantification over equalities]
-               | isHoleCt ct
-               = False  -- Don't quantify over type holes, obviously
-               | otherwise
-               = True
-
-       -- Note [The SimplifyRule Plan] step 3
-       ; let (quant_cts, no_quant_cts) = partitionBag quantify_ct
-                                                      zonked_lhs_simples
-
        ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
 
        ; traceTc "simplifyRule" $
          vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
               , text "lhs_wanted" <+> ppr lhs_wanted
               , text "rhs_wanted" <+> ppr rhs_wanted
        ; quant_evs <- mapM mk_quant_ev (bagToList quant_cts)
 
        ; traceTc "simplifyRule" $
          vcat [ text "LHS of rule" <+> doubleQuotes (ftext name)
               , text "lhs_wanted" <+> ppr lhs_wanted
               , text "rhs_wanted" <+> ppr rhs_wanted
-              , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples
               , text "quant_cts" <+> ppr quant_cts
               , text "quant_cts" <+> ppr quant_cts
-              , text "no_quant_cts" <+> ppr no_quant_cts
+              , text "residual_lhs_wanted" <+> ppr residual_lhs_wanted
               ]
 
               ]
 
-       ; return (quant_evs, lhs_wanted { wc_simple = no_quant_cts }) }
+       ; return (quant_evs, residual_lhs_wanted) }
 
   where
     mk_quant_ev :: Ct -> TcM EvVar
 
   where
     mk_quant_ev :: Ct -> TcM EvVar
@@ -368,3 +354,60 @@ simplifyRule name lhs_wanted rhs_wanted
                                 ; fillCoercionHole hole (mkTcCoVarCo ev_id)
                                 ; return ev_id }
     mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
                                 ; fillCoercionHole hole (mkTcCoVarCo ev_id)
                                 ; return ev_id }
     mk_quant_ev ct = pprPanic "mk_quant_ev" (ppr ct)
+
+
+getRuleQuantCts :: WantedConstraints -> (Cts, WantedConstraints)
+-- Extract all the constraints we can quantify over,
+--   also returning the depleted WantedConstraints
+--
+-- NB: we must look inside implications, because with
+--     -fdefer-type-errors we generate implications rather eagerly;
+--     see TcUnify.implicationNeeded. Not doing so caused Trac #14732.
+--
+-- Unlike simplifyInfer, we don't leave the WantedConstraints unchanged,
+--   and attempt to solve them from the quantified constraints.  That
+--   nearly works, but fails for a constraint like (d :: Eq Int).
+--   We /do/ want to quantify over it, but the short-cut solver
+--   (see TcInteract Note [Shortcut solving]) ignores the quantified
+--   and instead solves from the top level.
+--
+--   So we must partition the WantedConstraints ourselves
+--   Not hard, but tiresome.
+
+getRuleQuantCts wc
+  = float_wc emptyVarSet wc
+  where
+    float_wc :: TcTyCoVarSet -> WantedConstraints -> (Cts, WantedConstraints)
+    float_wc skol_tvs (WC { wc_simple = simples, wc_impl = implics })
+      = ( simple_yes `andCts` implic_yes
+        , WC { wc_simple = simple_no, wc_impl = implics_no })
+     where
+        (simple_yes, simple_no) = partitionBag (rule_quant_ct skol_tvs) simples
+        (implic_yes, implics_no) = mapAccumBagL (float_implic skol_tvs)
+                                                emptyBag implics
+
+    float_implic :: TcTyCoVarSet -> Cts -> Implication -> (Cts, Implication)
+    float_implic skol_tvs yes1 imp
+      = (yes1 `andCts` yes2, imp { ic_wanted = no })
+      where
+        (yes2, no) = float_wc new_skol_tvs (ic_wanted imp)
+        new_skol_tvs = skol_tvs `extendVarSetList` ic_skols imp
+
+    rule_quant_ct :: TcTyCoVarSet -> Ct -> Bool
+    rule_quant_ct skol_tvs ct
+      | EqPred _ t1 t2 <- classifyPredType (ctPred ct)
+      , not (ok_eq t1 t2)
+       = False        -- Note [RULE quantification over equalities]
+      | isHoleCt ct
+      = False         -- Don't quantify over type holes, obviously
+      | otherwise
+      = tyCoVarsOfCt ct `disjointVarSet` skol_tvs
+
+    ok_eq t1 t2
+       | t1 `tcEqType` t2 = False
+       | otherwise        = is_fun_app t1 || is_fun_app t2
+
+    is_fun_app ty   -- ty is of form (F tys) where F is a type function
+      = case tyConAppTyCon_maybe ty of
+          Just tc -> isTypeFamilyTyCon tc
+          Nothing -> False
diff --git a/testsuite/tests/typecheck/should_compile/T14732.hs b/testsuite/tests/typecheck/should_compile/T14732.hs
new file mode 100644 (file)
index 0000000..4fa070e
--- /dev/null
@@ -0,0 +1,34 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# OPTIONS_GHC -fdefer-type-errors -O #-}
+-- Oddly this bug was only triggered with -fdefer-type-errors
+-- The -O ensures that the RULE is processed
+
+module T14732 where
+
+import Prelude hiding (zip, zipWith)
+
+zipWith :: (a -> b -> c)
+        -> Bundle v a
+        -> Bundle v b
+        -> Bundle v c
+zipWith = undefined
+
+class GVector (v :: * -> *) a
+instance GVector Vector a
+
+data Bundle (v :: * -> *) a
+data Vector a
+class Unbox a
+
+stream :: GVector v a => v a -> Bundle v a
+{-# INLINE [1] stream #-}
+stream = undefined
+
+zip :: (Unbox a, Unbox b) => Vector a -> Vector b -> Vector (a, b)
+{-# INLINE [1] zip #-}
+zip = undefined
+{-# RULES "stream/zip [Vector.Unboxed]" forall as bs .
+  stream (zip as bs) = zipWith (,) (stream as)
+                                   (stream bs)   #-}
index fd05c20..8b93c09 100644 (file)
@@ -590,3 +590,4 @@ test('T14488', normal, compile, [''])
 test('T13032', normal, compile, [''])
 test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T13032', normal, compile, [''])
 test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
+test('T14732', normal, compile, [''])