Skip to content
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

area:match-types Match type reduction stuck on disjointness test for types of the form 1 | Nothing #20897

Closed
p-pavel opened this issue Jun 30, 2024 · 0 comments · Fixed by #21241
Assignees
Labels
Milestone

Comments

@p-pavel
Copy link

p-pavel commented Jun 30, 2024

Compiler version

3.4.2, 3.3.1

Minimized code

type Disj[A, B] = 
  A match 
    case B => true
    case _       => false

def f(a: Disj[1 | Nothing, 2 | Nothing]): Unit = ()

val t = f(false)

Output

Found:    (false : Boolean)
Required: com.perikov.typelevel.tests.Disj[(1 : Int) | Nothing, (2 : Int) | Nothing]

Note: a match type could not be fully reduced:

  trying to reduce  com.perikov.typelevel.tests.Disj[(1 : Int) | Nothing, (2 : Int) | Nothing]
  failed since selector (1 : Int) | Nothing
  does not match  case (2 : Int) | Nothing => (true : Boolean)
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining case

    case _ => (false : Boolean)

Expectation

Disj should reduce to false.

Types like this arise from Tuple.Union[(1,2,3)]

@p-pavel p-pavel added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels Jun 30, 2024
@Gedochao Gedochao added area:match-types area:union-types Issues tied to union types. and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels Jul 3, 2024
sjrd added a commit to dotty-staging/dotty that referenced this issue Jul 22, 2024
…pec.

`derivesFrom` normally returns `false` when the receiver is
`Nothing` or `Null`. However, it returns `true` if the right-hand-
side happens to be exactly the same class. For the purpose of
computing `provablyDisjoint`, we have to explicitly exclude those.

(Note that the spec text per se only explicitly specifies
`Nothing ⋔ Nothing`, not `Null ⋔ Null`, but that's because the spec
text punts on the `Null` issue. The intent of `provablyDisjoint`
is that there is no *non-null* value belonging to both types.)
@sjrd sjrd self-assigned this Jul 22, 2024
sjrd added a commit to dotty-staging/dotty that referenced this issue Jul 22, 2024
`derivesFrom`, used in `provablyDisjointClasses`, normally returns
`false` when the receiver is `Nothing`. However, it returns `true`
if the right-hand-side happens to be exactly `Nothing` as well.
For the purpose of computing `provablyDisjoint`, that is not what
we want.

The root issue was that we let the previous algorithm handle
`Nothing` like a class type, which it *is* in dotc but not in the
spec. That led to this mistake.

`AnyKind` suffers a similar issue, but already had special-cases in
various places to mitigate it.

Instead of adding a new special-case for `Nothing` inside
`provablyDisjointClasses`, we address the root issue. Now we deal
with `Nothing` and `AnyKind` early, before trying any of the code
paths that handle (real) class types.
@sjrd sjrd linked a pull request Jul 22, 2024 that will close this issue
sjrd added a commit that referenced this issue Jul 23, 2024
`derivesFrom`, used in `provablyDisjointClasses`, normally returns
`false` when the receiver is `Nothing`. However, it returns `true` if
the right-hand-side happens to be exactly `Nothing` as well. For the
purpose of computing `provablyDisjoint`, that is not what we want.

The root issue was that we let the previous algorithm handle `Nothing`
like a class type, which it *is* in dotc but not in the spec. That led
to this mistake.

`AnyKind` suffers a similar issue, but already had special-cases in
various places to mitigate it.

Instead of adding a new special-case for `Nothing` inside
`provablyDisjointClasses`, we address the root issue. Now we deal with
`Nothing` and `AnyKind` early, before trying any of the code paths that
handle (real) class types.
WojciechMazur pushed a commit that referenced this issue Aug 27, 2024
`derivesFrom`, used in `provablyDisjointClasses`, normally returns
`false` when the receiver is `Nothing`. However, it returns `true`
if the right-hand-side happens to be exactly `Nothing` as well.
For the purpose of computing `provablyDisjoint`, that is not what
we want.

The root issue was that we let the previous algorithm handle
`Nothing` like a class type, which it *is* in dotc but not in the
spec. That led to this mistake.

`AnyKind` suffers a similar issue, but already had special-cases in
various places to mitigate it.

Instead of adding a new special-case for `Nothing` inside
`provablyDisjointClasses`, we address the root issue. Now we deal
with `Nothing` and `AnyKind` early, before trying any of the code
paths that handle (real) class types.

[Cherry-picked b7846c4]
WojciechMazur added a commit that referenced this issue Aug 27, 2024
#21458)

Backports #21241 to the 3.5.2 branch.

PR submitted by the release tooling.
[skip ci]
@WojciechMazur WojciechMazur added this to the 3.5.2 milestone Oct 8, 2024
WojciechMazur added a commit that referenced this issue Dec 2, 2024
`derivesFrom`, used in `provablyDisjointClasses`, normally returns
`false` when the receiver is `Nothing`. However, it returns `true`
if the right-hand-side happens to be exactly `Nothing` as well.
For the purpose of computing `provablyDisjoint`, that is not what
we want.

The root issue was that we let the previous algorithm handle
`Nothing` like a class type, which it *is* in dotc but not in the
spec. That led to this mistake.

`AnyKind` suffers a similar issue, but already had special-cases in
various places to mitigate it.

Instead of adding a new special-case for `Nothing` inside
`provablyDisjointClasses`, we address the root issue. Now we deal
with `Nothing` and `AnyKind` early, before trying any of the code
paths that handle (real) class types.

[Cherry-picked b7846c4][modified]
WojciechMazur added a commit that referenced this issue Dec 3, 2024
…22077)

Backports #21241 to the 3.3.5.

PR submitted by the release tooling.
[skip ci]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging a pull request may close this issue.

4 participants