search

ggreif / omega

Automatically exported from code.google.com/p/omega
Other
7 stars 0 forks source link

Wrong type inference in rank-2-type #94

Closed GoogleCodeExporter closed 9 years ago

GoogleCodeExporter commented 9 years ago 
Following code:

data A = A (forall x. x -> x, Int)
f1 (A (a, b)) = a
f2 (A (a, b)) = b

infers wrong type for f2:

prompt> :t f1
f1 :: forall a.A -> a -> a

prompt> :t f2
f2 :: forall a.A -> a -> a

If components of the tuple are reversed, then both projections are typed A -> 
Int.

It works correctly with:

data B = B (forall x. x -> x) Int

I'm not sure if Omega supports impredicative polymorphism, perhaps definition 
of A should be forbidden.

Original issue reported on code.google.com by krz.gogo...@gmail.com on 24 Jul 2011 at 3:38

GoogleCodeExporter commented 9 years ago 
for this:

 f3 (A (c@(a, b))) = c

I get:

 Pattern match failure in do expression at Infer.hs:1632:25-30

Using "check c" I see the correct type. "check a" is ok too, "check b" is bad.

Original comment by ggr...@gmail.com on 8 Aug 2011 at 6:51

GoogleCodeExporter commented 9 years ago 
This works as expected:

 data A = A (forall x. (x -> x, Int))

Last line of previous comment (i.e. "check c") rules out a bunch of stuff, and 
this one shows that "forall" _in_ the product is the problem. Outside is okay. 
I see the problem too when I just flip the pair components in the original "A", 
getting "A -> Int" for f1 and f2.

There is a copy&paste error somewhere dissecting products with "foralls".

Original comment by ggr...@gmail.com on 8 Aug 2011 at 7:06

GoogleCodeExporter commented 9 years ago 
r763 fixes this, r764 fixes a related problem with sums (see checkin comment 
for details).

http://code.google.com/p/omega/issues/detail?id=94#c1 is the residual, 
unrelated problem I stumbled upon while debugging.

Original comment by ggr...@gmail.com on 9 Aug 2011 at 4:46