Stream: MetaCoq

Topic: Frustrating universe errors?


view this post on Zulip 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?

view this post on Zulip Jason Gross (Feb 21 2023 at 22:36):

Self-contained code at https://github.com/MetaCoq/metacoq/issues/853

view this post on Zulip 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?)

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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: May 24 2024 at 22:02 UTC