#9765 is now a strict subset of this PR, so that it is no longer needed to fix #9759.
The role of this PR is rather to enforce more invariants.

Note that a review of the semantics of propagation is still needed.
Currently some cases of type_expect are careful of returning the inferred type rather than an instance of the expected type (required to stick to the approach in the PolyML paper), the expected type being only used as a hint, but some other cases just return an instance of the expected type.
It might be clearer to adopt some form of bidirectional inference, where the return type is always an instance of the expected type (possibly with some extra unsharing for the parts that could be inferred).

@trefis, @lpw25, @diremy can be interested by this PR, and the discussion on propagation.

Minor remark:

It is built on top of #9765 but doesn't really reuse it (except for the example).

What do you mean by this? As far as I can tell, the one code change in #9765 (the use instance ty_record in the record case) is reused in this PR.

Naive questions.

Why do we need the begin_def () .. end_def () machinery here? As far as I vaguely understand, these blocks raise the current level, they were initially used for let-definitions which get generalized / introduced polymorphism, and are sprinkled in a few places related to polymorphism, and a couple more in -principal mode. Why are we now performing a generalization on each tuple, array or lazy expression in the program?

There are already def blocks in the pattern-matching code for those constructs, but those look slightly different from the ones introduced in this PR. In the array case for example, we have:

  | Ppat_array spl ->
      let ty_elt = newgenvar() in
      begin_def ();
      let expected_ty = instance expected_ty in
      end_def ();
      generalize_structure expected_ty;
      unify_pat_types ~refine
        loc env (Predef.type_array ty_elt) expected_ty;
      [...]

and now the PR proposes

  | Pexp_tuple sexpl ->
      begin_def ();
      let subtypes = List.map (fun _ -> newvar ()) sexpl in
      let to_unify = newty (Ttuple subtypes) in
      with_explanation (fun () ->
        unify_exp_types loc env to_unify (instance ty_expected));
      end_def ();
      List.iter generalize_structure subtypes;
      [...]

There are several differences here, for example:

• in the pattern case, the inference variable is created at the generic level,
  in the expression case at the local level (and then generalize_structure is called explicitly on it)
• the unification occurs at the local level in the expression case, but only once back at the current level in the pattern case
• we are always taking an instance of the expected type at the local level, but we only call generalize_structure ont it in the pattern case

Do these different approaches result in different behavior? My naive understanding is that the two approaches are essentially equivalent (in both cases the type parameter of the array constructor is lowered from generic to current level), so I'm not sure why we are writing things in fairly different ways. (The pattern approach look simpler, especially if we encapsulated taking-an-instance-at-a-local-level-then-lowering as a helper function).

Note: there is no instance of expected_ty taken in the Ppat_lazy case, is this a bug?

I had thought these cases were wrong when @trefis and I were adding the levels stuff to type_pat. That's why e.g. the Ppat_tuple case does something equivalent to the new version of Pexp_tuple here. But I had been unable to produce any actual buggy behaviour -- in the end I just left myself a todo item to come back later and try to find a bug. So I'm in favour of these changes, but I haven't read the code in detail yet.

Minor remark:

It is built on top of #9765 but doesn't really reuse it (except for the example).

What do you mean by this? As far as I can tell, the one code change in #9765 (the use instance ty_record in the record case) is reused in this PR.

As explained in the second message, this sentence is no longer true: this PR now truly extends #9765.

Taking a fresh instance of ty_expected is morally better that what was done in type_expect before, because it ensures that all the generic parts of the type scheme will be duplicated before unification. This may not be easily observable, but there is something wrong in unifying a type scheme, particularly one that we received, potentially modifying its representation. One could even imagine cases where this would cause the type scheme to become ambivalent, and cause errors later on; apparently there is already instantiation/duplication in other places so that it doesn't seem to really occur.

In you example, type_pat basically does the same thing as I propose for type_exp, in a subtly different way.
For uniformity, let's look at the tuple case:

      let spl_ann = List.map (fun p -> (p,newgenvar ())) spl in
      let ty = newgenty (Ttuple(List.map snd spl_ann)) in
      begin_def ();
      let expected_ty = instance expected_ty in
      end_def ();
      generalize_structure expected_ty;
      unify_pat_types ~refine loc env ty expected_ty;

It creates a generalized copy of the expected type, and unifies it with a fully general pattern type.
Since the expected type was copied, one will actually get the same structure and levels in expected_ty and subtypes as in the approach where both types were instantiated.
The difference is mostly a question of style, and being careful that while it is ok to unify directly with Predef.type_array ty_elt (which creates a new generic array node), one shouldn't unify directly with Predef.type_bool (which is shared).

