[Agda] Let bindings unpacking irrefutable patterns

[Jason -Zhong Sheng- Hu]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190214/66a33130/attachment.html>