cogent
cogent copied to clipboard
Unbox operator applied to function type.
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.)