":search mult n m = mult m n" causes idris to hang

[fieldstrength]

And the same thing for :search plus n m = plus m n.

[david-christiansen]

That's very strange. It used to work, I think. Finding associativity is lightning-fast, still.

@bmsherman - any ideas?

[bmsherman]

Yes, those searches used to work prior to this commit.

There is a call to match_unify which is not terminating.
The particular offending call seems to be the attempt to unify

plus n m = plus m n

(the return type of the searched type) with

plus left (plus centre right) = plus (plus left centre) right

(the return type of plusAssociative).

As a side note, these types do indeed "meet" at a common type

plus x (plus x x) = plus (plus x x) x

, which is more specific than both of the above two types.

The followSols part of match_unify (introduced in the above-mentioned commit) is given the following list of solutions:

[(m,left),(n,plus centre right),(left,centre),(centre,right),(right,left)]

. Therefore, it ends up caught in the cycle m := right, m := left, m := center, m := right, ...

There is a comment in the code for followSols which says

Are we guaranteed no cycles?

For my usage of match_unify, it seems that the answer is no. Now, it's definitely possible that I'm using match_unify in an improper manner. I'm not really sure what the right solution to this issue is, since I'm not familiar enough with the code for unify and match_unify. I'll have to think about it.

[edwinb]

That'd explain it. I think cycles in the result set should result in a unification failure. I haven't managed to contrive one in real code but it seems plausible. I'll add a check.