# Puzzling through some GADT errors **URL:** \ **Category:** Learning\ **Tags:** gadt\ **Created:** [September 12, 2021, 2:52pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478 "2021-09-12T14:52:50Z")\ **Posts on this page:** 20\ **Page:** 1
**Author:** ![Yaron\_Minsky](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yaron_minsky/32/11_2.png) [@Yaron\_Minsky](https://discuss.ocaml.org/u/Yaron_Minsky)\ **Post date:** [September 12, 2021, 2:52pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/1 "2021-09-12T14:52:50Z")
I’m playing around with GADTs and running in to some puzzling errors I’m trying to understand better. Here’s a simple, working example of a function that uses GADTs as a way of controlling its return type. ```ocaml module If_nothing_chosen = struct type (_, _) t = | Default_to : 'a -> ('a, 'a) t | Raise : ('a, 'a) t | Return_none : ('a, 'a option) t end let choose_one (type a b) test things (if_nothing_chosen : (a, b) If_nothing_chosen.t) = let rec loop (things : a list) : b = match things with | [] -> (match if_nothing_chosen with | Raise -> failwith "No matching item found" | Return_none -> None | Default_to x -> x) | thing :: rest -> if test thing then ( match if_nothing_chosen with | Default_to _ -> thing | Raise -> thing | Return_none -> Some thing) else loop rest in loop things ;; ``` This compiles just fine, but if I want to define `choose_one` itself as a recursive function, it doesn’t compile. ```ocaml let rec choose_one (type a b) (test : a -> bool) (things : a list) (if_nothing_chosen : (a, b) If_nothing_chosen.t) : b = match things with | [] -> (match if_nothing_chosen with | Raise -> failwith "No matching item found" | Return_none -> None | Default_to x -> x) | thing :: rest -> if test thing then ( match if_nothing_chosen with | Default_to _ -> thing | Raise -> thing | Return_none -> Some thing) else choose_one test rest if_nothing_chosen ;; ``` The error message I get is: ```auto File "src/w.ml", line 104, characters 20-24: 104 | else choose_one test rest if_nothing_chosen ^^^^ Error: This expression has type a -> bool but an expression was expected of type 'a The type constructor a would escape its scope ``` which I find pretty confusing! Given that there’s a recursive use of the function, I thought doing explicit polymorphic recursion might fix things, and indeed it did. ```ocaml let rec choose_one : type a b. (a -> bool) -> a list -> (a, b) If_nothing_chosen.t -> b = fun test things if_nothing_chosen -> match things with | [] -> (match if_nothing_chosen with | Raise -> failwith "No matching item found" | Return_none -> None | Default_to x -> x) | thing :: rest -> if test thing then ( match if_nothing_chosen with | Default_to _ -> thing | Raise -> thing | Return_none -> Some thing) else choose_one test rest if_nothing_chosen ;; ``` But I don’t really understand why it was necessary, given that the recursive call is happening at the same type. Also, I don’t fully understand why there’s a “type constructor would escape its scope” error in the first place. y ---
**Author:** ![CraigFe](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/craigfe/32/1989_2.png) [@CraigFe](https://discuss.ocaml.org/u/CraigFe)\ **Post date:** [September 12, 2021, 3:47pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/2 "2021-09-12T15:47:58Z")
(_Disclaimer: I’m not an expert on the OCaml type system. What follows is remembered conversation from @let-def; any mistakes my own._) Firstly, it’s worth noting that this behaviour isn’t to do with GADTs, but can apply wherever recursion and locally-abstract types mix: ```ocaml let rec find (type a) (f : a -> bool) : a list -> a option = function | [] -> None | x :: xs -> if f x then Some x else find f xs (* ^ * Error: This expression has type a -> bool * but an expression was expected of type 'a * The type constructor a would escape its scope *) ``` This is a particularly interesting example, because this function will be correctly typed if there are no annotations whatsoever. AFAIK, it has partly to do with the _order of introduction_ of type bindings, and partly that OCaml’s heuristic for typing polymorphic recursion is aborted when it sees a type binder. In the case of `(type a b)`, the bindings for the locally abstract types occur at the term level: _inside_ the binding for `choose_one` and after it has entered the typing environment. If we consider what the typing environment looks like at the moment of typing the recursive call: ```ocaml let rec choose_one (type a b) test ... = ... choose_one test ... (* HERE *) ``` We have something like this, from outermost to innermost bindings - `choose_one : '_choose_one` (there is a symbol `choose_one`, with no inferred type) - `type a b` (there are local types `a` and `b`) - `test : a -> bool` On observing the recursive call, we attempt to unify `'_choose_one` with `(a -> bool) -> _`. However, `a` was introduced after `choose_one`: if we complete this unification then we end up with `choose_one : (a -> bool) -> '_rest`, where `a` is not yet bound. `a` would escape its scope! So we reject the program for this reason. If we add an explicitly-polymorphic type annotation, we fix the problem by letting the type-checker take a _fresh_ instance of the polymorphic variable in order to type the recursive call: ```ocaml let rec choose_one : 'a 'b. ('a -> bool) -> ... = fun (type a b) test ... -> ... choose_one test ... (* HERE *) ``` (This variation is what the `type a b.` syntax expands to. The expaded form is a little clearer here at showing that this syntax introduces both type-level type bindings and term level type bindings.) This time around, we get a typing environment that looks like: - `choose_one : 'a. 'b. ('a -> bool) -> ...`. (No need to approximate the type, as it’s been given directly.) - `type a b` - `test : a -> bool` (Don’t need to take an instance of the outer polymorphic constraint: we can propagate the abstract type specification directly.) Now the unification implied by the recursive call succeeds: we can lookup `choose_one` in the type environment and instantiate a fresh instance with the specific abstract type `a`, without `a` escaping its scope. ---
**Author:** ![Yaron\_Minsky](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/yaron_minsky/32/11_2.png) [@Yaron\_Minsky](https://discuss.ocaml.org/u/Yaron_Minsky)\ **Post date:** [September 12, 2021, 7:35pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/3 "2021-09-12T19:35:22Z")
Hmm. I think I roughly understand the description here, but it’s pretty unsatisfying. It feels very implementation driven, and I’m not sure how to tell someone how to know which annotations will work and which won’t. I’m curious if anyone knows if this is a case where there are plans to make this simpler and more intuitive by improving the type inference, or if this is kind of as good as it gets. y ---
**Author:** ![EduardoRFS](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/eduardorfs/32/2259_2.png) [@EduardoRFS](https://discuss.ocaml.org/u/EduardoRFS)\ **Post date:** [September 13, 2021, 12:00am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/4 "2021-09-13T00:00:40Z")
I feel like there is no principal way to allow your code tho, as `let rec f p = f p` is just sugar to `let rec f = fun p -> f p`, which makes the problem a lot clearer. A principal’ish way that I could think of is `let v = (expr: typ)` being a special case where we look a head and improve the type constraint, and make so that `fun (a: int) -> a` is actually sugar to `(fun a -> a): int -> _`. This would solve the problem, ~~and it’s possible to even transform the `let v: typ = expr` be sugar to `let v = (expr: typ)`, making it slightly more principal~~ the let case is a Ppat\_constraint. Not sure if we do this kind of “lookahead” at any point in the typer, but it’s definitely not hard to implement, besides breaking a lot of PPX or making the AST be redundant. edit: After checking code, type\_approx is already a thing so we do the lookahead, I wonder why it’s not handling this case then, still trying to implement it. edit2: Was able to infer the type correctly, just need to clean a bit to ensure that the level + scope is all right. edit3: Will try to ensure that everything is working, I broke some warnings, and if I can do it, will open a PR. Mostly do basic approximation of patterns, and add approximation of pexp\_newtype. ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [September 13, 2021, 8:02am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/5 "2021-09-13T08:02:10Z")
> [@Yaron\_Minsky](#): > > ow to tell someone how to know which annotations will work and which won’t. One solution is to always use `let rec f: type x y ...` which works in most cases, and consider that `(type a b)` is only useful for showing off one understanding of the precise typing rule of the OCaml typechecker. With this `type a ... . ...` syntax, the only corner case which is not covered by this syntax is universal quantification over row type variables. ---
**Author:** ![EmileTrotignon](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/emiletrotignon/32/5913_2.png) [@EmileTrotignon](https://discuss.ocaml.org/u/EmileTrotignon)\ **Post date:** [September 13, 2021, 10:27pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/6 "2021-09-13T22:27:47Z")
Is there a syntax to cover this case ? ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [September 14, 2021, 8:21am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/7 "2021-09-14T08:21:30Z")
One must use the ordinary universal quantification in this case: ```auto let rec f: 'a. ([> `X] as 'a) -> unit = function | `X -> f `Y | _ -> () ``` ---
**Author:** ![gasche](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/gasche/32/4_2.png) [@gasche](https://discuss.ocaml.org/u/gasche)\ **Post date:** [September 15, 2021, 7:07pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/8 "2021-09-15T19:07:56Z")
Not exactly what you are asking for, but @Octachron wrote an excellent [chapter on GADTs](https://ocaml.org/releases/4.12/manual/gadts.html) in the OCaml manual, which could be recommended to people starting GADT programming. It explains why recursive functions on GADT need “explicit polymorphic annotations” in less “implementation driven” terms. (The chapter also demonstrates the new naming scheme for existential type variables introduced by GADT constructors, which can help a lot working through type errors, but are still a bit heavy and deserve a gentle introduction.) ---
**Author:** ![octachron](https://avatars.discourse-cdn.com/v4/letter/o/49beb7/32.png) [@octachron](https://discuss.ocaml.org/u/octachron)\ **Post date:** [September 15, 2021, 7:43pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/9 "2021-09-15T19:43:37Z")
I have only written the nomenclature part and a bit of the explanation for recursive functions in this chapter, @garrigue is the author of most of this chapter. ---
**Author:** ![garrigue](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/garrigue/32/2644_2.png) [@garrigue](https://discuss.ocaml.org/u/garrigue)\ **Post date:** [September 16, 2021, 12:11am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/10 "2021-09-16T00:11:22Z")
I see lots of good replies. This essentially boils down to: if you want to use both GADT refinement and recursion, use `type a. ....` annotations. Actually, I would even suggest to use them for all functions involving GADTs, as both the notation and behavior are more intuitive. As for why `(type a)` doesn’t play well with recursion, @CraigFe is basically correct, except that there are no heuristics involved. Namely polymorphic recursion in OCaml is always explicit, using either annotations of the form `'a. ...` or `type a. ...` (the latter being actually syntactic sugar for the former). Using `(type a)` with normal (monomorphic) recursion is bound to fail because it tries to unify the internal type `a`, which is a locally abstract type, with the external type, which is a type variable outside of the scope of `a`, hence the error. ---
**Author:** ![EduardoRFS](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/eduardorfs/32/2259_2.png) [@EduardoRFS](https://discuss.ocaml.org/u/EduardoRFS)\ **Post date:** [September 16, 2021, 11:17am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/11 "2021-09-16T11:17:05Z")
Any particular reason we couldn’t have a better type approximation from it? Seems explicitly enough to me that `fun (type a) (f: a t): a ->` would always have the same signature as `'a. 'a t -> 'a`. Is that wrong? ---
**Author:** ![garrigue](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/garrigue/32/2644_2.png) [@garrigue](https://discuss.ocaml.org/u/garrigue)\ **Post date:** [September 16, 2021, 12:21pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/12 "2021-09-16T12:21:38Z")
FIrst, to clarify, there is no connection between `(type a)` and `'a. ...`, and `'a. 'a t -> 'a` can only be used on let-definitions, so what you must be asking for is that `let g (type a) (f : a t) : a = ...` be interpreted as `let g : type a. a t -> a = fun f -> ...` While this is certainly doable, this would be a pain to implement: one has to collect all the components of the type from separate annotations, and redo all the processing after that. Moreover this creates the question of where we stop. If this is accepted when all annotations are provided, then people would start asking why `let g (type a) (f : a t) = ...` is not interpreted as `let g : type a. a t -> _ = fun f -> ...` which creates the question of whether this interpretation would not break backward compatibility. And people might even ask for more exotic stuff where it is no longer trivial to see which annotations participate to the definition. The advantage of the current approach is precisely that we don’t play heuristics: we are not reusing an existing syntax to do something else, but introduce a new syntax that does something specific. By the way, there are indeed situations where (type a) does not create a polymorphic type: ```ocaml let f : int -> int = fun (type a) (x : a) : a -> x;; val f : int -> int = ``` ---
**Author:** ![garrigue](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/garrigue/32/2644_2.png) [@garrigue](https://discuss.ocaml.org/u/garrigue)\ **Post date:** [September 16, 2021, 1:01pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/13 "2021-09-16T13:01:44Z")
I could easily find an example that types with the original annotation, but breaks if we combine it: ```ocaml let g (type a) (x : a) : _ = x;; val g : 'a -> 'a = let g : type a. a -> _ = fun x -> x;; Error: This definition has type 'b -> 'b which is less general than 'a. 'a -> 'c ``` So, we could only do this transformation when the combined annotation is closed, i.e. contains no unification variable. We do that for subtyping, but I’m afraid that here this would just add to the confusion. ---
**Author:** ![EduardoRFS](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/eduardorfs/32/2259_2.png) [@EduardoRFS](https://discuss.ocaml.org/u/EduardoRFS)\ **Post date:** [September 16, 2021, 3:31pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/14 "2021-09-16T15:31:02Z")
> [@garrigue](#): > > By the way, there are indeed situations where (type a) does not create a polymorphic type: ```ocaml let f : int -> int = fun (type a) (x : a) : a -> x;; (* is essentially *) let f = fun (type a) (x: a): a -> x;; let f: int -> int = f ``` Which seems to me that It creates a polymorphic type you’re just constraining it in sequence. > [@garrigue](#): > > I could easily find an example that types with the original annotation, but breaks if we combine it: Oh, good job on this, it definitely shows that my transformation doesn’t work for all cases, so I will try to understand, why is that the case? From what I understand is because `'a` cannot be unified with `'c'` which doesn’t make a ton of sense in my head and is probably related to how this Tpoly stuff works. But even then, on my current implementation which I believe to not be sound, the following works as the approximation added is the generalized one, so it’s not fully equivalent to `'a. 'a -> _` but more like `'a -> _`, where 'a is generalized and \_ is not, my assumption is that is safe as it is safe to allows `unify 'a _` to work. And the only change made here is improving the type approximation. to approximate the following type. ```ocaml let rec id (type a) (x: a): _ = let x' = id x in assert (x = x'); x ``` ---
**Author:** ![garrigue](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/garrigue/32/2644_2.png) [@garrigue](https://discuss.ocaml.org/u/garrigue)\ **Post date:** [September 17, 2021, 4:21am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/15 "2021-09-17T04:21:51Z")
I’m not sure I understand what you are doing, but to me it looks like it’s potentially unsound. If you assume that the type of `id` is `'a -> _` with `'a` generalized (which I would certainly write `'a. 'a -> _`, but you seem to make a distinction), then it means that occurrences of `id` in the body ignore the type of their argument. Wouldn’t then the following function be accepted in your system? ```ocaml let rec id (type a) (x: a): _ = let x' = id 1 in ignore (x = x'); x' ``` ---
**Author:** ![EduardoRFS](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/eduardorfs/32/2259_2.png) [@EduardoRFS](https://discuss.ocaml.org/u/EduardoRFS)\ **Post date:** [September 17, 2021, 6:22pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/16 "2021-09-17T18:22:31Z")
> [@garrigue](#): > > but you seem to make a distinction Mostly because I see `'a. 'a -> _` as a Tpoly('a → \_) which doesn’t unify with `'a -> _`. Will use the `'_weak` convention for weak vars so that it’s clear. > [@garrigue](#): > > Wouldn’t then the following function be accepted At first my thought was that it should be allowed as this function is infinitely recursive, but this function is rejected, which is also nice. As \_ is a weak variable introduced by the approximation, the following is how this function that you sent will be typed, it will be rejected on the `ignore (x = x')` as otherwise `a` would escape its scope. ```ocaml (* this reference was added just to have a weak variable *) let v = ref (assert false) (* this is the approximated type, 'a -> '_weak *) let id_approx (type a) (x: a): _ = !v let id (type a) (x: a): _ = let x' = id_approx 1 in ignore (x = x'); x' ``` ---
**Author:** ![ivg](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ivg/32/103_2.png) [@ivg](https://discuss.ocaml.org/u/ivg)\ **Post date:** [September 17, 2021, 9:02pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/17 "2021-09-17T21:02:32Z")
> [@Yaron\_Minsky](#): > > Also, I don’t fully understand why there’s a “type constructor would escape its scope” error in the first place. There is an [excellent post](http://okmij.org/ftp/ML/generalization.html) by Oleg Kiselyov, which I personally found very insightful in understanding the _scope_ part of the error. It will also answer why is recursion another scope. In summary, the main idea is that types in OCaml have a lifetime much like the values (indeed OCaml can create new types in runtime). And to ensure soundness we have to guarantee that no value can outlive its type, i.e., imagine if we have a value that has no type - **unsoundness**. Besides, the simplest example, that doesn’t involve any GADT is, ```auto let x = ref None type t = T let () = x := Some T ``` Functions and let expressions, all create scopes for types. And if the type is created inside of the function and there is a value that somehow escapes out of the scope of this function (either via a closure a directly as the returned value) that is unified with this local to the function type, then we have the soundness breach. The only option is to guarantee that the type existed before the application of the function, i.e., to unify the type with a parameter (because OCaml is strict and the value has to exist before the application and if the value exists then it has type). That is why we need a locally abstract type, which we can unify with some of the input parameters. Finally, the recursive part. Each invocation of a function, recursive or not, creates a new scope, so we have to prove that values from the inner scope do not escape to the outer scope (via unification). The easiest option is to disjoin them by annotating them as explicitly polymorphic. With that said, I believe that the reference to scope in the error message is confusing, as it refers to a notion that is not really defined in the manual and neither is a part of the programmer’s common knowledge. Yes, we commonly know about the scope of variables, but not that types also have scopes and that those scopes could be dynamic. So this error message is a leaking abstraction of the type checker implementation. ---
**Author:** ![ivg](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/ivg/32/103_2.png) [@ivg](https://discuss.ocaml.org/u/ivg)\ **Post date:** [September 17, 2021, 11:13pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/18 "2021-09-17T23:13:08Z")
> [@Yaron\_Minsky](#): > > ```auto > Error: This expression has type a -> bool > but an expression was expected of type 'a > The type constructor a would escape its scope > > ``` Also, I wasn’t able to reproduce this error message in the range of OCaml compilers starting from 4.09 til 4.13~alpha, all of them report, ```auto This expression has type 'a but an expression was expected of type b The type constructor b would escape its scope ``` So there is no unification between the `test` and the `thing`. ---
**Author:** ![EduardoRFS](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/eduardorfs/32/2259_2.png) [@EduardoRFS](https://discuss.ocaml.org/u/EduardoRFS)\ **Post date:** [September 18, 2021, 2:00am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/19 "2021-09-18T02:00:35Z")
@garrigue I believe the following code is close to the idea, it’s just a piece of code hacked together as essentially I wanted a `instance_poly` but in place. > It can type the example that started this thread and also fails to type all the unsound examples that you sent to me up to now. It also rejects the example that I gave, so effectively any usage of the local type variable needs to be explicitly annotated as always but at least the syntax for named parameters is not terrible. ```ocaml (* fails *) let rec id (type a) (x: a): _ = ... ``` I believe the implementation is unsound because the way it set the levels of everything, but there is anything fundamentally unsound on the idea? It is essentially improving the type approximation and dealing with the problem that the pattern will be typed as `'_a` and the approximation will be `'a -> 'a` but when unified with `'_a` it leads to `'_a -> '_a` which seems just an artifact and nothing meaningful as in reality the ident is not constraining the type at all, so in this code I fix the variables levels and the types levels to generic which definitely leads to bugs(as it fails even to compile the stdlib fully). ---
**Author:** ![viritrilbia](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/viritrilbia/32/3083_2.png) [@viritrilbia](https://discuss.ocaml.org/u/viritrilbia)\ **Post date:** [September 21, 2021, 4:27am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/20 "2021-09-21T04:27:59Z")
> [@octachron](#): > > With this `type a ... . ...` syntax, the only corner case which is not covered by this syntax is universal quantification over row type variables. > [@octachron](#): > > One must use the ordinary universal quantification in this case I recently had a situation where one function was universally quantified over multiple types, some of which were row type variables and others of which needed to be locally abstract. I wanted to write something like `'a. type b.` but OCaml wouldn’t accept it (I guess only one dot is allowed?). The only way I was able to figure out to annotate such a function was to manually expand out what [the manual](https://ocaml.org/manual/locallyabstract.html) says the `type a.` syntax is automatically expanded into. This required the type of the function to be written twice, once with the locally abstract type quoted and once not: ```auto let f : 'a 'b. ([> `Foo] as 'a) -> 'b -> 'a * 'b = fun (type b) -> (fun x y -> (x,y) : ([> `Foo] as 'a) -> b -> 'a * b);; ``` Ocamlformat then rewrote this into ```auto let f : 'a 'b. ([> `Foo] as 'a) -> 'b -> 'a * 'b = fun (type b) : (([> `Foo] as 'a) -> b -> 'a * b) -> fun x y -> (x, y) ``` which also compiles, but which I find even more puzzling to parse in my head (why does the type of the function come after the `fun (type b)` but before the `->` ?). Is there a better way to annotate the type of such a function? [Next page](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478.md?page=2)