Forwarding Oleg's message to the list. ----- Forwarded message from Oleg Grenrus <oleg.grenrus@iki.fi> ----- Date: Tue, 21 Jun 2016 05:27:13 +0300 From: Oleg Grenrus <oleg.grenrus@iki.fi> To: Lana Black <lanablack@amok.cc> Subject: Re: [Haskell-cafe] Easy type-level math X-Mailer: iPhone Mail (13F69) ghc-typelits-natnormalise can dismiss equality constraints, like `n + m ~ m + n`. OP needs to conjure KnownNat dictionary though, and that plugin cannot do. You can do it unsafely and manually with `reifyNat` from `reflections`: http://hackage.haskell.org/package/reflection-2.1.2/docs/Data-Reflection.htm... - Oleg

On 21 Jun 2016, at 03:12, Lana Black <lanablack@amok.cc> wrote:

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.

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

----- End forwarded message -----