Compilation failure under -Ycheck:typer involving type aliases and implicit search

[smarter]

Compiler version

3.2.1

Minimized code

The following code adapted from #16471 fails -Ycheck:typer (as well as -Yno-deep-subtypes)

object tag {
  type Tag[U]
  type @@[+T, U] = (T & Tag[U]) | Null
}
import tag.*

trait FromInput[Val]
object FromInput {
  trait CoercedScalaResult
  implicit def optionInput[T](implicit ev: FromInput[T]): FromInput[Option[T]]               = ???
  implicit def coercedScalaInput[T]:                      FromInput[T @@ CoercedScalaResult] = ???
}
import FromInput.CoercedScalaResult

object schema {
  trait InputType[+T] // This is critical! Making InputType invariant allows to compile

  case class OptionInputType[T](ofType: InputType[T]) extends InputType[Option[T]]
  class ScalarType[T] extends InputType[T @@ CoercedScalaResult]
  implicit val IntType: ScalarType[Int] = ???
}
export schema.*

trait WithoutInputTypeTags[T] { type Res }
object WithoutInputTypeTags   {
  implicit def coercedArgTpe[T]:    WithoutInputTypeTags[T @@ CoercedScalaResult] { type Res = T }                 = ???
  implicit def coercedOptArgTpe[T]: WithoutInputTypeTags[Option[T @@ CoercedScalaResult]] { type Res = Option[T] } = ???
}

trait Argument[T]
object Argument {
  def apply[T](argumentType: InputType[T])(implicit
      fromInput:     FromInput[T],
      res:           WithoutInputTypeTags[T]
  ): Argument[res.Res] = ???
}

@main def Test = {
  // -Ycheck:typer failure
  val optionalArgument = Argument(
    argumentType = OptionInputType(IntType),
  )
  // ok
  // val optionalArgument2 = Argument[Option[Int @@ CoercedScalaResult]](
  //   argumentType = OptionInputType(IntType),
  // )
}

Output

*** error while checking tests/pos-deep-subtype/i16471.scala after phase typer ***
java.lang.AssertionError: assertion failed: Found:    (IntType : => (schema.IntType : schema.ScalarType[Int]))
Required: schema.InputType[Nothing & tag.Tag[FromInput.CoercedScalaResult] &
  tag.Tag[FromInput.CoercedScalaResult] | Null]
found: ??
expected: ??
tree = IntType while running Ycheck on tests/pos-deep-subtype/i16471.scala
exception occurred while compiling tests/pos-deep-subtype/i16471.scala
java.lang.AssertionError: assertion failed: Found:    (IntType : => (schema.IntType : schema.ScalarType[Int]))
Required: schema.InputType[Nothing & tag.Tag[FromInput.CoercedScalaResult] &
  tag.Tag[FromInput.CoercedScalaResult] | Null]
found: ??
expected: ??
tree = IntType while compiling tests/pos-deep-subtype/i16471.scala
Exception in thread "main" java.lang.AssertionError: assertion failed: Found:    (IntType : => (schema.IntType : schema.ScalarType[Int]))
Required: schema.InputType[Nothing & tag.Tag[FromInput.CoercedScalaResult] &
  tag.Tag[FromInput.CoercedScalaResult] | Null]
