search

google-code-export / omega

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

annotated binding occurrences parsed but not enforced #82

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago 
What steps will reproduce the problem?

1. create test:

cat > test.prg
foo :: (forall (a::Tag) . Label a -> Int) -> Int
foo x = 42 + x `o

bar :: Label a -> Int
bar x = 25

baz = \(a :: Label `j) -> trace (show a) 4
baz' (a :: Label `j) = 121

quux :: Label `j -> Int
quux _ = 0

t1 = foo bar
t2 = foo baz
t2' = foo baz'
t3 = foo quux

2. run 'omega test.prg'

3. you see:

In the expression: quux
the result type: Label `j -> Int
was not what was expected: Label !a -> Int

where types have kinds:
   !a:Tag
truths:

(V) different types
   !a   !=   `j
(hb9,`j)

What is the expected output? What do you see instead?

I would expect that baz and baz' are both also not accepted as argument to foo. 
But they obviously are.
Looking at baz's type:

prompt> :t baz
baz :: forall a.a -> Int

prompt> :t baz'
baz' :: forall a.a -> Int

there is no trace of `j at all!

Original issue reported on code.google.com by ggr...@gmail.com on 5 Jan 2011 at 2:27