Nothing and dependent types interplay: assertion failed in the compiler

[p-pavel]

Compiler version

3.1.2

Minimized code

trait Tst:
  val a: Int

trait Q[A <: Tst]:
  def mk(a: A): a.a.type = a.a

object q extends Q[Nothing]

Output (click arrow to expand)

scalac: Error: assertion failed
java.lang.AssertionError: assertion failed
	at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:11)
	at dotty.tools.dotc.core.Types$MethodType.<init>(Types.scala:3705)
	at dotty.tools.dotc.core.Types$CachedMethodType.<init>(Types.scala:3725)
	at dotty.tools.dotc.core.Types$MethodTypeCompanion.apply(Types.scala:3796)
	at dotty.tools.dotc.core.Types$MethodTypeCompanion.apply(Types.scala:3795)
	at dotty.tools.dotc.core.Types$LambdaType.newLikeThis(Types.scala:3478)
	at dotty.tools.dotc.core.Types$LambdaType.newLikeThis$(Types.scala:3411)
	at dotty.tools.dotc.core.Types$MethodOrPoly.newLikeThis(Types.scala:3491)
	at dotty.tools.dotc.core.Types$LambdaType.derivedLambdaType(Types.scala:3468)
	at dotty.tools.dotc.core.Types$LambdaType.derivedLambdaType$(Types.scala:3411)
	at dotty.tools.dotc.core.Types$MethodOrPoly.derivedLambdaType(Types.scala:3491)
	at dotty.tools.dotc.core.TypeErasure.dotty$tools$dotc$core$TypeErasure$$apply(TypeErasure.scala:642)
	at dotty.tools.dotc.core.TypeErasure.eraseInfo(TypeErasure.scala:717)
	at dotty.tools.dotc.core.TypeErasure$.transformInfo(TypeErasure.scala:244)
	at dotty.tools.backend.jvm.BCodeHelpers.dotty$tools$backend$jvm$BCodeHelpers$$getStaticForwarderGenericSignature(BCodeHelpers.scala:942)
	at dotty.tools.backend.jvm.BCodeHelpers$BCForwardersGen.addForwarder(BCodeHelpers.scala:530)
	at dotty.tools.backend.jvm.BCodeHelpers$BCForwardersGen.addForwarders$$anonfun$3(BCodeHelpers.scala:610)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
	at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
	at scala.collection.immutable.List.foreach(List.scala:333)
	at dotty.tools.backend.jvm.BCodeHelpers$BCForwardersGen.addForwarders(BCodeHelpers.scala:612)
	at dotty.tools.backend.jvm.BCodeHelpers$BCForwardersGen.addForwarders$(BCodeHelpers.scala:506)
	at dotty.tools.backend.jvm.BCodeHelpers$JCommonBuilder.addForwarders(BCodeHelpers.scala:670)
	at dotty.tools.backend.jvm.BCodeHelpers$JMirrorBuilder.genMirrorClass(BCodeHelpers.scala:718)
	at dotty.tools.backend.jvm.GenBCodePipeline$Worker1.visit(GenBCode.scala:250)
	at dotty.tools.backend.jvm.GenBCodePipeline$Worker1.run(GenBCode.scala:224)
	at dotty.tools.backend.jvm.GenBCodePipeline.buildAndSendToDisk(GenBCode.scala:559)
	at dotty.tools.backend.jvm.GenBCodePipeline.run(GenBCode.scala:525)
	at dotty.tools.backend.jvm.GenBCode.run(GenBCode.scala:63)
	at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:308)
	at scala.collection.immutable.List.map(List.scala:246)
	at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:309)
	at dotty.tools.backend.jvm.GenBCode.runOn(GenBCode.scala:71)
	at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:259)
	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:1328)
	at dotty.tools.dotc.Run.runPhases$1(Run.scala:270)
	at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:278)
	at scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.scala:18)
	at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:68)
	at dotty.tools.dotc.Run.compileUnits(Run.scala:287)
	at dotty.tools.dotc.Run.compileSources(Run.scala:220)
	at dotty.tools.dotc.Run.compile(Run.scala:204)
	at dotty.tools.dotc.Driver.doCompile(Driver.scala:39)
	at dotty.tools.xsbt.CompilerBridgeDriver.run(CompilerBridgeDriver.java:88)
	at dotty.tools.xsbt.CompilerBridge.run(CompilerBridge.java:22)
	at sbt.internal.inc.AnalyzingCompiler.compile(AnalyzingCompiler.scala:91)

Additional info

There's a general problem with handling paths when type is instantiated as Nothing. Here's the example I started from:

trait WithPath:
  type A

trait Proto:
  type A <: WithPath
  def func(a: A): a.A

object Impl extends Proto:
  type A = Nothing
  def func(a: A) = a

This can't be typed (but I think it should because surely Nothing <: WithPath).

[odersky]

This can't be typed (but I think it should because surely Nothing <: WithPath).

Nothing does not have members, so it can't be typed. The error message is quite clear about this:

-- Error: i15377.scala:18:6 ----------------------------------------------------
18 |  def func(a: A) = a
   |  ^^^^^^^^^^^^^^^^^^
   |  a.A is not defined in inferred type a.A

The crash in the original code comes from the fact that the same problem happens in a forwarder generated by the backend, when that check is not done.

[p-pavel]

Nothing does not have members, so it can't be typed. The error message is quite clear about this:

Intersting. So infamous Liskov's substitution principle does not hold in case of Nothing.

Maybe we need something like "absurd pattern" in this case? Having argument of type Nothing let us provide no implementation?

to me Impl.func seems absolutely valid.

[odersky]

Intersting. So infamous Liskov's substitution principle does not hold in case of Nothing.

Correct. The LSP holds for values, but there is no value of type Nothing.

[p-pavel]

Correct. The LSP holds for values, but there is no value of type Nothing.

So does it mean that if anything holds for type T it holds for ANY value of type Nothing? Ok, I have to do my homework and read DOT calculus thoroughly.

The motivation for the original example was something like this btw:

trait Category:
  type IsObject <: {type T}
  type Arrow[_,_]
  def id(a: IsObject): Arrow[a.T, a.T]

object EmptyCategory extends Category:
  type IsObject = Nothing
  //compiles
  def id(a: Nothing): Nothing = a
  // this version breaks
  // def id(a: Nothing) = a

This resolves my request for 'absurd pattern': just overriding return type to Nothing solves the issue