<div dir="ltr"><div><div><div><div>This still worked on 2.5.2, but it stopped working because of my fix of #2407 (<a href="https://github.com/agda/agda/issues/2407">https://github.com/agda/agda/issues/2407</a>). The behaviour of agda-2.5.2 was to generate two cases `fun2 {i} (same {i = .i}) = ?` and `fun2 {i} (notSame {i = .i} {j = .i}) = ?` (with --show-implicit option), but the second case here is actually not even type-correct! Indeed, it throws the following error:<br>```<br>↑ i !=< i of type Size<br>when checking that the expression i has type Size< i<br>```<br></div><div>Replacing the .i by _ allowed the example to work, but this was clearly wrong and is now also prohibited by my fix.<br><br></div><div>To fix the problem in your code, you could replace the type of j in the notSame constructor by `Size< (↑ i)`, but this is perhaps not what you'd want.<br></div><div><br></div><div>OTOH, perhaps it could be reasonable to expect Agda to see that the case for `notSame` is impossible instead of giving up as it currently does. But I don't know enough about sized types to be sure that this would be sound. Perhaps Andreas can tell what the right behaviour should be here? <br></div><br></div></div>-- Jesper<br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Feb 11, 2017 at 12:28 AM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div><div><div>```<br>module test where<br><br>open import Size<br>open import Data.Nat<br><br>data test : ℕ → Set where<br>  One : test (suc zero)<br>  Two : test (suc (suc zero))<br><br><br>fun : test (suc zero) → ℕ<br>fun x = {!!}<br><br>data test2 : (i : Size) → (j : Size< ↑ i) → Set where<br>  same : ∀{i} → test2 i i<br>  notSame : {i : Size} → {j : Size< i} → test2 i j<br><br><br>fun2 : {i : Size} → test2 i i → ℕ<br>fun2 x = {!!}<br>`<br>```<br><br></div>Case splitting on fun2 results in error :<br><br>```<br>I'm not sure if there should be a case for the constructor notSame,<br>because I get stuck when trying to solve the following unification<br>problems (inferred index ≟ expected index):<br>  i₁ ≟ i<br>  j ≟ i<br>when checking that the expression ? has type ℕ<br>```<br><br></div>Is there a reason for this to happen? What can one do to remove this error?<br></div></div>
<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>
<br></blockquote></div><br></div>