Hi, I have a problem with this test-case which doesn't compile: module M : sig type a = [`A] type 'a b = [`B of 'a] val a : unit -> a val b : 'a -> 'a b end = struct type a = [`A] type 'a b = [`B of 'a ] let a () = `A let b x = `B x end;; let rec f = function `B x -> f x | `A -> ();; f (M.b (M.a ()));; and produce the following error: Error: This expression has type M.a M.b = [ `B of M.a ] but an expression was expected of type [< `B of 'a ] as 'a Type M.a = [ `A ] is not compatible with type M.a M.b = [ `B of M.a ] These two variant types have no intersection The thing is, if we define M.a and M.b with « unit -> [> a ] » and « 'a -> [> 'a b ] », it does compile but I don't know why the previous code doesn't. Does somebody have any hints ?