Wrong type inferred in type-level computation

[scabug]

The following works fine:

    sealed trait Nat {
      type Fold[U, F[_ <: U] <: U, Z <: U] <: U
    }

    final object Zero extends Nat {
      type Fold[U, F[_ <: U] <: U, Z <: U] = Z
    }

    final class Succ[N <: Nat] extends Nat {
      type Fold[U, F[_ <: U] <: U, Z <: U] = F[N#Fold[U, F, Z]]
    }

    trait HList {
      type Head
      type Tail <: HList
      type Drop[N <: Nat] = N#Fold[HList, ({ type L[X <: HList] = X#Tail })#L, this.type]
      type Apply[N <: Nat] = Drop[N]#Head
    }

    class #: [H, T <: HList] extends HList { type Head = H; type Tail = T }

    object HNil extends HList { type Head = Nothing;  type Tail = Nothing }

    val l1 = null: Int #: String #: Boolean #: String #: HNil.type

    type _2 = Succ[Succ[Zero.type]]

    val t1: Boolean = null.asInstanceOf[ l1.type#Drop[_2]#Head ]

But using Apply[N] instead of Drop[N]#Head (which should be the identical) fails:

    HLTest.scala:31: error: type mismatch;
     found   : HLTest.l1.Apply[HLTest._2]
     required: Boolean
      val t2: Boolean = null.asInstanceOf[ l1.type#Apply[_2] ]

It seems that a type xs#Apply[...] is always resolved to xs#Head, completely ignoring the Drop[N] part.

Using a type lambda instead of plain application as a work-around:

  //type Apply[N <: Nat] = Drop[N]#Head
  type Apply[N <: Nat] = ({ type L[X <: HList] = X#Head })#L[Drop[N]]

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-5294?orig=1
Reporter: @szeiger
Affected Versions: 2.9.1, 2.10.0

[scabug]

@okomok said:
Fold is parameterized by U, which means a type-level generic-method.
Scalac, for now, seems not to work well with any form of type-level generics.
I don't know whether this is a bug or limitation of type-system of scala, though.
BTW, you can find a painful workaround: design guidelines

[scabug]

@adriaanm said:
Unassigning and rescheduling to M6 as previous deadline was missed.

[scabug]

@retronym said (edited on Jun 22, 2015 11:18:34 PM UTC):
I think this is a plain bug, rather than an inherent limitation.

I can compile this example successfully with this patch to asSeenFrom.

https://github.com/retronym/scala/tree/ticket/5294

Hopefully there are no ill effects from this and we can get this merged in 2.12.

[scabug]

@retronym said:
Additional test cases in #9469 also seem to be fixed by my patch above, so I'm merging these tickets.

[scabug]

@adriaanm said:
scala/scala#5263