Section Tree.
Variable A : Set.

Variant branch (T : Set) : Set :=
  | elem (a : A)
  | rest (t : T).

CoInductive tree : Set :=
  mk { obs : branch tree }.
End Tree.

Arguments elem {_} {_}.
Arguments rest {_} {_}.
Arguments mk {_}.
Arguments obs {_}.

CoFixpoint bind
  {A B : Set}
  (t : tree A)
  (f : A -> tree B)
  : tree B :=
  match obs t with
  | elem a => f a
  | rest t => mk (rest (bind t f))
  end.

Fail CoFixpoint iter
  {A I : Set}
  (f : I -> tree (A + I))
  (i : I) : tree A :=
  bind
    (f i)
    (fun ai =>
       match ai with
       | inl a => mk (elem a)
       | inr i => mk (rest (iter f i))
       end).

The command has indeed failed with message:
Recursive definition of iter is ill-formed.
In environment
iter : forall A I : Set, (I -> tree (A + I)) -> I -> tree A
A : Set
I : Set
f : I -> tree (A + I)
i : I
Unguarded recursive call in
"cofix bind (A B : Set) (t : tree A) (f : A -> tree B) : tree B :=
   match obs t with
   | elem a => f a
   | rest t0 => {| obs := rest (bind A B t0 f) |}
   end".
Recursive definition is:
"fun (A I : Set) (f : I -> tree (A + I)) (i : I) =>
 bind (f i)
   (fun ai : A + I =>
    match ai with
    | inl a => {| obs := elem a |}
    | inr i0 => {| obs := rest (iter A I f i0) |}
    end)".

Reset bind.

Definition bind
  {A B : Set}
  (t : tree A)
  (f : A -> tree B)
  : tree B :=
  let cofix help
        (t : tree A) : tree B :=
    match obs t with
    | elem a => f a
    | rest t => mk (rest (help t))
    end in
  help t.

CoFixpoint iter
  {A I : Set}
  (f : I -> tree (A + I))
  (i : I) : tree A :=
  bind
    (f i)
    (fun ai =>
       match ai with
       | inl a => mk (elem a)
       | inr i => mk (rest (iter f i))
       end).

CoFixpoint iter
  {A I : Set}
  (f : I -> tree (A + I))
  (i : I) : tree A :=
  (cofix help t := match obs t with
  | elem ai => match ai with
       | inl a => mk (elem a)
       | inr i => mk (rest (iter f i))
       end
  | rest t => mk (rest (help t))
  end)
    (f i)
.