This is a bug fix. It needs a review.

It is easy to see that this PR only removes code, and it appears to being so consistently (it removes a global reference, so we would get a static error if a use-case had been forgotten). Jacques says that it removes a weird monster-barring feature that is not used anymore, and at least we can see that the regression tests he added when he introduced that feature are still passing, so it sounds reasonable that indeed the feature is not needed anymore -- which is good news as it was making the code more complex.

I tried to understand more of the code. I think it would help to have documentation for Reither somewhere (there are a few words for the two boolean fields in types.mli). If I understand correctly, the second parameter is a n-ary conjunction of possible types. (I don't understand what the third parameter does, but it is unrelated to the present PR.)

I don't understand what unify_row is supposed to be doing on conjunctions of Reither types ; in particular, in one codepath it unifies all types of the conjunct together, but in another it does not. (Naively, if we know that we are later going to unify them all, it would seem correct to always append the two lists to create a bigger conjunct without failing. Is it better to fail earlier?)

Finally, @garrigue, you mention that now "we always use GADT unification". What does this mean, and where is this in the code? What is the relation to unify_row?

Ok, lots of questions.
About Reither, its second argument represents a conjunction of types that its value argument is supposed to have. This list is extensible through its 4th argument, as Btype.row_field_repr shows. The 3rd argument indicates a special case where unification of the conjunction is forced, either during the typing of pattern-matching, or for so-called fixed types, whose row variable is either Tconstr or Tpoly.

Unification of the conjunction is delayed until the argument is known to be present, or if its 3rd argument is true, or in a special rigid_variants mode that is used when checking type equality with eqtype.

The special behavior for fixed types and eqtypes is because we are comparing type schemes: we do not want to allow instantiating them during the comparison. The pattern-matching case is a bit different: it allows the early detection of incoherent pattern matchings, where a branch expects a type for an argument, and another branch expects a different type, meaning that neither could be used.

The relation to GADTs is because #7269 was introduced to fix a problem in GADT exhaustiveness checking, and that this problem disappeared when we switched to GADT unification for exhaustiveness. So this fix is no longer necessary.

It would take me a lot of work to do a proper review by the standards I am usually comfortable with (eg. understanding the code that is modified, what causes the bug, the reason the change fixes the bug, and being able to reason about potential regressions) -- and a lot of time for Jacques to provide extra explanations. I don't know if I should do this (but I wasn't available for this last week and I don't know about this week), or hope for a providential better reviewer to show up, or just approve the thing because the testsuite passes.

One minor question: I apologize for being slow, but I still don't really know what @garrigue means by "we now use GADT unification". (If I wanted to understand what the "previous" behavior was, and how it sometimes required passive_variants, where should I look at?). In typecore, unify_pat_types has a conditional that calls either unify_gadt or unify, but trying to understand the difference between the two modes (in particular for polymorphic variants) by reading the code led me nowhere.

Thanks for the reviews !
Merged and cherry-picked to 4.11 as d6e8494

I had a meeting today with @garrigue and @trefis where we discussed rows again. I'm planning to send a PR with some documentation for which constructors are valid, but in the meantime let me dump my notes here, which were taken as a comment in a function (fold_row) that considers all possible cases:

let rec fold_row f init row =
  let result =
    List.fold_left
      (fun init (_, fi) ->
         match row_field_repr fi with
         | Rpresent(Some ty) -> f init ty
         | Reither(_, tl, _, _) -> List.fold_left f init tl
         | _ -> init)
      init
      row.row_fields
  in
  match (repr row.row_more).desc with
    Tvariant row -> fold_row f result row
  | Tvar _ | Tunivar _ | Tsubst _ | Tconstr _ | Tnil ->
      (* These are all the cases that can ever happen
         - Tvariant: recursive case
         - Tvar | Tunivar: "open" variant
         - Tsubst: go look below
         - Tnil: "static" row
                  (no variable in the variant structure, either in Field or in row_more)
         - Tconstr:
           - private rows
           - GADTs: the row is a locally-abstract type
             (happens when you add an equation between
              a locally-abstract type provided by the user
              and a polymorphic variant, during pattern typing)

         "fixed": a rigidified instance of Poly:
         + cannot add new fields
         + cannot change the status of existing fields
         + conjunctive types are not allowed
         you can have variables (including in the row) but they are rigid

         fixed_explanations are not prescriptive, they only inform on the choices
         that were made (and can be seen at some other place in the structure)
         for error-message purposes.

         Different of views: the row either denotes "the rest of the fields"
           ([`A | `B | 'r ])
         or "all the fields" (differential view)
           ([> 'A | 'B] as 'r)

         OCaml mixes both views (hmm...), the Tconstr actually uses
         the all-the-fields view, but the other
         cases use the rest-of-the-fields views.

         Canonical representation of polymorphic variants:
         - concatenate the fields
         - "substitute" the row_more in the Tconstr case,
           given that it uses the all-the-fields view.
           In practice the implementation does not actually
           do this.

         Rumors: maybe in unify_rows the Tconstr is differential.
      *)
    begin match
      Option.map (fun (_,l) -> List.fold_left f result l) row.row_name
    with
    | None -> result
    | Some result -> result
    end
  | _ -> assert false