Skip to content

Commit 16adab7

Browse files
isovectorpepeiborra
isovector
and
pepeiborra
authored
Pull Wingman's method hypotheses directly from in-scope dicts (#1517)
* Add some more debug show instances * Construct a better method hypothesis * Haddock and slight cleanup * Fix test * Add test * Remove unused bits of Context * Forgot to exclude `fail` from method choices Co-authored-by: Pepe Iborra <[email protected]>
1 parent 6fbc602 commit 16adab7

File tree

10 files changed

+103
-77
lines changed

10 files changed

+103
-77
lines changed

‎plugins/hls-tactics-plugin/hls-tactics-plugin.cabal

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ library
3434
Ide.Plugin.Tactic.FeatureSet
3535
Ide.Plugin.Tactic.GHC
3636
Ide.Plugin.Tactic.Judgements
37+
Ide.Plugin.Tactic.Judgements.Theta
3738
Ide.Plugin.Tactic.KnownStrategies
3839
Ide.Plugin.Tactic.KnownStrategies.QuickCheck
3940
Ide.Plugin.Tactic.LanguageServer

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Context.hs

Lines changed: 8 additions & 61 deletions
Original file line numberDiff line numberDiff line change
@@ -3,22 +3,14 @@
33

44
module Ide.Plugin.Tactic.Context where
55

6-
import Bag
7-
import Control.Arrow
8-
import Control.Monad.Reader
9-
import Data.List
10-
import Data.Maybe (mapMaybe)
11-
import Data.Set (Set)
12-
import qualified Data.Set as S
13-
import Development.IDE.GHC.Compat
14-
import Ide.Plugin.Tactic.FeatureSet (FeatureSet)
15-
import Ide.Plugin.Tactic.GHC (tacticsThetaTy)
16-
import Ide.Plugin.Tactic.Machinery (methodHypothesis)
17-
import Ide.Plugin.Tactic.Types
18-
import OccName
19-
import TcRnTypes
20-
import TcType (substTy, tcSplitSigmaTy)
21-
import Unify (tcUnifyTy)
6+
import Bag
7+
import Control.Arrow
8+
import Control.Monad.Reader
9+
import Development.IDE.GHC.Compat
10+
import Ide.Plugin.Tactic.FeatureSet (FeatureSet)
11+
import Ide.Plugin.Tactic.Types
12+
import OccName
13+
import TcRnTypes
2214

2315

2416
mkContext :: FeatureSet -> [(OccName, CType)] -> TcGblEnv -> Context
@@ -33,49 +25,6 @@ mkContext features locals tcg = Context
3325
}
3426

3527

