Simpler Tier 1 tactics for case splits

[ejconlon]

Is your enhancement request related to a problem? Please describe.

First, let me say that I appreciate all of the hard work the maintainers of HLS and plugins do and have done - you guys are superheroes!

It looks like hls-tactics-plugin has been disabled due to some conflict with GHC 9.2 that has not been resolved. This means that features like case splitting are no longer available in HLS. I am probably not along in having become very used to this feature, as it allows one to destruct large sum types quickly. In my opinion, this tactic should be a Tier 1 feature of HLS, at least for "simple" types (ADTs, maybe not GADTs). It would be great to see it re-enabled, but it seems like the machinery of the tactics plugin is a bit daunting for new contributors! It has support for type-directed program synthesis that may not be needed for simple tactics such as destruct (but please correct me if I am wrong).

Describe the solution you'd like

I propose a separate plugin that supports the simplest tactics like destruct and intros, and only on simple types. Ideally we would get it into a state where enough people would feel comfortable with maintenance that it could be a Tier 1 plugin. Doing this might be a good opportunity to pull out some reusable functionality that can be shared between tactics implementations and other plugins. (For example, right now tactics relies on refactor for printing and insertion.) Such reusable functionality might include:

• Identifying whether a code action may have a relevant hole (for example, when invoking quick-fix on a var on the LHS of a function definition with a hole in the body on the RHS).
• Identifying the type of the var under the point, or identifying the type of the relevant hole.
• Classifying which types can be easily destructed.
• Generating fresh (and relevant) names for pattern vars and named holes.
• Generating patterns from easily-destructible types
• Inserting generated syntax into the document.

