title: In GHC.TypeLits what is someNatVal good for (which we can't accomplish with natVal)?
body: <p>I'm trying to understand <a href="https://hackage.haskell.org/package/base-4.8.1.0/docs/GHC-TypeLits.html" rel="noreferrer"><code>GHC.TypeLits</code></a>, and specifically <code>someNatVal</code>. I understand the way it's used in this blog <a href="http://snak.tumblr.com/post/110021257487/convert-a-type-level-natural-number-to-a-value" rel="noreferrer">post here</a>, but as mentioned the same example could have been implemented using <code>natVal</code>, like:</p>
  
  <pre><code>isLength :: forall len a. KnownNat len =&gt; Integer -&gt; List len a -&gt; Bool
  isLength n _ = n == natVal (Proxy :: Proxy len)
  </code></pre>
  
  <p>Are there any uses of <code>someNatVal</code> that can't be rewritten with <code>natVal</code>?</p>