Original bug ID: 6952
Reporter: @c-cube
Status: acknowledged (set by @damiendoligez on 2015-11-27T14:51:25Z)
Resolution: open
Priority: normal
Severity: feature
Category: typing
Monitored by: @thizanne @Drup @diml @yallop @hcarty

Bug description

I hope this is not a duplicate of some old question or ML thread on the same topic. I apologize if it is the case. I am not a type theory expert, so the question might be stupid.

As far as I know, OCaml uses row variables internally to support inference on objects and polymorphic variants. However, this is hidden from the user (except for the object type notation <a: t; b: u; ..>).

I think several people would very much like to have access to this row variable with a type variable, both for objects and poly variants, as in (roughly):

val hide_foo : <foo: 'a; .. as 'r> -> < 'r >
val hide_foo' : [`Foo | .. as 'r] -> [>'r]

My guess is that 'r would not be a regular type variable, which would require a kind system or something similar?

Furthermore, if row variables were actually first-class, I think it would be very interesting to have "extensible tuples", such as 1, "foo", .. of type int * string * .. as 'r. If it were the case, some functions could be generalized, such as fst : 'a * .. -> 'a, snd : 'a * 'b * .. -> 'b, map_fst : ('a -> 'b) -> 'a * .. as 'r -> 'b * 'r, etc.