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

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

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

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