<div dir="ltr">NB Crossposted to <a href="http://stackoverflow.com/q/32021121/1312174">http://stackoverflow.com/q/32021121/1312174</a>.<br><div><br>This question is about<br><br>* how to help Agda get unstuck when solving unification problems, and<br>* how to convince Agda to solve a &quot;heterogeneous constraint&quot; (whatever that means)<br><br>The complete code for my question can be found [here](<a href="http://lpaste.net/138853">http://lpaste.net/138853</a>). I&#39;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:<br><br>    open import Data.Product<br>    open import Level<br>    open import Relation.Binary<br>    open import Relation.Binary.PropositionalEquality as P using (_≡_)<br><br>    module Data.AVL.Properties-Refuse<br>      {k v ℓ}<br>      {Key : Set k} (Value : Key → Set v)<br>      {_&lt;_ : Rel Key ℓ}<br>      (isStrictTotalOrder : IsStrictTotalOrder P._≡_ _&lt;_) where<br><br>      open import Data.AVL Value isStrictTotalOrder using (KV; module Extended-key; module Height-invariants; module Indexed)<br>      import Data.AVL Value isStrictTotalOrder as AVL<br>      open Extended-key                       <br>      open Height-invariants                  <br>      open Indexed                            <br><br>      open IsStrictTotalOrder isStrictTotalOrder<br><br>I then borrow [an idea from Vitus](<a href="http://stackoverflow.com/a/21083647/1312174">http://stackoverflow.com/a/21083647/1312174</a>) to represent membership:<br><br>      data _∈_ {lb ub} (K : Key) : ∀ {n} → Tree lb ub n → Set (k ⊔ v ⊔ ℓ) where<br>        here : ∀ {hˡ hʳ} V<br>          {l : Tree lb [ K ] hˡ}<br>          {r : Tree [ K ] ub hʳ}<br>          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>          K ∈ node (K , V) l r (proj₂ b)<br>        left : ∀ {hˡ hʳ K′} {V : Value K′}<br>          {l : Tree lb [ K′ ] hˡ}<br>          {r : Tree [ K′ ] ub hʳ}<br>          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>          K &lt; K′ →<br>          K ∈ l →<br>          K ∈ node (K′ , V) l r (proj₂ b)<br>        right : ∀ {hˡ hʳ K′} {V : Value K′}<br>          {l : Tree lb [ K′ ] hˡ}<br>          {r : Tree [ K′ ] ub hʳ}<br>          {b : ∃ λ h → hˡ ∼ hʳ ⊔ h} →<br>          K′ &lt; K →<br>          K ∈ r →<br>          K ∈ node (K′ , V) l r (proj₂ b)<br><br>I then declare a function (whose meaning is irrelevant -- this is a contrived and simple version of a more meaningful function not shown here):<br><br>      refuse1 : ∀ {kₗ kᵤ h}<br>                ( t : Tree kₗ kᵤ h )<br>                ( k : Key )<br>                ( k∈t : k ∈ t ) →<br>                Set<br>      refuse1 = {!!}<br><br>So far, so good. Now, I case split on the default variables:<br><br>      refuse2 : ∀ {kₗ kᵤ h}<br>                ( t : Tree kₗ kᵤ h )<br>                ( k : Key )<br>                ( k∈t : k ∈ t ) →<br>                Set<br>      refuse2 t k₁ k∈t = {!!}<br><br>And now I split on `t`:<br><br>      refuse3 : ∀ {kₗ kᵤ h}<br>                ( t : Tree kₗ kᵤ h )<br>                ( k : Key )<br>                ( k∈t : k ∈ t ) →<br>                Set<br>      refuse3 (leaf l&lt;u) k₁ k∈t = {!!}<br>      refuse3 (node k₁ t t₁ bal) k₂ k∈t = {!!}<br><br>And now on `bal`:<br><br>      refuse4 : ∀ {kₗ kᵤ h}<br>                ( t : Tree kₗ kᵤ h )<br>                ( k : Key )<br>                ( k∈t : k ∈ t ) →<br>                Set<br>      refuse4 (leaf l&lt;u) k₁ k∈t = {!!}<br>      refuse4 (node k₁ t t₁ ∼+) k₂ k∈t = {!!}<br>      refuse4 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}<br>      refuse4 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}<br><br>The first error comes when I try to case split on `k∈t` of the equation including `(node ... ∼+)`:<br><br>      refuse5 : ∀ {kₗ kᵤ h}<br>                ( t : Tree kₗ kᵤ h )<br>                ( k : Key )<br>                ( k∈t : k ∈ t ) →<br>                Set<br>      refuse5 (leaf l&lt;u) k₁ k∈t = {!!}<br>      refuse5 (node k₁ t t₁ ∼+) k₂ k∈t = {!k∈t!}<br>      {- ERROR<br>        I&#39;m not sure if there should be a case for the constructor here,<br>        because I get stuck when trying to solve the following unification<br>        problems (inferred index ≟ expected index):<br>          {_} ≟ {_}<br>          node (k₅ , V) l r (proj₂ b) ≟ node k₄<br>                                        t₂ t₃ ∼+<br>        when checking that the expression ? has type Set<br>      -}<br>      refuse5 (node k₁ t t₁ ∼0) k₂ k∈t = {!!}<br>      refuse5 (node k₁ t t₁ ∼-) k₂ k∈t = {!!}<br><br>Agda tells me it gets stuck doing the unification, but it&#39;s not clear to me why or how to help. In [a response to a similar question](<a href="http://stackoverflow.com/q/30951993/1312174">http://stackoverflow.com/q/30951993/1312174</a>), 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:<br><br>      open import Data.Nat.Base as ℕ<br><br>      refuse6 : ∀ {kₗ kᵤ h}<br>                ( t : Tree kₗ kᵤ h )<br>                ( k : Key )<br>                ( k∈t : k ∈ t ) →<br>                Set<br>      refuse6 {h = ℕ.suc .hˡ}<br>              (node (k , V) lk ku (∼+ {n = hˡ}))<br>              .k<br>              (here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku} {b = (ℕ.suc .hˡ , ∼+ {n = .hˡ})}) = {!!}<br>      {- ERROR<br>        Refuse to solve heterogeneous constraint proj₂ b :<br>        n ∼ hʳ ⊔ proj₁ b =?=<br>        ∼+ : n ∼ ℕ.suc n ⊔ ℕ.suc n<br>        when checking that the pattern<br>        here {hˡ = .hˡ} {hʳ = ℕ.suc .hˡ} .V {l = .lk} {r = .ku}<br>          {b = ℕ.suc .hˡ , ∼+ {n = .hˡ}}<br>        has type<br>        k₂ ∈ node (k₁ , V) lk ku ∼+<br>      -}<br>      refuse6 _ _ _ = ?<br><br>Oops. Now Agda goes from complaining that it&#39;s stuck to downright refusing to solve. What&#39;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?<br clear="all"><div><div class="gmail_signature"><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr"><div><div dir="ltr">--<br>Martin Stone Davis<br><div><br>Postal/Residential:<br></div><div style="margin-left:40px"><span>1223 Ferry St</span><span><span><br></span></span></div><div style="margin-left:40px"><span><span>Apt 5<br></span></span></div><div style="margin-left:40px"><span>Eugene, OR 97401</span><br></div>Talk / <span></span>Text / Voicemail: <a href="tel:3106993578" value="+13106993578" target="_blank">(310) 699-3578</a><br>Electronic Mail: <a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a><div><div><div><span></span></div></div></div></div></div><div dir="ltr"><span style="font-size:small">Website: </span><a href="http://martinstonedavis.com/" style="color:rgb(17,85,204);font-size:small" target="_blank">martinstonedavis.com</a></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div></div>
</div></div>