Hey GHC folks!<div> <div>In the case where type lits (naturals specifically) are statically known (rather than abstract), is it possible to have a sort of static copy propagation / Singelton simplification happen at compile time? (Ie can GHC do such things with  type lits as presently implemented?)</div>

<div><br></div><div>a simple example might be that a statically sized matrix, and being able to specialize the stride and bounds checking at compile time (pseudo code example follows)</div><div><br></div><div>data Mat (row::Nat) (col::Nat) elem = ... some vector representation</div>

<div><br></div><div><br></div><div>index:: (Mat r c  el) -&gt; (Word,Word) -&gt; el</div><div>index mt ix = ... some stride based indexing calculation that gets at the &quot;r&quot;  and &quot;c&quot; numbers via the singletons  to translate the ix tuple into the index into the underlying vector</div>

<div>representation</div><div>{-# perhaps an inline pragma? #-}</div><div><br></div><div>indexSpec3x3:: (Mat 3 3 el) -&gt; (Word, Word) -&gt; el</div><div>indexSpec3x3 smat ix = smat `index` ix</div><div><br></div><div>under what circumstances can i get something like the body of indexSpec3x3 to use the static type level natural number machinery to partially specialize the computation?</div>

<div>Does my question even make sense as phrased?</div><div><br></div><div>thanks!</div><div><br></div><div>-Carter</div><div><br></div><div><br></div><div><br></div></div>