Do not use instance ~partial for principality when typing case bodies

[garrigue]

This is a follow-up to #10362.
For some reason, Typecore.type_cases was using instance ~partial when typing bodies of branches in principal mode.
It appears that is was due to spurious scope updates on the expected type when using it to find concrete type definitions.

This PR does several things:

• It reverts Remove propagation from previous branches #9811, which was already reverted in 4.12, as it principality problems are better handled by -principal anyway.
• It uses the same ty_res for all case bodies in principal mode.
• It fixes a number of spurious scope updates by calling generic_instance where needed.
• In enables non-principality warnings for constructor/record disambiguation in case bodies.

[trefis]

There seem to be other occurrences of expand_head env ty_expected in Typecore than the ones you chose to "protect" in this PR.
Can you explain how/why some are protected and not the others?

[trefis]

This call to protect_extraction is redundant with the one done inside extract_concrete_record.
And actually, I think the calls inside extract_concrete_variant and extract_concrete_record should probably be pushed inside extract_concrete_typedecl (which has no other caller).

[garrigue]

Well spotted.
I would prefer not to move that to Ctype, as this is really Typecore related.

[Octachron]

In that case, would it make sense to have a final definition of extract_concrete_typedecl in Typecore and rename the version in Ctype to unprotected_extract_concrete_typedecl?

[trefis]

It reverts #9811, which was already reverted in 4.12, as it principality problems are better handled by -principal anyway.

I wish that wasn't done in this PR.
It's a clearly distinct/separate change from the rest of the PR, and it would be better discussed separately.

[garrigue]

Do you mean that I should first do a PR for the revert, then one for this.
Doing it in the opposite order makes the code more complicated.
The reversion would be dirty too.

[garrigue]

Put differently, I would prefer we discuss both changes jointly.
If people really want to keep #9811, I can remove the removal from this PR, but I would prefer not to do extra work if there is no need.

[garrigue]

There seem to be other occurrences of expand_head env ty_expected in Typecore than the ones you chose to "protect" in this PR.
Can you explain how/why some are protected and not the others?

Good question. The one I added are just those that caused errors in the test suite.
The only way I see is to check them one by one...
The idea is that one should never directly expand ty_expected, as one is always supposed to work with instances of it.
Ideally, we would need a counter-example for each of those, but this may not be very realistic.
It is only ok to expand directly if we are immediately going to raise an error.

I have made a pass over type_expect and friends, and added a few protect_expansion (a better name), but there may be hidden expansions, so this is not really satisfactory.
As Leo suggested, what we need is an expansion that does not change scopes, however we cannot just disable scope updates, as memoization keeps expansions inside the type. Maybe do some clever copying.
More fundamentally, we should probably never work on types at generic level, only on instances. But this requires sequences of instance/generalize that are going to be costly too.

[garrigue]

A few more remarks.

• Looking at the examples, you will see that the error messages in principal mode are now more detailed. In particular, in case of non-principal propagation between branches, you get a scoping error rather than just a type mismatch. So the idea is that now you can really use the principal mode to check principality, and normal mode can stick to backward compatibility as much as possible.
• protect_expansion is only needed for completeness, not for soundness. And adding it can only increase the programs accepted, so in non-principal mode there should be no regressions. I.e., we go back to compatibility with 4.12.
• On could also use it inside type_cases to make sure that spurious side-effect have no impact to other branches in principal mode (this is actually what correct_levels does for the non-principal mode), but this would just hide bugs. If we can accept that the principal mode tries to be more correctly coded, maybe at the cost of losing completeness in case of bugs.

[garrigue]

I have rebased.
Do you still demand that I split the reversal of #9811 in another PR ?
Is everything else fine ?

[kit-ty-kate]

Side note: The reversal of #9811 is necessary to fix the issue described in #10383 (comment)

[garrigue]

@trefis This PR is on the milestone for 4.13, so we should conclude.
Do you have reservations about the contents, or just about the fact it mixes the reversal of #9811 with a fix of principality?

[trefis]

Only about reverting #9811 here; I'd have liked to discuss that further.
Other than that, the fix itself looks good.

[kit-ty-kate]

I'd like to add some precision after a chat with @trefis, regarding the revert of #9811, the issue in parsexp mentioned above can be split into 2 separate issues:

• The genuine failure:

