Match type reduction failure

[Bersier]

Compiler version

3.4.0-RC1, 3.4.0-RC1-bin-20231221-beaf7b4-NIGHTLY

Minimized code

import OpaqueScope.Opaque

type MapSum[D1, D2] = D1 match
  case Opaque[l1] => D2 match
    case Opaque[l2] => Opaque[Sum[l1, l2]]

object OpaqueScope:
  opaque type Opaque[N <: NatT] = Double

  val foo: MapSum[Opaque[Succ[Zero]], Opaque[Zero]] = 1.0
end OpaqueScope

sealed trait NatT derives CanEqual
case class Zero() extends NatT
case class Succ[N <: NatT](n: N) extends NatT

type Sum[M <: NatT, N <: NatT] <: NatT = (M, N) match
  case (_, Zero) => M
  case (Zero, _) => N
  case (Succ[predM], Succ[predN]) => Succ[Succ[Sum[predM, predN]]]

Compiler output

[error] 10 |  val foo: OpaqueSum[Opaque[Succ[Zero]], Opaque[Zero]] = 1.0
[error]    |                                                         ^^^
[error]    |Found:    (1.0d : Double)
[error]    |Required: OpaqueSum[OpaqueScope.Opaque[Succ[Zero]], OpaqueScope.Opaque[Zero]]
[error]    |
[error]    |Note: a match type could not be fully reduced:
[error]    |
[error]    |  trying to reduce  OpaqueSum[OpaqueScope.Opaque[Succ[Zero]], OpaqueScope.Opaque[Zero]]
[error]    |  failed since selector OpaqueScope.Opaque[Succ[Zero]]
[error]    |  does not match  case OpaqueScope.Opaque[l1] => OpaqueScope.Opaque[Zero] match {
[error]    |  case OpaqueScope.Opaque[l2] => OpaqueScope.Opaque[Sum[l1, l2]]
[error]    |}
[error]    |  and cannot be shown to be disjoint from it either.
[error]    |
[error]    | longer explanation available when compiling with `-explain`

Expectation

The code is expected to compile, as in Scala 3.3.1 and 3.3.2-RC1.

(See also here)

[sjrd]

I believe it's more of the same as what I mentioned at #19309 (comment)

Inside OpaqueScope, the expansion of MapSum sees the alias of Opaque = Double, and therefore matching cannot attribute a unique answer to what are l1 and l2.

[Bersier]

@sjrd How could that code be fixed? foo cannot be defined outside OpaqueScope, as Double is only known to be Opaque within OpaqueScope. In the original project, there seem to be valid similar cases that cannot be refactored.

I wonder whether it wouldn't make more sense for MapSum to not know about Opaque = Double even when used inside OpaqueScope, since it was defined outside? One wouldn't expect an analoguous term function defined outside of OpaqueScope to suddendly stop working because of an ambiguity only present inside of OpaqueScope.

Finally, regardless of whether the compilation failure is intended, the error message still seems problematic, since Opaque = Double is never mentioned as the reason for the failure of the match type reduction. Also, unlike other errors that are caused by newly illegal match type cases, this one does not mention that using -source:3.3 would prevent it from happening.

[sjrd]

@sjrd How could that code be fixed? foo cannot be defined outside OpaqueScope, as Double is only known to be Opaque within OpaqueScope. In the original project, there seem to be valid similar cases that cannot be refactored.

At least in this case you could replace the usage of MapSum by its result, since it is known to be Opaque[Sum[Succ[Zero]], Zero]].

I wonder whether it wouldn't make more sense for MapSum to not know about Opaque = Double even when used inside OpaqueScope, since it was defined outside? One wouldn't expect an analoguous term function defined outside of OpaqueScope to suddendly stop working because of an ambiguity only present inside of OpaqueScope.

Unfortunately, that is not possible. MapSum is expanded at its call site, which is within OpaqueScope. The analogous in term functions is that you do a term match with a type test, and that type test will definitely know the most precise type of the value, which is how its call site created it, not its less precise type known at definition site.

Finally, regardless of whether the compilation failure is intended, the error message still seems problematic, since Opaque = Double is never mentioned as the reason for the failure of the match type reduction. Also, unlike other errors that are caused by newly illegal match type cases, this one does not mention that using -source:3.3 would prevent it from happening.

I agree that the error message is not great here. I am not sure how to detect this situation, however. Perhaps there is a way to add the information that an opaque type alias was involved somewhere in the match type reduction trace, in order to hint that there's probably an issue with the interaction between match types and opaque type aliases within their declaring scope.

[Bersier]

@sjrd thank you for your detailed reply. You are of course free to close the issue if you think improving the error message is not feasible.

Concerning the fix you suggested for the minimized code, I don't think it is applicable to my project. I started a thread on Scala users to continue this discussion.