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?

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

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.

Open an issue :)

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!

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: Oct 13 2024 at 01:02 UTC