Feature Request: Expose split tactic

[ProofOfKeags]

data A = ...
data B = ...
data C = ...

thing :: (A, B) -> C
thing = ...

expCurrentlyUnderImplementation :: C
expCurrentlyUnderImplementation = 
    let baz = case foo of
        Bar a -> _
    in thing baz

Consider the above scenario. I'd like to have a code action that fills the hole with (_, _). Conceptually this is working backwards from the result rather than case splitting which is working forward from the arguments. Perhaps this should only kick in if the desired result has a single top level constructor.

If baz' type infer's to HLS' Any type, then no code action would be suggested.

[isovector]

PR welcome. Implementation sketch:

1. Add a dcon for the code action

   haskell-language-server/plugins/tactics/src/Ide/Plugin/Tactic/TestTypes.hs

   Line 11 in 14e71db

   data TacticCommand

2. Hook it up

   haskell-language-server/plugins/tactics/src/Ide/Plugin/Tactic.hs

   Line 113 in 14e71db

   commandTactic :: TacticCommand -> OccName -> TacticsM ()

   to the const split tactic

   haskell-language-server/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs

   Line 154 in 14e71db

   split :: TacticsM ()

3. Customize the filter to only show it when there is a single dcon for the type of the hole

   haskell-language-server/plugins/tactics/src/Ide/Plugin/Tactic.hs

   Line 90 in 14e71db

   commandProvider :: TacticCommand -> TacticProvider

4. Write a test showing your code action comes up when there is a single dcon, and not when there are many:

   haskell-language-server/test/functional/Tactic.hs

   Lines 78 to 87 in 14e71db

   	, mkTest
   	"Produces lambdacase code actions"
   	"T3.hs" 7 13
   	[ (id, DestructLambdaCase, "")
   	]
   	, mkTest
   	"Doesn't suggest lambdacase without -XLambdaCase"
   	"T2.hs" 11 25
   	[ (not, DestructLambdaCase, "")
   	]

Shouldn't take more than half an hour to get everything up and running.

[WorldSEnder]

I've worked a bit to make the TacticCommand more strongly typed as preparation for this, see WorldSEnder@0bb120e. The idea behind all this work is to expose an option to split on each constructor (and maybe pattern synonyms) in case a type has multiple of those and merge it with the existing Intros for function types.

Let me know what you think. @isovector I suppose part of the implementation could be replaced by using singletons but after reading

The singletons library requires GHC 8.8.1 or greater

I'm not so sure about compatibility.

[isovector]

Great to see that you're diving in, @WorldSEnder. Do you have further plans for these dependently typed things? As it stands I'm not convinced the machinery is worth the cost. Type-level stuff works best to prevent dangerous and silent issues, but right now the worst that can happen is we use an OccName of "" and accidentally do no work. It's the sort of thing a test would catch immediately, and even if it did make it to production, hell would not break loose.

Furthermore, as I understand LSP, our interface is extremely limited and it's unlikely we'll ever push more information into TacticsParam; there simply isn't any good way to fill that information in. As such, I doubt there will ever be anything other than the var_name (which admittedly should be a Maybe OccName instead of a String).

[WorldSEnder]

Not further than that, I'm not fully convinced either. Having to add a TacticCommand in 11 places instead of 5 is overhead, definitely. I will ponder the question the next few days while I'm on vacation.

[ProofOfKeags]

I think I'd like to understand the purpose of the type machinery added. Looking at the commit referenced, I'm not quite sure exactly what it is doing. That said, one of the things I've used it for is basically hacking GHC's constraint solver to solve arbitrary constraints in the programmer's code.

[WorldSEnder]

@ProofOfKeags currently some TacticCommands are using a OccName as an argument, for example Destruct takes as argument the name of the variable to destruct. But there are also tactics that don't have any arguments, i.e. they currently just throw away the argument they are given. What the commit does is

• Introduce a type family TacticContext tc that tells you what kind of argument is expected
• Still keeps TacticCommand an ordinary datatype with Enum and Bounded instances, so you can easily enumerate it to see all available tactics
• Works some magic I learned from the singletons package to make it typesafe: You can only pass the correct TacticContext argument to the tactic. Since the argument gets passed via JSON, it also ensures that all contexts are serializable and equality comparable for testing.
• The gist of the singletons approach is that instead of an argument TacticCommand -> _ you have KnownTacticCommand tc => proxy tc -> _. The proxy is there so Haskell can deduce the type-level tc :: TacticCommand argument, and KnownTacticCommand tc gives you a way to reflect the value by matching on TCSing you get from tcReflect. For reference, this is akin to the approach taken in GHC.TypeLits