tmDefinition says that MetaCoq tactics are bugged and fail to declare universes

[JasonGross]

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

Local Open Scope bs.
Import MCMonadNotation.
Import ListNotations.

Local Set Primitive Projections.
Local Unset Universe Minimization ToSet.
Local Open Scope bs.
Import MCMonadNotation.

Class debug_opt := debug : bool.
Class quotation_of {T} (t : T) := quoted_term_of : Ast.term.
Class inductive_quotation_of {T} (t : T)
  := { qinductive : inductive
     ; qinst : Instance.t
     ; qquotation : quotation_of t := tInd qinductive qinst }.


Fixpoint tmRelaxSorts (U : Universe.t -> Universe.t) (t : term) {struct t} : term
  := match t with
     | tRel _
     | tVar _
     | tInt _
     | tFloat _
     | tConst _ _
     | tInd _ _
     | tConstruct _ _ _
       => t
     | tEvar ev args
       => tEvar ev (List.map (tmRelaxSorts U) args)
     | tCast t kind v
       => tCast (tmRelaxSorts U t) kind (tmRelaxSorts U v)
     | tProd na ty body
       => tProd na (tmRelaxSorts U ty) (tmRelaxSorts U body)
     | tLambda na ty body
       => tLambda na (tmRelaxSorts U ty) (tmRelaxSorts U body)
     | tLetIn na def def_ty body
       => tLetIn na (tmRelaxSorts U def) (tmRelaxSorts U def_ty) (tmRelaxSorts U body)
     | tApp f args
       => tApp (tmRelaxSorts U f) (List.map (tmRelaxSorts U) args)
     | tCase ci type_info discr branches
       => tCase ci (map_predicate (fun x => x) (tmRelaxSorts U) (tmRelaxSorts U) type_info) (tmRelaxSorts U discr) (map_branches (tmRelaxSorts U) branches)
     | tProj proj t
       => tProj proj (tmRelaxSorts U t)
     | tFix mfix idx
       => tFix (List.map (map_def (tmRelaxSorts U) (tmRelaxSorts U)) mfix) idx
     | tCoFix mfix idx
       => tCoFix (List.map (map_def (tmRelaxSorts U) (tmRelaxSorts U)) mfix) idx
     | tSort s => tSort (U s)
     end.

Definition tmRelaxSet (U : Universe.t) (t : term) : term
  := tmRelaxSorts (fun s => match option_map Level.is_set (Universe.get_is_level s) with
                            | Some true => U
                            | _ => s
                            end)
       t.

Definition tmRelaxType (U : Universe.t) (t : term) : term
  := tmRelaxSorts (fun s => match Universe.get_is_level s with
                            | Some _ => U
                            | _ => s
                            end)
       t.

