title: Haskell type level literal Nat: status?
body: <p>GHC has type level literal Nats. I can read a few things about them, for instance, here:</p>
  
  <p><a href="https://ghc.haskell.org/trac/ghc/wiki/TypeNats">https://ghc.haskell.org/trac/ghc/wiki/TypeNats</a></p>
  
  <p>Unfortunately, there seems to be little documentation about them, and almost nothing I try to do with them actually works. </p>
  
  <p>Comment 18 from <a href="https://ghc.haskell.org/trac/ghc/ticket/4385">this page</a> mentions this simple example of size parametrized Vecs (I've added LANGUAGE pragmas and an import statement):</p>
  
  <pre><code>{-# LANGUAGE DataKinds #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE TypeOperators #-}
  
  import GHC.TypeLits
  
  data Vec :: Nat -&gt; * -&gt; * where
    Nil  :: Vec 0 a
    (:&gt;) :: a -&gt; Vec n a -&gt; Vec (n+1) a
  
  (+++) :: Vec n a -&gt; Vec m a -&gt; Vec (n+m) a
  Nil       +++ bs = bs
  (a :&gt; as) +++ bs = a :&gt; (as +++ bs)
  </code></pre>
  
  <p>It wasn't working at the time, but then the implementation was supposedly modified so that this worked. That was 5 years ago... but it doesn't work on my GHC 7.10.1:</p>
  
  <pre><code>trash.hs:15:20:
      Could not deduce ((n + m) ~ ((n1 + m) + 1))
      from the context (n ~ (n1 + 1))
        bound by a pattern with constructor
                   :&gt; :: forall a (n :: Nat). a -&gt; Vec n a -&gt; Vec (n + 1) a,
                 in an equation for ‘+++’
        at trash.hs:15:2-8
      NB: ‘+’ is a type function, and may not be injective
      Expected type: Vec (n + m) a
        Actual type: Vec ((n1 + m) + 1) a
      Relevant bindings include
        bs :: Vec m a (bound at trash.hs:15:15)
        as :: Vec n1 a (bound at trash.hs:15:7)
        (+++) :: Vec n a -&gt; Vec m a -&gt; Vec (n + m) a
          (bound at trash.hs:14:1)
      In the expression: a :&gt; (as +++ bs)
      In an equation for ‘+++’: (a :&gt; as) +++ bs = a :&gt; (as +++ bs)
  </code></pre>
  
  <p>What's the deal here? Are type level literal Nats supposed to be usable for this kind of thing? If so, how do I implement the (+++) function? If not, what is their use case?</p>