<div dir="ltr">> {-# LANGUAGE DataKinds, KindSignatures, GADTs, StandaloneDeriving #-}<br><br>Hi.<br><br>Here is natural numbers and its singleton definition, which i take from "Part<br>I: Dependent Types in Haskell" article by Hiromi ISHII [1]:<br><br>> data Nat = Z | S Nat<br>>   deriving (Show)<br>><br>> data SNat :: Nat -> * where<br>>     SZ :: SNat 'Z<br>>     SN :: SNat n -> SNat ('S n)<br>> deriving instance Show (SNat n)<br><br>But i can't figure out how may i define function returning SNat value<br>depending on Nat value:<br><br>    f :: Nat -> SNat n<br>    f Z     = SZ<br>    f (S n) = SN (f n)<br><br>This does not typecheck, because, as i understand, ghc can't infer type n. Is<br>it possible to do this at all?<br><br>[1]: <a href="https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell#ordinals">https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell#ordinals</a><br><br></div>