Ensure that insolubles are fully rewritten
authorSimon Peyton Jones <simonpj@microsoft.com>
Fri, 19 May 2017 09:50:35 +0000 (10:50 +0100)
committerSimon Peyton Jones <simonpj@microsoft.com>
Fri, 19 May 2017 09:54:55 +0000 (10:54 +0100)
I was alerted to this by Trac #12468 and #11325.  We were treating
insolubles (and "hole" constraints are treated as insoluble)
inconsistently.  In some places we were carefully rewriting them
e.g. Note [Make sure that insolubles are fully rewritten] in
TcCanonical.  But in TcSimplify we weren't feeding them into
the solver.

As a result, "hole" constraints were not being rewritten, which
some users found confusing, and I think rightly so.

This patch also fixes a bug in TcSMonad.emitInsoluble, in which two
different "hole" constriants could be treated (bogusly) as duplicates,
thereby losing one.

compiler/typecheck/TcCanonical.hs
compiler/typecheck/TcRnTypes.hs
compiler/typecheck/TcSMonad.hs
compiler/typecheck/TcSimplify.hs
testsuite/tests/gadt/T12468.hs [new file with mode: 0644]
testsuite/tests/gadt/T12468.stderr [new file with mode: 0644]
testsuite/tests/gadt/all.T
testsuite/tests/typecheck/should_compile/hole_constraints.stderr

index b623541..f533750 100644 (file)
@@ -1246,7 +1246,7 @@ When an equality fails, we still want to rewrite the equality
 all the way down, so that it accurately reflects
  (a) the mutable reference substitution in force at start of solving
  (b) any ty-binds in force at this point in solving
-See Note [Kick out insolubles] in TcSMonad.
+See Note [Rewrite insolubles] in TcSMonad.
 And if we don't do this there is a bad danger that
 TcSimplify.applyTyVarDefaulting will find a variable
 that has in fact been substituted.
