Look inside implications in simplifyRule
authorSimon Peyton Jones <simonpj@microsoft.com>
Wed, 31 Jan 2018 14:25:50 +0000 (14:25 +0000)
committerSimon Peyton Jones <simonpj@microsoft.com>
Wed, 31 Jan 2018 14:27:59 +0000 (14:27 +0000)
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.

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 TyCon( isTypeFamilyTyCon )
 import Id
 import Var( EvVar )
+import VarSet
 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
 
-    RULE: f 3 |> (co :: T Int ~ Booo) = True
+    RULE: f 3 |> (co :: T Int ~ Bool) = True
 
 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
-  = 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
-       -- 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
-       ; 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
-       ; 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
-              , text "zonked_lhs_simples" <+> ppr zonked_lhs_simples
               , 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
@@ -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)
+
+
+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 9e68981..795e173 100644 (file)
@@ -591,3 +591,4 @@ test('T14488', normal, compile, [''])
 test('T14590', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
 test('T13032', normal, compile, [''])
 test('T14273', normal, compile, ['-fdefer-type-errors -fno-max-valid-substitutions'])
+test('T14732', normal, compile, [''])