`Switch` attribute for unique and/or full `Case`s

[awygle]

It would be useful to be able to indicate that a Switch should cover all possible Cases, or at least that the given Cases should not overlap.

[jeanthom]

Somewhat related to https://github.com/nmigen/nmigen/issues/404 and https://github.com/nmigen/nmigen/issues/436

[whitequark]

Yeah, I think all of these should be implemented as lints with configurable severity.

[awygle]

I actually disagree that these should be lints. To my mind, a lint would make sense if the property we were looking for wasn't wholly contained to a particular language construct. In this case, the semantics of Switch(mode="full") vs Switch(mode="unique") vs Switch(mode="priority") (syntax descriptive only at this time) are both well-defined and entirely contained to the Switch context manager. Can you explain on your thinking as to why these would be lints?

[whitequark]

Can you explain on your thinking as to why these would be lints?

Two reasons:

1. Lints are something that can be removed without changing the semantics of the program at all. Not everything that fulfills this requirement must be a lint, but lints are generally more lightweight, so I default to those.
2. In my mind, people will want something along the lines of "please ensure all of the cases in my program/file/module are full", and lints would need to have a mechanism for inheriting them from outer scopes.

[awygle]

I see. I agree that 2 is a good reason to have a lint. I'll sit and think a bit about whether I want a lint also or a lint instead.

For 1, what do you mean by "lightweight"? Syntactically, at least the way I'm imagining them working (and yes, I know we haven't designed them yet), from a user perspective using a lint would be heavier-weight than passing a constructor argument (not to mention adding rightward lean), but maybe you have a different mental picture.

[whitequark]

For 1, what do you mean by "lightweight"?

In the sense that it doesn't introduce changes to the core language, not in terms of end-user syntax. I agree that syntactically a lint can end up being heavier.

[whitequark]

We discussed this on the meeting. The conclusion was that we want both the Switch-specific attribute (syntactically a kwarg) and a lint, because they serve different goals: Switch(mode="unique") explicitly declares intent for this specific Switch, whereas enabling a lint that warns (or errors) on non-unique switches implicitly analyzes your code for suspicious constructs in general.

Also, without the kwarg, disabling the lint for just a single Switch that may contain nested Switches introduces extreme rightward drift of 2 indents, which would likely significantly detract from the lint's usability. In other words, the kwarg completes the lint instead of competing with it.

[whitequark]

I'm going to close this issue since not much need has been expressed for this feature and as a consequence there are no current plans to add support it. Please feel free to comment on this issue if you would like to see it happen.

Please also note that there was no strong consensus on whether the feature should be implemented as a lint or as a syntactic feature. It is not clear whether it would work well as a lint (that should probably be trialed on Amaranth code); as for it being a syntactic feature, it is unclear how it would interact with value-castables, which were introduced after this proposal has been made.