[commit: testsuite] master: Adapt to being a bit more picky about inference with GADTs (4e5ca8d)

Repository : ssh://darcs.haskell.org//srv/darcs/testsuite

On branch  : master

http://hackage.haskell.org/trac/ghc/changeset/4e5ca8d7dd0db07030e7dc43fc8bc1e8a78a07fc

>---------------------------------------------------------------

commit 4e5ca8d7dd0db07030e7dc43fc8bc1e8a78a07fc
Author: Simon Peyton Jones <[email protected]>
Date:   Fri Oct 19 02:25:16 2012 +0100

    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

>---------------------------------------------------------------

 tests/gadt/all.T                        |    6 +++---
 tests/gadt/gadt-escape1.hs              |    3 +++
 tests/gadt/gadt-escape1.stderr          |   19 +++++++++++++++++++
 tests/gadt/gadt13.hs                    |    3 +++
 tests/gadt/gadt13.stderr                |   16 ++++++++++++++++
 tests/gadt/gadt7.hs                     |    3 ++-
 tests/gadt/gadt7.stderr                 |   20 ++++++++++++++++++++
 tests/polykinds/Freeman.hs              |    8 +++++++-
 tests/typecheck/should_compile/T5655.hs |    1 +
 9 files changed, 74 insertions(+), 5 deletions(-)

diff --git a/tests/gadt/all.T b/tests/gadt/all.T
index e68d126..1b46565 100644
--- a/tests/gadt/all.T
+++ b/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/tests/gadt/gadt-escape1.hs b/tests/gadt/gadt-escape1.hs
index 4ff33b2..d90d6a9 100644
--- a/tests/gadt/gadt-escape1.hs
+++ b/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/tests/gadt/gadt-escape1.stderr b/tests/gadt/gadt-escape1.stderr
index e69de29..53885ff 100644
--- a/tests/gadt/gadt-escape1.stderr
+++ b/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/tests/gadt/gadt13.hs b/tests/gadt/gadt13.hs
index bd25262..d36f451 100644
--- a/tests/gadt/gadt13.hs
+++ b/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/tests/gadt/gadt13.stderr b/tests/gadt/gadt13.stderr
index e69de29..b03ff49 100644
--- a/tests/gadt/gadt13.stderr
+++ b/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/tests/gadt/gadt7.hs b/tests/gadt/gadt7.hs
index 9c775d2..105b60c 100644
--- a/tests/gadt/gadt7.hs
+++ b/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/tests/gadt/gadt7.stderr b/tests/gadt/gadt7.stderr
index e69de29..561b0b5 100644
--- a/tests/gadt/gadt7.stderr
+++ b/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 }
diff --git a/tests/polykinds/Freeman.hs b/tests/polykinds/Freeman.hs
index ea8aff0..13e5d5c 100644
--- a/tests/polykinds/Freeman.hs
+++ b/tests/polykinds/Freeman.hs
@@ -225,10 +225,13 @@ deriving instance Show a => Show (Alt a b)
 
 instance Rec (PHom (->) (->)) (FAlt a) (Alt a) where
   _in = mkPHom f g where
+    f,g :: FAlt a (Alt a) s -> Alt a s
     f FZero = Zero
     f (FSucc1 a b) = Succ1 a b
     g (FSucc2 a b) = Succ2 a b
+
   out = mkPHom f g where
+    f,g :: Alt a s -> FAlt a (Alt a) s
     f Zero = FZero
     f (Succ1 a b) = FSucc1 a b
     g (Succ2 a b) = FSucc2 a b
@@ -252,8 +255,11 @@ type PairUpResult a = K2 [(a, a)] (a, [(a, a)])
 pairUp :: Alt a Fst -> [(a, a)]
 pairUp xs = let (K21 xss) = (fstPHom (fold (mkPHom phi psi))) xs in xss 
  where
-   phi FZero = K21 []
+   phi :: FAlt y (K2 v (r,[(y,r)])) s -> K2 [(y,r)] (y,z) s
+   phi FZero                       = K21 []
    phi (FSucc1 x1 (K22 (x2, xss))) = K21 ((x1, x2):xss) 
+
+   psi :: FAlt y (K2 z w) s -> K2 [x] (y,z) s
    psi (FSucc2 x (K21 xss)) = K22 (x, xss) 
 
 main = print (Succ1 (0::Int) $ Succ2 1 $ Succ1 2 $ Succ2 3 $ Succ1 4 $ Succ2 5 Zero)
diff --git a/tests/typecheck/should_compile/T5655.hs b/tests/typecheck/should_compile/T5655.hs
index 232ea6b..c2eed90 100644
--- a/tests/typecheck/should_compile/T5655.hs
+++ b/tests/typecheck/should_compile/T5655.hs
@@ -23,4 +23,5 @@ f = ap (ETwice . twice)
 foo :: ETwice
 foo = ETwice (5 :: Int)
 
+bar :: IO ()
 bar = ap print (f foo)