[Agda] Sized types unification error.

[Jesper Cockx]

This still worked on 2.5.2, but it stopped working because of my fix of
#2407 (https://github.com/agda/agda/issues/2407). 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:
```
↑ i !=< i of type Size
when checking that the expression i has type Size< i
```
Replacing the .i by _ allowed the example to work, but this was clearly
wrong and is now also prohibited by my fix.

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.

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?

-- Jesper

On Sat, Feb 11, 2017 at 12:28 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> ```
> 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?
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170212/9984db39/attachment.html>