I agree Brian's really onto something with suggesting the totality
question is the same for the two features. I'm in favour of going
even further and removing the cast to allow = to do double duty here
for sealed types rather than introducing new syntax for it. The new
syntax ("__ construct" or "(total BarImpl)") highlights "this is
different" and I'm not sure we need to do that for sealed types.
Letting ='s do the work feels like a better form of auto-boxing where
javac does the compile-time analysis and errors out for non-total
cases or inserts the required total cast for the user. This gives
both compile time checking and runtime safety without needing to beat
the reader over the head about it.
We want to make it easier to read & write correct code - pushing the
analysis of totality for sealed types into javac does both for us.
To connect to the mail that crossed with Dan's, Dan is voting for:
- Allowing `P = e` when P is optimistically total on the static type
of `e`
In reviewing the discussions on this over the past few years, what I'm
seeing is that this requires a certain degree of "getting comfortable"
with it. At first, locutions like this seemed woefully imprecise, and
everyone got nervous, but over time, people have been coming around to
it. The "bargaining" stage involves things like "stick `let` in front
of it", "allow it for locals, but not method parameters", and "require
it to be strictly total (or total only with null remainder.") Over
time, many of these proposed restrictions are seen to be "bargaining"
with change, and we get comfortable with them.
Dan's observation here is that, with a suitable interpretation of total
pattern match as a generalization of local declaration, we don't need
the cast at all, so we sidestep the question.
That said, even if we do that, we're not totally out of the woods, for a
minor and major reason.
The minor reason is the use in expressions. Suppose we have a context
where we are limited to expressions, not statements (e.g., field
initializers, constructor arguments, etc.) or where we just don't want
to use a statement for aesthetic reasons. We still have to use a cast
in these cases, and the cast is still blind. But that's minor.
THe major reason is that we still don't have a way to say "this
statement switch is total, please typecheck that for me." I don't see a
way we get to inferring this, which means we need some syntax. Being
able to reuse the same syntax in other contexts (e.g., casts) may
reinforce it in both places.
