Commit 6c19112e authored by Simon Peyton Jones's avatar Simon Peyton Jones

Build more implications

The "non-local error" problem in Trac #14185 was due to the
interaction of constraints from different function definitions.

This patch makes a start towards fixing it.  It adds
TcUnify.alwaysBuildImplication to unconditionally build an
implication in some cases, to keep the constraints from different
functions separate.

See the new Note [When to build an implication] in TcUnify.

But a lot of error messages change, so for now I have set
   alwaysBuildImplication = False

Result: no operational change at all.  I'll get back to it!
parent 0dc86f6b
......@@ -1115,7 +1115,7 @@ checkConstraints :: SkolemInfo
-> TcM (TcEvBinds, result)
checkConstraints skol_info skol_tvs given thing_inside
= do { implication_needed <- implicationNeeded skol_tvs given
= do { implication_needed <- implicationNeeded skol_info skol_tvs given
; if implication_needed
then do { (tclvl, wanted, result) <- pushLevelAndCaptureConstraints thing_inside
......@@ -1154,15 +1154,12 @@ checkTvConstraints skol_info m_telescope thing_inside
; return (skol_tvs, result) }
implicationNeeded :: [TcTyVar] -> [EvVar] -> TcM Bool
-- With the solver producing unlifted equalities, we need
-- to have an EvBindsVar for them when they might be deferred to
-- runtime. Otherwise, they end up as top-level unlifted bindings,
-- which are verboten. See also Note [Deferred errors for coercion holes]
-- in TcErrors. cf Trac #14149 for an example of what goes wrong.
implicationNeeded skol_tvs given
implicationNeeded :: SkolemInfo -> [TcTyVar] -> [EvVar] -> TcM Bool
-- See Note [When to build an implication]
implicationNeeded skol_info skol_tvs given
| null skol_tvs
, null given
, not (alwaysBuildImplication skol_info)
= -- Empty skolems and givens
do { tc_lvl <- getTcLevel
; if not (isTopTcLevel tc_lvl) -- No implication needed if we are
......@@ -1177,6 +1174,23 @@ implicationNeeded skol_tvs given
| otherwise -- Non-empty skolems or givens
= return True -- Definitely need an implication
alwaysBuildImplication :: SkolemInfo -> Bool
-- See Note [When to build an implication]
alwaysBuildImplication _ = False
{- Commmented out for now while I figure out about error messages.
See Trac #14185
alwaysBuildImplication (SigSkol ctxt _ _)
= case ctxt of
FunSigCtxt {} -> True -- RHS of a binding with a signature
_ -> False
alwaysBuildImplication (RuleSkol {}) = True
alwaysBuildImplication (InstSkol {}) = True
alwaysBuildImplication (FamInstSkol {}) = True
alwaysBuildImplication _ = False
-}
buildImplicationFor :: TcLevel -> SkolemInfo -> [TcTyVar]
-> [EvVar] -> WantedConstraints
-> TcM (Bag Implication, TcEvBinds)
......@@ -1205,6 +1219,37 @@ buildImplicationFor tclvl skol_info skol_tvs given wanted
; return (unitBag implic', TcEvBinds ev_binds_var) }
{- Note [When to build an implication]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Suppose we have some 'skolems' and some 'givens', and we are
considering whether to wrap the constraints in their scope into an
implication. We must /always/ so if either 'skolems' or 'givens' are
non-empty. But what if both are empty? You might think we could
always drop the implication. Other things being equal, the fewer
implications the better. Less clutter and overhead. But we must
take care:
* If we have an unsolved [W] g :: a ~# b, and -fdefer-type-errors,
we'll make a /term-level/ evidence binding for 'g = error "blah"'.
We must have an EvBindsVar those bindings!, otherwise they end up as
top-level unlifted bindings, which are verboten. This only matters
at top level, so we check for that
See also Note [Deferred errors for coercion holes] in TcErrors.
cf Trac #14149 for an example of what goes wrong.
* If you have
f :: Int; f = f_blah
g :: Bool; g = g_blah
If we don't build an implication for f or g (no tyvars, no givens),
the constraints for f_blah and g_blah are solved together. And that
can yield /very/ confusing error messages, because we can get
[W] C Int b1 -- from f_blah
[W] C Int b2 -- from g_blan
and fundpes can yield [D] b1 ~ b2, even though the two functions have
literally nothing to do with each other. Trac #14185 is an example.
Building an implication keeps them separage.
-}
{-
************************************************************************
* *
......
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