Perform name lookup directly in TacticsM (#1924)

* Move IO out of the Parser and into Tactics where it belongs

* Remove KnownThings, since we can look it up in IO now

* Sort imports

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: isovector

plugins/hls-tactics-plugin/src/Wingman/Context.hs

@@ -8,7 +8,7 @@ import           Data.Foldable.Extra (allM)
 import           Data.Maybe (fromMaybe, isJust, mapMaybe)
 import qualified Data.Set as S
 import           Development.IDE.GHC.Compat
-import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env)
+import           GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env, extractModule)
 import           InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
 import           OccName
 import           TcRnTypes
@@ -23,11 +23,11 @@ mkContext
     :: Config
     -> [(OccName, CType)]
     -> TcGblEnv
+    -> HscEnv
     -> ExternalPackageState
-    -> KnownThings
     -> [Evidence]
     -> Context
-mkContext cfg locals tcg eps kt ev = fix $ \ctx ->
+mkContext cfg locals tcg hscenv eps ev = fix $ \ctx ->
   Context
     { ctxDefiningFuncs
         = fmap (second $ coerce $ normalizeType ctx) locals
@@ -46,8 +46,10 @@ mkContext cfg locals tcg eps kt ev = fix $ \ctx ->
           (eps_inst_env eps)
           (tcg_inst_env tcg)
           (tcVisibleOrphanMods tcg)
-    , ctxKnownThings = kt
     , ctxTheta = evidenceToThetaType ev
+    , ctx_hscEnv = hscenv
+    , ctx_occEnv = tcg_rdr_env tcg
+    , ctx_module = extractModule tcg
     }
 
 
@@ -75,19 +77,6 @@ getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
 getCurrentDefinitions = asks ctxDefiningFuncs
 
 
-------------------------------------------------------------------------------
--- | Extract something from 'KnownThings'.
-getKnownThing :: MonadReader Context m => (KnownThings -> a) -> m a
-getKnownThing f = asks $ f . ctxKnownThings
-
-
-------------------------------------------------------------------------------
--- | Like 'getInstance', but uses a class from the 'KnownThings'.
-getKnownInstance :: MonadReader Context m => (KnownThings -> Class) -> [Type] -> m (Maybe (Class, PredType))
-getKnownInstance f tys = do
-  cls <- getKnownThing f
-  getInstance cls tys
-
 
 ------------------------------------------------------------------------------
 -- | Determine if there is an instance that exists for the given 'Class' at the

plugins/hls-tactics-plugin/src/Wingman/EmptyCase.hs

@@ -59,7 +59,6 @@ codeLensProvider state plId (CodeLensParams _ _ (TextDocumentIdentifier uri))
   | Just nfp <- uriToNormalizedFilePath $ toNormalizedUri uri = do
       let stale a = runStaleIde "codeLensProvider" state nfp a
 
-      cfg <- getTacticConfig plId
       ccs <- getClientCapabilities
       liftIO $ fromMaybeT (Right $ List []) $ do
         dflags <- getIdeDynflags state nfp

plugins/hls-tactics-plugin/src/Wingman/GHC.hs

@@ -4,11 +4,12 @@
 module Wingman.GHC where
 
 import           Bag (bagToList)
+import           Class (classTyVars)
 import           ConLike
-import           Control.Applicative (empty)
 import           Control.Monad.State
 import           Control.Monad.Trans.Maybe (MaybeT(..))
 import           CoreUtils (exprType)
+import           Data.Bool (bool)
 import           Data.Function (on)
 import           Data.Functor ((<&>))
 import           Data.List (isPrefixOf)
@@ -18,22 +19,21 @@ import           Data.Set (Set)
 import qualified Data.Set as S
 import           Data.Traversable
 import           DataCon
-import           Development.IDE (HscEnvEq (hscEnv))
-import           Development.IDE.Core.Compile (lookupName)
 import           Development.IDE.GHC.Compat hiding (exprType)
 import           DsExpr (dsExpr)
 import           DsMonad (initDs)
 import           FamInst (tcLookupDataFamInst_maybe)
 import           FamInstEnv (normaliseType)
 import           GHC.SourceGen (lambda)
 import           Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
-import           GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal))
+import           GhcPlugins (Role (Nominal))
 import           OccName
 import           TcRnMonad
 import           TcType
 import           TyCoRep
 import           Type
 import           TysWiredIn (charTyCon, doubleTyCon, floatTyCon, intTyCon)
