[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Nils Anders Danielsson]

On 2018-05-25 13:04, Ulf Norell wrote:
> This is a deliberate change to the type checker. See the second bullet point
> in the changelog here:
> 
> https://github.com/agda/agda/blob/release-2.5.4/CHANGELOG.md#pattern-matching
> 
> and the corresponding issue
> 
> https://github.com/agda/agda/issues/2834
> 
> In your case the fix is to add a type signature to p (warning, untested code):
> 
>    map (\ (p : _ × _) → let (x , y) = p in (x , suc y))  ps

Issue #2834 is related to disambiguation of types based on patterns. In
this case, given that ps is known to be a list of pairs, it should be
possible for Agda to figure out what the type of p is without a type
annotation. I guess the problem is that Agda checks the pattern eagerly,
rather than waiting until the meta-variable ("_A_10") has been resolved.

-- 
/NAD