Reversible printing with sort printing and anonymous sort quality variables (combines #22155, #22283, #22310)

doc/changelog/08-vernac-commands-and-options/22155-printing-sorts-Added.rst

@@ -0,0 +1,9 @@
+- **Added:**
+  Added ``Printing Sorts`` flag, which displays sort variables that are
+  otherwise hidden (e.g. ``Type@{s;_}``) as well as universe instances
+  carrying sort qualities, with universe level variables replaced by ``_``,
+  making the sort structure visible without exposing internal universe
+  level names
+  (`#22155 <https://github.com/rocq-prover/rocq/pull/22155>`_,
+  fixes `#22153 <https://github.com/rocq-prover/rocq/issues/22153>`_,
+  by Jason Gross).

doc/changelog/08-vernac-commands-and-options/22283-reversible-printing-Added.rst

@@ -0,0 +1,11 @@
+- **Added:**
+  flags ``Printing Reversible Up To Unification``,
+  ``Printing Reversible Up To Conversion Modulo Sorts And Universes``,
+  ``Printing Reversible Up To Conversion Modulo Universes``,
+  ``Printing Reversible Up To Conversion Modulo Universe Unification`` and
+  ``Printing Reversible Up To Conversion``, which check, each time a term
+  is printed, that the printed form can be parsed and elaborated back to
+  a term equal to the original one up to the selected equivalence, and
+  progressively turn more printing options on until this is the case
+  (`#22283 <https://github.com/rocq-prover/rocq/pull/22283>`_,
+  written by Claude (Anthropic), for Jason Gross).

doc/changelog/08-vernac-commands-and-options/22310-printing-anon-qvars-Added.rst

@@ -0,0 +1,7 @@
+- **Added:**
+  flag ``Printing Sort Quality Variables Anonymously``, which prints
+  sort quality variables that cannot be referred to by name as ``_``
+  (which can be parsed back, denoting a fresh quality variable)
+  instead of their raw ``α``-names (which cannot)
+  (`#22310 <https://github.com/rocq-prover/rocq/pull/22310>`_,
+  written by Claude (Anthropic), for Jason Gross).

doc/sphinx/addendum/universe-polymorphism.rst

@@ -596,6 +596,18 @@ Printing universes
    terms apparently identical but internally different in the Calculus of Inductive
    Constructions.
 
+.. flag:: Printing Sorts
+
+   Turn this :term:`flag` on to display sort variables that are otherwise
+   hidden, with universe level variables replaced by ``_``.  Sorts without
+   sort variables (:g:`Type`, :g:`SProp`, :g:`Prop`, :g:`Set`) are printed
+   as usual, while sorts at a sort variable are printed like ``Type@{s;_}``
+   (or ``Type@{_}`` when :flag:`Printing Sort Qualities` is off).  Universe
+   instances of polymorphic references are displayed when they contain sort
+   qualities (with ``_`` in place of the universe levels) and stay hidden
+   otherwise.  Compared to :flag:`Printing Universes`, this makes the sort
+   structure visible without exposing internal universe level names.
+
 .. cmd:: Print {? Sorted } Universes {? Subgraph ( {* @debug_univ_name } ) } {? {| With | Without } Constraint Sources } {? @string }
    :name: Print Universes
 
@@ -1033,6 +1045,16 @@ It means that `s` and `s'` can respectively be instantiated to e.g., `Type` and
    become at the end of the definition unless it is unified with
    another rigid quality).
 
+.. flag:: Printing Sort Quality Variables Anonymously
+
+   When this :term:`flag` is on (it is off by default), sort quality
+   variables that cannot be referred to by name are printed as ``_``
+   (which, when parsed back, denotes a fresh quality variable) instead
+   of their raw representation — ``α`` followed by a number — which
+   cannot be parsed back. Quality variables that have a name (such as
+   the ``s`` of a ``@{s;u}`` universe declaration, in contexts where it
+   is bound) are printed by name as usual.
+
 Explicit Sorts
 ---------------
 

doc/sphinx/language/core/sorts.rst

