Any thoughts on what to do with https://github.com/MetaCoq/metacoq/pull/784?

I don't know if I'd be happy turning off guard checking (even locally) in MetaCoq.

What about adding it as another constructor to the template monad instead? (I'm not familiar with how the current template monad is hooked up, but I could try to write a PR for this.)

(Alternatively I could probably throw together a very hacky implementation in terms of `tmInferInstance`

, but that seems worse than the other two alternatives...)

Adding a fixpoint like this returning an inductive type is inconsistent, not sure whether you care about that.

my take would be that everybody who wants to run a non-terminating Fixpoint should locally unset guard checking - not least for transparency reasons

Do you really need the combinator Jason, or do you just use it a couple of times?

Oh, I guess having this as a constructor makes the inductive non-positive :-/ Grrr

@Yannick Forster I need it for `monad_trans`

in https://github.com/MetaCoq/metacoq/pull/776/files. I could fuel it instead, but that's sort of ugly. Do you see a better way?

@Pierre-Marie Pédrot What do you mean? Here's an implementation that passes the guard checker (only for the core template monad; if I want one in the extractable template monad I need a version of `tmUnquote`

for that (presumably routing through the native compiler, though I suspect that'll be painfully slow))

```
(** XXX FIXME THIS IS A HACK *)
Class HasFix := tmFix_ : forall {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)), A -> TemplateMonad B.
(* idk why this is needed... *)
#[local] Hint Extern 1 (Monad _) => refine TemplateMonad_Monad : typeclass_instances.
Definition tmFix {A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B)) : A -> TemplateMonad B
:= f
(fun a
=> tmFix <- tmInferInstance None HasFix;;
match tmFix with
| my_Some tmFix => tmFix _ _ f a
| my_None => tmFail "Internal Error: No tmFix instance"
end).
#[global] Hint Extern 0 HasFix => refine @tmFix : typeclass_instances.
```

I would have expected that you can define monad_trans as Fixpoint with disabled guardedness checking. That's similar to right now, but I think it's not inconsistent, whereas the definition of tmFix is

@Yannick Forster Note that I'm not wanting to run a fixpoint on the term level, but wanting an unbounded looping construct for the template monad itself. That is, I only want to have unbounded recursion inside `MetaCoq Run`

/ `run_template_program`

. The use-case is that I want to recursively look up the body of an inductive in the environment, and there's no way to efficiently determine ahead of time how many nested calls this will require (recursive quoting of the environment is too slow for my use-case).

whereas the definition of tmFix is

How is the definition of `tmFix`

inconsistent?

It allows me to inhabit `TemplateMonad False`

, but I can already inhabit that with `tmFail`

.

I've pushed the alternative to https://github.com/MetaCoq/metacoq/pull/790

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

Whether this really applies for the monad in `Prop`

I'm not sure, but it still looks strange to me

It should apply for subsingleton Props like Acc, but I guess that's not TemplateMonad?

Yes, direct computation of the size will fail because TemplateMonad is a proposition

And if the Prop isn't subsingleton, it seems the same reasoning should only prove proof irrelevance?

Okay, convinced, it won't be inconsistent for TemplateMonad. But the suggested `tmFix`

will also apply to the extractable monad `TM`

, and there it will be inconsistent (with a similar example but using `tmBind`

instead of `tmQuote`

)

Because `TM : Type -> Type`

Changing it to be a CoInductive might fix things once again, but given that there are easier ways out I'd say lets go with the easier ways

@Yannick Forster Oh, that is interesting, thanks for the example! What about if instead we do

```
Definition tmFix_body
{A B} (f : (A -> TemplateMonad B) -> (A -> TemplateMonad B))
(tmFix : unit -> A -> TemplateMonad B)
:= f (fun a => tmBind (tmReturn tmFix) (fun tmFix => tmFix tt a)).
```

?

Now the loopy recursion is blocked by `tmBind (tmReturn ...)`

, and I think there shouldn't be any way to bypass it. There's no way to directly inspect `tmFix`

for anything, and so you can't tell the difference between `tmReturn tmFix`

and something like `tmInferInstance`

, right?

My intuition the last time was that unsetting guard checking on inhabited return types is consistent. That was quickly debunked by PMP with an example. I at least can't come up with a problematic example for your suggested change, but I also don't have any intuition whether it's fine or not

I think the question boils down to is `C (fun _ => x) = x`

consistent for `Inductive T : Type := C (f : unit -> T).`

?

Ah, and I guess it's not, because we can pull the same counting trick with `match v with C f => S (f tt) end`

or something?

I think in the end the counting is not even necessary

```
Inductive T := C (f : unit -> T).
Goal forall x : T, C (fun _ => x) = x -> False.
Proof.
induction x.
intros E.
inversion E.
eapply (H tt).
rewrite <- H1.
f_equal. eauto.
Qed.
```

I used it earlier because dealing with the very dependent constructors of `TM`

is annoying

So my intuition would be that we're still in danger zone with this fix

Why would the unguarded `monad_trans`

be any better, then? I think I could probably exhibit an infinite codepath or similar from it.

I guess we should stick with the typeclass based one

If that's an option, I think it's a good option :) It's also not a problem to have inconsistent axioms around - after all MetaCoq comes with `Axiom todo : forall A, A`

- but it's good to limit them and make them easy to identify

For `monad_trans`

I don't have enough intuition to tell whether it's inconsistent or not - maybe it is

Last updated: Jul 13 2024 at 02:02 UTC