Comment author: @garrigue

I'll have to check in detail, but IIRC, this is required for soundness (this doesn't mean that there couldn't be another workaround).
Namely, GADT unification should succeed whenever it could have succeeded elsewhere.
Since such a recursive type could come from a module compiled with -rectypes, we have to assume that it could be built, and not reject it as impossible. (Here the fact -rectypes is inherited between compilation units is not relevant, since building a recursive type witness later would have the same impact.)
Note that this only occurs when one is refining an abstract type during GADT unification.
Maybe it would be a good idea to have a more formal look at the theory.

Comment author: @garrigue

Reading the report again, the fact it is rejected without the abbreviation is not surprising (since then GADT unification is not triggered), but the -principal case requires checking where the failure occurs. I.e., this shouldn't allow building a refutation case for some type that is actually inhabited.

Comment author: @garrigue

Sorry, I had misred the report: this code is accepted both with and without the annotation, but the inferred type is different.
Looking at past compilers, it seems that the recursive type appears in 4.03.
In 4.02.3, without the annotation we have an error.

For why this is accepted in non -principal mode, this is clear enough: the type of the first case is propagated to the second one, forcing unification between the parameters, which are GADT parameters, so unification is done in so-called pattern mode.
Here are the first two lines of Ctype.occur:

let occur env ty0 ty =
let allow_recursive = !Clflags.recursive_types || !umode = Pattern in

As explained before, this is needed because unification is also used to prune impossible cases during exhaustiveness check, and one could create a witness containing a recursive type when in recursive types mode.

In the -principal case, the type inferred for the first case is not propagated to the second one, so there is no failure during GADT unification, only later on when trying to unify the types of all cases, but then we are back in expression mode, and the occur check is strict.

A possible solution would be to add a flag to distinguish between normal inference and pruning; but this would break the symmetry we have now that one can always complete a pattern matching by the cases that were found missing.
So I'm not sure that any change is needed.

This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc.

Following a question by @fpottier on Mattermost, I'm looking into a warning for cases when one instantiates an external type variable in a GADT.

The warning PR is #9542, but it appears to be intrusive.
Concerning the first part, related to the creation of an unintended recursive type, we might be stricter when typing, now that it appears that the check mode has to be more lax than the typing mode anyway.