@@ -18,6 +18,7 @@ Sorts
    | Type
    | Type @%{ _ %}
    | Type @%{ {? @qualid {| %| | ; } } @universe %}
+   | Type @%{ _ ; @universe %}
    universe ::= max ( {+, @universe_expr } )
    | _
    | @universe_expr

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -1164,6 +1164,101 @@ Printing constructions in full
 
    This flag is off by default.
 
+.. _reversible-printing:
+
+Checking that printed terms can be parsed back (reversible printing)
+--------------------------------------------------------------------
+
+Because notations, hidden implicit arguments, hidden coercions or hidden
+universe instances can make different terms print alike, the printed form
+of a term cannot always be parsed and elaborated back to the term it
+stands for. Rather than unconditionally making printing fully explicit as
+:flag:`Printing All` does, the following flags keep the current printing
+options, but check, each time a term is printed, that its printed form
+can be parsed and elaborated back to a term equal to the original one, up
+to the equivalence selected by the flag; when the check fails, printing
+options are progressively turned on — first :flag:`Printing Coercions`,
+then :flag:`Printing Implicit`, then unsetting :flag:`Printing Notations`,
+then :flag:`Printing Universes` (first with, then without notations),
+then :flag:`Printing Parentheses` and finally all the options implied by
+:flag:`Printing All` — until the printed form passes the check.
+
+These five flags are mutually exclusive: setting one of them unsets the
+others, and unsetting the currently set one turns the checks off
+entirely. All are off by default. Since every displayed term is re-parsed
+and re-elaborated (possibly several times), printing can become
+noticeably more expensive when one of these flags is set.
+
+.. flag:: Printing Reversible Up To Unification
+
+   The re-parsed form must unify with the original term: holes standing
+   for arguments that are not printed and universes introduced by the
+   re-elaboration may be instantiated by unifying against the original
+   term. This is the most permissive of the five checks; it accepts any
+   printed form that can denote the original term, even if only in a
+   context where the expected type is known.
+
+   .. warn:: The printed form of this term could not be re-parsed and re-elaborated to an equal term (up to ...), even with all printing options turned on.
+
+      If no printed form, however explicit, passes the check, the most
+      explicit one is printed anyway and this warning is emitted. This
+      happens for instance for terms mentioning universes that cannot be
+      referred to by name, such as the sort of ``Check Type``.
+
+.. flag:: Printing Reversible Up To Conversion Modulo Sorts And Universes
+
+   The printed form must re-elaborate on its own (without help from the
+   original term) to a term with no unresolved holes, and that term must
+   be convertible to the original one when sorts and universes are
+   ignored entirely: sort qualities (``SProp``, ``Prop``, ``Type``),
+   universe levels and universe instances may all differ. This is the
+   laxest of the conversion-based checks; in particular, unlike
+   :flag:`Printing Reversible Up To Conversion Modulo Universes` below,
+   it accepts a printed form whose re-elaboration lives at a different
+   sort quality than the original term.
+
+.. flag:: Printing Reversible Up To Conversion Modulo Universes
+
+   The printed form must re-elaborate on its own (without help from the
+   original term) to a term with no unresolved holes, and that term must
+   be convertible to the original one when universe levels (and the level
+   components of universe instances) are ignored, but *sort qualities
+   must agree*: ``Set`` and ``Type@{u}`` are accepted, but ``Prop``,
+   ``SProp`` and ``Type`` are pairwise distinguished. With this flag,
+   implicit arguments that can only be inferred from the type of the
+   original term get printed, and the universe levels of sorts (such as
+   the sort of ``Check Type``) generally do not, but the *sort quality*
+   part of a polymorphic instance is kept when it would otherwise
+   re-elaborate to a different quality.
+
+.. flag:: Printing Reversible Up To Conversion Modulo Universe Unification
+
+   Like :flag:`Printing Reversible Up To Conversion Modulo Universes`,
+   but instead of ignoring universe levels it lets the universes (and
+   sort qualities) introduced by the re-elaboration be unified against
+   the original ones, enforcing new universe (in)equalities as needed.
+   This is stricter than
+   :flag:`Printing Reversible Up To Conversion Modulo Universes` on
+   universe levels — a universe level cannot be unified with an
+   algebraic universe, so the sort of ``Check Type`` is printed
+   explicitly — but laxer on sort qualities, which get unified rather
+   than required to match syntactically.
+
+.. flag:: Printing Reversible Up To Conversion
+
+   Like :flag:`Printing Reversible Up To Conversion Modulo Universe
+   Unification`, but no new universe constraints are enforced: the
+   universe (in)equalities needed for convertibility must already be
+   valid in the current universe graph. With this flag, universe
+   instances of polymorphic constants generally need to be printed
+   (turning on :flag:`Printing Universes` for the terms where they
+   matter).
+
+For all five flags, when the printed expression stands for a term (as
+opposed to a type), the types of the original and re-elaborated terms
+are compared as well, so that, e.g., a printed form whose re-elaboration
+lives at a different universe instance is not considered reversible.
+
 .. _controlling-typing-flags:
 
 Controlling Typing Flags

