Hello, the functions on type literals on the master branch are not yet implemented. If you want to play around with these kinds of things, please use the "type-nats" branch (please note that this is a development branch so things may occasionally break!). In the first example, GHC is saying that it can't solve "SingI (d :: Nat)", which is because the master branch cannot see that "d" must be 1. Similarly, in the second one it does not know about '<='. Both of these should work on the 'type-nats' branch though. The confusing arity issue in the first example is because of kind a polymorphism---SingI has one kind argument (e.g., Nat) and one type argument. (e.g., d) but---at present---GHC renders these in the same way. Hope this helps, and happy hacking! -Iavor On Thu, Aug 23, 2012 at 9:41 PM, Carter Schonwald < carter.schonwald@gmail.com> wrote:

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

_______________________________________________ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users