Restrict catch patterns under saferExceptions

Restrict catch patterns to `ex: T` with no guard under saferExceptions
so that capabilities can be generated safely.

Fixes #13849

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

@@ -1745,9 +1745,12 @@ class Typer extends Namer
         .withSpan(expr.span)
     val caps =
       for
-        case CaseDef(pat, EmptyTree, _) <- 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 = {

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

@@ -11,6 +11,6 @@ def foo(): Unit throws Ex = throw Ex(1)
 object Main:
   def main(args: Array[String]): Unit =
     try
-      foo() // error
+      foo()
     catch
-      case _: Ex if false => println("Caught")
+      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