Parameterized GADT type witnesses

Learning
, ,
1

My compiler’s AST is initially annotated with location but I dislike how location shows up in my expect tests. I’d like to strip location before testing, e.g. by replacing location with unit. This requires that my AST be parameterized on the type of annotation. For example,

...
and Output : sig
  type 'n t =
    | Text : string -> 'n t
    | Register : 'n Register.t -> 'n t
    | Register_index : 'n Register_index.t -> 'n t
    | Bit_field : 'n Bit_field.t -> 'n t
    | Scanner : 'n Scanner.t -> 'n t
end =
  Output

and Type : sig
  type (_, 'n) t =
    | Register : ('n Register.t, _) t
    | Register_index : ('n Register_index.t, _) t
    | Bit_field : ('n Bit_field.t, _) t
    | Macro : ('n Macro.t, _) t
    | Memory_region : ('n Memory_region.t, _) t
    | Pcode_op : ('n Pcode_op.t, _) t
    | Scanner : ('n Scanner.t, _) t
  [@@deriving sexp]
end =
  Type

My type environment works when not parameterized but when I try to parameterize it on the type of annotation, like this

module Type_env = struct
  type 'n t =
    | Nil
    | Cons : string * ('a, 'n) Type.t * 'a * 'n t -> 'n t

  type ('a, 'b, 'na, 'nb) eq = Refl : ('a, 'a, 'na, 'na) eq

  let make () = Nil

  let types_equal
    : type a b na nb.
      (a, na) Type.t -> (b, nb) Type.t -> (a, b, na, nb) eq option
    =
    fun a b ->
    let open Type in
    match a, b with
    | Register, Register -> Some Refl
    | Register_index, Register_index -> Some Refl
    | Bit_field, Bit_field -> Some Refl
    | Macro, Macro -> Some Refl
    | Memory_region, Memory_region -> Some Refl
    | _, _ -> None
  ;;

I get an error

Error: This expression has type (a, a, 'a, 'a) eq
       but an expression was expected of type (a, b, na, nb) eq
       Type a = $0 Register.t is not compatible with type b = $1 Register.t
       Type $0 is not compatible with type $1

Is it possible to do what I’m trying to do? How?

2

When you wrote

  type (_, 'n) t =
    | Register : ('n Register.t, _) t

did you expect the 2 'n to be the same? They are not.
Try writing

  type (_, _) t = (* or "type (_, 'n) t =", but since that 'n wouldn't be used _ is probably better *)
    | Register : ('n Register.t, 'n) t

instead.

3

Something is still off…

File "src/lib/ir.ml", line 240, characters 33-37:
240 |     | Register, Register -> Some Refl
                                       ^^^^
Error: This expression has type (a, a, 'a, 'a) eq
       but an expression was expected of type (a, b, $0, $1) eq
       Type a = $0 Register.t is not compatible with type b = $1 Register.t
       Type $0 is not compatible with type $1

for

and Type : sig
  type (_, _) t =
    | Register : ('n Register.t, 'n) t
    | Register_index : ('n Register_index.t, 'n) t
    | Bit_field : ('n Bit_field.t, 'n) t
    | Macro : ('n Macro.t, 'n) t
    | Memory_region : ('n Memory_region.t, 'n) t
    | Pcode_op : ('n Pcode_op.t, 'n) t
    | Scanner : ('n Scanner.t, 'n) t
  [@@deriving sexp]
end =
  Type

module Type_env = struct
  type 'n t =
    | Nil
    | Cons : string * ('a, 'n) Type.t * 'a * 'n t -> 'n t

  type ('a, 'b, 'na, 'nb) eq = Refl : ('a, 'a, 'na, 'na) eq

  let make () = Nil

  let types_equal
    : type a b na nb.
      (a, na) Type.t -> (b, nb) Type.t -> (a, b, na, nb) eq option
    =
    fun a b ->
    let open Type in
    match a, b with
    | Register, Register -> Some Refl
    | Register_index, Register_index -> Some Refl
    | Bit_field, Bit_field -> Some Refl
    | Macro, Macro -> Some Refl
    | Memory_region, Memory_region -> Some Refl
    | _, _ -> None
  ;;
4

There’s nothing making the annotation types of 2 Register equal is there?
Restricting types_equal to equal annotation types may work (types_equal: type a b n. (a, n) Type.t -> (b, n) Type.t -> (a, b, n, n) eq option)

5

When I’ve dealt with this exact problem before, I simply wrote my location’s pp function to output nothing, which works perfectly Dune’s built-in expect tests.

I’m not sure how flexible other expect-test runners are in this regard, but maybe a similar technique will work.

1 Like
6

It works perfectly, thank you very much!

7

Thanks! I envision being able to replace the annotations from position to type, or a combination of both, as I translate between trees so the parameterized approach works best for me.