Shadowing builtin types in Alt-Ergo native language

[Halbaroth]

Dolmen accepts to shadow some builtin types. For instance, the input file:

logic x : (int, int) farray
type ('a, 'b) farray
logic y : (int, int) farray

goal g : x = y

produces the error:

goal g : x = y
             ^^^^^
Error The term: `y` has type `farray(int, int)`
      but was expected to be of type `array(int, int)`

The legacy frontend of Alt-Ergo accepts this input file because it uses the names of types as identifiers.

Notice this file is refused by both legacy and Dolmen frontend:

type int 

goal g : true 

because int is a reserved token, which isn't the case of farray.

It seems shadowing is used in the SMT-LIB as noticed in the issue #712.

[Gbury]

Note: it is easy for Dolmen to change that behavior and for instance treat as errors a problem that would try to redefine/shadow a builtin type (that is already being done for the smtlib). It all depends on the rules for the native ae language, which the alt-ergo team can choose.

[Halbaroth]

I think we should forbid such redefinitions but we can do it after the next release.

[hra687261]

IIRC it was used on function and value names, not on theory symbols, AFAIK the shadowing of theory symbols is not allowed in the SMT-LIB standard.