I've never been convinced by the need to support GADTs in branches of or-patterns: or-patterns are just a comfortable feature, and it is reasonably easy to expand them, so why bother (knowing that the problem is difficult)?

This said, users of course have no idea of how difficult it is, and end up asking for it...
So I don't fault you for trying to do something.
The problem is that it seems to be complex, and not easy to give it good properties.

If it is OK to have some restrictions, then why not go for something simpler: backtrack!
Of course, there is one major restriction: it only works if the type propagated from outside is ground (i.e. we do not need to propagate anything back). But otherwise, it's really simple.

That's just an idea, of course.

If it is OK to have some restrictions, then why not go for something simpler: backtrack!

Could you expand on this? I don't know what you have in mind when you say backtrack here, do you mind giving a rough outline of what your proposition is?

For the record: the current patch doesn't seem to have a noticeable impact on the compilation time of the compiler (make clean && make world.opt).
I'll produce some more benchmarks (e.g. on the compilation and typing times of janestreet's code base) once the remaining issues (with constructors and records) are resolved.

I was thinking of the very restricted case where the type of the or-pattern is ground and fully know through propagation, and the or-patterns does not contain any pattern variables. In that case, one can just throw out everything, backtracking all unifications. I admit this is pretty restrictive, but how far do we want to go?
My concern with what you are doing is not performance, but the extra complexity of having levels inside patterns. The soundness of all that is not immediate: do you have a paper proof justifying that?

I admit this is pretty restrictive, but how far do we want to go?

All the way? Well, eventually.

My concern with what you are doing is not performance

I wasn't suggesting that, I was just following up on something I initially said when creating this GPR (« On another matter: I'm worried about the impact on typing time of this change ... »).

the extra complexity of having levels inside patterns. The soundness of all that is not immediate: do you have a paper proof justifying that?

Could you elaborate on that? Give an example of something that doesn't seem sound to you?

Just FTR, the current interaction between GADTs and or-patterns is one of the main "usability compromises" of GADTs that had lead me to not use GADTs to enforce stronger type guarantees in some cases.

My concern [is] the extra complexity of having levels inside patterns. The soundness of all that is not immediate: do you have a paper proof justifying that?

Sorry for asking again @garrigue, but could you clarify? Do you have a particular situation in mind?

At a high level, this seems no different from nesting matches, e.g.

# type _ t = Int : int t | Bool : bool t;;

type _ t = Int : int t | Bool : bool t

# let f (type a) (t : a t) (a : a) =
    match t, a with
    | Int, 3
    | Bool, true -> print_endline "OK"
    | Int, 0 -> print_endline "maybe"
    | _, _ -> print_endline "KO"
  ;;

val f : 'a t -> 'a -> unit = <fun>

# let g (type a) (t : a t) (a : a) =
    match t, a with
    | x, y when match x, y with
                | Int, 3 -> true
                | Bool, true -> true
                | _, _ -> false
      -> print_endline "OK"
    | Int, 0 -> print_endline "maybe"
    | _, _ -> print_endline "KO"
  ;;

val g : 'a t -> 'a -> unit = <fun>

If this is the semantics you have in mind, then I would like to know how you connect it with the implementation. The way the type checking is done is clearly different: in one case subpatterns are typed together with their context, and in the other case they are typed later separately.

@garrigue I would have thought that correctly tracking levels when typing patterns would be obviously more correct than what happens at the moment. For example, we currently fail to detect some obvious principality issues:

# #principal true;;
# module M = struct type t = A | B end;;
module M : sig type t = A | B end
# module N = struct type t = A | B end;;
module N : sig type t = A | B end
# open M;;
# open N;;
# let f = function
  | (A : M.t) | B -> ();;
  val f : M.t -> unit = <fun>
# let f = function
  | B | (A : M.t) -> ();;
  Characters 25-34:
    | B | (A : M.t) -> ();;
          ^^^^^^^^^
Error: This pattern matches values of type M.t
       but a pattern was expected which matches values of type N.t

due to not tracking the levels in patterns

