Skip to content

Error in -Ycheck:typer when refining String on StringOps defs #17465

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

Closed
timotheeandres opened this issue May 11, 2023 · 4 comments · Fixed by #18213
Closed

Error in -Ycheck:typer when refining String on StringOps defs #17465

timotheeandres opened this issue May 11, 2023 · 4 comments · Fixed by #18213
Labels
area:typer itype:bug Spree Suitable for a future Spree
Milestone

Comments

@timotheeandres
Copy link
Contributor

timotheeandres commented May 11, 2023

Compiler version

3.3.0-RC4

Minimized code

Compile this code with the -Ycheck:typer flag.

import reflect.Selectable.reflectiveSelectable

trait A[T](x: T{ def *(y: Int): T }):
  def f: T = x * 2

class B extends A("Hello")

Edit: further minimization (thanks to @nicolasstucki):

import reflect.Selectable.reflectiveSelectable
def f[T](x: T{ def *(y: Int): T }): T = x * 2
def test = f[scala.collection.StringOps | String]("Hello")

Output

checking a.scala after phase typer

  exception while retyping new A[scala.collection.StringOps | String](augmentString("Hello")) of class Apply # -1

  An unhandled exception was thrown in the compiler.
  Please file a crash report here:
  https://github.com/lampepfl/dotty/issues/new/choose

     while compiling: a.scala
        during phase: typer
                mode: Mode(ImplicitsEnabled)
     library version: version 2.13.10
    compiler version: version 3.3.1-RC1-bin-SNAPSHOT-nonbootstrapped-git-b3643ee
            settings: -Ycheck List(typer) -classpath C:\Users\Tim\AppData\Local\Coursier\Cache\v1\https\repo1.maven.org\maven2\org\scala-lang\scala-library\2.13.10\scala-library-2.13.10.jar;D:\Bureau\dotty\library\..\out\bootstrap\scala3-library-bootstrapped\scala-3.3.1-RC1-bin-SNAPSHOT-nonbootstrapped\scala3-library_3-3.3.1-RC1-bin-SNAPSHOT.jar

                tree: PackageDef(object <empty>)
       tree position: a.scala:1:0
           tree type: <empty>.type
              symbol: package <empty>
   symbol definition: final lazy module object <empty>: <empty> (a Symbol)
      symbol package: <root>
       symbol owners:
           call site: constructor B in class B in module class <empty>

  == Source file context for tree position ==

-- Error: a.scala:1:0 --------------------------------------------------------------------------------------------------
1 |import reflect.Selectable.reflectiveSelectable
  |^

2 |trait A[T](x: T{ def *(y: Int): T }):
3 |  def f: T = x * 2
4 |class B extends A("Hello")
*** error while checking a.scala after phase typer ***
Exception in thread "main" java.lang.AssertionError: assertion failed: Types differ
Original type : (x: (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}):
  A[scala.collection.StringOps | String]
After checking: (x: (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}):
  A[scala.collection.StringOps | String]