doc/tools/docgram/common.edit_mlg

@@ -170,6 +170,7 @@ DELETE: [
 | test_leftsquarebracket_equal
 | test_old_sort_qvar
 | test_sort_qvar
+| test_sort_anon_qvar
 | test_ltac2_ident
 | test_doublepipe_univ_decl
 | test_doublepipe_cumul_univ_decl

doc/tools/docgram/fullGrammar

@@ -29,6 +29,7 @@ sort: [
 | "Type" "@{" "_" "}"
 | "Type" "@{" test_old_sort_qvar reference "|" universe "}"
 | "Type" "@{" test_sort_qvar reference ";" universe "}"
+| "Type" "@{" test_sort_anon_qvar "_" ";" universe "}"
 | "Type" "@{" universe "}"
 ]
 

doc/tools/docgram/orderedGrammar

@@ -285,6 +285,7 @@ sort: [
 | "Type"
 | "Type" "@{" "_" "}"
 | "Type" "@{" OPT [ qualid [ "|" | ";" ] ] universe "}"
+| "Type" "@{" "_" ";" universe "}"
 ]
 
 universe: [

interp/constrextern.ml

@@ -787,36 +787,44 @@ let extern_glob_sort_name uvars = function
       | None -> CRawType u
     end
 
-let extern_glob_quality uvars = function
+let extern_glob_quality ~anon uvars = function
   | GLocalQVar {v=Anonymous;loc} -> CQAnon loc
   | GLocalQVar {v=Name id; loc} -> CQVar (qualid_of_ident ?loc id)
   | GRawQVar q -> CRawQuality (QVar q)
   | GQuality q -> begin match UnivNames.qualid_of_quality uvars q with
     | Some qid -> CQVar qid
-    | None -> CRawQuality q
+    | None ->
+      (* A quality variable with no name has no parsable form; print it
+         as "_" (a fresh quality variable when parsed back) when
+         [anon]. *)
+      match q with
+      | QVar _ when anon -> CQAnon None
+      | _ -> CRawQuality q
     end
 
-let extern_relevance uvars = function
+let extern_relevance ~anon uvars = function
   | GRelevant -> CRelevant
   | GIrrelevant -> CIrrelevant
-  | GRelevanceVar q -> CRelevanceVar (extern_glob_quality uvars q)
+  | GRelevanceVar q -> CRelevanceVar (extern_glob_quality ~anon uvars q)
 
-let extern_relevance_info uvars = Option.map (extern_relevance uvars)
+let extern_relevance_info ~anon uvars = Option.map (extern_relevance ~anon uvars)
 
-let extern_glob_sort uvars (q, l) =
-  Option.map (extern_glob_quality uvars) q,
+let extern_glob_sort ~anon uvars (q, l) =
+  Option.map (extern_glob_quality ~anon uvars) q,
   map_glob_sort_gen (List.map (on_fst (extern_glob_sort_name uvars))) l
 
-let extern_instance uvars = function
+let extern_instance ~anon uvars = function
   | Some (ql,ul) ->
-    let ql = List.map (extern_glob_quality uvars) ql in
+    let ql = List.map (extern_glob_quality ~anon uvars) ql in
     let ul = List.map (map_glob_sort_gen (extern_glob_sort_name uvars)) ul in
     Some (ql,ul)
   | None -> None
 
-let extern_ref {vars; uvars} ref us =
+let anon_qvars eenv = eenv.flags.ExternFlags.anonymous_qvars
+
+let extern_ref ({vars; uvars; _} as eenv) ref us =
   extern_global (select_stronger_impargs (implicits_of_global ref))
-    (extern_reference vars ref) (extern_instance uvars us)
+    (extern_reference vars ref) (extern_instance ~anon:(anon_qvars eenv) uvars us)
 
 let extern_var ?loc id = CRef (qualid_of_ident ?loc id,None)
 
@@ -926,7 +934,7 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r =
              (* Otherwise... *)
                extern_applied_ref ~flags inctx
                  (select_stronger_impargs (implicits_of_global ref))
-                 (ref,extern_reference ?loc eenv.vars ref) (extern_instance eenv.uvars us) args)
+                 (ref,extern_reference ?loc eenv.vars ref) (extern_instance ~anon:(anon_qvars eenv) eenv.uvars us) args)
          | GProj (f,params,c) ->
              extern_applied_proj depth inctx scopes eenv f params c args
          | _ ->