Polymorphic Definition tmRetypeRelaxSet@{U a t u} {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
  := qx <- tmQuote x;;
     qU <- tmQuoteUniverse@{U _ _};;
     let qx := tmRelaxSet qU qx in
     tmUnquoteTyped A qx.

Polymorphic Definition tmRetypeRelaxType@{U a t u} {A : Type@{a}} (x : A) : TemplateMonad@{t u} A
  := qx <- tmQuote x;;
     qU <- tmQuoteUniverse@{U _ _};;
     let qx := tmRelaxType qU qx in
     tmUnquoteTyped A qx.
(* hack around https://github.com/MetaCoq/metacoq/issues/850 *)
Definition kername_of_global_reference (g : global_reference) : option kername
  := match g with
     | VarRef _ => None
     | ConstRef x => Some x
     | IndRef ind
     | ConstructRef ind _
       => Some ind.(inductive_mind)
     end.
Fixpoint dedup_grefs' (g : list global_reference) (seen : KernameSet.t) : list global_reference
  := match g with
     | nil => nil
     | g :: gs
       => match kername_of_global_reference g with
          | None => g :: dedup_grefs' gs seen
          | Some kn
            => if KernameSet.mem kn seen
               then dedup_grefs' gs seen
               else g :: dedup_grefs' gs (KernameSet.add kn seen)
          end
     end.
Definition dedup_grefs (g : list global_reference) : list global_reference
  := dedup_grefs' g KernameSet.empty.
Polymorphic Definition tmObj_magic {A B} (x : A) : TemplateMonad B
  := qx <- tmQuote x;;
     tmUnquoteTyped B qx.
Polymorphic Definition tmQuoteToGlobalReference {A} (n : A) : TemplateMonad global_reference
  := qn <- tmQuote n;;
     match qn with
     | tVar id => tmReturn (VarRef id)
     | tConst c u => tmReturn (ConstRef c)
     | tInd ind u => tmReturn (IndRef ind)
     | tConstruct ind idx u => tmReturn (ConstructRef ind idx)
     | _ => _ <- tmMsg "tmQuoteToGlobalReference: Not a global reference";;
            _ <- tmPrint n;;
            _ <- tmPrint qn;;
            tmFail "tmQuoteToGlobalReference: Not a global reference"
     end.

Universe tmMakeQuotationOfConstants_qU.
Definition tmMakeQuotationOfConstants {debug:debug_opt} (do_existing_instance : bool) (cs : list global_reference) : TemplateMonad unit
  := let warn_bad_ctx c ctx :=
       (_ <- tmMsg "tmMakeQuotationOfModule: cannot handle polymorphism";;
        _ <- tmPrint c;;
        _ <- tmPrint ctx;;
        tmReturn tt) in
     let tmDebugMsg s := (if debug
                          then tmMsg s
                          else tmReturn tt) in
     let tmDebugPrint {T} (v : T) := (if debug
                                      then tmPrint v
                                      else tmReturn tt) in
     let cs := firstn 5 (dedup_grefs cs) in
     cs <- tmEval cbv cs;;
     _ <- tmDebugMsg "tmMakeQuotationOfConstants: looking up module constants";;
     ps <- monad_map
             (fun r
              => _ <- tmDebugMsg "tmMakeQuotationOfConstants: handling";;
                 _ <- tmDebugPrint r;;
                 match r with
                 | ConstRef ((mp, name) as c)
                   => inst <- (cb <- tmQuoteConstant c false;;
                               match cb.(cst_universes) with
                               | Monomorphic_ctx => tmReturn []
                               | (Polymorphic_ctx (univs, constraints)) as ctx
                                 => _ <- warn_bad_ctx r ctx;;
                                    tmReturn []
                               end);;
                      let c := tConst c inst in
                      _ <- tmDebugMsg "tmMakeQuotationOfConstants: tmUnquote";;
                      '{| my_projT1 := cty ; my_projT2 := cv |} <- tmUnquote c;;
                      _ <- tmDebugMsg "tmMakeQuotationOfConstants: tmUnquote done";;
                      let ty := @quotation_of cty cv in
                      tmReturn [("q" ++ name, {| my_projT1 := ty ; my_projT2 := c |})]
                 | IndRef ind
                   => inst <- (mib <- tmQuoteInductive ind.(inductive_mind);;
                               match mib.(ind_universes) with
                               | Monomorphic_ctx => tmReturn []
                               | (Polymorphic_ctx (univs, constraints)) as ctx
                                 => _ <- warn_bad_ctx r ctx;;
                                    tmReturn []
                               end);;
                      let '(mp, name) := ind.(inductive_mind) in
                      let c := tInd ind inst in
                      _ <- tmDebugMsg "tmMakeQuotationOfConstants: tmUnquote";;
                      '{| my_projT1 := cty ; my_projT2 := cv |} <- tmUnquote c;;
                      _ <- tmDebugMsg "tmMakeQuotationOfConstants: tmUnquote done";;
                      let ty := inductive_quotation_of cv in
                      let v : ty := {| qinductive := ind ; qinst := inst |} in
                      tmReturn [("q" ++ name, {| my_projT1 := ty ; my_projT2 := v |})]
                 | ConstructRef _ _ | VarRef _ => tmReturn []
                 end)
             cs;;
     let ps := flat_map (fun x => x) ps in
     _ <- tmDebugMsg "tmMakeQuotationOfConstants: relaxing Set and retyping module constants";;
     ps <- monad_map
             (fun '(name, {| my_projT1 := ty ; my_projT2 := v |})
              => _ <- tmDebugMsg ("tmMakeQuotationOfConstants: relaxing " ++ name);;
                 _ <- tmDebugPrint ("before"%bs, v, ":"%bs, ty);;
                 ty <- tmRetypeRelaxType@{tmMakeQuotationOfConstants_qU _ _ _} ty;;
                 v <- tmObj_magic v;;
                 _ <- tmDebugPrint ("after"%bs, v, ":"%bs, ty);;
                 tmReturn (name, {| my_projT1 := ty ; my_projT2 := v |}))
             ps;;
     _ <- tmDebugMsg "tmMakeQuotationOfConstants: defining module constants";;
     ps <- monad_map
             (fun '(name, {| my_projT1 := ty ; my_projT2 := v |})
              => _ <- tmDebugPrint (@tmDefinition name ty v);;
                 n <- @tmDefinition name ty v;;
                 _ <- tmDebugMsg "tmMakeQuotationOfConstants: tmQuoteToGlobalReference";;
                 qn <- tmQuoteToGlobalReference n;;
                 tmReturn qn)
             ps;;
     _ <- (if do_existing_instance
           then
             _ <- tmDebugMsg "tmMakeQuotationOfConstants: making instances";;
             monad_map tmExistingInstance ps
           else tmReturn []);;
     tmReturn tt.

Definition tmMakeQuotationOfModule {debug:debug_opt} (do_existing_instance : bool) (m : qualid) : TemplateMonad _
  := cs <- tmQuoteModule m;;
     tmMakeQuotationOfConstants do_existing_instance cs.
Global Arguments tmMakeQuotationOfModule {_%bool} _%bool _%bs.


Definition replace_inductive_modpath (mp : modpath) (ind : inductive) : inductive
  := {| inductive_mind := (mp, snd ind.(inductive_mind)) ; inductive_ind := ind.(inductive_ind) |}.

Definition rebase_global_reference (mp : modpath) (g : global_reference) : global_reference
  := match g with
     | VarRef x => VarRef x
     | ConstRef (_, i) => ConstRef (mp, i)
     | IndRef ind => IndRef (replace_inductive_modpath mp ind)
     | ConstructRef ind idx => ConstructRef (replace_inductive_modpath mp ind) idx
     end.
Definition tmMakeQuotationOfModuleAndRebase {debug:debug_opt} (do_existing_instance : bool) (reference_mp : qualid) (new_base_mp : modpath) : TemplateMonad _
  := cs <- tmQuoteModule reference_mp;;
     let cs := List.map (rebase_global_reference new_base_mp) cs in
     tmMakeQuotationOfConstants do_existing_instance cs.
Global Arguments tmMakeQuotationOfModuleAndRebase {_%bool} _%bool _%bs _.
Polymorphic Definition tmExtractBaseModPathFromMod (mp : qualid) : TemplateMonad modpath
  := vs <- tmQuoteModule mp;;
     match option_map kername_of_global_reference (hd_error vs) with
     | Some (Some (mp, _)) => ret mp
     | _ => tmFail "tmExtractBaseModPathFromMod: module has no accessible constant with a kername"
     end.

Module qKernameSet.
  (* kludge around https://github.com/MetaCoq/metacoq/issues/847 *)
  Module KernameSet'. Include KernameSet. End KernameSet'.
  Module qRaw.
    Module Raw'. Include KernameSet.Raw. End Raw'.
    Instance:debug_opt := true.
    Set Printing Universes. Set Printing Implicit.
    Definition foo := Kernames_mp <- tmExtractBaseModPathFromMod "Kernames";; tmMakeQuotationOfModuleAndRebase false "Raw'" (MPdot (MPdot Kernames_mp "KernameSet") "Raw").
    MetaCoq Run foo.
    (* Error: Undeclared universe: MetaCoq.Quotation.ToTemplate.Common.foo.1787
(maybe a bugged tactic). *)

[JasonGross]

Here is a smaller example:

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

Local Open Scope bs.
Import MCMonadNotation.
Import ListNotations.
Class quotation_of {T} (t : T) := quoted_term_of : Ast.term.
Module KernameSetOrdProp := MSetProperties.OrdProperties KernameSet.
Definition foo :=
  (top <- tmCurrentModPath tt;;
   let gr := tConst (MPdot (MPdot (MPdot (MPdot top "KernameSetOrdProp") "ME") "OrderTac") "OTF", "t") [] in
   (' {| my_projT1 := cty; my_projT2 := cv |} <- tmUnquote gr;;
    ' {| my_projT1 := cty0; my_projT2 := cv0 |} <- tmUnquote gr;;
    ps <- ret [("qOrderTac__DOT__OTF__t",
                 {| my_projT1 := quotation_of cv; my_projT2 := gr |});
               ("qOrderTac__DOT__TO__t",
                 {| my_projT1 := quotation_of cv0; my_projT2 := gr |})];;
    monad_map (fun '(name, {| my_projT1 := ty; my_projT2 := v |})
               => n <- @tmDefinition name ty v;; tmReturn tt)
      ps);;
   tmReturn tt).
MetaCoq Run foo.

[JasonGross]

And a slightly smaller example:

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.
Class quotation_of {T} (t : T) := quoted_term_of : Ast.term.
Definition foo :=
  (top <- tmCurrentModPath tt;;
   let gr := tConst (top, "t") [] in
   x1 <- tmUnquote gr;;
   x2 <- tmUnquote gr;;
   let ' {| my_projT1 := cty; my_projT2 := cv |} := x1 in
   let ' {| my_projT1 := cty0; my_projT2 := cv0 |} := x2 in
   tmPrint (x1, x2);;
   ps <- ret [("foo0",
                {| my_projT1 := quotation_of cv; my_projT2 := gr |});
              ("foo1",
                {| my_projT1 := quotation_of cv0; my_projT2 := gr |})];;
   tmPrint ps;;
   monad_map
     (fun '(name, {| my_projT1 := ty; my_projT2 := v |})
      => n <- @tmDefinition name ty v;; tmReturn tt)
     ps;;
  tmReturn tt).
Set Printing Universes. Set Printing Implicit.
MetaCoq Run foo.