Recursively finding valid fits for typed holes.
Very similar to the motivation of finding valid hole fits in the first place, this feature is also inspired by Agda's autofill feature. This approach has two obvious, and impactful, differences in user experience to the current approach:
- The suggestions will be more informative and helpful to, what I presume to be, the target audience of these messages.
- The required time to calculate these suggestions will massively increase.
I'm not trying to understate this downside, this feature would definitely be off by default. The main use could be found in IDE's, that can find these suggestions in the background, but asking for these suggestions through the commandline is also reasonable.
The suggestions will not be as useful as in Agda, where the dependant types often steer the program even more, but can be very useful for writing for example instances of typeclasses.
(I have recently done a group project where we implemented exactly this, for a minimal toy language. In that language, we found that a type signature and one or two test cases were often enough to ensure that the hole fit that passed the tests had the correct definition for simple funtions like length, sum, product, etc.)
Using a form of breadth-first search to recursively find valid fits for typed holes, that may consist of an application of multiple functions. Ideally this could be implemented purely by calling the current implementation of hole fits and refinement holes.
instance Functor Tree where
fmap f (Leaf a) = _ fmap f (Node a b) = _
instance Traversable Tree where
traverse f (Leaf a) = _ traverse f (Node a b) = _
The idea is that ghc could generate the "least complicated" typecorrect solutions to these holes, and the appropriate solution should be in the top few results. "Least complicated" here is defined by the number of funtions, which corresponds to the depth in our search tree.
I'm very interested in implementing this feature myself, but would like to hear your thoughts about it.