Unrestricted Recursion (tmFix) in TemplateMonad

[fakusb]

Have there been thought on integrating an monadic operation to the TemplateMonad to allow unguarded recursion?

I have seen a few monadic programs defined in the monad requiring fuel to allow non-structural recursion. It seems to me that it should be possible to have a fixpoint operator tmFix : forall X, (X -> X) -> X -> TM X that removes the need for fuel. Or is there a theoretical/practical argument against having this?

[gmalecha]

This was also suggested in #133

[gmalecha]

An alternative is to make the definition coinductive, which would also work and might make it possible to prove termination after the fact using existing Coq mechanisms.

[mattam82]

We could add this, but one can already rely on unchecked fixpoints in Coq, no?

[JasonGross]

Implemented for the non-extractable monad in #790.