(I know where some of this functionality is, but it's not easy to find and isolate! Documentation may help.)

The tactics plugin could then be focused on more advanced program synthesis.

Describe alternatives you've considered

The alternative is the status quo, where tactics may disappear in HLS releases as it is not Tier 1. Additional maintainers could change that, though. Improved documentation of the tactics plugin would also help.

Additional context

I am happy to contribute what I can, but I definitely need some help. I am also happy to try to break down and organize tasks.

[santiweight]

Hi @ejconlon

I've been AFK from HLS development for a few months. Let me give you my status.

I do not find myself excited to work on GHC-related refactoring tools. I personally find that the stability and quality of the ghc-exactprint API has made it unpleasant for me to work on new refactoring tools.

There were other reasons as well (personal), but the technical reasons are worth going into...

Why tactics and co haven't merged

The reason I've never merged hls-tactics-plugin, even though it works, is because maintaining it is just a massive pain. There are I think no more than 10 tests that are a little broken out of 130. It is worth merging as is if someone updates those test files to accept the slightly-broken results.

The new plugin is, as you describe, a simplified view of tactics, thanks to @isovector's work, which paved the way for me to update to 9.2 and migrate to the new exactprint API.

The same applies to [those] [3] [code] [actions] I [developed].

However, I personally am very frightened of the stability of GHC's exactprint API. Migrating to using GHC 9.2 was really quite exasperating for me. And developing tools against the 9.2 API from scratch was also exasperating.

My feelings on ghc-exactprint

Alan Zimmerman has done absolutely fantastic work on the ghc-exactprint API, and the effort is genuinely leviathan. I'm not exaggerating - it's a mind-boggling amount of work.

However, the result is still not easy enough to work with (for me) to make me want to work on it. I had a massive amount of energy and spent well over 60 hours on tactics and code actions. And by the end, I realized I could not trust that a future version of GHC wouldn't simply break all of it again.

I also, even after this massive amount of time investment, never felt like I reached a point of productivity and understanding. I have learned that that is not nice feeling!

The way forward

In my opinion, the way forward here is to get 5/6 people in a room to discuss a GHC exactprint API that will work, and be stable. I tried to upstream some of this, but I think there is simply too much work for one or two people to get it right - I think it requires collaboration.

Alan has already started some of that here

I think that developing the tools is not enough, we should build a more robust and welcoming API. I have kind of whined silently to myself about this. I'm sorry about that. I should have reached out - I didn't because I felt burned out. I'm sad about that, but I also don't feel that my burn out is unjustified, and the right thing to do is prevent those feelings first.

---

All my whinging done, I would be more than happy to answer any questions, pair program, etc. I can't personally do it on my own because of the burn-out I described. But I'd be more than happy to be part of a conversation on a stable API, and to revive my work that I got burned out over.

[ejconlon]

@santiweight This is really great context! Thanks for sharing it and thanks for all your hard work on the project! Let me digest a bit now…

[ejconlon]

OK, I understand better what some of the issues are. It seems like tactics is in trouble because the processes of parsing, modifying, inserting, and printing all change greatly between GHC versions. (Also, I like the code actions you added to the refactor plugin @santiweight - add to where clause, add argument, etc. These seem like they could be building blocks for other plugins.)

When you talk about the issues you had with the exactprint API, is the problem that the exactprint annotations and their meaning have been changing, or GHC syntax itself? Or is it that the Transform API, for example, has not been stable? (I don't have any context on this library.)

Finally, is there an understanding of what all the relevant transforms are for HLS as a whole? Would documenting this help clarify what a good transformation API would offer?

[santiweight]

These seem like they could be building blocks for other plugins.

That is still my hope! Happy to work on such ideas...

When you talk about the issues you had with the exactprint API, is the problem

I do, in general, mean the exactprint API, referring to the TransformT API. Here are some of my recollections:

1. There are few examples, and most examples are out of date (since the new API is untrodden)
2. The API doesn't feel particularly intuitive to me, and there's a lot of things that are confusing to me. They're kind of too many to ennumerate here. But you can probably see traces of it in my code and MRs.
3. Many things are not provided, such as unbound variables or moving declarations between groups (the add-to-where functionality is very buggy today for example). The implementations that I have are surely bad form.
4. The behavior is very confusing for bas inputs (for example misconfigured indentation), and the resulting behavior is not an error, sometimes hiding issues in the AST (e.g. a node might get skipped)

is there an understanding of what all the relevant transforms are for HLS as a whole?

I'm not aware of an exhaustive list. The places to look are in the big file of code actions, and also the tactics plugin. Those two places contain most of the usages. I once attempted to start congregating these usages into a new group of utilities. It was certainly challenging (I might still have that branch lying about).

Or is it that the Transform API, for example, has not been stable?

I don't think that the Transform API has been unstable, but it has been hard to use. For example, I would have guessed that the "add new declaration to a where clause; or introduce a new where clause if there wasn't one" would be hard, but it was much harder in ways that I didn't expect, and the implementation is iirc still not great.

It's important, however not to just write another API, but to build a group that maintains something together. Such higher-level APIs have been developed at least three times (HaRe, the tactics plugin, and that library that the tactics plugin uses), but they all seem to fall out of date.

---

If you want, a good place to start is probably to define some high level functionality that should be in the exactprint API, such as the one I tried to upstream. Perhaps we can get a foot in the door that way, and slowly upstream exactprint functionality?

If you'd like to work on that ghc-exactprint MR I linked above, I'd be happy to get that pushed through.

[isovector]

Just to reiterate; the hard part here is updating the text buffer with the results of having synthesized new code. Dealing with layout and comments and where blocks and all of Haskell's syntax is a Herculean effort that we used to pass the buck to the exactprint API to do. Which was still enormously difficult, but at least possible. Since ~9.2, exactprint got merged into GHC proper as part of the Trees That Grow infrastructure... which is a better place to have it than in some weird separate library, but it's still way too close to the metal.

Getting proper GHC-level support for grafting the AST and dumping it back out, comments and layouts and all, is the only tenable path forwards that I can see. For a bounty on the order or $5k I could be talked into getting tactics working again in HLS for a specific version of GHC, and we could use that same energy to think through what API GHC would need to provide us.

[ejconlon]

Right @isovector I thought originally the problem was lack of maintainer time for tactics, but I see that the problem is really in textual transformation. (Thanks for your efforts!) I can close this issue if you would like to continue the discussion in a clearer thread.

[michaelpj]

Just putting this link here since I think we should consider going this route if we resurrect a case-splitting plugin: #2437