Hello, <div><br></div><div>I'm trying to understand how much i can build on top of type literals, so as an exercise, i've been trying to see if I can define a type level</div><div>"absolute different of two natural numbers"</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'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't understand that (1<=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>