[Agda] error message in agda

[Jesper Cockx]

Hi Michel,

The reason why the error message does not mention the type of the
expression, is because it is an expression coming from the user code and
thus (in general) is not even necessarily well-typed. In general type
inference for Agda is undecidable so it would not always be possible to
print an error message of the form "expected vs inferred type" like in
Haskell. However, in cases where it is possible to infer the type (as in
this example) it might be a useful addition to Agda to also print the
inferred type. If you want, you could create a feature request on the issue
tracker (https://github.com/agda/agda/issues).

-- Jesper

On Sun, Mar 29, 2020 at 3:27 PM Michel Levy <michel.levy.imag at free.fr>
wrote:

> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200329/09b754a0/attachment.html>