Original bug ID: 7388
Reporter: @gasche
Assigned to: @garrigue
Status: acknowledged (set by @shindere on 2017-02-24T15:11:15Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing
Related to: #7389
Child of: #7409

Bug description

Consider the following code example

type 'a w = {a : 'a}

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

type u = {l : int}

type c = C of t

let f (x : c) = match x with C y -> y.a.l

When "-principal -w 41" is enabled, we get a warning that the project ".l" is not principal. However, it seems principal to me, given that (x : c) non-ambiguously determines the type of x, from which the type of y can be deduced (in a principal way?), and thus (in a principal way?) the type of y.a.

Would it be possible to strengthen type-information flow, or the principality information, to accept this example?

Additional information

Andreas Rossberg gave a talk at the ML workshop with some experience reports of using OCaml for the WebAssembly reference interpreter. One of his complaints was on type-based record field disambiguation not working for his use-case, forcing him to use hugarian field prefixes. I asked for more details, and we are discussing various use-cases -- this one does look like a fixable issue to me. The design pattern that they use and that stresses type-based propagation is the alternating recursion of variants (for the AST) and a record (for location information, etc.).