Scala中针对单例类型的GADT类型优化

问题描述

我有一个简单的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
  }

解决方法

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

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是一个类型类，将其用作隐式约束是很自然的，但是将其用作返回类型有点奇怪）。

gadt scala scala-cats singleton-type