Fix #5854: check type annotations for soundness

Author: liufengyun

compiler/src/dotty/tools/dotc/transform/init/Summarization.scala

@@ -107,7 +107,7 @@ object Summarization {
 
       case Typed(expr, tpt) =>
         if (tpt.tpe.hasAnnotation(defn.UncheckedAnnot)) Summary.empty
-        else analyze(expr)
+        else analyze(expr) ++ effectsOfType(tpt.tpe, tpt)
 
       case NamedArg(name, arg) =>
         analyze(arg)
@@ -201,20 +201,7 @@ object Summarization {
 
       case tdef: TypeDef =>
         if tdef.isClassDef then Summary.empty
-        else {
-          var summary = Summary.empty
-          val tp = tdef.symbol.info
-          val traverser = new TypeTraverser {
-            def traverse(tp: Type): Unit = tp match {
-              case TermRef(_: SingletonType, _) =>
-                summary = summary + analyze(tp, tdef.rhs)
-              case _ =>
-                traverseChildren(tp)
-            }
-          }
-          traverser.traverse(tp)
-          summary
-        }
+        else Summary(effectsOfType(tdef.symbol.info, tdef.rhs))
 
       case _: Import | _: Export =>
         Summary.empty
@@ -227,6 +214,19 @@ object Summarization {
     else summary
   }
 
+  private def effectsOfType(tp: Type, source: Tree)(implicit env: Env): Effects =
+    var summary = Summary.empty
+    val traverser = new TypeTraverser {
+      def traverse(tp: Type): Unit = tp match {
+        case TermRef(_: SingletonType, _) =>
+          summary = summary + analyze(tp, source)
+        case _ =>
+          traverseChildren(tp)
+      }
+    }
+    traverser.traverse(tp)
+    summary.effs
+
   def analyze(tp: Type, source: Tree)(implicit env: Env): Summary =
   trace("summarizing " + tp.show, init, s => s.asInstanceOf[Summary].show) {
     val summary: Summary = tp match {
@@ -257,8 +257,8 @@ object Summarization {
         }
         Summary(pots2, effs)
 
-      case _: TermParamRef =>
-        // possible from type definitions
+      case _: TermParamRef | _: RecThis  =>
+        // possible from checking effects of types
         Summary.empty
 
       case _ =>

tests/init/neg/i5854.scala

@@ -0,0 +1,5 @@
+class B {
+  val a: String = (((1: Any): b.A): Nothing): String
+  val b: { type A >: Any <: Nothing } = loop()         // error
+  def loop(): Nothing = loop()
+}

tests/neg-strict/i5854.scala

@@ -0,0 +1,24 @@
+object bar {
+  trait Sub {
+    type M
+    type L <: M
+    type U >: M
+    type M2 >: L <: U
+  }
+  class Box[V](val v: V)
+
+  class Caster[LL, UU] {
+    trait S2 {
+      type L = LL
+      type U = UU
+    }
+    final lazy val nothing: Nothing = nothing
+    final lazy val sub: S2 & Sub = nothing
+    final lazy val box : Box[S2 & Sub] = new Box(nothing)
+    def upcast(t: box.v.M2): box.v.M2 = t  // error // error
+  }
+  def main(args : Array[String]) : Unit = {
+    val zero : String = (new Caster[Int,String]()).upcast(0)
+    println("...")
+  }
+}