title: In Idris, what's the type of a list of lists of doubles, where all the lengths are known?
body: <p>An example value: <code>[[1, 2], [1]]</code></p>
  
  <p>Here, I would know that there are 2 lists, and that the first list has length 2, while the second one has length 1. Ideally, this function would compute those types:</p>
  
  <pre><code>func : (n ** Vect n Nat) -&gt; Type
  </code></pre>
  
  <p>But I don't know how to write it. I'm pretty sure it's something to do with dependent pairs, but I'm not sure how to write it.</p>
  
  <p>To clarify, I know it'd be possible to simply use <code>(n ** Vect n (p ** Vect p Double))</code> as the type of the example value. However, <code>n</code> only constrains the number of lists, not the number of their elements, because inside the list, <code>p</code> could be anything. I would most likely need something where the first element of the dependent pair is a <em>vector of lengths</em>, not just the number of lists. So something like <code>(Vect n Nat ** Vect n (Vect m Double))</code>--where each <code>m</code> is the corresponding element of the first vector.</p>