au-ts / cogent

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

Type variable is signaled as superfluous although used #308

Closed gteege closed 4 years ago

gteege commented 4 years ago
g: all(a).() -> a
h: all(a). a -> ()
f: all(t).() -> ()
f () = let x:t = g[t]() in h[t](x)

causes the error message:

cogent -g Superfluous.cogent 
Parsing...
Resolving dependencies...
Typechecking...
Error: Superfluous type variable(s) t
   in the definition at ("Superfluous.cogent" (line 5, column 1))
   for the function f
Compilation failed!

It seems that only the function type is checked for phantom type variables but the function body is not taken into account:

g: all(a).() -> a
f: all(t).() -> t
f () = g[t]()

is ok.