diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,29 @@
 
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).
 
+## UNRELEASED
+
+* Expose unsafe constructors `UnsafeMkId` and `UnsafeMkArg` for `Id` and `Arg`
+  respectively from `Covenant.Test`
+* Add read-only synonyms `Id` and `Arg` for the two data types with the same
+  name in `Covenant.ASG`
+* Modify `CovenantTypeError` for new catamorphism related errors
+* Rewrite `cata` to take explicit handlers for the base functor (similar to
+  `match`)
+
+## 1.3.0 -- 2025-10-07
+
+* Zipper for the ASG in `Covenant.Zipper`
+* `topLevelId` function in `Covenant.ASG`
+* Changed type name representation of base functors from a `_F` suffix to a `#` prefix. For example, the base functor for `List` is now named `#List` instead of `List_F`. 
+* Changed base functor lookup machinery / representation to not require raw TyName text manipulation 
+* Provided helper function for safe construction of base functor names from the parent TyName
+* `ASG` now exposes a read-only pattern synonym
+* `ValNodeInfo`'s pattern for `App` now exposes type applications as well
+* JSON serialization and deserialization support for `ASG`s with type
+  declarations
+* Removed `CaseData` and `CaseList`, as Plutus Core no longer supports them
+
 ## 1.2.0 -- 2025-08-27
 
 * Helper function for safely retrieving an in-scope type variable when constructing the ASG  
diff --git a/covenant.cabal b/covenant.cabal
--- a/covenant.cabal
+++ b/covenant.cabal
@@ -1,6 +1,6 @@
 cabal-version: 3.0
 name: covenant
-version: 1.2.0
+version: 1.3.0
 synopsis: Standalone IR for Cardano scripts.
 description:
   A library describing a call-by-push-value, Turner-total IR. Includes the ability to build up the IR programmatically.
@@ -13,7 +13,7 @@
 bug-reports: https://github.com/mlabs-haskell/covenant/issues
 copyright: (C) MLabs 2024-2025
 category: Covenant
-tested-with: ghc ==9.8.4 || ==9.10.2 || ==9.12.2
+tested-with: ghc ==9.8.4 || ==9.10.3 || ==9.12.2
 build-type: Simple
 extra-source-files:
   CHANGELOG.md
@@ -32,6 +32,7 @@
     -Wmisplaced-pragmas
     -Wmissing-export-lists
     -Wmissing-import-lists
+    -Wunused-imports
 
   default-extensions:
     BangPatterns
@@ -107,10 +108,12 @@
     Covenant.Data
     Covenant.DeBruijn
     Covenant.Index
+    Covenant.JSON
     Covenant.Prim
     Covenant.Test
     Covenant.Type
     Covenant.Util
+    Covenant.Zipper
 
   other-modules:
     Covenant.Internal.KindCheck
@@ -125,10 +128,12 @@
   build-depends:
     QuickCheck ==2.15.0.1,
     acc ==0.2.0.3,
+    aeson ==2.2.3.0,
     bimap ==0.5.0,
     bytestring >=0.12.1.0 && <0.13,
     containers >=0.6.8 && <0.8,
     enummapset ==0.7.3.0,
+    hex-text ==0.1.0.9,
     mtl >=2.3.1 && <3,
     nonempty-vector ==0.2.4,
     optics-core ==0.4.1.1,
@@ -193,5 +198,11 @@
   type: exitcode-stdio-1.0
   main-is: Main.hs
   hs-source-dirs: test/kindcheck
+
+test-suite json-conformance
+  import: test-lang
+  type: exitcode-stdio-1.0
+  main-is: Main.hs
+  hs-source-dirs: test/json-conformance
 
 -- Benchmarks
