From 3f6c9527b382351cd94b0fcde55338068f4917d4 Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Tue, 4 Mar 2025 12:30:16 +1300
Subject: [PATCH 1/4] Renamer

---
 cabal.project         |   2 +
 covenant.cabal        |  15 +++
 src/Covenant/Type.hs  | 292 ++++++++++++++++++++++++++++++++++++++++++
 test/renaming/Main.hs | 280 ++++++++++++++++++++++++++++++++++++++++
 4 files changed, 589 insertions(+)
 create mode 100644 src/Covenant/Type.hs
 create mode 100644 test/renaming/Main.hs

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..4b6a970 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
@@ -113,4 +121,11 @@ library
   hs-source-dirs: src
 
 -- Tests
+test-suite renaming
+  import: test-lang
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  build-depends: bimap
+  hs-source-dirs: test/renaming
+
 -- Benchmarks
diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs
new file mode 100644
index 0000000..eaa9a61
--- /dev/null
+++ b/src/Covenant/Type.hs
@@ -0,0 +1,292 @@
+module Covenant.Type
+  ( AbstractTy (..),
+    Renamed (..),
+    CompT (..),
+    ValT (..),
+    BuiltinFlatT (..),
+    BuiltinNestedT (..),
+    renameValT,
+    renameCompT,
+    RenameM,
+    runRenameM,
+  )
+where
+
+import Control.Monad.Reader (ask, local)
+import Control.Monad.State.Strict (gets, modify)
+import Control.Monad.Trans.RWS.CPS (RWS, runRWS)
+import Data.Bimap (Bimap)
+import Data.Bimap qualified as Bimap
+import Data.Functor.Classes (Eq1 (liftEq))
+import Data.Kind (Type)
+import Data.List.NonEmpty (NonEmpty)
+import Data.Word (Word64, Word8)
+
+data AbstractTy = ForallAA | BoundAtScope Word8 Word8
+  deriving stock (Eq, Show)
+
+data Renamed = CanSet Word8 | Can'tSet Word64
+  deriving stock (Eq, Ord, Show)
+
+data CompT (a :: Type) = CompT Word8 (NonEmpty (ValT a))
+  deriving stock (Eq, Show)
+
+instance Eq1 CompT where
+  {-# INLINEABLE liftEq #-}
+  liftEq f (CompT abses1 xs) (CompT abses2 ys) =
+    abses1 == abses2 && liftEq (liftEq f) xs ys
+
+data ValT (a :: Type)
+  = Abstraction a
+  | ThunkT (CompT a)
+  | BuiltinFlat BuiltinFlatT
+  | BuiltinNested (BuiltinNestedT a)
+  deriving stock (Eq, Show)
+
+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
+
+data BuiltinFlatT
+  = UnitT
+  | BoolT
+  | IntegerT
+  | StringT
+  | ByteStringT
+  | BLS12_381_G1_ElementT
+  | BLS12_381_G2_ElementT
+  | BLS12_381_MlResultT
+  | DataT
+  deriving stock (Eq, Show)
+
+data BuiltinNestedT (a :: Type)
+  = ListT Word8 (ValT a)
+  | PairT Word8 (ValT a) (ValT a)
+  deriving stock (Eq, Show)
+
+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
+
+newtype RenameM (a :: Type) = RenameM (RWS Int () (Word64, Bimap (Int, Word8) Word64) a)
+  deriving (Functor, Applicative, Monad) via (RWS Int () (Word64, Bimap (Int, Word8) Word64))
+
+stepDown :: forall (a :: Type). RenameM a -> RenameM a
+stepDown (RenameM comp) = RenameM (local (+ 1) comp)
+
+renameAbstraction :: AbstractTy -> RenameM Renamed
+renameAbstraction absTy = RenameM $ do
+  currLevel <- ask
+  case absTy of
+    ForallAA ->
+      if currLevel == 0
+        then pure . CanSet $ 0
+        else do
+          renaming <- Can'tSet <$> gets fst
+          -- We bump the source of fresh names, but don't record an entry for
+          -- this; all such entries are completely unique, but on restoring
+          -- original names, will be the same.
+          modify $ \(source, tracker) -> (source + 1, tracker)
+          pure renaming
+    -- We need to determine the true level to see if:
+    --
+    -- 1. We can set this at all (aka, whether it's unfixed and touchable); and
+    -- 2. Whether we've seen this before.
+    BoundAtScope scope ix -> do
+      let trueLevel = currLevel - fromIntegral scope
+      if trueLevel == 0
+        then pure . CanSet $ ix
+        else do
+          -- Check if this is something we already renamed previously, and if
+          -- so, rename consistently.
+          priorRename <- gets (Bimap.lookup (trueLevel, ix) . snd)
+          case priorRename of
+            Nothing -> do
+              renaming <- gets fst
+              modify $ \(source, tracker) -> (source + 1, Bimap.insert (trueLevel, ix) renaming tracker)
+              pure . Can'tSet $ renaming
+            Just renameIx -> pure . Can'tSet $ renameIx
+
+runRenameM ::
+  forall (a :: Type).
+  RenameM a -> (Bimap (Int, Word8) Word64, a)
+runRenameM (RenameM comp) = case runRWS comp 0 (0, Bimap.empty) of
+  (res, (_, tracker), ()) -> (tracker, res)
+
+renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
+renameValT = \case
+  Abstraction absTy -> Abstraction <$> renameAbstraction absTy
+  -- We're crossing a type abstraction boundary, so bump the level
+  ThunkT t -> ThunkT <$> renameCompT t
+  BuiltinFlat t -> pure . BuiltinFlat $ t
+  BuiltinNested t ->
+    BuiltinNested <$> case t of
+      -- We're crossing a type abstraction boundary, so bump the level
+      ListT abses t' -> ListT abses <$> stepDown (renameValT t')
+      PairT abses t1 t2 ->
+        PairT abses
+          <$> stepDown (renameValT t1)
+          <*> stepDown (renameValT t2)
+
+renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
+renameCompT (CompT abses xs) = CompT abses <$> stepDown (traverse renameValT xs)
+
+{-
+data TypeApplyError
+  = ExcessArgs [ValT]
+  | InsufficientArgs (NonEmpty ValT)
+  | IrrelevantTyVar Word8
+  | CouldNotUnify ValT ValT
+
+applyArgs :: CompT -> [ValT] -> Either TypeApplyError ValT
+applyArgs (CompT comp) args = fmap fst . evalRWST (go comp args) 0 $ Map.empty
+  where
+    go :: NonEmpty ValT -> [ValT] -> RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ValT
+    go = \case
+      res :| [] -> \case
+        [] -> resolveResult res
+        args' -> throwError . ExcessArgs $ args'
+      required@(curr :| (rest : rests)) -> \case
+        [] -> throwError . InsufficientArgs $ required
+        arg : args' -> unify curr arg >> go (rest :| rests) args'
+
+resolveResult :: ValT -> RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ValT
+resolveResult = \case
+  absT@(AbsT scope ix) -> do
+    level <- ask
+    if scope == level
+      then
+        gets (Map.lookup ix) >>= \case
+          Nothing -> throwError . IrrelevantTyVar $ ix
+          Just t -> pure t
+      else pure absT -- Not ours, so nothing we can really do here
+  ThunkT (CompT comp) -> ThunkT . CompT <$> local (+ 1) (traverse resolveResult comp)
+  BuiltinFlat t -> pure $ BuiltinFlat t -- nothing to resolve, we're concrete
+  BuiltinNested t ->
+    local
+      (+ 1)
+      ( BuiltinNested <$> case t of
+          ListT t' -> ListT <$> local (+ 1) (resolveResult t')
+          PairT t1 t2 -> PairT <$> local (+ 1) (resolveResult t1) <*> local (+ 1) (resolveResult t2)
+      )
+
+unify :: ValT -> ValT -> RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ()
+unify lhs rhs = case lhs of
+  BuiltinFlat t1 -> case rhs of
+    BuiltinFlat t2 -> unless (t1 == t2) failToUnify
+    AbsT scope ix -> do
+      level <- ask
+      if scope == level
+        then
+          gets (Map.lookup ix) >>= \case
+            -- We've never seen this tyvar before, and it's our choice
+            -- Set it to match lhs and move on
+            -- We can do this safely without cycle-checking because we couldn't
+            -- possibly break anything with such an assignment
+            Nothing -> modify (Map.insert ix lhs)
+            Just t -> unify lhs t
+        else failToUnify
+    _ -> throwError . CouldNotUnify lhs $ rhs
+  ThunkT compT1 -> case rhs of
+    ThunkT compT2 -> _
+    AbsT scope ix -> _
+    _ -> failToUnify
+  BuiltinNested t1 -> case rhs of
+    BuiltinNested t2 -> case t1 of
+      ListT t1' -> local (+ 1) $ case t2 of
+        ListT t2' -> local (+ 1) $ unify t1' t2'
+        _ -> failToUnify
+      PairT t11 t12 -> local (+ 1) $ case t2 of
+        PairT t21 t22 -> local (+ 1) (unify t11 t21) >> local (+ 1) (unify t21 t22)
+        _ -> failToUnify
+    AbsT scope ix -> _
+    _ -> failToUnify
+  AbsT scope1 ix1 ->
+    asks (compare scope1) >>= \case
+      -- This tyvar is abstract in a way we don't control. Thus, it matches only
+      -- itself.
+      LT -> case rhs of
+        AbsT scope2 ix2 -> unless (scope1 == scope2 && ix1 == ix2) failToUnify
+        _ -> failToUnify
+      -- This tyvar is a reference to one of our abstractions.
+      EQ ->
+        gets (Map.lookup ix1) >>= \case
+          -- We've never seen this tyvar before and it's our choice.
+          -- Becasue rhs could be anything, we have to tread carefully to avoid
+          -- accidentally forming a cycle (meaning, failing an occurs check).
+          Nothing -> _
+          -- We've seen (and defined) this before, so just try unifying with it
+          -- instead.
+          Just t -> unify t rhs
+      -- This tyvar is 'pinned' by someone above our scope. Thus, it
+      -- matches only itself.
+      GT -> case rhs of
+        AbsT scope2 ix2 -> unless (scope1 == scope2 && ix1 == ix2) failToUnify
+        _ -> failToUnify
+  where
+    failToUnify :: RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ()
+    failToUnify = throwError . CouldNotUnify lhs $ rhs
+
+-- Helpers
+
+-- forall a b . (a -> !b) -> [a] -> ![b]
+mapT :: CompT
+mapT = CompT $ fType :| [xsType, resultType]
+  where
+    fType :: ValT
+    fType = ThunkT (CompT $ AbsT 1 0 :| [AbsT 1 1]) -- One scope above for both, first var, then second var
+    xsType :: ValT
+    xsType = BuiltinNested . ListT $ AbsT 2 0 -- Two scopes above, first var
+    resultType :: ValT
+    resultType = BuiltinNested . ListT $ AbsT 2 1 -- Two scopes above, second var
+
+-- forall a b . a -> b -> !a
+const2T :: CompT
+const2T = CompT $ AbsT 0 0 :| [AbsT 0 1, AbsT 0 0]
+
+-- forall a . a -> !(forall b . b -> !a)
+const1T :: CompT
+const1T = CompT $ AbsT 0 0 :| [ThunkT . CompT $ AbsT 0 0 :| [AbsT 1 0]]
+
+-- forall a . [a]
+faListOuter :: ValT
+faListOuter = BuiltinNested . ListT $ AbsT 1 0 -- 1 scope out, first variable
+
+-- [forall a . a]
+faListInner :: ValT
+faListInner = BuiltinNested . ListT $ AbsT 0 0 -- our scope, first variable
+
+-- forall a b . (a, b)
+pairOuter :: ValT
+pairOuter = BuiltinNested . PairT (AbsT 1 0) $ AbsT 1 1
+
+-- forall a . (a, forall b . b)
+pairRInner :: ValT
+pairRInner = BuiltinNested . PairT (AbsT 1 0) $ AbsT 0 0
+
+-- forall b . (forall a . a, b)
+pairLInner :: ValT
+pairLInner = BuiltinNested . PairT (AbsT 0 0) $ AbsT 1 0
+
+-- (forall a . a, forall b . b)
+pairInner :: ValT
+pairInner = BuiltinNested . PairT (AbsT 0 0) $ AbsT 0 0
+-}
diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs
new file mode 100644
index 0000000..1586fff
--- /dev/null
+++ b/test/renaming/Main.hs
@@ -0,0 +1,280 @@
+module Main (main) where
+
+import Covenant.Type
+  ( AbstractTy (BoundAtScope, ForallAA),
+    BuiltinFlatT
+      ( BLS12_381_G1_ElementT,
+        BLS12_381_G2_ElementT,
+        BLS12_381_MlResultT,
+        BoolT,
+        ByteStringT,
+        DataT,
+        IntegerT,
+        StringT,
+        UnitT
+      ),
+    BuiltinNestedT (ListT, PairT),
+    CompT (CompT),
+    Renamed (Can'tSet, CanSet),
+    ValT (Abstraction, BuiltinFlat, BuiltinNested, ThunkT),
+    renameCompT,
+    renameValT,
+    runRenameM,
+  )
+import Data.Bimap qualified as Bimap
+import Data.Coerce (coerce)
+import Data.Functor.Classes (liftEq)
+import Data.List.NonEmpty (NonEmpty ((:|)))
+import Data.List.NonEmpty qualified as NonEmpty
+import Test.QuickCheck
+  ( Arbitrary (arbitrary, shrink),
+    Gen,
+    Property,
+    elements,
+    forAllShrinkShow,
+    listOf,
+    oneof,
+    sized,
+    (.&&.),
+    (===),
+  )
+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" $
+    [ testCase "bare abstraction" testBareAbs,
+      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 "Rename id type" testIdT,
+      testCase "Rename const type" testConstT,
+      testCase "Rename HeadList type" testHeadListT,
+      testCase "Rename SndPair type" testSndPairT,
+      testCase "Rename map function over lists" testMapT,
+      testGroup
+        "Nested foralls"
+        [ testCase "forall a b . (a, b)" testPairTOuterOuter,
+          testCase "forall a . (a, forall b . b)" testPairTOuterInner,
+          testCase "forall b . (forall a . a, b)" testPairTInnerOuter,
+          testCase "(forall a . a, forall b . b)" testPairTInnerInner
+        ]
+    ]
+  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
+
+testBareAbs :: IO ()
+testBareAbs = do
+  let absTy = Abstraction ForallAA
+  let expected = Abstraction (CanSet 0)
+  let (tracker, actual) = runRenameM . renameValT $ absTy
+  assertEqual "" expected actual
+  let entry = Bimap.lookup (0, 0) tracker
+  assertEqual "" Nothing entry
+
+testFlat :: BuiltinFlatT -> IO ()
+testFlat t = do
+  let input = BuiltinFlat t
+  let (tracker, actual) = runRenameM . renameValT $ input
+  assertBool "" (liftEq (\_ _ -> False) input actual)
+  assertEqual "" Bimap.empty tracker
+
+propNestedConcrete :: Property
+propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) ->
+  let (tracker, actual) = runRenameM . renameValT $ t
+   in tracker === Bimap.empty .&&. liftEq (\_ _ -> False) t actual
+
+testIdT :: IO ()
+testIdT = do
+  let absA = BoundAtScope 1 0
+  let idT = CompT 1 $ Abstraction absA :| [Abstraction absA]
+  let expected = CompT 1 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 0)]
+  let (tracker, actual) = runRenameM . renameCompT $ idT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testConstT :: IO ()
+testConstT = do
+  let absA = BoundAtScope 1 0
+  let absB = BoundAtScope 1 1
+  let constT = CompT 2 $ Abstraction absA :| [Abstraction absB, Abstraction absA]
+  let expected = CompT 2 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 1), Abstraction (CanSet 0)]
+  let (tracker, actual) = runRenameM . renameCompT $ constT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testHeadListT :: IO ()
+testHeadListT = do
+  let absA = BoundAtScope 1 0
+  let absAInner = BoundAtScope 2 0
+  let headListT = CompT 1 $ BuiltinNested (ListT 0 (Abstraction absAInner)) :| [Abstraction absA]
+  let expected = CompT 1 $ BuiltinNested (ListT 0 (Abstraction (CanSet 0))) :| [Abstraction (CanSet 0)]
+  let (tracker, actual) = runRenameM . renameCompT $ headListT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testSndPairT :: IO ()
+testSndPairT = do
+  let sndPairT =
+        CompT 2 $
+          BuiltinNested (PairT 0 (Abstraction (BoundAtScope 2 0)) (Abstraction (BoundAtScope 2 1)))
+            :| [Abstraction (BoundAtScope 1 1)]
+  let expected =
+        CompT 2 $
+          BuiltinNested (PairT 0 (Abstraction (CanSet 0)) (Abstraction (CanSet 1)))
+            :| [Abstraction (CanSet 1)]
+  let (tracker, actual) = runRenameM . renameCompT $ sndPairT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testMapT :: IO ()
+testMapT = do
+  let mapThunkT = ThunkT . CompT 0 $ Abstraction (BoundAtScope 2 0) :| [Abstraction (BoundAtScope 2 1)]
+  let mapT =
+        CompT 2 $
+          mapThunkT
+            :| [ BuiltinNested (ListT 0 (Abstraction (BoundAtScope 2 0))),
+                 BuiltinNested (ListT 0 (Abstraction (BoundAtScope 2 1)))
+               ]
+  let expectedMapThunkT = ThunkT . CompT 0 $ Abstraction (Can'tSet 0) :| [Abstraction (Can'tSet 1)]
+  let expectedThunkT = ThunkT . CompT 0 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 1)]
+  let expectedMapT =
+        CompT 2 $
+          expectedThunkT
+            :| [ BuiltinNested (ListT 0 (Abstraction (CanSet 0))),
+                 BuiltinNested (ListT 0 (Abstraction (CanSet 1)))
+               ]
+  let (trackerThunkT, actualThunkT) = runRenameM . renameValT $ mapThunkT
+  assertEqual "" expectedMapThunkT actualThunkT
+  let expectedThunkTracker = Bimap.fromList [((-1, 0), 0), ((-1, 1), 1)]
+  assertEqual "" expectedThunkTracker trackerThunkT
+  let (trackerMapT, actualMapT) = runRenameM . renameCompT $ mapT
+  assertEqual "" expectedMapT actualMapT
+  assertEqual "" Bimap.empty trackerMapT
+
+testPairTOuterOuter :: IO ()
+testPairTOuterOuter = do
+  let pairT =
+        BuiltinNested . PairT 2 (Abstraction (BoundAtScope 1 0)) . Abstraction . BoundAtScope 1 $ 1
+  let expected =
+        BuiltinNested . PairT 2 (Abstraction (CanSet 0)) . Abstraction . CanSet $ 1
+  let (tracker, actual) = runRenameM . renameValT $ pairT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testPairTInnerOuter :: IO ()
+testPairTInnerOuter = do
+  let pairT =
+        BuiltinNested . PairT 1 (Abstraction ForallAA) . Abstraction . BoundAtScope 1 $ 0
+  let expected =
+        BuiltinNested . PairT 1 (Abstraction (Can'tSet 0)) . Abstraction . CanSet $ 0
+  let (tracker, actual) = runRenameM . renameValT $ pairT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testPairTOuterInner :: IO ()
+testPairTOuterInner = do
+  let pairT =
+        BuiltinNested . PairT 1 (Abstraction (BoundAtScope 1 0)) . Abstraction $ ForallAA
+  let expected =
+        BuiltinNested . PairT 1 (Abstraction (CanSet 0)) . Abstraction . Can'tSet $ 0
+  let (tracker, actual) = runRenameM . renameValT $ pairT
+  assertEqual "" expected actual
+  assertEqual "" Bimap.empty tracker
+
+testPairTInnerInner :: IO ()
+testPairTInnerInner = do
+  let pairT =
+        BuiltinNested . PairT 0 (Abstraction ForallAA) . Abstraction $ ForallAA
+  let expected =
+        BuiltinNested . PairT 0 (Abstraction (Can'tSet 0)) . Abstraction . Can'tSet $ 1
+  let (tracker, actual) = runRenameM . renameValT $ pairT
+  assertEqual "" expected actual
+  let expectedTracker = Bimap.empty
+  assertEqual "" expectedTracker tracker
+
+-- Helpers
+
+-- 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 <$> ((:|) <$> go (size `quot` 4) <*> listOf (go (size `quot` 4)))
+              ]
+  {-# INLINEABLE shrink #-}
+  shrink (Concrete v) =
+    Concrete <$> case v of
+      -- impossible
+      Abstraction _ -> []
+      ThunkT (CompT _ ts) ->
+        -- Note (Koz, 26/02/2025): This is needed because, for some weird
+        -- reason, NonEmpty lacks an Arbitrary instance.
+        ThunkT . CompT 0 <$> do
+          let asList = NonEmpty.toList ts
+          shrunk <- fmap coerce . shrink . fmap Concrete $ asList
+          case shrunk of
+            [] -> []
+            x : xs -> pure (x :| 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]

From 67b0ccd98c84904ee31327761cd8119429a0f9b3 Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Tue, 4 Mar 2025 13:38:41 +1300
Subject: [PATCH 2/4] Documentation, cleanup

---
 src/Covenant/Type.hs  | 325 +++++++++++++++++++++---------------------
 test/renaming/Main.hs |  26 ++++
 2 files changed, 190 insertions(+), 161 deletions(-)

diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs
index eaa9a61..31f3e87 100644
--- a/src/Covenant/Type.hs
+++ b/src/Covenant/Type.hs
@@ -20,29 +20,105 @@ import Data.Bimap qualified as Bimap
 import Data.Functor.Classes (Eq1 (liftEq))
 import Data.Kind (Type)
 import Data.List.NonEmpty (NonEmpty)
-import Data.Word (Word64, Word8)
+import Data.Word (Word64)
 
-data AbstractTy = ForallAA | BoundAtScope Word8 Word8
-  deriving stock (Eq, Show)
+-- | A type abstraction.
+--
+-- = Important note
+--
+-- There is an implicit \'scope boundary\' in front of this. Thus, this
+-- construction can mean either:
+--
+-- * An untouchable (effectively @forall a . a@)
+-- * A single toplevel variable
+-- * A reference to another binding scope and index
+--
+-- The 'ForallAA' constructor plays the first two roles; which depends on the
+-- context. 'BoundAtScope' indicates instead how many scopes away it was bound,
+-- and also which binding we're referring to (first, second, etc).
+--
+-- @since 1.0.0
+data AbstractTy
+  = ForallAA
+  | BoundAtScope Word64 Word64
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Show
+    )
 
-data Renamed = CanSet Word8 | Can'tSet Word64
-  deriving stock (Eq, Ord, Show)
+-- | A renamed type abstraction. We separate them into two kinds:
+--
+-- * Ones we can decide on (that is, variables in the context of unification);
+-- and
+-- * Ones we /cannot/ decide on (either fixed in higher scopes than ours, or
+-- untouchable).
+--
+-- We use 'CanSet' plus an index for the first case; the second case is a unique
+-- index assigned by the renamer.
+--
+-- @since 1.0.0
+data Renamed = CanSet Word64 | Can'tSet Word64
+  deriving stock
+    ( -- | @since 1.0.0
+      Eq,
+      -- | @since 1.0.0
+      Ord,
+      -- | @since 1.0.0
+      Show
+    )
 
-data CompT (a :: Type) = CompT Word8 (NonEmpty (ValT a))
-  deriving stock (Eq, 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 (NonEmpty (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)
-  = Abstraction a
-  | ThunkT (CompT a)
-  | BuiltinFlat BuiltinFlatT
-  | BuiltinNested (BuiltinNestedT a)
-  deriving stock (Eq, Show)
+  = -- | 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
@@ -59,6 +135,8 @@ instance Eq1 ValT where
       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
@@ -69,13 +147,37 @@ data BuiltinFlatT
   | BLS12_381_G2_ElementT
   | BLS12_381_MlResultT
   | DataT
-  deriving stock (Eq, Show)
+  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 Word8 (ValT a)
-  | PairT Word8 (ValT a) (ValT a)
-  deriving stock (Eq, Show)
+  = 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
@@ -86,12 +188,44 @@ instance Eq1 BuiltinNestedT where
       PairT abses2 t21 t22 -> abses1 == abses2 && liftEq f t11 t21 && liftEq f t12 t22
       _ -> False
 
-newtype RenameM (a :: Type) = RenameM (RWS Int () (Word64, Bimap (Int, Word8) Word64) a)
-  deriving (Functor, Applicative, Monad) via (RWS Int () (Word64, Bimap (Int, Word8) Word64))
+-- | 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 (RWS Int () (Word64, Bimap (Int, Word64) Word64) a)
+  deriving
+    ( -- | @since 1.0.0
+      Functor,
+      -- | @since 1.0.0
+      Applicative,
+      -- | @since 1.0.0
+      Monad
+    )
+    via (RWS Int () (Word64, Bimap (Int, Word64) Word64))
 
+-- Increase the scope by one level.
 stepDown :: forall (a :: Type). RenameM a -> RenameM a
 stepDown (RenameM comp) = RenameM (local (+ 1) comp)
 
+-- Given an abstraction in relative form, transform it into an abstraction in
+-- absolute form.
 renameAbstraction :: AbstractTy -> RenameM Renamed
 renameAbstraction absTy = RenameM $ do
   currLevel <- ask
@@ -125,12 +259,20 @@ renameAbstraction absTy = RenameM $ do
               pure . Can'tSet $ renaming
             Just renameIx -> pure . Can'tSet $ renameIx
 
+-- | Run a renaming computation, while also producing the mapping of any fixed
+-- abstractions to their original (non-relative) scope and position.
+--
+-- @since 1.0.0
 runRenameM ::
   forall (a :: Type).
-  RenameM a -> (Bimap (Int, Word8) Word64, a)
+  RenameM a -> (Bimap (Int, Word64) Word64, a)
 runRenameM (RenameM comp) = case runRWS comp 0 (0, Bimap.empty) of
   (res, (_, tracker), ()) -> (tracker, res)
 
+-- | Given a value type with relative abstractions, produce the same value type,
+-- but with absolute abstractions.
+--
+-- @since 1.0.0
 renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
 renameValT = \case
   Abstraction absTy -> Abstraction <$> renameAbstraction absTy
@@ -146,147 +288,8 @@ renameValT = \case
           <$> stepDown (renameValT t1)
           <*> stepDown (renameValT t2)
 
+-- | As 'renameValT', but for computation types.
+--
+-- @since 1.0.0
 renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
 renameCompT (CompT abses xs) = CompT abses <$> stepDown (traverse renameValT xs)
-
-{-
-data TypeApplyError
-  = ExcessArgs [ValT]
-  | InsufficientArgs (NonEmpty ValT)
-  | IrrelevantTyVar Word8
-  | CouldNotUnify ValT ValT
-
-applyArgs :: CompT -> [ValT] -> Either TypeApplyError ValT
-applyArgs (CompT comp) args = fmap fst . evalRWST (go comp args) 0 $ Map.empty
-  where
-    go :: NonEmpty ValT -> [ValT] -> RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ValT
-    go = \case
-      res :| [] -> \case
-        [] -> resolveResult res
-        args' -> throwError . ExcessArgs $ args'
-      required@(curr :| (rest : rests)) -> \case
-        [] -> throwError . InsufficientArgs $ required
-        arg : args' -> unify curr arg >> go (rest :| rests) args'
-
-resolveResult :: ValT -> RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ValT
-resolveResult = \case
-  absT@(AbsT scope ix) -> do
-    level <- ask
-    if scope == level
-      then
-        gets (Map.lookup ix) >>= \case
-          Nothing -> throwError . IrrelevantTyVar $ ix
-          Just t -> pure t
-      else pure absT -- Not ours, so nothing we can really do here
-  ThunkT (CompT comp) -> ThunkT . CompT <$> local (+ 1) (traverse resolveResult comp)
-  BuiltinFlat t -> pure $ BuiltinFlat t -- nothing to resolve, we're concrete
-  BuiltinNested t ->
-    local
-      (+ 1)
-      ( BuiltinNested <$> case t of
-          ListT t' -> ListT <$> local (+ 1) (resolveResult t')
-          PairT t1 t2 -> PairT <$> local (+ 1) (resolveResult t1) <*> local (+ 1) (resolveResult t2)
-      )
-
-unify :: ValT -> ValT -> RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ()
-unify lhs rhs = case lhs of
-  BuiltinFlat t1 -> case rhs of
-    BuiltinFlat t2 -> unless (t1 == t2) failToUnify
-    AbsT scope ix -> do
-      level <- ask
-      if scope == level
-        then
-          gets (Map.lookup ix) >>= \case
-            -- We've never seen this tyvar before, and it's our choice
-            -- Set it to match lhs and move on
-            -- We can do this safely without cycle-checking because we couldn't
-            -- possibly break anything with such an assignment
-            Nothing -> modify (Map.insert ix lhs)
-            Just t -> unify lhs t
-        else failToUnify
-    _ -> throwError . CouldNotUnify lhs $ rhs
-  ThunkT compT1 -> case rhs of
-    ThunkT compT2 -> _
-    AbsT scope ix -> _
-    _ -> failToUnify
-  BuiltinNested t1 -> case rhs of
-    BuiltinNested t2 -> case t1 of
-      ListT t1' -> local (+ 1) $ case t2 of
-        ListT t2' -> local (+ 1) $ unify t1' t2'
-        _ -> failToUnify
-      PairT t11 t12 -> local (+ 1) $ case t2 of
-        PairT t21 t22 -> local (+ 1) (unify t11 t21) >> local (+ 1) (unify t21 t22)
-        _ -> failToUnify
-    AbsT scope ix -> _
-    _ -> failToUnify
-  AbsT scope1 ix1 ->
-    asks (compare scope1) >>= \case
-      -- This tyvar is abstract in a way we don't control. Thus, it matches only
-      -- itself.
-      LT -> case rhs of
-        AbsT scope2 ix2 -> unless (scope1 == scope2 && ix1 == ix2) failToUnify
-        _ -> failToUnify
-      -- This tyvar is a reference to one of our abstractions.
-      EQ ->
-        gets (Map.lookup ix1) >>= \case
-          -- We've never seen this tyvar before and it's our choice.
-          -- Becasue rhs could be anything, we have to tread carefully to avoid
-          -- accidentally forming a cycle (meaning, failing an occurs check).
-          Nothing -> _
-          -- We've seen (and defined) this before, so just try unifying with it
-          -- instead.
-          Just t -> unify t rhs
-      -- This tyvar is 'pinned' by someone above our scope. Thus, it
-      -- matches only itself.
-      GT -> case rhs of
-        AbsT scope2 ix2 -> unless (scope1 == scope2 && ix1 == ix2) failToUnify
-        _ -> failToUnify
-  where
-    failToUnify :: RWST Word8 () (Map Word8 ValT) (Either TypeApplyError) ()
-    failToUnify = throwError . CouldNotUnify lhs $ rhs
-
--- Helpers
-
--- forall a b . (a -> !b) -> [a] -> ![b]
-mapT :: CompT
-mapT = CompT $ fType :| [xsType, resultType]
-  where
-    fType :: ValT
-    fType = ThunkT (CompT $ AbsT 1 0 :| [AbsT 1 1]) -- One scope above for both, first var, then second var
-    xsType :: ValT
-    xsType = BuiltinNested . ListT $ AbsT 2 0 -- Two scopes above, first var
-    resultType :: ValT
-    resultType = BuiltinNested . ListT $ AbsT 2 1 -- Two scopes above, second var
-
--- forall a b . a -> b -> !a
-const2T :: CompT
-const2T = CompT $ AbsT 0 0 :| [AbsT 0 1, AbsT 0 0]
-
--- forall a . a -> !(forall b . b -> !a)
-const1T :: CompT
-const1T = CompT $ AbsT 0 0 :| [ThunkT . CompT $ AbsT 0 0 :| [AbsT 1 0]]
-
--- forall a . [a]
-faListOuter :: ValT
-faListOuter = BuiltinNested . ListT $ AbsT 1 0 -- 1 scope out, first variable
-
--- [forall a . a]
-faListInner :: ValT
-faListInner = BuiltinNested . ListT $ AbsT 0 0 -- our scope, first variable
-
--- forall a b . (a, b)
-pairOuter :: ValT
-pairOuter = BuiltinNested . PairT (AbsT 1 0) $ AbsT 1 1
-
--- forall a . (a, forall b . b)
-pairRInner :: ValT
-pairRInner = BuiltinNested . PairT (AbsT 1 0) $ AbsT 0 0
-
--- forall b . (forall a . a, b)
-pairLInner :: ValT
-pairLInner = BuiltinNested . PairT (AbsT 0 0) $ AbsT 1 0
-
--- (forall a . a, forall b . b)
-pairInner :: ValT
-pairInner = BuiltinNested . PairT (AbsT 0 0) $ AbsT 0 0
--}
diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs
index 1586fff..0ae86fb 100644
--- a/test/renaming/Main.hs
+++ b/test/renaming/Main.hs
@@ -82,6 +82,8 @@ main =
 
 -- Tests and properties
 
+-- Checks that `forall a . a` renames correctly. Also verifies that there are no
+-- fixed bindings in the tracker afterwards.
 testBareAbs :: IO ()
 testBareAbs = do
   let absTy = Abstraction ForallAA
@@ -91,6 +93,8 @@ testBareAbs = do
   let entry = Bimap.lookup (0, 0) tracker
   assertEqual "" Nothing entry
 
+-- Checks that the given 'flat' type renames to itself. Also verifies that there
+-- are no fixed bindings in the tracker afterwards.
 testFlat :: BuiltinFlatT -> IO ()
 testFlat t = do
   let input = BuiltinFlat t
@@ -98,11 +102,16 @@ testFlat t = do
   assertBool "" (liftEq (\_ _ -> False) input actual)
   assertEqual "" Bimap.empty tracker
 
+-- Checks that for any 'fully concretified' type (nested or not), renaming
+-- changes nothing. Also verifies that there are no fixed bindings in the
+-- tracker afterwards.
 propNestedConcrete :: Property
 propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) ->
   let (tracker, actual) = runRenameM . renameValT $ t
    in tracker === Bimap.empty .&&. liftEq (\_ _ -> False) t actual
 
+-- Checks that `forall a . a -> !a` correctly renames. Also verifies there are no
+-- fixed bindings in the tracker afterwards.
 testIdT :: IO ()
 testIdT = do
   let absA = BoundAtScope 1 0
@@ -112,6 +121,8 @@ testIdT = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall a b . a -> b -> !a` correctly renames. Also verifies that
+-- there are no fixed bindings in the tracker afterwards.
 testConstT :: IO ()
 testConstT = do
   let absA = BoundAtScope 1 0
@@ -122,6 +133,8 @@ testConstT = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall a . [a] -> !a` correctly renames. Also verifies that
+-- there are no fixed bindings in the tracker afterwards.
 testHeadListT :: IO ()
 testHeadListT = do
   let absA = BoundAtScope 1 0
@@ -132,6 +145,8 @@ testHeadListT = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall a b . (a, b) -> !b` correctly renames. Also verifies that
+-- there are no fixed bindings in the tracker afterwards.
 testSndPairT :: IO ()
 testSndPairT = do
   let sndPairT =
@@ -146,6 +161,9 @@ testSndPairT = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall a b . (a -> !b) -> [a] -> !b` correctly renames with
+-- nothing left in the tracker. Also renames the thunk argument type _only_, and
+-- checks that two fixed bindings remain in the tracker afterwards.
 testMapT :: IO ()
 testMapT = do
   let mapThunkT = ThunkT . CompT 0 $ Abstraction (BoundAtScope 2 0) :| [Abstraction (BoundAtScope 2 1)]
@@ -171,6 +189,8 @@ testMapT = do
   assertEqual "" expectedMapT actualMapT
   assertEqual "" Bimap.empty trackerMapT
 
+-- Checks that `forall a b . (a, b)` correctly renames with nothing left in the
+-- tracker.
 testPairTOuterOuter :: IO ()
 testPairTOuterOuter = do
   let pairT =
@@ -181,6 +201,8 @@ testPairTOuterOuter = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall b . (forall a . a, b)` renames correctly with nothing
+-- left in the tracker.
 testPairTInnerOuter :: IO ()
 testPairTInnerOuter = do
   let pairT =
@@ -191,6 +213,8 @@ testPairTInnerOuter = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall a . (a, forall b . b)` renames correctly with nothing
+-- left in the tracker.
 testPairTOuterInner :: IO ()
 testPairTOuterInner = do
   let pairT =
@@ -201,6 +225,8 @@ testPairTOuterInner = do
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `(forall a . a, forall b . b)` renames correctly with nothing
+-- left in the tracker. Also verifies that the two fixed renames are distinct.
 testPairTInnerInner :: IO ()
 testPairTInnerInner = do
   let pairT =

From 19a98a71c626fa0af4cd45a16034f5951959e93f Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Wed, 5 Mar 2025 11:38:32 +1300
Subject: [PATCH 3/4] Fix off-by-one, forbid certain constructions that make no
 sense

---
 src/Covenant/Type.hs  |  93 +++++++++++++++++----------------
 test/renaming/Main.hs | 118 +++++++++++++++---------------------------
 2 files changed, 88 insertions(+), 123 deletions(-)

diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs
index 31f3e87..95b5991 100644
--- a/src/Covenant/Type.hs
+++ b/src/Covenant/Type.hs
@@ -12,7 +12,7 @@ module Covenant.Type
   )
 where
 
-import Control.Monad.Reader (ask, local)
+import Control.Monad.Reader (asks, local)
 import Control.Monad.State.Strict (gets, modify)
 import Control.Monad.Trans.RWS.CPS (RWS, runRWS)
 import Data.Bimap (Bimap)
@@ -22,25 +22,17 @@ import Data.Kind (Type)
 import Data.List.NonEmpty (NonEmpty)
 import Data.Word (Word64)
 
--- | A type abstraction.
+-- | A type abstraction, using a DeBruijn index.
 --
 -- = Important note
 --
--- There is an implicit \'scope boundary\' in front of this. Thus, this
--- construction can mean either:
---
--- * An untouchable (effectively @forall a . a@)
--- * A single toplevel variable
--- * A reference to another binding scope and index
---
--- The 'ForallAA' constructor plays the first two roles; which depends on the
--- context. 'BoundAtScope' indicates instead how many scopes away it was bound,
--- and also which binding we're referring to (first, second, etc).
+-- 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
-  = ForallAA
-  | BoundAtScope Word64 Word64
+data AbstractTy = BoundAt Word64 Word64
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -220,6 +212,16 @@ newtype RenameM (a :: Type) = RenameM (RWS Int () (Word64, Bimap (Int, Word64) W
     )
     via (RWS Int () (Word64, Bimap (Int, Word64) Word64))
 
+-- Note (Koz, 05/04/2025): We could check that any type abstractions we have in
+-- our view (meaning, not bound higher than us) do not reference tyvars that
+-- don't exist, as every 'type abstraction boundary' specifies how many
+-- variables it binds. This would mean the renamer could fail if it encounters
+-- an impossible situation (such as asking for the index-3 type variable from a
+-- scope that only binds 2). This might not be worth it however, as we would
+-- have no way of checkin anything that comes from 'above us': namely, we would
+-- have to blindly trust any scopes that enclose us and that those type indexes
+-- are sensible.
+
 -- Increase the scope by one level.
 stepDown :: forall (a :: Type). RenameM a -> RenameM a
 stepDown (RenameM comp) = RenameM (local (+ 1) comp)
@@ -227,37 +229,36 @@ stepDown (RenameM comp) = RenameM (local (+ 1) comp)
 -- Given an abstraction in relative form, transform it into an abstraction in
 -- absolute form.
 renameAbstraction :: AbstractTy -> RenameM Renamed
-renameAbstraction absTy = RenameM $ do
-  currLevel <- ask
-  case absTy of
-    ForallAA ->
-      if currLevel == 0
-        then pure . CanSet $ 0
-        else do
-          renaming <- Can'tSet <$> gets fst
-          -- We bump the source of fresh names, but don't record an entry for
-          -- this; all such entries are completely unique, but on restoring
-          -- original names, will be the same.
-          modify $ \(source, tracker) -> (source + 1, tracker)
-          pure renaming
-    -- We need to determine the true level to see if:
-    --
-    -- 1. We can set this at all (aka, whether it's unfixed and touchable); and
-    -- 2. Whether we've seen this before.
-    BoundAtScope scope ix -> do
-      let trueLevel = currLevel - fromIntegral scope
-      if trueLevel == 0
-        then pure . CanSet $ ix
-        else do
-          -- Check if this is something we already renamed previously, and if
-          -- so, rename consistently.
-          priorRename <- gets (Bimap.lookup (trueLevel, ix) . snd)
-          case priorRename of
-            Nothing -> do
-              renaming <- gets fst
-              modify $ \(source, tracker) -> (source + 1, Bimap.insert (trueLevel, ix) renaming tracker)
-              pure . Can'tSet $ renaming
-            Just renameIx -> pure . Can'tSet $ renameIx
+renameAbstraction (BoundAt scope ix) = RenameM $ do
+  -- DeBruijn scope indices are relative to our own position. They could
+  -- potentially refer to stuff bound 'above' us (meaning they're fixed by our
+  -- callers), or stuff bound 'below' us (meaning that they're untouchable). As
+  -- the renamer walks, every time we cross a 'type abstraction barrier', we
+  -- have to take into account that, to reference something, we need an index
+  -- one higher.
+  --
+  -- We thus change the 'relative' indexes to absolute ones, choosing the
+  -- starting point as zero. Thus, we get the following scheme:
+  --
+  -- \* After one forall, scope 0 means 'can change': 1 - 0 = 1
+  -- \* After two foralls, scope 1 means 'can change': 2 - 1 = 1
+  -- \* After three foralls, scope 2 means 'can change': 3 - 2 = 1
+  --
+  -- Thus, we must check whether the difference between the current level and
+  -- the DeBruijn index is exactly 1. We call this the 'true level', although
+  -- it's not the best name.
+  trueLevel <- asks (\currentLevel -> currentLevel - fromIntegral scope)
+  if trueLevel == 1
+    then pure . CanSet $ ix
+    else do
+      -- Check if we already renamed this thing, and if so, rename consistently.
+      priorRename <- gets (Bimap.lookup (trueLevel, ix) . snd)
+      case priorRename of
+        Nothing -> do
+          renaming <- gets fst
+          modify $ \(source, tracker) -> (source + 1, Bimap.insert (trueLevel, ix) renaming tracker)
+          pure . Can'tSet $ renaming
+        Just renameIx -> pure . Can'tSet $ renameIx
 
 -- | Run a renaming computation, while also producing the mapping of any fixed
 -- abstractions to their original (non-relative) scope and position.
diff --git a/test/renaming/Main.hs b/test/renaming/Main.hs
index 0ae86fb..17c827a 100644
--- a/test/renaming/Main.hs
+++ b/test/renaming/Main.hs
@@ -1,7 +1,7 @@
 module Main (main) where
 
 import Covenant.Type
-  ( AbstractTy (BoundAtScope, ForallAA),
+  ( AbstractTy (BoundAt),
     BuiltinFlatT
       ( BLS12_381_G1_ElementT,
         BLS12_381_G2_ElementT,
@@ -45,8 +45,7 @@ import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)
 main :: IO ()
 main =
   defaultMain . adjustOption moreTests . testGroup "Renaming" $
-    [ testCase "bare abstraction" testBareAbs,
-      testGroup
+    [ testGroup
         "Builtin flat types"
         [ testCase "UnitT" $ testFlat UnitT,
           testCase "BoolT" $ testFlat BoolT,
@@ -59,18 +58,13 @@ main =
           testCase "DataT" $ testFlat DataT
         ],
       testProperty "Nested concrete types" propNestedConcrete,
-      testCase "Rename id type" testIdT,
-      testCase "Rename const type" testConstT,
-      testCase "Rename HeadList type" testHeadListT,
-      testCase "Rename SndPair type" testSndPairT,
-      testCase "Rename map function over lists" testMapT,
-      testGroup
-        "Nested foralls"
-        [ testCase "forall a b . (a, b)" testPairTOuterOuter,
-          testCase "forall a . (a, forall b . b)" testPairTOuterInner,
-          testCase "forall b . (forall a . a, b)" testPairTInnerOuter,
-          testCase "(forall a . a, forall b . b)" testPairTInnerInner
-        ]
+      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
     ]
   where
     -- Note (Koz, 26/02/2025): By default, QuickCheck runs only 100 tests per
@@ -82,17 +76,6 @@ main =
 
 -- Tests and properties
 
--- Checks that `forall a . a` renames correctly. Also verifies that there are no
--- fixed bindings in the tracker afterwards.
-testBareAbs :: IO ()
-testBareAbs = do
-  let absTy = Abstraction ForallAA
-  let expected = Abstraction (CanSet 0)
-  let (tracker, actual) = runRenameM . renameValT $ absTy
-  assertEqual "" expected actual
-  let entry = Bimap.lookup (0, 0) tracker
-  assertEqual "" Nothing entry
-
 -- Checks that the given 'flat' type renames to itself. Also verifies that there
 -- are no fixed bindings in the tracker afterwards.
 testFlat :: BuiltinFlatT -> IO ()
@@ -114,7 +97,7 @@ propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) ->
 -- fixed bindings in the tracker afterwards.
 testIdT :: IO ()
 testIdT = do
-  let absA = BoundAtScope 1 0
+  let absA = BoundAt 0 0
   let idT = CompT 1 $ Abstraction absA :| [Abstraction absA]
   let expected = CompT 1 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 0)]
   let (tracker, actual) = runRenameM . renameCompT $ idT
@@ -125,20 +108,38 @@ testIdT = do
 -- there are no fixed bindings in the tracker afterwards.
 testConstT :: IO ()
 testConstT = do
-  let absA = BoundAtScope 1 0
-  let absB = BoundAtScope 1 1
+  let absA = BoundAt 0 0
+  let absB = BoundAt 0 1
   let constT = CompT 2 $ Abstraction absA :| [Abstraction absB, Abstraction absA]
   let expected = CompT 2 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 1), Abstraction (CanSet 0)]
   let (tracker, actual) = runRenameM . renameCompT $ constT
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
+-- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames. Also verifies that
+-- there are no fixed bindings in the tracker afterwards.
+testConstT2 :: IO ()
+testConstT2 = do
+  let constT =
+        CompT 1 $
+          Abstraction (BoundAt 0 0)
+            :| [ ThunkT . CompT 1 $ Abstraction (BoundAt 0 0) :| [Abstraction (BoundAt 1 0)]
+               ]
+  let expected =
+        CompT 1 $
+          Abstraction (CanSet 0)
+            :| [ ThunkT . CompT 1 $ Abstraction (Can'tSet 0) :| [Abstraction (CanSet 0)]
+               ]
+  let (tracker, actual) = runRenameM . renameCompT $ constT
+  assertEqual "" expected actual
+  assertEqual "" (Bimap.singleton (2, 0) 0) tracker
+
 -- Checks that `forall a . [a] -> !a` correctly renames. Also verifies that
 -- there are no fixed bindings in the tracker afterwards.
 testHeadListT :: IO ()
 testHeadListT = do
-  let absA = BoundAtScope 1 0
-  let absAInner = BoundAtScope 2 0
+  let absA = BoundAt 0 0
+  let absAInner = BoundAt 1 0
   let headListT = CompT 1 $ BuiltinNested (ListT 0 (Abstraction absAInner)) :| [Abstraction absA]
   let expected = CompT 1 $ BuiltinNested (ListT 0 (Abstraction (CanSet 0))) :| [Abstraction (CanSet 0)]
   let (tracker, actual) = runRenameM . renameCompT $ headListT
@@ -151,8 +152,8 @@ testSndPairT :: IO ()
 testSndPairT = do
   let sndPairT =
         CompT 2 $
-          BuiltinNested (PairT 0 (Abstraction (BoundAtScope 2 0)) (Abstraction (BoundAtScope 2 1)))
-            :| [Abstraction (BoundAtScope 1 1)]
+          BuiltinNested (PairT 0 (Abstraction (BoundAt 1 0)) (Abstraction (BoundAt 1 1)))
+            :| [Abstraction (BoundAt 0 1)]
   let expected =
         CompT 2 $
           BuiltinNested (PairT 0 (Abstraction (CanSet 0)) (Abstraction (CanSet 1)))
@@ -166,12 +167,12 @@ testSndPairT = do
 -- checks that two fixed bindings remain in the tracker afterwards.
 testMapT :: IO ()
 testMapT = do
-  let mapThunkT = ThunkT . CompT 0 $ Abstraction (BoundAtScope 2 0) :| [Abstraction (BoundAtScope 2 1)]
+  let mapThunkT = ThunkT . CompT 0 $ Abstraction (BoundAt 1 0) :| [Abstraction (BoundAt 1 1)]
   let mapT =
         CompT 2 $
           mapThunkT
-            :| [ BuiltinNested (ListT 0 (Abstraction (BoundAtScope 2 0))),
-                 BuiltinNested (ListT 0 (Abstraction (BoundAtScope 2 1)))
+            :| [ BuiltinNested (ListT 0 (Abstraction (BoundAt 1 0))),
+                 BuiltinNested (ListT 0 (Abstraction (BoundAt 1 1)))
                ]
   let expectedMapThunkT = ThunkT . CompT 0 $ Abstraction (Can'tSet 0) :| [Abstraction (Can'tSet 1)]
   let expectedThunkT = ThunkT . CompT 0 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 1)]
@@ -183,7 +184,7 @@ testMapT = do
                ]
   let (trackerThunkT, actualThunkT) = runRenameM . renameValT $ mapThunkT
   assertEqual "" expectedMapThunkT actualThunkT
-  let expectedThunkTracker = Bimap.fromList [((-1, 0), 0), ((-1, 1), 1)]
+  let expectedThunkTracker = Bimap.fromList [((0, 0), 0), ((0, 1), 1)]
   assertEqual "" expectedThunkTracker trackerThunkT
   let (trackerMapT, actualMapT) = runRenameM . renameCompT $ mapT
   assertEqual "" expectedMapT actualMapT
@@ -191,53 +192,16 @@ testMapT = do
 
 -- Checks that `forall a b . (a, b)` correctly renames with nothing left in the
 -- tracker.
-testPairTOuterOuter :: IO ()
-testPairTOuterOuter = do
+testPairT :: IO ()
+testPairT = do
   let pairT =
-        BuiltinNested . PairT 2 (Abstraction (BoundAtScope 1 0)) . Abstraction . BoundAtScope 1 $ 1
+        BuiltinNested . PairT 2 (Abstraction (BoundAt 0 0)) . Abstraction . BoundAt 0 $ 1
   let expected =
         BuiltinNested . PairT 2 (Abstraction (CanSet 0)) . Abstraction . CanSet $ 1
   let (tracker, actual) = runRenameM . renameValT $ pairT
   assertEqual "" expected actual
   assertEqual "" Bimap.empty tracker
 
--- Checks that `forall b . (forall a . a, b)` renames correctly with nothing
--- left in the tracker.
-testPairTInnerOuter :: IO ()
-testPairTInnerOuter = do
-  let pairT =
-        BuiltinNested . PairT 1 (Abstraction ForallAA) . Abstraction . BoundAtScope 1 $ 0
-  let expected =
-        BuiltinNested . PairT 1 (Abstraction (Can'tSet 0)) . Abstraction . CanSet $ 0
-  let (tracker, actual) = runRenameM . renameValT $ pairT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
-
--- Checks that `forall a . (a, forall b . b)` renames correctly with nothing
--- left in the tracker.
-testPairTOuterInner :: IO ()
-testPairTOuterInner = do
-  let pairT =
-        BuiltinNested . PairT 1 (Abstraction (BoundAtScope 1 0)) . Abstraction $ ForallAA
-  let expected =
-        BuiltinNested . PairT 1 (Abstraction (CanSet 0)) . Abstraction . Can'tSet $ 0
-  let (tracker, actual) = runRenameM . renameValT $ pairT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
-
--- Checks that `(forall a . a, forall b . b)` renames correctly with nothing
--- left in the tracker. Also verifies that the two fixed renames are distinct.
-testPairTInnerInner :: IO ()
-testPairTInnerInner = do
-  let pairT =
-        BuiltinNested . PairT 0 (Abstraction ForallAA) . Abstraction $ ForallAA
-  let expected =
-        BuiltinNested . PairT 0 (Abstraction (Can'tSet 0)) . Abstraction . Can'tSet $ 1
-  let (tracker, actual) = runRenameM . renameValT $ pairT
-  assertEqual "" expected actual
-  let expectedTracker = Bimap.empty
-  assertEqual "" expectedTracker tracker
-
 -- Helpers
 
 -- A newtype wrapper which generates only 'fully concrete' ValTs

From 36ef4ae9b77a03b9585bf0923a1e0645eedfc3ed Mon Sep 17 00:00:00 2001
From: Koz Ross <koz.ross@retro-freedom.nz>
Date: Thu, 6 Mar 2025 14:29:54 +1300
Subject: [PATCH 4/4] Refactor renamer, support error detection, separate rigid
 from wildcard

---
 covenant.cabal        |   8 +-
 src/Covenant/Type.hs  | 214 +++++++++++++++++++----------------
 test/renaming/Main.hs | 251 ++++++++++++++++++++++++++----------------
 3 files changed, 281 insertions(+), 192 deletions(-)

diff --git a/covenant.cabal b/covenant.cabal
index 4b6a970..e9e83fd 100644
--- a/covenant.cabal
+++ b/covenant.cabal
@@ -110,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,
@@ -125,7 +126,12 @@ test-suite renaming
   import: test-lang
   type: exitcode-stdio-1.0
   main-is: Main.hs
-  build-depends: bimap
+  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
index 95b5991..ee35a5f 100644
--- a/src/Covenant/Type.hs
+++ b/src/Covenant/Type.hs
@@ -5,6 +5,7 @@ module Covenant.Type
     ValT (..),
     BuiltinFlatT (..),
     BuiltinNestedT (..),
+    RenameError (..),
     renameValT,
     renameCompT,
     RenameM,
@@ -12,14 +13,16 @@ module Covenant.Type
   )
 where
 
-import Control.Monad.Reader (asks, local)
-import Control.Monad.State.Strict (gets, modify)
-import Control.Monad.Trans.RWS.CPS (RWS, runRWS)
-import Data.Bimap (Bimap)
-import Data.Bimap qualified as Bimap
+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.List.NonEmpty (NonEmpty)
+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.
@@ -40,18 +43,18 @@ data AbstractTy = BoundAt Word64 Word64
       Show
     )
 
--- | A renamed type abstraction. We separate them into two kinds:
---
--- * Ones we can decide on (that is, variables in the context of unification);
--- and
--- * Ones we /cannot/ decide on (either fixed in higher scopes than ours, or
--- untouchable).
---
--- We use 'CanSet' plus an index for the first case; the second case is a unique
--- index assigned by the renamer.
---
--- @since 1.0.0
-data Renamed = CanSet Word64 | Can'tSet Word64
+-- | @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,
@@ -73,7 +76,7 @@ data Renamed = CanSet Word64 | Can'tSet Word64
 -- The /last/ entry in the 'NonEmpty' indicates the return type.
 --
 -- @since 1.0.0
-data CompT (a :: Type) = CompT Word64 (NonEmpty (ValT a))
+data CompT (a :: Type) = CompT Word64 (NonEmptyVector (ValT a))
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -180,6 +183,14 @@ instance Eq1 BuiltinNestedT where
       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.
@@ -201,7 +212,8 @@ instance Eq1 BuiltinNestedT where
 -- constant or fixed.
 --
 -- @since 1.0.0
-newtype RenameM (a :: Type) = RenameM (RWS Int () (Word64, Bimap (Int, Word64) Word64) a)
+newtype RenameM (a :: Type)
+  = RenameM (ExceptT RenameError (State RenameState) a)
   deriving
     ( -- | @since 1.0.0
       Functor,
@@ -210,87 +222,101 @@ newtype RenameM (a :: Type) = RenameM (RWS Int () (Word64, Bimap (Int, Word64) W
       -- | @since 1.0.0
       Monad
     )
-    via (RWS Int () (Word64, Bimap (Int, Word64) Word64))
-
--- Note (Koz, 05/04/2025): We could check that any type abstractions we have in
--- our view (meaning, not bound higher than us) do not reference tyvars that
--- don't exist, as every 'type abstraction boundary' specifies how many
--- variables it binds. This would mean the renamer could fail if it encounters
--- an impossible situation (such as asking for the index-3 type variable from a
--- scope that only binds 2). This might not be worth it however, as we would
--- have no way of checkin anything that comes from 'above us': namely, we would
--- have to blindly trust any scopes that enclose us and that those type indexes
--- are sensible.
-
--- Increase the scope by one level.
-stepDown :: forall (a :: Type). RenameM a -> RenameM a
-stepDown (RenameM comp) = RenameM (local (+ 1) comp)
+    via (ExceptT RenameError (State RenameState))
 
--- Given an abstraction in relative form, transform it into an abstraction in
--- absolute form.
-renameAbstraction :: AbstractTy -> RenameM Renamed
-renameAbstraction (BoundAt scope ix) = RenameM $ do
-  -- DeBruijn scope indices are relative to our own position. They could
-  -- potentially refer to stuff bound 'above' us (meaning they're fixed by our
-  -- callers), or stuff bound 'below' us (meaning that they're untouchable). As
-  -- the renamer walks, every time we cross a 'type abstraction barrier', we
-  -- have to take into account that, to reference something, we need an index
-  -- one higher.
-  --
-  -- We thus change the 'relative' indexes to absolute ones, choosing the
-  -- starting point as zero. Thus, we get the following scheme:
-  --
-  -- \* After one forall, scope 0 means 'can change': 1 - 0 = 1
-  -- \* After two foralls, scope 1 means 'can change': 2 - 1 = 1
-  -- \* After three foralls, scope 2 means 'can change': 3 - 2 = 1
-  --
-  -- Thus, we must check whether the difference between the current level and
-  -- the DeBruijn index is exactly 1. We call this the 'true level', although
-  -- it's not the best name.
-  trueLevel <- asks (\currentLevel -> currentLevel - fromIntegral scope)
-  if trueLevel == 1
-    then pure . CanSet $ ix
-    else do
-      -- Check if we already renamed this thing, and if so, rename consistently.
-      priorRename <- gets (Bimap.lookup (trueLevel, ix) . snd)
-      case priorRename of
-        Nothing -> do
-          renaming <- gets fst
-          modify $ \(source, tracker) -> (source + 1, Bimap.insert (trueLevel, ix) renaming tracker)
-          pure . Can'tSet $ renaming
-        Just renameIx -> pure . Can'tSet $ renameIx
-
--- | Run a renaming computation, while also producing the mapping of any fixed
--- abstractions to their original (non-relative) scope and position.
---
--- @since 1.0.0
 runRenameM ::
   forall (a :: Type).
-  RenameM a -> (Bimap (Int, Word64) Word64, a)
-runRenameM (RenameM comp) = case runRWS comp 0 (0, Bimap.empty) of
-  (res, (_, tracker), ()) -> (tracker, res)
+  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
 
--- | Given a value type with relative abstractions, produce the same value type,
--- but with absolute abstractions.
---
--- @since 1.0.0
 renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)
 renameValT = \case
-  Abstraction absTy -> Abstraction <$> renameAbstraction absTy
-  -- We're crossing a type abstraction boundary, so bump the level
+  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
-      -- We're crossing a type abstraction boundary, so bump the level
-      ListT abses t' -> ListT abses <$> stepDown (renameValT t')
-      PairT abses t1 t2 ->
-        PairT abses
-          <$> stepDown (renameValT t1)
-          <*> stepDown (renameValT t2)
-
--- | As 'renameValT', but for computation types.
---
--- @since 1.0.0
-renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)
-renameCompT (CompT abses xs) = CompT abses <$> stepDown (traverse renameValT xs)
+      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
index 17c827a..32582b0 100644
--- a/test/renaming/Main.hs
+++ b/test/renaming/Main.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE OverloadedLists #-}
+
 module Main (main) where
 
 import Covenant.Type
@@ -15,29 +17,29 @@ import Covenant.Type
       ),
     BuiltinNestedT (ListT, PairT),
     CompT (CompT),
-    Renamed (Can'tSet, CanSet),
+    RenameError (InvalidAbstractionReference, IrrelevantAbstraction),
+    Renamed (Rigid, Unifiable, Wildcard),
     ValT (Abstraction, BuiltinFlat, BuiltinNested, ThunkT),
     renameCompT,
     renameValT,
     runRenameM,
   )
-import Data.Bimap qualified as Bimap
 import Data.Coerce (coerce)
 import Data.Functor.Classes (liftEq)
-import Data.List.NonEmpty (NonEmpty ((:|)))
-import Data.List.NonEmpty qualified as NonEmpty
+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,
-    listOf,
+    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)
@@ -60,11 +62,20 @@ main =
       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 -> !(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
+      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
@@ -76,134 +87,180 @@ main =
 
 -- Tests and properties
 
--- Checks that the given 'flat' type renames to itself. Also verifies that there
--- are no fixed bindings in the tracker afterwards.
+-- Checks that the given 'flat' type renames to itself.
 testFlat :: BuiltinFlatT -> IO ()
 testFlat t = do
   let input = BuiltinFlat t
-  let (tracker, actual) = runRenameM . renameValT $ input
-  assertBool "" (liftEq (\_ _ -> False) input actual)
-  assertEqual "" Bimap.empty tracker
+  let result = runRenameM . renameValT $ input
+  assertRight (assertBool "" . liftEq (\_ _ -> False) input) result
 
 -- Checks that for any 'fully concretified' type (nested or not), renaming
--- changes nothing. Also verifies that there are no fixed bindings in the
--- tracker afterwards.
+-- changes nothing.
 propNestedConcrete :: Property
 propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) ->
-  let (tracker, actual) = runRenameM . renameValT $ t
-   in tracker === Bimap.empty .&&. liftEq (\_ _ -> False) t actual
+  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. Also verifies there are no
--- fixed bindings in the tracker afterwards.
+-- Checks that `forall a . a -> !a` correctly renames.
 testIdT :: IO ()
 testIdT = do
-  let absA = BoundAt 0 0
-  let idT = CompT 1 $ Abstraction absA :| [Abstraction absA]
-  let expected = CompT 1 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 0)]
-  let (tracker, actual) = runRenameM . renameCompT $ idT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
+  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. Also verifies that
--- there are no fixed bindings in the tracker afterwards.
+-- 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 $ Abstraction absA :| [Abstraction absB, Abstraction absA]
-  let expected = CompT 2 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 1), Abstraction (CanSet 0)]
-  let (tracker, actual) = runRenameM . renameCompT $ constT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
+  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. Also verifies that
--- there are no fixed bindings in the tracker afterwards.
+-- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames.
 testConstT2 :: IO ()
 testConstT2 = do
   let constT =
