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.