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?
>