[Agda] Cannot apply injectivity

[Sandro Stucki]

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