Higher-kinded type variable unification. #6069

TomasMikula · 2017-09-11T23:36:21Z

Currently, when checking whether [α]Foo[Bar[α]] is a subtype of (higher-kinded) type variable ?F, the current implementation eta-expands F to [β]F[β], substitutes the same type parameters [α]F[α] and then checks whether Foo[Bar[α]] <: F[α]. Then (I think) F is unified with Foo and α fails to unify with Bar[α].

This PR changes that to immediately unify F with [α]Foo[Bar[α]] if α is compatible with F's type parameter.

This change can cause ambiguous implicits, so is under a compiler flag
~~-Yhk-typevar-unification~~ -Xsource:2.13.

Fixes scala/bug#10185, scala/bug#10195, scala/bug#10197, scala/bug#10213, scala/bug#10238, scala/bug#10372.
Also fixes scala/bug#6895 in a different way than -Ypartial-unification.

TomasMikula · 2017-09-12T10:49:23Z

The build failed due to binary compatibility issues. How can I run the binary compatibility test locally?

lrytz · 2017-09-12T11:05:33Z

If you want to run all tests you can use testAll in sbt. For MiMa specifically, use mimaReportBinaryIssues.

TomasMikula · 2017-09-12T11:08:16Z

Thanks. I get

...
[info] scala-compiler: previous-artifact not set, not analyzing binary compatibility
...

lrytz · 2017-09-12T11:10:05Z

That's expected, we only check binary compatibility for scala-library and scala-reflect. Minor versions of the scala-compiler jar are not binary compatible.

TomasMikula · 2017-09-12T11:36:31Z

Oh, right, the incompatible change was in scala-reflect and my speculative "fix"

ProblemFilters.exclude[DirectMissingMethodProblem]("scala.reflect.runtime.Settings.YhkTypevarUnification")

worked, so hopefully the current build will succeed.

It also took me a while to figure out why mimaReportBinaryIssues kept crashing with

java.nio.charset.MalformedInputException: Input length = 1

Turns out I cannot have the file src/reflect/mima-filters/2.12.0.forwards.excludes open in vim, because it creates a temporary .2.12.0.forwards.excludes.swp file in the same directory, and mimaReportBinaryIssues apparently doesn't like that.

non · 2017-09-12T15:53:37Z

Great work @TomasMikula! This is really exciting! ✨

retronym · 2017-09-13T06:46:19Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

+        (ntp2.typeParams corresponds tv1.params)(methodHigherOrderTypeParamsSubVariance) &&
+        { tv1.addHiBound(ntp2); true }
+      case (tp1, tp2) => isSub2(tp1.normalize, tp2.normalize)  // @M! normalize reduces higher-kinded case to PolyType's
+    }


The implementations of <:< and =:= usually follow the same pattern. I wonder if a similar change needed in:

private def isSameHKTypes(tp1: Type, tp2: Type) = ( tp1.isHigherKinded && tp2.isHigherKinded && (tp1.normalize =:= tp2.normalize) )

It would be great to setup a unit test in the same vein as https://github.com/scala/scala/blob/9acab45aeeadef2f63da69faf81465cc15599789/test/junit/scala/reflect/internal/TypesTest.scala to directly demonstrate the new unification (rather than indirectly via compilation), and to explore whether the change preserves transitivity of subtyping and consistency with =:=.

I wonder if a similar change needed in:

private def isSameHKTypes(tp1: Type, tp2: Type)

If =:= also performs unification as a side effect, then yes. Otherwise, I think it is not necessary.

It does, via mutateNonTypeConstructs and then registerTypeEquality

Yeah. Nevertheless, mutateNonTypeConstructs already seems to handle the higher-kinded TypeVar case correctly.

retronym · 2017-09-13T08:13:00Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

