Tactics should make use of GHC hole refinment suggestions

[wz1000]

It would be awesome if we could add a tactic based on GHCs existing hole-fit system. I've added support to ghcide to capture relevant hole fits in haskell/ghcide#889.

Alternatively, tactics could directly call findValidHoleFits.

This would also let existing GHC Hole Fit Plugins easily extend the tactics mechanism to add functionality and guide synthesis.

/cc @isovector

[isovector]

I'm not convinced this would buy anything; there are looots of valid fits, and unsafeCoerce is always one of them :)

[wz1000]

unsafeCoerce is always one of them

Only if you import it.

We can always filter the hole fits to use only those that make the subgoals "smaller" in some way, so that we don't pick things like head _

[siraben]

Would it be possible to only consider "safe" functions?

[isovector]

Really and truly I don't think having these hole fits would help.

The hard part of solving holes is not the search, it's knowing what not to search. Just off the top of my head, GHC will report undefined, id _ and head _ for every hole, but that's always going to be a red herring. Maybe you'll argue that this is a property of polymorphism, and that we should exclude those --- but the trick is nailing what those heuristics actually need to be. Getting the tactics plugin to find useful solutions in a short time requires balancing an exceedingly precarious set of search parameters.

Explicitly opting-in to what you'd like to have in scope is the only sane solution I can think of here!

[siraben]

Explicitly opting-in to what you'd like to have in scope is the only sane solution I can think of here!

That sounds like a good idea! There's issues like #562 (program generation via combinators) that would be solved if the user could specify which values they would like to use.

[isovector]

It's on the roadmap: isovector#6

[isovector]

Closing this issue, but feel free to reopen if someone has a strong counterargument.