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).