Skip to content

Fix #2142: Skolemize arguments of dependent methods if necessary #2215

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 5 commits into from
Apr 11, 2017
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
14 changes: 11 additions & 3 deletions compiler/src/dotty/tools/dotc/printing/Formatting.scala
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ object Formatting {
else nonSensicalStartTag + str + nonSensicalEndTag
}

private type Recorded = AnyRef /*Symbol | TypeParamRef*/
private type Recorded = AnyRef /*Symbol | TypeParamRef | SkolemType */

private class Seen extends mutable.HashMap[String, List[Recorded]] {

Expand Down Expand Up @@ -135,8 +135,13 @@ object Formatting {
if ((sym is ModuleClass) && sym.sourceModule.exists) simpleNameString(sym.sourceModule)
else seen.record(super.simpleNameString(sym), sym)

override def TypeParamRefNameString(param: TypeParamRef): String =
seen.record(super.TypeParamRefNameString(param), param)
override def ParamRefNameString(param: ParamRef): String =
seen.record(super.ParamRefNameString(param), param)

override def toTextRef(tp: SingletonType): Text = tp match {
case tp: SkolemType => seen.record(tp.repr, tp)
case _ => super.toTextRef(tp)
}
}

/** Create explanation for single `Recorded` type or symbol */
Expand Down Expand Up @@ -165,6 +170,8 @@ object Formatting {
s"is a type variable${addendum("constraint", ctx.typeComparer.bounds(param))}"
case sym: Symbol =>
s"is a ${ctx.printer.kindString(sym)}${sym.showExtendedLocation}${addendum("bounds", sym.info)}"
case tp: SkolemType =>
s"is an unknown value of type ${tp.widen.show}"
}
}

Expand All @@ -176,6 +183,7 @@ object Formatting {
private def explanations(seen: Seen)(implicit ctx: Context): String = {
def needsExplanation(entry: Recorded) = entry match {
case param: TypeParamRef => ctx.typerState.constraint.contains(param)
case skolem: SkolemType => true
case _ => false
}

Expand Down
12 changes: 7 additions & 5 deletions compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala
Original file line number Diff line number Diff line change
Expand Up @@ -134,7 +134,7 @@ class PlainPrinter(_ctx: Context) extends Printer {
case tp: TypeType =>
toTextRHS(tp)
case tp: TermRef
if !tp.denotationIsCurrent && !homogenizedView || // always print underyling when testing picklers
if !tp.denotationIsCurrent && !homogenizedView || // always print underlying when testing picklers
tp.symbol.is(Module) ||
tp.symbol.name.isImportName =>
toTextRef(tp) ~ ".type"
Expand Down Expand Up @@ -183,7 +183,9 @@ class PlainPrinter(_ctx: Context) extends Printer {
toTextGlobal(tp.resultType)
}
case tp: TypeParamRef =>
TypeParamRefNameString(tp) ~ lambdaHash(tp.binder)
ParamRefNameString(tp) ~ lambdaHash(tp.binder)
case tp: TermParamRef =>
ParamRefNameString(tp) ~ ".type"
case AnnotatedType(tpe, annot) =>
toTextLocal(tpe) ~ " " ~ toText(annot)
case HKApply(tycon, args) =>
Expand All @@ -206,10 +208,10 @@ class PlainPrinter(_ctx: Context) extends Printer {
}
}.close

protected def TypeParamRefNameString(name: TypeName): String = name.toString
protected def ParamRefNameString(name: Name): String = name.toString

protected def TypeParamRefNameString(param: TypeParamRef): String =
TypeParamRefNameString(param.binder.paramNames(param.paramNum))
protected def ParamRefNameString(param: ParamRef): String =
ParamRefNameString(param.binder.paramNames(param.paramNum))

/** The name of the symbol without a unique id. Under refined printing,
* the decoded original name.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -604,7 +604,7 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) {
def optText[T >: Untyped](tree: List[Tree[T]])(encl: Text => Text): Text =
if (tree.exists(!_.isEmpty)) encl(blockText(tree)) else ""

override protected def TypeParamRefNameString(name: TypeName): String =
override protected def ParamRefNameString(name: Name): String =
name.unexpandedName.toString

override protected def treatAsTypeParam(sym: Symbol): Boolean = sym is TypeParam
Expand Down
5 changes: 2 additions & 3 deletions compiler/src/dotty/tools/dotc/typer/Applications.scala
Original file line number Diff line number Diff line change
Expand Up @@ -395,9 +395,8 @@ trait Applications extends Compatibility { self: Typer with Dynamic =>
def addTyped(arg: Arg, formal: Type): Type => Type = {
addArg(typedArg(arg, formal), formal)
if (methodType.isParamDependent)
_.substParam(methodType.newParamRef(n), typeOfArg(arg))
else
identity
substArgForParam(_, typeOfArg(arg), methodType.paramRefs(n))
else identity
}

def missingArg(n: Int): Unit = {
Expand Down
20 changes: 19 additions & 1 deletion compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala
Original file line number Diff line number Diff line change
Expand Up @@ -315,10 +315,28 @@ 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 substArgForParam(tp: Type, argType: Type, pref: ParamRef)(implicit ctx: Context) = {
Copy link
Member

Choose a reason for hiding this comment

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

Minor suggestion: all the subst* methods have the from argument before the to argument, here it's the reverse order which can be a bit confusing. If this is changed it probably makes sense to rename the method to substParamWithArg too.

val tp1 = tp.substParam(pref, argType)
if ((tp1 eq tp) || argType.isStable) tp1
else tp.substParam(pref, SkolemType(argType.widen))
Copy link
Member

Choose a reason for hiding this comment

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

I would have expected widenSingleton here but I don't know if that makes sense or not.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

For SkolemTypes, it's widen also elsewhere. We don't want to get ExprTypes in there.

}

def assignType(tree: untpd.Apply, fn: Tree, args: List[Tree])(implicit ctx: Context) = {
val ownType = fn.tpe.widen match {
case fntpe: MethodType =>
if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping) fntpe.instantiate(args.tpes)
Copy link
Member

Choose a reason for hiding this comment

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

Would it make sense to change the definition of instantiate to do the skolemization?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

No, I think that's too low-level. By analogy, asSeenFrom does not do skolemization, but reports back that skolemization is needed, and then Typer does it.

def substArgsForParams(tp: Type, args: List[Tree], params: List[ParamRef]): Type = params match {
case param :: params1 =>
val tp1 = substArgForParam(tp, args.head.tpe, param)
substArgsForParams(tp1, args.tail, params1)
case Nil =>
tp
}
if (sameLength(fntpe.paramInfos, args) || ctx.phase.prev.relaxedTyping)
if (fntpe.isDependent) substArgsForParams(fntpe.resultType, args, fntpe.paramRefs)
else fntpe.resultType
else
errorType(i"wrong number of arguments for $fntpe: ${fn.tpe}, expected: ${fntpe.paramInfos.length}, found: ${args.length}", tree.pos)
case t =>
Expand Down
28 changes: 28 additions & 0 deletions tests/neg/i2142.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,28 @@
object Foo {

class A
val a1 = new A()
val a2 = new A()

def f(x: A, y: x.type) = ()
f(a1, a1) // ok
f(a1, a2) // error
f(new A(), new A()) // error
f(new A(), a1) // error

def g(x: A)(y: x.type) = ()
g(a1)(a1) // ok
g(a1)(a2) // error
g(new A())(new A()) // error
g(new A())(a1) // error

val x0 = g(new A()) _
x0 (new A()) // error

class C[T]

def h(x: A): C[x.type] = ???
val x = h(a1)
val y = h(new A())

}