OCaml GADTs and avoiding "type constructor would escape its scope" errors

test.ml

(* GADT list that exposes the type of the head element *)
type _ hlist =
 | Nil: 'a hlist
 | Cons: ('a * 'b hlist) -> 'a hlist

(* let rec len = function *)
(* let rec len (type a) (l: a hlist): int = match l with *)
(* both of the above result in a "type constructor would escape its scope" error *)
(* correct version: *)
let rec len : type a. a hlist -> int = function
(* also correct: *)
(* let rec len : 'a. 'a hlist -> int = function *)
 | Nil -> 0
 | Cons (h, t) -> 1 + len t

(* NB: this only works if you don't extract your elements.
   if you need to extract the elements then the error is real, and you either need to redesign your code
   so that the inner types (to be extracted) are contained in the outer type param *)

What's the difference between (type n) and type n.

Aren't they both locally abstract types?

@ebresafegaga It's been a few years, but I think the difference is that in the incorrect version a refers to a unification variable that needs to be unified with the other types in the program; whereas in the correct version a is used in the context of an implicit forall a quantifier over the type, which is self-contained and does not need to be unified with the other types in the program.