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 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 > -- Caml-list mailing list. Subscription management and archives: https://sympa.inria.fr/sympa/arc/caml-list https://inbox.ocaml.org/caml-list Forum: https://discuss.ocaml.org/ Bug reports: http://caml.inria.fr/bin/caml-bugs