<div dir="ltr"><div><div><div>Hi Sandro,<br><br></div>If we're not working --without-K, then there's a simpler injectivity rule that can be applied that's very close to the naive one (see Lemma 3.53 in my thesis). I've implemented this alternative injectivity rule as a fallback to the current mechanism (only when --without-K is not enabled of course). This makes your example code typecheck. Thank you for providing a good motivating example for implementing this feature!<br><br></div>cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 21, 2017 at 5:44 PM, Sandro Stucki <span dir="ltr"><<a href="mailto:sandro.stucki@epfl.ch" target="_blank">sandro.stucki@epfl.ch</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Jesper,<br>
<br>
Thanks for the quick reply and the pointer to your CPP'17 paper<br>
<span class=""><br>
> One way to fix your problem would be to get rid of the 'green slime' in the<br>
</span>> type of `con`: (...)<br>
<br>
Yes, the green slime in the definition if Indexed is indeed<br>
unfortunate (and in fact unnecessary in my real use case). So I guess<br>
the take home message is simply "avoid green slime".<br>
<br>
Still, I'm curious what exactly goes wrong here, so I followed your suggestion:<br>
<span class=""><br>
> ps: To change the {_} in the error message into something more useful, you<br>
> can enable the --show-implicit option.<br>
<br>
</span>Thanks for pointing that out, I had forgotten about that option! With that I get<br>
<br>
  {m₂ + n₁} ≟ {m₁ + n}<br>
  {m₂ + suc n₁} ≟ {m₁ + suc n}<br>
  con m₂ {n₁} i₂ ≟ con m₁ {n} i₁<br>
  con m₂ {n₁} j ≟ con m₁ {n} i₁<br>
<br>
which indeed suggests that _+_ gets in the way.<br>
<br>
But I'm curious why Agda 2.5.1 was able to handle this case. I guess<br>
if we were to apply injectivity of constructors naively, we'd get<br>
<br>
  m₂ ≟ m₁<br>
  {n₁} ≟ {n}<br>
  i₂ ≟ i₁<br>
  j ≟ i₁<br>
