[Agda] Let bindings unpacking irrefutable patterns

[Jason -Zhong Sheng- Hu]

That's because product itself having definitional eta expansion, isn't it? What about those having not? Let me try later.

Thanks,
Jason Hu

On Feb 15, 2019 08:24, Andreas Nuyts <andreas.nuyts at cs.kuleuven.be> wrote:
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<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda








_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto: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/25ec5e4e/attachment.html>