adding error location to `Message.of_exn` · Ltac2

Would it be possible to tweak Message.of_exn to also print the location of the error? If so, would anyone object to it?
Details: In the goal:

 Example xx: exists a:Z, a=2.

Toplevel input, characters 8-12:
> exists (true+true).
>         ^^^^
Error:
In environment
thread_info : biIndex
_Σ : gFunctors
Σ : cpp_logic thread_info _Σ
gg : genv
modd : module ⊧ gg
The term "true" has type "bool" while it is expected to have type "Z".

  match Control.case (fun _ => exists (true+true)) with
  | Err e => Message.print (Message.of_exn e)
  | _ => ()
  end.

Internal
  (err:(In environment
  thread_info : biIndex
  _Σ : gFunctors
  Σ : cpp_logic thread_info _Σ
  gg : genv
  modd : module ⊧ gg
  The term "true" has type "bool" while it is expected to have type "Z".))

In particular, the error location information is missing. In my usecase, having the error location would be very useful.
Context:
I have written a proof engine that combines algorithmic reasoning (separation logic, arithmetic,..) with LLMs (when algorithms cannot figure stuff out like loop invariants, safe instantiation of existentials). One of my goals has been to write this engine mostly in Ltac2 rather than python/elisp/typescript. I have mostly succeeded: 99% of the logic is in Ltac2, but I do need to go out to a thin elisp shim because Ltac2 cannot do things like declare new lemmas/tactics for the proof or interpret strings (e.g. loop invariants produced by GPT) as constr. (it would be great if Ltac2 could interpret strings as constr in the current environment) I even do LLM queries in Ltac2.
The reason I want access to the error location is so that if GPT made an error in guessing the loop invariant, I can ask it to fix the error by providing as much helpful feedback as possible and I think the error location is crucial for that. I can do this part in the elisp shim but would highly prefer to do this in Ltac2 itself and that seems possible as long as Message.of_exn gives me the error location.

Also, I alluded to this in passing in the above paragraph, but would like to expand a bit: It would be nice to also add a function Constr.interpret : string -> constr which interprets a string as constr. Then I could take the string loop invariant produced by GPT and pass it to the loop tactic entirely in Ltac2. Currently, I have to exit to the elisp shim to do this.

Gaëtan Gilbert (Jun 24 2024 at 21:55):

the location is in the exninfo not the exn so of_exn isn't the right API, but we could expose a location type with APIs exninfo_loc : exninfo -> location option and Message.of_loc : location -> message

Abhishek Anand (Jun 24 2024 at 22:17):

Thanks. That makes sense and would work for me. Also, what do you think of the feasibility of exposing Constr.interpret : string -> constr?

Stream: Ltac2

Topic: adding error location to `Message.of_exn`

Abhishek Anand (Jun 24 2024 at 21:36):

Gaëtan Gilbert (Jun 24 2024 at 21:55):

Abhishek Anand (Jun 24 2024 at 22:17):