diff --git a/src/Covenant/ASG.hs b/src/Covenant/ASG.hs
--- a/src/Covenant/ASG.hs
+++ b/src/Covenant/ASG.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE MultiWayIf #-}
 {-# LANGUAGE PatternSynonyms #-}
 
 -- |
@@ -20,18 +21,19 @@
   ( -- * The ASG itself
 
     -- ** Types
-    ASG,
+    ASG (ASG),
 
     -- ** Functions
+    topLevelId,
     topLevelNode,
     nodeAt,
 
     -- * ASG components
 
     -- ** Types
-    Id,
+    Id (Id),
     Ref (..),
-    Arg,
+    Arg (Arg),
     CompNodeInfo
       ( Builtin1,
         Builtin2,
@@ -81,8 +83,13 @@
 
     -- ** Helpers
     ctor,
+    ctor',
     lazyLam,
     dtype,
+    baseFunctorOf,
+    naturalBF,
+    negativeBF,
+    app',
 
     -- *** Environment
     defaultDatatypes,
@@ -98,7 +105,7 @@
 import Data.Foldable (foldl')
 #endif
 
-import Control.Monad (foldM, join, unless, zipWithM)
+import Control.Monad (foldM, join, unless, zipWithM, (>=>))
 import Control.Monad.Except
   ( ExceptT,
     MonadError (throwError),
@@ -116,9 +123,9 @@
     runReaderT,
   )
 import Covenant.Constant (AConstant, typeConstant)
-import Covenant.Data (DatatypeInfo, mkDatatypeInfo)
+import Covenant.Data (DatatypeInfo, mkDatatypeInfo, primBaseFunctorInfos)
 import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
-import Covenant.Index (Count, Index, count0, intCount, intIndex, wordCount)
+import Covenant.Index (Count, Index, count0, intCount, intIndex, ix0, wordCount)
 import Covenant.Internal.KindCheck (EncodingArgErr (EncodingArgMismatch), checkEncodingArgs)
 import Covenant.Internal.Ledger (ledgerTypes)
 import Covenant.Internal.Rename
@@ -136,7 +143,8 @@
 import Covenant.Internal.Term
   ( ASGNode (ACompNode, AValNode, AnError),
     ASGNodeType (CompNodeType, ErrorNodeType, ValNodeType),
-    Arg (Arg),
+    Arg (UnsafeMkArg),
+    BoundTyVar (BoundTyVar),
     CompNodeInfo
       ( Builtin1Internal,
         Builtin2Internal,
@@ -149,16 +157,24 @@
       ( ApplyCompType,
         ApplyToError,
         ApplyToValType,
+        BaseFunctorDoesNotExistFor,
         BrokenIdReference,
-        CataAlgebraWrongArity,
-        CataApplyToNonValT,
-        CataNoBaseFunctorForType,
-        CataNoSuchType,
+        CataCouldNotRenameBB,
+        CataCouldNotRenameHandler,
+        CataCouldNotRenameSubstitutions,
+        CataDidNotUnify,
+        CataFixUpFailedForBB,
+        CataHandlerNotAValType,
+        CataInvalidStructure,
+        CataMonomorphicBaseFunctor,
+        CataNoTypeForBaseFunctor,
         CataNonRigidAlgebra,
-        CataNotAnAlgebra,
-        CataUnsuitable,
-        CataWrongBuiltinType,
-        CataWrongValT,
+        CataNotADatatypeBaseFunctor,
+        CataNotAValueType,
+        CataUnexpectedResultType,
+        CataWrongArity,
+        CataWrongNumberOfHandlers,
+        CataWrongOutputType,
         ConstructorDoesNotExistForType,
         DatatypeInfoRenameError,
         EncodingError,
@@ -193,9 +209,10 @@
         UndeclaredOpaquePlutusDataCtor,
         UndoRenameFailure,
         UnificationError,
+        WrongNumInstantiationsInApp,
         WrongReturnType
       ),
-    Id,
+    Id (UnsafeMkId),
     Ref (AnArg, AnId),
     ValNodeInfo (AppInternal, CataInternal, DataConstructorInternal, LitInternal, MatchInternal, ThunkInternal),
     typeASGNode,
@@ -227,6 +244,7 @@
       ),
     UnifyM,
     checkApp,
+    concretifyFT,
     fixUp,
     reconcile,
     runUnifyM,
@@ -244,8 +262,8 @@
     typeTwoArgFunc,
   )
 import Covenant.Type
-  ( CompT (Comp0),
-    CompTBody (ReturnT),
+  ( CompT (Comp0, Comp1, CompN),
+    CompTBody (ArgsAndResult, ReturnT, (:--:>)),
     Constructor,
     ConstructorName,
     DataDeclaration (OpaqueData),
@@ -253,8 +271,10 @@
     Renamed (Unifiable),
     TyName (TyName),
     ValT (Abstraction),
+    integerT,
     tyvar,
   )
+import Covenant.Util (pattern ConsV, pattern NilV)
 import Data.Bimap (Bimap)
 import Data.Bimap qualified as Bimap
 import Data.Coerce (coerce)
@@ -263,19 +283,18 @@
 import Data.List (find)
 import Data.Map.Strict (Map)
 import Data.Map.Strict qualified as Map
-import Data.Maybe (fromJust, isJust, mapMaybe)
+import Data.Maybe (fromJust, fromMaybe, isJust, mapMaybe)
 import Data.Set qualified as Set
 import Data.Text qualified as T
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Data.Vector.NonEmpty qualified as NonEmpty
 import Data.Void (Void, vacuous)
-import Data.Wedge (Wedge, wedge)
-import Data.Word (Word32)
+import Data.Wedge (Wedge (Nowhere), wedge)
+import Data.Word (Word32, Word64)
 import Optics.Core
   ( A_Lens,
     LabelOptic (labelOptic),
-    at,
     folded,
     ix,
     lens,
@@ -289,10 +308,22 @@
     _2,
   )
 
+-- | A read-only pattern for exposing the internals of an 'Id'.
+--
+-- @since 1.3.1
+pattern Id :: Word64 -> Id
+pattern Id w <- UnsafeMkId w
+
+-- | A read-only pattern for exposing the internals of an 'Arg'.
+--
+-- @since 1.3.1
+pattern Arg :: DeBruijn -> Index "arg" -> ValT AbstractTy -> Arg
+pattern Arg db i t <- UnsafeMkArg db i t
+
 -- | A fully-assembled Covenant ASG.
 --
 -- @since 1.0.0
-newtype ASG = ASG (Id, Map Id ASGNode)
+newtype ASG = ASGInternal (Id, Map Id ASGNode)
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -300,6 +331,12 @@
       Show
     )
 
+{-# COMPLETE ASG #-}
+
+-- | @since 1.3.0
+pattern ASG :: Map Id ASGNode -> ASG
+pattern ASG m <- ASGInternal (_, m)
+
 -- Note (Koz, 24/04/25): The `topLevelNode` and `nodeAt` functions use `fromJust`,
 -- because we can guarantee it's impossible to miss. For an end user, the only
 -- way to get hold of an `Id` is by inspecting a node, and since we control how
@@ -310,11 +347,17 @@
 -- unlikely and probably not worth trying to protect against, given the nuisance
 -- of having to work in `Maybe` all the time.
 
+-- | Retrieves the top-level 'Id' of an ASG.
+--
+-- @since 1.3.0
+topLevelId :: ASG -> Id
+topLevelId (ASGInternal (i, _)) = i
+
 -- | Retrieves the top-level node of an ASG.
 --
 -- @since 1.0.0
 topLevelNode :: ASG -> ASGNode
-topLevelNode asg@(ASG (rootId, _)) = nodeAt rootId asg
+topLevelNode asg@(ASGInternal (rootId, _)) = nodeAt rootId asg
 
 -- | Given an 'Id' and an ASG, produces the node corresponding to that 'Id'.
 --
@@ -327,7 +370,7 @@
 --
 -- @since 1.0.0
 nodeAt :: Id -> ASG -> ASGNode
-nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings
+nodeAt i (ASG mappings) = fromJust . Map.lookup i $ mappings
 
 -- | The environment used when \'building up\' an 'ASG'. This type is exposed
 -- only for testing, or debugging, and should /not/ be used in general by those
@@ -435,12 +478,24 @@
 pattern Lit :: AConstant -> ValNodeInfo
 pattern Lit c <- LitInternal c
 
--- | An application of a computation (the 'Id' field) to some arguments (the
--- 'Vector' field).
+-- | An application of a computation (the 'Id' field) to some arguments. The
+-- first 'Vector' argument contains the term arguments, while the second 'Vector'
+-- argument contains the type arguments, as one of:
 --
--- @since 1.0.0
-pattern App :: Id -> Vector Ref -> ValNodeInfo
-pattern App f args <- AppInternal f args
+-- * 'Data.Wedge.Nowhere', meaning \'inferred\';
+-- * 'Data.Wedge.Here', meaning \'a bound type variable from a parent scope\';
+-- or
+-- * 'Data.Wedge.There', meaning \'a concrete type\'.
+--
+-- The final CompT is the concretified function type, which is necessary for codegen.
+-- @since 1.3.0
+pattern App ::
+  Id ->
+  Vector Ref ->
+  Vector (Wedge BoundTyVar (ValT Void)) ->
+  CompT AbstractTy ->
+  ValNodeInfo
+pattern App f args instTys concreteFnTy <- AppInternal f args instTys concreteFnTy
 
 -- | Wrap a computation into a value (essentially delaying it).
 --
@@ -448,11 +503,14 @@
 pattern Thunk :: Id -> ValNodeInfo
 pattern Thunk i <- ThunkInternal i
 
--- | \'Tear down\' a self-recursive value with an algebra.
+-- | \'Tear down\' a self-recursive value with an algebra. The first argument is
+-- the signature of the algebra used; the second argument is
+-- a list of \'handlers\' for the base functor, represented similar to 'Match'
+-- handlers, while the third is the type of thing to be torn down.
 --
--- @since 1.0.0
-pattern Cata :: Ref -> Ref -> ValNodeInfo
-pattern Cata algebraRef valRef <- CataInternal algebraRef valRef
+-- @since 1.4.0
+pattern Cata :: CompT AbstractTy -> Vector Ref -> Ref -> ValNodeInfo
+pattern Cata algT handlerRefs valRef <- CataInternal algT handlerRefs valRef
 
 -- | Inject (zero or more) fields into a data constructor
 --
@@ -524,12 +582,12 @@
 --
 -- @since 1.1.0
 defaultDatatypes :: Map TyName (DatatypeInfo AbstractTy)
-defaultDatatypes = foldMap go ledgerTypes
+defaultDatatypes = foldMap go ledgerTypes <> primBaseFunctorInfos
   where
     go :: DataDeclaration AbstractTy -> Map TyName (DatatypeInfo AbstractTy)
     go decl = case mkDatatypeInfo decl of
       Left err' -> error $ "Unexpected failure in default datatypes: " <> show err'
-      Right info -> Map.singleton (view #datatypeName decl) info
+      Right info -> info
 
 -- | Executes an 'ASGBuilder' to make a \'finished\' ASG.
 --
@@ -549,7 +607,7 @@
           let (i, rootNode') = Bimap.findMax bm
           case rootNode' of
             AnError -> Left TopLevelError
-            ACompNode _ _ -> pure . ASG $ (i, Bimap.toMap bm)
+            ACompNode _ _ -> pure . ASGInternal $ (i, Bimap.toMap bm)
             AValNode t info -> Left . TopLevelValue bm t $ info
 
 -- | Given a scope and a positional argument index, construct that argument.
@@ -569,7 +627,7 @@
   lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % _2 % ix indexAsInt))
   case lookedUp of
     Nothing -> throwError . NoSuchArgument scope $ index
-    Just t -> pure . Arg scope index $ t
+    Just t -> pure . UnsafeMkArg scope index . fixArgType scope $ t
 
 -- | Construct a node corresponding to the given Plutus primop.
 --
@@ -662,7 +720,7 @@
       cntW = view wordCount cnt
   bodyRef <- local (over (#scopeInfo % #argumentInfo) (Vector.cons (cntW, args))) bodyComp
   case bodyRef of
-    AnArg (Arg _ _ argTy) -> do
+    AnArg (UnsafeMkArg _ _ argTy) -> do
       if argTy == resultT
         then refTo . ACompNode expectedT . LamInternal $ bodyRef
         else throwError . WrongReturnType resultT $ argTy
@@ -703,16 +761,23 @@
 -- * Not value types for 'Ref's
 -- * Renaming failures (likely due to a malformed function or argument type)
 --
--- = Note
+-- = Notes
 --
 -- We use the 'Wedge' data type to designate type arguments, as it can represent
 -- the three possibilities we need:
 --
--- * \'Infer this argument\', specified as 'Nowhere'.
--- * \'Use this type variable in our scope\', specified as 'Here'.
--- * \'Use this concrete type\', specified as 'There'.
+-- * \'Infer this argument\', specified as 'Data.Wedge.Nowhere'.
+-- * \'Use this type variable in our scope\', specified as 'Data.Wedge.Here'.
+-- * \'Use this concrete type\', specified as 'Data.Wedge.There'.
 --
--- @since 1.2.0
+-- The *only* purpose of explicit type application arguments is to instantiate a tyvar in the result which is
+-- not determined by any argument. These variables are instantiated after every other argument has been concretified.
+--
+-- For example, if you have a function
+--   @f :: forall a b c. (a -> b) -> (b -> a) -> b -> Either a c@
+-- Then you will need to supply _one_ explicit type application to concretify @c@.
+--
+-- @since 1.3.0
 app ::
   forall (m :: Type -> Type).
   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
@@ -728,17 +793,33 @@
   case lookedUp of
     CompNodeType fT -> case runRenameM scopeInfo . renameCompT $ fT of
       Left err' -> throwError . RenameFunctionFailed fT $ err'
-      Right renamedFT -> do
-        instantiatedFT <- instantiate subs renamedFT
-        renamedArgs <- traverse renameArg argRefs
-        tyDict <- asks (view #datatypeInfo)
-        result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)
-        restored <- undoRenameM result
-        checkEncodingWithInfo tyDict restored
-        refTo . AValNode restored . AppInternal fId $ argRefs
+      Right renamedFT@(CompT count _) -> do
+        let numInstantiations = Vector.length instTys
+            numVars = review intCount count
+        if numInstantiations /= numVars
+          then throwError $ WrongNumInstantiationsInApp renamedFT numVars numInstantiations
+          else do
+            renamedArgs <- traverse renameArg argRefs
+            let concretifiedFT = concretifyFT renamedFT renamedArgs
+            instantiatedFT <- instantiate subs concretifiedFT
+            tyDict <- asks (view #datatypeInfo)
+            result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)
+            restored <- undoRenameM result
+            unRenamedFnTy <- undoRenameCompT instantiatedFT
+            checkEncodingWithInfo tyDict restored
+            refTo . AValNode restored $ AppInternal fId argRefs instTys unRenamedFnTy
     ValNodeType t -> throwError . ApplyToValType $ t
     ErrorNodeType -> throwError ApplyToError
   where
+    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]
+    renameSubs subs =
+      askScope >>= \scope -> case traverse (traverse (runRenameM scope . renameValT)) subs of
+        Left err' -> throwError $ FailedToRenameInstantiation err'
+        Right res -> pure res
+
+    -- NOTE: The helper function below only concerns instantiations that result from
+    --       explicit type applications (via the third argument to `app`).
+    --
     mkSubstitutions :: Vector (Wedge BoundTyVar (ValT Void)) -> [(Index "tyvar", ValT AbstractTy)]
     mkSubstitutions =
       Vector.ifoldl'
@@ -752,14 +833,7 @@
         )
         []
 
-    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]
-    renameSubs subs =
-      askScope >>= \scope -> case traverse (traverse (runRenameM scope . renameValT)) subs of
-        Left err' -> throwError $ FailedToRenameInstantiation err'
-        Right res -> pure res
-
     instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)
-    instantiate [] fn = pure fn
     instantiate subs fn = do
       instantiated <- liftUnifyM . fixUp $ foldr (\(i, t) f -> substitute i t f) (ThunkT fn) subs
       case instantiated of
@@ -787,7 +861,7 @@
 -- case.
 --
 -- We resolve this problem by returning a thunk. In the case of our example,
--- @Nothing@ would produce @<forall a . !Maybe a>@.
+-- @Nothing@ would produce @\<forall a . !Maybe a\>@.
 --
 -- @since 1.2.0
 dataConstructor ::
@@ -913,7 +987,7 @@
       m (Constructor a)
     findConstructor xs = case find (\x -> view #constructorName x == ctorName) xs of
       Nothing -> throwError $ ConstructorDoesNotExistForType tyName ctorName
-      Just ctor' -> pure ctor'
+      Just ctor'' -> pure ctor''
 
     -- Looks up the DatatypeInfo for the type argument supplied
     -- and also renames (and rethrows the rename error if renaming fails)
@@ -951,76 +1025,130 @@
     ValNodeType t -> throwError . ThunkValType $ t
     ErrorNodeType -> throwError ThunkError
 
--- | Given a 'Ref' to an algebra (that is, something taking a base functor and
--- producing some result), and a 'Ref' to a value associated with that base
--- functor, build a catamorphism to tear it down. This can fail for a range of
--- reasons:
---
--- * First 'Ref' is not a thunk taking one argument
--- * The argument to the thunk isn't a base functor, or isn't a suitable base
---   functor for the second argument
--- * Second argument is not a value type
+-- | Given a computation type for an algebra (the \'stated algebra type\'), as
+-- well as a set of handlers designed to deal with each case of the stated
+-- algebra's base functor, plus a 'Ref' to a value associated with that base
+-- functor, build a catamorphism to tear that value down.
 --
--- = Note
+-- Ensure the following:
 --
--- 'cata' cannot work with /non-rigid/ algebras; that is, all algebras must be
--- functions that bind no type variables of their own.
+-- * The stated algebra type must be a 'Comp0' taking a base functor and
+--   returning the same type as the last type variable instantiation of that base
+--   functor.
+-- * The handlers must be provided in the same order as the constructors of the
+--   parameter of the stated algebra type. Handlers for \'arms\' with no fields
+--   must be non-thunks, while handlers for \'arms\' with fields must be thunks.
+-- * The third argument must be a value type with a base functor.
 --
--- @since 1.1.0
+-- @since 1.3.0
 cata ::
   forall (m :: Type -> Type).
   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
-  Ref ->
+  CompT AbstractTy ->
+  Vector Ref ->
   Ref ->
   m Id
-cata rAlg rVal =
-  typeRef rVal >>= \case
-    ValNodeType valT ->
-      typeRef rAlg >>= \case
-        t@(ValNodeType (ThunkT algT)) -> case algT of
-          Comp0 (CompTBody nev) -> do
-            let algebraArity = arity algT
-            unless (algebraArity == 1) (throwError . CataAlgebraWrongArity $ algebraArity)
-            case nev NonEmpty.! 0 of
-              Datatype bfName bfTyArgs -> do
-                -- If we got this far, we know at minimum that we have somewhat
-                -- sensical arguments. Now we have to make sure that we have a
-                -- suitable type for the algebra, and a suitable thing to tear
-                -- down.
-                --
-                -- After verifying this, we use `tryApply` so the unification
-                -- machinery can produce the type we expect with proper
-                -- concretifications.
-                unless (Vector.length bfTyArgs > 0) (throwError . CataNotAnAlgebra $ t)
-                let lastTyArg = Vector.last bfTyArgs
-                unless (nev NonEmpty.! 1 == lastTyArg) (throwError . CataNotAnAlgebra $ t)
-                appliedArgT <- case valT of
-                  BuiltinFlat bT -> case bT of
-                    ByteStringT -> do
-                      unless (bfName == "ByteString_F") (throwError . CataUnsuitable algT $ valT)
-                      pure $ Datatype "ByteString_F" . Vector.singleton $ lastTyArg
-                    IntegerT -> do
-                      let isSuitableBaseFunctor = bfName == "Natural_F" || bfName == "Negative_F"
-                      unless isSuitableBaseFunctor (throwError . CataUnsuitable algT $ valT)
-                      pure $ Datatype bfName . Vector.singleton $ lastTyArg
-                    _ -> throwError . CataWrongBuiltinType $ bT
-                  Datatype tyName tyVars -> do
-                    lookedUp <- asks (view (#datatypeInfo % at tyName))
-                    case lookedUp of
-                      Nothing -> throwError . CataNoSuchType $ tyName
-                      Just info -> case view #baseFunctor info of
-                        Just (DataDeclaration actualBfName _ _ _, _) -> do
-                          unless (bfName == actualBfName) (throwError . CataUnsuitable algT $ valT)
-                          let lastTyArg' = stepDownDB lastTyArg
-                          pure . Datatype bfName . Vector.snoc tyVars $ lastTyArg'
-                        _ -> throwError . CataNoBaseFunctorForType $ tyName
-                  _ -> throwError . CataWrongValT $ valT
-                resultT <- tryApply algT appliedArgT
-                refTo . AValNode resultT . CataInternal rAlg $ rVal
-              _ -> throwError . CataNotAnAlgebra $ t
-          _ -> throwError . CataNonRigidAlgebra $ algT
-        t -> throwError . CataNotAnAlgebra $ t
-    t -> throwError . CataApplyToNonValT $ t
+cata algT handlers rVal =
+  getCataInfo algT >>= \case
+    (resultT, IntegerCata) ->
+      typeRef rVal >>= \case
+        ValNodeType (BuiltinFlat IntegerT) -> tryApply resultT integerBB
+        ValNodeType t -> throwError . CataInvalidStructure algT $ t
+        t -> throwError . CataNotAValueType $ t
+    (resultT, ByteStringCata) ->
+      typeRef rVal >>= \case
+        ValNodeType (BuiltinFlat ByteStringT) -> tryApply resultT bsBB
+        ValNodeType t -> throwError . CataInvalidStructure algT $ t
+        t -> throwError . CataNotAValueType $ t
+    (resultT, RigidCata expectedTyName bbForm) ->
+      typeRef rVal >>= \case
+        ValNodeType t@(Datatype tyName _) -> do
+          unless (tyName == expectedTyName) (throwError . CataInvalidStructure algT $ t)
+          tryApply resultT bbForm
+        ValNodeType t -> throwError . CataInvalidStructure algT $ t
+        t -> throwError . CataNotAValueType $ t
+    (resultT, NonRigidCata expectedTyName bbf) ->
+      typeRef rVal >>= \case
+        ValNodeType t@(Datatype tyName tyVars) -> do
+          unless (tyName == expectedTyName) (throwError . CataInvalidStructure algT $ t)
+          tryApplySubstituting resultT bbf tyVars
+        ValNodeType t -> throwError . CataInvalidStructure algT $ t
+        t -> throwError . CataNotAValueType $ t
+  where
+    integerBB :: CompT AbstractTy
+    integerBB =
+      Comp1 $
+        tyvar Z ix0
+          :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix0))
+          :--:> ReturnT (tyvar Z ix0)
+    bsBB :: CompT AbstractTy
+    bsBB =
+      Comp1 $
+        tyvar Z ix0
+          :--:> ThunkT (Comp0 $ integerT :--:> tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix0))
+          :--:> ReturnT (tyvar Z ix0)
+    tryApplySubstituting :: ValT AbstractTy -> ValT AbstractTy -> Vector (ValT AbstractTy) -> m Id
+    tryApplySubstituting resultT bbThunk subs = do
+      scopeInfo <- askScope
+      tyDict <- asks (view #datatypeInfo)
+      case runRenameM scopeInfo . renameValT $ bbThunk of
+        Right renamedBBThunk -> case traverse (runRenameM scopeInfo . renameValT) subs of
+          Right renamedSubs -> case runUnifyM tyDict (fixUp . doSubsVal renamedSubs $ renamedBBThunk) of
+            Right substitutedBBThunk -> do
+              asArgs <- traverse handlerToArg handlers
+              case traverse (runRenameM scopeInfo . renameValT) asArgs of
+                Right renamedHandlers -> case checkApp tyDict (fromThunk substitutedBBThunk) (fmap Just . Vector.toList $ renamedHandlers) of
+                  Right result -> do
+                    restored <- undoRenameM result
+                    unless (restored == resultT) (throwError . CataUnexpectedResultType resultT $ restored)
+                    refTo . AValNode restored . CataInternal algT handlers $ rVal
+                  Left err' -> throwError . CataDidNotUnify algT handlers $ err'
+                Left err' -> throwError . CataCouldNotRenameHandler algT handlers $ err'
+            Left err' -> throwError . CataFixUpFailedForBB algT handlers subs renamedBBThunk $ err'
+          Left err' -> throwError . CataCouldNotRenameSubstitutions algT handlers (fromThunk bbThunk) subs $ err'
+        Left err' -> throwError . CataCouldNotRenameBB algT handlers (fromThunk bbThunk) $ err'
+    fromThunk :: forall (a :: Type). (Show a) => ValT a -> CompT a
+    fromThunk = \case
+      ThunkT t -> t
+      t -> error $ "cata: ValT given by getCataInfo wasn't a thunk as expected" <> show t
+    tryApply :: ValT AbstractTy -> CompT AbstractTy -> m Id
+    tryApply resultT bb = do
+      let bbArity = arity bb
+      unless (bbArity == Vector.length handlers) (throwError . CataWrongNumberOfHandlers algT $ handlers)
+      scopeInfo <- askScope
+      case runRenameM scopeInfo . renameCompT $ bb of
+        Right renamedBB -> do
+          tyDict <- asks (view #datatypeInfo)
+          asArgs <- traverse handlerToArg handlers
+          case traverse (runRenameM scopeInfo . renameValT) asArgs of
+            Right renamedHandlers -> case checkApp tyDict renamedBB (fmap Just . Vector.toList $ renamedHandlers) of
+              Right result -> do
+                restored <- undoRenameM result
+                unless (restored == resultT) (throwError . CataUnexpectedResultType resultT $ restored)
+                refTo . AValNode restored . CataInternal algT handlers $ rVal
+              Left err' -> throwError . CataDidNotUnify algT handlers $ err'
+            Left err' -> throwError . CataCouldNotRenameHandler algT handlers $ err'
+        Left err' -> throwError . CataCouldNotRenameBB algT handlers bb $ err'
+    handlerToArg :: Ref -> m (ValT AbstractTy)
+    handlerToArg =
+      typeRef >=> \case
+        ValNodeType t -> pure t
+        t -> throwError . CataHandlerNotAValType $ t
+    doSubsComp :: Vector (ValT Renamed) -> CompT Renamed -> CompT Renamed
+    doSubsComp subs (CompT count (CompTBody nev)) = CompT count . CompTBody . fmap (doSubsVal subs) $ nev
+    doSubsVal :: Vector (ValT Renamed) -> ValT Renamed -> ValT Renamed
+    doSubsVal subs = \case
+      -- Note (Koz, 11/11/2025): The indexing ends up being a bit strange here,
+      -- as the _last_ tyvar in a BB form is always meant to stay abstract.
+      -- However, this means that if we have `n` substitutions, we have `n + 1`
+      -- possible unifiables for those substitutions to go into. Thus, doing a
+      -- blind indexing into `subs` can blow up.
+      --
+      -- Thus, if we 'miss', we should leave it alone.
+      t@(Abstraction (Unifiable i)) -> fromMaybe t $ subs Vector.!? review intIndex i
+      ThunkT someComp -> ThunkT . doSubsComp subs $ someComp
+      Datatype tyName tyVars -> Datatype tyName . fmap (doSubsVal subs) $ tyVars
+      t -> t
 
 -- | Perform a pattern match. The first argument is the value to be matched on,
 -- and the second argument is a 'Vector' of \'handlers\' for each possible
@@ -1030,6 +1158,33 @@
 -- Polymorphic \'handlers\' (that is, thunks whose computation binds type
 -- variables of its own) will fail to compile.
 --
+-- = Note
+--
+-- Opaque the handlers for an opaque type must follow the order:
+--
+--  @
+--  [ PlutusI,
+--    PlutusB,
+--    PlutusConstr,
+--    PlutusMap,
+--    PlutusList
+--  ]
+--  @
+--
+--  Where types not included in the provided constructors to the opaque declaration are omitted.
+--
+--  Furthermore, the handlers for opaque constructors operate on the unwrapped arguments to
+--  their respective PlutusData constructor. That is, for some result type @r@, the handlers for a
+--  an opaque type which uses all the constructors should have the types:
+--
+--  @
+--    PlutusI :: Integer -> r
+--    PlutusB :: ByteString -> r
+--    PlutusConstr :: Integer -> [Data] -> r
+--    PlutusMap :: [(Integer,Data)] -> r
+--    PlutusList :: [Data] -> r
+--  @
+--
 -- @since 1.2.0
 match ::
   forall (m :: Type -> Type).
@@ -1084,7 +1239,7 @@
             Right res -> pure res
           -- The type constructor for the base-functor variant of the scrutinee type.
           let scrut = Datatype tn tyConArgs
-          let scrutF = Datatype (TyName $ rawTn <> "_F") (Vector.snoc tyConArgs scrut)
+          let scrutF = Datatype (TyName $ "#" <> rawTn) (Vector.snoc tyConArgs scrut)
           -- These are arguments to the original type constructor plus the snoc'd original type.
           -- E.g. if we have:
           --      Scrutinee: List Int
@@ -1144,54 +1299,6 @@
 
 -- Helpers
 
--- Note (Koz, 13/08/2025): We need this procedure specifically for `cata`. The
--- reason for this has to do with how we construct the 'base functor form' of
--- the value to be torn down by the catamorphism, in order to use the
--- unification machinery to get the type of the final result.
---
--- To be specific, suppose we have `<List_F r (Maybe r) -> !Maybe r>` as our algebra
--- argument (where `r` is some rigid), and `List r` as the value to be torn
--- down. If we assume the rigid is bound one scope away, `r`'s DeBruijn index
--- will be `S Z` for
--- the value to be torn down, but `S (S Z)` for the algebra argument. The way
--- our approach works is:
---
--- 1. Look at the algebra argument, specifically the base functor type. Take its
---    last type argument, which we will call `last`.
--- 2. Determine the base functor for the value to be torn down. Cook up a new
---    instance of the base functor type, copying all the type arguments from the
---    value to be torn down in the same order. Then put `last` at the end.
--- 3. Force the algebra argument thunk, then try and apply the result of Step 2
---    to that.
---
--- Following the steps above for our example, we would proceed as follows:
---
--- 1. Set `last` as `Maybe r`.
--- 2. Cook up `List_F r (Maybe r)`. Note that this matches what the algebra
---    expects.
--- 3. Use the unifier with `List_F r (Maybe r) -> !Maybe r`, applying the
---    argument `List_F r (Maybe r)` from Step 2.
---
--- However, if `last` is a rigid, we have an 'off by one error'. To see why,
--- consider the form of the algebra argument:
---
--- `ThunkT . Comp0 $ Datatype "List_F" [tyvar (S (S Z)) ix0, ....`
---
--- However, `tyvar (S (S Z)) ix0` is not valid in the scope of the value to be
--- torn down: that same rigid would have DeBruijn index `S Z` there instead.
--- This applies the same if the tyvar is part of a datatype.
---
--- As we prohibit non-rigid algebras, this requires us to lower the DeBruijn
--- index by one for our process.
-stepDownDB :: ValT AbstractTy -> ValT AbstractTy
-stepDownDB = \case
-  Abstraction (BoundAt db i) -> case db of
-    -- This is impossible, so we just return it unmodified
-    Z -> Abstraction (BoundAt db i)
-    (S db') -> Abstraction (BoundAt db' i)
-  Datatype tyName tyArgs -> Datatype tyName . fmap stepDownDB $ tyArgs
-  x -> x
-
 renameArg ::
   forall (m :: Type -> Type).
   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
@@ -1216,37 +1323,8 @@
   Left encErr -> throwError $ EncodingError encErr
   Right {} -> pure ()
 
-tryApply ::
-  forall (m :: Type -> Type).
-  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
-  CompT AbstractTy ->
-  ValT AbstractTy ->
-  m (ValT AbstractTy)
-tryApply algebraT argT =
-  askScope >>= \scope -> case runRenameM scope . renameCompT $ algebraT of
-    Left err' -> throwError . RenameFunctionFailed algebraT $ err'
-    Right renamedAlgebraT -> case runRenameM scope . renameValT $ argT of
-      Left err' -> throwError . RenameArgumentFailed argT $ err'
-      Right renamedArgT -> do
-        tyDict <- asks (view #datatypeInfo)
-        case checkApp tyDict renamedAlgebraT [Just renamedArgT] of
-          Left err' -> throwError . UnificationError $ err'
-          Right resultT -> undoRenameM resultT
-
 -- Putting this here to reduce chance of annoying manual merge (will move later)
 
--- | Wrapper around an `Arg` that we know represents an in-scope type variable.
--- @since 1.2.0
-data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")
-  deriving stock
-    ( -- @since 1.2.0
-      Show,
-      -- @since 1.2.0
-      Eq,
-      -- @since 1.2.0
-      Ord
-    )
-
 -- | Given a DeBruijn index (designating scope) and positional index (designating
 -- which variable in that scope we are interested in), retrieve an in-scope type
 -- variable.
@@ -1291,6 +1369,17 @@
     Left err' -> throwError $ UndoRenameFailure err'
     Right renamed -> pure renamed
 
+undoRenameCompT ::
+  forall (m :: Type -> Type).
+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  CompT Renamed ->
+  m (CompT AbstractTy)
+undoRenameCompT comp =
+  undoRenameM (ThunkT comp) >>= \case
+    ThunkT res -> pure res
+    -- This really should be impossible, not just unlikely.
+    _other -> error "Undoing renaming on a CompT resulting in something other than a thunk, which should be totally impossible"
+
 askScope ::
   forall (m :: Type -> Type).
   (MonadReader ASGEnv m) =>
@@ -1325,7 +1414,7 @@
 --
 -- Consider @Left 3@. In this case, the field only determines the first type
 -- argument to the @Either@ data type, and if we used 'dataConstructor', we
--- would be left with a thunk of type @<forall a . !Either Integer a>@. Using
+-- would be left with a thunk of type @\<forall a . !Either Integer a\>@. Using
 -- 'ctor', we can immediately specify what @a@ should be, and unwrap the thunk.
 --
 -- @since 1.2.0
@@ -1342,6 +1431,40 @@
   dataForced <- force (AnId dataThunk)
   app dataForced mempty instTys
 
+-- | 'ctor' without the instantiation arguments, which are left up to inference.
+--
+-- @since 1.3.0
+ctor' ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  TyName ->
+  ConstructorName ->
+  Vector.Vector Ref ->
+  m Id
+ctor' tn cn args = do
+  dataThunk <- dataConstructor tn cn args
+  dataForced <- force (AnId dataThunk)
+  app' dataForced mempty
+
+-- | A variant of `app` which does not take a 'Vector' of type instantiation
+-- arguments and instead will try to infer all type arguments.
+--
+-- @since 1.3.0
+app' ::
+  forall (m :: Type -> Type).
+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  Id ->
+  Vector Ref ->
+  m Id
+app' fId args =
+  typeId fId >>= \case
+    CompNodeType (CompT count _) -> do
+      let numVars = review intCount count
+          instArgs = Vector.replicate numVars Nowhere
+      app fId args instArgs
+    ValNodeType t -> throwError . ApplyToValType $ t
+    ErrorNodeType -> throwError ApplyToError
+
 -- | As 'lam', but produces a thunk value instead of a computation.
 --
 -- @since 1.2.0
@@ -1358,3 +1481,151 @@
 -- @since 1.2.0
 dtype :: TyName -> [ValT AbstractTy] -> ValT AbstractTy
 dtype tn = Datatype tn . Vector.fromList
+
+-- | Helper for constructing a base functor name without having know the internal naming convention for
+--   base functors.
+--
+-- @since 1.3.0
+baseFunctorOf ::
+  forall (m :: Type -> Type).
+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>
+  TyName ->
+  m TyName
+baseFunctorOf (TyName tn) = do
+  let bfTn = TyName ("#" <> tn)
+  tyDict <- asks (view #datatypeInfo)
+  case preview (ix bfTn) tyDict of
+    Nothing -> throwError $ BaseFunctorDoesNotExistFor (TyName tn)
+    Just {} -> pure bfTn
+
+-- | The name of the @Natural@ base functor for @Integer@.
+--
+-- This is required because @Integer@ is the only type with two base functors,
+-- and thus, its base functor cannot be determined from the type name alone.
+--
+-- @since 1.3.0
+naturalBF :: TyName
+naturalBF = TyName "#Natural"
+
+-- | The name of the @Negative@ base functor for @Integer@.
+--
+-- This is required because @Integer@ is the only type with two base functors,
+-- and thus, its base functor cannot be determined from the type name alone.
+--
+-- @since 1.3.0
+negativeBF :: TyName
+negativeBF = TyName "#Negative"
+
+-- Used as a helper for catamorphisms to classify what we need to do based on
+-- the stated algebra type
+data CataInfo
+  = IntegerCata
+  | ByteStringCata
+  | RigidCata TyName (CompT AbstractTy)
+  | NonRigidCata TyName (ValT AbstractTy)
+
+getCataInfo ::
+  forall (m :: Type -> Type).
+  (MonadReader ASGEnv m, MonadError CovenantTypeError m) =>
+  CompT AbstractTy -> m (ValT AbstractTy, CataInfo)
+getCataInfo t = case t of
+  Comp0 (CompTBody nev) -> do
+    unless (NonEmpty.length nev == 2) (throwError . CataWrongArity $ t)
+    let inputT = nev NonEmpty.! 0
+    let outputT = nev NonEmpty.! 1
+    case inputT of
+      Datatype bfTyName bfTyVars ->
+        (stepDown outputT,) <$> case Vector.unsnoc bfTyVars of
+          Just (tyVarInsts, lastT) -> do
+            unless (lastT == outputT) (throwError . CataWrongOutputType outputT $ lastT)
+            if
+              | bfTyName == naturalBF -> pure IntegerCata
+              | bfTyName == negativeBF -> pure IntegerCata
+              -- Note (Koz, 10/11/2025): This is hacky as hell, but since
+              -- ByteString is technically a builtin type, this is the only
+              -- way to spot its base functor.
+              | bfTyName == "#ByteString" -> pure ByteStringCata
+              | otherwise -> do
+                  datatypes <- asks (view #datatypeInfo)
+                  case Map.foldlWithKey' (go bfTyName) Nothing datatypes of
+                    Just (k, bbf) -> case tyVarInsts of
+                      NilV -> pure . RigidCata k $ bbf
+                      ConsV _ _ -> pure . NonRigidCata k . ThunkT $ bbf
+                    Nothing -> throwError . CataNoTypeForBaseFunctor $ bfTyName
+          _ -> throwError . CataMonomorphicBaseFunctor $ bfTyName
+      _ -> throwError . CataNotADatatypeBaseFunctor $ inputT
+  _ -> throwError . CataNonRigidAlgebra $ t
+  where
+    go ::
+      TyName ->
+      Maybe (TyName, CompT AbstractTy) ->
+      TyName ->
+      DatatypeInfo AbstractTy ->
+      Maybe (TyName, CompT AbstractTy)
+    go targetTyName acc currTyName currTyInfo = case acc of
+      Nothing -> case view #baseFunctor currTyInfo of
+        Just (DataDeclaration name _ _ _, _) ->
+          if name == targetTyName
+            then case view #bbForm currTyInfo of
+              Just (ThunkT bbfTy) -> Just (currTyName, bbfTy)
+              _ -> acc -- technically impossible
+            else acc
+        _ -> acc
+      _ -> acc
+    -- Note (Koz, 11/11/2025): We need this procedure specifically for `cata`. The
+    -- reason for this has to do with how we construct the 'base functor form' of
+    -- the value to be torn down by the catamorphism, in order to use the
+    -- unification machinery to get the type of the final result.
+    --
+    -- To be specific, suppose we have `<#List r (Maybe r) -> !Maybe r>` as our
+    -- stated algebra type, with `r` rigid. Suppose also that the value to be torn
+    -- down is `List r`. If we assume the rigid `r` is bound one scope away, `r`'s
+    -- DeBruijn index will be different for each of these:
+    --
+    -- \* In the stated algebra type, `r`'s index will be `S (S Z)`; but
+    -- \* In the value to be torn down, `r`'s index will be `S Z`.
+    --
+    -- As part of what we do here, we 'collect' the expected result of the
+    -- catamorphism according to the stated algebra type. Then, we use a
+    -- combination of the value to be torn down (or more precisely, its
+    -- Boehm-Berrarducci form), together with the handlers, as arguments to the
+    -- unifier to see what result we get on that basis. In theory, if the expected
+    -- result type and the result of this unification agree, we type check.
+    -- However, this would fail in our case: as the stated algebra type is
+    -- `Comp0 $ Datatype "#List" [tyvar (S (S Z)) ix0, ...`, the expected result
+    -- type would be `Datatype "Maybe" [tyvar (S (S Z) ix0]`. However, this is not
+    -- valid in the scope of the value to be torn down: that same rigid would have
+    -- the DeBruijn index `S Z` in that scope instead. This applies regardless of
+    -- whether the tyvar is part of a datatype or not. This gives us an 'off by
+    -- one' error.
+    --
+    -- As we prohibit non-rigid algebras, this requires us to lower the DeBruijn
+    -- index by one for our process. This is, in fact, _why_ stated algebra
+    -- types must be rigid: if they weren't, this process would become far more
+    -- complicated, as we would now have to be careful to establish _which_
+    -- tyvars need 'stepping down' and which don't!
+    stepDown :: ValT AbstractTy -> ValT AbstractTy
+    stepDown = \case
+      Abstraction (BoundAt db i) -> case db of
+        -- This is impossible, so we just return it unmodified
+        Z -> Abstraction (BoundAt db i)
+        (S db') -> Abstraction (BoundAt db' i)
+      Datatype tyName tyArgs -> Datatype tyName . fmap stepDown $ tyArgs
+      x -> x
+
+fixArgType :: DeBruijn -> ValT AbstractTy -> ValT AbstractTy
+fixArgType distance = \case
+  Abstraction tyVar ->
+    let tyVar' = addDeBruijn distance tyVar
+     in Abstraction tyVar'
+  ThunkT (CompN cnt (ArgsAndResult args res)) ->
+    let args' = fmap (fixArgType distance) args
+        res' = fixArgType distance res
+     in ThunkT (CompN cnt (ArgsAndResult args' res'))
+  bi@(BuiltinFlat {}) -> bi
+  Datatype tn dtArgs -> Datatype tn $ fmap (fixArgType distance) dtArgs
+  where
+    addDeBruijn :: DeBruijn -> AbstractTy -> AbstractTy
+    addDeBruijn toAdd (BoundAt db indx) =
+      let db' = fromJust . preview asInt $ review asInt toAdd + review asInt db
+       in BoundAt db' indx
diff --git a/src/Covenant/Data.hs b/src/Covenant/Data.hs
--- a/src/Covenant/Data.hs
+++ b/src/Covenant/Data.hs
@@ -36,6 +36,9 @@
     hasRecursive,
     everythingOf,
     mapValT,
+
+    -- ** Constants
+    primBaseFunctorInfos,
   )
 where
 
@@ -43,10 +46,15 @@
 import Control.Monad.Reader (MonadReader (ask, local), MonadTrans (lift), Reader, runReader)
 import Control.Monad.Trans.Except (ExceptT, runExceptT)
 import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
-import Covenant.Index (Count, Index, count0, intCount, intIndex)
+import Covenant.Index (Count, Index, count0, intCount, intIndex, ix0)
 import Covenant.Internal.PrettyPrint (ScopeBoundary (ScopeBoundary))
+import Covenant.Internal.Strategy
+  ( DataEncoding (SOP),
+    PlutusDataConstructor (PlutusB, PlutusConstr, PlutusI, PlutusList, PlutusMap),
+  )
 import Covenant.Internal.Type
   ( AbstractTy (BoundAt),
+    BuiltinFlatT (ByteStringT, IntegerT),
     CompT (CompT),
     CompTBody (CompTBody),
     Constructor (Constructor),
@@ -54,15 +62,36 @@
     DataDeclaration (DataDeclaration, OpaqueData),
     TyName (TyName),
     ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
+    byteStringBaseFunctor,
+    naturalBaseFunctor,
+    negativeBaseFunctor,
   )
+import Covenant.Type
+  ( CompT (Comp0, Comp1),
+    CompTBody (ReturnT, (:--:>)),
+    tyvar,
+  )
 import Data.Bitraversable (bisequence)
 import Data.Kind (Type)
+import Data.Map.Strict (Map)
+import Data.Map.Strict qualified as M
 import Data.Maybe (fromJust)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Vector qualified as V
 import Data.Vector.NonEmpty qualified as NEV
-import Optics.Core (A_Lens, LabelOptic (labelOptic), folded, lens, preview, review, toListOf, view, (%), _2)
+import Optics.Core
+  ( A_Lens,
+    LabelOptic (labelOptic),
+    folded,
+    lens,
+    preview,
+    review,
+    toListOf,
+    view,
+    (%),
+    _2,
+  )
 import Optics.Indexed.Core (A_Fold)
 
 -- | All possible errors that could arise when constructing a Boehm-Berrarducci
@@ -93,9 +122,12 @@
 data DatatypeInfo (var :: Type)
   = DatatypeInfo
   { _originalDecl :: DataDeclaration var,
+    -- The second element of the tuple here is the BB form of the Base functor
+    -- (this is what we actually care about most of the time)
     _baseFunctorStuff :: Maybe (DataDeclaration var, ValT var),
     -- NOTE: The ONLY type that won't have a BB form is `Void` (or something isomorphic to it)
-    _bbForm :: Maybe (ValT var)
+    _bbForm :: Maybe (ValT var),
+    _isBaseFunctor :: Bool
   }
   deriving stock
     ( -- | @since 1.1.0
@@ -114,8 +146,8 @@
   {-# INLINEABLE labelOptic #-}
   labelOptic =
     lens
-      (\(DatatypeInfo ogDecl _ _) -> ogDecl)
-      (\(DatatypeInfo _ b c) ogDecl -> DatatypeInfo ogDecl b c)
+      (\(DatatypeInfo ogDecl _ _ _) -> ogDecl)
+      (\(DatatypeInfo _ b c d) ogDecl -> DatatypeInfo ogDecl b c d)
 
 -- | The base functor for this data type, if it exists. Types which are not
 -- self-recursive lack base functors.
@@ -128,8 +160,8 @@
   {-# INLINEABLE labelOptic #-}
   labelOptic =
     lens
-      (\(DatatypeInfo _ baseF _) -> baseF)
-      (\(DatatypeInfo a _ c) baseF -> DatatypeInfo a baseF c)
+      (\(DatatypeInfo _ baseF _ _) -> baseF)
+      (\(DatatypeInfo a _ c d) baseF -> DatatypeInfo a baseF c d)
 
 -- | The Boehm-Berrarducci form of this type, if it exists. Types with no
 -- constructors (that is, types without inhabitants) lack Boehm-Berrarducci
@@ -143,8 +175,8 @@
   {-# INLINEABLE labelOptic #-}
   labelOptic =
     lens
-      (\(DatatypeInfo _ _ bb) -> bb)
-      (\(DatatypeInfo a b _) bb -> DatatypeInfo a b bb)
+      (\(DatatypeInfo _ _ bb _) -> bb)
+      (\(DatatypeInfo a b _ d) bb -> DatatypeInfo a b bb d)
 
 -- | The base functor Boehm-Berrarducci form of this type, if it exists. A type
 -- must have both a base functor and a Boehm-Berrarducci form to have a base
@@ -159,13 +191,42 @@
   {-# INLINEABLE labelOptic #-}
   labelOptic = #baseFunctor % folded % _2
 
+-- | Is this the DatatypeInfo for a base functor?
+-- @since 1.3.0
+instance
+  (k ~ A_Lens, a ~ Bool, b ~ Bool) =>
+  LabelOptic "isBaseFunctor" k (DatatypeInfo var) (DatatypeInfo var) a b
+  where
+  {-# INLINEABLE labelOptic #-}
+  labelOptic =
+    lens
+      (\(DatatypeInfo _ _ _ isbf) -> isbf)
+      (\(DatatypeInfo a b c _) isbf -> DatatypeInfo a b c isbf)
+
 -- | Given a declaration of a datatype, either produce its datatype info, or
--- fail.
+--   fail.
 --
--- @since 1.1.0
-mkDatatypeInfo :: DataDeclaration AbstractTy -> Either BBFError (DatatypeInfo AbstractTy)
-mkDatatypeInfo decl = DatatypeInfo decl <$> baseFStuff <*> mkBBF decl
+--   Returns a map because it will bundle the base functor declaration for a given type
+--   if a base functor can be generated.
+-- @since 1.3.0
+mkDatatypeInfo :: DataDeclaration AbstractTy -> Either BBFError (Map TyName (DatatypeInfo AbstractTy))
+mkDatatypeInfo decl = do
+  bbf <- mkBBF decl
+  baseF <- baseFStuff
+  case baseF of
+    Nothing ->
+      pure . M.singleton declTyName $ DatatypeInfo decl Nothing bbf False
+    bf@(Just (baseFDecl, baseFBB)) -> do
+      let baseFTyName = view #datatypeName baseFDecl
+          baseFDatatypeInfo =
+            M.singleton baseFTyName $
+              DatatypeInfo baseFDecl Nothing (Just baseFBB) True
+          parentDatatypeInfo =
+            M.singleton declTyName $
+              DatatypeInfo decl bf bbf False
+      pure $ baseFDatatypeInfo <> parentDatatypeInfo
   where
+    declTyName = view #datatypeName decl
     baseFStuff :: Either BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))
     baseFStuff =
       let baseFDecl = runReader (mkBaseFunctor decl) 0
@@ -184,20 +245,25 @@
 -- | Constructs a base functor from a suitable data declaration, returning
 -- 'Nothing' if the input is not a recursive type.
 --
--- @since 1.1.0
+-- Note that naming convention for base functors and their constructors gives "illegal" type names,
+-- i.e. names that users could not choose themselves. For example, in:
+-- @data List a = Nil | Cons a (List a)@
+-- The type name for the generated base functor is '#List' and the constructors of the base functor are
+-- '#Cons' and '#Nil'.
+-- @since 1.3.0
 mkBaseFunctor :: DataDeclaration AbstractTy -> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))
 mkBaseFunctor OpaqueData {} = pure Nothing
-mkBaseFunctor (DataDeclaration tn numVars ctors strat) = do
+mkBaseFunctor (DataDeclaration tn numVars ctors _) = do
   anyRecComponents <- or <$> traverse (hasRecursive tn) allCtorArgs
   if null ctors || not anyRecComponents
     then pure Nothing
     else do
       baseCtors <- traverse mkBaseCtor ctors
-      pure . Just $ DataDeclaration baseFName baseFNumVars baseCtors strat
+      pure . Just $ DataDeclaration baseFName baseFNumVars baseCtors SOP
   where
     baseFName :: TyName
     baseFName = case tn of
-      TyName tyNameInner -> TyName (tyNameInner <> "_F")
+      TyName tyNameInner -> TyName ("#" <> tyNameInner)
     baseFNumVars :: Count "tyvar"
     baseFNumVars = fromJust . preview intCount $ review intCount numVars + 1
     -- The argument position of the new type variable parameter (typically `r`).
@@ -228,7 +294,7 @@
     mkBaseCtor (Constructor ctorNm ctorArgs) = Constructor (baseFCtorName ctorNm) <$> traverse replaceAllRecursive ctorArgs
       where
         baseFCtorName :: ConstructorName -> ConstructorName
-        baseFCtorName (ConstructorName nm) = ConstructorName (nm <> "_F")
+        baseFCtorName (ConstructorName nm) = ConstructorName ("#" <> nm)
     allCtorArgs :: [ValT AbstractTy]
     allCtorArgs = concatMap (V.toList . view #constructorArgs) ctors
     -- This tells us whether the ValT *is* a recursive child of the parent type
@@ -364,7 +430,34 @@
 
 -- Only returns `Nothing` if there are no Constructors or the type is Opaque
 mkBBF' :: DataDeclaration AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)
-mkBBF' OpaqueData {} = lift Nothing
+mkBBF' (OpaqueData _ ctorsSet) = do
+  let bbfFunArgs = map mkOpaqueFn (Set.toList ctorsSet)
+  case NEV.fromList bbfFunArgs of
+    Nothing -> error "No ctors for opaque. If this happens it means we didn't run the kind checker."
+    Just fn -> lift . Just . ThunkT . Comp1 . CompTBody $ NEV.snoc fn (tyvar Z ix0)
+  where
+    -- `r` as it appears in the thunks
+    r :: ValT AbstractTy
+    r = Abstraction (BoundAt (S Z) ix0)
+    helper :: ValT AbstractTy -> ValT AbstractTy
+    helper arg = ThunkT . Comp0 $ arg :--:> ReturnT r
+    pList :: V.Vector (ValT AbstractTy) -> ValT AbstractTy
+    pList = Datatype "List"
+    pData :: ValT AbstractTy
+    pData = Datatype "Data" mempty
+    pPair :: ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy
+    pPair a b = Datatype "Pair" $ V.fromList [a, b]
+    mkOpaqueFn :: PlutusDataConstructor -> ValT AbstractTy
+    mkOpaqueFn = \case
+      PlutusI -> helper $ BuiltinFlat IntegerT
+      PlutusB -> helper $ BuiltinFlat ByteStringT
+      PlutusConstr ->
+        ThunkT . Comp0 $
+          BuiltinFlat IntegerT
+            :--:> pList (V.fromList [pData])
+            :--:> ReturnT r
+      PlutusList -> helper (pList (V.singleton pData))
+      PlutusMap -> helper (pList (V.singleton (pPair pData pData)))
 mkBBF' (DataDeclaration tn numVars ctors _)
   | V.null ctors = lift Nothing
   | otherwise = do
@@ -414,5 +507,27 @@
        they now occur within a Thunk), but after that bump everything is stable as indicated above.
 -}
 
-{- Here for lack of a better place to put it (has to be available to Unification and ASG)
+{- Primitive Base Functor Datatype Info
+
+   This has to be here to avoid cyclic dependencies and we have to write them by hand.
+
+   NOTE: THESE MUST BE INSERTED INTO THE DEFAULT ASGBUILDER CONTEXT WHEN IT IS CONSTRUCTED/INITIALIZED
+         (it's not yet clear where the best place to do that will be)
 -}
+
+primBaseFunctorInfos :: Map TyName (DatatypeInfo AbstractTy)
+primBaseFunctorInfos =
+  foldr
+    ( ( \x acc ->
+          let tnm = view (#originalDecl % #datatypeName) x
+           in M.insert tnm x acc
+      )
+        . unsafeMkPrimInfo
+    )
+    M.empty
+    [naturalBaseFunctor, negativeBaseFunctor, byteStringBaseFunctor]
+  where
+    unsafeMkPrimInfo :: DataDeclaration AbstractTy -> DatatypeInfo AbstractTy
+    unsafeMkPrimInfo decl = case mkBBF decl of
+      Left err -> error $ "Error constructing BBF for primitive base functor: " <> show err
+      Right bbf -> DatatypeInfo decl Nothing bbf True
diff --git a/src/Covenant/Internal/KindCheck.hs b/src/Covenant/Internal/KindCheck.hs
--- a/src/Covenant/Internal/KindCheck.hs
+++ b/src/Covenant/Internal/KindCheck.hs
@@ -72,6 +72,7 @@
   | MutualRecursionDetected (Set TyName)
   | InvalidStrategy TyName
   | EncodingMismatch (EncodingArgErr AbstractTy)
+  | OpaqueWithNoConstructors TyName
   deriving stock (Show, Eq)
 
 newtype KindCheckContext a = KindCheckContext (Map TyName (DataDeclaration a))
@@ -118,7 +119,9 @@
 checkDataDecls decls = runKindCheckM decls $ traverse_ checkDataDecl (M.elems decls)
 
 checkDataDecl :: DataDeclaration AbstractTy -> KindCheckM AbstractTy ()
-checkDataDecl OpaqueData {} = pure ()
+checkDataDecl (OpaqueData tn ctors)
+  | null ctors = throwError $ OpaqueWithNoConstructors tn
+  | otherwise = pure ()
 checkDataDecl decl@(DataDeclaration tn _ ctors _) = do
   unless (checkStrategy decl) $ throwError (InvalidStrategy tn)
   cycleCheck' mempty decl
diff --git a/src/Covenant/Internal/Rename.hs b/src/Covenant/Internal/Rename.hs
--- a/src/Covenant/Internal/Rename.hs
+++ b/src/Covenant/Internal/Rename.hs
@@ -310,11 +310,11 @@
 -- REVIEW: I am not sure if we really want the scope arg to runRenameM to be `mempty`.
 --         If something breaks w/ BB forms or datatypes, look here.
 renameDatatypeInfo :: DatatypeInfo AbstractTy -> Either RenameError (DatatypeInfo Renamed)
-renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM mempty $ do
+renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb isBF) = runRenameM mempty $ do
   ogDecl' <- renameDataDecl ogDecl
   baseFStuff' <- traverse (bitraverse renameDataDecl renameValT) baseFStuff
   bb' <- traverse renameValT bb
-  pure $ DatatypeInfo ogDecl' baseFStuff' bb'
+  pure $ DatatypeInfo ogDecl' baseFStuff' bb' isBF
 
 -- A way of 'undoing' the renaming process. This is meant to be used only after
 -- applications, and assumes that what is being un-renamed is the result of a
diff --git a/src/Covenant/Internal/Strategy.hs b/src/Covenant/Internal/Strategy.hs
--- a/src/Covenant/Internal/Strategy.hs
+++ b/src/Covenant/Internal/Strategy.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE GADTs #-}
+
 module Covenant.Internal.Strategy
   ( DataEncoding (..),
     PlutusDataStrategy (..),
@@ -9,30 +11,11 @@
 -- | Describes how a datatype is represented onchain.
 --
 -- @since 1.1.0
-data DataEncoding
-  = -- | The datatype is represented using the SOP primitives.
-    --
-    -- @since 1.1.0
-    SOP
-  | -- | The datatype is represented as @Data@, using the
-    -- specified strategy to determine specifics.
-    --
-    -- @since 1.1.0
-    PlutusData PlutusDataStrategy
-  | -- | The type uses one of the builtin \'special\' strategies. This
-    -- is used only for specific types and isn't generally available
-    -- for use.
-    --
-    -- @since 1.1.0
-    BuiltinStrategy InternalStrategy
-  deriving stock
-    ( -- | @since 1.1.0
-      Show,
-      -- | @since 1.1.0
-      Eq,
-      -- | @since 1.1.0
-      Ord
-    )
+data DataEncoding where
+  SOP :: DataEncoding
+  PlutusData :: PlutusDataStrategy -> DataEncoding
+  BuiltinStrategy :: InternalStrategy -> DataEncoding
+  deriving stock (Show, Eq, Ord)
 
 -- NOTE: Wrapped data-primitive (Integer + ByteString) require a special case for their encoders, which was originally
 --       part of a "WrapperData" strategy here which we generalized to the NewtypeData strategy.
diff --git a/src/Covenant/Internal/Term.hs b/src/Covenant/Internal/Term.hs
--- a/src/Covenant/Internal/Term.hs
+++ b/src/Covenant/Internal/Term.hs
@@ -1,8 +1,8 @@
 module Covenant.Internal.Term
   ( CovenantTypeError (..),
-    Id (..),
+    Id (UnsafeMkId),
     typeId,
-    Arg (..),
+    Arg (UnsafeMkArg),
     typeArg,
     Ref (..),
     typeRef,
@@ -11,6 +11,7 @@
     ASGNode (..),
     typeASGNode,
     ASGNodeType (..),
+    BoundTyVar (..),
   )
 where
 
@@ -23,7 +24,6 @@
 import Covenant.Internal.Rename (RenameError, UnRenameError)
 import Covenant.Internal.Type
   ( AbstractTy,
-    BuiltinFlatT,
     CompT,
     TyName,
     ValT,
@@ -33,7 +33,10 @@
 import Covenant.Type (ConstructorName, PlutusDataConstructor, Renamed)
 import Data.Kind (Type)
 import Data.Set qualified as Set
+import Data.Text (Text)
 import Data.Vector (Vector)
+import Data.Void (Void)
+import Data.Wedge (Wedge)
 import Data.Word (Word64)
 
 -- | An error that can arise during the construction of an ASG by programmatic
@@ -130,46 +133,6 @@
     --
     -- @since 1.1.0
     EncodingError (EncodingArgErr AbstractTy)
-  | -- | The first argument to a catamorphism wasn't an algebra, as
-    -- it had the wrong arity.
-    --
-    -- @since 1.2.0
-    CataAlgebraWrongArity Int
-  | -- | The first argument to a catamorphism wasn't an algebra.
-    --
-    -- @since 1.1.0
-    CataNotAnAlgebra ASGNodeType
-  | -- | The second argument to a catamorphism wasn't a value type.
-    --
-    -- @since 1.1.0
-    CataApplyToNonValT ASGNodeType
-  | -- The algebra given to this catamorphism is not rigid (that is, its
-    -- computation type binds variables).
-    --
-    -- @since 1.2.0
-    CataNonRigidAlgebra (CompT AbstractTy)
-  | -- | The second argument to a catamorphism is a builtin type, but not one
-    -- we can eliminate with a catamorphism.
-    --
-    -- @since 1.1.0
-    CataWrongBuiltinType BuiltinFlatT
-  | -- | The second argument to a catamorphism is a value type, but not one we
-    -- can eliminate with a catamorphism. Usually, this means it's a variable.
-    --
-    -- @since 1.1.0
-    CataWrongValT (ValT AbstractTy)
-  | -- | We requested a catamorphism for a type that doesn't exist.
-    --
-    -- @since 1.2.0
-    CataNoSuchType TyName
-  | -- | We requested a catamorphism for a type without a base functor.
-    --
-    -- @since 1.2.0
-    CataNoBaseFunctorForType TyName
-  | -- | The provided algebra is not suitable for the given type.
-    --
-    -- @since 1.1.0
-    CataUnsuitable (CompT AbstractTy) (ValT AbstractTy)
   | -- | Someone attempted to construct a tyvar using a DB index or argument position
     --   which refers to a scope (or argument) that does not exist.
     --
@@ -261,6 +224,114 @@
     --
     -- @since 1.2.0
     MatchNoDatatypeInfo TyName
+  | -- | We tried to get the base functor for a type in the ASG context, but the base functor does not exist.
+    --   This can occur either because the type is not recursive and has no base functor, or because the type
+    --   itself does not exist. It does not seem important to distinguish between the two failure cases.
+    --
+    -- @since 1.3.0
+    BaseFunctorDoesNotExistFor TyName
+  | -- | 'app' was called with a number of instantiation arguments that does not match the number of
+    -- type variables bound in Count the CompT of the function to which arguments are being applied.
+    -- The first Int is the  number of bound tyvars in the function type, the second is the number of
+    -- instantiations supplied.
+    --
+    -- @since 1.3.0
+    WrongNumInstantiationsInApp (CompT Renamed) Int Int
+  | -- | A miscellaneous error, needed to catch various things that can go wrong during datatype preparation and
+    -- deserialization.
+    --
+    -- @since 1.3.0
+    OtherError Text
+  | -- | The stated algebra type for a catamorphism has an arity different to what we
+    -- expected. Algebras must have an arity of 1.
+    --
+    -- @since 1.3.0
+    CataWrongArity (CompT AbstractTy)
+  | -- | The stated algebra type for a catamorphism has a different return type
+    -- to what we expected. Algebras must have the same return type as the last
+    -- type argument to the base functor.
+    --
+    -- The first field of this error is the type we expected, the second is the
+    -- one we actually found.
+    --
+    -- @since 1.3.0
+    CataWrongOutputType (ValT AbstractTy) (ValT AbstractTy)
+  | -- | The stated algebra type's base functor does not correspond to any type
+    -- known to us.
+    --
+    -- @since 1.3.0
+    CataNoTypeForBaseFunctor TyName
+  | -- | The stated algebra type's \'base functor\' is monomorphic.
+    --
+    -- @since 1.3.0
+    CataMonomorphicBaseFunctor TyName
+  | -- | The stated algebra type's \'base functor\' is not a datatype.
+    --
+    -- @since 1.3.0
+    CataNotADatatypeBaseFunctor (ValT AbstractTy)
+  | -- | The stated algebra type is not rigid: that is, it binds type variables.
+    --
+    -- @since 1.3.0
+    CataNonRigidAlgebra (CompT AbstractTy)
+  | -- | The structure to be torn down by a catamorphism is not suitable given
+    -- the stated algebra type.
+    --
+    -- @since 1.3.0
+    CataInvalidStructure (CompT AbstractTy) (ValT AbstractTy)
+  | -- | The number of handlers provided to a catamorphism is wrong for the
+    -- stated algebra type.
+    --
+    -- @since 1.3.0
+    CataWrongNumberOfHandlers (CompT AbstractTy) (Vector Ref)
+  | -- | The (internal) unification for a catamorphism failed. If you see this kind
+    -- of error, it means that one of your handlers is not typed correctly. The
+    -- exact unifier error is provided to help debug.
+    --
+    -- @since 1.3.0
+    CataDidNotUnify (CompT AbstractTy) (Vector Ref) TypeAppError
+  | -- | The (internal) renaming of the handlers for a catamorphism failed. If
+    -- you see this kind of error, it means that one of your handlers is
+    -- malformed. The exact renaming error is provided to help debug.
+    --
+    -- @since 1.3.0
+    CataCouldNotRenameHandler (CompT AbstractTy) (Vector Ref) RenameError
+  | -- | The (internal) Boehm-Berrarducci form of the structure to be torn down by
+    -- a catamorphism did not rename correctly. If you see this error, this is a
+    -- bug, so please report it!
+    --
+    -- @since 1.3.0
+    CataCouldNotRenameBB (CompT AbstractTy) (Vector Ref) (CompT AbstractTy) RenameError
+  | -- | A handler given to a catamorphism is not of a value type.
+    --
+    -- @since 1.3.0
+    CataHandlerNotAValType ASGNodeType
+  | -- | We could not rename one of the required substitutions into the (internal)
+    -- Boehm-Berrarducci form of the structure to be torn down by a catamorphism
+    -- over a polymorphic structure. If you see this error, this is a bug, so
+    -- please report it!
+    --
+    -- @since 1.3.0
+    CataCouldNotRenameSubstitutions (CompT AbstractTy) (Vector Ref) (CompT AbstractTy) (Vector (ValT AbstractTy)) RenameError
+  | -- | We could not \'fix up\' the (internal) Boehm-Berrarducci form of the
+    -- structure to be torn down by a catamorphism over a polymorphic structure
+    -- after substitution. If you see this error, this is a bug, so please
+    -- report it!
+    --
+    -- @since 1.3.0
+    CataFixUpFailedForBB (CompT AbstractTy) (Vector Ref) (Vector (ValT AbstractTy)) (ValT Renamed) TypeAppError
+  | -- | The argument given to a catamorphism to be torn down is not a value type.
+    --
+    -- @since 1.3.0
+    CataNotAValueType ASGNodeType
+  | -- | The expected result type of a catamorphism according to its stated algebra
+    -- was not the same as what we actually got after applying handlers. If you
+    -- see this error, it means that one or more of your handlers is not
+    -- correct.
+    --
+    -- The first field is the type we expected, the second is what we got.
+    --
+    -- @since 1.3.0
+    CataUnexpectedResultType (ValT AbstractTy) (ValT AbstractTy)
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -271,7 +342,17 @@
 -- | A unique identifier for a node in a Covenant program.
 --
 -- @since 1.0.0
-newtype Id = Id Word64
+newtype Id
+  = -- | = Important note
+    --
+    -- Using this constructor is /not safe/. Do not do this unless you know
+    -- /exactly/ what you are doing. We expose this constructor, in a limited way,
+    -- to allow for certain kinds of testing, and /absolutely nothing else ever/.
+    -- Attempts to use this in ways it was not designed to /will/ break, this
+    -- interface is /not/ stable, and relying on it is /not/ a good plan.
+    --
+    -- @since 1.3.1
+    UnsafeMkId Word64
   deriving
     ( -- | @since 1.0.0
       Eq,
@@ -305,7 +386,17 @@
 -- | An argument passed to a function in a Covenant program.
 --
 -- @since 1.0.0
-data Arg = Arg DeBruijn (Index "arg") (ValT AbstractTy)
+data Arg
+  = -- | = Important note
+    --
+    -- Using this constructor is /not safe/. Do not do this unless you know
+    -- /exactly/ what you are doing. We expose this constructor, in a limited way,
+    -- to allow for certain kinds of testing, and /absolutely nothing else ever/.
+    -- Attempts to use this in ways it was not designed to /will/ break, this
+    -- interface is /not/ stable, and relying on it is /not/ a good plan.
+    --
+    -- @since 1.3.1
+    UnsafeMkArg DeBruijn (Index "arg") (ValT AbstractTy)
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -317,7 +408,7 @@
 
 -- Helper to get the type of an argument.
 typeArg :: Arg -> ValT AbstractTy
-typeArg (Arg _ _ t) = t
+typeArg (UnsafeMkArg _ _ t) = t
 
 -- | A general reference in a Covenant program.
 --
@@ -374,10 +465,14 @@
 -- @since 1.0.0
 data ValNodeInfo
   = LitInternal AConstant
-  | AppInternal Id (Vector Ref)
+  | -- | The 'CompT' is the \'fully concretified\' function type: that is,
+    -- all unifications with arguments have been done.
+    --
+    -- @since 1.3.0
+    AppInternal Id (Vector Ref) (Vector (Wedge BoundTyVar (ValT Void))) (CompT AbstractTy)
   | ThunkInternal Id
   | -- | @since 1.1.0
-    CataInternal Ref Ref
+    CataInternal (CompT AbstractTy) (Vector Ref) Ref
   | -- | @since 1.2.0
     DataConstructorInternal TyName ConstructorName (Vector Ref)
   | -- | @since 1.2.0
@@ -440,4 +535,17 @@
       Ord,
       -- | @since 1.0.0
       Show
+    )
+
+-- | Wrapper around an `Arg` that we know represents an in-scope type variable.
+--
+-- @since 1.2.0
+data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")
+  deriving stock
+    ( -- @since 1.2.0
+      Show,
+      -- @since 1.2.0
+      Eq,
+      -- @since 1.2.0
+      Ord
     )
diff --git a/src/Covenant/Internal/Type.hs b/src/Covenant/Internal/Type.hs
--- a/src/Covenant/Internal/Type.hs
+++ b/src/Covenant/Internal/Type.hs
@@ -207,6 +207,13 @@
 -- | The name of a data type. This refers specifically to non-\'flat\' types
 -- either provided by the ledger, or defined by the user.
 --
+-- User-defined 'TyName's must follow a set of naming rules, which will be checked. Specifically,
+-- a 'TyName' must begin with a capital letter and consist only of alphanumeric characters and
+-- underscores.
+--
+-- Compiler-generated 'TyName's are not bound by these conventions, and generated names for
+-- base functors in particular use the naming convention of prefixing @#@ to the parent type.
+--
 -- @since 1.1.0
 newtype TyName = TyName Text
   deriving
@@ -451,30 +458,30 @@
         _ -> False
 
 naturalBaseFunctor :: DataDeclaration AbstractTy
-naturalBaseFunctor = DataDeclaration "Natural_F" count1 constrs SOP
+naturalBaseFunctor = DataDeclaration "#Natural" count1 constrs SOP
   where
     constrs :: Vector (Constructor AbstractTy)
     constrs =
-      [ Constructor "ZeroNat_F" [],
-        Constructor "SuccNat_F" [Abstraction . BoundAt Z $ ix0]
+      [ Constructor "#ZeroNat" [],
+        Constructor "#SuccNat" [Abstraction . BoundAt Z $ ix0]
       ]
 
 negativeBaseFunctor :: DataDeclaration AbstractTy
-negativeBaseFunctor = DataDeclaration "Negative_F" count1 constrs SOP
+negativeBaseFunctor = DataDeclaration "#Negative" count1 constrs SOP
   where
     constrs :: Vector (Constructor AbstractTy)
     constrs =
-      [ Constructor "ZeroNeg_F" [],
-        Constructor "PredNeg_F" [Abstraction . BoundAt Z $ ix0]
+      [ Constructor "#ZeroNeg" [],
+        Constructor "#PredNeg" [Abstraction . BoundAt Z $ ix0]
       ]
 
 byteStringBaseFunctor :: DataDeclaration AbstractTy
-byteStringBaseFunctor = DataDeclaration "ByteString_F" count1 constrs SOP
+byteStringBaseFunctor = DataDeclaration "#ByteString" count1 constrs SOP
   where
     constrs :: Vector (Constructor AbstractTy)
     constrs =
-      [ Constructor "EmptyByteString_F" [],
-        Constructor "ConsByteString_F" [BuiltinFlat IntegerT, Abstraction . BoundAt Z $ ix0]
+      [ Constructor "#EmptyByteString" [],
+        Constructor "#ConsByteString" [BuiltinFlat IntegerT, Abstraction . BoundAt Z $ ix0]
       ]
 
 -- Helpers
diff --git a/src/Covenant/Internal/Unification.hs b/src/Covenant/Internal/Unification.hs
--- a/src/Covenant/Internal/Unification.hs
+++ b/src/Covenant/Internal/Unification.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE CPP #-}
-{-# LANGUAGE MultiWayIf #-}
 
 module Covenant.Internal.Unification
   ( TypeAppError (..),
@@ -11,17 +10,20 @@
     substitute,
     fixUp,
     reconcile,
+    lookupDatatypeInfo,
+    concretifyFT,
   )
 where
 
-import Control.Monad (foldM, unless, when)
-import Data.Ord (comparing)
 #if __GLASGOW_HASKELL__==908
 import Data.Foldable (foldl')
 #endif
+
+import Control.Applicative (Alternative ((<|>)))
+import Control.Monad (foldM, unless, when)
 import Control.Monad.Except (MonadError, catchError, throwError)
 import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask)
-import Covenant.Data (DatatypeInfo, mkDatatypeInfo)
+import Covenant.Data (DatatypeInfo)
 import Covenant.Index (Index, intCount, intIndex)
 import Covenant.Internal.Rename (RenameError, renameDatatypeInfo)
 import Covenant.Internal.Type
@@ -29,22 +31,22 @@
     BuiltinFlatT,
     CompT (CompT),
     CompTBody (CompTBody),
+    DataDeclaration (OpaqueData),
     Renamed (Rigid, Unifiable, Wildcard),
-    TyName (TyName),
+    TyName,
     ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),
-    byteStringBaseFunctor,
-    naturalBaseFunctor,
-    negativeBaseFunctor,
   )
+import Covenant.Type (CompT (CompN), CompTBody (ArgsAndResult))
 import Data.Kind (Type)
 import Data.Map (Map)
+import Data.Map qualified as M
 import Data.Map.Merge.Strict qualified as Merge
 import Data.Map.Strict qualified as Map
 import Data.Maybe (fromJust, mapMaybe)
+import Data.Ord (comparing)
 import Data.Set (Set)
 import Data.Set qualified as Set
 import Data.Text (Text)
-import Data.Text qualified as Text
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
 import Data.Vector.NonEmpty (NonEmptyVector)
@@ -114,42 +116,13 @@
 lookupDatatypeInfo ::
   TyName ->
   UnifyM (DatatypeInfo Renamed)
-lookupDatatypeInfo tn@(TyName rawTyName) =
+lookupDatatypeInfo tn =
   ask >>= \tyDict -> case preview (ix tn) tyDict of
-    Nothing -> checkForBaseFunctor tyDict
+    Nothing -> throwError . NoDatatypeInfo $ tn
     Just dti -> renamedToUnify . renameDatatypeInfo $ dti
   where
-    checkForBaseFunctor :: Map TyName (DatatypeInfo AbstractTy) -> UnifyM (DatatypeInfo Renamed)
-    checkForBaseFunctor tyDict = case Text.stripSuffix "_F" rawTyName of
-      Nothing -> throwError . NoDatatypeInfo $ tn
-      Just rawTyNameStub ->
-        if
-          -- Note (Koz, 12/08/2025): None of these specific cases should _ever_
-          -- fail. Thus, `fromRight` is safe here.
-          | rawTyNameStub == "Natural" ->
-              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ naturalBaseFunctor
-          | rawTyNameStub == "Negative" ->
-              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ negativeBaseFunctor
-          | rawTyNameStub == "ByteString" ->
-              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ byteStringBaseFunctor
-          -- We have something that _looks_ like a base functor, but not a
-          -- special builtin case. We thus need to ask the environment for the
-          -- recursive type it stands for, if it exists.
-          | otherwise -> do
-              let standinTyName = TyName rawTyNameStub
-              case preview (ix standinTyName) tyDict of
-                -- Now we have _truly_ missed.
-                Nothing -> throwError . NoDatatypeInfo $ tn
-                Just dti -> case view #baseFunctor dti of
-                  Nothing -> throwError . NoDatatypeInfo $ tn
-                  -- Since this is generated, it can't fail to rename
-                  Just (bfDd, _) -> renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ bfDd
     renamedToUnify :: Either RenameError (DatatypeInfo Renamed) -> UnifyM (DatatypeInfo Renamed)
     renamedToUnify = either (throwError . DatatypeInfoRenameFailed tn) pure
-    fromRight :: forall a b. (Show a) => Either a b -> b
-    fromRight = \case
-      Left err -> error . show $ err
-      Right x -> x
 
 lookupBBForm :: TyName -> UnifyM (ValT Renamed)
 lookupBBForm tn =
@@ -157,6 +130,14 @@
     Nothing -> throwError $ NoBBForm tn
     Just bbForm -> pure bbForm
 
+-- Opaque types do not (and cannot) have a BB form, which breaks unification machinery that assumes all inhabiated types
+-- have such a form. We need to branch on the "Opacity" of a type in `expectDatatype` and this lets us do that
+isOpaqueType :: TyName -> UnifyM Bool
+isOpaqueType tn =
+  lookupDatatypeInfo tn >>= \dti -> case view #originalDecl dti of
+    OpaqueData {} -> pure True
+    _ -> pure False
+
 -- | Given information about in-scope datatypes, a computation type, and a list
 -- of arguments (some of which may be errors), try to construct the type of the
 -- result of the application of those arguments to the computation.
@@ -180,7 +161,7 @@
   when (numArgsActual < numArgsExpected) $
     throwError $
       InsufficientArgs numArgsActual f ys
-  when (numArgsExpected > numArgsActual) $
+  when (numArgsActual > numArgsExpected) $
     throwError $
       ExcessArgs f (Vector.fromList ys)
   go curr (Vector.toList rest) ys
@@ -365,18 +346,32 @@
     -- the BB form using the arguments to the actual datatype.
     -- For example, the BB form of `Maybe` is: forall a r. r -> (a -> r) -> r
     -- which, if we concretify while attempting to unify with `Maybe Int`, becomes: `forall r. r -> (Int -> r) -> r`
+    --
+    -- Opaque datatypes are a special exception and are treated analogously to Builtins: They unify only with themselves,
+    -- unifiables, or wildcards.
     expectDatatype tn args = do
-      bbForm <- lookupBBForm tn
-      bbFormConcreteE <- concretify bbForm args
-      case actual of
-        Abstraction (Rigid _ _) -> unificationError
-        Abstraction _ -> noSubUnify
-        Datatype tn' args'
-          | tn' /= tn -> unificationError
-          | otherwise -> do
-              bbFormConcreteA <- concretify bbForm args'
-              unify bbFormConcreteE bbFormConcreteA
-        _ -> unificationError
+      isOpaqueType tn >>= \case
+        False -> do
+          bbForm <- lookupBBForm tn
+          bbFormConcreteE <- concretify bbForm args
+          case actual of
+            Abstraction (Rigid _ _) -> unificationError
+            Abstraction _ -> noSubUnify
+            Datatype tn' args'
+              | tn' /= tn -> unificationError
+              | otherwise -> do
+                  bbFormConcreteA <- concretify bbForm args'
+                  unify bbFormConcreteE bbFormConcreteA
+            _ -> unificationError
+        True -> case actual of
+          Abstraction Rigid {} -> unificationError
+          Abstraction _ -> noSubUnify
+          -- Opaque datatypes cannot be parameterized, so we only need to check the TyName
+          Datatype tn' _args ->
+            if tn == tn'
+              then noSubUnify
+              else unificationError
+          _ -> unificationError
     concretify :: ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed)
     concretify (ThunkT (CompT count (CompTBody fn))) args = fixUp $ ThunkT (CompT count (CompTBody newFn))
       where
@@ -414,3 +409,59 @@
           _ -> case new of
             Abstraction (Unifiable _) -> pure old
             _ -> throwError $ CouldNotReconcile i old new
+
+----- Extra stuff
+
+concretifyFT ::
+  CompT Renamed ->
+  Vector (Maybe (ValT Renamed)) ->
+  CompT Renamed
+concretifyFT (CompN cnt (ArgsAndResult fromFn res)) fromArgs = unfixedResult
+  where
+    unfixedResult :: CompT Renamed
+    unfixedResult = CompN cnt (ArgsAndResult subbedArgs subbedRes)
+
+    subbedArgs = substMany allSubstitutions <$> fromFn
+    subbedRes = substMany allSubstitutions res
+
+    substMany :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed
+    substMany subs val = foldl' (\acc (tv, ty) -> substitute tv ty acc) val subs
+
+    allUnifiables = Set.toList $ Vector.foldMap collectUnifiables fromFn
+
+    allSubstitutions = M.toList $ getInstantiations allUnifiables (Vector.toList fromFn) (Vector.toList fromArgs)
+
+getInstantiations :: [Index "tyvar"] -> [ValT Renamed] -> [Maybe (ValT Renamed)] -> Map (Index "tyvar") (ValT Renamed)
+getInstantiations [] _ _ = M.empty
+getInstantiations _ [] _ = M.empty
+getInstantiations _ _ [] = M.empty
+getInstantiations vs (_ : fEs) (Nothing : aEs) = getInstantiations vs fEs aEs
+getInstantiations (var : vars) fs@(fE : fEs) as@(aE' : aEs) =
+  -- somewhat subjective but I think doing it w/ fromJust makes the logic easier to follow here
+  let aE = fromJust aE'
+   in case instantiates (Unifiable var) aE fE of
+        Nothing -> getInstantiations [var] fEs aEs <> getInstantiations vars fs as
+        Just t -> M.insert var t $ getInstantiations vars fs as
+
+instantiates ::
+  Renamed ->
+  ValT Renamed -> -- the "more concrete type", usually the actual argument from 'app'
+  ValT Renamed -> -- the "more polymorphic type', usually from the fn definition
+  Maybe (ValT Renamed)
+instantiates var concrete abstract = case (concrete, abstract) of
+  (x, Abstraction a) -> if var == a then Just x else Nothing -- N.b. we need to be sure we only run this w/ unifiables as the first arg
+  (ThunkT (CompN _ concreteFn), ThunkT (CompN _ abstractFn)) ->
+    let concreteFn' = Vector.toList $ compTBodyToVec concreteFn
+        abstractFn' = Vector.toList $ compTBodyToVec abstractFn
+     in go concreteFn' abstractFn'
+  (Datatype tnC argsC, Datatype tnA argsA)
+    | tnC == tnA -> go (Vector.toList argsC) (Vector.toList argsA)
+  _ -> Nothing
+  where
+    go :: [ValT Renamed] -> [ValT Renamed] -> Maybe (ValT Renamed)
+    go [] _ = Nothing
+    go _ [] = Nothing
+    go (c : cs) (a : as) = instantiates var c a <|> go cs as
+
+compTBodyToVec :: forall a. CompTBody a -> Vector (ValT a)
+compTBodyToVec (ArgsAndResult args res) = Vector.snoc args res
diff --git a/src/Covenant/JSON.hs b/src/Covenant/JSON.hs
new file mode 100644
--- /dev/null
+++ b/src/Covenant/JSON.hs
@@ -0,0 +1,1529 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE RankNTypes #-}
+
+-- |
+-- Module: Covenant.JSON
+-- Copyright: (C) MLabs 2025
+-- License: Apache 2.0
+-- Maintainer: koz@mlabs.city, sean@mlabs.city
+--
+-- JSON serialization and deserialization utilities for the ASG.
+--
+-- = Note on Sum Type Encoding:
+--
+-- Unless otherwise noted, a Haskell sum type like:
+--
+--    @data Foo = Bar | Baz Int@
+--
+-- Is encoded to JSON using @{tag: \<CTOR NAME\>, fields: [\<Arg1\>, \<Arg2\>, \<ArgN\>]}@
+--
+-- This is used for all Haskell sum types which do /not/ have 'LabelOptic'
+-- instnaces. For those with field names given by such instances, the @fields@
+-- part of the encoded sum is not an array of arguments, but instead a JSON
+-- object, with fields whose names correspond to the label optics. Comments make
+-- it clear which types are encoded in which way.
+--
+-- @since 1.3.0
+module Covenant.JSON
+  ( -- * Serialization
+    Version (..),
+    SerializeErr (..),
+    mkDatatypeInfos,
+    compileAndSerialize,
+
+    -- * Deserialization
+    DeserializeErr (..),
+    deserializeAndValidate,
+    deserializeAndValidate_,
+  )
+where
+
+#if __GLASGOW_HASKELL__==908
+import Data.Foldable (foldl')
+#endif
+import Control.Exception (throwIO)
+import Control.Monad (foldM, unless)
+import Control.Monad.Error.Class (MonadError (throwError))
+import Control.Monad.HashCons (MonadHashCons (lookupRef))
+import Control.Monad.IO.Class (MonadIO (liftIO))
+import Control.Monad.Reader (local)
+import Control.Monad.Trans.Except (ExceptT, runExceptT)
+import Covenant.ASG
+  ( ASG (ASG),
+    ASGBuilder,
+    ASGNode,
+    Arg,
+    CompNodeInfo,
+    CovenantError,
+    Id,
+    Ref,
+    ValNodeInfo,
+    app,
+    builtin1,
+    builtin2,
+    builtin3,
+    builtin6,
+    cata,
+    dataConstructor,
+    err,
+    force,
+    lam,
+    lit,
+    match,
+    runASGBuilder,
+    thunk,
+  )
+import Covenant.Constant (AConstant (ABoolean, AByteString, AString, AUnit, AnInteger))
+import Covenant.Data (DatatypeInfo, mkDatatypeInfo, primBaseFunctorInfos)
+import Covenant.DeBruijn (DeBruijn, asInt)
+import Covenant.Index (Count, Index, intCount, intIndex)
+import Covenant.Internal.KindCheck (checkDataDecls)
+import Covenant.Internal.Strategy
+  ( InternalStrategy
+      ( InternalAssocMapStrat,
+        InternalListStrat,
+        InternalOpaqueStrat,
+        InternalPairStrat
+      ),
+  )
+import Covenant.Internal.Term
+  ( ASGNode (ACompNode, AValNode, AnError),
+    Arg (UnsafeMkArg),
+    BoundTyVar (BoundTyVar),
+    CompNodeInfo
+      ( Builtin1Internal,
+        Builtin2Internal,
+        Builtin3Internal,
+        Builtin6Internal,
+        ForceInternal,
+        LamInternal
+      ),
+    CovenantTypeError (OtherError),
+    Id (UnsafeMkId),
+    Ref (AnArg, AnId),
+    ValNodeInfo
+      ( AppInternal,
+        CataInternal,
+        DataConstructorInternal,
+        LitInternal,
+        MatchInternal,
+        ThunkInternal
+      ),
+  )
+import Covenant.Internal.Type
+  ( AbstractTy (BoundAt),
+    CompT (CompT),
+    CompTBody (CompTBody),
+    ConstructorName (ConstructorName),
+    DataDeclaration (OpaqueData),
+    ValT (BuiltinFlat, ThunkT),
+  )
+import Covenant.Prim
+  ( OneArgFunc
+      ( BData,
+        BLS12_381_G1_compress,
+        BLS12_381_G1_neg,
+        BLS12_381_G1_uncompress,
+        BLS12_381_G2_compress,
+        BLS12_381_G2_neg,
+        BLS12_381_G2_uncompress,
+        Blake2b_224,
+        Blake2b_256,
+        ComplementByteString,
+        CountSetBits,
+        DecodeUtf8,
+        EncodeUtf8,
+        FindFirstSetBit,
+        FstPair,
+        HeadList,
+        IData,
+        Keccak_256,
+        LengthOfByteString,
+        ListData,
+        MapData,
+        NullList,
+        Ripemd_160,
+        SerialiseData,
+        Sha2_256,
+        Sha3_256,
+        SndPair,
+        TailList,
+        UnBData,
+        UnConstrData,
+        UnIData,
+        UnListData,
+        UnMapData
+      ),
+    SixArgFunc (ChooseData),
+    ThreeArgFunc
+      ( AndByteString,
+        ChooseList,
+        ExpModInteger,
+        IfThenElse,
+        IntegerToByteString,
+        OrByteString,
+        VerifyEcdsaSecp256k1Signature,
+        VerifyEd25519Signature,
+        VerifySchnorrSecp256k1Signature,
+        WriteBits,
+        XorByteString
+      ),
+    TwoArgFunc
+      ( AddInteger,
+        AppendByteString,
+        AppendString,
+        BLS12_381_G1_add,
+        BLS12_381_G1_equal,
+        BLS12_381_G1_hashToGroup,
+        BLS12_381_G1_scalarMul,
+        BLS12_381_G2_add,
+        BLS12_381_G2_equal,
+        BLS12_381_G2_hashToGroup,
+        BLS12_381_G2_scalarMul,
+        BLS12_381_finalVerify,
+        BLS12_381_millerLoop,
+        BLS12_381_mulMlResult,
+        ByteStringToInteger,
+        ChooseUnit,
+        ConsByteString,
+        ConstrData,
+        DivideInteger,
+        EqualsByteString,
+        EqualsData,
+        EqualsInteger,
+        EqualsString,
+        IndexByteString,
+        LessThanByteString,
+        LessThanEqualsByteString,
+        LessThanEqualsInteger,
+        LessThanInteger,
+        MkCons,
+        MkPairData,
+        ModInteger,
+        MultiplyInteger,
+        QuotientInteger,
+        ReadBit,
+        RemainderInteger,
+        ReplicateByte,
+        RotateByteString,
+        ShiftByteString,
+        SubtractInteger,
+        Trace
+      ),
+  )
+import Covenant.Type
+  ( BuiltinFlatT
+      ( BLS12_381_G1_ElementT,
+        BLS12_381_G2_ElementT,
+        BLS12_381_MlResultT,
+        BoolT,
+        ByteStringT,
+        IntegerT,
+        StringT,
+        UnitT
+      ),
+    Constructor (Constructor),
+    DataDeclaration (DataDeclaration),
+    DataEncoding (BuiltinStrategy, PlutusData, SOP),
+    PlutusDataConstructor
+      ( PlutusB,
+        PlutusConstr,
+        PlutusI,
+        PlutusList,
+        PlutusMap
+      ),
+    PlutusDataStrategy (EnumData, NewtypeData, ProductListData),
+    TyName (TyName),
+    ValT (Abstraction, Datatype),
+  )
+import Covenant.Type qualified as Ty
+import Data.Aeson
+  ( FromJSON (parseJSON),
+    ToJSON (toEncoding),
+    Value,
+    eitherDecodeFileStrict,
+    (.=),
+  )
+import Data.Aeson.Encoding
+  ( Encoding,
+    encodingToLazyByteString,
+    int,
+    list,
+    pair,
+    pairs,
+    text,
+  )
+import Data.Aeson.KeyMap qualified as KM
+import Data.Aeson.Types
+  ( Array,
+    Key,
+    Object,
+    Parser,
+    Value (Object, String),
+    withArray,
+    withObject,
+    withText,
+  )
+import Data.Bifunctor (Bifunctor (first))
+import Data.ByteString (ByteString)
+import Data.ByteString.Lazy qualified as BL
+import Data.Char (isAlphaNum, isUpper)
+import Data.Foldable (toList, traverse_)
+import Data.Kind (Type)
+import Data.Map (Map)
+import Data.Map qualified as M
+import Data.Maybe (fromJust)
+import Data.Set qualified as S
+import Data.Text (Text)
+import Data.Text qualified as T
+import Data.Vector (Vector)
+import Data.Vector qualified as Vector
+import Data.Vector.NonEmpty qualified as NEV
+import Data.Void (Void, absurd)
+import Data.Wedge (Wedge (Here, Nowhere, There))
+import GHC.TypeLits (KnownSymbol, Symbol)
+import Optics.Core (preview, review, set, view)
+import Text.Hex qualified as Hex
+
+-- | The errors that can arise from 'compileAndSerialize' not stemming from
+-- 'IO'.
+--
+-- @since 1.3.0
+data SerializeErr
+  = -- | A datatype was specified in a way that isn't valid.
+    DatatypeConversionFailure String
+  | -- | The supplied ASG failed to compile.
+    ASGCompilationFailure CovenantError
+  deriving stock
+    ( -- @since 1.3.0
+      Show,
+      -- @since 1.3.0
+      Eq
+    )
+
+-- | Given a 'FilePath' to write output to, a collection of data declarations,
+-- an 'ASGBuilder' and a version tag, compile the ASG, then write it to the
+-- given file path in its JSON serialized form, together with the data types.
+--
+-- @since 1.3.0
+compileAndSerialize ::
+  forall (a :: Type).
+  FilePath ->
+  [DataDeclaration AbstractTy] ->
+  ASGBuilder a ->
+  Version ->
+  ExceptT SerializeErr IO ()
+compileAndSerialize path decls asgBuilder version = do
+  case mkDatatypeInfos decls of
+    Left err' -> throwError . DatatypeConversionFailure $ err'
+    Right infos -> case runASGBuilder infos asgBuilder of
+      Left err' -> throwError . ASGCompilationFailure $ err'
+      Right (ASG asg) -> do
+        let cu = CompilationUnit (Vector.fromList decls) asg version
+        liftIO $ writeJSONWith path cu encodeCompilationUnit
+
+-- | The errors that can arise from 'deserializeAndValidate' not stemming from
+-- 'IO'.
+--
+-- @since 1.3.0
+data DeserializeErr
+  = -- | The serial form's JSON was not valid. This means that the given file
+    -- cannot be an ASG.
+    JSONParseFailure String
+  | -- | The deserialized JSON corresponds to an ASG, but not a valid one.
+    ASGValidationFail CovenantError
+  deriving stock
+    ( -- @since 1.3.0
+      Show,
+      -- @since 1.3.0
+      Eq
+    )
+
+-- | Given a 'FilePath' to a serialized ASG, decode it if possible.
+--
+-- @since 1.3.0
+deserializeAndValidate ::
+  FilePath ->
+  ExceptT DeserializeErr IO ASG
+deserializeAndValidate path = do
+  rawCU <- readJSON @CompilationUnit path
+  case validateCompilationUnit rawCU of
+    Left err' -> throwError . ASGValidationFail $ err'
+    Right asg -> pure asg
+
+-- | Like 'deserializeAndValidate' but runs directly in 'IO'.
+--
+-- = Note
+--
+-- This is mostly designed for use in tests, as it has no ability to \'trap\'
+-- validation or deserialization errors. You most likely want
+-- 'deserializeAndValidate'.
+--
+-- @since 1.3.0
+deserializeAndValidate_ :: FilePath -> IO ASG
+deserializeAndValidate_ path =
+  runExceptT (deserializeAndValidate path) >>= either (throwIO . userError . show) pure
+
+-- | Represents a Covenant version. This is currently just a tag, but may be
+-- used in the future to enforce compatibility.
+--
+-- @since 1.3.0
+data Version = Version {_major :: Int, _minor :: Int}
+  deriving stock
+    ( -- | @since 1.3.0
+      Show,
+      -- | @since 1.3.0
+      Eq,
+      -- | @since 1.3.0
+      Ord
+    )
+
+data CompilationUnit
+  = CompilationUnit
+  { _datatypes :: Vector (DataDeclaration AbstractTy),
+    _asg :: Map Id ASGNode,
+    _version :: Version
+  }
+  deriving stock (Show, Eq)
+
+-- NOTE: We run w/ an empty map because the declarations get inserted after they are kindchecked
+validateCompilationUnit :: CompilationUnit -> Either CovenantError ASG
+validateCompilationUnit = runASGBuilder M.empty . validateCompilationUnit'
+
+validateCompilationUnit' :: CompilationUnit -> ASGBuilder ()
+validateCompilationUnit' (CompilationUnit datatypes asg _) = do
+  case mkDatatypeInfos (toList datatypes) of
+    Left err' -> throwError $ OtherError (T.pack err')
+    Right infos -> local (set #datatypeInfo infos) $ traverse_ go (M.toList asg)
+  where
+    go :: (Id, ASGNode) -> ASGBuilder ()
+    go (parsedId, parsedNode) = case parsedNode of
+      ACompNode compT compInfo -> case compInfo of
+        Builtin1Internal bi1 -> checkNode "builtin1" (builtin1 bi1)
+        Builtin2Internal bi2 -> checkNode "builtin2" (builtin2 bi2)
+        Builtin3Internal bi3 -> checkNode "builtin3" (builtin3 bi3)
+        Builtin6Internal bi6 -> checkNode "builtin6" (builtin6 bi6)
+        LamInternal bodyRef -> checkNode "lam" $ lam compT (pure bodyRef)
+        ForceInternal ref -> checkNode "force" $ force ref
+      AValNode _ valInfo -> case valInfo of
+        LitInternal aConstant -> checkNode "Lit" (lit aConstant)
+        AppInternal fId argRefs instTys _ -> checkNode "App" (app fId argRefs instTys)
+        ThunkInternal i -> checkNode "Thunk" (thunk i)
+        CataInternal t r1 r2 -> checkNode "Cata" (cata t r1 r2)
+        DataConstructorInternal tn cn args -> checkNode "DataConstructor" (dataConstructor tn cn args)
+        MatchInternal scrut matcharms -> checkNode "Match" (match scrut matcharms)
+      AnError -> checkNode "errorNode" err
+      where
+        checkNode :: String -> ASGBuilder Id -> ASGBuilder ()
+        checkNode msg constructedId = do
+          xid <- constructedId
+          unless (parsedId == xid) $ error $ msg <> " id mismatch"
+          lookupRef xid >>= \case
+            Nothing -> error $ msg <> " node not found"
+            Just asgNode ->
+              unless (asgNode == parsedNode) $ do
+                let errMsg =
+                      "unexpected "
+                        <> msg
+                        <> " node"
+                        <> "\n  expected: "
+                        <> show parsedNode
+                        <> "\n  actual: "
+                        <> show asgNode
+                error errMsg
+
+{- CompilationUnit
+
+   Encodes as an object. The maps are represented by KV pairs in arrays. Example:
+
+   {datatypes: [{k: "Maybe", v: ...}, {k: "Foo", v: ...}],
+    asg: [{k: 0, v: ...}],
+    version: {major: 1, minor: 2}
+   }
+-}
+
+encodeCompilationUnit :: CompilationUnit -> Encoding
+encodeCompilationUnit (CompilationUnit datatypes asg version) =
+  pairs $
+    pair "datatypes" (list encodeDataDeclarationAbstractTy . toList $ datatypes)
+      <> pair "asg" (encodeMap encodeId encodeASGNode asg)
+      <> pair "version" (encodeVersion version)
+
+instance FromJSON CompilationUnit where
+  parseJSON = withObject "CompilationUnit" $ \obj -> do
+    datatypes <- lookupAndParse' obj "datatypes" $ withArray "datatype" $ \arr -> traverse decodeDataDeclarationAbstractTy arr
+    asg <- lookupAndParse' obj "asg" $ decodeMap decodeId decodeASGNode
+    version <- lookupAndParse' obj "version" decodeVersion
+    pure $ CompilationUnit datatypes asg version
+
+{- Version
+
+   Serializes as an object with the fields you'd expect.
+
+     Version 1 2
+   ->
+     {major: 1, minor: 2}
+
+-}
+
+-- |  @since 1.3.0
+encodeVersion :: Version -> Encoding
+encodeVersion (Version major minor) = pairs ("major" .= major <> "minor" .= minor)
+
+-- | @since 1.3.0
+decodeVersion :: Value -> Parser Version
+decodeVersion = withObject "Version" $ \obj -> do
+  major <- withField "major" parseJSON obj
+  minor <- withField "minor" parseJSON obj
+  pure $ Version major minor
+
+{- DataDeclaration & its components -}
+
+{- Special handling to account for base functors (including "strange" base functors for Natural)
+
+   {tyName: "Foo"}
+   | {baseFunctorOf: "Foo"}
+   | "NaturalBF" | "NegativeBF"
+-}
+
+-- | @since 1.3.0
+encodeTyName :: TyName -> Encoding
+encodeTyName (TyName tn) = case T.stripPrefix "#" tn of
+  Nothing -> pairs ("tyName" .= tn)
+  Just rootTypeName -> case rootTypeName of
+    "Natural" -> text "NaturalBF"
+    "Negative" -> text "NegativeBF"
+    other -> pairs ("baseFunctorOf" .= other)
+
+-- | The type name must conform with the type naming rules, i.e. it must
+--   1. Begin with a capital letter
+--   2. Consist only of alphanumeric characters and underscores
+-- @since 1.3.0
+decodeTyName :: Value -> Parser TyName
+decodeTyName = \case
+  String str -> case str of
+    "NaturalBF" -> pure "#Natural"
+    "NegativeBF" -> pure "#Negative"
+    other -> fail $ "Expected 'NaturalBF' or 'NegativeBF' but got " <> T.unpack other
+  Object km -> case KM.lookup "tyName" km of
+    Nothing -> case KM.lookup "baseFunctorOf" km of
+      Nothing -> fail "Received an object for TyName, but it didn't have any valid fields"
+      Just rootType -> TyName . ("#" <>) <$> (parseJSON rootType >>= validateProperName)
+    Just tn -> TyName <$> (parseJSON tn >>= validateProperName)
+  other -> fail $ "Expected a String or Object for TyName, but got: " <> show other
+
+validateProperName :: Text -> Parser Text
+validateProperName nm
+  | T.null nm = fail "Empty String cannot be a TyName or ConstructorName"
+  | (isUpper (T.head nm) || T.head nm == '#') && T.all (\c -> isAlphaNum c || c == '_') nm = pure nm
+  | otherwise = fail $ "Could not validate TyName or ConstructorName '" <> T.unpack nm <> "'"
+
+{- Encodes as a simple JSON string, e.g.
+   ConstructorName "Foo" -> "Foo"
+-}
+
+-- | @since 1.3.0
+encodeConstructorName :: ConstructorName -> Encoding
+encodeConstructorName (ConstructorName cn) = toEncoding cn
+
+-- | The ctor name must conform with the ctor naming rules, i.e. it must
+--   1. Begin with a capital letter
+--   2. Consist only of alphanumeric characters and underscores
+-- @since 1.3.0
+decodeConstructorName :: Value -> Parser ConstructorName
+decodeConstructorName = withText "ConstructorName" $ fmap ConstructorName . validateProperName
+
+{- Encodes as an object. E.g.:
+
+   Constructor "Just" [IntegerT]
+   ->
+   { constructorName: "Just"
+   , constructorArgs: [...]}
+
+-}
+
+-- | @since 1.3.0
+encodeConstructor :: Constructor AbstractTy -> Encoding
+encodeConstructor (Constructor nm args) =
+  let encodedArgs = list encodeValTAbstractTy $ Vector.toList args
+   in pairs $
+        pair "constructorName" (encodeConstructorName nm)
+          <> pair "constructorArgs" encodedArgs
+
+-- | @since 1.3.0
+decodeConstructor :: Value -> Parser (Constructor AbstractTy)
+decodeConstructor = withObject "Constructor" $ \obj -> do
+  ctorNm <- lookupAndParse' obj "constructorName" decodeConstructorName
+  ctorArgs <-
+    lookupAndParse' obj "constructorArgs" $
+      withArray "Constructor Args" (traverse decodeValTAbstractTy)
+  pure $ Constructor ctorNm ctorArgs
+
+{- DataEncoding encodes as a typical sum type, and will look like:
+
+   {tag: "SOP", fields: []}
+   | {tag: "PlutusData", fields: [...]}
+   | {tag: "BuiltinStrategy", fields: [...]}
+-}
+
+-- | @since 1.3.0
+encodeDataEncoding :: DataEncoding -> Encoding
+encodeDataEncoding = \case
+  SOP -> taggedFields "SOP" []
+  PlutusData strat -> taggedFields "PlutusData" [encodePlutusDataStrategy strat]
+  BuiltinStrategy internalStrat -> taggedFields "BuiltinStrategy" [encodeInternalStrategy internalStrat]
+
+-- | @since 1.3.0
+decodeDataEncoding :: Value -> Parser DataEncoding
+decodeDataEncoding = withObject "DataEncoding" go
+  where
+    go :: Object -> Parser DataEncoding
+    go obj = do
+      tagStr <- lookupAndParse' obj "tag" (parseJSON @Text)
+      fieldsArrVal <- lookupAndParse' obj "fields" pure
+      mfield0 <- withArray "index 0" (\arr -> pure $ arr Vector.!? 0) fieldsArrVal
+      case tagStr of
+        "SOP" -> pure SOP
+        otherTag -> case mfield0 of
+          Nothing -> fail "No fields present when deserializing a PlutusData"
+          Just field0 -> case otherTag of
+            "PlutusData" -> PlutusData <$> decodePlutusDataStrategy field0
+            "BuiltinStrategy" -> BuiltinStrategy <$> decodeInternalStrategy field0
+            other -> fail $ "Invalid DataEncoding tag: " <> show other
+
+{- PlutusDataStrategy encodes as a typical sum type. (Omitting the 'fields' field b/c it's an enumeration)
+
+   {tag: "EnumData"}
+   | {tag: "ProductListData"}
+   | {tag: "ConstrData"}
+   | {tag: "NewtypeData"}
+
+-}
+
+-- | @since 1.3.0
+encodePlutusDataStrategy :: PlutusDataStrategy -> Encoding
+encodePlutusDataStrategy = encodeEnum
+
+-- | @since 1.3.0
+decodePlutusDataStrategy :: Value -> Parser PlutusDataStrategy
+decodePlutusDataStrategy =
+  caseOnTag
+    [ "EnumData" :=> constM EnumData,
+      "ProductListData" :=> constM ProductListData,
+      "ConstrData" :=> constM Ty.ConstrData,
+      "NewtypeData" :=> constM NewtypeData
+    ]
+
+{- InternalStrategy encodes as a typical enumeration type:
+  {tag: "InternalListStrat"}
+  | {tag: "InternalPairStrat"}
+  | {tag: "InternalDataStrat"}
+  | {tag: "InternalAssocMapStrat"}
+  | {tag: "InternalOpaqueStrat"}
+
+-}
+encodeInternalStrategy :: InternalStrategy -> Encoding
+encodeInternalStrategy = encodeEnum
+
+decodeInternalStrategy :: Value -> Parser InternalStrategy
+decodeInternalStrategy =
+  caseOnTag
+    [ "InternalListStrat" :=> constM InternalListStrat,
+      "InternalPairStrat" :=> constM InternalPairStrat,
+      "InternalAssocMapStrat" :=> constM InternalAssocMapStrat,
+      "InternalOpaqueStrat" :=> constM InternalOpaqueStrat
+    ]
+
+{- PlutusDataConstructor encodes as a typical enumeration type:
+
+  {tag: "PlutusI"}
+  | {tag: "PlutusB"}
+  | {tag: "PlutusConstr"}
+  | {tag: "PlutusList"}
+  | {tag: PlutusMap}
+
+-}
+
+-- | @since 1.3.0
+encodePlutusDataConstructor :: PlutusDataConstructor -> Encoding
+encodePlutusDataConstructor = encodeEnum
+
+-- | @since 1.3.0
+decodePlutusDataConstructor :: Value -> Parser PlutusDataConstructor
+decodePlutusDataConstructor =
+  caseOnTag
+    [ "PlutusI" :=> constM PlutusI,
+      "PlutusB" :=> constM PlutusB,
+      "PlutusConstr" :=> constM PlutusConstr,
+      "PlutusList" :=> constM PlutusList,
+      "PlutusMap" :=> constM PlutusMap
+    ]
+
+{- DataDeclaration AbstractTy is a bit atypical. It is a sum type, but we encode
+   the arguments to the `DataDeclaration` constructor as an object instead of an array
+   (to reduce the possibility for frontend errors).
+
+   For example, if we have:
+
+     @DataDeclaration "Maybe" (Count 1) [...Nothing...,...Just...] SOP@
+
+   It will seralize like:
+
+     {tag: "DataDeclaration"
+     , fields: {
+        datatypeName: "Maybe",
+        datatypeBinders: 1,
+        datatypeConstructors: [...],
+        datatypeEncoding: {tag: "SOP"}
+     }}
+
+   For consistency, we do the same thing with Opaques. E.g.:
+
+     @OpaqueData "Foo" [Plutus_I]@
+
+   Will serialize to:
+
+     { tag: "OpaqueData"
+     , fields: {
+       datatypeName: "Foo",
+       opaquePlutusConstructors: [{tag: "Plutus_I"}]
+     }}
+-}
+
+-- | @since 1.3.0
+encodeDataDeclarationAbstractTy :: DataDeclaration AbstractTy -> Encoding
+encodeDataDeclarationAbstractTy = \case
+  DataDeclaration nm cnt ctors enc ->
+    let fieldObj =
+          pairs $
+            pair "datatypeName" (encodeTyName nm)
+              <> pair "datatypeBinders" (encodeCount cnt)
+              <> pair "datatypeConstructors" (list encodeConstructor . Vector.toList $ ctors)
+              <> pair "datatypeEncoding" (encodeDataEncoding enc)
+     in pairs $ pair "tag" "DataDeclaration" <> pair "fields" fieldObj
+  OpaqueData nm plutusCtors ->
+    let fieldObj =
+          pairs $
+            pair "datatypeName" (encodeTyName nm)
+              <> pair "opaquePlutusConstructors" (list encodePlutusDataConstructor . toList $ plutusCtors)
+     in pairs $ pair "tag" "OpaqueData" <> pair "fields" fieldObj
+
+-- | @since 1.3.0
+decodeDataDeclarationAbstractTy :: Value -> Parser (DataDeclaration AbstractTy)
+decodeDataDeclarationAbstractTy =
+  caseOnTag
+    [ "DataDeclaration" :=> goDataDecl,
+      "OpaqueData" :=> goOpaqueData
+    ]
+  where
+    goDataDecl :: Object -> Parser (DataDeclaration AbstractTy)
+    goDataDecl obj = do
+      fieldsObj <- lookupAndParse' obj "fields" (withObject "Datatype fields" pure)
+      dtName <- lookupAndParse' fieldsObj "datatypeName" decodeTyName
+      dtBinders <- lookupAndParse' fieldsObj "datatypeBinders" decodeCount
+      dtCtors <- lookupAndParse' fieldsObj "datatypeConstructors" (withArray "Datatype ctors" (traverse decodeConstructor))
+      dtEncoding <- lookupAndParse' fieldsObj "datatypeEncoding" decodeDataEncoding
+      pure $ DataDeclaration dtName dtBinders dtCtors dtEncoding
+
+    goOpaqueData :: Object -> Parser (DataDeclaration AbstractTy)
+    goOpaqueData obj = do
+      fieldsObj <- lookupAndParse' obj "fields" (withObject "Datatype fields (Opaque)" pure)
+      dtName <- lookupAndParse' fieldsObj "datatypeName" decodeTyName
+      plutusCtors <-
+        lookupAndParse'
+          fieldsObj
+          "opaquePlutusConstructors"
+          (withArray "Opaque Plutus Ctors" (traverse decodePlutusDataConstructor))
+      pure $ OpaqueData dtName (S.fromList . Vector.toList $ plutusCtors)
+
+{- ASG Specific Types & Components
+
+-}
+
+{- Id encodes directly as a number. E.g.:
+
+   @Id 101@ -> 101
+-}
+
+-- | @since 1.3.0
+encodeId :: Id -> Encoding
+encodeId (UnsafeMkId n) = toEncoding n
+
+-- | @since 1.3.0
+decodeId :: Value -> Parser Id
+decodeId = fmap UnsafeMkId . parseJSON
+
+{- Ref encodes as a typical sum type without named fields:
+
+   {tag: "AnArg", fields: [...]}
+   | {tag: "AnId": fields: [101]}
+-}
+
+-- | @since 1.3.0
+encodeRef :: Ref -> Encoding
+encodeRef = \case
+  AnArg arg' -> taggedFields "AnArg" [encodeArg arg']
+  AnId i -> taggedFields "AnId" [encodeId i]
+
+-- | @since 1.3.0
+decodeRef :: Value -> Parser Ref
+decodeRef =
+  caseOnTag
+    [ "AnArg" :=> withFields (withIndex 0 (fmap AnArg . decodeArg)),
+      "AnId" :=> withFields (withIndex 0 (fmap AnId . decodeId))
+    ]
+
+{- Arg encodes as an object, e.g.:
+
+   {argDeBruijn: 0,
+    argIndex: 1,
+    argType: ...
+   }
+
+-}
+
+-- | @since 1.3.0
+encodeArg :: Arg -> Encoding
+encodeArg (UnsafeMkArg db ix ty) =
+  let dbEnc = encodeDeBruijn db
+      ixEnc = encodeIndex ix
+      tyEnc = encodeValTAbstractTy ty
+   in pairs $
+        pair "argDeBruijn" dbEnc
+          <> pair "argIndex" ixEnc
+          <> pair "argType" tyEnc
+
+-- | @since 1.3.0
+decodeArg :: Value -> Parser Arg
+decodeArg = withObject "Arg" $ \obj -> do
+  argDB <- withField "argDeBruijn" decodeDeBruijn obj
+  argIX <- withField "argIndex" decodeIndex obj
+  argTy <- withField "argType" decodeValTAbstractTy obj
+  pure $ UnsafeMkArg argDB argIX argTy
+
+{- AConstant
+
+   Serializes as a sum type without named fields:
+
+   {tag: "AUnit"}
+   | {tag: "ABoolean", fields: [true]}
+   | {tag: "AnInteger", fields: [22]}
+   | {tag: "AByteString", fields: ["\0x32"]}
+   | {tag: "AString", fields: ["Hello"]}
+
+-}
+
+-- | @since 1.3.0
+encodeAConstant :: AConstant -> Encoding
+encodeAConstant = \case
+  AUnit -> pairs $ pair "tag" "AUnit"
+  ABoolean b -> taggedFields "ABoolean" [toEncoding b]
+  AnInteger i -> taggedFields "AnInteger" [toEncoding i]
+  AByteString bs -> taggedFields "AByteString" [toEncoding . Hex.encodeHex $ bs]
+  AString str -> taggedFields "AString" [toEncoding str]
+
+-- | @since 1.3.0
+decodeAConstant :: Value -> Parser AConstant
+decodeAConstant =
+  caseOnTag
+    [ "AUnit" :=> constM AUnit,
+      "ABoolean" :=> withField0 (fmap ABoolean . parseJSON),
+      "AnInteger" :=> withField0 (fmap AnInteger . parseJSON),
+      "AByteString" :=> withField0 (fmap AByteString . decodeByteStringHex),
+      "AString" :=> withField0 (fmap AString . parseJSON)
+    ]
+
+{- ValNodeInfo
+
+   Serializes as a sum type without named fields:
+
+   {tag: "Lit", fields: [a]}
+   | {tag: "App", fields: [a,b,c,d]}
+   | {tag: "Thunk",fields: [a]}
+   | {tag: "Cata", fields: [a,b]}
+   | {tag: "DataConstructor", fields: [a,b,c]}
+   | {tag: "Match", fields: [a,b]}
+
+-}
+
+-- | @since 1.3.0
+encodeValNodeInfo :: ValNodeInfo -> Encoding
+encodeValNodeInfo = \case
+  LitInternal aconst -> taggedFields "Lit" [encodeAConstant aconst]
+  AppInternal f args instTys fTy ->
+    taggedFields
+      "App"
+      [ encodeId f,
+        list encodeRef . toList $ args,
+        list encodeInstTy . toList $ instTys,
+        encodeCompT encodeAbstractTy fTy
+      ]
+  ThunkInternal f -> taggedFields "Thunk" [encodeId f]
+  CataInternal t handlers r2 -> taggedFields "Cata" [encodeCompT encodeAbstractTy t, list encodeRef . toList $ handlers, encodeRef r2]
+  DataConstructorInternal tn cn args ->
+    taggedFields
+      "DataConstructor"
+      [ encodeTyName tn,
+        encodeConstructorName cn,
+        list encodeRef . toList $ args
+      ]
+  MatchInternal scrut branches ->
+    taggedFields "Match" [encodeRef scrut, list encodeRef . toList $ branches]
+
+-- | @since 1.3.0
+decodeValNodeInfo :: Value -> Parser ValNodeInfo
+decodeValNodeInfo =
+  caseOnTag
+    [ "Lit" :=> withField0 (fmap LitInternal . decodeAConstant),
+      "App"
+        :=> withFields
+        $ \fieldsArr -> do
+          f <- withIndex 0 decodeId fieldsArr
+          args <- withIndex 1 (withArray "App args" (traverse decodeRef)) fieldsArr
+          instTys <- withIndex 2 (withArray "App instTys" (traverse decodeInstTy)) fieldsArr
+          fTy <- withIndex 3 (decodeCompT decodeAbstractTy) fieldsArr
+          pure $ AppInternal f args instTys fTy,
+      "Thunk" :=> withField0 (fmap ThunkInternal . decodeId),
+      "Cata"
+        :=> withFields
+        $ \fieldsArr -> do
+          t <- withIndex 0 (decodeCompT decodeAbstractTy) fieldsArr
+          handlers <- withIndex 1 (withArray "Cata arms" (traverse decodeRef)) fieldsArr
+          r2 <- withIndex 2 decodeRef fieldsArr
+          pure $ CataInternal t handlers r2,
+      "DataConstructor"
+        :=> withFields
+        $ \fieldsArr -> do
+          tn <- withIndex 0 decodeTyName fieldsArr
+          ctorNm <- withIndex 1 decodeConstructorName fieldsArr
+          args <- withIndex 2 (withArray "Datatype args" (traverse decodeRef)) fieldsArr
+          pure $ DataConstructorInternal tn ctorNm args,
+      "Match"
+        :=> withFields
+        $ \fieldsArr -> do
+          scrut <- withIndex 0 decodeRef fieldsArr
+          args <- withIndex 1 (withArray "Match branches" (traverse decodeRef)) fieldsArr
+          pure $ MatchInternal scrut args
+    ]
+
+{- CompNodeInfo
+
+   Serializes as a sum type without named fields:
+
+   {tag: "Builtin1Internal", fields: [f]}
+   | {tag: "Builtin2Internal", fields: [f]}
+   | {tag: "Builtin3Internal", fields: [f]}
+   | {tag: "Builtin6Internal", fields: [f]}
+   | {tag: "LamInternal", fields: [r]}
+   | {tag: "ForceInternal", fields: [r]}
+-}
+
+-- | @since 1.3.0
+encodeCompNodeInfo :: CompNodeInfo -> Encoding
+encodeCompNodeInfo = \case
+  Builtin1Internal fun1 -> taggedFields "Builtin1Internal" [encodeOneArgFunc fun1]
+  Builtin2Internal fun2 -> taggedFields "Builtin2Internal" [encodeTwoArgFunc fun2]
+  Builtin3Internal fun3 -> taggedFields "Builtin3Internal" [encodeThreeArgFunc fun3]
+  Builtin6Internal fun6 -> taggedFields "Builtin6Internal" [encodeSixArgFunc fun6]
+  LamInternal f -> taggedFields "LamInternal" [encodeRef f]
+  ForceInternal f -> taggedFields "ForceInternal" [encodeRef f]
+
+-- | @since 1.3.0
+decodeCompNodeInfo :: Value -> Parser CompNodeInfo
+decodeCompNodeInfo =
+  caseOnTag
+    [ "Builtin1Internal" :=> withField0 (fmap Builtin1Internal . decodeOneArgFunc),
+      "Builtin2Internal" :=> withField0 (fmap Builtin2Internal . decodeTwoArgFunc),
+      "Builtin3Internal" :=> withField0 (fmap Builtin3Internal . decodeThreeArgFunc),
+      "Builtin6Internal" :=> withField0 (fmap Builtin6Internal . decodeSixArgFunc),
+      "LamInternal" :=> withField0 (fmap LamInternal . decodeRef),
+      "ForceInternal" :=> withField0 (fmap ForceInternal . decodeRef)
+    ]
+
+{- ASGNode
+
+   Serializes as a sum type without named fields:
+
+   {tag: "ACompNode", fields: [ty,info]}
+   | {tag: "AValNode", fields: [ty,info]}
+   | {tag: "AnError"}
+
+-}
+
+-- | @since 1.3.0
+encodeASGNode :: ASGNode -> Encoding
+encodeASGNode = \case
+  ACompNode compT compInfo -> taggedFields "ACompNode" [encodeCompT encodeAbstractTy compT, encodeCompNodeInfo compInfo]
+  AValNode valT valInfo -> taggedFields "AValNode" [encodeValTAbstractTy valT, encodeValNodeInfo valInfo]
+  AnError -> pairs $ pair "tag" "AnError"
+
+-- | @since 1.3.0
+decodeASGNode :: Value -> Parser ASGNode
+decodeASGNode =
+  caseOnTag
+    [ "ACompNode" :=> withFields $ \fields -> do
+        compT <- withIndex 0 (decodeCompT decodeAbstractTy) fields
+        compInfo <- withIndex 1 decodeCompNodeInfo fields
+        pure $ ACompNode compT compInfo,
+      "AValNode" :=> withFields $ \fields -> do
+        valT <- withIndex 0 decodeValTAbstractTy fields
+        valInfo <- withIndex 1 decodeValNodeInfo fields
+        pure $ AValNode valT valInfo,
+      "AnError" :=> constM AnError
+    ]
+
+--
+-- ValT, CompT & Friends/Components
+--
+
+{- DeBruijn
+
+   Encodes directly as a number. E.g.
+
+     @S Z@
+   ->
+     1
+
+-}
+
+-- | @since 1.3.0
+encodeDeBruijn :: DeBruijn -> Encoding
+encodeDeBruijn = int . review asInt
+
+-- | @since 1.3.0
+decodeDeBruijn :: Value -> Parser DeBruijn
+decodeDeBruijn v = do
+  vRaw <- parseJSON @Int v
+  if vRaw < 0
+    then fail "Negative DeBruijn"
+    else pure . fromJust . preview asInt $ vRaw
+
+{- AbstractTy
+
+   Standard product serialization as array:
+
+     @BoundAt (S Z) ix0@
+   ->
+     [1,0]
+-}
+
+-- | @since 1.3.0
+encodeAbstractTy :: AbstractTy -> Encoding
+encodeAbstractTy (BoundAt db i) = list id [encodeDeBruijn db, encodeIndex i]
+
+-- | @since 1.3.0
+decodeAbstractTy :: Value -> Parser AbstractTy
+decodeAbstractTy = withArray "AbstractTy" $ \arr -> do
+  guardArrLen 2 arr
+  db <- withIndex 0 decodeDeBruijn arr
+  i <- withIndex 1 decodeIndex arr
+  pure $ BoundAt db i
+
+{- Count
+
+   Serializes as a Number.
+
+    @count0@
+   ->
+    0
+
+    count1
+   ->
+    1
+-}
+
+-- | @since 1.3.0
+encodeCount :: forall (s :: Symbol). Count s -> Encoding
+encodeCount = int . review intCount
+
+-- | @since 1.3.0
+decodeCount :: forall (s :: Symbol). (KnownSymbol s) => Value -> Parser (Count s)
+decodeCount v = do
+  vRaw <- parseJSON @Int v
+  if vRaw < 0
+    then fail "Negative Count"
+    else pure . fromJust . preview intCount $ vRaw
+
+{- Index
+
+   Serializes as a number. NOTE: Will require a type application for the decoder.
+
+     ix0
+   ->
+     0
+
+     ix1
+   ->
+     1
+-}
+
+-- | @since 1.3.0
+encodeIndex :: forall (s :: Symbol). Index s -> Encoding
+encodeIndex = int . review intIndex
+
+-- | @since 1.3.0
+decodeIndex :: forall (s :: Symbol). (KnownSymbol s) => Value -> Parser (Index s)
+decodeIndex v = do
+  vRaw <- parseJSON @Int v
+  if vRaw < 0
+    then fail "Negative Index"
+    else pure . fromJust . preview intIndex $ vRaw
+
+{- CompT AbstractTy
+
+   Standard serialization as an array:
+
+     @CompT count0 ...body...@
+    ->
+     [0,...encodedBody...]
+
+-}
+
+-- | @since 1.3.0
+encodeCompT :: forall (a :: Type). (a -> Encoding) -> CompT a -> Encoding
+encodeCompT fa (CompT cnt body) = list id [encodeCount cnt, encodeCompTBody fa body]
+
+-- | @since 1.3.0
+decodeCompT :: forall (a :: Type). (Value -> Parser a) -> Value -> Parser (CompT a)
+decodeCompT fa = withArray "CompT" $ \arr -> do
+  guardArrLen 2 arr
+  cnt <- withIndex 0 decodeCount arr
+  body <- withIndex 1 (decodeCompTBody fa) arr
+  pure $ CompT cnt body
+
+{- CompTBodyAbstractTy
+
+   This is a newtype over a NonEmptyVector and so encodes directly as an array.
+
+     @CompTBody [t1,t2,t3]@
+   ->
+     [encodedT1,encodedT2,encodedT3]
+
+-}
+
+-- | @since 1.3.0
+encodeCompTBody :: forall (a :: Type). (a -> Encoding) -> CompTBody a -> Encoding
+encodeCompTBody fa (CompTBody tys) = list (encodeValT fa) . toList $ tys
+
+-- | @since 1.3.0
+decodeCompTBody :: forall (a :: Type). (Value -> Parser a) -> Value -> Parser (CompTBody a)
+decodeCompTBody fa = withArray "CompTBody" $ \arr -> do
+  decodedBody <- NEV.fromVector <$> traverse (decodeValT fa) arr
+  case decodedBody of
+    Nothing -> fail "Empty vector of types in a CompTBody"
+    Just res -> pure . CompTBody $ res
+
+{- BuiltinFlatT
+
+   Encodes as an enumeration (i.e. tag-only sum)
+
+   {tag: "UnitT"}
+   | {tag: "BoolT"}
+   | {tag: "IntegerT"}
+   | {tag: "StringT"}
+   | {tag: "ByteStringT"}
+   | {tag: "BLS12_381_G1_ElementT"}
+   | {tag: "BLS12_381_G2_ElementT"}
+   | {tag: "BLS12_381_MlResultT"}
+
+-}
+
+-- | @since 1.3.0
+encodeBuiltinFlatT :: BuiltinFlatT -> Encoding
+encodeBuiltinFlatT = encodeEnum
+
+-- | @since 1.3.0
+decodeBuiltinFlatT :: Value -> Parser BuiltinFlatT
+decodeBuiltinFlatT =
+  caseOnTag
+    [ "UnitT" :=> constM UnitT,
+      "BoolT" :=> constM BoolT,
+      "IntegerT" :=> constM IntegerT,
+      "StringT" :=> constM StringT,
+      "ByteStringT" :=> constM ByteStringT,
+      "BLS12_381_G1_ElementT" :=> constM BLS12_381_G1_ElementT,
+      "BLS12_381_G2_ElementT" :=> constM BLS12_381_G2_ElementT,
+      "BLS12_381_MlResultT" :=> constM BLS12_381_MlResultT
+    ]
+
+{- OneArgFunc
+
+   Encodes as an enumeration (i.e. tag-only sum).
+
+   The name of the tag literally matches the name of the constructor. (Too many to list)
+-}
+
+-- | @since 1.3.0
+encodeOneArgFunc :: OneArgFunc -> Encoding
+encodeOneArgFunc = encodeEnum
+
+-- | @since 1.3.0
+decodeOneArgFunc :: Value -> Parser OneArgFunc
+decodeOneArgFunc =
+  caseOnTag
+    [ "LengthOfByteString" :=> constM LengthOfByteString,
+      "Sha2_256" :=> constM Sha2_256,
+      "Sha3_256" :=> constM Sha3_256,
+      "Blake2b_256" :=> constM Blake2b_256,
+      "EncodeUtf8" :=> constM EncodeUtf8,
+      "DecodeUtf8" :=> constM DecodeUtf8,
+      "FstPair" :=> constM FstPair,
+      "SndPair" :=> constM SndPair,
+      "HeadList" :=> constM HeadList,
+      "TailList" :=> constM TailList,
+      "NullList" :=> constM NullList,
+      "MapData" :=> constM MapData,
+      "ListData" :=> constM ListData,
+      "IData" :=> constM IData,
+      "BData" :=> constM BData,
+      "UnConstrData" :=> constM UnConstrData,
+      "UnMapData" :=> constM UnMapData,
+      "UnListData" :=> constM UnListData,
+      "UnIData" :=> constM UnIData,
+      "UnBData" :=> constM UnBData,
+      "SerialiseData" :=> constM SerialiseData,
+      "BLS12_381_G1_neg" :=> constM BLS12_381_G1_neg,
+      "BLS12_381_G1_compress" :=> constM BLS12_381_G1_compress,
+      "BLS12_381_G1_uncompress" :=> constM BLS12_381_G1_uncompress,
+      "BLS12_381_G2_neg" :=> constM BLS12_381_G2_neg,
+      "BLS12_381_G2_compress" :=> constM BLS12_381_G2_compress,
+      "BLS12_381_G2_uncompress" :=> constM BLS12_381_G2_uncompress,
+      "Keccak_256" :=> constM Keccak_256,
+      "Blake2b_224" :=> constM Blake2b_224,
+      "ComplementByteString" :=> constM ComplementByteString,
+      "CountSetBits" :=> constM CountSetBits,
+      "FindFirstSetBit" :=> constM FindFirstSetBit,
+      "Ripemd_160" :=> constM Ripemd_160
+    ]
+
+{- TwoArgFunc
+
+   Encodes as an enumeration (i.e. tag-only sum).
+
+   The name of the tag literally matches the name of the constructor. (Too many to list)
+-}
+
+-- | @since 1.3.0
+encodeTwoArgFunc :: TwoArgFunc -> Encoding
+encodeTwoArgFunc = encodeEnum
+
+-- | @since 1.3.0
+decodeTwoArgFunc :: Value -> Parser TwoArgFunc
+decodeTwoArgFunc =
+  caseOnTag
+    [ "AddInteger" :=> constM AddInteger,
+      "SubtractInteger" :=> constM SubtractInteger,
+      "MultiplyInteger" :=> constM MultiplyInteger,
+      "DivideInteger" :=> constM DivideInteger,
+      "QuotientInteger" :=> constM QuotientInteger,
+      "RemainderInteger" :=> constM RemainderInteger,
+      "ModInteger" :=> constM ModInteger,
+      "EqualsInteger" :=> constM EqualsInteger,
+      "LessThanInteger" :=> constM LessThanInteger,
+      "LessThanEqualsInteger" :=> constM LessThanEqualsInteger,
+      "AppendByteString" :=> constM AppendByteString,
+      "ConsByteString" :=> constM ConsByteString,
+      "IndexByteString" :=> constM IndexByteString,
+      "EqualsByteString" :=> constM EqualsByteString,
+      "LessThanByteString" :=> constM LessThanByteString,
+      "LessThanEqualsByteString" :=> constM LessThanEqualsByteString,
+      "AppendString" :=> constM AppendString,
+      "EqualsString" :=> constM EqualsString,
+      "ChooseUnit" :=> constM ChooseUnit,
+      "Trace" :=> constM Trace,
+      "MkCons" :=> constM MkCons,
+      "ConstrData" :=> constM ConstrData,
+      "EqualsData" :=> constM EqualsData,
+      "MkPairData" :=> constM MkPairData,
+      "BLS12_381_G1_add" :=> constM BLS12_381_G1_add,
+      "BLS12_381_G1_scalarMul" :=> constM BLS12_381_G1_scalarMul,
+      "BLS12_381_G1_equal" :=> constM BLS12_381_G1_equal,
+      "BLS12_381_G1_hashToGroup" :=> constM BLS12_381_G1_hashToGroup,
+      "BLS12_381_G2_add" :=> constM BLS12_381_G2_add,
+      "BLS12_381_G2_scalarMul" :=> constM BLS12_381_G2_scalarMul,
+      "BLS12_381_G2_equal" :=> constM BLS12_381_G2_equal,
+      "BLS12_381_G2_hashToGroup" :=> constM BLS12_381_G2_hashToGroup,
+      "BLS12_381_millerLoop" :=> constM BLS12_381_millerLoop,
+      "BLS12_381_mulMlResult" :=> constM BLS12_381_mulMlResult,
+      "BLS12_381_finalVerify" :=> constM BLS12_381_finalVerify,
+      "ByteStringToInteger" :=> constM ByteStringToInteger,
+      "ReadBit" :=> constM ReadBit,
+      "ReplicateByte" :=> constM ReplicateByte,
+      "ShiftByteString" :=> constM ShiftByteString,
+      "RotateByteString" :=> constM RotateByteString
+    ]
+
+{- ThreeArgFunc
+
+   Encodes as an enumeration (i.e. tag-only sum).
+
+   The name of the tag literally matches the name of the constructor. (Too many to list)
+-}
+
+-- | @since 1.3.0
+encodeThreeArgFunc :: ThreeArgFunc -> Encoding
+encodeThreeArgFunc = encodeEnum
+
+-- | @since 1.3.0
+decodeThreeArgFunc :: Value -> Parser ThreeArgFunc
+decodeThreeArgFunc =
+  caseOnTag
+    [ "VerifyEd25519Signature" :=> constM VerifyEd25519Signature,
+      "VerifyEcdsaSecp256k1Signature" :=> constM VerifyEcdsaSecp256k1Signature,
+      "VerifySchnorrSecp256k1Signature" :=> constM VerifySchnorrSecp256k1Signature,
+      "IfThenElse" :=> constM IfThenElse,
+      "ChooseList" :=> constM ChooseList,
+      "IntegerToByteString" :=> constM IntegerToByteString,
+      "AndByteString" :=> constM AndByteString,
+      "OrByteString" :=> constM OrByteString,
+      "XorByteString" :=> constM XorByteString,
+      "WriteBits" :=> constM WriteBits,
+      "ExpModInteger" :=> constM ExpModInteger
+    ]
+
+{- SixArgFunc
+
+   Encodes as an enumeration (i.e. tag-only sum).
+
+   The name of the tag literally matches the name of the constructor. (Too many to list)
+-}
+
+-- | @since 1.3.0
+encodeSixArgFunc :: SixArgFunc -> Encoding
+encodeSixArgFunc = encodeEnum
+
+-- | @since 1.3.0
+decodeSixArgFunc :: Value -> Parser SixArgFunc
+decodeSixArgFunc =
+  caseOnTag
+    [ "ChooseData" :=> constM ChooseData
+    ]
+
+{- ValT
+
+   Encodes as a tagged sum without explicit field names:
+
+   {tag: "Abstraction", fields: [...]}
+   | {tag: "ThunkT", fields: [...]}
+   | {tag: "BuiltinFlat", fields: : [...]}
+   | {tag: "Datatype", fields: [...]}
+
+-}
+
+encodeValT :: forall (a :: Type). (a -> Encoding) -> ValT a -> Encoding
+encodeValT fa = \case
+  Abstraction x -> taggedFields "Abstraction" [fa x]
+  ThunkT compT -> taggedFields "ThunkT" [encodeCompT fa compT]
+  BuiltinFlat biFlat -> taggedFields "BuiltinFlat" [encodeBuiltinFlatT biFlat]
+  Datatype tn args -> taggedFields "Datatype" [encodeTyName tn, list (encodeValT fa) . toList $ args]
+
+decodeValT :: forall (a :: Type). (Value -> Parser a) -> Value -> Parser (ValT a)
+decodeValT fa =
+  caseOnTag
+    [ "Abstraction" :=> withField0 (fmap Abstraction . fa),
+      "ThunkT" :=> withField0 (fmap ThunkT . decodeCompT fa),
+      "BuiltinFlat" :=> withField0 (fmap BuiltinFlat . decodeBuiltinFlatT),
+      "Datatype" :=> withFields $ \arr -> do
+        tn <- withIndex 0 decodeTyName arr
+        ctors <- withIndex 1 (withArray "datatype args" (traverse (decodeValT fa))) arr
+        pure $ Datatype tn ctors
+    ]
+
+{- Encodes as an array [DeBruijn, Index "tyvar"]
+-}
+encodeBoundTyVar :: BoundTyVar -> Encoding
+encodeBoundTyVar (BoundTyVar db ix) = list id [encodeDeBruijn db, encodeIndex ix]
+
+decodeBoundTyVar :: Value -> Parser BoundTyVar
+decodeBoundTyVar = withArray "BoundTyVar" $ \arr -> do
+  db <- withIndex 0 decodeDeBruijn arr
+  ix <- withIndex 1 decodeIndex arr
+  pure $ BoundTyVar db ix
+
+{- Encoding is fully determined by other functions
+-}
+encodeInstTy :: Wedge BoundTyVar (ValT Void) -> Encoding
+encodeInstTy = encodeWedge encodeBoundTyVar (encodeValT encodeVoid)
+
+decodeInstTy :: Value -> Parser (Wedge BoundTyVar (ValT Void))
+decodeInstTy = decodeWedge decodeBoundTyVar (decodeValT decodeVoid)
+
+-- | @since 1.3.0
+encodeValTAbstractTy :: ValT AbstractTy -> Encoding
+encodeValTAbstractTy = encodeValT encodeAbstractTy
+
+-- | @since 1.3.0
+decodeValTAbstractTy :: Value -> Parser (ValT AbstractTy)
+decodeValTAbstractTy = decodeValT decodeAbstractTy
+
+-- Helpers
+
+encodeVoid :: Void -> Encoding
+encodeVoid = absurd
+
+decodeVoid :: Value -> Parser Void
+decodeVoid _ = fail "Void isn't inhabited, you can't decode a value to it"
+
+{- We encode maps as arrays of {key: k, value: v} pairs
+-}
+encodeMap :: forall k v. (k -> Encoding) -> (v -> Encoding) -> Map k v -> Encoding
+encodeMap fk fv m =
+  list id $
+    M.foldlWithKey'
+      ( \acc k v ->
+          let entry = pairs $ pair "key" (fk k) <> pair "value" (fv v)
+           in entry : acc
+      )
+      []
+      m
+
+decodeMap ::
+  forall k v.
+  (Ord k) =>
+  (Value -> Parser k) ->
+  (Value -> Parser v) ->
+  Value ->
+  Parser (Map k v)
+decodeMap fk fv = withArray "Map" $ \arr ->
+  foldM
+    ( \acc x -> flip (withObject "kvPair") x $ \obj -> do
+        kfield <- lookupAndParse' obj "key" fk
+        vfield <- lookupAndParse' obj "value" fv
+        pure $ M.insert kfield vfield acc
+    )
+    M.empty
+    arr
+
+{- We encode wedges as a normal sum type, a la:
+
+    {tag: "Nowhere"}
+    | {tag: "Here", fields: [a]}
+    | {tag: "There", fields: [b]}
+-}
+encodeWedge ::
+  forall (a :: Type) (b :: Type).
+  (a -> Encoding) ->
+  (b -> Encoding) ->
+  Wedge a b ->
+  Encoding
+encodeWedge fa fb = \case
+  Nowhere -> pairs $ pair "tag" "Nowhere"
+  Here a -> taggedFields "Here" [fa a]
+  There b -> taggedFields "There" [fb b]
+
+decodeWedge ::
+  forall (a :: Type) (b :: Type).
+  (Value -> Parser a) ->
+  (Value -> Parser b) ->
+  Value ->
+  Parser (Wedge a b)
+decodeWedge fa fb =
+  caseOnTag
+    [ "Nowhere" :=> constM Nowhere,
+      "Here" :=> fmap Here . withField0 fa,
+      "There" :=> fmap There . withField0 fb
+    ]
+
+-- Mainly for readability/custom fixity, effectively (,)
+data (:=>) a b = a :=> b
+
+infixr 0 :=>
+
+-- Simulated pattern matching on the `tag` field of an object. Will throw an error if the
+-- value is not an object. This is a convenience function, and it is *very* convenient.
+caseOnTag :: forall (a :: Type). [Text :=> (Object -> Parser a)] -> Value -> Parser a
+caseOnTag xs = withObject "CaseOnTag" go
+  where
+    go :: Object -> Parser a
+    go obj = do
+      let caseDict = foldl' (\acc (t :=> fn) -> M.insert t fn acc) M.empty xs
+      tagVal <- lookupAndParse' obj "tag" (parseJSON @Text)
+      case M.lookup tagVal caseDict of
+        Just f -> f obj
+        Nothing -> fail $ "Expected a tagged object with one of the tags: " <> show (M.keys caseDict) <> " but got " <> show obj
+
+-- Stupid helper to avoid have to type `\_ -> pure x` a million times in `caseOnTag` matches
+constM :: forall (f :: Type -> Type) (a :: Type). (Applicative f) => a -> (forall (b :: Type). b -> f a)
+constM x _ = pure x
+
+guardArrLen :: Int -> Array -> Parser ()
+guardArrLen expectedLen arr
+  | Vector.length arr == expectedLen = pure ()
+  | otherwise =
+      fail $
+        "Expected an array with "
+          <> show expectedLen
+          <> " elements, but got one with "
+          <> show (Vector.length arr)
+          <> " elements"
+
+-- Do something with the array at the tag "fields" in an object. Convenience helper.
+withFields :: forall (a :: Type). (Array -> Parser a) -> Object -> Parser a
+withFields f obj = lookupAndParse' obj "fields" $ \arrVal -> withArray "field array" f arrVal
+
+-- Do something with the element at a given index in a JSON array.
+withIndex :: forall (a :: Type). Int -> (Value -> Parser a) -> Array -> Parser a
+withIndex i f arr = case arr Vector.!? i of
+  Nothing -> fail $ "No element at index " <> show i <> " found in array " <> show arr
+  Just elemAtIx -> f elemAtIx
+
+-- flipped variant of lookupAndParse', for point free functions
+withField :: forall (a :: Type). Key -> (Value -> Parser a) -> Object -> Parser a
+withField k f obj = lookupAndParse' obj k f
+
+-- A lot of our sums have a "fields" object with only one element, this saves us a bit of repetition for that common case.
+-- Because this is intended to be used with either `withObject` or `caseOnTag`, it takes an Object which is expected to have a
+-- "fields" fieldName with an array
+withField0 :: forall (a :: Type). (Value -> Parser a) -> Object -> Parser a
+withField0 f = withFields (\arr -> guardArrLen 1 arr >> withIndex 0 f arr)
+
+-- Lookup the key in an object and apply the given monadic function to the value you get.
+lookupAndParse' :: forall (a :: Type). Object -> Key -> (Value -> Parser a) -> Parser a
+lookupAndParse' obj k f = case KM.lookup k obj of
+  Nothing -> fail $ "No key '" <> show k <> "' found in object"
+  Just v -> f v
+
+-- NOTE: Must *ONLY* be used on *true* Enums, i.e. sum types with only 0-argument constructors
+encodeEnum :: forall (a :: Type). (Show a) => a -> Encoding
+encodeEnum = pairs . ("tag" .=) . show
+
+-- Helper for constructing sum type Encodings.
+-- 'taggedFields "name" [f1,f2,f3]' generates '{tag: "name", fields: [f1,f2,f3]}
+taggedFields :: Text -> [Encoding] -> Encoding
+taggedFields tg fieldArgs = pairs $ "tag" .= tg <> pair "fields" (list id fieldArgs)
+
+-- Decodes a hex encoded bytestring
+decodeByteStringHex :: Value -> Parser ByteString
+decodeByteStringHex = withText "ByteString (Hex Encoded)" $ \txt -> case Hex.decodeHex txt of
+  Nothing -> fail $ "Failed to decode hex bytestring: " <> show txt
+  Just bs -> pure bs
+
+-- | Given a collection of datatype declarations, convert them to
+-- 'DatatypeInfo's by generating their base functor and Boehm-Berrarducci
+-- encodings. Then add to these all the base functors for the built-in types.
+--
+-- @since 1.3.0
+mkDatatypeInfos ::
+  [DataDeclaration AbstractTy] ->
+  Either String (Map TyName (DatatypeInfo AbstractTy))
+mkDatatypeInfos decls = do
+  let tyDict = foldl' (\acc x -> M.insert (view #datatypeName x) x acc) M.empty decls
+  case checkDataDecls tyDict of
+    Left kcErr -> Left $ "KindCheck error: " <> show kcErr
+    Right _ ->
+      first (("DatatypeInfo error: " <>) . show) $
+        foldl'
+          (\acc decl -> (<>) <$> mkDatatypeInfo decl <*> acc)
+          (Right primBaseFunctorInfos)
+          tyDict
+
+-- IO Helpers
+
+writeJSONWith :: forall (a :: Type). FilePath -> a -> (a -> Encoding) -> IO ()
+writeJSONWith path x f = BL.writeFile path (encodingToLazyByteString . f $ x)
+
+readJSON :: forall (a :: Type). (FromJSON a) => FilePath -> ExceptT DeserializeErr IO a
+readJSON path =
+  liftIO (eitherDecodeFileStrict @a path) >>= \case
+    Left err' -> throwError . JSONParseFailure $ err'
+    Right res -> pure res
diff --git a/src/Covenant/Prim.hs b/src/Covenant/Prim.hs
--- a/src/Covenant/Prim.hs
+++ b/src/Covenant/Prim.hs
@@ -20,13 +20,13 @@
   )
 where
 
-import Covenant.DeBruijn (DeBruijn (S, Z))
+import Covenant.DeBruijn (DeBruijn (Z))
 import Covenant.Index (ix0, ix1)
 import Covenant.Type
   ( AbstractTy,
     CompT (Comp0, Comp1, Comp2),
     CompTBody (ReturnT, (:--:>)),
-    ValT (ThunkT),
+    ValT,
     boolT,
     byteStringT,
     dataType1T,
@@ -366,8 +366,6 @@
   | IfThenElse
   | -- | @since 1.1.0
     ChooseList
-  | -- | @since 1.1.0
-    CaseList
   | IntegerToByteString
   | AndByteString
   | OrByteString
@@ -395,7 +393,6 @@
         VerifySchnorrSecp256k1Signature,
         IfThenElse,
         ChooseList,
-        CaseList,
         IntegerToByteString,
         AndByteString,
         OrByteString,
@@ -414,12 +411,6 @@
   VerifySchnorrSecp256k1Signature -> signatureT
   IfThenElse -> Comp1 $ boolT :--:> aT :--:> aT :--:> ReturnT aT
   ChooseList -> Comp2 $ listT aT :--:> bT :--:> bT :--:> ReturnT bT
-  CaseList ->
-    Comp2 $
-      bT
-        :--:> ThunkT (Comp0 $ aTOuter :--:> listT aTOuter :--:> ReturnT bTOuter)
-        :--:> listT aT
-        :--:> ReturnT bT
   IntegerToByteString ->
     Comp0 $
       boolT :--:> integerT :--:> integerT :--:> ReturnT byteStringT
@@ -454,9 +445,7 @@
 -- | All six-argument primitives provided by Plutus.
 --
 -- @since 1.1.0
-data SixArgFunc
-  = ChooseData
-  | CaseData
+data SixArgFunc = ChooseData
   deriving stock
     ( -- | @since 1.0.0
       Eq,
@@ -471,7 +460,7 @@
 -- @since 1.1.0
 instance Arbitrary SixArgFunc where
   {-# INLINEABLE arbitrary #-}
-  arbitrary = elements [ChooseData, CaseData]
+  arbitrary = pure ChooseData
 
 -- | Produce the type of a six-argument primop.
 --
@@ -487,15 +476,6 @@
         :--:> aT
         :--:> aT
         :--:> ReturnT aT
-  CaseData ->
-    Comp1 $
-      ThunkT (Comp0 $ integerT :--:> listT dataT :--:> ReturnT aTOuter)
-        :--:> ThunkT (Comp0 $ listT (pairT dataT dataT) :--:> ReturnT aTOuter)
-        :--:> ThunkT (Comp0 $ listT dataT :--:> ReturnT aTOuter)
-        :--:> ThunkT (Comp0 $ integerT :--:> ReturnT aTOuter)
-        :--:> ThunkT (Comp0 $ byteStringT :--:> ReturnT aTOuter)
-        :--:> dataT
-        :--:> ReturnT aT
 
 -- Helpers
 
@@ -511,11 +491,5 @@
 aT :: ValT AbstractTy
 aT = tyvar Z ix0
 
-aTOuter :: ValT AbstractTy
-aTOuter = tyvar (S Z) ix0
-
 bT :: ValT AbstractTy
 bT = tyvar Z ix1
-
-bTOuter :: ValT AbstractTy
-bTOuter = tyvar (S Z) ix1
diff --git a/src/Covenant/Test.hs b/src/Covenant/Test.hs
--- a/src/Covenant/Test.hs
+++ b/src/Covenant/Test.hs
@@ -1,6 +1,9 @@
 {-# LANGUAGE CPP #-}
+{-# LANGUAGE OverloadedLists #-}
 {-# LANGUAGE PolyKinds #-}
 
+{- HLINT ignore "Use camelCase" -}
+
 -- |
 -- Module: Covenant.Test
 -- Copyright: (C) MLabs 2025
@@ -32,12 +35,15 @@
 
     -- ** Test helpers
     checkApp,
+    conformanceDatatypes1,
+    conformanceDatatypes2,
     failLeft,
     tyAppTestDatatypes,
     list,
     tree,
     weirderList,
     unsafeTyCon,
+    unsafeMkDatatypeInfos,
 
     -- ** Datatype checks
     cycleCheck,
@@ -63,6 +69,12 @@
     DebugASGBuilder (..),
     debugASGBuilder,
     typeIdTest,
+    Arg (UnsafeMkArg),
+    Id (UnsafeMkId),
+
+    -- ** Exports for codegen tests
+    concretifyMinimalBuilder,
+    concretifyMegaTest,
   )
 where
 
@@ -83,23 +95,16 @@
   )
 import Control.Monad.Trans (MonadTrans (lift))
 import Control.Monad.Trans.Except (ExceptT, runExceptT)
-import Covenant.ASG (ASGEnv (ASGEnv), ASGNode, CovenantError (TypeError), CovenantTypeError, Id, ScopeInfo (ScopeInfo))
+import Covenant.ASG (ASGBuilder, ASGEnv (ASGEnv), ASGNode, CovenantError (TypeError), CovenantTypeError, Id, Ref (AnArg, AnId), ScopeInfo (ScopeInfo), app', arg, boundTyVar, builtin2, builtin3, ctor, ctor', dtype, force, lam, lazyLam, lit, match, thunk)
+import Covenant.Constant (AConstant (ABoolean, AnInteger))
 import Covenant.Data
   ( DatatypeInfo,
     mkDatatypeInfo,
     noPhantomTyVars,
-  )
-import Covenant.DeBruijn (DeBruijn (Z), asInt)
-import Covenant.Index
-  ( Count,
-    count0,
-    count1,
-    count2,
-    intCount,
-    intIndex,
-    ix0,
-    ix1,
+    primBaseFunctorInfos,
   )
+import Covenant.DeBruijn (DeBruijn (S, Z), asInt)
+import Covenant.Index (Count, Index, count0, count1, count2, intCount, intIndex, ix0, ix1, ix2, ix3)
 import Covenant.Internal.KindCheck
   ( checkDataDecls,
     checkEncodingArgs,
@@ -127,9 +132,15 @@
   )
 import Covenant.Internal.Strategy
   ( DataEncoding (PlutusData, SOP),
+    PlutusDataConstructor (PlutusB, PlutusI),
     PlutusDataStrategy (ConstrData),
   )
-import Covenant.Internal.Term (ASGNodeType (CompNodeType, ValNodeType), typeId)
+import Covenant.Internal.Term
+  ( ASGNodeType (CompNodeType, ValNodeType),
+    Arg (UnsafeMkArg),
+    Id (UnsafeMkId),
+    typeId,
+  )
 import Covenant.Internal.Type
   ( AbstractTy (BoundAt),
     BuiltinFlatT
@@ -150,9 +161,12 @@
     runConstructorName,
   )
 import Covenant.Internal.Unification (checkApp)
+import Covenant.Prim (ThreeArgFunc (IfThenElse), TwoArgFunc (EqualsInteger))
 import Covenant.Type
-  ( CompT (Comp0, CompN),
-    CompTBody (ArgsAndResult),
+  ( CompT (Comp0, Comp1, Comp2, CompN),
+    CompTBody (ArgsAndResult, ReturnT, (:--:>)),
+    boolT,
+    tyvar,
   )
 import Covenant.Util (prettyStr)
 import Data.Coerce (coerce)
@@ -167,6 +181,7 @@
 import Data.Text qualified as T
 import Data.Vector (Vector)
 import Data.Vector qualified as Vector
+import Data.Wedge (Wedge (Here))
 import GHC.Exts (fromListN)
 import GHC.Word (Word32)
 import Optics.Core
@@ -370,8 +385,13 @@
 --
 -- @since 1.1.0
 tyAppTestDatatypes :: M.Map TyName (DatatypeInfo AbstractTy)
-tyAppTestDatatypes =
-  foldl' (\acc decl -> M.insert (view #datatypeName decl) (unsafeMkDatatypeInfo decl) acc) M.empty testDatatypes
+tyAppTestDatatypes = unsafeMkDatatypeInfos testDatatypes
+
+-- | Construct a datatype information dictionary (which is what the ASGBuilder actually needs)
+--   from a collection of data declarations (which are what people actually write)
+-- @since 1.3.0
+unsafeMkDatatypeInfos :: [DataDeclaration AbstractTy] -> M.Map TyName (DatatypeInfo AbstractTy)
+unsafeMkDatatypeInfos = mappend primBaseFunctorInfos . foldl' (\acc decl -> unsafeMkDatatypeInfo decl <> acc) M.empty
   where
     unsafeMkDatatypeInfo d = case mkDatatypeInfo d of
       Left err -> error (show err)
@@ -929,4 +949,220 @@
       (PlutusData ConstrData)
 
 testDatatypes :: [DataDeclaration AbstractTy]
-testDatatypes = [maybeT, eitherT, unitT, pair, list]
+testDatatypes = [maybeT, eitherT, unitT, pair, list, conformance_OpaqueFoo]
+
+{- For conformance testing. All of the ledger types are data encoded, so we need some variants which
+   are not data encoded to ensure adequate test coverage.
+data Maybe a = Nothing | Just a
+
+data Result e a = Exception e | OK a
+
+data Pair a b = Pair a b
+
+data List a = Nil | Cons a (List a)
+-}
+conformanceDatatypes1 :: [DataDeclaration AbstractTy]
+conformanceDatatypes1 = [conformance_Maybe_SOP, conformance_Result, pair, list]
+
+conformanceDatatypes2 :: [DataDeclaration AbstractTy]
+conformanceDatatypes2 = [conformance_Void, conformance_OpaqueFoo, conformance_Maybe_SOP, pair]
+
+conformance_Void :: DataDeclaration AbstractTy
+conformance_Void = mkDecl $ Decl "Void" count0 [] SOP
+
+conformance_OpaqueFoo :: DataDeclaration AbstractTy
+conformance_OpaqueFoo = OpaqueData "Foo" (Set.fromList [PlutusI, PlutusB])
+
+conformance_Maybe_SOP :: DataDeclaration AbstractTy
+conformance_Maybe_SOP =
+  mkDecl $
+    Decl
+      "Maybe"
+      count1
+      [ Ctor "Nothing" [],
+        Ctor "Just" [tyvar Z ix0]
+      ]
+      SOP
+
+conformance_Result :: DataDeclaration AbstractTy
+conformance_Result =
+  mkDecl $
+    Decl
+      "Result"
+      count2
+      [ Ctor "Exception" [tyvar Z ix0],
+        Ctor "OK" [tyvar Z ix1]
+      ]
+      (PlutusData ConstrData)
+
+-- These are canned tests for concretification. They do double duty as tests for
+-- part of the code generator, so we put them here to avoid having to duplicate them across
+-- repositories.
+
+intT :: ValT AbstractTy
+intT = BuiltinFlat IntegerT
+
+mkMaybeT :: ValT AbstractTy -> ValT AbstractTy
+mkMaybeT t = dtype "Maybe" [t]
+
+ix4 :: forall s. Index s
+ix4 = fromJust $ preview intIndex 4
+
+thunk0 :: forall (a :: Type). CompTBody a -> ValT a
+thunk0 = ThunkT . Comp0
+
+(#==) :: Ref -> Ref -> ASGBuilder Ref
+x #== y = do
+  equals <- builtin2 EqualsInteger
+  AnId <$> app' equals [x, y]
+
+-- This is the minimal example, largely for testing that our fix to the concretification/unification glitch
+-- in this repo works.
+concretifyMinimalBuilder :: ASGBuilder Id
+concretifyMinimalBuilder = lam topLevelTy body
+  where
+    topLevelTy :: CompT AbstractTy
+    topLevelTy = Comp0 $ intT :--:> boolT :--:> ReturnT intT
+
+    body :: ASGBuilder Ref
+    body = do
+      intArg <- AnArg <$> arg Z ix0
+      boolArg <- AnArg <$> arg Z ix1
+      fElim <- fPolyOneElimMinimal
+      maybeInt <- ctor' "Maybe" "Just" [intArg]
+      AnId <$> app' fElim [AnId maybeInt, boolArg]
+
+    fPolyOneElimMinimal :: ASGBuilder Id
+    fPolyOneElimMinimal = lam fPolyOneElimTy $ do
+      maybeA <- AnArg <$> arg Z ix0
+      nothingHandler <- lazyLam (Comp0 $ ReturnT intT) $ do
+        AnId <$> lit (AnInteger 0)
+      justHandler <- lazyLam (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT intT) $ do
+        AnId <$> lit (AnInteger 0)
+      AnId <$> match maybeA [AnId justHandler, AnId nothingHandler]
+      where
+        fPolyOneElimTy :: CompT AbstractTy
+        fPolyOneElimTy =
+          Comp2 $ -- forall a b.
+            mkMaybeT (tyvar Z ix0) -- Maybe a
+              :--:> tyvar Z ix1 -- b
+              :--:> ReturnT intT -- Int
+
+-- This is a torture test example. We'll use it here since we have it and it's relevant, but it's largely
+-- designed for a test in the code generator.
+concretifyMegaTest :: ASGBuilder Id
+concretifyMegaTest = lam topLevelTy body
+  where
+    body :: ASGBuilder Ref
+    body = do
+      intArg <- AnArg <$> arg Z ix0
+      boolArg <- AnArg <$> arg Z ix1
+      idF <- AnId <$> (thunk =<< identitee)
+      fmono <- AnId <$> (thunk =<< fMono)
+      gmono <- AnId <$> (thunk =<< gMono)
+      mConst <- AnId <$> (thunk =<< monoConst)
+      fIntro <- fPolyOneIntro
+      fElim <- fPolyOneElim
+      introApplied <- app' fIntro [fmono, mConst, gmono, intArg, boolArg]
+      -- REVIEW @Koz: You said that a fully polymorphic identity function *should not work* as the second arg here, but it does work?
+      AnId <$> app' fElim [AnId introApplied, idF, boolArg, fmono]
+
+    ifte :: ASGBuilder Id
+    ifte = lam (Comp1 $ boolT :--:> tyvar Z ix0 :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do
+      cond <- AnArg <$> arg Z ix0
+      t <- AnArg <$> arg Z ix1
+      f <- AnArg <$> arg Z ix2
+      ifThen <- builtin3 IfThenElse
+      AnId <$> app' ifThen [cond, t, f]
+
+    -- NOTE: I wonder what happens if we tried to define id and monoConst in terms of each other?
+    --       Like if we do it so that we get infinite mutual recursion. I should probably *try*
+    --       to compile something like that just to see whether it explodes.
+    identitee :: ASGBuilder Id
+    identitee = lam (Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do
+      -- Not how you would typically implement `id` lol
+      mConst <- monoConst
+      x <- AnArg <$> arg Z ix0
+      -- Might not need the ty app?
+      AnId <$> app' mConst [x, x] -- [Here tyX]
+
+    -- forall a. a -> a -> a
+    monoConst :: ASGBuilder Id
+    monoConst = lam (Comp1 $ tyvar Z ix0 :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do
+      AnArg <$> arg Z ix1
+
+    topLevelTy :: CompT AbstractTy
+    topLevelTy = Comp0 $ intT :--:> boolT :--:> ReturnT intT
+
+    fPolyOneElim :: ASGBuilder Id
+    fPolyOneElim = lam fPolyOneElimTy $ do
+      zero <- AnId <$> lit (AnInteger 0)
+      maybeA <- AnArg <$> arg Z ix0
+      nothingHandler <- lazyLam (Comp0 $ ReturnT intT) $ do
+        mConst <- monoConst
+        b <- AnArg <$> arg (S Z) ix2
+        bToInt <- force . AnArg =<< arg (S Z) ix3
+        x <- AnId <$> app' bToInt [b]
+        AnId <$> app' mConst [zero, x]
+      justHandler <- lazyLam (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT intT) $ do
+        aToInt <- force . AnArg =<< arg (S Z) ix1
+        a <- AnArg <$> arg Z ix0
+        AnId <$> app' aToInt [a]
+      AnId <$> match maybeA [AnId justHandler, AnId nothingHandler] -- ,AnId justHandler]
+      where
+        fPolyOneElimTy :: CompT AbstractTy
+        fPolyOneElimTy =
+          Comp2 $ -- forall a b.
+            mkMaybeT (tyvar Z ix0) -- Maybe a
+              :--:> thunk0 (tyvar (S Z) ix0 :--:> ReturnT intT) -- (a -> Int)
+              :--:> tyvar Z ix1 -- b
+              :--:> thunk0 (tyvar (S Z) ix1 :--:> ReturnT intT) -- (b -> Int)
+              :--:> ReturnT intT -- Int
+    fPolyOneIntro :: ASGBuilder Id
+    fPolyOneIntro = lam fPolyOneIntroTy $ do
+      fba <- force . AnArg =<< arg Z ix0
+      faa <- force . AnArg =<< arg Z ix1
+      predA <- force . AnArg =<< arg Z ix2
+      a <- AnArg <$> arg Z ix3
+      b <- AnArg <$> arg Z ix4
+      -- let ba = fba (monoConst b b)
+      mConst <- monoConst
+      fbaArg <- AnId <$> app' mConst [b, b]
+      ba <- AnId <$> app' fba [fbaArg]
+      -- let aaa = monoConst a (faa a ba)
+      aaaArg <- AnId <$> app' faa [a, ba]
+      aaa <- AnId <$> app' mConst [a, aaaArg]
+      -- if (predA aaa) then Nothing else Just aaa
+      tvA <- boundTyVar Z ix0
+      nothing <- ctor "Maybe" "Nothing" [] [Here tvA]
+      justAAA <- ctor' "Maybe" "Just" [aaa]
+      ifThen <- ifte
+      cond <- app' predA [aaa]
+      AnId <$> app' ifThen [AnId cond, AnId nothing, AnId justAAA]
+      where
+        fPolyOneIntroTy :: CompT AbstractTy
+        fPolyOneIntroTy =
+          Comp2 $ -- forall a b.
+            ThunkT (Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix0)) -- (b -> a)
+              :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix0)) -- (a -> a -> a)
+              :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT boolT) -- (a -> Bool)
+              :--:> tyvar Z ix0 -- a
+              :--:> tyvar Z ix1 -- b
+              :--:> ReturnT (mkMaybeT (tyvar Z ix0)) -- Maybe a
+    fMono :: ASGBuilder Id
+    fMono = lam (Comp0 $ boolT :--:> ReturnT intT) $ do
+      aBool <- AnArg <$> arg Z ix0
+      one <- AnId <$> lit (AnInteger 1)
+      zero <- AnId <$> lit (AnInteger 0)
+      ifThen <- ifte
+      AnId <$> app' ifThen [aBool, one, zero]
+
+    gMono :: ASGBuilder Id
+    gMono = lam (Comp0 $ intT :--:> ReturnT boolT) $ do
+      anInt <- AnArg <$> arg Z ix0
+      zero <- AnId <$> lit (AnInteger 0)
+      cond <- anInt #== zero
+      ifThen <- ifte
+      false <- AnId <$> lit (ABoolean False)
+      troo <- AnId <$> lit (ABoolean True)
+      AnId <$> app' ifThen [cond, false, troo]
diff --git a/src/Covenant/Type.hs b/src/Covenant/Type.hs
--- a/src/Covenant/Type.hs
+++ b/src/Covenant/Type.hs
@@ -235,9 +235,10 @@
 --
 -- @since 1.0.0
 pattern CompN ::
+  forall (a :: Type).
   Count "tyvar" ->
-  CompTBody AbstractTy ->
-  CompT AbstractTy
+  CompTBody a ->
+  CompT a
 pattern CompN count xs <- CompT count xs
   where
     CompN count xs = CompT count xs
diff --git a/src/Covenant/Zipper.hs b/src/Covenant/Zipper.hs
new file mode 100644
--- /dev/null
+++ b/src/Covenant/Zipper.hs
@@ -0,0 +1,281 @@
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE ViewPatterns #-}
+
+-- |
+-- Module: Covenant.Zipper
+-- Copyright: (C) MLabs 2025
+-- License: Apache 2.0
+-- Maintainer: koz@mlabs.city, sean@mlabs.city
+--
+-- A read-only zipper for the Covenant ASG, based on an action monad.
+--
+-- @since 1.3.0
+module Covenant.Zipper
+  ( -- * Types
+    ZipperAction,
+    Tape (..),
+    ZipperState (WorkingZipper, BrokenZipper),
+    ASGZipper,
+
+    -- * Functions
+
+    -- ** Actions
+    moveUp,
+    moveDown,
+    moveLeft,
+    moveRight,
+    resetZipper,
+
+    -- ** Elimination
+    runASGZipper,
+  )
+where
+
+import Control.Monad.Action
+  ( Action (StateOf, act),
+    Actionable,
+    MonadUpdate,
+    UpdateT,
+    actionable,
+    runUpdateT,
+  )
+import Covenant.ASG
+  ( ASG,
+    ASGNode (ACompNode, AValNode, AnError),
+    Arg,
+    CompNodeInfo (Force, Lam),
+    Id,
+    Ref (AnArg, AnId),
+    ValNodeInfo (App, Cata, DataConstructor, Match, Thunk),
+    nodeAt,
+    topLevelId,
+  )
+import Covenant.Util (pattern ConsV, pattern NilV)
+import Data.Functor.Identity (Identity, runIdentity)
+import Data.Kind (Type)
+import Data.Monoid (Endo (Endo))
+import Data.Vector qualified as Vector
+import GHC.Exts (toList)
+
+-- | A requested movement from the zipper. To build these, use dedicated smart
+-- constructors in this module. You can \'chain together\' 'ZipperAction' using
+-- the 'Semigroup' instance.
+--
+-- @since 1.3.0
+newtype ZipperAction = ZipperAction (Actionable ZipperStep)
+  deriving
+    ( -- | @since 1.3.0
+      Semigroup,
+      -- | @since 1.3.0
+      Monoid
+    )
+    via (Actionable ZipperStep)
+
+-- | @since 1.3.0
+instance Action ZipperAction where
+  type StateOf ZipperAction = ZipperState
+  act (ZipperAction acts) = foldMap go acts
+    where
+      go :: ZipperStep -> Endo ZipperState
+      go =
+        Endo . \case
+          ZipperDown -> downStep
+          ZipperUp -> upStep
+          ZipperLeft -> leftStep
+          ZipperRight -> rightStep
+          ZipperReset -> resetStep
+
+-- | Move towards the source of the ASG, \'back up\' along the path taken to
+-- reach the current position. Will put the zipper in a broken state if used at
+-- the source node.
+--
+-- @since 1.3.0
+moveUp :: ZipperAction
+moveUp = ZipperAction . actionable $ ZipperUp
+
+-- | Move to the leftmost child of the current position. Will put the zipper in
+-- a broken state if used at a sink node.
+--
+-- @since 1.3.0
+moveDown :: ZipperAction
+moveDown = ZipperAction . actionable $ ZipperDown
+
+-- | Move to the sibling immediately to the left of the current position. Will
+-- put the zipper in a broken state if used at a leftmost sibling.
+--
+-- @since 1.3.0
+moveLeft :: ZipperAction
+moveLeft = ZipperAction . actionable $ ZipperLeft
+
+-- | Move to the sibling immediately to the right of the current position. Will
+-- put the zipper in a broken state if used at a rightmost sibling.
+--
+-- @since 1.3.0
+moveRight :: ZipperAction
+moveRight = ZipperAction . actionable $ ZipperRight
+
+-- | If the zipper is currently in a broken state, reset it to the last position
+-- it was at before breaking. Otherwise, this does nothing.
+--
+-- @since 1.3.0
+resetZipper :: ZipperAction
+resetZipper = ZipperAction . actionable $ ZipperReset
+
+-- | A \'list with a focus\', which may be of a different type to the rest. The
+-- first field is \'backwards\', in that its first element is actually the
+-- /furthest/ from the focus. Thus, if we have @Tape [3, 2, 1] "foo" [4, 5]@,
+-- the \'list\' actually looks like this:
+--
+-- @[1, 2, 3, "foo", 4, 5]@
+--
+-- but /not/ like this:
+--
+-- @[3, 2, 1, "foo", 4, 5]@
+--
+-- @since 1.3.0
+data Tape a b = Tape [a] b [a]
+  deriving stock
+    ( -- | @since 1.3.0
+      Functor
+    )
+
+-- | The current state of the zipper, including whether it's in a broken state
+-- or not, and if not in a broken state, the current position and the path taken
+-- to get here.
+--
+-- @since 1.3.0
+data ZipperState = ZipperState Bool ASG [Tape Ref Id] (Tape Ref Ref)
+
+-- | Matches on a working zipper, giving access to a stack of 'Tape's
+-- representing the path taken to get here (tracking sibling positions) and the
+-- current position, with the focus at either an 'Arg' or an 'ASGNode'.
+--
+-- Parent positions use 'Id' for the focus, as 'Arg's cannot have descendants.
+--
+-- @since 1.3.0
+pattern WorkingZipper :: [Tape Ref Id] -> Tape Ref (Either Arg (Id, ASGNode)) -> ZipperState
+pattern WorkingZipper parents curr <- ZipperState False g parents (getNodeInfo g -> curr)
+
+-- | Matches on a zipper in a broken state.
+--
+-- @since 1.3.0
+pattern BrokenZipper :: ZipperState
+pattern BrokenZipper <- ZipperState True _ _ _
+
+{-# COMPLETE WorkingZipper, BrokenZipper #-}
+
+-- | A \'zipper command monad\', designed to traverse an ASG. Based on an action
+-- monad.
+--
+-- To perform zipper moves, use 'Control.Monad.Action.send' together with a
+-- 'ZipperAction'. If you want to find out something about where we're standing,
+-- use 'Control.Monad.Action.request', together with pattern matching on
+-- 'ZipperState'.
+--
+-- @since 1.3.0
+newtype ASGZipper (a :: Type)
+  = ASGZipper (UpdateT ZipperAction Identity a)
+  deriving
+    ( -- | @since 1.3.0
+      Functor,
+      -- | @since 1.3.0
+      Applicative,
+      -- | @since 1.3.0
+      Monad,
+      -- | @since 1.3.0
+      MonadUpdate ZipperAction
+    )
+    via (UpdateT ZipperAction Identity)
+
+-- | Perform the stated actions to traverse over the 'ASG' given by the
+-- argument.
+--
+-- @since 1.3.0
+runASGZipper ::
+  forall (a :: Type).
+  ASG ->
+  ASGZipper a ->
+  a
+runASGZipper g (ASGZipper comp) =
+  let i = topLevelId g
+   in (\(_, _, x) -> x)
+        . runIdentity
+        . runUpdateT comp
+        . ZipperState False g []
+        . Tape [] (AnId i)
+        $ []
+
+-- Helpers
+
+data ZipperStep = ZipperDown | ZipperUp | ZipperLeft | ZipperRight | ZipperReset
+  deriving stock (Eq, Show)
+
+downStep :: ZipperState -> ZipperState
+downStep zs@(ZipperState walkedOff g parentLevels currentLevel) =
+  if walkedOff
+    then zs
+    else case currentLevel of
+      Tape lefts curr rights ->
+        let miss = ZipperState True g parentLevels currentLevel
+         in case curr of
+              AnArg _ -> miss
+              AnId i ->
+                let next = ZipperState walkedOff g (Tape lefts i rights : parentLevels)
+                 in case nodeAt i g of
+                      ACompNode _ info -> case info of
+                        Lam r -> next . Tape [] r $ []
+                        Force r -> next . Tape [] r $ []
+                        _ -> miss
+                      AValNode _ info -> case info of
+                        App f args _ _ -> next . Tape [] (AnId f) . toList $ args
+                        Thunk f -> next . Tape [] (AnId f) $ []
+                        Cata _ arms x -> case arms of
+                          NilV -> zs -- impossible
+                          ConsV c cs -> next . Tape [] c . toList . Vector.snoc cs $ x -- next . Tape [] alg $ [x]
+                        DataConstructor _ _ args -> case args of
+                          NilV -> miss
+                          ConsV arg args' -> next . Tape [] arg . toList $ args'
+                        Match x handlers -> next . Tape [] x . toList $ handlers
+                        _ -> miss
+                      AnError -> miss
+
+upStep :: ZipperState -> ZipperState
+upStep zs@(ZipperState walkedOff g parentLevels currentLevel) =
+  if walkedOff
+    then zs
+    else case parentLevels of
+      [] -> ZipperState True g parentLevels currentLevel
+      (p : ps) -> case p of
+        Tape lefts curr rights -> ZipperState walkedOff g ps . Tape lefts (AnId curr) $ rights
+
+leftStep :: ZipperState -> ZipperState
+leftStep zs@(ZipperState walkedOff g parentLevels currentLevel) =
+  if walkedOff
+    then zs
+    else case currentLevel of
+      Tape lefts curr rights -> case lefts of
+        [] -> ZipperState True g parentLevels currentLevel
+        (l : ls) -> ZipperState walkedOff g parentLevels . Tape ls l $ curr : rights
+
+rightStep :: ZipperState -> ZipperState
+rightStep zs@(ZipperState walkedOff g parentLevels currentLevel) =
+  if walkedOff
+    then zs
+    else case currentLevel of
+      Tape lefts curr rights -> case rights of
+        [] -> ZipperState True g parentLevels currentLevel
+        (r : rs) -> ZipperState walkedOff g parentLevels . Tape (curr : lefts) r $ rs
+
+resetStep :: ZipperState -> ZipperState
+resetStep zs@(ZipperState walkedOff g parentLevels currentLevel) =
+  if walkedOff
+    then ZipperState False g parentLevels currentLevel
+    else zs
+
+getNodeInfo :: ASG -> Tape Ref Ref -> Tape Ref (Either Arg (Id, ASGNode))
+getNodeInfo g =
+  fmap
+    ( \case
+        AnId i -> Right (i, nodeAt i g)
+        AnArg arg -> Left arg
+    )
diff --git a/test/asg/Main.hs b/test/asg/Main.hs
--- a/test/asg/Main.hs
+++ b/test/asg/Main.hs
@@ -24,7 +24,7 @@
       ( ApplyCompType,
         ApplyToError,
         ApplyToValType,
-        CataNoBaseFunctorForType,
+        BaseFunctorDoesNotExistFor,
         CataNonRigidAlgebra,
         ForceCompType,
         ForceError,
@@ -38,13 +38,16 @@
     Ref (AnArg, AnId),
     ValNodeInfo (Lit),
     app,
+    app',
     arg,
+    baseFunctorOf,
     boundTyVar,
     builtin1,
     builtin2,
     builtin3,
     cata,
     ctor,
+    ctor',
     dataConstructor,
     defaultDatatypes,
     dtype,
@@ -54,6 +57,8 @@
     lazyLam,
     lit,
     match,
+    naturalBF,
+    negativeBF,
     runASGBuilder,
     thunk,
     topLevelNode,
@@ -63,7 +68,7 @@
     typeConstant,
   )
 import Covenant.DeBruijn (DeBruijn (S, Z))
-import Covenant.Index (Index, intIndex, ix0, ix1)
+import Covenant.Index (Index, intIndex, ix0, ix1, ix2)
 import Covenant.Prim
   ( typeOneArgFunc,
     typeThreeArgFunc,
@@ -72,13 +77,15 @@
 import Covenant.Test
   ( Concrete (Concrete),
     DebugASGBuilder,
+    concretifyMegaTest,
+    concretifyMinimalBuilder,
     debugASGBuilder,
     tyAppTestDatatypes,
     typeIdTest,
   )
 import Covenant.Type
   ( AbstractTy,
-    BuiltinFlatT (IntegerT, UnitT),
+    BuiltinFlatT (ByteStringT, IntegerT, UnitT),
     CompT (Comp0, Comp1, Comp2, CompN),
     CompTBody (ArgsAndResult, ReturnT, (:--:>)),
     ValT (BuiltinFlat, Datatype, ThunkT),
@@ -94,7 +101,7 @@
 import Data.Map qualified as M
 import Data.Maybe (fromJust)
 import Data.Vector qualified as Vector
-import Data.Wedge (Wedge (Here, Nowhere, There), wedgeLeft)
+import Data.Wedge (Wedge (Here, There), wedgeLeft)
 import Optics.Core (preview, review)
 import Test.QuickCheck
   ( Gen,
@@ -143,15 +150,15 @@
       justNothingIntro,
       testGroup
         "Catamorphisms"
-        [ testCase "Natural_F can tear down an Integer" unitCataNaturalF,
-          testCase "Negative_F can tear down an Integer" unitCataNegativeF,
-          testCase "ByteString_F can tear down a ByteString" unitCataByteStringF,
+        [ testCase "#Natural can tear down an Integer" unitCataNaturalF,
+          testCase "#Negative can tear down an Integer" unitCataNegativeF,
+          testCase "#ByteString can tear down a ByteString" unitCataByteStringF,
           testCase "Non-recursive type cata should fail" unitCataMaybeF,
           testCase "Cata with non-rigid algebra should fail" unitCataNonRigidF,
-          testCase "<List_F Integer Bool -> !Bool> with List Integer should be Bool" unitCataListInteger,
-          testCase "<List_F Integer r -> !r> with List Integer should be r" unitCataListIntegerRigid,
-          testCase "<List_F r Integer -> !Integer> with List r should be Integer" unitCataListRigid,
-          testCase "<List_F r (Maybe r) -> !Maybe r> with List r should be Maybe r" unitCataListMaybeRigid,
+          testCase "<#List Integer Bool -> !Bool> with List Integer should be Bool" unitCataListInteger,
+          testCase "<#List Integer r -> !r> with List Integer should be r" unitCataListIntegerRigid,
+          testCase "<#List r Integer -> !Integer> with List r should be Integer" unitCataListRigid,
+          testCase "<#List r (Maybe r) -> !Maybe r> with List r should be Maybe r" unitCataListMaybeRigid,
           testCase "introduction then cata elimination" unitCataIntroThenEliminate
         ],
       testGroup
@@ -159,7 +166,13 @@
         [ matchMaybe,
           matchList,
           maybeToList
-        ]
+        ],
+      testGroup
+        "Opaque"
+        [unifyOpaque],
+      testGroup "matchOpaque" [matchOpaque],
+      testGroup "argBugTest" [argBugUnitTest],
+      testGroup "concretify" [simpleConcretifyUnitTest, excessiveConcretifyUnitTest]
     ]
   where
     moreTests :: QuickCheckTests -> QuickCheckTests
@@ -197,176 +210,250 @@
     Left (TypeError _ ThunkError) -> pure ()
     _ -> assertFailure $ "Unexpected result: " <> show result
 
--- Construct a function of type `<Natural_F Bool -> !Bool> -> Integer -> !Bool`, whose
--- body performs a cata over its second argument using its first argument. This
--- should compile, and type as expected.
+-- Construct a function of type `Bool -> <Bool -> !Bool> -> Integer ->
+-- !Bool`, whose body performs a cata over its third argument using the first
+-- and second argument as handlers. The stated algebra type is `Natural Bool ->
+-- !Bool`, where `Natural` refers to the natural-number base functor of
+-- `Integer`. This should compile and type as expected.
 unitCataNaturalF :: IO ()
 unitCataNaturalF = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "Natural_F" [boolT] :--:> ReturnT boolT
-  let ty = Comp0 $ thunkTy :--:> integerT :--:> ReturnT boolT
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let algTy = Comp0 $ Datatype naturalBF [boolT] :--:> ReturnT boolT
+  let resultTy =
+        Comp0 $
+          boolT
+            :--:> ThunkT (Comp0 $ boolT :--:> ReturnT boolT)
+            :--:> integerT
+            :--:> ReturnT boolT
+  let comp = lam resultTy $ do
+        armZ <- arg Z ix0
+        armS <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata algTy (Vector.fromList . fmap AnArg $ [armZ, armS]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `<Negative_F Bool -> !Bool> -> Integer -> !Bool`, whose
--- body performs a cata over its second argument using its first argument. This
--- should compile, and type as expected.
+-- Construct a function of type `Bool -> <Bool -> !Bool> -> Integer ->
+-- !Bool`, whose body performs a cata over its third argument using the first
+-- and second argument as handlers. The stated algebra type is `Negative Bool -> !Bool`,
+-- where `Negative` refers to the negative-number base functor of `Integer`.
+-- This should compile and type as expected.
 unitCataNegativeF :: IO ()
 unitCataNegativeF = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "Negative_F" [boolT] :--:> ReturnT boolT
-  let ty = Comp0 $ thunkTy :--:> integerT :--:> ReturnT boolT
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let algTy = Comp0 $ Datatype negativeBF [boolT] :--:> ReturnT boolT
+  let resultTy =
+        Comp0 $
+          boolT
+            :--:> ThunkT (Comp0 $ boolT :--:> ReturnT boolT)
+            :--:> integerT
+            :--:> ReturnT boolT
+  let comp = lam resultTy $ do
+        armZ <- arg Z ix0
+        armS <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata algTy (Vector.fromList . fmap AnArg $ [armZ, armS]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `<ByteString_F Integer -> !Integer> -> ByteString
--- -> !Bool`, whose body performs a cata over its second argument using its
--- first argument. This should compile, and type as expected.
+-- Construct a function of type `Bool -> <Integer -> Bool -> !Bool>
+-- -> ByteString -> !Bool>, whose body performs a cata over its third argument
+-- using the first and second argument as handlers. The stated algebra type is
+-- `ByteString# Bool -> !Bool`, where `ByteString#` refers to the base functor
+-- of `ByteString`. This should compile and type as expected.
 unitCataByteStringF :: IO ()
 unitCataByteStringF = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "ByteString_F" [integerT] :--:> ReturnT integerT
-  let ty = Comp0 $ thunkTy :--:> byteStringT :--:> ReturnT integerT
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let algTy = do
+        bfName <- baseFunctorOf "ByteString"
+        pure . Comp0 $ Datatype bfName [boolT] :--:> ReturnT boolT
+  let resultTy =
+        Comp0 $
+          boolT
+            :--:> ThunkT (Comp0 $ integerT :--:> boolT :--:> ReturnT boolT)
+            :--:> byteStringT
+            :--:> ReturnT boolT
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `forall a . <Maybe_F a Integer -> !Integer> -> Maybe
--- a -> !Integer`, whose body performs a cata over its second argument
--- using its first argument. This should fail to compile, indicating that
--- `Maybe` doesn't have a base functor.
+-- Construct a function of type `forall a . Integer -> <a -> !Integer> ->
+-- Maybe a -> !Integer`, whose body performs a cata over its third argument
+-- using the first and second argument as handlers. The stated algebra type is
+-- `Maybe# a Integer -> !Integer`, with `a` rigid. This should fail to compile,
+-- indicating that `Maybe` lacks a base functor.
 unitCataMaybeF :: IO ()
 unitCataMaybeF = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "Maybe_F" [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT
-  let ty = Comp1 $ thunkTy :--:> Datatype "Maybe" [tyvar Z ix0] :--:> ReturnT integerT
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
+  let algTy = do
+        bfName <- baseFunctorOf "Maybe"
+        pure . Comp0 $ Datatype bfName [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT
+  let resultTy =
+        Comp1 $
+          integerT
+            :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT integerT)
+            :--:> Datatype "Maybe" [tyvar Z ix0]
+            :--:> ReturnT integerT
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNothing <- arg Z ix0
+        armJust <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNothing, armJust]) (AnArg x)
   withCompilationFailureUnit comp $ \case
-    TypeError _ (CataNoBaseFunctorForType tyName) -> assertEqual "" "Maybe" tyName
+    TypeError _ (BaseFunctorDoesNotExistFor tyName) -> assertEqual "" "Maybe" tyName
     err' -> assertFailure $ "Failed with unexpected type of error: " <> show err'
 
--- Construct a function of type `<forall a . ListF a (Maybe a) -> !Maybe a> -> List
--- Integer -> !Maybe Integer`, whose body performs a cata over its second
--- argument using its first argument. This should fail to compile due to a
--- non-rigid algebra.
+-- Construct a function of type forall a . Maybe a -> <a -> Maybe a ->
+-- !(Maybe a)> ->
+-- List Integer -> !(Maybe Integer)`, whose body performs a cata over its third
+-- argument using the first and second argument as handlers. The stated algebra
+-- type is `forall b. List# b (Maybe b) -> !(Maybe b)`. This should fail to
+-- compile due to a non-rigid algebra.
 unitCataNonRigidF :: IO ()
 unitCataNonRigidF = do
-  let nonRigidCompT = Comp1 $ Datatype "List_F" [tyvar Z ix0, Datatype "Maybe" [tyvar Z ix0]] :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])
-  let thunkTy = ThunkT nonRigidCompT
-  let ty = Comp0 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT (Datatype "Maybe" [integerT])
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
+  let algTy = do
+        listBfName <- baseFunctorOf "List"
+        pure . Comp1 $ Datatype listBfName [tyvar Z ix0, Datatype "Maybe" [tyvar Z ix0]] :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])
+  let resultTy =
+        Comp1 $
+          Datatype "Maybe" [tyvar (S Z) ix0]
+            :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> Datatype "Maybe" [tyvar (S Z) ix0] :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix0]))
+            :--:> Datatype "List" [tyvar Z ix0]
+            :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnArg x)
   withCompilationFailureUnit comp $ \case
-    TypeError _ (CataNonRigidAlgebra t) -> assertEqual "" nonRigidCompT t
+    TypeError _ (CataNonRigidAlgebra _) -> pure ()
     err' -> assertFailure $ "Failed with unexpected type of error: " <> show err'
 
--- Construct a function of type `<List_F Integer Bool -> !Bool> -> List Integer
--- -> !Bool`, whose body performs a cata over its second argument using its
--- first argument. This should compile, and type as expected.
+-- Construct a function of type `Bool -> <Integer -> Bool -> !Bool> -> List
+-- Integer -> !Bool`, whose body performs a cata over its third argument using
+-- the first and second argument as handlers. The stated algebra type is `List#
+-- Integer Bool -> !Bool`. This should compile and type as expected.
 unitCataListInteger :: IO ()
 unitCataListInteger = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [integerT, boolT] :--:> ReturnT boolT
-  let ty = Comp0 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT boolT
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let algTy = do
+        listBfName <- baseFunctorOf "List"
+        pure . Comp0 $ Datatype listBfName [integerT, boolT] :--:> ReturnT boolT
+  let resultTy =
+        Comp0 $
+          boolT
+            :--:> ThunkT (Comp0 $ integerT :--:> boolT :--:> ReturnT boolT)
+            :--:> Datatype "List" [integerT]
+            :--:> ReturnT boolT
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `forall a . <List_F Integer a -> !a> -> List
--- Integer -> !a`, whose body performs a cata over its second argument using its
--- first argument. This should compile, and type as expected.
+-- Construct a function of type `forall a . a -> <!Integer -> a -> !a> ->
+-- List Integer -> !a>, whose body performs a cata over its third argument using
+-- the first and second argument as handlers. The stated algebra type is `List#
+-- Integer a -> !a`, with `a` rigid. This should compile and type as expected.
 unitCataListIntegerRigid :: IO ()
 unitCataListIntegerRigid = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [integerT, tyvar (S Z) ix0] :--:> ReturnT (tyvar (S Z) ix0)
-  let ty = Comp1 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT (tyvar Z ix0)
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let algTy = do
+        listBfName <- baseFunctorOf "List"
+        pure . Comp0 $ Datatype listBfName [integerT, tyvar (S Z) ix0] :--:> ReturnT (tyvar (S Z) ix0)
+  let resultTy =
+        Comp1 $
+          tyvar Z ix0
+            :--:> ThunkT (Comp0 $ integerT :--:> tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix0))
+            :--:> Datatype "List" [integerT]
+            :--:> ReturnT (tyvar Z ix0)
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `forall a . <List_F a Integer -> !Integer> -> List
--- a -> !Integer`, whose body performs a cata over its second argument using its
--- first argument. This should compile, and type as expected.
+-- Construct a function of type `forall a . Integer -> <a -> Integer ->
+-- !Integer> -> List a -> !Integer`, whose body performs a cata over its third
+-- argument using the first and second argument as handlers. The stated algebra
+-- type is `List# a Integer -> !Integer`, holding `a` rigid. This should compile
+-- and type as expected.
 unitCataListRigid :: IO ()
 unitCataListRigid = do
-  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT
-  let ty = Comp1 $ thunkTy :--:> Datatype "List" [tyvar Z ix0] :--:> ReturnT integerT
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let algTy = do
+        listBfName <- baseFunctorOf "List"
+        pure . Comp0 $ Datatype listBfName [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT
+  let resultTy =
+        Comp1 $
+          integerT
+            :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> integerT :--:> ReturnT integerT)
+            :--:> Datatype "List" [tyvar Z ix0]
+            :--:> ReturnT integerT
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `forall a . <List_F a (Maybe a) -> !Maybe a> ->
--- List a -> !Maybe a`, whose body performs a cata over its second argument
--- using its first argument. This should compile, and type as expected.
+-- Construct a function of type `forall a . Maybe a -> <a -> Maybe a ->
+-- !(Maybe a)> -> List a -> !(Maybe a)`, whose body performs a cata over its
+-- third argument using the first and second argument as handlers. The stated
+-- algebra type is `List# a (Maybe a) -> !(Maybe a)`, keeping `a` rigid. This
+-- should compile and type as expected.
 unitCataListMaybeRigid :: IO ()
 unitCataListMaybeRigid = do
-  let thunkTy =
-        ThunkT $
-          Comp0 $
-            Datatype "List_F" [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix0]]
-              :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix0])
-  let ty =
+  let algTy = do
+        listBfName <- baseFunctorOf "List"
+        pure . Comp0 $ Datatype listBfName [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix0]] :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix0])
+  let resultTy =
         Comp1 $
-          thunkTy
+          Datatype "Maybe" [tyvar Z ix0]
+            :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> Datatype "Maybe" [tyvar (S Z) ix0] :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix0]))
             :--:> Datatype "List" [tyvar Z ix0]
             :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
-        result <- cata (AnArg alg) (AnArg x)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+  let comp = lam resultTy $ do
+        t <- algTy
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        x <- arg Z ix2
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnArg x)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
--- Construct a function of type `forall a b . <List_F a (Maybe b) -> !Maybe b> ->
--- a -> !Maybe b`. In its body, we construct a singleton list, then eliminate it
--- using a cata with the first argument as the algebra. THis should compile and
--- type as expected.
+-- Construct a function of type `forall a b . Maybe b -> <a -> Maybe b ->
+-- !(Maybe b)> -> a -> !(Maybe b)`. In its body, we construct a singleton list
+-- using the third argument, then eliminate it using a cata with the first and
+-- second argument as handlers. The stated type of the algebra is `List# a
+-- (Maybe b) -> !(Maybe b)`, keeping `a, b` rigid. This should compile and type
+-- as expected.
 unitCataIntroThenEliminate :: IO ()
 unitCataIntroThenEliminate = do
-  let thunkTy =
-        ThunkT $
-          Comp0 $
-            Datatype "List_F" [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix1]]
-              :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix1])
-  let ty =
+  let algTy = do
+        listBfName <- baseFunctorOf "List"
+        pure . Comp0 $ Datatype listBfName [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix1]] :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix1])
+  let resultTy =
         Comp2 $