found: ??
expected: ??
tree = IntType
        at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:8)
        at dotty.tools.dotc.transform.TreeChecker$Checker.adapt(TreeChecker.scala:653)
        at dotty.tools.dotc.typer.ProtoTypes$FunProto.typedArg(ProtoTypes.scala:495)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.typedArg(Applications.scala:889)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.typedArg(Applications.scala:889)
        at dotty.tools.dotc.typer.Applications$Application.addTyped$1(Applications.scala:581)
        at dotty.tools.dotc.typer.Applications$Application.matchArgs(Applications.scala:645)
        at dotty.tools.dotc.typer.Applications$Application.init(Applications.scala:484)
        at dotty.tools.dotc.typer.Applications$TypedApply.<init>(Applications.scala:771)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.<init>(Applications.scala:888)
        at dotty.tools.dotc.typer.Applications.ApplyTo(Applications.scala:1115)
        at dotty.tools.dotc.typer.Applications.ApplyTo$(Applications.scala:351)
        at dotty.tools.dotc.typer.Typer.ApplyTo(Typer.scala:121)
        at dotty.tools.dotc.typer.Applications.simpleApply$1(Applications.scala:961)
        at dotty.tools.dotc.typer.Applications.realApply$1$$anonfun$2(Applications.scala:1041)
        at dotty.tools.dotc.typer.Typer.tryEither(Typer.scala:3188)
        at dotty.tools.dotc.typer.Applications.realApply$1(Applications.scala:1052)
        at dotty.tools.dotc.typer.Applications.typedApply(Applications.scala:1090)
        at dotty.tools.dotc.typer.Applications.typedApply$(Applications.scala:351)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedApply(TreeChecker.scala:446)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2914)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2977)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.typedNamedArg(Typer.scala:979)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2920)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2977)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.ProtoTypes$FunProto.$anonfun$7(ProtoTypes.scala:493)
        at dotty.tools.dotc.typer.ProtoTypes$FunProto.cacheTypedArg(ProtoTypes.scala:416)
        at dotty.tools.dotc.typer.ProtoTypes$FunProto.typedArg(ProtoTypes.scala:494)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.typedArg(Applications.scala:889)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.typedArg(Applications.scala:889)
        at dotty.tools.dotc.typer.Applications$Application.addTyped$1(Applications.scala:581)
        at dotty.tools.dotc.typer.Applications$Application.matchArgs(Applications.scala:645)
        at dotty.tools.dotc.typer.Applications$Application.init(Applications.scala:484)
        at dotty.tools.dotc.typer.Applications$TypedApply.<init>(Applications.scala:771)
        at dotty.tools.dotc.typer.Applications$ApplyToUntyped.<init>(Applications.scala:888)
        at dotty.tools.dotc.typer.Applications.ApplyTo(Applications.scala:1115)
        at dotty.tools.dotc.typer.Applications.ApplyTo$(Applications.scala:351)
        at dotty.tools.dotc.typer.Typer.ApplyTo(Typer.scala:121)
        at dotty.tools.dotc.typer.Applications.simpleApply$1(Applications.scala:961)
        at dotty.tools.dotc.typer.Applications.realApply$1$$anonfun$2(Applications.scala:1041)
        at dotty.tools.dotc.typer.Typer.tryEither(Typer.scala:3188)
        at dotty.tools.dotc.typer.Applications.realApply$1(Applications.scala:1052)
        at dotty.tools.dotc.typer.Applications.typedApply(Applications.scala:1090)
        at dotty.tools.dotc.typer.Applications.typedApply$(Applications.scala:351)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedApply(TreeChecker.scala:446)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2914)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2977)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3164)
        at dotty.tools.dotc.typer.Applications.realApply$1(Applications.scala:933)
        at dotty.tools.dotc.typer.Applications.typedApply(Applications.scala:1090)
        at dotty.tools.dotc.typer.Applications.typedApply$(Applications.scala:351)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedApply(TreeChecker.scala:446)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2914)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2977)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3164)
        at dotty.tools.dotc.typer.Typer.typedValDef(Typer.scala:2316)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2887)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2976)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3070)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3120)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:572)
        at dotty.tools.dotc.typer.Typer.typedBlockStats(Typer.scala:1076)
        at dotty.tools.dotc.typer.Typer.typedBlock(Typer.scala:1080)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock$$anonfun$1$$anonfun$1(TreeChecker.scala:554)
        at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:191)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock$$anonfun$1(TreeChecker.scala:554)
        at dotty.tools.dotc.transform.TreeChecker$Checker.withBlock(TreeChecker.scala:219)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedBlock(TreeChecker.scala:554)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2922)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2977)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3164)
        at dotty.tools.dotc.typer.Typer.$anonfun$48(Typer.scala:2372)
        at dotty.tools.dotc.inlines.PrepareInlineable$.dropInlineIfError(PrepareInlineable.scala:249)
        at dotty.tools.dotc.typer.Typer.typedDefDef(Typer.scala:2372)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedDefDef$$anonfun$1(TreeChecker.scala:529)
        at dotty.tools.dotc.transform.TreeChecker$Checker.withDefinedSyms(TreeChecker.scala:191)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedDefDef(TreeChecker.scala:532)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2890)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2976)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3070)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3120)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:572)
        at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:2548)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedClassDef(TreeChecker.scala:507)
        at dotty.tools.dotc.typer.Typer.typedTypeOrClassDef$1(Typer.scala:2902)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:2906)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2976)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3070)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3120)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:572)
        at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:2678)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedPackageDef(TreeChecker.scala:598)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:2947)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:2977)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:342)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3044)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3048)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:325)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3164)
        at dotty.tools.dotc.transform.TreeChecker.check(TreeChecker.scala:143)
        at dotty.tools.dotc.transform.TreeChecker.run(TreeChecker.scala:110)
        at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:324)
        at scala.collection.immutable.List.map(List.scala:246)
        at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:328)
        at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:244)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
        at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1321)
        at dotty.tools.dotc.Run.runPhases$1(Run.scala:260)
        at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:268)
        at dotty.tools.dotc.Run.compileUnits$$anonfun$adapted$1(Run.scala:277)
        at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:68)
        at dotty.tools.dotc.Run.compileUnits(Run.scala:277)
        at dotty.tools.dotc.Run.compileSources(Run.scala:195)
        at dotty.tools.dotc.Run.compile(Run.scala:179)
        at dotty.tools.dotc.Driver.doCompile(Driver.scala:35)
        at dotty.tools.dotc.Driver.process(Driver.scala:195)
        at dotty.tools.dotc.Driver.process(Driver.scala:163)
        at dotty.tools.dotc.Driver.process(Driver.scala:175)
        at dotty.tools.dotc.Driver.main(Driver.scala:205)
        at dotty.tools.dotc.Main.main(Main.scala)

Expectation

If -Ycheck:typer fails, it means there's a bug in the typechecker somewhere that needs to be fixed.

[SethTisue]

It's hard to be sure if this is truly minimal, but Dale & and I found this minimization and haven't been able to reduce it further.

trait Foo
trait Bar[A] { type Res }
class Box[B](value: B)
trait Opt[+C]

abstract class Test:
  def meth[D](box: Box[T], bar1: Bar[T], bar2: Bar[T]): bar2.Res

  def bar[E]: Bar[Opt[E & Foo]] { type Res = E }
  val int:      Opt[Int & Foo]

  def test: Int = meth(Box(int), bar, bar)

We're groveling through typer logs trying to figure out how the bad Nothing arises. It seems that the mutual dependence of the type parameters on the two Bars confuses typer (see also #16311 (comment)), and we end up with mutually recursive constraints E1 >: E2 & Foo and E2 >: E1 & Foo — and then E2 ends up as Nothing.

(There are some doubled Foos, as in Foo & Foo, and it's unclear whether that's contributing — probably it's unimportant.)