Rewrite check_scope_escape using proper marking and unmarking
This uses the Btype.snapshot/backtrack mechanism, to ensure that we
always undo marking on types from the environment and to avoid a
`try ... with ...` construction for each recursive call.
Instead of the erasure scheme that was used up to now, where we
considered that the type was always principal.
Note: the erasure still happens when polymorphic variants appear in the
patterns, and the type of the scrutinee contains a Reither.
`build_subtype` is invoked only through `enlarge_type` when typechecking Pexp_coerce.
The type passed to `build_subtype` can only have `Cok` arrows because:
- the base type is the direct result of `Typetexp.transl_simple_type_delayed` which only introduces `Cok` arrows
- the other source of arrows could be the result of unification; however at this point the type variables are fresh, they have not been unified with any existing types.
Adding this assertion ensures that this property won't be broken by accident.
improved error messages for fixed row polymorphic variants: keep track of the motivation behind a fixed row (e.g it was bound to an universal or existential type variable, or private) in the types themselves and use this explanation in error messages.
* unification trace: track univar renaming
This PR fixes an inconsistency introduced by #2047 : when an universal type variable was renamed in Printtyp, the explanation part of the error message kept the original name leading to potentially confusing error messages.
This PR fixes this inconsistency by keeping the whole type expression in the explanation part of the unification message instead of just its original name (and add a test for this behavior).
Previously, not having a scope meant the type was used in every context,
now we set the scope to "Btype.lowest_level" to mean the same thing.
The equivalence was made obvious by the recent changes to identifiers
scoping.
- when including: the elements are rescoped to the current level (as
well as being given a fresh stamp, which was already the case)
- extension constructors idents cannot be local: they can be used as
types when the constructor's argument is an inlined record. They must be
given a scope
- in check_recmod_inclusion: create a new scope at each iteration
- when checking that type declarations inside recursive modules are well
founded, we now take a generic instance of the declaration (this is
reminiscent of what is done in Ctype.moregeneral)
- Ident.create now takes a scope as argument
- added Ident.create_var to use when the scope doesn't matter
- the current_time and the current_level are unrelated as of this
commit. But one has to remember to bump the level when creating new
scopes.
Thomas Refis
Florian Angeletti
Matthew Ryan
Jacques Garrigue
Gabriel Scherer
Leo White
Leo White
Jeremie Dimino
Florian Angeletti
Jules Aguillon
Alain Frisch