is this a type lits/nats bug or my incorrect understanding ?

Hello, 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 "absolute different of two natural numbers" 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) here's the gist for the misleading type error version (it seems to indicate that SingI arity 2, rather than arity 1) https://gist.github.com/3445419 heres the gist for the version that type checks in a useless way! and complains that it doesn't understand that (1<=2) https://gist.github.com/3445456 are these bugs in type nats, or am I missing something? thanks! Carter Schonwald