Original tree : new A[scala.collection.StringOps | String]
After checking: new A[scala.collection.StringOps | String]
Why different :
             Subtype trace:
   A[scala.collection.StringOps | String]  <:  (x: (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}):
    ==> (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String} in frozen constraint
      ==> (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  scala.collection.StringOps | String in frozen constraint
        ==> (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  scala.collection.StringOps | String in frozen constraint
          ==> (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  scala.collection.StringOps in frozen constraint
            ==> lub(scala.collection.StringOps, <notype>, canConstrain=false, isSoft=true)
            <== lub(scala.collection.StringOps, <notype>, canConstrain=false, isSoft=true) = <notype>
          <== (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  scala.collection.StringOps in frozen constraint = false
          ==> (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  String in frozen constraint
            ==> lub(<notype>, String, canConstrain=false, isSoft=true)
            <== lub(<notype>, String, canConstrain=false, isSoft=true) = <notype>
          <== (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  String in frozen constraint = false
        <== (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  scala.collection.StringOps | String in frozen constraint = false
      <== (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  scala.collection.StringOps | String in frozen constraint = false
    <== (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}  <:  (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String} in frozen constraint = false
   A[scala.collection.StringOps | String] = false: (scala.collection.StringOps | String){def *(y: Int): scala.collection.StringOps | String}):
        at scala.runtime.Scala3RunTime$.assertFailed(Scala3RunTime.scala:8)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:408)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3175)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3179)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:378)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3291)
        at dotty.tools.dotc.typer.Applications.realApply$1(Applications.scala:941)
        at dotty.tools.dotc.typer.Applications.typedApply(Applications.scala:1101)
        at dotty.tools.dotc.typer.Applications.typedApply$(Applications.scala:352)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedApply(TreeChecker.scala:501)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3040)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3103)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:395)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3175)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3179)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:378)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3291)
        at dotty.tools.dotc.typer.Typer.typedParent$1(Typer.scala:2560)
        at dotty.tools.dotc.typer.Typer.$anonfun$58(Typer.scala:2644)
        at dotty.tools.dotc.core.Decorators$.loop$1(Decorators.scala:94)
        at dotty.tools.dotc.core.Decorators$.mapconserve(Decorators.scala:110)
        at dotty.tools.dotc.typer.Typer.typedClassDef(Typer.scala:2644)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedClassDef(TreeChecker.scala:567)
        at dotty.tools.dotc.typer.Typer.typedTypeOrClassDef$1(Typer.scala:3028)
        at dotty.tools.dotc.typer.Typer.typedNamed$1(Typer.scala:3032)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3102)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:395)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3175)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3179)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:378)
        at dotty.tools.dotc.typer.Typer.traverse$1(Typer.scala:3201)
        at dotty.tools.dotc.typer.Typer.typedStats(Typer.scala:3247)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedStats(TreeChecker.scala:632)
        at dotty.tools.dotc.typer.Typer.typedPackageDef(Typer.scala:2804)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedPackageDef(TreeChecker.scala:658)
        at dotty.tools.dotc.typer.Typer.typedUnnamed$1(Typer.scala:3073)
        at dotty.tools.dotc.typer.Typer.typedUnadapted(Typer.scala:3103)
        at dotty.tools.dotc.typer.ReTyper.typedUnadapted(ReTyper.scala:126)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typedUnadapted(TreeChecker.scala:395)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3175)
        at dotty.tools.dotc.typer.Typer.typed(Typer.scala:3179)
        at dotty.tools.dotc.transform.TreeChecker$Checker.typed(TreeChecker.scala:378)
        at dotty.tools.dotc.typer.Typer.typedExpr(Typer.scala:3291)
        at dotty.tools.dotc.transform.TreeChecker.check(TreeChecker.scala:126)
        at dotty.tools.dotc.transform.TreeChecker.run(TreeChecker.scala:106)
        at dotty.tools.dotc.core.Phases$Phase.runOn$$anonfun$1(Phases.scala:324)
        at scala.collection.immutable.List.map(List.scala:246)
        at dotty.tools.dotc.core.Phases$Phase.runOn(Phases.scala:328)
        at dotty.tools.dotc.Run.runPhases$1$$anonfun$1(Run.scala:246)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:15)
        at scala.runtime.function.JProcedure1.apply(JProcedure1.java:10)
        at scala.collection.ArrayOps$.foreach$extension(ArrayOps.scala:1321)
        at dotty.tools.dotc.Run.runPhases$1(Run.scala:262)
        at dotty.tools.dotc.Run.compileUnits$$anonfun$1(Run.scala:270)
        at dotty.tools.dotc.Run.compileUnits$$anonfun$adapted$1(Run.scala:279)
        at dotty.tools.dotc.util.Stats$.maybeMonitored(Stats.scala:67)
        at dotty.tools.dotc.Run.compileUnits(Run.scala:279)
        at dotty.tools.dotc.Run.compileSources(Run.scala:194)
        at dotty.tools.dotc.Run.compile(Run.scala:179)
        at dotty.tools.dotc.Driver.doCompile(Driver.scala:37)
        at dotty.tools.dotc.Driver.process(Driver.scala:197)
        at dotty.tools.dotc.Driver.process(Driver.scala:165)
        at dotty.tools.dotc.Driver.process(Driver.scala:177)
        at dotty.tools.dotc.Driver.main(Driver.scala:207)
        at dotty.tools.dotc.Main.main(Main.scala)

