Support parameter constraints in module signature type equalities

[gasche]

Sometimes it is natural to consider two different interfaces for a data structure, one where the container type is parametrized, and one where it is monomorphic. I propose to let us instantiate the polymorphic signature into the monomorphic signature by using a type constraint to transform occurrences of the type parameter.

For example, if we have

module type Poly = sig
  type 'a t
  val return : 'a -> 'a t
  val map : ('a -> 'b) -> 'a t -> 'b t
end

then I propose to write

module type Mono = sig
  type elt
  type t
  include Poly with type 'a t := t constraint 'a = elt
end

and to have the type-checker understand this as the following signature:

module type Mono = sig
  type elt
  type t
  val return : elt -> t
  val map : (elt -> elt) -> t -> t
end

To apply the equation type 'a t = u constraint 'a = foo, for each occurrence of bar t in the signature, we unify foo with bar and apply the resulting substitution. We fail with an error if foo and bar are not unifiable, for example if we used int t in another item of the Poly signature above.

[gasche]

cc @garrigue : if this is unsound for a well-known reason, @garrigue would be aware of it.

[gasche]

Note: it is currently possible to derive both interfaces by introducing a signature that encapsulates the use of the type parameters.

module type Generic = sig
  type 'a t
  type 'a param
  val return : 'a param -> 'a t
  val map : ('a param -> 'b param) -> 'a t -> 'b t
end

module type Poly = Generic with type 'a param := 'a
module type Mono = sig
  type t
  type elt
  include Generic with type 'a t = t and type 'a param = elt
end

[garrigue]

That is an interesting proposal.
However, it requires an important amount of work to be implemented: basically, you need to both substitute the occurrences of t and unify its arguments. There is no code doing that in the type checker yet.
Since doing that also means that you have to re-check the coherence of all the types, I suppose that there is no soundness problem; it would have to be detected anyway.

If we want to do things like that, it probably means that we want a way to reason about types at a higher level, rather than just substitution and unification, that would be more amenable to this kinds of extra checks.