New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Unbox operator applied to function type. #351

Open

gteege opened this issue Feb 4, 2020 · 0 comments

Labels

bug cogent tc newcomer

Contributor

gteege commented Feb 4, 2020

The unbox type operator should have no effect when applied to a non-linear type.
However the code

f: U8 -> U32
f i = i+1

g: #(U8 -> U32) -> U32
g f = f 0

h: () -> U32
h () = g f

causes the error message

Parsing...
Resolving dependencies...
Typechecking...
Error: Leftover constraint!
#(U8 -> U32) :< U8 -> U32
   in the definition at ("UnboxFunction.cogent" (line 4, column 1))
   for the function g
Compilation failed!

That is, a function type F is not equivalent to #F.
(No high priority, just an observation.)

The text was updated successfully, but these errors were encountered:

zilinc added bug cogent compiler cogent tc newcomer and removed cogent compiler labels

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment