Commit 1b6988e7 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Test T2239 actually succeeds without impredicativity, because of the new...

Test T2239 actually succeeds without impredicativity, because of the new co/contra subsumption check
parent 7b1a8562
......@@ -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
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)
......@@ -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, [''])
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment