<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>