[Agda] Sized types unification error.

[Apostolis Xekoukoulotakis]

```
module test where

open import Size
open import Data.Nat

data test : ℕ → Set where
  One : test (suc zero)
  Two : test (suc (suc zero))


fun : test (suc zero) → ℕ
fun x = {!!}

data test2 : (i : Size) → (j : Size< ↑ i) → Set where
  same : ∀{i} → test2 i i
  notSame : {i : Size} → {j : Size< i} → test2 i j


fun2 : {i : Size} → test2 i i → ℕ
fun2 x = {!!}
`
```

Case splitting on fun2 results in error :

```
I'm not sure if there should be a case for the constructor notSame,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  i₁ ≟ i
  j ≟ i
when checking that the expression ? has type ℕ
```

Is there a reason for this to happen? What can one do to remove this error?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170211/989993cb/attachment.html>