Skip to content

Commit 6409ce8

Browse files
isovectormergify[bot]
isovector
and
mergify[bot]
authored
Let Wingman peek through type families (#1881)
* Let Wingman peek through type families * Cleanup imports * We can just use normalizejudgment in mkFirstJudgment * Add support for data families too Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
1 parent 2ee2943 commit 6409ce8

16 files changed

+169
-45
lines changed

‎plugins/hls-tactics-plugin/src/Wingman/CodeGen.hs‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ module Wingman.CodeGen
1313
import ConLike
1414
import Control.Lens ((%~), (<>~), (&))
1515
import Control.Monad.Except
16+
import Control.Monad.Reader (ask)
1617
import Control.Monad.State
1718
import Data.Bool (bool)
1819
import Data.Functor ((<&>))
@@ -24,6 +25,7 @@ import Data.Traversable
2425
import DataCon
2526
import Development.IDE.GHC.Compat
2627
import GHC.Exts
28+
import GHC.SourceGen (occNameToStr)
2729
import GHC.SourceGen.Binds
2830
import GHC.SourceGen.Expr
2931
import GHC.SourceGen.Overloaded
@@ -39,7 +41,6 @@ import Wingman.Judgements.Theta
3941
import Wingman.Machinery
4042
import Wingman.Naming
4143
import Wingman.Types
42-
import GHC.SourceGen (occNameToStr)
4344

4445

4546
destructMatches
@@ -69,6 +70,7 @@ destructMatches use_field_puns f scrut t jdg = do
6970
args = conLikeInstOrigArgTys' con apps
7071
modify $ appEndo $ foldMap (Endo . evidenceToSubst) ev
7172
subst <- gets ts_unifier
73+
ctx <- ask
7274

7375
let names_in_scope = hyNamesInScope hy
7476
names = mkManyGoodNames (hyNamesInScope hy) args
@@ -79,8 +81,8 @@ destructMatches use_field_puns f scrut t jdg = do
7981
$ zip names'
8082
$ coerce args
8183
j = fmap (CType . substTyAddInScope subst . unCType)
82-
$ introduce hy'
83-
$ introduce method_hy
84+
$ introduce ctx hy'
85+
$ introduce ctx method_hy
8486
$ withNewGoal g jdg
8587
ext <- f con j
8688
pure $ ext
@@ -289,13 +291,14 @@ letForEach rename solve (unHypothesis -> hy) jdg = do
289291
case hy of
290292
[] -> newSubgoal jdg
291293
_ -> do
294+
ctx <- ask
292295
let g = jGoal jdg
293296
terms <- fmap sequenceA $ for hy $ \hi -> do
294297
let name = rename $ hi_name hi
295298
res <- tacticToRule jdg $ solve hi
296299
pure $ fmap ((name,) . unLoc) res
297300
let hy' = fmap (g <$) $ syn_val terms
298301
matches = fmap (fmap (\(occ, expr) -> valBind (occNameToStr occ) expr)) terms
299-
g <- fmap (fmap unLoc) $ newSubgoal $ introduce (userHypothesis hy') jdg
302+
g <- fmap (fmap unLoc) $ newSubgoal $ introduce ctx (userHypothesis hy') jdg
300303
pure $ fmap noLoc $ let' <$> matches <*> g
301304

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

Lines changed: 25 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -3,16 +3,18 @@ module Wingman.Context where
33
import Bag
44
import Control.Arrow
55
import Control.Monad.Reader
6+
import Data.Coerce (coerce)
67
import Data.Foldable.Extra (allM)
78
import Data.Maybe (fromMaybe, isJust, mapMaybe)
89
import qualified Data.Set as S
910
import Development.IDE.GHC.Compat
10-
import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys)
11+
import GhcPlugins (ExternalPackageState (eps_inst_env), piResultTys, eps_fam_inst_env)
1112
import InstEnv (lookupInstEnv, InstEnvs(..), is_dfun)
1213
import OccName
1314
import TcRnTypes
1415
import TcType (tcSplitTyConApp, tcSplitPhiTy)
1516
import TysPrim (alphaTys)
17+
import Wingman.GHC (normalizeType)
1618
import Wingman.Judgements.Theta
1719
import Wingman.Types
1820

@@ -25,24 +27,28 @@ mkContext
2527
-> KnownThings
2628
-> [Evidence]
2729
-> Context
28-
mkContext cfg locals tcg eps kt ev = Context
29-
{ ctxDefiningFuncs = locals
30-
, ctxModuleFuncs
31-
= fmap splitId
32-
. mappend (locallyDefinedMethods tcg)
33-
. (getFunBindId =<<)
34-
. fmap unLoc
35-
. bagToList
36-
$ tcg_binds tcg
37-
, ctxConfig = cfg
38-
, ctxInstEnvs =
39-
InstEnvs
40-
(eps_inst_env eps)
41-
(tcg_inst_env tcg)
42-
(tcVisibleOrphanMods tcg)
43-
, ctxKnownThings = kt
44-
, ctxTheta = evidenceToThetaType ev
45-
}
30+
mkContext cfg locals tcg eps kt ev = fix $ \ctx ->
31+
Context
32+
{ ctxDefiningFuncs
33+
= fmap (second $ coerce $ normalizeType ctx) locals
34+
, ctxModuleFuncs
35+
= fmap (second (coerce $ normalizeType ctx) . splitId)
36+
. mappend (locallyDefinedMethods tcg)
37+
. (getFunBindId =<<)
38+
. fmap unLoc
39+
. bagToList
40+
$ tcg_binds tcg
41+
, ctxConfig = cfg
42+
, ctxFamInstEnvs =
43+
(eps_fam_inst_env eps, tcg_fam_inst_env tcg)
44+
, ctxInstEnvs =
45+
InstEnvs
46+
(eps_inst_env eps)
47+
(tcg_inst_env tcg)
48+
(tcVisibleOrphanMods tcg)
49+
, ctxKnownThings = kt
50+
, ctxTheta = evidenceToThetaType ev
51+
}
4652

4753

4854
locallyDefinedMethods :: TcGblEnv -> [Id]

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

Lines changed: 23 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,9 +23,11 @@ import Development.IDE.Core.Compile (lookupName)
2323
import Development.IDE.GHC.Compat hiding (exprType)
2424
import DsExpr (dsExpr)
2525
import DsMonad (initDs)
26+
import FamInst (tcLookupDataFamInst_maybe)
27+
import FamInstEnv (normaliseType)
2628
import GHC.SourceGen (lambda)
2729
import Generics.SYB (Data, everything, everywhere, listify, mkQ, mkT)
28-
import GhcPlugins (extractModule, GlobalRdrElt (gre_name))
30+
import GhcPlugins (extractModule, GlobalRdrElt (gre_name), Role (Nominal))
2931
import OccName
3032
import TcRnMonad
3133
import TcType
@@ -374,3 +376,23 @@ mkFunTys' =
374376
mkVisFunTys
375377
#endif
376378

379+
380+
------------------------------------------------------------------------------
381+
-- | Expand type and data families
382+
normalizeType :: Context -> Type -> Type
383+
normalizeType ctx ty =
384+
let ty' = expandTyFam ctx ty
385+
in case tcSplitTyConApp_maybe ty' of
386+
Just (tc, tys) ->
387+
-- try to expand any data families
388+
case tcLookupDataFamInst_maybe (ctxFamInstEnvs ctx) tc tys of
389+
Just (dtc, dtys, _) -> mkAppTys (mkTyConTy dtc) dtys
390+
Nothing -> ty'
391+
Nothing -> ty'
392+
393+
------------------------------------------------------------------------------
394+
-- | Expand type families
395+
expandTyFam :: Context -> Type -> Type
396+
expandTyFam ctx = snd . normaliseType (ctxFamInstEnvs ctx) Nominal
397+
398+

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

Lines changed: 22 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ import Development.IDE.Spans.LocalBindings
1717
import OccName
1818
import SrcLoc
1919
import Type
20-
import Wingman.GHC (algebraicTyCon)
20+
import Wingman.GHC (algebraicTyCon, normalizeType)
2121
import Wingman.Types
2222

2323

@@ -69,11 +69,19 @@ withNewGoal :: a -> Judgement' a -> Judgement' a
6969
withNewGoal t = field @"_jGoal" .~ t
7070

7171

72-
introduce :: Hypothesis a -> Judgement' a -> Judgement' a
72+
normalizeHypothesis :: Functor f => Context -> f CType -> f CType
73+
normalizeHypothesis = fmap . coerce . normalizeType
74+
75+
normalizeJudgement :: Functor f => Context -> f CType -> f CType
76+
normalizeJudgement = normalizeHypothesis
77+
78+
79+
introduce :: Context -> Hypothesis CType -> Judgement' CType -> Judgement' CType
7380
-- NOTE(sandy): It's important that we put the new hypothesis terms first,
7481
-- since 'jAcceptableDestructTargets' will never destruct a pattern that occurs
7582
-- after a previously-destructed term.
76-
introduce hy = field @"_jHypothesis" %~ mappend hy
83+
introduce ctx hy =
84+
field @"_jHypothesis" %~ mappend (normalizeHypothesis ctx hy)
7785

7886

7987
------------------------------------------------------------------------------
@@ -393,17 +401,20 @@ substJdg subst = fmap $ coerce . substTy subst . coerce
393401

394402

395403
mkFirstJudgement
396-
:: Hypothesis CType
404+
:: Context
405+
-> Hypothesis CType
397406
-> Bool -- ^ are we in the top level rhs hole?
398407
-> Type
399408
-> Judgement' CType
400-
mkFirstJudgement hy top goal = Judgement
401-
{ _jHypothesis = hy
402-
, _jBlacklistDestruct = False
403-
, _jWhitelistSplit = True
404-
, _jIsTopHole = top
405-
, _jGoal = CType goal
406-
}
409+
mkFirstJudgement ctx hy top goal =
410+
normalizeJudgement ctx $
411+
Judgement
412+
{ _jHypothesis = hy
413+
, _jBlacklistDestruct = False
414+
, _jWhitelistSplit = True
415+
, _jIsTopHole = top
416+
, _jGoal = CType goal
417+
}
407418

408419

409420
------------------------------------------------------------------------------

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -275,7 +275,9 @@ mkJudgementAndContext cfg g (TrackedStale binds bmap) rss (TrackedStale tcg tcgm
275275
subst = ts_unifier $ appEndo (foldMap (Endo . evidenceToSubst) evidence) defaultTacticState
276276
pure $
277277
( disallowing AlreadyDestructed already_destructed
278-
$ fmap (CType . substTyAddInScope subst . unCType) $ mkFirstJudgement
278+
$ fmap (CType . substTyAddInScope subst . unCType) $
279+
mkFirstJudgement
280+
ctx
279281
(local_hy <> cls_hy)
280282
(isRhsHole tcg_rss tcs)
281283
g

‎plugins/hls-tactics-plugin/src/Wingman/Machinery.hs‎

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -49,10 +49,13 @@ newSubgoal
4949
:: Judgement
5050
-> Rule
5151
newSubgoal j = do
52-
unifier <- gets ts_unifier
53-
subgoal
54-
$ substJdg unifier
55-
$ unsetIsTopHole j
52+
ctx <- ask
53+
unifier <- gets ts_unifier
54+
subgoal
55+
$ normalizeJudgement ctx
56+
$ substJdg unifier
57+
$ unsetIsTopHole
58+
$ normalizeJudgement ctx j
5659

5760

5861
tacticToRule :: Judgement -> TacticsM () -> Rule

‎plugins/hls-tactics-plugin/src/Wingman/Tactics.hs‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -83,7 +83,8 @@ recursion = requireConcreteHole $ tracing "recursion" $ do
8383
unless (any (flip M.member pat_vals) $ syn_used_vals ext) empty
8484

8585
let hy' = recursiveHypothesis defs
86-
localTactic (apply $ HyInfo name RecursivePrv ty) (introduce hy')
86+
ctx <- ask
87+
localTactic (apply $ HyInfo name RecursivePrv ty) (introduce ctx hy')
8788
<@> fmap (localTactic assumption . filterPosition name) [0..]
8889

8990

@@ -110,15 +111,15 @@ intros'
110111
-> TacticsM ()
111112
intros' names = rule $ \jdg -> do
112113
let g = jGoal jdg
113-
ctx <- ask
114114
case tacticsSplitFunTy $ unCType g of
115115
(_, _, [], _) -> throwError $ GoalMismatch "intros" g
116116
(_, _, as, b) -> do
117+
ctx <- ask
117118
let vs = fromMaybe (mkManyGoodNames (hyNamesInScope $ jEntireHypothesis jdg) as) names
118119
num_args = length vs
119120
top_hole = isTopHole ctx jdg
120121
hy' = lambdaHypothesis top_hole $ zip vs $ coerce as
121-
jdg' = introduce hy'
122+
jdg' = introduce ctx hy'
122123
$ withNewGoal (CType $ mkFunTys' (drop num_args as) b) jdg
123124
ext <- newSubgoal jdg'
124125
pure $

‎plugins/hls-tactics-plugin/src/Wingman/Types.hs‎

Lines changed: 5 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,8 +26,11 @@ import Data.Set (Set)
2626
import Data.Text (Text)
2727
import qualified Data.Text as T
2828
import Data.Tree
29+
import Development.IDE (Range)
30+
import Development.IDE.Core.UseStale
2931
import Development.IDE.GHC.Compat hiding (Node)
3032
import Development.IDE.GHC.Orphans ()
33+
import FamInstEnv (FamInstEnvs)
3134
import GHC.Generics
3235
import GHC.SourceGen (var)
3336
import InstEnv (InstEnvs(..))
@@ -39,8 +42,6 @@ import UniqSupply (takeUniqFromSupply, mkSplitUniqSupply, UniqSupply)
3942
import Unique (nonDetCmpUnique, Uniquable, getUnique, Unique)
4043
import Wingman.Debug
4144
import Wingman.FeatureSet
42-
import Development.IDE.Core.UseStale
43-
import Development.IDE (Range)
4445

4546

4647
------------------------------------------------------------------------------
@@ -422,6 +423,7 @@ data Context = Context
422423
, ctxConfig :: Config
423424
, ctxKnownThings :: KnownThings
424425
, ctxInstEnvs :: InstEnvs
426+
, ctxFamInstEnvs :: FamInstEnvs
425427
, ctxTheta :: Set CType
426428
}
427429

@@ -452,6 +454,7 @@ emptyContext
452454
, ctxModuleFuncs = mempty
453455
, ctxConfig = emptyConfig
454456
, ctxKnownThings = error "empty known things from emptyContext"
457+
, ctxFamInstEnvs = mempty
455458
, ctxInstEnvs = InstEnvs mempty mempty mempty
456459
, ctxTheta = mempty
457460
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -36,6 +36,7 @@ spec = describe "auto for tuple" $ do
3636
runTactic
3737
emptyContext
3838
(mkFirstJudgement
39+
emptyContext
3940
(Hypothesis $ pure $ HyInfo (mkVarOcc "x") UserPrv $ CType in_type)
4041
True
4142
out_type)

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,9 @@ spec = do
1717
destructTest "a" 7 25 "SplitPattern"
1818
destructTest "a" 6 18 "DestructPun"
1919
destructTest "fp" 31 14 "DestructCthulhu"
20+
destructTest "b" 7 10 "DestructTyFam"
21+
destructTest "b" 7 10 "DestructDataFam"
22+
destructTest "b" 17 10 "DestructTyToDataFam"
2023

2124
describe "layout" $ do
2225
destructTest "b" 4 3 "LayoutBind"

0 commit comments

Comments
 (0)