> {-# 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-safety/dependent-types-in-haskell#ordinals