Fix #4031: Check arguments of dependent methods for realizability #4036

odersky · 2018-02-26T15:03:47Z

Also some additions to realizability tests

odersky · 2018-02-26T17:56:35Z

I now think we should try to avoid this split into isStable (checked in Typer) and checkRealizable in PostTyper, at least as far as lazy vals are concerned. We should try to test for realizibility when checking whether a lazy val is stable. If this runs into cycles, we can always back out by being conservative, i.e. assume non-stable in case of cycles. I think that's at least worth a try. The alternatives look all even less appealing.

Blaisorblade · 2018-02-26T20:49:26Z

Treating lazy vals as unstable here would already be an improvement. Is “running into cycles” insensitive to compilation order/separate compilation, or does it have a suitable conservative approximation?

Beyond “what we can implement” we should probably think of what we can specify and explain to an (advanced) user.

Blaisorblade · 2018-02-26T20:53:01Z

tests/neg/i50-volatile.scala


+  def intToString(i: Int): String = xToString(i)


Self-TODO: dig how this test broke and if this affected other tests for #50 and #1051. I suspect that’s because the logic changed at some point.

Test was modified in 955b04a (#1106), which also seems to have removed a test in tests/neg/i1050c.scala; but I guess the tests had stopped passing because of other changes. I just reenabled that test on this branch, but this PR doesn't fix it yet.

The test did not break. It's masked by the other failures. Taken alone, it would be reported later.

Blaisorblade · 2018-02-26T21:44:06Z

compiler/src/dotty/tools/dotc/transform/PostTyper.scala

@@ -205,6 +205,11 @@ class PostTyper extends MacroTransform with IdentityDenotTransformer { thisPhase
              Checking.checkInstantiable(tree.tpe, nu.pos)
              withNoCheckNews(nu :: Nil)(super.transform(tree))
            case _ =>
+              tree.fun.tpe.widen match {
+                case mt: MethodType if mt.isDependent || mt.isParamDependent =>


Gotta s/isDependent/isResultDependent/ because I merged #4039.

Blaisorblade · 2018-02-26T21:44:56Z

tests/neg/i4031.scala

+
+
+  def main(args: Array[String]): Unit = {
+    //println(coerce("Uh oh!"))


Comment back in, that's the actual ClassCastException-triggerer.

Blaisorblade · 2018-02-26T22:02:40Z

tests/neg/i1050c.scala

@@ -4,7 +4,7 @@ object Import {
    trait B { type L >: Any}
    trait U {
      lazy val p: B
-      locally { val x: p.L = ??? } // old-error: nonfinal lazy
+      locally { val x: p.L = ??? } // error: nonfinal lazy
      locally {
        import p._ // error: Import.B(U.this.p) is not a legal path
        val x: L = ??? // old-error: nonfinal lazy


Probably this should also be re-enabled, but at least the import p._ fails.

Blaisorblade · 2018-02-26T22:04:33Z

tests/neg/i1050c.scala

@@ -4,7 +4,7 @@ object Import {
    trait B { type L >: Any}
    trait U {
      lazy val p: B
-      locally { val x: p.L = ??? } // old-error: nonfinal lazy
+      locally { val x: p.L = ??? } // error: nonfinal lazy


p.L has bad bounds, and this test was disabled (by mistake) by unrelated PR #1106 (probably because it had broken), so re-enabling this test.

Since it isn't about a method call it's not addressed by the current fix, but it's still related to realizability checks I guess.

No, it was because the tests in 1050c are done during typer and the non-final lazy is detected later in PostTyper, so not detected when there are typer errors. The comment was misleading.
There are tests like this in i1050.scala, which get reported correctly.

odersky · 2018-03-17T18:17:03Z

test performance please

dottybot · 2018-03-17T18:17:15Z

performance test scheduled: 1 job(s) in queue, 0 running.

dottybot · 2018-03-17T20:00:59Z

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/4036/ to see the changes.

Benchmarks is based on merging with master (eeff384)

odersky · 2018-03-19T17:05:57Z

Last commit should fix the broken build.

Blaisorblade · 2018-03-19T19:22:32Z

Cherry-picked last commit in #4141.

Blaisorblade · 2018-03-18T14:29:58Z

compiler/src/dotty/tools/dotc/core/SymDenotations.scala

-      isType || !is(Erased) && (is(Stable) || !(is(UnstableValue) || info.isInstanceOf[ExprType]))
+    final def isStable(implicit ctx: Context) = {
+      def isUnstableValue = is(UnstableValue) || info.isInstanceOf[ExprType]
+      isType || is(Stable) || !isUnstableValue


✅ To be sure: we'd get different results for Stable | Erased but that combo is currently illegal (and Erased symbols might become Stable in the future anyway).

Blaisorblade · 2018-03-18T14:30:23Z

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -155,6 +156,12 @@ object Types {
      case _ => false
    }

+    /** Does this type denote a realizable stable reference? Much more expensive to checl


checl->check

Blaisorblade · 2018-03-19T17:54:38Z

compiler/src/dotty/tools/dotc/core/Types.scala

@@ -4136,7 +4145,7 @@ object Types {
          forwarded.orElse(
            range(super.derivedSelect(tp, preLo), super.derivedSelect(tp, preHi)))
        case _ =>
-          super.derivedSelect(tp, pre)
+          if (pre == defn.AnyType) pre else super.derivedSelect(tp, pre)


TODO: understand

Blaisorblade · 2018-03-19T19:38:38Z

compiler/src/dotty/tools/dotc/typer/TypeAssigner.scala

+    else {
+      val widenedArgType = argType.widen
+      if (realizability(widenedArgType) == Realizable)
+        tp.substParam(pref, SkolemType(widenedArgType))


widenedArgType can be realizable when argType isn't if argType is a lazy/erased value.
If argType is a normal value it's realizable always, even if widenedArgType isn't.

If neither is realizable, one could try harder, with an even wider type, but we don't have a reliable way to get at it — there are wider types (such as Any) but it's unclear there's a smallest wider type, since the class hierarchy is a DAG.

Blaisorblade · 2018-03-19T19:41:39Z

tests/pos/z1720.scala

@@ -3,7 +3,7 @@ package test
 class Thing {
  def info: Info[this.type] = InfoRepository.getInfo(this)
  def info2: Info[this.type] = {
-    def self: this.type = this
+    val self: this.type = this


So it seems that this.type should be as realizable as this, no?

Yes you are right. I added a further tweak to support this in 8389bea

odersky · 2018-03-20T12:42:31Z

Based on #4108, because that way we could remove a puzzler in derivedSelect.

Blaisorblade · 2018-03-26T20:54:46Z

Should rebase on top of #4108 (now merged). Can try next week.

Blaisorblade · 2018-04-01T23:48:57Z

compiler/src/dotty/tools/dotc/core/CheckRealizable.scala

+          if (r == Realizable) sym.setFlag(Stable)
+          r
+        }
+      if (r == Realizable || tp.info.isStableRealizable) Realizable else r


r == Realizable || can be dropped without changing meaning. In fact, it's unclear why we should check tp.info.isStableRealizable at this point — if this is necessary, it seems to warrant a comment. Maybe this subtly depends on setFlag influencing isStableRealizable.

Should we check tp.info.isStableRealizable first and skip all the other expensive computations? That doesn't set the sym.is(Stable) cache, but it can be set on request the next time.*

Otherwise, should tp.info.isStableRealizable be used when computing r?

Playing with this myself.

Blaisorblade · 2018-04-10T19:07:02Z

Status: I modified the checking algorithm (for small optimizations and to cache everything cacheable) but it should check the same "typing rules" — except for any undiscovered bugs due to internal mutations/cycles/...

I removed a code which seemed to repeat a call to realizability(tp.info), but I'm not sure if anything could actually trigger it before.

The changes might make the code faster in some cases — but the reason I made them was to make the code IMHO more sensible: now symbols are marked as is(Stable) in any of the conditions that show the symbol is Stable.

TODO: urgently rename isStable to something else.

Blaisorblade · 2018-06-26T13:02:39Z

Martin mentioned he will look at this once I assign him, so I should decide what to do about the small issues I wanted to fix.

Add the rule T <: Any for any *-Type T. This was not include fully before. We did have the rule that T <: Any, if Any is in the base types of T. However, it could be that the base type wrt Any does not exist. Example: Any#L <: Any yielded false before, now yields true. This error manifested itself in i4031.scala. With the new rule, we can drop again the special case in derivedSelect.

A TermRef is stable if its underlying type is stable. Realizability should behave the same way. This obviates the change in z1720.scala.

I had a TypeError crash in refchecks after screwing up a typeclass encoding in a particularly bad way. This commit reports an error instead.

That is, set is(Stable) for symbols that satisfy isStable.

I wrote this because I feared (incorrectly) exponential slowdowns in realizability checking for this code. But debugging suggests that the complexity of realizability checking is constant in the size of these expressions (even after I disable caching of `Stable`). Beware 1: these expressions almost smash the stack by sheer size. Beware 2: this fails with `-Yno-deep-subtypes`, but simply because the checking heuristics assumes people don't try to do this.

This reduces confusion with `Type.isStable`. I'm tempted to call this `isPure`.

This follows scala#4360. I'd love to add a test but scala#4360 has none, so I'm not 100% sure what it'd look like.

This reverts commit 283f261 because it introduces failures (which I don't get yet), as also shown in http://dotty-ci.epfl.ch/lampepfl/dotty/5085/4.

Blaisorblade · 2018-08-20T10:34:32Z

TODO: check this PR fixes https://twitter.com/propensive/status/1031419434320179200?s=21:

implicitly[(A with B)#Z =:= Int]
implicitly[(A with B)#Z =:= Char]
implicitly[(A with B)#Z =:= (B with A)#Z]

After porting the commit from scala#4036, this line newly gives an error. Might be OK, investigate.

Blaisorblade · 2018-12-02T18:14:04Z

Closed in favor of #5558 and #5559.

odersky requested a review from Blaisorblade February 26, 2018 15:03

Blaisorblade mentioned this pull request Feb 26, 2018

Good old unsoundness, CCE #4031

Closed

Blaisorblade reviewed Feb 26, 2018

View reviewed changes

Blaisorblade mentioned this pull request Mar 1, 2018

Unsoundness due to erased #4060

Closed

Blaisorblade mentioned this pull request Mar 9, 2018

Unsoundness due to projections from structural types #4098

Closed

odersky force-pushed the fix-#4031 branch from 2334158 to b85f964 Compare March 17, 2018 18:16

odersky assigned Blaisorblade Mar 17, 2018

odersky force-pushed the fix-#4031 branch from 7277c05 to a8344d3 Compare March 19, 2018 17:05

Blaisorblade reviewed Mar 19, 2018

View reviewed changes

odersky force-pushed the fix-#4031 branch from a8344d3 to cf6e895 Compare March 20, 2018 12:36

Blaisorblade mentioned this pull request Mar 20, 2018

Add kind polymorphism #4108

Merged

odersky force-pushed the fix-#4031 branch from 8389bea to d0a2c74 Compare March 28, 2018 15:57

Blaisorblade reviewed Apr 1, 2018

View reviewed changes

Blaisorblade force-pushed the fix-#4031 branch 2 times, most recently from 18ab4d0 to b62f6db Compare April 10, 2018 15:38

Blaisorblade added area:typer stat:needs review exp:advanced labels Apr 10, 2018

Blaisorblade removed the stat:needs review label Apr 10, 2018

Blaisorblade mentioned this pull request Apr 10, 2018

WIP Relax realizability for erased members, treat them like lazy ones #4290

Closed

Blaisorblade force-pushed the fix-#4031 branch from 0653040 to ef200be Compare May 25, 2018 17:11

Blaisorblade mentioned this pull request May 29, 2018

Type mismatch error involving type member #3058

Closed

odersky and others added 11 commits August 16, 2018 12:06

Clean up logic for isStable

63535f0

Fix scala#4031: Check arguments of dependent methods for realizability

db552da

Fix typo

bd55b74

Align isRealizable with isStable

9125f58

A TermRef is stable if its underlying type is stable. Realizability should behave the same way. This obviates the change in z1720.scala.

Harden RefChecks

d1e5d40

I had a TypeError crash in refchecks after screwing up a typeclass encoding in a particularly bad way. This commit reports an error instead.

Refactor realizability to also cache result of isStableRealizable

ed51433

Clarify documentation

6e21f42

Seal Realizability

61d26b9

Cache stability of non-lazy stable symbols

37b8720

That is, set is(Stable) for symbols that satisfy isStable.

Blaisorblade force-pushed the fix-#4031 branch from 9dd31f8 to 887ff57 Compare August 16, 2018 10:09

Blaisorblade added 4 commits August 16, 2018 12:52

Rename SymDenotation.isStable to SymDenotation.isStableMember

8ac0c6f

This reduces confusion with `Type.isStable`. I'm tempted to call this `isPure`.

Replace isLambdaSub with hasSimpleKind

37e1a01

This follows scala#4360. I'd love to add a test but scala#4360 has none, so I'm not 100% sure what it'd look like.

Revert "Replace isLambdaSub with hasSimpleKind"

23e6beb

This reverts commit 283f261 because it introduces failures (which I don't get yet), as also shown in http://dotty-ci.epfl.ch/lampepfl/dotty/5085/4.

Use ProblemInUnderlying consistently

ad1167c

Blaisorblade force-pushed the fix-#4031 branch from 887ff57 to ad1167c Compare August 16, 2018 10:52

Blaisorblade mentioned this pull request Nov 29, 2018

Fix #5521: prefix not checked in realizability check #5522

Merged

Blaisorblade added a commit to dotty-staging/dotty that referenced this pull request Dec 2, 2018

XXX accept new error report in test

f0f5625

After porting the commit from scala#4036, this line newly gives an error. Might be OK, investigate.

Blaisorblade mentioned this pull request Dec 2, 2018

Cleanup and improve realizability #5558

Closed

Blaisorblade added a commit to dotty-staging/dotty that referenced this pull request Dec 2, 2018

XXX accept new error report in test

ea568bb

After porting the commit from scala#4036, this line newly gives an error. Might be OK, investigate.

Blaisorblade added a commit to dotty-staging/dotty that referenced this pull request Dec 2, 2018

XXX accept new error report in test

75ba857

After porting the commit from scala#4036, this line newly gives an error. Might be OK, investigate.

Blaisorblade mentioned this pull request Dec 2, 2018

Fix #4031, v3: Check arguments of dependent methods for realizability #5559

Closed

Blaisorblade closed this Dec 2, 2018

odersky mentioned this pull request Dec 5, 2018

Refinements to realizability #5568

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix #4031: Check arguments of dependent methods for realizability #4036

Fix #4031: Check arguments of dependent methods for realizability #4036

odersky commented Feb 26, 2018

odersky commented Feb 26, 2018

Blaisorblade commented Feb 26, 2018

Blaisorblade Feb 26, 2018

Blaisorblade Feb 26, 2018

odersky Mar 17, 2018

Blaisorblade Feb 26, 2018

Blaisorblade Feb 26, 2018

Blaisorblade Feb 26, 2018

Blaisorblade Feb 26, 2018

odersky Mar 17, 2018

odersky commented Mar 17, 2018

dottybot commented Mar 17, 2018

dottybot commented Mar 17, 2018

odersky commented Mar 19, 2018

Blaisorblade commented Mar 19, 2018

Blaisorblade Mar 18, 2018

Blaisorblade Mar 18, 2018

Blaisorblade Mar 19, 2018

Blaisorblade Mar 19, 2018

Blaisorblade Mar 19, 2018

odersky Mar 20, 2018

odersky commented Mar 20, 2018

Blaisorblade commented Mar 26, 2018

Blaisorblade Apr 1, 2018

Blaisorblade Apr 5, 2018

Blaisorblade commented Apr 10, 2018

Blaisorblade commented Jun 26, 2018

Blaisorblade commented Aug 20, 2018

Blaisorblade commented Dec 2, 2018



		def main(args: Array[String]): Unit = {
		//println(coerce("Uh oh!"))

Fix #4031: Check arguments of dependent methods for realizability #4036

Fix #4031: Check arguments of dependent methods for realizability #4036

Conversation

odersky commented Feb 26, 2018

odersky commented Feb 26, 2018

Blaisorblade commented Feb 26, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky commented Mar 17, 2018

dottybot commented Mar 17, 2018

dottybot commented Mar 17, 2018

odersky commented Mar 19, 2018

Blaisorblade commented Mar 19, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

odersky commented Mar 20, 2018

Blaisorblade commented Mar 26, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Blaisorblade commented Apr 10, 2018

Blaisorblade commented Jun 26, 2018

Blaisorblade commented Aug 20, 2018

Blaisorblade commented Dec 2, 2018