Safer exceptions with many cases in catch

[prolativ]

Compiler version

3.1.1-RC1-bin-20211020-afaac17-NIGHTLY

Minimized code

import language.experimental.saferExceptions

class Ex1 extends Exception("Ex1")
class Ex2 extends Exception("Ex2")

def foo1(i: Int): Unit throws Ex1 throws Ex2 =
   if i > 0 then throw new Ex1 else throw new Ex2

def foo2(i: Int): Unit throws (Ex1 | Ex2) =
   if i > 0 then throw new Ex1 else throw new Ex2

def foo3(i: Int)(using CanThrow[Ex1], CanThrow[Ex2]) =
   if i > 0 then throw new Ex1 else throw new Ex2

def foo4(i: Int)(using CanThrow[Ex1])(using CanThrow[Ex2]) =
   if i > 0 then throw new Ex1 else throw new Ex2

def foo5(i: Int)(using CanThrow[Ex1 | Ex2]) =
   if i > 0 then throw new Ex1 else throw new Ex2

def test(): Unit =
  try {
    foo1(1)
    foo2(1) // error
    foo3(1)
    foo4(1)
    foo5(1) // error
  } catch {
    case _: Ex1 =>
    case _: Ex2 => 
  }

Output

[error] -- Error: /Users/mpalka/Projects/dotty-test/tmp/src/main/scala/test.scala:24:11 
[error] 24 |    foo2(1) // error
[error]    |           ^
[error]    |      The capability to throw exception Ex1 | Ex2 is missing.
[error]    |      The capability can be provided by one of the following:
[error]    |       - A using clause `(using CanThrow[Ex1 | Ex2])`
[error]    |       - A `throws` clause in a result type such as `X throws Ex1 | Ex2`
[error]    |       - an enclosing `try` that catches Ex1 | Ex2
[error]    |
[error]    |      The following import might fix the problem:
[error]    |
[error]    |        import unsafeExceptions.canThrowAny
[error]    |
[error] -- Error: /Users/mpalka/Projects/dotty-test/tmp/src/main/scala/test.scala:27:11 
[error] 27 |    foo5(1) // error
[error]    |           ^
[error]    |      The capability to throw exception Ex1 | Ex2 is missing.
[error]    |      The capability can be provided by one of the following:
[error]    |       - A using clause `(using CanThrow[Ex1 | Ex2])`
[error]    |       - A `throws` clause in a result type such as `X throws Ex1 | Ex2`
[error]    |       - an enclosing `try` that catches Ex1 | Ex2
[error]    |
[error]    |      The following import might fix the problem:
[error]    |
[error]    |        import unsafeExceptions.canThrowAny
[error]    |
[error] two errors found
[error] two errors found

Expectation

The compiler should be able to figure out that all the declared exceptions are handled. Interestingly adding case _: (Ex1 | Ex2) => inside catch makes the compiler stop complaining

[odersky]

The first error we can fix but not the second.

We do not allow aggregation of CanThrow arguments. That is out of scope and would require new theoritac research to address.

[prolativ]

I might be misunderstanding something but looking at the discussions around the original PR #11721 I still don't understand why throws Ex1 | Ex2 should get translated to (using CanThrow[Ex1 & Ex2]) and not (using CanThrow[Ex1 | Ex2]) as we either throw one type of exception or the other, not something that inherits from both.

If we had a simple contravariant type class like

trait Show[-A]:
  def show(a: A): String

def show[A : Show](a: A) = summon[Show[A]].show(a)

given Show[Int | String] = _ match
  case i: Int => i.toString
  case s: String => s

Then an instance of Show[Int | String] can handle both Ints and Strings. Also intuitively CanThrow[Ex1 | Ex2] should be able to handle both Ex1 and Ex2 (formally if both Ex1 and Ex2 extend Ex1 | Ex2 then, as CanThrow is contravariant, CanThrow[Ex1 | Ex2] is a subtype of both CanThrow[Ex1] and CanThrow[Ex2]).
So why don't we just slightly change the desugaring of try clauses?
Currently

try {
  ....
} catch {
  case _: Ex1 =>
  case _: Ex2 =>
}

desugars to

try {
  erased given CanThrow[Ex1] = ???
  erased given CanThrow[Ex2] = ???
  ....
} catch {
  case _: Ex1 =>
  case _: Ex2 =>
}

but if it instead gets desugared to

try {
  erased given CanThrow[Ex1 | Ex2] = ???
  ....
} catch {
  case _: Ex1 =>
  case _: Ex2 =>
}

then everything should work.
I even tried implementing this change (which is actually very simple) and indeed the initial example compiled successfully even foo5.
@odersky Did I miss something? If this seems correct then I'll push my fix to the PR.

[odersky]

@prolativ: You are right. I was confused because throws E1 | E2 logically translates to CanThrow[E1] & CanThrow[E2]
but that by itself is again CanThrow[E1 | E1] since CanThrow is contravariant. So, please go ahead and push your fix to the PR.