# Context

OCaml uses type information to disambiguate constructor variants and
record fields: when you see `Foo t` or `t.bar`, several different
types may have a constructor `Foo` or a field `bar`. If the
type-checker is able to infer the type of `t`, then we know which
constructor/field is meant. Otherwise the compiler defaults to the
suitable type introduced last in scope, but emits a warning -- this is
non-principal and fragile.

(Principality is the property that the type inferred by the OCaml
compiler is the most general type possible for the program. In
particular, it guarantees that adding extra annotations (which can
only force you to use more specific type) can never break typability;
more generally, with principal types you will never find "after the
fact" that the wrong type was inferred. This is a formal property with
important usability properties, that OCaml tries to
preserve. Sometimes doing so would be costly from an efficiency
perspective, and then the default behavior may be non-principal, with
a -principal flag to force the principal behavior. Let's say that we
take principality seriously in the evolution of the OCaml type
system.)

In addition to unification-based type inference, Ocaml has some
dedicated logic to propagate type information from annotations. For
example if you write

  let f : foo -> bar = fun x ->
    Bar x

then the type-checker will know from the `foo -> bar` annotation that
the expected type of `Bar x` is `bar`, so we can disambiguate the
constructor.

While the current situation works in many cases, some users have hit
the limitation of the relatively weak type propagation that
we perform. Consider a let-expression:

    let p = e in body

the implementation has to make a choice between:

- inferring the type of `p` (without knowing what to expect),
  and checking `e` at the resulting inferred type
  (if we were able to infer one with certainty, typically if `p` is an
   annotated pattern `(p' : ty)`)

- inferring the type of `e` (without knowing what to expect),
  and checking `p` at the resulting inferred type
  (if we were able to infer one with certainty, typically if `e` is an
   annotated expression `(e : ty)` or otherwise an inferrable
   neutral term)

Some programs would be nicer (require less annotations) if we inferred
`p` first, others would be nicer if we inferred `e` first. We get
complains from users in either cases.


# Project proposal

We propose to implement a principal strategy for type-based
disambiguation, in an implementation of type inference by constraint
solving. The general idea is to delay the type-checking of the parts
of the program that depend on disambiguation until other parts of the
program have led to the inferrence of a precise type for disambiguation.

In the `let p = e in ...` example, we would have the constraints for
the inference of `p`, and of `e`, in the set of constraints to solve,
and could work on them in parallel. If one gets delayed because
a disambiguation is required, this part of the constraint remains
blocked until disambiguation information is available; we can continue
solving the other side, and that may reveal more type information,
unblocking the blocked constraint.

More precisely, we propose to:

- Extend the Inferno library of François Pottier (for type inference
  with constraint) with support for delayed/blocked constraints.

  https://gitlab.inria.fr/fpottier/inferno

- Extend the ML fragment implemented with Inferno with variant and
  record types and type-based constructor/field disambiguation.