
Hi! I wrote one thing with type-level numbers that were represented as simple data Zero data Succ a Then, in order to not invent my own peano numbers, I decided to go look for ones, and found GHC.TypeLits. But unfortunately, it shows a weird error for me. Here is a piece of code: https://gist.github.com/k-bx/a7b49165399658f87358 The one that's below "main" is working properly, while the one on top of it gives this error: typenats.hs:17:16: No instance for (Op D (0 + 1)) arising from a use of `f' Possible fix: add an instance declaration for (Op D (0 + 1)) In the expression: f (VJ i :: VJ D (0 + 1)) In an equation for `f': f (VJ i) = f (VJ i :: VJ D (0 + 1)) In the instance declaration for `Op D 0' Maybe I worked too much on type-level numbers today to not understand this simple error I'm getting, but could someone be so kind and explain me what am I doing wrong? Thank you very much!

18.08.2014, 23:16, "Konstantine Rybnikov"
The one that's below "main" is working properly, while the one on top of it gives this error:
typenats.hs:17:16: No instance for (Op D (0 + 1)) arising from a use of `f' Possible fix: add an instance declaration for (Op D (0 + 1)) In the expression: f (VJ i :: VJ D (0 + 1)) In an equation for `f': f (VJ i) = f (VJ i :: VJ D (0 + 1)) In the instance declaration for `Op D 0'
Hello Konstantine, I think you're using GHC 7.6.x series which had no solver for type-level natural numbers, resulting in 0+1 not typechecking with 1. You may find some history in https://ghc.haskell.org/trac/ghc/ticket/4385. With GHC 7.8 this compiles fine. Probably you can overcome the issue by providing the required instances of `+` type family by hand (up to the desired number), but it's hackish and may be tedious without TH. Just switch to 7.8 already.

On Mon, Aug 18, 2014 at 10:51 PM, Dmitry Dzhus
18.08.2014, 23:16, "Konstantine Rybnikov"
: The one that's below "main" is working properly, while the one on top of it gives this error:
typenats.hs:17:16: No instance for (Op D (0 + 1)) arising from a use of `f' Possible fix: add an instance declaration for (Op D (0 + 1)) In the expression: f (VJ i :: VJ D (0 + 1)) In an equation for `f': f (VJ i) = f (VJ i :: VJ D (0 + 1)) In the instance declaration for `Op D 0'
Hello Konstantine,
I think you're using GHC 7.6.x series which had no solver for type-level natural numbers, resulting in 0+1 not typechecking with 1.
You may find some history in https://ghc.haskell.org/trac/ghc/ticket/4385.
With GHC 7.8 this compiles fine.
Probably you can overcome the issue by providing the required instances of `+` type family by hand (up to the desired number), but it's hackish and may be tedious without TH. Just switch to 7.8 already.
Dmitry, you are 100% correct. Thank you very much! Moving to 7.8 straight away.
participants (2)
-
Dmitry Dzhus
-
Konstantine Rybnikov