diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index a96106fb45..0643624a53 100644 --- a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal +++ b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal @@ -34,6 +34,7 @@ library Ide.Plugin.Tactic.FeatureSet Ide.Plugin.Tactic.GHC Ide.Plugin.Tactic.Judgements + Ide.Plugin.Tactic.Judgements.Theta Ide.Plugin.Tactic.KnownStrategies Ide.Plugin.Tactic.KnownStrategies.QuickCheck Ide.Plugin.Tactic.LanguageServer diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs index f13421b4e1..28df47b695 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs @@ -3,22 +3,14 @@ module Ide.Plugin.Tactic.Context where -import Bag -import Control.Arrow -import Control.Monad.Reader -import Data.List -import Data.Maybe (mapMaybe) -import Data.Set (Set) -import qualified Data.Set as S -import Development.IDE.GHC.Compat -import Ide.Plugin.Tactic.FeatureSet (FeatureSet) -import Ide.Plugin.Tactic.GHC (tacticsThetaTy) -import Ide.Plugin.Tactic.Machinery (methodHypothesis) -import Ide.Plugin.Tactic.Types -import OccName -import TcRnTypes -import TcType (substTy, tcSplitSigmaTy) -import Unify (tcUnifyTy) +import Bag +import Control.Arrow +import Control.Monad.Reader +import Development.IDE.GHC.Compat +import Ide.Plugin.Tactic.FeatureSet (FeatureSet) +import Ide.Plugin.Tactic.Types +import OccName +import TcRnTypes mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context @@ -33,49 +25,6 @@ mkContext features locals tcg = Context } ------------------------------------------------------------------------------- --- | Find all of the class methods that exist from the givens in the context. -contextMethodHypothesis :: Context -> Hypothesis CType -contextMethodHypothesis ctx - = Hypothesis - . excludeForbiddenMethods - . join - . concatMap - ( mapMaybe methodHypothesis - . tacticsThetaTy - . unCType - ) - . mapMaybe (definedThetaType ctx) - . fmap fst - $ ctxDefiningFuncs ctx - - ------------------------------------------------------------------------------- --- | Many operations are defined in typeclasses for performance reasons, rather --- than being a true part of the class. This function filters out those, in --- order to keep our hypothesis space small. -excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a] -excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name) - where - forbiddenMethods :: Set OccName - forbiddenMethods = S.map mkVarOcc $ S.fromList - [ -- monadfail - "fail" - ] - - ------------------------------------------------------------------------------- --- | Given the name of a function that exists in 'ctxDefiningFuncs', get its --- theta type. -definedThetaType :: Context -> OccName -> Maybe CType -definedThetaType ctx name = do - (_, CType mono) <- find ((== name) . fst) $ ctxDefiningFuncs ctx - (_, CType poly) <- find ((== name) . fst) $ ctxModuleFuncs ctx - let (_, _, poly') = tcSplitSigmaTy poly - subst <- tcUnifyTy poly' mono - pure $ CType $ substTy subst $ snd $ splitForAllTys poly - - splitId :: Id -> (OccName, CType) splitId = occName &&& CType . idType @@ -91,5 +40,3 @@ getFunBindId _ = [] getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)] getCurrentDefinitions = asks ctxDefiningFuncs -getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)] -getModuleHypothesis = asks ctxModuleFuncs diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs new file mode 100644 index 0000000000..9559f77756 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Judgements.Theta + ( getMethodHypothesisAtHole + ) where + +import Data.Maybe (fromMaybe) +import Data.Set (Set) +import qualified Data.Set as S +import Development.IDE.GHC.Compat +import Generics.SYB +import GhcPlugins (EvVar, mkVarOcc) +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Types + + +------------------------------------------------------------------------------ +-- | Create a 'Hypothesis' containing 'ClassMethodPrv' provenance. For every +-- dictionary that is in scope at the given 'SrcSpan', find every method and +-- superclass method available. +getMethodHypothesisAtHole :: SrcSpan -> LHsBinds GhcTc -> Hypothesis CType +getMethodHypothesisAtHole dst + = Hypothesis + . excludeForbiddenMethods + . fromMaybe [] + . foldMap methodHypothesis + . (everything (<>) $ mkQ mempty $ evbinds dst) + + +------------------------------------------------------------------------------ +-- | Many operations are defined in typeclasses for performance reasons, rather +-- than being a true part of the class. This function filters out those, in +-- order to keep our hypothesis space small. +excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a] +excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name) + where + forbiddenMethods :: Set OccName + forbiddenMethods = S.map mkVarOcc $ S.fromList + [ -- monadfail + "fail" + ] + + +------------------------------------------------------------------------------ +-- | Extract the types of the evidence bindings in scope. +evbinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType] +evbinds dst (L src (AbsBinds _ _ h _ _ _ _)) + | dst `isSubspanOf` src = fmap idType h +evbinds _ _ = [] + diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs index 671d16bffd..172e847b38 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs @@ -44,6 +44,7 @@ import Ide.Plugin.Tactic.Context import Ide.Plugin.Tactic.FeatureSet import Ide.Plugin.Tactic.GHC import Ide.Plugin.Tactic.Judgements +import Ide.Plugin.Tactic.Judgements.Theta (getMethodHypothesisAtHole) import Ide.Plugin.Tactic.Range import Ide.Plugin.Tactic.Types import Language.LSP.Server (MonadLsp, sendNotification) @@ -139,7 +140,7 @@ mkJudgementAndContext -> TcModuleResult -> (Judgement, Context) mkJudgementAndContext features g binds rss tcmod = do - let tcg = tmrTypechecked tcmod + let tcg = tmrTypechecked tcmod tcs = tcg_binds tcg ctx = mkContext features (mapMaybe (sequenceA . (occName *** coerce)) @@ -148,7 +149,7 @@ mkJudgementAndContext features g binds rss tcmod = do top_provs = getRhsPosVals rss tcs local_hy = spliceProvenance top_provs $ hypothesisFromBindings rss binds - cls_hy = contextMethodHypothesis ctx + cls_hy = getMethodHypothesisAtHole (RealSrcSpan rss) tcs in ( mkFirstJudgement (local_hy <> cls_hy) (isRhsHole rss tcs) diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs index 7af41cbacd..9179f5d677 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs @@ -68,6 +68,8 @@ assume name = rule $ \jdg -> do recursion :: TacticsM () +-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test, +-- presumably due to running afoul of 'requireConcreteHole'. Look into this! recursion = requireConcreteHole $ tracing "recursion" $ do defs <- getCurrentDefinitions attemptOn (const defs) $ \(name, ty) -> markRecursion $ do diff --git a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs index 72e4daa823..312b765828 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs @@ -124,6 +124,12 @@ instance Show CType where instance Show OccName where show = unsafeRender +instance Show Name where + show = unsafeRender + +instance Show Type where + show = unsafeRender + instance Show Var where show = unsafeRender @@ -142,6 +148,9 @@ instance Show (HsExpr GhcPs) where instance Show (Pat GhcPs) where show = unsafeRender +instance Show (LHsSigType GhcPs) where + show = unsafeRender + ------------------------------------------------------------------------------ -- | The state that should be shared between subgoals. Extracts move towards diff --git a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index c448bf8715..995b9dc29d 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs @@ -47,6 +47,7 @@ spec = do autoTest 2 9 "Fgmap.hs" autoTest 4 19 "FmapJoinInLet.hs" autoTest 9 12 "AutoEndo.hs" + autoTest 12 10 "AutoThetaFix.hs" failing "flaky in CI" $ autoTest 2 11 "GoldenApplicativeThen.hs" diff --git a/plugins/hls-tactics-plugin/test/UnificationSpec.hs b/plugins/hls-tactics-plugin/test/UnificationSpec.hs index ef47cbd174..013193fec8 100644 --- a/plugins/hls-tactics-plugin/test/UnificationSpec.hs +++ b/plugins/hls-tactics-plugin/test/UnificationSpec.hs @@ -4,25 +4,20 @@ module UnificationSpec where import Control.Arrow -import Data.Bool (bool) -import Data.Functor ((<&>)) -import Data.Maybe (mapMaybe) -import qualified Data.Set as S +import Data.Bool (bool) +import Data.Functor ((<&>)) +import Data.Maybe (mapMaybe) +import qualified Data.Set as S import Data.Traversable -import Data.Tuple (swap) -import Ide.Plugin.Tactic.Debug +import Data.Tuple (swap) import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Types -import TcType (substTy, tcGetTyVar_maybe) +import TcType (substTy, tcGetTyVar_maybe) import Test.Hspec import Test.QuickCheck -import Type (mkTyVarTy) -import TysPrim (alphaTyVars) -import TysWiredIn (mkBoxedTupleTy) - - -instance Show Type where - show = unsafeRender +import Type (mkTyVarTy) +import TysPrim (alphaTyVars) +import TysWiredIn (mkBoxedTupleTy) spec :: Spec diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs b/plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs new file mode 100644 index 0000000000..014e6441da --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs @@ -0,0 +1,13 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +data Fix f a = Fix (f (Fix f a)) + +instance ( Functor f + -- FIXME(sandy): Unfortunately, the recursion tactic fails to fire + -- on this case. By explicitly adding the @Functor (Fix f)@ + -- dictionary, we can get Wingman to generate the right definition. + , Functor (Fix f) + ) => Functor (Fix f) where + fmap = _ + diff --git a/plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs.expected b/plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs.expected new file mode 100644 index 0000000000..21a5b69691 --- /dev/null +++ b/plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs.expected @@ -0,0 +1,7 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE UndecidableInstances #-} + +data Fix f a = Fix (f (Fix f a)) +instance (Functor f, Functor (Fix f)) => Functor (Fix f) where + fmap fab (Fix fffa) = Fix (fmap (fmap fab) fffa) +