Failure to get the compiler to realise two types are equal

First, I want to make it clear that I’m not at all sure my expectations are reasonable. I might be wanting the compiler to do something that it has very good reasons to refuse. That’s a large chunk of asking this question: I would like to understand why this is unreasonable!

I’m working with Scala 3.6.2. Here’s the code I’m struggling with:

enum Type:
  case Num
  case Bool

enum TypeRepr[A <: Type]:
  case Num extends TypeRepr[Type.Num.type]
  case Bool extends TypeRepr[Type.Bool.type]

def from[A <: Type](tpe: A): TypeRepr[A] = tpe match
  case Type.Bool => TypeRepr.Bool
  case Type.Num  => TypeRepr.Num

This does not compile, with the following error:

Found:    (Playground.TypeRepr.Bool :
  Playground.TypeRepr[(Playground.Type.Bool² : Playground.Type)])
Required: Playground.TypeRepr[A]

where:    A     is a type in method from with bounds <: Playground.Type
          Bool  is a value in object TypeRepr
          Bool² is a value in object Type

I, maybe naively, expected the compiler to realise that Type.Bool was of type Type.Bool.type, and that TypeRepr.Bool was of type TypeRepr[Type.Bool.type], so it was a legal value to return there.

The reason I expected this was because the following code compiles without an issue:

def to[A <: Type](repr: TypeRepr[A]): A = repr match
  case TypeRepr.Bool => Type.Bool
  case TypeRepr.Num  => Type.Num

Here, the compiler seems perfectly happy to conclude that the types are equal.

I suspect the difference’s to do with Scala “only” implementing local type equalities with GADTs, which TypeRepr is and Type isn’t. I’d quite like to understand whether this is an oversight, a choice, or an inevitability (or a complete misunderstanding of what all these terms mean!).

Thanks!

2 Likes