Sign-indexed Peano numbers

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

data Sign = Zero | Pos

data Nat :: Sign -> * where
    Z :: Nat Zero
    S :: Nat a -> Nat Pos

divide :: Nat a -> Nat Pos -> Nat a
divide = error "exercise for the reader"

main :: IO ()
main = return ()