[Agda] Let bindings unpacking irrefutable patterns

[Andreas Nuyts]

It doesn't really matter, though, as Agda acknowledges that they are 
definitionally equal:

```
module LetPatterns where

open import Data.Product
open import Relation.Binary.PropositionalEquality

_∋_ : (A : Set) (a : A) → A
A ∋ a = a

foo : ∀ {A : Set} {B : ∀ (a : A) → Set} → (p : Σ A B) → proj₁ p ≡ proj₁ p
foo tup = let x , y = tup in (x ≡ proj₁ tup) ∋ refl
```

Andreas

On 15/02/19 13:08, Guillaume Allais wrote:
> Hi,
>
> This is a known problem (https://github.com/agda/agda/issues/1181)
> and unfortunately has not been fixed yet. It's in the 'icebox' meaning
> that if anyone contributes a fix, it'll be gladly accepted but there
> is no set deadline for it.
>
> Cheers,
> --
> gallais
>
> On 14/02/2019 23:28, Jason -Zhong Sheng- Hu wrote:
>> Hi,
>>
>> consider following program:
>>
>> ```
>> foo : ∀ {A : Set} {B : ∀ (a : A) → Set} → Σ A B → Set
>> foo tup = let x , y = tup in {!!}
>> ```
>>
>> In the hole there, we can see the following environment:
>>
>> ```
>> Goal: Set
>> ————————————————————————————————————————————————————————————
>> y   : .B (proj₁ tup)
>> x   : .A
>> tup : Σ .A .B
>> .B  : .A → Set
>> .A  : Set
>> ```
>>
>> I think the highlighted part is quite unexpected, as I would consider let bindings have the same effect as with patterns when dealing with irrefutable patterns. In particular, I'd hope y has type `.B x` in this case. Is this a bug or expected behavior? I am asking this because it's quite confusing as it seems to indicate let bindings are very weak in agda.
>>
>> Sincerely Yours,
>>
>> Jason Hu
>>
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
> _______________________________________________
> 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/20190215/bc1e008d/attachment.html>