Is it feasible to use type members to reduce type verbosity in Scala?

Question

So, this may sound like a general question about language design, but I think there is something concrete here. Specifically I am interested in what technical challenges prevent the kludgy code that follows from being generally useful.

We all know that "Scala's type inference isn't as good as Haskell's", and that there are many reasons it just can't be as good, and still do all the things Scala does. But what also becomes apparent, after programming Scala long enough, is that poor type inference isn't really that bad, so much as is the verbosity that is required to specify some common types. So, for example, in the polymorphic tail function,

def tail[A](ls: List[A]) =
    ls match {
        case Nil     => sys.error("Empty list")
        case x :: xs => xs
    }

it is required to explicitly name a type parameter in order to make the method useful; no way around it. tail(ls: List[Any]) won't work because Scala can't figure out that the result type is the same is the input type, even though to a human this is "obvious".

So, inspired by this difficulty, and knowing that Scala can sometimes be cleverer with type members than with type parameters, I wrote a version of List that uses type members:

sealed trait TMList {
    self =>
    type Of
    def :::(x: Of) = new TMCons {
        type Of = self.Of
        val head = x
        val tail = (self: TMList { type Of = self.Of })
    }
}
abstract class TMNil extends TMList
def ATMNil[A] = new TMNil { type Of = A }
abstract class TMCons extends TMList {
    self =>
    val head: Of
    val tail: TMList { type Of = self.Of }
}

OK, the definition looks awful, but it is at least straightforward, and it allows us to write our tail method as follows:

def tail4(ls: TMList) =
    ls match {
        case _: TMNil => sys.error("Empty list")
        case c: TMCons with ls.type => c.tail
    }

And the beauty is that this works, so we can write (with head defined as you'd expect)

val ls = 1 ::: 2 ::: ATMNil
val a = tail4(ls)
println(head4(a) * head4(a))

and Scala knows that the output type member is still Int. We had to write something a little funny with TMCons with ls.type, and Scala complains that the match is not exhaustive, but that bit of code could just have been inserted by Scala for us, because of course when you match on ls any case has to be of ls.type, and of course the match is exhaustive.

So my question is: what's the catch? Why don't we do all our polymorphic types this way, and just modify the language so the syntax doesn't look so bad? What technical problems would we run into?

Clearly there is a problem that a class cannot be covariant in its type members; but I'm not so interested in that; I think that's a separate issue. Assume for the moment we're not concerned about variance. What else would go wrong?

I suspect this may introduce new problems for type inference (like how I had to define ATMNil for the example to work) but I don't understand Scala's type inference well enough to know what those would be.

edit to respond to 0__: I think you may have found it. A version with a type parameter works,

def move2[A](a: TMList { type Of = A }, b: TMList { type Of = A }) = b match {
    case c: TMCons with b.type => c.head ::: a
    case _                     => a
}

But what's interesting is that, without an explicit return type, a curried dependently typed version doesn't:

def move3(a: TMList)(b: TMList { type Of = a.Of }) = b match {
    case c: TMCons with b.type => c.head ::: a
    case _                     => a
}

Scala infers the return type to be TMList; this is an upper bound of the two types of the case, TMList { type Of = a.Of } and a.type. Of course, TMList { type Of = a.Of } would also be an upper bound (and the one I want, which is why adding an explicit return type works), and, I think, a more specific upper bound. I wonder why Scala doesn't infer the more specific upper bound.

Answer 1

You will want to read type refinements do everything.

Answer 2

Have a try to rewrite the following with the TMList:

def move[A](a: List[A], b: List[A]): List[A] = b match {
   case head :: _ => head :: a
   case _ => a
}

move(List(1,2,3),List(4,5,6))