Ill-typed with/rewrite desugaring

Question

The background is the data type of finite maps ordered by keys, as mentioned in this previous question:

open import Function
open import Relation.Binary renaming (IsEquivalence to IsEq)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module Data.Temp
   {k v ℓ ℓ′}
   {Key : Set k}
   (Value : Set v)
   {_<_ : Rel Key ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
   where

   open import Algebra.FunctionProperties
   open import Data.Product
   open IsStrictTotalOrder isStrictTotalOrder
   open import Level

   KV : Set (k ⊔ v)
   KV = Key × Value

   -- Adapted from the sorted lists presented in Why Dependent Types Matter (Altenkirch, Mcbride & McKinna).
   -- The lower bound is not tight.
   data FiniteMap (l : Key) : Set (k ⊔ v ⊔ ℓ) where
      [] : FiniteMap l
      _∷[_]_ : (kv : KV) → let k = proj₁ kv in l < k → (m : FiniteMap k) → FiniteMap l

   infixr 3 _∷[_]_

   -- Split into two definitions to help the termination checker.
   unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
   unionWith′ : ∀ {l} → Op₂ Value → (kv : KV) → let k = proj₁ kv in l < k → FiniteMap k → Op₁ (FiniteMap l)

   unionWith _ [] [] = []
   unionWith _ [] m = m
   unionWith _ m [] = m
   unionWith ∙ (k , v ∷[ k<l ] m) (k′ , v′ ∷[ k′<l ] m′) with compare k k′
   ... | tri< k<k′ _ _ = k , v ∷[ k<l ] unionWith ∙ m (k′ , v′ ∷[ k<k′ ] m′)
   ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = k , (v ⟨ ∙ ⟩ v′) ∷[ k<l ] unionWith ∙ m m′
   ... | tri> _ _ k′<k = k′ , v′ ∷[ k′<l ] unionWith′ ∙ (k , v) k′<k m m′

   unionWith′ _ (k , v) l<k m [] = k , v ∷[ l<k ] m
   unionWith′ ∙ (k , v) l<k m (k′ , v′ ∷[ k′<l ] m′) with compare k k′
   ... | tri< k<k′ _ _ = k , v ∷[ l<k ] unionWith ∙ m (k′ , v′ ∷[ k<k′ ] m′)
   ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = k , (v ⟨ ∙ ⟩ v′) ∷[ l<k ] unionWith ∙ m m′
   ... | tri> _ _ k′<k = k′ , v′ ∷[ k′<l ] unionWith′ ∙ (k , v) k′<k m m′

I'm now interested in proving that this type constructor preserves any commutative monoidal structure over A, where the monoid operation for finite maps is unionWith ∙ (and where ∙ is the commutative operation of the underlying monoid). I should point out that although unionWith ∙ is clearly commutative up to erasure of the bounds embedded in the maps, I'm not certain yet that it holds "on the nose", i.e. taking the bounds into account as well.

So, that caveat aside, I'm running into an error message trying to state a refined goal in my attempted proof. Here's the skeleton of the proof, with the problematic bit commented out:

comm : ∀ {l} (∙ : Op₂ Value) → Commutative _≡_ ∙ → 
                               Commutative _≡_ (unionWith {l} ∙)
comm ∙ _ [] [] = P.refl
comm ∙ _ [] (_ ∷[ _ ] _) = P.refl
comm ∙ _ (_ ∷[ _ ] _) [] = P.refl
comm {l} ∙ _ (k , v ∷[ k<l ] m) (k′ , v′ ∷[ k′<l ] m′) with compare k k′
... | tri< _ _ _ = {!!}
... | tri≈ _ k≡k′ _ {- rewrite P.sym k≡k′ -} = {!!}
... | tri> _ _ _ = {!!}

and here is the refined goal I would like to be able to insert for the k≡k′ case:

  begin
     k , (v ⟨ ∙ ⟩ v′) ∷[ l<k ] unionWith ∙ m m′
  ≡⟨ ? ⟩
     unionWith ∙ (k′ , v′ ∷[ k′<l ] m′) (k , v ∷[ k<l ] m)
  ∎ where
     open import Relation.Binary.EqReasoning (P.setoid (FiniteMap l))

But for this to be well-typed, I need that k ≡ k'. Following the definition of unionWith, I would like to insert the rewrite P.sym k≡k′ commented out in the code above.

Unfortunately I then get a rather nasty error message:

k′ != w of type Key
when checking that the type [scary stuff]
≡
(unionWith Value isStrictTotalOrder ∙ (w , v′ ∷[ k′<l ] m′)
 (k₁ , v₁ ∷[ k<l ] m)
 | compare w k₁)
of the generated with function is well-formed.

The issue of quality of with error messages is discussed here. Of course the quality of the error message is not my immediate concern, but it's not helping me understand whether I'm doing something wrong here.

Am I proceeding in the roughly the right way, i.e. using with and rewrite to refine my context to the point where I can start proving specific cases? (From this question, I think the answer is probably yes.) If so, what's causing the problem?

Answer 1

I'm going to answer my own question, as it seems I wasn't understanding how to use with clauses properly. Inside the k ≡ k' case, I need to give the full pattern again for the two finite maps, rather than just reusing the existing pattern via "...". Then I can put .k instead of k, and match the value of type k ≡ k' against refl (to justify the .k).

Then my refined goal type-checks (this version already in the scope of a suitable l, ∙ and Commutative _≡_ ∙):

     comm′ : Commutative (unionWith ∙)
     comm′ [] [] = P.refl
     comm′ [] (_ ∷[ _ ] _) = P.refl
     comm′ (_ ∷[ _ ] _) [] = P.refl
     comm′ (k , _ ∷[ _ ] _) (k′ , _ ∷[ _ ] _) with compare k k′
     ... | tri< _ _ _ = {!!}
     comm′ (k , v ∷[ k<l ] m) (.k , v′ ∷[ k′<l ] m′) | tri≈ _ P.refl _ =
       begin
           k , (v ⟨ ∙ ⟩ v′) ∷[ k<l ] unionWith ∙ m m′
        ≡⟨ {!!} ⟩
           unionWith ∙ (k , v′ ∷[ k′<l ] m′) (k , v ∷[ k<l ] m)
        ∎
     ... | tri> _ _ _ = {!!}

Do people think the original question is still useful? I could delete it otherwise.