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

Carter Schonwald carter.schonwald at
Fri Aug 24 06:41:00 CEST 2012


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

 here's the gist for the misleading type error version
(it seems to indicate that SingI arity 2, rather than arity 1)

heres the gist for the version that type checks in a useless way!
and complains that it doesn't understand that (1<=2)

are these bugs in type nats, or am I missing something?

Carter Schonwald
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list