The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Coq reduces terms like

(fix f (y : bool) := y) t

only if the argument term t starts with a constructor. 
The reference manual hints that this constraint is needed
to preserve strong normalization.

I tried to construct an example that would justify the constraint
but failed.  It seems to me that Coq restricts recursive applications
such that they are always guarded by matches, and that this makes
the constraint on fix reduction unnecessary.

Is there an example that justifies the constraint on fix reduction?