36-
------------------------------------------------------------------------------
37-
-- | Find all of the class methods that exist from the givens in the context.
38-
contextMethodHypothesis :: Context -> Hypothesis CType
39-
contextMethodHypothesis ctx
40-
= Hypothesis
41-
. excludeForbiddenMethods
42-
. join
43-
. concatMap
44-
( mapMaybe methodHypothesis
45-
. tacticsThetaTy
46-
. unCType
47-
)
48-
. mapMaybe (definedThetaType ctx)
49-
. fmap fst
50-
$ ctxDefiningFuncs ctx
51-
52-
53-
------------------------------------------------------------------------------
54-
-- | Many operations are defined in typeclasses for performance reasons, rather
55-
-- than being a true part of the class. This function filters out those, in
56-
-- order to keep our hypothesis space small.
57-
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
58-
excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
59-
where
60-
forbiddenMethods :: Set OccName
61-
forbiddenMethods = S.map mkVarOcc $ S.fromList
62-
[ -- monadfail
63-
"fail"
64-
]
65-
66-
67-
------------------------------------------------------------------------------
68-
-- | Given the name of a function that exists in 'ctxDefiningFuncs', get its
69-
-- theta type.
70-
definedThetaType :: Context -> OccName -> Maybe CType
71-
definedThetaType ctx name = do
72-
(_, CType mono) <- find ((== name) . fst) $ ctxDefiningFuncs ctx
73-
(_, CType poly) <- find ((== name) . fst) $ ctxModuleFuncs ctx
74-
let (_, _, poly') = tcSplitSigmaTy poly
75-
subst <- tcUnifyTy poly' mono
76-
pure $ CType $ substTy subst $ snd $ splitForAllTys poly
77-
78-
7928
splitId :: Id -> (OccName, CType)
8029
splitId = occName &&& CType . idType
8130

@@ -91,5 +40,3 @@ getFunBindId _ = []
9140
getCurrentDefinitions :: MonadReader Context m => m [(OccName, CType)]
9241
getCurrentDefinitions = asks ctxDefiningFuncs
9342

94-
getModuleHypothesis :: MonadReader Context m => m [(OccName, CType)]
95-
getModuleHypothesis = asks ctxModuleFuncs

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Judgements/Theta.hs

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
{-# LANGUAGE ViewPatterns #-}
2+
3+
module Ide.Plugin.Tactic.Judgements.Theta
4+
( getMethodHypothesisAtHole
5+
) where
6+
7+
import Data.Maybe (fromMaybe)
8+
import Data.Set (Set)
9+
import qualified Data.Set as S
10+
import Development.IDE.GHC.Compat
11+
import Generics.SYB
12+
import GhcPlugins (EvVar, mkVarOcc)
13+
import Ide.Plugin.Tactic.Machinery
14+
import Ide.Plugin.Tactic.Types
15+
16+
17+
------------------------------------------------------------------------------
18+
-- | Create a 'Hypothesis' containing 'ClassMethodPrv' provenance. For every
19+
-- dictionary that is in scope at the given 'SrcSpan', find every method and
20+
-- superclass method available.
21+
getMethodHypothesisAtHole :: SrcSpan -> LHsBinds GhcTc -> Hypothesis CType
22+
getMethodHypothesisAtHole dst
23+
= Hypothesis
24+
. excludeForbiddenMethods
25+
. fromMaybe []
26+
. foldMap methodHypothesis
27+
. (everything (<>) $ mkQ mempty $ evbinds dst)
28+
29+
30+
------------------------------------------------------------------------------
31+
-- | Many operations are defined in typeclasses for performance reasons, rather
32+
-- than being a true part of the class. This function filters out those, in
33+
-- order to keep our hypothesis space small.
34+
excludeForbiddenMethods :: [HyInfo a] -> [HyInfo a]
35+
excludeForbiddenMethods = filter (not . flip S.member forbiddenMethods . hi_name)
36+
where
37+
forbiddenMethods :: Set OccName
38+
forbiddenMethods = S.map mkVarOcc $ S.fromList
39+
[ -- monadfail
40+
"fail"
41+
]
42+
43+
44+
------------------------------------------------------------------------------
45+
-- | Extract the types of the evidence bindings in scope.
46+
evbinds :: SrcSpan -> LHsBindLR GhcTc GhcTc -> [PredType]
47+
evbinds dst (L src (AbsBinds _ _ h _ _ _ _))
48+
| dst `isSubspanOf` src = fmap idType h
49+
evbinds _ _ = []
50+

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/LanguageServer.hs

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -44,6 +44,7 @@ import Ide.Plugin.Tactic.Context
4444
import Ide.Plugin.Tactic.FeatureSet
4545
import Ide.Plugin.Tactic.GHC
4646
import Ide.Plugin.Tactic.Judgements
47+
import Ide.Plugin.Tactic.Judgements.Theta (getMethodHypothesisAtHole)
4748
import Ide.Plugin.Tactic.Range
4849
import Ide.Plugin.Tactic.Types
4950
import Language.LSP.Server (MonadLsp, sendNotification)
@@ -139,7 +140,7 @@ mkJudgementAndContext
139140
-> TcModuleResult
140141
-> (Judgement, Context)
141142
mkJudgementAndContext features g binds rss tcmod = do
142-
let tcg = tmrTypechecked tcmod
143+
let tcg = tmrTypechecked tcmod
143144
tcs = tcg_binds tcg
144145
ctx = mkContext features
145146
(mapMaybe (sequenceA . (occName *** coerce))
@@ -148,7 +149,7 @@ mkJudgementAndContext features g binds rss tcmod = do
148149
top_provs = getRhsPosVals rss tcs
149150
local_hy = spliceProvenance top_provs
150151
$ hypothesisFromBindings rss binds
151-
cls_hy = contextMethodHypothesis ctx
152+
cls_hy = getMethodHypothesisAtHole (RealSrcSpan rss) tcs
152153
in ( mkFirstJudgement
153154
(local_hy <> cls_hy)
154155
(isRhsHole rss tcs)

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Tactics.hs

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -68,6 +68,8 @@ assume name = rule $ \jdg -> do
6868

6969

7070
recursion :: TacticsM ()
71+
-- TODO(sandy): This tactic doesn't fire for the @AutoThetaFix@ golden test,
72+
-- presumably due to running afoul of 'requireConcreteHole'. Look into this!
7173
recursion = requireConcreteHole $ tracing "recursion" $ do
7274
defs <- getCurrentDefinitions
7375
attemptOn (const defs) $ \(name, ty) -> markRecursion $ do

‎plugins/hls-tactics-plugin/src/Ide/Plugin/Tactic/Types.hs

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,12 @@ instance Show CType where
124124
instance Show OccName where
125125
show = unsafeRender
126126

127+
instance Show Name where
128+
show = unsafeRender
129+
130+
instance Show Type where
131+
show = unsafeRender
132+
127133
instance Show Var where
128134
show = unsafeRender
129135

@@ -142,6 +148,9 @@ instance Show (HsExpr GhcPs) where
142148
instance Show (Pat GhcPs) where
143149
show = unsafeRender
144150

151+
instance Show (LHsSigType GhcPs) where
152+
show = unsafeRender
153+
145154

146155
------------------------------------------------------------------------------
147156
-- | The state that should be shared between subgoals. Extracts move towards

‎plugins/hls-tactics-plugin/test/CodeAction/AutoSpec.hs

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -47,6 +47,7 @@ spec = do
4747
autoTest 2 9 "Fgmap.hs"
4848
autoTest 4 19 "FmapJoinInLet.hs"
4949
autoTest 9 12 "AutoEndo.hs"
50+
autoTest 12 10 "AutoThetaFix.hs"
5051

5152
failing "flaky in CI" $
5253
autoTest 2 11 "GoldenApplicativeThen.hs"

‎plugins/hls-tactics-plugin/test/UnificationSpec.hs

Lines changed: 9 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -4,25 +4,20 @@
44
module UnificationSpec where
55

66
import Control.Arrow
7-
import Data.Bool (bool)
8-
import Data.Functor ((<&>))
9-
import Data.Maybe (mapMaybe)
10-
import qualified Data.Set as S
7+
import Data.Bool (bool)
8+
import Data.Functor ((<&>))
9+
import Data.Maybe (mapMaybe)
10+
import qualified Data.Set as S
1111
import Data.Traversable
12-
import Data.Tuple (swap)
13-
import Ide.Plugin.Tactic.Debug
12+
import Data.Tuple (swap)
1413
import Ide.Plugin.Tactic.Machinery
1514
import Ide.Plugin.Tactic.Types
16-
import TcType (substTy, tcGetTyVar_maybe)
15+
import TcType (substTy, tcGetTyVar_maybe)
1716
import Test.Hspec
1817
import Test.QuickCheck
19-
import Type (mkTyVarTy)
20-
import TysPrim (alphaTyVars)
21-
import TysWiredIn (mkBoxedTupleTy)
22-
23-
24-
instance Show Type where
25-
show = unsafeRender
18+
import Type (mkTyVarTy)
19+
import TysPrim (alphaTyVars)
20+
import TysWiredIn (mkBoxedTupleTy)
2621

2722

2823
spec :: Spec

‎plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{-# LANGUAGE FlexibleContexts #-}
2+
{-# LANGUAGE UndecidableInstances #-}
3+
4+
data Fix f a = Fix (f (Fix f a))
5+
6+
instance ( Functor f
7+
-- FIXME(sandy): Unfortunately, the recursion tactic fails to fire
8+
-- on this case. By explicitly adding the @Functor (Fix f)@
9+
-- dictionary, we can get Wingman to generate the right definition.
10+
, Functor (Fix f)
11+
) => Functor (Fix f) where
12+
fmap = _
13+

‎plugins/hls-tactics-plugin/test/golden/AutoThetaFix.hs.expected

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,7 @@
1+
{-# LANGUAGE FlexibleContexts #-}
2+
{-# LANGUAGE UndecidableInstances #-}
3+
4+
data Fix f a = Fix (f (Fix f a))
5+
instance (Functor f, Functor (Fix f)) => Functor (Fix f) where
6+
fmap fab (Fix fffa) = Fix (fmap (fmap fab) fffa)
7+

0 commit comments

Comments
 (0)