Specifying weaker Aux type bound does not cause compile error

Question

Here is an example:

sealed trait Type
object Type {
    case object Type1 extends Type
    case object Type2 extends Type
}

sealed trait TypedTrait {
    type Tpe <: Type
}

object TypedTrait {
    type Aux[T <: Type] = TypedTrait{ type Tpe = T }
}

sealed trait Test {
    //Bounded with TypedTrait.Aux[Type.Type1.type]
    type TptTrait <: TypedTrait.Aux[Type.Type1.type]
}

object Test {
    //No TypedTrait.Aux[Type.Type1.type] type bound
    type Aux[T <: TypedTrait] = Test { type TptTrait = T } //compiles fine, but I expected error
}

The example compiles for both Scala 2 and Scala 3, but it does not seem to make sense. Why does it compile?

Answer 1

While this compiles you cannot instantiate this type with a bad type:

class Wololo extends TypedTrait { type Tpe = Type.Type2.type } // bad type
val ax: Test.Aux[Wololo] = new Test { type TptTrait = Wololo }

This fails with

cmd1.sc:24: incompatible type in overriding
type TptTrait <: ammonite.$sess.cmd1.TypedTrait.Aux[ammonite.$sess.cmd1.Type.Type1.type] (defined in trait Test);
 found   : ammonite.$sess.cmd1.Wololo
 required:  <: ammonite.$sess.cmd1.TypedTrait.Aux[ammonite.$sess.cmd1.Type.Type1.type]
    (which expands to)   <: ammonite.$sess.cmd1.TypedTrait{type Tpe = ammonite.$sess.cmd1.Type.Type1.type}
val ax: Test.Aux[Wololo] = new Test { type TptTrait = Wololo }
                                           ^
Compilation Failed

Meanwhile

class Wololo extends TypedTrait { type Tpe = Type.Type1.type } // good type
val ax: Test.Aux[Wololo] = new Test { type TptTrait = Wololo }

succeeds with

ax: Test.Aux[Wololo] = ammonite.$sess.cmd1$$anon$1@78de58ea

So we can conclude that the bounds here combines, but aren't failing until you actually try to create an instance that would violate the constraints. Probably this isn't triggering any of cases where spec would let it fail immediately (after all you can create a valid instance!), so the check/proof is deferred until you try to create an actual instance.

(I evaluated it in Ammonite as a whole block because of sealed traits)

@ {
  sealed trait Type
  object Type {
      case object Type1 extends Type
      case object Type2 extends Type
  }

  sealed trait TypedTrait {
      type Tpe <: Type
  }

  object TypedTrait {
      type Aux[T <: Type] = TypedTrait{ type Tpe = T }
  }

  sealed trait Test {
      //Bounded with TypedTrait.Aux[Type.Type1.type]
      type TptTrait <: TypedTrait.Aux[Type.Type1.type]
  }

  object Test {
      type Aux[T <: TypedTrait] = Test { type TptTrait = T }
  }
  class Wololo extends TypedTrait { type Tpe = Type.Type1.type }
  val ax: Test.Aux[Wololo] = new Test { type TptTrait = Wololo }
  }
defined trait Type
defined object Type
defined trait TypedTrait
defined object TypedTrait
defined trait Test
defined object Test
defined class Wololo
ax: Test.Aux[Wololo] = ammonite.$sess.cmd1$$anon$1@78de58ea