From 9308c736d43b92bf8634babf565048e66e071bd8 Mon Sep 17 00:00:00 2001
From: Simon Peyton Jones <simonpj@microsoft.com>
Date: Sat, 16 Jan 2016 00:37:15 +0000
Subject: 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.
---
 .../should_compile/IndTypesPerfMerge.hs            | 44 ++++++++++++++++++++++
 testsuite/tests/indexed-types/should_compile/all.T |  1 +
 .../tests/typecheck/should_fail/tcfail201.stderr   |  4 +-
 3 files changed, 47 insertions(+), 2 deletions(-)

(limited to 'testsuite/tests')

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
diff --git a/testsuite/tests/indexed-types/should_compile/all.T b/testsuite/tests/indexed-types/should_compile/all.T
index 15c5b3e027..fe2688e109 100644
--- a/testsuite/tests/indexed-types/should_compile/all.T
+++ b/testsuite/tests/indexed-types/should_compile/all.T
@@ -270,3 +270,4 @@ test('T11067', normal, compile, [''])
 test('T10318', normal, compile, [''])
 test('UnusedTyVarWarnings', normal, compile, ['-W'])
 test('UnusedTyVarWarningsNamedWCs', normal, compile, ['-W'])
+test('T11408', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/tcfail201.stderr b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
index 9aef660dbd..b142cb18bd 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail201.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail201.stderr
@@ -1,6 +1,6 @@
 
 tcfail201.hs:17:56: error:
-    • Couldn't match type ‘a’ with ‘HsDoc id0’
+    • Couldn't match type ‘a’ with ‘HsDoc t0’
       ‘a’ is a rigid type variable bound by
         the type signature for:
           gfoldl' :: forall (c :: * -> *) a.
@@ -8,7 +8,7 @@ tcfail201.hs:17:56: error:
                      -> (forall g. g -> c g) -> a -> c a
         at tcfail201.hs:15:12
       Expected type: c a
-        Actual type: c (HsDoc id0)
+        Actual type: c (HsDoc t0)
     • In the expression: z DocEmpty
       In a case alternative: DocEmpty -> z DocEmpty
       In the expression: case hsDoc of { DocEmpty -> z DocEmpty }
-- 
cgit v1.2.1