Type definition contains a cycle?

While the type checker does not expand Either.t, it does not treat it as abstract either. As mentioned by others, it knows that Either.t constructs a value, and as a result your type definition is allowed in -rectypes modes, which is of course sound (i.e., -rectypes is not unsafe).

So why is your definition refused by default?
This is mainly because allowing it makes type inference less useful at detecting mistakes.
Here is an example using -rectypes:

# let rec append l1 l2 = match l1 with [] -> l2 | a::l -> a :: append a l2;;
val append : ('a list as 'a) -> 'a list -> 'a list = <fun>

About 20 years ago OCaml used to have -rectypes as default for some time, but it was eventually decided the confusion caused by accepting such definitions was not worth the added expressive power.

Note that the trade-off is different for polymorphic variants and objects. There, recursion is allowed as long as it goes through either a polymorphic variant or object type.

# let rec append l1 l2 = match l1 with `Nil -> l2 | `Cons (a,l) -> `Cons (a, append l l2);;
val append :
  ([< `Cons of 'b * 'a | `Nil ] as 'a) -> ([> `Cons of 'b * 'c ] as 'c) -> 'c =
  <fun>

So you could actually write your code by defining Either.t as:

type ('a,'b) either = [`Left of 'a | `Right of 'b]

Note that inferring such equi-recursive types (as mentioned by @octhacron) also comes with some restrictions on the form of recursion allowed (only regular types are allowed, which is weaker than for explicit type definitions). But this is another story (while there does exist a stronger algorithm, it is extremely complex).

4 Likes