Adding expressiveness to polymorphic variants

[vicuna]

Original bug ID: 5924
Reporter: jpdeplaix
Assigned to: @garrigue
Status: closed (set by @xavierleroy on 2015-12-11T18:18:30Z)
Resolution: won't fix
Priority: normal
Severity: minor
Version: 4.00.1
Category: typing

Bug description

Hi,

I'd like to be able to do the kind of functions described here:
http://caml.inria.fr/pub/docs/manual-ocaml/manual006.html

This function:
let f = function A -> C | B -> D | x -> x
is typed as:
val f : ([> A | B | C | D ] as 'a) -> 'a
but a more fine type would be:
val f : [ A | B | 'r ] -> [ C | D | 'r ]

gasche already told me that it is choice made by the caml developers, but I'm very interested in making such functions. So, if someone can add this expressiveness to the language or explain me why it is really not possible to add this, it would be very helpful.

[vicuna]

Comment author: @garrigue

This is not strictly impossible to do that, but this requires huge changes in the type system.

• since we would have explicit row variables, you need to introduce a notion of type variable sort

• one would need to add exclusion information on row variables. For instance, with your example,
  we would the information that 'r cannot contain any of A, B, C, D. This is implicit in the type
  of f, but it can become hidden in more complex functions, so it would have to be explicit.

• typing of pattern-matching would have to compute remaining cases, which is not trivial in the general case.

For all these reasons there is no plan to introduce something like that at this point.

If you are interested in this subject, you can read papers by Didier Rémy and, more recently, Matthias Blume.