diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,7 +4,16 @@
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
-## UNRELEASED
+## 1.2.0 -- 2025-08-27
+
+* Helper function for safely retrieving an in-scope type variable when constructing the ASG  
+* Removed Return nodes, associated pattern synonyms, and the `ret` ASGBuilder function
+* Reworked the renamer to be context sensitive
+* Added new error types for un-renaming
+* Modified ASG helper functions and updated tests to conform with renamer rework
+* Added support for introduction forms (ValNode stuff, ASG helper function, tests)
+* Added support for catamorphism elimination forms
+* Added support for pattern matching elimination form
 
 ## 1.1.0 -- 2025-07-11
 
diff --git a/covenant.cabal b/covenant.cabal
--- a/covenant.cabal
+++ b/covenant.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: covenant
-version: 1.1.0
+version: 1.2.0
 synopsis: Standalone IR for Cardano scripts.
 description:
   A library describing a call-by-push-value, Turner-total IR. Includes the ability to build up the IR programmatically.
@@ -84,6 +84,7 @@
     nonempty-vector ==0.2.4,
     optics-core ==0.4.1.1,
     prettyprinter ==1.7.1,
+    smash ==0.1.0.0,
     tasty ==1.5.3,
     tasty-expected-failure ==0.12.3,
     tasty-hunit ==0.10.2,
@@ -92,7 +93,8 @@
 
 common bench-lang
   import: lang
-  ghc-options: -O2
+  ghc-options:
+    -O2
 
 -- Primary library
 library
@@ -135,6 +137,7 @@
     prettyprinter ==1.7.1,
     quickcheck-instances ==0.3.32,
     quickcheck-transformer ==0.3.1.2,
+    smash ==0.1.0.0,
     tasty-hunit ==0.10.2,
     text >=2.1.1 && <2.2,
     transformers >=0.6.1.0 && <0.7.0.0,
diff --git a/src/Covenant/ASG.hs b/src/Covenant/ASG.hs
--- a/src/Covenant/ASG.hs
+++ b/src/Covenant/ASG.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 -- |
@@ -37,11 +38,11 @@
         Builtin3,
         Builtin6,
         Lam,
-        Force,
-        Return
+        Force
       ),
-    ValNodeInfo (Lit, App, Thunk),
+    ValNodeInfo (Lit, App, Thunk, Cata, DataConstructor, Match),
     ASGNode (..),
+    ASGNodeType (..),
 
     -- ** Functions
     typeASGNode,
@@ -50,36 +51,54 @@
 
     -- ** Types
     CovenantError (..),
-    ScopeInfo,
+    ScopeInfo (..),
     ASGBuilder,
     TypeAppError (..),
     RenameError (..),
+    UnRenameError (..),
+    EncodingArgErr (..),
     CovenantTypeError (..),
+    BoundTyVar,
 
     -- ** Introducers
+    boundTyVar,
     arg,
     builtin1,
     builtin2,
     builtin3,
     builtin6,
     force,
-    ret,
     lam,
     err,
     lit,
     thunk,
+    dataConstructor,
+
+    -- ** Eliminators
     app,
+    cata,
+    match,
 
-    -- ** Elimination
+    -- ** Helpers
+    ctor,
+    lazyLam,
+    dtype,
 
     -- *** Environment
     defaultDatatypes,
 
     -- *** Function
     runASGBuilder,
+    -- only for tests
+    ASGEnv (..),
   )
 where
 