+import           Unify
 import           Unique
 import           Var
 import           Wingman.Types
@@ -323,40 +323,6 @@ unXPat (XPat (L _ pat)) = unXPat pat
 unXPat pat              = pat
 
 
-------------------------------------------------------------------------------
--- | Build a 'KnownThings'.
-knownThings :: TcGblEnv -> HscEnvEq -> MaybeT IO KnownThings
-knownThings tcg hscenv= do
-  let cls = knownClass tcg hscenv
-  KnownThings
-    <$> cls (mkClsOcc "Semigroup")
-    <*> cls (mkClsOcc "Monoid")
-
-
-------------------------------------------------------------------------------
--- | Like 'knownThing' but specialized to classes.
-knownClass :: TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO Class
-knownClass = knownThing $ \case
-  ATyCon tc -> tyConClass_maybe tc
-  _         -> Nothing
-
-
-------------------------------------------------------------------------------
--- | Helper function for defining 'knownThings'.
-knownThing :: (TyThing -> Maybe a) -> TcGblEnv -> HscEnvEq -> OccName -> MaybeT IO a
-knownThing f tcg hscenv occ = do
-  let modul = extractModule tcg
-      rdrenv = tcg_rdr_env tcg
-
-  case lookupOccEnv rdrenv occ of
-    Nothing -> empty
-    Just elts -> do
-      mvar <- lift $ lookupName (hscEnv hscenv) modul $ gre_name $ head elts
-      case mvar of
-        Just tt -> liftMaybe $ f tt
-        _ -> empty
-
-
 liftMaybe :: Monad m => Maybe a -> MaybeT m a
 liftMaybe a = MaybeT $ pure a
 
@@ -396,3 +362,34 @@ expandTyFam :: Context -> Type -> Type
 expandTyFam ctx = snd . normaliseType  (ctxFamInstEnvs ctx) Nominal
 
 
+------------------------------------------------------------------------------
+-- | Like 'tcUnifyTy', but takes a list of skolems to prevent unification of.
+tryUnifyUnivarsButNotSkolems :: Set TyVar -> CType -> CType -> Maybe TCvSubst
+tryUnifyUnivarsButNotSkolems skolems goal inst =
+  case tcUnifyTysFG
+         (bool BindMe Skolem . flip S.member skolems)
+         [unCType inst]
+         [unCType goal] of
+    Unifiable subst -> pure subst
+    _               -> Nothing
+
+
+updateSubst :: TCvSubst -> TacticState -> TacticState
+updateSubst subst s = s { ts_unifier = unionTCvSubst subst (ts_unifier s) }
+
+
+------------------------------------------------------------------------------
+-- | Get the class methods of a 'PredType', correctly dealing with
+-- instantiation of quantified class types.
+methodHypothesis :: PredType -> Maybe [HyInfo CType]
+methodHypothesis ty = do
+  (tc, apps) <- splitTyConApp_maybe ty
+  cls <- tyConClass_maybe tc
+  let methods = classMethods cls
+      tvs     = classTyVars cls
+      subst   = zipTvSubst tvs apps
+  pure $ methods <&> \method ->
+    let (_, _, ty) = tcSplitSigmaTy $ idType method
+    in ( HyInfo (occName method) (ClassMethodPrv $ Uniquely cls) $ CType $ substTy subst ty
+       )
+

plugins/hls-tactics-plugin/src/Wingman/Judgements/Theta.hs

@@ -32,7 +32,7 @@ import           TcEvidence
 import           TcType (substTy)
 import           TcType (tcTyConAppTyCon_maybe)
 import           TysPrim (eqPrimTyCon)
-import           Wingman.Machinery
+import           Wingman.GHC
 import           Wingman.Types
 
 

plugins/hls-tactics-plugin/src/Wingman/KnownStrategies.hs

@@ -2,12 +2,12 @@ module Wingman.KnownStrategies where
 
 import Control.Monad.Error.Class
 import Data.Foldable (for_)
-import OccName (mkVarOcc)
+import OccName (mkVarOcc, mkClsOcc)
 import Refinery.Tactic
-import Wingman.Context (getCurrentDefinitions, getKnownInstance)
+import Wingman.Context (getCurrentDefinitions)
 import Wingman.Judgements (jGoal)
 import Wingman.KnownStrategies.QuickCheck (deriveArbitrary)
