title: Generic types with Type.Reflection and Nats
body: <p>I have a simple definition for a Nat and a definition for types indexed by Nat's, Natty.</p>
  
  <pre><code>data Nat :: * where 
      Zero :: Nat
      Suc  :: Nat -&gt; Nat              deriving(Show, Typeable)
  
  data Natty :: Nat -&gt; * where
      Zy :: Natty Zero
      Sy :: Natty n -&gt; Natty (Suc n)  deriving Typeable
  </code></pre>
  
  <p>I want to  store and manipulate these Natty's in a generic fashion with the use of the Type.Reflection module.</p>
  
  <p>Storing as a Nat as a type rep works fine. </p>
  
  <pre><code>foo :: Nat -&gt; SomeTypeRep
  foo x = SomeTypeRep (typeOf x)
  </code></pre>
  
  <p>But storing a Natty as a type rep doesn't work unless extra constraints are added.</p>
  
  <pre><code>boo :: Natty n -&gt; SomeTypeRep
  boo x = SomeTypeRep (typeOf x)
  </code></pre>
  
  <p>boo produces the following error:</p>
  
  <pre><code>No instance for (Typeable n) arising from the use of 'typeOf'
  </code></pre>
  
  <p><strong>My question is why can Haskell not recognise that n is a nat and should therefore be Typeable?</strong></p>
  
  <p>Like I said I can fix this issue by adding the constraint of Typeable n to the beginning of boo but when I'm using a function that returns natty in the middle of another function its not that simple. </p>
  
  <p>The following extensions and imports have been used.</p>
  
  <pre><code>{-# LANGUAGE DataKinds, KindSignatures, GADTs #-} 
  import Type.Reflection
  </code></pre>