Puzzling through some GADT errors

Learning
21

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

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

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:

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

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

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

Extra fun fact, you can also write:

fun (type a) -> 1

And it’s just an int.

23

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

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?

1 Like
24

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.