[Agda] Sized types unification error.

[Apostolis Xekoukoulotakis]

I am avoiding this issue at the moment, so no hurry. But I am interested in
the answer.

On Sun, Feb 12, 2017 at 12:47 PM, Jesper Cockx <Jesper at sikanda.be> wrote:

> 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/20170213/76700347/attachment-0001.html>