No it's not though. You've already special cased TopIndex as well. That's
what I'm concerned about here: we seem to be writing an algorithm that
scales quadratically in the number of kinds. And for all I really know
there may be other corner cases you're missing also, since you apparently
only just now thought of this one. so I'm not really very pleased with this
method even if we can remove the corner case in question. If we're doing
things based on sorts but having to do cases kind by kind, what have we
done to solve this in the past? This sounds very similar to something we
should have had to deal with for the unification algorithm itself. How did
we handle it there?
On Mar 7, 2014 12:43 PM, "Yilong Li" <notifications@github.com> wrote:

> In
> src/javasources/KTool/src/org/kframework/backend/java/indexing/KLabelIndex.java:
>
> >      @Override
> >      public boolean isUnifiable(Index index) {
> > -        return index instanceof TopIndex || equals(index);
> > +        return index instanceof TopIndex
> > +                || equals(index)
> > +                || (index instanceof TokenIndex &&
> > +                        kLabel.sorts().contains(((TokenIndex) index).sort()));
>
> For now, it is just between TokenIndex and KLabelIndex. I am not sure what
> would be a better way to handle this but I will keep that in mind.
>
> I am afraid I cannot answer your second question. I would like to get rid
> of all these tricky cases and keep my code clean of course. @grosu<https://github.com/grosu>
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/270/files#r10399060>
> .
>