[Agda] Let bindings unpacking irrefutable patterns

[Guillaume Allais]

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
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190215/f1fca388/attachment.sig>