Skip to content
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

Correct bounds for higher-kinded GADT skolems #9417

Merged
merged 2 commits into from Jan 6, 2021

Conversation

joroKr21
Copy link
Member

@joroKr21 joroKr21 commented Dec 29, 2020

Fixes scala/bug#12295
@xuwei-k can you check if this fixes scala/bug#11692?

@scala-jenkins scala-jenkins added this to the 2.13.5 milestone Dec 29, 2020
@joroKr21

This comment has been minimized.

@joroKr21 joroKr21 marked this pull request as ready for review December 29, 2020 14:06
@diesalbla
Copy link
Contributor

Is there a way to try this out before the binary release 2.13.5? In fs2 we have quite a few "work-arounds" to avoid compiler's bugs with pattern-matching Higher-Kinded covariant types. That could be quite a testbed.

@joroKr21
Copy link
Member Author

joroKr21 commented Dec 29, 2020

It's described here: https://github.com/scala/scala#scala-ci

You can use Scala builds in the validation repository locally by adding a resolver and specifying the corresponding scalaVersion:

$ sbt
> set resolvers += "pr" at "https://scala-ci.typesafe.com/artifactory/scala-pr-validation-snapshots/"
> set scalaVersion := "2.12.2-bin-abcd123-SNAPSHOT"
> console

So this one: https://scala-ci.typesafe.com/artifactory/scala-pr-validation-snapshots/org/scala-lang/scala-compiler/2.13.5-bin-69b04d1-SNAPSHOT/

@joroKr21 joroKr21 force-pushed the hk-skolems branch 2 times, most recently from c2c42ec to 51c04ee Compare December 29, 2020 18:08
@SethTisue
Copy link
Member

@SethTisue
Copy link
Member

@xuwei-k have you had a chance yet to consider @joroKr21's question?

@SethTisue
Copy link
Member

@diesalbla agree that sounds like a good testbed – let us know if you're able to try it

@dwijnand
Copy link
Member

dwijnand commented Jan 5, 2021

@joroKr21 so, knowing next to nothing about these parts of the compiler, how come in one case you genPolyType and then apply it and in the other case just genPolyType?

@joroKr21
Copy link
Member Author

joroKr21 commented Jan 5, 2021

In fs2 we have quite a few "work-arounds" to avoid compiler's bugs with pattern-matching Higher-Kinded covariant types.

@diesalbla, just by looking at source code of fs2 I'm not able to find the workarounds you mentioned.
Someone more familiar with the code base might have more success.

@SethTisue awesome, thank you 🙏

@xuwei-k have you had a chance yet to consider @joroKr21's question?

Actually if the branch with the reproduction is still there, I can check that too.

knowing next to nothing about these parts of the compiler, how come in one case you genPolyType and then apply it and in the other case just genPolyType?

@dwijnand good question, I want to try something and get back to you

@diesalbla
Copy link
Contributor

@diesalbla, just by looking at source code of fs2 I'm not able to find the workarounds you mentioned.
Someone more familiar with the code base might have more success.

Mostly on the develop branch, not the main branch. Several extra type variables and asInstanceOf conversions... https://github.com/typelevel/fs2/blob/develop/core/shared/src/main/scala/fs2/Pull.scala#L938-L992

I refer to having to use extra variables for the types and a few asInstanceOf conversions... and sometimes we get a Kinding errors, if it infers that the new type variable has kind * where it should have inferred [_]...

Will try to report on specific errors (or minimise that code), but don't let that delay you from merging this one 🙂

@joroKr21
Copy link
Member Author

joroKr21 commented Jan 5, 2021

@dwijnand to build some intuition about how types work I like to fiddle with the console in :power mode:

class Foo[F[x] <: Seq[x]]
val f = symbolOf[Foo[List]].typeParams.head

Here are some interesting things you can try:

