Inductive construction of the Integers for https://codereview.stackexchange.com/questions/79761/integers-from-scratch-in-haskell

Integers.hs

module Integers where

data Nat = Zero | Succ Nat
    deriving Show

data Z = Negative Nat | NonNegative Nat
    deriving Show

plus :: Nat -> Nat -> Nat
Zero     `plus` m = m
(Succ n) `plus` m = Succ (n `plus` m)

sub :: Nat -> Nat -> Either Nat Nat
Zero     `sub` m        = Right m
n        `sub` Zero     = Left n
(Succ n) `sub` (Succ m) = n `sub` m

mul :: Nat -> Nat -> Nat
Zero     `mul` _ = Zero
(Succ n) `mul` m = plus m $ n `mul` m

instance Num Z where
    abs (Negative n) = NonNegative n
    abs z            = z
    
    signum (Negative _)       = Negative (Succ Zero)
    signum (NonNegative Zero) = NonNegative Zero
    signum (NonNegative _)    = NonNegative (Succ Zero)
    
    negate (Negative n)       = NonNegative n
    negate (NonNegative Zero) = NonNegative Zero
    negate (NonNegative n)    = Negative n
    
    fromInteger i | i < 0 = Negative n
                  | otherwise = NonNegative n
        where
            n = iterate Succ Zero !! fromInteger (abs i)
    
    (Negative n)       + (Negative m)    = Negative (n `plus` m)
    (NonNegative n)    + (NonNegative m) = NonNegative (n `plus` m)
    (Negative n)       + (NonNegative m) = case (n `sub` m) of
                                               Left Zero  -> NonNegative Zero -- Unreachable by `sub`, included for totality
                                               Left n'    -> Negative n'
                                               Right Zero -> NonNegative Zero
                                               Right m'   -> NonNegative m'
    zn@(NonNegative n) + zm@(Negative m) = zm + zn
    
    (Negative n)       * (Negative m)    = NonNegative (n `mul` m)
    (Negative n)       * (NonNegative m) = case (n `mul` m) of
                                            Zero -> NonNegative Zero
                                            n'   -> Negative n'
    zn@(NonNegative n) * zm@(Negative m) = zm * zn
    (NonNegative n)    * (NonNegative m) = NonNegative (n `mul` m)