Thanks, that looks promising. I've also discovered some tricks:
1. With TypeFamilies and PartialTypeSignatures one can write: test :: _ => FixedGetter i j (Int32, Int32, Int32, Int32) where test's body is: int32Host >>>= \a -> int32Host >>>= \b -> int32Host >>>= \c -> int32Host >>>= \d -> ireturn (a, b, c, d). Haskell will infer that "_" (skipped type context with some type-level math on i and j) is a (KnownNat i), ((KnownNat (i + 4)), (KnownNat (i + 4) + 4) and so on freeing the programmer from declaring all of this manually.
2. One can specify types explicitly. For example test :: FixedGetter 0 16 (Int32, Int32, Int32, Int32) works, unexpectedly. 

2016-06-21 3:12 GMT+03:00 Lana Black <lanablack@amok.cc>:
GHC currently lacks an ability to normalize type level arithmetic equations. There is a plugin however [1] that implements this feature.  I believe that's what you are looking for. 


From: Станислав Черничкин
Sent: Monday, June 20, 2016 11:37 PM
Subject: [Haskell-cafe] Easy type-level math

With DataKinds and TypeOperators and GHC.TypeLits and, probably, KindSignatures I have:

test :: (KnownNat i, KnownNat (i + 4)) => MyType i ((i + 4) + 4)

and it's typecheck perfectly.

But what I really want to have is:

test :: (KnownNat i) => MyType i (i +8)

and it does not typecheck.

Does not ((i + 4) + 4) == (i +8)?

Does not (KnownNat i) implies (KnownNat (i + 4))? 

Did I miss something about Haskell?

--
Thanks, Stanislav Chernichkin.




--
Sincerely, Stanislav Chernichkin.