[Agda] Explain this strange effect from the order of arguments (and provide a workaround, if possible)

[Martin Stone Davis]

(NB: Crossposted to http://stackoverflow.com/q/31913210/1312174)

While trying to come up with a solution to a question I posed [here](
http://stackoverflow.com/questions/31900036/proof-help-in-agda-node-balancing-in-data-avl),
I discovered that the acceptability (by Agda) of a refl proof depends in a
strange way on the order of arguments of a function that is called on one
side of the equation.

In code below, see how all but one of the bottom 4 theorems are proved with
refl. It's important to note that `join` and `join'` differ only in the
order of arguments. Correspondingly, I would think that the `thm`s that
invoke them should be proved equivalently, but apparently that is not so.

Why the discrepancy? Does this represent a bug in Agda? How would I prove
the remaining theorem (`thm1`)?

    open import Data.Nat
    open import Data.Product

    -- Stolen (with little modification) from Data.AVL

    data ℕ₂ : Set where
      0# : ℕ₂
      1# : ℕ₂

    infixl 6 _⊕_

    _⊕_ : ℕ₂ → ℕ → ℕ
    0# ⊕ n = n
    1# ⊕ n = suc n

    infix 4 _∼_⊔_

    data _∼_⊔_ : ℕ → ℕ → ℕ → Set where
      ∼+ : ∀ {n} →     n ∼ suc n ⊔ suc n
      ∼0 : ∀ {n} →     n ∼ n     ⊔ n
      ∼- : ∀ {n} → suc n ∼ n     ⊔ suc n

    max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m
    max∼ ∼+ = ∼-
    max∼ ∼0 = ∼0
    max∼ ∼- = ∼0

    ∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m
    ∼max ∼+ = ∼0
    ∼max ∼0 = ∼0
    ∼max ∼- = ∼+

    -- for simplicity, this tree has no keys
    data Tree : ℕ → Set where
      leaf : Tree 0
      node : ∀ {l u h}
             (L : Tree l)
             (U : Tree u)
             (bal : l ∼ u ⊔ h) →
             Tree (suc h)

    -- similar to joinˡ⁺ from Data.AVL

    join : ∀ {hˡ hʳ h : ℕ} →
           (∃ λ i → Tree (i ⊕ hˡ)) →
           Tree hʳ →
           (bal : hˡ ∼ hʳ ⊔ h) →
           ∃ λ i → Tree (i ⊕ (suc h))
    join (1# , node t₁
                    (node t₃ t₅ bal)
                    ∼+) t₇ ∼-  = (0# , node
                                            (node t₁ t₃ (max∼ bal))
                                            (node t₅ t₇ (∼max bal))
                                            ∼0)
    join (1# , node t₁ t₃ ∼-) t₅ ∼-  = (0# , node t₁ (node t₃ t₅ ∼0) ∼0)
    join (1# , node t₁ t₃ ∼0) t₅ ∼-  = (1# , node t₁ (node t₃ t₅ ∼-) ∼+)
    join (1# , t₁)            t₃ ∼0  = (1# , node t₁ t₃ ∼-)
    join (1# , t₁)            t₃ ∼+  = (0# , node t₁ t₃ ∼0)
    join (0# , t₁)            t₃ bal = (0# , node t₁ t₃ bal)

    -- just like join but with "bal" earlier in the argument list
    join' : ∀ {hˡ hʳ h : ℕ} →
           (bal : hˡ ∼ hʳ ⊔ h) →
           (∃ λ i → Tree (i ⊕ hˡ)) →
           Tree hʳ →
           ∃ λ i → Tree (i ⊕ (suc h))
    join' ∼- (1# , node t₁
                    (node t₃ t₅ bal)
                    ∼+) t₇  = (0# , node
                                            (node t₁ t₃ (max∼ bal))
                                            (node t₅ t₇ (∼max bal))
                                            ∼0)
    join' ∼-  (1# , node t₁ t₃ ∼-) t₅ = (0# , node t₁ (node t₃ t₅ ∼0) ∼0)
    join' ∼-  (1# , node t₁ t₃ ∼0) t₅ = (1# , node t₁ (node t₃ t₅ ∼-) ∼+)
    join' ∼0  (1# , t₁)            t₃ = (1# , node t₁ t₃ ∼-)
    join' ∼+  (1# , t₁)            t₃ = (0# , node t₁ t₃ ∼0)
    join' bal (0# , t₁)            t₃ = (0# , node t₁ t₃ bal)

    open import Relation.Binary.PropositionalEquality

    thm0  : ∀ {h : ℕ} (tl : Tree      h ) (tr : Tree (suc h)) → join (0# ,
tl) tr ∼+ ≡ (0# , node tl tr ∼+)
    thm0 tl tr = refl

    thm1  : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h)) → join (1# ,
tl) tr ∼+ ≡ (0# , node tl tr ∼0)
    thm1 tl tr = {!!} -- FIXME refl doesn't work here!

    thm0' : ∀ {h : ℕ} (tl : Tree      h ) (tr : Tree (suc h)) → join' ∼+
(0# , tl) tr ≡ (0# , node tl tr ∼+)
    thm0' tl tr = refl

    thm1' : ∀ {h : ℕ} (tl : Tree (suc h)) (tr : Tree (suc h)) → join' ∼+
(1# , tl) tr ≡ (0# , node tl tr ∼0)
    thm1' tl tr = refl -- refl works fine here, and all I did was switch
the order of arguments to join(')

If I try to prove `thm1` with refl, I get the following error:

    proj₁ (join (1# , tl) tr ∼+) != 0# of type ℕ₂
    when checking that the expression refl has type
    join (1# , tl) tr ∼+ ≡ (0# , node tl tr ∼0)

NB: This is using Agda 2.4.2.3 and the stdlib of the same version (pulled
from github [here](https://github.com/agda/agda-stdlib/tree/2.4.2.3).
--
Martin Stone Davis

Postal/Residential:
1223 Ferry St
Apt 5
Eugene, OR 97401
Talk / Text / Voicemail: (310) 699-3578 <3106993578>
Electronic Mail: martin.stone.davis at gmail.com
Website: martinstonedavis.com
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150810/199c0975/attachment.html