Fix #6687: handle gadt bounds in match type reduction

[OlivierBlanvillain]

on top of #7364

Handling GADT bounds in the match type reduction algorithm turns out to be relatively straightforward, it boils down to adding two extra cases in provablyDisjoint as done in the last commit cd55b20.

However doing so requires to get rid of the widenAbstractTypes check, as this check can preemptively rule out pair of types that can be proved disjoint using GADT information. I believe after #7364 this check is redundant and can therefore be removed entierly, as done in the "Simplify MT reduction algorithm" commit.

Remove that check uncovered another bug in the provablyDisjoint algorithm which is fixed in the "Use .superType instead of .underlying" commit. Using underlying was incorrect as it can change the kind of types, and thus lead to an incorrect conclusion. To paraphrase the example from the commit message, in master it was possible to come to the erroneous conclusion that f[Dummy] (for some type f) and Int are disjoint. The issue came from the fact that .underlying on f[Dummy] returns a type lambda which is kind incompatible with Int. The fix is to use .superType which properly preserves kinds.

That bug was exploited in tests/run-macros/tasty-simplified/quoted_2.scala (from @milessabin) in the Appy/Unapply pattern. I hope this pattern isn't a crucial piece of shapeless, because it breaks with this PR, and (probably) can't be fixed with the current match type semantics.

[milessabin]

@OlivierBlanvillain as things stand that Apply/Unapply trick is important.

I'd be happy to replace if there's a suitable alternative now. Can you suggest a approach which will work after this PR?

[OlivierBlanvillain]

@milessabin I'll to think about it but it might help to have a bit more context, where/why do you need that trick?

I have a feeling that there might be something fundamentally impossible about what this Unapply is trying to achieve. It's trying to tell appart HKT from ground type, but every ground type X can me made to match f[Dummy] with type f[a] = X...

[odersky]

The changes look good to me. I agree that it must be superType instead of underlying. We should dig deeper what we need to do to recover shapeless compilation.

[milessabin]

The version for kind * -> * (there are similar versions for other kinds) in shapeless looks like this,

type Id[t] = t
type Const[c] = [t] =>> c

case class Wrap[T](t: T)

class Dummy
type Apply[T[_]] = T[Dummy]
type Unapply[F[_[_]], T] = T match {
  case Wrap[Apply[a]] => F[a]
  case Wrap[Dummy] => F[Id]
  case Wrap[c] => F[Const[c]]
}

type LiftP[F[_[_]], T[_]] = LiftP0[F, Apply[T]]

type LiftP0[F[_[_]], T] <: Tuple = T match {
  case Unit => Unit
  case (a *:  b) => Unapply[F, Wrap[a]] *: LiftP0[F, b]
}

The idea is that given,

trait Functor[_[_]]

type Repr[t] = (Option[t], t, Int)

we should have,

LiftP[Functor, Repr] =:= (Functor[Option], Functor[Id], Functor[Const[Int]])

This works very nicely prior to this PR, and could be encoded at the term level using givens.

I'd be happy to use any mechanism which allowed me to express this at the type level without the need for intermediary terms.

[milessabin]

As an addendum to my previous comment, I have no particular attachment to the Apply/Unapply/Wrap trick. It was a workaround in an attempt to achieve what I had hoped would be possible with,

type Unapply[F[_[_]], T[_]] = T[Dummy] match {
  case Dummy => F[Id]
  case a[Dummy] => F[a]
  case c => F[Const[c]]
}

Clearly for this to work matches would have to be sequential and potentially overlapping, and we would also have to refuse to instantiate a to Const[t].

I think there's a good case for sequential and overlapping match semantics, if only to keep alignment between term and type matches.

I see that preventing a from being instantiated to Const[t] in the second case looks more problematic, but this is an important kind of match, with wide applicability. Perhaps we could support it via built in "type extractors", eg. Apply below,

type Unapply[F[_[_]], T[_]] = T[Dummy] match {
  case Dummy => F[Id]
  case Apply[a, Dummy] => F[a]
  case c => F[Const[c]]
}

