<div dir="ltr"><div>Hi Michel,</div><div><br></div><div>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 (<a href="https://github.com/agda/agda/issues">https://github.com/agda/agda/issues</a>).</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sun, Mar 29, 2020 at 3:27 PM Michel Levy <<a href="mailto:michel.levy.imag@free.fr">michel.levy.imag@free.fr</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
  

    
  
  <div>
    When you make an mistake on the type of an expression, you may get
    the following message<br>
    <br>
    5 != 4 of type ℕ <br>
    when checking that the expression s≤s {n = 4} (s≤s z≤n) <br>
    has type 2 ≤ 4<br>
    <br>
    Why agda doesn't give the type of the expression ? In my example
    (coming from an exercise of Philip Wadler)<br>
    I would have appreciated the longer message<br>
    <br>
    5 != 4 of type ℕ<br>
    when checking that the expression s≤s {n = 4} (s≤s z≤n) <br>
    <b>of type 2  ≤ 5 </b><br>
    has type 2 ≤ 4
    <div><br>
    </div>
    <div>-- <br>
      mail : <a href="mailto:michel.levy.imag@free.fr" target="_blank">michel.levy.imag@free.fr</a> <br>
      mobile : 06 59 13 42 53<br>
      web : <a href="http://michel.levy.imag.free.fr" target="_blank">michel.levy.imag.free.fr</a>
    </div>
  </div>

_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>