-import Wingman.Machinery (tracing)
+import Wingman.Machinery (tracing, getKnownInstance)
 import Wingman.Tactics
 import Wingman.Types
 
@@ -55,7 +55,7 @@ deriveMappend = do
   destructAll
   split
   g <- goal
-  minst <- getKnownInstance kt_semigroup
+  minst <- getKnownInstance (mkClsOcc "Semigroup")
          . pure
          . unCType
          $ jGoal g
@@ -77,7 +77,7 @@ deriveMempty :: TacticsM ()
 deriveMempty = do
   split
   g <- goal
-  minst <- getKnownInstance kt_monoid [unCType $ jGoal g]
+  minst <- getKnownInstance (mkClsOcc "Monoid") [unCType $ jGoal g]
   for_ minst $ \(cls, df) -> do
     applyMethod cls df $ mkVarOcc "mempty"
   try assumption

plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

@@ -44,7 +44,6 @@ import           Development.IDE.Spans.LocalBindings (Bindings, getDefiningBindi
 import qualified FastString
 import           GHC.Generics (Generic)
 import           Generics.SYB hiding (Generic)
-import           GhcPlugins (extractModule)
 import           GhcPlugins (tupleDataCon, consDataCon, substTyAddInScope, ExternalPackageState, HscEnv (hsc_EPS), unpackFS)
 import qualified Ide.Plugin.Config as Plugin
 import           Ide.Plugin.Properties
@@ -59,13 +58,12 @@ import           OccName
 import           Prelude hiding (span)
 import           Retrie (transformA)
 import           SrcLoc (containsSpan)
-import           TcRnTypes (tcg_binds, TcGblEnv (tcg_rdr_env))
+import           TcRnTypes (tcg_binds, TcGblEnv)
 import           Wingman.Context
 import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Judgements.SYB (everythingContaining, metaprogramQ)
 import           Wingman.Judgements.Theta
-import           Wingman.Metaprogramming.Lexer (ParserContext(..))
 import           Wingman.Range
 import           Wingman.StaticPlugin (pattern WingmanMetaprogram, pattern MetaprogramSyntax)
 import           Wingman.Types
@@ -215,9 +213,8 @@ judgementForHole state nfp range cfg = do
       -- involved, so it's not crucial to track ages.
       let henv = untrackedStaleValue $ hscenv
       eps <- liftIO $ readIORef $ hsc_EPS $ hscEnv henv
-      kt <- knownThings (untrackedStaleValue tcg) henv
 
-      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg eps kt
+      (jdg, ctx) <- liftMaybe $ mkJudgementAndContext cfg g binds new_rss tcg (hscEnv henv) eps
       let mp = getMetaprogramAtSpan (fmap RealSrcSpan tcg_rss) tcg_t
 
       dflags <- getIdeDynflags state nfp
@@ -240,10 +237,10 @@ mkJudgementAndContext
     -> TrackedStale Bindings
     -> Tracked 'Current RealSrcSpan
     -> TrackedStale TcGblEnv
+    -> HscEnv
     -> ExternalPackageState
-    -> KnownThings
     -> Maybe (Judgement, Context)
-mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) eps kt = do
+mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgmap) hscenv eps = do
   binds_rss <- mapAgeFrom bmap rss
   tcg_rss <- mapAgeFrom tcgmap rss
 
@@ -253,8 +250,8 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
                 $ unTrack
                 $ getDefiningBindings <$> binds <*> binds_rss)
               (unTrack tcg)
+              hscenv
               eps
-              kt
               evidence
       top_provs = getRhsPosVals tcg_rss tcs
       already_destructed = getAlreadyDestructed (fmap RealSrcSpan tcg_rss) tcs
@@ -598,25 +595,3 @@ getMetaprogramAtSpan (unTrack -> ss)
   . tcg_binds
   . unTrack
 
-
-------------------------------------------------------------------------------
--- | The metaprogram parser needs the ability to lookup terms from the module
--- and imports. The 'ParserContext' contains everything we need to find that
--- stuff.
-getParserState
-    :: IdeState
-    -> NormalizedFilePath
-    -> Context
-    -> MaybeT IO ParserContext
-getParserState state nfp ctx = do
-  let stale a = runStaleIde "getParserState" state nfp a
-
-  TrackedStale (unTrack -> tcmod) _  <- stale TypeCheck
-  TrackedStale (unTrack -> hscenv) _ <- stale GhcSessionDeps
-
-  let tcgblenv = tmrTypechecked tcmod
-      modul = extractModule tcgblenv
-      rdrenv = tcg_rdr_env tcgblenv
-
-  pure $ ParserContext (hscEnv hscenv) rdrenv modul ctx
-