-          thunkTy
+          Datatype "Maybe" [tyvar Z ix1]
+            :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> Datatype "Maybe" [tyvar (S Z) ix1] :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix1]))
             :--:> tyvar Z ix0
             :--:> ReturnT (Datatype "Maybe" [tyvar Z ix1])
-  let comp = lam ty $ do
-        alg <- arg Z ix0
-        x <- arg Z ix1
+  let comp = lam resultTy $ do
+        t <- algTy
+        x <- arg Z ix2
         nilThunk <- dataConstructor "List" "Nil" []
         nilForced <- force (AnId nilThunk)
         aT <- boundTyVar Z ix0
         nilApplied <- app nilForced [] [Here aT]
         singleThunk <- dataConstructor "List" "Cons" [AnArg x, AnId nilApplied]
         singleForced <- force (AnId singleThunk)
-        singleApplied <- app singleForced [] [Nowhere]
-        result <- cata (AnArg alg) (AnId singleApplied)
-        pure . AnId $ result
-  withCompilationSuccessUnit comp $ matchesType ty
+        singleApplied <- app' singleForced []
+        armNil <- arg Z ix0
+        armCons <- arg Z ix1
+        AnId <$> cata t (Vector.fromList . fmap AnArg $ [armNil, armCons]) (AnId singleApplied)
+  withCompilationSuccessUnit comp (matchesType resultTy)
 
 -- Properties
 
