What about the following structure?
type ('data, 'kind) t
type array_kind
type stack_kind
(* use tuples as type-level lists:
(a * (b * (c * unit))) for the stack of type-shape [a;b;c] *)
val newstate : unit -> (unit, stack) t
val getglobal : (unit, stack) t -> (top * unit, stack) t
val objlen : (top * 'a, 'k) t -> int
This uses polymorphism (on 'k
) to express that "any kind is
fine". Using polymorphic variants, it is possible to use subtyping
instead, but I would rather advise against it, because it is more
complex and its interaction with GADTs (which you want to use
internally to implement your phantom-types signature, or maybe
directly expose GADTs) is more problematic.
PS: this is exactly how the standard Bigarray module uses "kind types" for a similar purpose.
Edit: the formulation above is a bit awkward as polymorphic variant also use polymorphism (subtyping being used in restricted specific cases), and it's possible to only use polymorphism in type-level variants. My remark about excessive complexity of this solution still stands.