Skip to content

Refinements to skolemizaton #23513

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jul 15, 2025
Merged
Show file tree
Hide file tree
Changes from 3 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 7 additions & 3 deletions compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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
}
}

Expand Down
5 changes: 4 additions & 1 deletion compiler/src/dotty/tools/dotc/transform/patmat/Space.scala
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
4 changes: 3 additions & 1 deletion compiler/src/dotty/tools/dotc/typer/Inferencing.scala
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ import Decorators._
import config.Printers.{gadts, typr}
import annotation.tailrec
import reporting.*
import TypeAssigner.skolemizeArgType
import collection.mutable
import scala.annotation.internal.sharable

Expand Down Expand Up @@ -853,7 +854,8 @@ trait Inferencing { this: Typer =>
val arg = findArg(call)
if !arg.isEmpty then
var argType = arg.tpe.widenIfUnstable
if !argType.isSingleton then argType = SkolemType(argType)
if !argType.isSingleton then
argType = skolemizeArgType(argType, arg)
argType <:< tvar
case _ =>
end constrainIfDependentParamRef
Expand Down
3 changes: 2 additions & 1 deletion compiler/src/dotty/tools/dotc/typer/Namer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -2245,8 +2245,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
Expand Down
43 changes: 32 additions & 11 deletions compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,7 @@ import collection.mutable
import reporting.*
import Checking.{checkNoPrivateLeaks, checkNoWildcard}
import cc.CaptureSet
import util.Property
import transform.Splicer

trait TypeAssigner {
Expand Down Expand Up @@ -273,33 +274,32 @@ trait TypeAssigner {
/** Substitute argument type `argType` for parameter `pref` in type `tp`,
* skolemizing the argument type if it is not stable and `pref` occurs in `tp`.
*/
def safeSubstParam(tp: Type, pref: ParamRef, argType: Type)(using Context): Type = {
def safeSubstParam(tp: Type, pref: ParamRef, argType: Type, arg: Tree | 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 tp.substParam(pref, skolemizeArgType(argType.widen, arg))
}

/** 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.
*/
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)
def safeSubstParams(tp: Type, params: List[ParamRef], args: List[Tree])(using Context): Type = args match
case arg :: args1 =>
val tp1 = safeSubstParam(tp, params.head, arg.tpe, arg)
safeSubstParams(tp1, params.tail, args1)
case Nil =>
tp
}

def safeSubstMethodParams(mt: MethodType, argTypes: List[Type])(using Context): Type =
if mt.isResultDependent then safeSubstParams(mt.resultType, mt.paramRefs, argTypes)
def safeSubstMethodParams(mt: MethodType, args: List[Tree])(using Context): Type =
if mt.isResultDependent then safeSubstParams(mt.resultType, mt.paramRefs, args)
else mt.resultType

def assignType(tree: untpd.Apply, fn: Tree, args: List[Tree])(using Context): Apply = {
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 safeSubstMethodParams(fntpe, args)
else fntpe.resultType // fast path optimization
else
val erroringPhase =
Expand Down Expand Up @@ -570,6 +570,27 @@ trait TypeAssigner {
}

object TypeAssigner extends TypeAssigner:

/** An attachment on an argument in an application indicating that the argument's
* type was converted to the given skolem type.
*/
private val Skolemized = new Property.StickyKey[SkolemType]

/** A skolem type wrapping `argType`, associated with `arg` if it is non-null.
* Skolem types for the same arguments with equal underlying `argType`s are re-used.
*/
def skolemizeArgType(argType: Type, arg: tpd.Tree | Null)(using Context): Type =
if arg == null then
SkolemType(argType)
else
arg.getAttachment(Skolemized) match
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Couldn't it happen that the same argument tree is shared among different application trees? In that case, wouldn't that be wrong to give them the same skolem type?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that's indeed a concern. We don't usually share trees but we don't have a guarantee here.

case Some(sk @ SkolemType(tp)) if argType frozen_=:= tp =>
sk
case _ =>
val sk = SkolemType(argType)
arg.putAttachment(Skolemized, sk)
sk

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)
2 changes: 1 addition & 1 deletion compiler/src/dotty/tools/dotc/typer/Typer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4355,7 +4355,7 @@ class Typer(@constructorOnly nestingLevel: Int = 0) extends Namer
def inferArgsAfter(leading: Tree) =
val formals2 =
if wtp.isParamDependent && leading.tpe.exists then
formals1.mapconserve(f1 => safeSubstParam(f1, wtp.paramRefs(argIndex), leading.tpe))
formals1.mapconserve(f1 => safeSubstParam(f1, wtp.paramRefs(argIndex), leading.tpe, leading))
else formals1
implicitArgs(formals2, argIndex + 1, pt)

Expand Down
13 changes: 13 additions & 0 deletions tests/pos/i23489.scala
Original file line number Diff line number Diff line change
@@ -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()))
Loading