[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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160621/db6c5136/attachment.html>