Fix #7044: Approximate GADT bounds to avoid explicit type ascriptions #8728

radeusgd · 2020-04-15T11:49:05Z

Adding GADT approximation mechanism created by @AleksanderBG, updated with a recovery mechanism that preserves good error messages on approximation failure in the recovery stage, in order to avoid having to specify explicitly ascribe type bounds that can be inferred from the context, as described in #7044.

dottybot

Hello, and thank you for opening this PR! 🎉

All contributors have signed the CLA, thank you! ❤️

Commit Messages

We want to keep history, but for that to actually be useful we have
some rules on how to format our commit messages (relevant xkcd).

Please stick to these guidelines for commit messages:

Separate subject from body with a blank line

When fixing an issue, start your commit message with Fix #<ISSUE-NBR>:

Limit the subject line to 72 characters

Capitalize the subject line

Do not end the subject line with a period

Use the imperative mood in the subject line ("Add" instead of "Added")

Wrap the body at 80 characters

Use the body to explain what and why vs. how

adapted from https://chris.beams.io/posts/git-commit

Have an awesome day! ☀️

radeusgd · 2020-04-15T11:52:10Z

tests/neg/boundspropagation.scala

@@ -25,19 +25,6 @@ object test3 {
  }
 }

-// Example contributed by Jason.


This test has been removed as we discussed with @AleksanderBG and we think it is correct for it to actually compile.

My reasoning is following:
we have y: Tree[S, T] where Nothing <: S, Option[Nothing] <: Option[S] <: T
we ascribe y: Tree[Nothing, Option[Nothing]]

we can do that because:
Nothing <: S, Option[Nothing] <: T so Tree[S, T] <: Tree[Nothing, Option[Nothing]]
(because Tree is contravariant in both its parameters)

we want y to conform to Tree[A,B] where B <: Option[N], as Option[Nothing] <: Option[N], it typechecks

Shouldn't this be re added as a pos test?

Indeed, I have added it.

abgruszecki

Looks good! Thanks for you work, Radek.

Reg. CI failing: could you try rebasing on newest master? I ran dotty-boostrapped clean and test on my machine and everything succeeded, so if the error was something that was on master, as you wrote to me, then rebase should fix it.

Reg. tuples: I took a look at Paolo's code, the following version works:

scala> {                                                                                                                                                                                                           
     | object GadtAscription {
     |   enum Var[G, A] {
     |     case Z[G, A]() extends Var[(A, G), A]
     |     case S[G, A, B](x: Var[G, A]) extends Var[(B, G), A]
     |   }
     | 
     |   import Var._
     |   def evalVar[G, A](x: Var[G, A])(rho: G): A = x match {
     |     case _: Z[g, a] =>
     |       rho(0)
     |     case s: S[g, a, b] =>
     |       evalVar(s.x)(rho(1))
     |   }
     | }
     | }
approximated G  ~~  (a, g) 
 [AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class *:),List(TypeRef(NoPrefix,type a), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class *:),List(TypeRef(NoPrefix,type g), TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Unit)))))]
approximated G  ~~  (b, g) 
 [AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class *:),List(TypeRef(NoPrefix,type b), AppliedType(TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class *:),List(TypeRef(NoPrefix,type g), TypeRef(ThisType(TypeRef(NoPrefix,module class scala)),class Unit)))))]
// defined object GadtAscription

It'd be good to add it as a test. You can also see that sth weird is going on w/ GADT bounds if you take a closer look at the .toString-s of approximated types: they contain essentially a *: g *: Unit, which is our list-like tuple representation. Where these come from, I do not fully know, but it's my understanding that tuple(n) is going to be the normal way of selecting tuple members going forward, so it's fine if ._1 doesn't work.

abgruszecki · 2020-04-17T12:56:16Z

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

