[Agda] SOLVED: Cannot get definitional equality to trigger?

[Wolfram Kahl]

On Tue, Nov 22, 2011 at 01:14:33PM -0500, I wrote:
> intersection  :  {m₁ : Maybe K} → SUList m₁ → {m₂ : Maybe K} → SUList m₂
>               →  Σ[ m ∶  Maybe K ] SUList m
> intersection [] {m₂} _ = nothing , []
> intersection {m₁} _ [] = nothing , []
> intersection {just k₁} es₁ {just k₂} es₂ with compareK k₁ k₂
> -- ========= The following line should trigger for |intersection-drop₁|: =========
> intersection {just .(key e₁)} (e₁ ∶< e₁<es₁ <∶ es₁) {just k₂} es₂
>              | tri< k₁<k₂ ¬k₁≈k₂ ¬k₂<k₁ = intersection es₁ es₂
> intersection {just k₁} es₁ {just .(key e₂)} (e₂ ∶< e₂<es₂ <∶ es₂)
>              | tri> ¬k₁<k₂ ¬k₁≈k₂ k₂<k₁ = intersection es₁ es₂
> intersection {just .(key e₁)} (e₁ ∶< e₁<es₁ <∶ es₁) {just .(key e₂)} (e₂ ∶< e₂<es₂ <∶ es₂)
>              | tri≈ ¬k₁<k₂ k₁≈k₂ ¬k₂<k₁ = nothing , [] -- Truncated to isolate problem
> 
> -- I cannot get the second simplification to type-check:
> intersection-drop₁ : (e₁ : Elem) {m₁ : Maybe K} (e₁<es₁ : key e₁ <M m₁) (es₁ : SUList m₁)
>                      {k₂ : K} (es₂ : SUList (just k₂)) → (key e₁ <K k₂)
>                    → intersection (e₁ ∶< e₁<es₁ <∶ es₁) es₂ ≡ intersection es₁ es₂
> intersection-drop₁ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ with compareK (key e₁) k₂
> intersection-drop₁ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ | tri< k₁<k₂′ ¬b ¬c = {! ≡-refl !}
> [...]

At the heart of the problem seems to be the fact
that in intersection,  es₂  has previously been matched against [],
so that intersection-drop₁ needs to supply a constructor term instead of
just  es₂  to make the relevant intersection line applicable.
(I have a version with ``manual with'' working now.)
I had patterns there in intersection, too, originally,
but the termination checker did not like them...


Wolfram