The scheme followed for tracking levels in type_pattern here is the same as the one used in type_expect for expressions. It passes forward an expected type whose known structure is
generalized and then ensures the the resulting type is an instance of that expected type. Since
the difference between the new scheme and the old is simply sharing between known structure
it is hard to see how it could affect soundness (modulo bugs in the implementation).

Do you have some specific concern that differs between the expression case -- where we already use this approach -- and the pattern case?

If not then I think that this part of the patch is an improvement in and of itself, and we should consider merging it anyway regardless of how we feel about or-patterns and GADTs.

If you want to turn it into a real proof

A proof of which properties?

If it's soundness, shouldn't it be impossible for a change to the sharing of type structure to affect soundness, and shouldn't changes to the levels of the structure only affect their sharing?

If it's principality, then where is the proof of principality or even formalization for the current treatment of patterns? As I've said, I think this example shows a lack of principality:

# #principal true;;
# module M = struct type t = A | B end;;
module M : sig type t = A | B end
# module N = struct type t = A | B end;;
module N : sig type t = A | B end
# open M;;
# open N;;
# let f = function
  | (A : M.t) | B -> ();;
  val f : M.t -> unit = <fun>
# let f = function
  | B | (A : M.t) -> ();;
  Characters 25-34:
    | B | (A : M.t) -> ();;
          ^^^^^^^^^
Error: This pattern matches values of type M.t
       but a pattern was expected which matches values of type N.t

because any reasonably declarative system for typing patterns will not give the first f a most general type and not the second. To do so would require basically encoding the inference algorithm in the declarative system.

However, even if you don't think that counts for some reason, the "current erasure scheme" which you used instead of levels causes other more obvious principality issues:

# #principal true;;
# module M = struct type t = A end;;
module M : sig type t = A end
# module N = struct type t = A end;;
module N : sig type t = A end
# open M open N;;
# type 'a idpair = 'a * 'a;;
type 'a idpair = 'a * 'a
# type ('a, 'b) pair = 'a * 'b;;
type ('a, 'b) pair = 'a * 'b
# let foo p (x : 'a idpair) (y : ('a, 'a) pair) =
    let z = if p then x else y in
    match z with
    | (A : M.t), A -> ();;
      val foo : bool -> M.t idpair -> (M.t, M.t) pair -> unit = <fun>
# let foo p (x : 'a idpair) (y : ('a, 'a) pair) =
    let z = if p then y else x in
    match z with
    | (A : M.t), A -> ();;
      Characters 105-117:
      | (A : M.t), A -> ();;
        ^^^^^^^^^^^^
Error: This pattern matches values of type (M.t, N.t) pair = M.t * N.t
       but a pattern was expected which matches values of type
         (M.t, M.t) pair = M.t * M.t
       Type N.t is not compatible with type M.t 

whereas with this PR the first foo definition gives a principality warning.

I think the root of the issue here is that we disagree about what this change is doing. To me, this change is taking a part of the system that has no relation to any formalization and replacing it with
an approach that is based on the formalization in your paper. I agree that it is possible that the properties of your formalization may not transfer to patterns causing unexpected problems, but I think it is much more likely that the current approach has such unexpected problems. I also see no particular reason to think that your results wouldn't apply to patterns. So essentially I see this change as putting us on a more stable footing with respect to the theory. It seems strange to ask for proofs about this more theoretically grounded approach when we have none for the more ad-hoc approach that is currently used.

Whereas you seem to think that the current approach is theoretically justified and so this change is moving us to a less justified system since the formalization it is based on has not been extended to patterns.

the problem of proofs by similarity is that they are no proof at all,

As a side note, proofs by similarity are all we have for OCaml. There is no formalisation for OCaml itself, all there is are proofs of small calculi that we think are similar to what OCaml does. I don't think there is anything wrong with this, but it is worth bearing in mind before dismissing such arguments as without merit.

@lpw25 First and foremost, soundness. One wrong level is sufficient to break all the typer.
The problem is both correctly detecting ambivalence, and keeping proper levels in the environment. If ambivalence is not properly detected, then an equation may leak. I think that @trefis approach is correct w.r.t. ambivalence, but having multiple levels inside patterns raises some questions. More generally, what is the meaning of levels in this context: for expressions, they are clearly connected with parts of types shared with the environment; in patterns this seems different.