#=== ERROR while compiling parsexp.v0.14.0 ====================================#
# context              2.1.0~rc | linux/x86_64 | ocaml-variants.4.13.0+trunk | file:///src
# path                 ~/.opam/4.13/.opam-switch/build/parsexp.v0.14.0
# command              ~/.opam/opam-init/hooks/sandbox.sh build dune build -p parsexp -j 47
# exit-code            1
# env-file             ~/.opam/log/parsexp-20-72a07e.env
# output-file          ~/.opam/log/parsexp-20-72a07e.out
### output ###
# File "src/parser_automaton_internal.ml", line 485, characters 44-66:
# 485 |     | Sexp -> if is_not_ignoring state then Sexp (Atom str, stack) else stack
#                                                   ^^^^^^^^^^^^^^^^^^^^^^
# Error: The constructor Sexp expects 0 argument(s),
#        but is applied here to 1 argument(s)
#     ocamlopt src/.parsexp.objs/native/parsexp__Parser_automaton_internal.{cmx,o} (exit 2)
# (cd _build/default && /home/opam/.opam/4.13/bin/ocamlopt.opt -w -40 -g -I src/.parsexp.objs/byte -I src/.parsexp.objs/native -I /home/opam/.opam/4.13/lib/base/caml -I /home/opam/.opam/4.13/lib/sexplib0 -intf-suffix .ml -no-alias-deps -open Parsexp__ -o src/.parsexp.objs/native/parsexp__Parser_automaton_internal.cmx -c -impl src/parser_automaton_internal.ml)

This can be fixed with some annotations on the let bindings above the matches: janestreet/parsexp@4a4f08e

• The extra warning:

