"dependent" example in Haskell

SimpleComplicatedDT.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}

module DepFun where

data Nat = NatZ | NatS Nat

type family Codom (n :: Nat) where
  Codom NatZ     = Int
  Codom (NatS n) = Int -> Codom n

data NatP (a :: Nat) where
  Z :: NatP NatZ
  S :: NatP n -> NatP (NatS n)


sumN :: NatP n -> Codom n
sumN n = sumNacc n 0


sumNacc :: NatP n -> Int -> Codom n
sumNacc Z     acc = acc
sumNacc (S n) acc = \x -> sumNacc n (acc + x)

-- examples:

zero = sumN Z
five = sumN (S Z) 5
eleven = sumN (S (S Z)) 5 6

threeParams :: Int -> Int -> Int -> Int
threeParams = sumN (S (S (S Z)))

typeError :: Int -> Int -> Int
typeError = sumN (S Z) -- Couldn't match type `Int` with `Int -> Int`

have a look at the sumN function
it's type depend on the very first value you give it

sumN Z :: Int
sumN (S Z) :: Int -> Int
sumN (S (S Z)) :: Int -> Int -> Int
...