diff --git a/app/Main.hs b/app/Main.hs
index 5405f64..40a85e4 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -1,10 +1,10 @@
+{-# LANGUAGE BlockArguments, LambdaCase #-}
 module Main where
 
 import Control.Monad (forever)
 import System.IO (hFlush, stdout)
-import Text.Parsec (parse)
 import UntypedLambdaCalculus (eval)
-import UntypedLambdaCalculus.Parser (expr)
+import UntypedLambdaCalculus.Parser (parseExpr)
 
 prompt :: String -> IO String
 prompt text = do
@@ -13,8 +13,6 @@ prompt text = do
   getLine
 
 main :: IO ()
-main = forever $ do
-  input <- expr "stdin" <$> prompt ">> "
-  case input of
-    Left parseError -> putStrLn $ "Parse error: " ++ show parseError
-    Right ast -> print $ eval ast
+main = forever $ parseExpr "stdin" <$> prompt ">> " >>= \case
+  Left parseError -> putStrLn $ "Parse error: " ++ show parseError
+  Right expr -> print $ eval expr
diff --git a/package.yaml b/package.yaml
index f3737e3..93c3a4a 100644
--- a/package.yaml
+++ b/package.yaml
@@ -16,8 +16,6 @@ dependencies:
 - base >= 4.7 && < 5
 - mtl >= 2.2 && < 3
 - parsec >= 3.1 && < 4
-- recursion-schemes >= 5.1 && < 6
-- unordered-containers >= 0.2.10 && < 0.3
 - transformers >= 0.5.6 && < 0.6
 
 library:
diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs
index 6229f28..0b9d466 100644
--- a/src/Data/Fin.hs
+++ b/src/Data/Fin.hs
@@ -1,56 +1,48 @@
-{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, FlexibleInstances #-}
-module Data.Fin (Fin (Zero, Succ), toInt, pred, finRemove) where
+{-# LANGUAGE GADTs, DataKinds, KindSignatures #-}
+module Data.Fin (Fin (FZ, FS), toInt, coerceFin, pred, extract) where
 
-import Data.Functor.Foldable (Base, Recursive, project, cata)
-import Data.Injection (Injection, inject)
-import Data.Type.Nat (Nat, Zero, Succ, GTorEQ)
+import Data.Nat (Nat (S))
 import Prelude hiding (pred)
 import Unsafe.Coerce (unsafeCoerce)
 
-data Fin n where
+-- | A type with `n` inhabitants, or alternatively,
+-- | a natural number less than the upper bound parameter.
+data Fin :: Nat -> * where
   -- Fin Zero is uninhabited. Fin (Succ Zero) has one inhabitant.
-  Zero :: Nat n => Fin (Succ n)
-  Succ :: Nat n => Fin n -> Fin (Succ n)
+  FZ :: Fin ('S n)
+  FS :: Fin n -> Fin ('S n)
 
-type instance Base (Fin n) = Maybe
+instance Eq (Fin n) where
+  FZ   == FZ   = True
+  FS n == FS m = n == m
+  _    == _    = False
 
-instance (Nat n) => Injection (Fin n) (Fin (Succ n)) where
-  inject Zero = Zero
-  inject (Succ n) = Succ (inject n)
+instance Ord (Fin n) where
+  FZ   `compare` FZ   = EQ
+  FS _ `compare` FZ   = GT
+  FZ   `compare` FS _ = LT
+  FS n `compare` FS m = n `compare` m
 
-instance (Nat n) => Recursive (Fin n) where
-  project Zero     = Nothing
-  project (Succ n) = Just $ inject n
+toInt :: Fin n -> Int
+toInt FZ     = 0
+toInt (FS n) = 1 + toInt n
 
-instance (Nat n) => Eq (Fin n) where
-  Zero == Zero = True
-  Succ n == Succ m = n == m
-  _ == _ = False
-
-instance Nat n => Ord (Fin n) where
-  compare Zero     Zero     = EQ
-  compare (Succ n) Zero     = GT
-  compare Zero     (Succ n) = LT
-  compare (Succ n) (Succ m) = compare n m
-
-toInt :: Nat n => Fin n -> Int
-toInt = cata alg
-  where alg Nothing  = 0
-        alg (Just n) = n + 1
-
-instance (Nat n) => Show (Fin n) where
+instance Show (Fin n) where
   show = show . toInt
 
-pred :: Nat n => Fin (Succ n) -> Maybe (Fin n)
-pred Zero     = Nothing
-pred (Succ n) = Just n
+coerceFin :: Fin n -> Fin ('S n)
+coerceFin FZ     = FZ
+coerceFin (FS n) = FS $ coerceFin n
 
--- | Remove an element from a `Fin`'s domain.
--- | Like a generalized `pred`, only you can remove elements other than `Zero`.
-finRemove :: Nat n => Fin (Succ n) -> Fin (Succ n) -> Maybe (Fin n)
-finRemove n m
+pred :: Fin ('S n) -> Maybe (Fin n)
+pred FZ     = Nothing
+pred (FS n) = Just n
+
+-- | Match against an element in `Fin`, removing it from its domain.
+extract :: Fin ('S n) -> Fin ('S n) -> Maybe (Fin n)
+extract n m
   | n == m = Nothing
   | n >  m = pred n
   -- I am convinced it is not possible to prove to the compiler
   -- that this function is valid without `unsafeCoerce`.
-  | n <  m = Just $ unsafeCoerce n
+  | otherwise = Just $ unsafeCoerce n
diff --git a/src/Data/Injection.hs b/src/Data/Injection.hs
deleted file mode 100644
index 982a3cd..0000000
--- a/src/Data/Injection.hs
+++ /dev/null
@@ -1,11 +0,0 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
-module Data.Injection (Injection, inject) where
-
-class Injection a b where
-  inject :: a -> b
-
-instance Injection a a where
-  inject = id
-
-instance Injection a (Maybe a) where
-  inject = Just
diff --git a/src/Data/Nat.hs b/src/Data/Nat.hs
new file mode 100644
index 0000000..7550824
--- /dev/null
+++ b/src/Data/Nat.hs
@@ -0,0 +1,3 @@
+module Data.Nat (Nat (Z, S)) where
+
+data Nat = Z | S Nat
diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs
deleted file mode 100644
index c04598e..0000000
--- a/src/Data/Type/Nat.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-}
-module Data.Type.Nat (Nat, Zero, Succ, TOrdering, GT, EQ, LT, Compare, GTorEQ) where
-
-class Nat n
-data Zero
-instance Nat Zero
-data Succ n
-instance (Nat n) => Nat (Succ n)
-
-class TOrdering c
-data GT
-instance TOrdering GT
-data EQ
-instance TOrdering EQ
-data LT
-
-class Compare n m c | n m -> c
-
-instance Compare Zero Zero EQ
-instance Nat n => Compare (Succ n) Zero GT
-instance Nat n => Compare Zero (Succ n) LT
-instance (Nat n, Nat m, TOrdering c, Compare n m c) => Compare (Succ n) (Succ m) c
-
-class GTorEQ n m
-instance GTorEQ Zero Zero
-instance Nat n => GTorEQ n n
-instance Nat n => GTorEQ (Succ n) Zero
-instance (Nat n, Nat m, GTorEQ n m) => GTorEQ (Succ n) (Succ m)
diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs
index 12c209c..f54ec0b 100644
--- a/src/Data/Vec.hs
+++ b/src/Data/Vec.hs
@@ -1,28 +1,20 @@
-{-# LANGUAGE GADTs, TypeOperators, TypeSynonymInstances, FlexibleInstances #-}
-module Data.Vec (Vec (Empty, (:.)), (!.), elemIndexVec) where
+{-# LANGUAGE GADTs, TypeOperators, DataKinds #-}
+module Data.Vec (Vec (Empty, (:.)), (!.), elemIndex) where
 
-import Data.Fin (Fin (Zero, Succ))
-import Data.Type.Nat (Nat, Zero, Succ)
+import Data.Fin (Fin (FZ, FS))
+import Data.Nat (Nat (Z, S))
 
 data Vec n a where
-  Empty :: Vec Zero a
-  (:.)  :: Nat n => a -> Vec n a -> Vec (Succ n) a
+  Empty :: Vec 'Z a
+  (:.)  :: a -> Vec n a -> Vec ('S n) a
 
-instance Nat n => Functor (Vec n) where
-  fmap _ Empty     = Empty
-  fmap f (x :. xs) = f x :. fmap f xs
+(!.) :: Vec n a -> Fin n -> a
+(x :. _ ) !. FZ     = x
+(_ :. xs) !. (FS n) = xs !. n
+_         !. _      = error "Impossible"
 
-instance Nat n => Foldable (Vec n) where
-  foldr _ base Empty     = base
-  foldr f base (x :. xs) = x `f` foldr f base xs
-
-(!.) :: Nat n => Vec n a -> Fin n -> a
-(x :. _ ) !. Zero     = x
-(_ :. xs) !. (Succ n) = xs !. n
-_         !. _        = error "Impossible"
-
-elemIndexVec :: (Eq a, Nat n) => a -> Vec n a -> Maybe (Fin n)
-elemIndexVec _ Empty = Nothing
-elemIndexVec x (x' :. xs)
-  | x == x'   = Just Zero
-  | otherwise = Succ <$> elemIndexVec x xs
+elemIndex :: Eq a => a -> Vec n a -> Maybe (Fin n)
+elemIndex _ Empty = Nothing
+elemIndex x (x' :. xs)
+  | x == x'   = Just FZ
+  | otherwise = FS <$> elemIndex x xs
diff --git a/src/UntypedLambdaCalculus.hs b/src/UntypedLambdaCalculus.hs
index 0e27883..4f64cf0 100644
--- a/src/UntypedLambdaCalculus.hs
+++ b/src/UntypedLambdaCalculus.hs
@@ -1,73 +1,72 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, MultiParamTypeClasses #-}
+{-# LANGUAGE GADTs, FlexibleInstances, DataKinds #-}
 module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), eval) where
 
 import Control.Monad.Reader (Reader, runReader, withReader, reader, asks)
-import Data.Fin (Fin (Zero, Succ), finRemove)
-import Data.Injection (Injection, inject)
-import Data.Type.Nat (Nat, Succ, Zero)
+import Data.Fin (Fin (FZ, FS), extract, coerceFin)
+import Data.Functor ((<&>))
+import Data.Nat (Nat (S, Z))
 import Data.Vec (Vec (Empty, (:.)), (!.))
 
 -- | A lambda calculus expression where variables are identified
 -- | by their distance from their binding site (De Bruijn indices).
 data Expr n = Free String
             | Var (Fin n)
-            | Lam String (Expr (Succ n))
+            | Lam String (Expr ('S n))
             | App (Expr n) (Expr n)
 
-instance (Nat n) => Injection (Expr n) (Expr (Succ n)) where
-  inject (Free v)  = Free v
-  inject (Var v)   = Var $ inject v
-  inject (Lam v e) = Lam v $ inject e
-  inject (App f x) = App (inject f) (inject x)
+coerceExpr :: Expr n -> Expr ('S n)
+coerceExpr (Free v)  = Free v
+coerceExpr (Var v)   = Var $ coerceFin v
+coerceExpr (Lam v e) = Lam v $ coerceExpr e
+coerceExpr (App f x) = App (coerceExpr f) (coerceExpr x)
 
-instance Show (Expr Zero) where
-  show expr = runReader (alg expr) Empty
-    where alg :: Nat n => Expr n -> Reader (Vec n String) String
-          alg (Free v)   = return v
-          alg (Var  v)   = reader (\vars -> vars !. v ++ ':' : show v)
-          alg (Lam  v e) = do
-            body <- withReader (v :.) $ alg e
-            return $ "(\\" ++ v ++ ". " ++ body ++ ")"
-          alg (App f' x') = do
-            f <- alg f'
-            x <- alg x'
-            return $ "(" ++ f ++ " " ++ x ++ ")"
+instance Show (Expr 'Z) where
+  show expr = runReader (show' expr) Empty
+    where show' :: Expr n -> Reader (Vec n String) String
+          show' (Free v)    = return v
+          show' (Var  v)    = reader (\vars -> vars !. v ++ ':' : show v)
+          show' (Lam  v e') = withReader (v :.) (show' e') <&>
+                           \body -> "(\\" ++ v ++ ". " ++ body ++ ")"
+          show' (App f' x') = do
+                             f <- show' f'
+                             x <- show' x'
+                             return $ "(" ++ f ++ " " ++ x ++ ")"
 
 -- | Determine whether the variable bound by a lambda expression is used in its body.
 -- | This is used in eta reduction, where `(\x. f x)` reduces to `f` when `x` is not bound in `f`.
-unbound :: Nat n => Expr (Succ n) -> Bool
-unbound expr = runReader (alg expr) Zero
-  where alg :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) Bool
-        alg (Free _)  = return True
-        alg (Var v)   = reader (/= v)
-        alg (App f x) = (&&) <$> alg f <*> alg x
-        alg (Lam _ e) = withReader Succ $ alg e
+unbound :: Expr ('S n) -> Bool
+unbound expr = runReader (unbound' expr) FZ
+  where unbound' :: Expr ('S n) -> Reader (Fin ('S n)) Bool
+        unbound' (Free _)  = return True
+        unbound' (Var v)   = reader (/= v)
+        unbound' (App f x) = (&&) <$> unbound' f <*> unbound' x
+        unbound' (Lam _ e) = withReader FS $ unbound' e
 
 -- | When we bind a new variable, we enter a new scope.
 -- | Since variables are identified by their distance from their binder,
 -- | we must increment them to account for the incremented distance,
 -- | thus embedding them into the new expression.
-embed' :: Nat n => Expr n -> Expr (Succ n)
-embed' (Var v) = Var $ Succ v
-embed' o@(Lam _ _) = inject o
-embed' (Free x) = Free x
-embed' (App f x) = App (embed' f) (embed' x)
+embed :: Expr n -> Expr ('S n)
+embed   (Var v) = Var $ FS v
+embed o@(Lam _ _) = coerceExpr o
+embed   (Free x) = Free x
+embed   (App f x) = App (embed f) (embed x)
 
-subst :: Nat n => Expr n -> Expr (Succ n) -> Expr n
-subst value expr = runReader (subst' value expr) Zero
-  where subst' :: Nat n => Expr n -> Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n)
+subst :: Expr n -> Expr ('S n) -> Expr n
+subst value expr = runReader (subst' value expr) FZ
+  where subst' :: Expr n -> Expr ('S n) -> Reader (Fin ('S n)) (Expr n)
         subst' _   (Free x)  = return $ Free x
-        subst' val (Var x)   = maybe val Var <$> asks (finRemove x)
+        subst' val (Var x)   = maybe val Var <$> asks (extract x)
         subst' val (App f x) = App <$> subst' val f <*> subst' val x
-        subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (embed' val) e)
+        subst' val (Lam v e) = Lam v <$> withReader FS (subst' (embed val) e)
 
 -- | Evaluate an expression to normal form.
-eval :: Nat n => Expr n -> Expr n
+eval :: Expr n -> Expr n
 eval (App f' x) = case eval f' of
   -- Beta reduction.
   Lam _ e -> eval $ subst x e
   f -> App f (eval x)
-eval o@(Lam _ (App f (Var Zero)))
+eval o@(Lam _ (App f (Var FZ)))
   -- Eta reduction. We know that `0` is not bound in `f`,
   -- so we can simply substitute it for undefined.
   | unbound f = eval $ subst undefined f
diff --git a/src/UntypedLambdaCalculus/Parser.hs b/src/UntypedLambdaCalculus/Parser.hs
index 9b2aa60..e8ca9dd 100644
--- a/src/UntypedLambdaCalculus/Parser.hs
+++ b/src/UntypedLambdaCalculus/Parser.hs
@@ -1,15 +1,12 @@
-{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
-module UntypedLambdaCalculus.Parser (expr) where
+{-# LANGUAGE DataKinds #-}
+module UntypedLambdaCalculus.Parser (parseExpr) where
 
-import Control.Applicative (liftA)
 import Control.Monad.Reader (ReaderT, runReaderT, withReaderT, mapReaderT, ask)
 import Control.Monad.Trans.Class (lift)
-import Data.Functor (void)
 import Data.List (foldl1')
-import Data.Type.Nat (Nat, Zero )
-import Data.Vec (Vec (Empty, (:.)), elemIndexVec)
-import Text.Parsec hiding (Empty)
-import Unsafe.Coerce (unsafeCoerce)
+import Data.Nat (Nat (Z))
+import Data.Vec (Vec (Empty, (:.)), elemIndex)
+import Text.Parsec (Parsec, SourceName, ParseError, many, sepBy1, letter, alphaNum, char, between, (<|>), spaces, parse)
 import UntypedLambdaCalculus (Expr (Free, Var, Lam, App))
 
 type Parser s a = ReaderT s (Parsec String ()) a
@@ -22,36 +19,26 @@ name = do
   return $ c : cs
 
 -- | A variable expression.
-var :: Nat n => Parser (Vec n String) (Expr n)
+var :: Parser (Vec n String) (Expr n)
 var = do
   varn <- lift name
   bound <- ask
-  return $ maybe (Free varn) Var $ elemIndexVec varn bound
+  return $ maybe (Free varn) Var $ elemIndex varn bound
 
 -- | Run parser between parentheses.
 parens :: Parsec String () a -> Parsec String () a
-parens p = do
-  _ <- char '('
-  x <- p
-  _ <- char ')'
-  return x
+parens = between (char '(') (char ')')
 
 -- | A lambda expression.
-lam :: Nat n => Parser (Vec n String) (Expr n)
+lam :: Parser (Vec n String) (Expr n)
 lam = do
-  vars <- lift $ do
-    _ <- char '\\'
-    vars <- name `sepBy1` spaces
-    _ <- char '.'
-    spaces
-    return vars
-  help vars
-  where help :: Nat n => [String] -> Parser (Vec n String) (Expr n)
+  (lift $ between (char '\\') (char '.' >> spaces) $ name `sepBy1` spaces) >>= help
+  where help :: [String] -> Parser (Vec n String) (Expr n)
         help []     = app
         help (v:vs) = Lam v <$> withReaderT (v :.) (help vs)
 
 -- | An application expression.
-app :: Nat n => Parser (Vec n String) (Expr n)
+app :: Parser (Vec n String) (Expr n)
 app = foldl1' App <$> mapReaderT (`sepBy1` spaces) safeExpr
 
 ll :: (Parsec String () a -> Parsec String () b -> Parsec String () c) -> Parser s a -> Parser s b -> Parser s c
@@ -62,10 +49,10 @@ ll f p1 p2 = do
 -- | An expression, but where applications must be surrounded by parentheses,
 -- | to avoid ambiguity (infinite recursion on `app` in the case where the first
 -- | expression in the application is also an `app`, consuming no input).
-safeExpr :: Nat n => Parser (Vec n String) (Expr n)
+safeExpr :: Parser (Vec n String) (Expr n)
 safeExpr = ll (<|>) var $ ll (<|>) lam $ mapReaderT parens (ll (<|>) lam app)
 
 -- | Since applications do not require parentheses and can contain only a single item,
 -- | the `app` parser is sufficient to parse any expression at all.
-expr :: SourceName -> String -> Either ParseError (Expr Zero)
-expr sourceName code = parse (runReaderT app Empty) sourceName code
+parseExpr :: SourceName -> String -> Either ParseError (Expr 'Z)
+parseExpr sourceName code = parse (runReaderT app Empty) sourceName code