<div dir="ltr"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span class="gmail-im">
</span>Is Agda's unifier too eager in this case?</blockquote><div><br></div><div>Agda's case splitter requires all unification problems from the previous case split to be solved before it can start on the next one. In other words, each set of patterns must correspond to a series of consecutive case splits.<br><br>In this case, it first wants to complete the case split on the argument of type "Test zero" before it continues with the case split on the argument of Tost. But for this first case split Agda needs to unify zero with "fn n", which fails because "fn n" doesn't reduce. It doesn't know yet whether n is equal to zero or suc because that case split only comes after the current one.<br><br>In this case it would theoretically be possible to postpone the unification problem and first do the second case split, which would solve the problem. But in general this would be problematic as the types of the constructor arguments may change as a result of the unification. So a proper solution would require interleaving case splitting and unification, allowing unification problems to persist over multiple case splits. <br><br>This is certainly a cool idea, but would require a nontrivial engineering effort to represent this more general split-and-unify problem. Does someone have an idea if this is what they do in Idris, or do they have a different solution to the problem?<br><br></div><div>Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Dec 11, 2016 at 7:50 AM, Roman <span dir="ltr"><<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">If you postpone unication a bit, `tn` type checks:<br>
<br>
open import Relation.Binary.<wbr>PropositionalEquality<br>
<span class=""><br>
data Test : ℕ → Set where<br>
Tist : Test zero<br>
</span> Tostq : ∀ {m} → (n : ℕ) → m ≡ fn n → Test m<br>
<br>
pattern Tost n = Tostq n refl<br>
<span class=""><br>
tn : (n : ℕ) → Test (fn n) → ℕ<br>
tn zero Tist = zero<br>
tn zero (Tost zero) = zero<br>
</span>tn zero (Tost (suc n)) = zero<br>
<span class="">tn (suc y) x = {!!}<br>
<br>
</span>Is Agda's unifier too eager in this case?<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>