Summoning instance for opaque type in an object with match type fails-CodePudding

This is a fairly niche problem I'm running into here ~~and I suspect it's a compiler bug~~, but since I'm still quite new to match types, I figured to ask here first.

import scala.deriving.*

type Flatten[A <: Tuple] <: Tuple = A match
  case ((a, b), c) => Tuple.Append[Flatten[(a, b)], c]
  case (_, _)      => A
  case Tuple1[_]   => A
  case EmptyTuple  => EmptyTuple


opaque type MyString = String

object Bar:
  opaque type MyString = String

def run =
  summon[(MyString, Int) =:= Flatten[(MyString, Int)]]
  summon[(Bar.MyString, Int) =:= Flatten[(Bar.MyString, Int)]]

Scastie

The last line fails to compile while the line above (with almost identical code) succeeds. It works, however, when the first recursive case in the match type is disabled.

CodePudding user response：

Not an expert on that, but I think I could make some sense out of it:

The compiler error says:

Note: a match type could not be fully reduced:

  trying to reduce  Playground.Flatten[(Playground.Bar.MyString, Int)]
  failed since selector  (Playground.Bar.MyString, Int)
  does not match  case ((a, b), c) => Tuple.Append[Playground.Flatten[(a, b)], c]
  and cannot be shown to be disjoint from it either.
  Therefore, reduction cannot advance to the remaining cases

Since Bar.MyString is actually "opaque" from within your def run, the compiler does not know (or behaves like it does not know) what type it is. Note that you cannot summon[Bar.MyString =:= String] from def run, but you can summon[MyString =:= String].

So, from within def run, the actual type behind Bar.MyString could be a String, but it could also be something else - for example, it could be (Int, Int), in which case case ((a, b), c) would match. So: the compiler cannot determine whether case ((a, b), c) does or doesn't match and hence fails.

On the other hand, MyString is not actually "opaque" from within def foo, because it is defined in the same scope, so it is known that the type is String and hence it is known that (MyString, Int) cannot match case ((a, b), c).

Note that this does compile (because summoning happens in the same scope as the definition of Bar.MyString so the actual type behind the opaque type is visible):

object Bar:
  opaque type MyString = String
  def runLocally =
    summon[(MyString, Int) =:= Flatten[(MyString, Int)]]