[OlivierBlanvillain]

and we would also have to refuse to instantiate a to Const[t].

What about teaching to the compiler to do exactly that?

In

T[Dummy] match {
  case Dummy => F[Id]
  case a[Dummy] => F[a]
  case c => F[Const[c]]
}

If a is instantiate to Const[t] as a fallback, then the 2rd case would simply subsume the 3rd one!

[milessabin]

If a is instantiate to Const[t] as a fallback, then the 2rd case would simply subsume the 3rd one!

That certainly works in this case.

[milessabin]

That certainly works in this case.

Indeed, I can imagine you could also arrange for the compiler to instantiate a to Id.

But, and it's a big but, this is just one example for one kind. In shapeless we need this to be either open to the addition of support for additional kinds by users (what we have now), or generalized for all kinds.

To give a flavour of this, the following are the equivalents for kinds (* -> *) -> * and * -> * -> *, which are both included in shapeless and support derivation of type classes corresponding to those shapes (FunctorK and Bifunctor for example),

// (* -> *) -> *

type Id[t] = [f[_]] =>> f[t]
type Const[c] = [f[_]] =>> c

class Dummy[T]
type Apply[T[_[_]]] = T[Dummy]
type Unapply[F[_[_[_]]], T] = T match {
  case Wrap[Apply[a]] => F[a]
  case Wrap[Dummy[a]] => F[Id[a]]
  case Wrap[c] => F[Const[c]]
}

type LiftP[F[_[_[_]]], T[_[_]]] = LiftP0[F, Apply[T]]

type LiftP0[F[_[_[_]]], T] <: Tuple = T match {
  case Unit => Unit
  case (a *:  b) => Unapply[F, Wrap[a]] *: LiftP0[F, b]
}

// * -> * -> *

type Id1[t, u] = t
type Id2[t, u] = u
type Const[c] = [t, u] =>> c

class Dummy1
class Dummy2
type Apply[T[_, _]] = T[Dummy1, Dummy2]
type Unapply[F[_[_, _]], T] = T match {
  case Wrap[Apply[a]] => F[a]
  case Wrap[Dummy1] => F[Id1]
  case Wrap[Dummy2] => F[Id2]
  case Wrap[c] => F[Const[c]]
}

type LiftP[F[_[_, _]], T[_, _]] = LiftP0[F, Apply[T]]

type LiftP0[F[_[_, _]], T] <: Tuple = T match {
  case Unit => Unit
  case (a *:  b) => Unapply[F, Wrap[a]] *: LiftP0[F, b]
}

Note that the kinds of Id and Const change to match the kind of the type we're trying to extract.

I think this can be automated in a principled way, but it's not quite as straightforward as the * -> * case might suggest.

[OlivierBlanvillain]

Indeed, I can imagine you could also arrange for the compiler to instantiate a to Id.

Yes, but not that case, Id[Int] wouldn't match a[Dummy].

But, and it's a big but, this is just one example for one kind.
I think this can be automated in a principled way, but it's not quite as straightforward as the * -> * case might suggest.

I see. So, to support these other kinds, all we need would be the ability to synthesize Const of the corresponding kind, or I'm I missing something?

I'm going to spend a bit more time trying to convince TypeComparer of doing that... But it turns out too complicated, what do you think about these alternatives:

1. Fallback to implicit search for that computation.

2. Change the type of Repr to some sort of HK tuple, removing the need for Unapply altogether: (I belive this is what they are doing in GHC)

   type Repr = Tuple3K(Option, [X] =>> X, [X] =>> Int)

[milessabin]

So, to support these other kinds, all we need would be the ability to synthesize Const of the corresponding kind, or I'm I missing something?

That sounds about right.

But it turns out too complicated, what do you think about these alternatives

1. It would be a shame to have to fall back to implicit search here. Aside from anything else, requiring a term really complicates things in many situations.

2. No, that's not viable: there's an open ended set of kinds we would need to support and that can't be handled with a fixed budget of of TupleXxx's. I've experimented with this sort of approach in the past, and it gets very unpleasant very quickly.

