gadt.ml

type _ t =
  | Bar : 'a -> 'a t
  | Foo : 'a list t -> 'a t

let rec f : type a. a t -> a = function
  | Bar y -> y
  | Foo y ->
    begin match f y with
      | [] -> assert false
      | h :: r -> h
    end

let rec f (type a) (x: a t) : a =
  match x with
  | Bar y -> y
  | Foo y ->
    begin match f y with
      | [] -> assert false
      | h :: r -> h
    end
(*
File "gadt.ml", line 17, characters 18-19:
10 |     begin match f y with
                       ^
Error: This expression has type a list t
       but an expression was expected of type 'a
       The type constructor a would escape its scope
*)