Hello,

The problem I’m about to describe initially arose using Ocsigen with some pretty large polymorphic variant types. I tried to simplify the problem as much as possible, but please keep in mind that a solution like “change your types” is not relevant for me

Consider the following source code:

```
type u1 = [ `A | `B ]
type u2 = [ `A | `B | `C ]
let p1 = function `T (`A) | `T (`B) -> ()
let p2 = function `T (`A) | `T (`B) | `T (`C) -> ()
let p3 = function `T (`A) | `T (`B) | `T (`C) | `U -> ()
let f h =
p1 (h :> [ `T of u1 ]);
p2 (h :> [ `T of u2 ]);
p3 (h :> [ `T of u2 | `U ])
```

When asking OCaml to infer its type (`ocamlc -i mnwe.ml`

), I get:

```
type u1 = [ `A | `B ]
type u2 = [ `A | `B | `C ]
val p1 : [< `T of [< `A | `B ] ] -> unit
val p2 : [< `T of [< `A | `B | `C ] ] -> unit
val p3 : [< `T of [< `A | `B | `C ] | `U ] -> unit
val f : [< `T of [< u2 ] & [< u2 ] & [< u1 ] ] -> unit
```

So far so good, just note how weird the type of `f`

is, specifying twice that `T`

(I don’t know how to typeset “acute T” in code on this forum ) should contain a subtype of `u2`

.

The problem is if I want to add an mli interface to that implementation.

Here are two interfaces. The first will compile (it is a subset of the interface inferred by OCaml, so its no surprise), but is ugly in my opinion, especially with larger types. The second won’t compile, while it seems obvious that it is the same.

First interface (working):

```
type u1 = [ `A | `B ]
type u2 = [ `A | `B | `C ]
val f : [< `T of [< u2] & [< u2] & [< u1] ] -> unit
```

Second interface (not working): It is forbidden to remove duplicates in the conjunction.

```
type u1 = [ `A | `B ]
type u2 = [ `A | `B | `C ]
val f : [< `T of [< u2] & [< u1] ] -> unit
```

The example won’t compile either with the following interface.

Third interface (not working): It is forbidden to change the order of conjuncts in the conjunction. This is true even when adapting the example to use only p1 and p2.

```
type u1 = [ `A | `B ]
type u2 = [ `A | `B | `C ]
val f : [< `T of [< u2] & [< u1] & [< u2] ] -> unit
```

I tried to force the type of the `h`

parameter in the `f`

function, but the inferred type just got even more bloated:

```
let f (h : [< `T of [< u2] & [< u1] ]) =
p1 (h :> [ `T of u1 ]);
p2 (h :> [ `T of u2 ]);
p3 (h :> [ `T of u2 | `U ])
val f : [< `T of [< u2] & [< u1] & [< u1] & [< u2] & [< u2] -> unit
```

I am using OCaml 4.03.0.

So the questions are : Is there some trick that would allow me to have beautiful interfaces? Should this be considered a bug and should I fill a bug report? Am I too much of a newbie to fiddle with such advanced constructions of the language?

Have a nice day!

Fabian Pijcke