Closed
Description
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