Skip to content

Commit

Permalink
Relax avoidance checks more for match type reduction
Browse files Browse the repository at this point in the history
TypeParamRefs in match types do not have a corresponding TypeVar so they get
assigned level Int.MaxValue by default, this means they can refer to variables
at any level, but to avoid a crash in i14921 we also need the reverse
direction (they can appear in the bounds of variables of any level), both
direction should be safe because these constraints only exist during match type
reduction (see `MatchType#reduced`).

Fixes #14921.
  • Loading branch information
smarter committed Apr 26, 2022
1 parent 0761c50 commit 7533217
Show file tree
Hide file tree
Showing 4 changed files with 55 additions and 19 deletions.
27 changes: 15 additions & 12 deletions compiler/src/dotty/tools/dotc/core/ConstraintHandling.scala
Expand Up @@ -81,16 +81,26 @@ trait ConstraintHandling {
assert(homogenizeArgs == false)
assert(comparedTypeLambdas == Set.empty)

def nestingLevel(param: TypeParamRef) = constraint.typeVarOfParam(param) match
def nestingLevel(param: TypeParamRef)(using Context) = constraint.typeVarOfParam(param) match
case tv: TypeVar => tv.nestingLevel
case _ => Int.MaxValue
case _ =>
// This should only happen when reducing match types or in uncommitable TyperStates
// (as asserted in ProtoTypes.constrained) and is special-cased in `levelOK` below.
Int.MaxValue

/** Is `level` <= `maxLevel` or legal in the current context? */
def levelOK(level: Int, maxLevel: Int)(using Context): Boolean =
level <= maxLevel ||
ctx.isAfterTyper || !ctx.typerState.isCommittable || // Leaks in these cases shouldn't break soundness
level == Int.MaxValue // See `nestingLevel` above.

/** If `param` is nested deeper than `maxLevel`, try to instantiate it to a
* fresh type variable of level `maxLevel` and return the new variable.
* If this isn't possible, throw a TypeError.
*/
def atLevel(maxLevel: Int, param: TypeParamRef)(using Context): TypeParamRef =
if nestingLevel(param) <= maxLevel then return param
if levelOK(nestingLevel(param), maxLevel) then
return param
LevelAvoidMap(0, maxLevel)(param) match
case freshVar: TypeVar => freshVar.origin
case _ => throw new TypeError(
Expand Down Expand Up @@ -129,18 +139,12 @@ trait ConstraintHandling {

/** An approximating map that prevents types nested deeper than maxLevel as
* well as WildcardTypes from leaking into the constraint.
* Note that level-checking is turned off after typer and in uncommitable
* TyperState since these leaks should be safe.
*/
class LevelAvoidMap(topLevelVariance: Int, maxLevel: Int)(using Context) extends TypeOps.AvoidMap:
variance = topLevelVariance

/** Are we allowed to refer to types of the given `level`? */
private def levelOK(level: Int): Boolean =
level <= maxLevel || ctx.isAfterTyper || !ctx.typerState.isCommittable

def toAvoid(tp: NamedType): Boolean =
tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel)
tp.prefix == NoPrefix && !tp.symbol.isStatic && !levelOK(tp.symbol.nestingLevel, maxLevel)

/** Return a (possibly fresh) type variable of a level no greater than `maxLevel` which is:
* - lower-bounded by `tp` if variance >= 0
Expand Down Expand Up @@ -185,7 +189,7 @@ trait ConstraintHandling {
end legalVar

override def apply(tp: Type): Type = tp match
case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel) =>
case tp: TypeVar if !tp.isInstantiated && !levelOK(tp.nestingLevel, maxLevel) =>
legalVar(tp)
// TypeParamRef can occur in tl bounds
case tp: TypeParamRef =>
Expand Down Expand Up @@ -431,7 +435,6 @@ trait ConstraintHandling {
final def approximation(param: TypeParamRef, fromBelow: Boolean)(using Context): Type =
constraint.entry(param) match
case entry: TypeBounds =>
val maxLevel = nestingLevel(param)
val useLowerBound = fromBelow || param.occursIn(entry.hi)
val inst = if useLowerBound then fullLowerBound(param) else fullUpperBound(param)
typr.println(s"approx ${param.show}, from below = $fromBelow, inst = ${inst.show}")
Expand Down
16 changes: 9 additions & 7 deletions compiler/src/dotty/tools/dotc/typer/Inferencing.scala
Expand Up @@ -637,13 +637,15 @@ trait Inferencing { this: Typer =>
else if v.intValue != 0 then
typr.println(i"interpolate $tvar in $state in $tree: $tp, fromBelow = ${v.intValue == 1}, $constraint")
toInstantiate += ((tvar, v.intValue == 1))
else if tvar.nestingLevel > ctx.nestingLevel then
// Invariant: a type variable of level N can only appear
// in the type of a tree whose enclosing scope is level <= N.
typr.println(i"instantiate nonvariant $tvar of level ${tvar.nestingLevel} to a type variable of level <= ${ctx.nestingLevel}, $constraint")
comparing(_.atLevel(ctx.nestingLevel, tvar.origin))
else
typr.println(i"no interpolation for nonvariant $tvar in $state")
else comparing(cmp =>
if !cmp.levelOK(tvar.nestingLevel, ctx.nestingLevel) then
// Invariant: The type of a tree whose enclosing scope is level
// N only contains type variables of level <= N.
typr.println(i"instantiate nonvariant $tvar of level ${tvar.nestingLevel} to a type variable of level <= ${ctx.nestingLevel}, $constraint")
cmp.atLevel(ctx.nestingLevel, tvar.origin)
else
typr.println(i"no interpolation for nonvariant $tvar in $state")
)

/** Instantiate all type variables in `buf` in the indicated directions.
* If a type variable A is instantiated from below, and there is another
Expand Down
28 changes: 28 additions & 0 deletions tests/pos/i14921/A_1.scala
@@ -0,0 +1,28 @@
import scala.compiletime.ops.int.*

final class Label (val getLabel: String)

trait ShapelessPolyfill {

type Represented[R] = R match {
case IndexedSeq[a] => a
}

type TupleSized[R, A, N <: Int] <: Tuple = N match {
case 0 => EmptyTuple
case S[n] => A *: TupleSized[R, A, n]
}

extension [R, A, N <: Int] (s: TupleSized[R, A, N]) {
def unsized: IndexedSeq[A] = s.productIterator.toIndexedSeq.asInstanceOf[IndexedSeq[A]]
}

type Nat = Int

type Sized[Repr, L <: Nat] = TupleSized[Repr, Represented[Repr], L]

object Sized {
def apply[A](a1: A): Sized[IndexedSeq[A], 1] = Tuple1(a1)
}
}
object poly extends ShapelessPolyfill
3 changes: 3 additions & 0 deletions tests/pos/i14921/B_2.scala
@@ -0,0 +1,3 @@
import poly.*

def failing: Tuple1[Label] = Sized(new Label("foo"))

0 comments on commit 7533217

Please sign in to comment.