Fix a number of subtle solver bugs

As a result of some other unrelated changes I found that
IndTypesPerf was failing, and opened Trac #11408.  There's
a test in indexed-types/should-compile/T11408.

The bug was that a type like
 forall t. (MT (UL t) (UR t) ~ t) => UL t -> UR t -> Int
is in fact unambiguous, but it's a bit subtle to prove
that it is unambiguous.

In investigating, Dimitrios and I found several subtle
bugs in the constraint solver, fixed by this patch

* canRewrite was missing a Derived/Derived case.  This was
  lost by accident in Richard's big kind-equality patch.

* Interact.interactTyVarEq would discard [D] a ~ ty if there
  was a [W] a ~ ty in the inert set.  But that is wrong because
  the former can rewrite things that the latter cannot.
  Fix: a new function eqCanDischarge

* In TcSMonad.addInertEq, the process was outright wrong for
  a Given/Wanted in the (GWModel) case.  We were adding a new
  Derived without kicking out things that it could rewrite.
  Now the code is simpler (no special GWModel case), and works
  correctly.

* The special case in kickOutRewritable for [W] fsk ~ ty,
  turns out not to be needed.  (We emit a [D] fsk ~ ty which
  will do the job.

I improved comments and documentation, esp in TcSMonad.

1 files changed, 44 insertions, 0 deletions

diff --git a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
index f011bcf465..7cfd19f751 100644
--- a/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
+++ b/testsuite/tests/indexed-types/should_compile/IndTypesPerfMerge.hs
@@ -51,6 +51,50 @@ merge ::
 -}
 merge x y = mkMerge (merger x y) x y
 
+
+{- ------------- NASTY TYPE FOR merge -----------------
+   -- See Trac #11408
+
+   x:tx, y:ty
+   mkMerge @ gamma
+   merger @ alpha beta
+   merge :: tx -> ty -> tr
+
+Constraints generated:
+   gamma ~ MergerType alpha beta
+   UnmergedLeft gamma ~ tx
+   UnmergedRight gamma ~ ty
+   alpha ~ tx
+   beta ~ ty
+   tr ~ Merged gamma
+   Mergeable tx ty
+   Merger gamma
+
+One solve path:
+  gamma := t
+  tx := alpha := UnmergedLeft t
+  ty := beta  := UnmergedRight t
+
+  Mergeable (UnmergedLeft t) (UnmergedRight t)
+  Merger t
+  t ~ MergerType (UnmergedLeft t) (UnmergedRight t)
+
+  LEADS TO AMBIGUOUS TYPE
+
+Another solve path:
+  tx := alpha
+  ty := beta
+  gamma := MergerType alpha beta
+
+  UnmergedLeft (MergerType alpah beta) ~ alpha
+  UnmergedRight (MergerType alpah beta) ~ beta
+  Merger (MergerType alpha beta)
+  Mergeable alpha beta
+
+  LEADS TO NON-AMBIGUOUS TYPE
+---------------  -}
+
+
 data TakeRight a
 data TakeLeft a
 data DiscardRightHead a b c d