diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -2,4 +2,23 @@
 
 [![CircleCI](https://circleci.com/gh/ejconlon/blanks/tree/master.svg?style=svg)](https://circleci.com/gh/ejconlon/blanks/tree/master)
 
-Fill-in-the-blanks - A library factoring out substitution from ASTs. (Not production ready!)
+Fill-in-the-blanks - A library factoring out substitution from ASTs.
+
+It's a pain to track de Bruijn indices yourself to implement capture-avoiding subsititution,
+so this library provides some wrappers that help. One of the best libraries for this is
+[bound](https://hackage.haskell.org/package/bound), which uses a clever representation to make
+these operations safe and fast. The tradeoff is that you have to define a `Monad` instance
+for your expression functor, which in practice can be tricky. (It's even trickier to derive
+`Eq` and `Show`!)
+
+This library takes the simpler, slower, and rather "succ-y" free-monad-ish approach,
+but with a twist. It expects you to rewrite all name-binding constructors in your expression
+as annotations on a single "binder" constructor. This allows you to use the provided `Scope`
+type (or a variant) as a wrapper around your expression functor, which is only required to
+implement `Functor`. This representation is less safe (since you can inspect and manipulate
+bound variables), but if you stick to the provided combinators, things will work out fine.
+
+You'll get most of what you want by just importing this module unqualified.
+See the `Blanks` class definition and related methods to manipulate variables and abstractions.
+See `Scope` for the basic wrapper and `LocScope` for a wrapper with annotations you can use
+for source locations and the like. See the test suite for examples.
diff --git a/app/Main.hs b/app/Main.hs
deleted file mode 100644
--- a/app/Main.hs
+++ /dev/null
@@ -1,5 +0,0 @@
-module Main where
-
--- TODO(ejconlon) Create demo app
-main :: IO ()
-main = pure ()
diff --git a/blanks.cabal b/blanks.cabal
--- a/blanks.cabal
+++ b/blanks.cabal
@@ -1,13 +1,13 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.31.2.
+-- This file has been generated from package.yaml by hpack version 0.33.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 6dd5dac29a7eb8991e9d2728daa61f8651bf8e283305aa1063f1daf4dce65fd8
+-- hash: dce6fa2995f08e5b1615eab81bbbbb7339ba49c1db0902125b8495fc24c84bd1
 
 name:           blanks
-version:        0.3.0
+version:        0.4.0
 synopsis:       Fill-in-the-blanks - A library factoring out substitution from ASTs
 description:    Please see the README on GitHub at <https://github.com/ejconlon/blanks#readme>
 category:       Language
@@ -29,64 +29,51 @@
 library
   exposed-modules:
       Blanks
-      Blanks.Class
+      Blanks.Interface
+      Blanks.Located
       Blanks.LocScope
       Blanks.Name
-      Blanks.PureScope
-      Blanks.RightAdjunct
-      Blanks.ScopeT
+      Blanks.NatNewtype
+      Blanks.Scope
+      Blanks.ScopeW
       Blanks.Sub
       Blanks.UnderScope
   other-modules:
       Paths_blanks
   hs-source-dirs:
       src
-  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies
+  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds
   build-depends:
-      adjunctions >=4.4
-    , base >=4.12 && <5
-    , containers >=0.6
-    , distributive >=0.6
-    , mtl >=2.2
-  default-language: Haskell2010
-
-executable blanks-exe
-  main-is: Main.hs
-  other-modules:
-      Paths_blanks
-  hs-source-dirs:
-      app
-  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies
-  ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds -threaded -rtsopts -with-rtsopts=-N
-  build-depends:
-      adjunctions >=4.4
+      adjunctions >=4.4 && <5
     , base >=4.12 && <5
-    , blanks
-    , containers >=0.6
-    , distributive >=0.6
-    , mtl >=2.2
+    , containers >=0.6 && <1
+    , distributive >=0.6 && <1
+    , mtl >=2.2 && <3
   default-language: Haskell2010
 
 test-suite blanks-test
   type: exitcode-stdio-1.0
-  main-is: Tasty.hs
+  main-is: Main.hs
   other-modules:
       Test.Blanks.Assertions
-      Test.Blanks.BlanksTest
+      Test.Blanks.LocScopeTest
+      Test.Blanks.Parsing
+      Test.Blanks.ScopeTest
       Paths_blanks
   hs-source-dirs:
       test
-  default-extensions: BangPatterns DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses Rank2Types TypeFamilies
+  default-extensions: BangPatterns ConstraintKinds DeriveFunctor DeriveFoldable DeriveGeneric DeriveTraversable FlexibleContexts FlexibleInstances FunctionalDependencies GeneralizedNewtypeDeriving KindSignatures MultiParamTypeClasses PatternSynonyms Rank2Types TypeFamilies
   ghc-options: -Wall -Wcompat -Widentities -Wincomplete-record-updates -Wincomplete-uni-patterns -Wpartial-fields -Wredundant-constraints -fno-warn-unused-top-binds -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      adjunctions >=4.4
+      adjunctions >=4.4 && <5
     , base >=4.12 && <5
     , blanks
-    , containers >=0.6
-    , distributive >=0.6
-    , mtl >=2.2
+    , containers >=0.6 && <1
+    , distributive >=0.6 && <1
+    , megaparsec
+    , mtl >=2.2 && <3
     , tasty
-    , tasty-discover
     , tasty-hunit
+    , text
   default-language: Haskell2010
diff --git a/src/Blanks.hs b/src/Blanks.hs
--- a/src/Blanks.hs
+++ b/src/Blanks.hs
@@ -1,12 +1,30 @@
+-- | Fill-in-the-blanks - A library factoring out substitution from ASTs.
+--
+-- It's a pain to track de Bruijn indices yourself to implement capture-avoiding subsititution,
+-- so this library provides some wrappers that help. One of the best libraries for this is
+-- <https://hackage.haskell.org/package/bound bound>, which uses a clever representation to make
+-- these operations safe and fast. The tradeoff is that you have to define a 'Monad' instance
+-- for your expression functor, which in practice can be tricky. (It's even trickier to derive
+-- 'Eq' and 'Show'!)
+--
+-- This library takes the simpler, slower, and rather "succ-y" free-monad-ish approach,
+-- but with a twist. It expects you to rewrite all name-binding constructors in your expression
+-- as annotations on a single "binder" constructor. This allows you to use the provided 'Scope'
+-- type (or a variant) as a wrapper around your expression functor, which is only required to
+-- implement 'Functor'. This representation is less safe (since you can inspect and manipulate
+-- bound variables), but if you stick to the provided combinators, things will work out fine.
+--
+-- You'll get most of what you want by just importing this module unqualified.
+-- See the 'Blanks' class definition and related methods to manipulate variables and abstractions.
+-- See 'Scope' for the basic wrapper and 'LocScope' for a wrapper with annotations you can use
+-- for source locations and the like. See the test suite for examples.
 module Blanks
   ( module Blanks
   ) where
 
-import Blanks.Class as Blanks
+import Blanks.Interface as Blanks
+import Blanks.Located as Blanks
 import Blanks.LocScope as Blanks
 import Blanks.Name as Blanks
-import Blanks.PureScope as Blanks
-import Blanks.RightAdjunct as Blanks
-import Blanks.ScopeT as Blanks
+import Blanks.Scope as Blanks
 import Blanks.Sub as Blanks
-import Blanks.UnderScope as Blanks
diff --git a/src/Blanks/Class.hs b/src/Blanks/Class.hs
deleted file mode 100644
--- a/src/Blanks/Class.hs
+++ /dev/null
@@ -1,53 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-
-module Blanks.Class
-  ( BlankAbstract (..)
-  , BlankCodomain
-  , BlankEmbed (..)
-  , BlankFunctor
-  , BlankInfo
-  ) where
-
-import Blanks.Sub (SubError)
-import Data.Sequence (Seq)
-import qualified Data.Sequence as Seq
-
-type family BlankInfo (m :: * -> *) :: *
-type family BlankFunctor (m :: * -> *) :: * -> *
-type family BlankCodomain (m :: * -> *) :: * -> *
-
-class BlankEmbed (m :: * -> *) where
-  -- | "embed functor"
-  blankEmbed :: BlankFunctor m (m a) -> BlankCodomain m (m a)
-
-class BlankAbstract (m :: * -> *) where
-  -- | "free name"
-  blankFree :: a -> BlankCodomain m (m a)
-
-  -- | "abstract info names body"
-  blankAbstract :: Eq a => BlankInfo m -> Seq a -> m a -> BlankCodomain m (m a)
-
-  -- | 'blankAbstract' for a single argument
-  blankAbstract1 :: Eq a => BlankInfo m -> a -> m a -> BlankCodomain m (m a)
-  blankAbstract1 n k = blankAbstract n (Seq.singleton k)
-
-  -- | "unAbstract names body"
-  blankUnAbstract :: Seq a -> m a -> m a
-
-  -- 'blankUnAbstract' for a single argument
-  blankUnAbstract1 :: a -> m a -> m a
-  blankUnAbstract1 = blankUnAbstract . Seq.singleton
-
-  -- | "instantiate args body"
-  blankInstantiate :: Seq (BlankCodomain m (m a)) -> m a -> m a
-
-  -- | 'blankInstantiate' for a single argument
-  blankInstantiate1 :: BlankCodomain m (m a) -> m a -> m a
-  blankInstantiate1 = blankInstantiate . Seq.singleton
-
-  -- | "apply args abstraction"
-  blankApply :: Seq (BlankCodomain m (m a)) -> m a -> Either SubError (m a)
-
-  -- | 'blankApply' for a single argument
-  blankApply1 :: BlankCodomain m (m a) -> m a -> Either SubError (m a)
-  blankApply1 = blankApply . Seq.singleton
diff --git a/src/Blanks/Interface.hs b/src/Blanks/Interface.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/Interface.hs
@@ -0,0 +1,209 @@
+module Blanks.Interface
+  ( Blank
+  , BlankLeft
+  , BlankRight
+  , BlankInfo
+  , BlankFunctor
+  , BlankRawFold
+  , BlankFold
+  , BlankPair
+  , blankFree
+  , blankEmbed
+  , blankAbstract
+  , blankAbstract1
+  , blankUnAbstract
+  , blankUnAbstract1
+  , blankInstantiate
+  , blankInstantiate1
+  , blankApply
+  , blankApply1
+  , blankApplyThrow
+  , blankApply1Throw
+  , blankBind
+  , blankBindOpt
+  , blankLift
+  , blankRawFold
+  , blankFold
+  , blankLiftAnno
+  , blankHoistAnno
+  , blankMapAnno
+  ) where
+
+import Blanks.NatNewtype (NatNewtype)
+import Blanks.ScopeW
+import Blanks.Sub (SubError, ThrowSub, rethrowSub)
+import Blanks.UnderScope (UnderScopeFold)
+import Data.Functor.Adjunction (Adjunction)
+import Data.Kind (Type)
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+
+-- | The left adjoint functor used by 'g'.
+type family BlankLeft (g :: Type -> Type) :: Type -> Type
+
+-- | The right adjoint functor used by 'g'
+type family BlankRight (g :: Type -> Type) :: Type -> Type
+
+-- | The binder info used by 'g'.
+type family BlankInfo (g :: Type -> Type) :: Type
+
+-- | The expression functor used by 'g'.
+type family BlankFunctor (g :: Type -> Type) :: Type -> Type
+
+type BlankRawFold (g :: Type -> Type) (a :: Type) (r :: Type) = UnderScopeFold (BlankInfo g) (BlankFunctor g) (g a) a r
+type BlankFold (g :: Type -> Type) (a :: Type) (r :: Type) = BlankRawFold g a (BlankRight g r)
+
+-- | Indicates that 'g' is a "scope" functor we can use for name-binding. (Behind-the-scenes, 'g' must
+-- be a newtype wrapper over the 'ScopeW' datatype.) Most of the time you will use 'Scope' or 'LocScope'
+-- directly, which are instances of this class.
+--
+-- We use the pair of adjoint functors indexed by 'g' to shift the burden of operating in context
+-- where it is more convenient. For example, 'LocScope' uses a pair of functors that are
+-- essentially 'Env' and 'Reader'. The left adjoint 'Env' lets us annotate every level of our
+-- expression tree with a location, and the right adjoint 'Reader' informs us of that location
+-- so we don't have to make one up out of thin air!
+--
+-- 'Scope' uses the pair of functors 'Identity' and 'Identity', which means there is
+-- no ability to store any additional information in the tree, but there's also no additional
+-- burden to provide that information.
+class
+  ( Adjunction (BlankLeft g) (BlankRight g)
+  , Applicative (BlankRight g)
+  , Functor (BlankFunctor g)
+  , NatNewtype (ScopeW (BlankLeft g) (BlankInfo g) (BlankFunctor g) g) g
+  ) => Blank (g :: Type -> Type)
+
+-- | A pair of 'Blank' functors that index the same info and embedded functors. Used to change adjoint functors.
+type BlankPair g h = (Blank g, Blank h, BlankInfo g ~ BlankInfo h, BlankFunctor g ~ BlankFunctor h)
+
+-- | Creates a free variable in context.
+blankFree ::
+  Blank g
+  => a -- ^ The name of the free variable
+  -> BlankRight g (g a)
+blankFree = scopeWFree
+{-# INLINE blankFree #-}
+
+-- | Embeds an expression functor in context.
+blankEmbed ::
+  Blank g
+  => BlankFunctor g (g a) -- ^ An expression
+  -> BlankRight g (g a)
+blankEmbed = scopeWEmbed
+{-# INLINE blankEmbed #-}
+
+-- | Binds free variables in an expression and returns a binder.
+blankAbstract ::
+  (Blank g, Eq a)
+  => BlankInfo g -- ^ Annotation specific to your expression functor.
+                 -- Might contain original variable names and types, or might
+                 -- mark this as a "let" vs a "lambda".
+  -> Seq a -- ^ Free variables to bind, like the names of function parameters
+  -> g a -- ^ The expression to bind in, like the body of a function
+  -> BlankRight g (g a)
+blankAbstract = scopeWAbstract
+{-# INLINE blankAbstract #-}
+
+-- | 'blankAbstract' for a single argument.
+blankAbstract1 :: (Blank g, Eq a) => BlankInfo g -> a -> g a -> BlankRight g (g a)
+blankAbstract1 n k = scopeWAbstract n (Seq.singleton k)
+{-# INLINE blankAbstract1 #-}
+
+-- | Un-bind free variables in an expression. Basically the inverse of
+-- 'blankAbstract'. Take care to match the arity of the binder! ('blankApply' is safer.)
+blankUnAbstract ::
+  Blank g
+  => Seq a -- ^ The names of the variables you're freeing
+  -> g a -- ^ The expression to substitutue in (typically a binder)
+  -> g a
+blankUnAbstract = scopeWUnAbstract
+{-# INLINE blankUnAbstract #-}
+
+-- 'blankUnAbstract' for a single argument.
+blankUnAbstract1 :: Blank g => a -> g a -> g a
+blankUnAbstract1 = scopeWUnAbstract . Seq.singleton
+{-# INLINE blankUnAbstract1 #-}
+
+-- | Instantiate the bound variables in an expression with other expressions.
+-- Take care to match the arity of the binder! ('blankApply' is safer.)
+blankInstantiate ::
+  Blank g
+  => Seq (BlankRight g (g a)) -- ^ Expressions to substitute in place of bound vars
+  -> g a -- ^ The expression to substitute in (typically a binder)
+  -> g a
+blankInstantiate = scopeWInstantiate
+{-# INLINE blankInstantiate #-}
+
+-- | 'blankInstantiate' for a single argument.
+blankInstantiate1 :: Blank g => BlankRight g (g a) -> g a -> g a
+blankInstantiate1 = scopeWInstantiate . Seq.singleton
+{-# INLINE blankInstantiate1 #-}
+
+-- | Instantiates the bound variables in an expression with other expressions.
+-- Throws errors on mismatched arity, non binder expression, unbound vars, etc.
+-- A version of 'blankInstantiate' that fails loudly instead of silently!
+blankApply ::
+  Blank g
+  => Seq (BlankRight g (g a)) -- ^ Expressions to substitute in place of bound vars
+  -> g a -- ^ The binder expression to substitute in
+  -> Either SubError (g a)
+blankApply = scopeWApply
+{-# INLINE blankApply #-}
+
+-- | 'blankApply' for a single argument.
+blankApply1 :: Blank g => BlankRight g (g a) -> g a -> Either SubError (g a)
+blankApply1 = scopeWApply . Seq.singleton
+{-# INLINE blankApply1 #-}
+
+-- | A 'ThrowSub' version of 'blankApply'.
+blankApplyThrow :: (Blank g, ThrowSub m, Applicative m) => Seq (BlankRight g (g a)) -> g a -> m (g a)
+blankApplyThrow ks = rethrowSub . scopeWApply ks
+{-# INLINE blankApplyThrow #-}
+
+-- | A 'ThrowSub' version of 'blankApply1'.
+blankApply1Throw :: (Blank g, ThrowSub m, Applicative m) => BlankRight g (g a) -> g a -> m (g a)
+blankApply1Throw k = rethrowSub . scopeWApply (Seq.singleton k)
+{-# INLINE blankApply1Throw #-}
+
+-- | Substitution as a kind of monadic bind.
+blankBind :: Blank g => (a -> BlankRight g (g b)) -> g a -> g b
+blankBind = scopeWBind
+{-# INLINE blankBind #-}
+
+-- | Optional substitution as another kind of monadic bind.
+blankBindOpt :: Blank g => (a -> Maybe (BlankRight g (g a))) -> g a -> g a
+blankBindOpt = scopeWBindOpt
+{-# INLINE blankBindOpt #-}
+
+-- | Lift an expression functor into the scope functor.
+blankLift :: (Blank g, Monad (BlankRight g), Traversable (BlankFunctor g)) => BlankFunctor g a -> BlankRight g (g a)
+blankLift = scopeWLift
+{-# INLINE blankLift #-}
+
+-- | Pattern match all cases of the scope functor.
+blankRawFold :: Blank g => BlankRawFold g a r -> g a -> BlankLeft g r
+blankRawFold = scopeWRawFold
+{-# INLINE blankRawFold #-}
+
+-- | Pattern match all cases of the scope functor, and eliminate the adjoints.
+blankFold :: Blank g => BlankFold g a r -> g a -> r
+blankFold = scopeWFold
+{-# INLINE blankFold #-}
+
+-- | Lift a value of your left adjoint functor (annotating the tree) into your
+-- scope functor.
+blankLiftAnno :: Blank g => BlankLeft g a -> g a
+blankLiftAnno = scopeWLiftAnno
+{-# INLINE blankLiftAnno #-}
+
+-- | Apply a natural transformation to your left adjoint functor (annotating the tree) to
+-- change scope functors.
+blankHoistAnno :: BlankPair g h => (forall x. BlankLeft g x -> BlankLeft h x) -> g a -> h a
+blankHoistAnno = scopeWHoistAnno
+{-# INLINE blankHoistAnno #-}
+
+-- | Apply a function to the free variables in scope in the context of the left adjoint functor.
+-- (Allows you to read annotations when fmapping.)
+blankMapAnno :: Blank g => (BlankLeft g a -> BlankLeft g b) -> g a -> g b
+blankMapAnno = scopeWMapAnno
+{-# INLINE blankMapAnno #-}
diff --git a/src/Blanks/LocScope.hs b/src/Blanks/LocScope.hs
--- a/src/Blanks/LocScope.hs
+++ b/src/Blanks/LocScope.hs
@@ -1,98 +1,85 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Blanks.LocScope
-  ( Colocated (..)
-  , Located (..)
-  , LocScope (..)
-  , LocScopeRawFold
-  , LocScopeFold
-  , askColocated
-  , colocated
-  , locScopeBind
-  , locScopeEmbed
-  , locScopeRawFold
-  , locScopeFold
-  , locScopeFree
-  , runColocated
+  ( LocScope (..)
+  , pattern LocScopeBound
+  , pattern LocScopeFree
+  , pattern LocScopeBinder
+  , pattern LocScopeEmbed
+  , locScopeLocation
+  , locScopeForget
   ) where
 
-import Blanks.Class
-import Blanks.RightAdjunct (RightAdjunct)
-import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFold, scopeTFree, scopeTRawFold)
-import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)
+import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankHoistAnno, blankMapAnno)
+import Blanks.Located (Colocated, Located (..), askColocated)
+import Blanks.NatNewtype (NatNewtype)
+import Blanks.Scope (Scope (..))
+import Blanks.ScopeW (ScopeW (..))
+import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,
+                          pattern UnderScopeFree)
 import Control.Monad (ap)
 import Control.Monad.Identity (Identity (..))
-import Control.Monad.Reader (MonadReader, Reader, ReaderT (..), ask, runReader)
-import Data.Distributive (Distributive (..))
-import Data.Functor.Adjunction (Adjunction (..))
-import Data.Functor.Rep (Representable)
+import Control.Monad.Writer (MonadWriter (..))
 
-data Located l a = Located
-  { _locatedLoc :: !l
-  , _locatedVal :: !a
-  } deriving (Eq, Show, Functor, Foldable, Traversable)
+-- | A 'Scope' annotated with some information between constructors.
+-- See 'Blank' for usage, and see the patterns in this module for easy manipulation
+-- and inspection.
+newtype LocScope l n f a = LocScope
+  { unLocScope :: ScopeW (Located l) n f (LocScope l n f) a
+  } deriving (Functor, Foldable, Traversable)
 
-newtype Colocated l a = Colocated
-  { unColocated :: Reader l a
-  } deriving (Functor, Applicative, Monad, MonadReader l, Representable)
+type instance BlankLeft (LocScope l n f) = Located l
+type instance BlankRight (LocScope l n f) = Colocated l
+type instance BlankInfo (LocScope l n f) = n
+type instance BlankFunctor (LocScope l n f) = f
 
-type instance RightAdjunct (Located l) = Colocated l
+instance Functor f => Blank (LocScope l n f)
+instance NatNewtype (ScopeW (Located l) n f (LocScope l n f)) (LocScope l n f)
 
-colocated :: (l -> a) -> Colocated l a
-colocated f = Colocated (ReaderT (Identity . f))
+pattern LocScopeBound :: l -> Int -> LocScope l n f a
+pattern LocScopeBound l b = LocScope (ScopeW (Located l (UnderScopeBound b)))
 
-askColocated :: Colocated l l
-askColocated = Colocated ask
+pattern LocScopeFree :: l -> a -> LocScope l n f a
+pattern LocScopeFree l a = LocScope (ScopeW (Located l (UnderScopeFree a)))
 
-runColocated :: Colocated l a -> l -> a
-runColocated = runReader . unColocated
+pattern LocScopeBinder :: l -> Int -> n -> LocScope l n f a -> LocScope l n f a
+pattern LocScopeBinder l i n e = LocScope (ScopeW (Located l (UnderScopeBinder i n e)))
 
-instance Distributive (Colocated l) where
-  distribute = Colocated . distribute . fmap unColocated
+pattern LocScopeEmbed :: l -> f (LocScope l n f a) -> LocScope l n f a
+pattern LocScopeEmbed l fe = LocScope (ScopeW (Located l (UnderScopeEmbed fe)))
 
-instance Adjunction (Located l) (Colocated l) where
-  leftAdjunct v a = colocated (v . flip Located a)
-  rightAdjunct h (Located l a) = runColocated (h a) l
+{-# COMPLETE LocScopeBound, LocScopeFree, LocScopeBinder, LocScopeEmbed #-}
 
-instance Monoid l => Applicative (Located l) where
-  pure = Located mempty
+-- | Extract the location (annotation) from this scope.
+locScopeLocation :: LocScope l n f a -> l
+locScopeLocation s =
+  case s of
+    LocScopeBound l _ -> l
+    LocScopeFree l _ -> l
+    LocScopeBinder l _ _ _ -> l
+    LocScopeEmbed l _ -> l
+
+instance (Monoid l, Functor f) => Applicative (LocScope l n f) where
+  pure = LocScopeFree mempty
   (<*>) = ap
 
-instance Monoid l => Monad (Located l) where
+instance (Monoid l, Functor f) => Monad (LocScope l n f) where
   return = pure
-  Located l a >>= f = let Located p b = f a in Located (l <> p) b
-
-newtype LocScope l n f a = LocScope
-  { unLocScope :: ScopeT (Located l) n f a
-  } deriving (Functor, Foldable, Traversable, BlankAbstract)
-
-type instance BlankInfo (LocScope l n f) = n
-type instance BlankFunctor (LocScope l n f) = f
-type instance BlankCodomain (LocScope l n f) = Colocated l
+  s >>= f = blankBind go s where
+    go a = fmap (\l1 -> let LocScope (ScopeW (Located l2 b)) = f a in LocScope (ScopeW (Located (l1 <> l2) b))) askColocated
 
-instance Functor f => BlankEmbed (LocScope l n f) where
-  blankEmbed = locScopeEmbed
+instance (Monoid l, Functor f) => MonadWriter l (LocScope l n f) where
+  writer (a, l) = LocScopeFree l a
+  tell l = LocScopeFree l ()
+  listen = blankMapAnno (\(Located l a) -> Located l (a, l))
+  pass = blankMapAnno (\(Located l (a, f)) -> Located (f l) a)
 
-instance (Eq (f (ScopeT (Located l) n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where
+instance (Eq (f (LocScope l n f a)), Eq l, Eq n, Eq a) => Eq (LocScope l n f a) where
   LocScope su == LocScope sv = su == sv
 
-instance (Show (f (ScopeT (Located l) n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where
-  showsPrec d (LocScope (ScopeT tu)) = showString "LocScope " . showsPrec (d+1) tu
-
-locScopeEmbed :: Functor f => f (LocScope l n f a) -> Colocated l (LocScope l n f a)
-locScopeEmbed fe = colocated (\l -> LocScope (ScopeT (Located l (UnderEmbedScope (EmbedScope (fmap unLocScope fe))))))
-
-locScopeBind :: Functor f => (a -> Colocated l (LocScope l n f b)) -> LocScope l n f a -> LocScope l n f b
-locScopeBind f = LocScope . scopeTBind (fmap unLocScope . f) . unLocScope
-
-locScopeFree :: a -> Colocated l (LocScope l n f a)
-locScopeFree = fmap LocScope . scopeTFree
-
-type LocScopeRawFold l n f a r = UnderScopeFold n f (LocScope l n f a) a r
-type LocScopeFold l n f a r = LocScopeRawFold l n f a (Colocated l r)
-
-locScopeRawFold :: Functor f => LocScopeRawFold l n f a r -> LocScope l n f a -> Located l r
-locScopeRawFold usf = scopeTRawFold (underScopeFoldContraMap LocScope usf) . unLocScope
+instance (Show (f (LocScope l n f a)), Show l, Show n, Show a) => Show (LocScope l n f a) where
+  showsPrec d (LocScope (ScopeW tu)) = showString "LocScope " . showsPrec (d+1) tu
 
-locScopeFold :: Functor f => LocScopeFold l n f a r -> LocScope l n f a -> r
-locScopeFold usf = scopeTFold (underScopeFoldContraMap LocScope usf) . unLocScope
+-- | Forget all the annotations and yield a plain 'Scope'.
+locScopeForget :: Functor f => LocScope l n f a -> Scope n f a
+locScopeForget = blankHoistAnno (\(Located _ a) -> Identity a)
diff --git a/src/Blanks/Located.hs b/src/Blanks/Located.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/Located.hs
@@ -0,0 +1,59 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Blanks.Located
+  ( Colocated (..)
+  , Located (..)
+  , askColocated
+  , colocated
+  , runColocated
+  ) where
+
+import Control.Monad (ap)
+import Control.Monad.Reader (MonadReader, Reader, ReaderT (..), ask, reader, runReader)
+import Control.Monad.Writer (MonadWriter (..))
+import Data.Distributive (Distributive (..))
+import Data.Functor.Adjunction (Adjunction (..))
+import Data.Functor.Rep (Representable)
+
+-- | This is basically the 'Env' comonad, but with the env strict.
+-- It's also basically the 'Writer' monad in certain contexts.
+-- We define a new, non-transforming datatype so we can pattern-match.
+data Located l a = Located
+  { _locatedLoc :: !l
+  , _locatedVal :: a
+  } deriving (Eq, Show, Functor, Foldable, Traversable)
+
+-- | Because we defined a unique left adjoint, we have to define the unique right.
+newtype Colocated l a = Colocated
+  { unColocated :: Reader l a
+  } deriving (Functor, Applicative, Monad, MonadReader l, Representable)
+
+colocated :: (l -> a) -> Colocated l a
+colocated f = Colocated (reader f)
+
+askColocated :: Colocated l l
+askColocated = Colocated ask
+
+runColocated :: Colocated l a -> l -> a
+runColocated = runReader . unColocated
+
+instance Distributive (Colocated l) where
+  distribute = Colocated . distribute . fmap unColocated
+
+instance Adjunction (Located l) (Colocated l) where
+  leftAdjunct v a = colocated (v . flip Located a)
+  rightAdjunct h (Located l a) = runColocated (h a) l
+
+instance Monoid l => Applicative (Located l) where
+  pure = Located mempty
+  (<*>) = ap
+
+instance Monoid l => Monad (Located l) where
+  return = pure
+  Located l a >>= f = let Located p b = f a in Located (l <> p) b
+
+instance Monoid l => MonadWriter l (Located l) where
+  writer (a, l) = Located l a
+  tell l = Located l ()
+  listen (Located l a) = Located l (a, l)
+  pass (Located l (a, f)) = Located (f l) a
diff --git a/src/Blanks/Name.hs b/src/Blanks/Name.hs
--- a/src/Blanks/Name.hs
+++ b/src/Blanks/Name.hs
@@ -1,16 +1,26 @@
 module Blanks.Name
   ( Name (..)
   , NameOnly
+  , pattern NameOnly
   ) where
 
+-- | 'Name' is compared on value only, allowing you to define and use
+-- things like 'NameOnly' in your 'BlankInfo' values to make alpha-equivalent
+-- terms structurally ('Eq') equivalent.
 data Name n a =
   Name
-    { nameKey :: n
-    , nameValue :: a
+    { _nameKey :: n
+    , _nameValue :: a
     }
   deriving (Show, Functor, Foldable, Traversable)
 
 instance Eq a => Eq (Name n a) where
   Name _ x == Name _ y = x == y
 
+-- An erased 'Name'.
 type NameOnly n = Name n ()
+
+pattern NameOnly :: n -> NameOnly n
+pattern NameOnly n = Name n ()
+
+{-# COMPLETE NameOnly #-}
diff --git a/src/Blanks/NatNewtype.hs b/src/Blanks/NatNewtype.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/NatNewtype.hs
@@ -0,0 +1,29 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+
+module Blanks.NatNewtype
+  ( NatNewtype
+  , natNewtypeFrom
+  , natNewtypeTo
+  ) where
+
+import Data.Coerce (Coercible, coerce)
+import Data.Kind (Type)
+
+-- | A "natural isomorphism" between two functors, like exists
+-- derivably between newtyped functors and their wrapped types.
+-- The functional dependency requires that 'g' be the newtype
+-- and 'm' the wrapped type.
+class
+  ( forall a. Coercible (m a) (g a)
+  , forall a. Coercible (g a) (m a)
+  )=> NatNewtype (m :: Type -> Type) (g :: Type -> Type) | g -> m
+
+-- | Coerce from the wrapped type to the newtype.
+natNewtypeTo :: NatNewtype m g => m a -> g a
+natNewtypeTo = coerce
+{-# INLINE natNewtypeTo #-}
+
+-- | Coerce from the newtype to the wrapped type.
+natNewtypeFrom :: NatNewtype m g => g a -> m a
+natNewtypeFrom = coerce
+{-# INLINE natNewtypeFrom #-}
diff --git a/src/Blanks/PureScope.hs b/src/Blanks/PureScope.hs
deleted file mode 100644
--- a/src/Blanks/PureScope.hs
+++ /dev/null
@@ -1,55 +0,0 @@
-{-# LANGUAGE UndecidableInstances #-}
-
-module Blanks.PureScope
-  ( PureScope (..)
-  , PureScopeFold
-  , pureScopeBind
-  , pureScopeEmbed
-  , pureScopeFold
-  , pureScopeFree
-  ) where
-
-import Blanks.Class
-import Blanks.ScopeT (ScopeT (..), scopeTBind, scopeTFree, scopeTRawFold)
-import Blanks.UnderScope (EmbedScope (..), UnderScope (..), UnderScopeFold (..), underScopeFoldContraMap)
-import Control.Monad (ap)
-import Control.Monad.Identity (Identity (..))
-
-newtype PureScope n f a = PureScope
-  { unPureScope :: ScopeT Identity n f a
-  } deriving (Functor, Foldable, Traversable, BlankAbstract)
-
-type instance BlankInfo (PureScope n f) = n
-type instance BlankFunctor (PureScope n f) = f
-type instance BlankCodomain (PureScope n f) = Identity
-
-instance Functor f => Applicative (PureScope n f) where
-  pure = pureScopeFree
-  (<*>) = ap
-
-instance Functor f => Monad (PureScope n f) where
-  return = pureScopeFree
-  s >>= f = pureScopeBind f s
-
-instance Functor f => BlankEmbed (PureScope n f) where
-  blankEmbed = Identity . pureScopeEmbed
-
-instance (Eq (f (ScopeT Identity n f a)), Eq n, Eq a) => Eq (PureScope n f a) where
-  PureScope su == PureScope sv = su == sv
-
-instance (Show (f (ScopeT Identity n f a)), Show n, Show a) => Show (PureScope n f a) where
-  showsPrec d (PureScope (ScopeT tu)) = showString "PureScope " . showsPrec (d+1) tu
-
-pureScopeFree :: a -> PureScope n f a
-pureScopeFree = PureScope . runIdentity . scopeTFree
-
-pureScopeBind :: Functor f => (a -> PureScope n f b) -> PureScope n f a -> PureScope n f b
-pureScopeBind f = PureScope . scopeTBind (Identity . unPureScope . f) . unPureScope
-
-pureScopeEmbed :: Functor f => f (PureScope n f a) -> PureScope n f a
-pureScopeEmbed fe = PureScope (ScopeT (Identity (UnderEmbedScope (EmbedScope (fmap unPureScope fe)))))
-
-type PureScopeFold n f a r = UnderScopeFold n f (PureScope n f a) a r
-
-pureScopeFold :: Traversable f => PureScopeFold n f a r -> PureScope n f a -> r
-pureScopeFold usf = runIdentity . scopeTRawFold (underScopeFoldContraMap PureScope usf) . unPureScope
diff --git a/src/Blanks/RightAdjunct.hs b/src/Blanks/RightAdjunct.hs
deleted file mode 100644
--- a/src/Blanks/RightAdjunct.hs
+++ /dev/null
@@ -1,20 +0,0 @@
-{-# LANGUAGE ConstraintKinds #-}
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module Blanks.RightAdjunct
-  ( RightAdjunct
-  , RightAdjunction
-  , RightAdjunctionApplicative
-  ) where
-
-import Control.Monad.Identity (Identity)
-import Data.Functor.Adjunction (Adjunction (..))
-
-type family RightAdjunct (t :: * -> *) :: * -> *
-
-type instance RightAdjunct Identity = Identity
-
-type RightAdjunction (t :: * -> *) = Adjunction t (RightAdjunct t)
-
-type RightAdjunctionApplicative t = (RightAdjunction t, Applicative (RightAdjunct t))
diff --git a/src/Blanks/Scope.hs b/src/Blanks/Scope.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/Scope.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+module Blanks.Scope
+  ( Scope (..)
+  , pattern ScopeBound
+  , pattern ScopeFree
+  , pattern ScopeBinder
+  , pattern ScopeEmbed
+  ) where
+
+import Blanks.Interface (Blank, BlankFunctor, BlankInfo, BlankLeft, BlankRight, blankBind, blankFree)
+import Blanks.NatNewtype (NatNewtype)
+import Blanks.ScopeW (ScopeW (..))
+import Blanks.UnderScope (pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,
+                          pattern UnderScopeFree)
+import Control.Monad (ap)
+import Control.Monad.Identity (Identity (..))
+
+-- | A simple wrapper for your expression functor that knows how to name-bind.
+-- See 'Blank' for usage, and see the patterns in this module for easy manipulation
+-- and inspection.
+newtype Scope n f a = Scope
+  { unScope :: ScopeW Identity n f (Scope n f) a
+  } deriving (Functor, Foldable, Traversable)
+
+type instance BlankLeft (Scope n f) = Identity
+type instance BlankRight (Scope n f) = Identity
+type instance BlankInfo (Scope n f) = n
+type instance BlankFunctor (Scope n f) = f
+
+instance Functor f => Blank (Scope n f)
+instance NatNewtype (ScopeW Identity n f (Scope n f)) (Scope n f)
+
+pattern ScopeBound :: Int -> Scope n f a
+pattern ScopeBound b = Scope (ScopeW (Identity (UnderScopeBound b)))
+
+pattern ScopeFree :: a -> Scope n f a
+pattern ScopeFree a = Scope (ScopeW (Identity (UnderScopeFree a)))
+
+pattern ScopeBinder :: Int -> n -> Scope n f a -> Scope n f a
+pattern ScopeBinder i n e = Scope (ScopeW (Identity (UnderScopeBinder i n e)))
+
+pattern ScopeEmbed :: f (Scope n f a) -> Scope n f a
+pattern ScopeEmbed fe = Scope (ScopeW (Identity (UnderScopeEmbed fe)))
+
+{-# COMPLETE ScopeBound, ScopeFree, ScopeBinder, ScopeEmbed #-}
+
+instance Functor f => Applicative (Scope n f) where
+  pure = runIdentity . blankFree
+  (<*>) = ap
+
+instance Functor f => Monad (Scope n f) where
+  return = pure
+  s >>= f = blankBind (Identity . f) s
+
+instance (Eq (f (Scope n f a)), Eq n, Eq a) => Eq (Scope n f a) where
+  Scope su == Scope sv = su == sv
+
+instance (Show (f (Scope n f a)), Show n, Show a) => Show (Scope n f a) where
+  showsPrec d (Scope (ScopeW tu)) = showString "Scope " . showsPrec (d+1) tu
diff --git a/src/Blanks/ScopeT.hs b/src/Blanks/ScopeT.hs
deleted file mode 100644
--- a/src/Blanks/ScopeT.hs
+++ /dev/null
@@ -1,171 +0,0 @@
-{-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE FlexibleInstances #-}
-{-# LANGUAGE UndecidableInstances #-}
-
-module Blanks.ScopeT
-  ( ScopeT (..)
-  , ScopeTFold
-  , ScopeTRawFold
-  , scopeTBind
-  , scopeTEmbed
-  , scopeTFold
-  , scopeTFree
-  , scopeTHoistAnno
-  , scopeTLiftAnno
-  , scopeTRawFold
-  ) where
-
-import Blanks.Class
-import Blanks.RightAdjunct
-import Blanks.Sub (SubError (..))
-import Blanks.UnderScope (BinderScope (..), BoundScope (..), EmbedScope (..), FreeScope (..), UnderScope (..),
-                          UnderScopeFold (..), underScopeFold, underScopePure, underScopeShift)
-import Data.Bifoldable (bifoldr)
-import Data.Bifunctor (bimap, first)
-import Data.Bitraversable (bitraverse)
-import Data.Functor.Adjunction (Adjunction (..))
-import Data.Maybe (fromMaybe)
-import Data.Sequence (Seq)
-import qualified Data.Sequence as Seq
-
-newtype ScopeT t n f a = ScopeT
-  { unScopeT :: t (UnderScope n f (ScopeT t n f a) a)
-  }
-
-instance Eq (t (UnderScope n f (ScopeT t n f a) a)) => Eq (ScopeT t n f a) where
-  ScopeT tu == ScopeT tv = tu == tv
-
-instance Show (t (UnderScope n f (ScopeT t n f a) a)) => Show (ScopeT t n f a) where
-  showsPrec d (ScopeT tu) = showString "ScopeT " . showsPrec (d+1) tu
-
-instance (Functor t, Functor f) => Functor (ScopeT t n f) where
-  fmap f (ScopeT tu) = ScopeT (fmap (bimap (fmap f) f) tu)
-
-instance (Foldable t, Foldable f) => Foldable (ScopeT t n f) where
-  foldr f z (ScopeT tu) = foldr (flip (bifoldr (flip (foldr f)) f)) z tu
-
-instance (Traversable t, Traversable f) => Traversable (ScopeT t n f) where
-  traverse f (ScopeT tu) = fmap ScopeT (traverse (bitraverse (traverse f) f) tu)
-
-type instance BlankFunctor (ScopeT t n f) = f
-type instance BlankInfo (ScopeT t n f) = n
-type instance BlankCodomain (ScopeT t n f) = RightAdjunct t
-
-instance RightAdjunction t => BlankEmbed (ScopeT t n f) where
-  blankEmbed = scopeTEmbed
-
-instance (RightAdjunctionApplicative t, Functor f) => BlankAbstract (ScopeT t n f) where
-  blankFree = scopeTFree
-  blankAbstract = scopeTAbstract
-  blankUnAbstract = scopeTUnAbstract
-  blankInstantiate = scopeTInstantiate
-  blankApply = scopeTApply
-
-scopeTWrap :: RightAdjunction t => UnderScope n f (ScopeT t n f a) a -> RightAdjunct t (ScopeT t n f a)
-scopeTWrap = fmap ScopeT . unit
-
-scopeTBound :: RightAdjunction t => Int -> RightAdjunct t (ScopeT t n f a)
-scopeTBound = scopeTWrap . UnderBoundScope . BoundScope
-
-scopeTFree :: RightAdjunction t => a -> RightAdjunct t (ScopeT t n f a)
-scopeTFree = scopeTWrap . UnderFreeScope . FreeScope
-
-scopeTBinder :: RightAdjunction t => Int -> n -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)
-scopeTBinder r n e = scopeTWrap (UnderBinderScope (BinderScope r n e))
-
-scopeTEmbed :: RightAdjunction t => f (ScopeT t n f a) -> RightAdjunct t (ScopeT t n f a)
-scopeTEmbed fe = fmap ScopeT (unit (UnderEmbedScope (EmbedScope fe)))
-
-scopeTShiftN :: (Functor t, Functor f) => Int -> Int -> ScopeT t n f a -> ScopeT t n f a
-scopeTShiftN c d (ScopeT tu) = ScopeT (fmap (underScopeShift scopeTShiftN c d) tu)
-
-scopeTShift :: (Functor t, Functor f) => Int -> ScopeT t n f a -> ScopeT t n f a
-scopeTShift = scopeTShiftN 0
-
-scopeTBindOptN :: (RightAdjunctionApplicative t, Functor f) => (a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> Int -> ScopeT t n f a -> ScopeT t n f a
-scopeTBindOptN f = scopeTModOpt . go where
-  go i us =
-    case us of
-      UnderBoundScope _ -> Nothing
-      UnderFreeScope (FreeScope a) -> fmap (fmap (scopeTShift i)) (f a)
-      UnderBinderScope (BinderScope r x e) -> Just (scopeTBinder r x (scopeTBindOptN f (i + r) e))
-      UnderEmbedScope (EmbedScope fe) -> Just (scopeTEmbed (fmap (scopeTBindOptN f i) fe))
-
-scopeTBindOpt :: (RightAdjunctionApplicative t, Functor f) => (a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> ScopeT t n f a -> ScopeT t n f a
-scopeTBindOpt f = scopeTBindOptN f 0
-
-scopeTBindN :: (RightAdjunction t, Functor f) => (a -> RightAdjunct t (ScopeT t n f b)) -> Int -> ScopeT t n f a -> ScopeT t n f b
-scopeTBindN f = scopeTMod . go where
-  go i us =
-    case us of
-      UnderBoundScope (BoundScope b) -> scopeTBound b
-      UnderFreeScope (FreeScope a) -> fmap (scopeTShift i) (f a)
-      UnderBinderScope (BinderScope r x e) -> scopeTBinder r x (scopeTBindN f (i + r) e)
-      UnderEmbedScope (EmbedScope fe) -> scopeTEmbed (fmap (scopeTBindN f i) fe)
-
-scopeTBind :: (RightAdjunction t, Functor f) => (a -> RightAdjunct t (ScopeT t n f b)) -> ScopeT t n f a -> ScopeT t n f b
-scopeTBind f = scopeTBindN f 0
-
-subScopeTAbstract :: (RightAdjunctionApplicative t, Functor f, Eq a) => Int -> n -> Seq a -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)
-subScopeTAbstract r n ks e =
-  let f = fmap scopeTBound . flip Seq.elemIndexL ks
-      e' = scopeTBindOpt f e
-  in scopeTBinder r n e'
-
-scopeTAbstract :: (RightAdjunctionApplicative t, Functor f, Eq a) => n -> Seq a -> ScopeT t n f a -> RightAdjunct t (ScopeT t n f a)
-scopeTAbstract n ks =
-  let r = Seq.length ks
-  in subScopeTAbstract r n ks . scopeTShift r
-
-scopeTUnAbstract :: (RightAdjunctionApplicative t, Functor f) => Seq a -> ScopeT t n f a -> ScopeT t n f a
-scopeTUnAbstract ks = scopeTInstantiate (fmap scopeTFree ks)
-
-scopeTModOpt :: RightAdjunctionApplicative t => (UnderScope n f (ScopeT t n f a) a -> Maybe (RightAdjunct t (ScopeT t n f a))) -> ScopeT t n f a -> ScopeT t n f a
-scopeTModOpt f s = rightAdjunct (fromMaybe (pure s) . f) (unScopeT s)
-
-scopeTModM :: (RightAdjunctionApplicative t, Traversable m) => (UnderScope n f (ScopeT t n f a) a -> m (RightAdjunct t x)) -> ScopeT t n f a -> m x
-scopeTModM f = rightAdjunct (sequenceA . f) . unScopeT
-
-scopeTMod :: RightAdjunction t => (UnderScope n f (ScopeT t n f a) a -> RightAdjunct t x) -> ScopeT t n f a -> x
-scopeTMod f = rightAdjunct f . unScopeT
-
-scopeTInstantiateN :: (RightAdjunctionApplicative t, Functor f) => Int -> Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> ScopeT t n f a
-scopeTInstantiateN h vs = scopeTModOpt (go h vs) where
-  go i ws us =
-    case us of
-      UnderBoundScope (BoundScope b) -> vs Seq.!? (b - i)
-      UnderFreeScope _ -> Nothing
-      UnderBinderScope (BinderScope r n e) ->
-        let ws' = fmap (fmap (scopeTShift r)) ws
-            e' = scopeTInstantiateN (r + i) ws' e
-        in Just (scopeTBinder r n e')
-      UnderEmbedScope (EmbedScope fe) -> Just (scopeTEmbed (fmap (scopeTInstantiateN i ws) fe))
-
-scopeTInstantiate :: (RightAdjunctionApplicative t,  Functor f) => Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> ScopeT t n f a
-scopeTInstantiate = scopeTInstantiateN 0
-
-scopeTApply :: (RightAdjunctionApplicative t, Functor f) => Seq (RightAdjunct t (ScopeT t n f a)) -> ScopeT t n f a -> Either SubError (ScopeT t n f a)
-scopeTApply vs = scopeTModM go where
-  go us =
-    case us of
-      UnderBinderScope (BinderScope r _ e) ->
-        let len = Seq.length vs
-        in if len == r
-              then Right (pure (scopeTShift (-1) (scopeTInstantiate vs e)))
-              else Left (ApplyError len r)
-      _ -> Left NonBinderError
-
-type ScopeTRawFold t n f a r = UnderScopeFold n f (ScopeT t n f a) a r
-type ScopeTFold t n f a r = ScopeTRawFold t n f a (RightAdjunct t r)
-
-scopeTRawFold :: Functor t => ScopeTRawFold t n f a r -> ScopeT t n f a -> t r
-scopeTRawFold usf = fmap (underScopeFold usf) . unScopeT
-
-scopeTFold :: RightAdjunction t => ScopeTFold t n f a r -> ScopeT t n f a -> r
-scopeTFold usf = counit . scopeTRawFold usf
-
-scopeTLiftAnno :: Functor t => t a -> ScopeT t n f a
-scopeTLiftAnno ta = ScopeT (fmap underScopePure ta)
-
-scopeTHoistAnno :: (Functor t, Functor f) => (forall x. t x -> w x) -> ScopeT t n f a -> ScopeT w n f a
-scopeTHoistAnno nat (ScopeT tu) = ScopeT (nat (fmap (first (scopeTHoistAnno nat)) tu))
diff --git a/src/Blanks/ScopeW.hs b/src/Blanks/ScopeW.hs
new file mode 100644
--- /dev/null
+++ b/src/Blanks/ScopeW.hs
@@ -0,0 +1,188 @@
+{-# LANGUAGE UndecidableInstances #-}
+
+-- | Internals. You'd need to newtype 'ScopeW' to implement your own 'Blank'.
+module Blanks.ScopeW
+  ( ScopeC
+  , ScopeW (..)
+  , ScopeWRawFold
+  , ScopeWFold
+  , scopeWFree
+  , scopeWEmbed
+  , scopeWAbstract
+  , scopeWUnAbstract
+  , scopeWInstantiate
+  , scopeWApply
+  , scopeWBind
+  , scopeWBindOpt
+  , scopeWLift
+  , scopeWRawFold
+  , scopeWFold
+  , scopeWLiftAnno
+  , scopeWHoistAnno
+  , scopeWMapAnno
+  ) where
+
+import Blanks.NatNewtype (NatNewtype, natNewtypeFrom, natNewtypeTo)
+import Blanks.Sub (SubError (..))
+import Blanks.UnderScope (UnderScope, pattern UnderScopeBinder, pattern UnderScopeBound, pattern UnderScopeEmbed,
+                          UnderScopeFold, pattern UnderScopeFree, underScopeFold, underScopeShift)
+import Data.Bifoldable (bifoldr)
+import Data.Bifunctor (bimap, first)
+import Data.Bitraversable (bitraverse)
+import Data.Functor.Adjunction (Adjunction (..))
+import Data.Maybe (fromMaybe)
+import Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
+
+-- * ScopeW, patterns, and instances
+
+newtype ScopeW t n f g a = ScopeW
+  { unScopeW :: t (UnderScope n f (g a) a)
+  }
+
+instance Eq (t (UnderScope n f (g a) a)) => Eq (ScopeW t n f g a) where
+  ScopeW tu == ScopeW tv = tu == tv
+
+instance Show (t (UnderScope n f (g a) a)) => Show (ScopeW t n f g a) where
+  showsPrec d (ScopeW tu) = showString "ScopeW " . showsPrec (d+1) tu
+
+instance (Functor t, Functor f, Functor g) => Functor (ScopeW t n f g) where
+  fmap f (ScopeW tu) = ScopeW (fmap (bimap (fmap f) f) tu)
+
+instance (Foldable t, Foldable f, Foldable g) => Foldable (ScopeW t n f g) where
+  foldr f z (ScopeW tu) = foldr (flip (bifoldr (flip (foldr f)) f)) z tu
+
+instance (Traversable t, Traversable f, Traversable g) => Traversable (ScopeW t n f g) where
+  traverse f (ScopeW tu) = fmap ScopeW (traverse (bitraverse (traverse f) f) tu)
+
+type ScopeC t u n f g = (Adjunction t u, Applicative u, Functor f, NatNewtype (ScopeW t n f g) g)
+
+-- * Smart constructors, shift, and bind
+
+scopeWMod :: ScopeC t u n f g => (UnderScope n f (g a) a -> u x) -> g a -> x
+scopeWMod f = rightAdjunct f . unScopeW . natNewtypeFrom
+
+scopeWModOpt :: ScopeC t u n f g => (UnderScope n f (g a) a -> Maybe (u (g a))) -> g a -> g a
+scopeWModOpt f s = rightAdjunct (fromMaybe (pure s) . f) (unScopeW (natNewtypeFrom s))
+
+scopeWModM :: (ScopeC t u n f g, Traversable m) => (UnderScope n f (g a) a -> m (u x)) -> g a -> m x
+scopeWModM f = rightAdjunct (sequenceA . f) . unScopeW . natNewtypeFrom
+
+scopeWBound :: ScopeC t u n f g => Int -> u (g a)
+scopeWBound b = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBound b))
+
+scopeWFree :: ScopeC t u n f g => a -> u (g a)
+scopeWFree a = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeFree a))
+
+scopeWShift :: ScopeC t u n f g => Int -> g a -> g a
+scopeWShift = scopeWShiftN 0
+
+scopeWShiftN :: ScopeC t u n f g => Int -> Int -> g a -> g a
+scopeWShiftN c d e =
+  let ScopeW tu = natNewtypeFrom e
+  in natNewtypeTo (ScopeW (fmap (underScopeShift scopeWShiftN c d) tu))
+
+scopeWBinder :: ScopeC t u n f g => Int -> n -> g a -> u (g a)
+scopeWBinder r n e = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeBinder r n e))
+
+scopeWEmbed :: ScopeC t u n f g => f (g a) -> u (g a)
+scopeWEmbed fe = fmap (natNewtypeTo . ScopeW) (unit (UnderScopeEmbed fe))
+
+scopeWBind :: ScopeC t u n f g => (a -> u (g b)) -> g a -> g b
+scopeWBind f = scopeWBindN f 0
+
+scopeWBindN :: ScopeC t u n f g => (a -> u (g b)) -> Int -> g a -> g b
+scopeWBindN f = scopeWMod . go where
+  go i us =
+    case us of
+      UnderScopeBound b -> scopeWBound b
+      UnderScopeFree a -> fmap (scopeWShift i) (f a)
+      UnderScopeBinder r x e -> scopeWBinder r x (scopeWBindN f (i + r) e)
+      UnderScopeEmbed fe -> scopeWEmbed (fmap (scopeWBindN f i) fe)
+
+scopeWBindOpt :: ScopeC t u n f g => (a -> Maybe (u (g a))) -> g a -> g a
+scopeWBindOpt f = scopeWBindOptN f 0
+
+scopeWBindOptN :: ScopeC t u n f g => (a -> Maybe (u (g a))) -> Int -> g a -> g a
+scopeWBindOptN f = scopeWModOpt . go where
+  go i us =
+    case us of
+      UnderScopeBound _ -> Nothing
+      UnderScopeFree a -> fmap (fmap (scopeWShift i)) (f a)
+      UnderScopeBinder r x e -> Just (scopeWBinder r x (scopeWBindOptN f (i + r) e))
+      UnderScopeEmbed fe -> Just (scopeWEmbed (fmap (scopeWBindOptN f i) fe))
+
+scopeWLift :: (ScopeC t u n f g, Monad u, Traversable f) => f a -> u (g a)
+scopeWLift fa = traverse scopeWFree fa >>= scopeWEmbed
+
+-- * Abstraction
+
+subScopeWAbstract :: (ScopeC t u n f g, Eq a) => Int -> n -> Seq a -> g a -> u (g a)
+subScopeWAbstract r n ks e =
+  let f = fmap scopeWBound . flip Seq.elemIndexL ks
+      e' = scopeWBindOpt f e
+  in scopeWBinder r n e'
+
+scopeWAbstract :: (ScopeC t u n f g, Eq a) => n -> Seq a -> g a -> u (g a)
+scopeWAbstract n ks =
+  let r = Seq.length ks
+  in subScopeWAbstract r n ks . scopeWShift r
+
+scopeWUnAbstract :: ScopeC t u n f g => Seq a -> g a -> g a
+scopeWUnAbstract ks = scopeWInstantiate (fmap scopeWFree ks)
+
+scopeWInstantiate :: ScopeC t u n f g => Seq (u (g a)) -> g a -> g a
+scopeWInstantiate = scopeWInstantiateN 0
+
+scopeWInstantiateN :: ScopeC t u n f g => Int -> Seq (u (g a)) -> g a -> g a
+scopeWInstantiateN h vs = scopeWModOpt (go h) where
+  go i us =
+    case us of
+      UnderScopeBound b -> vs Seq.!? (b - i)
+      UnderScopeFree _ -> Nothing
+      UnderScopeBinder r n e ->
+        let vs' = fmap (fmap (scopeWShift r)) vs
+            e' = scopeWInstantiateN (r + i) vs' e
+        in Just (scopeWBinder r n e')
+      UnderScopeEmbed fe -> Just (scopeWEmbed (fmap (scopeWInstantiateN i vs) fe))
+
+scopeWApply :: ScopeC t u n f g => Seq (u (g a)) -> g a -> Either SubError (g a)
+scopeWApply vs = scopeWModM go where
+  go us =
+    case us of
+      UnderScopeBinder r _ e ->
+        let len = Seq.length vs
+        in if len == r
+              then Right (pure (scopeWShift (-1) (scopeWInstantiate vs e)))
+              else Left (ApplyError len r)
+      _ -> Left NonBinderError
+
+-- * Folds
+
+type ScopeWRawFold n f g a r = UnderScopeFold n f (g a) a r
+type ScopeWFold u n f g a r = ScopeWRawFold n f g a (u r)
+
+scopeWRawFold :: (NatNewtype (ScopeW t n f g) g, Functor t) => ScopeWRawFold n f g a r -> g a -> t r
+scopeWRawFold usf = fmap (underScopeFold usf) . unScopeW . natNewtypeFrom
+
+scopeWFold :: (NatNewtype (ScopeW t n f g) g, Adjunction t u) => ScopeWFold u n f g a r -> g a -> r
+scopeWFold usf = counit . scopeWRawFold usf
+
+-- * Annotation functions
+
+scopeWLiftAnno :: (NatNewtype (ScopeW t n f g) g, Functor t) => t a -> g a
+scopeWLiftAnno = natNewtypeTo . ScopeW . fmap UnderScopeFree
+
+scopeWHoistAnno :: (NatNewtype (ScopeW t n f g) g, NatNewtype (ScopeW w n f h) h, Functor t, Functor w, Functor f) => (forall x. t x -> w x) -> g a -> h a
+scopeWHoistAnno nat ga =
+  let ScopeW tu = natNewtypeFrom ga
+      s = ScopeW (nat (fmap (first (scopeWHoistAnno nat)) tu))
+  in natNewtypeTo s
+
+scopeWMapAnno :: ScopeC t u n f g => (t a -> t b) -> g a -> g b
+scopeWMapAnno f = scopeWMod go where
+  go us = case us of
+    UnderScopeBound b -> scopeWBound b
+    UnderScopeFree a -> fmap (natNewtypeTo . ScopeW . fmap UnderScopeFree . f) (unit a)
+    UnderScopeBinder r x e -> scopeWBinder r x (scopeWMapAnno f e)
+    UnderScopeEmbed fe -> scopeWEmbed (fmap (scopeWMapAnno f) fe)
diff --git a/src/Blanks/Sub.hs b/src/Blanks/Sub.hs
--- a/src/Blanks/Sub.hs
+++ b/src/Blanks/Sub.hs
@@ -1,37 +1,32 @@
 module Blanks.Sub
-  ( Sub (..)
-  , SubError (..)
+  ( SubError (..)
   , ThrowSub (..)
   , rethrowSub
-  , runSub
   ) where
 
-import Control.Exception (Exception)
-import Control.Monad.Except (Except, MonadError (..), runExcept)
-import Data.Typeable (Typeable)
+import Control.Exception (Exception, throwIO)
 
+-- | Errors that happen in the course of instantiation, thrown by 'blankApply'
+-- and related functions.
 data SubError
   = ApplyError !Int !Int
   | UnboundError !Int
   | NonBinderError
-  deriving (Eq, Show, Typeable)
+  deriving (Eq, Show)
 
 instance Exception SubError
 
+-- | Some monadic context that lets you throw a 'SubError'.
+-- Exists to let you rethrow to a more convenient context rather than
+-- pattern maching.
 class ThrowSub m where
   throwSub :: SubError -> m a
 
 rethrowSub :: (Applicative m, ThrowSub m) => Either SubError a -> m a
 rethrowSub = either throwSub pure
 
-newtype Sub a =
-  Sub
-    { unSub :: Except SubError a
-    }
-  deriving (Functor, Applicative, Monad, Foldable, Traversable)
-
-instance ThrowSub Sub where
-  throwSub = Sub . throwError
+instance ThrowSub (Either SubError) where
+  throwSub = Left
 
-runSub :: Sub a -> Either SubError a
-runSub = runExcept . unSub
+instance ThrowSub IO where
+  throwSub = throwIO
diff --git a/src/Blanks/UnderScope.hs b/src/Blanks/UnderScope.hs
--- a/src/Blanks/UnderScope.hs
+++ b/src/Blanks/UnderScope.hs
@@ -1,3 +1,4 @@
+-- | Internals. You will probably never need these.
 module Blanks.UnderScope
   ( BinderScope (..)
   , BoundScope (..)
@@ -5,9 +6,11 @@
   , FreeScope (..)
   , UnderScope (..)
   , UnderScopeFold (..)
+  , pattern UnderScopeBound
+  , pattern UnderScopeFree
+  , pattern UnderScopeBinder
+  , pattern UnderScopeEmbed
   , underScopeFold
-  , underScopeFoldContraMap
-  , underScopePure
   , underScopeShift
   ) where
 
@@ -31,7 +34,7 @@
   BinderScope
     { binderScopeArity :: !Int
     , binderScopeInfo :: !n
-    , binderScopeBody :: !e
+    , binderScopeBody :: e
     }
   deriving (Eq, Show, Functor, Foldable, Traversable)
 
@@ -48,6 +51,20 @@
   | UnderEmbedScope !(EmbedScope f e)
   deriving (Eq, Show, Functor)
 
+pattern UnderScopeBound :: Int -> UnderScope n f e a
+pattern UnderScopeBound i = UnderBoundScope (BoundScope i)
+
+pattern UnderScopeFree :: a -> UnderScope n f e a
+pattern UnderScopeFree a = UnderFreeScope (FreeScope a)
+
+pattern UnderScopeBinder :: Int -> n -> e -> UnderScope n f e a
+pattern UnderScopeBinder i n e = UnderBinderScope (BinderScope i n e)
+
+pattern UnderScopeEmbed :: f e -> UnderScope n f e a
+pattern UnderScopeEmbed fe = UnderEmbedScope (EmbedScope fe)
+
+{-# COMPLETE UnderScopeBound, UnderScopeFree, UnderScopeBinder, UnderScopeEmbed #-}
+
 instance Functor f => Bifunctor (UnderScope n f) where
   bimap _ _ (UnderBoundScope (BoundScope b)) = UnderBoundScope (BoundScope b)
   bimap _ g (UnderFreeScope (FreeScope a)) = UnderFreeScope (FreeScope (g a))
@@ -66,9 +83,6 @@
   bitraverse f _ (UnderBinderScope (BinderScope i x e)) = fmap (UnderBinderScope . BinderScope i x) (f e)
   bitraverse f _ (UnderEmbedScope (EmbedScope fe)) = fmap (UnderEmbedScope . EmbedScope) (traverse f fe)
 
-underScopePure :: a -> UnderScope n f e a
-underScopePure = UnderFreeScope . FreeScope
-
 underScopeShift :: Functor f => (Int -> Int -> e -> e) -> Int -> Int -> UnderScope n f e a -> UnderScope n f e a
 underScopeShift recShift c d us =
   case us of
@@ -96,9 +110,3 @@
     UnderFreeScope x -> free x
     UnderBinderScope x -> binder x
     UnderEmbedScope x -> embed x
-
-underScopeFoldContraMap :: Functor f => (x -> e) -> UnderScopeFold n f e a r -> UnderScopeFold n f x a r
-underScopeFoldContraMap f (UnderScopeFold bound free binder embed) = UnderScopeFold bound free binder' embed' where
-  binder' (BinderScope r n x) = binder (BinderScope r n (f x))
-  embed' (EmbedScope fx) = embed (EmbedScope (fmap f fx))
-
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,10 @@
+module Main
+  ( main
+  ) where
+
+import Test.Blanks.LocScopeTest (testLocScope)
+import Test.Blanks.ScopeTest (testScope)
+import Test.Tasty (defaultMain, testGroup)
+
+main :: IO ()
+main = defaultMain (testGroup "Blanks" [testScope, testLocScope])
diff --git a/test/Tasty.hs b/test/Tasty.hs
deleted file mode 100644
--- a/test/Tasty.hs
+++ /dev/null
@@ -1,1 +0,0 @@
-{-# OPTIONS_GHC -F -pgmF tasty-discover #-}
diff --git a/test/Test/Blanks/BlanksTest.hs b/test/Test/Blanks/BlanksTest.hs
deleted file mode 100644
--- a/test/Test/Blanks/BlanksTest.hs
+++ /dev/null
@@ -1,87 +0,0 @@
-module Test.Blanks.BlanksTest where
-
-import Blanks
-import Control.Monad.Identity (Identity (..))
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Test.Blanks.Assertions ((@/=))
-import Test.Tasty
-import Test.Tasty.HUnit
-
-type BareScope = PureScope (NameOnly Char) Identity Char
-
-abst :: Char -> BareScope -> BareScope
-abst a = runIdentity . blankAbstract1 (Name a ()) a
-
-bound :: Int -> BareScope
-bound = PureScope . ScopeT . pure . UnderBoundScope . BoundScope
-
-var :: Char -> BareScope
-var = pure
-
-freeVars :: BareScope -> Set Char
-freeVars = foldMap Set.singleton
-
-test_sub :: TestTree
-test_sub =
-  let svar = var 'x'
-      sbound = bound 0
-      sfree = abst 'y' (var 'x')
-      sfree2 = abst 'z' (abst 'y' (var 'x'))
-      sid = abst 'x' (var 'x')
-      swonky = abst 'x' (bound 0)
-      sconst = abst 'x' (abst 'y' (var 'x'))
-      sflip = abst 'x' (abst 'y' (var 'y'))
-      svar2 = var 'e'
-      swonky2 = abst 'x' svar2
-
-      testEq =
-        testCase "eq" $ do
-          svar @?= svar
-          svar @/= svar2
-          sid @?= abst 'x' (var 'x')
-          sid @?= abst 'y' (var 'y')
-          sid @/= abst 'x' (var 'y')
-          sid @/= abst 'y' (var 'x')
-          sid @/= svar
-
-      testFreeVars =
-        testCase "free vars" $ do
-          freeVars svar @?= Set.singleton 'x'
-          freeVars sbound @?= Set.empty
-          freeVars sfree @?= Set.singleton 'x'
-          freeVars sfree2 @?= Set.singleton 'x'
-          freeVars sid @?= Set.empty
-          freeVars swonky @?= Set.empty
-          freeVars sconst @?= Set.empty
-          freeVars sflip @?= Set.empty
-          freeVars svar2 @=? Set.singleton 'e'
-          freeVars swonky2 @?= Set.singleton 'e'
-
-      testInstantiate =
-        testCase "instantiate" $ do
-          blankInstantiate1 (pure svar2) svar @?= svar
-          blankInstantiate1 (pure svar2) sbound @?= svar2
-          blankInstantiate1 (pure svar2) sid @?= sid
-          blankInstantiate1 (pure svar2) swonky @?= swonky2
-
-      testApply =
-        testCase "apply" $ do
-          blankApply1 (pure svar2) sid @?= Right svar2
-          blankApply1 (pure svar2) swonky @?= Right sbound
-          blankApply1 (pure svar2) sconst @?= Right swonky2
-          blankApply1 (pure svar2) sflip @?= Right sid
-
-      testVarSub =
-        testCase "var sub" $ do
-          (svar >>= const svar2) @?= svar2
-          (sfree >>= const svar2) @?= abst 'y' svar2
-          (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2)
-
-      testIdSub =
-        testCase "id sub" $ do
-          (svar >>= const sid) @?= sid
-          (sfree >>= const sid) @?= abst 'y' sid
-          (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid)
-
-   in testGroup "sub" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub]
diff --git a/test/Test/Blanks/LocScopeTest.hs b/test/Test/Blanks/LocScopeTest.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Blanks/LocScopeTest.hs
@@ -0,0 +1,159 @@
+module Test.Blanks.LocScopeTest where
+
+import Blanks
+import Data.String (IsString)
+import Test.Blanks.Parsing
+import Test.Tasty
+import Test.Tasty.HUnit
+
+-- A newtype indicating an identifier in our language
+newtype Ident = Ident { unIdent :: String } deriving (Eq, Show, Ord, IsString)
+
+-- The type of concrete expressions, labeled with source location
+data CExp l =
+    CExpTrue !l
+  | CExpFalse !l
+  | CExpInt !l !Int
+  | CExpApp !l (CExp l) (CExp l)
+  | CExpAdd !l (CExp l) (CExp l)
+  | CExpIf !l (CExp l) (CExp l) (CExp l)
+  | CExpIsZero !l (CExp l)
+  | CExpVar !l !Ident
+  | CExpAbs !l !Ident (CExp l)
+  deriving (Eq, Show)
+
+-- Extracts the location from a concrete expression
+cexpLoc :: CExp l -> l
+cexpLoc ce =
+  case ce of
+    CExpTrue l -> l
+    CExpFalse l -> l
+    CExpInt l _ -> l
+    CExpApp l _ _ -> l
+    CExpAdd l _ _ -> l
+    CExpIf l _ _ _ -> l
+    CExpIsZero l _ -> l
+    CExpVar l _ -> l
+    CExpAbs l _ _ -> l
+
+-- Just the expressions of our language that have nothing to do with naming
+data Exp a =
+    ExpTrue
+  | ExpFalse
+  | ExpInt !Int
+  | ExpApp a a
+  | ExpAdd a a
+  | ExpIf a a a
+  | ExpIsZero a
+  deriving (Eq, Show, Functor, Foldable, Traversable)
+
+-- A nameless equivalent to 'CExp'
+type ExpScope l = LocScope l (NameOnly Ident) Exp Ident
+
+-- Parsers a concrete expression from a string
+cexpParser :: Parser (CExp SourceSpan)
+cexpParser = result where
+  result = branch
+    [ trueParser
+    , falseParser
+    , intParser
+    , addParser
+    , ifParser
+    , isZeroParser
+    , absParser
+    , appParser
+    , varParser
+    ]
+
+  trueParser = around (const . CExpTrue) (symbol "#t")
+
+  falseParser = around (const . CExpFalse) (symbol "#f")
+
+  intParser = around CExpInt signed
+
+  addParser = around2 CExpAdd (parens (symbol "+" >> double cexpParser))
+
+  ifParser = around3 CExpIf (parens (symbol "if" >> triple cexpParser))
+
+  isZeroParser = around CExpIsZero (parens (symbol "zero?" >> cexpParser))
+
+  absParser = around2 CExpAbs $ parens $ do
+    _ <- symbol "lambda"
+    n <- parens (fmap Ident identifier)
+    b <- cexpParser
+    pure (n, b)
+
+  appParser = around2 CExpApp (parens (double cexpParser))
+
+  varParser = around CExpVar (fmap Ident identifier)
+
+-- Convert to nameless representation
+nameless :: CExp l -> ExpScope l
+nameless ce =
+  case ce of
+    CExpTrue l -> LocScopeEmbed l ExpTrue
+    CExpFalse l -> LocScopeEmbed l ExpFalse
+    CExpInt l i -> LocScopeEmbed l (ExpInt i)
+    CExpApp l a b -> LocScopeEmbed l (ExpApp (nameless a) (nameless b))
+    CExpAdd l a b -> LocScopeEmbed l (ExpAdd (nameless a) (nameless b))
+    CExpIf l a b c -> LocScopeEmbed l (ExpIf (nameless a) (nameless b) (nameless c))
+    CExpIsZero l a -> LocScopeEmbed l (ExpIsZero (nameless a))
+    CExpVar l x -> LocScopeFree l x
+    CExpAbs l x a -> runColocated (blankAbstract1 (NameOnly x) x (nameless a)) l
+
+-- Convert back to named representation. Usually this isn't a necessary operation,
+-- but we want to do round-trip testing
+named :: ExpScope l -> Maybe (CExp l)
+named e =
+  case e of
+    LocScopeBound _ _ -> Nothing
+    LocScopeFree l a -> pure (CExpVar l a)
+    LocScopeBinder l _ (NameOnly x) b -> CExpAbs l x <$> named (blankUnAbstract1 x b)
+    LocScopeEmbed l fe ->
+      case fe of
+        ExpTrue -> pure (CExpTrue l)
+        ExpFalse -> pure (CExpFalse l)
+        ExpInt i -> pure (CExpInt l i)
+        ExpApp a b -> CExpApp l <$> named a <*> named b
+        ExpAdd a b -> CExpAdd l <$> named a <*> named b
+        ExpIf a b c -> CExpIf l <$> named a <*> named b <*> named c
+        ExpIsZero a -> CExpIsZero l <$> named a
+
+-- An ExpScope without locations
+type ExpSimpleScope = Scope (NameOnly Ident) Exp Ident
+
+testSingle :: TestName -> String -> ExpSimpleScope -> TestTree
+testSingle name input expected = testCase name $ do
+  namedExp <- runParserIO cexpParser input
+  let namelessExp = nameless namedExp
+  cexpLoc namedExp @?= locScopeLocation namelessExp
+  let actual = locScopeForget namelessExp
+  expected @?= actual
+  let renamedExp = named namelessExp
+  Just namedExp @?= renamedExp
+
+testLocScope :: TestTree
+testLocScope = testGroup "LocScope" cases where
+  xIdent = Ident "x"
+  yIdent = Ident "y"
+  xExp = ScopeFree xIdent
+  yExp = ScopeFree yIdent
+  trueExp = ScopeEmbed ExpTrue
+  intExp = ScopeEmbed (ExpInt 42)
+  negIntExp = ScopeEmbed (ExpInt (-42))
+  cases =
+    [ testSingle "var" "x" xExp
+    , testSingle "true" "#t" trueExp
+    , testSingle "false" "#f" (ScopeEmbed ExpFalse)
+    , testSingle "int" "42" intExp
+    , testSingle "neg int" "-42" negIntExp
+    , testSingle "add" "(+ 42 -42)" (ScopeEmbed (ExpAdd intExp negIntExp))
+    , testSingle "if" "(if #t 42 -42)" (ScopeEmbed (ExpIf trueExp intExp negIntExp))
+    , testSingle "add var" "(+ 42 x)" (ScopeEmbed (ExpAdd intExp xExp))
+    , testSingle "iszero" "(zero? 42)" (ScopeEmbed (ExpIsZero intExp))
+    , testSingle "app" "(x y)" (ScopeEmbed (ExpApp xExp yExp))
+    , testSingle "abs yy" "(lambda (y) y)" (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0))
+    , testSingle "abs xyy" "(lambda (x) (lambda (y) y))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 0)))
+    , testSingle "abs xyx" "(lambda (x) (lambda (y) x))" (ScopeBinder 1 (NameOnly xIdent) (ScopeBinder 1 (NameOnly yIdent) (ScopeBound 1)))
+    , testSingle "app abs" "((lambda (x) x) 42)" (ScopeEmbed (ExpApp (ScopeBinder 1 (NameOnly xIdent) (ScopeBound 0)) intExp))
+    ]
diff --git a/test/Test/Blanks/Parsing.hs b/test/Test/Blanks/Parsing.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Blanks/Parsing.hs
@@ -0,0 +1,75 @@
+module Test.Blanks.Parsing where
+
+import Control.Applicative (Alternative (..))
+import Control.Exception (throwIO)
+import Data.Void (Void)
+import qualified Text.Megaparsec as MP
+import qualified Text.Megaparsec.Char as MPC
+import qualified Text.Megaparsec.Char.Lexer as MPCL
+
+type Parser = MP.Parsec Void String
+
+-- The parser is not the SUT here, so if it fails,
+-- so does the test. We ensure valid input.
+runParserIO :: Parser a -> String -> IO a
+runParserIO p s =
+  case MP.runParser p "<test>" s of
+    Left e -> throwIO e
+    Right a -> pure a
+
+data SourceSpan = SourceSpan
+  { _ssName :: !FilePath
+  , _ssStartLine :: !MP.Pos
+  , _ssStartColumn :: !MP.Pos
+  , _ssEndLine :: !MP.Pos
+  , _ssEndColumn :: !MP.Pos
+  } deriving (Eq, Show, Ord)
+
+mkSourceSpan :: MP.SourcePos -> MP.SourcePos -> SourceSpan
+mkSourceSpan (MP.SourcePos n sl sc) (MP.SourcePos _ el ec) = SourceSpan n sl sc el ec
+
+around :: (SourceSpan -> a -> b) -> Parser a -> Parser b
+around f pa = (\s a e -> f (mkSourceSpan s e) a) <$> MP.getSourcePos <*> pa <*> MP.getSourcePos
+
+around2 :: (SourceSpan -> a -> b -> c) -> Parser (a, b) -> Parser c
+around2 f pab = (\s (a, b) e -> f (mkSourceSpan s e) a b) <$> MP.getSourcePos <*> pab <*> MP.getSourcePos
+
+around3 :: (SourceSpan -> a -> b -> c -> d) -> Parser (a, b, c) -> Parser d
+around3 f pabc = (\s (a, b, c) e -> f (mkSourceSpan s e) a b c) <$> MP.getSourcePos <*> pabc <*> MP.getSourcePos
+
+double :: Parser a -> Parser (a, a)
+double p = (,) <$> p <*> p
+
+triple :: Parser a -> Parser (a, a, a)
+triple p = (,,) <$> p <*> p <*> p
+
+spaceConsumer :: Parser ()
+spaceConsumer = MPCL.space MPC.space1 lineCmnt blockCmnt
+  where
+    lineCmnt = MPCL.skipLineComment ";"
+    blockCmnt = MPCL.skipBlockComment "#|" "|#"
+
+lexeme :: Parser a -> Parser a
+lexeme = MPCL.lexeme spaceConsumer
+
+symbol :: String -> Parser String
+symbol = MPCL.symbol spaceConsumer
+
+parens :: Parser a -> Parser a
+parens = MP.between (symbol "(") (symbol ")")
+
+nonDelimPred :: Char -> Bool
+nonDelimPred c = c /= '(' && c /= ')' && c /= ' ' && c /= '\t' && c /= '\n'
+
+identifier :: Parser String
+identifier = lexeme (MP.takeWhile1P Nothing nonDelimPred)
+
+-- Take the first successful result, backtracking on failure.
+branch :: [Parser a] -> Parser a
+branch xs =
+  case xs of
+    [] -> empty
+    x:xs' -> MP.try x <|> branch xs'
+
+signed :: Parser Int
+signed = MPCL.signed spaceConsumer (lexeme MPCL.decimal)
diff --git a/test/Test/Blanks/ScopeTest.hs b/test/Test/Blanks/ScopeTest.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Blanks/ScopeTest.hs
@@ -0,0 +1,89 @@
+module Test.Blanks.ScopeTest
+  ( testScope
+  ) where
+
+import Blanks
+import Control.Monad.Identity (Identity (..))
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Test.Blanks.Assertions ((@/=))
+import Test.Tasty
+import Test.Tasty.HUnit
+
+type BareScope = Scope (NameOnly Char) Identity Char
+
+abst :: Char -> BareScope -> BareScope
+abst a = runIdentity . blankAbstract1 (Name a ()) a
+
+bound :: Int -> BareScope
+bound = ScopeBound
+
+var :: Char -> BareScope
+var = pure
+
+freeVars :: BareScope -> Set Char
+freeVars = foldMap Set.singleton
+
+testScope :: TestTree
+testScope =
+  let svar = var 'x'
+      sbound = bound 0
+      sfree = abst 'y' (var 'x')
+      sfree2 = abst 'z' (abst 'y' (var 'x'))
+      sid = abst 'x' (var 'x')
+      swonky = abst 'x' (bound 0)
+      sconst = abst 'x' (abst 'y' (var 'x'))
+      sflip = abst 'x' (abst 'y' (var 'y'))
+      svar2 = var 'e'
+      swonky2 = abst 'x' svar2
+
+      testEq =
+        testCase "eq" $ do
+          svar @?= svar
+          svar @/= svar2
+          sid @?= abst 'x' (var 'x')
+          sid @?= abst 'y' (var 'y')
+          sid @/= abst 'x' (var 'y')
+          sid @/= abst 'y' (var 'x')
+          sid @/= svar
+
+      testFreeVars =
+        testCase "free vars" $ do
+          freeVars svar @?= Set.singleton 'x'
+          freeVars sbound @?= Set.empty
+          freeVars sfree @?= Set.singleton 'x'
+          freeVars sfree2 @?= Set.singleton 'x'
+          freeVars sid @?= Set.empty
+          freeVars swonky @?= Set.empty
+          freeVars sconst @?= Set.empty
+          freeVars sflip @?= Set.empty
+          freeVars svar2 @=? Set.singleton 'e'
+          freeVars swonky2 @?= Set.singleton 'e'
+
+      testInstantiate =
+        testCase "instantiate" $ do
+          blankInstantiate1 (pure svar2) svar @?= svar
+          blankInstantiate1 (pure svar2) sbound @?= svar2
+          blankInstantiate1 (pure svar2) sid @?= sid
+          blankInstantiate1 (pure svar2) swonky @?= swonky2
+
+      testApply =
+        testCase "apply" $ do
+          blankApply1 (pure svar2) sid @?= Right svar2
+          blankApply1 (pure svar2) swonky @?= Right sbound
+          blankApply1 (pure svar2) sconst @?= Right swonky2
+          blankApply1 (pure svar2) sflip @?= Right sid
+
+      testVarSub =
+        testCase "var sub" $ do
+          (svar >>= const svar2) @?= svar2
+          (sfree >>= const svar2) @?= abst 'y' svar2
+          (sfree2 >>= const svar2) @?= abst 'c' (abst 'd' svar2)
+
+      testIdSub =
+        testCase "id sub" $ do
+          (svar >>= const sid) @?= sid
+          (sfree >>= const sid) @?= abst 'y' sid
+          (sfree2 >>= const sid) @?= abst 'c' (abst 'd' sid)
+
+   in testGroup "Scope" [testEq, testFreeVars, testInstantiate, testApply, testVarSub, testIdSub]