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.
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:
We get application to a non-function.
The simple fix should be to let recursive type stubs accept and hold onto parameters.