Inconsistent match type reduction

[johnynek]

compiler version 3.0.1-RC2

This compiles without warning

package example    
    
object RecMap {                                            
                                                                                   
  object Record {                               
    // use this scope to bound who can see inside the opaque type
    opaque type Rec[A <: Tuple] = Map[String, Any]
                                                   
    object Rec {                          
      type HasKey[A <: Tuple, K] =
        A match
          case (K, t) *: _ => t
          case _ *: t => HasKey[t, K]

      val empty: Rec[EmptyTuple] = Map.empty
                                                                
      extension [A <: Tuple](toMap: Rec[A])                     
        def fetch[K <: String & Singleton](key: K): HasKey[A, K] =
          toMap(key).asInstanceOf[HasKey[A, K]]
    }                                              
  }                                                                      
                                 
  def main(args: Array[String]) =
    import Record._                                                    
                               
    val foo: Any = Rec.empty.fetch("foo")          
    //summon[Rec.HasKey[EmptyTuple, "foo"] =:= Any]
                                    
  end main
}

but I don't think it should. Rec.empty has type Rec[EmptyTuple] and there is no value of HasKey[EmptyTuple, Any].

When you uncomment the summon you get the correct result:

[error] -- Error: /Users/oboykin/oss_code/scala3_examples/src/main/scala/RecMap.scala:48:49 
[error] 48 |    summon[Rec.HasKey[EmptyTuple, "foo"] =:= Any]
[error]    |                                                 ^
[error]    |Cannot prove that example.RecMap.Record.Rec.HasKey[EmptyTuple, ("foo" : String)] =:= Any.
[error]    |
[error]    |Note: a match type could not be fully reduced:
[error]    |
[error]    |  trying to reduce  example.RecMap.Record.Rec.HasKey[EmptyTuple, ("foo" : String)]
[error]    |  failed since selector  EmptyTuple
[error]    |  matches none of the cases
[error]    |
[error]    |    case (("foo" : String), t) *: _ => t
[error]    |    case _ *: t => example.RecMap.Record.Rec.HasKey[t, ("foo" : String)]
[error] one error found

[johnynek]

a fuller working example is here:

https://gist.github.com/johnynek/1e3cbddf461bd3da9b00e2f4f126c253

(but this only shows positive cases, it didn't exercise showing a compile failure for invalid keys or types).

[johnynek]

related to #10747 and #12768