Opting into totality

[Brian Goetz]

Note that this:

On 8/25/2020 7:53 PM, Brian Goetz wrote:
> 	`default <deconstruction pattern>` means the same thing as `case <deconstruction pattern>`
> 		but it is a static error if the <deconstruction pattern> is not_weakly_  total on the type of the selector

when combined with

> I’ll add that in the last case, it is as if there is an implicit `case null: throw`.

comports nicely with the planned semantics for pattern assignment:

     P = e

requires that P be (weakly) total on the static type of e, and is 
permitted to NPE when e is null.  When P is a total type pattern or an 
any pattern, this degenerates to normal variable declaration + 
initialization.  So:

     Box<String> b = ...

     String s = b  // type error
     Box bb = b  // fine, total
     Box(Object o) bb = b  // fine, weakly total, throws NPE when b = null

I will consolidate all of this today into a new message.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.openjdk.java.net/pipermail/amber-spec-experts/attachments/20200826/8ea2f6f9/attachment.htm>