From c82f61e4773341c3178c0b152678c10a317c004d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 11:11:04 -0800 Subject: [PATCH 1/7] Add some more debug show instances --- .../hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs | 9 +++++++++ 1 file changed, 9 insertions(+) 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 1dead7f8e4..037d103fde 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 From bf723722898d4325ef537ee14e01661fbb95eaf6 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 11:13:30 -0800 Subject: [PATCH 2/7] Construct a better method hypothesis --- .../hls-tactics-plugin.cabal | 1 + .../src/Ide/Plugin/Tactic/Context.hs | 28 +++--------------- .../src/Ide/Plugin/Tactic/Judgements/Theta.hs | 29 +++++++++++++++++++ .../src/Ide/Plugin/Tactic/LanguageServer.hs | 5 ++-- 4 files changed, 37 insertions(+), 26 deletions(-) create mode 100644 plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs diff --git a/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal b/plugins/hls-tactics-plugin/hls-tactics-plugin.cabal index a507a5e657..c6cae0a368 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..d5179c70bc 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs @@ -7,18 +7,15 @@ 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 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 TcType (substTy, tcSplitSigmaTy) +import Unify (tcUnifyTy) mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context @@ -33,23 +30,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 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..7d165326d0 --- /dev/null +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs @@ -0,0 +1,29 @@ +{-# LANGUAGE ViewPatterns #-} + +module Ide.Plugin.Tactic.Judgements.Theta where + +import Data.Maybe (fromMaybe) +import Development.IDE.GHC.Compat +import Generics.SYB +import GhcPlugins (EvVar) +import Ide.Plugin.Tactic.Machinery +import Ide.Plugin.Tactic.Types + + +getMethodHypothesisAtHole :: Data a => SrcSpan -> a -> Hypothesis CType +getMethodHypothesisAtHole dst + = Hypothesis + . fromMaybe [] + . foldMap methodHypothesis + . getEvidenceAtHole dst + + +getEvidenceAtHole :: Data a => SrcSpan -> a -> [PredType] +getEvidenceAtHole dst a = everything (<>) (mkQ mempty $ evbinds dst) a + + +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 e5b2aab4c1..6ef5c58b1b 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) @@ -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) From 9532aaf4f56cee29a29ea0ca3700b7753d2080a1 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 11:19:28 -0800 Subject: [PATCH 3/7] Haddock and slight cleanup --- .../src/Ide/Plugin/Tactic/Judgements/Theta.hs | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) 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 index 7d165326d0..fb596e34bb 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs @@ -1,6 +1,8 @@ {-# LANGUAGE ViewPatterns #-} -module Ide.Plugin.Tactic.Judgements.Theta where +module Ide.Plugin.Tactic.Judgements.Theta + ( getMethodHypothesisAtHole + ) where import Data.Maybe (fromMaybe) import Development.IDE.GHC.Compat @@ -10,18 +12,20 @@ import Ide.Plugin.Tactic.Machinery import Ide.Plugin.Tactic.Types -getMethodHypothesisAtHole :: Data a => SrcSpan -> a -> Hypothesis CType +------------------------------------------------------------------------------ +-- | 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 . fromMaybe [] . foldMap methodHypothesis - . getEvidenceAtHole dst - - -getEvidenceAtHole :: Data a => SrcSpan -> a -> [PredType] -getEvidenceAtHole dst a = everything (<>) (mkQ mempty $ evbinds dst) a + . (everything (<>) $ mkQ mempty $ evbinds dst) +------------------------------------------------------------------------------ +-- | 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 From 83549375a6933ab6fb4e023840e62a49b4bf5e04 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 11:23:40 -0800 Subject: [PATCH 4/7] Fix test --- .../test/UnificationSpec.hs | 23 ++++++++----------- 1 file changed, 9 insertions(+), 14 deletions(-) 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 From e4394d59bbd2857f0da318229f2a56bce52be78d Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 11:36:14 -0800 Subject: [PATCH 5/7] Add test --- .../src/Ide/Plugin/Tactic/Tactics.hs | 2 ++ .../hls-tactics-plugin/test/CodeAction/AutoSpec.hs | 1 + .../hls-tactics-plugin/test/golden/AutoThetaFix.hs | 13 +++++++++++++ .../test/golden/AutoThetaFix.hs.expected | 7 +++++++ 4 files changed, 23 insertions(+) create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs create mode 100644 plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs.expected 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 ab1932036a..c8a4095699 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/test/CodeAction/AutoSpec.hs b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs index 7e01a0a2eb..aa3eefb449 100644 --- a/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs +++ b/plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs @@ -45,6 +45,7 @@ spec = do autoTest 2 14 "FmapJoin.hs" autoTest 2 9 "Fgmap.hs" autoTest 4 19 "FmapJoinInLet.hs" + autoTest 12 10 "AutoThetaFix.hs" failing "flaky in CI" $ autoTest 2 11 "GoldenApplicativeThen.hs" 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) + From 2ad382ea6ce2ebb2d2660bcdb56cc29d1d0fd2fe Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 11:46:18 -0800 Subject: [PATCH 6/7] Remove unused bits of Context --- .../src/Ide/Plugin/Tactic/Context.hs | 17 ----------------- 1 file changed, 17 deletions(-) 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 d5179c70bc..4ccbf1c256 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs @@ -6,7 +6,6 @@ module Ide.Plugin.Tactic.Context where import Bag import Control.Arrow import Control.Monad.Reader -import Data.List import Data.Set (Set) import qualified Data.Set as S import Development.IDE.GHC.Compat @@ -14,8 +13,6 @@ import Ide.Plugin.Tactic.FeatureSet (FeatureSet) import Ide.Plugin.Tactic.Types import OccName import TcRnTypes -import TcType (substTy, tcSplitSigmaTy) -import Unify (tcUnifyTy) mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context @@ -44,18 +41,6 @@ excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name ] ------------------------------------------------------------------------------- --- | 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 @@ -71,5 +56,3 @@ getFunBindId _ = [] getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)] getCurrentDefinitions = asks ctxDefiningFuncs -getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)] -getModuleHypothesis = asks ctxModuleFuncs From 2f845e80d95ce6dcc979e8e7a6aa491f72d5e435 Mon Sep 17 00:00:00 2001 From: Sandy Maguire Date: Sun, 7 Mar 2021 13:57:37 -0800 Subject: [PATCH 7/7] Forgot to exclude `fail` from method choices --- .../src/Ide/Plugin/Tactic/Context.hs | 32 +++++-------------- .../src/Ide/Plugin/Tactic/Judgements/Theta.hs | 29 +++++++++++++---- 2 files changed, 31 insertions(+), 30 deletions(-) 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 4ccbf1c256..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,16 +3,14 @@ module Ide.Plugin.Tactic.Context where -import Bag -import Control.Arrow -import Control.Monad.Reader -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.Types -import OccName -import TcRnTypes +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 @@ -27,20 +25,6 @@ mkContext features locals tcg = Context } ------------------------------------------------------------------------------- --- | 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" - ] - - splitId :: Id -> (OccName, CType) splitId = occName &&& CType . idType 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 index fb596e34bb..9559f77756 100644 --- a/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs +++ b/plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs @@ -4,12 +4,14 @@ module Ide.Plugin.Tactic.Judgements.Theta ( getMethodHypothesisAtHole ) where -import Data.Maybe (fromMaybe) -import Development.IDE.GHC.Compat -import Generics.SYB -import GhcPlugins (EvVar) -import Ide.Plugin.Tactic.Machinery -import Ide.Plugin.Tactic.Types +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 ------------------------------------------------------------------------------ @@ -19,11 +21,26 @@ import Ide.Plugin.Tactic.Types 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]