au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

Internal TC failed for banged array type. #369

Closed gteege closed 4 years ago

gteege commented 4 years ago

The code

type A
type T = A[3]!
f: T -> ()
f t = ()

causes the error message

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

It seems that the bang operator has no effect for the array element type. Note that it works fine for A#[3]!.