[Agda] Cannot get definitional equality to trigger?

[Wolfram Kahl]

-- --------- Core2i.agda -------------
{-
I am defining a datatype |SUList| of sorted lists with unique keys;
while trying to prove a propositional equality |intersection-drop₁|
about a special case of intersection,
I cannot get the relevant line, indicated in the definition of |intersection|,
to trigger.
(I cut out the most important part of the definition of |intersection|
 since it does not contribute to the problem,
 but doubles the size of the file.)
I tried to replace the |with| with a mutal definition,
essentially defining the |with| function manually,
but that does not change anything.

Can anybody help me understand what is going on here,
and how to get this to work?

(My Agda and standard library are from November 12.)


Wolfram
kahl at cas.mcmaster.ca
-}

open import Level renaming (_⊔_ to _⊍_)

open import Relation.Binary using
  ( Tri ; tri< ; tri≈ ; tri> 
  ; StrictTotalOrder ; module StrictTotalOrder
  ; module IsEquivalence
  )

open import Relation.Binary.PropositionalEquality using ( _≡_ ; inspect ; [_])
  renaming (refl to ≡-refl ; sym to ≡-sym ; subst to ≡-subst)

open import Data.Maybe using (Maybe ; nothing ; just ; maybe)
open import Data.Product using ( proj₁ ; proj₂ ; Σ ; _×_ ; _,_ )
open import Data.Empty using (⊥-elim)

module Core2i
    (ℓE : Level) (Elem : Set ℓE)
    (ℓK ℓk₁ ℓk₂ : Level) (Key : StrictTotalOrder ℓK ℓk₁ ℓk₂)
    (key : Elem → StrictTotalOrder.Carrier Key)
  where

open StrictTotalOrder Key using ()
  renaming (Carrier to K ; _≈_ to _≈K_ ; _<_ to _<K_ ; compare to compareK)

-- Generalised unit:
record ⊤ {k : Level} : Set k where constructor tt

infixr 14 _∶<_<∶_
infix   5 _<M_

_<M_ : K → Maybe K → Set ℓk₂
k <M nothing = ⊤
k <M (just k′) = k <K k′

data SUList : Maybe K → Set (ℓE ⊍ ℓK ⊍ ℓk₂) where
  [] : SUList nothing
  _∶<_<∶_ : (e : Elem) → {m : Maybe K} (e<es : key e <M m) → (es : SUList m) → SUList (just (key e))

-- The type of the two arguments of an |SUList| intersection is not sufficient
-- to determine the type of the result:

-- Original definition
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

{- A |mutual| definition without ``|with|'' has the same effect. -}

-- The first simplification works easily:
intersection-[]₂  : {m₁ : Maybe K} → (es₁ : SUList m₁) → intersection es₁ [] ≡ (nothing , [])
intersection-[]₂ [] = ≡-refl
intersection-[]₂ (e₁ ∶< e₁<es₁ <∶ es₁)  = ≡-refl

-- 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!}
intersection-drop₁ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ | tri≈ ¬k₁<k₂ b ¬c = ⊥-elim (¬k₁<k₂ k₁<k₂)
intersection-drop₁ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ | tri> ¬k₁<k₂ ¬b c = ⊥-elim (¬k₁<k₂ k₁<k₂)

{- ===================================
just (key e₁) != .m₁ of type Maybe K
when checking that the expression ≡-refl has type
intersection (e₁ ∶< e₁<es₁ <∶ es₁) es₂ ≡ intersection es₁ es₂
=================================== -}

-- I cannot get inspect on steroids to help either:
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 (e₁ ∶< e₁<es₁ <∶ es₁) es₂
                       | inspect (intersection (e₁ ∶< e₁<es₁ <∶ es₁)) es₂
intersection-drop₁′ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ | tri< k₁<k₂′ ¬b ¬c | es | [ eq ] = {!!}
intersection-drop₁′ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ | tri≈ ¬k₁<k₂ b ¬c | _ | _ = ⊥-elim (¬k₁<k₂ k₁<k₂)
intersection-drop₁′ e₁ e₁<es₁ es₁ {k₂} es₂ k₁<k₂ | tri> ¬k₁<k₂ ¬b c | _ | _ = ⊥-elim (¬k₁<k₂ k₁<k₂)

{- ===================================
just (key e₁) != .m₁ of type Maybe K
when checking that the expression ≡-sym eq has type
es ≡ intersection es₁ es₂
=================================== -}