File "src/parser_automaton_internal.ml", lines 536-540, characters 2-14:
536 | ..match state.kind with
537 |   | Cst ->
538 |     In_sexp_comment
539 |       { hash_semi_pos = current_pos state ~delta:(-1); rev_comments = []; stack }
540 |   | _ -> stack
Error (warning 18 [not-principal]): 
  The return type of this pattern-matching is ambiguous.
  Please add a type annotation, as the choice of `s' is not principal.

This one was classified too fast as an error by myself due to the status of warnings in dune. For this one, the fix is a litte different and requires the user to annotate the expression inside the first case of the match: kit-ty-kate/parsexp@2ea32ee

Given it is the only opam package that has this issue we might want to discuss it further to understand if these two new behaviours are expected or not. Regardless I've pined the JaneStreet maintainer to make a release of parsexp with the first patch as it is already merged.

[trefis]

It looks like both the failure and the warning have the same cause: some annotation being lost. So I'm not sure that split is so relevant.

[garrigue]

Only about reverting #9811 here; I'd have liked to discuss that further.
Other than that, the fix itself looks good.

Sorry for the slow answer, I was giving an intensive course in Kyushu.

For the rationale of combining this with reversal of #9811, the best answer is to look at the changes in warnings/errors.
Basically, this PR removes the warning in non-principal mode (which makes sense as this was essentially a principality warning), and replaces it with a more informative error message in principal mode (making clear that the problem is a missing annotation).
To me, this is better in line with our standard policy.
The idea to provide a warning, and eventually align the behavior to the principal mode, created more problems than it solved (anyway, it is not possible to strictly align on the principal mode, since there is not enough information in normal mode).

Another option would be to work harder at turning the errors in principal mode into warnings, but I'm not sure it is worth the extra complexity (and this can be done independently).

[trefis]

The idea to provide a warning, and eventually align the behavior to the principal mode, created more problems than it solved

Sure, because trying to get a warning implied adding some non trivial code, backtracking, etc. Which I believed is the source for many of the issues we've seen.
The initial idea was just to remove inter-branch propagation. As far as I can tell thousands of opam packages compiled fine, and a few showed the expected error, which could be fixed by adding a type annotation.
I would still be in favor of going that way instead of just reverting everything.

Apparently I'm the only one who cares.

I'll let someone who doesn't care (or who disagrees with my assessment!) approve this PR.

[garrigue]

OK, I'm going to split this one in two, so that you can approve the change here, and somebody else can approve the reversal.
(I would have a problem with somebody else approving the change here without understanding the details.)

[trefis]

Let's perhaps ping @lpw25, @gasche and @Octachron here first, I'm believe they can follow what's going on. (And are likely to have an opinion).

Sorry for all the trouble @garrigue!

[garrigue]

Ok, then let me state my point of view.
When I first proposed to remove propagation from previous branches in normal mode, the goal was to make the normal mode closer to principal, and it was under the assumption that it was not going to break existing code.
I was wrong, and some important opam packages were broken.
Then I hoped that the breakage could be somehow fixed by some backtracking, providing a transition path, but there were too many interactions, and we ended up reverting #9811 in 4.12. At this point I would have preferred reverting in trunk too, but there was some hope that there could be a better solution in 4.13.
My impression is that this PR is the better solution: remove the clumsy backtracking, and have a proper error message.

Now, what to do with the non-principal mode.
There is a rule in ocaml that we do not break existing code without a good reason. Here I do not see a good reason: yes, ideally it is better if the normal mode is closer to the principal mode, but here this is completely unrelated to soundness, or any new feature that would require this change.
Of course, one could work under the assumption that all existing code is in opam, so that fixing the few breakages in opam solves the problem. Unfortunately, I do not think this is true.

This said, if we just remove the special case for ty_expected in non-principal mode inside the type-checking of branches, we get the same improved error message in non-principal mode as for principal mode, so this in itself should help fix broken code.

In the end, my impression is that we agree that this PR is the way to go, the only difference being whether to remove the two lines that allow inter-branch propagation in non-principal mode or not.
I would prefer to keep them, at least for 4.13. And maybe remove them in 5.00 ?

[Octachron]

I tend to agree with @garrigue here: decreasing the gap with the -principal mode seems to bring a too mild benefit compared to the cost of rejecting currently compiling code.

But thinking about the issue, I am probably the one in the wrong here: I should have opened a reverting PR in trunk to mirror the revert in the 4.12 branch. Should I do that right now?

[garrigue]

@Octachron I you want to do that, you can just cherry-pick the first commit from this PR. It already solves the conflicts, and would avoid new conflicts in this PR.

[garrigue]

@trefis You are talking about parts that are not covered by this PR?
I'm not sure my check for places that need to be protected was exhaustive.

[garrigue]

The first expand_head, in type_unknown_arg seems fine, because it is required: there is an argument, so this must be a function.
The second one, in the error message, seems fine too, for the same reason.
The 3rd and 4th, in type_args, need not be protected if there are arguments, but should not be done if sargs is empty (in that case there is no need to expand).
I'm planning to fix that, but this need not be in this PR.

[garrigue]

I did the fix, and now understand your comment: this recovers the symmetry in typing-gadts/ambivalent_apply.ml

[gasche]

@trefis and @garrigue, where are we on this PR?

[garrigue]

For me, it's ready. I'm just waiting for a final review.

[garrigue]

@trefis rebased.

[trefis]

Hm, I just approved because I looked at the changes in typing/ and the testsuite, but by doing that I overlooked that this PR changes makefiles and apparently needs a bootstrap.

The makefile changes feel out of place in this PR. And I would enjoy a one-sentence explanation of why the bootstrap is needed before anyone merges.

unrelated changes in the PR

[garrigue]

I'm working on an M1 Mac, and this makefile change avoids having to reboot every 30mn.
I'll remove it before merging.
I'll check whether the bootstrap is needed, but if it is, it is...

[garrigue]

Ok, I checked.
The bootstrap is needed because of this error:

File "/Users/garrigue/Projects/ocaml/trunk/asmcomp/mach.ml", line 1:
Error: The files /Users/garrigue/Projects/ocaml/trunk/asmcomp/arch.cmi
       and /Users/garrigue/Projects/ocaml/trunk/asmcomp/mach.cmi
       make inconsistent assumptions over interface Arch

Namely, the file arch.ml has no mli, and as a result a new arch.cmi is created when it is compiled with ocamlopt.
However, mach.mli, which was compiled with boot/ocamlc, is not recompiled.
As soon as boot/ocamlc and ocamlopt produce different outputs on arch.ml, a bootstrap is needed.

More precisely, arch.ml contains several pattern-matchings, and it is not too surprising that this PR would change the typing internally (even isomorphic types can easily differ).

[shindere]

See PR #11288 which systematically adds .mli files to all the modules
in the codebase and turns on warning 70 about missing interfaces.
The PR reports the warning as an error.

[garrigue]

@trefis What about cherry-picking this one to 5.0.
As noted in #11340, with was cherry-picked to 5.0 as a regression fix, this PR is also essentially a bug fix, which do not break existing programs (only add warnings).

[Octachron]

I asked @trefis directly and he agrees that it is ok to cherry-pick the fix to 5.0 .

[Octachron]

Cherry-picked on 5.0 as ba12c0e (with the test fix and the correct bootstrapping)