[Haskell-beginners] Type depending on value

{-# LANGUAGE DataKinds, KindSignatures, GADTs, StandaloneDeriving #-}

Hi. Here is natural numbers and its singleton definition, which i take from "Part I: Dependent Types in Haskell" article by Hiromi ISHII [1]:

data Nat = Z | S Nat deriving (Show)

data SNat :: Nat -> * where SZ :: SNat 'Z SN :: SNat n -> SNat ('S n) deriving instance Show (SNat n)

But i can't figure out how may i define function returning SNat value depending on Nat value: f :: Nat -> SNat n f Z = SZ f (S n) = SN (f n) This does not typecheck, because, as i understand, ghc can't infer type n. Is it possible to do this at all? [1]: https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safet...