Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
s5bug opened this issue Apr 16, 2025 · 0 comments

Comments

@s5bug
Copy link

s5bug commented Apr 16, 2025

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.

@s5bug s5bug added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Apr 16, 2025
@Gedochao Gedochao added area:typer area:match-types and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Apr 24, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants