<div dir="ltr"><div><div>Andreas has a good point. It is important to keep that promise.<br><br></div>I case split the code in Idris by hand, but the point of types is to guide you, thus not doing it manually.<br><br></div>Given that there is an easy way around it, the fact that agda rejects this code altogether is good for pedagogical reasons.<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Dec 11, 2016 at 1:10 PM, Andreas Abel <span dir="ltr">&lt;<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Agda&#39;s promise is that everything that is generated by successive splits can be type-checked. (That this promise is not always kept is another story).<br>
<br>
At this point<span class=""><br>
<br>
  tn : (n : ℕ) → Test (fn n) → ℕ<br></span>
  tn zero    t = {!t!}<br>
  tn (suc n) t = {!!}<br>
<br>
there is no way to split on t : Test 0 since it is not clear whether Tost is a possible case:<br>
<br>
  I&#39;m not sure if there should be a case for the constructor Tost,<br>
  because I get stuck when trying to solve the following unification<br>
  problems (inferred index ≟ expected index):<br>
    fn n ≟ fn zero<br>
<br>
What should be the result of splitting on t?  A deep splitting until all unification constraints are satisfied??<br>
<br>
I am not sure there is a clear story behind this example, except Roman&#39;s advice: Be careful with function applications in the target type of your constructors!<br>
<br>
--Andreas<div><div class="h5"><br>
<br>
On 11.12.2016 11:29, Jesper Cockx wrote:<br>
</div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5">
    Is Agda&#39;s unifier too eager in this case?<br>
<br>
<br>
Agda&#39;s case splitter requires all unification problems from the previous<br>
case split to be solved before it can start on the next one. In other<br>
words, each set of patterns must correspond to a series of consecutive<br>
case splits.<br>
<br>
In this case, it first wants to complete the case split on the argument<br>
of type &quot;Test zero&quot; before it continues with the case split on the<br>
argument of Tost. But for this first case split Agda needs to unify zero<br>
with &quot;fn n&quot;, which fails because &quot;fn n&quot; doesn&#39;t reduce. It doesn&#39;t know<br>
yet whether n is equal to zero or suc because that case split only comes<br>
after the current one.<br>
<br>
In this case it would theoretically be possible to postpone the<br>
unification problem and first do the second case split, which would<br>
solve the problem. But in general this would be problematic as the types<br>
of the constructor arguments may change as a result of the unification.<br>
So a proper solution would require interleaving case splitting and<br>
unification, allowing unification problems to persist over multiple case<br>
splits.<br>
<br>
This is certainly a cool idea, but would require a nontrivial<br>
engineering effort to represent this more general split-and-unify<br>
problem. Does someone have an idea if this is what they do in Idris, or<br>
do they have a different solution to the problem?<br>
<br>
Jesper<br>
<br>
On Sun, Dec 11, 2016 at 7:50 AM, Roman &lt;<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a><br></div></div><span class="">
&lt;mailto:<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>&gt;<wbr>&gt; wrote:<br>
<br>
    If you postpone unication a bit, `tn` type checks:<br>
<br>
    open import Relation.Binary.PropositionalE<wbr>quality<br>
<br>
    data Test : ℕ → Set where<br>
      Tist : Test zero<br>
      Tostq : ∀ {m} → (n : ℕ) → m ≡ fn n → Test m<br>
<br>
    pattern Tost n = Tostq n refl<br>
<br>
    tn : (n : ℕ) → Test (fn n) → ℕ<br>
    tn zero  Tist          = zero<br>
    tn zero (Tost  zero)   = zero<br>
    tn zero (Tost (suc n)) = zero<br>
    tn (suc y) x = {!!}<br>
<br>
    Is Agda&#39;s unifier too eager in this case?<br>
    ______________________________<wbr>_________________<br>
    Agda mailing list<br></span>
    <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> &lt;mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><wbr>&gt;<br>
    <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
    &lt;<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a>&gt;<span class=""><br>
<br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
<br>
</span></blockquote><span class="HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel  &lt;&gt;&lt;      Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~ab<wbr>el/</a><br>
</font></span></blockquote></div><br></div>