I was trying to obtain all the constructors of the following inductive type:

```
Inductive C :=
| r : C
| g : nat -> C
| b : bool -> nat -> C.
```

I was able to do something like that with

```
MetaCoq Quote Recursively Definition qC := C.
Definition default_global_decl :=
ConstantDecl (Build_constant_body
(tVar ""%string)
None
(Monomorphic_ctx
(LevelSet.Mkt []%list, ConstraintSet.Mkt []%list))).
Definition default_kername : kername :=
(MPfile []%list, ""%string).
Definition default_kg : (kername * global_decl) :=
(default_kername, default_global_decl).
Definition aux (p : program) : list (list (ident * term * nat)) :=
let genv := fst p in
let kgd := List.hd default_kg genv in
let gd := snd kgd in
let oibs :=
match gd with
| ConstantDecl _ => []%list
| InductiveDecl mib => mib.(ind_bodies)
end in
map (fun o:one_inductive_body => o.(ind_ctors)) oibs.
Compute aux qC.
(*
= [[("r", tRel 0, 0);
("g",
tProd nAnon
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
inductive_ind := 0 |} []) (tRel 1), 1);
("b",
tProd nAnon
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "bool");
inductive_ind := 0 |} [])
(tProd nAnon
(tInd
{|
inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"],
"nat");
inductive_ind := 0 |} []) (tRel 2)), 2)]]
: list (list ((ident × term) × nat))
*)
```

How can something similar be done with `TemplateMonad`

? I tried

```
Definition aux'2 (qname : qualid) : TemplateMonad unit :=
x <- tmLocate1 qname ;;
(*x2 <- tmQuoteInductive x;;*)
match x with
| IndRef ind =>
oibs <- tmQuoteInductive ind.(inductive_mind) ;;
(* list one_inductive_body *)
rs <- map (fun o:one_inductive_body => o.(ind_ctors)) oibs ;;
tmPrint rs
| _ => tmFail "not an inductive"
end.
```

But that didn't work out. Got quite a long error.

The error was:

```
The following term contains unresolved implicit arguments:
(fun qname : qualid =>
x <- tmLocate1 qname;;
match x with
| VarRef i => tmFail "not an inductive"
| ConstRef k => tmFail "not an inductive"
| IndRef ind =>
oibs <- tmQuoteInductive (inductive_mind ind);;
rs <- map (fun o : one_inductive_body => ind_ctors o) oibs;;
tmPrint rs
| ConstructRef i n => tmFail "not an inductive"
end)
More precisely:
- ?Monad: Cannot infer this placeholder of type "Monad ?T" (no type class
instance found) in environment:
qname : qualid
- ?T: Cannot infer a subterm of type "Type -> Type" in the type of this
pattern-matching problem in environment:
qname : qualid
- ?T0: Cannot infer a subterm of type "Type" in the type of this
pattern-matching problem in environment:
qname : qualid
- ?A: Cannot infer the implicit parameter A of tmFail whose type is
"Type" in environment:
qname : qualid
x : global_reference
i : ident
- ?A0: Cannot infer the implicit parameter A of tmFail whose type is
"Type" in environment:
qname : qualid
x : global_reference
k : kername
- ?Monad0: Cannot infer this placeholder of type "Monad ?m" (no type class
instance found) in
environment:
qname : qualid
x : global_reference
ind : inductive
- ?Monad1: Cannot infer this placeholder of type "Monad ?m0" (no type class
instance found) in
environment:
qname : qualid
x : global_reference
ind : inductive
oibs : list one_inductive_body
- ?t: Cannot infer this placeholder of type "Type" in
environment:
qname : qualid
x : global_reference
ind : inductive
oibs : list one_inductive_body
- ?A1: Cannot infer the implicit parameter A of tmPrint whose type is
"Type" in
environment:
qname : qualid
x : global_reference
ind : inductive
oibs : list one_inductive_body
- ?m: Cannot infer this placeholder of type "Type -> Type" in
environment:
qname : qualid
- ?m0: Cannot infer this placeholder of type "Type -> Type" in
environment:
qname : qualid
- ?A2: Cannot infer the implicit parameter A of tmFail whose type is
"Type" in
environment:
qname : qualid
x : global_reference
i : inductive
n : nat
```

Unfortunately, type errors in template programs show up as these big ugly unreadable things. Whenever something like this happens you can read it as "type error" - don't try to read the message

I debug them by commenting out chunks of the program and replacing them by tmFail to see where the error is

My guess here would be that it is the `rs <- map`

