fix: Make quoting consider sort polymorphic types

This is a hacky fix that removes the commands from the inductive
and instead declares tmQuote as an axiom, just to avoid having to update
the complete inductive type to be sort polymorphic.

Author: TDiazT

template-rocq/theories/TemplateMonad/Core.v

@@ -46,12 +46,6 @@ Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Prop :=
 | tmCurrentModPath : unit -> TemplateMonad modpath
 
 (* Quoting and unquoting commands *)
-(* Similar to MetaRocq Quote Definition ... := ... *)
-| tmQuote : forall {A:Type@{t}}, A  -> TemplateMonad Ast.term
-(* Similar to MetaRocq Quote Recursively Definition but takes a boolean "bypass opacity" flag.
-  ([true] - quote bodies of all dependencies (transparent and opaque);
-   [false] -quote bodies of transparent definitions only) *)
-| tmQuoteRecTransp : forall {A:Type@{t}}, A -> bool(* bypass opacity? *) -> TemplateMonad program
 (* Quote the body of a definition or inductive. Its name need not be fully qualified *)
 | tmQuoteInductive : kername -> TemplateMonad mutual_inductive_body
 | tmQuoteUniverses : TemplateMonad ConstraintSet.t
@@ -70,6 +64,20 @@ Cumulative Inductive TemplateMonad@{t u} : Type@{t} -> Prop :=
 | tmInferInstance : option reductionStrategy -> forall A : Type@{t}, TemplateMonad (option_instance A)
 .
 
+(* Moving outside of the inductive definition only to make it sort polymorphic but
+   avoid having to update all of the TemplateMonad definition to be sort poylmorphic *)
+(* Similar to MetaRocq Quote Definition ... := ... *)
+Polymorphic Axiom tmQuote@{s; t u}
+  : forall {A : Type@{s;t}}, A -> TemplateMonad@{t u} Ast.term.
+
+(* Moving outside of the inductive definition only to make it sort polymorphic but
+   avoid having to update all of the TemplateMonad definition to be sort poylmorphic *)
+(* Similar to MetaRocq Quote Recursively Definition but takes a boolean "bypass opacity" flag.
+  ([true] - quote bodies of all dependencies (transparent and opaque);
+   [false] -quote bodies of transparent definitions only) *)
+Polymorphic Axiom tmQuoteRecTransp@{s; t u}
+  : forall {A : Type@{s;t}}, A -> bool(* bypass opacity? *) -> TemplateMonad@{t u} program.
+
 (** This version of [tmBind] flattens nesting structure; using it in deeply recursive template programs can speed things up drastically *)
 (** We use [tmBind] in the recursive position to avoid quadratic blowup in the number of [tmOptimizedBind]s *)
 Fixpoint tmOptimizedBind@{t u} {A B : Type@{t}} (v : TemplateMonad@{t u} A) : (A -> TemplateMonad@{t u} B) -> TemplateMonad@{t u} B

test-suite/_RocqProject.in

@@ -41,6 +41,7 @@ order_rec.v
 # primitive.v
 proj.v
 quotation_notations.v
+quote_global_sort.v
 reduction_test.v
 run_in_tactic.v
 safechecker_test.v
@@ -56,4 +57,3 @@ unfold.v
 univ.v
 vs.v
 ind_fresh_univ.v
-

test-suite/quote_global_sort.v

@@ -0,0 +1,19 @@
+From MetaRocq.Utils Require Import utils.
+From MetaRocq.Template Require Import All.
+Import MRMonadNotation.
+
+Set Universe Polymorphism.
+#[universes(polymorphic=no)]
+Sort Exc.
+
+MetaRocq Run (tmQuote Type@{Exc;Set} >>= tmPrint).
+
+Axiom ax_raise@{u} : forall (A : Type@{Exc;u}), A.
+
+MetaRocq Run (tmQuote ax_raise >>= tmPrint).
+
+(* This one requires -allow-rewrite-rules enabled
+Symbol raise@{u} : forall (A : Type@{Exc;u}), A.
+
+MetaRocq Run (tmQuote raise >>= tmPrint).
+*)