(* Here's a good old implementation of map *)
Fixpoint map {A B} (f: A -> B) (l : list A) : list B :=
  match l with
  | [] => []
  | x :: l => f x :: map f l
  end.

(* And a datatype of trees *)
Inductive Foo : Set := | Leaf | Node : list Foo -> Foo.

(* Problem: if I do a (non-trivial) recursive call via map, it fails because "map" passes `traverse_Foo` as argument. *)
Fail Fixpoint traverse_Foo (x : Foo) : bool :=
  match x with
  | Leaf => true
  | Node Fs => match map traverse_Foo Fs with | cons _ _ =>  true | _ => false end
  end.

(* This alternate definition of "map" hacks its way around: by defining the local fix, `f` is completely inlined after just an unfolding of `map'` *)
Definition map' {A B} (f: A -> B) (l : list A) : list B :=
  let fix loop l :=
      match l with
      | [] => []
      | x :: l => f x :: loop l
      end
  in loop l.

(* Hence the fixpoint goes through because Coq does this unfolding and hence can see it's safe *)
Fixpoint traverse_Foo (x : Foo) : bool :=
  match x with
  | Leaf => true
  | Node Fs => match map' traverse_Foo Fs with | cons _ _ =>  true | _ => false end
  end.

(* However this alternate definition has a shitty behavior w.r.t. `cbn`! *)
Goal forall A B f x xs, @map A B f (x::xs) = map' f (x::xs).
  intros.
  cbn.
 Abort.

Definition map' {A B} (f: A -> B) : list A -> list B :=
  fix map' l :=
      match l with
      | [] => []
      | x :: l => f x :: map' l
      end
.

Section S.
  Context {A B} (f:A -> B).
  Fixpoint map'  l :=
    match l with
    | [] => []
    | x :: l => f x :: map' l
    end.
End S.