Mapping GADT with Polymorphic Variant into a more restrictive form

Learning
, , , ,
2

It seems that you have a fundamental issue. The following term is accepted:

B (B (A, T "foo"), C (E, T "foo"))

However you cannot find any term t that could replace both occurrences of T "foo" (unless you use another T constructor).

If you expect that you won’t have to deal with such terms, you can re-type your terms during replacement. Here is something that seems to work for me:

type f = [ `f ]
type c = [ `c ]

type _ t =
  | A : f t
  | B : f t * f t -> f t
  | C : c t * c t -> f t
  | D : [< f | c] t * c t -> c t
  | E : c t
  | T : string -> [< f | c] t

type _ wit =
  | Wc : c wit
  | Wf : f wit

type t_with_wit =
  | Pack : 'a t * 'a wit -> t_with_wit

type env = (string * t_with_wit) list

exception Type_error

let rec replace : type a. env -> a t -> t_with_wit = fun env t ->
  match t with
  | A -> Pack (A, Wf)
  | B (x, y) ->
    let Pack (x, x_wit) = replace env x in
    let Pack (y, y_wit) = replace env y in
    begin match x_wit, y_wit with
      | Wf, Wf -> Pack (B (x, y), Wf)
      | _, _ -> raise Type_error
    end
  | C (x, y) ->
    let Pack (x, x_wit) = replace env x in
    let Pack (y, y_wit) = replace env y in
    begin match x_wit, y_wit with
      | Wc, Wc -> Pack (C (x, y), Wf)
      | _, _ -> raise Type_error
    end
  | D (x, y) ->
    let Pack (x, x_wit) = replace env x in
    let Pack (y, y_wit) = replace env y in
    begin match x_wit, y_wit with
      | Wc, Wc -> Pack (D (x, y), Wc)
      | Wf, Wc -> Pack (D (x, y), Wc)
      | _, Wf -> raise Type_error
    end
  | E -> Pack (E, Wc)
  | T s -> List.assoc s env

let expect_type : type a. a wit -> t_with_wit -> a t =
  fun wit t_wit ->
  match wit, t_wit with
  | Wc, Pack (t, Wc) -> t
  | Wf, Pack (t, Wf) -> t
  | _, _ -> raise Type_error

let replace_same_type : type a. env -> a t -> a t =
  fun env t ->
  match t with
  | A -> expect_type Wf (replace env t)
  | B (_, _) -> expect_type Wf (replace env t)
  | C (_, _) -> expect_type Wf (replace env t)
  | D (_, _) -> expect_type Wc (replace env t)
  | E -> expect_type Wc (replace env t)
  | T _ -> (* Cannot infer expected type *) raise Type_error

You will note that it’s not possible with my solution to use replace_same_type on terms of the form T _. This is because with such a term, you cannot know what the expected type was, so whatever term you replace it with, you cannot guarantee that it will have the same type. However, as long as the top constructor is not T, everything works.

I’ve tried a version where the constructor T carries a type witness, and it seems like it should work but fails because of what I see as limitations in the type inference of GADTs with polymorphic variants (it works if f and c are not polymorphic variants).
Here is the version that works, without polymorphic variants:

type f = private F
type c = private C

type _ wit =
  | Wc : c wit
  | Wf : f wit

type _ t =
  | A : f t
  | B : f t * f t -> f t
  | C : c t * c t -> f t
  | D : _ t * c t -> c t
  | E : c t
  | T : string * 'a wit -> 'a t

type t_with_wit =
  | Pack : 'a t * 'a wit -> t_with_wit

type env = (string * t_with_wit) list

exception Type_error

let rec replace : type a. env -> a t -> a t = fun env t ->
  match t with
  | A -> A
  | B (x, y) -> B (replace env x, replace env y)
  | C (x, y) -> C (replace env x, replace env y)
  | D (x, y) -> D (replace env x, replace env y)
  | E -> E
  | T (s, wit) ->
    let Pack (t, t_wit) = List.assoc s env in
    begin match wit, t_wit with
      | Wc, Wc -> t
      | Wf, Wf -> t
      | _, _ -> raise Type_error
    end
2 Likes