[Haskell-beginners] Type depending on value

[Dmitriy Matrosov]

> {-# 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/beginners/attachments/20160411/19222f45/attachment-0001.html>