Hi,

I was reading chapter 7 of the mathcomp book. And this was the code associated.

When running

```
Fail Check forall T n (t : n.-tuple T),
let LHS := [LHS of size_tuple _] in
let RDX := size (rev t) in
[unify LHS with RDX].
```

The failure message on my computer and on the web version of coq is

```
The command has indeed failed with message:
In environment
T : Type
n : nat_eqType
t : n .-tuple T
LHS := (fix size (s : seq T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end)
((fix catrev (s1 s2 : seq T) {struct s1} : seq T := match s1 with
| [::] => s2
| x :: s1' => catrev s1' (x :: s2)
end) (let (tval, _) := t in tval) [::])(*...*) :
nat
RDX := size (rev t) : nat
The term "erefl LHS" has type "LHS = LHS"
while it is expected to have type "LHS = RDX" (cannot satisfy
constraint
"(fix size (s : seq ?T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end) ?t" == "(fix size (s : seq T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end)
((fix catrev (s1 s2 : seq T) {struct s1} : seq T := match s1 with
| [::] => s2
| x :: s1' => catrev s1' (x :: s2)
end) (let (tval, _) := t in tval) [::])").
```

But according to the book the message should be:

```
Error:
In environment
T : Type
n : nat
t : n .-tuple T
LHS := size (tval ?94 ?92 ?96) (*...*) : nat
RDX := size (rev (tval n T t)) : nat
The term "erefl ?95" has type "?95 = ?95" while
it is expected to have type "LHS = RDX".
```

What should I do to make the error message more readable?

Thanks!

Coq decided to unfold the definition of size in the error message, I'm afraid you can't do much

Last updated: Oct 03 2023 at 04:02 UTC