Not exactly what you are asking for, but @Octachron wrote an excellent chapter on GADTs in the OCaml manual, which could be recommended to people starting GADT programming. It explains why recursive functions on GADT need “explicit polymorphic annotations” in less “implementation driven” terms.
(The chapter also demonstrates the new naming scheme for existential type variables introduced by GADT constructors, which can help a lot working through type errors, but are still a bit heavy and deserve a gentle introduction.)