<div dir="ltr"><div><div><div><div>Hi Sandro,<br></div><div><br></div><div>The error message "cannot generalize over the indices" is thrown by Agda when it encounters a unification problem of the form `c us =?= c vs` where `c` is a constructor of an indexed datatype, but the indices in the *type* of this equation are something other than distinct variables (i.e. they should be fully general). If they are not, Agda tries to apply a technique called higher-dimensional unification (see our CPP 2017 paper) to bring them in a fully general form. However, this unfortunately doesn't always succeed, for example in your code it gets stuck on the _+_ function in the index of `con`.</div><div><br></div><div>One way to fix your problem would be to get rid of the 'green slime' in the type of `con`: it's better to use only variables and constructors in the indices of your datatypes, and use explicit proofs of equality for the heavier work.<br></div><div><br></div></div><div>On the other hand, it's possible that there's something more that Agda could do in this situation. Roughly a year ago, I wrote the following comment at 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></div>""". It seems it is necessary in some situations after all. I'll try to remember what I meant with that and implement it.<br><br></div>Best regards,<br></div>Jesper<br><div><div><br><div>ps: To change the {_} in the error message into something more useful, you can enable the --show-implicit option. Maybe it would be better if Agda did this by default.<br></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Thu, Sep 21, 2017 at 11:47 AM, 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 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 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 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 `{_} ≟ {_}` 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>
</blockquote></div><br></div>