User-curated list of functions in scope

[isovector]

Let users decide which functions are in scope when running auto.

Maybe we could use a module level annotation with TH names?

[isovector]

from bgamari:

{-# LANGUAGE CPP #-}
module Plugin where

#if MIN_VERSION_ghc(9,0,0)
import GHC.Tc.Utils.Monad
import GHC.ThToHs (convertToHsExpr)
import GHC.Types.Basic (Origin(..))
import GHC.Utils.Error (MsgDoc)
#elif MIN_VERSION_ghc(8,10,0)
import TcRnMonad as GHC.Tc.Utils.Monad
import GHC.ThToHs (convertToHsExpr)
import RnEnv (lookupOccRn)
import Plugins (Plugin)
import BasicTypes (Origin(..))
import ErrUtils (MsgDoc)
import TcEnv (tcLookupId)
import Annotations
#endif

import GHC
import Language.Haskell.TH.Syntax as TH

resolveTHName :: TypecheckedModule -> TH.Name -> RealSrcSpan -> Ghc (Maybe Id)
resolveTHName tcm th_name src_span = do
  hsc_env <- getSession
  let (gbl_env, _) = tm_internals_ tcm
  (msgs, mb_id) <- liftIO $ GHC.Tc.Utils.Monad.initTcWithGbl hsc_env gbl_env src_span $ do
    Right rdr <- pure $ cvtName FromSource undefined th_name
    name <- lookupOccRn (unLoc rdr)
    tcLookupId (unLoc name)
  return mb_id

cvtName :: Origin -> SrcSpan -> TH.Name -> Either MsgDoc (Located GHC.RdrName)
cvtName origin span v =
  fmap (f . unLoc) (convertToHsExpr origin span (VarE v))
    where
      f (HsVar _ v') = v'
      f _ = error "this shouldn't happen"

[googleson78]

Inspiration could also be taken from Tritlos work - e.g. writing names in holes (this is also how you "add names to scope" for Agdas auto)?

Also this mr - https://gitlab.haskell.org/ghc/ghc/-/merge_requests/1766, which is unfortunately not ready yet.

[Tritlo]

Inspiration could also be taken from Tritlos work - e.g. writing names in holes (this is also how you "add names to scope" for Agdas auto)?

Also this mr - https://gitlab.haskell.org/ghc/ghc/-/merge_requests/1766, which is unfortunately not ready yet.

Yes! Unfortunately, that MR requires a change in syntax, which means going through the whole GHC proposal process first. Though I've since worked on hole-fit plugins and now have a running use case, so I'll pick this thread up again soon!