If the type variable ident actually occurs in typexpr, a recursive type is created. Recursive types for which there exists a recursive path that does not contain an object or polymorphic variant type constructor are rejected, except when the -rectypes mode is selected.

Adding more confusion… Is an error expected when the second type keyword is replaced by and?

# type 'a r = [`R of 'a] type 'a t = 'a r as 'a ;;
type 'a r = [ `R of 'a ]
type 'a t = 'a constraint 'a = 'a r
# type 'a r = [`R of 'a] and 'a t = 'a r as 'a ;;
Error: The definition of t contains a cycle:
'a r as 'a

type 'a rw = [`R of 'a]
type r = (int -> 'a rw) as 'a

I think that the first line is not a type definition, but a type alias (like type t = int). So in the second line, this alias is expanded to the following, which contains a cycle.

Consider the translation of your ADT definition to a polymorphic variant:

type tree = [ `Leaf of int | `Node of 'tree * 'tree ] as 'tree

The recursive ADT definition leads to a recursive polymorphic variant type expressions. Thus if we want polymorphic variants to be as expressive as regular variants we need to allow recursive polymorphic variant types.

This works too, it is another way to write the same recursive type expression.

This is not well typed: aliases like _ as 'x works on type expression.

| Leaf of int
| Node of ...

is a type definition not an expression. Such type definition introduces a fresh type name which gives us an easy way to define recursion by going through this new name. In particular, recursion can only be achieved by expanding the new mutually recursive types. Recursive type expressions can be more unwieldy:

let f (`X x: [ `X of [`Y of 'b * 'a | `Z ] as 'b] as 'a) = x

Indeed polymorphic variants are structural types (aka type expressions), thus a recursive function like

let rec proj x = match x with
| `Leaf leaf -> leaf
| `Node (left,_) -> proj left

needs to be able to decide that the type of x and the type of left are the same. Thus the type system needs to be able to handle equations inside the type expressions. Contrarily with a nominal variant, it is the type definition itself that introduces the type equations

type tree =
| Leaf of int
| Node of tree * tree

and we know in advance that those equations only needs to be used when building or deconstructing a value of type tree. (And since the recursion is more constrained, type definions can handle non-regular recursive types like

type 'a balanced =
| Leaf of 'a
| Node of ('a * 'a) balanced