[Agda] Cannot apply injectivity

[Sandro Stucki]

Hi Jesper,

Thanks for the quick reply and the pointer to your CPP'17 paper

> One way to fix your problem would be to get rid of the 'green slime' in the
> type of `con`: (...)

Yes, the green slime in the definition if Indexed is indeed
unfortunate (and in fact unnecessary in my real use case). So I guess
the take home message is simply "avoid green slime".

Still, I'm curious what exactly goes wrong here, so I followed your suggestion:

> ps: To change the {_} in the error message into something more useful, you
> can enable the --show-implicit option.

Thanks for pointing that out, I had forgotten about that option! With that I get

  {m₂ + n₁} ≟ {m₁ + n}
  {m₂ + suc n₁} ≟ {m₁ + suc n}
  con m₂ {n₁} i₂ ≟ con m₁ {n} i₁
  con m₂ {n₁} j ≟ con m₁ {n} i₁

which indeed suggests that _+_ gets in the way.

But I'm curious why Agda 2.5.1 was able to handle this case. I guess
if we were to apply injectivity of constructors naively, we'd get

  m₂ ≟ m₁
  {n₁} ≟ {n}
  i₂ ≟ i₁
  j ≟ i₁

and substituting these, the equations involving _+_ would become trivial.

I had a quick look at your paper and it seems the problem is not so
much generalizing the indices `m + n` and `m + suc n` but dealing with
the resulting higher-dimensional equations. Is that correct? If yes,
then maybe the error message is slightly misleading.

I'm also curious if and how uniqueness-of-identity proofs would help
in dealing with the higher-dimensional equations generated when you
generalize indices.

Cheers
/Sandro


On Thu, Sep 21, 2017 at 1:36 PM, Jesper Cockx <Jesper at sikanda.be> wrote:
> Hi Sandro,
>
> 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`.
>
> 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.
>
> 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: """
>     -- TODO: we could still make progress here if not --without-K,
>     -- but I'm not sure if it's necessary.
> """. It seems it is necessary in some situations after all. I'll try to
> remember what I meant with that and implement it.
>
> Best regards,
> Jesper
>
> 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.
>
> On Thu, Sep 21, 2017 at 11:47 AM, Sandro Stucki <sandro.stucki at epfl.ch>
> wrote:
>>
>> Hi all,
>>
>> I recently ported some code from Agda 2.5.1 to 2.5.2 and ran into some
>> errors, probably caused by a change in the unifier. I've reduced the
>> offending code down to the following:
>>
>> ----
>> open import Data.Nat using (ℕ; suc; _+_)
>> open import Data.Fin using (Fin)
>>
>> data Indexed : ℕ → ℕ → Set where
>>   con : ∀ m {n} (i : Fin n) → Indexed (m + n) (m + suc n)
>>
>> data RelIndexed : ∀ {m n} → Indexed m n → Indexed m n → Set where
>>   relIdx : ∀ {m n} (i : Fin n) (j : Fin n) → RelIndexed (con m i) (con m
>> j)
>>
>> test1 : ∀ {m n} {a b : Indexed m n} → RelIndexed a b → Indexed m n
>> test1 (relIdx {m} i _) = con m i
>>
>> test2 : ∀ {m n} {a : Indexed m n} → RelIndexed a a → Indexed m n
>> test2 (relIdx {m} i _) = con m i
>> ----
>>
>> I'm using the modules Data.Nat and Data.Fin from the standard library
>> here.
>>
>> The idea is that `Indexed` is some datatype indexed by naturals, and
>> `RelIndexed` is a family of relations over `Indexed` at given `n` and
>> `m`. I want to write a function (actually a lemma) similar to `test2`
>> for a reflexive instance of `RelIndexed`, i.e. where some `Indexed`
>> instance is related to itself. But somehow the Agda 2.5.2 unifier is
>> not happy about this.
>>
>> For `test1` the unifier succeeds, but for `test2` it apparently fails
>> to solve `con m i = con m j`. The error is
>>
>> ----
>> Cannot apply injectivity to the equation con m i = con m j of type
>> Indexed (m + n) (m + suc n) because I cannot generalize over the
>> indices [m + n, m + suc n]
>> when checking that the pattern relIdx {m} i _ has type
>> RelIndexed a a
>> ----
>>
>> What does it mean to "generalize over the indices [m + n, m + suc n]",
>> and why is this necessary here?
>>
>> If I rewrite test2 as `test2 r = ?` and attempt a case split on `r` I
>> get instead
>>
>> ----
>> I'm not sure if there should be a case for the constructor relIdx,
>> because I get stuck when trying to solve the following unification
>> problems (inferred index ≟ expected index):
>>   {_} ≟ {_}
>>   {_} ≟ {_}
>>   con m₁ i ≟ a
>>   con m₁ j ≟ a
>> when checking that the expression ? has type Indexed .m .n
>> ----
>>
>> I'm not sure how to interpret this either, especially the `{_} ≟ {_}`
>> lines.
>>
>> Cheers
>> /Sandro
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>