Modelling a grammar with GADT, but type parameter won't unify

Question

I thought that I've found a neat way to model grammars using GADTs by giving each constructor (e.g. Char) a return type parameter that is a polymorphic variant (e.g. [`Char] t) and then using polymorphic variant unification feature to restrict which constructors are allowed next (e.g. [<`Minus | `Char] t).

(* Grammar ::= Open (Minus? Char)+ Close *)

type _ t =
  | Open:  [<`Minus | `Char] t -> [`Open] t
  | Minus: [<`Char] t -> [`Minus] t
  | Char:  [<`Minus | `Char | `Close] t -> [`Char] t
  | Close: [`Close] t

This works as intended allowing only the sequences that fit the grammar:

let example =
  Open (Minus (Char (Char (Minus (Char (Close))))))

(* let counter_example =
  Open (Minus (Char (Minus (Minus (Char (Close)))))) *)

However, it seems impossible to write any trivial function for this type:

let rec to_list = function
  | Open rest -> "(" :: to_list rest
  | Minus rest -> "-" :: to_list rest
  | Char rest -> "a" :: to_list rest
  | Close -> [")"]

File "./tmp.ml", line 21, characters 4-14:
21 |   | Minus rest -> "-" :: to_list rest
         ^^^^^^^^^^
Error: This pattern matches values of type [ `Minus ] t
       but a pattern was expected which matches values of type [ `Open ] t
       Type [ `Minus ] is not compatible with type [ `Open ]

As far as I understand the polymorphic variants are not unified because GADTs type parameters cannot have variance. Does this mean that this approach is totally useless?

Answer 1

You just need to use a locally abstract type to be able to refine the type for each branch:

let rec to_list : type a. a t -> string list = function
  | Open rest -> "(" :: to_list rest
  | Minus rest -> "-" :: to_list rest
  | Char rest -> "a" :: to_list rest
  | Close -> [")"]

For explanation, @octachron wrote a great answer for this on a similar question earlier today.

Edit:

To restrict this function to a subset of the cases, I think you have to apply two different type signatures. One external signature for the polymorphic variant, and one internal for the locally abstract type. However, since the function is recursive we also need the locally abstract type to be external when we recurse on it. Otherwise we could have just annotated the value being pattern matched.

I can think of a couple of ways to do this:

Option 1, wrap it in a module (or put the external signature in the .mli):

module M : sig
  val to_list : [<`Minus | `Char | `Close] t -> string list
end = struct
  let rec to_list : type a. a t -> string list = function
    | Open rest -> "(" :: to_list rest
    | Minus rest -> "-" :: to_list rest
    | Char rest -> "a" :: to_list rest
    | Close -> [")"]
end

Option 2, use a locally defined function to put the "inner" signature on:

let to_list : [<`Minus | `Char | `Close] t -> string list =
  let rec aux : type a. a t -> string list = function
    | Open rest -> "(" :: aux rest
    | Minus rest -> "-" :: aux rest
    | Char rest -> "a" :: aux rest
    | Close -> [")"]
  in
  aux