When type splaying, generation of recursive types is stubbed with an unusable value. However, in the presence of parametric recursive types, the mu type is actually a type function, and this encoding fails.
For example:
let t = mu t a.
| `Nil of unit
| `Cons of { hd : a ; tl : t a }
let rec length (type a) (ls : t a) : int =
match ls with
| `Nil _ -> 0
| `Cons r -> 1 + length a r.tl
end
We get application to a non-function.
The simple fix should be to let recursive type stubs accept and hold onto parameters.