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

[Iavor Diatchki]

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 at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/glasgow-haskell-users/attachments/20120828/3ba5fa19/attachment.htm>