diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index b623541e0cedd3662e5cc0981c97dbc6a8b77b7c..f53375087428f1c443055b9efdfdbdab8e47307f 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 40d4f78bc03e5e7eaf4cb2e72180c0b5d9a5023d..481b2a733e904e2777afa389e9930683db7a25b8 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 e943254d189805ae328239b205c7ed1436ace092..f7153f8d2a3e730c316cd2530ec86858b237abeb 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 2822985f542caf8348b38226462e26148b70db8b..557d40de1e8c125077f513ffa21c153227af42fd 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 0000000000000000000000000000000000000000..a147c09fa6a649c2b8013eab6e722221c383cf44
--- /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 0000000000000000000000000000000000000000..729b5c45b0323532310e2a95a0f5c1dc3deb9bfd
--- /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 d29fa8e4b06eda4a89803e3df9b615b11fc457e9..877943b0c525e01ed626b51dadbf6f2bf5321b8a 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 1d49afa706c7ef9159b73c8166c9dc0ece0a7fff..b464547365880c84082c16484d33fa81c7958806 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