The annotation needs to be directly at the "function" node:

let rec walk : type a b . (a place -> b place -> (a, b) nearby) =

(fun x goal ->

((function Same -> Here (x, goal)

| NotSame ->

let Ex1 ((y, to_y)) = wander x in

Transitive (to_y, walk y goal))

: ((a, b) meet -> (a, b) nearby))

(compare x goal))

Regarding the first part, thanks to Gabriel, that explained it to me.

On Mon, Dec 9, 2013 at 6:24 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:

On Mon, Dec 9, 2013 at 6:16 PM, Lukasz Stafiniak <lukstafi@gmail.com> wrote:

Hello,

I am at a loss as to the difference between ['a.] syntax and [type a.] syntax of introducing polymorphic recursion. I will provide some examples. (Bear with me, they are automatically generated.)

[...]
Now to a more complex example.

In the complex example, the problem is not the difference between ['a.] syntax and [type a.] syntax, but polymorphic recursion and GADTs in OCaml generally. What type annotations do I need to provide?