Hello, <div><br></div><div>I&#39;m trying to understand how much i can build on top of type literals, so as an exercise, i&#39;ve been trying to see if I can define a type level</div><div>&quot;absolute different of two natural numbers&quot;</div>

<div><br></div><div>i have a minimal example that either type checks in a useless way, or gives a misleading type errors! (or perhaps i am fundamentally not understanding someting)</div><div><br></div><div><br></div><div>

 here&#39;s the gist for the misleading type error version </div><div>(it seems to indicate that SingI arity 2, rather than arity 1)</div><div><a href="https://gist.github.com/3445419">https://gist.github.com/3445419</a></div>

<div><br></div><div>heres the gist for the version that type checks in a useless way!</div><div>and complains that it doesn&#39;t understand that (1&lt;=2)</div><div><a href="https://gist.github.com/3445456">https://gist.github.com/3445456</a></div>

<div><br></div><div>are these bugs in type nats, or am I missing something?</div><div><br></div><div>thanks!</div><div>Carter Schonwald</div><div><br></div><div><br></div>