I don't sure what you mean, but i've checked now the differences between my code and reflection package, and there are some substantial ones.
Sorry, I thought that natVal is a part of KnownNat, and I didn't bother to check.
but they're not (and, if i'm correct, they can't, because there is no types with kind Nat (remember, they've defined only kind)).
Nat is somewhat magic, as it's built into GHC. Type literals like 0,1,2,3... are all legal types of this kind. It is possible to write type class instances for them, but they're uninhabited, and thus can only be used as parameters for other types. I guess KnownNat is just magic too, but I think in principle it could be defined by induction, though the last time I've checked GHC had problems with realizing that '0' and 'n + 1' are not overlapping.
So, you're right: `reifyNat` defines dictionary for `KnownNat n` (and this is the only instance we have) as Integer. But though dictionary is a function `natSing :: SNat n`, now SNat is newtype and its runtime representation should indeed be equivalent to Integer and all is fine.
Well, ok, i think i understand how correct `reifyNat` works. Thanks!
But i still don't understand why mine works too, though is probably wrong.
I think that, while "newtype SNat (n :: Nat) = SNat Integer" is reliably coercible to Integer, your SNat happens to be coercible to your Nat too, but again, I have no idea if this is the expected behavior. It's playing with unsafeCoerce and GHC internals after all, so weird things can happen. You could define SNat as something "newtype SNat (n :: Nat) = SNat Nat" to be on the safer side, and then define SNatClass and natVal as something like: class SNatClass (n :: Nat) where singN :: SNat n instance SNatClass Z where singN = SNat Z instance SNatClass n => SNatClass (S n) where singN = SNat (S n) where SNat n = (singN :: SNat n) natVal :: forall n proxy. SNatClass n => proxy n -> Nat natVal _ = case (singN :: SNat n) of SNat n -> n Best regards, Marcin Mrotek