Original bug ID: 7389
Reporter: @gasche
Assigned to: @garrigue
Status: acknowledged (set by @garrigue on 2016-10-18T23:00:20Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing
Has duplicate: #7582
Related to: #7344 #7388
Child of: #7409
Monitored by: @ygrek @jmeber @yallop

Bug description

As with #7388, I'm working on examples given by Andreas Rossberg that are (simplified forms) of trying to use type-based disambiguation for an AST built using the variant/record alternation pattern.

The following example warns when arguably it should not:

type 'a w = {a : 'a}

type t = t' w
and t' = {l : int}

type u = u' w
and u' = {l : int}

let f (x : u) = let {l; _} = x.a in l

File "warn-41.ml", line 9, characters 20-26 ("{l; _} ="):
Warning 41: these field labels belong to several types: u' t'
The first one was selected. Please disambiguate if this is wrong.

The issue here is that while (x.a) is known to be of type u (for example, "let a = x.a in a.l" does not warn), there is no information flowing from the let-defining expression to the let-pattern, so the let-pattern is type-checked without this information available.

For non-recursive let bindings, it should be possible to type-check the let-defining expression, and flow the inferred information into the let-pattern, to accept this example without a warning. Would such a strengthening be reasonable?

(It's a bit irritating to have two different type-inference paths for recursive and non-recursive binding, while we currently have a regular implementation for both. But if it comes with a usability win for a reasonable usage pattern...)

Additional information

The type-checker type-checks the left-hand-side (lhs) of the let-binding before the right-hand-side (rhs), and furthermore flows information from the lhs-check to the rhs-check in the form of an updated typing environment:

https://github.com/ocaml/ocaml/blob/2da2fcd/typing/typecore.ml#L2059-L2075

  | Pexp_let(rec_flag, spat_sexp_list, sbody) ->
    [...]
    let (pat_exp_list, new_env, unpacks) =
      type_let env rec_flag spat_sexp_list scp true in
    let body =
      type_expect new_env (wrap_unpacks sbody unpacks) ty_expected in
    [...]

This is necessary for recursive declarations as the pattern-bound variables may be used in the let-defining expression. But I don't see why that would be necessary for non-recursive declarations. (Of course in the function form "let f p1 p2 ... = e" you need to type-check the pi before e.)

Note that there is an equivalent way to write the same code using "match", where the typing information flow is as expected:

let f (x : u) = match x.a with {l; _} -> l

However, this code pattern is a bit unnatural, and as Andreas writes (thinking of non-expert OCaml programmers), "it's unlikely that anybody will understand why they should be doing that".