+    res
+  }
+
+  private class IsFullyDefinedAccumulator2(implicit ctx: Context) extends TypeMap {


This class should probably be renamed, to something like ApproximateGadtAccumulator perhaps? Also it would be nice to add a comment stating it's mostly copied from IsFullyDefinedAccumulator.

abgruszecki · 2020-04-17T13:00:24Z

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

+        val res =
+          ctx.gadt.approximation(sym, fromBelow = variance < 0)
+
+        debug.println(i"approximated $tp  ~~  $res")


Overally feedback re. debug stmts (I know that most of these are leftovers from me :P):

My general impression is that using debug Printer is to be avoided in master-branch code. debug is mostly used for, as name suggests, quick debugging stmts and we usually want only the stmts we just added to print, not the ones half a codebase away. For this message, I'd use the gadt printer.

At a glance, there's too much debugging stmts remaining. As a first approximation, I'd say only this statement should be left, but since you were the one to work on this code most recently, I'll leave it to you to decide if other stmts should also be left, for the convenience of future debugging.

Thanks, I have left this one and another one that displays some information from the GADT context, as I think it was most useful for debugging. I moved both to the gadts printer.

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

radeusgd · 2020-04-22T16:02:21Z

For some reason there's the following error in test_bootstrapped ~~(which at least at first seems unrelated)~~:

[info] Test dotty.tools.dotc.BootstrappedOnlyCompilationTests.runMacros started
Cyclic macro dependencies in tests/run-macros/tasty-tree-map/quoted_1.scala.
Compilation stopped since no further progress can be made.

To fix this, place macros in one set of files and their callers in another.

Compiling with  -Xprint-suspension   gives more information.
-- [E006] Not Found Error: tests/run-macros/tasty-tree-map/quoted_2.scala:2:7 ------------------------------------------
2 |import Macros._
  |       ^^^^^^
  |       Not found: Macros
Compilation failed for: 'tests/run-macros/tasty-tree-map'                       
[error] Test dotty.tools.dotc.BootstrappedOnlyCompilationTests.runMacros failed: java.lang.AssertionError: Run test failed, but should not, reasons:
[error] 
[error]   - encountered 1 test failures(s), took 15.948 sec
[error]     at dotty.tools.vulpix.ParallelTesting$CompilationTest.checkRuns(ParallelTesting.scala:909)
[error]     at dotty.tools.dotc.BootstrappedOnlyCompilationTests.runMacros(BootstrappedOnlyCompilationTests.scala:123)

~~When testing locally on the current master (namely 755a81f), I also get an error but a different one (removed as this doesn't seem related).~~

radeusgd · 2020-04-27T20:30:24Z

Regarding the previous comment, it was my mistake - the tasty-tree-map test is also failing locally for me, I must have missed that somehow.

And it is indeed related to the GADT approximation somehow, because when I disabled it, the test is back to normal.

I will try investigating further what is the cause of that failure.

An easy way to reproduce the error is to run dotc tests/run-macros/tasty-tree-map/quoted_1.scala.

nicolasstucki · 2020-05-01T09:50:12Z

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

+    val IsDummyTree = new Property.Key[Unit]
+
+    def apply(tp: Type)(implicit src: SourceFile): Tree =
+      (untpd.Literal(Constant(null)) withTypeUnchecked tp).withAttachment(IsDummyTree, ())


Maybe we should introduce a proper internal construct for these trees. Maybe have a scala.internal.bla.dummyTree[T] .

Same for the unapply

We can improve on this later.

@nicolasstucki can you elaborate on what scala.internal.bla.dummyTree[T] should be? Some sort of special fictional value? I think creating a special Tree subclass for this purpose would work.

@smarter it turned out that it was dummyTreeOfType that was the source of the null we talked about. Could you chime in with an opinion on whether it ever makes sense to adapt dummy trees created by this function?

honestly no clue, I myself only learned about dummyTreeOfType recently.

abgruszecki · 2020-05-12T11:00:05Z

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

-  def adapt(tree: Tree, pt: Type, locked: TypeVars)(using Context): Tree =
-    trace(i"adapting $tree to $pt", typr, show = true) {
+  def adapt(tree: Tree, pt: Type, locked: TypeVars, tryGadtHealing: Boolean = true)(using Context): Tree = {
+    val last = Thread.currentThread.getStackTrace()(2).toString;


@radeusgd one final bit of work: this should 100% be a def. Getting a stack trace is costly and adapt is, I'd hazard the guess, called very often. Everything else looks good. Thanks again for your excellent work on this PR!

Now that I look at it, I think it was just a part of my debugging and possibly can be removed altogether.

I have double checked and this stack trace here wasn't very useful (probably that's why I forgot to remove it, as I wasn't using it much during debugging), I have removed it from this trace and made (tryGadtHealing=???) appear only if it's false (because most of the time it's true and it would just clutter the traces), is that ok?

This is your code and your debugging statements, it sure is :)

dottybot reviewed Apr 15, 2020

View reviewed changes

radeusgd commented Apr 15, 2020

View reviewed changes

radeusgd force-pushed the gadt-ascription3 branch from 321dbb0 to 072a7a0 Compare April 15, 2020 20:50

abgruszecki reviewed Apr 17, 2020

View reviewed changes

radeusgd force-pushed the gadt-ascription3 branch from 072a7a0 to 8d8a362 Compare April 22, 2020 12:50

smarter reviewed Apr 22, 2020

View reviewed changes

compiler/src/dotty/tools/dotc/typer/Typer.scala Outdated Show resolved Hide resolved

radeusgd force-pushed the gadt-ascription3 branch from 8d8a362 to 7f262a1 Compare April 22, 2020 13:02

Add GADT approximation in adaptToSubType

89a2104

radeusgd force-pushed the gadt-ascription3 branch from 7f262a1 to 9941c2a Compare April 30, 2020 23:14

nicolasstucki reviewed May 1, 2020

View reviewed changes

nicolasstucki linked an issue May 1, 2020 that may be closed by this pull request

Member selection does not take GADT constraints into account #7044

Closed

radeusgd requested review from abgruszecki and smarter May 1, 2020 10:50

abgruszecki reviewed May 12, 2020

View reviewed changes

Fix lampepfl#7044: Added GADT recovery with fallback to default error.

b98d94b

radeusgd force-pushed the gadt-ascription3 branch from 9941c2a to b98d94b Compare May 12, 2020 12:34

radeusgd requested a review from abgruszecki May 12, 2020 13:36

abgruszecki merged commit b0c010e into scala:master May 12, 2020

smarter mentioned this pull request Jul 2, 2020

Incorrect code ends up passing the typechecker due to GADT logic misfiring #9274

Closed

Fix #7044: Approximate GADT bounds to avoid explicit type ascriptions #8728

Fix #7044: Approximate GADT bounds to avoid explicit type ascriptions #8728

Uh oh!

Conversation

radeusgd commented Apr 15, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

dottybot left a comment

Choose a reason for hiding this comment

Commit Messages

Uh oh!

radeusgd Apr 15, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

abgruszecki left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

radeusgd commented Apr 22, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

radeusgd commented Apr 27, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

radeusgd commented Apr 15, 2020 •

edited

Loading

radeusgd Apr 15, 2020 •

edited

Loading

abgruszecki left a comment •

edited

Loading

radeusgd commented Apr 22, 2020 •

edited

Loading

radeusgd commented Apr 27, 2020 •

edited

Loading