[Agda] pattern matching on records

[Twan van Laarhoven]

If I write

     simplify : {t₁ t₂ : U•} → (c₁ : t₁ ⟷ t₂) → (t₂ ⟷ t₁)
     simplify swap1₊ = swap2₊
     simplify swap2₊ = swap1₊

then agda colors this yellow, because there are unsolved metas. In particular, 
the type of swap1₊ fixes ∣ t₁ ∣, ∣ t₂ ∣ and (• t₁), but not (• t₂).

These problems go away if you change _⟷_ to

     data _⟷_ : U• → U• → Set where
       swap1₊  : ∀ {∣t₁∣ ∣t₂∣ •t₁} → •[ PLUS ∣t₁∣ ∣t₂∣ , inj₁ •t₁ ] ⟷
                                   •[ PLUS ∣t₂∣ ∣t₁∣ , inj₂ •t₁ ]
       swap2₊  : ∀ {∣t₁∣ ∣t₂∣ •t₂} → •[ PLUS ∣t₁∣ ∣t₂∣ , inj₂ •t₂ ] ⟷
                                   •[ PLUS ∣t₂∣ ∣t₁∣ , inj₁ •t₂ ]


Twan

On 2014-06-30 17:59, Amr Sabry wrote:
> How does one do "deep" pattern matches on records involving dot
> patterns. Is it even possible? In the attached program 'simplify' should
> have the "obvious" definition commented at the bottom but nothing I can
> write will allow Agda to infer or even pattern match on the implicit
> arguments. Any help would be appreciated. Thanks. --Amr
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>