Simplify polyfunction logic #18200

nicolasstucki · 2023-07-13T15:22:59Z

smarter · 2023-07-14T10:12:38Z

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

-                    return isSubInfo(tp1.refinedInfo, tp2.refinedInfo)
-                  case _ =>
+              tp1w.widenDealias match
+                case tp1: RefinedType =>


What if the refinement is for another member than apply ? I don't really understand either the previous or current logic, it seems we should be checking for apply in both tp1 and tp2, but then why do we even need special logic for functions instead of the normal logic for refinements?

This code was added in https://github.com/lampepfl/dotty/pull/15877/files#diff-c163f9660fb06bb487b0120921d06353fc52154ae1b3066f58da1c73ecd00914R613-R641

It has the following comment

// A relaxed version of subtyping for dependent functions where method types // are treated as contravariant. // TODO: Merge with isSubInfo in hasMatchingMember. Currently, we can't since // the isSubinfo of hasMatchingMember has problems dealing with PolyTypes // (---> orphan params during pickling)

Removing this completely makes some cc tests fail (such as tests/neg-custom-args/captures/heal-tparam-cs.scala).

@odersky do you have more insight on this?

a orphan param thing can be fixed by using comparingTypeLambdas when recursing in the PolyTypes, I'll update the PR.

smarter · 2023-07-14T16:10:31Z

I've pushed c304f1a which merges the two isSubInfo but that breaks capture-checking:

The isSubInfo for capture-checking got two additional cases involving
CapturingTypes in 3e690a8, I don't know what
they're supposed to do, but moving those to the regular isSubInfo breaks
various capture-checking tests:
-- [E007] Type Mismatch Error: tests/pos-custom-args/captures/classes.scala:11:32 --------------------------------------
11 |  val c1: C{val n: B^{x}}^{x} = c0
   |                                ^^
   |                                Found:    (c0 : C{val n: B^}^{x})
   |                                Required: C{val n: B^{x}}^{x}
So this commit breaks capture-checking and I don't know enough about what this
code is supposed to do to fix it.

/cc @Linyxus

The isSubInfo for capture-checking introduced in scala#15877 had the following TODO: // A relaxed version of subtyping for dependent functions where method types // are treated as contravariant. // TODO: Merge with isSubInfo in hasMatchingMember. Currently, we can't since // the isSubinfo of hasMatchingMember has problems dealing with PolyTypes // (---> orphan params during pickling) The orphan params error was due to the recursion on the result of the PolyTypes being done without first calling `compareTypeLambda`. After fixing this we can safely merge the two versions while keeping the new behavior for dependent and polymorphic function types hidden under the `captureChecking` feature since they're language changes. I'll open a separate PR to create a `relaxedSubtyping` feature for these improvements since their usefulness is independent of capture checking. The isSubInfo for capture-checking got two additional cases involving CapturingTypes in 3e690a8, I don't know what they're supposed to do, but moving those to the regular isSubInfo breaks various capture-checking tests: -- [E007] Type Mismatch Error: tests/pos-custom-args/captures/classes.scala:11:32 -------------------------------------- 11 | val c1: C{val n: B^{x}}^{x} = c0 | ^^ | Found: (c0 : C{val n: B^}^{x}) | Required: C{val n: B^{x}}^{x} So this commit breaks capture-checking and I don't know enough about what this code is supposed to do to fix it.

- Keep the shortcut for function types in compareRefined - Temper isSubInfo logic

Linyxus · 2023-07-18T20:01:57Z

I just pushed a commit, which tweaks the merged isSubInfo to work for capture checking. However, the shortcut for function types in compareRefined is kept. I tried to remove it and traced the problem down; it turns out to be related to both the setup of CC and member lookup (tp.member(name)), and seems to be a rabbit hole.

smarter · 2023-07-18T20:16:29Z

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

+      else isSubType(info1, info2)
+    val isCCPhase = ctx.phase == Phases.checkCapturesPhase
+
+    (info1, info2) match


The previous version used two pattern matches on info1 and info2 instead of a pattern match on a tuple for performance, I suggest keeping the two pattern matches since this code path could be hot.

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

smarter · 2023-07-18T20:19:07Z

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

-                  && isSubInfo(parent1, info2, symInfo1)
-              case _ => fallback
+      def fallback = (info1: Type, info2: Type) =>
+        def tp1IsSingleton: Boolean = tp1.isInstanceOf[SingletonType]


Using a def here instead of a val doesn't seem useful since it's evaluated in the next line

@smarter

instead of matching a tuple. Suggested by @smarter.

- Document the shortcut in compareRefined for function types under CC phase - Change a `def` to a `val`

odersky

Looking at this closely, I doubt this is an improvement.

Positive: We have merged to subInfo definitions into one.

Negative: The new subInfo definition is a lot more complicated and needs to be parameterized with two auxiliary functions.

I think at least for me the net result is a loss in legibility. And despite the attempt to remove duplication, the code is now longer than before.

Is there a strong reason we need to do this refactoring?

smarter · 2023-07-24T22:06:31Z

Is there a strong reason we need to do this refactoring?

The problem is that the current capture checking logic is relying on hacks, the refactoring at least makes this clearer. To recap:

The duplication was introduced in https://github.com/dotty-staging/dotty/blob/943d84aadfb3f4a07dfaec92b9b5696196977b24/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L616-L621, with a TODO mentioning an error with orphan parameters when merging the logic
Extra cases were added in 3e690a8
It turns out that I know how to solve the original TODO (using comparingTypeLambda), but merging the two isSubInfo isn't possible anymore because the cases introduced in 2. are accidentally relying on being only in one of the two isSubInfo, and no one understands why.

