Unexpected rejection of a fixpoint by the guard, despite providing a subterm

[Mbodin]

Description of the problem

Consider the following code:

Inductive tree :=
| Foo : list tree -> tree.

Fixpoint f (l : list tree) {struct l} :=
  match l with
  | nil => 0
  | cons (Foo l') _ => f l'
  end.

This code is refused by Coq, with the following error message:

Recursive definition of f is ill-formed.
In environment
f : list tree -> nat
l : list tree
t : tree
l0 : list tree
l' : list tree
Recursive call to f has principal argument equal to 
"l'" instead of "l0".
Recursive definition is:
"fun l : list tree =>
 match l with
 | nil => 0
 | (Foo l' :: _)%list => f l'
 end".

I may be missing something, be it seems to me that the recursive call to f is done in a strict subterm of its argument l.
The error message seems to consider three different lists: l, l0, and l'. I guess that l0 corresponds to the wildcard in the pattern matching (if so, it would be nice to write it down in the printed term). I fully agree that the wildcard would also be a good sublist to recursively call, but this is not what I want to define. Or does the subterm relation doesn't pass through more than one constructor? If so, an example like this one would be very welcomed in the documentation (that currently goes very mathy to explain the notion of subterm).

Surprisingly, the following definition is accepted, despite seemingly be in the same situation (where tree and list are inversed):

Fixpoint f (t : tree) :=
  match t with
  | Foo (cons x _) => f x
  | Foo _ => 0
  end.

Coq also accepts the definition if instead of using the usual list, one uses a custom mutually recursive list. This is however not an option for me as it breaks modularity: one has to change the definition of the inductive to make this work.

Note that there might be a very good reason to reject the first function and not the others: this may just a documentation issue rather than a guard issue.

This is a possible duplicate of issue #12020.

Coq Version

$ coqc --version
The Coq Proof Assistant, version 8.10.2 (May 2020)
compiled on May 20 2020 17:34:49 with OCaml 4.09.1