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.

[1] ‎https://hackage.haskell.org/package/ghc-typelits-natnormalise

From: Станислав Черничкин

Sent: Monday, June 20, 2016 11:37 PM

To: haskell-cafe@haskell.org

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.