I think the longer we keep the two isSubInfo, the more problems like this we're likely to introduce, and the harder compiler maintenance becomes in general (in particular, I was trying to experiment with changes to isSubInfo, but having to maintain and tests two versions in parallel makes that a lot more tedious that it needs to be).

I agree that as-is the PR isn't great because of the lingering FIXME, but I don't know enough about the capture checking logic to fix that myself right now.

odersky · 2023-07-25T07:29:36Z

It's actually not a hack. CC checking converts all function types to dependent function types but then intentionally uses only the refinement in a function type for comparisons and ignores the parent. In a sense it moves already what towards what we think a principled handling of function types should do. Given this, it seems at present counter-productive to merge the two cases. It's better to isolate the capture checking case in its own corner.

smarter · 2023-07-25T13:23:57Z

Given this, it seems at present counter-productive to merge the two cases.

OK, could the documentation of the cc isSubInfo be updated to remove the TODO mentioning merging them then?
https://github.com/lampepfl/dotty/blob/3e00a0d801ec0528992708dc210a0c102dd1eb8f/compiler/src/dotty/tools/dotc/core/TypeComparer.scala#L648
More documentation explaining why this is treated differently than in regular typechecking would also be helpful because I'm pretty lost at this point.

odersky · 2023-07-25T13:25:34Z

OK, I'll update the comment.

odersky · 2023-07-27T16:22:02Z

I'll roll the doc change into another PR.

nicolasstucki force-pushed the simplify-polyfunction-logic branch from c224a3b to 4b3d61b Compare July 14, 2023 06:58

nicolasstucki mentioned this pull request Jul 14, 2023

Refactor function type logic #18193

Merged

nicolasstucki requested a review from smarter July 14, 2023 09:08

nicolasstucki assigned smarter Jul 14, 2023

nicolasstucki marked this pull request as ready for review July 14, 2023 09:08

smarter reviewed Jul 14, 2023

View reviewed changes

nicolasstucki assigned odersky and unassigned smarter Jul 14, 2023

nicolasstucki assigned smarter and Linyxus and unassigned odersky Jul 17, 2023

smarter removed their assignment Jul 17, 2023

Linyxus force-pushed the simplify-polyfunction-logic branch 2 times, most recently from 5efada6 to ea842be Compare July 18, 2023 19:51

nicolasstucki and others added 3 commits July 19, 2023 03:52

Simplify polyFunction logic in TypeComparer

a839c03

Tweak isSubInfo for capture checking

dd21be8

- Keep the shortcut for function types in compareRefined - Temper isSubInfo logic

Linyxus force-pushed the simplify-polyfunction-logic branch from ea842be to dd21be8 Compare July 18, 2023 19:52

smarter reviewed Jul 18, 2023

View reviewed changes

compiler/src/dotty/tools/dotc/core/TypeComparer.scala Show resolved Hide resolved

smarter reviewed Jul 18, 2023

View reviewed changes

Linyxus added 2 commits July 19, 2023 09:40

Use nested pattern matching in isSubInfo

e4fc9e4

instead of matching a tuple. Suggested by @smarter.

Address review comments

01e3397

- Document the shortcut in compareRefined for function types under CC phase - Change a `def` to a `val`

Linyxus requested a review from odersky July 19, 2023 07:24

Linyxus assigned odersky and unassigned Linyxus Jul 20, 2023

odersky reviewed Jul 23, 2023

View reviewed changes

odersky removed their assignment Jul 23, 2023

odersky assigned nicolasstucki Jul 23, 2023

nicolasstucki assigned odersky and unassigned nicolasstucki Jul 27, 2023

odersky closed this Jul 27, 2023

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Simplify polyfunction logic #18200

Simplify polyfunction logic #18200

Uh oh!

nicolasstucki commented Jul 13, 2023 •

edited

Loading

Uh oh!

smarter Jul 14, 2023

Uh oh!

nicolasstucki Jul 14, 2023

Uh oh!

smarter Jul 14, 2023

Uh oh!

smarter commented Jul 14, 2023

Uh oh!

Linyxus commented Jul 18, 2023 •

edited

Loading

Uh oh!

smarter Jul 18, 2023

Uh oh!

Uh oh!

smarter Jul 18, 2023

Uh oh!

odersky left a comment

Uh oh!

smarter commented Jul 24, 2023 •

edited

Loading

Uh oh!

odersky commented Jul 25, 2023

Uh oh!

smarter commented Jul 25, 2023

Uh oh!

odersky commented Jul 25, 2023

Uh oh!

odersky commented Jul 27, 2023

Uh oh!

Uh oh!

Simplify polyfunction logic #18200

Simplify polyfunction logic #18200

Uh oh!

Conversation

nicolasstucki commented Jul 13, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smarter Jul 14, 2023

Choose a reason for hiding this comment

Uh oh!

nicolasstucki Jul 14, 2023

Choose a reason for hiding this comment

Uh oh!

smarter Jul 14, 2023

Choose a reason for hiding this comment

Uh oh!

smarter commented Jul 14, 2023

Uh oh!

Linyxus commented Jul 18, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

smarter Jul 18, 2023

Choose a reason for hiding this comment

Uh oh!

Uh oh!

smarter Jul 18, 2023

Choose a reason for hiding this comment

Uh oh!

odersky left a comment

Choose a reason for hiding this comment

Uh oh!

smarter commented Jul 24, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

odersky commented Jul 25, 2023

Uh oh!

smarter commented Jul 25, 2023

Uh oh!

odersky commented Jul 25, 2023

Uh oh!

odersky commented Jul 27, 2023

Uh oh!

Uh oh!

nicolasstucki commented Jul 13, 2023 •

edited

Loading

Linyxus commented Jul 18, 2023 •

edited

Loading

smarter commented Jul 24, 2023 •

edited

Loading