diff options
| -rw-r--r-- | compiler/typecheck/TcEvidence.lhs | 29 | ||||
| -rw-r--r-- | compiler/typecheck/TcSMonad.lhs | 26 |
2 files changed, 31 insertions, 24 deletions
diff --git a/compiler/typecheck/TcEvidence.lhs b/compiler/typecheck/TcEvidence.lhs index 12149058c9..321809f91d 100644 --- a/compiler/typecheck/TcEvidence.lhs +++ b/compiler/typecheck/TcEvidence.lhs @@ -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] ~~~~~~~~~~~~~~~~~ diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs index aa92866ec6..f6f1c7878b 100644 --- a/compiler/typecheck/TcSMonad.lhs +++ b/compiler/typecheck/TcSMonad.lhs @@ -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 |