diff --git a/cabal.project b/cabal.project
index 135da73..2a09431 100644
--- a/cabal.project
+++ b/cabal.project
@@ -1,5 +1,7 @@
 packages: ./covenant.cabal
 
+tests: true
+
 test-show-details: direct
 
 package covenant
diff --git a/covenant.cabal b/covenant.cabal
index a247bb1..e9e83fd 100644
--- a/covenant.cabal
+++ b/covenant.cabal
@@ -73,6 +73,13 @@ common test-lang
     -rtsopts
     -with-rtsopts=-N
 
+  build-depends:
+    QuickCheck ==2.15.0.1,
+    covenant,
+    tasty ==1.5.3,
+    tasty-hunit ==0.10.2,
+    tasty-quickcheck ==0.11.1,
+
 common bench-lang
   import: lang
   ghc-options: -O2
@@ -87,6 +94,7 @@ library
     Covenant.Constant
     Covenant.Ledger
     Covenant.Prim
+    Covenant.Type
 
   other-modules:
     Covenant.Internal.ASG
@@ -102,6 +110,7 @@ library
     containers >=0.6.8 && <0.8,
     enummapset ==0.7.3.0,
     mtl >=2.3.1 && <3,
+    nonempty-vector ==0.2.4,
     optics-core ==0.4.1.1,
     optics-th ==0.4.1,
     quickcheck-instances ==0.3.32,
@@ -113,4 +122,16 @@ library
   hs-source-dirs: src
 
 -- Tests
+test-suite renaming
+  import: test-lang
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  build-depends:
+    bimap,
+    nonempty-vector,
+    quickcheck-instances ==0.3.32,
+    vector,
+
+  hs-source-dirs: test/renaming
+
 -- Benchmarks
diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs
new file mode 100644
index 0000000..ee35a5f
--- /dev/null
+++ b/src/Covenant/Type.hs
@@ -0,0 +1,322 @@
+module Covenant.Type
+  ( AbstractTy (..),
+    Renamed (..),
+    CompT (..),
+    ValT (..),
+    BuiltinFlatT (..),
+    BuiltinNestedT (..),
+    RenameError (..),
+    renameValT,
+    renameCompT,
+    RenameM,
+    runRenameM,
+  )
+where
+
+import Control.Monad (unless)
+import Control.Monad.Except (ExceptT, MonadError (throwError), runExceptT)
+import Control.Monad.State.Strict (State, evalState, gets, modify)
+import Data.Coerce (coerce)
+import Data.Functor.Classes (Eq1 (liftEq))
+import Data.Kind (Type)
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Data.Vector.NonEmpty (NonEmptyVector)
+import Data.Vector.NonEmpty qualified as NonEmpty
+import Data.Word (Word64)
+
+-- | A type abstraction, using a DeBruijn index.
+--
+-- = Important note
+--
+-- This is a /relative/ representation: @'BoundAt' 1 0@ could refer to different
+-- things at different points in the ASG. Note that only the first field is a
+-- DeBruijn index: the second indicates which type variable bound at that
+-- \'level\' we mean.
+--
+-- @since 1.0.0
+data AbstractTy = BoundAt Word64 Word64
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Show
+    )
+
+-- | @since 1.0.0
+data Renamed
+  = -- | Set by an enclosing scope, and thus is essentially a
+    -- concrete type, we just don't know which. First field is its \'true
+    -- level\', second field is the index.
+    Rigid Int Word64
+  | -- | Can be unified with something, but must be consistent: that is, only one
+    -- unification for every instance. Field is this variable's positional index.
+    Unifiable Word64
+  | -- | /Must/ unify with everything, except with other distinct wildcards in the
+    -- same scope. First field is a unique /scope/ identifier, second is index.
+    Wildcard Word64 Word64
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Ord,
+      -- | @since 1.0.0
+      Show
+    )
+
+-- | A computation type, with abstractions indicated by the type argument. In
+-- pretty much any case imaginable, this would be either 'AbstractTy' (in the
+-- ASG), or 'Renamed' (after renaming).
+--
+-- = Important note
+--
+-- This type has a \'type abstraction boundary\' just before it: the first field
+-- indicates how many type variables it binds.
+--
+-- The /last/ entry in the 'NonEmpty' indicates the return type.
+--
+-- @since 1.0.0
+data CompT (a :: Type) = CompT Word64 (NonEmptyVector (ValT a))
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Show
+    )
+
+-- Note (Koz, 04/03/2025): We use this for testing to compare for structural
+-- similarity.
+instance Eq1 CompT where
+  {-# INLINEABLE liftEq #-}
+  liftEq f (CompT abses1 xs) (CompT abses2 ys) =
+    abses1 == abses2 && liftEq (liftEq f) xs ys
+
+-- | A value type, with abstractions indicated by the type argument. In pretty
+-- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or
+-- 'Renamed' (after renaming).
+--
+-- @ since 1.0.0
+data ValT (a :: Type)
+  = -- | An abstract type.
+    Abstraction a
+  | -- | A suspended computation.
+    ThunkT (CompT a)
+  | -- | A builtin type without any nesting.
+    BuiltinFlat BuiltinFlatT
+  | -- | A builtin type which is \'nested\'; something like lists, pairs etc.
+    BuiltinNested (BuiltinNestedT a)
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Show
+    )
+
+-- Note (Koz, 04/03/2025): We use this for testing to compare for structural
+-- similarity.
+instance Eq1 ValT where
+  {-# INLINEABLE liftEq #-}
+  liftEq f = \case
+    Abstraction abs1 -> \case
+      Abstraction abs2 -> f abs1 abs2
+      _ -> False
+    ThunkT t1 -> \case
+      ThunkT t2 -> liftEq f t1 t2
+      _ -> False
+    BuiltinFlat t1 -> \case
+      BuiltinFlat t2 -> t1 == t2
+      _ -> False
+    BuiltinNested t1 -> \case
+      BuiltinNested t2 -> liftEq f t1 t2
+      _ -> False
+
+-- | All builtin types that are \'flat\': that is, do not have other types
+-- \'nested inside them\'.
+data BuiltinFlatT
+  = UnitT
+  | BoolT
+  | IntegerT
+  | StringT
+  | ByteStringT
+  | BLS12_381_G1_ElementT
+  | BLS12_381_G2_ElementT
+  | BLS12_381_MlResultT
+  | DataT
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Show
+    )
+
+-- | Builtin types which have \'nested\' types. This is currently lists and
+-- pairs only.
+--
+-- = Important note
+--
+-- Both \'arms\' of this type have \'type abstraction boundaries\' just before
+-- them: their first field indicates how many type variables they bind.
+--
+-- While in truth, these types aren't /really/ polymorphic (as they cannot hold
+-- thunks, for example), we define them this way for now.
+--
+-- @since 1.0.0
+data BuiltinNestedT (a :: Type)
+  = ListT Word64 (ValT a)
+  | PairT Word64 (ValT a) (ValT a)
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Show
+    )
+
+-- Note (Koz, 04/03/2025): We use this for testing to compare for structural
+-- similarity.
+instance Eq1 BuiltinNestedT where
+  {-# INLINEABLE liftEq #-}
+  liftEq f = \case
+    ListT abses1 t1 -> \case
+      ListT abses2 t2 -> abses1 == abses2 && liftEq f t1 t2
+      _ -> False
+    PairT abses1 t11 t12 -> \case
+      PairT abses2 t21 t22 -> abses1 == abses2 && liftEq f t11 t21 && liftEq f t12 t22
+      _ -> False
+
+data RenameState = RenameState Word64 (Vector (Vector Bool, Word64))
+  deriving stock (Eq, Show)
+
+data RenameError
+  = InvalidAbstractionReference Int Word64
+  | IrrelevantAbstraction
+  deriving stock (Eq, Show)
+
+-- | A \'renaming monad\' which allows us to convert type representations from
+-- ones that use /relative/ abstraction labelling to /absolute/ abstraction
+-- labelling.
+--
+-- = Why this is necessary
+--
+-- Consider the following 'AbstractTy': @'BoundAtScope' 1 0@. The meaning of
+-- this is relative to where in a type it is positioned: it could be bound by a
+-- scope higher than our own, or something we can unify with. Because its
+-- meaning (namely, what it refers to) is situational, type checking becomes
+-- more difficult, although it has other advantages.
+--
+-- This monad allows us to convert this relative form into an absolute one. More
+-- specifically, the renamer does two things:
+--
+-- * Ensures that any given abstraction refers to one, and /only/ one, thing;
+-- and
+-- * Indicates which abstractions are unifiable, and which are (effectively)
+-- constant or fixed.
+--
+-- @since 1.0.0
+newtype RenameM (a :: Type)
+  = RenameM (ExceptT RenameError (State RenameState) a)
+  deriving
+    ( -- | @since 1.0.0
+      Functor,
+      -- | @since 1.0.0
+      Applicative,
+      -- | @since 1.0.0
+      Monad
+    )
+    via (ExceptT RenameError (State RenameState))
+
+runRenameM ::
+  forall (a :: Type).
+  RenameM a -> Either RenameError a
+runRenameM (RenameM comp) = evalState (runExceptT comp) . RenameState 0 $ Vector.empty
+
+renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
+renameCompT (CompT abses xs) = RenameM $ do
+  -- Step up a scope
+  modify
+    ( \(RenameState fresh tracker) ->
+        RenameState
+          (fresh + 1)
+          (Vector.cons (Vector.replicate (fromIntegral abses) False, fresh) tracker)
+    )
+  -- Rename, but only the arguments
+  renamedArgs <- Vector.generateM (NonEmpty.length xs - 1) (\i -> coerce . renameValT $ xs NonEmpty.! i)
+  -- Check the relevance condition is met
+  ourAbstractions <- gets (\(RenameState _ tracker) -> fst . Vector.head $ tracker)
+  unless (Vector.and ourAbstractions) (throwError IrrelevantAbstraction)
+  -- Check result type
+  renamedResult <- coerce . renameValT . NonEmpty.last $ xs
+  -- Roll back state
+  modify (\(RenameState fresh tracker) -> RenameState fresh (Vector.tail tracker))
+  -- Rebuild and return
+  pure . CompT abses . NonEmpty.snocV renamedArgs $ renamedResult
+
+renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
+renameValT = \case
+  Abstraction (BoundAt scope ix) ->
+    Abstraction
+      <$> RenameM
+        ( do
+            trueLevel <- gets (\(RenameState _ tracker) -> Vector.length tracker - fromIntegral scope)
+            scopeInfo <- gets (\(RenameState _ tracker) -> tracker Vector.!? fromIntegral scope)
+            case scopeInfo of
+              -- This variable is bound at a scope that encloses our starting
+              -- point. Thus, this variable is rigid.
+              Nothing -> pure . Rigid trueLevel $ ix
+              Just (varTracker, uniqueScopeId) -> case varTracker Vector.!? fromIntegral ix of
+                Nothing -> throwError . InvalidAbstractionReference trueLevel $ ix
+                Just beenUsed -> do
+                  -- Note that we've seen this particular variable
+                  unless
+                    beenUsed
+                    ( modify $ \(RenameState fresh tracker) ->
+                        let varTracker' = varTracker Vector.// [(fromIntegral ix, True)]
+                         in RenameState fresh $ tracker Vector.// [(fromIntegral scope, (varTracker', uniqueScopeId))]
+                    )
+                  pure $
+                    if trueLevel == 1
+                      -- If the true level is 1, this is a unifiable
+                      then Unifiable ix
+                      -- This variable is a wildcard
+                      else Wildcard uniqueScopeId ix
+        )
+  ThunkT t -> ThunkT <$> renameCompT t
+  BuiltinFlat t -> pure . BuiltinFlat $ t
+  BuiltinNested t ->
+    BuiltinNested <$> case t of
+      ListT abses t' -> RenameM $ do
+        -- Step up a scope
+        modify
+          ( \(RenameState fresh tracker) ->
+              RenameState
+                (fresh + 1)
+                (Vector.cons (Vector.replicate (fromIntegral abses) False, fresh) tracker)
+          )
+        -- Rename the inner type
+        renamed <- coerce . renameValT $ t'
+        -- Check the use condition is met
+        ourAbstractions <- gets (\(RenameState _ tracker) -> fst . Vector.head $ tracker)
+        unless (Vector.and ourAbstractions) (throwError IrrelevantAbstraction)
+        -- Roll back state
+        modify
+          (\(RenameState fresh tracker) -> RenameState fresh (Vector.tail tracker))
+        -- Rebuild and return
+        pure . ListT abses $ renamed
+      PairT abses t1 t2 -> RenameM $ do
+        -- Step up a scope
+        modify
+          ( \(RenameState fresh tracker) ->
+              RenameState
+                (fresh + 1)
+                (Vector.cons (Vector.replicate (fromIntegral abses) False, fresh) tracker)
+          )
+        -- Rename t1, then t2, without any scope shifts
+        renamed1 <- coerce . renameValT $ t1
+        renamed2 <- coerce . renameValT $ t2
+        -- Check the use condition is met
+        ourAbstractions <- gets (\(RenameState _ tracker) -> fst . Vector.head $ tracker)
+        unless (Vector.and ourAbstractions) (throwError IrrelevantAbstraction)
+        -- Roll back state
+        modify
+          (\(RenameState fresh tracker) -> RenameState fresh (Vector.tail tracker))
+        -- Rebuild and return
+        pure . PairT abses renamed1 $ renamed2
diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs
new file mode 100644
index 0000000..32582b0
--- /dev/null
+++ b/test/renaming/Main.hs
@@ -0,0 +1,327 @@
+{-# LANGUAGE OverloadedLists #-}
+
+module Main (main) where
+
+import Covenant.Type
+  ( AbstractTy (BoundAt),
+    BuiltinFlatT
+      ( BLS12_381_G1_ElementT,
+        BLS12_381_G2_ElementT,
+        BLS12_381_MlResultT,
+        BoolT,
+        ByteStringT,
+        DataT,
+        IntegerT,
+        StringT,
+        UnitT
+      ),
+    BuiltinNestedT (ListT, PairT),
+    CompT (CompT),
+    RenameError (InvalidAbstractionReference, IrrelevantAbstraction),
+    Renamed (Rigid, Unifiable, Wildcard),
+    ValT (Abstraction, BuiltinFlat, BuiltinNested, ThunkT),
+    renameCompT,
+    renameValT,
+    runRenameM,
+  )
+import Data.Coerce (coerce)
+import Data.Functor.Classes (liftEq)
+import Data.Kind (Type)
+import Data.Vector qualified as Vector
+import Data.Vector.NonEmpty qualified as NonEmpty
+import Test.QuickCheck
+  ( Arbitrary (arbitrary, shrink),
+    Gen,
+    Property,
+    elements,
+    forAllShrinkShow,
+    liftArbitrary,
+    oneof,
+    sized,
+  )
+import Test.QuickCheck.Instances.Vector ()
+import Test.Tasty (adjustOption, defaultMain, testGroup)
+import Test.Tasty.HUnit (assertBool, assertEqual, testCase)
+import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)
+
+main :: IO ()
+main =
+  defaultMain . adjustOption moreTests . testGroup "Renaming" $
+    [ testGroup
+        "Builtin flat types"
+        [ testCase "UnitT" $ testFlat UnitT,
+          testCase "BoolT" $ testFlat BoolT,
+          testCase "IntegerT" $ testFlat IntegerT,
+          testCase "StringT" $ testFlat StringT,
+          testCase "ByteStringT" $ testFlat ByteStringT,
+          testCase "G1ElementT" $ testFlat BLS12_381_G1_ElementT,
+          testCase "G2ElementT" $ testFlat BLS12_381_G2_ElementT,
+          testCase "MlResultT" $ testFlat BLS12_381_MlResultT,
+          testCase "DataT" $ testFlat DataT
+        ],
+      testProperty "Nested concrete types" propNestedConcrete,
+      testCase "forall a . a -> !a" testIdT,
+      testCase "forall a b . a -> b -> !a" testConstT,
+      testCase "forall a . a -> !(forall b . b -> !a)" testConstT2,
+      testCase "forall a . [a] -> !a" testHeadListT,
+      testCase "forall a b . (a, b) -> !b" testSndPairT,
+      testCase "forall a b . (a -> !b) -> [a] -> ![b]" testMapT,
+      testCase "forall a b . (a, b)" testPairT,
+      testGroup
+        "Irrelevance"
+        [ testCase "forall a b . a -> !a" testDodgyIdT,
+          testCase "forall a b . a -> !(b -> !a)" testDodgyConstT
+        ],
+      testGroup
+        "Non-existent abstractions"
+        [ testCase "forall a . b -> !a" testIndexingIdT
+        ]
+    ]
+  where
+    -- Note (Koz, 26/02/2025): By default, QuickCheck runs only 100 tests per
+    -- property, which is far to few. Using the method below, we can ensure that
+    -- we run a decent number of tests, while also permitting more than this to
+    -- be set via the CLI if we want.
+    moreTests :: QuickCheckTests -> QuickCheckTests
+    moreTests = max 10_000
+
+-- Tests and properties
+
+-- Checks that the given 'flat' type renames to itself.
+testFlat :: BuiltinFlatT -> IO ()
+testFlat t = do
+  let input = BuiltinFlat t
+  let result = runRenameM . 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
+   in case result of
+        Left _ -> False
+        Right actual -> liftEq (\_ _ -> False) t actual
+
+-- Checks that `forall a . a -> !a` correctly renames.
+testIdT :: IO ()
+testIdT = do
+  let idT = CompT 1 . NonEmpty.consV (Abstraction (BoundAt 0 0)) $ [Abstraction (BoundAt 0 0)]
+  let expected = CompT 1 . NonEmpty.consV (Abstraction (Unifiable 0)) $ [Abstraction (Unifiable 0)]
+  let result = runRenameM . renameCompT $ idT
+  assertRight (assertEqual "" expected) result
+
+-- Checks that `forall a b . a -> b -> !a` correctly renames.
+testConstT :: IO ()
+testConstT = do
+  let absA = BoundAt 0 0
+  let absB = BoundAt 0 1
+  let constT = CompT 2 . NonEmpty.consV (Abstraction absA) $ [Abstraction absB, Abstraction absA]
+  let expected = CompT 2 . NonEmpty.consV (Abstraction (Unifiable 0)) $ [Abstraction (Unifiable 1), Abstraction (Unifiable 0)]
+  let result = runRenameM . renameCompT $ constT
+  assertRight (assertEqual "" expected) result
+
+-- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames.
+testConstT2 :: IO ()
+testConstT2 = do
+  let constT =
+        CompT 1
+          . NonEmpty.consV
+            (Abstraction (BoundAt 0 0))
+          $ [ ThunkT . CompT 1 . NonEmpty.consV (Abstraction (BoundAt 0 0)) $ [Abstraction (BoundAt 1 0)]
+            ]
+  let expected =
+        CompT 1
+          . NonEmpty.consV
+            (Abstraction (Unifiable 0))
+          $ [ ThunkT . CompT 1 . NonEmpty.consV (Abstraction (Wildcard 1 0)) $ [Abstraction (Unifiable 0)]
+            ]
+  let result = runRenameM . renameCompT $ constT
+  assertRight (assertEqual "" expected) result
+
+-- Checks that `forall a . [a] -> !a` correctly renames.
+testHeadListT :: IO ()
+testHeadListT = do
+  let absA = BoundAt 0 0
+  let absAInner = BoundAt 1 0
+  let headListT =
+        CompT 1
+          . NonEmpty.consV (BuiltinNested (ListT 0 (Abstraction absAInner)))
+          $ [Abstraction absA]
+  let expected =
+        CompT 1
+          . NonEmpty.consV (BuiltinNested (ListT 0 (Abstraction (Unifiable 0))))
+          $ [Abstraction (Unifiable 0)]
+  let result = runRenameM . renameCompT $ headListT
+  assertRight (assertEqual "" expected) result
+
+-- Checks that `forall a b . (a, b) -> !b` correctly renames.
+testSndPairT :: IO ()
+testSndPairT = do
+  let sndPairT =
+        CompT 2
+          . NonEmpty.consV
+            (BuiltinNested (PairT 0 (Abstraction (BoundAt 1 0)) (Abstraction (BoundAt 1 1))))
+          $ [Abstraction (BoundAt 0 1)]
+  let expected =
+        CompT 2
+          . NonEmpty.consV
+            (BuiltinNested (PairT 0 (Abstraction (Unifiable 0)) (Abstraction (Unifiable 1))))
+          $ [Abstraction (Unifiable 1)]
+  let result = runRenameM . renameCompT $ sndPairT
+  assertRight (assertEqual "" expected) result
+
+-- Checks that `forall a b . (a -> !b) -> [a] -> !b` correctly renames.
+-- Also renames the thunk argument type _only_, to check that rigid arguments
+-- behave as expected.
+testMapT :: IO ()
+testMapT = do
+  let mapThunkT =
+        ThunkT
+          . CompT 0
+          . NonEmpty.consV (Abstraction (BoundAt 1 0))
+          $ [Abstraction (BoundAt 1 1)]
+  let mapT =
+        CompT 2
+          . NonEmpty.consV
+            mapThunkT
+          $ [ BuiltinNested (ListT 0 (Abstraction (BoundAt 1 0))),
+              BuiltinNested (ListT 0 (Abstraction (BoundAt 1 1)))
+            ]
+  let expectedMapThunkT =
+        ThunkT
+          . CompT 0
+          . NonEmpty.consV (Abstraction (Rigid 0 0))
+          $ [Abstraction (Rigid 0 1)]
+  let expectedMapT =
+        CompT 2
+          . NonEmpty.consV
+            (ThunkT . CompT 0 . NonEmpty.consV (Abstraction (Unifiable 0)) $ [Abstraction (Unifiable 1)])
+          $ [ BuiltinNested (ListT 0 (Abstraction (Unifiable 0))),
+              BuiltinNested (ListT 0 (Abstraction (Unifiable 1)))
+            ]
+  let resultThunkT = runRenameM . renameValT $ mapThunkT
+  assertRight (assertEqual "" expectedMapThunkT) resultThunkT
+  let resultMapT = runRenameM . renameCompT $ mapT
+  assertRight (assertEqual "" expectedMapT) resultMapT
+
+-- Checks that `forall a b . (a, b)` correctly renames.
+testPairT :: IO ()
+testPairT = do
+  let pairT =
+        BuiltinNested . PairT 2 (Abstraction (BoundAt 0 0)) . Abstraction . BoundAt 0 $ 1
+  let expected =
+        BuiltinNested . PairT 2 (Abstraction (Unifiable 0)) . Abstraction . Unifiable $ 1
+  let result = runRenameM . renameValT $ pairT
+  assertRight (assertEqual "" expected) result
+
+-- Checks that `forall a b . a -> !a` triggers the irrelevance checker.
+testDodgyIdT :: IO ()
+testDodgyIdT = do
+  let idT = CompT 2 . NonEmpty.consV (Abstraction (BoundAt 0 0)) $ [Abstraction (BoundAt 0 0)]
+  let result = runRenameM . renameCompT $ idT
+  case result of
+    Left IrrelevantAbstraction -> assertBool "" True
+    Left _ -> assertBool "wrong renaming error" False
+    _ -> assertBool "renaming succeeded when it should have failed" False
+
+-- Checks that `forall a b. a -> !(b -> !a)` triggers the irrelevance checker.
+testDodgyConstT :: IO ()
+testDodgyConstT = do
+  let constT =
+        CompT 2 . NonEmpty.consV (Abstraction (BoundAt 0 0)) $
+          [ ThunkT (CompT 0 . NonEmpty.consV (Abstraction (BoundAt 1 1)) $ [Abstraction (BoundAt 1 0)])
+          ]
+  let result = runRenameM . renameCompT $ constT
+  case result of
+    Left IrrelevantAbstraction -> assertBool "" True
+    Left _ -> assertBool "wrong renaming error" False
+    _ -> assertBool "renaming succeeded when it should have failed" False
+
+-- Checks that `forall a . b -> !a` triggers the variable indexing checker.
+testIndexingIdT :: IO ()
+testIndexingIdT = do
+  let t = CompT 1 . NonEmpty.consV (Abstraction (BoundAt 0 0)) $ [Abstraction (BoundAt 0 1)]
+  let result = runRenameM . renameCompT $ t
+  case result of
+    Left (InvalidAbstractionReference trueLevel ix) -> do
+      assertEqual "" trueLevel 1
+      assertEqual "" ix 1
+    Left _ -> assertBool "wrong renaming error" False
+    _ -> assertBool "renaming succeeded when it should have failed" False
+
+-- Helpers
+
+assertRight ::
+  forall (a :: Type) (b :: Type).
+  (b -> IO ()) ->
+  Either a b ->
+  IO ()
+assertRight f = \case
+  Left _ -> assertBool "renamer errored" False
+  Right actual -> f actual
+
+-- A newtype wrapper which generates only 'fully concrete' ValTs
+newtype Concrete = Concrete (ValT AbstractTy)
+  deriving (Eq) via (ValT AbstractTy)
+  deriving stock (Show)
+
+instance Arbitrary Concrete where
+  {-# INLINEABLE arbitrary #-}
+  arbitrary = Concrete <$> sized go
+    where
+      go :: Int -> Gen (ValT AbstractTy)
+      go size
+        | size <= 0 =
+            BuiltinFlat
+              <$> elements
+                [ UnitT,
+                  BoolT,
+                  IntegerT,
+                  StringT,
+                  ByteStringT,
+                  BLS12_381_G1_ElementT,
+                  BLS12_381_G2_ElementT,
+                  BLS12_381_MlResultT,
+                  DataT
+                ]
+        | otherwise =
+            oneof
+              [ pure . BuiltinFlat $ UnitT,
+                pure . BuiltinFlat $ BoolT,
+                pure . BuiltinFlat $ IntegerT,
+                pure . BuiltinFlat $ StringT,
+                pure . BuiltinFlat $ ByteStringT,
+                pure . BuiltinFlat $ BLS12_381_G1_ElementT,
+                pure . BuiltinFlat $ BLS12_381_G2_ElementT,
+                pure . BuiltinFlat $ BLS12_381_MlResultT,
+                pure . BuiltinFlat $ DataT,
+                BuiltinNested . ListT 0 <$> go (size `quot` 4),
+                BuiltinNested <$> (PairT 0 <$> go (size `quot` 4) <*> go (size `quot` 4)),
+                ThunkT . CompT 0 <$> (NonEmpty.consV <$> go (size `quot` 4) <*> liftArbitrary (go (size `quot` 4)))
+              ]
+  {-# INLINEABLE shrink #-}
+  shrink (Concrete v) =
+    Concrete <$> case v of
+      -- impossible
+      Abstraction _ -> []
+      ThunkT (CompT _ ts) ->
+        -- Note (Koz, 06/04/2025): This is needed because non-empty Vectors
+        -- don't have Arbitrary instances.
+        ThunkT . CompT 0 <$> do
+          let asList = NonEmpty.toList ts
+          shrunk <- fmap coerce . shrink . fmap Concrete $ asList
+          case shrunk of
+            [] -> []
+            x : xs -> pure (NonEmpty.consV x . Vector.fromList $ xs)
+      -- Can't shrink this
+      BuiltinFlat _ -> []
+      BuiltinNested t ->
+        BuiltinNested <$> case t of
+          ListT _ t' -> do
+            Concrete shrunk <- shrink (Concrete t')
+            pure . ListT 0 $ shrunk
+          PairT _ t1 t2 -> do
+            Concrete shrunkT1 <- shrink (Concrete t1)
+            Concrete shrunkT2 <- shrink (Concrete t2)
+            [PairT 0 shrunkT1 t2, PairT 0 t1 shrunkT2]