@@ -365,9 +365,23 @@ trait TypeComparers {

  // @assume tp1.isHigherKinded || tp2.isHigherKinded
  def isHKSubType(tp1: Type, tp2: Type, depth: Depth): Boolean = {
-    def isSub(ntp1: Type, ntp2: Type) = (ntp1.withoutAnnotations, ntp2.withoutAnnotations) match {
+    def isSub(tp1: Type, tp2: Type) = (tp1.withoutAnnotations, tp2.withoutAnnotations) match {
      case (TypeRef(_, AnyClass, _), _)                                     => false                    // avoid some warnings when Nothing/Any are on the other side
      case (_, TypeRef(_, NothingClass, _))                                 => false


Type aliases for Any and Nothing would evade the short circuit now that the caller doesn't normalize.

Thanks, will move these 2 lines down to isSub2.

retronym · 2017-09-13T08:57:16Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

+      case (tp1, tv2 @ TypeVar(_, _)) if settings.YhkTypevarUnification =>
+        val ntp1 = tp1.normalize
+        (tv2.params corresponds ntp1.typeParams)(methodHigherOrderTypeParamsSubVariance) &&
+        { tv2.addLoBound(ntp1); true }


The existing code in TypeVar.registerBound that responsible for unifying applied hk type vars walks up the base type sequence to find an arity match. What do we know about tv2.params.length == ntp1.typeParams.length by virtue of making it to this line of code?

We know tv2.params.length == ntp1.typeParams.length thanks to a successful corresponds on the previous line.

TomasMikula · 2017-09-14T18:12:27Z

Added some tests, some of them currently failing. Pending resolution of #6080 before I continue on this one.

Atry · 2017-09-19T09:18:58Z

Does this PR solve https://stackoverflow.com/questions/32182694/how-to-define-an-existential-higher-kinded-type-in-scala?

TomasMikula · 2017-09-19T21:48:09Z

@Atry That is not solved by this PR.

adriaanm

Exciting! I have a few questions/suggestions. Thanks for taking this on.

adriaanm · 2017-09-20T18:50:53Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

-    def isSub(ntp1: Type, ntp2: Type) = (ntp1.withoutAnnotations, ntp2.withoutAnnotations) match {
+
+    def isSub(tp1: Type, tp2: Type) = (tp1.withoutAnnotations, tp2.withoutAnnotations) match {
+      case (tv1 @ TypeVar(_, _), tv2 @ TypeVar(_, _)) if settings.YhkTypevarUnification =>


I'd rather not add more individual feature flags, they end up sticking around and complicating the user experience. Let's just use -Xsource:2.13, and let's test that flag only once, instead of in each guard (pull out the more advanced type var unification into another method?)

adriaanm · 2017-09-20T18:52:23Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

+    def isSub(tp1: Type, tp2: Type) = (tp1.withoutAnnotations, tp2.withoutAnnotations) match {
+      case (tv1 @ TypeVar(_, _), tv2 @ TypeVar(_, _)) if settings.YhkTypevarUnification =>
+        (tv2.params corresponds tv1.params)(methodHigherOrderTypeParamsSubVariance) &&
+        { tv1.addHiBound(tv2); tv2.addLoBound(tv1); true }


Let's debug this and get some statistics on how (often) we actually get here during a bootstrap/test suite. As Jason said, inference that compares TVs on both ends is likely to fail in the end.

Will investigate.

I tried to add assert(false) to this branch and it is not triggered by tests or bootstrap. What do you suggest? Should I just change that branch to assert(false)?

I wouldn't risk a crash, but we could consider a warning to test our theory since this codepath isn't enabled by default. I haven't thought about it much, but there's precedent (grep "please report" for another warning).

We can get here thanks to

scala/src/compiler/scala/tools/nsc/typechecker/Infer.scala

Lines 538 to 550 in 3a76f41

// Then define remaining type variables from argument types.

map2(argtpes, formals) { (argtpe, formal) =>

val tp1 = argtpe.deconst.instantiateTypeParams(tparams, tvars)

val pt1 = formal.instantiateTypeParams(tparams, tvars)

// Note that isCompatible side-effects: subtype checks involving typevars

// are recorded in the typevar's bounds (see TypeConstraint)

if (!isCompatible(tp1, pt1)) {

throw new DeferredNoInstance(() =>

"argument expression's type is not compatible with formal parameter type" + foundReqMsg(tp1, pt1))

}

}

val targs = solvedTypes(tvars, tparams, tparams map varianceInTypes(formals), upper = false, lubDepth(formals) max lubDepth(argtpes))

adriaanm · 2017-09-20T18:58:18Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

+
+    def isSub(tp1: Type, tp2: Type) = (tp1.withoutAnnotations, tp2.withoutAnnotations) match {
+      case (tv1 @ TypeVar(_, _), tv2 @ TypeVar(_, _)) if settings.YhkTypevarUnification =>
+        (tv2.params corresponds tv1.params)(methodHigherOrderTypeParamsSubVariance) &&


It's kind of confusing that we check methodHigherOrderTypeParamsSubVariance(tp2.typeParams, tp1.typeParams) to compute isSub(tp1, tp2) (what's the logic behind going in the opposite direction?)

I took this from isPolySubType, assuming the reason for opposite direction was that type parameters in [X, Y] => T appear in contravariant position. Looking at the implementation of methodHigherOrderTypeParamsSubVariance, from 2.11 onwards it always returns true, so could now be removed altogether?

adriaanm · 2017-09-20T19:29:01Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

+        (ntp2.typeParams corresponds tv1.params)(methodHigherOrderTypeParamsSubVariance) &&
+        { tv1.addHiBound(ntp2); true }
+      case (tp1, tp2) => isSub2(tp1.normalize, tp2.normalize)  // @M! normalize reduces higher-kinded case to PolyType's
+    }


It does, via mutateNonTypeConstructs and then registerTypeEquality

adriaanm · 2017-09-27T16:22:26Z

Needs a mima exception:

ProblemFilters.exclude[DirectMissingMethodProblem]("scala.reflect.runtime.Settings.isScala213")

TomasMikula · 2017-09-27T17:02:08Z

Thanks! Fixed.

TomasMikula · 2017-09-27T23:23:24Z

Just realized that this PR also fixes some problems with pattern matching:

Pattern matching on Foo[A, F[_ <: A]] doesn't compile bug#10185
Pattern matching on Foo[F[_]] where F is a type alias with phantom type parameter doesn't work bug#10195

Added positive tests for those to this PR.

TomasMikula · 2017-09-28T09:17:28Z

As per comments in #6080, seems like the two failing tests added in the latter commit can be ignored, since those cases should be unreachable through compilation.

adriaanm · 2017-09-28T21:59:39Z

Our policy is not to merge PRs that contain failing commits (so, let's testHigherKindedTypeVarUnification). Also, on second thought (sorry), I'd rather not ignore MiMa's advice (I've come to regret that before). Let's inline isScala213.

We'll allow PRs currently scheduled for 2.12.4 to be merged until Friday, run benchmarks and community builds over the weekend and Monday, and cut the release on Tuesday. Any PRs that regress performance / break the community build will be reverted and rescheduled for 2.12.5.

TomasMikula · 2017-09-28T22:31:21Z

Ideas how I can inline isScala213? In scala.tools.nsc.settings.ScalaSettings it is defined as source.value >= version213, but source is not a member of scala.reflect.internal.settings.MutableSettings.

adriaanm

Nice! Thanks for pushing this all the way through!

adriaanm · 2017-09-29T16:02:44Z

PS: for the "fixes" command in the PR description to be picked up (and bugs to be auto-closed on merge), the syntax for the bug reference is scala/bug#NNNNN (I updated the description)

TomasMikula · 2017-09-29T16:05:37Z

Thanks! I thought it was sufficient that the "fixes" were spelled out this way in the commit message.

In scala#6092, `-Xsource:2.13` was enabled by default. Between this PRs parent and current 2.13.x, there were some changes that depended on this flag (scala#5983, scala#6069).

Since scala#6069, it is possible to have type variables compared to the eta expansion of a class type, which is `[CLASSTPARAM] => Class[CLASSTPARAM]`. After separate compilation, the owner this higher kinded type param is adjusted to the root class (see the comments and special cases in Pickler.localizedOwner), which makes it show up to certain subsequent as-seen-from maps as a type parameter of an enclosing class. SBT's ExtractAPI phase runs into this problem. This commit pins down the problem with a test and offers a straw-man fix, which clones the type params at a different owner (currently, NoOwner, but with a bit more refactoring this should be context.owner) when type when instantiating the type variables. An alternative might be to clone during eta-expansion (although to which owner? NoSymbol? A user provided one? What does this mean for our strategy of caching normalized types for performance?) A third fix would be to do the `cloneInfo` before registering the bound in `TypeComparers`. We'd need to refactor somewhat to thread through `context.owner` to that code, however. Fixes scala/bug#t10762

Since scala#6069, it is possible to have type variables compared to the eta expansion of a class type, which is `[CLASSTPARAM] => Class[CLASSTPARAM]`. After separate compilation, the owner of this type constructor param is adjusted to the root class (see the comments and special cases in Pickler.localizedOwner), which makes it show up to certain subsequent as-seen-from maps as a type parameter of an enclosing class. SBT's ExtractAPI phase runs into this problem. Eta expansion of the tycon type ref uses an owner (NoSymbol) that will not become a class after pickling. Fixes scala/bug#10762

joroKr21 · 2018-12-27T22:00:33Z

Regression: scala/bug#11303

joroKr21 · 2018-12-27T22:05:07Z

src/reflect/scala/reflect/internal/tpe/TypeComparers.scala

+            """.trim)
+        false
+      case (tp1, tv2 @ TypeVar(_, _)) =>
+        val ntp1 = tp1.normalize


I don't understand, what was the reason for calling normalize here on the to-be-bound?

scala-jenkins added this to the 2.12.4 milestone Sep 11, 2017

TomasMikula force-pushed the hk-typevar-unification branch from 65bddd5 to 9987289 Compare September 12, 2017 10:48

TomasMikula force-pushed the hk-typevar-unification branch from 9987289 to db768cf Compare September 12, 2017 11:01

retronym reviewed Sep 13, 2017

View reviewed changes

TomasMikula mentioned this pull request Sep 14, 2017

Failing tests for type comparisons. #6080

Closed

TomasMikula force-pushed the hk-typevar-unification branch from db768cf to 2f97833 Compare September 14, 2017 18:11

adriaanm suggested changes Sep 20, 2017

View reviewed changes

TomasMikula force-pushed the hk-typevar-unification branch from 2f97833 to 25db6f7 Compare September 26, 2017 13:23

TomasMikula force-pushed the hk-typevar-unification branch from 25db6f7 to f3e1d33 Compare September 27, 2017 17:01

TomasMikula force-pushed the hk-typevar-unification branch 2 times, most recently from d944d07 to c6c10b1 Compare September 27, 2017 23:18

TomasMikula force-pushed the hk-typevar-unification branch 2 times, most recently from 279d3cf to ef39378 Compare September 28, 2017 01:17

adriaanm approved these changes Sep 29, 2017

View reviewed changes

adriaanm merged commit 64dd408 into scala:2.12.x Sep 29, 2017

SethTisue added the release-notes worth highlighting in next release notes label Oct 2, 2017

TomasMikula mentioned this pull request Oct 20, 2017

Enable -Xsource:2.13 and resolve subsequent ambiguous implicits scalaz/scalaz#1494

Merged

lrytz mentioned this pull request Dec 1, 2017

Remove logic to check if a named arg could be an assignment (and enable -Xsource:2.13 by default) #6092

Merged

lrytz mentioned this pull request Dec 1, 2017

Fix tests that failed due to -Xsource:2.13 #6206

Merged

martijnhoekstra mentioned this pull request Dec 11, 2017

failure to infer hk type parameter scala/bug#10653

Open

TomasMikula mentioned this pull request Jan 25, 2018

scalaz doesn't compile in what will soon become Scala 2.13.0-M3 scalaz/scalaz#1629

Closed

adriaanm mentioned this pull request Feb 1, 2018

Document features conditional on source and target versions scala/scala-dev#470

Open

SethTisue mentioned this pull request Feb 14, 2018

Release for Scala 2.13.0-M3, please? etorreborre/specs2#632

Closed

hrhino mentioned this pull request Feb 20, 2018

No type parameters for method exists when HKT involved scala/bug#10738

Closed

retronym mentioned this pull request Jul 12, 2018

Regression in 2.13.0-M3: compiler crash with mismatched type params and args in Scalacheck clients scala/bug#10762

Closed

adriaanm mentioned this pull request Jul 13, 2018

Eta-expanded tycon's type params need own owner #6932

Closed

joroKr21 reviewed Dec 27, 2018

View reviewed changes

joroKr21 mentioned this pull request Mar 17, 2019

Implicit conversion fails whenever an unnamed identity type lambda is present scala/bug#11435

Closed

neko-kai mentioned this pull request Mar 17, 2019

Covariant HKT implicits fail to resolve scala/bug#11427

Open

joroKr21 mentioned this pull request Jan 6, 2021

HK unification of anonymous type aliases during implicit resolution scala/bug#10617

Closed

joroKr21 mentioned this pull request Jul 18, 2022

Resolution of given instances for nested type constructors scala/scala3#15344

Open

	// Then define remaining type variables from argument types.
	map2(argtpes, formals) { (argtpe, formal) =>
	val tp1 = argtpe.deconst.instantiateTypeParams(tparams, tvars)
	val pt1 = formal.instantiateTypeParams(tparams, tvars)

	// Note that isCompatible side-effects: subtype checks involving typevars
	// are recorded in the typevar's bounds (see TypeConstraint)
	if (!isCompatible(tp1, pt1)) {
	throw new DeferredNoInstance(() =>
	"argument expression's type is not compatible with formal parameter type" + foundReqMsg(tp1, pt1))
	}
	}
	val targs = solvedTypes(tvars, tparams, tparams map varianceInTypes(formals), upper = false, lubDepth(formals) max lubDepth(argtpes))

Higher-kinded type variable unification. #6069

Higher-kinded type variable unification. #6069

Conversation

TomasMikula commented Sep 11, 2017 • edited by adriaanm Loading

TomasMikula commented Sep 12, 2017 • edited Loading

lrytz commented Sep 12, 2017

TomasMikula commented Sep 12, 2017

lrytz commented Sep 12, 2017

TomasMikula commented Sep 12, 2017

non commented Sep 12, 2017

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

TomasMikula commented Sep 14, 2017

Atry commented Sep 19, 2017

TomasMikula commented Sep 19, 2017

adriaanm left a 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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

TomasMikula Sep 26, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adriaanm commented Sep 27, 2017

TomasMikula commented Sep 27, 2017

TomasMikula commented Sep 27, 2017 • edited Loading

TomasMikula commented Sep 28, 2017

adriaanm commented Sep 28, 2017 • edited Loading

TomasMikula commented Sep 28, 2017

adriaanm left a comment

Choose a reason for hiding this comment

adriaanm commented Sep 29, 2017 • edited Loading

TomasMikula commented Sep 29, 2017 • edited Loading

joroKr21 commented Dec 27, 2018

Choose a reason for hiding this comment

TomasMikula commented Sep 11, 2017 •

edited by adriaanm

Loading

TomasMikula commented Sep 12, 2017 •

edited

Loading

TomasMikula Sep 26, 2017 •

edited

Loading

TomasMikula commented Sep 27, 2017 •

edited

Loading

adriaanm commented Sep 28, 2017 •

edited

Loading

adriaanm commented Sep 29, 2017 •

edited

Loading

TomasMikula commented Sep 29, 2017 •

edited

Loading