Skip to content

Bounds checking on AnyKind match type forgets parallel information about scrutinee #23010

Open
@s5bug

Description

@s5bug

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.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions