Empty exhaustive switches and the ability to refine type variables

[Tesla Zhang]

Thanks!! That's great to hear.





Regards,
Tesla

---Original---
From: "Brian Goetz"<brian.goetz at oracle.com>
Date: Tue, Mar 22, 2022 16:17 PM
To: "Tesla Zhang"<ice1000kotlin at foxmail.com>;"amber-dev"<amber-dev at openjdk.java.net>;
Subject: Re: Empty exhaustive switches and the ability to refine type variables


           I think I may have         misunderstood your earlier question.  An uninhabitable switch is         one over a sealed type for which none of the type patterns         apply, such as:
         
             sealed interface X<T> { }
             final class A implements X<String> {} 
             final class B implements X<Integer> {}
         
             X<Frog> x = ...
             switch (x) { 
                 // none of the subtypes of X are applicable
             }
         
         So this would fall out as a natural consequence of eliminating         inapplicable choices.  
         
         In any case, the issues surrounding GADTs are more than just         exhaustiveness; you mention type refinement, and there are also         other consequences for type checking.  These are going to take a         while to work through.  Rest assured they're on our radar.  
       
     On 3/22/2022 4:13 PM, Tesla Zhang       wrote:
     
            Greetings, I asked if empty switch (the switched expression has an uninhabitable type so no case clause is needed) would be possible because the second preview of switch expressions allows refuting patterns, and Brian told me it's 'unlikely', see https://mail.openjdk.java.net/pipermail/amber-dev/2021-November/007161.html. I still don't understand why it's unlikely, because for example sealed interface I<T&gt; {} record R() implements I<String&gt; {} <T&gt; T test(I<Integer&gt; i) { return switch (i) { <what to do here?&gt; }; } The switch should be well-typed without any case, which is a counterexample. Apart from that, Brian also mentioned a 'probable bug' in&nbsp;https://mail.openjdk.java.net/pipermail/amber-dev/2021-November/007156.html related to casting refinable types, is that addressed now? I explored the mailing list archive but I didn't find relevant discussions. I think it would be very nice for javac to be able to refine a local type. Best regards, Tesla