Further refine the test for 'given' equalities

Trac #8651 revealed that my previous fix (itself in response to #8644)
wasn't quite right.  The plan, using the CtOrigin to identify
constraints arising from flattening, is described in TcSimplify,
Note [When does an implication have given equalities?]

5 files changed, 68 insertions, 39 deletions

diff --git a/compiler/typecheck/TcCanonical.lhs b/compiler/typecheck/TcCanonical.lhs
index 21018600bc..823b37fa1a 100644
--- a/compiler/typecheck/TcCanonical.lhs
+++ b/compiler/typecheck/TcCanonical.lhs
@@ -208,7 +208,7 @@ canTuple ev tys
   = do { traceTcS "can_pred" (text "TuplePred!")
        ; let xcomp = EvTupleMk
              xdecomp x = zipWith (\_ i -> EvTupleSel x i) tys [0..]
-       ; ctevs <- xCtFlavor ev (XEvTerm tys xcomp xdecomp)
+       ; ctevs <- xCtEvidence ev (XEvTerm tys xcomp xdecomp)
        ; canEvVarsCreated ctevs }
 \end{code}
 
@@ -335,7 +335,7 @@ newSCWorkFromFlavored flavor cls xis
              xev = XEvTerm { ev_preds  =  sc_theta
                            , ev_comp   = panic "Can't compose for given!"
                            , ev_decomp = xev_decomp }
-       ; ctevs <- xCtFlavor flavor xev
+       ; ctevs <- xCtEvidence flavor xev
        ; emitWorkNC ctevs }
 
   | isEmptyVarSet (tyVarsOfTypes xis)
@@ -875,7 +875,7 @@ can_eq_flat_app ev swapped s1 t1 ps_ty1 ty2 ps_ty2
                  xevdecomp x = let xco = evTermCoercion x
                                in [ EvCoercion (mkTcLRCo CLeft xco)
                                   , EvCoercion (mkTcLRCo CRight xco)]
-           ; ctevs <- xCtFlavor ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
+           ; ctevs <- xCtEvidence ev (XEvTerm [mkTcEqPred s1 s2, mkTcEqPred t1 t2] xevcomp xevdecomp)
            ; canEvVarsCreated ctevs }
 
 
@@ -899,7 +899,7 @@ canDecomposableTyConAppOK ev tc1 tys1 tys2
   = do { let xcomp xs  = EvCoercion (mkTcTyConAppCo Nominal tc1 (map evTermCoercion xs))
              xdecomp x = zipWith (\_ i -> EvCoercion $ mkTcNthCo i (evTermCoercion x)) tys1 [0..]
              xev = XEvTerm (zipWith mkTcEqPred tys1 tys2) xcomp xdecomp
-       ; ctevs <- xCtFlavor ev xev
+       ; ctevs <- xCtEvidence ev xev
        ; canEvVarsCreated ctevs }
 
 canEqFailure :: CtEvidence -> TcType -> TcType -> TcS StopOrContinue
diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index b1f9dbab13..866902ea70 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -555,7 +555,7 @@ solveFunEq :: CtEvidence    -- From this  :: F tys ~ xi1
            -> Type
            -> TcS ()
 solveFunEq from_this xi1 solve_this xi2
