a) ideally, Exference would take into account all locally defined (or even all visible) functions. This is problematic, as one generally has to be careful adding too many / the wrong functions to the environment because it can blow up the search space. There might be some heuristics to determine what can safely be added; alternatively the user could selectively add functions.
Is this a major problem? As far as I can tell Agda's automated proof search does not take into account any globally defined functions or constants and yet is still (moderately) useful. Have you seen the recent announcement of Mote, a Vim plugin trying to replicate something akin to Agda-mode for Haskell? https://github.com/imeckler/mote It seems that marrying these two projects, extending Mote with a search facility based on exference, would be a good idea?