What is type declaration for in definition of Nat in shapeless?

Question

This is the definition of Nat in package shapeless:

   trait Nat {
     type N <: Nat
   }

   case class Succ[P <: Nat]() extends Nat {
     type N = Succ[P]
   }

   class _0 extends Nat with Serializable {
     type N = _0
   }

What are the type declarations for ? Once removed it seems to me that the definition works equally well.

Answer 1

They're used where Nat is the target type of an implicit conversion from a literal Int ... see here, for example, in the definition of the Int indexing method for HList,

def at(n : Nat)(implicit at : At[L, n.N]) : at.Out = ...

Here the intention is that the method is invoked with a literal Int argument,

(23 :: "foo" :: true :: HNil).at(1)

The argument is converted to a Nat by an implicit macro which is able to inspect the compile time argument tree and construct the corresponding Nat value. We can then refer to the type member N of n and use it as an index for the At type class which extracts the desired element from the HList.