Open
Description
Compiler version
3.6.4
3.7.1-RC1-bin-20250415-06886b0-NIGHTLY
Minimized code
type Foo[X <: Int] <: AnyKind = X match {
case 0 => Any
}
case class Bar[X <: Int, F[_ <: Foo[X]], G <: Foo[X]](fg: F[G])
type Qux[F[_]] = Bar[0, F, Nothing]
Actual use case
import scala.compiletime.ops.int.*
type ES[X <: Int] <: Int = X match {
case -2 => -1
case -1 => 0
case _ => S[X]
}
type K[X <: Int] <: AnyKind = X match {
case -1 => Nothing
case 0 => Any
case S[a] => a match {
case 0 => [_ <: K[0]] =>> Any
case S[b] => [_ <: K[a]] =>> Any
}
}
type Unfix[L <: Int, F[_ <: K[ES[L]], _ <: K[L]] <: Any, I <: K[L]] <: Any = L match {
case -1 => F[KFix[-1, F, I], Nothing]
case 0 => F[[x <: Any] =>> KFix[0, F, x], I]
case S[l] => F[[x <: K[L]] =>> KFix[L, F, x], I]
}
final case class KFix[L <: Int, F[_ <: K[ES[L]], _ <: K[L]] <: Any, I <: K[L]](unfix: Unfix[L, F, I])
type Fix[F[_]] = KFix[-1, [x, _] =>> F[x], Nothing]
type HFix[F[_[_], _], I] = KFix[0, F, I]
Output
-- [E057] Type Mismatch Error: -------------------------------------------------
1 |type Qux[F[_]] = Bar[0, F, Nothing]
| ^
|Type argument F does not conform to upper bound [_ <: Foo[(0 : Int)]] =>> Any
|-----------------------------------------------------------------------------
| Explanation (enabled by `-explain`)
|- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
| I tried to show that
| F
| conforms to
| [_ <: Foo[(0 : Int)]] =>> Any
| but none of the attempts shown below succeeded:
|
| ==> F <: [_ <: Foo[(0 : Int)]] =>> Any
| ==> [_] =>> F[_] <: [_ <: Foo[(0 : Int)]] =>> Any
| ==> type bounds [ <: Foo[(0 : Int)]] <: type bounds []
| ==> Foo[(0 : Int)] <: Any = false
| ==> [_] =>> Any <: [_ <: Foo[(0 : Int)]] =>> Any
| ==> type bounds [ <: Foo[(0 : Int)]] <: type bounds []
| ==> Foo[(0 : Int)] <: Any = false
|
| The tests were made under the empty constraint
-----------------------------------------------------------------------------
1 error found
Expectation
One can summon[Foo[0] =:= Any]
, so Foo[0] <: Any
should test true.