Fix tricky typing bug with type substitutions

[stedolan]

The following code crashes the compiler with Fatal error: fold Tsubst:

type t = bool
module type Subst = sig
  type t2 := t
  type _ s = C : 'a -> (t * t2 * 'a) s
end

The bug concerns the cached type expansion abbreviations in Ctype.simple_abbrevs. The sequence of events, as far as I can follow it, is:

1. After typechecking the signature, we have two simple_abbrevs entries: t = bool and t2 = t.
   The three occurrences of t (one in s, two in simple_abbrevs) are physically equal type_expr nodes.
   The two occurrences of t2 (one in s, one in simple_abbrevs) are physically equal type_expr nodes.
2. We begin applying the substitution t2 := t to the definition of s, and traverse the tuple t * t2 * 'a in Subst.tyexp
3. Subst.tyexp visits t, sees that there is no transformation to apply, so copies t to a fresh type_expr node (also t) and mutates the original to be a Tsubst.
   NB: Since this t is shared with simple_abbrevs, we now have t2 = Tsubst ... in simple_abbrevs.
4. Subst.tyexp visits t2, sees that it must apply the transformation t2 := t, so calls Ctype.apply.
5. Ctype.apply tries to expand t2 by calling instance_parameterized_type
6. instance_parameterized_type notices that it has a simple_abbrevs to hand, and so expands t2 not to t but to Tsubst ...
7. Ctype.apply feeds the result to the unifier, which explodes upon seeing a Tsubst.

Since Ctype.apply is called from the middle of substitution (during which types are temporarily changed to Tsubst), it seems dangerous to use the shared simple_abbrevs cache. So, the patch here is to clear that cache in apply.

This makes the issue go away, but I'm not convinced it's the right fix as I barely understand how any of the abbrevs / simple_abbrevs machinery works. Opinions? (cc @garrigue @lpw25)

[lpw25]

I think that this is a reasonable fix. It's not quite clear to me under which conditions simple_abbrev doesn't need to be cleared -- it is cleared in surprisingly few and it's hard to see why that's fine. Clearing them in apply makes sense though, it's sound and it clearly fixes a bug in this case.

[garrigue]

Well, simple_abbrevs started as a performance hack, and I don't think any real analysis has been done about its correctness. It handles only simple cases, and as a result seems to kind of work.
It seems strange that it is not cleared every time cleanup_abbrevs is called; on the other hand it is called every time generalize is called, which is quite often, and might explain why problems did not arise.
Note that the interaction found this time is somehow orthogonal to the problem of the validity wrt. the environment.
I'm going to try to look at it myself too.

[garrigue]

After looking carefully at the code in Subst, it is clear that calling Ctype.apply from there is breaking the invariant that types are only modified by Subst.typexp itself, since Ctype.apply may trigger unifications. Subst.typexp, like Ctype.copy, is assuming that nobody else is touching the types while it is working.
While setting simple_abbrevs to Mnil is perfectly fine, this does not really fix the problem.
This brings back the need for an alternative way to do type instantiation, which I attempted without success last year.

[stedolan]

This brings back the need for an alternative way to do type instantiation

I tried doing a specialised version of this for Subst.Type_function, for which the problem is more restricted: type parameters are always distinct variables, and the type is always generic.

Does the new Subst.apply_type_function look correct to you? (It needs some refactoring, though - I copy-pasted most of the Tvariant case from Ctype.copy, and that complicated logic should be factored out somewhere)

[garrigue]

The approach looks correct, but give me a bit more time to check it.
Also, while looking at the implementation of Typemod.params_are_constrained, I discovered that it was using physical equality (List.memq hd tl), while it should be using eq_type : List.exists (eq_type hd) tl.
So the check that the parameters are all distinct could be wrong.
(More precisely, it seems to be the single occurrence of List.memq in typing that went unnoticed in always_repr)

[garrigue]

I did a new check, and see nothing wrong in this PR.
I have a few comments, but they are not strict requirements.
It would still be a good idea to fix Typemod.params_are_constrained, as the current code may break invariants you assume here.

[garrigue]

If you want to check invariants, then I suppose that Tvar should be an error here, and also for get_desc ty: there should not be unbound type variables in a type abbreviation.
Since this should indeed be the case, you could just remove it here to make it clear.

[garrigue]

I was not sure this case was needed here.
Looking at Ctype.add_gadt_equation, Subst.type_expr gets called when we add local constraints during unification, so if this were done by Subst.typexp, there would be no need to do it here.
Before such a change, it seems safer to assume that this is still needed.

[gasche]

The CI seems to fail on the tests tests/typing-signatures/regression_tsubst_error.ml

@garrigue and @stedolan, do you know if it is a serious issue and how to fix it?

[Octachron]

@gasche , that was a problem due to the change of ocamltest syntax. I have pushed a version of the PR with the right test syntax.