The approach you're describing sounds a lot like proof-search in idris and agda (coq too, I thing), and it's nicer than you think: you're very often working wit

The approach you're describing sounds a lot like proof-search in idris and agda (coq too, I thing), and it's nicer than you think: you're very often working with definition-stubs created by automated case-splitting, which adds holes for you. Jumping around between holes becomes how you program, not an irritating interruption. But even aside from that, I don't think verb-first needs to be a showstopper: given that we've got type signatures, there's a lot of local context to work with. You're probably calling a function on one or more of the parameters, or else you're typing the leftmost-piece of a composition chain that gives you your result type. So throw Param1Type -> a, b -> ResultType etc at hoogle and populate a completion list. Completion doesn't have to be perfect to be useful. The hard part would be performance: if completion isn't fast, what's the point?