Question about typing polymorphic variants

Learning
1

I’m not sure why the following code fails to type check:

module M : sig
  type a = [`A]
  val v : [> a]
end = struct
  type a = [`A]
  type b = B of a
  let v = match B `A with B x -> x
end

Error: Signature mismatch:
   Modules do not match:
     sig type a = [ `A ] type b = B of a val v : a end
   is not included in
     sig type a = [ `A ] val v : [> a ] end
   Values do not match: val v : a is not included in val v : [> a ]

Changing B x to B (#a as x) solves the problem, but I can’t figure out why the annotation should help. Could anyone explain what the type checker is doing here?

2

It’s because the pattern B x types x as (exactly) a. It’s the same as if you were to write:

let a: a = `A
let v = a