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 < [email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/glasgow-haskell-users > >
_______________________________________________ Glasgow-haskell-users mailing list [email protected] http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
