Scala 中单例类型的 GADT 类型细化

Question

我有一个简单的 GADT 声明如下：

sealed trait T[A]
object T {
  case class MkT[A <: String with Singleton](name: A) extends T[A]
}

现在我想编写一个方法来检查两个T 对象的单例类型参数是否相同，如果是这种情况，则以cats.evidence.Is 对象的形式返回该事实的证据。 我尝试了以下方法，但它不起作用：

import cats.evidence.Is
def checkIs[A, B](ta: T[A], tb: T[B]): Option[Is[A, B]] =
  (ta, tb) match {
    case (ta: T.MkT[a], tb: T.MkT[b]) if ta.name == tb.name => 
      Some(Is.refl[A])
    case _ => None
  }
// [error] Main.scala:36:75: type mismatch;
// [error]  found   : cats.evidence.Is[A,A]
// [error]  required: cats.evidence.Is[A,B]

如何让编译器相信这是正确的？

// 编辑：正如@Dmytro Mitin 指出的那样，进行运行时检查并在编译时说服编译器类型相同似乎是自相矛盾的。但这实际上是可能的，可以用更简单的 GADT 来证明：

sealed trait SI[A]
object SI {
  case object S extends SI[String]
  case object I extends SI[Int]
}
def checkInt[A](si: SI[A]): Option[Is[A, Int]] =
  si match {
    case SI.I => Some(Is.refl[Int])
    case _ => None
  }

Answer 1

通过模式匹配，您尝试在运行时 (ta.name == tb.name) 检查“两个 T 对象的单例类型参数是否相同”，但希望在编译时说服编译器。我会尝试一个类型类

trait CheckIs[A, B] {
  def checkIs(ta: T[A], tb: T[B]): Option[Is[A, B]]
}
object CheckIs {
  implicit def same[A]: CheckIs[A, A] = (_, _) => Some(Is.refl[A])
  implicit def diff[A, B]: CheckIs[A, B] = (_, _) => None
}

def checkIs[A, B](ta: T[A], tb: T[B])(implicit ci: CheckIs[A, B]): Option[Is[A, B]] = ci.checkIs(ta, tb)

checkIs(T.MkT("a"), T.MkT("a")) //Some(cats.evidence.Is$$anon$2@28f67ac7)
checkIs(T.MkT("a"), T.MkT("b")) //None

（顺便说一句，Is 是一个类型类，将其用作隐式约束很自然，但将其用作返回类型有点奇怪。）