Another fallback idea: all we're really trying to do here is split a type into a non-trivial application of a type constructor to a type. If it's too complicated to bake this into TypeComparers could we make a poly-kinded Apply/Unapply a primitive match type?

[OlivierBlanvillain]

Having Apply/Unapply as a primitive sounds like the best option.

The fact that type Apply[a[_]] = a[Dummy] can be used to emulate case a[Dummy] => almost feels like a bug (or a miracle depending on how you look at it 😛), so I'm not very confortable building things on top of that...

[milessabin]

Thanks for the rebase ...

I think something like the following is the primitive we need: a pair of kind-polymorphic match types Head and Tail which are able to get under the binder of any lambda type which has a Tuple result type, each yielding a lambda type of the same kind. This can be done fairly straightforwardly in the compiler, but isn't possible using the Apply/Unapply trick after this PR.

object Test {
  // Simulation of primitive kind-polymorphic Head/Tail for kind * -> *

  class Apply1[F[_]]

  // hard-coded types for illustration only
  type P0 = [t] =>> (t, List[t], Int)
  type P1 = [t] =>> (List[t], Int)
  type P2 = [t] =>> Tuple1[Int]

  type Head[F[_]] <: ([t] =>> Any) = Apply1[F] match {
    case Apply1[P0] => [t] =>> t
    case Apply1[P1] => List
    case Apply1[P2] => [t] =>> Int
  }

  type Tail[F[_]] <: ([t] =>> Any) = Apply1[F] match {
    case Apply1[P0] => P1
    case Apply1[P1] => P2
    case Apply1[P2] => [t] =>> Unit
  }

  // shapeless library code

  type Id[t] = t
  type Const[C] = [t] =>> C

  type Nil = [t] =>> Unit

  type LiftP[F[_[_]], T[_]] <: Tuple = Apply1[T] match {
    case Apply1[Nil] => Unit
    case _ => F[Head[T]] *: LiftP[F, Tail[T]]
  }

  // shapeless client code

  trait Functor[F[_]]

  type Repr[t] = (t, List[t], Int)

  summon[LiftP[Functor, Repr] =:= (Functor[Id], Functor[List], Functor[Const[Int]])]
}

[abgruszecki]

Instead of creating special HeadPK and TailPK primitive match types (Head and Tail from Miles' post above), I think it would be feasible to instead have a LiftPK primitive (lift poly-kinded)
which allows lifting any type operator of kind * -> * to operate on types of arbitrary kinds, and thus allows defining HeadPK and TailPK. The benefit is that LiftPK allows making all type operators poly-kinded, instead of special-casing Head and Tail, and doesn't seem significantly harder to define. It would behave as follows:

type LiftPK[_[_]] = ... // compiler-provided
type HeadPK[t] = LiftPK[Head][t] // consistent behaviour with Miles' Head
Head[(1,2,3)] === 1
HeadPK[(1,2,3)] === 1
HeadPK[[t] => (t, 2, 3)]] === [t] => t
type TailPK[t] = LiftPK[Tail][t] // similarly, has behaviour consistent with Tail from the preceding post