@@ -530,7 +617,7 @@
             Left bi1 -> builtin1 bi1
             Right (Left bi2) -> builtin2 bi2
             Right (Right bi3) -> builtin3 bi3
-          app i (Vector.singleton . AnId $ arg') mempty
+          app' i (Vector.singleton . AnId $ arg')
    in withCompilationFailure comp $ \case
         TypeError _ (ApplyCompType actualT) -> t === actualT
         TypeError _ err' -> failWrongTypeError err'
@@ -700,14 +787,10 @@
 justNothingIntro :: TestTree
 justNothingIntro = runIntroFormTest "justNothingIntro" expectedThunk $ do
   thunkL <- lam expectedComp $ do
-    nothingThunk <- dataConstructor "Maybe" "Nothing" mempty
     var <- boundTyVar Z ix0
-    nothingForced <- force (AnId nothingThunk)
-    nothingApplied <- app nothingForced mempty (Vector.singleton . wedgeLeft . Just $ var)
-    justNothing <- dataConstructor "Maybe" "Just" (Vector.singleton (AnId nothingApplied))
-    justNothingForced <- force (AnId justNothing)
-    justNothingApplied <- app justNothingForced mempty (Vector.singleton Nowhere)
-    pure (AnId justNothingApplied)
+    nothing <- ctor "Maybe" "Nothing" mempty (Vector.singleton . wedgeLeft . Just $ var)
+    justNothing <- ctor' "Maybe" "Just" (Vector.singleton (AnId nothing))
+    pure (AnId justNothing)
   typeIdTest thunkL
   where
     expectedComp :: CompT AbstractTy
