Infinite loop in the REPL for GenerateDefinition on binary tree

[eviefp]

The REPL seems to be able to generate the definition for specialized linear map definition for List, but if we add a second recursive parameter (such as required for a binary tree), then generate definition loops forever.

Steps to Reproduce

Please see https://gist.github.com/vladciobanu/a9509be6e005312af698a03d324cc0d9 for a trivial reproduction example. The code includes the List version to showcase the differences.

Expected Behavior

Generate the correct implementation, or at least report it can't.

Observed Behavior

Infinite loop.

---

Possibly related, but unsure. Let me know if I should create a different issue for this.

If I change the definition of Tree to

data Tree a = TNil | Node a (List' (Tree a))

mapTree : ((1 x : a) -> b) -> (1 t : Tree a) -> Tree b

and try to generate its map function, I get:

mapTree f TNil = TNil
mapTree f (Node x y) = mapTree f (Node x (Cons TNil y))

If I change the definition to

data Tree a = NNode a (List' (Tree a))

Then it reports it can't find a definition for the same mapTree, although we can write:

mapTree f (Node x xs) = Node (f x) (mapList (mapTree f) xs)

[edwinb]

I get a crash due to stack overflow, it's interesting that you don't see that behaviour! Or maybe you compiled Idris2 with -O2 which might change one of the functions to be tail recursive?

In any case - this isn't an infinite loop, but rather the search space getting too big because the tree is branching. The expression search really is very simple, and just does a brute force search of the whole space. There's probably things we can do to prune the tree and make this sort of search work better, but in the short term I think the best we can do is cut off the search and say the problem is too big.

Part of the reason this problem gets big is that it doesn't look at how linear bindings affect the result until after generating a candidate expression. So there's a lot more candidates to check than there should be.