`singlet` and `Mu` do not work on higher kinded types.

[brandonzstride]

The definitions of singlet and Mu can only work on types that do not have a parameter. This is not a bug, but it's a limitation in the definitions.

A parametrized type is a function on types, and a function is not a type. Hence the e in singlet e and Mu t. e cannot be a parametrized/higher-kinded type. It must only be an expression that evaluates to a type.

Here are practical cases for wanting them to work with parametrized types.

let F : (S : sig val t : type -> type end) -> (sig val t : singlet S.t end) =
  fun S -> struct
    let t = S.t
  end

This is more readable (to me) as the following.

let F : (S : sig val t : type -> type end) -> (sig val t = S.t end) =
  fun S -> struct
    let t = S.t
  end

Any parametrized recursive type must be written as a recursive function, which works just fine but messes with some heuristics we use for performance.

let rec t a = e

... might be better written as ...

let t = Mu t a. e

or

let t = Mu t. fun a -> e

if possible. I think this is similarly as difficult to fix as the singlet issue.

[brandonzstride]

We can get singlet to work on higher kinded types if we declare the number of parameters. Consider the following way to show that two higher kinded types are equivalent.

(*
  Here is how we assert that X.t is the returned t
*)
let F : (X : sig val t : type --> type end) -> sig
  val t : (a : type) -> singlet (X.t a)
end = fun X -> struct
  let t = X.t
end

(*
  This is saying that Y.t = X.t, and we check that it is still type --> type.
*)
let F : (X : sig val t : type --> type end) -> (Y : sig val t : (a : type) -> singlet (X.t a) end) -> sig
  val t : type --> type
end = fun X Y -> struct
  let t = Y.t
end

Deterministic functions are necessary because of the application (X.t a). It doesn't make sense to use type -> type anywhere here in place of type --> type, but because singlet (X.t a) has one member, we don't need determinism in the (a : type) -> singlet (X.t a) part. A function to a type with one member is always deterministic, but maybe there is some edge case I'm not thinking about.

A proposed sugar for the first functor above is the following.

let F : (X : sig val t : type --> type end) -> sig
  val t : singlet1 X.t (* for one type parameter)
end = fun X -> struct
  let t = X.t
end

[brandonzstride]

The commit 030dbda that references this issue only solves the mu part with syntax like follows.

let t = mu t a.
  | `Nil of unit
  | `Cons of { hd : a ; tl : t a }

That is, the first identifier following mu is bound to the body and is parametrized by the remaining (potentially nonexistent) identifiers.