Feature Request: Case-split QuickFix on pattern argument

[konn]

As reported in #1602, typed holes make typechecking significantly slower.
It might be good if we can invoke the powerful Wingman without using holes if possible.

I think one such example is case split tactic. Consider the following:

foo :: Maybe a -> Int
foo may = ...

I think we can provide Case split on may on may in Line 2.
One thing that we must think is the treatment of the function body.
If the function body is mere typed hole _, we can copy them as-is.
If the ... part contains some other contents, we have a few options:

1. Copy the body as-is, regardless of the occurrence of may.
2. Replaces all the occurrence of may with destructed value.

• This won't work if the destructed constructor contains implicit existential variables which cannot be determined from the type of its arguemtns.

3. Copy the body as-is and prefixing each destructed pattern with as-patterns; e.g. may@(Just mayj).
   • We might omit as-patterns if there is no occurrence of may.

[isovector]

Yeah, I've been thinking about this. The backend machinery is all in place (except for at patterns, which have a TODO); the hardest part is getting the code action to come up on the pattern binding.

[isovector]

I don't plan to tackle this anytime soon. But if someone wanted to send a PR that changed this:

haskell-language-server/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

Lines 165 to 169 in d60dee0

	getSpanAndTypeAtHole
	:: PositionMapping
	-> Range
	-> HieASTs b
	-> Maybe (Span, b)

to work on things that aren't holes, and then figure out which bit of this needs to change:

haskell-language-server/plugins/hls-tactics-plugin/src/Wingman/LanguageServer.hs

Lines 137 to 143 in d60dee0

	mkJudgementAndContext
	:: FeatureSet
	-> Type
	-> Bindings
	-> RealSrcSpan
	-> TcModuleResult
	-> (Judgement, Context)

then I'd be happy to push through the rest of the work.

[isovector]

Relatedly, @kcsongor suggests:

don’t know if this is wingman related, but something I quite often wish I could do with a code action is this:

foo (Foo a b c) = pure a
foo (Bar a b) = pure b

apply code action ->

foo (Foo a _b _c) = pure a
foo (Bar _a b) = pure b

2:50
that is, prepending _ to the unused bindings to squash the warning
2:52
somewhat related to this is the following scenario:

foo (Baz a b c) = ()

here, the important thing is that none of the bound variables are actually used. What I do in this situation is rewrite the pattern to the following:

foo Baz {} = ()

which I prefer to Baz _a _b _c because it’s more resilient to extending the constructor - I would love to have a code action that can do this
2:54
then, as a bonus point, if I could UNDO this.given

foo Baz {} = ()

I change my mind and want to bind stuff from Baz :

foo (Baz a b c) = ()

2:54
I guess these code actions would need to show up on the patterns rather than inside holes, since most of the time they’re applicable when the RHS is already filled in