walker (Mar 15 2022 at 14:03): 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?
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
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.
Ali Caglayan (Mar 15 2022 at 14:10):Open an issue :)
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!
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". *)
I opened an issue:
https://github.com/coq/coq/issues/15813
Last updated: Dec 05 2023 at 12:01 UTC