Need to qualify type constructor in state type declaration
Closed this issue · 1 comments
When declaring the type of the state, we use the type of the models.
They are usually types from the Gospelstdlib (but this is not a gospel obligation).
The code generated does not qualify the type constructors, so list
is really from the OCaml standard library and sequence
raises an error.
There are two possibilities:
- qualify the type constructors in the
type state
declaration (this need checking that this is indeed a type from the Gospelstdlib) - open
Ortac_runtime.Gospelstdlib
before (we need to chack that this does not raise name capture problem)
Oh! That’s ringing a bell!
core_type_of_ty_with_subst
has a special case for integer
(but core_type_of_tysymbol
has not, and I don’t know why) which is a really adhoc solution. But now, it turns out that there are more than one such case.
And contrary to what term
does, those functions don’t rely on Ident.t
unicity to ensure the proper name resolution is performed.
I suggest we use for types what we do for value names, ie adding them to the context with the proper full name. Adding integer
to the stdlib
field of the context (along with all the types of the Gospelstdlib) would be a nicer special case than what is done currently.
Do you agree?