I'm tempted to say yes: since the discarding was only used for principal, there should be no impact on soundness.
However, we go back to one of my original complaints: you introduce a new notion of principality inside patterns, without having defined it.
The current definition of principal in patterns is: discard all non-principal information before starting typing patterns, and then admit all information generated by the typing as principal (i.e. consider the algorithm itself as principal).
Now you introduce a definition such that some typings of patterns may be considered as non-principal. I expect that some patterns may raise new warnings.
For instance, I would expect your code to deem the following code non-principal (I didn't actually check):

type t = {a:int}
type u = {a:bool}
let f = function [|({a=x}:t); {a=y}|] -> x+y | _ -> 0

The change cannot be decided just on intuition.

you introduce a new notion of principality inside patterns, without having defined it

That's not quite right, though I see what you mean.
Let's go back to your definition, which includes the key element:

The current definition of principal in patterns is: discard all non-principal information before starting typing patterns, and then [...]

Formulated differently, what that's saying is: before typing the patterns, we have some information which is principally known.

It used to be the case that when typing patterns, we passed forward (as expected type) an instance of the type of the scrutinee. Which means that when typing patterns, there is no way to distinguish what was known principally from what wasn't. Which explains the erasure scheme that was in place (and that you defined in your previous message): if we've erased all non-principal information then everything we know, we know principally.

However, since #1909, we now pass a generic type forward when typing patterns. That is: we're now able to distinguish what is principally known from what isn't. Just like we do for expressions. So we don't need to erase the non-principal parts before starting to type patterns, we simply warn when we use them.

For instance, I would expect your code to deem the following code non-principal (I didn't actually check):

It does indeed raise a warning.
There are several other examples of changes in the testsuite.

OK, so your title is a complete misnomer: you are not enforcing principality of the typing of patterns (since you have not defined that), but trying to propagate all types from expressions to patterns while still tracking which part was deemed "principal" (i.e. has polymorphic marks) in those types.
There are advantages: in many cases we end up with warnings rather than errors.
But there are also drawbacks: while until now propagated types could only improve the typing of patterns, they can now weaken it. And there is no clear definition.

This said, with a proper semantics, this might be OK. I.e., it might turn out only to add warnings, never to cause a failure.
However, you would at least need to replace generalize_structure in half_typed_cases by generalize, because it breaks principality.

One year later, could @garrigue render a decision on this PR?

My position hasn't changed: this PR turns a number of typing errors (in principal mode) into principality warnings. So far so good.
It also introduces some new warnings in code that didn't cause any before.
This is a change of behavior, and a change of specification.
In order to judge on that I need to see the new specification.
In particular, in which cases information inferred from the pattern itself can be seen as non-principal.

I'm dubious about "principality" inside patterns (contrary to principality of information coming from outside of the pattern) for two reasons:

• inference propagates information from left to right in patterns, so it would be strange to restrict that direction (I think this PR doesn't do that, at least intentionally, but it is not explicitly stated)
• since GADT unification doesn't even have a mgu, we don't have a real basis to talk about principality other than the inference algorithm itself (there is no such thing as a principality property).

I think I discussed that with @trefis in March, but I understand that doing something about this can take some time.

I'm not sure I can give a specification, but I think I can at least address these two points:

• inference propagates information from left to right in patterns, so it would be strange to restrict that direction (I think this PR doesn't do that, at least intentionally, but it is not explicitly stated)

It indeed does not restrict information flowing from left to right. It restricts the flow of information between the branches of or-patterns.

• since GADT unification doesn't even have a mgu, we don't have a real basis to talk about principality other than the inference algorithm itself (there is no such thing as a principality property).

In the case of or-patterns we do not allow any equations to escape -- so IIUC I think we are back to having a sensible notion of mgu there -- which is what matters here.

I'm not shocked by making flow between branches of or-patterns non-principal, if this is the only restriction. Note that at some time there was a discussion of having the dual of disambiguation by record field for variants:

function M.A -> e1 | B -> e2

This would make it non-principal. But now that disambiguation is by type, one can write an annotation elsewhere.

I'm more concerned about unintended consequences: unification with a variable of lower level making turning an otherwise principal information into non principal. This applies only to corner cases.

For the mgu question, this is not so much about the interaction of your tracking with GADTs, but rather whether we can have a meaningful definition.

I think that the { f1 = ..; M.f2 = ... } feature predates disambiguation, and it can be thought more as a syntactic shortcut to not repeat the module path in each field (relying on the obvious invariant that all fields must be declared in the same module). Note that it works if any field is explicitly prefixed, not just the first one, so it is robust to reordering. We could give the same meaning to the same shortcut on sum types (I'm still in favor) -- but how would it interact with extensible variants?

That is fairly orthogonal to the current discussion, however, given that Leo's example in #1675 (comment) used type annotations rather than path prefixing. I'm repeating it here for the record:

# #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

My position hasn't changed [...]
I think I discussed that with @trefis in March, but I understand that doing something about this can take some time.

I'm a bit surprised by this, I thought that by the end of the discussion your position had changed, at least a bit.

For the question of principality inside patterns, Leo has produced a satisfying answer, which I believe we had already covered when we met, but it was a while ago, so I might be remembering incorrectly.

What I do remember, is that we spent a long while going over all of the tests (added or updated) of this PR, as well as trying some other examples that weren't in the testsuite. At that point, my impression was that you seemed to agree that this PR (and principality inside patterns) made sense, but that there remained one problem with the implementation: the following example should warn, but didn't:

type _ t = IntLit : int t | BoolLit : bool t;;

let f (type a) t (x : a) =
  ignore  (t : a t);
  match t, x with IntLit, n -> n+1 | BoolLit, b -> 1;;

I believe that's where we stopped, as that's one of the examples you sent to me by email.

I should have pushed them on this PR straightaway, I had gone as far as commiting them, but apparently it slipped my mind @xavierleroy pinged this PR (thanks!).

So let me push them now, along with a commit that does fix the implementation: the compiler is now producing warning 18 when introducing GADT equations that rely on non principal information (as in your example above).

Would you mind going over all of the tests once more? If you still have doubts after that, then hopefully we can find some time to discuss them next week.

There were some offline discussions between @garrigue, @lpw25 and I since my last message in November. It is my impression that the PR in its current state (it has changed since November) is satisfactory to everyone.

I have just rebased it, and it is now ready for a proper review.