-        CompT 1 $
-          Abstraction (BoundAt 0 0)
-            :| [ ThunkT . CompT 1 $ Abstraction (BoundAt 0 0) :| [Abstraction (BoundAt 1 0)]
-               ]
+        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 $
-          Abstraction (CanSet 0)
-            :| [ ThunkT . CompT 1 $ Abstraction (Can'tSet 0) :| [Abstraction (CanSet 0)]
-               ]
-  let (tracker, actual) = runRenameM . renameCompT $ constT
-  assertEqual "" expected actual
-  assertEqual "" (Bimap.singleton (2, 0) 0) tracker
+        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. Also verifies that
--- there are no fixed bindings in the tracker afterwards.
+-- 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 $ BuiltinNested (ListT 0 (Abstraction absAInner)) :| [Abstraction absA]
-  let expected = CompT 1 $ BuiltinNested (ListT 0 (Abstraction (CanSet 0))) :| [Abstraction (CanSet 0)]
-  let (tracker, actual) = runRenameM . renameCompT $ headListT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
+  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. Also verifies that
--- there are no fixed bindings in the tracker afterwards.
+-- Checks that `forall a b . (a, b) -> !b` correctly renames.
 testSndPairT :: IO ()
 testSndPairT = do
   let sndPairT =
-        CompT 2 $
-          BuiltinNested (PairT 0 (Abstraction (BoundAt 1 0)) (Abstraction (BoundAt 1 1)))
-            :| [Abstraction (BoundAt 0 1)]
+        CompT 2
+          . NonEmpty.consV
+            (BuiltinNested (PairT 0 (Abstraction (BoundAt 1 0)) (Abstraction (BoundAt 1 1))))
+          $ [Abstraction (BoundAt 0 1)]
   let expected =
-        CompT 2 $
-          BuiltinNested (PairT 0 (Abstraction (CanSet 0)) (Abstraction (CanSet 1)))
-            :| [Abstraction (CanSet 1)]
-  let (tracker, actual) = runRenameM . renameCompT $ sndPairT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
+        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 with
--- nothing left in the tracker. Also renames the thunk argument type _only_, and
--- checks that two fixed bindings remain in the tracker afterwards.
+-- 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 $ Abstraction (BoundAt 1 0) :| [Abstraction (BoundAt 1 1)]
+  let mapThunkT =
+        ThunkT
+          . CompT 0
+          . NonEmpty.consV (Abstraction (BoundAt 1 0))
+          $ [Abstraction (BoundAt 1 1)]
   let mapT =
-        CompT 2 $
-          mapThunkT
-            :| [ BuiltinNested (ListT 0 (Abstraction (BoundAt 1 0))),
-                 BuiltinNested (ListT 0 (Abstraction (BoundAt 1 1)))
-               ]
-  let expectedMapThunkT = ThunkT . CompT 0 $ Abstraction (Can'tSet 0) :| [Abstraction (Can'tSet 1)]
-  let expectedThunkT = ThunkT . CompT 0 $ Abstraction (CanSet 0) :| [Abstraction (CanSet 1)]
+        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 $
-          expectedThunkT
-            :| [ BuiltinNested (ListT 0 (Abstraction (CanSet 0))),
-                 BuiltinNested (ListT 0 (Abstraction (CanSet 1)))
-               ]
-  let (trackerThunkT, actualThunkT) = runRenameM . renameValT $ mapThunkT
-  assertEqual "" expectedMapThunkT actualThunkT
-  let expectedThunkTracker = Bimap.fromList [((0, 0), 0), ((0, 1), 1)]
-  assertEqual "" expectedThunkTracker trackerThunkT
-  let (trackerMapT, actualMapT) = runRenameM . renameCompT $ mapT
-  assertEqual "" expectedMapT actualMapT
-  assertEqual "" Bimap.empty trackerMapT
+        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 with nothing left in the
--- tracker.
+-- 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 (CanSet 0)) . Abstraction . CanSet $ 1
-  let (tracker, actual) = runRenameM . renameValT $ pairT
-  assertEqual "" expected actual
-  assertEqual "" Bimap.empty tracker
+        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)
@@ -241,7 +298,7 @@ instance Arbitrary Concrete where
                 pure . BuiltinFlat $ DataT,
                 BuiltinNested . ListT 0 <$> go (size `quot` 4),
                 BuiltinNested <$> (PairT 0 <$> go (size `quot` 4) <*> go (size `quot` 4)),
-                ThunkT . CompT 0 <$> ((:|) <$> go (size `quot` 4) <*> listOf (go (size `quot` 4)))
+                ThunkT . CompT 0 <$> (NonEmpty.consV <$> go (size `quot` 4) <*> liftArbitrary (go (size `quot` 4)))
               ]
   {-# INLINEABLE shrink #-}
   shrink (Concrete v) =
@@ -249,14 +306,14 @@ instance Arbitrary Concrete where
       -- impossible
       Abstraction _ -> []
       ThunkT (CompT _ ts) ->
-        -- Note (Koz, 26/02/2025): This is needed because, for some weird
-        -- reason, NonEmpty lacks an Arbitrary instance.
+        -- 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 (x :| xs)
+            x : xs -> pure (NonEmpty.consV x . Vector.fromList $ xs)
       -- Can't shrink this
       BuiltinFlat _ -> []
       BuiltinNested t ->