<div dir="ltr"><div>I guess we should postpone checking a pattern let when the type is blocked on a meta, like we already do for pattern lambdas and top-level pattern matching definitions. I filed an issue here: <a href="https://github.com/agda/agda/issues/3085">https://github.com/agda/agda/issues/3085</a></div><div><br></div><div>-- Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, May 25, 2018 at 3:10 PM, Nils Anders Danielsson <span dir="ltr"><<a href="mailto:nad@cse.gu.se" target="_blank">nad@cse.gu.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 2018-05-25 13:04, Ulf Norell wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
This is a deliberate change to the type checker. See the second bullet point<br>
in the changelog here:<br>
<br>
<a href="https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching" rel="noreferrer" target="_blank">https://github.com/agda/agda/b<wbr>lob/release-2.5.4/CHANGELOG.md<wbr>#pattern-matching</a><br>
<br>
and the corresponding issue<br>
<br>
<a href="https://github.com/agda/agda/issues/2834" rel="noreferrer" target="_blank">https://github.com/agda/agda/i<wbr>ssues/2834</a><br>
<br>
In your case the fix is to add a type signature to p (warning, untested code):<br>
<br>
   map (\ (p : _ × _) → let (x , y) = p in (x , suc y))  ps<br>
</blockquote>
<br></span>
Issue #2834 is related to disambiguation of types based on patterns. In<br>
this case, given that ps is known to be a list of pairs, it should be<br>
possible for Agda to figure out what the type of p is without a type<br>
annotation. I guess the problem is that Agda checks the pattern eagerly,<br>
rather than waiting until the meta-variable ("_A_10") has been resolved.<span class="HOEnZb"><font color="#888888"><br>
<br>
-- <br>
/NAD</font></span><div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<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/mail<wbr>man/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>