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

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


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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120824/f1f261e1/attachment.htm>


More information about the Glasgow-haskell-users mailing list