+#if __GLASGOW_HASKELL__==908
+import Data.Foldable (foldl')
+#endif
+
+import Control.Monad (foldM, join, unless, zipWithM)
 import Control.Monad.Except
   ( ExceptT,
     MonadError (throwError),
@@ -98,15 +117,18 @@
   )
 import Covenant.Constant (AConstant, typeConstant)
 import Covenant.Data (DatatypeInfo, mkDatatypeInfo)
-import Covenant.DeBruijn (DeBruijn, asInt)
-import Covenant.Index (Index, count0, intIndex)
-import Covenant.Internal.KindCheck (checkEncodingArgs)
+import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
+import Covenant.Index (Count, Index, count0, intCount, intIndex, wordCount)
+import Covenant.Internal.KindCheck (EncodingArgErr (EncodingArgMismatch), checkEncodingArgs)
 import Covenant.Internal.Ledger (ledgerTypes)
 import Covenant.Internal.Rename
   ( RenameError
-      ( InvalidAbstractionReference
+      ( InvalidAbstractionReference,
+        InvalidScopeReference
       ),
+    UnRenameError (NegativeDeBruijn, UnRenameWildCard),
     renameCompT,
+    renameDatatypeInfo,
     renameValT,
     runRenameM,
     undoRename,
@@ -121,21 +143,45 @@
         Builtin3Internal,
         Builtin6Internal,
         ForceInternal,
-        LamInternal,
-        ReturnInternal
+        LamInternal
       ),
     CovenantTypeError
       ( ApplyCompType,
         ApplyToError,
         ApplyToValType,
         BrokenIdReference,
+        CataAlgebraWrongArity,
+        CataApplyToNonValT,
+        CataNoBaseFunctorForType,
+        CataNoSuchType,
+        CataNonRigidAlgebra,
+        CataNotAnAlgebra,
+        CataUnsuitable,
+        CataWrongBuiltinType,
+        CataWrongValT,
+        ConstructorDoesNotExistForType,
+        DatatypeInfoRenameError,
         EncodingError,
+        FailedToRenameInstantiation,
         ForceCompType,
         ForceError,
         ForceNonThunk,
+        IntroFormErrorNodeField,
+        IntroFormWrongNumArgs,
+        InvalidOpaqueField,
+        LambdaResultsInCompType,
         LambdaResultsInNonReturn,
-        LambdaResultsInValType,
+        MatchErrorAsHandler,
+        MatchNoBBForm,
+        MatchNoDatatypeInfo,
+        MatchNonDatatypeScrutinee,
+        MatchNonThunkBBF,
+        MatchNonValTy,
+        MatchPolymorphicHandler,
+        MatchRenameBBFail,
+        MatchRenameTyConArgFail,
         NoSuchArgument,
+        OutOfScopeTyVar,
         RenameArgumentFailed,
         RenameFunctionFailed,
         ReturnCompType,
@@ -143,24 +189,29 @@
         ReturnWrapsError,
         ThunkError,
         ThunkValType,
+        TypeDoesNotExist,
+        UndeclaredOpaquePlutusDataCtor,
+        UndoRenameFailure,
         UnificationError,
         WrongReturnType
       ),
     Id,
     Ref (AnArg, AnId),
-    ValNodeInfo (AppInternal, LitInternal, ThunkInternal),
+    ValNodeInfo (AppInternal, CataInternal, DataConstructorInternal, LitInternal, MatchInternal, ThunkInternal),
     typeASGNode,
     typeId,
     typeRef,
   )
 import Covenant.Internal.Type
-  ( AbstractTy,
+  ( AbstractTy (BoundAt),
+    BuiltinFlatT (ByteStringT, IntegerT),
     CompT (CompT),
     CompTBody (CompTBody),
-    DataDeclaration,
+    DataDeclaration (DataDeclaration),
     Renamed,
     TyName,
-    ValT (ThunkT),
+    ValT (BuiltinFlat, Datatype, ThunkT),
+    arity,
   )
 import Covenant.Internal.Unification
   ( TypeAppError
@@ -174,7 +225,13 @@
         NoBBForm,
         NoDatatypeInfo
       ),
+    UnifyM,
     checkApp,
+    fixUp,
+    reconcile,
+    runUnifyM,
+    substitute,
+    unify,
   )
 import Covenant.Prim
   ( OneArgFunc,
@@ -186,27 +243,50 @@
     typeThreeArgFunc,
     typeTwoArgFunc,
   )
+import Covenant.Type
+  ( CompT (Comp0),
+    CompTBody (ReturnT),
+    Constructor,
+    ConstructorName,
+    DataDeclaration (OpaqueData),
+    PlutusDataConstructor (PlutusB, PlutusConstr, PlutusI, PlutusList, PlutusMap),
+    Renamed (Unifiable),
+    TyName (TyName),
+    ValT (Abstraction),
+    tyvar,
+  )
 import Data.Bimap (Bimap)
 import Data.Bimap qualified as Bimap
 import Data.Coerce (coerce)
 import Data.Functor.Identity (Identity, runIdentity)
 import Data.Kind (Type)
+import Data.List (find)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
-import Data.Maybe (fromJust)
+import Data.Maybe (fromJust, isJust, mapMaybe)
+import Data.Set qualified as Set
+import Data.Text qualified as T
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Data.Vector.NonEmpty qualified as NonEmpty
+import Data.Void (Void, vacuous)
+import Data.Wedge (Wedge, wedge)
+import Data.Word (Word32)
 import Optics.Core
   ( A_Lens,
     LabelOptic (labelOptic),
+    at,
+    folded,
     ix,
     lens,
     over,
     preview,
     review,
+    toListOf,
     view,
     (%),
+    _1,
+    _2,
   )
 
 -- | A fully-assembled Covenant ASG.
@@ -249,8 +329,14 @@
 nodeAt :: Id -> ASG -> ASGNode
 nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings
 
+-- | The environment used when \'building up\' an 'ASG'. This type is exposed
+-- only for testing, or debugging, and should /not/ be used in general by those
+-- who just want to build an 'ASG'.
+--
+-- @since 1.2.0
 data ASGEnv = ASGEnv ScopeInfo (Map TyName (DatatypeInfo AbstractTy))
 
+-- | @since 1.2.0
 instance
   (k ~ A_Lens, a ~ ScopeInfo, b ~ ScopeInfo) =>
   LabelOptic "scopeInfo" k ASGEnv ASGEnv a b
@@ -261,6 +347,7 @@
       (\(ASGEnv si _) -> si)
       (\(ASGEnv _ dti) si -> ASGEnv si dti)
 
+-- | @since 1.2.0
 instance
   (k ~ A_Lens, a ~ Map TyName (DatatypeInfo AbstractTy), b ~ Map TyName (DatatypeInfo AbstractTy)) =>
   LabelOptic "datatypeInfo" k ASGEnv ASGEnv a b
@@ -281,8 +368,8 @@
 -- the functionality provided by this module is not recommended, unless you know
 -- /exactly/ what you're doing.
 --
--- @since 1.0.0
-newtype ScopeInfo = ScopeInfo (Vector (Vector (ValT AbstractTy)))
+-- @since 1.2.0
+newtype ScopeInfo = ScopeInfo (Vector (Word32, Vector (ValT AbstractTy)))
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -296,9 +383,9 @@
 -- enclosing scope, 2 is the enclosing scope of our enclosing scope, etc. The
 -- \'inner\' 'Vector's are positional lists of argument types.
 --
--- @since 1.0.0
+-- @since 1.2.0
 instance
-  (k ~ A_Lens, a ~ Vector (Vector (ValT AbstractTy)), b ~ Vector (Vector (ValT AbstractTy))) =>
+  (k ~ A_Lens, a ~ Vector (Word32, Vector (ValT AbstractTy)), b ~ Vector (Word32, Vector (ValT AbstractTy))) =>
   LabelOptic "argumentInfo" k ScopeInfo ScopeInfo a b
   where
   {-# INLINEABLE labelOptic #-}
@@ -334,19 +421,13 @@
 pattern Force :: Ref -> CompNodeInfo
 pattern Force r <- ForceInternal r
 
--- | Produce the result of a computation.
---
--- @since 1.0.0
-pattern Return :: Ref -> CompNodeInfo
-pattern Return r <- ReturnInternal r
-
 -- | A lambda.
 --
--- @since 1.0.0
-pattern Lam :: Id -> CompNodeInfo
-pattern Lam i <- LamInternal i
+-- @since 1.2.0
+pattern Lam :: Ref -> CompNodeInfo
+pattern Lam r <- LamInternal r
 
-{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Return, Lam #-}
+{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Lam #-}
 
 -- | A compile-time literal of a flat builtin type.
 --
@@ -367,8 +448,26 @@
 pattern Thunk :: Id -> ValNodeInfo
 pattern Thunk i <- ThunkInternal i
 
-{-# COMPLETE Lit, App, Thunk #-}
+-- | \'Tear down\' a self-recursive value with an algebra.
+--
+-- @since 1.0.0
+pattern Cata :: Ref -> Ref -> ValNodeInfo
+pattern Cata algebraRef valRef <- CataInternal algebraRef valRef
 
+-- | Inject (zero or more) fields into a data constructor
+--
+-- @since 1.2.0
+pattern DataConstructor :: TyName -> ConstructorName -> Vector Ref -> ValNodeInfo
+pattern DataConstructor tyName ctorName fields <- DataConstructorInternal tyName ctorName fields
+
+-- | Deconstruct a value of a data type using the supplied handlers for each arm
+--
+-- @since 1.2.0
+pattern Match :: Ref -> Vector Ref -> ValNodeInfo
+pattern Match scrutinee handlers <- MatchInternal scrutinee handlers
+
+{-# COMPLETE Lit, App, Thunk, Cata, DataConstructor, Match #-}
+
 -- | Any problem that might arise when building an ASG programmatically.
 --
 -- @since 1.0.0
@@ -467,7 +566,7 @@
 arg scope index = do
   let scopeAsInt = review asInt scope
   let indexAsInt = review intIndex index
-  lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % ix indexAsInt))
+  lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % _2 % ix indexAsInt))
   case lookedUp of
     Nothing -> throwError . NoSuchArgument scope $ index
     Just t -> pure . Arg scope index $ t
@@ -538,24 +637,6 @@
     CompNodeType t -> throwError . ForceCompType $ t
     ErrorNodeType -> throwError ForceError
 
--- | Given the result of a function body (either a value or an error), construct
--- the return for it. Will fail if that reference aims at a computation node.
---
--- @since 1.0.0
-ret ::
-  forall (m :: Type -> Type).
-  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
-  Ref ->
-  m Id
-ret r = do
-  refT <- typeRef r
-  case refT of
-    ValNodeType t -> do
-      let t' = CompT count0 . CompTBody . NonEmpty.singleton $ t
-      refTo . ACompNode t' . ReturnInternal $ r
-    CompNodeType t -> throwError . ReturnCompType $ t
-    ErrorNodeType -> err
-
 -- | Given a desired type, and a computation which will construct a lambda body
 -- when executed (with the scope extended with the arguments the functions can
 -- expect), construct a lambda.
@@ -567,37 +648,34 @@
 -- \'bottom-up\', whereas function arguments (and their scopes) are necessarily
 -- top-down. Thus, we need to \'delay\' the construction of a lambda's body to
 -- ensure that proper scoped argument information can be given to it, hence why
--- the argument being passed is an @m Id@.
+-- the argument being passed is an @m Ref@.
 --
--- @since 1.0.0
+-- @since 1.2.0
 lam ::
   forall (m :: Type -> Type).
   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
   CompT AbstractTy ->
-  m Id ->
+  m Ref ->
   m Id
-lam expectedT@(CompT _ (CompTBody xs)) bodyComp = do
+lam expectedT@(CompT cnt (CompTBody xs)) bodyComp = do
   let (args, resultT) = NonEmpty.unsnoc xs
-  bodyId <- local (over (#scopeInfo % #argumentInfo) (Vector.cons args)) bodyComp
-  bodyNode <- lookupRef bodyId
-  case bodyNode of
-    Nothing -> throwError . BrokenIdReference $ bodyId
-    -- This unifies with anything, so we're fine
-    Just AnError -> refTo . ACompNode expectedT . LamInternal $ bodyId
-    Just (ACompNode t specs) -> case specs of
-      ReturnInternal r -> do
-        rT <- typeRef r
-        case rT of
-          -- Note (Koz, 17/04/2025): I am not 100% sure about this, but I can't
-          -- see how anything else would make sense.
-          ValNodeType actualT ->
-            if resultT == actualT
-              then refTo . ACompNode expectedT . LamInternal $ bodyId
-              else throwError . WrongReturnType resultT $ actualT
-          ErrorNodeType -> throwError ReturnWrapsError -- Should be impossible
-          CompNodeType t' -> throwError . ReturnWrapsCompType $ t'
-      _ -> throwError . LambdaResultsInNonReturn $ t
-    Just (AValNode t _) -> throwError . LambdaResultsInValType $ t
+      cntW = view wordCount cnt
+  bodyRef <- local (over (#scopeInfo % #argumentInfo) (Vector.cons (cntW, args))) bodyComp
+  case bodyRef of
+    AnArg (Arg _ _ argTy) -> do
+      if argTy == resultT
+        then refTo . ACompNode expectedT . LamInternal $ bodyRef
+        else throwError . WrongReturnType resultT $ argTy
+    AnId bodyId ->
+      lookupRef bodyId >>= \case
+        Nothing -> throwError . BrokenIdReference $ bodyId
+        -- This unifies with anything, so we're fine
+        Just AnError -> refTo . ACompNode expectedT . LamInternal . AnId $ bodyId
+        Just (AValNode ty _) -> do
+          if ty == resultT
+            then refTo . ACompNode expectedT . LamInternal . AnId $ bodyId
+            else throwError . WrongReturnType resultT $ ty
+        Just (ACompNode t _) -> throwError $ LambdaResultsInCompType t
 
 -- | Construct the error node.
 --
@@ -608,37 +686,245 @@
   m Id
 err = refTo AnError
 
--- | Given an 'Id' referring to a computation, and a 'Vector' of 'Ref's to the
--- desired arguments, construct the application of the arguments to that
--- computation. This can fail for a range of reasons:
+-- | Performs both term and type application. More precisely, given:
 --
+-- * An 'Id' referring to a computation; and
+-- * A 'Vector' of 'Ref's for the desired term arguments to the computation, in
+--   order; and
+-- * A 'Vector' of (optional) type arguments to the computation, also in order.
+--
+-- we produce the result of that application.
+--
+-- This can fail for a range of reasons:
+--
 -- * Type mismatch between what the computation expects and what it's given
 -- * Too many or too few arguments
 -- * Not a computation type for 'Id' argument
 -- * Not value types for 'Ref's
+-- * Renaming failures (likely due to a malformed function or argument type)
 --
--- @since 1.0.0
+-- = Note
+--
+-- We use the 'Wedge' data type to designate type arguments, as it can represent
+-- the three possibilities we need:
+--
+-- * \'Infer this argument\', specified as 'Nowhere'.
+-- * \'Use this type variable in our scope\', specified as 'Here'.
+-- * \'Use this concrete type\', specified as 'There'.
+--
+-- @since 1.2.0
 app ::
   forall (m :: Type -> Type).
   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
   Id ->
   Vector Ref ->
+  Vector (Wedge BoundTyVar (ValT Void)) ->
   m Id
-app fId argRefs = do
+app fId argRefs instTys = do
   lookedUp <- typeId fId
+  let rawSubs = mkSubstitutions instTys
+  subs <- renameSubs rawSubs
+  scopeInfo <- askScope
   case lookedUp of
-    CompNodeType fT -> case runRenameM . renameCompT $ fT of
+    CompNodeType fT -> case runRenameM scopeInfo . renameCompT $ fT of
       Left err' -> throwError . RenameFunctionFailed fT $ err'
       Right renamedFT -> do
+        instantiatedFT <- instantiate subs renamedFT
         renamedArgs <- traverse renameArg argRefs
         tyDict <- asks (view #datatypeInfo)
-        result <- either (throwError . UnificationError) pure $ checkApp tyDict renamedFT (Vector.toList renamedArgs)
-        let restored = undoRename result
+        result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)
+        restored <- undoRenameM result
         checkEncodingWithInfo tyDict restored
         refTo . AValNode restored . AppInternal fId $ argRefs
     ValNodeType t -> throwError . ApplyToValType $ t
     ErrorNodeType -> throwError ApplyToError
+  where
+    mkSubstitutions :: Vector (Wedge BoundTyVar (ValT Void)) -> [(Index "tyvar", ValT AbstractTy)]
+    mkSubstitutions =
+      Vector.ifoldl'
+        ( \acc i' w ->
+            let i = fromJust . preview intIndex $ i'
+             in wedge
+                  acc
+                  (\(BoundTyVar dbIx posIx) -> (i, tyvar dbIx posIx) : acc)
+                  (\v -> (i, vacuous v) : acc)
+                  w
+        )
+        []
 
+    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]
+    renameSubs subs =
+      askScope >>= \scope -> case traverse (traverse (runRenameM scope . renameValT)) subs of
+        Left err' -> throwError $ FailedToRenameInstantiation err'
+        Right res -> pure res
+
+    instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)
+    instantiate [] fn = pure fn
+    instantiate subs fn = do
+      instantiated <- liftUnifyM . fixUp $ foldr (\(i, t) f -> substitute i t f) (ThunkT fn) subs
+      case instantiated of
+        ThunkT res -> pure res
+        other ->
+          throwError . UnificationError . ImpossibleHappened $
+            "Impossible happened: Result of tyvar instantiation should be a thunk, but is: "
+              <> T.pack (show other)
+
+-- | Introduce a data constructor.
+--
+-- The first argument is a type name (for example, @\"Maybe\"@). The second
+-- argument is a constructor of that type (for example, @\"Just\"@ or
+-- @\"Nothing\"@). The third argument are the values to \'fill in\' all the fields
+-- of the constructor requested.
+--
+-- = Note
+--
+-- 'dataConstructor' yields thunks, which must be forced, and then possibly have
+-- type arguments applied to them. The reason for this is subtle, but important.
+-- Consider the @Nothing@ constructor of @Maybe@: as this has no fields, we
+-- cannot use the field type to determine what the type argument to @Maybe@
+-- should be in this case. As datatype terms are values, they do not bind type
+-- variables, and thus, we cannot have a return type that makes sense in this
+-- case.
+--
+-- We resolve this problem by returning a thunk. In the case of our example,
+-- @Nothing@ would produce @<forall a . !Maybe a>@.
+--
+-- @since 1.2.0
+dataConstructor ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  TyName ->
+  ConstructorName ->
+  Vector Ref ->
+  m Id
+dataConstructor tyName ctorName fields = do
+  thisTyInfo <- lookupDatatypeInfo
+  let thisTyDecl = view #originalDecl thisTyInfo
+  renamedFieldTypes <-
+    traverse renameArg fields
+      >>= ( \case
+              Nothing -> throwError $ IntroFormErrorNodeField tyName ctorName fields
+              Just ok -> pure ok
+          )
+        . sequence
+  {- The procedures for handling a typed declared as Opaque and a "normal" type are totally different.
+
+     For Opaque types, we just have to check that the "ConstructorName" we get corresponds to a constructor of
+     PlutusData, then validate that the arguments conform with that PlutusData constructor.
+  -}
+  case thisTyDecl of
+    OpaqueData _ opaqueCtorSet -> do
+      checkOpaqueArgs opaqueCtorSet renamedFieldTypes
+      refTo $ AValNode (Datatype tyName mempty) (DataConstructorInternal tyName ctorName fields)
+    DataDeclaration _ count ctors _ -> do
+      -- First we check that the arity of the constructor is equal to the number of fields in the decl.
+      checkFieldArity (Vector.length fields) thisTyInfo
+      -- Then we resolve the supplied field Refs, rename, and throw an error if we're passed an error node.
+
+      -- Then we construct the return type.
+      resultThunk <- mkResultThunk count ctors renamedFieldTypes
+      -- Then we undo the renaming.
+      restored <- undoRenameM resultThunk
+      -- Then we check the compatibility of the arguments with the datatype's encoding.
+      asks (view #datatypeInfo) >>= \dti -> checkEncodingWithInfo dti restored
+      -- Finally, if nothing has thrown an error, we return a reference to our result node, decorated with the
+      -- return type we constructed.
+      refTo $ AValNode restored (DataConstructorInternal tyName ctorName fields)
+  where
+    {- Constructs the result type of the introduction form. Arguments are:
+         1. The count (number of tyvars) from the data declaration.
+         2. The vector of constructors from the data declaration.
+         3. The (renamed and resolved) vector of supplied arguments.
+
+       The procedure goes like:
+         1. Extract the argument types from the constructor in the declaration. Any tyvars here
+            *have* to be Unifiable (unless something has slipped past the kind checker) -
+            data declarations have atomic, independent scopes.
+         2. Unify those with the actual, supplied field types, yielding a set of substitutions.
+         3. Construct a fully abstract (i.e. parameterized only by unifiable type variables) representation of the
+            type constructor.
+         4. Apply those substitutions to the abstract type constructor.
+         5. Wrap the "concretified" type constructor in a thunk and use `fixUp` to sort out the `Count` and
+            indices.
+    -}
+    mkResultThunk :: Count "tyvar" -> Vector (Constructor Renamed) -> Vector (ValT Renamed) -> m (ValT Renamed)
+    mkResultThunk count' declCtors fieldArgs' = do
+      declCtorFields <- Vector.toList . view #constructorArgs <$> findConstructor declCtors
+      subs <- unifyFields declCtorFields fieldArgs
+      let tyConAbstractArgs = mapMaybe (fmap (Abstraction . Unifiable) . preview intIndex) [0, 1 .. (count - 1)]
+          tyConAbstract = Datatype tyName (Vector.fromList tyConAbstractArgs)
+      let tyConConcrete = Map.foldlWithKey' (\acc i t -> substitute i t acc) tyConAbstract subs
+      liftUnifyM . fixUp . ThunkT . Comp0 . ReturnT $ tyConConcrete
+      where
+        count :: Int
+        count = review intCount count'
+
+        fieldArgs :: [ValT Renamed]
+        fieldArgs = Vector.toList fieldArgs'
+
+    {- Unifies the declaration fields (which may be abstract) with the supplied fields
+       (which will be "concrete", in the sense that "they have to be rigid if they're tyvars").
+
+       Returns a (reconciled) set of substitutions which can be applied to a fully-abstract (i.e.
+       parameterized only by Unifiable tyVars) to yield the concrete, applied type constructor.
+    -}
+    unifyFields :: [ValT Renamed] -> [ValT Renamed] -> m (Map (Index "tyvar") (ValT Renamed))
+    unifyFields declFields suppliedFields = liftUnifyM $ do
+      rawSubs <- zipWithM unify declFields suppliedFields
+      foldM reconcile Map.empty rawSubs
+
+    {- Checks that the number of fields supplied as arguments is equal to the
+       number of fields in the corresponding constructor of the data declaration.
+
+       This is needed because `zipWithM unifyFields` won't throw an error in the case that they are not equal.
+    -}
+    checkFieldArity :: Int -> DatatypeInfo Renamed -> m ()
+    checkFieldArity actualNumFields dtInfo = do
+      let ctors = toListOf (#originalDecl % #datatypeConstructors % folded) dtInfo
+      expectedNumFields <- Vector.length . view #constructorArgs <$> findConstructor ctors
+      unless (actualNumFields == expectedNumFields) $
+        throwError $
+          IntroFormWrongNumArgs tyName ctorName actualNumFields
+
+    checkOpaqueArgs :: Set.Set PlutusDataConstructor -> Vector (ValT Renamed) -> m ()
+    checkOpaqueArgs declCtors fieldArgs' = case ctorName of
+      "I" -> opaqueCheck PlutusI [BuiltinFlat IntegerT]
+      "B" -> opaqueCheck PlutusB [BuiltinFlat ByteStringT]
+      "List" -> opaqueCheck PlutusList [Datatype "List" (Vector.fromList [Datatype "Data" mempty])]
+      "Map" -> opaqueCheck PlutusMap [Datatype "Map" (Vector.fromList [Datatype "Data" mempty, Datatype "Data" mempty])]
+      "Constr" -> opaqueCheck PlutusConstr [BuiltinFlat IntegerT, Datatype "List" (Vector.fromList [Datatype "Data" mempty])]
+      _ -> throwError $ UndeclaredOpaquePlutusDataCtor declCtors ctorName
+      where
+        fieldArgs :: [ValT Renamed]
+        fieldArgs = Vector.toList fieldArgs'
+        opaqueCheck :: PlutusDataConstructor -> [ValT Renamed] -> m ()
+        opaqueCheck setMustHaveThis fieldShouldBeThis = do
+          unless (setMustHaveThis `Set.member` declCtors) $ throwError (UndeclaredOpaquePlutusDataCtor declCtors ctorName)
+          unless (fieldArgs == fieldShouldBeThis) $ throwError (InvalidOpaqueField declCtors ctorName fieldArgs)
+
+    -- convenience helpers
+
+    -- Looks up a constructor in a foldable container of constructors (which is probably always a vector but w/e)
+    -- Exists to avoid duplicating this code in a few places.
+    findConstructor ::
+      forall (t :: Type -> Type) (a :: Type).
+      (Foldable t) =>
+      t (Constructor a) ->
+      m (Constructor a)
+    findConstructor xs = case find (\x -> view #constructorName x == ctorName) xs of
+      Nothing -> throwError $ ConstructorDoesNotExistForType tyName ctorName
+      Just ctor' -> pure ctor'
+
+    -- Looks up the DatatypeInfo for the type argument supplied
+    -- and also renames (and rethrows the rename error if renaming fails)
+    lookupDatatypeInfo :: m (DatatypeInfo Renamed)
+    lookupDatatypeInfo =
+      asks (preview (#datatypeInfo % ix tyName)) >>= \case
+        Nothing -> throwError $ TypeDoesNotExist tyName
+        Just infoAbstract -> case renameDatatypeInfo infoAbstract of
+          Left e -> throwError $ DatatypeInfoRenameError e
+          Right infoRenamed -> pure infoRenamed
+
 -- | Construct a node corresponding to the given constant.
 --
 -- @since 1.0.0
@@ -665,20 +951,260 @@
     ValNodeType t -> throwError . ThunkValType $ t
     ErrorNodeType -> throwError ThunkError
 
+-- | Given a 'Ref' to an algebra (that is, something taking a base functor and
+-- producing some result), and a 'Ref' to a value associated with that base
+-- functor, build a catamorphism to tear it down. This can fail for a range of
+-- reasons:
+--
+-- * First 'Ref' is not a thunk taking one argument
+-- * The argument to the thunk isn't a base functor, or isn't a suitable base
+--   functor for the second argument
+-- * Second argument is not a value type
+--
+-- = Note
+--
+-- 'cata' cannot work with /non-rigid/ algebras; that is, all algebras must be
+-- functions that bind no type variables of their own.
+--
+-- @since 1.1.0
+cata ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  Ref ->
+  Ref ->
+  m Id
+cata rAlg rVal =
+  typeRef rVal >>= \case
+    ValNodeType valT ->
+      typeRef rAlg >>= \case
+        t@(ValNodeType (ThunkT algT)) -> case algT of
+          Comp0 (CompTBody nev) -> do
+            let algebraArity = arity algT
+            unless (algebraArity == 1) (throwError . CataAlgebraWrongArity $ algebraArity)
+            case nev NonEmpty.! 0 of
+              Datatype bfName bfTyArgs -> do
+                -- If we got this far, we know at minimum that we have somewhat
+                -- sensical arguments. Now we have to make sure that we have a
+                -- suitable type for the algebra, and a suitable thing to tear
+                -- down.
+                --
+                -- After verifying this, we use `tryApply` so the unification
+                -- machinery can produce the type we expect with proper
+                -- concretifications.
+                unless (Vector.length bfTyArgs > 0) (throwError . CataNotAnAlgebra $ t)
+                let lastTyArg = Vector.last bfTyArgs
+                unless (nev NonEmpty.! 1 == lastTyArg) (throwError . CataNotAnAlgebra $ t)
+                appliedArgT <- case valT of
+                  BuiltinFlat bT -> case bT of
+                    ByteStringT -> do
+                      unless (bfName == "ByteString_F") (throwError . CataUnsuitable algT $ valT)
+                      pure $ Datatype "ByteString_F" . Vector.singleton $ lastTyArg
+                    IntegerT -> do
+                      let isSuitableBaseFunctor = bfName == "Natural_F" || bfName == "Negative_F"
+                      unless isSuitableBaseFunctor (throwError . CataUnsuitable algT $ valT)
+                      pure $ Datatype bfName . Vector.singleton $ lastTyArg
+                    _ -> throwError . CataWrongBuiltinType $ bT
+                  Datatype tyName tyVars -> do
+                    lookedUp <- asks (view (#datatypeInfo % at tyName))
+                    case lookedUp of
+                      Nothing -> throwError . CataNoSuchType $ tyName
+                      Just info -> case view #baseFunctor info of
+                        Just (DataDeclaration actualBfName _ _ _, _) -> do
+                          unless (bfName == actualBfName) (throwError . CataUnsuitable algT $ valT)
+                          let lastTyArg' = stepDownDB lastTyArg
+                          pure . Datatype bfName . Vector.snoc tyVars $ lastTyArg'
+                        _ -> throwError . CataNoBaseFunctorForType $ tyName
+                  _ -> throwError . CataWrongValT $ valT
+                resultT <- tryApply algT appliedArgT
+                refTo . AValNode resultT . CataInternal rAlg $ rVal
+              _ -> throwError . CataNotAnAlgebra $ t
+          _ -> throwError . CataNonRigidAlgebra $ algT
+        t -> throwError . CataNotAnAlgebra $ t
+    t -> throwError . CataApplyToNonValT $ t
+
+-- | Perform a pattern match. The first argument is the value to be matched on,
+-- and the second argument is a 'Vector' of \'handlers\' for each possible
+-- \'arm\' of the type of the value to be matched on.
+--
+-- All handlers must be thunks, and must all return the same (concrete) result.
+-- Polymorphic \'handlers\' (that is, thunks whose computation binds type
+-- variables of its own) will fail to compile.
+--
+-- @since 1.2.0
+match ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  Ref ->
+  Vector Ref ->
+  m Id
+match scrutinee handlers = do
+  scrutNodeTy <- typeRef scrutinee
+  case scrutNodeTy of
+    ValNodeType scrutTy@(Datatype tn args) ->
+      isRecursive scrutTy >>= \case
+        True -> goRecursive tn args
+        False -> goNonRecursive tn args
+    ValNodeType other -> throwError $ MatchNonDatatypeScrutinee other
+    other -> throwError $ MatchNonValTy other
+  where
+    isRecursive :: ValT AbstractTy -> m Bool
+    isRecursive (Datatype tyName _) = do
+      datatypeInfoExists <- asks (isJust . preview (#datatypeInfo % ix tyName))
+      if datatypeInfoExists
+        then asks (isJust . join . preview (#datatypeInfo % ix tyName % #baseFunctor))
+        else throwError $ MatchNoDatatypeInfo tyName
+    isRecursive _ = pure False
+
+    goRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id
+    goRecursive tn@(TyName rawTn) tyConArgs = do
+      -- This fromJust is safe b/c the presence of absence of base functor data is the condition that
+      -- determines whether we're in this branch or the non-recursive one
+      rawBFBB <- asks (snd . fromJust . join . preview (#datatypeInfo % ix tn % #baseFunctor))
+      bfbb <- instantiateBFBB rawBFBB
+      handlers' <- Vector.toList <$> traverse cleanupHandler handlers
+      tyDict <- asks (view #datatypeInfo)
+      case checkApp tyDict bfbb (Just <$> handlers') of
+        Right appliedBfbb -> do
+          result <- undoRenameM appliedBfbb
+          refTo $ AValNode result (MatchInternal scrutinee handlers)
+        Left err' -> throwError . UnificationError $ err'
+      where
+        instantiateBFBB :: ValT AbstractTy -> m (CompT Renamed)
+        instantiateBFBB bfbb = do
+          -- we have a BFBB like:
+          -- listBB :: forall a r . r -> <a -> r -> !r> -> !r
+          -- And we need to:
+          --   1. Instantiate all of the type arguments to the original datatype (e.g. the 'a' in List a)
+          --      into the BFBB
+          --   2. Instantiate the *last* tyvar bound by the BBBF to the type of the original datatype
+          --      giving us, e.g. ListF a (List a)
+          scope <- askScope
+          renamedBFBB <- case runRenameM scope (renameValT bfbb) of
+            Left err' -> throwError $ MatchRenameBBFail err'
+            Right res -> pure res
+          -- The type constructor for the base-functor variant of the scrutinee type.
+          let scrut = Datatype tn tyConArgs
+          let scrutF = Datatype (TyName $ rawTn <> "_F") (Vector.snoc tyConArgs scrut)
+          -- These are arguments to the original type constructor plus the snoc'd original type.
+          -- E.g. if we have:
+          --      Scrutinee: List Int
+          --   this should be:
+          --   [Int, List Int]
+          let bfInstArgs = Vector.snoc tyConArgs scrutF
+          renamedArgs <- case runRenameM scope (traverse renameValT bfInstArgs) of
+            Left err' -> throwError $ MatchRenameTyConArgFail err'
+            Right res -> pure res
+          let subs :: Vector (Index "tyvar", ValT Renamed)
+              subs = Vector.imap (\i v -> (fromJust . preview intIndex $ i, v)) renamedArgs
+              subbed = foldl' (\bbf (i, v) -> substitute i v bbf) renamedBFBB subs
+          case subbed of
+            ThunkT bfComp -> pure bfComp
+            other -> throwError $ MatchNonThunkBBF other
+
+    -- Unwraps a thunk handler if it is a handler for a nullary constructor.
+    cleanupHandler :: Ref -> m (ValT Renamed)
+    cleanupHandler r =
+      renameArg r >>= \case
+        Nothing ->
+          throwError $ MatchErrorAsHandler r
+        Just hVal -> case hVal of
+          hdlr@(ThunkT (CompT cnt (ReturnT v)))
+            | cnt == count0 -> pure v
+            | otherwise -> throwError $ MatchPolymorphicHandler hdlr
+          other -> pure other
+
+    goNonRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id
+    goNonRecursive tn tyConArgs = do
+      rawBBF <- asks (fromJust . preview (#datatypeInfo % ix tn % #bbForm))
+      (instantiatedBBF :: CompT Renamed) <- instantiateBB rawBBF tyConArgs
+      handlers' <- Vector.toList <$> traverse cleanupHandler handlers
+      tyDict <- asks (view #datatypeInfo)
+      case checkApp tyDict instantiatedBBF (Just <$> handlers') of
+        Right appliedBBF -> do
+          result <- undoRenameM appliedBBF
+          refTo $ AValNode result (MatchInternal scrutinee handlers)
+        Left err' -> throwError . UnificationError $ err'
+      where
+        instantiateBB :: Maybe (ValT AbstractTy) -> Vector (ValT AbstractTy) -> m (CompT Renamed)
+        instantiateBB Nothing _ = throwError $ MatchNoBBForm tn
+        instantiateBB (Just bb) tyArgs = do
+          scope <- askScope
+          renamedBB <- case runRenameM scope (renameValT bb) of
+            Left err' -> throwError $ MatchRenameBBFail err'
+            Right res -> pure res
+          renamedArgs <- case runRenameM scope (traverse renameValT tyArgs) of
+            Left err' -> throwError $ MatchRenameTyConArgFail err'
+            Right res -> pure res
+          let subs :: Vector (Index "tyvar", ValT Renamed)
+              subs = Vector.imap (\i v -> (fromJust . preview intIndex $ i, v)) renamedArgs
+              subbed = foldl' (\bbf (i, v) -> substitute i v bbf) renamedBB subs
+          case subbed of
+            ThunkT bbComp -> pure bbComp
+            other -> throwError $ MatchNonThunkBBF other
+
 -- Helpers
 
+-- Note (Koz, 13/08/2025): We need this procedure specifically for `cata`. The
+-- reason for this has to do with how we construct the 'base functor form' of
+-- the value to be torn down by the catamorphism, in order to use the
+-- unification machinery to get the type of the final result.
+--
+-- To be specific, suppose we have `<List_F r (Maybe r) -> !Maybe r>` as our algebra
+-- argument (where `r` is some rigid), and `List r` as the value to be torn
+-- down. If we assume the rigid is bound one scope away, `r`'s DeBruijn index
+-- will be `S Z` for
+-- the value to be torn down, but `S (S Z)` for the algebra argument. The way
+-- our approach works is:
+--
+-- 1. Look at the algebra argument, specifically the base functor type. Take its
+--    last type argument, which we will call `last`.
+-- 2. Determine the base functor for the value to be torn down. Cook up a new
+--    instance of the base functor type, copying all the type arguments from the
+--    value to be torn down in the same order. Then put `last` at the end.
+-- 3. Force the algebra argument thunk, then try and apply the result of Step 2
+--    to that.
+--
+-- Following the steps above for our example, we would proceed as follows:
+--
+-- 1. Set `last` as `Maybe r`.
+-- 2. Cook up `List_F r (Maybe r)`. Note that this matches what the algebra
+--    expects.
+-- 3. Use the unifier with `List_F r (Maybe r) -> !Maybe r`, applying the
+--    argument `List_F r (Maybe r)` from Step 2.
+--
+-- However, if `last` is a rigid, we have an 'off by one error'. To see why,
+-- consider the form of the algebra argument:
+--
+-- `ThunkT . Comp0 $ Datatype "List_F" [tyvar (S (S Z)) ix0, ....`
+--
+-- However, `tyvar (S (S Z)) ix0` is not valid in the scope of the value to be
+-- torn down: that same rigid would have DeBruijn index `S Z` there instead.
+-- This applies the same if the tyvar is part of a datatype.
+--
+-- As we prohibit non-rigid algebras, this requires us to lower the DeBruijn
+-- index by one for our process.
+stepDownDB :: ValT AbstractTy -> ValT AbstractTy
+stepDownDB = \case
+  Abstraction (BoundAt db i) -> case db of
+    -- This is impossible, so we just return it unmodified
+    Z -> Abstraction (BoundAt db i)
+    (S db') -> Abstraction (BoundAt db' i)
+  Datatype tyName tyArgs -> Datatype tyName . fmap stepDownDB $ tyArgs
+  x -> x
+
 renameArg ::
   forall (m :: Type -> Type).
-  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
   Ref ->
   m (Maybe (ValT Renamed))
 renameArg r =
-  typeRef r >>= \case
-    CompNodeType t -> throwError . ApplyCompType $ t
-    ValNodeType t -> case runRenameM . renameValT $ t of
-      Left err' -> throwError . RenameArgumentFailed t $ err'
-      Right renamed -> pure . Just $ renamed
-    ErrorNodeType -> pure Nothing
+  askScope >>= \scope ->
+    typeRef r >>= \case
+      CompNodeType t -> throwError . ApplyCompType $ t
+      ValNodeType t -> case runRenameM scope . renameValT $ t of
+        Left err' -> throwError . RenameArgumentFailed t $ err'
+        Right renamed -> pure . Just $ renamed
+      ErrorNodeType -> pure Nothing
 
 checkEncodingWithInfo ::
   forall (a :: Type) (m :: Type -> Type).
@@ -689,3 +1215,146 @@
 checkEncodingWithInfo tyDict valT = case checkEncodingArgs (view (#originalDecl % #datatypeEncoding)) tyDict valT of
   Left encErr -> throwError $ EncodingError encErr
   Right {} -> pure ()
+
+tryApply ::
+  forall (m :: Type -> Type).
+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  CompT AbstractTy ->
+  ValT AbstractTy ->
+  m (ValT AbstractTy)
+tryApply algebraT argT =
+  askScope >>= \scope -> case runRenameM scope . renameCompT $ algebraT of
+    Left err' -> throwError . RenameFunctionFailed algebraT $ err'
+    Right renamedAlgebraT -> case runRenameM scope . renameValT $ argT of
+      Left err' -> throwError . RenameArgumentFailed argT $ err'
+      Right renamedArgT -> do
+        tyDict <- asks (view #datatypeInfo)
+        case checkApp tyDict renamedAlgebraT [Just renamedArgT] of
+          Left err' -> throwError . UnificationError $ err'
+          Right resultT -> undoRenameM resultT
+
+-- Putting this here to reduce chance of annoying manual merge (will move later)
+
+-- | Wrapper around an `Arg` that we know represents an in-scope type variable.
+-- @since 1.2.0
+data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")
+  deriving stock
+    ( -- @since 1.2.0
+      Show,
+      -- @since 1.2.0
+      Eq,
+      -- @since 1.2.0
+      Ord
+    )
+
+-- | Given a DeBruijn index (designating scope) and positional index (designating
+-- which variable in that scope we are interested in), retrieve an in-scope type
+-- variable.
+--
+-- This will error if we request a type variable in a scope that doesn't exist,
+-- or at a position that doesn't exist in that scope.
+--
+-- @since 1.2.0
+boundTyVar ::
+  forall (m :: Type -> Type).
+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  DeBruijn ->
+  Index "tyvar" ->
+  m BoundTyVar
+boundTyVar scope index = do
+  let scopeAsInt = review asInt scope
+      indexAsWord :: Word32
+      indexAsWord = fromIntegral $ review intIndex index
+  tyVarInScope <-
+    asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % _1)) >>= \case
+      Nothing -> pure False
+      Just varsBoundAtScope ->
+        -- varsBoundAtScope is the count of the CompT binding context verbatim
+        if varsBoundAtScope <= 0
+          then pure False
+          else pure $ indexAsWord < varsBoundAtScope
+  if tyVarInScope
+    then pure (BoundTyVar scope index)
+    else throwError $ OutOfScopeTyVar scope index
+
+-- To avoid annoying code duplication
+
+-- Helper to avoid having to manually catch and rethrow the error
+undoRenameM ::
+  forall (m :: Type -> Type).
+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  ValT Renamed ->
+  m (ValT AbstractTy)
+undoRenameM val = do
+  scope <- asks (fmap fst . view (#scopeInfo % #argumentInfo))
+  case undoRename scope val of
+    Left err' -> throwError $ UndoRenameFailure err'
+    Right renamed -> pure renamed
+
+askScope ::
+  forall (m :: Type -> Type).
+  (MonadReader ASGEnv m) =>
+  m (Vector Word32)
+askScope = asks (fmap fst . view (#scopeInfo % #argumentInfo))
+
+-- Runs a UnifyM computation in our abstract monad. Again, largely to avoid superfluous code
+-- duplication.
+liftUnifyM ::
+  forall (m :: Type -> Type) (a :: Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  UnifyM a ->
+  m a
+liftUnifyM act = do
+  tyDict <- asks (view #datatypeInfo)
+  case runUnifyM tyDict act of
+    Left e -> throwError $ UnificationError e
+    Right res -> pure res
+
+-- Utility functions for ASG construction. These are not strictly necessary, but are extremely convenient.
+
+-- | Constructs a datatype value at given constructor. This is different to
+-- 'dataConstructor', as it doesn't produce a thunk.
+--
+-- The third argument is a 'Vector' of values to \'fill in\' all the fields
+-- required by the stated constructor. The fourth argument is a 'Vector' of
+-- \'type instantiations\', which allow \'concretification\' of any lingering
+-- polymorphic type variables which are not determined by the field values given
+-- as the third argument.
+--
+-- = Example
+--
+-- Consider @Left 3@. In this case, the field only determines the first type
+-- argument to the @Either@ data type, and if we used 'dataConstructor', we
+-- would be left with a thunk of type @<forall a . !Either Integer a>@. Using
+-- 'ctor', we can immediately specify what @a@ should be, and unwrap the thunk.
+--
+-- @since 1.2.0
+ctor ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  TyName ->
+  ConstructorName ->
+  Vector.Vector Ref ->
+  Vector.Vector (Wedge BoundTyVar (ValT Void)) ->
+  m Id
+ctor tn cn args instTys = do
+  dataThunk <- dataConstructor tn cn args
+  dataForced <- force (AnId dataThunk)
+  app dataForced mempty instTys
+
+-- | As 'lam', but produces a thunk value instead of a computation.
+--
+-- @since 1.2.0
+lazyLam ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  CompT AbstractTy ->
+  m Ref ->
+  m Id
+lazyLam expected bodyComp = lam expected bodyComp >>= thunk
+
+-- | Helper to avoid using 'Vector.fromList' when defining data types.
+--
+-- @since 1.2.0
+dtype :: TyName -> [ValT AbstractTy] -> ValT AbstractTy
+dtype tn = Datatype tn . Vector.fromList
diff --git a/src/Covenant/Data.hs b/src/Covenant/Data.hs
--- a/src/Covenant/Data.hs
+++ b/src/Covenant/Data.hs
@@ -35,6 +35,7 @@
     isRecursiveChildOf,
     hasRecursive,
     everythingOf,
+    mapValT,
   )
 where
 
diff --git a/src/Covenant/Index.hs b/src/Covenant/Index.hs
--- a/src/Covenant/Index.hs
+++ b/src/Covenant/Index.hs
@@ -22,6 +22,7 @@
     count2,
     ix3,
     count3,
+    wordCount,
   )
 where
 
@@ -31,6 +32,7 @@
 import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum))
 import Data.Word (Word32)
 import GHC.TypeLits (Symbol)
+import Optics.Core (Lens', lens)
 import Optics.Prism (Prism', prism)
 import Test.QuickCheck (Arbitrary)
 
@@ -146,6 +148,11 @@
   prism
     (fromIntegral . coerce @_ @Word32)
     (\i -> maybe (Left i) (Right . Count) . toIntegralSized $ i)
+
+-- | We use the Word32 directly during renaming, and a Lens is more appropriate
+-- than a Prism if we're working with Word32s
+wordCount :: forall (ofWhat :: Symbol). Lens' (Count ofWhat) Word32
+wordCount = lens (\(Count x) -> x) (\_ w -> Count w)
 
 -- | Helper for a count of zero items.
 --
diff --git a/src/Covenant/Internal/KindCheck.hs b/src/Covenant/Internal/KindCheck.hs
--- a/src/Covenant/Internal/KindCheck.hs
+++ b/src/Covenant/Internal/KindCheck.hs
@@ -186,8 +186,18 @@
 
 -}
 
--- First arg is the name of the type constructor w/ a bad argument, second arg is the bad argument.
-data EncodingArgErr a = EncodingArgMismatch TyName (ValT a)
+-- | Indicates that we tried to instantiate a polymorphic data type using a type
+-- whose encoding is incompatible. The most common case of this is when we have
+-- a \'polymorphic\' data type that uses some kind of @Data@ encoding and we try
+-- to instantiate it with a type which has a SOP encoding.
+--
+-- @since 1.2.0
+data EncodingArgErr a
+  = -- | First field is a constructor name for the type we tried to instantiate,
+    -- second field is the bad instantiator.
+    --
+    -- @since 1.2.0
+    EncodingArgMismatch TyName (ValT a)
   deriving stock (Show, Eq)
 
 -- | Verifies that a datatype (third argument) is valid according to its stated
diff --git a/src/Covenant/Internal/Rename.hs b/src/Covenant/Internal/Rename.hs
--- a/src/Covenant/Internal/Rename.hs
+++ b/src/Covenant/Internal/Rename.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE MultiWayIf #-}
+
 module Covenant.Internal.Rename
   ( RenameM,
     RenameError (..),
@@ -7,17 +9,21 @@
     renameCompT,
     undoRename,
     renameDatatypeInfo,
+    UnRenameM,
+    UnRenameError (..),
+    runUnRenameM,
   )
 where
 
-import Control.Monad (unless)
 import Control.Monad.Except
   ( ExceptT,
+    MonadError,
     runExceptT,
     throwError,
   )
 import Control.Monad.Reader
-  ( Reader,
+  ( MonadReader,
+    Reader,
     asks,
     local,
     runReader,
@@ -29,8 +35,8 @@
     modify,
   )
 import Covenant.Data (DatatypeInfo (DatatypeInfo))
-import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
-import Covenant.Index (Count, Index, intCount, intIndex)
+import Covenant.DeBruijn (DeBruijn (Z), asInt)
+import Covenant.Index (Count, Index, intIndex, wordCount)
 import Covenant.Internal.Type
   ( AbstractTy (BoundAt),
     CompT (CompT),
@@ -43,17 +49,16 @@
 import Data.Bitraversable (Bitraversable (bitraverse))
 import Data.Coerce (coerce)
 import Data.Kind (Type)
-import Data.Tuple.Optics (_1)
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Data.Vector.NonEmpty qualified as NonEmpty
-import Data.Word (Word64)
+import Data.Word (Word32, Word64)
 import Optics.Core
   ( A_Lens,
     LabelOptic (labelOptic),
-    ix,
     lens,
     over,
+    preview,
     review,
     set,
     to,
@@ -62,12 +67,14 @@
   )
 
 -- Used during renaming. Contains a source of fresh indices for wildcards, as
--- well as tracking:
+-- well as:
 --
--- 1. How many variables are bound by each scope;
--- 2. Which of these variables have been noted as used; and
--- 3. A unique identifier for each scope (for wildcards).
-data RenameState = RenameState Word64 (Vector (Vector Bool, Word64))
+-- 1. The first Word64 argument is the "source of freshness" for WildCards
+-- 2. The second Word64 argument is the inherited scope size
+-- 3. The *size* of the vector tracks the current scope size (the enclosing scope is inherited, but it may grow during renaming)
+-- 4. The first element of the tuple in the vector is the *count* of TyVars bound in each scope. (Note: It is therefore 1 greater than the index)
+-- 5. The second element of the tuple in the vector is the unique identifier for wildcards in each scope.
+data RenameState = RenameState Word64 Word32 (Vector (Word32, Word64))
   deriving stock (Eq, Show)
 
 -- Note (Koz, 11/04/2025): We need this field as a source of unique identifiers
@@ -94,35 +101,65 @@
   {-# INLINEABLE labelOptic #-}
   labelOptic =
     lens
-      (\(RenameState x _) -> x)
-      (\(RenameState _ y) x' -> RenameState x' y)
+      (\(RenameState x _ _) -> x)
+      (\(RenameState _ b c) a' -> RenameState a' b c)
 
--- The 'outer' vector represents a stack of scopes. Each entry is a combination
--- of a vector of used variables (length is equal to the number of variables
--- bound by that scope), together with a unique identifier not only for that
--- scope, but also the `step` into that scope, as required by wildcard renaming.
 instance
-  (k ~ A_Lens, a ~ Vector (Vector Bool, Word64), b ~ Vector (Vector Bool, Word64)) =>
+  (k ~ A_Lens, a ~ Word32, b ~ Word32) =>
+  LabelOptic "inheritedScope" k RenameState RenameState a b
+  where
+  {-# INLINEABLE labelOptic #-}
+  labelOptic =
+    lens
+      (\(RenameState _ x _) -> x)
+      (\(RenameState a _ c) b' -> RenameState a b' c)
+
+instance
+  (k ~ A_Lens, a ~ Vector (Word32, Word64), b ~ Vector (Word32, Word64)) =>
   LabelOptic "tracker" k RenameState RenameState a b
   where
   {-# INLINEABLE labelOptic #-}
   labelOptic =
     lens
-      (\(RenameState _ y) -> y)
-      (\(RenameState x _) y' -> RenameState x y')
+      (\(RenameState _ _ y) -> y)
+      (\(RenameState x y _) z' -> RenameState x y z')
 
 -- | Ways in which the renamer can fail.
 --
 -- @since 1.1.0
 data RenameError
   = -- | An attempt to reference an abstraction in a scope where this
-    -- abstraction doesn't exist. First field is the true level, second is
-    -- the index that was requested.
+    -- abstraction doesn't exist, but where the scope itself /does/ exist.
+    -- Put another way: This gets thrown when the argument index of an
+    -- abstraction inconsistent with the `Count` of the scope its DB index refers to.
+    -- First field is the true level, second is the index that was requested.
     --
-    -- @since 1.0.0
+    -- @since 1.2.0
     InvalidAbstractionReference Int (Index "tyvar")
+  | -- | An abstraction refers to a scope which does not exist. That is: The abstraction's
+    -- DeBruijn index points to a scope "higher than" the top-level scope.
+    --
+    -- @since 1.2.0
+    InvalidScopeReference Int (Index "tyvar")
   deriving stock (Eq, Show)
 
+-- | Ways in which the un-renamer can fail.
+--
+-- @since 1.2.0
+data UnRenameError
+  = -- | We tried to un-rename a wildcard. This means something has gone very wrong internally.
+    -- @since 1.2.0
+    UnRenameWildCard Renamed
+  | -- | We received a negative DeBruijn in our true level calculation. This is impossible, and indicates another
+    --   internal malfunction or bug
+    NegativeDeBruijn Int
+  deriving stock
+    ( -- | @since 1.2.0
+      Eq,
+      -- | @since 1.2.0
+      Show
+    )
+
 -- | A \'renaming monad\' which allows us to convert type representations from
 -- ones that use /relative/ abstraction labelling to /absolute/ abstraction
 -- labelling.
@@ -156,15 +193,74 @@
     )
     via (ExceptT RenameError (State RenameState))
 
+-- | The portions of the RenameState needed for unrenaming. Lacks the unique indicator for
+-- wildcards, since trying to un-rename a wildcard is an error.
+data UnRenameCxt = UnRenameCxt Word32 (Vector Word32)
+  deriving stock
+    ( -- @since 1.2.0
+      Show,
+      -- @since 1.2.0
+      Eq,
+      -- @since 1.2.0
+      Ord
+    )
+
+instance
+  (k ~ A_Lens, a ~ Word32, b ~ Word32) =>
+  LabelOptic "inheritedScopeSize" k UnRenameCxt UnRenameCxt a b
+  where
+  {-# INLINEABLE labelOptic #-}
+  labelOptic =
+    lens
+      (\(UnRenameCxt x _) -> x)
+      (\(UnRenameCxt _ y) x' -> UnRenameCxt x' y)
+
+instance
+  (k ~ A_Lens, a ~ Vector Word32, b ~ Vector Word32) =>
+  LabelOptic "scopeInfo" k UnRenameCxt UnRenameCxt a b
+  where
+  {-# INLINEABLE labelOptic #-}
+  labelOptic =
+    lens
+      (\(UnRenameCxt _ y) -> y)
+      (\(UnRenameCxt x _) y' -> UnRenameCxt x y')
+
+-- | @since 1.2.0
+newtype UnRenameM (a :: Type) = UnRenameM (ExceptT UnRenameError (Reader UnRenameCxt) a)
+  deriving
+    ( -- | @since 1.2.0
+      Functor,
+      -- | @since 1.2.0
+      Applicative,
+      -- | @since 1.2.0
+      Monad,
+      -- | @since 1.2.0
+      MonadReader UnRenameCxt,
+      -- | @since 1.2.0
+      MonadError UnRenameError
+    )
+    via (ExceptT UnRenameError (Reader UnRenameCxt))
+
 -- | Execute a renaming computation.
 --
--- @since 1.0.0
+-- @since 1.2.0
 runRenameM ::
   forall (a :: Type).
+  Vector Word32 ->
   RenameM a ->
   Either RenameError a
-runRenameM (RenameM comp) = evalState (runExceptT comp) . RenameState 0 $ Vector.empty
+runRenameM scopeInfo (RenameM comp) =
+  evalState (runExceptT comp)
+    . RenameState 0 (fromIntegral $ Vector.length scopeInfo)
+    $ Vector.map (,0) scopeInfo
 
+runUnRenameM ::
+  forall (a :: Type).
+  UnRenameM a ->
+  Vector Word32 ->
+  Either UnRenameError a
+runUnRenameM (UnRenameM comp) inherited = runReader (runExceptT comp) $ UnRenameCxt (fromIntegral $ Vector.length inherited) inherited
+
 -- | Rename a computation type.
 --
 -- @since 1.0.0
@@ -211,8 +307,10 @@
     renameCtor :: Constructor AbstractTy -> RenameM (Constructor Renamed)
     renameCtor (Constructor cn args) = Constructor cn <$> traverse renameValT args
 
+-- REVIEW: I am not sure if we really want the scope arg to runRenameM to be `mempty`.
+--         If something breaks w/ BB forms or datatypes, look here.
 renameDatatypeInfo :: DatatypeInfo AbstractTy -> Either RenameError (DatatypeInfo Renamed)
-renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM $ do
+renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM mempty $ do
   ogDecl' <- renameDataDecl ogDecl
   baseFStuff' <- traverse (bitraverse renameDataDecl renameValT) baseFStuff
   bb' <- traverse renameValT bb
@@ -221,60 +319,65 @@
 -- A way of 'undoing' the renaming process. This is meant to be used only after
 -- applications, and assumes that what is being un-renamed is the result of a
 -- computation.
-undoRename :: ValT Renamed -> ValT AbstractTy
-undoRename t = runReader (go t) 1
+--
+-- @since 1.2.0
+undoRename :: Vector Word32 -> ValT Renamed -> Either UnRenameError (ValT AbstractTy)
+undoRename scope t = runUnRenameM (go t) scope
   where
-    go :: ValT Renamed -> Reader Int (ValT AbstractTy)
+    go :: ValT Renamed -> UnRenameM (ValT AbstractTy)
     go = \case
       Abstraction t' ->
         Abstraction <$> case t' of
-          Unifiable index -> BoundAt <$> trueLevelToDB 1 <*> pure index
-          Rigid trueLevel index -> BoundAt <$> trueLevelToDB trueLevel <*> pure index
-          Wildcard _ trueLevel index -> BoundAt <$> trueLevelToDB trueLevel <*> pure index
+          Rigid trueLevel index -> do
+            db <- unTrueLevel trueLevel
+            pure $ BoundAt db index
+          w@(Wildcard {}) -> throwError $ UnRenameWildCard w
+          Unifiable index -> pure $ BoundAt Z index
       ThunkT (CompT abses (CompTBody xs)) ->
-        ThunkT . CompT abses . CompTBody <$> local (+ 1) (traverse go xs)
+        ThunkT
+          . CompT abses
+          . CompTBody
+          <$> local (over #scopeInfo (Vector.cons $ view wordCount abses)) (traverse go xs)
       BuiltinFlat t' -> pure . BuiltinFlat $ t'
       Datatype tn args -> Datatype tn <$> traverse go args
 
--- Helpers
-
-trueLevelToDB :: Int -> Reader Int DeBruijn
-trueLevelToDB trueLevel = asks (go . subtract trueLevel)
-  where
-    go :: Int -> DeBruijn
-    go = \case
-      0 -> Z
-      n -> S . go $ n - 1
+    unTrueLevel :: Int -> UnRenameM DeBruijn
+    unTrueLevel tl = do
+      trackerLen <- asks (Vector.length . view #scopeInfo)
+      inheritedSize <- asks (fromIntegral . view #inheritedScopeSize)
+      let db = trackerLen - 1 - inheritedSize - tl
+      case preview asInt db of
+        Nothing -> throwError $ NegativeDeBruijn db
+        Just res -> pure res
 
 renameAbstraction :: AbstractTy -> RenameM Renamed
 renameAbstraction (BoundAt scope index) = RenameM $ do
-  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - review asInt scope)
+  inheritedScopeSize <- gets (fromIntegral . view #inheritedScope)
+  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - 1 - inheritedScopeSize - review asInt scope)
   scopeInfo <- gets (\x -> view #tracker x Vector.!? review asInt scope)
   let asIntIx = review intIndex index
   case scopeInfo of
-    -- This variable is bound in a scope that encloses the renaming scope. Thus,
-    -- the variable is rigid.
-    Nothing -> pure . Rigid trueLevel $ index
-    Just (occursTracker, uniqueScopeId) -> case occursTracker Vector.!? asIntIx of
-      Nothing -> throwError . InvalidAbstractionReference trueLevel $ index
-      Just beenUsed -> do
-        -- Note that this variable has occurred
-        unless beenUsed (modify (noteUsed scope index))
-        pure $
-          if trueLevel == 1
-            -- This is a unifiable variable
-            then Unifiable index
-            -- This is a wildcard variable
-            else Wildcard uniqueScopeId trueLevel index
+    Nothing -> throwError . InvalidScopeReference trueLevel $ index
+    Just (occursTracker, uniqueScopeId) ->
+      if
+        | not (checkVarIxExists asIntIx occursTracker) -> throwError . InvalidAbstractionReference trueLevel $ index
+        | trueLevel == 0 -> pure $ Unifiable index
+        | trueLevel < 0 -> pure $ Rigid trueLevel index
+        | otherwise -> pure $ Wildcard uniqueScopeId trueLevel index
+  where
+    checkVarIxExists :: Int -> Word32 -> Bool
+    checkVarIxExists i wCount = fromIntegral i < wCount
 
+-- Helpers
+
 -- Given a number of abstractions bound by a scope, modify the state to track
 -- that scope.
 stepUpScope :: Count "tyvar" -> RenameState -> RenameState
 stepUpScope abses x =
   let fresh = view #idSource x
-      absesI = review intCount abses
+      absesW = view wordCount abses
       -- Label (speculatively) the current scope 'step' with a unique value.
-      entry = (Vector.replicate absesI False, fresh)
+      entry = (absesW, fresh)
    in -- Ensure that our source of fresh identifiers is incremented
       over #tracker (Vector.cons entry) . set #idSource (fresh + 1) $ x
 
@@ -286,9 +389,3 @@
 -- achieve our goal of renaming wildcards.
 dropDownScope :: RenameState -> RenameState
 dropDownScope = over #tracker Vector.tail
-
--- Given a pair of DeBruijn index and positional index for a variable, note that
--- we've seen this variable.
-noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState
-noteUsed scope index =
-  set (#tracker % ix (review asInt scope) % _1 % ix (review intIndex index)) True
diff --git a/src/Covenant/Internal/Term.hs b/src/Covenant/Internal/Term.hs
--- a/src/Covenant/Internal/Term.hs
+++ b/src/Covenant/Internal/Term.hs
@@ -20,11 +20,19 @@
 import Covenant.DeBruijn (DeBruijn)
 import Covenant.Index (Index)
 import Covenant.Internal.KindCheck (EncodingArgErr)
-import Covenant.Internal.Rename (RenameError)
-import Covenant.Internal.Type (AbstractTy, CompT, ValT)
+import Covenant.Internal.Rename (RenameError, UnRenameError)
+import Covenant.Internal.Type
+  ( AbstractTy,
+    BuiltinFlatT,
+    CompT,
+    TyName,
+    ValT,
+  )
 import Covenant.Internal.Unification (TypeAppError)
 import Covenant.Prim (OneArgFunc, SixArgFunc, ThreeArgFunc, TwoArgFunc)
+import Covenant.Type (ConstructorName, PlutusDataConstructor, Renamed)
 import Data.Kind (Type)
+import Data.Set qualified as Set
 import Data.Vector (Vector)
 import Data.Word (Word64)
 
@@ -94,8 +102,8 @@
     ReturnCompType (CompT AbstractTy)
   | -- | The body of a lambda results in a value-typed node, which isn't allowed.
     --
-    -- @since 1.0.0
-    LambdaResultsInValType (ValT AbstractTy)
+    -- @since 1.2.0
+    LambdaResultsInCompType (CompT AbstractTy)
   | -- | The body of a lambda results in a computation-typed node which isn't
     -- a return, which isn't allowed.
     --
@@ -118,10 +126,141 @@
     --
     -- @since 1.0.0
     WrongReturnType (ValT AbstractTy) (ValT AbstractTy)
-  | -- @since 1.1.0
-
-    -- | Wraps an encoding argument mismatch error from KindCheck
+  | -- | Wraps an encoding argument mismatch error from KindCheck
+    --
+    -- @since 1.1.0
     EncodingError (EncodingArgErr AbstractTy)
+  | -- | The first argument to a catamorphism wasn't an algebra, as
+    -- it had the wrong arity.
+    --
+    -- @since 1.2.0
+    CataAlgebraWrongArity Int
+  | -- | The first argument to a catamorphism wasn't an algebra.
+    --
+    -- @since 1.1.0
+    CataNotAnAlgebra ASGNodeType
+  | -- | The second argument to a catamorphism wasn't a value type.
+    --
+    -- @since 1.1.0
+    CataApplyToNonValT ASGNodeType
+  | -- The algebra given to this catamorphism is not rigid (that is, its
+    -- computation type binds variables).
+    --
+    -- @since 1.2.0
+    CataNonRigidAlgebra (CompT AbstractTy)
+  | -- | The second argument to a catamorphism is a builtin type, but not one
+    -- we can eliminate with a catamorphism.
+    --
+    -- @since 1.1.0
+    CataWrongBuiltinType BuiltinFlatT
+  | -- | The second argument to a catamorphism is a value type, but not one we
+    -- can eliminate with a catamorphism. Usually, this means it's a variable.
+    --
+    -- @since 1.1.0
+    CataWrongValT (ValT AbstractTy)
+  | -- | We requested a catamorphism for a type that doesn't exist.
+    --
+    -- @since 1.2.0
+    CataNoSuchType TyName
+  | -- | We requested a catamorphism for a type without a base functor.
+    --
+    -- @since 1.2.0
+    CataNoBaseFunctorForType TyName
+  | -- | The provided algebra is not suitable for the given type.
+    --
+    -- @since 1.1.0
+    CataUnsuitable (CompT AbstractTy) (ValT AbstractTy)
+  | -- | Someone attempted to construct a tyvar using a DB index or argument position
+    --   which refers to a scope (or argument) that does not exist.
+    --
+    -- @since 1.2.0
+    OutOfScopeTyVar DeBruijn (Index "tyvar")
+  | -- | We failed to rename an "instantiation type" supplied to 'Covenant.ASG.app'.
+    --
+    -- @since 1.2.0
+    FailedToRenameInstantiation RenameError
+  | -- | Un-renaming failed.
+    --
+    -- @since 1.2.0
+    UndoRenameFailure UnRenameError
+  | -- | We tried to look up the 'DatatypeInfo' corresponding to a 'TyName' and came up empty handed.
+    --
+    -- @since 1.2.0
+    TypeDoesNotExist TyName
+  | -- | We tried to rename a 'DatatypeInfo' and failed.
+    --
+    -- @since 1.2.0
+    DatatypeInfoRenameError RenameError
+  | -- | We tried to look up a constructor for a given type. The type exists, but the constructor does not.
+    --
+    -- @since 1.2.0
+    ConstructorDoesNotExistForType TyName ConstructorName
+  | -- | When using the helper function to construct an introduction form, the type and constructor exist but the
+    --   number of fields provided as an argument does not match the number of declared fields.
+    --   The 'Int' is the /incorrect/ number of /supplied/ fields.
+    --
+    -- @since 1.2.0
+    IntroFormWrongNumArgs TyName ConstructorName Int
+  | -- | The user passed an error node as an argument to a datatype into form. We return the arguments given
+    --   to 'Covenant.ASG.dataConstructor' in the error.
+    --
+    -- @since 1.2.0
+    IntroFormErrorNodeField TyName ConstructorName (Vector Ref)
+  | -- | The user tried to construct an introduction form using a Plutus @Data@ constructor not found in the
+    --   opaque datatype declaration.
+    --
+    -- @since 1.2.0
+    UndeclaredOpaquePlutusDataCtor (Set.Set PlutusDataConstructor) ConstructorName
+  | -- | The user tried to construct an introduction form with a valid Plutus @Data@ constructor, but
+    --   supplied a 'Covenant.ASG.Ref' to a field of the wrong type.
+    --
+    -- @since 1.2.0
+    InvalidOpaqueField (Set.Set PlutusDataConstructor) ConstructorName [ValT Renamed]
+  | -- The user tried to match on (i.e. use as a scrutinee) a node that wasn't a value.
+    --
+    -- @since 1.2.0
+    MatchNonValTy ASGNodeType
+  | -- | Internal error: we found a base functor Boehm-Berrarducci form that isn't a thunk after instantiation
+    --   during pattern matching.Somehow we got a BFBB that is something other than a thunk after instantiation during pattern matching.
+    --
+    --   This should not normally happen: let us know if you see this error!
+    --
+    -- @since 1.2.0
+    MatchNonThunkBBF (ValT Renamed)
+  | -- | We encountered a rename error during pattern matching. This will refer
+    -- to either the Boehm-Berrarducci form, or the base functor Boehm-Berrarducci form, depending on what type we tried to match.
+    --
+    -- @since 1.2.0
+    MatchRenameBBFail RenameError
+  | -- | This indicates that we encountered an error when renaming the arguments to the type constructor of the
+    --   /scrutinee type/ during pattern matching. That is, if we're matching on @Either a b@, this means that
+    --   either @a@ or @b@ failed to rename.
+    --
+    --  This should not normally happen: let us know if you see this error!
+    --
+    -- @since 1.2.0
+    MatchRenameTyConArgFail RenameError
+  | -- | A user tried to use a polymorphic handler in a pattern match, which is not currently allowed.
+    --
+    -- @since 1.2.0
+    MatchPolymorphicHandler (ValT Renamed)
+  | -- | We tried to use an error node as a pattern match handler.
+    --
+    -- @since 1.2.0
+    MatchErrorAsHandler Ref
+  | -- | The non-recursive branch of a pattern match needs a Boehm-Berrarducci form for the given type
+    -- name, but it doesn't exist.
+    --
+    -- @since 1.2.0
+    MatchNoBBForm TyName
+  | -- | Someone tried to match on something that isn't a datatype.
+    --
+    -- @since 1.2.0
+    MatchNonDatatypeScrutinee (ValT AbstractTy)
+  | -- | The scrutinee is a datatype, be don't have it in our datatype dictionary.
+    --
+    -- @since 1.2.0
+    MatchNoDatatypeInfo TyName
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -219,9 +358,8 @@
   | Builtin2Internal TwoArgFunc
   | Builtin3Internal ThreeArgFunc
   | Builtin6Internal SixArgFunc
-  | LamInternal Id
+  | LamInternal Ref
   | ForceInternal Ref
-  | ReturnInternal Ref
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -238,6 +376,12 @@
   = LitInternal AConstant
   | AppInternal Id (Vector Ref)
   | ThunkInternal Id
+  | -- | @since 1.1.0
+    CataInternal Ref Ref
+  | -- | @since 1.2.0
+    DataConstructorInternal TyName ConstructorName (Vector Ref)
+  | -- | @since 1.2.0
+    MatchInternal Ref (Vector Ref)
   deriving stock
     ( -- | @since 1.0.0
       Eq,
diff --git a/src/Covenant/Internal/Type.hs b/src/Covenant/Internal/Type.hs
--- a/src/Covenant/Internal/Type.hs
+++ b/src/Covenant/Internal/Type.hs
@@ -21,6 +21,7 @@
     naturalBaseFunctor,
     negativeBaseFunctor,
     byteStringBaseFunctor,
+    arity,
   )
 where
 
@@ -158,7 +159,9 @@
       -- | @since 1.0.0
       Ord,
       -- | @since 1.0.0
-      Show
+      Show,
+      -- | @since 1.2.0
+      Functor
     )
 
 -- | @since 1.0.0
@@ -179,7 +182,9 @@
       -- | @since 1.0.0
       Ord,
       -- | @since 1.0.0
-      Show
+      Show,
+      -- | @since 1.2.0
+      Functor
     )
 
 -- | @since 1.0.0
@@ -192,6 +197,13 @@
 instance Pretty (CompT Renamed) where
   pretty = runPrettyM . prettyCompTWithContext
 
+-- | Determine the arity of a computation type: that is, how many arguments a
+-- function of this type must be given.
+--
+-- @since 1.0.0
+arity :: forall (a :: Type). CompT a -> Int
+arity (CompT _ (CompTBody xs)) = NonEmpty.length xs - 1
+
 -- | The name of a data type. This refers specifically to non-\'flat\' types
 -- either provided by the ledger, or defined by the user.
 --
@@ -230,7 +242,9 @@
       -- | @since 1.0.0
       Ord,
       -- | @since 1.0.0
-      Show
+      Show,
+      -- | @since 1.2.0
+      Functor
     )
 
 -- | @since 1.0.0
diff --git a/src/Covenant/Internal/Unification.hs b/src/Covenant/Internal/Unification.hs
--- a/src/Covenant/Internal/Unification.hs
+++ b/src/Covenant/Internal/Unification.hs
@@ -1,10 +1,16 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE MultiWayIf #-}
 
 module Covenant.Internal.Unification
   ( TypeAppError (..),
     checkApp,
     runUnifyM,
     UnifyM,
+    -- These are exported for use with ASG helpers, largely (but not exclusively) the intro forms helper
+    unify,
+    substitute,
+    fixUp,
+    reconcile,
   )
 where
 
@@ -15,7 +21,7 @@
 #endif
 import Control.Monad.Except (MonadError, catchError, throwError)
 import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask)
-import Covenant.Data (DatatypeInfo)
+import Covenant.Data (DatatypeInfo, mkDatatypeInfo)
 import Covenant.Index (Index, intCount, intIndex)
 import Covenant.Internal.Rename (RenameError, renameDatatypeInfo)
 import Covenant.Internal.Type
@@ -24,8 +30,11 @@
     CompT (CompT),
     CompTBody (CompTBody),
     Renamed (Rigid, Unifiable, Wildcard),
-    TyName,
+    TyName (TyName),
     ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
+    byteStringBaseFunctor,
+    naturalBaseFunctor,
+    negativeBaseFunctor,
   )
 import Data.Kind (Type)
 import Data.Map (Map)
@@ -35,6 +44,7 @@
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
+import Data.Text qualified as Text
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Data.Vector.NonEmpty (NonEmptyVector)
@@ -76,6 +86,9 @@
     --
     -- @since 1.1.0
     ImpossibleHappened Text
+  | -- Could not reconcile two assignments with the same index
+    -- @since 1.2.0
+    CouldNotReconcile (Index "tyvar") (ValT Renamed) (ValT Renamed)
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -101,10 +114,42 @@
 lookupDatatypeInfo ::
   TyName ->
   UnifyM (DatatypeInfo Renamed)
-lookupDatatypeInfo tn =
+lookupDatatypeInfo tn@(TyName rawTyName) =
   ask >>= \tyDict -> case preview (ix tn) tyDict of
-    Nothing -> throwError $ NoDatatypeInfo tn
-    Just dti -> either (throwError . DatatypeInfoRenameFailed tn) pure $ renameDatatypeInfo dti
+    Nothing -> checkForBaseFunctor tyDict
+    Just dti -> renamedToUnify . renameDatatypeInfo $ dti
+  where
+    checkForBaseFunctor :: Map TyName (DatatypeInfo AbstractTy) -> UnifyM (DatatypeInfo Renamed)
+    checkForBaseFunctor tyDict = case Text.stripSuffix "_F" rawTyName of
+      Nothing -> throwError . NoDatatypeInfo $ tn
+      Just rawTyNameStub ->
+        if
+          -- Note (Koz, 12/08/2025): None of these specific cases should _ever_
+          -- fail. Thus, `fromRight` is safe here.
+          | rawTyNameStub == "Natural" ->
+              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ naturalBaseFunctor
+          | rawTyNameStub == "Negative" ->
+              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ negativeBaseFunctor
+          | rawTyNameStub == "ByteString" ->
+              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ byteStringBaseFunctor
+          -- We have something that _looks_ like a base functor, but not a
+          -- special builtin case. We thus need to ask the environment for the
+          -- recursive type it stands for, if it exists.
+          | otherwise -> do
+              let standinTyName = TyName rawTyNameStub
+              case preview (ix standinTyName) tyDict of
+                -- Now we have _truly_ missed.
+                Nothing -> throwError . NoDatatypeInfo $ tn
+                Just dti -> case view #baseFunctor dti of
+                  Nothing -> throwError . NoDatatypeInfo $ tn
+                  -- Since this is generated, it can't fail to rename
+                  Just (bfDd, _) -> renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ bfDd
+    renamedToUnify :: Either RenameError (DatatypeInfo Renamed) -> UnifyM (DatatypeInfo Renamed)
+    renamedToUnify = either (throwError . DatatypeInfoRenameFailed tn) pure
+    fromRight :: forall a b. (Show a) => Either a b -> b
+    fromRight = \case
+      Left err -> error . show $ err
+      Right x -> x
 
 lookupBBForm :: TyName -> UnifyM (ValT Renamed)
 lookupBBForm tn =
@@ -210,8 +255,6 @@
 
 fixUp :: ValT Renamed -> UnifyM (ValT Renamed)
 fixUp = \case
-  -- We have a result that's effectively `forall a . a` but not an error
-  Abstraction (Unifiable index) -> throwError . LeakingUnifiable $ index
   -- We're doing the equivalent of failing the `ST` trick
   Abstraction (Wildcard scopeId trueLevel index) -> throwError . LeakingWildcard scopeId trueLevel $ index
   -- We may have a result with fewer unifiables than we started with
@@ -344,28 +387,30 @@
         go :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed
         go subs arg = foldl' (\val (i, concrete) -> substitute i concrete val) arg subs
     concretify _ _ = throwError $ ImpossibleHappened "bbForm is not a thunk"
-    reconcile ::
-      Map (Index "tyvar") (ValT Renamed) ->
-      Map (Index "tyvar") (ValT Renamed) ->
-      UnifyM (Map (Index "tyvar") (ValT Renamed))
-    -- Note (Koz, 14/04/2025): This utter soup means the following:
-    --
-    -- - If the old map and the new map don't have any overlapping assignments,
-    --   just union them.
-    -- - Otherwise, for any assignment to a unifiable that is present in both
-    --   maps, ensure they assign to the same thing; if they do, it's fine,
-    --   otherwise we have a problem.
-    reconcile =
-      Merge.mergeA
-        Merge.preserveMissing
-        Merge.preserveMissing
-        (Merge.zipWithAMatched combineBindings)
+
+reconcile ::
+  Map (Index "tyvar") (ValT Renamed) ->
+  Map (Index "tyvar") (ValT Renamed) ->
+  UnifyM (Map (Index "tyvar") (ValT Renamed))
+-- Note (Koz, 14/04/2025): This utter soup means the following:
+--
+-- - If the old map and the new map don't have any overlapping assignments,
+--   just union them.
+-- - Otherwise, for any assignment to a unifiable that is present in both
+--   maps, ensure they assign to the same thing; if they do, it's fine,
+--   otherwise we have a problem.
+reconcile =
+  Merge.mergeA
+    Merge.preserveMissing
+    Merge.preserveMissing
+    (Merge.zipWithAMatched combineBindings)
+  where
     combineBindings :: Index "tyvar" -> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed)
-    combineBindings _ old new =
+    combineBindings i old new =
       if old == new
         then pure old
         else case old of
           Abstraction (Unifiable _) -> pure new
           _ -> case new of
             Abstraction (Unifiable _) -> pure old
-            _ -> unificationError
+            _ -> throwError $ CouldNotReconcile i old new
diff --git a/src/Covenant/Test.hs b/src/Covenant/Test.hs
--- a/src/Covenant/Test.hs
+++ b/src/Covenant/Test.hs
@@ -57,6 +57,12 @@
 
     -- *** Elimination
     runRenameM,
+    undoRename,
+
+    -- ** ASG
+    DebugASGBuilder (..),
+    debugASGBuilder,
+    typeIdTest,
   )
 where
 
@@ -65,6 +71,9 @@
 #endif
 import Control.Applicative ((<|>))
 import Control.Monad (void)
+import Control.Monad.Error.Class (MonadError)
+import Control.Monad.HashCons (HashConsT, MonadHashCons, runHashConsT)
+import Control.Monad.Reader (MonadReader, ReaderT, runReaderT)
 import Control.Monad.State.Strict
   ( MonadState (get, put),
     State,
@@ -73,6 +82,8 @@
     modify,
   )
 import Control.Monad.Trans (MonadTrans (lift))
+import Control.Monad.Trans.Except (ExceptT, runExceptT)
+import Covenant.ASG (ASGEnv (ASGEnv), ASGNode, CovenantError (TypeError), CovenantTypeError, Id, ScopeInfo (ScopeInfo))
 import Covenant.Data
   ( DatatypeInfo,
     mkDatatypeInfo,
@@ -106,17 +117,19 @@
   )
 import Covenant.Internal.PrettyPrint (ScopeBoundary)
 import Covenant.Internal.Rename
-  ( RenameError (InvalidAbstractionReference),
+  ( RenameError (InvalidAbstractionReference, InvalidScopeReference),
     RenameM,
     renameCompT,
     renameDataDecl,
     renameValT,
     runRenameM,
+    undoRename,
   )
 import Covenant.Internal.Strategy
   ( DataEncoding (PlutusData, SOP),
     PlutusDataStrategy (ConstrData),
   )
+import Covenant.Internal.Term (ASGNodeType (CompNodeType, ValNodeType), typeId)
 import Covenant.Internal.Type
   ( AbstractTy (BoundAt),
     BuiltinFlatT
@@ -143,6 +156,7 @@
   )
 import Covenant.Util (prettyStr)
 import Data.Coerce (coerce)
+import Data.Functor.Identity (Identity (runIdentity))
 import Data.Kind (Type)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as M
@@ -325,7 +339,9 @@
 -- @since 1.1.0
 chooseInt ::
   forall (m :: Type -> Type).
-  (MonadGen m) => (Int, Int) -> m Int
+  (MonadGen m) =>
+  (Int, Int) ->
+  m Int
 chooseInt bounds = GT.liftGen $ QC.chooseInt bounds
 
 -- | The same as 'QC.scale', but lifted to work in any 'MonadGen'.
@@ -333,7 +349,10 @@
 -- @since 1.1.0
 scale ::
   forall (m :: Type -> Type) (a :: Type).
-  (MonadGen m) => (Int -> Int) -> m a -> m a
+  (MonadGen m) =>
+  (Int -> Int) ->
+  m a ->
+  m a
 scale f g = GT.sized (\n -> GT.resize (f n) g)
 
 -- | If the argument is a 'Right', pass the assertion; otherwise, fail the
@@ -828,9 +847,64 @@
 genDataList :: forall (a :: Type). DataGenM a -> Gen [a]
 genDataList = runDataGenM . GT.listOf
 
+-- ASG Stuff
+
+-- | This is a @newtype@ over 'ASGBuilder' to clearly indicate that it should be used only for testing, as it is
+-- useful to have a variant of the 'ASGBuilder' monad which has a \'runner\'.
+--
+-- @since 1.2.0
+newtype DebugASGBuilder (a :: Type)
+  = DebugASGBuilder (ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a)
+  deriving
+    ( -- | @since 1.0.0
+      Functor,
+      -- | @since 1.0.0
+      Applicative,
+      -- | @since 1.0.0
+      Monad,
+      -- | @since 1.1.0
+      MonadReader ASGEnv,
+      -- | @since 1.0.0
+      MonadError CovenantTypeError,
+      -- | @since 1.0.0
+      MonadHashCons Id ASGNode
+    )
+    via ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))
+
+-- | \'Runner\' for 'DebugASGBuilder'.
+--
+-- @since 1.2.0
+debugASGBuilder ::
+  forall (a :: Type).
+  Map TyName (DatatypeInfo AbstractTy) ->
+  DebugASGBuilder a ->
+  Either CovenantError a
+debugASGBuilder tyDict (DebugASGBuilder comp) =
+  case runIdentity . runHashConsT . runExceptT . runReaderT comp $ ASGEnv (ScopeInfo Vector.empty) tyDict of
+    (result, bm) -> case result of
+      Left err' -> Left . TypeError bm $ err'
+      Right a -> pure a
+
+-- | Looks up the type of a node, wrapping computation node types into a thunk.
+--
+-- This is /only/ for use in testing!
+--
+-- @since 1.2.0
+typeIdTest ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>
+  Id ->
+  m (ValT AbstractTy)
+typeIdTest i =
+  typeId i >>= \case
+    ValNodeType t -> pure t
+    -- FIXME: This is quick & dirty but I need it for something
+    CompNodeType t -> pure $ ThunkT t
+    other -> error $ "Expected a ValT but got: " <> show other
+
 -- For convenience. Don't remove this, necessary for efficient development on future work
 unsafeRename :: forall (a :: Type). RenameM a -> a
-unsafeRename act = case runRenameM act of
+unsafeRename act = case runRenameM mempty act of
   Left err -> error $ show err
   Right res -> res
 
@@ -855,4 +929,4 @@
       (PlutusData ConstrData)
 
 testDatatypes :: [DataDeclaration AbstractTy]
-testDatatypes = [maybeT, eitherT, unitT, pair]
+testDatatypes = [maybeT, eitherT, unitT, pair, list]
diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs
--- a/src/Covenant/Type.hs
+++ b/src/Covenant/Type.hs
@@ -105,6 +105,7 @@
     Renamed (Rigid, Unifiable, Wildcard),
     TyName (TyName),
     ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
+    arity,
   )
 import Data.Coerce (coerce)
 import Data.Kind (Type)
@@ -176,13 +177,6 @@
 {-# COMPLETE ArgsAndResult #-}
 
 {-# COMPLETE ReturnT, (:--:>) #-}
-
--- | Determine the arity of a computation type: that is, how many arguments a
--- function of this type must be given.
---
--- @since 1.0.0
-arity :: forall (a :: Type). CompT a -> Int
-arity (CompT _ (CompTBody xs)) = NonEmpty.length xs - 1
 
 -- | A computation type that does not bind any type variables. Use this like a
 -- data constructor.
diff --git a/test/asg/Main.hs b/test/asg/Main.hs
--- a/test/asg/Main.hs
+++ b/test/asg/Main.hs
@@ -1,30 +1,36 @@
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 module Main (main) where
 
 import Control.Applicative ((<|>))
-import Control.Monad (guard)
+import Control.Monad (guard, void)
 import Covenant.ASG
   ( ASG,
     ASGBuilder,
-    ASGNode (ACompNode, AValNode),
+    ASGNode (ACompNode, AValNode, AnError),
     CompNodeInfo
       ( Builtin1,
         Builtin2,
-        Builtin3,
-        Return
+        Builtin3
       ),
-    CovenantError (EmptyASG, TopLevelError, TopLevelValue, TypeError),
+    CovenantError
+      ( EmptyASG,
+        TopLevelError,
+        TopLevelValue,
+        TypeError
+      ),
     CovenantTypeError
       ( ApplyCompType,
         ApplyToError,
         ApplyToValType,
+        CataNoBaseFunctorForType,
+        CataNonRigidAlgebra,
         ForceCompType,
         ForceError,
         ForceNonThunk,
-        LambdaResultsInValType,
         NoSuchArgument,
-        ReturnCompType,
+        OutOfScopeTyVar,
         ThunkError,
         ThunkValType
       ),
@@ -33,34 +39,54 @@
     ValNodeInfo (Lit),
     app,
     arg,
+    boundTyVar,
     builtin1,
     builtin2,
     builtin3,
+    cata,
+    ctor,
+    dataConstructor,
+    defaultDatatypes,
+    dtype,
     err,
     force,
     lam,
+    lazyLam,
     lit,
-    nodeAt,
-    ret,
+    match,
     runASGBuilder,
     thunk,
     topLevelNode,
   )
-import Covenant.Constant (typeConstant)
-import Covenant.DeBruijn (DeBruijn (Z))
-import Covenant.Index (Index, intIndex, ix0)
+import Covenant.Constant
+  ( AConstant (AUnit, AnInteger),
+    typeConstant,
+  )
+import Covenant.DeBruijn (DeBruijn (S, Z))
+import Covenant.Index (Index, intIndex, ix0, ix1)
 import Covenant.Prim
   ( typeOneArgFunc,
     typeThreeArgFunc,
     typeTwoArgFunc,
   )
-import Covenant.Test (Concrete (Concrete))
+import Covenant.Test
+  ( Concrete (Concrete),
+    DebugASGBuilder,
+    debugASGBuilder,
+    tyAppTestDatatypes,
+    typeIdTest,
+  )
 import Covenant.Type
   ( AbstractTy,
-    CompT (Comp0, CompN),
-    CompTBody (ArgsAndResult, ReturnT),
-    ValT,
+    BuiltinFlatT (IntegerT, UnitT),
+    CompT (Comp0, Comp1, Comp2, CompN),
+    CompTBody (ArgsAndResult, ReturnT, (:--:>)),
+    ValT (BuiltinFlat, Datatype, ThunkT),
     arity,
+    boolT,
+    byteStringT,
+    integerT,
+    tyvar,
   )
 import Covenant.Util (pattern ConsV, pattern NilV)
 import Data.Coerce (coerce)
@@ -68,6 +94,7 @@
 import Data.Map qualified as M
 import Data.Maybe (fromJust)
 import Data.Vector qualified as Vector
+import Data.Wedge (Wedge (Here, Nowhere, There), wedgeLeft)
 import Optics.Core (preview, review)
 import Test.QuickCheck
   ( Gen,
@@ -82,8 +109,8 @@
     shrink,
     (===),
   )
-import Test.Tasty (adjustOption, defaultMain, testGroup)
-import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)
+import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup)
+import Test.Tasty.HUnit (Assertion, assertEqual, assertFailure, testCase)
 import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)
 
 main :: IO ()
@@ -97,9 +124,7 @@
       testProperty "toplevel one-arg builtin compiles and has the right type" propTopLevelBuiltin1,
       testProperty "toplevel two-arg builtin compiles and has the right type" propTopLevelBuiltin2,
       testProperty "toplevel three-arg builtin compiles and has the right type" propTopLevelBuiltin3,
-      testProperty "toplevel return compiles and has the right type" propTopLevelReturn,
       testProperty "forcing a thunk has the same type as what the thunk wraps" propForceThunk,
-      testProperty "applying zero arguments to a return has the same type as what the return wraps" propApplyReturn,
       testProperty "forcing a computation type does not compile" propForceComp,
       testProperty "forcing a non-thunk value type does not compile" propForceNonThunk,
       testProperty "thunking a value type does not compile" propThunkValType,
@@ -108,8 +133,33 @@
       testProperty "passing computations as arguments does not compile" propApplyComp,
       testProperty "requesting a non-existent argument does not compile" propNonExistentArg,
       testProperty "requesting an argument that exists compiles" propExistingArg,
-      testProperty "returning a computation from a lambda does not compile" propReturnComp,
-      testProperty "a lambda body having a value type does not compile" propLambdaValBody
+      testCase "db indices are well behaved (non-datatype case)" newLamTest1,
+      testCase "db indices are well behaved (datatype case)" newLamTest2,
+      testCase "calling down an in-scope tyvar works" boundTyVarHappy,
+      testCase "calling down an out-of-scope tyvar fails" boundTyVarShouldFail,
+      nothingIntro,
+      justConcreteIntro,
+      justRigidIntro,
+      justNothingIntro,
+      testGroup
+        "Catamorphisms"
+        [ testCase "Natural_F can tear down an Integer" unitCataNaturalF,
+          testCase "Negative_F can tear down an Integer" unitCataNegativeF,
+          testCase "ByteString_F can tear down a ByteString" unitCataByteStringF,
+          testCase "Non-recursive type cata should fail" unitCataMaybeF,
+          testCase "Cata with non-rigid algebra should fail" unitCataNonRigidF,
+          testCase "<List_F Integer Bool -> !Bool> with List Integer should be Bool" unitCataListInteger,
+          testCase "<List_F Integer r -> !r> with List Integer should be r" unitCataListIntegerRigid,
+          testCase "<List_F r Integer -> !Integer> with List r should be Integer" unitCataListRigid,
+          testCase "<List_F r (Maybe r) -> !Maybe r> with List r should be Maybe r" unitCataListMaybeRigid,
+          testCase "introduction then cata elimination" unitCataIntroThenEliminate
+        ],
+      testGroup
+        "Matching"
+        [ matchMaybe,
+          matchList,
+          maybeToList
+        ]
     ]
   where
     moreTests :: QuickCheckTests -> QuickCheckTests
@@ -147,11 +197,182 @@
     Left (TypeError _ ThunkError) -> pure ()
     _ -> assertFailure $ "Unexpected result: " <> show result
 
+-- Construct a function of type `<Natural_F Bool -> !Bool> -> Integer -> !Bool`, whose
+-- body performs a cata over its second argument using its first argument. This
+-- should compile, and type as expected.
+unitCataNaturalF :: IO ()
+unitCataNaturalF = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "Natural_F" [boolT] :--:> ReturnT boolT
+  let ty = Comp0 $ thunkTy :--:> integerT :--:> ReturnT boolT
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `<Negative_F Bool -> !Bool> -> Integer -> !Bool`, whose
+-- body performs a cata over its second argument using its first argument. This
+-- should compile, and type as expected.
+unitCataNegativeF :: IO ()
+unitCataNegativeF = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "Negative_F" [boolT] :--:> ReturnT boolT
+  let ty = Comp0 $ thunkTy :--:> integerT :--:> ReturnT boolT
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `<ByteString_F Integer -> !Integer> -> ByteString
+-- -> !Bool`, whose body performs a cata over its second argument using its
+-- first argument. This should compile, and type as expected.
+unitCataByteStringF :: IO ()
+unitCataByteStringF = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "ByteString_F" [integerT] :--:> ReturnT integerT
+  let ty = Comp0 $ thunkTy :--:> byteStringT :--:> ReturnT integerT
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `forall a . <Maybe_F a Integer -> !Integer> -> Maybe
+-- a -> !Integer`, whose body performs a cata over its second argument
+-- using its first argument. This should fail to compile, indicating that
+-- `Maybe` doesn't have a base functor.
+unitCataMaybeF :: IO ()
+unitCataMaybeF = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "Maybe_F" [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT
+  let ty = Comp1 $ thunkTy :--:> Datatype "Maybe" [tyvar Z ix0] :--:> ReturnT integerT
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationFailureUnit comp $ \case
+    TypeError _ (CataNoBaseFunctorForType tyName) -> assertEqual "" "Maybe" tyName
+    err' -> assertFailure $ "Failed with unexpected type of error: " <> show err'
+
+-- Construct a function of type `<forall a . ListF a (Maybe a) -> !Maybe a> -> List
+-- Integer -> !Maybe Integer`, whose body performs a cata over its second
+-- argument using its first argument. This should fail to compile due to a
+-- non-rigid algebra.
+unitCataNonRigidF :: IO ()
+unitCataNonRigidF = do
+  let nonRigidCompT = Comp1 $ Datatype "List_F" [tyvar Z ix0, Datatype "Maybe" [tyvar Z ix0]] :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])
+  let thunkTy = ThunkT nonRigidCompT
+  let ty = Comp0 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT (Datatype "Maybe" [integerT])
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationFailureUnit comp $ \case
+    TypeError _ (CataNonRigidAlgebra t) -> assertEqual "" nonRigidCompT t
+    err' -> assertFailure $ "Failed with unexpected type of error: " <> show err'
+
+-- Construct a function of type `<List_F Integer Bool -> !Bool> -> List Integer
+-- -> !Bool`, whose body performs a cata over its second argument using its
+-- first argument. This should compile, and type as expected.
+unitCataListInteger :: IO ()
+unitCataListInteger = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [integerT, boolT] :--:> ReturnT boolT
+  let ty = Comp0 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT boolT
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `forall a . <List_F Integer a -> !a> -> List
+-- Integer -> !a`, whose body performs a cata over its second argument using its
+-- first argument. This should compile, and type as expected.
+unitCataListIntegerRigid :: IO ()
+unitCataListIntegerRigid = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [integerT, tyvar (S Z) ix0] :--:> ReturnT (tyvar (S Z) ix0)
+  let ty = Comp1 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT (tyvar Z ix0)
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `forall a . <List_F a Integer -> !Integer> -> List
+-- a -> !Integer`, whose body performs a cata over its second argument using its
+-- first argument. This should compile, and type as expected.
+unitCataListRigid :: IO ()
+unitCataListRigid = do
+  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT
+  let ty = Comp1 $ thunkTy :--:> Datatype "List" [tyvar Z ix0] :--:> ReturnT integerT
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `forall a . <List_F a (Maybe a) -> !Maybe a> ->
+-- List a -> !Maybe a`, whose body performs a cata over its second argument
+-- using its first argument. This should compile, and type as expected.
+unitCataListMaybeRigid :: IO ()
+unitCataListMaybeRigid = do
+  let thunkTy =
+        ThunkT $
+          Comp0 $
+            Datatype "List_F" [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix0]]
+              :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix0])
+  let ty =
+        Comp1 $
+          thunkTy
+            :--:> Datatype "List" [tyvar Z ix0]
+            :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        result <- cata (AnArg alg) (AnArg x)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
+-- Construct a function of type `forall a b . <List_F a (Maybe b) -> !Maybe b> ->
+-- a -> !Maybe b`. In its body, we construct a singleton list, then eliminate it
+-- using a cata with the first argument as the algebra. THis should compile and
+-- type as expected.
+unitCataIntroThenEliminate :: IO ()
+unitCataIntroThenEliminate = do
+  let thunkTy =
+        ThunkT $
+          Comp0 $
+            Datatype "List_F" [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix1]]
+              :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix1])
+  let ty =
+        Comp2 $
+          thunkTy
+            :--:> tyvar Z ix0
+            :--:> ReturnT (Datatype "Maybe" [tyvar Z ix1])
+  let comp = lam ty $ do
+        alg <- arg Z ix0
+        x <- arg Z ix1
+        nilThunk <- dataConstructor "List" "Nil" []
+        nilForced <- force (AnId nilThunk)
+        aT <- boundTyVar Z ix0
+        nilApplied <- app nilForced [] [Here aT]
+        singleThunk <- dataConstructor "List" "Cons" [AnArg x, AnId nilApplied]
+        singleForced <- force (AnId singleThunk)
+        singleApplied <- app singleForced [] [Nowhere]
+        result <- cata (AnArg alg) (AnId singleApplied)
+        pure . AnId $ result
+  withCompilationSuccessUnit comp $ matchesType ty
+
 -- Properties
 
 propTopLevelConstant :: Property
 propTopLevelConstant = forAllShrinkShow arbitrary shrink show $ \c ->
-  let builtUp = lit c
+  let builtUp = AnId <$> lit c
    in withCompilationFailure builtUp $ \case
         TopLevelValue _ t info -> case info of
           Lit c' ->
@@ -201,25 +422,6 @@
                 ]
             _ -> failUnexpectedCompNodeInfo info
 
-propTopLevelReturn :: Property
-propTopLevelReturn = forAllShrinkShow arbitrary shrink show $ \c ->
-  let builtUp = lit c >>= \i -> ret (AnId i)
-   in withCompilationSuccess builtUp $ \asg ->
-        withToplevelCompNode asg $ \t info ->
-          case info of
-            Return r -> withExpectedId r $ \i ->
-              withExpectedValNode i asg $ \t' info' ->
-                case info' of
-                  Lit c' ->
-                    let cT = typeConstant c
-                     in conjoin
-                          [ c' === c,
-                            cT === t',
-                            t === Comp0 (ReturnT cT)
-                          ]
-                  _ -> failUnexpectedValNodeInfo info'
-            _ -> failUnexpectedCompNodeInfo info
-
 -- We use builtins only for this test, but this should demonstrate the
 -- properties well enough
 propForceThunk :: Property
@@ -247,30 +449,15 @@
             force (AnId thunkI)
        in (comp, forceThunkComp)
 
--- As we can't build toplevel value ASGs, this has to be a bit roundabout
-propApplyReturn :: Property
-propApplyReturn = forAllShrinkShow arbitrary shrink show $ \c ->
-  let comp = do
-        i <- lit c
-        ret (AnId i)
-      applyReturnComp = do
-        i <- comp
-        applied <- app i Vector.empty
-        ret (AnId applied)
-   in withCompilationSuccess comp $ \expectedASG ->
-        withCompilationSuccess applyReturnComp $ \applyReturnASG ->
-          withToplevelCompNode expectedASG $ \expectedT _ ->
-            withToplevelCompNode applyReturnASG $ \actualT _ ->
-              expectedT === actualT
-
 propForceComp :: Property
 propForceComp = forAllShrinkShow arbitrary shrink show $ \x ->
-  let comp = do
-        i <- case x of
-          Left bi1 -> builtin1 bi1
-          Right (Left bi2) -> builtin2 bi2
-          Right (Right bi3) -> builtin3 bi3
-        force (AnId i)
+  let comp =
+        AnId <$> do
+          i <- case x of
+            Left bi1 -> builtin1 bi1
+            Right (Left bi2) -> builtin2 bi2
+            Right (Right bi3) -> builtin3 bi3
+          force (AnId i)
       expectedT = case x of
         Left bi1 -> typeOneArgFunc bi1
         Right (Left bi2) -> typeTwoArgFunc bi2
@@ -282,9 +469,10 @@
 
 propForceNonThunk :: Property
 propForceNonThunk = forAllShrinkShow arbitrary shrink show $ \c ->
-  let comp = do
-        i <- lit c
-        force (AnId i)
+  let comp =
+        AnId <$> do
+          i <- lit c
+          force (AnId i)
    in withCompilationFailure comp $ \case
         TypeError _ (ForceNonThunk actualT) -> typeConstant c === actualT
         TypeError _ err' -> failWrongTypeError err'
@@ -292,9 +480,10 @@
 
 propThunkValType :: Property
 propThunkValType = forAllShrinkShow arbitrary shrink show $ \c ->
-  let comp = do
-        i <- lit c
-        thunk i
+  let comp =
+        AnId <$> do
+          i <- lit c
+          thunk i
    in withCompilationFailure comp $ \case
         TypeError _ (ThunkValType actualT) -> typeConstant c === actualT
         TypeError _ err' -> failWrongTypeError err'
@@ -302,10 +491,11 @@
 
 propApplyToVal :: Property
 propApplyToVal = forAllShrinkShow arbitrary shrink show $ \c args ->
-  let comp = do
-        args' <- traverse (fmap AnId . lit) args
-        i <- lit c
-        app i args'
+  let comp =
+        AnId <$> do
+          args' <- traverse (fmap AnId . lit) args
+          i <- lit c
+          app i args' mempty
    in withCompilationFailure comp $ \case
         TypeError _ (ApplyToValType t) -> typeConstant c === t
         TypeError _ err' -> failWrongTypeError err'
@@ -313,10 +503,11 @@
 
 propApplyToError :: Property
 propApplyToError = forAllShrinkShow arbitrary shrink show $ \args ->
-  let comp = do
-        args' <- traverse (fmap AnId . lit) args
-        i <- err
-        app i args'
+  let comp =
+        AnId <$> do
+          args' <- traverse (fmap AnId . lit) args
+          i <- err
+          app i args' mempty
    in withCompilationFailure comp $ \case
         TypeError _ ApplyToError -> property True
         TypeError _ err' -> failWrongTypeError err'
@@ -332,13 +523,14 @@
         Right (Left bi2) -> typeTwoArgFunc bi2
         Right (Right bi3) -> typeThreeArgFunc bi3
 
-      comp = do
-        i <- builtin1 f
-        arg' <- case arg1 of
-          Left bi1 -> builtin1 bi1
-          Right (Left bi2) -> builtin2 bi2
-          Right (Right bi3) -> builtin3 bi3
-        app i (Vector.singleton . AnId $ arg')
+      comp =
+        AnId <$> do
+          i <- builtin1 f
+          arg' <- case arg1 of
+            Left bi1 -> builtin1 bi1
+            Right (Left bi2) -> builtin2 bi2
+            Right (Right bi3) -> builtin3 bi3
+          app i (Vector.singleton . AnId $ arg') mempty
    in withCompilationFailure comp $ \case
         TypeError _ (ApplyCompType actualT) -> t === actualT
         TypeError _ err' -> failWrongTypeError err'
@@ -346,7 +538,7 @@
 
 propNonExistentArg :: Property
 propNonExistentArg = forAllShrinkShow arbitrary shrink show $ \(db, index) ->
-  let comp = arg db index >>= \i -> ret (AnArg i)
+  let comp = arg db index >>= \i -> pure $ AnArg i
    in withCompilationFailure comp $ \case
         TypeError _ (NoSuchArgument db' index') -> conjoin [db === db', index === index']
         TypeError _ err' -> failWrongTypeError err'
@@ -359,7 +551,7 @@
 propExistingArg = forAllShrinkShow gen shr show $ \(t, index) ->
   let comp = lam t $ do
         arg1 <- arg Z index
-        ret (AnArg arg1)
+        pure (AnArg arg1)
    in withCompilationSuccess comp $ \asg ->
         withToplevelCompNode asg $ \t' _ ->
           t' === t
@@ -399,41 +591,217 @@
                   Just (Concrete res') -> pure (Comp0 (ArgsAndResult (coerce args') res'), index)
            in shrinkOnIndex <|> shrinkOnArgs
 
-propReturnComp :: Property
-propReturnComp = forAllShrinkShow arbitrary shrink show $ \x ->
-  let t = case x of
-        Left bi1 -> typeOneArgFunc bi1
-        Right (Left bi2) -> typeTwoArgFunc bi2
-        Right (Right bi3) -> typeThreeArgFunc bi3
-      comp = do
-        i <- case x of
-          Left bi1 -> builtin1 bi1
-          Right (Left bi2) -> builtin2 bi2
-          Right (Right bi3) -> builtin3 bi3
-        ret (AnId i)
-   in withCompilationFailure comp $ \case
-        TypeError _ (ReturnCompType actualT) -> t === actualT
-        TypeError _ err' -> failWrongTypeError err'
-        err' -> failWrongError err'
+boundTyVarHappy :: Assertion
+boundTyVarHappy = run $ do
+  lam lamTy $ do
+    arg1 <- AnArg <$> arg Z ix0
+    void $ boundTyVar Z ix0
+    pure arg1
+  where
+    lamTy :: CompT AbstractTy
+    lamTy = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)
 
-propLambdaValBody :: Property
-propLambdaValBody = forAllShrinkShow arbitrary shrink show $ \(Concrete t, c) ->
-  let resultT = typeConstant c
-      comp = lam (Comp0 (ArgsAndResult (Vector.singleton t) resultT)) $ lit c
-   in withCompilationFailure comp $ \case
-        TypeError _ (LambdaResultsInValType actualT) -> resultT === actualT
-        TypeError _ err' -> failWrongTypeError err'
-        err' -> failWrongError err'
+    run :: forall (a :: Type). ASGBuilder a -> IO ()
+    run act = case runASGBuilder M.empty act of
+      Left err' -> assertFailure . show $ err'
+      Right {} -> pure ()
 
+boundTyVarShouldFail :: Assertion
+boundTyVarShouldFail = run $ boundTyVar Z ix0
+  where
+    run :: forall (a :: Type). (Show a) => ASGBuilder a -> IO ()
+    run act = case runASGBuilder M.empty act of
+      Left (TypeError _ (OutOfScopeTyVar db argpos)) ->
+        if db == Z && argpos == ix0
+          then pure ()
+          else assertFailure $ "Expected OutOfScopeTyVar error for Z, ix0 but got: " <> show db <> ", " <> show argpos
+      Left err' -> assertFailure $ "Expected an OutofScopeTyVar error, but got: " <> show err'
+      Right x -> assertFailure $ "Expected boundTyVar to fail, but got: " <> show x
+
+-- TODO: better name
+newLamTest1 :: Assertion
+newLamTest1 = case runASGBuilder M.empty fn of
+  Left err' -> assertFailure (show err')
+  Right {} -> pure ()
+  where
+    fn :: ASGBuilder Id
+    fn = lam expected $ do
+      f <- arg Z ix0 >>= force . AnArg
+      a <- AnArg <$> arg Z ix1
+      AnId <$> app f (Vector.singleton a) mempty
+
+    expected :: CompT AbstractTy
+    expected =
+      Comp2 $
+        ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix1))
+          :--:> tyvar Z ix0
+          :--:> ReturnT (tyvar Z ix1)
+
+newLamTest2 :: Assertion
+newLamTest2 = case runASGBuilder tyAppTestDatatypes fn of
+  Left err' -> assertFailure (show err')
+  Right {} -> pure ()
+  where
+    fn :: ASGBuilder Id
+    fn = lam expected $ do
+      f <- arg Z ix0 >>= force . AnArg
+      a <- AnArg <$> arg Z ix1
+      AnId <$> app f (Vector.singleton a) mempty
+
+    expected :: CompT AbstractTy
+    expected =
+      Comp2 $
+        ThunkT (Comp0 $ Datatype "Maybe" (Vector.singleton $ tyvar (S Z) ix0) :--:> ReturnT (tyvar (S Z) ix1))
+          :--:> Datatype "Maybe" (Vector.singleton $ tyvar Z ix0)
+          :--:> ReturnT (tyvar Z ix1)
+
+-- Intro form tests
+
+nothingIntro :: TestTree
+nothingIntro =
+  runIntroFormTest "nothing" expectNothingThunk $
+    dataConstructor "Maybe" "Nothing" mempty >>= typeIdTest
+  where
+    expectNothingThunk :: ValT AbstractTy
+    expectNothingThunk = ThunkT . Comp1 . ReturnT $ Datatype "Maybe" (Vector.fromList [tyvar Z ix0])
+
+justConcreteIntro :: TestTree
+justConcreteIntro = runIntroFormTest "justConcreteIntro" expected $ do
+  argRef <- AnId <$> lit AUnit
+  dataConstructor "Maybe" "Just" (Vector.singleton argRef) >>= typeIdTest
+  where
+    expected :: ValT AbstractTy
+    expected = ThunkT . Comp0 . ReturnT $ Datatype "Maybe" (Vector.singleton $ BuiltinFlat UnitT)
+
+justRigidIntro :: TestTree
+justRigidIntro = runIntroFormTest "justRigidIntro" expected $ do
+  lamId <- lam lamTy $ do
+    arg1 <- AnArg <$> arg Z ix0
+    justRigid <- dataConstructor "Maybe" "Just" (Vector.singleton arg1)
+    pure (AnId justRigid)
+  lamThunked <- thunk lamId
+  typeIdTest lamThunked
+  where
+    lamTy :: CompT AbstractTy
+    lamTy =
+      Comp1 $
+        tyvar Z ix0
+          :--:> ReturnT
+            ( ThunkT
+                . Comp0
+                . ReturnT
+                $ Datatype "Maybe"
+                $ Vector.singleton (tyvar (S Z) ix0)
+            )
+
+    expected :: ValT AbstractTy
+    expected = ThunkT lamTy
+
+justNothingIntro :: TestTree
+justNothingIntro = runIntroFormTest "justNothingIntro" expectedThunk $ do
+  thunkL <- lam expectedComp $ do
+    nothingThunk <- dataConstructor "Maybe" "Nothing" mempty
+    var <- boundTyVar Z ix0
+    nothingForced <- force (AnId nothingThunk)
+    nothingApplied <- app nothingForced mempty (Vector.singleton . wedgeLeft . Just $ var)
+    justNothing <- dataConstructor "Maybe" "Just" (Vector.singleton (AnId nothingApplied))
+    justNothingForced <- force (AnId justNothing)
+    justNothingApplied <- app justNothingForced mempty (Vector.singleton Nowhere)
+    pure (AnId justNothingApplied)
+  typeIdTest thunkL
+  where
+    expectedComp :: CompT AbstractTy
+    expectedComp =
+      Comp1
+        . ReturnT
+        . Datatype "Maybe"
+        . Vector.singleton
+        . Datatype "Maybe"
+        $ Vector.singleton
+        $ tyvar Z ix0
+
+    expectedThunk :: ValT AbstractTy
+    expectedThunk = ThunkT expectedComp
+
+-- pattern matching
+
+{- Construct a pattern match on 'Maybe Unit' that returns an integer.
+
+   This is effectively the simplest possible pattern matching test: The type is non-recursive and the
+   parameters to the type constructor are all concrete.
+-}
+matchMaybe :: TestTree
+matchMaybe = runIntroFormTest "matchMaybe" (BuiltinFlat IntegerT) $ do
+  unit <- AnId <$> lit AUnit
+  scrutinee <- ctor "Maybe" "Just" (Vector.singleton unit) (Vector.singleton Nowhere)
+  nothingHandler <- lazyLam (Comp0 $ ReturnT (BuiltinFlat IntegerT)) (AnId <$> lit (AnInteger 0))
+  justHandler <- lazyLam (Comp0 $ BuiltinFlat UnitT :--:> ReturnT (BuiltinFlat IntegerT)) (AnId <$> lit (AnInteger 1))
+  result <- match (AnId scrutinee) (AnId <$> Vector.fromList [justHandler, nothingHandler])
+  typeIdTest result
+
+{- Construct a pattern match on 'List Unit' that returns an integer.
+
+   A simple test for pattern matches on values of recursive types.
+-}
+matchList :: TestTree
+matchList = runIntroFormTest "matchList" (BuiltinFlat IntegerT) $ do
+  unit <- AnId <$> lit AUnit
+  nilUnit <- ctor "List" "Nil" mempty (Vector.singleton $ There (BuiltinFlat UnitT))
+  scrutinee <- ctor "List" "Cons" (Vector.fromList [unit, AnId nilUnit]) (Vector.singleton Nowhere)
+  let nilHandlerTy = Comp0 $ ReturnT (BuiltinFlat IntegerT)
+      consHandlerTy =
+        Comp0 $
+          BuiltinFlat UnitT
+            :--:> Datatype "List_F" (Vector.fromList [BuiltinFlat UnitT, Datatype "List" (Vector.singleton $ BuiltinFlat UnitT)])
+            :--:> ReturnT (BuiltinFlat IntegerT)
+  nilHandler <- lazyLam nilHandlerTy (AnId <$> lit (AnInteger 0))
+  consHandler <- lazyLam consHandlerTy (AnId <$> lit (AnInteger 0))
+  result <- match (AnId scrutinee) (AnId <$> Vector.fromList [nilHandler, consHandler])
+  typeIdTest result
+
+{- This differs from the two above tests in that we're using pattern matching to construct the
+   'maybeToList :: forall a. Maybe a -> List a' function. This is very useful, because if successful, it provides good evidence that:
+     1. Pattern matching works on datatypes with rigid parameters.
+     2. Pattern matching works inside the body of a lambda.
+     3. Nothing breaks renaming anywhere.
+-}
+maybeToList :: TestTree
+maybeToList = runIntroFormTest "maybeToList" maybeToListTy $ do
+  thonk <- lazyLam maybeToListCompTy $ do
+    let nothingHandlerTy = Comp0 $ ReturnT (dtype "List" [tyvar (S Z) ix0])
+        justHandlerTy = Comp0 $ tyvar (S Z) ix0 :--:> ReturnT (dtype "List" [tyvar (S Z) ix0])
+    nothingHandler <- lazyLam nothingHandlerTy $ do
+      tvA <- boundTyVar (S Z) ix0
+      AnId <$> ctor "List" "Nil" mempty (Vector.singleton (Here tvA))
+    justHandler <- lazyLam justHandlerTy $ do
+      tvA <- boundTyVar (S Z) ix0
+      vA <- AnArg <$> arg Z ix0
+      nil <- AnId <$> ctor "List" "Nil" mempty (Vector.singleton (Here tvA))
+      AnId <$> ctor "List" "Cons" (Vector.fromList [vA, nil]) (Vector.singleton Nowhere)
+    scrutinee <- AnArg <$> arg Z ix0
+    AnId <$> match scrutinee (AnId <$> Vector.fromList [justHandler, nothingHandler])
+  typeIdTest thonk
+  where
+    maybeToListCompTy :: CompT AbstractTy
+    maybeToListCompTy = Comp1 (dtype "Maybe" [tyvar Z ix0] :--:> ReturnT (dtype "List" [tyvar Z ix0]))
+
+    maybeToListTy :: ValT AbstractTy
+    maybeToListTy = ThunkT maybeToListCompTy
+
 -- Helpers
 
+runIntroFormTest :: String -> ValT AbstractTy -> DebugASGBuilder (ValT AbstractTy) -> TestTree
+runIntroFormTest nm expectedTy act = testCase nm $ case debugASGBuilder tyAppTestDatatypes act of
+  Left err' -> assertFailure ("ASG Error: " <> show err')
+  Right actualTy -> assertEqual nm expectedTy actualTy
+
 failWrongTypeError :: CovenantTypeError -> Property
 failWrongTypeError err' = failWithCounterExample ("Unexpected type error: " <> show err')
 
 failWrongError :: CovenantError -> Property
 failWrongError err' = failWithCounterExample ("Unexpected error: " <> show err')
 
-withCompilationFailure :: ASGBuilder Id -> (CovenantError -> Property) -> Property
+withCompilationFailure :: ASGBuilder Ref -> (CovenantError -> Property) -> Property
 withCompilationFailure comp cb = case runASGBuilder M.empty comp of
   Left err' -> cb err'
   Right asg -> failWithCounterExample ("Unexpected success: " <> show asg)
@@ -459,6 +827,23 @@
 failUnexpectedValNodeInfo info =
   failWithCounterExample ("Unexpected ValNodeInfo: " <> show info)
 
+withCompilationSuccessUnit :: ASGBuilder Id -> (ASG -> IO ()) -> IO ()
+withCompilationSuccessUnit comp cb = case runASGBuilder defaultDatatypes comp of
+  Left err' -> assertFailure $ "Did not compile: " <> show err'
+  Right asg -> cb asg
+
+withCompilationFailureUnit :: ASGBuilder Id -> (CovenantError -> IO ()) -> IO ()
+withCompilationFailureUnit comp cb = case runASGBuilder defaultDatatypes comp of
+  Left err' -> cb err'
+  Right asg -> assertFailure $ "Unexpected compilation success: " <> show asg
+
+matchesType :: CompT AbstractTy -> ASG -> IO ()
+matchesType expectedTy asg = case topLevelNode asg of
+  ACompNode actualTy _ -> assertEqual "" expectedTy actualTy
+  u@(AValNode _ _) -> assertFailure $ "Got a value node: " <> show u
+  AnError -> assertFailure "Got an error node"
+
+{- NOTE: Not 100% sure I won't need these
 withExpectedId :: Ref -> (Id -> Property) -> Property
 withExpectedId r cb = case r of
   AnId i -> cb i
@@ -468,3 +853,4 @@
 withExpectedValNode i asg cb = case nodeAt i asg of
   AValNode t info -> cb t info
   node -> failWithCounterExample ("Unexpected node: " <> show node)
+--}
diff --git a/test/bb/Main.hs b/test/bb/Main.hs
--- a/test/bb/Main.hs
+++ b/test/bb/Main.hs
@@ -2,8 +2,6 @@
 
 module Main (main) where
 
--- import Data.Either (isRight)
-
 import Control.Exception (throwIO)
 import Control.Monad ((<=<))
 import Covenant.Data
@@ -69,7 +67,7 @@
     Right (catMaybes -> bbfDecls) ->
       let results =
             mapM
-              ( \valT -> case runRenameM . renameValT $ valT of
+              ( \valT -> case runRenameM mempty . renameValT $ valT of
                   Left err -> Left (err, valT)
                   Right res -> Right res
               )
@@ -149,8 +147,8 @@
 testMonotypeBB :: TestTree
 testMonotypeBB = testCase "unitBbf" $ do
   let expected = Comp1 $ Abstraction (BoundAt Z ix0) :--:> ReturnT (Abstraction $ BoundAt Z ix0)
-  expected' <- failLeft . runRenameM . renameCompT $ expected
+  expected' <- failLeft . runRenameM mempty . renameCompT $ expected
   actual <- case fromJust . (view #bbForm <=< M.lookup "Unit") $ tyAppTestDatatypes of
-    ThunkT inner -> either (throwIO . userError . show) pure . runRenameM $ renameCompT inner
+    ThunkT inner -> either (throwIO . userError . show) pure . runRenameM mempty $ renameCompT inner
     _ -> assertFailure "BB form not a thunk!"
   assertEqual "unit bbf" expected' actual
diff --git a/test/primops/Main.hs b/test/primops/Main.hs
--- a/test/primops/Main.hs
+++ b/test/primops/Main.hs
@@ -292,7 +292,7 @@
   Property
 mkRenameProp typingFun = forAll arbitrary $ \f ->
   let t = typingFun f
-      result = runRenameM . renameCompT $ t
+      result = runRenameM mempty . renameCompT $ t
    in case result of
         Left err -> counterexample (show err) False
         Right renamed -> property $ liftEq eqRenamedVar t renamed
@@ -309,7 +309,7 @@
   CompT AbstractTy ->
   (CompT Renamed -> IO ()) ->
   IO ()
-withRenamedComp t f = case runRenameM . renameCompT $ t of
+withRenamedComp t f = case runRenameM mempty . renameCompT $ t of
   Left err -> assertFailure $ "Could not rename: " <> show err
   Right t' -> f t'
 
@@ -319,7 +319,7 @@
   t (ValT AbstractTy) ->
   (t (ValT Renamed) -> IO ()) ->
   IO ()
-withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of
+withRenamedVals vals f = case runRenameM mempty . traverse renameValT $ vals of
   Left err -> assertFailure $ "Could not rename: " <> show err
   Right vals' -> f vals'
 
diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs
--- a/test/renaming/Main.hs
+++ b/test/renaming/Main.hs
@@ -81,14 +81,14 @@
 testFlat :: BuiltinFlatT -> IO ()
 testFlat t = do
   let input = BuiltinFlat t
-  let result = runRenameM . renameValT $ input
+  let result = runRenameM mempty . renameValT $ input
   assertRight (assertBool "" . liftEq (\_ _ -> False) input) result
 
 -- Checks that for any 'fully concretified' type (nested or not), renaming
 -- changes nothing.
 propNestedConcrete :: Property
 propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) ->
-  let result = runRenameM . renameValT $ t
+  let result = runRenameM mempty . renameValT $ t
    in case result of
         Left _ -> False
         Right actual -> liftEq (\_ _ -> False) t actual
@@ -101,7 +101,7 @@
         Comp1 $
           Abstraction (Unifiable ix0)
             :--:> ReturnT (Abstraction (Unifiable ix0))
-  let result = runRenameM . renameCompT $ idT
+  let result = runRenameM mempty . renameCompT $ idT
   assertRight (assertEqual "" expected) result
 
 -- Checks that `forall a b . a -> b -> !a` correctly renames.
@@ -113,7 +113,7 @@
           Abstraction (Unifiable ix0)
             :--:> Abstraction (Unifiable ix1)
             :--:> ReturnT (Abstraction (Unifiable ix0))
-  let result = runRenameM . renameCompT $ constT
+  let result = runRenameM mempty . renameCompT $ constT
   assertRight (assertEqual "" expected) result
 
 -- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames.
@@ -126,22 +126,23 @@
           Abstraction (Unifiable ix0)
             :--:> ReturnT
               ( ThunkT . Comp1 $
-                  Abstraction (Wildcard 1 2 ix0)
+                  Abstraction (Wildcard 1 1 ix0)
                     :--:> ReturnT (Abstraction (Unifiable ix0))
               )
-  let result = runRenameM . renameCompT $ constT
+  let result = runRenameM mempty . renameCompT $ constT
   assertRight (assertEqual "" expected) result
 
 -- Checks that `forall a . b -> !a` triggers the variable indexing checker.
 testIndexingIdT :: IO ()
 testIndexingIdT = do
-  let t = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix1)
-  let result = runRenameM . renameCompT $ t
+  let t = Comp1 $ tyvar Z ix1 :--:> ReturnT (tyvar Z ix0)
+  let result = runRenameM mempty . renameCompT $ t
+
   case result of
     Left (InvalidAbstractionReference trueLevel ix) -> do
-      assertEqual "" trueLevel 1
+      assertEqual "" trueLevel 0
       assertEqual "" ix ix1
-    _ -> assertBool "renaming succeeded when it should have failed" False
+    _ -> assertBool ("renaming succeeded when it should have failed: " <> show result) False
 
 -- Helpers
 
diff --git a/test/type-applications/Main.hs b/test/type-applications/Main.hs
--- a/test/type-applications/Main.hs
+++ b/test/type-applications/Main.hs
@@ -3,7 +3,6 @@
 module Main (main) where
 
 import Control.Applicative ((<|>))
-import Control.Monad (guard)
 import Covenant.ASG
   ( TypeAppError
       ( DoesNotUnify,
@@ -14,6 +13,7 @@
 import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
 import Covenant.Index
   ( Index,
+    intIndex,
     ix0,
     ix1,
     ix2,
@@ -43,27 +43,35 @@
 import Data.Functor.Identity (Identity (Identity))
 import Data.Kind (Type)
 import Data.Map qualified as M
+import Data.Maybe (fromJust)
+import Data.Vector (Vector)
 import Data.Vector qualified as Vector
-import Optics.Core (review)
+import Data.Word (Word32)
+import Optics.Core (preview, review)
 import Test.QuickCheck
   ( Gen,
     Property,
     arbitrary,
+    chooseInt,
     counterexample,
     discard,
     elements,
+    forAll,
     forAllShrink,
+    getNonZero,
     getSize,
+    liftArbitrary,
     liftShrink,
     oneof,
     shrink,
     suchThat,
+    suchThatMap,
     vectorOf,
     (===),
   )
 import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup)
 import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)
-import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)
+import Test.Tasty.QuickCheck (QuickCheckMaxSize, QuickCheckTests, testProperty)
 
 main :: IO ()
 main =
@@ -79,13 +87,13 @@
       testGroup
         "Unification"
         [ testProperty "concrete expected, concrete actual" propUnifyConcrete,
-          testProperty "rigid expected, concrete actual" propUnifyRigidConcrete,
+          adjustOption smallerTests . testProperty "rigid expected, concrete actual" $ propUnifyRigidConcrete,
           testProperty "wildcard expected, concrete actual" propUnifyWildcardConcrete,
           testProperty "wildcard expected, unifiable actual" propUnifyWildcardUnifiable,
-          testProperty "concrete expected, rigid actual" propUnifyConcreteRigid,
-          testProperty "unifiable expected, rigid actual" propUnifyUnifiableRigid,
+          adjustOption smallerTests . testProperty "concrete expected, rigid actual" $ propUnifyConcreteRigid,
+          adjustOption smallerTests . testProperty "unifiable expected, rigid actual" $ propUnifyUnifiableRigid,
           testProperty "rigid expected, rigid actual" propUnifyRigid,
-          testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid,
+          adjustOption smallerTests . testProperty "wildcard expected, rigid actual" $ propUnifyWildcardRigid,
           testProperty "thunk with unifiable result" propThunkWithUnifiableResult
         ],
       testGroup
@@ -110,14 +118,20 @@
     moreTests :: QuickCheckTests -> QuickCheckTests
     moreTests = max 10_000
 
+    -- fewerTests :: QuickCheckTests -> QuickCheckTests
+    -- fewerTests = const 100
+
+    smallerTests :: QuickCheckMaxSize -> QuickCheckMaxSize
+    smallerTests = (`div` 4)
+
 -- Units and properties
 
 -- Try to apply more than one argument to `forall a . a -> !a`.
 -- Result should indicate excess arguments.
 propTooManyArgs :: Property
 propTooManyArgs = forAllShrink gen shr $ \excessArgs ->
-  withRenamedComp idT $ \renamedIdT ->
-    withRenamedVals excessArgs $ \renamedExcessArgs ->
+  withRenamedComp mempty idT $ \renamedIdT ->
+    withRenamedVals mempty excessArgs $ \renamedExcessArgs ->
       case renamedExcessArgs of
         [] -> discard -- should be impossible
         _ : extraArgs ->
@@ -147,7 +161,7 @@
 -- insufficient arguments.
 unitInsufficientArgs :: IO ()
 unitInsufficientArgs = do
-  renamedIdT <- failLeft . runRenameM . renameCompT $ idT
+  renamedIdT <- failLeft . runRenameM mempty . renameCompT $ idT
   let expected = Left $ InsufficientArgs 0 renamedIdT []
   let actual = checkApp M.empty renamedIdT []
   assertEqual "" expected actual
@@ -156,8 +170,8 @@
 -- that type.
 propIdConcrete :: Property
 propIdConcrete = forAllShrink arbitrary shrink $ \(Concrete t) ->
-  withRenamedComp idT $ \renamedIdT ->
-    withRenamedVals (Identity t) $ \(Identity t') ->
+  withRenamedComp mempty idT $ \renamedIdT ->
+    withRenamedVals mempty (Identity t) $ \(Identity t') ->
       let expected = Right t'
           actual = checkApp M.empty renamedIdT [Just t']
        in expected === actual
@@ -166,8 +180,8 @@
 -- Result should be that type.
 propConst2Same :: Property
 propConst2Same = forAllShrink arbitrary shrink $ \(Concrete t) ->
-  withRenamedComp const2T $ \renamedConst2T ->
-    withRenamedVals (Identity t) $ \(Identity t') ->
+  withRenamedComp mempty const2T $ \renamedConst2T ->
+    withRenamedVals mempty (Identity t) $ \(Identity t') ->
       let expected = Right t'
           actual = checkApp M.empty renamedConst2T [Just t', Just t']
        in expected === actual
@@ -178,9 +192,9 @@
 propConst2Different = forAllShrink arbitrary shrink $ \(Concrete t1, Concrete t2) ->
   if t1 == t2
     then discard
-    else withRenamedComp const2T $ \renamedConst2T ->
-      withRenamedVals (Identity t1) $ \(Identity t1') ->
-        withRenamedVals (Identity t2) $ \(Identity t2') ->
+    else withRenamedComp mempty const2T $ \renamedConst2T ->
+      withRenamedVals mempty (Identity t1) $ \(Identity t1') ->
+        withRenamedVals mempty (Identity t2) $ \(Identity t2') ->
           let expected = Right t1'
               actual = checkApp M.empty renamedConst2T [Just t1', Just t2']
            in expected === actual
@@ -191,8 +205,8 @@
 -- unification error otherwise.
 propUnifyConcrete :: Property
 propUnifyConcrete = forAllShrink gen shr $ \(tA, mtB) ->
-  withRenamedComp (Comp0 $ tA :--:> ReturnT integerT) $ \f ->
-    withRenamedVals (Identity tA) $ \(Identity tA') ->
+  withRenamedComp mempty (Comp0 $ tA :--:> ReturnT integerT) $ \f ->
+    withRenamedVals mempty (Identity tA) $ \(Identity tA') ->
       case mtB of
         Nothing ->
           let expected = Right integerT
@@ -201,7 +215,7 @@
         Just tB ->
           if tA == tB
             then discard
-            else withRenamedVals (Identity tB) $ \(Identity arg) ->
+            else withRenamedVals mempty (Identity tB) $ \(Identity arg) ->
               let expected = Left . DoesNotUnify tA' $ arg
                   actual = checkApp M.empty f [Just arg]
                in expected === actual
@@ -226,26 +240,27 @@
 -- !Integer` to `b`. Result should fail to unify.
 propUnifyRigidConcrete :: Property
 propUnifyRigidConcrete = forAllShrink arbitrary shrink $ \(Concrete t, scope, ix) ->
-  withRenamedComp (Comp0 $ tyvar (S scope) ix :--:> ReturnT integerT) $ \f ->
-    withRenamedVals (Identity t) $ \(Identity t') ->
-      -- This is a little confusing, as we would expect that the true level will
-      -- be based on `S scope`, since that's what's in the computation type.
-      -- However, we actually have to reduce it by 1, as we have a 'scope
-      -- stepdown' for `f` even though we bind no variables.
-      let trueLevel = negate . review asInt $ scope
-          expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t'
-          actual = checkApp M.empty f [Just t']
-       in expected === actual
+  let mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex ix + 1)
+   in withRenamedComp mockScope (Comp0 $ tyvar (S scope) ix :--:> ReturnT integerT) $ \f ->
+        withRenamedVals mockScope (Identity t) $ \(Identity t') ->
+          -- This is a little confusing, as we would expect that the true level will
+          -- be based on `S scope`, since that's what's in the computation type.
+          -- However, we actually have to reduce it by 1, as we have a 'scope
+          -- stepdown' for `f` even though we bind no variables.
+          let trueLevel = ezTrueLevel mockScope scope ix
+              expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t'
+              actual = checkApp M.empty f [Just t']
+           in expected === actual
 
 -- Randomly pick a concrete type A, then try to apply `(forall a . a ->
 -- !Integer) -> !Integer` to `(A -> !Integer)`. Result should fail to unify.
 propUnifyWildcardConcrete :: Property
 propUnifyWildcardConcrete = forAllShrink arbitrary shrink $ \(Concrete t) ->
   let thunk = ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT integerT
-   in withRenamedComp (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->
+   in withRenamedComp mempty (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->
         let argT = ThunkT . Comp0 $ t :--:> ReturnT integerT
-         in withRenamedVals (Identity argT) $ \(Identity argT') ->
-              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT
+         in withRenamedVals mempty (Identity argT) $ \(Identity argT') ->
+              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 1 ix0) :--:> ReturnT integerT
                   expected = Left . DoesNotUnify lhs $ argT'
                   actual = checkApp M.empty f [Just argT']
                in expected === actual
@@ -255,102 +270,100 @@
 -- to `A`.
 propUnifyWildcardUnifiable :: Property
 propUnifyWildcardUnifiable = forAllShrink arbitrary shrink $ \(Concrete t) ->
-  withRenamedComp (Comp0 $ ThunkT (Comp1 $ tyvar Z ix0 :--:> ReturnT t) :--:> ReturnT t) $ \f ->
-    withRenamedVals (Identity t) $ \(Identity t') ->
-      withRenamedVals (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) ->
-        let expected = Right t'
-            actual = checkApp M.empty f [Just arg]
-         in expected === actual
+  let mockScope = Vector.singleton 1
+   in withRenamedComp mockScope (Comp0 $ ThunkT (Comp1 $ tyvar Z ix0 :--:> ReturnT t) :--:> ReturnT t) $ \f ->
+        withRenamedVals mockScope (Identity t) $ \(Identity t') ->
+          withRenamedVals mockScope (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) ->
+            let expected = Right t'
+                actual = checkApp M.empty f [Just arg]
+             in expected === actual
 
 -- Randomly generate a concrete type A, and a rigid type B, then try to apply `A
 -- -> !Integer` to `B`. Result should fail to unify.
 propUnifyConcreteRigid :: Property
 propUnifyConcreteRigid = forAllShrink arbitrary shrink $ \(Concrete aT, scope, index) ->
-  withRenamedComp (Comp0 $ aT :--:> ReturnT integerT) $ \f ->
-    withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) ->
-      withRenamedVals (Identity aT) $ \(Identity aT') ->
-        let level = negate . review asInt $ scope
-            expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index
-            actual = checkApp M.empty f [Just arg]
-         in expected === actual
+  let mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex index + 1)
+   in withRenamedComp mockScope (Comp0 $ aT :--:> ReturnT integerT) $ \f ->
+        withRenamedVals mockScope (Identity $ tyvar scope index) $ \(Identity arg) ->
+          withRenamedVals mockScope (Identity aT) $ \(Identity aT') ->
+            let level = ezTrueLevel mockScope scope index
+                expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index
+                actual = checkApp M.empty f [Just arg]
+             in expected === actual
 
 -- Randomly generate a rigid type A, then try to apply `forall a . a -> !a` to
 -- `A`. Result should unify to `A`.
 propUnifyUnifiableRigid :: Property
 propUnifyUnifiableRigid = forAllShrink arbitrary shrink $ \(scope, index) ->
-  withRenamedComp idT $ \f ->
-    withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) ->
-      let expected = Right arg
-          actual = checkApp M.empty f [Just arg]
-       in expected === actual
+  let mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex index + 1)
+   in withRenamedComp mockScope idT $ \f ->
+        withRenamedVals mockScope (Identity $ tyvar scope index) $ \(Identity arg) ->
+          let expected = Right arg
+              actual = checkApp M.empty f [Just arg]
+           in expected === actual
 
--- Randomly generate a scope S and an index I, then another scope S' and another
--- index I', that may or may not be different to S and/or I respectively. Let
--- `T` be the rigid type that results from `S` and `I`, and `U` be the rigid
--- type that results from `S'` and `I'`. Attempt to unify `T -> !Integer` with
--- `U`. This should unify to `Integer` if, and only if, `T == U`; otherwise, it
--- should fail to unify.
+-- Randomly generate a scope stack of height at least 2, then two indexes `I`
+-- and `J`, both valid in that scope stack. `I` and `J` may be different or the
+-- same, with equal probability. Let `T` be the rigid type corresponding to some
+-- variable index in the scope stack at the position for `I`, and `U` be the
+-- rigid type corresponding to some variable index in the scope stack at the
+-- position for `J`. Attempt to unify `T -> !Integer` with `U`. This should
+-- unify to `Integer` if, and only if, `T == U`; otherwise, it should fail to
+-- unify.
 propUnifyRigid :: Property
-propUnifyRigid = forAllShrink gen shr $ \testData ->
-  withTestData testData $ \(f, arg, expected) ->
-    let actual = checkApp M.empty f [Just arg]
-     in expected === actual
+propUnifyRigid = forAll gen $ \(scopeStack, t, u, same) ->
+  withRenamedComp scopeStack (Comp0 $ t :--:> ReturnT integerT) $ \fun ->
+    withRenamedVals scopeStack (Identity u) $ \(Identity arg) ->
+      case checkApp mempty fun [Just arg] of
+        Left err -> counterexample ("Identical rigids, but got " <> show err) $ not same
+        Right res -> counterexample ("Different rigids, but unified to " <> show res) same
   where
-    gen :: Gen (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))
+    gen :: Gen (Vector Word32, ValT AbstractTy, ValT AbstractTy, Bool)
     gen = do
-      db <- arbitrary
-      index <- arbitrary
-      (db,index,)
-        <$> oneof
-          [ pure Nothing,
-            Just . Left <$> suchThat arbitrary (db /=),
-            Just . Right <$> suchThat arbitrary (index /=)
-          ]
-    shr ::
-      (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) ->
-      [(DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))]
-    shr (db, index, mrest) = do
-      db' <- shrink db
-      index' <- shrink index
-      case mrest of
-        Nothing -> pure (db', index, Nothing) <|> pure (db, index', Nothing)
-        Just (Left db2) -> do
-          db2' <- shrink db2
-          (db', index, Just (Left db2)) <$ guard (db' /= db2)
-            <|> pure (db, index', Just (Left db2))
-            <|> (db, index, Just (Left db2')) <$ guard (db /= db2')
-        Just (Right index2) -> do
-          index2' <- shrink index2
-          pure (db', index, Just (Right index2))
-            <|> (db, index', Just (Right index2)) <$ guard (index' /= index2)
-            <|> (db, index, Just (Right index2')) <$ guard (index /= index2')
-    withTestData ::
-      (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) ->
-      ((CompT Renamed, ValT Renamed, Either TypeAppError (ValT Renamed)) -> Property) ->
-      Property
-    withTestData (db, index, mrest) f =
-      withRenamedComp (Comp0 $ tyvar (S db) index :--:> ReturnT integerT) $ \fun ->
-        case mrest of
-          Nothing -> withRenamedVals (Identity . tyvar db $ index) $ \(Identity arg) ->
-            f (fun, arg, Right integerT)
-          Just rest ->
-            let level = negate . review asInt $ db
-                lhs = Abstraction . Rigid level $ index
-             in case rest of
-                  Left db2 -> withRenamedVals (Identity . tyvar db2 $ index) $ \(Identity arg) ->
-                    f (fun, arg, Left . DoesNotUnify lhs $ arg)
-                  Right index2 -> withRenamedVals (Identity . tyvar db $ index2) $ \(Identity arg) ->
-                    f (fun, arg, Left . DoesNotUnify lhs $ arg)
+      -- Note (Koz, 08/08/2025): We have to use this rather odd method to ensure
+      -- that we never have any scope stack smaller than 2 elements. If we have
+      -- an empty stack, we loop forever as we can't find a valid index, and if
+      -- the scope stack is a singleton, we can never hit the 'different' case.
+      --
+      -- Furthermore, we must ensure every scope stack has at least 1 available
+      -- variable, as otherwise, our subsequent generator can 'miss'.
+      firstScope <- getNonZero <$> arbitrary
+      secondScope <- getNonZero <$> arbitrary
+      restOfScopes <- liftArbitrary (getNonZero <$> arbitrary)
+      let scopeStack = Vector.cons firstScope . Vector.cons secondScope $ restOfScopes
+      (t, u, same) <- genAbstractions scopeStack
+      pure (scopeStack, t, u, same)
+    genAbstractions :: Vector Word32 -> Gen (ValT AbstractTy, ValT AbstractTy, Bool)
+    genAbstractions scopeStack = do
+      let len = Vector.length scopeStack
+      iPosition <- chooseInt (0, len - 1)
+      jPosition <- suchThat (chooseInt (0, len - 1)) (/= iPosition)
+      let iDB = fromJust . preview asInt $ iPosition
+      let jDB = fromJust . preview asInt $ jPosition
+      let iVarsAvailable = fromIntegral $ scopeStack Vector.! iPosition
+      let jVarsAvailable = fromIntegral $ scopeStack Vector.! jPosition
+      iIx <- suchThatMap (chooseInt (0, iVarsAvailable - 1)) (preview intIndex)
+      jIx <- suchThatMap (chooseInt (0, jVarsAvailable - 1)) (preview intIndex)
+      -- Note (Koz, 08/08/2025): We have to offset `t` by 1, because it's being
+      -- bundled directly into a `Comp0`, which means that to refer to the same
+      -- position in the scope stack, it needs to be one higher.
+      elements
+        [ -- 'Same' option.
+          (tyvar (S iDB) iIx, tyvar iDB iIx, True),
+          -- 'Different' option.
+          (tyvar (S iDB) iIx, tyvar jDB jIx, False)
+        ]
 
 -- Randomly pick a rigid type A, then try to apply `(forall a . a -> !Integer)
 -- -> !Integer` to `(A -> !Integer)`. Result should fail to unify.
 propUnifyWildcardRigid :: Property
 propUnifyWildcardRigid = forAllShrink arbitrary shrink $ \(scope, index) ->
   let thunk = ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT integerT
-   in withRenamedComp (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->
+      mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex index + 1)
+   in withRenamedComp mockScope (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->
         let argT = ThunkT . Comp0 $ tyvar (S scope) index :--:> ReturnT integerT
-         in withRenamedVals (Identity argT) $ \(Identity argT') ->
-              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT
+         in withRenamedVals mockScope (Identity argT) $ \(Identity argT') ->
+              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 1 ix0) :--:> ReturnT integerT
                   expected = Left . DoesNotUnify lhs $ argT'
                   actual = checkApp M.empty f [Just argT']
                in expected === actual
@@ -363,9 +376,9 @@
   let funThunkArgT = ThunkT $ Comp0 $ aT :--:> bT :--:> ReturnT (tyvar (S Z) ix0)
       funT = Comp1 $ funThunkArgT :--:> ReturnT (tyvar Z ix0)
       thunkT = ThunkT $ Comp0 $ aT :--:> bT :--:> ReturnT aT
-   in withRenamedComp funT $ \f ->
-        withRenamedVals (Identity thunkT) $ \(Identity argT) ->
-          withRenamedVals (Identity aT) $ \(Identity aT') ->
+   in withRenamedComp mempty funT $ \f ->
+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->
+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->
             let expected = Right aT'
                 actual = checkApp M.empty f [Just argT]
              in expected === actual
@@ -382,7 +395,7 @@
       arg3 = Datatype "Either" . Vector.fromList $ [BuiltinFlat UnitT, BuiltinFlat BoolT]
 
       expected = BuiltinFlat IntegerT
-  defaultLeftRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft
+  defaultLeftRenamed <- failLeft . runRenameM mempty . renameCompT $ defaultLeft
   actual <-
     either (assertFailure . show) pure $
       checkApp
@@ -411,8 +424,8 @@
           tyvar Z ix0
             :--:> ThunkT (Comp0 (BuiltinFlat BoolT :--:> ReturnT (tyvar (S Z) ix0)))
             :--:> ReturnT (tyvar Z ix0)
-  fnRenamed <- failLeft . runRenameM . renameCompT $ testFn
-  argRenamed <- failLeft . runRenameM . renameValT $ testArg
+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ testFn
+  argRenamed <- failLeft . runRenameM mempty . renameValT $ testArg
   result <-
     either (assertFailure . show) pure $
       checkApp tyAppTestDatatypes fnRenamed [Just argRenamed]
@@ -428,7 +441,7 @@
   let arg1 = Abstraction $ Unifiable ix0
       arg2 = ThunkT (Comp0 $ BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT))
       arg3 = Datatype "Either" . Vector.fromList $ [arg1, BuiltinFlat BoolT]
-  fnRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft
+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ defaultLeft
   actual <-
     either (assertFailure . show) pure $
       checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3])
@@ -445,7 +458,7 @@
       arg2 = BuiltinFlat BoolT
       arg3 = ThunkT $ Comp0 $ Abstraction (Rigid 1 ix0) :--:> BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT)
       arg4 = Datatype "Pair" (Vector.fromList [arg1, BuiltinFlat BoolT])
-  fnRenamed <- failLeft . runRenameM . renameCompT $ defaultPair
+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ defaultPair
   actual <-
     either (assertFailure . show) pure $
       checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3, arg4])
@@ -459,7 +472,7 @@
           Datatype "Maybe" (Vector.fromList [tyvar Z ix0])
             :--:> ReturnT (BuiltinFlat IntegerT)
       testArg = Datatype "Maybe" (Vector.fromList [BuiltinFlat BoolT])
-  fnRenamed <- failLeft . runRenameM . renameCompT $ testFn
+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ testFn
   result <-
     either (assertFailure . catchInsufficientArgs) pure $
       checkApp tyAppTestDatatypes fnRenamed [Just testArg]
@@ -478,7 +491,7 @@
         Comp1 $
           Datatype "Maybe" (Vector.singleton $ tyvar Z ix0)
             :--:> ReturnT (Datatype "Maybe" (Vector.singleton . Datatype "Maybe" . Vector.singleton $ tyvar Z ix0))
-  fnRenamed <- failLeft . runRenameM . renameCompT $ fn
+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ fn
   let arg = Datatype "Maybe" . Vector.singleton $ integerT
   let expected = Datatype "Maybe" . Vector.singleton . Datatype "Maybe" . Vector.singleton $ integerT
   case checkApp tyAppTestDatatypes fnRenamed [Just arg] of
@@ -494,9 +507,9 @@
       funThunkArg = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT (tyvar (S Z) ix0)
       funT = Comp1 $ funThunkArg :--:> ReturnT (tyvar Z ix0)
       thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT
-   in withRenamedComp funT $ \f ->
-        withRenamedVals (Identity thunkT) $ \(Identity argT) ->
-          withRenamedVals (Identity aT) $ \(Identity aT') ->
+   in withRenamedComp mempty funT $ \f ->
+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->
+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->
             let expected = Right aT'
                 actual = checkApp tyAppTestDatatypes f [Just argT]
              in expected === actual
@@ -510,9 +523,9 @@
       funThunkArg = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT
       funT = Comp0 $ funThunkArg :--:> ReturnT aT
       thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT
-   in withRenamedComp funT $ \f ->
-        withRenamedVals (Identity thunkT) $ \(Identity argT) ->
-          withRenamedVals (Identity aT) $ \(Identity aT') ->
+   in withRenamedComp mempty funT $ \f ->
+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->
+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->
             let expected = Right aT'
                 actual = checkApp tyAppTestDatatypes f [Just argT]
              in expected === actual
@@ -526,9 +539,9 @@
       funThunkArg = ThunkT $ Comp1 $ tyvar (S Z) ix0 :--:> maybeT :--:> ReturnT aT
       funT = Comp1 $ funThunkArg :--:> ReturnT aT
       thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT
-   in withRenamedComp funT $ \f ->
-        withRenamedVals (Identity thunkT) $ \(Identity argT) ->
-          withRenamedVals (Identity aT) $ \(Identity aT') ->
+   in withRenamedComp mempty funT $ \f ->
+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->
+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->
             let expected = Right aT'
                 actual = checkApp tyAppTestDatatypes f [Just argT]
              in expected === actual
@@ -543,9 +556,9 @@
       funThunkArg = ThunkT $ Comp0 $ maybeTConcrete :--:> ReturnT (tyvar (S Z) ix0)
       funT = Comp1 $ funThunkArg :--:> ReturnT (tyvar Z ix0)
       thunkT = ThunkT $ Comp0 $ maybeTConcrete :--:> ReturnT aT
-   in withRenamedComp funT $ \f ->
-        withRenamedVals (Identity thunkT) $ \(Identity argT) ->
-          withRenamedVals (Identity aT) $ \(Identity aT') ->
+   in withRenamedComp mempty funT $ \f ->
+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->
+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->
             let expected = Right aT'
                 actual = checkApp tyAppTestDatatypes f [Just argT]
              in expected === actual
@@ -581,19 +594,27 @@
       :--:> ReturnT (tyvar Z ix2)
 
 withRenamedComp ::
+  Vector.Vector Word32 ->
   CompT AbstractTy ->
   (CompT Renamed -> Property) ->
   Property
-withRenamedComp t f = case runRenameM . renameCompT $ t of
+withRenamedComp scope t f = case runRenameM scope . renameCompT $ t of
   Left err -> counterexample (show err) False
   Right t' -> f t'
 
 withRenamedVals ::
   forall (t :: Type -> Type).
   (Traversable t) =>
+  Vector.Vector Word32 ->
   t (ValT AbstractTy) ->
   (t (ValT Renamed) -> Property) ->
   Property
-withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of
+withRenamedVals scope vals f = case runRenameM scope . traverse renameValT $ vals of
   Left err -> counterexample (show err) False
   Right vals' -> f vals'
+
+ezTrueLevel :: Vector.Vector Word32 -> DeBruijn -> Index "tyvar" -> Int
+ezTrueLevel inherited db ix = case runRenameM inherited . renameValT $ tyvar db ix of
+  Left err' -> error ("ezTrueLevel: " <> show err')
+  Right (Abstraction (Rigid res _)) -> res
+  other -> error $ "ezTrueLevel didn't get a rigid, but got: " <> show other