GADTs and polymorphic variants (once again)

Learning
1

I recently wrote the following piece of code:

type _ t =
  | Block : { field : int } -> [< `B | `I > `B] t
  | Empty : [ `B | `I ] t

let narrow (x : [ `B | `I ] t) : [ `B ] t option =
  match x with
  | Block _ as y -> Some y
  | Empty -> None

fully expecting it not to work (my previous forays into combining GADTs and polymorphic variants have never been successful). But to my surprise this is accepted by the typer without issues.

Of course if I actually use the variable in Block then this is properly rejected:

type _ t =
  | Block : { field : [< `B | `I > `B] as 'a } -> 'a t
  | Empty : [< `B | `I > `I] t

let narrow (x : [ `B | `I ] t) : [ `B ] t option =
  match x with
  | Block _ as y -> Some y
  | Empty -> None

$ ocaml file.ml
File "file.ml", line 7, characters 25-26:
7 |   | Block _ as y -> Some y
                             ^
Error: This expression has type [ `B | `I ] t
       but an expression was expected of type [ `B ] t
       The second variant type does not allow tag(s) `I

Given the error message, I assume that in the first example, the type of y is a fresh variable of type [< `B | `I > `B], but I don’t really understand why it is OK for that variable to unify with [ `B ] at toplevel.

The following is also accepted:

type _ t =
  | K : int -> [> ] t

let transmute (x : [ `A ] t) : [ `B ] t =
  match x with K _ as y -> y

On one hand, I am quite happy this works (I tested both of these using OCaml 5.1.1 and the alpha release of OCaml 5.3), because it seems useful. On the other hand, after discussing with @vlaviron, we are not quite sure whether this is intended behavior.

I know the interactions between GADTs and polymorphic variants are not very well understood; so I am wondering if a type system wizard could shine some light on what’s happening here. I am both interested in knowing whether this is sound and can be relied upon, and on the type-theoretic reasons for why it is so.

2

I don’t see any interaction with GADT here. For instance, rewriting your example as

module M = struct
  type 'a t = A of int | B
end
open M
let narrow (x : [ `B | `I ] t) : [ `B ] t option =
  match x with
  | A _ as y -> Some y
  | B -> None

let transmute (x : [ `A ] t) : [ `B ] t =
  match x with A _ as y -> y | B as y -> y

works too. What happens is that an as pattern is typed as it would be typed if the bound constructors were inlined on the expression side. The behavior might be even more visible with the following example:

type void = |
let transmute: void list -> int list = function [] as x -> x
1 Like
3

Ah! I briefly considered it but I (incorrectly) assumed it to be too magical and discarded the possibility. That explains it, thanks!