Expectation

The code compiles both with and without the -Ycheck:typer flag.

More information

This seems to be related to the widening of String to scala.collection.StringOps | String, as this issue does not arise with a homemade class: the following code passes the check.

import reflect.Selectable.reflectiveSelectable

class C:
  def *(y: Int): C = this

trait A[T](x: T{ def *(y: Int): T }):
  def f: T = x * 2

class B extends A(new C())
@timotheeandres timotheeandres added itype:bug stat:needs triage Every issue needs to have an "area" and "itype" label labels May 11, 2023
@nicolasstucki nicolasstucki added area:typer and removed stat:needs triage Every issue needs to have an "area" and "itype" label labels May 11, 2023
@nicolasstucki
Copy link
Contributor

nicolasstucki commented May 11, 2023

Minimization

import reflect.Selectable.reflectiveSelectable
def f[T](x: T{ def *(y: Int): T }): T = x * 2
def test = f[scala.collection.StringOps | String]("Hello")

@nicolasstucki
Copy link
Contributor

Maybe it is because class StringOps extends AnyVal.

@mbovel mbovel added the Spree Suitable for a future Spree label May 25, 2023
@scala-center-bot
Copy link

This issue was picked for the Issue Spree No. 31 of 30 May 2023 which takes place in 2 days. @Linyxus, @hamzaremmal, @TheElectronWill will be working on it. If you have any insight into the issue or guidance on how to fix it, please leave it here.

@mbovel
Copy link
Member

mbovel commented May 30, 2023

Relevant documentation:

Linyxus added a commit that referenced this issue Jul 20, 2023
Fixes #17465.

In TypeComparer, `fourthTry` calls `isNewSubType` and `isCovered` to
detect the subtype queries that have been covered by previous attempts
and prune them. However, the pruning is spurious when both sides contain
union types, as exemplified by the following subtype trace before the
PR:
```
==> isSubType (test1 : (Int | String){def foo(x: Int): Int}) <:< Int | String?
  ==> isSubType (Int | String){def foo(x: Int): Int} <:< Int | String?
    ==> isSubType (Int | String){def foo(x: Int): Int} <:< Int?
    <== isSubType (Int | String){def foo(x: Int): Int} <:< Int = false
    ==> isSubType (Int | String){def foo(x: Int): Int} <:< String?
      ==> isSubType (Int | String){def foo(x: Int): Int} <:< String?
      <== isSubType (Int | String){def foo(x: Int): Int} <:< String = false
    <== isSubType (Int | String){def foo(x: Int): Int} <:< String = false
    // (1): follow-up subtype checks are pruned here by isNewSubType
  <== isSubType (Int | String){def foo(x: Int): Int} <:< Int | String = false
<== isSubType (test1 : (Int | String){def foo(x: Int): Int}) <:< Int | String = false
```
At `(1)`, the pruning condition is met, and follow-up recursions are
skipped. However, in this case, only after `(1)` are the refinement on
LHS dropped and the subtype between two identical OrTypes are accepted.
The pruning is spurious.

This PR tempers the pruning conditions specified in `isCovered` and
`isNewSubType` to fix these false negatives.
@Kordyjan Kordyjan added this to the 3.4.0 milestone Aug 1, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area:typer itype:bug Spree Suitable for a future Spree
Projects
None yet
Development

Successfully merging a pull request may close this issue.

5 participants