Locally abstract type VS explicit polymorphism in polymorphic recursion context

Could you explain me why this program does typecheck

let rec plop1 : 'a 'b 'c. 'a -> 'b * 'c = 
  fun x -> (fst (plop1 ""), snd (plop1 1))

while this one does not?

let rec plop2 (type a b c) (x : a) : b * c = 
  (fst (plop2 ""), snd (plop2 1))

I already read definition of locally abstract type in the OCaml manual; What is the difference between 'a. and type a. and when to use each?; and What is the difference between type variables and locally abstract types?, but they are not clear enough for me.

Polymorphic recursion requires an explicitly polymorphic annotation of the type of the function. This is needed in order to be able to use this explicit type as the type of the function inside its own body. For instance,

type 'a btree = Leaf of 'a | Node of ('a * 'a) btree
let rec sum: 'a. ('a -> int) -> 'a btree -> int =
fun f btree -> match btree with
| Leaf x -> f x
| Node x -> sum (fun (x,y) -> f x + f y) x
let sum = sum Fun.id

See https://ocaml.org/manual/5.2/polymorphism.html#s%3Apolymorphic-recursion for more details.

There is no such explicit type annotation on the whole function in your second case

let rec plop2 (type a b c) (x : a) : b * c = 
  (fst (plop2 ""), snd (plop2 1))

only some annotation over parts of the function. This is an meaningful difference because values are normally only made polymorphic on let.

More generally, locally abstract types are not really relevant for polymorphic recursion. A local abstract type introduces a fresh type name, which can be used in type definitions or to add local equation inside a branch of pattern match with GADTs. In other words,

fun (type a) -> ...

would be equivalent to a hypothetical

let type a in ... (* <1> *)

which create a fresh abstract type limited to the scope <1>.

Notably, this means that the OCaml construction fun (type a) -> ... is not equivalent to system-F 𝛬. For instance, fun (type a) (x:a) -> ... is not equivalent to 𝛬a. 𝜆(x:a) ....

The closer transcription in OCaml might be

let f: type a. a -> _ = ...

but this notation in itself is a syntactic sugar for

let rec plop2: 'a. 'a -> _ = fun (type a) (x:a) ->
  fst (plop2 ""), snd (plop2 1)

and it is the first part which matters for polymorphic recursion.