Why can't I add type constraints when implementing a module type?

Question

I was trying (just out of interest) to do this:

module type CAT = sig
  type ('a, 'b) t
  val id : ('a, 'a) t
  val (@) : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t
end

module Lst = struct
  type ('a, 'b) t = 'a list constraint 'a = 'b
  let id = []
  let (@) = (@)
end

module L : CAT = Lst (* (error) *)

But I get:

   Type declarations do not match:
     type ('b, 'a) t = 'b list constraint 'a = 'b
   is not included in
     type ('a, 'b) t

Why isn't this safe? Everything that can see the concrete type can also see the constraint, so I don't think you could make something with a wrong type (e.g. call @ with a (string, int) t argument).

---

Update: to those saying that my module doesn't implement the signature because it requires the types to be the same, consider that the following (which just wraps the lists in a List variant) is accepted despite having the same behaviour:

module Lst = struct
  type ('a, 'b) t =
    List : 'a list  -> ('a, 'a) t

  let id = List []
  let (@) (type a) (type b) (type c) (a:(b, c) t) (b:(a, b) t) : (a, c) t =
    match a, b with
    | List a, List b -> List (a @ b)
end

Answer 1

The example can be reduced to the type definition alone:

module type S =
sig
  type ('a, 'b) t
end

module M =
struct
  type ('a, 'b) t = 'a list constraint 'a = 'b
end

As Jeffrey already pointed out, M is not of type S, because it allows fewer applications of t: according to signature S, the type (int, string) t would be perfectly legal (it is well-formed), but M does not allow this type ((int, string) M.t is not a legal type, because it violates the explicit constraint).

All that is completely independent from the question whether the type is actually inhabited, i.e., whether you can construct values of the type. In your second example, the module makes the respective type well-formed, though it is uninhabited. Uninhabited types are legal, however, and sometimes even useful (see e.g. the concept of phantom types).

Answer 2

The type signature CAT is more general than the type of the Lst module. You need to put the type constraint on the abstract type too, i.e. type ('a, 'b) t constraint 'a = 'b.

This gives us the following:

module type CAT = sig
  type ('a, 'b) t constraint 'a = 'b
  val id : ('a, 'a) t
  val (@) : ('b, 'c) t -> ('a, 'b) t -> ('a, 'c) t
end

which is printed as follows by the toplevel, showing a single type variable in the signature of (@):

module type CAT = 
  sig
    type ('b, 'a) t constraint 'a = 'b                                          
    val id : ('a, 'a) t
    val ( @ ) : ('c, 'c) t -> ('c, 'c) t -> ('c, 'c) t
  end

Error messages of the form "type x is not included in type y" refer to types or module types as specifications of sets of possible values, hence the use of the term "included".

In the case of a module implementation (Lst), we have a module type for it. Applying a signature (module type CAT) to a module is only allowed if that signature is as specialized (equal set) or more specialized (strict subset) than the original signature of the module.

One can write module X : sig val f : unit -> unit end = struct let f x = x end but not module X : sig val f : 'a -> 'a end = struct let f () = () end. The latter gives the following error:

Error: Signature mismatch:
       Modules do not match:
       sig val f : unit -> unit end                                           
       is not included in
         sig val f : 'a -> 'a end
       Values do not match:
         val f : unit -> unit
       is not included in
         val f : 'a -> 'a

This is different than placing type constraints on certain expressions, in which case the constraint is a mask to be applied (a set to intersect with) rather than a subset. For example it is fine to write let f : unit -> 'a = fun x -> x even though f's signature ends up being unit -> unit, a strict subset - or subtype - of unit -> 'a.