[Agda] Cannot apply injectivity

[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

On Thu, Sep 21, 2017 at 5:44 PM, Sandro Stucki <sandro.stucki at epfl.ch>
wrote:

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