-  = do { ctevs <- xCtFlavor solve_this xev
+  = do { ctevs <- xCtEvidence solve_this xev
              -- No caching!  See Note [Cache-caused loops]
              -- Why not (mkTcEqPred xi1 xi2)? See Note [Efficient orientation]
 
@@ -578,7 +578,7 @@ solveFunEq from_this xi1 solve_this xi2
 Note [Cache-caused loops]
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 It is very dangerous to cache a rewritten wanted family equation as 'solved' in our
-solved cache (which is the default behaviour or xCtFlavor), because the interaction
+solved cache (which is the default behaviour or xCtEvidence), because the interaction
 may not be contributing towards a solution. Here is an example:
 
 Initial inert set:
@@ -1520,7 +1520,7 @@ doTopReactFunEq _ct fl fun_tc args xi
 
     succeed_with :: String -> TcCoercion -> TcType -> TcS TopInteractResult
     succeed_with str co rhs_ty    -- co :: fun_tc args ~ rhs_ty
-      = do { ctevs <- xCtFlavor fl xev
+      = do { ctevs <- xCtEvidence fl xev
            ; traceTcS ("doTopReactFunEq " ++ str) (ppr ctevs)
            ; case ctevs of
                [ctev] -> updWorkListTcS $ extendWorkListEq $
diff --git a/compiler/typecheck/TcRnTypes.lhs b/compiler/typecheck/TcRnTypes.lhs
index b005bdcf59..1ad567eaa2 100644
--- a/compiler/typecheck/TcRnTypes.lhs
+++ b/compiler/typecheck/TcRnTypes.lhs
@@ -1756,6 +1756,9 @@ pprSkolInfo UnkSkol = WARN( True, text "pprSkolInfo: UnkSkol" ) ptext (sLit "Unk
 \begin{code}
 data CtOrigin
   = GivenOrigin SkolemInfo
+  | FlatSkolOrigin              -- Flatten-skolems created for Givens
+                                -- Note [When does an implication have given equalities?]
+                                -- in TcSimplify
 
   -- All the others are for *wanted* constraints
   | OccurrenceOf Name           -- Occurrence of an overloaded identifier
@@ -1806,6 +1809,7 @@ data CtOrigin
 
 pprO :: CtOrigin -> SDoc
 pprO (GivenOrigin sk)      = ppr sk
+pprO FlatSkolOrigin        = ptext (sLit "a given flatten-skolem")
 pprO (OccurrenceOf name)   = hsep [ptext (sLit "a use of"), quotes (ppr name)]
 pprO AppOrigin             = ptext (sLit "an application")
 pprO (SpecPragOrigin name) = hsep [ptext (sLit "a specialisation pragma for"), quotes (ppr name)]
diff --git a/compiler/typecheck/TcSMonad.lhs b/compiler/typecheck/TcSMonad.lhs
index 77e19d26c1..b01a67a110 100644
--- a/compiler/typecheck/TcSMonad.lhs
+++ b/compiler/typecheck/TcSMonad.lhs
@@ -41,8 +41,8 @@ module TcSMonad (
     XEvTerm(..),
     MaybeNew (..), isFresh, freshGoal, freshGoals, getEvTerm, getEvTerms,
 
-    xCtFlavor,          -- Transform a CtEvidence during a step
-    rewriteEvidence,    -- Specialized version of xCtFlavor for coercions
+    xCtEvidence,        -- Transform a CtEvidence during a step
+    rewriteEvidence,    -- Specialized version of xCtEvidence for coercions
     rewriteEqEvidence,  -- Yet more specialised, for equality coercions
     maybeSym,
 
@@ -120,7 +120,6 @@ import Name
 import RdrName (RdrName, GlobalRdrEnv)
 import RnEnv (addUsedRdrNames)
 import Var
-import VarSet
 import VarEnv
 import Outputable
 import Bag
@@ -144,6 +143,7 @@ import Data.IORef
 import Data.List( partition )
 
 #ifdef DEBUG
+import VarSet
 import Digraph
 #endif
 \end{code}
@@ -424,7 +424,7 @@ data InertCans
               -- Set to False when adding a new equality
               -- (eq/funeq) or potential equality (irred)
               -- whose evidence is not a constant
-              -- See Note [Canonicalise givens before float decison]
+              -- See Note [When does an implication have given equalities?]
               -- in TcSimplify
        }
 
@@ -512,15 +512,15 @@ emptyInert
 ---------------
 addInertCan :: InertCans -> Ct -> InertCans
 -- Precondition: item /is/ canonical
-addInertCan ics item@(CTyEqCan {})
+addInertCan ics item@(CTyEqCan { cc_ev = ev })
   = ics { inert_eqs = extendVarEnv_C (\eqs _ -> item : eqs)
                               (inert_eqs ics)
                               (cc_tyvar item) [item]
-        , inert_no_eqs = False }
+        , inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
 
 addInertCan ics item@(CFunEqCan { cc_fun = tc, cc_tyargs = tys, cc_ev = ev })
   = ics { inert_funeqs = addFunEq (inert_funeqs ics) tc tys item
-        , inert_no_eqs = not (isLocalGiven ev) && inert_no_eqs ics }
+        , inert_no_eqs = isFlatSkolEv ev && inert_no_eqs ics }
 
 addInertCan ics item@(CIrredEvCan {})
   = ics { inert_irreds = inert_irreds ics `Bag.snocBag` item
@@ -539,12 +539,13 @@ addInertCan _ item
     ppr item   -- Can't be CNonCanonical, CHoleCan,
                -- because they only land in inert_insols
 
-isLocalGiven :: CtEvidence -> Bool
--- True if (a) it's a Given and (b) it mentions a locally-bound evidence variable
--- Thus it is false of flatten-skol equalities, which are Refls
--- See Note Note [Canonicalise givens before float decison]
-isLocalGiven (CtGiven { ctev_evtm = tm }) = not (isEmptyVarSet (evVarsOfTerm tm))
-isLocalGiven _                            = False
+isFlatSkolEv :: CtEvidence -> Bool
+-- True if (a) it's a Given and (b) it is evidence for
+-- (or derived from) a flatten-skolem equality.
+-- See Note [When does an implication have given equalities?] in TcSimplify
+isFlatSkolEv ev = case ctLocOrigin (ctev_loc ev) of
+                    FlatSkolOrigin -> True
+                    _              -> False
 
 --------------
 insertInertItemTcS :: Ct -> TcS ()
@@ -1443,7 +1444,7 @@ newFlattenSkolem ev fam_ty
        ; let rhs_ty = mkTyVarTy tv
              ctev = CtGiven { ctev_pred = mkTcEqPred fam_ty rhs_ty
                             , ctev_evtm = EvCoercion (mkTcNomReflCo fam_ty)
-                            , ctev_loc =  ctev_loc ev }
+                            , ctev_loc =  (ctev_loc ev) { ctl_origin = FlatSkolOrigin } }
        ; return (ctev, rhs_ty) }
 
   | otherwise  -- Wanted or Derived: make new unification variable
@@ -1618,8 +1619,8 @@ Note: The [CtEvidence] returned is a subset of the subgoal-preds passed in
 
 Example
     ev : Tree a b ~ Tree c d
-    xCtFlavor ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
-                                     , ev_decomp = \c. [nth 1 c, nth 2 c] })
+    xCtEvidence ev [a~c, b~d] (XEvTerm { ev_comp = \[c1 c2]. <Tree> c1 c2
+                                       , ev_decomp = \c. [nth 1 c, nth 2 c] })
               (\fresh-goals.  stuff)
 
 Note [Bind new Givens immediately]
@@ -1664,12 +1665,12 @@ This is bad.  We "fix" this by simply ignoring
 But the Right Thing is to add kind equalities!
 
 \begin{code}
-xCtFlavor :: CtEvidence            -- Original flavor
-          -> XEvTerm               -- Instructions about how to manipulate evidence
-          -> TcS [CtEvidence]
+xCtEvidence :: CtEvidence            -- Original flavor
+            -> XEvTerm               -- Instructions about how to manipulate evidence
+            -> TcS [CtEvidence]
 
-xCtFlavor (CtGiven { ctev_evtm = tm, ctev_loc = loc })
-          (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
+xCtEvidence (CtGiven { ctev_evtm = tm, ctev_loc = loc })
+            (XEvTerm { ev_preds = ptys, ev_decomp = decomp_fn })
   = ASSERT( equalLength ptys (decomp_fn tm) )
     mapM (newGivenEvVar loc)     -- See Note [Bind new Givens immediately]
          (filterOut bad_given_pred (ptys `zip` decomp_fn tm))
@@ -1681,14 +1682,14 @@ xCtFlavor (CtGiven { ctev_evtm = tm, ctev_loc = loc })
       | otherwise
       = False
 
-xCtFlavor (CtWanted { ctev_evar = evar, ctev_loc = loc })
-          (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
+xCtEvidence (CtWanted { ctev_evar = evar, ctev_loc = loc })
+            (XEvTerm { ev_preds = ptys, ev_comp = comp_fn })
   = do { new_evars <- mapM (newWantedEvVar loc) ptys
        ; setEvBind evar (comp_fn (getEvTerms new_evars))
        ; return (freshGoals new_evars) }
 
-xCtFlavor (CtDerived { ctev_loc = loc })
-          (XEvTerm { ev_preds = ptys })
+xCtEvidence (CtDerived { ctev_loc = loc })
+            (XEvTerm { ev_preds = ptys })
   = do { ders <- mapM (newDerived loc) ptys
        ; return (catMaybes ders) }
 
diff --git a/compiler/typecheck/TcSimplify.lhs b/compiler/typecheck/TcSimplify.lhs
index 4ffa40f2fc..0fdd2ba3f5 100644
--- a/compiler/typecheck/TcSimplify.lhs
+++ b/compiler/typecheck/TcSimplify.lhs
@@ -1041,15 +1041,15 @@ Consequence: classes with functional dependencies don't matter (since there is
 no evidence for a fundep equality), but equality superclasses do matter (since
 they carry evidence).
 
-Note [Canonicalise givens before float decison]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Note [When does an implication have given equalities?]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider an implication
    beta => alpha ~ Int
 where beta is a unification variable that has already been unified
-to () in an outer scope.  Then we can float the (alpah ~ Int) out
+to () in an outer scope.  Then we can float the (alpha ~ Int) out
 just fine. So when deciding whether the givens contain an equality,
 we should canonicalise first, rather than just looking at the original
-givens.
+givens (Trac #8644).
 
 This is the entire reason for the inert_no_eqs field in InertCans.
 We initialise it to False before processing the Givens of an implication;
@@ -1059,9 +1059,33 @@ However, when flattening givens, we generate given equalities like
   <F [a]> : F [a] ~ f,
 with Refl evidence, and we *don't* want those to count as an equality
 in the givens!  After all, the entire flattening business is just an
-internal matter.  So we set the flag to False when adding an equality
-whose evidence has a locally-bound evidence variable; anything with
-constants (axioms, Refl) is fine.  See isLocalGiven in TcSMonad.
+internal matter, and the evidence does not mention any of the 'givens'
+of this implication.
+
+So we set the flag to False when adding an equality
+(TcSMonad.addInertCan) whose evidence whose CtOrigin is
+FlatSkolOrigin; see TcSMonad.isFlatSkolEv.  Note that we may transform
+the original flat-skol equality before adding it to the inerts, so
+it's important that the transformation preserves origin (which
+xCtEvidence and rewriteEvidence both do).  Example
+     instance F [a] = Maybe a
+     implication: C (F [a]) => blah
+  We flatten (C (F [a])) to C fsk, with <F [a]> : F [a] ~ fsk
+  Then we reduce the F [a] LHS, giving
+       g22 = ax7 ; <F [a]>
+       g22 : Maybe a ~ fsk
+  And before adding g22 we'll re-orient it to an ordinary tyvar
+  equality.  None of this should count as "adding a given equality".
+  This really happens (Trac #8651).
+
+An alternative we considered was to
+  * Accumulate the new inert equalities (in TcSMonad.addInertCan)
+  * In solveInteractGiven, check whether the evidence for the new
+    equalities mentions any of the ic_givens of this implication.
+This seems like the Right Thing, but it's more code, and more work
+at runtime, so we are using the FlatSkolOrigin idea intead. It's less
+obvious that it works, but I htink it does, and it's simple and efficient.
+
 
 Note [Float equalities from under a skolem binding]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~