tmFixpoint combinator

[JasonGross]

Presumably this should be built in as a constructor instead of hacked in?

This is split off from #776

[JasonGross]

If we ever want to be able to prove things about tmFix (do we want to prove things about template-monad definitions?), then we could do

diff --git a/template-coq/theories/TemplateMonad/Common.v b/template-coq/theories/TemplateMonad/Common.v
index 60ac98e0..ec33d244 100644
--- a/template-coq/theories/TemplateMonad/Common.v
+++ b/template-coq/theories/TemplateMonad/Common.v
@@ -53,9 +53,18 @@ Monomorphic Variant locality :=
 | Discharge
 | Global (_ : import_status).

+(* Separate out the body into a separate definition to allow for proofs without non-termination *)
+Definition tmFix_body
+           {TM : TMInstance} {A B} (f : (A -> TemplateMonad TM B) -> (A -> TemplateMonad TM B))
+           (tmFix : unit -> A -> TemplateMonad TM B)
+  := f (fun a => tmFix tt a).
 (** XXX FIXME THIS IS A HACK *)
 Local Unset Guard Checking.
 Definition tmFix (TM : TMInstance) {A B} (f : (A -> TemplateMonad TM B) -> (A -> TemplateMonad TM B)) : A -> TemplateMonad TM B
   := (fix tmFix (dummy : unit) {struct dummy} : A -> @TemplateMonad TM B
-      := f (fun a => tmFix tt a)) tt.
+      := tmFix_body f tmFix) tt.
 Local Set Guard Checking.
+Global Strategy 1000 [tmFix].
+Global Strategy 10000 [tmFix_body].
+Lemma unfold_tmFix {TM A B f} : @tmFix TM A B f = f (@tmFix TM A B f).
+Proof. reflexivity. Qed.

[JasonGross]

I think this is actually inconsistent as per @yforster and @ppedrot on Zulip:

It's inconsistent for a version of TemplateMonad : Type -> Type I think - I'm not so sure about the Prop version
The reason is that

From MetaCoq.Template Require Import All Loader.
Local Unset Guard Checking.
Definition tmFix_body
           {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B))
           (tmFix : unit -> A -> TemplateMonad B)
  := f (fun a => tmFix tt a).
Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B
  := (fix tmFix (dummy : unit) {struct dummy} : A -> @TemplateMonad B
      := tmFix_body f tmFix) tt.
Local Set Guard Checking.

Definition bla := tmFix (fun f (x : unit) => tmQuote (f tt)).

Goal bla tt = tmQuote (bla tt).
Proof.
  reflexivity.
Qed.

And now for an inductive type x = C x for C being a constructor of this type is a problem
For instance, if I would write a function recursing on an inductive element of TemplateMonad and counting how often a tmQuote constructor occurs stacked on the top, then this equation lets me prove n = S n for n being size (bla tt)
and n = S n is inconsistent
Actually I learned about such problems from PMP not too long ago

I will close in favor of #790