Rename user-defined holes on naming conflict

[0xd34df00d]

Personally, I often find myself duplicating hole names if I want to postpone work on some piece of my code to a later time (using something like ?later). This worked perfectly with Idris 1, but Idris 2 isn't so happy about code like

foo : SomeTy
foo = bar ?later ?later

erroring out on the second ?later because it's already defined.

This PR addresses this. In particular, it renames the holes roughly following Idris 1 behaviour (so that the first ?later above remains as ?later, and the second one becomes ?later1). Moreover, I've checked the REPL recognizes this correctly and shows the type of the first hole when asked for :t later, and the type of the second one on :t later1.

It only renames holes if they conflict with another hole and not a user-defined function, so things like

example : Nat
example = ?example

are still erroneous. I'm quite new to the Idris 2 internals though, so I might have got that check wrong, of course.

One thing missing here is tests. I'm not sure what's the right tests/ subdir to put this in, so, if this change is not frowned upon, I'd be happy to add those!

[edwinb]

I see the need for this, and I've wanted something a bit like it myself sometimes, like in Idris 1, but something about it does worry me, which is why I haven't implemented this behaviour so far - namely, that it doesn't work well with the IDE mode. If you ask for the type of the second later in the editor, you'll get the type of the first, which is going to be confusing.

So for the moment I prefer this to be an error, but I think the behaviour you want is achievable with just a little bit more support in the IDE mode. I don't really have the time to go into the full details right now, except to say that there's an IDE mode that checks types with location, but doesn't currently take the location into account. If it did, I think this'd be fine.

Any one else have thoughts on this? Perhaps I'm worrying about nothing. Sorry to be a bit negative, because there is a need for it, and the problem is the fault of the IDE mode, not this PR, but I'm not sure the behaviour is quite right yet.

[andrevidela]

This should definitely be a compiler error, but the IDE mode should detect this case and suggest a renaming for the second hole. A repl for Idris could display the following interface

> There are multiple holes with the same name, would you like to rename them with distinct names? Y/n

A given implementation of the protocol could have an option to automatically update the source code with new names without having to go through this little interaction every time one wants to recompile.

[andrevidela]

If you don't mind I will close this since overlapping hole names is a non-goal.

However, I've added your feature request here https://github.com/idris-lang/Idris2/wiki/The-Idris-editor-experience , so we can track which editors support which features :)