Explicitly name types in GADT patterns

Community
1

Hi everyone, Section 7.6 of the manual gives a syntax to explicitly name existential types in GADTs, but it doesn’t say what to do when the type is not an existential type. Here’s a snippet that I would want to work. How could I write it differently in order for it to work?

type _ t =
	| A: 'a -> ('a * 'a) t

let f: type a. a t -> a =
	fun x ->
	begin match x with
	| A (type u) (a:u) -> (a, a)
	end

Here the code is correct except for the typing annotation, and it works when you remove it, but this is a MWE, and in my actual case (something involving let module), I absolutely need the typing annotation.

Any help would be appreciated, thanks

1 Like
2

You should extend your example to cover your use case.

Without more information, it sounds likely that something similar to:

let a_branch (type a) (x:a) =
   let module M = Set.Make(struct type t = a * a let compare = Stdlib.compare end) in
   x, x
let f : type a. a t -> a =fun (A x) -> a_branch x

would work.

3

You can always add a trivial redex to name a type:

let f x =
  match x with
  | A a -> a |> fun (type u) (a:u) -> (a, a)

(This is fundamentally the same as @octachron’s solution, but without the need for lambda-lifting.)

2 Likes
4

It doesn’t explain the really cryptic error message:

let f : type a. a t -> a = function
  | A (type u) (x : u) -> (x, x)
;;
Error: This pattern matches values of type u
       but a pattern was expected which matches values of type $0

I believe the purpose of the introduction of this syntax was to avoid the type $0 in error messages, and why u and $0 don’t unify?

@gasche : if I remember correctly you introduce this new syntax, but I don’t understand why it doesn’t work in this case. Why the type variables u and $0 don’t unify? It puzzles me… :thinking:
To be clear, what I was expecting is that u and $0 unify and then that a unifies with u * u.

1 Like
5

I agree that the error message is bad, and that one could expect this example to work.

I would also expect the following to work:

type _ th =
  | Thunk : 'a * ('a -> 'b) -> 'b th

let f (type t) : t th -> t = function
  | Thunk (type a b) (x, f : a * (a -> b)) -> f x

and it currently does not. So maybe the implementation needs refining.

Currently it looks like only “pure existentials” can be named this way, not existentials that are equated with a part of the rigid type variable being refined with an equality. But I don’t think that we should expect users to make this distinction, they probably want to name all the variables local to the GADT constructor in the type declaration.

I think we should open an upstream issue to track this limitation of the current implementation.

(This is probably a sign that not too many people have tried to use it yet, otherwise I think they would have reported similar confusions?)

Note: I did not introduce the new syntax, this is work from @garrigue.

1 Like
6

My memory is playing tricks on me…

If the problem deserves an upstream issue could you open one? I don’t have a github account.

7

In this case, @silene trick still works:

let foo : type t. t th -> t = function
  | Thunk (x, f) -> (fun (type a b) (f : a -> b) (x : a) -> f x) f x;;
val foo : 't th -> 't = <fun>

And this one, similar to manual’s one, also works:

let foo : type t. t th -> t = function
  | Thunk (x, f) -> (fun (type a) (f : a -> _) (x : a) -> f x) f x;;
val foo : 't th -> 't = <fun>

Maybe the type checker should follow the same path that it takes with the trick and with the new syntax?

8

The trick of silene is doing something quite different and the two features are not equivalent.

9

Indeed, that’s what I realized after more reflection. I guess the type checker first type the anonymous lambda with ('a -> 'b) -> 'a -> 'b and then apply this scheme with the local type of the GADT.

By the way, there may be some problem also with local abstract type unrelated to GADT. This example, close to yours, give me a weird error message:

fun (type a b) (x,f : a * a -> b) -> f x;;
Error: This pattern matches values of type 'a * 'b
       but a pattern was expected which matches values of type a * a -> b
10

The error message is trying to tell you that (x, f) cannot be of type (a * a) -> b, and it is not so bad.

11

Indeed, with the right parenthesis it works. :laughing:

12

(We could possibly stop assuming that people are familiar with the respective precedence of * and -> in the type printer, or think of way of mentioning the head type constructors that clash in addition to showing the full types.)

13

Maybe. To me -> is an exponential and it should have precedence over product. I wrote 5 * 3 ^ 2 to mean 5 * 9 and not 15 ^ 2. :wink:

Edit: in reality, it’s even worse. When you see -> as an exponential, 3 ^ 2 should be written 2 -> 3. And so, with the precedence rules of Ocaml, instead of 5 * 9, I get:

5 * 3 ^ 2 = 5 * 2 -> 3 = (5 * 2) -> 3 = 3 ^ (5 * 2) = 3 ^ 10

Edit2: choose prime numbers to avoid particular equality.