Jason Gross (Feb 21 2023 at 22:28): Jason Gross (Feb 21 2023 at 22:28):I have a template monad program with the fragment
_ <- tmPrint (@tmDefinition name ty v);;
n <- @tmDefinition name ty v;;
_ <- tmMsg "done";;
in the middle of it. The definition is monomorphic.
Using MetaCoq Run, my tactic program prints
[...]
(@tmDefinition@{tmMakeQuotationOfConstants.u6 tmMakeQuotationOfConstants.u2}
("q" ^ "tree")
(@inductive_quotation_of Type@{tmMakeQuotationOfConstants_qU}
KernameSet.Raw.tree)
{|
qinductive :=
{|
inductive_mind :=
(MPdot (MPdot (MPfile ["Kernames"; "Common"; "MetaCoq"]) "KernameSet")
"Raw", "tree");
inductive_ind := 0
|};
qinst := []
|})
Toplevel input, characters 0-163:
Error: Undeclared universe: MetaCoq.Quotation.ToTemplate.Common.Kernames.6016
(maybe a bugged tactic).
But if I take the tmDefinition that was printed, and run that manually with MetaCoq Run, there is no issue. What the heck could be going on here?
Jason Gross (Feb 21 2023 at 22:36):Self-contained code at https://github.com/MetaCoq/metacoq/issues/853
Jason Gross (Feb 28 2023 at 04:44):It seems that tmUnquote sometimes introduces new universes, for example in
Definition t : Type := nat.
Set Printing Universes.
MetaCoq Run (top <- tmCurrentModPath tt;; tmUnquote (tConst (top, "t") []) >>= tmPrint).
and it both fails to declare this universe (?), resulting in https://github.com/MetaCoq/metacoq/issues/853,
and it fails to impose the universe constraint that this universe should be lower than the second universe argument to tmUnquote, resulting in https://github.com/MetaCoq/metacoq/issues/842.
Where's the code that should be introducing the universes, and how should it be doing this? (Alternatively, is someone willing to submit a patch to fix these bugs?)
Jason Gross (Feb 28 2023 at 04:47):Presumably
| TmUnquote t ->
begin
try
debug Pp.(fun () -> str"Unquoting:" ++ Printer.pr_constr_env env evm t);
let t = reduce_all env evm t in
let evm, t' = denote_term env evm t in
let typ = Retyping.get_type_of env evm (EConstr.of_constr t') in
let evm, typ = Evarsolve.refresh_universes (Some false) env evm typ in
let make_typed_term typ term evm =
match Lazy.force texistT_typed_term with
| GlobRef.ConstructRef ctor ->
let (evm,c) = Evd.fresh_global (Global.env ()) evm (Lazy.force texistT_typed_term) in
let term = Constr.mkApp
(EConstr.to_constr evm c, [|EConstr.to_constr evm typ; t'|]) in
let evm, _ = Typing.type_of env evm (EConstr.of_constr term) in
(env, evm, term)
| _ -> CErrors.anomaly (str "texistT_typed_term does not refer to a constructor")
in
let env, evm, term = make_typed_term typ t' evm in
k ~st env evm term
with Reduction.NotArity -> CErrors.user_err (str "unquoting ill-typed term")
end
in template-coq/src/run_template_monad.ml needs to be modified somehow?
Jason Gross (Feb 28 2023 at 05:10):I guess that somehow in let evm, _ = Typing.type_of env evm (EConstr.of_constr term) in we're supposed to impose that the universes of the type fit within the universes that we're given somehow?
Jason Gross (Feb 28 2023 at 05:14):And somehow Evarsolve.refresh_universes is supposed to declare universes? Or we're supposed to thread a set of "pending universe declarations" which get declared and reset at tmDefinition / tmAxiom / tmLemma?
Last updated: Jun 04 2023 at 22:30 UTC