Looking again at the code, I think the second part of your message is completely irrelevant: this PR still relies on the erasure approach for principality, so it's only adding a new feature (GADTs in or-patterns), not modifying the current approach.

Also, I do not buy your claim that whole OCaml is only proof by similarity. It is of course only a partial proof (only part of the cases were proved), and only about the theory, not the implementation. But what I meant by "proof by similarity" is proof about a different object, that just looks similar. There, none of the cases apply, so you don't even have a partial proof.

And I'm not claiming that all I've done is clean. It's actually the experience of doing things without thinking enough ahead, and regretting it later, which leads me to ask for better guarantees.

Of course thank you for the principality counter-example. I believe it is just an instance of the problem described before: when talking about levels inside a type that has been expansed once, we should look at the expansed version, so we need to keep it. This seems to be perfectly doable. I'm considering fixing that (i.e. the original problem), as it indeed seems more important with GADTs than it was with polymorphic methods.

Allow me to quickly answer the following:

Looking again at the code, I think the second part of your message is
completely irrelevant: this PR still relies on the erasure approach for
principality, so it's only adding a new feature (GADTs in or-patterns), not
modifying the current approach.

You are correct. We had left that in because it seems needed for the typing of polymorphic variants. However, since it should not be needed anymore for other principality concerns, I just pushed a commit (b05445c) removing it in that case.

The output of a bunch of tests changed as a result, most of the changes being an improvement (typing-warnings/records.ml, typing-warnings/pr6872.ml, typing-misc/disambiguate-principality.ml, typing-gadts/or_patterns.ml, typing-gadts/pr6690.ml, typing-gadts/pr7016.ml, typing-gadts/pr7222.ml), and one being neither a clear improvement nor really a regression ( typing-gadts/test.ml).

To reiterate: the erasure approach is currently still used when a polymorphic variant appears in the patterns and the expected type contains a Reither. We assume that this is still needed for the principality of polymorphic variants typing, but it would be interesting to see if a level based approach could be used instead.

On another note, it seems to me that you didn't really adress one of Leo's point (which is understandable as this discussion is spread in many directions), which was:

[...] you seem to think that the current approach is theoretically justified
and so this change is moving us to a less justified system since the
formalization it is based on has not been extended to patterns.

Do you agree with his statement? And if so, could you explain to us why you think the current approach is justified?

@trefis
First on principality. It's interesting, and I agree that the error message using erasure are bound to be worse, since we discard the parts of the type whose level is not high enough. I didn't check in details, but are there cases where the result really differs (i.e. one of the sides as neither warning nor error)?
If this is the way to go, one would still have to erase a bit for polymorphic variants, but it may be possible to keep the other parts of the type.

Next on the second statement, this is indeed the main point. I think that Leo was talking of principality, while my main concern is soundness. For soundness, I don't see any problem with the current approach: we propagate only part of the type, and unify later with the whole type. And we do not allow creating different contexts, so there is no risk of having equations leaking. For principality, the idea is to remove the parts of the type which we should not refer to. Since the remaining parts are "well-known" (as an expression type), using them is principal (modulo the weakness wrt. abbreviations). Thinking again, it may be that erasure is actually not necessary anymore (in absence of polymorphic variants) since the introduction of ambivalence detection.

I agree that using levels inside patterns may be an improvement. But I would like to see it really defined, at the type system level, in a way that can be used later when modifying type_pat.

I didn't check in details, but are there cases where the result really differs (i.e. one of the sides as neither warning nor error)?

Yes, in two flavors actually:

1. I believe the example Leo gave above is one:

   # module M = struct type t = A | B end;;
   module M : sig type t = A | B end
   # module N = struct type t = A | B end;;
   module N : sig type t = A | B end
   # open M open N;;
   # let f = function (A : M.t) | B -> ();;
   Warning 18: this type-based constructor disambiguation is not principal.
   val f : M.t -> unit = <fun>

   The warning is (obviously) only present with the change of this PR.
