Variable of unboxed abstract type is treated as linear.

[gteege]

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]

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

[zilinc]

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]

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