module GADT = struct
module Kind = struct
type 'k t =
| A : [ `A ] t
| B : [ `B ] t
| C : [ `C ] t
end
type 'k t =
{ kind : 'k Kind.t
; data : string
}
let only_a_or_b (_ : [< `A | `B ] t) = ()
let any (type k) (t : k t) =
match t.kind with
| A -> only_a_or_b t
| B -> only_a_or_b t
| C -> ()
;;
end

only_a_or_b will only accept an [`A] t or a [`B] t, but we can call it from anybecause:

The constraints associated to each constructor can be recovered through pattern-matching. Namely, if the type of the scrutinee of a pattern-matching contains a locally abstract type, this type can be refined according to the constructor used.

The following is similar in intention, but we don’t get the same kind of type refinement, so it won’t compile:

module Polymorphic_variant = struct
module Kind = struct
type t =
[ `A
| `B
| `C
]
end
type 'k t =
{ kind : 'k
; data : string
}
let only_a_or_b (_ : [< `A | `B ] t) = ()
let any_exn (t : Kind.t t) =
match t.kind with
| `A | `B -> only_a_or_b t
| `C -> ()
;;
end

The specific error looks like this:

File "src/v2.ml", line 180, characters 29-30:
180 | | `A | `B -> only_a_or_b t
^
Error: This expression has type Kind.t t
but an expression was expected of type ([< `A | `B ] as 'a) t
Type Kind.t = [ `A | `B | `C ] is not compatible with type
[< `A | `B ] as 'a
The first variant type does not allow tag(s) `C

Is there any way to get this rough idea to work using polymorphic variants?

Hi,
You can use a pattern alias to refine the type, so this works,
but I don’t know if that is good enough

module Polymorphic_variant = struct
module Kind = struct
type t =
[ `A
| `B
| `C
]
end
type 'k t =
{ kind : 'k
; data : string
}
let only_a_or_b (kind : [< `A | `B ]) data = ()
let any_exn (t : Kind.t t) =
match t.kind with
| (`A | `B) as k -> only_a_or_b k t.data
| `C -> ()
end;;

module Polymorphic_variant = struct
module Kind = struct
type t = [ `A | `B | `C ]
end
module T = struct
type 'k t = { kind : 'k; data : string }
end
let only_a_or_b (_ : [< `A | `B ] T.t) = ()
let any_exn (t : Kind.t T.t) =
match t with
| { kind = `A | `B; _ } as x -> only_a_or_b x
| { kind = `C; _ } -> ()
end

But as soon as you make T.t private, it breaks. So, no luck there.

I’m not sure if this is a necessary restriction or if it’s just a place where the type checker could be made more general.

If you have two kind fields, you definitely need to match on both to refine the type, but I don’t see why private types make this case more problematic.

For example, this works:

module Polymorphic_variant2 = struct
module Kind = struct
type t = [ `A | `B | `C ]
end
module T = struct
type 'k t = { kind1 : 'k; kind2 : 'k }
end
let only_a_or_b (_ : [< `A | `B ] T.t) = ()
let any_exn (t : Kind.t T.t) =
match t with
| { kind1 = `A | `B; kind2 = `B } as x -> only_a_or_b x
| _ -> ()
end

but this doesn’t:

module Polymorphic_variant2 = struct
module Kind = struct
type t = [ `A | `B | `C ]
end
module T = struct
type 'k t = private { kind1 : 'k; kind2 : 'k }
end
let only_a_or_b (_ : [< `A | `B ] T.t) = ()
let any_exn (t : Kind.t T.t) =
match t with
| { kind1 = `A | `B; kind2 = `B } as x -> only_a_or_b x
| _ -> ()
end

I’m pretty sure that any solution involving abstract types won’t work, but I don’t quite get why private types don’t.