"bound at" information isn't very precise.

[zilinc]

This program doesn't look correct but typechecks:

foo : all a. (a, a!) -> a

type A

bar : (A, A) -> A
bar (a,a') = let a'' = foo (a, a') !a'
              in a''

[liamoc]

Why isn't it correct?

Edit: Ah, I suppose you should be required to use a'.. wonder why that happened...

[zilinc]

Something very wrong... even code like

type A
foo : A -> ()
foo a = ()

will pass.

[liamoc]

It's a simple bug. I just forgot to emit Drop constraints when stuff goes out of scope.

[liamoc]

Fixed.

[zilinc]

fail_ticket-e36.cogent still passes

[liamoc]

No, it gives this for me:

./tests/fail_ticket-e36.cogent
Parsing...
Resolving dependencies...
Typechecking...
Cannot discard type A but this is needed as the variable a' bound at "././tests/fail_ticket-e36.cogent" (line 5, column 1)
was never used.
   from constraint Drop A
   in the 1st alternative (a, a')
   in the definition at ("././tests/fail_ticket-e36.cogent" (line 5, column 1))
   for the function bar
Compilation failed!

[zilinc]

Indeed.. don't know why it didn't install to the right place..

[zilinc]

the first location isn't good.

[liamoc]

First location?

[zilinc]

this one ---> bound at "././tests/fail_ticket-e36.cogent" (line 5, column 1)

[liamoc]

Yeah unfortunately the locations aren't very precise in the column... patterns don't carry location information IIRC. I might be able to fix that at some point but it means reworking the AST a bit.