Fail to do unification for dependent path types

xieyuheng · June 30, 2019, 6:04pm

I tried to model the Category of groups by dependent path type,
but found the following errors:

xieyuheng/pracat/blob/master/src/main/scala/xieyuheng/pracat/Group.scala#L40


type A = GroupHom


def dom(hom: GroupHom) = hom.dom
def cod(hom: GroupHom) = hom.cod


def id(x: Group): GroupHom = new GroupHom {
  val dom: Group = x
  val cod: Group = x


  def hom(x: dom.T): cod.T = ???
  // should be `x` but:
  // [error] type mismatch;
  // [error]  found   : x.type (with underlying type this.dom.T)
  // [error]  required: this.cod.T
}


def composeRaw(f: GroupHom, g: GroupHom): GroupHom = new GroupHom {
  val dom: Group = f.dom
  val cod: Group = g.cod


  def hom(x: dom.T): cod.T = ???

Katrix · July 1, 2019, 9:57am

Problem is that when you say val dom: Group = x, you’re erasing that underlying type you’re interested in