<div dir="ltr"><div>This is a deliberate change to the type checker. See the second bullet point</div><div>in the changelog here:</div><div><br></div><div><a href="https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching">https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching</a></div><div><br></div><div>and the corresponding issue</div><div><br></div><div><a href="https://github.com/agda/agda/issues/2834">https://github.com/agda/agda/issues/2834</a></div><div><br></div><div>In your case the fix is to add a type signature to p (warning, untested code):</div><div><br></div><div>  map (\ (p : _ × _) → let (x , y) = p in (x , suc y))  ps</div><div><br></div><div>/ Ulf<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Fri, May 25, 2018 at 12:56 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</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 Sat, 2018-05-19 at 15:33 -0500, Andrés Sicard-Ramírez wrote:<br>
</span><span class="">> Dear all,<br>
> <br>
> The Agda Team is very pleased to announce the first release candidate<br>
> of Agda 2.5.4. We plan to release 2.5.4 in one week.<br>
><br>
</span>> []<br>
<span class="">> <br>
> Enjoy the RC and please test as much as possible.<br>
> <br>
<br>
</span>On <br>
<br>
------------------------------<wbr>-------------------<br>
open import Data.Product using (_×_; _,_)<br>
open import Data.List    using (List; map)<br>
open import Data.Nat     using (ℕ; suc)<br>
<br>
f : List (ℕ × ℕ) → List (ℕ × ℕ)<br>
f ps =<br>
     map (\p → let (x , y) = p in (x , suc y))  ps<br>
------------------------------<wbr>--------------------<br>
<br>
<br>
Agda 2.5.3.20180519  reports<br>
<br>
/home/mechvel/agda/tosave/<wbr>bugs/T.agda:7,21-26<br>
Cannot split on argument of non-datatype _A_10 ps<br>
when checking that the pattern x , y has type _A_10 ps<br>
<br>
Is this a bug in Agda?<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>