@@ -733,7 +816,7 @@
 matchMaybe :: TestTree
 matchMaybe = runIntroFormTest "matchMaybe" (BuiltinFlat IntegerT) $ do
   unit <- AnId <$> lit AUnit
-  scrutinee <- ctor "Maybe" "Just" (Vector.singleton unit) (Vector.singleton Nowhere)
+  scrutinee <- ctor' "Maybe" "Just" (Vector.singleton unit)
   nothingHandler <- lazyLam (Comp0 $ ReturnT (BuiltinFlat IntegerT)) (AnId <$> lit (AnInteger 0))
   justHandler <- lazyLam (Comp0 $ BuiltinFlat UnitT :--:> ReturnT (BuiltinFlat IntegerT)) (AnId <$> lit (AnInteger 1))
   result <- match (AnId scrutinee) (AnId <$> Vector.fromList [justHandler, nothingHandler])
@@ -747,12 +830,12 @@
 matchList = runIntroFormTest "matchList" (BuiltinFlat IntegerT) $ do
   unit <- AnId <$> lit AUnit
   nilUnit <- ctor "List" "Nil" mempty (Vector.singleton $ There (BuiltinFlat UnitT))
-  scrutinee <- ctor "List" "Cons" (Vector.fromList [unit, AnId nilUnit]) (Vector.singleton Nowhere)
+  scrutinee <- ctor' "List" "Cons" (Vector.fromList [unit, AnId nilUnit])
   let nilHandlerTy = Comp0 $ ReturnT (BuiltinFlat IntegerT)
       consHandlerTy =
         Comp0 $
           BuiltinFlat UnitT
