Unsound GADT reasoning with equality patterns

[LPTK]

CC @AleksanderBG

Minimized code

Bug found by @julianmichael on the contributors forum.

case class KeyHolder[K[_], A](key: K[A])

case class AlignedPairOf[A, K[_], V[_]](key: KeyHolder[K, A], value: V[A])

type AlignedPair[K[_], V[_]] = AlignedPairOf[?, K, V]

def get[K[_], V[_], B](key: KeyHolder[K, B]): List[AlignedPair[K, V]] => Option[V[B]] = {
  case (AlignedPairOf(`key`, v)) :: _ => Some(v) // wrong assumption here
  case _ :: xs => get(key)(xs)
  case Nil => None
}

@main def test_1 = {
  type C[A] = Int
  type Id[A] = A
  val u = AlignedPairOf[String, C, Id](KeyHolder[C, String](1), "omg")
  val v = AlignedPairOf[Double, C, Id](KeyHolder[C, Double](1), 9000.1)
  val xs = u :: Nil
  println(get(u.key)(xs): Option[String]) // Some(omg)
  println(get(v.key)(xs): Option[Double]) // Some(omg) --- Silently wrong!
  println(get(v.key)(xs).map(_ + 1): Option[Double]) // java.lang.ClassCastException: java.lang.String cannot be cast to java.lang.Double
}

Output

java.lang.ClassCastException: java.base/java.lang.String cannot be cast to java.base/java.lang.Double
	at scala.runtime.BoxesRunTime.unboxToDouble(BoxesRunTime.java:112)
	at dotty.runtime.function.JFunction1$mcDD$sp.apply(JFunction1$mcDD$sp.java:12)
	at scala.Option.map(Option.scala:242)
	at rs$line$5$.test_1(rs$line$5:9)
	at rs$line$6$.<init>(rs$line$6:1)
	at rs$line$6$.<clinit>(rs$line$6)
	at rs$line$6.res0(rs$line$6)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at java.base/jdk.internal.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
	at java.base/jdk.internal.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
	at java.base/java.lang.reflect.Method.invoke(Method.java:564)
	at dotty.tools.repl.Rendering.$anonfun$3(Rendering.scala:84)
	at scala.Option.map(Option.scala:242)
	at dotty.tools.repl.Rendering.valueOf(Rendering.scala:84)
	at dotty.tools.repl.Rendering.renderVal(Rendering.scala:121)
	at dotty.tools.repl.ReplDriver.$anonfun$13(ReplDriver.scala:309)
	at scala.collection.immutable.List.flatMap(List.scala:293)
	at scala.collection.immutable.List.flatMap(List.scala:79)
	at dotty.tools.repl.ReplDriver.extractAndFormatMembers$2(ReplDriver.scala:309)
	at dotty.tools.repl.ReplDriver.renderDefinitions$$anonfun$2(ReplDriver.scala:330)
	at scala.Option.map(Option.scala:242)
	at dotty.tools.repl.ReplDriver.renderDefinitions(ReplDriver.scala:333)
	at dotty.tools.repl.ReplDriver.compile$$anonfun$2(ReplDriver.scala:252)
	at scala.util.Either.fold(Either.scala:189)
	at dotty.tools.repl.ReplDriver.compile(ReplDriver.scala:268)
	at dotty.tools.repl.ReplDriver.interpret(ReplDriver.scala:196)
	at dotty.tools.repl.ReplDriver.loop$1(ReplDriver.scala:129)
	at dotty.tools.repl.ReplDriver.runUntilQuit$$anonfun$1(ReplDriver.scala:132)
	at dotty.tools.repl.ReplDriver.withRedirectedOutput(ReplDriver.scala:151)
	at dotty.tools.repl.ReplDriver.runUntilQuit(ReplDriver.scala:132)
	at dotty.tools.repl.Main$.main(Main.scala:6)
	at dotty.tools.repl.Main.main(Main.scala)

Expectation

Type error.

For the record, the correct implementation is:

def get[K[_], V[_], B](key: KeyHolder[K, B]): List[AlignedPair[K, V]] => Option[V[B]] = {
  case (AlignedPairOf(k: key.type, v)) :: _ => Some(v)
  case _ :: xs => get(key)(xs)
  case Nil => None
}

[martijnhoekstra]

Another variation of the same issue?

sealed trait Tag[A]
case object StringTag extends Tag[String] {
  override def equals(that: Any) = true
}
case object DoubleTag extends Tag[Double] {
  override def equals(that: Any) = true
}
final case class Value[A](tag: Tag[A], value: A)

def getFromValue[A, B](t: Tag[A], v: Value[B]): Option[A] =
  v match {
    case Value(`t`, value) => Some(value)
    case _                 => None
  }

val omg: Option[String] = getFromValue(StringTag, Value(DoubleTag, 1.3)) //omg Some(1.3)
omg.map(_.length) //omg ClassCastException