Commit 433b80de authored by Simon Peyton Jones's avatar Simon Peyton Jones

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.
parent 7b52525e
......@@ -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.
......
......@@ -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]
......
......@@ -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)
......
......@@ -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
......
{-# LANGUAGE GADTs #-}
module T12468 where
data T a where
I :: T Int
f :: T a -> a
f I = _
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)
......@@ -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, [''])
......@@ -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
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment