title: TypeLits or Singletons: Promoting an `Integer` to `KnownNat` (`Nat`) at Runtime
body: <p>I've found two ways to promote an Integer to a Nat (or KnownNat, I don't get the distintion yet) at runtime, either using TypeLits and Proxy (Data.Proxy and GHC.TypeLits), or Singletons (Data.Singletons). In the code below you can see how each of the two approaches is used:</p>
  
  <pre><code>{-# LANGUAGE DataKinds #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE NoImplicitPrelude #-}
  
  module Main where
  
  import Prelude hiding (replicate)
  import Data.Proxy (Proxy(Proxy))
  import Data.Monoid ((&lt;&gt;))
  import Data.Singletons (SomeSing(..), toSing)
  import GHC.TypeLits
  import Data.Singletons.TypeLits
  import Data.Vector.Sized (Vector, replicate)
  
  main :: IO ()
  main = playingWithTypes 8
  
  playingWithTypes :: Integer -&gt; IO ()
  playingWithTypes nn = do
  
    case someNatVal nn of
      Just (SomeNat (proxy :: Proxy n)) -&gt; do
  --      let (num :: Integer) = natVal proxy
  --      putStrLn $ "Some num: " &lt;&gt; show num
        putStrLn $ "Some vector: " &lt;&gt; show (replicate 5 :: Vector n Int)
      Nothing -&gt; putStrLn "There's no number, the integer was not a natural number"
  
    case (toSing nn :: SomeSing Nat) of
      SomeSing (SNat :: Sing n) -&gt; do
  --      let (num :: Integer) = natVal (Proxy :: Proxy n)
  --      putStrLn $ "Some num: " &lt;&gt; show num
        putStrLn $ "Some vector: " &lt;&gt; show (replicate 5 :: Vector n Int)
  </code></pre>
  
  <p>The documentation for <a href="https://hackage.haskell.org/package/base-4.10.0.0/docs/GHC-TypeLits.html" rel="noreferrer">TypeLits</a> indicates that it shouldn't be used by developers, but Singletons don't capture the case in which the given Integer is not a natural number (i.e., running <code>playingWithTypes 8</code> runs without errors, but <code>playingWithTypes (-2)</code> fails when we try to create a Singleton from the non-natural number).</p>
  
  <p>So, what is the "standard" way to promote an <code>Integer</code> to a <code>Nat</code>? Or what is the best approach to promote, using TypeLits and Proxy, or Singletons?</p>