[Haskell-cafe] Type-level Nat to Integer

[Gautier DI FOLCO]

Hi all,

I'm trying to change type-level Nat to Integer as following:
{-# LANGUAGE DataKinds, KindSignatures, GADTs, PolyKinds #-}

data Nat = Z | S Nat

class NatToInt n where
    natToInt :: n -> Int

instance NatToInt Z where
    natToInt _ = 0

instance NatToInt (S n) where
    natToInt = 1 + natToInt (undefined :: n)

I understand why it fails (Z and S have not the right kind).
How to specify that NatToInt is Nat-specific?
Moreover, if you have any advanced explanations/links which could give me a
deeper understanding on what going on, I'll take them.

Thanks in advance for your help.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140703/74de80b3/attachment.html>