! (Nothing <:< refinement type) for members

[scabug]

After reading the specs, I'm convinced I should have:

TPlus { type T <: Nothing } <:< TPlus { type T <: TPlus {type H <: A} } 

simply because

Nothing <:< TPlus {type H <: A}

but the former does not hold while the latter does, as you can see below.

package shapelessexperiments

sealed trait Coproduct

sealed trait TPlus extends Coproduct {
  type H
  type T <: Coproduct
}

object Bug {
  sealed trait Term
  case class A() extends Term
  case class B() extends Term
  case class C(x: Int) extends Term

  implicitly[TPlus { type T <: Nothing } <:< TPlus { type T <: TPlus } ]
  implicitly[TPlus { type T <: Nothing } <:< TPlus { type T <: TPlus {type H <: A} } ] //FAILS!
  implicitly[Nothing <:< TPlus {type H <: A} ] //But it should only recurse on this, which succeeds!
  implicitly[TPlus { type T <: TPlus {type H <: Nothing} } <:< TPlus { type T <: TPlus {type H <: A} } ]

  implicitly[TPlus { type H <: A; type T <: TPlus { type H <: Nothing } } <:< TPlus { type H <: A; type T <: TPlus { type H <: B } }]
}

At the very least, dotty agrees with me.

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-8678?orig=1
Reporter: @Blaisorblade
Affected Versions: 2.11.1

[Blaisorblade]

Unlikely to be fixed in Scala 2.

[milessabin]

I'd like to take a look at this.