Unifying GADTs with polymorphic variant constraints

Learning
1

Let’s say I have some GADT with polymorphic variant constraints:

type 'a t = 
  | Foo : [ `foo ] t
  | Bar : [ `bar ] t
  | Baz : [ `baz ] t

I want to write a function that only is valid over [< `foo | `bar ] t.

Attempt #1:
The naive approach.

let f = function
  | Foo -> "foo"
  | Bar -> "bar"

Here the compiler complains that Bar is not of type [ `foo ] t and so it fails to compile.

Attempt #2:
Locally abstract types.

let f (type a) : a t -> string = function
  | Foo -> "foo"
  | Bar -> "bar"

This compiles, but with the expected warning that the match is not exhaustive, since our function is supposed to be defined over all 'a t

Is it possible to define a constrained locally abstract type such that externally f accepts [< `foo | `bar ] t but internally a is abstract?

2 Likes
2

Ahh, yes, I’ve run into this problem myself as well.

I’m not sure if this is the best solution, because it requires explicitly having extra cases in your definition, but if what you care about is the resulting type, then this does fit the criterion:

let f: ([< `foo | `bar ] as 'a) t -> string = fun (type a) (vl: a t) ->
  match vl with
  | Foo -> "foo"
  | Bar -> "bar"
  | _ -> failwith "unsupported"

I’d be curious to know if there is a good/better way to solve it.

2 Likes
3 
# type 'a t =
    | Foo : [> `foo ] t
    | Bar : [> `bar ] t
    | Baz : [> `baz ] t ;;

# let f : [< `foo | `bar ] t -> string = function
    | Foo -> "foo"
    | Bar -> "bar" ;;
val f : [ `bar | `foo ] t -> string = <fun>

# f Foo ;;
- : string = "foo"
# f Bar ;;
- : string = "bar"
# f Baz ;;
Error: This expression has type [> `baz ] t
       but an expression was expected of type [ `bar | `foo ] t
       The second variant type does not allow tag(s) `baz
6 Likes
4

This approach works too. It allows you to keep the Foo, etc., constructors monomorphic. The foo_bar type is an implementation detail of f and can be hidden behind a module type.

type 'a t = 
  | Foo : [ `foo ] t
  | Bar : [ `bar ] t
  | Baz : [ `baz ] t

type foo_bar = Foo_bar : [< `foo | `bar ] t -> foo_bar

let f x =
  let Foo_bar x = Foo_bar x in
  match x with
  | Foo -> "foo"
  | Bar -> "bar"

(* val f : [< `bar | `foo ] t -> string = <fun> *)
3 Likes
5

Ah thanks @art-w! This made me realize that polymorphic variants are inferred to be open in pattern matching. If I force them to be closed, i.e.

let f = function
  | (`x : [ `x ]) -> 1
  | `y -> 2

this also doesn’t work. So it’s not really a quirk with polymorphic variants and GADTs as much as it is a part of the type system I was unaware of.