Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

3 files changed, 22 insertions, 4 deletions

diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f82b9cef68..b7fefca22b 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -221,14 +221,22 @@ let print_if_is_coercion ref =
 (*******************)
 (* *)
 
+let pr_template_variables = function
+  | [] -> mt ()
+  | vars -> str "on " ++ prlist_with_sep spc UnivNames.pr_with_global_universes vars
+
 let print_polymorphism ref =
   let poly = Global.is_polymorphic ref in
   let template_poly = Global.is_template_polymorphic ref in
-  [ pr_global ref ++ str " is " ++ str
-      (if poly then "universe polymorphic"
+  let template_checked = Global.is_template_checked ref in
+  let template_variables = Global.get_template_polymorphic_variables ref in
+  [ pr_global ref ++ str " is " ++
+      (if poly then str "universe polymorphic"
        else if template_poly then
-	 "template universe polymorphic"
-       else "not universe polymorphic") ]
+         (if not template_checked then str "assumed " else mt()) ++
+         str "template universe polymorphic "
+         ++ h 0 (pr_template_variables template_variables)
+       else str "not universe polymorphic") ]
 
 let print_type_in_type ref =
   let unsafe = Global.is_type_in_type ref in
diff --git a/printing/printer.ml b/printing/printer.ml
index e3225fadd5..328082fbc2 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -854,6 +854,8 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
+                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =
@@ -873,10 +875,13 @@ struct
         Constant.CanOrd.compare k1 k2
     | Positive m1 , Positive m2 ->
         MutInd.CanOrd.compare m1 m2
+    | TemplatePolymorphic m1, TemplatePolymorphic m2 ->
+        MutInd.CanOrd.compare m1 m2
     | Guarded k1 , Guarded k2 ->
         GlobRef.Ordered.compare k1 k2
     | _ , Constant _ -> 1
     | _ , Positive _ -> 1
+    | _, TemplatePolymorphic _ -> 1
     | _ -> -1
 
   let compare x y =
@@ -937,6 +942,9 @@ let pr_assumptionset env sigma s =
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded gr ->
           hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"is assumed to be guarded.")
+      | TemplatePolymorphic m ->
+          hov 2 (safe_pr_inductive env m ++ spc () ++
+                 strbrk"is assumed template polymorphic on all its universe parameters.")
       | TypeInType gr ->
          hov 2 (safe_pr_global env gr ++ spc () ++ strbrk"relies on an unsafe hierarchy.")
     in
diff --git a/printing/printer.mli b/printing/printer.mli
index 788f303aee..d62d3789d3 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -192,6 +192,8 @@ type axiom =
   | Constant of Constant.t (* An axiom or a constant. *)
   | Positive of MutInd.t (* A mutually inductive definition which has been assumed positive. *)
   | Guarded of GlobRef.t (* a constant whose (co)fixpoints have been assumed to be guarded *)
+  | TemplatePolymorphic of MutInd.t (* A mutually inductive definition whose template polymorphism
+                                       on parameter universes has not been checked. *)
   | TypeInType of GlobRef.t (* a constant which relies on type in type *)
 
 type context_object =