diff --git a/ChangeLog.md b/ChangeLog.md
--- a/ChangeLog.md
+++ b/ChangeLog.md
@@ -1,3 +1,14 @@
 # Changelog for type-errors
 
+## 0.2.0.0 (2019-07-03)
+
+### Breaking Changes
+
+- The `UnlessPhantom` and various `Subst` type families were broken in the
+    presence of stuckness. This rendered them almost entirely unusable --- so
+    they now have a new implementation in terms of `te`.
+- Added `te`, a TemplateHaskell splice, which will perform symbolic
+    substitutions over types. See haddock for the migration details.
+
 ## Unreleased changes
+
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -26,7 +26,7 @@
 
 This project wouldn't be possible without the help of two amazing people:
 
-* [ksongor](https://kcsongor.github.io/) who came up with the original
+* [kcsongor](https://kcsongor.github.io/) who came up with the original
   technology behind this library.
 * [Lysxia](https://blog.poisson.chat/) for articulating the approach to making
   `IfStuck` work for things of all kinds, and for helping me with the
diff --git a/src/Type/Errors.hs b/src/Type/Errors.hs
--- a/src/Type/Errors.hs
+++ b/src/Type/Errors.hs
@@ -1,3 +1,8 @@
+------------------------------------------------------------------------------
+-- | This module provides useful tools for writing better type-errors. For
+-- a quickstart guide to the underlying 'GHC.TypeLits.TypeError' machinery,
+-- check out Dmitrii Kovanikov's excellent blog post
+-- <https://chshersh.github.io/type-errors A story told by Type Errors>.
 module Type.Errors
   ( -- * Generating Error Messages
     ErrorMessage (..)
@@ -16,10 +21,12 @@
   , WhenStuck
   , UnlessStuck
 
+    -- * Running Magic Stuck Type Families
+  , te
+
     -- * Observing Phantomness
   , PHANTOM
   , UnlessPhantom
-  , UnlessPhantomFcf
 
     -- * Performing Type Substitutions
   , Subst
@@ -32,10 +39,14 @@
   , Pure
   ) where
 
-import Data.Coerce
-import Data.Kind
-import Fcf
-import GHC.TypeLits
+import           Control.Applicative
+import           Data.Coerce
+import           Data.Generics
+import           Data.Kind
+import           Fcf
+import           GHC.TypeLits
+import qualified Language.Haskell.TH as TH
+import           Language.Haskell.TH hiding (Type, Exp)
 
 
 
@@ -168,7 +179,46 @@
 --
 -- @since 0.1.0.0
 type family IfStuck (expr :: k) (b :: k1) (c :: Exp k1) :: k1 where
-  IfStuck (_ AnythingOfAnyKind) b c = b
+  -- The type pattern @_ Foo@ is interpretered by the compiler as being of
+  -- any kind. This is great and exactly what we want here, except that things
+  -- like @forall s. Maybe s@ will get stuck on it.
+  --
+  -- So instead, we just propagate out 100 of these type variables and assume
+  -- that 100 type variables ought to be enough for anyone.
+  IfStuck (_ AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind AnythingOfAnyKind AnythingOfAnyKind
+             AnythingOfAnyKind) b c = b
   IfStuck a                     b c = Eval c
 
 data AnythingOfAnyKind
@@ -205,26 +255,93 @@
 -- This can be used to ensure an expression /isn't/ stuck before analyzing it
 -- further.
 --
--- See the example under 'UnlessPhantomFcf' for an example of this use-case.
+-- See the example under 'UnlessPhantom' for an example of this use-case.
 --
 -- @since 0.1.0.0
 type UnlessStuck expr c = IfStuck expr NoError c
 
 
 ------------------------------------------------------------------------------
--- | A meta-variable for marking which argument should be a phantom when
--- working with 'UnlessPhantom' and 'UnlessPhantomFcf'.
+-- | This library provides tools for performing lexical substitutions over
+-- types. For example, the function 'UnlessPhantom' asks you to mark phantom
+-- variables via 'PHANTOM'.
 --
+-- Unfortunately, this substitution cannot reliably be performed via
+-- type families, since it will too often get stuck. Instead we provide 'te',
+-- which is capable of reasoning about types symbolically.
+--
+-- Any type which comes with the warning /"This type family is always stuck."/
+-- __must__ be used in the context of 'te' and the magic @[t|@ quasiquoter. To
+-- illustrate, the following is stuck:
+--
+-- >>> :{
+-- foo :: SubstVar VAR Bool
+-- foo = True
+-- :}
+-- ...
+-- ... Couldn't match expected type ...SubstVar VAR Bool...
+-- ... with actual type ...Bool...
+-- ...
+--
+-- But running it via 'te' makes everything work:
+--
+-- >>> :{
+-- foo :: $(te[t| SubstVar VAR Bool |])
+-- foo = True
+-- :}
+--
+-- If you don't want to think about when to use 'te', it's a no-op when used
+-- with everyday types:
+--
+-- >>> :{
+-- bar :: $(te[t| Bool |])
+-- bar = True
+-- :}
+--
+-- @since 0.2.0.0
+te :: Q TH.Type -> Q TH.Type
+te = liftA $ everywhere $ mkT parseSubst
+
+
+replaceWhen :: Data a => TH.Type -> TH.Type -> a -> a
+replaceWhen a b = everywhere $ mkT $ \case
+  x | x == a -> b
+  x -> x
+
+
+parseSubst :: TH.Type -> TH.Type
+parseSubst (ConT phantom `AppT` expr `AppT` msg)
+  | phantom == ''UnlessPhantom =
+    ConT ''Coercible
+      `AppT` (replaceWhen (ConT ''PHANTOM) (ConT ''Stuck) expr)
+      `AppT` (replaceWhen (ConT ''PHANTOM)
+                          (ConT ''DelayError `AppT` msg)
+                          expr)
+parseSubst (ConT subst `AppT` t `AppT` a `AppT` b)
+  | subst == ''Subst = replaceWhen a b t
+parseSubst (ConT subst `AppT` t `AppT` b)
+  | subst == ''SubstVar = replaceWhen (ConT ''VAR) b t
+parseSubst a = a
+
+
+------------------------------------------------------------------------------
+-- | __This type family is always stuck. It must be used in the context of 'te'.__
+--
+-- A meta-variable for marking which argument should be a phantom when working
+-- with 'UnlessPhantom'.
+--
 -- 'PHANTOM' is polykinded and can be used in several settings.
 --
 -- See 'UnlessPhantom' for examples.
 --
 -- @since 0.1.0.0
-type PHANTOM = VAR
+type family PHANTOM :: k
 
 
 ------------------------------------------------------------------------------
--- | @'UnlessPhantom' expr err@ determines if the type described by @expr@
+-- | __This type family is always stuck. It must be used in the context of 'te'.__
+--
+-- @'UnlessPhantom' expr err@ determines if the type described by @expr@
 -- is phantom in the variables marked via 'PHANTOM'. If it's not, it produces
 -- the error message @err@.
 --
@@ -236,12 +353,12 @@
 --
 -- which is phantom in @a@:
 --
--- >>> :eval_error UnlessPhantom (Qux PHANTOM Int) ('Text "Ok")
+-- >>> :eval_error $(te[t| UnlessPhantom (Qux PHANTOM Int) ('Text "Ok") |])
 -- ()
 --
 -- but not in @b@:
 --
--- >>> :eval_error UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!")
+-- >>> :eval_error $(te[t| UnlessPhantom (Qux Int PHANTOM) ('Text "Bad!") |])
 -- ...
 -- ... Bad!
 -- ...
@@ -249,106 +366,106 @@
 -- Unfortunately there is no known way to emit an error message if the variable
 -- /is/ a phantom.
 --
--- @since 0.1.0.0
-type UnlessPhantom exp err = Eval (UnlessPhantomFcf exp err)
-
-
-------------------------------------------------------------------------------
--- | Like 'UnlessPhantom', but implemented as a first-class family. As such,
--- this allows 'UnlessPhantomFcf' to be chained after 'IfStuck' to only be run
--- if an expression isn't stuck.
+-- Often you'll want to guard 'UnlessPhantom' against 'IfStuck', to ensure you
+-- don't get errors when things are merely ambiguous. You can do this by
+-- writing your own fcf whose implementation is 'UnlessPhantom':
 --
--- This can be used to avoid emitting false error messages when a type variable
--- isn't phantom, just ambiguous.
+-- >>> :{
+-- data NotPhantomErrorFcf :: k -> Exp Constraint
+-- type instance Eval (NotPhantomErrorFcf f) =
+--   $(te[t| UnlessPhantom (f PHANTOM)
+--                         ( ShowTypeQuoted f
+--                    ':<>: 'Text " is not phantom in its argument!")
+--         |])
+-- :}
 --
 -- >>> :{
 -- observe_phantom
 --     :: UnlessStuck
 --          f
---          (UnlessPhantomFcf
---            (f PHANTOM)
---            ('Text "It's not phantom!"))
+--          (NotPhantomErrorFcf f)
 --     => f p
 --     -> ()
 -- observe_phantom _ = ()
 -- :}
 --
+-- We then notice that using @observe_phantom@ against 'Data.Proxy.Proxy'
+-- doesn't produce any errors, but against 'Maybe' does:
+--
 -- >>> observe_phantom Proxy
 -- ()
 --
 -- >>> observe_phantom (Just 5)
 -- ...
--- ... It's not phantom!
+-- ... 'Maybe' is not phantom in its argument!
 -- ...
 --
--- In the next example, we leave @observe_phantom@ unsaturated, and therefore
--- @f@ isn't yet known. Without guarding the 'UnlessPhantomFcf' behind
--- 'UnlessStuck', this would incorrectly produce the message "It's not
--- phantom!"
+-- Finally, we leave @observe_phantom@ unsaturated, and therefore @f@ isn't yet
+-- known. Without guarding the 'UnlessPhantom' behind 'UnlessStuck', this would
+-- incorrectly produce the message "'f' is not phantom in its argument!"
 --
 -- >>> observe_phantom
 -- ...
--- ... No instance for (Show ...
+-- ... No instance for (Show (f0 p0 -> ()))
 -- ...
 --
--- @since 0.1.0.0
-data UnlessPhantomFcf :: k -> ErrorMessage -> Exp Constraint
-type instance Eval (UnlessPhantomFcf exp err) =
-  Coercible (SubstVar exp Stuck)
-            (SubstVar exp (DelayError err))
+-- @since 0.2.0.0
+type family UnlessPhantom :: k -> ErrorMessage -> Constraint
 
 
 ------------------------------------------------------------------------------
--- | @'Subst' expr a b@ substitutes all instances of @a@ for @b@ in @expr@.
+-- | __This type family is always stuck. It must be used in the context of 'te'.__
 --
--- >>> :kind! Subst (Either Int Int) Int Bool
+-- @'Subst' expr a b@ substitutes all instances of @a@ for @b@ in @expr@.
+--
+-- >>> :kind! $(te[t| Subst (Either Int Int) Int Bool |])
 -- ...
 -- = Either Bool Bool
 --
--- >>> :kind! Subst (Either Int Bool) Int [Char]
+-- >>> :kind! $(te[t| Subst (Either Int Bool) Int [Char] |])
 -- ...
 -- = Either [Char] Bool
 --
--- >>> :kind! Subst (Either Int Bool) Either (->)
+-- >>> :kind! $(te[t| Subst (Either Int Bool) Either (,) |])
 -- ...
--- = Int -> Bool
+-- = (Int, Bool)
 --
--- @since 0.1.0.0
-type family Subst (e :: k1) (var :: k2) (sub :: k2) :: k1 where
-  Subst var var sub   = sub
-  Subst (a b) var sub = Subst a var sub (Subst b var sub)
-  Subst a var sub     = a
+-- @since 0.2.0.0
+type family Subst :: k1 -> k1 -> k2 -> k2
 
-data Var
-type family SubMe :: Type -> k
 
 ------------------------------------------------------------------------------
--- | 'VAR' is a meta-varaible which marks a substitution in 'SubstVar'. The
+-- | __This type family is always stuck. It must be used in the context of 'te'.__
+--
+-- 'VAR' is a meta-varaible which marks a substitution in 'SubstVar'. The
 -- result of @'SubstVar' expr val@ is @expr[val/'VAR']@.
 --
 -- 'VAR' is polykinded and can be used in several settings.
 --
 -- See 'SubstVar' for examples.
 --
--- @since 0.1.0.0
-type VAR = SubMe Var
+-- @since 0.2.0.0
+type family VAR :: k
 
 
 ------------------------------------------------------------------------------
--- | Like 'Subst', but uses the explicit meta-variable 'VAR' to mark
--- substitution points.
+-- | __This type family is always stuck. It must be used in the context of 'te'.__
 --
--- >>> :kind! SubstVar (Either VAR Bool) [Char]
+-- Like 'Subst', but uses the explicit meta-variable 'VAR' to mark substitution
+-- points.
+--
+-- >>> :kind! $(te[t| SubstVar (Either VAR VAR) Bool |])
 -- ...
+-- = Either Bool Bool
+--
+-- >>> :kind! $(te[t| SubstVar (Either VAR Bool) [Char] |])
+-- ...
 -- = Either [Char] Bool
 --
--- >>> :kind! SubstVar (VAR Int Bool :: Type) (->)
+-- >>> :kind! $(te[t| SubstVar (VAR Int Bool) (,) |])
 -- ...
--- = Int -> Bool
+-- = (Int, Bool)
 --
--- @since 0.1.0.0
-type family SubstVar (e :: k1) (r :: k2) :: k1 where
-  SubstVar (_ Var) r = r
-  SubstVar (a b) r   = SubstVar a r (SubstVar b r)
-  SubstVar a r       = a
+-- @since 0.2.0.0
+type family SubstVar :: k1 -> k2 -> k2
 
diff --git a/test/Main.hs b/test/Main.hs
--- a/test/Main.hs
+++ b/test/Main.hs
@@ -15,14 +15,16 @@
   , "-package first-class-families"
   , "-XConstraintKinds"
   , "-XDataKinds"
+  , "-XFlexibleContexts"
   , "-XKindSignatures"
+  , "-XLambdaCase"
   , "-XPolyKinds"
   , "-XScopedTypeVariables"
+  , "-XTemplateHaskell"
+  , "-XTypeApplications"
   , "-XTypeFamilies"
   , "-XTypeOperators"
   , "-XUndecidableInstances"
-  , "-XTypeApplications"
-  , "-XFlexibleContexts"
 
 #if __GLASGOW_HASKELL__ < 806
   , "-XTypeInType"
diff --git a/type-errors.cabal b/type-errors.cabal
--- a/type-errors.cabal
+++ b/type-errors.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: c34b99cb7785b40b9930c5de60ab842dfd436ec4458a51b595b426da5fcd4a3f
+-- hash: 89d18eac6ec0d221b9fa775523c8c4417ebbfa1c65bbcbf42c0f8569fd040337
 
 name:           type-errors
-version:        0.1.0.0
+version:        0.2.0.0
 synopsis:       Tools for writing better type errors
 description:    Please see the README on GitHub at <https://github.com/isovector/type-errors#readme>
 category:       Type
@@ -34,11 +34,14 @@
       Paths_type_errors
   hs-source-dirs:
       src
-  default-extensions: ConstraintKinds DataKinds PolyKinds ScopedTypeVariables TypeFamilies TypeOperators UndecidableInstances TypeApplications FlexibleContexts
+  default-extensions: ConstraintKinds DataKinds FlexibleContexts LambdaCase PolyKinds ScopedTypeVariables TemplateHaskellQuotes TypeApplications TypeFamilies TypeOperators UndecidableInstances
   ghc-options: -Wall
   build-depends:
       base >=4.7 && <5
     , first-class-families >=0.5.0.0
+    , syb
+    , template-haskell
+    , th-abstraction
   if impl(ghc < 8.6)
     default-extensions: TypeInType
   default-language: Haskell2010
@@ -50,12 +53,15 @@
       Paths_type_errors
   hs-source-dirs:
       test
-  default-extensions: ConstraintKinds DataKinds PolyKinds ScopedTypeVariables TypeFamilies TypeOperators UndecidableInstances TypeApplications FlexibleContexts
+  default-extensions: ConstraintKinds DataKinds FlexibleContexts LambdaCase PolyKinds ScopedTypeVariables TemplateHaskellQuotes TypeApplications TypeFamilies TypeOperators UndecidableInstances
   ghc-options: -Wall -threaded -rtsopts -with-rtsopts=-N
   build-depends:
       base >=4.7 && <5
     , doctest >=0.16.0.1 && <0.17
     , first-class-families >=0.5.0.0
+    , syb
+    , template-haskell
+    , th-abstraction
     , type-errors
   if impl(ghc < 8.6)
     default-extensions: TypeInType