Concretizing abstract types across multiple constructors with pattern matching

Learning
1

Sorry for the confusing title, I’m not quite sure how to describe what I’m looking for here.

Let’s say I have some trivial GADT t:

type 'a t =
  | A : int t
  | B : int t
  | C : float t

Using locally abstract types and pattern matching, I can take some abstract a t and narrow/concretize a based on the constructor. Here’s an example:

let f (type a) : a t -> a = function
  | A -> 1
  | B -> 1
  | C -> 2.

This works well, but ideally would be written more compactly as

let g (type a) : a t -> a = function
  | (A | B) -> 1
  | C -> 2.

However, this function doesn’t compile with the error:

Error: This expression has type int but an expression was expected of type a

(which refers to line 2 of the g block).

Is there any way to write this case such that a is narrowed to an int?

2 Likes
2

The short answer is no, not at the moment. You can find a bit more context here: Support GADTs in or-patterns · Issue #5736 · ocaml/ocaml · GitHub.
There are a number of related discussions that you can find by searching for GADTs and or-patterns. I believe that it’s still a long term goal of the type-checking team, but it is complicated to do it correctly.

To give you an example of the kind of issues you can get into:

type t1 = { b : int }
type t2 = { a : int; b : int }
type t =
| T1 : t1 -> t
| T2 : t2 -> t

let f = function
  | (T1 x | T2 x) -> x.b

Every branch would individually type-check, but there is no single way to compile x.b that would be correct for all branches.

2 Likes
3

Thanks @vlaviron!

I have a follow up question to your answer, though. The block you gave is problematic for normal variants as well, is it not? In fact, that GADT seems isomorphic to

type t =
  | T1 of t1
  | T2 of t2

You can also “solve” this problem by writing f as:

let f  = function
  | (T1 { b; _ } | T2 { b } ) -> b

Forgive me but I’m struggling to think of another example where this breaks apart specifically for GADTs. The PR you linked states the problem similarly, but lacks a specific example.

1 Like
4

With a normal variant, the two occurrences of x in the patterns have different types, so the compiler will forbid it. With GADTs, you could (with a bit more work, involving an extra parameter to the type t) make it so their types are compatible.
Something like that:

type _ t =
| T1 : t1 -> t1 t
| T2 : t2 -> t2 t

let f (type a) (t : a t) = match t with
  | (T1 x | T2 x) ->
    (* x has type a, which is abstract at this point, so we should have an error *)
    x.b

Your solution moves the field access back into the patterns, so it should work with regular variants and with GADTs (on recent enough versions of the compiler), as the right-hand side doesn’t depend on GADT equations anymore.

1 Like