[Agda] [ANNOUNCE] Agda 2.5.4 release candidate 1

[Jesper Cockx]

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:
https://github.com/agda/agda/issues/3085

-- Jesper

On Fri, May 25, 2018 at 3:10 PM, Nils Anders Danielsson <nad at cse.gu.se>
wrote:

> 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
>
> _______________________________________________
> 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/20180525/5bd7c340/attachment.html>