Refine the "kick-out" predicate for CTyVarEq

Consider
   Work item:   k ~ *
   Inert item:  (a::k) ~ Int

Then we must kick out the inert item!  We weren't doing that,
something I discovered when fixing Trac #7384.

Discussed with Dimitrios, and we wrote a long comment
Note [Delicate equality kick-out] to explain.

1 files changed, 39 insertions, 28 deletions

diff --git a/compiler/typecheck/TcInteract.lhs b/compiler/typecheck/TcInteract.lhs
index a75890f70a..3facc1e7e4 100644
--- a/compiler/typecheck/TcInteract.lhs
+++ b/compiler/typecheck/TcInteract.lhs
@@ -335,13 +335,17 @@ kickOutRewritable new_flav new_tv
                     --     constraints that mention type variables whose
                     --     kinds could contain this variable!
 
-    kick_out_eq inert_ct = kick_out_ct inert_ct && 
-                           not (ctFlavour inert_ct `canRewrite` new_flav)
-               -- If also the inert can rewrite the subst then there is no danger of 
-               -- occurs check errors sor keep it there. No need to rewrite the inert equality
-               -- (as we did in the past) because of point (8) of 
-               -- See Note [Detailed InertCans Invariants] 
-               -- and Note [Delicate equality kick-out]
+    kick_out_eq (CTyEqCan { cc_tyvar = tv, cc_rhs = rhs, cc_ev = ev })
+      =  (new_flav `canRewrite` inert_flav)  -- See Note [Delicate equality kick-out]
+      && (new_tv `elemVarSet` kind_vars ||              -- (1)
+          (not (inert_flav `canRewrite` new_flav) &&    -- (2)
+           new_tv `elemVarSet` (extendVarSet (tyVarsOfType rhs) tv)))
+      where
+        inert_flav = ctEvFlavour ev
+        kind_vars = tyVarsOfType (tyVarKind tv) `unionVarSet`
+                    tyVarsOfType (typeKind rhs)
+
+    kick_out_eq other_ct = pprPanic "kick_out_eq" (ppr other_ct)
 \end{code}
 
 Note [Kick out insolubles]
@@ -355,27 +359,34 @@ outer type constructors match.
 
 Note [Delicate equality kick-out]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ 
-Delicate:
-When kicking out rewritable constraints, it would be safe to simply
-kick out all rewritable equalities, but instead we only kick out those
-that, when rewritten, may result in occur-check errors. Example:
-
-          WorkItem =   [G] a ~ b
-          Inerts   = { [W] b ~ [a] }
-Now at this point the work item cannot be further rewritten by the
-inert (due to the weaker inert flavor). Instead the workitem can 
-rewrite the inert leading to potential occur check errors. So we must
-kick the inert out. On the other hand, if the inert flavor was as 
-powerful or more powerful than the workitem flavor, the work-item could 
-not have reached this stage (because it would have already been 
-rewritten by the inert).
-
-The coclusion is: we kick out the 'dangerous' equalities that may
-require recanonicalization (occurs checks) and the rest we keep 
-there in the inerts without further checks.
-
-In the past we used to rewrite-on-the-spot those equalities that we keep in,
-but this is no longer necessary see Note [Non-idempotent inert substitution].
+When adding an equality (a ~ xi), we kick out an inert type-variable 
+equality (b ~ phi) in two cases
+
+(1) If the new tyvar can rewrite the kind LHS or RHS of the inert
+    equality.  Example:
+    Work item: [W] k ~ *
+    Inert:     [W] (a:k) ~ ty        
+               [W] (b:*) ~ c :: k
+    We must kick out those blocked inerts so that we rewrite them
+    and can subsequently unify.
+
+(2) If the new tyvar can 
+          Work item:  [G] a ~ b
+          Inert:      [W] b ~ [a]
+    Now at this point the work item cannot be further rewritten by the
+    inert (due to the weaker inert flavor). But we can't add the work item
+    as-is because the inert set would then have a cyclic substitution, 
+    when rewriting a wanted type mentioning 'a'. So we must kick the inert out. 
+
+    We have to do this only if the inert *cannot* rewrite the work item;
+    it it can, then the work item will have been fully rewritten by the 
+    inert during canonicalisation.  So for example:
+         Work item: [W] a ~ Int
+         Inert:     [W] b ~ [a]
+    No need to kick out the inert, beause the inert substitution is not
+    necessarily idemopotent.  See Note [Non-idempotent inert substitution].
+
+See also point (8) of Note [Detailed InertCans Invariants] 
 
 \begin{code}
 data SPSolveResult = SPCantSolve