Okay, but this doesn't feel scalable. Are we going to have an or clause for
every pairwise set of kinds? Can't we handle this more generically somehow?

Also, do we even want to support this use case? It feels wrong to me to
have the ability to overload token sorts with arbitrary productions.
On Mar 7, 2014 11:46 AM, "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()));
>
> Consider the following productions and the lookup rule in fun-untyped:
> syntax Name ::= Token{[a-z][\_a-zA-Z0-9]*} [notInRules]
> syntax Name ::= "$h"
>
>   rule <k> X:Name => V ...</k>
>        <env>... X |-> L ...</env>
>        <store>... L |-> V ...</store>
>
> Name is a token sort thanks to the first production and, therefore, the
> lookup rule has a TokenIndex. However, $h has a KLabelIndex and will get
> stuck when it appears on top of the k cell.
>
> --
> Reply to this email directly or view it on GitHub<https://github.com/kframework/k/pull/270/files#r10396875>
> .
>