Match types involving `Nothing` behave unexpectedly in some cases

Language Design
1

Consider this example match type from Jamie Thompson:

type Last[T] = T match
  case x *: EmptyTuple.type => x case _ *: xs => Last[xs]
  case _ *: xs              => Last[xs]

We expect

summon[Boolean =:= Last[Int *: String *: Boolean *: EmptyTuple.type]]

to return a witness since Boolean is the last type in the tuple type, and it does:

scala> summon[Boolean =:= Last[Int *: String *: Boolean *: EmptyTuple.type]]
val res32: Boolean =:= Boolean = generalized constraint

I would similarly expect

summon[Nothing =:= Last[Nothing *: EmptyTuple.type]]

to return a witness. There are several reasons to expect this besides the code of the match type. It could be my expectations are off, though. If there is something about the type system preventing this equality from being proved, we’d expect the message to be Cannot prove that Nothing =:= Last[Nothing *: EmptyTuple.type]. (Edit: I misspoke in my original post and wasn’t able to edit it till a moderator posted it, so I am going to edit a few spots to fix errors and clarify).

We do get the “cannot prove”, which I find puzzling. Additionally, the reason we are given has to do with Nothing being uninhabited preventing a reduction:

scala> summon[Nothing =:= Last[Nothing *: EmptyTuple.type]]
-- [E172] Type Error: ----------------------------------------------------------
1 |summon[Nothing =:= Last[Nothing *: EmptyTuple.type]]
  |                                                    ^
  |           Cannot prove that Nothing =:= Last[Nothing *: EmptyTuple.type].
  |
  |           Note: a match type could not be fully reduced:
  |
  |             trying to reduce  Last[Nothing *: EmptyTuple.type]
  |             failed since selector Nothing *: EmptyTuple.type
  |             is uninhabited (there are no values of that type).
1 error found

You also see unexpected behavior this way:

type N = Last[Nothing *: EmptyTuple.type]
summon[Nothing =:= N]

which results in

scala> summon[N =:= Nothing]
-- [E172] Type Error: ----------------------------------------------------------
1 |summon[Nothing =:= N]
  |                     ^
  |                     Cannot prove that Nothing =:= N.
1 error found

Referential transparency leads me to think that, at the very least, the behavior should be the same in both cases regardless of what that behavior turns out to be.

Lest one believe the complexity of the example is to blame, the following code results in the same error:

type NameOf[X] = X match
  case Int     => "Int"
  case String  => "String"
  case Nothing => "Nothing"
  case _       => "unknown"

summon[NameOf[Nothing] =:= "Nothing"]

while the corresponding summons for Int and String work as expected.

I don’t know enough about the scala internals to guess at the source of this error message, but taken at face value the message suggests match types only work as one might naively expect when the types involved are inhabited. I find this counterintuitive and difficult to explain. Is there a rationale for this behavior that I’m missing? Thanks!

Incidentally I ran the above with

#> scala-cli repl                                                                                                                                                                 
Welcome to Scala 3.8.3 (17, Java OpenJDK 64-Bit Server VM).
Type in expressions for evaluation. Or try :help.
2

I don’t know about the inhabited error message you get. From what I can see, you can construct match types on sealed traits without inhabitants fairly easily.

However, in your example you are also matching against Nothing. Nothing essentially extends all types, which also means match types containing it stop making sense. As the match type progresses, you are asking, “Does Nothing extend *:?“. Yes it does, but what will the match type then be invoked with? It just stops making sense.

Consider this type:

type IsNestedList[X] = X match
  case List[List[_]] => true
  case _             => false

What does IsNestedList[Nil.type] return?

3

Thanks for weighing in. I take your point, which is why I included the second example. NameOf below exhibits similar behavior that is counterintuitive to me:

type NameOf[X] = X match
  case Int     => "Int"
  case String  => "String"
  case Nothing => "Nothing"
  case _       => "unknown"

This summon:

summon[NameOf[Nothing] =:= "Nothing"]

results in the “cannot prove” message and the bit about not being able to reduce the term because Nothing is uninhabited. It doesn’t fall through to the case _ case, suggesting it’s hitting the case Nothing part and failing there in the case analysis mechanism. The evidence suggests, per your point above that such a thing operates as expected on user-defined uninhabited types, that there’s something special in the processing of Nothing. I’m curious what the rationale for that is.

