[Agda] Cannot apply injectivity

[Jesper Cockx]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170921/39400934/attachment.html>