# Puzzling through some GADT errors

**URL:** <https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478>\
**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:** 4\
**Page:** 2

<div class="post-metadata">

**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 21, 2021, 7:53am UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/21 "2021-09-21T07:53:35Z")

</div>

Not much better, but it should be enough to connect `b` with one occurrence.

```auto
let f : 'a 'b. ([> `Foo] as 'a) -> 'b -> 'a * 'b =
  fun (type b) x (y : b) -> (x,y) ;;

```

---

<div class="post-metadata">

**Author:** ![emillon](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/emillon/32/1206_2.png) [@emillon](https://discuss.ocaml.org/u/emillon)\
**Post date:** [September 21, 2021, 12:26pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/22 "2021-09-21T12:26:46Z")

</div>

> [@viritrilbia](#):
>
> 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 `->` ?).

It’s a fun puzzle!

- `(type b)` is represented as an argument in the parse tree. So in the same way that `fun x y -> r` is the same as `fun x -> fun y -> r`, `fun (type a) x -> r` is also the same as `fun (type a) -> fun x -> r`.
- it’s possible to annotate a `fun` with the return type by adding a type just before the arrow, such as `fun x : string -> ""`

You can combine the syntaxes: it’s possible to write the the identity function, monomorphized to ints:

```ocaml
fun (type a) : (int -> int) -> Fun.id

```

Expand the definition and you’re not far from your example:

```ocaml
fun (type a) : (int -> int) -> fun x -> x

```

Extra fun fact, you can also write:

```ocaml
fun (type a) -> 1

```

And it’s just an int.

---

<div class="post-metadata">

**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:09pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/23 "2021-09-21T16:09:56Z")

</div>

Thanks @garrigue! That significantly reduces the duplication in my actual example.

> [@emillon](#):
>
> it’s possible to annotate a `fun` with the return type by adding a type just before the arrow, such as `fun x : string -> ""`

Huh. Why? That looks dangerously easy to confuse with `fun (x : string) -> ""`. Wouldn’t it make more sense for the return type to be an annotation on the return _value_?

---

<div class="post-metadata">

**Author:** ![emillon](https://sea2.discourse-cdn.com/flex020/user_avatar/discuss.ocaml.org/emillon/32/1206_2.png) [@emillon](https://discuss.ocaml.org/u/emillon)\
**Post date:** [September 22, 2021, 12:14pm UTC](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478/24 "2021-09-22T12:14:24Z")

</div>

I can’t comment on the “why”, but this way you can annotate both the arguments and the return value (`fun (x:int) : string -> ""`). You can also annotate the return value. IIRC it parses to the same abstract syntax.

[Previous page](https://discuss.ocaml.org/t/puzzling-through-some-gadt-errors/8478.md?page=1)