[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

[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.

Post by 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
----
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
{_} ≟ {_}
{_} ≟ {_}
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
https://lists.chalmers.se/mailman/listinfo/agda

[Sandro Stucki]

Hi Jesper,

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

Post by Jesper Cockx
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".

Post by Jesper Cockx
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

Post by 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.

Post by 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
----
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
{_} ≟ {_}
{_} ≟ {_}
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
https://lists.chalmers.se/mailman/listinfo/agda

[Jesper Cockx]

Hi Sandro,

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!

cheers,
Jesper

Post by Sandro Stucki
Hi Jesper,
Thanks for the quick reply and the pointer to your CPP'17 paper

Post by Jesper Cockx
One way to fix your problem would be to get rid of the 'green slime' in

the

Post by Jesper Cockx
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".

Post by Jesper Cockx
ps: To change the {_} in the error message into something more useful,

you

Post by Jesper Cockx
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

Post by 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

Post by Jesper Cockx
`c` is a constructor of an indexed datatype, but the indices in the

*type*

Post by Jesper Cockx
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

Post by Jesper Cockx
called higher-dimensional unification (see our CPP 2017 paper) to bring

them

Post by Jesper Cockx
in a fully general form. However, this unfortunately doesn't always

succeed,

Post by Jesper Cockx
for example in your code it gets stuck on the _+_ function in the index

of

Post by Jesper Cockx
`con`.
One way to fix your problem would be to get rid of the 'green slime' in

the

Post by Jesper Cockx
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

Post by Jesper Cockx
do in this situation. Roughly a year ago, I wrote the following comment

at

Post by Jesper Cockx
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

Post by Jesper Cockx
can enable the --show-implicit option. Maybe it would be better if Agda

did

Post by Jesper Cockx
this by default.

Post by 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
----
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
{_} ≟ {_}
{_} ≟ {_}
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
https://lists.chalmers.se/mailman/listinfo/agda