Indeed excellent! I finally found some time last week and read the three tutorials.
I would also recommend Raphael’s tutorials on lwt also on this website. It helped a lot when I started to use lwt.

It’s fun to know the GADT uses object types for parameters, but no object appears at runtime.

I have no ppx experience but I wonder whether/how GADT can be used in ppx.

May be i have misunderstood something however i believe GADTs also allow existentially quantified type variable(s) like 'c in the following example

(* 'a and 'b are universally quantified *)
(* 'c is existentially quantified *)
type ('a,'b) chain =
| Link : 'a * 'b -> ('a,'b) chain
| Append : ('a,'c) chain * ('c,'b) chain -> ('a,'b) chain
let rec length : type a b. (a,b) chain -> int =
function
| Link _ -> 1
| Append(p,q) -> length p + length q

I’m not sure this is really adressed in your tutorial. May be because my chain type is too weird.

It appears in the part2’s example Equal case though it’s not called existentially there.

type _ expr =
| Value : 'a v -> 'a expr
| Equal : 'a expr * 'a expr -> bool expr
| IfThenElse : bool expr * 'a expr * 'a expr -> 'a expr
(* more constructors as needed *)

As mentioned by @arbipher there’s something along those lines in part 2. But I also think it’d be worth pointing out explicitly so I’ll add a paragraph somewhere.