<html><head></head><body lang="en-US" style="background-color: rgb(255, 255, 255); line-height: initial;"> <div style="width: 100%; font-size: initial; font-family: Calibri, 'Slate Pro', sans-serif, sans-serif; color: rgb(31, 73, 125); text-align: initial; background-color: rgb(255, 255, 255);">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. </div><div style="width: 100%; font-size: initial; font-family: Calibri, 'Slate Pro', sans-serif, sans-serif; color: rgb(31, 73, 125); text-align: initial; background-color: rgb(255, 255, 255);"><br></div><div style="width: 100%; font-size: initial; font-family: Calibri, 'Slate Pro', sans-serif, sans-serif; color: rgb(31, 73, 125); text-align: initial; background-color: rgb(255, 255, 255);">[1] https://hackage.haskell.org/package/ghc-typelits-natnormalise</div> <div style="width: 100%; font-size: initial; font-family: Calibri, 'Slate Pro', sans-serif, sans-serif; color: rgb(31, 73, 125); text-align: initial; background-color: rgb(255, 255, 255);"><br></div> <div style="font-size: initial; font-family: Calibri, 'Slate Pro', sans-serif, sans-serif; color: rgb(31, 73, 125); text-align: initial; background-color: rgb(255, 255, 255);"></div> <table width="100%" style="background-color:white;border-spacing:0px;"> <tbody><tr><td colspan="2" style="font-size: initial; text-align: initial; background-color: rgb(255, 255, 255);"> <div style="border-style: solid none none; border-top-color: rgb(181, 196, 223); border-top-width: 1pt; padding: 3pt 0in 0in; font-family: Tahoma, 'BB Alpha Sans', 'Slate Pro'; font-size: 10pt;"> <div><b>From: </b>Станислав Черничкин</div><div><b>Sent: </b>Monday, June 20, 2016 11:37 PM</div><div><b>To: </b>haskell-cafe@haskell.org</div><div><b>Subject: </b>[Haskell-cafe] Easy type-level math</div></div></td></tr></tbody></table><div style="border-style: solid none none; border-top-color: rgb(186, 188, 209); border-top-width: 1pt; font-size: initial; text-align: initial; background-color: rgb(255, 255, 255);"></div><br><div id="_originalContent" style=""><div dir="ltr">With DataKinds and TypeOperators and GHC.TypeLits and, probably, KindSignatures I have:<div><br></div><div>test :: (KnownNat i, KnownNat (i + 4)) => MyType i ((i + 4) + 4)<br></div><div><br></div><div>and it's typecheck perfectly.</div><div><br></div><div>But what I really want to have is:</div><div><br></div><div>test :: (KnownNat i) => MyType i (i +8)</div><div><br></div><div>and it does not typecheck.</div><div><br></div><div>Does not ((i + 4) + 4) == (i +8)?</div><div><br></div><div>Does not (KnownNat i) implies (KnownNat (i + 4))? </div><div><br></div><div>Did I miss something about Haskell?</div><div><div><br></div>-- <br><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><span style="font-family:arial;font-size:small">Thanks, Stanislav Chernichkin.</span><br></div></div>
</div></div>
<br><!--end of _originalContent --></div></body></html>