[Agda] Why unification fail?

[Serge Leblanc]

In the following example, I'm incapable of matching the types although I
have tried the 'inspect' idiom. Would anyone please tell me the way?

En la sekva ekzemplo, mi nekapablas kongrui la tipojn kvankam mi provis
la idiomon 'inspect'. Ĉu iu bonvolus indiki al mi la vojon?

Sinceran dankon.

-- 
Serge Leblanc
------------------------------------------------------------------------
gpg --search-keys 0x67B17A3F
Fingerprint = 2B2D AC93 8620 43D3 D2C2 C2D3 B67C F631 67B1 7A3F
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190311/078e54aa/attachment.html>
-------------- next part --------------
module Chomp2 where

  open import Data.Nat --as ℕ
  open import Data.Nat.Properties


  --open import Function using (id ; _∘_)
  open import Relation.Binary.PropositionalEquality as PropEq
    using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ) -- ; _≗_ ; refl ; sym ; trans ; cong ; cong₂ ; cong-app)
  open PropEq.≡-Reasoning


  infixr 15 _∷_

  data 𝕃 : ℕ → Set where
    [_] : (o : ℕ) → 𝕃 o
    _∷_ : ∀ {n} → (x : ℕ) → (xs : 𝕃 n) → 𝕃 (x + n)

  ŋ : ∀ {n} → 𝕃 n → ℕ
  ŋ [ o ] = o
  ŋ (h ∷ t) = h + ŋ t

  --infix 25  _⪾_   -- U+2ABE ⪾

  +-distribˡ-⊔′ : (m k : ℕ) → suc (m + k) ⊔ m ≡ suc (k + m)
  +-distribˡ-⊔′ m k = begin
    suc (m + k) ⊔ m ≡⟨ cong (λ s → suc s ⊔ m) (+-comm  m k) ⟩
    suc (k + m) ⊔ m ≡⟨ sym (+-distribʳ-⊔ m (suc k) 0) ⟩
    suc (k + m)
    ∎

  +-distribˡ-⊔″ : (m k : ℕ) → suc (m + k) ⊔ m ≡ suc (m + k)
  +-distribˡ-⊔″ m k = begin
    suc (m + k) ⊔ m ≡⟨ +-distribˡ-⊔′ m k ⟩
    suc (k + m) ≡⟨ cong suc (+-comm k m) ⟩
    suc (m + k)
    ∎

  +-distribʳ-⊔′ : (m k : ℕ) → m ⊔ suc (m + k) ≡ suc (k + m)
  +-distribʳ-⊔′ m k = begin
    m ⊔ suc (m + k) ≡⟨ cong (λ s → m ⊔ suc s) (+-comm m k) ⟩
    m ⊔ suc (k + m) ≡⟨ sym (+-distribʳ-⊔ m 0 (suc k)) ⟩
    suc (k + m)
    ∎

  +-distribʳ-⊔″ : (m k : ℕ) → m ⊔ suc (m + k) ≡ suc (m + k)
  +-distribʳ-⊔″ m k = begin
    m ⊔ suc (m + k) ≡⟨ +-distribʳ-⊔′ m k ⟩
    suc (k + m) ≡⟨ cong suc (+-comm k m) ⟩
    suc (m + k)
    ∎

  l₁ = 3 ∷ 2 ∷ [ 4 ]
  l₂ = 3 ∷ 3 ∷ 5 ∷ [ 3 ]

  ⪾ : ∀ {n₁ n₂} → 𝕃 n₁ → 𝕃 n₂ → 𝕃 (n₁ ⊔ n₂)
  ⪾ l₁@([ o₁ ]) l₂@([ o₂ ]) with compare o₁ o₂
  ... | less m k rewrite +-distribʳ-⊔′ m k = suc k ∷ [ m ]
  ... | equal m rewrite ⊔-idem m = [ m ]
  ... | greater m k rewrite +-distribˡ-⊔′ m k = suc k ∷ [ m ]
  ⪾ {q₁} {q₂} l₁@([ o₁ ]) l₂@(h₂ ∷ t₂) with q₂ | compare q₁ q₂
  ... | ŋl | less m k rewrite +-distribʳ-⊔″ m k = {! (ŋl ∸ (ŋ (⪾ l₁ t₂))) ∷ ⪾ l₁ t₂ !}
  ... | ŋl | equal m rewrite ⊔-idem m = {! l₂  !}
  ... | ŋl | greater m k rewrite +-distribˡ-⊔′ m k = {! suc k ∷ l₂ !}
  ⪾ {q₁} {q₂} l₁@(h₁ ∷ t₁) l₂@([ o₂ ]) with q₁ | compare q₁ q₂
  ... | ŋl | less m k rewrite +-distribʳ-⊔′ m k = {! suc k ∷ l₁ !}
  ... | ŋl | equal m rewrite ⊔-idem m = {! l₁  !}
  ... | ŋl | greater m k rewrite +-distribˡ-⊔″ m k = {! (ŋl ∸ (ŋ (⪾ t₁ l₂))) ∷ ⪾ t₁ l₂ !}
  ⪾ {q₁} {q₂} l₁@(h₁ ∷ t₁) l₂@(h₂ ∷ t₂) with q₁ | q₂ | compare q₁ q₂
  ... | ŋl₁ | ŋl₂ | less m k rewrite +-distribʳ-⊔″ m k = {! (ŋl₂ ∸ ŋ (⪾ l₁ t₂)) ∷ ⪾ l₁ t₂ !}
  ... | ŋl₁ | ŋl₂ | equal m rewrite ⊔-idem m = {! (m ∸ ŋ (⪾ t₁ t₂)) ∷ ⪾ t₁ t₂ !}
  ... | ŋl₁ | ŋl₂ | greater m k rewrite +-distribˡ-⊔″ m k = {! (ŋl₁ ∸ ŋ (⪾ t₁ l₂)) ∷ ⪾ t₁ l₂ !}
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190311/078e54aa/attachment.sig>