[Agda] more about insertion to a list

[Sergei Meshveliani]

Who can tell, please,
why the attached code (about 30 nonempty lines) is not type-checked
in Agda 2.6.0-e384ae7
?

Namely,  PE.refl  is reported in the end as having a wrong type.

The code is about the lemma  comm  below:

----------------------------
Mon = ℕ × ℕ

add : Mon → List Mon → List Mon
add (a , e) []                 =  (a , e) ∷ []
add (a , e) ((b , e') ∷ mons)  with compare e e'
...
    | tri> _ _ _ = (a , e ) ∷ (b , e') ∷ mons
... | tri< _ _ _ = (b , e') ∷ (add (a , e) mons)
... | tri≈ _ _ _ = (a + b , e) ∷ mons

comm :  ∀ a e b e' mons → add (a , e ) (add (b , e') mons) ≡
                          add (b , e') (add (a , e ) mons)
----------------------------


The question is about  
                comm a e b e' ((c , e₁) ∷ mons),

and only for the branch of  e > e';  e > e₁;  e' > e₁;  e' < e.

The branches are represented by cascading with the construct of
                         with compare x y | PE.inspect (compare x) y  
and by using `rewrite'.
In the considered brach, LHS and and RHS must normalize to the same
term:
  LHS =  add (a , e) (add (b , e') ((c , e₁) ∷ mons))   ≡[ e'>e₁ ]  
         add (a , e) ((b , e') ∷ (c , e₁) ∷ mons)       ≡[ e>e'  ]  
         (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons   

  RHS =  add (b , e') (add (a , e) ((c , e₁) ∷ mons))   ≡[ e>e₁ ]    
         add (b , e') ((a , e) ∷ (c , e₁) ∷ mons)       ≡[ e'<e ] 
         (a , e) ∷ (add (b , e') ((c , e₁) ∷ mons))     ≡[ e'>e₁ ]
         (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons                    
   
But Agda does not agree with this.

Am I missing something? May be I misuse `inspect' and `rewrite' ?
Can anybody fix the proof?

Thanks,

------
Sergei
-------------- next part --------------
open import Relation.Binary using (Tri; StrictTotalOrder)
open import Relation.Binary.PropositionalEquality as PE using (_≡_; _≢_)
open PE.≡-Reasoning renaming (_≡⟨_⟩_ to _≡[_]_; begin_ to ≡begin_;
                                                          _∎ to _≡end)
open import Data.Empty   using (⊥-elim) 
open import Data.Product using (_×_; _,_)
open import Data.List    using (List; []; _∷_)
open import Data.Nat     using (ℕ; _+_; _<_)
open import Data.Nat.Properties using (strictTotalOrder)


------------------------------------------------------------------------------
postulate anything : ∀ {a} {A : Set a} → A         -- for debug

open StrictTotalOrder strictTotalOrder using (compare)

Mon : Set 
Mon = ℕ × ℕ 

open Tri 

add : Mon → List Mon → List Mon

add (a , e) []                 =  (a , e) ∷ []
add (a , e) ((b , e') ∷ mons)  with compare e e'
...
    | tri> _ _ _ = (a , e ) ∷ (b , e') ∷ mons
... | tri< _ _ _ = (b , e') ∷ (add (a , e) mons)
... | tri≈ _ _ _ = (a + b , e) ∷ mons
  
------------------------------------------------------------------------------
comm :  ∀ a e b e' mons → add (a , e ) (add (b , e') mons) ≡ 
                          add (b , e') (add (a , e ) mons)

comm _ _ _ _ [] =  anything

comm a e b e' ((c , e₁) ∷ mons)  with compare e e' | PE.inspect (compare e) e'

comm a e b e' ((c , e₁) ∷ mons)
  | tri> e>e' _ _ | PE.[ eq-e>e' ] rewrite eq-e>e'
                                 with compare e e₁ | PE.inspect (compare e) e₁
comm a e b e' ((c , e₁) ∷ mons)
  | tri> e>e' _ _ | _ | tri> _ _ e>e₁ | PE.[ eq-e>e₁ ] rewrite eq-e>e₁
                               with compare e' e₁ | PE.inspect (compare e') e₁
comm a e b e' ((c , e₁) ∷ mons)
  | tri> e>e' _ _ | _ | tri> _ _ e>e₁ | _ | tri> _ _ e'>e₁ |
                                            PE.[ eq-e'>e₁ ] rewrite eq-e'>e₁
                                 with compare e' e | PE.inspect (compare e') e
comm a e b e' ((c , e₁) ∷ mons)
  | tri> e>e' _ _ | _ | tri> _ _ e>e₁ | _ | tri> _ _ e'>e₁ | _ | tri< e'<e _ _
                                            | PE.[ eq-e'<e ] rewrite eq-e'<e =
                                                                       PE.refl

comm a e b e' ((c , e₁) ∷ mons) | _ | _ =  anything


{- ----------------
  LHS =  add (a , e) (add (b , e') ((c , e₁) ∷ mons))   ≡[ e'>e₁ ]
         add (a , e) ((b , e') ∷ (c , e₁) ∷ mons)       ≡[ e>e'  ] 
         (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons

  RHS =  add (b , e') (add (a , e) ((c , e₁) ∷ mons))   ≡[ e>e₁ ]
         add (b , e') ((a , e) ∷ (c , e₁) ∷ mons)       ≡[ e'<e ]
         (a , e) ∷ (add (b , e') ((c , e₁) ∷ mons))     ≡[ e'>e₁ ]
         (a , e) ∷ (b , e') ∷ (c , e₁) ∷ mons
  -----------------
-}