-            :--:> Datatype "List_F" (Vector.fromList [BuiltinFlat UnitT, Datatype "List" (Vector.singleton $ BuiltinFlat UnitT)])
+            :--:> Datatype "#List" (Vector.fromList [BuiltinFlat UnitT, Datatype "List" (Vector.singleton $ BuiltinFlat UnitT)])
             :--:> ReturnT (BuiltinFlat IntegerT)
   nilHandler <- lazyLam nilHandlerTy (AnId <$> lit (AnInteger 0))
   consHandler <- lazyLam consHandlerTy (AnId <$> lit (AnInteger 0))
@@ -777,7 +860,7 @@
       tvA <- boundTyVar (S Z) ix0
       vA <- AnArg <$> arg Z ix0
       nil <- AnId <$> ctor "List" "Nil" mempty (Vector.singleton (Here tvA))
-      AnId <$> ctor "List" "Cons" (Vector.fromList [vA, nil]) (Vector.singleton Nowhere)
+      AnId <$> ctor "List" "Cons" (Vector.fromList [vA, nil]) Vector.empty
     scrutinee <- AnArg <$> arg Z ix0
     AnId <$> match scrutinee (AnId <$> Vector.fromList [justHandler, nothingHandler])
   typeIdTest thonk
@@ -787,6 +870,65 @@
 
     maybeToListTy :: ValT AbstractTy
     maybeToListTy = ThunkT maybeToListCompTy