<br>
and substituting these, the equations involving _+_ would become trivial.<br>
<br>
I had a quick look at your paper and it seems the problem is not so<br>
much generalizing the indices `m + n` and `m + suc n` but dealing with<br>
the resulting higher-dimensional equations. Is that correct? If yes,<br>
then maybe the error message is slightly misleading.<br>
<br>
I'm also curious if and how uniqueness-of-identity proofs would help<br>
in dealing with the higher-dimensional equations generated when you<br>
generalize indices.<br>
<br>
Cheers<br>
<span class="HOEnZb"><font color="#888888">/Sandro<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
<br>
On Thu, Sep 21, 2017 at 1:36 PM, Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>> wrote:<br>
> Hi Sandro,<br>
><br>
> The error message "cannot generalize over the indices" is thrown by Agda<br>
> when it encounters a unification problem of the form `c us =?= c vs` where<br>
> `c` is a constructor of an indexed datatype, but the indices in the *type*<br>
> of this equation are something other than distinct variables (i.e. they<br>
> should be fully general). If they are not, Agda tries to apply a technique<br>
> called higher-dimensional unification (see our CPP 2017 paper) to bring them<br>
> in a fully general form. However, this unfortunately doesn't always succeed,<br>
> for example in your code it gets stuck on the _+_ function in the index of<br>
> `con`.<br>
><br>
> One way to fix your problem would be to get rid of the 'green slime' in the<br>
> type of `con`: it's better to use only variables and constructors in the<br>
> indices of your datatypes, and use explicit proofs of equality for the<br>
> heavier work.<br>
><br>
> On the other hand, it's possible that there's something more that Agda could<br>
> do in this situation. Roughly a year ago, I wrote the following comment at<br>
> the place where this error is thrown: """<br>
>     -- TODO: we could still make progress here if not --without-K,<br>
>     -- but I'm not sure if it's necessary.<br>
> """. It seems it is necessary in some situations after all. I'll try to<br>
> remember what I meant with that and implement it.<br>
><br>
> Best regards,<br>
> Jesper<br>
><br>
> ps: To change the {_} in the error message into something more useful, you<br>
> can enable the --show-implicit option. Maybe it would be better if Agda did<br>
> this by default.<br>
><br>
> On Thu, Sep 21, 2017 at 11:47 AM, Sandro Stucki <<a href="mailto:sandro.stucki@epfl.ch">sandro.stucki@epfl.ch</a>><br>
> wrote:<br>
>><br>
>> Hi all,<br>
>><br>
>> I recently ported some code from Agda 2.5.1 to 2.5.2 and ran into some<br>
>> errors, probably caused by a change in the unifier. I've reduced the<br>
>> offending code down to the following:<br>
>><br>
>> ----<br>
>> open import Data.Nat using (ℕ; suc; _+_)<br>
>> open import Data.Fin using (Fin)<br>
>><br>
>> data Indexed : ℕ → ℕ → Set where<br>
>>   con : ∀ m {n} (i : Fin n) → Indexed (m + n) (m + suc n)<br>
>><br>
>> data RelIndexed : ∀ {m n} → Indexed m n → Indexed m n → Set where<br>
>>   relIdx : ∀ {m n} (i : Fin n) (j : Fin n) → RelIndexed (con m i) (con m<br>
>> j)<br>
>><br>
>> test1 : ∀ {m n} {a b : Indexed m n} → RelIndexed a b → Indexed m n<br>
>> test1 (relIdx {m} i _) = con m i<br>
>><br>
>> test2 : ∀ {m n} {a : Indexed m n} → RelIndexed a a → Indexed m n<br>
>> test2 (relIdx {m} i _) = con m i<br>
>> ----<br>
>><br>
>> I'm using the modules Data.Nat and Data.Fin from the standard library<br>
>> here.<br>
>><br>
>> The idea is that `Indexed` is some datatype indexed by naturals, and<br>
>> `RelIndexed` is a family of relations over `Indexed` at given `n` and<br>
>> `m`. I want to write a function (actually a lemma) similar to `test2`<br>
>> for a reflexive instance of `RelIndexed`, i.e. where some `Indexed`<br>
>> instance is related to itself. But somehow the Agda 2.5.2 unifier is<br>
>> not happy about this.<br>
>><br>
>> For `test1` the unifier succeeds, but for `test2` it apparently fails<br>
>> to solve `con m i = con m j`. The error is<br>
>><br>
>> ----<br>
>> Cannot apply injectivity to the equation con m i = con m j of type<br>
>> Indexed (m + n) (m + suc n) because I cannot generalize over the<br>
>> indices [m + n, m + suc n]<br>
>> when checking that the pattern relIdx {m} i _ has type<br>
>> RelIndexed a a<br>
>> ----<br>
>><br>
>> What does it mean to "generalize over the indices [m + n, m + suc n]",<br>
>> and why is this necessary here?<br>
>><br>
>> If I rewrite test2 as `test2 r = ?` and attempt a case split on `r` I<br>
>> get instead<br>
>><br>
>> ----<br>
>> I'm not sure if there should be a case for the constructor relIdx,<br>
>> because I get stuck when trying to solve the following unification<br>
>> problems (inferred index ≟ expected index):<br>
>>   {_} ≟ {_}<br>
>>   {_} ≟ {_}<br>
>>   con m₁ i ≟ a<br>
>>   con m₁ j ≟ a<br>
>> when checking that the expression ? has type Indexed .m .n<br>
>> ----<br>
>><br>
>> I'm not sure how to interpret this either, especially the `{_} ≟ {_}`<br>
>> lines.<br>
>><br>
>> Cheers<br>
>> /Sandro<br>
>> ______________________________<wbr>_________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
><br>
><br>
</div></div></blockquote></div><br></div>