Hey GHC folks! 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?) 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) data Mat (row::Nat) (col::Nat) elem = ... some vector representation index:: (Mat r c el) -> (Word,Word) -> el index mt ix = ... some stride based indexing calculation that gets at the "r" and "c" numbers via the singletons to translate the ix tuple into the index into the underlying vector representation {-# perhaps an inline pragma? #-} indexSpec3x3:: (Mat 3 3 el) -> (Word, Word) -> el indexSpec3x3 smat ix = smat `index` ix 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? Does my question even make sense as phrased? thanks! -Carter