Set Implicit Arguments.
Implicit Arguments LNil [A].

CoFixpoint append (A:Set) (l1 l2 : LList A) : LList A :=
  match l1 with
  | LNil => l2
  | LCons x xs => LCons x (append xs l2)
  end.

CoFixpoint cycle (A:Set) (input : LList A) : LList A :=
  match input with
  | LNil => LNil
  | LCons x xs => LCons x (append xs (cycle input))  (* "unguarded recursive call" *)
  end.

Section Foo.

Variable A:Set.
Variable l2:LList A.

CoFixpoint append0 l1 : LList A :=
  match l1 with
  | LNil => l2
  | LCons x xs => LCons x (append0 xs)
  end.

End Foo.

Definition append (A:Set) (l1 l2:LList A) := append0 l2 l1.

CoFixpoint cycle (A:Set) (input : LList A) : LList A :=
  match input with
  | LNil => LNil
  | LCons x xs => LCons x (append xs (cycle input))  (* "unguarded recursive call" *)
  end.