map returns a list, whereas the `<-`

notation strictly expects a monadic value

So you need to replace this part by a plain `let`

ah, this is the problem where _all_ implicits are logged if _one_ of them fails to infer? Luckily Matthieu merged a fix for this error reporting in Coq 8.15 to be released soon (https://github.com/coq/coq/pull/13952)

Yes, I think it is trying to infer `Monad list`

If this is fixed now I'll move to 8.15 on all projects and never look back

Yannick Forster said:

So you need to replace this part by a plain

`let`

Tried using a `let`

, but couldn't get it right.

```
Definition aux'2 (qname : qualid) : TemplateMonad unit :=
x <- tmLocate1 qname ;;
(*x2 <- tmQuoteInductive x;;*)
match x with
| IndRef ind =>
oibs <- tmQuoteInductive ind.(inductive_mind) ;;
(* list one_inductive_body *)
let rs := (map (fun o:one_inductive_body => o.(ind_ctors)) oibs) in
tmPrint rs
| _ => tmFail "not an inductive"
end.
```

Is it wrong? What else could I be missing?

Still the same error message?

Did you try finding the problem by replacing parts of the program with `tmFail "test"`

?

Ah: You're mapping on `oibs`

, but you want to map on `oibs.(ind_bodies)`

Yannick Forster said:

Did you try finding the problem by replacing parts of the program with

`tmFail "test"`

?

When we use `tmFail`

to debug, we got to remove the code following it, right?

As in

```
Definition aux'2_1 (qname : qualid) : TemplateMonad unit :=
x <- tmLocate1 qname ;;
(*x2 <- tmQuoteInductive x;;*)
match x with
| IndRef ind =>
oibs <- tmQuoteInductive ind.(inductive_mind) ;;
(* list one_inductive_body *)
tmFail "test"
(* Nothing should come after this, right? *)
(*
rs <- map (fun o:one_inductive_body => o.(ind_ctors)) oibs ;;
tmPrint rs *)
| _ => tmFail "not an inductive"
end.
```

Yannick Forster said:

Ah: You're mapping on

`oibs`

, but you want to map on`oibs.(ind_bodies)`

I don't know why I thought what I had named `oibs`

was a `list one_inductive_body`

when it was actually a `mutual_inductive_body`

.. :grimacing:

I modified it to

```
Definition aux'2 (qname : qualid) : TemplateMonad unit :=
x <- tmLocate1 qname ;;
(*x2 <- tmQuoteInductive x;;*)
match x with
| IndRef ind =>
mib <- tmQuoteInductive ind.(inductive_mind) ;;
(* mib : mutual_inductive_body *)
(* o.(ind_ctors) : list one_inductive_body *)
let rs := map (fun o:one_inductive_body => o.(ind_ctors))
mib.(ind_bodies) in
tmPrint rs
(* rs : list (list ((ident * term) * nat) ) *)
| _ => tmFail "not an inductive"
end.
```

and it got defined without error.

But upon running it, it looks like it's not being evaluated.

```
MetaCoq Run (aux'2 "C").
```

Output was:

```
(map (fun o : one_inductive_body => ind_ctors o)
(ind_bodies
{|
ind_finite := Finite;
ind_npars := 0;
ind_params := [];
ind_bodies := [{|
ind_name := "C";
ind_type := tSort
(Universe.from_kernel_repr
(Level.lSet, false) []);
ind_kelim := InType;
ind_ctors := [("r", tRel 0, 0);
("g",
tProd nAnon
(tInd
{|
inductive_mind := (
MPfile
["Datatypes"; "Init"; "Coq"],
"nat");
inductive_ind := 0 |} [])
(tRel 1), 1);
("b",
tProd nAnon
(tInd
{|
inductive_mind := (
MPfile
["Datatypes"; "Init"; "Coq"],
"bool");
inductive_ind := 0 |} [])
(tProd nAnon
(tInd
{|
inductive_mind := (
MPfile
["Datatypes"; "Init"; "Coq"],
"nat");
inductive_ind := 0 |} [])
(tRel 2)), 2)];
ind_projs := [] |}];
ind_universes := Monomorphic_ctx
(LevelSetProp.of_list [], ConstraintSet.empty);
ind_variance := None |}))
```

Yes, it really isn't evaluated :) You need `res <- tmEval cbn rs ;; tmPrint res`

You have a lot of control over evaluation in the TemplateMonad

Got it working now. Thanks a lot!

Julin S has marked this topic as resolved.

Last updated: May 31 2023 at 09:01 UTC