Ltac2 should never elide top-level arguments of uncaught exceptions (constr failed to print)

[JasonGross]

Description of the problem

When I write

Ltac2 Type exn ::= [ Cannot_eliminate_functional_dependencies (constr) ].

and then do Control.zero (Cannot_eliminate_functional_dependencies term), it's not really very useful to get

Uncaught Ltac2 exception: RewriteRules.Reify.Cannot_eliminate_functional_dependencies (constr:(...))

I presume this is because the constr is too big, but even Set Printing Depth 10000000. does not get the constr to display. I cannot reproduce this issue in a small test case, but it can be seen at https://github.com/JasonGross/fiat-crypto/tree/xxx-coq-bug-ltac2-constr-msg, branch xxx-coq-bug-ltac2-constr-msg, with make TIMED=1 src/Rewriter/Passes/MultiRetSplit.vo

Coq Version

8.16

[SkySkimmer]

... means there was an error while printing, not a printing depth issue.

There are probably more ways to produce printing errors, but for instance

Require Import Ltac2.Ltac2.

Set Primitive Projections.
Record R A := mkR { r : A }.

Ltac2 Type exn ::= [ E (constr) ].

Set Printing Projections.
Set Printing Primitive Projection Parameters.

Ltac2 Eval Control.zero (E open_constr:(_.(r _))).
(* Error: Uncaught Ltac2 exception: E (constr:(...)) *)

Error printing doesn't have access to the evar map so when printing ?foo.(r _) it cannot recover the _ from ?foo and the printer hasn't been hardened against this particular case.

[JasonGross]

Hmmm, maybe user-level Ltac2 errors (if not other errors) should carry an (optional?) evar map under the hood, so printing works? I don't believe there are any evars in the constr I'm trying to print, but there might be binders (Var, I think?) that are no longer in scope at error printing?

`Message.of_constr` gives

(fun u2 : Z =>
             existT
               (RewriteRules.Compile.rewrite_ruleTP
                  IdentifiersGENERATED.Compilers.pattern.ident.arg_types_unfolded)
               {|
                 pattern.type_of_anypattern :=
                   type.base
                     (pattern.base.type.type_base Compilers.Z *
                      pattern.base.type.type_base Compilers.Z)%pbtype;
                 pattern.pattern_of_anypattern :=
                   #Compilers.pattern_ident_Z_cast2 @
                   (#(Compilers.pattern_ident_pair
                        (pattern.base.type.type_base Compilers.zrange)
                        (pattern.base.type.type_base Compilers.zrange)) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange) @
                    #(Compilers.pattern_ident_Literal Compilers.zrange)) @
                   (#Compilers.pattern_ident_Z_mul_split @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)) @
                    pattern.Wildcard
                      (type.base (pattern.base.type.type_base Compilers.Z)))
               |}
               {|
                 RewriteRules.Compile.rew_should_do_again := true;
                 RewriteRules.Compile.rew_with_opt := true;
                 RewriteRules.Compile.rew_under_lets := true;
                 RewriteRules.Compile.rew_replacement :=
                   fun (t t0 : ZRange.zrange)
                     (x0 x1
                      x2 : API.expr
                             (type.base (base.type.type_base Compilers.Z)))
                   =>
                   if
                    ((0 <=? 2 ^ bitwidth - 1)%Z && (0 <=? u1)%Z &&
                     (0 <=? u2)%Z &&
                     Definitions.Z.divideb (u1 + 1) (2 ^ bitwidth - 1 + 1) &&
                     Definitions.Z.divideb (u2 + 1) (2 ^ bitwidth - 1 + 1) &&
                     (negb (u1 =? 2 ^ bitwidth - 1)%Z
                      || negb (u2 =? 2 ^ bitwidth - 1)%Z) &&
                     ZRange.zrange_beq t
                       {| ZRange.lower := 0; ZRange.upper := u1 |} &&
                     ZRange.zrange_beq t0
                       {| ZRange.lower := 0; ZRange.upper := u2 |})%bool
                   then
                    Some
                      (RewriteRules.Reify.expr_value_to_rewrite_rule_replacement
                         (@RewriteRules.Compile.reflect_ident_iota
                            Compilers.base
                            IdentifiersBasicGENERATED.Compilers.ident
                            Compilers.base_interp Compilers.baseHasNat
                            Compilers.buildIdent Compilers.buildEagerIdent
                            Compilers.toRestrictedIdent
                            Compilers.toFromRestrictedIdent
                            Compilers.invertIdent Compilers.baseHasNatCorrect
                            Compilers.try_make_base_transport_cps var) true
                         (#Compilers.ident_Z_cast2 @
                          (###{| ZRange.lower := 0; ZRange.upper := u1 |},
                           ###{| ZRange.lower := 0; ZRange.upper := u2 |}) @
                          (#Compilers.ident_Z_cast2 @
                           (###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |},
                            ###{|
                                 ZRange.lower := 0;
                                 ZRange.upper := 2 ^ bitwidth - 1
                               |}) @
                           (#Compilers.ident_Z_mul_split @ $$x0 @ $$x1 @ $$x2))))
                   else None
               |})

[SkySkimmer]

In ocaml we capture the current env and evar map for this sort of thing. We could try to do something similar in ltac2, ie an API like

Ltac2 Type 'a printable.
Ltac2 create : 'a -> 'a printable. (* capture current env + evar map *)
Ltac2 get : 'a printable -> 'a.

and printer support

Not sure if good idea