2. typing-gadts/pr7016.ml: with the erasing scheme the code is accepted in normal mode and node in principal mode. And I believe that is a bug: in MPR#6993 you say that the creation of recursive types is now allowed during unification of GADT indices (in patterns), but in principal mode as unification of branches is delayed, it doesn't happen in pattern mode, and so the occur check triggered.

Coming back to the broader discussion about the soundness of all this, I discussed it with Leo this morning and it seems that what worries you is the introduction of local scopes (i.e. the fact that we raise the level) which is done to add support for GADTs under or-patterns, not the passing forward of a generalized expected type.

Talking about the meaning of levels, you said:

for expressions, [levels] are clearly connected with parts of types shared with the environment

Which is correct and certainly the meaning associated to levels when they were originaly used for detecting sharing of type variables during generalization.
However, they are now used more generally to detect sharing of types across the boundaries of a scope.
For instance, in the examples below, the sharing doesn't come from the environment but from the return type of the expression:

# type ex = Ex : 'a -> ex
  let f = function Ex x -> x;;
Characters 49-50:
  let f = function Ex x -> x;;
                           ^
Error: This expression has type $Ex_'a but an expression was expected of type
         'a
       The type constructor $Ex_'a would escape its scope

# type _ t = Int : int t
  let f (type a) (x : a t) b = match x with Int -> if b then 3 else (3 : a);;
Characters 89-96:
  let f (type a) (x : a t) b = match x with Int -> if b then 3 else (3 : a);;
                                                                    ^^^^^^^
Error: This expression has type a = int
       but an expression was expected of type int
       This instance of int is ambiguous:
       it would escape the scope of its equation

As you pointed out, for patterns there is no sharing of types with the environment. But there might still be sharing through the return type, as well as through the types of the pattern variables being introduced in the environment. And that is exactly what levels help us detect here.

I think this just leaves your concern about keeping proper levels in the environment. This could happen only in these two cases (that is: sharing with the return type and binding of pattern variables) and, since we unify these types with types from the outter level to check for escapes, the deeper levels can never make it into the environment.

To make the implementation clearer on that last point, I removed some useless calls to check_scope_escapes, and swapped some others out for calls to unify_var (to make sure we update the level of types allowed to escape when leaving the scope of the or-pattern).

What makes things complicated is that levels are used for two things: sharing (with the environment, or with the global state for the value restriction) and scoping (for type definitions, locally abstract types, and ambivalence). All these can be related to the environment (either sharing with it, or scoping), if you see type definitions and GADT equations as being part of the environment. I think the ambivalence paper is relatively clear about that (modulo the absence of weak variables).
When you change levels inside patterns, you interact with both sharing and scoping.
My understanding is that your goal here is to enforce scoping, but you also happen to change sharing, as we see with the new warnings.
I would like to understand the full meaning of levels in patterns. This is not only about this PR, but about how we can use levels in patterns in the future, otherwise this is just a hack that happens to work.

Well, you've confused me a bit now. In an earlier comment it seemed like you were worrying that the addition of new levels within the pattern match -- in other words the change here -- would affect soundness. However, it now seems that it is the changes to sharing caused by passing a type with generalized structure to type_pat that you are worried about instead.

This brings us back to the question of how a change to the sharing of the structural parts of a type could affect soundness. You've mentioned the levels of ambivalent types, but as you've said that isn't an issue with this change, and besides it would always be caught by @trefis recent changes to how the scopes of equations are tracked. So I still don't see by what mechanism you are proposing that soundness could be broken by decreasing the sharing of the structural parts of types -- and to be honest if there is such a mechanism I would be surprised if I couldn't use it to break soundness in a variety of places in the existing code.

My understanding is that your goal here is to enforce scoping, but you also happen to change sharing, as we see with the new warnings.

