Right now it doesn't. Before I added the isCanonical condition, it looped because neither fixpoint combinators nor recursive definitions have normal forms with unrestricted unfolding. For a variable x, fix f x reduced to f (fix f x) which reduced to f (f (fix f x)) and so on. If a recursive definition is terminating, it only makes recursive calls with smaller arguments than the input. If the argument to fix f is neutral, no computation can make progress on it, so unfolding will not terminate. If the argument is canonical, the total recursive definitions necessarily make progress on it and only make recursive calls on smaller values, so unfolding will either terminate eventually, or hit a neutral value, in which case the fix f x application itself is blocked.

Btw, in untyped lambda calculus it is not actually true that every function is structurally larger than any of its result values, so this gist can still do infinite fix unfolding. In Coq however, the type system ensures (with some exotic exceptions) that a function is always larger than its results.

To be more precise, we want that the ordering on values which is generated by

• All constructors are larger than their fields
• f is larger than f x for any x

Is well-founded.

Ah, now I see it. So basically, we only evaluate Fix when we know that it's applied to an argument that can determine control flow (by some computation on it), so as to not unfold inner recursive calls indefinitely. Thanks for the explanation!