Improve error: the pattern contains an unaccounted type parameter

[TomasMikula]

Compiler version

3.6.4

Minimized code

sealed trait KV[K, V]
sealed trait Append[Init, KV]

type KeysOf[KVs] = KVs match
  case KV[k, v] => k
  case Append[init, KV[k, v]] => KeysOf[init] | k

// OK
summon[KeysOf[KV["x", Int]] =:= "x"]

// Error
summon[KeysOf[Append[KV["x", Int], KV["y", String]]] =:= ("x" | "y")]

Output

The match type contains an illegal case:
    case Append[init, KV[k, v]] => KeysOf[init] | k
The pattern contains an unaccounted type parameter `k`.
(this error can be ignored for now with `-source:3.3`)

https://scastie.scala-lang.org/6ZDIroNFQQuOwgG78Ju83w

Expectation

Should compile.

[Gedochao]

Works correctly with LTS, including 3.3.5 and 3.3.6-RC1
Last good release: 3.4.0-RC1-bin-20231214-423cd6c-NIGHTLY
First bad release: 3.4.0-RC1-bin-20231218-ec2b8bc-NIGHTLY
The bisect script points at 90f9d22, but it fails with a different error (and can't be right, since it actually has been backported to the LTS, which works fine).

So the faulty commit is somewhere in between 90f9d22..ec2b8bc

[Gedochao]

Bisected it manually.
The faulty commit is 881e945 (#18262)
cc @sjrd

[sjrd]

It looks to be as designed per the spec, although the error message is misleading. k is "unaccounted for" because it is twice nested within contravariant type constructors.

The match type can be rewritten as follows to make it a legal match type:

type KeysOf[KVs] = KVs match
  case KV[k, v] => k
  case Append[init, kv] =>
    kv match
      case KV[k, v] => KeysOf[init] | k

Generally, only the deepest type constructor before type variables can be non-covariant. The 1-to-(n-1) outer type constructors must be covariant.

[Gedochao]

It looks to be as designed per the spec, although the error message is misleading.

@sjrd Should we try to improve the error message?

[sjrd]

Yes, it would be nice to have a better error message.

[TomasMikula]

It looks to be as designed per the spec, although the error message is misleading. k is "unaccounted for" because it is twice nested within contravariant type constructors.

@sjrd It's twice-nested invariant constructors (not contravariant). But anyway, the spec does list case Inv[Inv[t]] => as an illegal pattern.
Any reason why that's the case? Why do covariant type constructors have a privileged status? On the surface, it seems to me like an implementation restriction leaking into the spec. Or is there a fundamental reason for it? If anything, I would assume invariant constructors to work best; and contravariant to be symmetric to covariant from theoretical perspective. This is even more perplexing as the simple expansion to nested matches that you provided works just fine.

[sjrd]

Ah yes, twice nested invariant, indeed. But yes, that's intentional. And no, it's not an implementation detail leaking into the spec. This spec was entirely developed on paper before I did whatever it took to implement.

I don't remember exactly the reason for this one right now, but I remember there was a reason. Overall it's because matching is defined in terms of baseType, and that is fundamentally linked to subtyping, not type equivalence (and no, you can't just apply subtyping in both direction, because match types have a strong asymmetry between scrutinee and pattern).

[TomasMikula]

So a pattern A will match any of A's subtypes (I did not expect that, but OK):

trait A
trait B extends A

type Foo[T] = T match
  case A => String
  case B => Int

summon[Foo[B] =:= String] // OK
summon[Foo[B] =:= Int]    // Error: Cannot prove that String =:= Int.

(https://scastie.scala-lang.org/w4n3iRbmTR2nm2J8c91nzw)

I still don't see why

• variance does not work as it works with subtyping (e.g. double contravariant is covariant);
• nested match makes a difference, as opposed to nested pattern.

[sjrd]

Nested match works because it explicitly allows subtyping of the inner thing. With the nested pattern you would need type equivalence to satisfy the invariant position.

Variance does not work the same as elsewhere because we have tocapture type parameters in a way that survives type narrowing.

[TomasMikula]

Nested match works because it explicitly allows subtyping of the inner thing. With the nested pattern you would need type equivalence to satisfy the invariant position.

I'm not sure I'm following. Is it a matter of giving the typechecker an intermediate variable (kv in your workaround) to work with? One that it could potentially synthesize on its own? Otherwise, if the two cases are indeed fundamentally different, then it sure is very confusing.

Variance does not work the same as elsewhere because we have to capture type parameters in a way that survives type narrowing.

Maybe an example would help.