cogent icon indicating copy to clipboard operation
cogent copied to clipboard

Unbox operator applied to function type.

Open gteege opened this issue 5 years ago • 0 comments

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.)

gteege avatar Feb 04 '20 15:02 gteege