This works as expected, even though the defined NotInt should be uninhabited (which we can verify):

scala> type NotInt = Int => Nothing
// defined alias type NotInt = Int => Nothing

scala> summon[Int => Nothing]
-- [E172] Type Error: ----------------------------------------------------------
1 |summon[Int => Nothing]
  |                      ^
  |No given instance of type Int => Nothing was found for parameter x of method summon in object Predef
1 error found

scala> type NameOf[X] = X match
         case Int     => "Int"
         case String  => "String"
         case Nothing => "Nothing"
         case NotInt  => "NotInt"
         case _       => "unknown"
                                                                                                                                                                   
scala> summon[NameOf[NotInt] =:= "NotInt"]
val res19: "NotInt" =:= "NotInt" = generalized constraint

I’m not adept with scala internals, clearly, but from a naive type theoretic perspective I’d expect the NameOf[Nothing] term to reduce: NameOf[Nothing] unifies with NameOf[X] in an environment with X = Nothing, which could be amenable to the case analysis in the definition. How that proceeds would depend on details I’m not familiar with, but again from a naive point of view, it seems a rewrite/reduction of a typelevel expression should be able to proceed regardless of whether the types are inhabited. Indeed it seems to proceed fine unless that uninhabited type is the special bottom type Nothing(modulo other edge cases that haven’t come up yet).

I understand that this is a strange thing to do and whatever is going on is unlikely to have practical consequences for real programs. It’s just that I find this behavior a bit puzzling and am trying to adjust my intuition appropriately.

4

First off, the type Int => Nothing is not uninhabited. I can trivially define an instance of such a function like this (x: Int) => throw new Exception(s"Got $x").

Uninhabited here means that there is no values of a type. For example, Nothing has no values. Int & String is another type which has no values. There are no values, which are both a string and an int.

Even if you ignore the uninhabited error, Nothing in a match types does not make sense in the way you think. For example, Nothing is a subtype of both Int and String (and all other types). To show this, let’s define a new match type like yours, which just ignores the uninhabited error.

type NameOf[X] = List[X] match
  case List[Int] => "Int"
  case List[String] => "String"
  case List[Nothing] => "Nothing"
  case _ => "unknown"

summon[NameOf[Nothing] =:= "Nothing"]

Surely this compiles? No, we get the error message Cannot prove that ("Int" : String) =:= ("Nothing" : String). This is a direct consequence of Nothing extending all other types. Int was the first check, so that’s what it picked.

Maybe it would help you to read about the match type reduction here

5

This is all as specified. You may find it informative to read

1 Like
6

in general, match type reduction works on the assumption that there is a value of that type (therefore follows runtime semantics for picking a case or “falling through” to the next case). it isnt a purely static construct

7

Thanks for this reference. It seems to be just what I needed and was after but somehow didn’t uncover when I poked around.

I’ll read more carefully, but it seems the behavior I observed results from

Nothing is disjoint from everything (including itself)

and this part of the reduction rule:

  • If X matches P1 with type capture instantiations [...ts => ts']:
    • If X â‹” P1 [X is provably disjoint from P1], do not reduce.

It appears from the commentary above this definition in the SIP that this subrule was chosen as an even safer variant of what was already being done:

It [the mechanism in the pre-SIP-56 algorithm] was added a [sic] safeguard against matching an empty (Nothing) scrutinee. The problem with doing so is that an empty scrutinee will be considered both as matching the pattern and as provably disjoint from the pattern. This can result in the match type reducing to different cases depending on the context. To sidestep this issue, the current algorithm refuses to consider a scrutinee that is provablyEmpty.

So it would seem to really really understand the rationale I’d have to dig a little deeper still, but I think this is illuminating enough to adjust my intuitions for now, which is what I was after. Thanks all.

1 Like
8

OK, thanks for this—it’s something that didn’t click for me before.

Thanks for the link; that helps. This is probably the most important bit for present purposes:

  • If the scrutinee type S is an empty set of values (such as Nothing or String & Int), do not reduce.

This feels like a strange choice, frankly, but like I’ve said a few times I’m naive about scala internals and I’m sure there’s a rationale for it. I saw @sjrd posted SIP-56, which I imagine has the details I need to understand (haven’t read it yet).

As a sidenote, the example of NameOf using List is a meaningfully different example because of the covariance of List and exactly how list deconstruction is handled during type inference. My original example does not contain that complexity because the type is being matched directly.