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: https://github.com/haskell/haskell-language-server/pull/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 18a89965e4b161c72824f013328d5212a36d30ea), 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 https://github.com/haskell/haskell-language-server/commit/18a89965e4b161c72824f013328d5212a36d30ea), 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.