Fix #13579 by removing equations_generation

[garrigue]

Issue #13579 discovered a soundness issue in unification.
This is a side-effect of using the equations_generation = Forbidden mode in unify3.
Namely, this mode was used when unifying non-injective types parameters in Pattern mode.
The assumption was that, since those unifications were not allowed to instantiate abstract types, non-injective types could not cause the introduction of equations.
#13759 shows that this assumption was wrong: if we allow instantiations in non-injective type parameters, those instantiations can later on cause the introduction of equations while unifying injective one.

The reasonable thing to do is just to scrape the equations_generation = Forbidden mode (it was only used in a single place), and only reify in that case, like we do everywhere else.

There is no failure in the testsuite. I wonder whether this unsoundness was unwittingly used in the wild.

[goldfirere]

I'm not deeply expert here, but this looks like a simplification -- removing a special case that is deemed now unwise. That's generally a safe thing to do, and I'm encouraged that the testsuite passes.

[Octachron]

The can_generate_equations function is now an alias for in_pattern_mode. I think it might be clearer to remove the function.
At the very least, the redundant checks on if in_pattern_mode uenv then (... if can_generate_equations then ...) should be removed in unify3_var and unify3.

[Octachron]

Except for the minor nitpicking above, I agree that the changes not only fixes the soundness of issue of creating channels to leak equality but also make the code simpler.

[garrigue]

Thanks for spotting the duplication. The code can be further simplified as a result.

[Octachron]

A change of behavior with this PR is that:

module M = struct type 'a p end
type _ t = W: int M.p t
let f (W: _ M.p t) = ()

now fails with

Error: This pattern matches values of type int M.p t
       but a pattern was expected which matches values of type $0 M.p t
       The type constructor $0 would escape its scope

whereas

module M = struct type 'a p end
type _ t = W: int M.p t
let f (W: _ t) = ()

is allowed and inferred to be f: int M.p t -> unit.

[garrigue]

Indeed, this behavior is to be expected, since we do not allow unification under non-injective type constructors.
IIRC, the goal of the current code was precisely to avoid this.
A way to handle such cases would be to try again unification in expression mode (not locally, but globally, i.e. before entering unify), or to check the presence of instantiable types before the unification (if there are none, there is no need to use pattern mode).
It would be good to know how much this happens in the wild.

[Octachron]

I would propose to add this example of a not-so-obvious behavior to the test in the PR, and merge this soundness fix in 5.3. If somehow the change of behavior is too unwieldy, we will have time to ponder on alternative solution.

[garrigue]

OK, I will do it. Soundness is paramount.

For the possible workaround, I am thinking of the following steps in unify_gadt:

• first check whether the types contain free variables
• if they don't, do unification in pattern mode
• if they do, first attempt unification in expression mode
• if it fails, backtrack and do unification in patten mode

The only case were the behavior would be changed is if both there are free variables and pattern mode is required, which is already a very fragile situation.

[Octachron]

Cherry-picked to 5.3 in 7244085 in time for the first beta of 5.3.0.

I am planning to review the two remaining type system bug fix before the second beta (planned around the 15th November).

[garrigue]

I have written a fix for your example in #13585 , while I have it in mind.
I think that the error message is sufficiently confusing that it is better to avoid it.