CanThrow capability shouldn't be synthesized for nonexhaustive catch clauses

[prolativ]

Compiler version

3.1.1-RC1

Minimized code

import annotation.experimental
import language.experimental.saferExceptions

@experimental
case class Ex(i: Int) extends Exception(s"Exception: $i")

@experimental
def foo(): Unit throws Ex = throw Ex(1)

@experimental
object Main:
  def main(args: Array[String]): Unit =
    try
      foo()
    catch
      case _: Ex if false => println("Caught")

Output

[error] Ex: Exception: 1
[error]         at Ex$.apply(test.scala:4)
[error]         at test$package$.foo(test.scala:8)
[error]         at Main$.main(test.scala:14)
[error]         at Main.main(test.scala)
[error]         at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
[error]         at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
[error]         at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
[error]         at java.lang.reflect.Method.invoke(Method.java:498)

Expectation

This should not compile. The compiler should not synthesize given instances of CanThrow if it cannot prove at compile time that all subcases for a given exception type are handled.
Beside boolean guards we should also handle extractors like

    catch
      case Ex(0) => println("Caught")

[prolativ]

We should also think how/whether to handle situations when a match is exhaustive but spread across multiple try/catch clauses, e.g.

import annotation.experimental
import language.experimental.saferExceptions

@experimental
case class Ex(i: Int) extends Exception(s"Exception: $i")

@experimental
def foo(): Unit throws Ex = Ex(1)

@experimental
object Main:
  def main(args: Array[String]): Unit =
    try
      try
        foo()
      catch
        case Ex(x) if x > 0 => println("Caught positive Ex")
    catch
      case Ex(x) if x <= 0 => println("Caught nonpositive Ex")

[odersky]

I don't think there's a chance we could handle this.

[odersky]

The intention is that this is a simple & transparent desugaring. That means we should not overthink this and add all sorts of additional conditions for certain things to trigger.

[prolativ]

How about synthesizing given CanThrow only for typed catch patterns in the shape of case ex: Ex => without guards and extractors? Inside the body of the case clause ex could still be matched on to handle specific cases with extractors or in some situations it could be rethrown if it cannot be properly handled (that would require the method in which the entire try block is embedded to declare throws Ex as well but this seems consistent and still gives us a lot of flexibility without loosing type safety)

[odersky]

Yes I think that is the way to go. I think we should make it an error to use other handlers for checked exceptions if saferExceptions is imported.