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.