The changes to sharing are just as much a goal of the change as the checking of scoping. They are required because you want to allow different equations on different sides of the or-patterns. If you share types between both sides of the or-pattern then your equations escape their scope (and @trefis' scoping checks promptly complain that the code is ambiguous).

As I've said before, the changes to sharing seem worth having on their own because they are more correct than the current approach with respect to principality, and just as sound as the current approach.

Here is another example of the difference in sharing:

# type 'a r = { a : 'a; b: 'a };;
type 'a r = { a : 'a; b : 'a; }

# type 'a ty = Int : int ty | Float : float ty;;
type 'a ty = Int : int ty | Float : float ty

# let foo (type a) (ty : a ty) (x : a r) =
    match ty, x with
    | Int, { a = 3; b } -> b
    | _ -> assert false;;
      Characters 89-90:
      | Int, { a = 3; b } -> b
                             ^
Error: This expression has type a = int
       but an expression was expected of type 'a
       This instance of int is ambiguous:
       it would escape the scope of its equation

fails with the current compiler, but is allowed after this PR. Again this is not some unexpected side-effect it is a natural consequence of not adding spurious sharing between sub-patterns. It is the natural counterpart to:

# let foo (type a) (ty : a ty) b : a r =
    match ty with
    | Int -> { a = 3; b }
    | _ -> assert false;;
      val foo : 'a ty -> 'a -> 'a r = <fun>

which is already accepted by the current compiler.

I don't see where you read that in my answer.
I'm concerned by reviewing some code without the appropriate theoretical framework to make sense of it. From the beginning, this hasn't changed.

Well, you said:

but having multiple levels inside patterns raises some questions

but then you started talking about sharing, which is not related to having multiple levels inside of patterns.

I still don't understand which "appropriate theoretical framework" describes the current code but not this patch. If you don't think we have sufficient theory to decide which types should be shared in a pattern, then I don't see how you justify the choice of sharing in the current code. Especially since, as I've shown through multiple examples, it is incorrect in terms of principality and different from the equivalent sharing in expressions.

but then you started talking about sharing, which is not related to having multiple levels inside of patterns.

To make this clearer, should I split out the part of this patch that only changes the sharing into it's own PR? Because at the moment, I still cannot tell whether or not that is the part whose soundness is being debated. Hopefully that would provide some clarity to this discussion.

When I was talking of sharing it was actually about your example how you could detect propagation of type information from one branch of an or-pattern to the other, and also of the potential interaction with the generated environment, not specifically of the uncaring you're doing through generalization.
I'm more confident about the unsharing, because it can be seen as improved generalization inside the expression type, something that has already been proposed in the past, and has both a logical and practical counterpart (i.e. one is just accessing subparts of the value matched on). Do you really think there is much to gain by including this change first?

Thanks, that makes things clearer. I'll give a more thorough response on Monday when England aren't playing football.

Do you really think there is much to gain by including this change first?

Well, if I'm understanding you correctly, that would already be sufficient to make:

# type 'a r = { a : 'a; b: 'a };;
type 'a r = { a : 'a; b : 'a; }

# type 'a ty = Int : int ty | Float : float ty;;
type 'a ty = Int : int ty | Float : float ty

# let foo (type a) (ty : a ty) (x : a r) =
    match ty, x with
    | Int, { a = 3; b } -> b
    | _ -> assert false;;

type-check, bringing it into line with the behaviour for expressions. That seems a worthwhile improvement to me. I also think that dividing this PR into separate coherent parts will make the discussion clearer.

If you think so, feel free to submit a separate PR. I see no theoretical problem for the generalization part.
Note however that if you're pursuing symmetry, you should be careful of what happens with let in too. It seems that type_cases is called whenever the pattern contains constructors (may_contain_gadts is a misnomer), so at least for your example it is fine.

Note however that if you're pursuing symmetry, you should be careful of what happens with let in too.

Well, let in are already a problem even without these changes. And we do plan to address them (cf. https://blog.janestreet.com/plans-for-ocaml-408/#improve-type-propagation-in-lets ), but for the moment I don't think there's much that can be done in type_let (as when it calls type_pattern, the expected type is always a fresh variable).

Everything has been split out in smaller, more focused PRs.
I'm closing this one.