index 40d4f78..481b2a7 100644 (file)
@@ -86,7 +86,7 @@ module TcRnTypes(
         addInsols, getInsolubles, insolublesOnly, addSimples, addImplics,
         tyCoVarsOfWC, dropDerivedWC, dropDerivedSimples, dropDerivedInsols,
         tyCoVarsOfWCList, trulyInsoluble,
-        isDroppableDerivedLoc, insolubleImplic,
+        isDroppableDerivedLoc, isDroppableDerivedCt, insolubleImplic,
         arisesFromGivens,
 
         Implication(..), ImplicStatus(..), isInsolubleStatus, isSolvedStatus,
@@ -1834,11 +1834,14 @@ See Note [The superclass story] in TcCanonical.
 
 dropDerivedInsols :: Cts -> Cts
 -- See Note [Dropping derived constraints]
-dropDerivedInsols insols = filterBag keep insols
-  where                    -- insols can include Given
-    keep ct
-      | isDerivedCt ct = not (isDroppableDerivedLoc (ctLoc ct))
-      | otherwise      = True
+dropDerivedInsols insols
+  = filterBag (not . isDroppableDerivedCt) insols
+              -- insols can include Given
+
+isDroppableDerivedCt :: Ct -> Bool
+isDroppableDerivedCt ct
+  | isDerivedCt ct = isDroppableDerivedLoc (ctLoc ct)
+  | otherwise      = False
 
 isDroppableDerivedLoc :: CtLoc -> Bool
 -- See Note [Dropping derived constraints]
index e943254..f7153f8 100644 (file)
@@ -1499,7 +1499,7 @@ kick_out_rewritable new_fr new_tv ics@(IC { inert_eqs      = tv_eqs
     (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
     (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
     (insols_out, insols_in) = partitionBag     kick_out_ct insols
-      -- Kick out even insolubles: See Note [Kick out insolubles]
+      -- Kick out even insolubles: See Note [Rewrite insolubles]
 
     fr_may_rewrite :: CtFlavourRole -> Bool
     fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
@@ -1591,14 +1591,29 @@ new equality, to maintain the inert-set invariants.
     take the substitution into account
 
 
-Note [Kick out insolubles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [Rewrite insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~
 Suppose we have an insoluble alpha ~ [alpha], which is insoluble
-because an occurs check.  And then we unify alpha := [Int].
-Then we really want to rewrite the insoluble to [Int] ~ [[Int]].
-Now it can be decomposed.  Otherwise we end up with a "Can't match
-[Int] ~ [[Int]]" which is true, but a bit confusing because the
-outer type constructors match.
+because an occurs check.  And then we unify alpha := [Int].  Then we
+really want to rewrite the insoluble to [Int] ~ [[Int]].  Now it can
+be decomposed.  Otherwise we end up with a "Can't match [Int] ~
+[[Int]]" which is true, but a bit confusing because the outer type
+constructors match.
+
+Similarly, if we have a CHoleCan, we'd like to rewrite it with any
+Givens, to give as informative an error messasge as possible
+(Trac #12468, #11325).
+
+Hence:
+ * In the main simlifier loops in TcSimplify (solveWanteds,
+   simpl_loop), we feed the insolubles in solveSimpleWanteds,
+   so that they get rewritten (albeit not solved).
+
+ * We kick insolubles out of the inert set, if they can be
+   rewritten (see TcSMonad.kick_out_rewritable)
+
+ * We rewrite those insolubles in TcCanonical.
+   See Note [Make sure that insolubles are fully rewritten]
 -}
 
 
@@ -2567,10 +2582,11 @@ emitInsoluble ct
   where
     this_pred = ctPred ct
     add_insol is@(IS { inert_cans = ics@(IC { inert_insols = old_insols }) })
-      | already_there = is
-      | otherwise     = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
+      | drop_it   = is
+      | otherwise = is { inert_cans = ics { inert_insols = old_insols `snocCts` ct } }
       where
-        already_there = not (isWantedCt ct) && anyBag (tcEqType this_pred . ctPred) old_insols
+        drop_it = isDroppableDerivedCt ct &&
+                  anyBag (tcEqType this_pred . ctPred) old_insols
              -- See Note [Do not add duplicate derived insolubles]
 
 newTcRef :: a -> TcS (TcRef a)
index 2822985..557d40d 100644 (file)
@@ -1201,7 +1201,9 @@ solveWanteds :: WantedConstraints -> TcS WantedConstraints
 solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
   = do { traceTcS "solveWanteds {" (ppr wc)
 
-       ; wc1 <- solveSimpleWanteds simples
+       ; wc1 <- solveSimpleWanteds (simples `unionBags` insols)
+                -- Why solve 'insols'?  See Note [Rewrite insolubles] in TcSMonad
+
        ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
 
        ; (floated_eqs, implics2) <- solveNestedImplications (implics `unionBags` implics1)
@@ -1213,8 +1215,9 @@ solveWanteds wc@(WC { wc_simple = simples, wc_insol = insols, wc_impl = implics
        ; dflags <- getDynFlags
        ; final_wc <- simpl_loop 0 (solverIterations dflags) floated_eqs
                                 no_new_scs
-                                (WC { wc_simple = simples2, wc_impl = implics2
-                                    , wc_insol  = insols `unionBags` insols1 })
+                                (WC { wc_simple = simples2
+                                    , wc_insol  = insols1
+                                    , wc_impl   = implics2 })
 
        ; bb <- TcS.getTcEvBindsMap
        ; traceTcS "solveWanteds }" $
@@ -1257,25 +1260,30 @@ simpl_loop n limit floated_eqs no_new_deriveds
 
        -- solveSimples may make progress if either float_eqs hold
        ; (unifs1, wc1) <- reportUnifications $
-                          solveSimpleWanteds (floated_eqs `unionBags` simples)
-                               -- Put floated_eqs first so they get solved first
-                               -- NB: the floated_eqs may include /derived/ equalities
-                               --     arising from fundeps inside an implication
+                          solveSimpleWanteds $
+                          floated_eqs `unionBags` simples `unionBags` insols
+            -- Notes:
+            --   - Why solve 'insols'?  See Note [Rewrite insolubles] in TcSMonad
+            --   - Put floated_eqs first so they get solved first
+            --     NB: the floated_eqs may include /derived/ equalities
+            --     arising from fundeps inside an implication
 
        ; let WC { wc_simple = simples1, wc_insol = insols1, wc_impl = implics1 } = wc1
        ; (no_new_scs, simples2) <- expandSuperClasses simples1
 
        -- We have already tried to solve the nested implications once
        -- Try again only if we have unified some meta-variables
-       -- (which is a bit like adding more givens
+       -- (which is a bit like adding more givens)
        -- See Note [Cutting off simpl_loop]
        ; (floated_eqs2, implics2) <- if unifs1 == 0 && isEmptyBag implics1
                                      then return (emptyBag, implics)
                                      else solveNestedImplications (implics `unionBags` implics1)
 
        ; simpl_loop (n+1) limit floated_eqs2 no_new_scs
-                    (WC { wc_simple = simples2, wc_impl = implics2
-                        , wc_insol  = insols `unionBags` insols1 }) }
+                    (WC { wc_simple = simples2
+                        , wc_insol  = insols1
+                        , wc_impl   = implics2 }) }
+
 
 expandSuperClasses :: Cts -> TcS (Bool, Cts)
 -- If there are any unsolved wanteds, expand one step of
diff --git a/testsuite/tests/gadt/T12468.hs b/testsuite/tests/gadt/T12468.hs
new file mode 100644 (file)
index 0000000..a147c09
--- /dev/null
@@ -0,0 +1,9 @@
+{-# LANGUAGE GADTs #-}
+
+module T12468 where
+
+data T a where
+    I :: T Int
+
+f :: T a -> a
+f I = _
diff --git a/testsuite/tests/gadt/T12468.stderr b/testsuite/tests/gadt/T12468.stderr
new file mode 100644 (file)
index 0000000..729b5c4
--- /dev/null
@@ -0,0 +1,6 @@
+
+T12468.hs:9:7: error:
+    • Found hole: _ :: Int
+    • In the expression: _
+      In an equation for ‘f’: f I = _
+    • Relevant bindings include f :: T a -> a (bound at T12468.hs:9:1)
index d29fa8e..877943b 100644 (file)
@@ -112,3 +112,4 @@ test('T7974', normal, compile, [''])
 test('T7558', normal, compile_fail, [''])
 test('T9096', normal, compile, [''])
 test('T9380', normal, compile_and_run, [''])
+test('T12468', normal, compile_fail, [''])
index 1d49afa..b464547 100644 (file)
@@ -37,8 +37,8 @@ hole_constraints.hs:16:35: warning: [-Wtyped-holes (in -Wdefault)]
       Constraints include Eq a (from hole_constraints.hs:16:10-22)
 
 hole_constraints.hs:20:19: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: b
-      Where: ‘b’ is a rigid type variable bound by
+    • Found hole: _ :: a
+      Where: ‘a’ is a rigid type variable bound by
                the type signature for:
                  castWith :: forall a b. (a :~: b) -> a -> b
                at hole_constraints.hs:19:1-29