Typechecking error with polymorphic constructor in where assignment

[tneele]

Consider the following specification

init ((2 |> L whr L = [] end) == [1,1]) -> tau.delta <> delta;

Linearising this fails with the message

[error]   this is not a sort expression untyped_sort
[error]   Type error while typechecking the data variable L:List(untyped_sort).
[error]   Error occurred while typechecking the where expression 2 |> L whr L=[] end.

The same can be observed with mcrl2i:

mCRL2 interpreter (type h for help)
? v L: List(Pos)
? e 1 |> L whr L=[] end
this is not a sort expression untyped_sort
Type error while typechecking the data variable L:List(untyped_sort).
Error occurred while typechecking the where expression 1 |> L whr L=[] end.
Could not type check data expression 1 |> L whr L=[] end

The fact that we declared L here has no effect, since the where expression introduces a new scope.

The same issue likely occurs with sets and bags, which have the polymorphic constructor {}. I see that it is very difficult to typecheck such constructions. Perhaps the mCRL2 language would benefit from type annotation syntax, for example L = ([] type List(Pos)), where type is a new keyword. I have seen this in several other languages, such as Haskell and SMT-LIB2, so such syntax might be unavoidable in certain situations (this is a wild guess).

[jgroote]

This is a fundamental problem of the typing system. The fact that an error is generated is understandable in this case. I tend to see this as a problem that may be resolved when reimplementing the type system for expressions. We may also consider adding some typing syntax when more changes apply to the language. I would like to rebaptise this is a feature request.