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