plugins/hls-tactics-plugin/src/Wingman/LanguageServer/Metaprogram.hs

@@ -10,7 +10,6 @@ module Wingman.LanguageServer.Metaprogram
 
 import           Control.Applicative (empty)
 import           Control.Monad
-import           Control.Monad.Reader (runReaderT)
 import           Control.Monad.Trans
 import           Control.Monad.Trans.Maybe
 import           Data.List (find)
@@ -52,8 +51,7 @@ hoverProvider state plId (HoverParams (TextDocumentIdentifier uri) (unsafeMkCurr
             Just (trss, program) -> do
               let tr_range = fmap realSrcSpanToRange trss
               HoleJudgment{hj_jdg=jdg, hj_ctx=ctx} <- judgementForHole state nfp tr_range cfg
-              ps <- getParserState state nfp ctx
-              z <- liftIO $ flip runReaderT ps $ attempt_it ctx jdg $ T.unpack program
+              z <- liftIO $ attempt_it ctx jdg $ T.unpack program
               pure $ Hover
                 { _contents = HoverContents
                             $ MarkupContent MkMarkdown

plugins/hls-tactics-plugin/src/Wingman/LanguageServer/TacticProviders.hs

@@ -12,7 +12,6 @@ module Wingman.LanguageServer.TacticProviders
   ) where
 
 import           Control.Monad
-import           Control.Monad.Reader (runReaderT)
 import           Data.Aeson
 import           Data.Bool (bool)
 import           Data.Coerce
@@ -34,27 +33,26 @@ import           Wingman.Auto
 import           Wingman.GHC
 import           Wingman.Judgements
 import           Wingman.Machinery (useNameFromHypothesis)
-import           Wingman.Metaprogramming.Lexer (ParserContext)
 import           Wingman.Metaprogramming.Parser (parseMetaprogram)
 import           Wingman.Tactics
 import           Wingman.Types
 
 
 ------------------------------------------------------------------------------
 -- | A mapping from tactic commands to actual tactics for refinery.
-commandTactic :: ParserContext -> TacticCommand -> T.Text -> IO (TacticsM ())
-commandTactic _ Auto                   = pure . const auto
-commandTactic _ Intros                 = pure . const intros
-commandTactic _ Destruct               = pure . useNameFromHypothesis destruct . mkVarOcc . T.unpack
-commandTactic _ DestructPun            = pure . useNameFromHypothesis destructPun . mkVarOcc . T.unpack
-commandTactic _ Homomorphism           = pure . useNameFromHypothesis homo . mkVarOcc . T.unpack
-commandTactic _ DestructLambdaCase     = pure . const destructLambdaCase
-commandTactic _ HomomorphismLambdaCase = pure . const homoLambdaCase
-commandTactic _ DestructAll            = pure . const destructAll
-commandTactic _ UseDataCon             = pure . userSplit . mkVarOcc . T.unpack
-commandTactic _ Refine                 = pure . const refine
-commandTactic _ BeginMetaprogram       = pure . const metaprogram
-commandTactic c RunMetaprogram         = flip runReaderT c . parseMetaprogram
+commandTactic :: TacticCommand -> T.Text -> TacticsM ()
+commandTactic Auto                   = const auto
+commandTactic Intros                 = const intros
+commandTactic Destruct               = useNameFromHypothesis destruct . mkVarOcc . T.unpack
+commandTactic DestructPun            = useNameFromHypothesis destructPun . mkVarOcc . T.unpack
+commandTactic Homomorphism           = useNameFromHypothesis homo . mkVarOcc . T.unpack
+commandTactic DestructLambdaCase     = const destructLambdaCase
+commandTactic HomomorphismLambdaCase = const homoLambdaCase
+commandTactic DestructAll            = const destructAll
+commandTactic UseDataCon             = userSplit . mkVarOcc . T.unpack
+commandTactic Refine                 = const refine
+commandTactic BeginMetaprogram       = const metaprogram
+commandTactic RunMetaprogram         = parseMetaprogram
 
 
 ------------------------------------------------------------------------------