Provide a constrained type as an implementation for an abstract type

Learning
1

Hello,
I am a bit confused…
I would like to use a constrained type for an abstract type (for example to instantiate a functor),
like in the following.

module type S =
  sig
    type 'a t
  end

module I =
  struct
    type 'a t = [< `A | `B] as 'a
  end

module I' =
  struct
    type 'a t = 'a
  end

module I_ok = (I' : S)
module I_error = (I : S);;

But I get for the line I_error (in utop with OCaml 4.05.0):

Error: Signature mismatch:
       Modules do not match:
         sig type 'a t = 'a constraint 'a = [< `A | `B ] end
       is not included in
         S
       Type declarations do not match:
         type 'a t = 'a constraint 'a = [< `A | `B ]
       is not included in
         type 'a t
       Their constraints differ.

which I don’t really understand.

Thank you for your help,

2

The problem is that

module type C = sig type 'a t constraint 'a = [< `A ] end

is not a subtype of

module type U = sig type 'a t end

This is easier to see with this simple functor

module F(X:U) = struct type x = float X.t end

This functor create a new valid module for any module X that implements the U signature. However, we cannot give it as argument a module M of type C because it would be break the constraint that the type constructor M.t can only be applied to types of the form [<`A].

This is why you cannot use a constrained type constructor in place of an unconstrained one.

3

Oh yes thank you ! It seems a lot more obvious this way.
I guess I am very often confused about the subtyping relation…