Opaque types do not work with match types

[chuwy]

Compiler version

3.3.0-RC3 and 3.2.2

Minimized code

import scala.compiletime.constValue

type IsInt[A] = A match
  case Int => true
  case _   => false

constValue[IsInt[Int]]     // val res2: Boolean = true; works as expected                                                                                                                        
constValue[IsInt[String]]  // val res3: Boolean = false; works as expected

object Foo:
  opaque type Foo = Int

constValue[IsInt[Foo.Foo]]    // compile-time error

Output

1 |constValue[IsInt[Foo.Foo]]
  |^^^^^^^^^^^^^^^^^^^^^^^^^^
  |not a constant type: IsInt[rs$line$2#Foo.Foo]; cannot take constValue

Expectation

I don't know if it should have been true or false (probably false), but compilation error certainly wasn't expected. My expectation was that an opaque type T is treated as any other T >: Nothing <: Any.

[sjrd]

The error message is not ideal--it would be better if it included the match trace--but there must be a compile error. IsInt[Foo.Foo] cannot be reduced because, at that spot, it is not known whether Foo.Foo is a subtype of Int or not. Therefore IsInt[Foo.Foo] is not a constant type, and therefore constValue refuses it.

[dwijnand]

I don't know if it should have been true or false (probably false), but compilation error certainly wasn't expected. My expectation was that an opaque type T is treated as any other T >: Nothing <: Any.

Your expectations don't agree with each other. Because Foo is treated as any other T >: Nothing <: Any and that's why it doesn't reduce to anything, and therefore it isn't a constant type:

-- Error: foo.scala:14:26 ------------------------------------------------------
14 |def res5[Foo] = constValue[IsInt[Foo]]
   |                ^^^^^^^^^^^^^^^^^^^^^^
   |                not a constant type: IsInt[Foo]; cannot take constValue

[chuwy]

My point being (correct me if I'm wrong), that when we define an opaque type of Int we actually detach it from Int, so for the Typer it's NOT a subtype of Int in any way and hence the match type should get reduced into false.

I'm not sure if I'm trying to challenge the design decision here, but just stating that from my (very limited) experience, I cannot see why we would want to match an opaque type over the pattern (Int in first example, Option in below one). Even if I did wanted to match it, I imagine we could do it explicitly:

type Dealias[T] = T      // pseudocode

type IsInt[A] = A match
  case Int          => true
  case Dealias[Int] => true     // matches opaque types
  case _            => false

---

Here's the actual use case I where I stumbled upon it:

type GetRequiredLabels[T <: Tuple] = T match
  case Labelled[?, Option[?]] *: tail => GetRequiredLabels[tail]
  case Labelled[IsSingleton[l], ?] *: tail => l *: GetRequiredLabels[tail]
  case EmptyTuple => EmptyTuple

I want to check exactly for that type. And if user for some reasons add an opaque type - the whole logic gets broken, while I expect that opaque types are well usual types.

[chuwy]

Because Foo is treated as any other T >: Nothing <: Any and that's why it doesn't reduce to anything

But aren't String or trait Bar also treated as T >: Nothing <: Any? And yet they do work with above match type. From what @sjrd said, I understand that compiler cannot be sure whether Foo is a subtype of Int or not and therefore to avoid ambiguity it refuses to compile it and above I was trying to make a point that maybe it should be certain that it's just a type unrelated to Int.

[sjrd]

It is definitely not unrelated to Int. Opaque type aliases are truly aliases of their underlying type. They're opaque in the sense that that knowledge is hidden from most of the world. The fact that knowledge is hidden does not make that piece of knowledge false; it makes it unknown.

[dwijnand]

so for the Typer it's NOT a subtype of Int in any way and hence the match type should get reduced into false.

Here's where what you say doesn't correspond: it's not known, statically, to be a subtype of Int, but it could be, and therefore it shouldn't reduce to true and it shouldn't proceed to false either.

But aren't String or trait Bar also treated as T >: Nothing <: Any? And yet they do work with above match type.

The difference between Foo and eitherString or trait Bar, when matching against a pattern Int, is that Foo is an abstract type with bounds (either in my type parameter example, or your original opaque type example) so we can't prove that it's disjoint from Int. String and trait Bar are class types, so we can tell whether they're disjoint from Int, from their class definitions, and from the fact that Int is a final class (so is String).

[chuwy]

Ok, thanks for your input both, much appreciated. I think I'm going hold to my point of view that it's a better DX choice for the time being, but can't waste your time on the argument anymore.

However, if we think it's an area of reporting, I find it odd that the compile-time error happens only when we try to materialize the constant type:

type A = IsInt[Foo.Foo]  // this is fine
constValue[A]            // error is here

However, if we construct another non-sense type:

type IsIntOrString[A] = A match
  case Int => "int"
  case String => "string"

type B = IsIntOrString[Boolean]   // error is here
constValue[B]                     // we don't even get here

The error comes in much earlier, during type application and I don't see much difference between two cases.

[dwijnand]

Yeah, I can see how that confusion. I think in the first release of match types they didn't error when they reduced to no matching, and user's preferred and asked for the eager error. The reason IsInt[Foo.Foo] isn't an error is because, as opposed to the other one where we know none of the cases match, in this one we don't know if it will match one of the cases or not, so the reduction is "stuck", and then will only act like an abstract type with its upper bound. There's nothing wrong in that, per-se, but it won't be a constant type.

[mbovel]

Could we extend the error message with a note saying that a match type could not be fully reduced, like we do in other places? Do you think that would be hard (c.f. appropriate for a spree)?