What's the problem of this match type?

Here is the code, I do not know why the last line fail:

Welcome to Scala 3.1.0-RC2 (11.0.9.1, Java OpenJDK 64-Bit Server VM).
Type in expressions for evaluation. Or try :help.
                                                                                                                                                                                               
scala> type F[T <: Tuple] <: Tuple = T match
     |   case EmptyTuple => EmptyTuple
     |   case h *: t     => h match
     |     case Tuple    => Tuple.Concat[F[h], F[t]]
     |     case _        => h *: F[t]
     | 
                                                                                                                                                                                               
scala> summon[F[((Int, Char), String)] =:= (Int, Char, String)]
val res0: Int *: Char *: String *: EmptyTuple =:= Int *: Char *: String *: EmptyTuple = generalized constraint
                                                                                                                                                                                               
scala> summon[F[((Int, Char), AnyVal)] =:= (Int, Char, AnyVal)]
val res1: Int *: Char *: AnyVal *: EmptyTuple =:= Int *: Char *: AnyVal *: EmptyTuple = generalized constraint
                                                                                                                                                                                               
scala> summon[F[((Int, Char), AnyRef)] =:= (Int, Char, AnyRef)]
-- Error:
1 |summon[F[((Int, Char), AnyRef)] =:= (Int, Char, AnyRef)]
  |                                                        ^
  |                                                        Cannot prove that Int *: Char *: 
  |                                                          (Object match {
  |                                                            case Tuple => Tuple.Concat[F[Object], F[EmptyTuple.type]]
  |                                                            case _ => Object *: F[EmptyTuple.type]
  |                                                          } <: Tuple) =:= (Int, Char, AnyRef).

I’m not fluent with dependent/match types at all, yet, just a guess…

scala> summon[Tuple <:< AnyRef]
val res0: Tuple =:= Tuple = generalized constraint

scala> summon[((Int, Char), (Int, Char)) <:< ((Int, Char), AnyRef)]
val res1: ((Int, Char), (Int, Char)) =:= ((Int, Char), (Int, Char)) = generalized constraint

So I’d guess the problem is that AnyRef might actually be specialized to Tuple, yielding a different result type, so the generic AnyRef result variant really cannot be proven.

1 Like

From Match Types :

Match type reduction follows the semantics of match expressions, that is, a match type of the form S match { P1 => T1 ... Pn => Tn } reduces to Ti if and only if s: S match { _: P1 => T1 ... _: Pn => Tn } evaluates to a value of type Ti for all s: S.

A value of type AnyRef could match a case of type Tuple, so the inner match type cannot be reduced when h is AnyRef.

1 Like