typing: fix a try_expand_once forgotten from #10170

[gasche]

(In #10170, almost all callsites of try_expand_once were replaced by calls to try_expand_safe which catches the Escape exception and returns None instead, except a few places that were already catching Escape... and the one occurrence in the diff here, which should also have been replaced.)

On OCaml versions 5.1 and older, this glitch causes a Ctype.Escape(_) uncaught exception on the included test case. See #12971.

With the fix in the present PR (which applies cleanly to 4.14, trunk and everything in between), the included test case results in a proper error on OCaml 5.1 and older.

In OCaml 5.2 and trunk, the included test case does not raise an uncaught exception, and it does not fail with an error instead, the program is accepted with a (recursive) type. This is due to #12691 (included in 5.2), which improved the definition of some expansion functions to not raise Escape and do something more sensible instead. (Edit: not more sensible, it was in fact a regression, see discussion below.)

The summary of my understanding of the issue:

• The present PR is a trivial (obvious, one-line) fix to an uncaught-exception bug from 4.14 to 5.1, and even in trunk/5.2 it makes the code strictly more consistent.
• The behavior inherited from Cleanup expand_abbrev_gen #12691 is even better than the one-line fix (Edit: wrong). But backporting it to older versions (as @Octachron suggested) would be sensibly more work -- I would not take the initiative to do it.

I therefore propose to merge the present PR in trunk, and backport it in 4.14 for now.

[Octachron]

Accepting the code in your test without -rectypes is a bug, not a bugfix.

[gasche]

Hmmm. I agree, and I wonder why I didn't notice this earlier -- I guess I had convinced myself that the test somehow used a feature that allows equi-recursive types.

This suggests that something is slightly wrong with #12691 that we want to fix before the 5.2 release.

I think that this also strengthens my point that this one-line PR is good to have, if only to then backport it to older versions. What do you think?

[Octachron]

Sorry to forgot to mention it before, but #12691 is not enough to replicate the bug in isolation.
I am not sure why we would want to backport a bug to 4.14 ?
I would rather suggest that we first fix what is going wrong in 5.2 before thinking of backporting to 4.14 .

[gasche]

I am not sure why we would want to backport a bug to 4.14 ?

Sorry for being unclear. I propose to include in 4.14 a fix for the uncaught Escape exception, and to start by including the fix in trunk, even though the uncaught exception does not happen anymore (something else does that is weird), because it fixes an inconsistency in the ctype.ml codebase.

[Octachron]

Hard disagree: that would be backporting a bug to 4.14 to erase a bad error message.

[gasche]

I'm confused. If I apply my change to 4.14, the repro case behavior changes from

Fatal error: exception Ctype.Escape(_)

to

19 | ..let T x = xt in
20 |   Seq.cons Seq.empty x
Error: This expression has type ('a Seq.t as 'a) Seq.t Seq.t
       but an expression was expected of type 'b
       The type variable 'b occurs inside ('a Seq.t as 'a) Seq.t Seq.t

Are you saying that the latter output is buggy? (The error message looks a bit odd, but who doesn't?)

[gasche]

For reference, the behavior of the testcase on 4.12 and older (the bug was introduced in 4.13) is as follows:

File "test.ml", lines 4-5, characters 2-22:
4 | ..let T x = xt in
5 |   Seq.cons Seq.empty x
Error: This expression has type
         ('a Seq.t as 'a) Seq.t Seq.t = unit -> 'a Seq.t Seq.node
       but an expression was expected of type 'b
       Type 'c is not compatible with type 'a = unit -> 'c Seq.node 
       The type variable 'c occurs inside 'a

[Octachron]

Ah, I was mislead by your test case and missed the fact that the change resulted in a error message on 4.14. Sorry!

However, the wording of the error message might hint to a deeper problem with error trace, and I would still prefer to understand and fix the issue on 5.2 before backporting to 4.14.

[gasche]

I disagree with your analysis (the bug has been around since 4.13, so I don't understand why figuring out what went wrong with an independent change in 5.2 should be taken as a prerequisite to fixing it), but I will wait to see you in-person to discuss this further.

[gasche]

After an in-person discussion, Florian remains unconvinced that this is the right first move. (I remain convinced.) I am closing for now, I guess he volunteered to look at this himself.

[Octachron]

Alternative test which leads to the same error on 5.2:

let strange x = Seq.[cons x empty; cons empty x]

[Octachron]

After reminding me of the context, I think that this is a correct partial fix.

In particular, the "Escape" error during expansion might be a nested recursive occurrence. In this case, we need to forget all the unifications and abbreviations expansions done in this branch of the occur check and possibly retry at a parent node. And this is the semantics of your try_expand_safe version.

This PR doesn't solve the general bug described in #10170 (that it is possible to escape from the scrutiny of occur_rec and creates recursive types) but it prevents naked error messages while being more principled than the current implementation.

[gasche]

Would you like to see further changes to the PR (besides writing a Changes entry) before approving?

(Should I replace the test with your alternative proposal? Or maybe include both?)

[Octachron]

The current state is fine now that I agree that the state after this PR is clearer.
Having both test seems like a good option since the behavior in the two case has diverged on trunk.

[gasche]

I added a Changes entry, a second test as you suggested, and wrote a comment in the first test explaining that the current output is not correct.

[Octachron]

Sorry I forgot to mention it, but there is already a test for recursive occurrence in tests/typing-misc/occur_rec.ml, I would prefer to have the two test version here rather than multiplying the number of test file.

[gasche]

Ok. I initially did not use an expect test because I wanted to reproduce the uncaught exception error on 4.x, but this is less relevant now so I will move the tests there.

[gasche]

The behavior of your testcase on trunk is interesting:

let strange x = Seq.[cons x empty; cons empty x];;
[%%expect{|
Uncaught exception: Ctype.Escape(_)

|}, Principal{|
val strange : 'a Seq.t Seq.t -> 'a Seq.t Seq.t Seq.t list = <fun>
|}];;

[gasche]

@Octachron I have rebased the PR with the test as you suggested. The first commit adds the test on trunk (no type-checker change), so we can see the before-PR beahvior; the second commit has the fix and updates the testsuite.

[Octachron]

Self-comment: this unsound part is somehow dependent on the previous test, the compiler does not give this unsound type to strange by itself.

[gasche]

(This makes me strictly less confident in except tests for this kind of bugs, but oh well.)

[Octachron]

Cherry-picked to 4.14, 5.2, and changes entry duplicated to the 5.2 section.