Expression Result getClass Explanation
f.tpe F[x] TypeRef Same as tpe_* - applied to dummy args if higher-kinded
f.tpeHK F TypeRef Unlike tpe and tpe_* - preserves the kind
f.info [x] <: Seq[x] PolyType For a HKT parameter this is params -> bounds
f.tpe.bounds <: Seq[x] TypeBounds Unsurprisingly, the dummy args carry under
f.tpeHK.bounds <: Seq[x] TypeBounds ❌ Bad (until now) - kind is lost
f.tpeHK.bounds <: [x]Seq[x] TypeBounds ✅ Ok (this branch) - kind carries under
f.info.bounds <: [x]Seq[x] TypeBounds Kind carries under PolyType
f.tpe.lowerBound Nothing TypeRef
f.tpe.upperBound Seq[x] TypeRef
f.tpeHK.lowerBound Nothing TypeRef ❌ Bad (until now) - kind is lost
f.tpeHK.lowerBound [x]Nothing PolyType ✅ Ok (this branch) - kind carries under
f.tpeHK.upperBound Seq[x] TypeRef ❌ Bad (until now) - kind is lost
f.tpeHK.upperBound [x]Seq[x] PolyType ✅ Ok (this branch) - kind carries under
f.info.lowerBound [x]Nothing PolyType Kind carries under PolyType
f.info.upperBound [x]Seq[x] PolyType Kind carries under PolyType

Things to note:

  • TypeRef of a HKT without type arguments should be equivalent to its eta-expansion (a PolyType):
    i.e. f should be equivalent to f.etaExpand (in types: F =:= [x]F[x])
  • Taking the bounds of equivalent types should yield equivalent bounds
  • We also learned that the kind carries under PolyType when we take its bounds.
    Therefore the type should also carry under f.tpeHK - thus the relativeInfo change.
  • .bounds return TypeBounds - but they are not suitable as the info of a higher-kinded type symbol.
    For example f.info.bounds return TypeBounds with PolyTypes as lo and hi.
    Therefore we need to use PolyType to construct the info of a higher-kinded GADT skolem.

Sorry if that is too long, it helped me to do this systematically.

@joroKr21
Copy link
Member Author

joroKr21 commented Jan 6, 2021

TypeRef of a HKT without type arguments should be equivalent to its eta-expansion (a PolyType):
i.e. f should be equivalent to f.etaExpand (in types: F =:= [x]F[x])

case in point: scala/scala3#9566

@dwijnand
Copy link
Member

dwijnand commented Jan 6, 2021

Sorry if that is too long, it helped me to do this systematically.

Not at all - it was very helpful, thank you.

@dwijnand
Copy link
Member

dwijnand commented Jan 6, 2021

queued: scala-ci.typesafe.com/job/scala-2.13.x-jdk11-integrate-community-build/2344

Seth aborted that (I assume b/c of the disk space issues) and rescheduled it as https://scala-ci.typesafe.com/job/scala-2.13.x-jdk11-integrate-community-build/2346/ (and it's still not finished, 5 hours in).

But that's using the previous SHA, we need a run for the cd13abc: https://scala-ci.typesafe.com/job/scala-2.13.x-jdk11-integrate-community-build/2348/ (404 link until the build starts).

Copy link
Member

@dwijnand dwijnand left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM from my point of view, hopefully the community build comes back clean.

@diesalbla
Copy link
Contributor

Let's go ahead to the next phase. If something fails we can revert later on.

@diesalbla diesalbla merged commit b049775 into scala:2.13.x Jan 6, 2021
@joroKr21 joroKr21 deleted the hk-skolems branch January 6, 2021 13:27
@dwijnand
Copy link
Member

dwijnand commented Jan 6, 2021

I would have preferred to wait for the confirmation first, that's what I implied. I wish GitHub's review had a task completion system... Perhaps I should approve less readily to avoid miscommunicating.

@SethTisue
Copy link
Member

SethTisue commented Jan 6, 2021

The failures in 2346 are known-intermittent, so it's a "green enough" run.

2348 is still running.

@joroKr21
Copy link
Member Author

joroKr21 commented Jan 6, 2021

@xuwei-k can you check if this fixes scala/bug#11692?

I checked that and it works btw 🎉

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
5 participants