Proposal: Pattern matching on types in type definition

I recently implemented a utility function for Shapeless:

 trait IndexOf[X, L <: HList] extends DepFn0 with Serializable { type Out <: Nat }
 object IndexOf {
   def apply[X, L <: HList](implicit indexOf: IndexOf[X, L]): Aux[X, L, indexOf.Out] = indexOf
   type Aux[X, L <: HList, Out0] = IndexOf[X, L] { type Out = Out0 }
   implicit def indexOfHead[X, T <: HList]: Aux[X, X :: T, _0] =
     new IndexOf[X, X :: T] {
       type Out = _0
       def apply() = Nat._0

   implicit def indexOfOthers[X, H, T <: HList, I <: Nat]
   (implicit indexOf: IndexOf.Aux[X, T, I]): Aux[X, H :: T, Succ[I]] =
     new IndexOf[X, H :: T] {
       type Out = Succ[I]
       def apply() = Succ[I]

This is so verbose. I would definitely like to have something like pattern matching in Scala type definition, like something below:

type IndexOf[X, L <: HList] = (X, L) match {
  case (X, X :: T) ==> _0
  case (X, H :: T) ==> Succ[IndexOf[X, T]]

(=> cannot be used because it itself is a type. Here I used ==> as a placeholder)
Another example, the Pred on Nats. It’d be very nice to have

type Pred[N <: Nat] = N match {
  case Succ[P] ==> P

And this, after compilation, became all these implicit defs (each case clause is compiled into one implicit def). So this is just a syntactic sugar over the current implicit defs.


I know @adriaanm dreams of type-level pattern matching :).


I think that the greatest obstacle with this proposal is the recursive type definition.