The last commit removes the extra call to correct_levels.
It was replaced by a proper use of instance ty_record in type_expect.
This was the absence of this call that caused the wrong scoping.

If I understand #9759 correctly, the issue is not specific to 4.11 and trunk, the bug has been present in GADT-typing from the start.

Looking at the use of unify_exp_types and instance: it looks like currently there are two mode of uses of unify_exp_types in typecore:

• either the unified type is made of fresh variables created right before it (to unify just a type constructor spine),
  and no instance-taking is done (neither on the unified type nor on the expected type); this is the case for Pexp_tuple, Pexp_array, Pexp_lazy for example
• or the type is an "old" type reused, and we should take an instance, this is the case for Pexp_poly or in the Kept ty_arg1 case of record-field typing

The Pexp_record case defines a unified type ty_record that sometimes is fresh, sometimes is old. The proposed fix is to take an instance of it in any case at unification time. If I understand correctly, it should also be correct to take instances of old types in the ty_record definition, and those are the two occurrences of ty_expected in the definition (on lines 2893 and 2909 of the current trunk). Is this correct?

Another question, are we sure that it was not possible to exploit the current lack of instance to make some programs falls in working order? In other words, are we sure that this cannot break even the most baroque and ill-meaning code?

If I understand #9759 correctly, the issue is not specific to 4.11 and trunk, the bug has been present in GADT-typing from the start.

To be more precise, it is probably there since the introduction of ambivalence tracking. I don't remember quire whether it was already there in 4.00 or 4.01.

Looking at the use of unify_exp_types and instance: it looks like currently there are two mode of uses of unify_exp_types in typecore:

To clarify, here we are talking on of the expected type, which is a type whose structure may be at generic level, but whose variables must be at current_level (or lower).

• either the unified type is made of fresh variables created right before it (to unify just a type constructor spine),
  and no instance-taking is done (neither on the unified type nor on the expected type); this is the case for Pexp_tuple, Pexp_array, Pexp_lazy for example

Indeed. While this is correct from the point of view of levels (assuming that the fresh type is a generic_level), this may introduce ambivalence into the type, and fundamentally unifying a type scheme seems wrong. Hence #9767 changes those too.

• or the type is an "old" type reused, and we should take an instance, this is the case for Pexp_poly or in the Kept ty_arg1 case of record-field typing

This seems the right way to do it, even if it may cause a bit more duplication.

The Pexp_record case defines a unified type ty_record that sometimes is fresh, sometimes is old. The proposed fix is to take an instance of it in any case at unification time. If I understand correctly, it should also be correct to take instances of old types in the ty_record definition, and those are the two occurrences of ty_expected in the definition (on lines 2893 and 2909 of the current trunk). Is this correct?

Since we want to exploit the generic levels inside ty_record, it is import to delay the instantiation until the final unification on line 2920.

Another question, are we sure that it was not possible to exploit the current lack of instance to make some programs falls in working order? In other words, are we sure that this cannot break even the most baroque and ill-meaning code?

What is the direction of this question?
Whether this fix could break valid programs?
This shouldn't be the case, since the only difference is that, thanks to the addition of instance, one avoids a bit of ambivalence, the precise bit that caused the failure in #9759 .
Since the type variables themselves are shared, there is no addition or loss of information.

Since the changelog entry is in 4.11, and we are at the end of the beta cycle, I am mostly asking if we are absolutely certain that this change cannot break any code that compile today even if the code is kind of invalid and only accidentally compiles.

Then I would say this is highly improbable. This would certainly have to rely on a bug somewhere else: in a normal situation, this use of instance can only improve things.

I agree: I believe the patch is safe enough to go in 4.11 if we want. (And if it did break code somehow, it would be code that is wrong and can be fixed; knowing about it later in the 4.11 release cycle is not as good as earlier, but not worse than waiting for 4.12 to find out.) On the other hand, given that the bug is very old, personally I would not bother integrating it in the release pipeline; if I was release manager I would just ignore it to make my life easier.

I don't really see the point of this PR actually / of merging this in 4.11.
The bug is not that critical (no one had noticed it in the past ~8years, not even people writing the testsuite), and we have a more principled fix in #9767 .

I'd vote for closing it.

I agree with @trefis actually. @garrigue, would it work for you?

I want just to make sure there is no misunderstanding.
As it stands now, this PR is just the minimal part of #9767 that fixes the bug.
So it is not so much a question of being principled or not, as how far we want to go.
When #9767 is merged, it will supersede this one, so the question becomes moot at that point.

As I understand it this doesn't fix the bug, it fixes part of the bug (which is fully fixed by #9767). And I don't believe this part of the bug is more critical than the others or that it should be fixed first.

Since there seems to be an agreement that there is no need to merge this and 4.11, and #9767 is better for 4.12, I close this one.