Note also that the approach in type_pat can be slightly optimized:

      ...
      begin_def ();
      init_def generic_level;
      let expected_ty = instance expected_ty in
      end_def ();
      unify_pat_types ~refine loc env ty expected_ty;

That is, by setting the level to generic_level, one avoids to call generalize_structure.
This relies on the fact that the type variables in expected_ty are not at generic_level.

Finally, is there any advantage in doing the unification on types at current_level rather than generic_level?
While it is legal to do unification at generic_level, and levels will be lowered appropriately, this is partly the cause of the bug in #9759 (not seeing that only one side was a type scheme).
If we switch to a representation where nodes at generic_level are distinguished from shared nodes, then direct unification on type schemes may become illegal.

Finally, is there any advantage in doing the unification on types at current_level rather than generic_level?

I don't think there is any particular advantage to it. If you want to change the code in type_pat to match the code in typ_exp, that would be fine by me. It would be great to one day ban unification on type schemes.

Would it be possible to abstract away some of the machinery here in a helper function?

This is easier to do with the pattern approach, because basically it suffices to abstract

let generic_instance ty =
  begin_def ();
  init_def generic_level;
  let inst = instance expected_ty in
  end_def ();
  inst

[...]
| Ppat_array spatl ->
  let ty_elt = newgenvar () in
  unify_pat_types ~refine loc env (Predef.type_array ty_elt) (generic_instance expected_ty);
  [...]

| Pexp_array sargl ->
  let ty_elt = newgenvar () in
  with_explanation (fun () ->
    unify_exp_types loc env (Predef.type_array ty_elt) (generic_instance expected_ty));
  [...]

But I understand that unifying schemes (that is, types with some parts remaining at the generic level) is frowned upon. The expression approach proposed in this PR is a bit harder to factor out. Maybe something like:

let def_and_generalize f =
  begin_def ();
  let vars = Queue.create () in
  let gen_var () =
    let v = newvar () in
    Queue.add vars v; v
  let ty = f gen_var in
  end_def ();
  Queue.iter generalize_structure vars;
  ty

  | Ppat_array(spatl) ->
      let elt_ty =
        def_and_generalize @@ fun gen_var ->
	let ty = gen_var () in
	unify_pat_types ~refine loc env (Predef.type_array ty) (instance ty_expected);
        ty
      in

  | Pexp_array(sargl) ->
      let elt_ty =
        def_and_generalize @@ fun gen_var ->
	let ty = gen_var () in
	with_explanation (fun () ->
	  unify_exp_types loc env (Predef.type_array ty) (instance ty_expected));
	ty
      in

OK, up to now we have discussed implementation details.
I agree that it is probably better to have a uniform approach for type_exp and type_pat.
@gasche has a point that the generic instance approach is more easily factorizable, even if it may have to go in the future.

However, my main concern is not here, but rather the last commit, which makes ambiguity detection stricter, by removing the clutch that made camlinternalFormat.ml compilable, but only in non-principal mode.
For me, this is reasonable, as the vocation of the non-principal mode is not to compile more programs.
Yet, this may come at the cost of breaking some programs in the wild (requiring more type annotations).

One way to go would be to split the PR in two, quickly converge on the part that is consensual and fixes the bug, and then for the second commit with the last commit do opam-wide testing to have an idea of how much code is broken in the wild.

FTR: I'm quite keen to see the last commit being merged!

But @gasche suggestion also seems reasonable.

I'm also okay with deciding to go ahead and break some programs that were not annotated enough. They are easy to fix in a backward-compatible way.

I have done as announced:

• use generic_instance (which was already defined) where possible
• temporarily reinstate propagation between branches

Once we converge and merge this PR, I will make a separate PR removing propagation between branches.

I'm looking at the code now, and it looks much nicer, thanks!

Why is there no generic instance taken in the Ppat_lazy case?

Why is there no generic instance taken in the Ppat_lazy case?

Seems I missed it. Or more precisely, it was missing in the original code.

Note: generic_instance could also be used in the build_as_type definition.

Actually, no. It can only be used if the variables of the original type are not at generic_level, and build_as_type requires them to be at generic_level. If we use generic_instance we lose the sharing between (instance ty) and ty.

This seems good to go when the CI is green. (You should probably add @trefis and myself as reviewers.)

I haven't had time to give this a proper review yet. I'd be happy to do so, but it will probably have to wait until Monday.

I haven't had time to give this a proper review yet. I'd be happy to do so, but it will probably have to wait until Monday.

I'll wait for that. No hurry.