Luv 2 type addition

Add.hs

-- An unserious response to
--
-- > I will believe in type systems the day one of them warns me about this code:
-- > pub fn add_two_integers(num1: Int, num2: Int) -> Int {
-- >   num1 - num2
-- > }
--
-- I don't understand why people don't want to program like this. Types!

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

import Data.Proxy (Proxy(..))
import GHC.TypeLits (type (+), type (-), KnownNat(..))
import qualified GHC.TypeLits as TypeLits

-- | Kind of natural numbers
data Nat = Z | S Nat deriving (Eq, Ord, Show)

-- | Type-level addition on natural numbers
type family Add (n :: Nat) (m :: Nat) :: Nat where
  Add 'Z m = m
  Add ('S n) m = 'S (Add n m)

-- | Term-level natural numbers indexed by their type
--
-- "Singleton" natural numbers.
--
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

deriving instance Show (SNat n)

-- | "Typed" Term level addition of natural numbers
add :: SNat n -> SNat m -> SNat (Add n m)
add SZ     m = m
add (SS n) m = SS (add n m)

-- | Convert GHC type literals to our '@Nat'@ kind
type family FromLit (t :: TypeLits.Nat) :: Nat where
  FromLit 0 = 'Z
  FromLit n = 'S (FromLit (n - 1))

-- | Typeclass for converting GHC type literals to term level natural numbers
class Lit (t :: TypeLits.Nat) (n :: Nat) where
  litProxy :: p t -> SNat n

-- | Base case: we can always convert '0' to 'Z'
instance Lit 0 'Z where
  litProxy _ = SZ

-- | Inductive case: apply 'SS' to 'litProxy (Proxy @(t - 1))'
instance (KnownNat t, FromLit t ~ n, n ~ 'S m, u ~ (t - 1), Lit u m) => Lit t ('S m) where
  litProxy _ = SS (litProxy (Proxy @u))

-- | Non-proxy version of 'litProxy'. Use a type application
lit :: forall t n . (KnownNat t, n ~ FromLit t, Lit t n) => SNat n
lit = litProxy (Proxy @t)

-- | Beware! Type erasure!
toInt :: SNat n -> Int
toInt SZ     = 0
toInt (SS n) = 1 + toInt n

-- | Typed addition!
main :: IO ()
main = print $ toInt n
 where
  n :: SNat (Add (FromLit 4) (FromLit 5))
  n = add (lit @4) (lit @5)