sealed trait Type
case object TypeRecHole extends Type
case object IntType extends Type
case object UnitType extends Type
case class ProductType(types: Type*) extends Type
case class LabeledType(ty: Type, label: String) extends Type
case class TypeVar(name: String) extends Type
case class MuType(param: String, ty: Type) extends Type

object SubtypeSum extends App {
  def substRecTyVar(recParamName: String, ty: Type) = ty match {
    case TypeVar(name) if name == recParamName => TypeRecHole
    case
  }
  def geqType: (Type, Type) => Boolean = {
    case (LabeledType(_, l1), LabeledType(_, l2)) => l1 >= l2
    case (LabeledType(_, _), _) => true
  }
  def sub: (Type, Type) => Boolean = {
    case (ProductType(ts1 @ _*), ProductType(ts2 @ _*)) =>
      ts1.sortWith(geqType).zip(ts2.sortWith(geqType)).map(sub.tupled).reduce(_ && _)
    case (LabeledType(ty1, l1), LabeledType(ty2, l2)) =>
      if (l1 == l2) { assert(ty1 == ty2); true } else false
    case (MuType(p1, ty1), MuType(p2, ty2)) =>
      sub(substRecTyVar(p1, ty1), substRecTyVar(p2, ty2))
    case (a, b) => a == b
  }

  implicit class TypeOps(ty: Type) extends AnyRef {
    def @@(label: String) = LabeledType(ty, label)
  }

  val ty1 = MuType("X", ProductType( // μX.(nil|stop|cons Int X)
    UnitType @@ "nil",
    UnitType @@ "stop",
    ProductType(IntType, TypeVar("X")) @@ "cons"
  ))

  val ty2 = MuType("Y", ProductType( // μY.(nil|cons Int Y)
    UnitType @@ "nil",
    ProductType(IntType, TypeVar("Y")) @@ "cons"
  ))

  println(sub(ty1, ty2))
}