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

Iavor Diatchki iavor.diatchki at
Tue Aug 28 17:27:23 CEST 2012


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!

On Thu, Aug 23, 2012 at 9:41 PM, Carter Schonwald <
carter.schonwald at> 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)
> 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?
> thanks!
> Carter Schonwald
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>

More information about the Glasgow-haskell-users mailing list