GADT type refinement for singleton types in Scala

Question

I have a simple GADT declared like this:

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

Now I would like to write a method that will check if the singleton type parameter is the same for two T objects and return evidence of that fact in the form of a cats.evidence.Is object if that is the case. I've tried the following, but it doesn't work:

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]

How can I convince the compiler that this is sound?

// edit: as @Dmytro Mitin pointed out, it seems paradoxical to do a run-time check and yet convince the compiler at compile-time that the types are the same. But this is in fact possible, and it can be demonstrated with a simpler 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

With the pattern matching you try to check that "the singleton type parameter is the same for two T objects" at runtime (ta.name == tb.name) but want to convince the compiler at compile time. I would try a type class

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

(By the way, Is is a type class, it's natural to use it as implicit constraint but a little weird to use it as return type.)