@@ -1030,7 +1038,7 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r =
              in
              CCoFix (CAst.(make ?loc idv.(n)),Array.to_list listdecl))
 
-  | GSort s -> CSort (extern_glob_sort eenv.uvars s)
+  | GSort s -> CSort (extern_glob_sort ~anon:(anon_qvars eenv) eenv.uvars s)
 
   | GHole e -> CHole (Some e)
 
@@ -1056,7 +1064,7 @@ let rec extern depth0 inctx scopes (eenv:extern_env) r =
 
   | GArray(u,t,def,ty) ->
     CArray(
-      extern_instance eenv.uvars u,
+      extern_instance ~anon:(anon_qvars eenv) eenv.uvars u,
       Array.map (extern depth inctx scopes eenv) t,
       extern depth inctx scopes eenv def,
       extern_typ depth scopes eenv ty)
@@ -1070,7 +1078,7 @@ and sub_extern depth inctx (subentry,(_,scopes)) = extern depth inctx (subentry,
 
 and factorize_prod depth scopes eenv na r bk t c =
   let implicit_type = is_reserved_type ~flags:eenv.flags na t in
-  let r = extern_relevance_info eenv.uvars r in
+  let r = extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r in
   let aty = extern_typ depth scopes eenv t in
   let eenv = add_vname eenv na in
   let store, get = set_temporary_memory () in
@@ -1107,7 +1115,7 @@ and factorize_prod depth scopes eenv na r bk t c =
 
 and factorize_lambda depth inctx scopes eenv na r bk t c =
   let implicit_type = is_reserved_type ~flags:eenv.flags na t in
-  let r = extern_relevance_info eenv.uvars r in
+  let r = extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r in
   let aty = extern_typ depth scopes eenv t in
   let eenv = add_vname eenv na in
   let store, get = set_temporary_memory () in
@@ -1150,7 +1158,7 @@ and extern_local_binder depth scopes eenv = function
       let (assums,ids,l) =
         extern_local_binder depth scopes (on_eenv_vars (Name.fold_right Id.Set.add na) eenv) l in
       (assums,na::ids,
-       CLocalDef(CAst.make na, extern_relevance_info eenv.uvars r, extern depth false scopes eenv bd,
+       CLocalDef(CAst.make na, extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r, extern depth false scopes eenv bd,
                    Option.map (extern_typ depth scopes eenv) ty) :: l)
 
     | GLocalAssum (na,r,bk,ty) ->
@@ -1167,7 +1175,7 @@ and extern_local_binder depth scopes eenv = function
        | (assums,ids,l) ->
          let ty = if implicit_type then hole else ty in
          (na::assums,na::ids,
-          CLocalAssum([CAst.make na],extern_relevance_info eenv.uvars r,Default bk,ty) :: l))
+          CLocalAssum([CAst.make na],extern_relevance_info ~anon:(anon_qvars eenv) eenv.uvars r,Default bk,ty) :: l))
 
     | GLocalPattern ((p,_),_,bk,_) ->
       let p = mkCPatOr (List.map (extern_cases_pattern ~flags:eenv.flags eenv.vars) p) in
