Split tactic for datatypes #30
Conversation
|
This is excellent work, thank you @WorldSEnder! We don't have a good story around scoping rules yet, so I wouldn't worry about it in this PR. I'm more worried about unexported data cons than unqualified occnames, as other plugins will notice the issue and suggest fixes. I'm happy to merge this if you're happy with it! |
|
I'll merge this later today! |
|
And with the addition of not suggesting |
| @@ -95,7 +96,9 @@ commandProvider Intros = | |||
| provide Intros "" | |||
| commandProvider Split = | |||
| foldMapGoalType (F.fold . tyDataCons) $ \dc -> | |||
| provide Split $ T.pack $ occNameString $ getOccName dc | |||
| let cname = occNameString $ getOccName dc | |||
| in requireExtensionWhen MagicHash ("#" `L.isSuffixOf` cname) $ | |||
There was a problem hiding this comment.
Let's use the algebraicTyCon function to do this check instead, though I'd be open to moving this check there.
There was a problem hiding this comment.
There was a problem hiding this comment.
Oh sorry, I misunderstood the check here. I'd argue this behavior is so far out of the ordinary experience of most developers that it's not worth supporting. On second thought, maybe we should gate algebraicTyCon behind -XMagicHash as well. It's a small price to pay, and if someone is going to explicitly enable -XMagicHash we might as well support it.
There was a problem hiding this comment.
For the moment, I will use the algebraicTyCon check, add an ignored test case refering to #31 and tackle it in a follow up PR.
There was a problem hiding this comment.
Sounds good to me. I really appreciate your keen eye on this!
One code action per datatype constructor is produced.
suggesting I# for Int probably is not what you want 99% of the time also reuse tyDataCons, tacname
WorldSEnder
force-pushed
the
split-tactic
branch
from
8d4901b
to
e8c1c03
Compare
Implements #21 but allowing datatypes with more than one constructor: one code action per constructor is produced.
In the current state, the constructor is not scope checked. This works fine most of the time, but might cause troubles down the line. I'm not sure how to implement scope checking correctly: imports might be qualified, renamed or specific to some constructors only. Is there existing machinery to deal with that sort of backwards name resolution inplace of just using
occNameas I did here?