Open ProofOfKeags opened 3 years ago
PR welcome. Implementation sketch:
const split
tactic https://github.com/isovector/haskell-language-server/blob/14e71db4a34cda595cba9ba5f9ab4a1422dd2744/plugins/tactics/src/Ide/Plugin/Tactic/Tactics.hs#L154Shouldn't take more than half an hour to get everything up and running.
I've worked a bit to make the TacticCommand
more strongly typed as preparation for this, see https://github.com/WorldSEnder/haskell-language-server/commit/0bb120e7f85825a5310835569ceb3e85b4e65e6f. 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.
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
).
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.
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.
@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
TacticContext tc
that tells you what kind of argument is expectedTacticCommand
an ordinary datatype with Enum
and Bounded
instances, so you can easily enumerate it to see all available tacticssingletons
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.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
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.