<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>