[Agda] error message in agda

[Michel Levy]

When you make an mistake on the type of an expression, you may get the
following message

5 != 4 of type ℕ
when checking that the expression s≤s {n = 4} (s≤s z≤n)
has type 2 ≤ 4

Why agda doesn't give the type of the expression ? In my example (coming
from an exercise of Philip Wadler)
I would have appreciated the longer message

5 != 4 of type ℕ
when checking that the expression s≤s {n = 4} (s≤s z≤n)
*of type 2  ≤ 5 *
has type 2 ≤ 4

-- 
mail : michel.levy.imag at free.fr
mobile : 06 59 13 42 53
web : michel.levy.imag.free.fr
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200329/0c3fe8b4/attachment.html>