Variable of unboxed abstract type is treated as linear.

au-ts / cogent

Cogent Project

https://trustworthy.systems/projects/TS/cogent.pml

Other

158 stars 26 forks source link

Variable of unboxed abstract type is treated as linear. #309

Open gteege opened 5 years ago

gteege commented 5 years ago

type A
type B a

f : #(B A)  -> ()
f b = ()

causes the error message:

Parsing...
Resolving dependencies...
Typechecking...
Desugaring and typing...
Internal TC failed: Didn't use linear variable
Compilation failed!

If A is not abstract (replaced by U32) it works.

zilinc commented 5 years ago

~~Need to check if the Isabelle side agrees with the compiler.~~

zilinc commented 5 years ago

91101fc doesn't match the Isabelle spec. In the spec when it checks the kind of TCon tn ts s, it looks at both ts and the sigil s, whereas in the surface TC it only looks at the sigil. Core TC (before 91101fc) was actually correct w.r.t the spec.

zilinc commented 5 years ago

#T can either mean a stack object which contains pointers to the heap, or a purely stack allocated object. From the type we can't tell them apart. But their linearity properties are quite different: the former is linear, and the latter is non-linear. According to the Isabelle semantics, #T seems to mean the latter, but #(T A) means the former, which means that to express the former case, you are forced to parameterise the abstract type with something, but you can instantiate the type var with any linear type.