Skip to content

Commit

Permalink
Demonstrate more potential unsoundness with a CCE reproducer.
Browse files Browse the repository at this point in the history
This additional test demonstrates that relaxing the `isConcrete`
in a particular way around `AndType`s would also cause unsoundness.

This justifies new failures in the Open Community Build.
  • Loading branch information
sjrd committed Dec 8, 2023
1 parent c2df8f3 commit fa6c198
Show file tree
Hide file tree
Showing 3 changed files with 111 additions and 0 deletions.
3 changes: 3 additions & 0 deletions compiler/src/dotty/tools/dotc/core/TypeComparer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3346,6 +3346,9 @@ class TrackingTypeComparer(initctx: Context) extends TypeComparer(initctx) {
* upper bound of an abstract type.
*
* See notably neg/wildcard-match.scala for examples of this.
*
* See neg/i13780.scala and neg/i13780-1.scala for ClassCastException
* reproducers if we disable this check.
*/

def followEverythingConcrete(tp: Type): Type =
Expand Down
39 changes: 39 additions & 0 deletions tests/neg/i13780-1.check
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
-- [E007] Type Mismatch Error: tests/neg/i13780-1.scala:38:24 ----------------------------------------------------------
38 | case x: (h *: t) => x.head // error
| ^^^^^^
| Found: Tuple.Head[VS & h *: t]
| Required: h
|
| where: VS is a type in method foo with bounds <: Tuple
| h is a type in method foo with bounds
| t is a type in method foo with bounds <: Tuple
|
|
| Note: a match type could not be fully reduced:
|
| trying to reduce Tuple.Head[VS & h *: t]
| failed since selector VS & h *: t
| does not uniquely determine parameter x in
| case x *: _ => x
| The computed bounds for the parameter are:
| x <: h
| Note that implicit conversions were not tried because the result of an implicit conversion
| must be more specific than h
|
| longer explanation available when compiling with `-explain`
-- [E007] Type Mismatch Error: tests/neg/i13780-1.scala:52:31 ----------------------------------------------------------
52 | def unpair: SelectH[Y & W] = "" // error
| ^^
| Found: ("" : String)
| Required: SelectH[A.this.Y & A.this.W]
|
| Note: a match type could not be fully reduced:
|
| trying to reduce SelectH[A.this.Y & A.this.W]
| failed since selector A.this.Y & A.this.W
| does not uniquely determine parameter h in
| case h *: _ => h
| The computed bounds for the parameter are:
| h
|
| longer explanation available when compiling with `-explain`
69 changes: 69 additions & 0 deletions tests/neg/i13780-1.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,69 @@
/* It is tempting to relax the `isConcrete` test of match types for `AndType`
* in the following way:
*
* (isConcrete(tp.tp1) || !tp.tp1.derivesFrom(targetClass)) && (... same for tp.tp2)
*
* but the test in this file shows that this would be unsound.
*
* If we did relax the rule, it would help usages of match types applied to the
* singleton type of term pattern match scrutinees. For example:
*
* def foo[VS <: Tuple](x: VS): SelectH[VS] = x match
* case x: (h *: t) => x.head
*
* The type of `x` in the branch body is `(VS & (h *: t))`. The result of
* `x.head` is therefore a `Tuple.Head[VS & (h *: t)]`, which does not reduce
* according to the current rules, but would reduce to `h` with the relaxed
* rule.
*
* Note that the code can be fixed with an explicit type argument to `.head`:
*
* def foo[VS <: Tuple](x: VS): SelectH[VS] = x match
* case x: (h *: t) => x.head[h *: t]
*
* So it *seems* like it would be fine to relax the rule, based on the insight
* that `VS` in `Tuple.Head[VS & (h *: t)]` does not contribute anything to the
* computed type capture in `Tuple.Head`.
*
* The test is this file demonstrates that relaxing the rule can cause
* unsoundness. So don't do it.
*/

type SelectH[VS <: Tuple] = VS match
case h *: ? => h

// The original example found in the fingo/spata library
object ExampleFromSpata:
def foo[VS <: Tuple](x: VS): SelectH[VS] = x match
case x: (h *: t) => x.head // error

def bar[VS <: Tuple](x: VS): SelectH[VS] = x match
case x: (h *: t) => x.head[h *: t] // ok
end ExampleFromSpata

trait Z {
type Y <: Tuple
type W <: Tuple
def unpair: SelectH[Y & W]
}

class A extends Z {
type Y = Tuple2[Any, Any]
def unpair: SelectH[Y & W] = "" // error
def any: Any = unpair
}

class B extends A { this: Z =>
type W = Tuple2[Int, Int]
def int: Int = unpair
}

class C extends A { this: Z =>
type W = Tuple2[String, String]
def string: String = unpair
}

object Main {
def main(args: Array[String]): Unit =
println((new B).int + 1) // would give ClassCastException
}

0 comments on commit fa6c198

Please sign in to comment.