Stream: Coq users

Topic: Error reporting


view this post on Zulip walker (Mar 15 2022 at 14:03):

Why doesn't coq use human-readable bound variable names in error reporting ?
See this error

Unable to unify
 "P ?M1359 ?M1360 --> P ?M1359 ?M1361"
with "P t1 x -->* P t1 z".

It would have been much easier if we got something that is not full of numbers, no?

view this post on Zulip Andrew Hirsch (Mar 15 2022 at 14:08):

Those are the unification variables that we talked about yesterday. That's always how they're reported, I guess because they (a) are autogenerated and (b) need to be separated from regular variables

view this post on Zulip Andrew Hirsch (Mar 15 2022 at 14:08):

That being said, I kinda agree the that current UX with unification variables could be improved, and this seems like a relatively easy place to improve them.

view this post on Zulip Ali Caglayan (Mar 15 2022 at 14:10):

Open an issue :)

view this post on Zulip James Wood (Mar 15 2022 at 14:42):

I think it would be a reasonable feature request to ask for the numbers be minimised before being displayed, for example. That would give:

Unable to unify
  "P ?M0 ?M1 --> P ?M0 ?M2"
with "P t1 x -->* P t1 z".

I have no idea what that would be like to implement, though!

view this post on Zulip Gaƫtan Gilbert (Mar 15 2022 at 14:44):

evars already do something like that

Axioms P Q : nat -> Prop.

Axiom f : forall n, P n.

Goal Q 0.
  Fail apply f.
  (* Unable to unify "P ?M150" with "Q 0". *)

  Fail refine (f _).
  (* The term "f ?n" has type "P ?n" while it is expected to have type "Q 0". *)

view this post on Zulip walker (Mar 15 2022 at 14:52):

I opened an issue:
https://github.com/coq/coq/issues/15813


Last updated: Feb 08 2023 at 23:03 UTC