In scala shapeless, is it possible to use literal type as a generic type parameter?

Question

Assuming that I'm writing a program for vector multiplication. Following the requirement in this article:

https://etrain.github.io/2015/05/28/type-safe-linear-algebra-in-scala

The multiplication should only compile successfully if the dimension of both vectors are equal. For this I define a generic type Axis that uses a shapeless literal type (the number of dimension) as the type parameter:

import shapeless.Witness

trait Axis extends Serializable

case object UnknownAxis extends Axis

trait KnownAxis[W <: Witness.Lt[Int]] extends Axis {

  def n: Int

  def ++(that: KnownAxis[W]): Unit = {}
}

object KnownAxis {

  val w1 = Witness(1)
  val w2 = Witness(2)

  case class K1(n: Witness.`1`.T) extends KnownAxis[w1.type]
  case class K2(n: Witness.`2`.T) extends KnownAxis[w2.type]

//  K2(2) ++ K1(1) // doesn't compile

  K2(2) ++ K2(2)
}

So far so good, the problem however appears when I try to generalise it for all n:

  case class KN[W <: Witness.Lt[Int]](n: W#T) extends KnownAxis[W]

  KN(1)

The above code triggers a compilation error:

Axis.scala:36: type mismatch;
 found   : Int(1)
 required: this.T
[ERROR]   KN(1)
[ERROR]      ^
[ERROR] one error found

My question is: why Spark is incapable of focusing on the more refined type Witness.`1`.T, instead it is using type Int? What does it take to override this behaviour so case class KN can be successfully defined?

UPDATE 1: The follow up has been moved to a new question:

When using the singleton type feature of Scala shapeless, how to force the compiler to use narrow/singleton type as an implicit parameter?

Answer 1

It isn't surprising that Scala can't infer W given W#T, because generally speaking it's possible for two different Ws to have the same W#T. Not for witness types, but they aren't treated specially by the compiler.

What I expected to work (and not sure why it doesn't) is to specify the type parameter:

KN[Witness.`1`](1)
// error: type arguments [scala.this.Any] do not conform to method apply's type parameter bounds [W <: shapeless.this.Witness.Lt[scala.this.Int]]

or more likely

KN[w1.type](1)
// error: type mismatch;
// found   : scala.this.Int(1)
// required: .this.T

What does work:

case class KN[W <: Witness.Lt[Int]](w: W) extends KnownAxis[W] {
  val n = w.value
}

KN(Witness(1))

It seems to suit the requirements in your question, but I don't know if it'll work with the rest of your code.

You may also want to consider this alternative which doesn't require Shapeless in Scala 2.13:

trait Axis extends Serializable

case object UnknownAxis extends Axis

trait KnownAxis[W <: Int with Singleton] extends Axis {

  def n: W

  def ++(that: KnownAxis[W]): Unit = {}
}

case class KN[W <: Int with Singleton](n: W) extends KnownAxis[W]

KN(1)

For 2.12

import shapeless.syntax.singleton._

...
KN(1.narrow)