What is the difference / meaning of `type a.` versus (type a):`

Question

I've stumbled onto 'GADT's in Ocaml. They look interesting and powerful, but they are a bit of a head scratcher.

As I'm reading through this 'tutorial' here... it reads mostly like giberish to me. But let's try and focus a question out of that to make some headway.

It gives an example of a simple expression language.

type _ term =
  | Int : int -> int term
  | Add : (int -> int -> int) term
  | App : ('b -> 'a) term * 'b term -> 'a term

The motivation for this (similar if not identical example) and why GADTs are good/useful is actually better explained in the Real World Ocaml book. It sort of makes sense.

But neither of these sources really explains the meaning of some 'special' type declaration syntaxes for recursive functions on GADTs that they are using, and that seem crucial into having things type-check and compile.

From ocaml manual/tutorial:

let rec eval : type a. a term -> a = function
  | Int n    -> n                 (* a = int *)
  | Add      -> (fun x y -> x+y)  (* a = int -> int -> int *)
  | App(f,x) -> (eval f) (eval x)
          (* eval called at types (b->a) and b for fresh b *)

And it then says:

It is important to remark that the function eval is using the polymorphic syntax for locally abstract types.

What on earth is a 'polymorphic syntax for locally abstract types' I guess they are talking about the strange type a. notation, but that still doesn't tell me what that notation actually means.

And they compare/contrast this with

let rec eval (type a) : a term -> a = function ...

This looks almost the same to me. But I suppose it means something subtly different.

For good measure, I can add one more 'similar' but more familiar looking thing that probably still means something different still:

let rec eval : 'a term -> 'a

Can someone explain what exactly each of these three notations means and how they are saying something (subtly) different from each other (naively... to me they all look similarly 'polymorphic' as they are seemingly saying the same thing (translated into informal English):

eval takes a term of type a and returns a value of type a