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

SIP-56: Better foundations for match types #18262

Merged
merged 17 commits into from
Dec 18, 2023

Conversation

sjrd
Copy link
Member

@sjrd sjrd commented Jul 21, 2023

@sjrd sjrd self-assigned this Jul 24, 2023
@sjrd sjrd force-pushed the better-foundations-for-match-types branch 7 times, most recently from 8c754e6 to f0339b3 Compare August 10, 2023 09:21
@sjrd sjrd changed the title WiP: Better foundations for match types SIP-56: Better foundations for match types Aug 14, 2023
@sjrd sjrd force-pushed the better-foundations-for-match-types branch from c88d23a to aea28b9 Compare August 15, 2023 09:44
@sjrd sjrd force-pushed the better-foundations-for-match-types branch from aea28b9 to fa9f3ad Compare August 31, 2023 13:27
@sjrd sjrd force-pushed the better-foundations-for-match-types branch from fa9f3ad to f45738c Compare August 31, 2023 13:46
@soronpo
Copy link
Contributor

soronpo commented Aug 31, 2023

@sjrd Can you please take a look at this example that yields a recursion limit error (this doesn't work also on the current match type system)?

type TupleOfRecur[T, UB, Orig] = T match
  case EmptyTuple => Orig
  case UB *: xs => TupleOfRecur[xs, UB, Orig]
  case _ => Nothing
type TupleOf[T, UB] = TupleOfRecur[T, UB, T]

def tupleOfInt[T, Check >: T <: TupleOf[T, Int]](t: T): T = t

val ok = tupleOfInt((1, 2, 3)) //should compile
val err = tupleOfInt((1, 2, "three")) //should fail compilation

This was an attempt of mine to make an upper bound check for tuple contents.
I actually was successful, using a slightly modified version.

sealed trait TupleCheck
type TupleOfRecur[T, UB, Orig] = T match
  case EmptyTuple => TupleCheck
  case UB *: xs => TupleOfRecur[xs, UB, Orig]
  case _ => Nothing

type TupleOf[T, UB] = TupleOfRecur[T, UB, T]

def foo[T, __ >: TupleCheck <: TupleOf[T, Int]](t: T): T = t

val ok = foo((1, 2, 3)) //compiles
val err = foo((1, 2, "three")) //error: Type argument TupleCheck does not conform to upper bound TupleOf[(Int, Int, String), Int]

@sjrd
Copy link
Member Author

sjrd commented Sep 1, 2023

That still doesn't work. But I think it is legit that it does not. The recursion includes trying prove T disjoint from EmptyTuple. But T from def tupleOfInt is upper-bounded by TupleOf[T, Int]. So to prove disjointness, according to the rules for ⌈X⌉, it tries to reduce TupleOf[T, Int]. But to do that, it needs to prove disjointness between T and EmptyTuple. etc.

This is a legit cyclic reference to me. Even as a human I don't see how to cut the recursion short. We have to attempt to prove disjointness.

@sjrd sjrd force-pushed the better-foundations-for-match-types branch 4 times, most recently from 90dce88 to a7d3e79 Compare September 7, 2023 12:27
@sjrd sjrd force-pushed the better-foundations-for-match-types branch 2 times, most recently from a9696ac to e248076 Compare November 24, 2023 16:17
@sjrd sjrd marked this pull request as ready for review November 24, 2023 16:20
@sjrd sjrd requested review from dwijnand and odersky November 24, 2023 16:21
@sjrd sjrd assigned dwijnand and odersky and unassigned sjrd Nov 24, 2023
@sjrd
Copy link
Member Author

sjrd commented Nov 24, 2023

This is now ready for review. 🎉 The SIP was approved for the design stage, and I rebased and cleaned up everything.

@WojciechMazur Could you please run an Open Community Build based on this PR?

@WojciechMazur
Copy link
Contributor

WojciechMazur commented Nov 25, 2023

There seems to be plenty of new comilation errors in community build when compared with the last nightly version - 3.4.0-RC1-bin-20231123-00e9e6b-NIGHTLY:

Project Version Build URL Notes
7mind/izumi -> 1.2.3 Open CB logs value == in class Int does not take parameters
avast/scala-server-toolkit 0.18.4 Open CB logs value == in class Int does not take parameters
avokka/avokka 0.0.8 Open CB logs value == in class Int does not take parameters
geirolz/toolkit 0.0.11 Open CB logs value == in class Int does not take parameters
kevin-lee/openai4s 0.1.0-alpha6 Open CB logs value == in class Int does not take parameters
permutive-engineering/functional-google-clients 1.0.0-RC2 Open CB logs value == in class Int does not take parameters
typebricks/pureconfig-toggleable 1.0.0 Open CB logs value == in class Int does not take parameters
fingo/spata 3.1.0 Open CB logs Mismatch error
foldables-io/skunk-tables 0.0.2 Open CB logs The match type contains an illegal case
iheartradio/ficus 1.5.2 Open CB logs The match type contains an illegal case
kory33/s2mc-test 0.2.3 Open CB logs The match type contains an illegal case
joan38/kubernetes-client 0.10.0 Open CB logs mill build issue?
johnhungerford/generic-schema 1.2.0 Open CB logs Mismatch error
kordyjan/pytanie 0.1.7 Open CB logs Recursion limit exceeded
scalanlp/breeze 2.1.0 Open CB logs java.lang.StackOverflowError

Some of failures I've checked might be expected, eg. in iheartradio/ficus or kory33/s2mc-test we get the following error:

Error:  6 |  type EnumValue[A <: Enumeration] = A match {
Error:    |                                     ^
Error:    |               The match type contains an illegal case:
Error:    |                   case net.ceedubs.ficus.util.EnumerationUtil.Aux[a] => a
Error:    |               (this error can be ignored for now with `-source:3.3`)
Error:  7 |    case Aux[a] => a
Error:  8 |  }

I'm not sure about some of the failures related to usage of @experimental, eg. 7mind/izumi, fmonniot/scala3mock. Unless there was something missing when building the compiler from the dotty-staging branch the created compiler should already be treated as experimental. I would check and adapt our compiler building workflow next time if necessary.

#Edit
The version of compiler build from sources had no SNAPSHOT/NIGHTLY substring though it was not treated as experimental. I would retry the build with this fix.

#Edit 2
Most of the @experimental issues were fixed, in 1 project 7mind/izumi there was found a compilation similar to other fund cases.

@sjrd sjrd force-pushed the better-foundations-for-match-types branch from fa6c198 to a089833 Compare December 15, 2023 13:33
sjrd added 17 commits December 18, 2023 20:10
For now, we only have `SubTypeTest` and `LegacyPatMat`.

* `SubTypeTest` is used when there is no type capture.
* `LegacyPatMat` is used when there are captures.

In the match type reduction algorithm, we already have a simpler
path for `SubTypeTest`.

The `LegacyPatMat` path is basically the same as before, but with
static knowledge that we have an `HKTypeLambda`.
This is the first step in using the new specified algorithm for
match type reduction. When the pattern of a case satisfies
elibility conditions, we use the new algorithm. Otherwise, we fall
back on the legacy algorithm.

To be eligible, a pattern with at least one capture must be:
an applied *class* type constructor whose arguments are all:
- either a type capture,
- or a fully defined type that contains no inner capture,
- or the argument must be in covariant position and recursively
  qualify to the elibility conditions.

With those criteria, all the type captures can be *computed* using
`baseType`, instead of inferred through the full `TypeComparer`
machinery.

The new algorithm directly handles preventing widening abstract
types, when doing so leads to captures being under-defined. With
the legacy algorithm, this prevention is scattered elsewhere in
the type comparer. Making it centralized improves the error
messages in those situations; it seems they were previously
entirely misleading (see changed check files).
So that they do not fall into the legacy fallback.
An abstract tycon can be matched if it is exactly equal to the
scrutinee's tycon.
The error can be silenced with `-source:3.3`. In that case,
illegal match types are reduced using the legacy matching
algorithm, as before.
Previously the disjointnessBoundary of HKTypeLambda's was
implicitly their `resultType`, through the use of
`superTypeNormalized`. This was fine as long as both sides of
`provablyDisjoint` ended up being HKTypeLambda's at the same time,
but this may not always be the case (notably with any-kinded types).

It is safer to consider type lambdas as boundaries themselves, and
explicitly recurse on the result types when arities match.

This change surfaced a weird case in `TypeTestsCasts`, which called
`provablyDisjoint` with ill-kinded types. We now explicitly apply
what I suspect are partially-erased types to wildcards to recover
appropriate kinds.
… instead.

Fundamentally, the `provablyEmpty(scrut)` test was meant to prevent
situations where both `scrut <: pattern` and
`provablyDisjoint(scrut, pattern)` are true. That is a problem
because it allows a match type to reduce in two different ways
depending on the context.

Instead, we basically use that combination of `scrut <: pattern`
and `provablydisjoint(scrut, pattern)` as the *definition* for
`provablyEmpty`. When both those conditions arise together, we
refuse to reduce the match type.

This allows one example to pass that did not pass before, but that
particular example does not seem to cause unsoundness. In a sense,
`provablyEmpty` was too strong here.
This should improve consistency with the actual earlier compilers,
since it means the matching algorithm will be intact.

Note that the new behavior of `provablyDisjoint` is always applied,
even under `-source:3.3`. This includes using `provablyDisjoint`
instead of `provablyEmpty`. So it is still possible that something
behaves differently than the actual earlier compilers.
This was already done for `TypeApply` in
cecfb61. We apply the same logic
for `Apply` nodes.
And add an additional test for another cause of infinite recursion
that was fixed earlier.
This additional test demonstrates that relaxing the `isConcrete`
in a particular way around `AndType`s would also cause unsoundness.

This justifies new failures in the Open Community Build.
@sjrd sjrd force-pushed the better-foundations-for-match-types branch from a089833 to c3b9d9b Compare December 18, 2023 19:11
@sjrd sjrd enabled auto-merge December 18, 2023 19:12
@sjrd sjrd merged commit 881e945 into scala:main Dec 18, 2023
16 checks passed
@sjrd sjrd deleted the better-foundations-for-match-types branch December 18, 2023 20:25
@Kordyjan Kordyjan added this to the 3.4.0 milestone Dec 20, 2023
julianpeeters added a commit to julianpeeters/polynomial that referenced this pull request Jan 9, 2024
Type matches become more strict following scala/scala3#18262
tp.derivedAppliedType(
tycon,
targs.mapConserve(_.stripAnnots(keep = _.symbol.derivesFrom(defn.RefiningAnnotationClass)))
)
Copy link
Contributor

@olhotak olhotak Mar 5, 2024

Choose a reason for hiding this comment

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

@sjrd Is it supposed to be possible for the targs to be LazyRefs? If they are, the pending set would also fail since LazyRefs compare using reference equality. We could call stripLazyRef here.

I have LazyRefs showing up in a modified version of the compiler in an example with F-bounds, but I don't have a self-contained test case that would make them show up in the unmodified compiler. If it is indeed possible for them to show up, would you have any hints on constructing a test case? In general I have difficulty constructing test cases that even trigger provablyDisjoint to be called on a desired pair of types.

mbovel added a commit that referenced this pull request Oct 15, 2024
https://stackoverflow.com/q/68877939/21927647

Answer to the question:

> You were not doing anything wrong, this was an implementation
limitation.
>
> Your example compiles successfully since Scala 3.4, thanks to the
changes introduced in SIP-56 "Proper specification for match types"
([text](https://docs.scala-lang.org/sips/match-types-spec.html#:~:text=This%20SIP%20proposes%20a%20proper,the%20specification%20of%20the%20language.),
[PR](#18262)).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

7 participants