Commit 7d83fdea authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Bind "given" evidence to a variable, always

This was being done in xCtFlavor, but not in rewriteCtFlavor,
resulting in Trac #7238.

See Note [Bind new Givens immediately] in TcSMonad and
and Note [Coercion evidence terms] in TcEvidence.
parent f4c327ad
......@@ -492,27 +492,26 @@ data EvLit
Note [Coercion evidence terms]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
An evidence term for a coercion, of type (t1 ~ t2), always takes one of
these forms:
co_tm ::= EvId v
A "coercion evidence term" takes one of these forms
co_tm ::= EvId v where v :: t1 ~ t2
| EvCoercion co
| EvCast co_tm co
An alternative would be
* To establish the invariant that coercions are represented only
by EvCoercion
* To maintain the invariant by smart constructors. Eg
mkEvCast (EvCoercion c1) c2 = EvCoercion (TcCastCo c1 c2)
mkEvCast t c = EvCast t c
I don't think it matters much... but maybe we'll find a good reason to
do one or the other. But currently we allow any of the three forms.
We do quite often need to get a TcCoercion from an EvTerm; see
'evTermCoercion'.
INVARIANT: The evidence for any constraint with type (t1~t2) is
a coercion evidence term. Consider for example
[G] g :: F Int a
If we have
ax7 a :: F Int a ~ (a ~ Bool)
then we do NOT generate the constraint
[G} (g |> ax7 a) :: a ~ Bool
because that does not satisfy the invariant. Instead we make a binding
g1 :: a~Bool = g |> ax7 a
and the constraint
[G] g1 :: a~Bool
See Trac [7238]
Note [EvKindCast]
~~~~~~~~~~~~~~~~~
......
......@@ -1478,6 +1478,20 @@ Example
, ev_decomp = \c. [nth 1 c, nth 2 c] })
(\fresh-goals. stuff)
Note [Bind new Givens immediately]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
For Givens we make new EvVars and bind them immediately. We don't worry
about caching, but we don't expect complicated calculations among Givens.
It is important to bind each given:
class (a~b) => C a b where ....
f :: C a b => ....
Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
But that superclass selector can't (yet) appear in a coercion
(see evTermCoercion), so the easy thing is to bind it to an Id.
See Note [Coercion evidence terms] in TcEvidence.
\begin{code}
xCtFlavor :: CtEvidence -- Original flavor
-> [TcPredType] -- New predicate types
......@@ -1494,14 +1508,7 @@ xCtFlavor_cache :: Bool -- True = if wanted add to the solved bag!
xCtFlavor_cache _ (Given { ctev_gloc = gl, ctev_evtm = tm }) ptys xev
= ASSERT( equalLength ptys (ev_decomp xev tm) )
zipWithM (newGivenEvVar gl) ptys (ev_decomp xev tm)
-- For Givens we make new EvVars and bind them immediately. We don't worry
-- about caching, but we don't expect complicated calculations among Givens.
-- It is important to bind each given:
-- class (a~b) => C a b where ....
-- f :: C a b => ....
-- Then in f's Givens we have g:(C a b) and the superclass sc(g,0):a~b.
-- But that superclass selector can't (yet) appear in a coercion
-- (see evTermCoercion), so the easy thing is to bind it to an Id
-- See Note [Bind new Givens immediately]
xCtFlavor_cache cache ctev@(Wanted { ctev_wloc = wl, ctev_evar = evar }) ptys xev
= do { new_evars <- mapM (newWantedEvVar wl) ptys
......@@ -1560,7 +1567,8 @@ rewriteCtFlavor_cache _cache (Derived { ctev_wloc = wl }) pty_new _co
= newDerived wl pty_new
rewriteCtFlavor_cache _cache (Given { ctev_gloc = gl, ctev_evtm = old_tm }) pty_new co
= return (Just (Given { ctev_gloc = gl, ctev_pred = pty_new, ctev_evtm = new_tm }))
= do { new_ev <- newGivenEvVar gl pty_new new_tm -- See Note [Bind new Givens immediately]
; return (Just new_ev) }
where
new_tm = mkEvCast old_tm (mkTcSymCo co) -- mkEvCase optimises ReflCo
......
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