As for compiler implementation (and probably as a reminer for @OlivierBlanvillain), LiftPK should be implementable by inventing an abstract type for each type parameter, replacing type parameter references with those types, reducing match type (if there's any to be reduced) and undoing the type parameter substitution.

[milessabin]

This appears to be commenting out roughly 3/4 of shapeless (ie. pretty much everything higher-kinded) to pass the community build.

If we go down the LiftPK primitive route suggested by @abgruszecki above I'd try and find the time to adapt shapeless to that approach. But if we don't, and there's no other workaround available, then I don't think there's a great deal of point in continuing to have shapeless in the community build.

[OlivierBlanvillain]

The situation is the same as it was one year ago when we first discussed it on this PR. To summarize, this PR uncovered a soundness bug in match type reduction. Unfortunately, shapeless3 heavily relies on the unsoundness in its Unapply match type that's needed for higher kinded type class derivation. There is no easy fix here; even with dedicated compiler support we would need substantial rework on the shapeless3 side.

I don't think the work on a new primitive type-level lifting operator belongs to this PR. I also think this work should be done in conjunction with the shapeless3 changes, or we risk ending up with a new very advanced type operator that doesn't serve its primary purpose...

From a dotty perspective, there is still value in what's left of shapeless tests after the breakage: type class derivation for Monoid, Eq, Show and Read using a bunch of under-tested constructs: inline givens, inline matches, by name implicits, summonFrom, constValue, and the tasty reflect API.

[mpilquist]

My 2 cents from open source ecosystem perspective: given the substantial impact to Shapeless and the timeline for 3.0.0 RC1, this PR should be deferred until a suitable alternative is developed and integrated with Shapeless 3. If that can fit in before 3.0.0 RC1, great, but otherwise should be deferred.

[OlivierBlanvillain]

Is the ecosystem already depending on shapeless3? I think it was a mistake not to merge this a year ago and delaying it any further just makes the situation worse.

One compromise to move forward is to keep the unsound behavior under a -Y flag to ease the transition, I can try to update my PR with that if that helps...

[djspiewak]

I agree that the soundness hole should be plugged, and the way that Shapeless is exploiting it is definitely unsound even at a glance. However, it's worth putting in the effort to provide sound functionality which serves the same purpose.

While Shapeless 3 is not yet heavily depended upon by the Scala 3 ecosystem, it is representative of most of the things that are required to apply Scala 3's metaprogramming capabilities to useful problems. Libraries like Circe and Scodec have, in practice, re-tread the same paths in numerous ways. As the ecosystem expands and more higher-kinded applications of the system are attempted, the limitation encoded here, without the amelioration of something like LiftPK, will inevitably become quite crippling.

I would invite everyone to view this less in terms of "crippling one library" and more in terms of "removing fundamental functionality from the language which is necessary to apply a core feature (metaprogramming) in a general fashion". The fact that Shapeless is the only current member of the ecosystem which uses that fundamental functionality is representative of adoption stage of the language, not representative of significance.

[b-studios]

@OlivierBlanvillain @milessabin Do I understand correctly that explicitly representing shapes and interpreting them would still work with this PR?

sealed trait Shape
class ID extends Shape
class CONST[t] extends Shape
class APP[f[_]] extends Shape

type Id[t] = t
type Const[c] = [t] =>> c

type Interp[F[_[_]], T <: Shape] = T match {
  case ID => F[Id]
  case CONST[t] => F[Const[t]]
  case APP[g] => F[g]
}

type LiftP[F[_[_]], T] <: Tuple = T match {
  case EmptyTuple => EmptyTuple
  case (a *: b) => Interp[F, a] *: LiftP[F, b]    
}

// user code
trait Functor[F[_]]

// Now Repr is of kind *
type Repr = (APP[Option], ID, CONST[Int])

implicitly[LiftP[Functor, Repr] =:= (Functor[Option], Functor[Id], Functor[Const[Int]])]

[LPTK]

@b-studios I don't know if this fits all the use cases in shapeless, but it seems by far to be the cleanest option!

Maybe a possible alternative could be to rely on implicit search and inline definitions, which have been shown to work in some cases. For instance, when ctx is an inline implicit function which returns a singleton type, one can write things like ctx.T inside types even though ctx is not a stable path but a function – as there are no unstable paths left after implicit search and inlining...

[milessabin]

@b-studios the problem is with your suggested,

// Now Repr is of kind *
type Repr = (APP[Option], ID, CONST[Int])

and this explains why this change is crippling for Dotty's type class derivation infrastructure.

Mirrors define these Repr types for all possible representation shapes, for instance the representation type for case class Foo[T](Option[T], T, Int) is,

type MirroredElemTypes[t] = (Option[t], t, Int)

We could only rewrite this in the form you're suggesting if we added those wrapper types to the standard library and, (literally) infinitely worse, all the additional wrapper types needed for all possible product type constructor signatures.

I was very careful in the design of Dotty's mirrors to ensure that such an explosion would be unnecessary. The ability to define something like LiftPK or, failing that, have it as a primitive, was absolutely critical in that. shapeless 3 in the community build has been a guarantee that this continues to be the case.

To be clear, this doesn't merely do significant damage to shapeless 3, it also severely compromises Scala 3's type class derivation infrastructure.

[abgruszecki]

I, uh, am not entirely convinced that being able to switch to an unsound match type reduction algorithm with a -Y flag is the best of approaches. In particular, all Shapeless3 users would need to opt into that flag to make use of HK features (if I understand correctly), and seeing as that'd make them use an unsound match type reduction algorithm, that's not very good.

I think it's important that we ensure Shapeless3 is working and functional when we finally release Scala 3, and there's still the possibility of adding a primitive like LiftPK. I agree with @OlivierBlanvillain that we should work on the new primitive together with updating Shapeless, to ensure that the primitive is actually useful. A good point to start would be actually implementing the primitive in the compiler. I checked the implementation of match types and I think what I suggested a year ago is still feasible and shouldn't be too difficult to implement. That is, LiftPK[M, T] can be implemented more-or-less just by going under every TypeLambda binder in T while replacing each parameter with a freshly invented abstract type (which gives us the "terminal" type T'), then trying to reduce M[T'], and if successful, reversing the going-under-binders operation. A remaining question is how much work would be necessary to update Shapeless3 to LiftPK.

[milessabin]

A remaining question is how much work would be necessary to update Shapeless3 to LiftPK.

Not a huge amount. Shapeless has rough equivalents to LiftPK for each of the kinds it handles, implemented in terms of the unsound match types. With any luck it should be possible to simply remove them and replace their uses with LiftPK.

If I have the primitive I can find the time to do that.

[OlivierBlanvillain]

That all sounds good to me, but I don't think the work on LiftPK/shapeless3 should be a blocker to fix the soundness bug in question. (I will open an issue to continue the LiftPK discussion)

To reiterate, the compiler is currently broken and the more we wait, the worse things get since more and more users might depend on the current unsound behavior. This is also getting rather annoying to maintain; I've already rebased this PR multiple times, and every time I minimize a match type issue, I have to checkout this branch to see if the bug still exists here.

@abgruszecki To be clear, the added Y flag is not a long term solution and is not intended to be used by anyone but shapeless3 in the community build. It is merely a compromise to move forward with the PR without losing the benefits of compiling the shapeless3 prototype on every PR. There is also the option of releasing a broken compiler and delaying the fix every further, potentially hindering every match type user, is this what people are suggesting?

[smarter]

To be clear, the added Y flag is not a long term solution and is not intended to be used by anyone but shapeless3 in the community build.

I think the problem mentioned by @abgruszecki is that if shapeless needs this flag to compile, then users of shapeless will also need that flag to use its match types, so it will propagate through the ecosystem.

[abgruszecki]

To be clear, the added Y flag is not a long term solution and is not intended to be used by anyone but shapeless3 in the community build.

I think the problem mentioned by @abgruszecki is that if shapeless needs this flag to compile, then users of shapeless will also need that flag to use its match types, so it will propagate through the ecosystem.

Yes, that's basically it. If the flag is not intended to be a long-term solution, then how long do we intend to keep it? It seems dangerous to me to even have it in M3, though rather less dangerous than having unsound match types.

I just think that it's important that we commit somehow to ensuring that both Shapeless3 and typeclass derivation are at their best for the final Scala3 release.

[OlivierBlanvillain]

@smarter @abgruszecki If you are not convinced about the Y flag then I'll go back to my original proposal with commented out tests. Since I started reviving this PR I already got 3 different conflicts on the shapeless submodule, so there is clearly a lot of value of keeping it there as it is.

[OlivierBlanvillain]

After further discussion we decided to merge this PR with the Y flag, knowing that this is only a temporary solution and the flag will be removed by the 3.0 release. The work on the LiftPK operator is high priority since it is a blocker for Miles to do the corresponding rework in shapeless3.