`tmUnquote` (or `tmDefinition`) fails to propagate universe constraints

[JasonGross]

From MetaCoq.Utils Require Import utils MCList.
From MetaCoq.Template Require Import MonadBasicAst MonadAst TemplateMonad Ast Loader.
Require Import Equations.Prop.Classes.
Require Import Coq.Lists.List.
Import ListNotations.

Local Set Primitive Projections.
Local Open Scope bs.
Import MCMonadNotation.

Class quotation_of {T} (t : T) := quoted_term_of : Ast.term.
Class ground_quotable T := quote_ground : forall t : T, quotation_of t.
Class inductive_quotation_of {T} (t : T)
  := { qinductive : inductive
     ; qinst : Instance.t
     ; qquotation : quotation_of t := tInd qinductive qinst }.

Require Import MSetPositive.
Definition tmMakeQuotationOfModule (m : qualid) : TemplateMonad _
  := cs <- tmQuoteModule m;;
     let dummy_inst := [] in
     ps <- monad_map
             (fun r
              => match r with
                 | ConstRef ((mp, name) as c)
                   => let c := tConst c dummy_inst in
                      '{| my_projT2 := cv |} <- tmUnquote c;;
                      let ty := quotation_of cv in
                      n <- @tmDefinition ("q" ++ name) ty c;;
                      tmReturn (Some (existT (fun T => T) ty n))
                 | IndRef ind
                   => let '(mp, name) := ind.(inductive_mind) in
                      let inst := dummy_inst in
                      let c := tInd ind inst in
                      '{| my_projT2 := cv |} <- tmUnquote c;;
                      let ty := inductive_quotation_of cv in
                      let v : ty := {| qinductive := ind ; qinst := inst |} in
                      n <- @tmDefinition ("q" ++ name) ty v;;
                      tmReturn (Some (existT (fun T => T) ty n))
                 | ConstructRef _ _ | VarRef _ => tmReturn None
                 end)
             cs;;
     tmReturn ps.
MetaCoq Run (tmMakeQuotationOfModule "Coq.MSets.MSetPositive.PositiveSet"%bs).
(* Error: Illegal application:
The term "@quotation_of" of type "forall T : Type, T -> Type"
cannot be applied to the terms
 "Type" : "Type"
 "PositiveSet.elt" : "Type"
The 1st term has type "Type@{MetaCoq.Quotation.ToTemplate.test.86+1}"
which should be coercible to "Type@{quotation_of.u0}".
*)

[JasonGross]

Workaround: If I define

Polymorphic Definition tmRetype {A} (x : A) : TemplateMonad A
  := qx <- tmQuote x;;
     tmUnquoteTyped A qx.

and then insert

_ <- tmRetype ty;;

before tmDefinition, then it goes through fine.

My guess is that tmUnquote@{t u} is not propagating the universe constraint that the type of the thing it's unquoting has to fit in Type@{u}.

[JasonGross]

Here is a smaller example showing how tmUnquote is failing:

From Coq Require Import Lists.List.
From MetaCoq.Utils Require Import bytestring monad_utils.
From MetaCoq.Template Require Import TemplateMonad Ast Loader.

Local Open Scope bs.
Import MCMonadNotation.
Import ListNotations.
Definition t : Type := nat.
Definition foo :=
  (top <- tmCurrentModPath tt;;
   ' {| my_projT1 := cty; my_projT2 := cv |} <- tmUnquote (tConst (top, "t") []);;
   @tmAxiom "bar" (@id Type cty);;
   tmReturn tt).
Set Printing Universes. Set Printing Implicit.
MetaCoq Run foo.
(* Error: Illegal application:
The term "@id" of type "ID"
cannot be applied to the terms
 "Type@{foo.u0}" : "Type@{foo.u0+1}"
 "Type@{MetaCoq.Quotation.ToTemplate.QuotationOf.Common.Kernames.Instances.1105}"
   : "Type@{MetaCoq.Quotation.ToTemplate.QuotationOf.Common.Kernames.Instances.1105+1}"
The 2nd term has type
 "Type@{MetaCoq.Quotation.ToTemplate.QuotationOf.Common.Kernames.Instances.1105+1}"
which should be coercible to "Type@{foo.u0}".
*)