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 all 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
34 changes: 23 additions & 11 deletions 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.SkolemizedArgs
import collection.mutable
import scala.annotation.internal.sharable

Expand Down Expand Up @@ -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
}
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
50 changes: 35 additions & 15 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 @@ -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 =
Expand All @@ -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 = {
Expand Down Expand Up @@ -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)
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