Merge pull request #13866 from dotty-staging/fix-13846

Refine handling of CanThrow capabilities

Author: odersky

compiler/src/dotty/tools/dotc/typer/Checking.scala

@@ -33,6 +33,7 @@ import NameKinds.DefaultGetterName
 import NameOps._
 import SymDenotations.{NoCompleter, NoDenotation}
 import Applications.unapplyArgs
+import Inferencing.isFullyDefined
 import transform.patmat.SpaceEngine.isIrrefutable
 import config.Feature
 import config.Feature.sourceVersion
@@ -1362,6 +1363,21 @@ trait Checking {
   def checkCanThrow(tp: Type, span: Span)(using Context): Unit =
     if Feature.enabled(Feature.saferExceptions) && tp.isCheckedException then
       ctx.typer.implicitArgTree(defn.CanThrowClass.typeRef.appliedTo(tp), span)
+
+  /** Check that catch can generate a good CanThrow exception */
+  def checkCatch(pat: Tree, guard: Tree)(using Context): Unit = pat match
+    case Typed(_: Ident, tpt) if isFullyDefined(tpt.tpe, ForceDegree.none) && guard.isEmpty =>
+      // OK
+    case Bind(_, pat1) =>
+      checkCatch(pat1, guard)
+    case _ =>
+      val req =
+        if guard.isEmpty then "for cases of the form `ex: T` where `T` is fully defined"
+        else "if no pattern guard is given"
+      report.error(
+        em"""Implementation restriction: cannot generate CanThrow capability for this kind of catch.
+            |CanThrow capabilities can only be generated $req.""",
+        pat.srcPos)
 }
 
 trait ReChecking extends Checking {
@@ -1375,6 +1391,7 @@ trait ReChecking extends Checking {
   override def checkMatchable(tp: Type, pos: SrcPos, pattern: Boolean)(using Context): Unit = ()
   override def checkNoModuleClash(sym: Symbol)(using Context) = ()
   override def checkCanThrow(tp: Type, span: Span)(using Context): Unit = ()
+  override def checkCatch(pat: Tree, guard: Tree)(using Context): Unit = ()
 }
 
 trait NoChecking extends ReChecking {

compiler/src/dotty/tools/dotc/typer/Typer.scala

@@ -1751,9 +1751,12 @@ class Typer extends Namer
         .withSpan(expr.span)
     val caps =
       for
-        CaseDef(pat, _, _) <- cases
+        case CaseDef(pat, guard, _) <- cases
         if Feature.enabled(Feature.saferExceptions) && pat.tpe.widen.isCheckedException
-      yield makeCanThrow(pat.tpe.widen)
+      yield
+        checkCatch(pat, guard)
+        makeCanThrow(pat.tpe.widen)
+
     caps.foldLeft(expr)((e, g) => untpd.Block(g :: Nil, e))
 
   def typedTry(tree: untpd.Try, pt: Type)(using Context): Try = {
@@ -1942,14 +1945,20 @@ class Typer extends Namer
       }
       var checkedArgs = preCheckKinds(args1, paramBounds)
         // check that arguments conform to bounds is done in phase PostTyper
-      if (tpt1.symbol == defn.andType)
+      val tycon = tpt1.symbol
+      if (tycon == defn.andType)
         checkedArgs = checkedArgs.mapconserve(arg =>
           checkSimpleKinded(checkNoWildcard(arg)))
-      else if (tpt1.symbol == defn.orType)
+      else if (tycon == defn.orType)
         checkedArgs = checkedArgs.mapconserve(arg =>
           checkSimpleKinded(checkNoWildcard(arg)))
+      else if tycon == defn.throwsAlias
+          && checkedArgs.length == 2
+          && checkedArgs(1).tpe.derivesFrom(defn.RuntimeExceptionClass)
+      then
+        report.error(em"throws clause cannot be defined for RuntimeException", checkedArgs(1).srcPos)
       else if (ctx.isJava)
-        if (tpt1.symbol eq defn.ArrayClass) then
+        if tycon eq defn.ArrayClass then
           checkedArgs match {
             case List(arg) =>
               val elemtp = arg.tpe.translateJavaArrayElementType

docs/docs/reference/experimental/canthrow.md

@@ -179,6 +179,20 @@ closure may refer to capabilities in its free variables. This means that `map` i
 already effect polymorphic even though we did not change its signature at all.
 So the takeaway is that the effects as capabilities model naturally provides for effect polymorphism whereas this is something that other approaches struggle with.
 
+**Note 1:** The compiler will only treat checked exceptions that way. An exception type is _checked_ if it is a subtype of
+`Exception` but not of `RuntimeException`. The signature of `CanThrow` still admits `RuntimeException`s since `RuntimeException` is a proper subtype of its bound, `Exception`. But no capabilities will be generated for `RuntimeException`s. Furthermore, `throws` clauses
+also may not refer to `RuntimeException`s.
+
+**Note 2:** To keep things simple, the compiler will currently only generate capabilities
+for catch clauses of the form
+```scala
+  case ex: Ex =>
+```
+where `ex` is an arbitrary variable name (`_` is also allowed), and `Ex` is an arbitrary
+checked exception type. Constructor patterns such as `Ex(...)` or patterns with guards
+are not allowed. The compiler will issue an error if one of these is used to catch
+a checked exception and `saferExceptions` is enabled.
+
 ## Gradual Typing Via Imports
 
 Another advantage is that the model allows a gradual migration from current unchecked exceptions to safer exceptions. Imagine for a moment that `experimental.saferExceptions` is turned on everywhere. There would be lots of code that breaks since functions have not yet been properly annotated with `throws`. But it's easy to create an escape hatch that lets us ignore the breakages for a while: simply add the import

tests/neg/i13846.check

@@ -0,0 +1,17 @@
+-- Error: tests/neg/i13846.scala:3:22 ----------------------------------------------------------------------------------
+3 |def foo(): Int throws ArithmeticException = 1 / 0 // error
+  |                      ^^^^^^^^^^^^^^^^^^^
+  |                      throws clause cannot be defined for RuntimeException
+-- Error: tests/neg/i13846.scala:7:9 -----------------------------------------------------------------------------------
+7 |    foo() // error
+  |         ^
+  |         The capability to throw exception ArithmeticException is missing.
+  |         The capability can be provided by one of the following:
+  |          - A using clause `(using CanThrow[ArithmeticException])`
+  |          - A `throws` clause in a result type such as `X throws ArithmeticException`
+  |          - an enclosing `try` that catches ArithmeticException
+  |
+  |         The following import might fix the problem:
+  |
+  |           import unsafeExceptions.canThrowAny
+  |

tests/neg/i13846.scala

@@ -0,0 +1,9 @@
+import language.experimental.saferExceptions
+
+def foo(): Int throws ArithmeticException = 1 / 0 // error
+
+def test(): Unit =
+  try
+    foo() // error
+  catch
+    case _: ArithmeticException => println("Caught")

tests/neg/i13849.check

@@ -0,0 +1,5 @@
+-- Error: tests/neg/i13849.scala:16:11 ---------------------------------------------------------------------------------
+16 |      case _: Ex if false => println("Caught") // error
+   |           ^^^^^
+   |           Implementation restriction: cannot generate CanThrow capability for this kind of catch.
+   |           CanThrow capabilities can only be generated if no pattern guard is given.

tests/neg/i13849.scala

@@ -0,0 +1,16 @@
+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") // error

tests/neg/i13864.check

@@ -0,0 +1,18 @@
+-- Error: tests/neg/i13864.scala:11:9 ----------------------------------------------------------------------------------
+11 |    case Ex(i: Int) => println("Caught an Int") // error
+   |         ^^^^^^^^^^
+   |         Implementation restriction: cannot generate CanThrow capability for this kind of catch.
+   |         CanThrow capabilities can only be generated for cases of the form `ex: T` where `T` is fully defined.
+-- Error: tests/neg/i13864.scala:9:10 ----------------------------------------------------------------------------------
+9 |    foo(1) // error
+  |          ^
+  |          The capability to throw exception Ex[Int] is missing.
+  |          The capability can be provided by one of the following:
+  |           - A using clause `(using CanThrow[Ex[Int]])`
+  |           - A `throws` clause in a result type such as `X throws Ex[Int]`
+  |           - an enclosing `try` that catches Ex[Int]
+  |
+  |          The following import might fix the problem:
+  |
+  |            import unsafeExceptions.canThrowAny
+  |

tests/neg/i13864.scala

@@ -0,0 +1,11 @@
+import language.experimental.saferExceptions
+
+case class Ex[A](a: A) extends Exception(s"Ex: $a")
+
+def foo[A](a: A): Unit throws Ex[A] = throw new Ex(a)
+
+def test(): Unit =
+  try
+    foo(1) // error
+  catch
+    case Ex(i: Int) => println("Caught an Int") // error