Type refinement in polymorphic variant matches

The following code using GADTs works:

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 any because:

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;;

Unfortunately, I’m trying to do this in a context where t is abstract. I.e., I want to normally avoid having users combine arbitrary kinds and data.

Oddly, this works:

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.

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.

I would say it’s necessary, think about what your matches would look like if you had type 'k t = { kind : 'k; other_kind : 'k }.

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.