[commit: ghc] master: Test T2239 actually succeeds without impredicativity, because of the new co/contra subsumption check (1b6988e)

[git at git.haskell.org]

Repository : ssh://git@git.haskell.org/ghc

On branch  : master
Link       : http://ghc.haskell.org/trac/ghc/changeset/1b6988e773229ed10a12ca157117d12826609c07/ghc

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

commit 1b6988e773229ed10a12ca157117d12826609c07
Author: Simon Peyton Jones <simonpj at microsoft.com>
Date:   Fri Nov 21 11:31:25 2014 +0000

    Test T2239 actually succeeds without impredicativity, because of the new co/contra subsumption check


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

1b6988e773229ed10a12ca157117d12826609c07
 testsuite/tests/indexed-types/should_fail/T2239.hs | 24 +++++++++++++++----
 .../tests/indexed-types/should_fail/T2239.stderr   | 28 ----------------------
 testsuite/tests/indexed-types/should_fail/all.T    |  2 +-
 3 files changed, 21 insertions(+), 33 deletions(-)

diff --git a/testsuite/tests/indexed-types/should_fail/T2239.hs b/testsuite/tests/indexed-types/should_fail/T2239.hs
index 750fdd9..d84ea17 100644
--- a/testsuite/tests/indexed-types/should_fail/T2239.hs
+++ b/testsuite/tests/indexed-types/should_fail/T2239.hs
@@ -42,10 +42,26 @@ simpleFD = id :: (forall b. MyEq b Bool => b->b)
 
 simpleTF = id :: (forall b. b~Bool => b->b)
 
--- These two both involve impredicative instantiation,
--- and should fail (in the same way)
+-- Actually these two do not involve impredicative instantiation,
+-- so they now succeed
 complexFD = id :: (forall b. MyEq b Bool => b->b)
-               -> (forall b. MyEq b Bool => b->b)
+               -> (forall c. MyEq c Bool => c->c)
 
 complexTF = id :: (forall b. b~Bool => b->b)
-               -> (forall b. b~Bool => b->b)
+               -> (forall c. c~Bool => c->c)
+
+{- For exmaple, here is how the subsumption check works for complexTF
+   when type-checking the expression
+      (id :: (forall b. b~Bool => b->b) -> (forall c. c~Bool => c->c))
+
+   First, deeply skolemise the type sig, (level 3) before calling
+   tcExpr on 'id'.  Then instantiate id's type:
+
+      b~Bool |-3  alpha[3] -> alpha <= (forall c. c~Bool => c->c) -> b -> b
+
+   Now decompose the ->
+
+      b~Bool |-3  alpha[3] ~ b->b,  (forall c. c~Bool => c->c) <= a
+
+   And this is perfectly soluble.  alpha is touchable; and c is instantiated.
+-}
\ No newline at end of file
diff --git a/testsuite/tests/indexed-types/should_fail/T2239.stderr b/testsuite/tests/indexed-types/should_fail/T2239.stderr
deleted file mode 100644
index a5e5227..0000000
--- a/testsuite/tests/indexed-types/should_fail/T2239.stderr
+++ /dev/null
@@ -1,28 +0,0 @@
-
-T2239.hs:47:13:
-    Couldn't match type ‘b -> b’
-                  with ‘forall b1. MyEq b1 Bool => b1 -> b1’
-    Expected type: (forall b1. MyEq b1 Bool => b1 -> b1) -> b -> b
-      Actual type: (b -> b) -> b -> b
-    In the expression:
-        id ::
-          (forall b. MyEq b Bool => b -> b)
-          -> (forall b. MyEq b Bool => b -> b)
-    In an equation for ‘complexFD’:
-        complexFD
-          = id ::
-              (forall b. MyEq b Bool => b -> b)
-              -> (forall b. MyEq b Bool => b -> b)
-
-T2239.hs:50:13:
-    Couldn't match type ‘Bool -> Bool’
-                  with ‘forall b1. (b1 ~ Bool) => b1 -> b1’
-    Expected type: (forall b1. (b1 ~ Bool) => b1 -> b1) -> b -> b
-      Actual type: (b -> b) -> b -> b
-    In the expression:
-        id ::
-          (forall b. b ~ Bool => b -> b) -> (forall b. b ~ Bool => b -> b)
-    In an equation for ‘complexTF’:
-        complexTF
-          = id ::
-              (forall b. b ~ Bool => b -> b) -> (forall b. b ~ Bool => b -> b)
diff --git a/testsuite/tests/indexed-types/should_fail/all.T b/testsuite/tests/indexed-types/should_fail/all.T
index 998193f..233dc67 100644
--- a/testsuite/tests/indexed-types/should_fail/all.T
+++ b/testsuite/tests/indexed-types/should_fail/all.T
@@ -61,7 +61,7 @@ test('T3330b', normal, compile_fail, [''])
 test('T3330c', normal, compile_fail, [''])
 test('T4179', normal, compile_fail, [''])
 test('T4254', normal, compile, [''])
-test('T2239', normal, compile_fail, [''])
+test('T2239', normal, compile, [''])
 test('T3440', normal, compile_fail, [''])
 test('T4485', normal, compile_fail, [''])
 test('T4174', normal, compile_fail, [''])