+
+{- This tests that Opaques don't break the unifier. Arguably it should be in type-applications, but we need a bunch of
+   ASG stuff that's not imported there to construct the test, so it is here instead.
+
+   The lambda we construct has the type: Maybe Opaque -> Integer
+-}
+
+unifyOpaque :: TestTree
+unifyOpaque = runIntroFormTest "unifyOpaque" unifyOpaqueTy $ do
+  thonk <- lazyLam unifyOpaqueCompTy $ do
+    let nothingHandlerTy = Comp0 $ ReturnT (BuiltinFlat IntegerT)
+        justHandlerTy = Comp0 $ dtype "Foo" [] :--:> ReturnT (BuiltinFlat IntegerT)
+    nothingHandler <- lazyLam nothingHandlerTy (AnId <$> lit (AnInteger 0))
+    justHandler <- lazyLam justHandlerTy (AnId <$> lit (AnInteger 1))
+    scrutinee <- AnArg <$> arg Z ix0
+    AnId <$> match scrutinee (AnId <$> Vector.fromList [justHandler, nothingHandler])
+  typeIdTest thonk
+  where
+    unifyOpaqueCompTy :: CompT AbstractTy
+    unifyOpaqueCompTy = Comp0 $ dtype "Maybe" [dtype "Foo" []] :--:> ReturnT (BuiltinFlat IntegerT)
+    unifyOpaqueTy :: ValT AbstractTy
+    unifyOpaqueTy = ThunkT unifyOpaqueCompTy
+
+matchOpaque :: TestTree
+matchOpaque = runIntroFormTest "matchOpaque" matchOpaqueTy $ do
+  thonk <- lazyLam matchOpaqueCompTy $ do
+    let iHandlerTy = Comp0 $ BuiltinFlat IntegerT :--:> ReturnT (BuiltinFlat IntegerT)
+        bHandlerTy = Comp0 $ BuiltinFlat ByteStringT :--:> ReturnT (BuiltinFlat IntegerT)
+    iHandler <- lazyLam iHandlerTy $ AnId <$> lit (AnInteger 0)
+    bHandler <- lazyLam bHandlerTy $ AnId <$> lit (AnInteger 1)
+    scrutinee <- AnArg <$> arg Z ix0
+    AnId <$> match scrutinee (AnId <$> Vector.fromList [iHandler, bHandler])
+  typeIdTest thonk
+  where
+    matchOpaqueCompTy :: CompT AbstractTy
+    matchOpaqueCompTy = Comp0 $ dtype "Foo" [] :--:> ReturnT (BuiltinFlat IntegerT)
+    matchOpaqueTy :: ValT AbstractTy
+    matchOpaqueTy = ThunkT matchOpaqueCompTy
+
+argBugUnitTest :: TestTree
+argBugUnitTest = testCase "argBugTest" $ withCompilationSuccessUnit asg (\_ -> pure ())
+  where
+    intT :: ValT AbstractTy
+    intT = BuiltinFlat IntegerT
+    asg :: ASGBuilder Id
+    asg = lam (Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)) $ do
+      gimmeZ0 <- lam (Comp0 $ intT :--:> ReturnT (tyvar (S Z) ix0)) $ do
+        AnArg <$> arg (S Z) ix0
+      one <- AnId <$> lit (AnInteger 1)
+      AnId <$> app' gimmeZ0 [one]
+
+-- tests for our concretification fix in `app`.
+-- We only care that compilation succeeds.
+
+simpleConcretifyUnitTest :: TestTree
+simpleConcretifyUnitTest = testCase "simpleConcretify" $ withCompilationSuccessUnit concretifyMinimalBuilder (\_ -> pure ())
+
+excessiveConcretifyUnitTest :: TestTree
+excessiveConcretifyUnitTest = testCase "excessiveConcretify" $ withCompilationSuccessUnit concretifyMegaTest (\_ -> pure ())
 
 -- Helpers
 
