From 433b80dec1cfef787fc1327a9eada1791b11c12e Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Fri, 19 May 2017 10:50:35 +0100
Subject: [PATCH] Ensure that insolubles are fully rewritten
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 | 2 +-
compiler/typecheck/TcRnTypes.hs | 15 +++++---
compiler/typecheck/TcSMonad.hs | 38 +++++++++++++------
compiler/typecheck/TcSimplify.hs | 28 +++++++++-----
testsuite/tests/gadt/T12468.hs | 9 +++++
testsuite/tests/gadt/T12468.stderr | 6 +++
testsuite/tests/gadt/all.T | 1 +
.../should_compile/hole_constraints.stderr | 4 +-
8 files changed, 73 insertions(+), 30 deletions(-)
create mode 100644 testsuite/tests/gadt/T12468.hs
create mode 100644 testsuite/tests/gadt/T12468.stderr
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index b623541e0ced..f53375087428 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -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.
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 40d4f78bc03e..481b2a733e90 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -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]
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index e943254d1898..f7153f8d2a3e 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -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)
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 2822985f542c..557d40de1e8c 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -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
index 000000000000..a147c09fa6a6
--- /dev/null
+++ b/testsuite/tests/gadt/T12468.hs
@@ -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
index 000000000000..729b5c45b032
--- /dev/null
+++ b/testsuite/tests/gadt/T12468.stderr
@@ -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)
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index d29fa8e4b06e..877943b0c525 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -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, [''])
diff --git a/testsuite/tests/typecheck/should_compile/hole_constraints.stderr b/testsuite/tests/typecheck/should_compile/hole_constraints.stderr
index 1d49afa706c7..b46454736588 100644
--- a/testsuite/tests/typecheck/should_compile/hole_constraints.stderr
+++ b/testsuite/tests/typecheck/should_compile/hole_constraints.stderr
@@ -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
--
GitLab