Pre-SIP : Proper Specification for Match Types

Opaque type aliases have a surprisingly small footprint in terms of specification. There is basically only one “if/then/else” in the memberType function of the spec that deals with opaque type aliases. When seen from the enclosing C.this prefix, their “underlying type definition” is the alias = U; and when seen from anywhere else, it is the bounds >: L <: H. That “underlying type definition” then feeds into subtyping and the match type reduction algorithm.

Concretely, that means opaque type aliases are almost always seen as abstract type members from the point of view of match types. In your particular case, when you look at RefinedTypeOps[Temperature], you really see RefinedTypeOps[>: Nothing <: Any]. And that can basically never reduce because >: Nothing <: Any is not a subtype of nor provablyDisjoint from any other proper type. If, through type substitution, you end up somewhere where Temperature is actually EnclosingPackageObject.this.Temperature, then you see the alias = RefinedType[Int, Positive] instead, and it will reduce.

We analyzed all public libs for now-illegal match cases. We did not test all public libs.

Excuse my imprecise wording.

I’ve meant with “testing” a test for “does it still reduce to the same type”. At least that’s how I’ve understood your “quantitative studies”.

The quantitative study only analyzed which match types would become illegal according to the proposed spec. We believe that reduction (of the remaining legal match types) won’t be affected except, but we have no proof of that.

Hmm, seeing some issues with implicits and match types which I assume is caused by this. Is this to be expected?

trait Foo[A, B <: Int]
object Foo:

  given [A](using m: Mirror.ProductOf[A]): Foo[A, Tuple.Size[m.MirroredElemTypes]] =
    new Foo[A, Tuple.Size[m.MirroredElemTypes]] {}

case class Bar(baz: String)

//No given instance of type Foo[Bar, (1 : Int)] was found for parameter x of method summon in object Predef
val t3: Foo[Bar, 1] = summon[Foo[Bar, 1]]

My actual usecase looks something more like this.

trait Ops[A]:
  type Index[B]
  def index[B](a: A, index: Index[B]): B

trait ExtraTypes[A]:
  type Index[B]
  type Names <: String
  type FieldOf[Name <: Names]

  def indexOf[Name <: Names](name: Name): Index[FieldOf[Name]]

extension [A](a: A)(
    using ops: Ops[A],
    types: ExtraTypes[A] {
      type Index[B] = ops.Index[B]
    }
)
  def foo[X <: types.Names](x: X): types.FieldOf[X] =
    ops.index(a, types.indexOf(x))

Ops used to contain what ExtraTypes contains, but those types are expensive to compute, and I’d rather not compute them unless needed.

If this is intended, are there any workarounds for this?

Could you elaborate what the relationship you see here? The provided snippet fails to compile on all of 3.2.1, 3.3.0, 3.3.1, dotty’s main branch right now and the branch where I implemented those new match types.

Ahh wait, missed that. Sorry. Guess it’s not related this this then

Today the SIP committee accepted this proposal to move into the implementation & experimental stage.
Congrats @sjrd !

6 Likes

It’s a proper Sebification.

5 Likes

The new spec disallows bounded type aliases:

type IsSeq[X <: Seq[Any]] = X

type TypeAliasWithBoundMT[X] = X match // error
  case IsSeq[t] => t

For a while I thought this could be a problematic limitation, but it seems we can in fact do without because we don’t check bounds in the rhs of match types:

class Wrap[S <: Int](x: S)

type WrapInt[X] = X match
  case Int => Wrap[X] // X is not upper-bounded by Int, but we don't check that here.
  case _ => X

type WrapIntInTuple[T <: Tuple] = T match
  case h *: t => WrapInt[h] *: WrapIntInTuple[t]

val x: WrapIntInTuple[(String, Int)] = ("foo", Wrap(1))

Can we rely on this behavior? If so, it should be spec’ed, otherwise, can we think of an alternative to this pattern? /cc @dwijnand @Decel

1 Like

What happens with the following:

class Wrap[S <: Int](x: S)

type WrapString[X] = X match
  case String => Wrap[X] // it is not true that X <: Int
  case _ => X

(I’d happily check it myself, but scastie is not working ?)

It typechecks, I thought the error would be reported at use-site when we reduce to the first case but it turns out this doesn’t happen right now:

class Wrap[S <: Int](x: S)

type WrapString[X] = X match
  case String => Wrap[X] // it is not true that X <: Int
  case _ => X
val x: WrapString[Double] = 1.0 // No error here (as I expected)
val y: WrapString[String] = ??? // No error here (but I would expect one)

For me it would make sense for it not to compile at all, could we add both these checks and X <: Int in the relevant branch ?

This is somewhat outside the specification effort of course.

The issue is that strict checks would affect expressiveness if we also take away matching on bounded type aliases, so I think both need to be considered together.

Could it be that since Nothing <: anything, the compiler doesn’t even reduce the match type ?

It was never intended not to be checked. @dwijnand has been working on checking these things. This is irrespective of this SIP because type bounds should always be checked. We would have needed dedicated spec text–or even just a hint in documentation–to justify not checking them there.

Expressiveness can always be recovered with a “type-level cast”, which is an intersection.

No, it happens even if Nothing isn’t involved: Scastie - An interactive playground for Scala.

Expressiveness can always be recovered with a “type-level cast”, which is an intersection.

Aha, thanks, intersections seem to do the trick indeed.

Update:
The PR has now been merged. From the next 3.4 nightly release the new Match Type implementation will take place. For the near future you can still use the “old” implementation under a -source:3.3 flag.

4 Likes

Amazing to hear !

Last week the SIP committee approved the Match Type Specification SIP, and it’s now a completed SIP. It will be shipped part of the 3.4.0 release.
Still known issues to be investigated:

  • Interactions with opaque types.
  • Interactions with type projections.
  • Better diagnostics.

Good work, and good luck!

6 Likes