@@ -1305,7 +1313,7 @@ and extern_applied_proj depth inctx scopes eenv (cst,us) params c extraargs =
   let args = extern_args (extern depth true) eenv args in
   let imps = select_stronger_impargs (implicits_of_global ref) in
   let f = extern_reference eenv.vars ref in
-  let us = extern_instance eenv.uvars us in
+  let us = extern_instance ~anon:(anon_qvars eenv) eenv.uvars us in
   extern_projection ~flags:eenv.flags inctx (f,us) nparams args imps
 
 let extern inctx scopes eenv c : constr_expr = extern (init_depth eenv.flags) inctx scopes eenv c
@@ -1346,9 +1354,9 @@ let extern_type ?(goal_concl_style=false) ~(flags:PrintingFlags.t) env sigma ?im
   let r = Detyping.detype Detyping.Later ~isgoal:goal_concl_style ~avoid ~flags:flags.detype env sigma t in
   extern_glob_type ?impargs (extern_env ~flags:flags.extern env sigma) r
 
-let extern_sort ~universes ~qualities sigma s =
-  extern_glob_sort (Evd.universe_binders sigma)
-    (detype_sort ~universes ~qualities sigma s)
+let extern_sort ~universes ~sorts ~qualities ~anonymous_qvars sigma s =
+  extern_glob_sort ~anon:anonymous_qvars (Evd.universe_binders sigma)
+    (detype_sort ~universes ~sorts ~qualities sigma s)
 
 let extern_closed_glob ?(goal_concl_style=false) ?(inctx=false) ?scope ~(flags:PrintingFlags.t) env sigma t =
   let avoid = make_avoid goal_concl_style env in

interp/constrextern.mli

@@ -53,7 +53,7 @@ val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> qualid
 val extern_type : ?goal_concl_style:bool ->
   flags:PrintingFlags.t -> env -> Evd.evar_map ->
   ?impargs:Glob_term.binding_kind list -> types -> constr_expr
-val extern_sort : universes:bool -> qualities:bool -> Evd.evar_map -> Sorts.t -> sort_expr
+val extern_sort : universes:bool -> sorts:bool -> qualities:bool -> anonymous_qvars:bool -> Evd.evar_map -> Sorts.t -> sort_expr
 val extern_rel_context : flags:PrintingFlags.t -> env -> Evd.evar_map ->
   rel_context -> local_binder_expr list
 

parsing/g_constr.mlg

@@ -92,6 +92,12 @@ let test_sort_qvar =
     lk_ident >> lk_list lk_field >> lk_kw ";"
   end
 
+let test_sort_anon_qvar =
+  let open Procq.Lookahead in
+  to_entry "test_sort_anon_qvar" begin
+    lk_kw "_" >> lk_kw ";"
+  end
+
 let test_record_nowith =
   let open Procq.Lookahead in
   to_entry "test_record_nowith" begin
@@ -163,6 +169,9 @@ GRAMMAR EXTEND Gram
       | "Type"; "@{"; test_sort_qvar; q = reference; ";"; u = universe; "}" -> {
           Some (CQVar q), u
         }
+      | "Type"; "@{"; test_sort_anon_qvar; "_"; ";"; u = universe; "}" -> {
+          Some (CQAnon (Some loc)), u
+        }
       | "Type"; "@{"; u = universe; "}" -> { None, u } ] ]
   ;
   sort_quality_or_set: