Support Wingman on ghc 9.2

[santiweight]

Wingman does not currently compile with 9.2. I've investigated a little and I think I've figured out one of the main barriers for the migration.

In <9.x, the staticPlugins field was in DynFlags. Something like:

data DynFlags = {
  ...,
  staticPlugins :: [StaticPlugin]
  }

In 9.2+, plugins are now contained in the Plugins datatype:

data Plugins = Plugins
  { staticPlugins :: ![StaticPlugin]
  , loadedPlugins :: ![LoadedPlugin]
  , loadedPluginDeps :: !([Linkable], PkgsLoaded)
  }

which is now found in HscEnv:

data HscEnv
  = HscEnv {
        hsc_dflags :: DynFlags,
        , hsc_plugins :: !Plugins
  }

Afaict, this means that the PluginDescriptor type should really have a HscEnvModifications field, or alternatively also include a GhcPluginsModifications field.

I figure this is quite a hefty and widespread change, since you would have to update all tutorials and current HLS plugins; so maybe someone knows of a better way to modify the HscEnv?

Paging @isovector and @anka-213 since they might have good feedback

[santiweight]

Linking to #2179

[michaelpj]

Well, I think pluginModifyDynFlags was added exclusively for wingman and I don't see any other users, so I think you can do what you want with it. That said, it seems subtle, looking at the original discussion: #1814

[ProofOfKeags]

Please <3. How pervasive a change would it be? Is it doable by a first time contributor?

[santiweight]

I investigated some more yesterday (I would be a first time contributor; though I've poked around the internals before).

The biggest barrier has ended up being the GHC exactprint API changes. I was able to modify the plugins logic to compile, but then ran into a bunch of errors relating to the new exactprint AST in GHC. This is definitely surmountable, but it is hard for me to tell immediately what parts of the AST isovector is using, and for what. I was working through whack-a-moling the exactprint errors when I stopped. I'll be coming back to it soon...

For example, I can't tell which pass Wingman lives in. Much of the logic is polymorphic in its GHC pass but that no longer works (I think) because you can only annotate certain passes of the GHC with certain annotations. So such polymorphism might be less possible iiuc.

@ProofOfKeags if you want to work on this together let me know :)

[santiweight]

I hope I'm not misusing the issue thread! But here's some materials that could help the migration (I haven'y looked through them yet.:

• a 20 min yt video on the new annotations: https://www.youtube.com/watch?v=GkoQbJofm1A&t=469s
• a blog similar to the above: https://blog.shaynefletcher.org/2021/05/annotations-in-ghc.html
• the design doc/spec for the in-tree exactprint changes: https://gitlab.haskell.org/ghc/ghc/-/wikis/api-annotations

[isovector]

I'm happy to help someone on getting this up and running! I don't have too much time to put towards it right now, but happy to answer questions / do a pairing session.

I can't tell which pass Wingman lives in.

Code synthesis happens in GhcPs, while extraction of the context for auto/etc happens in GhcTc.

---

I suspect most of the value in Wingman is in case split, which we could feasibly pull out as a much smaller plugin --- minimizing the maintenance burden on the GHC AST.

[isovector]

The static plugin stuff is necessary for case..of completion (but not function body splitting) and for inline metaprograms (which AFAIK nobody uses). In the former, we want to enable -XAllowEmptyCase, and in the latter, -XTemplateHaskellSplices

[santiweight]

I think, as you say, the best way forward could well be to extract the simpler case splitting logic stuff and maintain the two aspects of Wingman in separate plugins. Wingman is already quite large - but you would know best about whether the splitting would reduce maintenance burden.

[ProofOfKeags]

The biggest barrier has ended up being the GHC exactprint API changes. I was able to modify the plugins logic to compile, but then ran into a bunch of errors relating to the new exactprint AST in GHC. This is definitely surmountable, but it is hard for me to tell immediately what parts of the AST isovector is using, and for what. I was working through whack-a-moling the exactprint errors when I stopped. I'll be coming back to it soon...

Is it possible to get a diff of what happened to the GHC AST between then and now?

...and for inline metaprograms (which AFAIK nobody uses)

I haven't figured out how to use them. Perhaps discoverability and explorability is the barrier there. Perhaps that can be a different plugin still though.

I think, as you say, the best way forward could well be to extract the simpler case splitting logic stuff and maintain the two aspects of Wingman in separate plugins. Wingman is already quite large - but you would know best about whether the splitting would reduce maintenance burden.

I wonder if anything else is usefully carvable.

Lastly, do you have a branch you're working off of @santiweight

[santiweight]

I don't have a lot of work: just the plugin infrastructure update and the start of the GHC AST update.

but for that I got stuck with a whole bunch of GhcPs<->GhcTc generalization in Wingman, which might be best to split out. As much as the generalization is nice, it certainly incurs some mental overhead. This is something I'd really want @isovector's opinion on first in a phone call etc.

I can push a branch later today: are HLS devs okay with random draft PRs or is a fork preferable?

Is it possible to get a diff of what happened to the GHC AST between then and now?

It's not really going to be super helpful; the exactprint changes are mostly a logical shift in the GHC AST. The changes are well described in some of those above links, but migrating to the new AST is not a simple "use this datatype instead". Instead, we'll have to figure out whether the generalization Wingman has assumed is still applicable to the new AST...

In other words: the diff is the entire AST's annotation infrastructure, and every annotation for GhcPs and GhcTc has changed. So the diff will simply be to reimplement everything for the new exactprint annotations.

[ProofOfKeags]

In other words: the diff is the entire AST's annotation infrastructure, and every annotation for GhcPs and GhcTc has changed. So the diff will simply be to reimplement everything for the new exactprint annotations.

I see. Perhaps I should dive into the code, hence me asking about whether or not you had a branch. But I can also fork it myself and take a look. Just figuered a consolidated effort would be more effective.

[santiweight]

Also, with the new exactprint infrastructure, it might be best to only support GHC 9.2.1+. I'm a little apprehensive about the potential spaghetti caused by supporting two exactprint infrastructures as a newer-to-ghcer. Perhaps @alanz or Shayne Fletcher (I don't know his user) could give us an estimate on the difficulties of developing a compatibility layer vs using CPP.

[santiweight]

I have been using the diffs of hackage docs. Fair warning: the docs for ghc 9.2.2 don't exist yet. When you use hoogle to search for something, load the hackage page and then manually alter the URL to point to ghc-9.2.1; that works just fine and contains the exactprint changes.

[ProofOfKeags]

Also, with the new exactprint infrastructure, it might be best to only support GHC 9.2.1+

You want to deprecate support for wingman for GHC <9.2.1? Seems not a good choice imo. 8.6.5 is still a lot of people's workhorses and it'd be a shame for them to lose access to newer versions of wingman because we chose to require the almost newest version of the compiler.

[santiweight]

I don't think we'll remove the old support, I meant "stop maintaining" rather than "remove support".

Btw @ProofOfKeags I sent you an email so we can discover this code together in private 😆

[santiweight]

Update: we were able to get a whole bunch of the errors out of Wingman. 19/34 modules are compiling, which means that we got past most of the GHC AST stuff. There's some functions in exactprint that have moved around (modifyAnnsT etc.), but we will come back to that later.

https://github.com/santiweight/haskell-language-server/tree/wingman-9.2

The change was quite invasive, but not horribly so. Because of the fact that the new AST anns uses type families, if you want to abstract over the type families, afaict, you need a number of type equalities in the contexts of the pattern synonyms isovector has written. But an easier solution is duplication:

------------------------------------------------------------------------------
-- | A GRHS that caontains no guards.
pattern UnguardedRHSsPs
  :: LHsExpr GhcPs -> (GRHSs GhcPs (LHsExpr GhcPs))
pattern UnguardedRHSsPs body <-
  GRHSs {grhssGRHSs = [L _ (GRHS _ [] body)]}

------------------------------------------------------------------------------
-- | A GRHS that caontains no guards.
pattern UnguardedRHSsTc
  :: LHsExpr GhcTc -> (GRHSs GhcTc (LHsExpr GhcTc))
pattern UnguardedRHSsTc body <-
  GRHSs {grhssGRHSs = [L _ (GRHS _ [] body)]}

Avoiding this duplication would be nice, but with backwards compatibility in mind, such deduplication might not be a great experience. It's worth looking into some typeclass with the relevant type equality constraints/type mappings with the appropriate CPP.

[isovector]

@santiweight and I jumped on a call, and decided the play here is to fork wingman into a separate plugin for 9.2, where it supports only a minimal surface area (case splitting and lambda introductions.) The resulting plugin should be a fraction of the size of wingman, and thus significantly more maintainable in the presence of future GHC breakages. We'll then leave wingman to bit rot, never to be updated past GHC 9.

[isovector]

I've done an initial pass at making a new plugin and ripping out the complexity of wingman:

https://github.com/haskell/haskell-language-server/compare/wingman-to-new-plugin?expand=1

There's one call to bottom in it still, but the test suite seems to pass.

Besides that, I think the result is a good candidate for a new plugin, modulo renaming/cleanup. It continues to support Intro, Refine, and the various destructs, as well as work in simple GADT cases.

What's been removed is Auto and metaprogramming support.

[isovector]

A good next action if someone wanted to pick it up would be to run weeder on the resulting plugin and see if I left any dead code around. We could then chop that out, and the resulting codebase should be significantly easier to port to 9.2.

[isovector]

The failing tests in the new branch are:

• DestructAllGADTEvidence
• DestructTyToDataFam
• DestructDataFam
• DestructTyFam
• SubsequentTactics

The first four are pretty reasonable; GADT splitting got dumber as a result of shedding a bunch of complexity around typechecking. The latter is a little worrisome (see 18a8996), but I don't see any particular reason it would be failing; I didn't run it against HEAD to find out if it's my machine or my branch.

EDIT: I've now removed the failing GADT tests from the branch.

[michaelpj]

From the HLS point of view it would be nice if this could be contained within the existing plugin. Can you just make the removed stuff conditional? Or is that going to be too annoying?

[isovector]

It would be a giant mess of CPP which IMO would only enhance the maintenance burden. We could alternatively remove the features from the existing plugin, but that seems like poor form.

[konn]

The latter is a little worrisome (see 18a8996), but I don't see any particular reason it would be failing; I didn't run it against HEAD to find out if it's my machine or my branch.

It might be rather off-topic, but it seems that in some cases, custom tactic block stops working already with with GHC 9.0.2 as I reported here. Is this related to that faiulre?

[michaelpj]

It would be a giant mess of CPP which IMO would only enhance the maintenance burden.

if impl (ghc >= 9.2)
   exposed-modules: WingmanNew.X, ...
   other-modules:  ...
else
  exposed-modules: WingmanOld.X, ...
  other-modules:  ...

Adding a new package means all kinds of admin, like uploading it to Hackage, eventually retiring the old one and replacing it with the new one (so we'd be stuck with the new name forever).

Although perhaps I'm misunderstanding you: I think by all means this can be a new plugin (i.e. Haskell value), but it would be better if it wasn't a new plugin (package).

We could alternatively remove the features from the existing plugin, but that seems like poor form.

Personally I would be okay with that. "The maintainers of the plugin have decided to pare it back to make it maintainable on an ongoing basis". I suspect this change also indicates that you're not going to fix bugs in the old plugin for old versions? If the truth is that we're giving up on some of the functionality, I think it's honest to just delete it. But it's arguable.

[isovector]

That's fair. I don't have strong opinions here; happy to acquiesce to whatever people think is best!

[alanz]

You could also take the approach I took on ghc-exactprint. Keep the package name, give it a major version bump, and adjust the cabal file so that for GHC <9.2 it only builds up to the legacy version, and the new version only builds with GHC 9.2+
If the API exposed to HLS is identical for both, it should be straightforward.

It is effectively a throw away old, build new, but cabal is ok to deal with it in the same namespace.

[ProofOfKeags]

What is the rationale for not wanting to port the full functionality? Is it not useful? I've found it to be, although I can live without it. Is it simply just that @isovector can't/doesn't want to maintain it, or is it that it is dead end research? If it's the former maybe we can pare it back but allow for others to pick up the more complex functionality. I think deleting the code will make it harder for anyone to pick up.

[santiweight]

I think it's more a question of maintainability and the value for cost ratio. When we discussed, neither isovector nor I were keen on maintaining the full Wingman. I am sure you would be helped, but I don't think anyone (yet) has displayed enough motivation to maintain it themselves.

Whether or not we maintain both, the first step is still to split out the simple type destruction stuff from the tactics language. There is no need, as far as we could tell to have the two live side-by-side as they do currently. Having the two live together means that the case-splitting stuff is unnecessarily held back for new GHC releases by the more-complex tactics language.

I personally think there are lower hanging fruit than the tactics plugin, that would work in mini-Wingman. Some features that come to mind:

• completing partial pattern matches
• switching between function and case-of pattern matching
• switching between different types of record pattern matching (by name, structurally)

[isovector]

What is the rationale for not wanting to port the full functionality?

Complexity. Axing the metaprogramming component means we can remove:

• the static plugin machinery that enables [wingman||] blocks
• the parser and related swarth of tactic combinators
• a huge chunk of LSP machinery for finding wingman blocks
• an interface to GHC internals for finding typeclasses and fundeps

In addition, removing auto support means we can also chop out:

• expensive program search
• a host of expensive, complicated and ad-hoc internal details for attempting to steer the auto search
• the tactics engine entirely

My initial attempt at this is a red diff ~4500 lines long, significantly decoupling wingman from the GHC internals, which in turn makes the entire project much easier to port between breaking GHC API changes. It's not ideal, but makes sense that 95% of the use of this plugin is case splitting.

[ProofOfKeags]

Got it, so the main issue is that tactics metaprogramming isn't worth its cost in maintenance burden. But WIngman still has the goal of being an assistant code synthesis tool.

[santiweight]

I apologize for the delay; I'm back on this :)

[santiweight]

Based on Sandy's changes, I now have a compiling version of the new minimal plugin on 9.2.

Tests are all failing for now because no actions are provided... I'll keep trucking along.

https://github.com/santiweight/haskell-language-server/tree/new-wingman-9.2

[santiweight]

I'm coming up on some odd bug in GHC(?). For some reason, I am having the following output from exact-ring (notice the badly formed case statement:

data Foo = A Int | B Bool | C

foo :: Foo -> ()
foo x = x of
  A n -> _
  B b -> _
  C -> _

after transforming the following original source:

data Foo = A Int | B Bool | C

foo :: Foo -> ()
foo x = case x of

I couldn't see anything obvious in the exact print source code in GHC. It's also odd because when I Outputtable the AST I am transforming into, I get the right thing:

case x of
  A n -> _
  B b -> _
  C -> _

At some point, wingman goes through retrie's transformA, which is where the problem happens. At this point, I spent a little while trying to decipher why this would happen, but I can't figure it out, because the one relevant line I can find in exact-print doesn't apply, since I am not producing a EpAnnNotUsed.

Paging @alanz for any thoughts :)

code, which I am running with cabal test hls-refine-destruct-plugin --test-options="-p EmptyCaseADT"

[isovector]

@santiweight I don't know about the new exactprint api, but the only one wouldn't play nicely if any Anns were missing, and getting them is nontrivial. That's why the HLS ExactPrint module does this weird roundtrip parsing thing --- it's the reliable way I could find to get the necessary anns. My guess is somehow the necessary anns for case got dropped somewhere in the transformation.

[santiweight]

I've been able to work on this again recently, and will continue to do so over the weekend.

I've been able to start getting tests to pass! Not many (just 8 actually right now). But this milestone represents my general understanding of how to use the new API, and gives me a lot of hope for at least support the empty-case stuff in wingman.

Edit: for those interested I now support the empty-case plugin, and will now work on the tactics plugin

[santiweight]

Wingman's tactics are now working with 9.2.4! There's a few details to polish, but I'm nearly done thankfully.

When is the next release expected for? I am very keen to hit the next release...

Relevant branch is wingman-confused (I am now less confused 😅).

[rami3l]

@santiweight The next minor release seems to be planned in #3236, however:

The release is only for critical bug fixes [..]

... so probably we have to wait for the next major release? 🤔

[santiweight]

I have found the motivation to get this over the line and will follow the following plan:

1. Move the old wingman src code to a new folder called old, which will be a pure refactor
2. Copy and paste the old wingman src code to a new folder called new which will introduce a pure-copy of wingman. This new wingman src will not be in HLS, but is a helpful way to get better diffs when Sandy's changes and subsequently mine are applied.
3. Apply Sandy's wingman simplification to the new directory. This code will still not be run in CI or in HLS...
4. Apply my 9.2.1+ compatibility changes to Sandy's simplified codebase. At this point we will add the new directory as a conditional compilation to the hls-tactics-plugins cabal file.

The cabal file looks something like:

  if impl(ghc) >= 9.2.1:
    hs-source-dirs: new/src
    exposed-modules:
      ... (the simplified wingman)
  else:
    hs-source-dirs: old/src
    exposed-modules:
      ... (the old wingman)

[michaelpj]

I'm happy for you to do multiple steps in the plan in one PR, if the commits show the diffs clearly, but up to you!

[haroldcarr]

What is the status of this work?

[isovector]

#3525 (comment) and #3525 (comment) I think sum it up