Vas asks the question, how come the following doesn't satisfy the guardedness condition?

Set Implicit Arguments.

CoInductive LList (A:Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.

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.

The problems with this is that Coq is concerned that append will do something nasty like consume some constructors. If it did then cycle would not be productive.

The first solution I came up with was to inline append and simplify. That worked, but I didn't understand why Coq wasn't doing that in the original code. Coq will do reduction when checking the guardedness condition. The problem was that my simplifications was neither β nor ι reduction. I was substituting parametric parameters into the definition of append. If we make the parametric parameters actual function parameters, then Coq will be able to do this substitution by β reduction. One small problem is that A and l2 are the parametric parameters, and we will need to reorder the parameters so that all the parametric ones come first. However, a little notation will allow us to write the parameters in a natural order.

Set Implicit Arguments.

CoInductive LList (A:Set) : Set :=
| LNil : LList A
| LCons : A -> LList A -> LList A.

Implicit Arguments LNil [A].

Section Append.

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 Append.

Notation "'append' l1 l2" := (append0 l2 l1) (at level 0, l1 at level 0, l2 at level 0).

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

I'm not an expert on parsing levels, but setting everything to level 0 seems to work in the few cases I've tried. Defining an infix notation is probably more reasonable for append anyways.