Adapt to being a bit more picky about inference with GADTs

This means adding a few type signature, and some tests failing
(as they should) rather than succeeding

7 files changed, 66 insertions, 4 deletions

diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index e68d1264a4..1b46565fd8 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -11,12 +11,12 @@ test('gadt3', normal, compile, [''])
 test('gadt4', skip_if_fast, compile_and_run, [''])
 test('gadt5', skip_if_fast, compile_and_run, [''])
 test('gadt6', normal, compile, [''])
-test('gadt7', normal, compile, [''])
+test('gadt7', normal, compile_fail, [''])
 test('gadt8', normal, compile, [''])
 test('gadt9', normal, compile, [''])
 test('gadt10', normal, compile_fail, [''])
 test('gadt11', normal, compile_fail, [''])
-test('gadt13', normal, compile, [''])
+test('gadt13', normal, compile_fail, [''])
 test('gadt14', normal, compile, [''])
 test('gadt15', normal, compile, [''])
 test('gadt16', normal, compile, [''])
@@ -73,7 +73,7 @@ test('data2', normal, compile, [''])
 test('termination', normal, compile, [''])
 test('set', normal, compile, [''])
 test('scoped', normal, compile, [''])
-test('gadt-escape1', normal, compile, [''])
+test('gadt-escape1', normal, compile_fail, [''])
 
 # New ones from Dimitrios
 
diff --git a/testsuite/tests/gadt/gadt-escape1.hs b/testsuite/tests/gadt/gadt-escape1.hs
index 4ff33b299b..d90d6a951a 100644
--- a/testsuite/tests/gadt/gadt-escape1.hs
+++ b/testsuite/tests/gadt/gadt-escape1.hs
@@ -12,6 +12,9 @@ hval = Hidden (ExpInt 0) (ExpInt 1)
 -- With the type sig this is ok, but without it maybe
 -- should be rejected becuase the result type is wobbly
 --    weird1 :: ExpGADT Int
+--
+-- And indeed it is rejected by GHC 7.8 because OutsideIn
+-- doesn't unify under an equality constraint.
 
 weird1 = case (hval :: Hidden) of Hidden (ExpInt _) a -> a
   -- Hidden t (ExpInt (co :: t ~ Int) _ :: ExpGADT t) (a :: ExpGADT t)
diff --git a/testsuite/tests/gadt/gadt-escape1.stderr b/testsuite/tests/gadt/gadt-escape1.stderr
index e69de29bb2..53885ffaf2 100644
--- a/testsuite/tests/gadt/gadt-escape1.stderr
+++ b/testsuite/tests/gadt/gadt-escape1.stderr
@@ -0,0 +1,19 @@
+

+gadt-escape1.hs:19:58:

+    Couldn't match type `t' with `ExpGADT Int'

+      `t' is untouchable

+        inside the constraints (t1 ~ Int)

+        bound by a pattern with constructor

+                   ExpInt :: Int -> ExpGADT Int,

+                 in a case alternative

+        at gadt-escape1.hs:19:43-50

+      `t' is a rigid type variable bound by

+          the inferred type of weird1 :: t at gadt-escape1.hs:19:1

+    Expected type: t

+      Actual type: ExpGADT t1

+    Relevant bindings include

+      weird1 :: t (bound at gadt-escape1.hs:19:1)

+    In the expression: a

+    In a case alternative: Hidden (ExpInt _) a -> a

+    In the expression:

+      case (hval :: Hidden) of { Hidden (ExpInt _) a -> a }

diff --git a/testsuite/tests/gadt/gadt13.hs b/testsuite/tests/gadt/gadt13.hs
index bd25262ca6..d36f451c91 100644
--- a/testsuite/tests/gadt/gadt13.hs
+++ b/testsuite/tests/gadt/gadt13.hs
@@ -2,6 +2,9 @@
 
 -- This should fail, because there is no annotation on shw,
 -- but it succeeds in 6.4.1
+--
+-- It fails again with 7.8 because Outside in doesn't
+-- unify under an equality constraint
 
 module ShouldFail where
 
diff --git a/testsuite/tests/gadt/gadt13.stderr b/testsuite/tests/gadt/gadt13.stderr
index e69de29bb2..b03ff492fa 100644
--- a/testsuite/tests/gadt/gadt13.stderr
+++ b/testsuite/tests/gadt/gadt13.stderr
@@ -0,0 +1,16 @@
+

+gadt13.hs:15:13:

+    Couldn't match expected type `t'

+                with actual type `String -> [Char]'

+      `t' is untouchable

+        inside the constraints (t1 ~ Int)

+        bound by a pattern with constructor

+                   I :: Int -> Term Int,

+                 in an equation for `shw'

+        at gadt13.hs:15:6-8

+      `t' is a rigid type variable bound by

+          the inferred type of shw :: Term t1 -> t at gadt13.hs:15:1

+    Relevant bindings include

+      shw :: Term t1 -> t (bound at gadt13.hs:15:1)

+    In the expression: ("I " ++) . shows t

+    In an equation for `shw': shw (I t) = ("I " ++) . shows t

diff --git a/testsuite/tests/gadt/gadt7.hs b/testsuite/tests/gadt/gadt7.hs
index 9c775d2f23..105b60c807 100644
--- a/testsuite/tests/gadt/gadt7.hs
+++ b/testsuite/tests/gadt/gadt7.hs
@@ -11,7 +11,8 @@ data T a where
 i1 :: T a -> a -> Int
 i1 t y = (\t1 y1 -> case t1 of K -> y1) t y
 
--- No type signature; should type-check
+-- No type signature; should not type-check,
+-- because we can't unify under the equalty constraint for K
 i1b t y = (\t1 y1 -> case t1 of K -> y1) t y
 
 i2 :: T a -> a -> Int
diff --git a/testsuite/tests/gadt/gadt7.stderr b/testsuite/tests/gadt/gadt7.stderr
index e69de29bb2..561b0b52b7 100644
--- a/testsuite/tests/gadt/gadt7.stderr
+++ b/testsuite/tests/gadt/gadt7.stderr
@@ -0,0 +1,20 @@
+

+gadt7.hs:16:38:

+    Couldn't match expected type `t' with actual type `t1'

+      `t1' is untouchable

+        inside the constraints (t2 ~ Int)

+        bound by a pattern with constructor

+                   K :: T Int,

+                 in a case alternative

+        at gadt7.hs:16:33

+      `t1' is a rigid type variable bound by

+           the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1

+      `t' is a rigid type variable bound by

+          the inferred type of i1b :: T t2 -> t1 -> t at gadt7.hs:16:1

+    Relevant bindings include

+      i1b :: T t2 -> t1 -> t (bound at gadt7.hs:16:1)

+      y :: t1 (bound at gadt7.hs:16:7)

+      y1 :: t1 (bound at gadt7.hs:16:16)

+    In the expression: y1

+    In a case alternative: K -> y1

+    In the expression: case t1 of { K -> y1 }