covenant 1.2.0 → 1.3.0

raw patch · 19 files changed

+3609/−591 lines, 19 filesdep +aesondep +hex-textPVP ok

version bump matches the API change (PVP)

Dependencies added: aeson, hex-text

API changes (from Hackage documentation)

Files

• CHANGELOG.md +23/−0
• covenant.cabal +13/−2
• src/Covenant/ASG.hs +473/−202
• src/Covenant/Data.hs +135/−20
• src/Covenant/Internal/KindCheck.hs +4/−1
• src/Covenant/Internal/Rename.hs +2/−2
• src/Covenant/Internal/Strategy.hs +7/−24
• src/Covenant/Internal/Term.hs +156/−48
• src/Covenant/Internal/Type.hs +16/−9
• src/Covenant/Internal/Unification.hs +103/−52
• src/Covenant/JSON.hs +1529/−0
• src/Covenant/Prim.hs +4/−30
• src/Covenant/Test.hs +254/−18
• src/Covenant/Type.hs +3/−2
• src/Covenant/Zipper.hs +281/−0
• test/asg/Main.hs +291/−149
• test/json-conformance/Main.hs +307/−0
• test/primops/Main.hs +6/−30
• test/type-applications/Main.hs +2/−2

@@ -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  

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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.

@@ -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     )

@@ -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

@@ -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

@@ -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

@@ -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

@@ -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]

@@ -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

@@ -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+    )

@@ -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 

@@ -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]

@@ -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 

@@ -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