Your function g is incorrect; in the None case, it claims that the constructor A has the type (a t) for an unknown (arbitrary) type parameter (a). A only has the type (a t) for a specific type (a = [`A]), not for all types.
If you want g to be able to return a value of type (a t) for *some* type (a) that g chooses, instead of for *any* type (a) chosen by the context/caller, then you should use an existential type wrapping:

  type any_t = Any : a t -> any_t.

  [...]
  | Some A -> Any A
  | Some B -> Any B
  | None -> Any A

On Thu, Jan 17, 2019 at 11:02 AM Christopher Zimmermann <christopher@gmerlin.de> wrote:
On Thu, 17 Jan 2019 10:46:11 +0100
Christopher Zimmermann <christopher@gmerlin.de> wrote:

Hi,

why does the f type correctly while g fails to type?

Christopher

type 'a t =
  | A : unit t

let f =
  fun (type a) ~(p :a t option) () -> match p with
    | Some A -> ()
    | None -> ()

let g =
  fun (type a) ~(p :a t option) () -> match p with
    | Some A (* TYPING ERROR HERE *)
    | None -> ()

Error: This pattern matches values of type unit t
       but a pattern was expected which matches values of type a t
       Type unit is not compatible with type a



to add to the confusion, why does f type while g fails to type ?

type 'a t =
  | A : [`A] t
  | B : [`A|`B] t

let f =
  fun (type a) ~(p :a t) () -> match p with
    | A -> (A: a t)
    | B -> (B: a t)

let g =
  fun (type a) ~(p :a t option) () -> match p with
    | Some B -> (B: a t)
    | Some A -> (A: a t)
    | None -> (A (* TYPE ERROR HERE *) : a t)

Error: This expression has type [ `A ] t
       but an expression was expected of type a t
       Type [ `A ] is not compatible with type a

--
http://gmerlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2  0DEF 87E2 92A7 13E5 DEE1