<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"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Agda'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'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'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's unifier too eager in this case?<br>
<br>
<br>
Agda'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 "Test zero" 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 "fn n", which fails because "fn n" doesn't reduce. It doesn'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 <<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a><br></div></div><span class="">
<mailto:<a href="mailto:effectfully@gmail.com" target="_blank">effectfully@gmail.com</a>><wbr>> 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'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> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><wbr>><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>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a>><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 <>< 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>