title: Can I get KnownNat n to imply KnownNat (n * 3), etc?
body: <p>I'm working with data types of this shape, using <code>V</code> from <code>linear</code>:</p>
  
  <pre><code>type Foo n = V (n * 3) Double -&gt; Double
  </code></pre>
  
  <p>Having it fixed on <code>n</code> is pretty important, because I want to be able to ensure that I'm passing in the right number of elements at compile-time.  This is a part of my program that already works well, independent of what I'm doing here.</p>
  
  <p>For any <code>KnownNat n</code>, I can generate a <code>Foo n</code> satisfying the behavior that my program needs.  For the purposes of this question it can be something silly like</p>
  
  <pre><code>mkFoo :: KnownNat (n * 3) =&gt; Foo n
  mkFoo = sum
  </code></pre>
  
  <p>Or for a more meaningful example, it can generate a random <code>V</code> of the same length and use <code>dot</code> on the two.  The <code>KnownNat</code> constraint here is redundant, but in reality, it's needed to do make a <code>Foo</code>.  I make one <code>Foo</code> and use it for my entire program (or with multiple inputs), so this guarantees me that whenever I use it, I'm using on things with the same length, and on things that the structure of the <code>Foo</code> dictates.</p>
  
  <p>And finally, I have a function that makes inputs for a <code>Foo</code>:</p>
  
  <pre><code>bar :: KnownNat (n * 3) =&gt; Proxy n -&gt; [V (n * 3) Double]
  </code></pre>
  
  <p><em>bar</em> is actually the reason why i'm using <code>n * 3</code> as a type function, instead of just manually expanding it out.  The reason is that <code>bar</code> might do its job by using three vectors of length <code>n</code> and appending them all together as a vector of length <code>n * 3</code>.  Also, <code>n</code> is a much more meaningful parameter to the function, semantically, than <code>n * 3</code>.  This also lets me disallow improper values like <code>n</code>'s that aren't multiples of 3, etc.</p>
  
  <p>Now, before, everything worked fine as long as I defined a type synonym at the beginning:</p>
  
  <pre><code>type N = 5
  </code></pre>
  
  <p>And I can just then pass in <code>Proxy :: Proxy N</code> to <code>bar</code>, and use <code>mkFoo :: Foo N</code>.  And everything worked fine.</p>
  
  <pre><code>-- works fine
  doStuff :: [Double]
  doStuff = let inps = bar (Proxy :: Proxy N)
            in  map (mkFoo :: Foo N) inps
  </code></pre>
  
  <p>But now I want to be able to adjust <code>N</code> during runtime by loading information from a file, or from command line arguments.</p>
  
  <p>I tried doing it by calling <code>reflectNat</code>:</p>
  
  <pre><code>doStuff :: Integer -&gt; Double
  doStuff n = reflectNat 5 $ \pn@(Proxy :: Proxy n) -&gt;
                let inps = bar (Proxy :: Proxy n)
                in  map (mkFoo :: Foo n) inps
  </code></pre>
  
  <p>But...<code>bar</code> and <code>mkFoo</code> require <code>KnownNat (n * 3)</code>, but <code>reflectNat</code> just gives me <code>KnownNat n</code>.</p>
  
  <p>Is there any way I can generalize the proof that <code>reflectNat</code> gives me to satisfy <code>foo</code> ?</p>