diff --git a/test/json-conformance/Main.hs b/test/json-conformance/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/json-conformance/Main.hs
@@ -0,0 +1,307 @@
+{-# LANGUAGE OverloadedLists #-}
+
+module Main (main) where
+
+import Control.Monad (void)
+import Covenant.ASG
+  ( ASG,
+    ASGBuilder,
+    CovenantError,
+    Id,
+    Ref (AnArg, AnId),
+    app',
+    arg,
+    baseFunctorOf,
+    builtin2,
+    cata,
+    ctor,
+    ctor',
+    dtype,
+    err,
+    lam,
+    lazyLam,
+    lit,
+    match,
+    runASGBuilder,
+  )
+import Covenant.Constant
+  ( AConstant (AString, AnInteger),
+  )
+import Covenant.DeBruijn (DeBruijn (S, Z))
+import Covenant.Index (ix0, ix1)
+import Covenant.JSON (deserializeAndValidate_)
+import Covenant.Prim (TwoArgFunc (AddInteger, EqualsInteger, SubtractInteger))
+import Covenant.Test
+  ( conformanceDatatypes1,
+    conformanceDatatypes2,
+    unsafeMkDatatypeInfos,
+  )
+import Covenant.Type
+  ( AbstractTy,
+    BuiltinFlatT (BoolT, IntegerT, StringT),
+    CompT (Comp0, Comp1),
+    CompTBody (ReturnT, (:--:>)),
+    ValT (BuiltinFlat, Datatype),
+    tyvar,
+  )
+import Data.Either (isRight)
+import Data.Vector qualified as Vector
+import Data.Wedge (Wedge (There))
+import Test.Tasty (defaultMain, testGroup)
+import Test.Tasty.HUnit (assertBool, testCase)
+
+main :: IO ()
+main =
+  defaultMain . testGroup "Conformance" $
+    [ testCase "conformance1_asg" (assertBool "case 1 compiles to asg" $ isRight conformance_body1),
+      testCase "conformance2_asg" (assertBool "case 2 compiles to asg" $ isRight conformance_body2),
+      testCase "deserialize_1" (void $ deserializeAndValidate_ "./test/json-conformance/conformance_case_1.json"),
+      testCase "deserialize_2" (void $ deserializeAndValidate_ "./test/json-conformance/conformance_case_2.json")
+    ]
+
+{- Case 1:
+
+Datatypes:
+
+data Maybe a = Nothing | Just a
+
+data Result e a = Exception e | OK a
+
+data Pair a b = Pair a b
+
+data List a = Nil | Cons a (List a)
+
+Body:
+
+f :: Maybe (Pair Integer Integer) -> List Integer -> Result String Integer
+f = \inpMPair inpList ->
+  match inpMPair
+    (Exception "Input is Nothing")
+    (\pair ->
+       match
+         (\a b ->
+            let listSum = cata (\listF -> match listF
+                                  (0)
+                                  (\x r -> x + r)
+                               )
+            in OK (a + b + listSum)
+         )
+    )
+
+-}
+
+(#+) :: Ref -> Ref -> ASGBuilder Ref
+x #+ y = do
+  plus <- builtin2 AddInteger
+  AnId <$> app' plus [x, y]
+
+(#-) :: Ref -> Ref -> ASGBuilder Ref
+x #- y = do
+  minus <- builtin2 SubtractInteger
+  AnId <$> app' minus [x, y]
+
+(#==) :: Ref -> Ref -> ASGBuilder Ref
+x #== y = do
+  equals <- builtin2 EqualsInteger
+  AnId <$> app' equals [x, y]
+
+conformance_body1 :: Either CovenantError ASG
+conformance_body1 =
+  runASGBuilder
+    (unsafeMkDatatypeInfos conformanceDatatypes1)
+    conformance_body1_builder
+
+conformance_body1_builder :: ASGBuilder Id
+conformance_body1_builder = lam topLevelTy body
+  where
+    {- arg1: Maybe (Pair Integer Integer)
+       arg2: List Integer
+    -}
+    body :: ASGBuilder Ref
+    body = do
+      maybeIntPair <- AnArg <$> arg Z ix0
+      nothingHandler' <- nothingHandler
+      justHandler' <- justHandler
+      AnId <$> match maybeIntPair [AnId nothingHandler', AnId justHandler']
+
+    nothingHandler :: ASGBuilder Id
+    nothingHandler = lazyLam nothingHandlerT $ do
+      errMsg <- AnId <$> lit (AString "Input is nothing")
+      AnId <$> ctor "Result" "Exception" (Vector.singleton errMsg) [There (BuiltinFlat IntegerT)]
+      where
+        nothingHandlerT :: CompT AbstractTy
+        nothingHandlerT = Comp0 $ ReturnT resultT
+
+    justHandler :: ASGBuilder Id
+    justHandler = lazyLam justHandlerT $ do
+      intPair <- AnArg <$> arg Z ix0
+      pairHandler' <- pairHandler
+      AnId <$> match intPair [AnId pairHandler']
+      where
+        justHandlerT :: CompT AbstractTy
+        justHandlerT = Comp0 $ intPairT :--:> ReturnT resultT
+
+    pairHandler :: ASGBuilder Id
+    pairHandler = lazyLam pairHandlerT $ do
+      int1 <- AnArg <$> arg Z ix0
+      int2 <- AnArg <$> arg Z ix1
+      summedArgs <- int1 #+ int2
+      tlListInt <- AnArg <$> arg (S (S Z)) ix1
+      summedList <- AnId <$> sumList tlListInt
+      finalResult <- summedArgs #+ summedList
+      AnId <$> ctor "Result" "OK" [finalResult] [There (BuiltinFlat StringT)]
+      where
+        pairHandlerT :: CompT AbstractTy
+        pairHandlerT = Comp0 $ intT :--:> intT :--:> ReturnT resultT
+
+    sumList :: Ref -> ASGBuilder Id
+    sumList listToSum = do
+      listF <- baseFunctorOf "List"
+      let cataTy = Comp0 $ Datatype listF [intT, intT] :--:> ReturnT intT
+      nilHandler <- AnId <$> lit (AnInteger 0)
+      consHandler <- lazyLam (Comp0 $ intT :--:> intT :--:> ReturnT intT) $ do
+        x <- AnArg <$> arg Z ix0
+        y <- AnArg <$> arg Z ix1
+        x #+ y
+      cata cataTy [nilHandler, AnId consHandler] listToSum
+    {-
+    sumList :: Ref -> ASGBuilder Id
+    sumList listToSum = do
+      sumListF' <- AnId <$> sumListF
+      cata sumListF' listToSum
+
+    sumListF :: ASGBuilder Id
+    sumListF = lazyLam (Comp0 $ listFIntT :--:> ReturnT intT) $ do
+      listFInt <- AnArg <$> arg Z ix0
+      nilHandler <- lazyLam (Comp0 . ReturnT $ intT) (AnId <$> lit (AnInteger 0))
+      consHandler <- lazyLam (Comp0 $ intT :--:> intT :--:> ReturnT intT) $ do
+        x <- AnArg <$> arg Z ix0
+        y <- AnArg <$> arg Z ix1
+        x #+ y
+      AnId <$> match listFInt (AnId <$> [nilHandler, consHandler])
+      where
+        listFIntT :: ValT AbstractTy
+        listFIntT = dtype "#List" [intT, intT]
+    -}
+
+    intT :: ValT AbstractTy
+    intT = BuiltinFlat IntegerT
+
+    stringT :: ValT AbstractTy
+    stringT = BuiltinFlat StringT
+
+    intPairT :: ValT AbstractTy
+    intPairT = dtype "Pair" [intT, intT]
+
+    maybeIntPairT :: ValT AbstractTy
+    maybeIntPairT =
+      dtype
+        "Maybe"
+        [intPairT]
+
+    listIntT :: ValT AbstractTy
+    listIntT = dtype "List" [intT]
+
+    resultT :: ValT AbstractTy
+    resultT = dtype "Result" [stringT, intT]
+
+    topLevelTy :: CompT AbstractTy
+    topLevelTy = Comp0 $ maybeIntPairT :--:> listIntT :--:> ReturnT resultT
+
+{- Case 2:
+
+opaque data Foo = Foo
+
+data Void
+
+data Maybe a = Nothing | Just a
+
+data Pair a b = Pair a b
+
+f :: Maybe (Pair Integer Foo) -> Maybe Boolean
+f mabPairIntFoo =
+  let g :: forall a. Integer -> a  -> Integer
+      g n _x = n + n
+  in match mabPairIntFoo
+       (error "Input is nothing")
+       (\pairIntFoo ->
+          match pairIntFoo (\n foo ->
+            let doubled = g n foo
+                zero    = doubled - doubled
+            in Just (zero == 0)
+          )
+       )
+-}
+
+conformance_body2 :: Either CovenantError ASG
+conformance_body2 =
+  runASGBuilder
+    (unsafeMkDatatypeInfos conformanceDatatypes2)
+    conformance_body2_builder
+
+conformance_body2_builder :: ASGBuilder Id
+conformance_body2_builder = lam topLevelTy body
+  where
+    body :: ASGBuilder Ref
+    body = do
+      maybeIntFooPair <- AnArg <$> arg Z ix0
+      g' <- g
+      nothingHandler' <- nothingHandler
+      justHandler' <- justHandler g'
+      AnId <$> match maybeIntFooPair [AnId nothingHandler', AnId justHandler']
+
+    nothingHandler :: ASGBuilder Id
+    nothingHandler = lazyLam nothingHandlerT (AnId <$> err)
+      where
+        nothingHandlerT :: CompT AbstractTy
+        nothingHandlerT = Comp0 $ ReturnT maybeBoolT
+
+    justHandler :: Id -> ASGBuilder Id
+    justHandler gx = lazyLam justHandlerTy $ do
+      intFooPair <- AnArg <$> arg Z ix0
+      pairHandler' <- pairHandler gx
+      AnId <$> match intFooPair [AnId pairHandler']
+      where
+        justHandlerTy :: CompT AbstractTy
+        justHandlerTy = Comp0 $ pairIntFooT :--:> ReturnT maybeBoolT
+
+    pairHandler :: Id -> ASGBuilder Id
+    pairHandler gx = lazyLam pairHandlerTy $ do
+      intArg <- AnArg <$> arg Z ix0
+      fooArg <- AnArg <$> arg Z ix1
+      doubled <- AnId <$> app' gx [intArg, fooArg]
+      zero <- doubled #- doubled
+      zeroIs0 <- zero #== zero
+      AnId <$> ctor' "Maybe" "Just" [zeroIs0]
+      where
+        pairHandlerTy :: CompT AbstractTy
+        pairHandlerTy = Comp0 $ integerT :--:> fooT :--:> ReturnT maybeBoolT
+
+    g :: ASGBuilder Id
+    g = lam gTy $ do
+      intArg <- AnArg <$> arg Z ix0
+      intArg #+ intArg
+      where
+        gTy :: CompT AbstractTy
+        gTy = Comp1 $ integerT :--:> tyvar Z ix0 :--:> ReturnT integerT
+
+    topLevelTy :: CompT AbstractTy
+    topLevelTy = Comp0 $ maybePairIntFooT :--:> ReturnT maybeBoolT
+
+    integerT :: forall a. ValT a
+    integerT = BuiltinFlat IntegerT
+
+    boolT :: forall a. ValT a
+    boolT = BuiltinFlat BoolT
+
+    fooT :: ValT AbstractTy
+    fooT = dtype "Foo" []
+
+    pairIntFooT :: ValT AbstractTy
+    pairIntFooT = dtype "Pair" [integerT, fooT]
+
+    maybePairIntFooT :: ValT AbstractTy
+    maybePairIntFooT = dtype "Maybe" [pairIntFooT]
+
+    maybeBoolT :: ValT AbstractTy
+    maybeBoolT = dtype "Maybe" [boolT]
diff --git a/test/primops/Main.hs b/test/primops/Main.hs
--- a/test/primops/Main.hs
+++ b/test/primops/Main.hs
@@ -21,8 +21,8 @@
         UnListData,
         UnMapData
       ),
-    SixArgFunc (CaseData, ChooseData),
-    ThreeArgFunc (CaseList, ChooseList),
+    SixArgFunc (ChooseData),
+    ThreeArgFunc (ChooseList),
     TwoArgFunc (ConstrData, EqualsData, MkCons, MkPairData),
     typeOneArgFunc,
     typeSixArgFunc,
@@ -37,15 +37,13 @@
   )
 import Covenant.Type
   ( AbstractTy (BoundAt),
-    CompT (Comp0),
+    CompT,
     Renamed (Unifiable),
-    ValT (Datatype, ThunkT),
+    ValT (Datatype),
     arity,
     boolT,
     byteStringT,
     integerT,
-    pattern ReturnT,
-    pattern (:--:>),
   )
 import Data.Functor.Classes (liftEq)
 import Data.Functor.Identity (Identity (Identity))
@@ -111,13 +109,11 @@
             ],
           testGroup
             "Three arguments"
-            [ testCase "ChooseList" unitChooseList,
-              testCase "CaseList" unitCaseList
+            [ testCase "ChooseList" unitChooseList
             ],
           testGroup
             "Six arguments"
-            [ testCase "ChooseData" unitChooseData,
-              testCase "CaseData" unitCaseData
+            [ testCase "ChooseData" unitChooseData
             ]
         ]
     ]
@@ -248,30 +244,10 @@
    in withRenamedVals [listT, byteStringT, byteStringT] $
         tryAndApply byteStringT renamedFunT
 
-unitCaseList :: IO ()
-unitCaseList = withRenamedComp (typeThreeArgFunc CaseList) $ \renamedFunT ->
-  let listT = Datatype "List" . Vector.singleton $ integerT
-      thunkT = ThunkT $ Comp0 $ integerT :--:> listT :--:> ReturnT byteStringT
-   in withRenamedVals [byteStringT, thunkT, listT] $
-        tryAndApply byteStringT renamedFunT
-
 unitChooseData :: IO ()
 unitChooseData = withRenamedComp (typeSixArgFunc ChooseData) $ \renamedFunT ->
   withRenamedVals [dataT, integerT, integerT, integerT, integerT, integerT] $
     tryAndApply integerT renamedFunT
-
-unitCaseData :: IO ()
-unitCaseData = withRenamedComp (typeSixArgFunc CaseData) $ \renamedFunT ->
-  let listDataT = Datatype "List" . Vector.singleton $ dataT
-      pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT]
-      listPairDataT = Datatype "List" . Vector.singleton $ pairDataT
-      constrThunkT = ThunkT $ Comp0 $ integerT :--:> listDataT :--:> ReturnT integerT
-      mapThunkT = ThunkT $ Comp0 $ listPairDataT :--:> ReturnT integerT
-      listThunkT = ThunkT $ Comp0 $ listDataT :--:> ReturnT integerT
-      integerThunkT = ThunkT $ Comp0 $ integerT :--:> ReturnT integerT
-      byteStringThunkT = ThunkT $ Comp0 $ byteStringT :--:> ReturnT integerT
-   in withRenamedVals [constrThunkT, mapThunkT, listThunkT, integerThunkT, byteStringThunkT, dataT] $
-        tryAndApply integerT renamedFunT
 
 -- Helpers
 
diff --git a/test/type-applications/Main.hs b/test/type-applications/Main.hs
--- a/test/type-applications/Main.hs
+++ b/test/type-applications/Main.hs
@@ -134,8 +134,8 @@
     withRenamedVals mempty excessArgs $ \renamedExcessArgs ->
       case renamedExcessArgs of
         [] -> discard -- should be impossible
-        _ : extraArgs ->
-          let expected = Left . ExcessArgs renamedIdT . Vector.fromList . fmap Just $ extraArgs
+        arg : extraArgs ->
+          let expected = Left . ExcessArgs renamedIdT . Vector.fromList . fmap Just $ (arg : extraArgs)
               actual = checkApp M.empty renamedIdT (fmap Just renamedExcessArgs)
            in expected === actual
   where