Refinements to skolemizaton (#23513)

1. Deskolemize after fully defining type

The order was the opposite before. That led to skolem types escaping in
the constraint and then being installed in the inferred type of a val or
def. See #23489 for a test case where this shows up.

2. Re-use skolems generated for arguments. 

Fixes #23489

Author: odersky

compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala

@@ -459,9 +459,13 @@ class PlainPrinter(_ctx: Context) extends Printer {
         if (idx >= 0) selfRecName(idx + 1)
         else "{...}.this" // TODO move underlying type to an addendum, e.g. ... z3 ... where z3: ...
       case tp: SkolemType =>
-        if (homogenizedView) toText(tp.info)
-        else if (ctx.settings.XprintTypes.value) "<" ~ toText(tp.repr) ~ ":" ~ toText(tp.info) ~ ">"
-        else toText(tp.repr)
+        def reprStr = toText(tp.repr) ~ hashStr(tp)
+        if homogenizedView then
+          toText(tp.info)
+        else if ctx.settings.XprintTypes.value then
+          "<" ~ reprStr ~ ":" ~ toText(tp.info) ~ ">"
+        else
+          reprStr
     }
   }
 

compiler/src/dotty/tools/dotc/transform/patmat/Space.scala

@@ -570,7 +570,10 @@ object SpaceEngine {
     // Case unapplySeq:
     // 1. return the type `List[T]` where `T` is the element type of the unapplySeq return type `Seq[T]`
 
-    val resTp = wildApprox(ctx.typeAssigner.safeSubstMethodParams(mt, scrutineeTp :: Nil).finalResultType)
+    var resTp0 = mt.resultType
+    if mt.isResultDependent then
+      resTp0 = ctx.typeAssigner.safeSubstParam(resTp0, mt.paramRefs.head, scrutineeTp)
+    val resTp = wildApprox(resTp0.finalResultType)
 
     val sig =
       if (resTp.isRef(defn.BooleanClass))

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

@@ -13,6 +13,7 @@ import Decorators._
 import config.Printers.{gadts, typr}
 import annotation.tailrec
 import reporting.*
+import TypeAssigner.SkolemizedArgs
 import collection.mutable
 import scala.annotation.internal.sharable
 
@@ -839,22 +840,33 @@ trait Inferencing { this: Typer =>
     if tvar.origin.paramName.is(NameKinds.DepParamName) then
       representedParamRef(tvar.origin) match
         case ref: TermParamRef =>
-          def findArg(tree: Tree)(using Context): Tree = tree match
-            case Apply(fn, args) =>
+          def findArg(tree: Tree)(using Context): Option[(Tree, Apply)] = tree match
+            case app @ Apply(fn, args) =>
               if fn.tpe.widen eq ref.binder then
-                if ref.paramNum < args.length then args(ref.paramNum)
-                else EmptyTree
+                if ref.paramNum < args.length then Some((args(ref.paramNum), app))
+                else None
               else findArg(fn)
             case TypeApply(fn, _) => findArg(fn)
             case Block(_, expr) => findArg(expr)
             case Inlined(_, _, expr) => findArg(expr)
-            case _ => EmptyTree
-
-          val arg = findArg(call)
-          if !arg.isEmpty then
-            var argType = arg.tpe.widenIfUnstable
-            if !argType.isSingleton then argType = SkolemType(argType)
-            argType <:< tvar
+            case _ => None
+
+          findArg(call) match
+            case Some((arg, app)) =>
+              var argType = arg.tpe.widenIfUnstable
+              if !argType.isSingleton then
+                argType = app.getAttachment(SkolemizedArgs) match
+                  case Some(mapping) =>
+                    mapping.get(arg) match
+                      case Some(sk @ SkolemType(at)) =>
+                        assert(argType frozen_=:= at)
+                        sk
+                      case _ =>
+                        SkolemType(argType)
+                  case _ =>
+                    SkolemType(argType)
+              argType <:< tvar
+            case _ =>
         case _ =>
   end constrainIfDependentParamRef
 }

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

@@ -2247,8 +2247,9 @@ class Namer { typer: Typer =>
     // it would be erased to BoxedUnit.
     def dealiasIfUnit(tp: Type) = if (tp.isRef(defn.UnitClass)) defn.UnitType else tp
 
-    def cookedRhsType = dealiasIfUnit(rhsType).deskolemized
+    def cookedRhsType = dealiasIfUnit(rhsType)
     def lhsType = fullyDefinedType(cookedRhsType, "right-hand side", mdef.srcPos)
+      .deskolemized
     //if (sym.name.toString == "y") println(i"rhs = $rhsType, cooked = $cookedRhsType")
     if (inherited.exists)
       if sym.isInlineVal || isTracked then lhsType else inherited

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

@@ -12,6 +12,7 @@ import collection.mutable
 import reporting.*
 import Checking.{checkNoPrivateLeaks, checkNoWildcard}
 import cc.CaptureSet
+import util.Property
 import transform.Splicer
 
 trait TypeAssigner {
@@ -270,36 +271,43 @@ trait TypeAssigner {
     untpd.cpy.Super(tree)(qual, tree.mix)
       .withType(superType(qual.tpe, tree.mix, mixinClass, tree.srcPos))
 
+  private type SkolemBuffer = mutable.ListBuffer[(Tree, SkolemType)]
+
   /** Substitute argument type `argType` for parameter `pref` in type `tp`,
    *  skolemizing the argument type if it is not stable and `pref` occurs in `tp`.
+   *  If skolemization happens the new SkolemType is passed to `recordSkolem`
+   *  provided the latter is non-null.
    */
-  def safeSubstParam(tp: Type, pref: ParamRef, argType: Type)(using Context): Type = {
+  def safeSubstParam(tp: Type, pref: ParamRef, argType: Type,
+      recordSkolem: (SkolemType => Unit) | Null = null)(using Context): Type =
     val tp1 = tp.substParam(pref, argType)
-    if ((tp1 eq tp) || argType.isStable) tp1
-    else tp.substParam(pref, SkolemType(argType.widen))
-  }
+    if (tp1 eq tp) || argType.isStable then tp1
+    else
+      val narrowed = SkolemType(argType.widen)
+      if recordSkolem != null then recordSkolem(narrowed)
+      tp.substParam(pref, narrowed)
 
   /** Substitute types of all arguments `args` for corresponding `params` in `tp`.
    *  The number of parameters `params` may exceed the number of arguments.
    *  In this case, only the common prefix is substituted.
+   *  Skolems generated by `safeSubstParam` are stored in `skolems`.
    */
-  def safeSubstParams(tp: Type, params: List[ParamRef], argTypes: List[Type])(using Context): Type = argTypes match {
-    case argType :: argTypes1 =>
-      val tp1 = safeSubstParam(tp, params.head, argType)
-      safeSubstParams(tp1, params.tail, argTypes1)
+  private def safeSubstParams(tp: Type, params: List[ParamRef],
+      args: List[Tree], skolems: SkolemBuffer)(using Context): Type = args match
+    case arg :: args1 =>
+      val tp1 = safeSubstParam(tp, params.head, arg.tpe, sk => skolems += ((arg, sk)))
+      safeSubstParams(tp1, params.tail, args1, skolems)
     case Nil =>
       tp
-  }
-
-  def safeSubstMethodParams(mt: MethodType, argTypes: List[Type])(using Context): Type =
-    if mt.isResultDependent then safeSubstParams(mt.resultType, mt.paramRefs, argTypes)
-    else mt.resultType
 
   def assignType(tree: untpd.Apply, fn: Tree, args: List[Tree])(using Context): Apply = {
+    var skolems: SkolemBuffer | Null = null
     val ownType = fn.tpe.widen match {
       case fntpe: MethodType =>
         if fntpe.paramInfos.hasSameLengthAs(args) || ctx.phase.prev.relaxedTyping then
-          if fntpe.isResultDependent then safeSubstMethodParams(fntpe, args.tpes)
+          if fntpe.isResultDependent then
+            skolems = new mutable.ListBuffer()
+            safeSubstParams(fntpe.resultType, fntpe.paramRefs, args, skolems.nn)
           else fntpe.resultType // fast path optimization
         else
           val erroringPhase =
@@ -312,7 +320,13 @@ trait TypeAssigner {
         if (ctx.settings.Ydebug.value) new FatalError("").printStackTrace()
         errorType(err.takesNoParamsMsg(fn, ""), tree.srcPos)
     }
-    ConstFold.Apply(tree.withType(ownType))
+    val app = tree.withType(ownType)
+    if skolems != null
+        && skolems.nn.nonEmpty  // @notional why is `.nn` needed here?
+        && skolems.nn.size == skolems.nn.toSet.size // each skolemized argument is unique
+    then
+      app.putAttachment(SkolemizedArgs, skolems.nn.toMap)
+    ConstFold.Apply(app)
   }
 
   def assignType(tree: untpd.TypeApply, fn: Tree, args: List[Tree])(using Context): TypeApply = {
@@ -570,6 +584,12 @@ trait TypeAssigner {
 }
 
 object TypeAssigner extends TypeAssigner:
+
+  /** An attachment on an application indicating a map from arguments to the skolem types
+   *  that were created in safeSubstParams.
+   */
+  private[typer] val SkolemizedArgs = new Property.Key[Map[tpd.Tree, SkolemType]]
+
   def seqLitType(tree: untpd.SeqLiteral, elemType: Type)(using Context) = tree match
     case tree: untpd.JavaSeqLiteral => defn.ArrayOf(elemType)
     case _ => if ctx.erasedTypes then defn.SeqType else defn.SeqType.appliedTo(elemType)

tests/pos/i23489.scala

@@ -0,0 +1,13 @@
+import scala.language.experimental.modularity
+
+class Box1[T <: Singleton](val x: T)
+class Box2[T : Singleton](x: => T)
+def id(x: Int): x.type = x
+def readInt(): Int = ???
+
+def Test = ()
+  val x = Box1(id(readInt()))
+
+  val _: Box1[? <: Int] = x
+
+  val y = Box2(id(readInt()))