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.

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