[Agda] A sticky refusal

[Martin Stone Davis]

NB Crossposted to http://stackoverflow.com/q/32021121/1312174.

This question is about

* how to help Agda get unstuck when solving unification problems, and
* how to convince Agda to solve a "heterogeneous constraint" (whatever that
means)

The complete code for my question can be found [here](
http://lpaste.net/138853). I'll lay out my code and eventually get to the
question. My project concerns proving things in Data.AVL, so I start with
some boilerplate for that:

    open import Data.Product
    open import Level
    open import Relation.Binary
    open import Relation.Binary.PropositionalEquality as P using (_≡_)

    module Data.AVL.Properties-Refuse
      {k v ℓ}
      {Key : Set k} (Value : Key → Set v)
      {_<_ : Rel Key ℓ}
      (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _<_) where

      open import Data.AVL Value isStrictTotalOrder using (KV; module
Extended-key; module Height-invariants; module Indexed)
      import Data.AVL Value isStrictTotalOrder as AVL
      open Extended-key
      open Height-invariants
      open Indexed

      open IsStrictTotalOrder isStrictTotalOrder

I then borrow [an idea from Vitus](
http://stackoverflow.com/a/21083647/1312174) to represent membership:

      data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ)
where
        here : ∀ {hˡ hʳ} V
          {l : Tree lb [ K ] hˡ}
          {r : Tree [ K ] ub hʳ}
          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
          K ∈ node (K , V) l r (proj₂ b)
        left : ∀ {hˡ hʳ K′} {V : Value K′}
          {l : Tree lb [ K′ ] hˡ}
          {r : Tree [ K′ ] ub hʳ}
          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
          K < K′ →
          K ∈ l →
          K ∈ node (K′ , V) l r (proj₂ b)
        right : ∀ {hˡ hʳ K′} {V : Value K′}
          {l : Tree lb [ K′ ] hˡ}
          {r : Tree [ K′ ] ub hʳ}
          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →
          K′ < K →
          K ∈ r →
          K ∈ node (K′ , V) l r (proj₂ b)

I then declare a function (whose meaning is irrelevant -- this is a
contrived and simple version of a more meaningful function not shown here):

      refuse1 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
                Set
      refuse1 = {!!}

So far, so good. Now, I case split on the default variables:

      refuse2 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
                Set
      refuse2 t k₁ k∈t = {!!}

And now I split on `t`:

      refuse3 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
                Set
      refuse3 (leaf l<u) k₁ k∈t = {!!}
      refuse3 (node k₁ t t₁ bal) k₂ k∈t = {!!}

And now on `bal`:

      refuse4 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
                Set
      refuse4 (leaf l<u) k₁ k∈t = {!!}
      refuse4 (node k₁ t t₁ ∼+) k₂ k∈t = {!!}
      refuse4 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
      refuse4 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}

The first error comes when I try to case split on `k∈t` of the equation
including `(node ... ∼+)`:

      refuse5 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
                Set
      refuse5 (leaf l<u) k₁ k∈t = {!!}
      refuse5 (node k₁ t t₁ ∼+) k₂ k∈t = {!k∈t!}
      {- ERROR
        I'm not sure if there should be a case for the constructor here,
        because I get stuck when trying to solve the following unification
        problems (inferred index ≟ expected index):
          {_} ≟ {_}
          node (k₅ , V) l r (proj₂ b) ≟ node k₄
                                        t₂ t₃ ∼+
        when checking that the expression ? has type Set
      -}
      refuse5 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}
      refuse5 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}

Agda tells me it gets stuck doing the unification, but it's not clear to me
why or how to help. In [a response to a similar question](
http://stackoverflow.com/q/30951993/1312174), Ulf suggested first
case-splitting on another variable. So, now working by hand, I focus on
case-splitting the `∼+` line from `refuse5` and include many of the
implicit variables:

      open import Data.Nat.Base as ℕ

      refuse6 : ∀ {kₗ kᵤ h}
                ( t : Tree kₗ kᵤ h )
                ( k : Key )
                ( k∈t : k ∈ t ) →
                Set
      refuse6 {h = ℕ.suc .hˡ}
              (node (k , V) lk ku (∼+ {n = hˡ}))
              .k
              (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku} {b =
(ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}
      {- ERROR
        Refuse to solve heterogeneous constraint proj₂ b :
        n ∼ hʳ ⊔ proj₁ b =?=
        ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n
        when checking that the pattern
        here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}
          {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}
        has type
        k₂ ∈ node (k₁ , V) lk ku ∼+
      -}
      refuse6 _ _ _ = ?

Oops. Now Agda goes from complaining that it's stuck to downright refusing
to solve. What's going on here? Is it possible to specify the lhs of the
equations with at least as much detail as in refuse5 **and also** case
split on `k∈t`? If so, how?
--
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/20150814/dc6246df/attachment-0001.html