[Agda] no-eta-equality

[Nils Anders Danielsson]

On 2016-09-29 16:55, Ulf Norell wrote:
> Unless you're using lots of nested sigmas (in which case you're on
> your own)

Nested sigmas can be useful, I have lots of library lemmas that apply to
sigma types.

If you use nested records, then copatterns can lead to a quadratic
blowup in the size of the code. Example:

   record R₁ : Set₂ where
     constructor _,_
     field
       A B : Set₁

   record R₂ : Set₂ where
     constructor _,_
     field
       f₁ : R₁
       C  : Set₁

   record R₃ : Set₂ where
     constructor _,_
     field
       f₂ : R₂
       D  : Set₁

   record R₄ : Set₂ where
     constructor _,_
     field
       f₃ : R₃
       E  : Set₁

   r₄ : R₄
   R₁.A (R₂.f₁ (R₃.f₂ (R₄.f₃ r₄))) = Set
   R₁.B (R₂.f₁ (R₃.f₂ (R₄.f₃ r₄))) = Set
   R₂.C        (R₃.f₂ (R₄.f₃ r₄))  = Set
   R₃.D               (R₄.f₃ r₄)   = Set
   R₄.E                      r₄    = Set

   r₄′ : R₄
   r₄′ = (((Set , Set) , Set) , Set) , Set

One can avoid this kind of blowup by splitting up the definition into
multiple, smaller definitions:

   r₁ : R₁
   R₁.A r₁ = Set
   R₁.B r₁ = Set

   r₂ : R₂
   R₂.f₁ r₂ = r₁
   R₂.C  r₂ = Set

   r₃ : R₃
   R₃.f₂ r₃ = r₂
   R₃.D  r₃ = Set

   r₄ : R₄
   R₄.f₃ r₄ = r₃
   R₄.E  r₄ = Set

> {-# MAGIC_REWRITE_INTO_COPATTERNS Σ #-}
>
> foo : (x , y) ≡ (x , y)
> foo = refl   -- error since the two pairs got rewritten into two different copattern definitions

I was imagining one pragma per definition, not one per type.

-- 
/NAD