covenant 1.0.0 → 1.1.0

raw patch · 25 files changed

+4221/−478 lines, 25 filesdep +tasty-expected-failuredep ~nonempty-vectordep ~optics-coredep ~vectorPVP ok

version bump matches the API change (PVP)

Dependencies added: tasty-expected-failure

Dependency ranges changed: nonempty-vector, optics-core, vector

API changes (from Hackage documentation)

Files

• CHANGELOG.md +16/−1
• covenant.cabal +35/−3
• src/Covenant/ASG.hs +119/−49
• src/Covenant/Constant.hs +2/−2
• src/Covenant/Data.hs +417/−0
• src/Covenant/DeBruijn.hs +5/−5
• src/Covenant/Internal/KindCheck.hs +263/−0
• src/Covenant/Internal/Ledger.hs +706/−0
• src/Covenant/Internal/PrettyPrint.hs +169/−0
• src/Covenant/Internal/Rename.hs +37/−20
• src/Covenant/Internal/Strategy.hs +100/−0
• src/Covenant/Internal/Term.hs +11/−3
• src/Covenant/Internal/Type.hs +297/−140
• src/Covenant/Internal/Unification.hs +148/−28
• src/Covenant/Prim.hs +160/−76
• src/Covenant/Test.hs +773/−19
• src/Covenant/Type.hs +60/−36
• src/Covenant/Util.hs +15/−0
• test/asg/Main.hs +10/−7
• test/base-functor/Main.hs +46/−0
• test/bb/Main.hs +156/−0
• test/kindcheck/Main.hs +159/−0
• test/primops/Main.hs +238/−10
• test/renaming/Main.hs +8/−38
• test/type-applications/Main.hs +271/−41

@@ -6,6 +6,21 @@  ## UNRELEASED -## 1.0.0 -- 08-05-2025+## 1.1.0 -- 2025-07-11 +### Added ++* Representation of datatype declarations and datatype types +* Generators for various flavors of data declaration and value type +* A "kind checker" which serves as a basic sanity check on datatype declarations ingested by the pipeline +* Base functor transformation machinery +* Tests for the base functor transformation +* Misc internal helpers to support the above functionality +* Ledger type definitions for use in the ASG+* Support for primops over data types+* Support for arity-six primops in the ASG+ Initial version++## 1.0.0 -- 2025-05-07+  

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: covenant-version: 1.0.0+version: 1.1.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.@@ -11,9 +11,9 @@ author: Koz Ross, Sean Hunter maintainer: koz@mlabs.city, sean@mlabs.city bug-reports: https://github.com/mlabs-haskell/covenant/issues-copyright: (C) MLabs 2024+copyright: (C) MLabs 2024-2025 category: Covenant-tested-with: ghc ==9.8.4 || ==9.10.1 || ==9.12.1+tested-with: ghc ==9.8.4 || ==9.10.2 || ==9.12.2 build-type: Simple extra-source-files:   CHANGELOG.md@@ -76,11 +76,19 @@     -with-rtsopts=-N    build-depends:+    -- temporary, maybe, for debugging tests     QuickCheck ==2.15.0.1,+    containers >=0.6.8 && <0.8,     covenant,+    mtl >=2.3.1 && <3,+    nonempty-vector ==0.2.4,+    optics-core ==0.4.1.1,+    prettyprinter ==1.7.1,     tasty ==1.5.3,+    tasty-expected-failure ==0.12.3,     tasty-hunit ==0.10.2,     tasty-quickcheck ==0.11.1,+    vector ==0.13.2.0,  common bench-lang   import: lang@@ -94,6 +102,7 @@     Control.Monad.HashCons     Covenant.ASG     Covenant.Constant+    Covenant.Data     Covenant.DeBruijn     Covenant.Index     Covenant.Prim@@ -102,7 +111,11 @@     Covenant.Util    other-modules:+    Covenant.Internal.KindCheck+    Covenant.Internal.Ledger+    Covenant.Internal.PrettyPrint     Covenant.Internal.Rename+    Covenant.Internal.Strategy     Covenant.Internal.Term     Covenant.Internal.Type     Covenant.Internal.Unification@@ -122,6 +135,7 @@     prettyprinter ==1.7.1,     quickcheck-instances ==0.3.32,     quickcheck-transformer ==0.3.1.2,+    tasty-hunit ==0.10.2,     text >=2.1.1 && <2.2,     transformers >=0.6.1.0 && <0.7.0.0,     vector ==0.13.2.0,@@ -135,6 +149,12 @@   main-is: Main.hs   hs-source-dirs: test/renaming +test-suite base-functor+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test/base-functor+ test-suite type-applications   import: test-lang   type: exitcode-stdio-1.0@@ -158,5 +178,17 @@     vector,    hs-source-dirs: test/asg++test-suite bb+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test/bb++test-suite kindcheck+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test/kindcheck  -- Benchmarks

@@ -35,6 +35,7 @@       ( Builtin1,         Builtin2,         Builtin3,+        Builtin6,         Lam,         Force,         Return@@ -51,38 +52,16 @@     CovenantError (..),     ScopeInfo,     ASGBuilder,-    CovenantTypeError-      ( BrokenIdReference,-        ForceCompType,-        ForceNonThunk,-        ForceError,-        ThunkValType,-        ThunkError,-        ApplyToValType,-        ApplyToError,-        ApplyCompType,-        RenameFunctionFailed,-        RenameArgumentFailed,-        NoSuchArgument,-        ReturnCompType,-        LambdaResultsInValType,-        LambdaResultsInNonReturn,-        ReturnWrapsError,-        ReturnWrapsCompType,-        WrongReturnType,-        UnificationError-      ),-    RenameError-      ( InvalidAbstractionReference,-        IrrelevantAbstraction,-        UndeterminedAbstraction-      ),+    TypeAppError (..),+    RenameError (..),+    CovenantTypeError (..),      -- ** Introducers     arg,     builtin1,     builtin2,     builtin3,+    builtin6,     force,     ret,     lam,@@ -92,6 +71,11 @@     app,      -- ** Elimination++    -- *** Environment+    defaultDatatypes,++    -- *** Function     runASGBuilder,   ) where@@ -113,13 +97,14 @@     runReaderT,   ) import Covenant.Constant (AConstant, typeConstant)+import Covenant.Data (DatatypeInfo, mkDatatypeInfo) import Covenant.DeBruijn (DeBruijn, asInt) import Covenant.Index (Index, count0, intIndex)+import Covenant.Internal.KindCheck (checkEncodingArgs)+import Covenant.Internal.Ledger (ledgerTypes) import Covenant.Internal.Rename   ( RenameError-      ( InvalidAbstractionReference,-        IrrelevantAbstraction,-        UndeterminedAbstraction+      ( InvalidAbstractionReference       ),     renameCompT,     renameValT,@@ -134,6 +119,7 @@       ( Builtin1Internal,         Builtin2Internal,         Builtin3Internal,+        Builtin6Internal,         ForceInternal,         LamInternal,         ReturnInternal@@ -143,6 +129,7 @@         ApplyToError,         ApplyToValType,         BrokenIdReference,+        EncodingError,         ForceCompType,         ForceError,         ForceNonThunk,@@ -170,15 +157,32 @@   ( AbstractTy,     CompT (CompT),     CompTBody (CompTBody),+    DataDeclaration,     Renamed,+    TyName,     ValT (ThunkT),   )-import Covenant.Internal.Unification (checkApp)+import Covenant.Internal.Unification+  ( TypeAppError+      ( DatatypeInfoRenameFailed,+        DoesNotUnify,+        ExcessArgs,+        ImpossibleHappened,+        InsufficientArgs,+        LeakingUnifiable,+        LeakingWildcard,+        NoBBForm,+        NoDatatypeInfo+      ),+    checkApp,+  ) import Covenant.Prim   ( OneArgFunc,+    SixArgFunc,     ThreeArgFunc,     TwoArgFunc,     typeOneArgFunc,+    typeSixArgFunc,     typeThreeArgFunc,     typeTwoArgFunc,   )@@ -201,6 +205,7 @@     over,     preview,     review,+    view,     (%),   ) @@ -244,6 +249,28 @@ nodeAt :: Id -> ASG -> ASGNode nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings +data ASGEnv = ASGEnv ScopeInfo (Map TyName (DatatypeInfo AbstractTy))++instance+  (k ~ A_Lens, a ~ ScopeInfo, b ~ ScopeInfo) =>+  LabelOptic "scopeInfo" k ASGEnv ASGEnv a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(ASGEnv si _) -> si)+      (\(ASGEnv _ dti) si -> ASGEnv si dti)++instance+  (k ~ A_Lens, a ~ Map TyName (DatatypeInfo AbstractTy), b ~ Map TyName (DatatypeInfo AbstractTy)) =>+  LabelOptic "datatypeInfo" k ASGEnv ASGEnv a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(ASGEnv _ dti) -> dti)+      (\(ASGEnv si _) dti -> ASGEnv si dti)+ -- | A tracker for scope-related information while building an ASG -- programmatically. Currently only tracks available arguments. --@@ -295,6 +322,12 @@ pattern Builtin3 :: ThreeArgFunc -> CompNodeInfo pattern Builtin3 f <- Builtin3Internal f +-- | A Plutus primop with six arguments.+--+-- @since 1.1.0+pattern Builtin6 :: SixArgFunc -> CompNodeInfo+pattern Builtin6 f <- Builtin6Internal f+ -- | Force a thunk back into the computation it wraps. -- -- @since 1.0.0@@ -313,7 +346,7 @@ pattern Lam :: Id -> CompNodeInfo pattern Lam i <- LamInternal i -{-# COMPLETE Builtin1, Builtin2, Builtin3, Force, Return, Lam #-}+{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Return, Lam #-}  -- | A compile-time literal of a flat builtin type. --@@ -369,7 +402,7 @@ -- -- @since 1.0.0 newtype ASGBuilder (a :: Type)-  = ASGBuilder (ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a)+  = ASGBuilder (ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a)   deriving     ( -- | @since 1.0.0       Functor,@@ -377,24 +410,38 @@       Applicative,       -- | @since 1.0.0       Monad,-      -- | @since 1.0.0-      MonadReader ScopeInfo,+      -- | @since 1.1.0+      MonadReader ASGEnv,       -- | @since 1.0.0       MonadError CovenantTypeError,       -- | @since 1.0.0       MonadHashCons Id ASGNode     )-    via ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))+    via ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) +-- | A standard collection of types required for almost any realistic script.+-- This includes non-\'flat\' builtin types (such as lists and pairs), as well+-- as all types required by the ledger (including types like @Maybe@).+--+-- @since 1.1.0+defaultDatatypes :: Map TyName (DatatypeInfo AbstractTy)+defaultDatatypes = foldMap go ledgerTypes+  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+ -- | Executes an 'ASGBuilder' to make a \'finished\' ASG. -- -- @since 1.0.0 runASGBuilder ::   forall (a :: Type).+  Map TyName (DatatypeInfo AbstractTy) ->   ASGBuilder a ->   Either CovenantError ASG-runASGBuilder (ASGBuilder comp) =-  case runIdentity . runHashConsT . runExceptT . runReaderT comp . ScopeInfo $ Vector.empty of+runASGBuilder tyDict (ASGBuilder comp) =+  case runIdentity . runHashConsT . runExceptT . runReaderT comp $ ASGEnv (ScopeInfo Vector.empty) tyDict of     (result, bm) -> case result of       Left err' -> Left . TypeError bm $ err'       Right _ -> case Bimap.size bm of@@ -413,14 +460,14 @@ -- @since 1.0.0 arg ::   forall (m :: Type -> Type).-  (MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>   DeBruijn ->   Index "arg" ->   m Arg arg scope index = do-  let scopeAsInt = asInt scope+  let scopeAsInt = review asInt scope   let indexAsInt = review intIndex index-  lookedUp <- asks (preview (#argumentInfo % ix scopeAsInt % ix indexAsInt))+  lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % ix indexAsInt))   case lookedUp of     Nothing -> throwError . NoSuchArgument scope $ index     Just t -> pure . Arg scope index $ t@@ -461,6 +508,18 @@   let node = ACompNode (typeThreeArgFunc bi) . Builtin3Internal $ bi   refTo node +-- | As 'builtin1', but for six-argument primops.+--+-- @since 1.1.0+builtin6 ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m) =>+  SixArgFunc ->+  m Id+builtin6 bi = do+  let node = ACompNode (typeSixArgFunc bi) . Builtin6Internal $ bi+  refTo node+ -- | Given a reference to a thunk, turn it back into a computation. Will fail if -- the reference isn't a thunk. --@@ -513,13 +572,13 @@ -- @since 1.0.0 lam ::   forall (m :: Type -> Type).-  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>   CompT AbstractTy ->   m Id ->   m Id lam expectedT@(CompT _ (CompTBody xs)) bodyComp = do   let (args, resultT) = NonEmpty.unsnoc xs-  bodyId <- local (over #argumentInfo (Vector.cons args)) bodyComp+  bodyId <- local (over (#scopeInfo % #argumentInfo) (Vector.cons args)) bodyComp   bodyNode <- lookupRef bodyId   case bodyNode of     Nothing -> throwError . BrokenIdReference $ bodyId@@ -561,7 +620,7 @@ -- @since 1.0.0 app ::   forall (m :: Type -> Type).-  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>   Id ->   Vector Ref ->   m Id@@ -572,11 +631,11 @@       Left err' -> throwError . RenameFunctionFailed fT $ err'       Right renamedFT -> do         renamedArgs <- traverse renameArg argRefs-        case checkApp renamedFT . Vector.toList $ renamedArgs of-          Left err' -> throwError . UnificationError $ err'-          Right result -> do-            let restored = undoRename result-            refTo . AValNode restored . AppInternal fId $ argRefs+        tyDict <- asks (view #datatypeInfo)+        result <- either (throwError . UnificationError) pure $ checkApp tyDict renamedFT (Vector.toList renamedArgs)+        let restored = undoRename result+        checkEncodingWithInfo tyDict restored+        refTo . AValNode restored . AppInternal fId $ argRefs     ValNodeType t -> throwError . ApplyToValType $ t     ErrorNodeType -> throwError ApplyToError @@ -611,7 +670,8 @@ renameArg ::   forall (m :: Type -> Type).   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>-  Ref -> m (Maybe (ValT Renamed))+  Ref ->+  m (Maybe (ValT Renamed)) renameArg r =   typeRef r >>= \case     CompNodeType t -> throwError . ApplyCompType $ t@@ -619,3 +679,13 @@       Left err' -> throwError . RenameArgumentFailed t $ err'       Right renamed -> pure . Just $ renamed     ErrorNodeType -> pure Nothing++checkEncodingWithInfo ::+  forall (a :: Type) (m :: Type -> Type).+  (MonadError CovenantTypeError m) =>+  Map TyName (DatatypeInfo a) ->+  ValT AbstractTy ->+  m ()+checkEncodingWithInfo tyDict valT = case checkEncodingArgs (view (#originalDecl % #datatypeEncoding)) tyDict valT of+  Left encErr -> throwError $ EncodingError encErr+  Right {} -> pure ()

@@ -49,7 +49,6 @@       Show     ) --- | @since 1.0.0 instance Arbitrary AConstant where   {-# INLINEABLE arbitrary #-}   arbitrary =@@ -73,7 +72,8 @@ -- @since 1.0.0 typeConstant ::   forall (a :: Type).-  AConstant -> ValT a+  AConstant ->+  ValT a typeConstant =   BuiltinFlat . \case     AUnit -> UnitT

@@ -0,0 +1,417 @@+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module: Covenant.Data+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- Information about datatype definitions, and various ways to interact with+-- them. Most of the useful functionality is in 'DatatypeInfo' and its optics.+--+-- = Note+--+-- Some of the low-level functions in the module make use of @ScopeBoundary@.+-- This is mostly an artifact of needing this for tests; if you ever need their+-- functionality, assume that the only sensible value is @0@, which will work+-- via its overloaded number syntax.+--+-- @since 1.1.0+module Covenant.Data+  ( -- * Types+    BBFError (..),+    DatatypeInfo (..),++    -- * Functions++    -- ** Datatype-related+    mkDatatypeInfo,+    allComponentTypes,+    mkBBF,+    noPhantomTyVars,++    -- ** Lower-level+    mkBaseFunctor,+    isRecursiveChildOf,+    hasRecursive,+    everythingOf,+  )+where++import Control.Monad.Except (MonadError (throwError))+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.Internal.PrettyPrint (ScopeBoundary (ScopeBoundary))+import Covenant.Internal.Type+  ( AbstractTy (BoundAt),+    CompT (CompT),+    CompTBody (CompTBody),+    Constructor (Constructor),+    ConstructorName (ConstructorName),+    DataDeclaration (DataDeclaration, OpaqueData),+    TyName (TyName),+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+  )+import Data.Bitraversable (bisequence)+import Data.Kind (Type)+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.Indexed.Core (A_Fold)++-- | All possible errors that could arise when constructing a Boehm-Berrarducci+-- form.+--+-- @since 1.1.0+data BBFError+  = -- | The type is recursive in a prohibited way. Typically, this means+    -- contravariant recursion. This gives the type name and the invalid+    -- recursive constructor argument.+    --+    -- @since 1.1.0+    InvalidRecursion TyName (ValT AbstractTy)+  deriving stock+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq+    )++-- | Contains essential information about datatype definitions. Most of the+-- time, you want to use this type via its optics, rather than directly.+--+-- In pretty much any case imaginable, the @var@ type variable will be one of+-- 'AbstractTy' or 'Renamed'.+--+-- @since 1.1.0+data DatatypeInfo (var :: Type)+  = DatatypeInfo+  { _originalDecl :: DataDeclaration var,+    _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)+  }+  deriving stock+    ( -- | @since 1.1.0+      Eq,+      -- | @since 1.1.0+      Show+    )++-- | The original declaration of the data type.+--+-- @since 1.1.0+instance+  (k ~ A_Lens, a ~ DataDeclaration var, b ~ DataDeclaration var) =>+  LabelOptic "originalDecl" k (DatatypeInfo var) (DatatypeInfo var) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(DatatypeInfo ogDecl _ _) -> ogDecl)+      (\(DatatypeInfo _ b c) ogDecl -> DatatypeInfo ogDecl b c)++-- | The base functor for this data type, if it exists. Types which are not+-- self-recursive lack base functors.+--+-- @since 1.1.0+instance+  (k ~ A_Lens, a ~ Maybe (DataDeclaration var, ValT var), b ~ Maybe (DataDeclaration var, ValT var)) =>+  LabelOptic "baseFunctor" k (DatatypeInfo var) (DatatypeInfo var) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(DatatypeInfo _ baseF _) -> baseF)+      (\(DatatypeInfo a _ c) baseF -> DatatypeInfo a baseF c)++-- | The Boehm-Berrarducci form of this type, if it exists. Types with no+-- constructors (that is, types without inhabitants) lack Boehm-Berrarducci+-- forms.+--+-- @since 1.1.0+instance+  (k ~ A_Lens, a ~ Maybe (ValT var), b ~ Maybe (ValT var)) =>+  LabelOptic "bbForm" k (DatatypeInfo var) (DatatypeInfo var) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(DatatypeInfo _ _ bb) -> bb)+      (\(DatatypeInfo a b _) bb -> DatatypeInfo a b bb)++-- | 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+-- functor Boehm-Berrarducci form. In other words, they must have at least one+-- constructor and be self-recursive.+--+-- @since 1.1.0+instance+  (k ~ A_Fold, a ~ ValT var, b ~ ValT var) =>+  LabelOptic "bbBaseF" k (DatatypeInfo var) (DatatypeInfo var) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = #baseFunctor % folded % _2++-- | Given a declaration of a datatype, either produce its datatype info, or+-- fail.+--+-- @since 1.1.0+mkDatatypeInfo :: DataDeclaration AbstractTy -> Either BBFError (DatatypeInfo AbstractTy)+mkDatatypeInfo decl = DatatypeInfo decl <$> baseFStuff <*> mkBBF decl+  where+    baseFStuff :: Either BBFError (Maybe (DataDeclaration AbstractTy, ValT AbstractTy))+    baseFStuff =+      let baseFDecl = runReader (mkBaseFunctor decl) 0+          baseBBF = case baseFDecl of+            Nothing -> Right Nothing+            Just d -> mkBBF d+       in (bisequence . (baseFDecl,) <$> baseBBF)++-- | Returns all datatype constructors used as any argument to the datatype+-- defined by the first argument.+--+-- @since 1.1.0+allComponentTypes :: DataDeclaration AbstractTy -> [ValT AbstractTy]+allComponentTypes = toListOf (#datatypeConstructors % folded % #constructorArgs % folded)++-- | Constructs a base functor from a suitable data declaration, returning+-- 'Nothing' if the input is not a recursive type.+--+-- @since 1.1.0+mkBaseFunctor :: DataDeclaration AbstractTy -> Reader ScopeBoundary (Maybe (DataDeclaration AbstractTy))+mkBaseFunctor OpaqueData {} = pure Nothing+mkBaseFunctor (DataDeclaration tn numVars ctors strat) = 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+  where+    baseFName :: TyName+    baseFName = case tn of+      TyName tyNameInner -> TyName (tyNameInner <> "_F")+    baseFNumVars :: Count "tyvar"+    baseFNumVars = fromJust . preview intCount $ review intCount numVars + 1+    -- The argument position of the new type variable parameter (typically `r`).+    -- A count represents the number of variables, but indices for those variables start at 0,+    -- so an additional tyvar will always have an index == the old count+    rIndex :: Index "tyvar"+    rIndex = fromJust . preview intIndex $ review intCount numVars+    -- Replace recursive children with a DeBruijn index & position index that points at the top-level binding context+    -- (technically the top level binding context is the ONLY admissable binding context if we forbid higher-rank types,+    -- but we still have to regard a computation type that binds 0 variables as having a scope boundary)+    replaceWithR :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)+    replaceWithR vt =+      isRecursive vt >>= \case+        True -> do+          ScopeBoundary here <- ask -- this should be the distance from the initial binding context (which is what we want)+          let db = fromJust $ preview asInt here+          pure $ Abstraction (BoundAt db rIndex)+        False -> pure vt+    -- TODO: This should be refactored with `mapMValT`, which I will do after I write it :P+    replaceAllRecursive :: ValT AbstractTy -> Reader ScopeBoundary (ValT AbstractTy)+    replaceAllRecursive = \case+      abst@Abstraction {} -> pure abst+      bif@BuiltinFlat {} -> pure bif+      ThunkT (CompT cnt (CompTBody compTargs)) ->+        local (+ 1) $ ThunkT . CompT cnt . CompTBody <$> traverse replaceAllRecursive compTargs+      Datatype tx args -> (replaceWithR . Datatype tx =<< traverse replaceAllRecursive args)+    mkBaseCtor :: Constructor AbstractTy -> Reader ScopeBoundary (Constructor AbstractTy)+    mkBaseCtor (Constructor ctorNm ctorArgs) = Constructor (baseFCtorName ctorNm) <$> traverse replaceAllRecursive ctorArgs+      where+        baseFCtorName :: ConstructorName -> ConstructorName+        baseFCtorName (ConstructorName nm) = ConstructorName (nm <> "_F")+    allCtorArgs :: [ValT AbstractTy]+    allCtorArgs = concatMap (V.toList . view #constructorArgs) ctors+    -- This tells us whether the ValT *is* a recursive child of the parent type+    isRecursive :: ValT AbstractTy -> Reader ScopeBoundary Bool+    isRecursive = isRecursiveChildOf tn++-- | Returns 'True' if the second argument is a recursive child of the datatype+-- named by the first argument.+--+-- @since 1.1.0+isRecursiveChildOf :: TyName -> ValT AbstractTy -> Reader ScopeBoundary Bool+isRecursiveChildOf tn = \case+  Datatype tn' args+    | tn' == tn -> V.ifoldM checkArgsIsRec' True args+    | otherwise -> pure False+  _ -> pure False+  where+    checkArgsIsRec' :: Bool -> Int -> ValT AbstractTy -> Reader ScopeBoundary Bool+    checkArgsIsRec' acc n = \case+      Abstraction (BoundAt db varIx) -> do+        ScopeBoundary here <- ask+        let dbInt = review asInt db+        -- Explanation: A component ValT is only a recursive instance of the parent type if+        --              the DeBruijn index of its type variables points to Z (and the other conditions obtain)+        if dbInt - here == 0 && review intIndex varIx == n+          then pure acc+          else pure False+      _ -> pure False++-- | Determines whether the type represented by the second argument and named by+-- the first requires a base functor.+--+-- @since 1.1.0+hasRecursive :: TyName -> ValT AbstractTy -> Reader ScopeBoundary Bool+hasRecursive tn = \case+  Abstraction {} -> pure False+  BuiltinFlat {} -> pure False+  -- NOTE: This assumes that we've forbidden higher rank arguments to constructors (i.e. we can ignore the scope here)+  ThunkT (CompT _ (CompTBody (NEV.toList -> compTArgs))) -> local (+ 1) $ do+    or <$> traverse (hasRecursive tn) compTArgs+  dt@(Datatype _ args) -> do+    thisTypeIsRecursive <- isRecursiveChildOf tn dt+    aComponentIsRecursive <- or <$> traverse (hasRecursive tn) args+    pure $ thisTypeIsRecursive || aComponentIsRecursive++-- | Constructs a base functor Boehm-Berrarducci form for the given datatype.+-- Returns 'Nothing' if the type is not self-recursive.+--+-- @since 1.1.0+mkBBF :: DataDeclaration AbstractTy -> Either BBFError (Maybe (ValT AbstractTy))+mkBBF decl = sequence . runExceptT $ mkBBF' decl++-- | Verifies that all type variables declared by the given datatype have a+-- corresponding value in some \'arm\'.+--+-- @since 1.1.0+noPhantomTyVars :: DataDeclaration AbstractTy -> Bool+noPhantomTyVars OpaqueData {} = True+noPhantomTyVars decl@(DataDeclaration _ numVars _ _) =+  let allChildren = allComponentTypes decl+      allResolved = Set.unions $ runReader (traverse allResolvedTyVars' allChildren) 0+      indices :: [Index "tyvar"]+      indices = fromJust . preview intIndex <$> [0 .. (review intCount numVars - 1)]+      declaredTyVars = BoundAt Z <$> indices+   in all (`Set.member` allResolved) declaredTyVars++-- | Collect all (other) value types a given value type refers to.+--+-- @since 1.1.0+everythingOf :: forall (a :: Type). (Ord a) => ValT a -> Set (ValT a)+everythingOf = foldValT (flip Set.insert) Set.empty++-- Helpers++{- NOTE: For the purposes of base functor transformation, we follow the pattern established by Edward Kmett's+         'recursion-schemes' library. That is, we regard a datatype as "recursive" if and only if at least one+         argument to a constructor contains "the exact same thing as we find to the left of the =". Dunno how to+         describe it more precisely, but the general idea is that things like these ARE recursive for us:++           data Foo = End Int | More Foo Int -- contains 'Foo' as a ctor arg++           data Bar a = Beep | Boom a (Bar a) -- contains 'Bar a'++         but things like this are NOT recursive by our reckoning (even though in some sense they might be considered as such):++           data FunL a b = Done b | Go (FunL b a) a -- `FunL b a` isn't `FunL a b` so it's not literally recursive++         Obviously we're working with DeBruijn indices so the letters are more-or-less fictitious, but hopefully+         these examples nonetheless get the point across.+-}++-- TODO: Rewrite this as `mapMValT`. The change to a `Reader` below makes this unusable, but we can+--       write the non-monadic version as a special case of the monadic version and it is *highly* likely+--       we will need both going forward.+mapValT :: forall (a :: Type). (ValT a -> ValT a) -> ValT a -> ValT a+mapValT f = \case+  -- for terminal nodes we just apply the function+  absr@(Abstraction {}) -> f absr+  bif@BuiltinFlat {} -> f bif+  -- For CompT and Datatype we apply the function to the components and then to the top level+  ThunkT (CompT cnt (CompTBody compTargs)) -> f (ThunkT $ CompT cnt (CompTBody (mapValT f <$> compTargs)))+  Datatype tn args -> f $ Datatype tn (mapValT f <$> args)++-- Did in fact need it+foldValT :: forall (a :: Type) (b :: Type). (b -> ValT a -> b) -> b -> ValT a -> b+foldValT f e = \case+  absr@(Abstraction {}) -> f e absr+  bif@(BuiltinFlat {}) -> f e bif+  thk@(ThunkT (CompT _ (CompTBody compTArgs))) ->+    let e' = NEV.foldl' f e compTArgs+     in f e' thk+  dt@(Datatype _ args) ->+    let e' = V.foldl' f e args+     in f e' dt++allResolvedTyVars' :: ValT AbstractTy -> Reader Int (Set AbstractTy)+allResolvedTyVars' = \case+  Abstraction (BoundAt db argpos) -> do+    here <- ask+    let db' = fromJust . preview asInt $ review asInt db - here+    pure . Set.singleton $ BoundAt db' argpos+  ThunkT (CompT _ (CompTBody nev)) -> local (+ 1) $ do+    Set.unions <$> traverse allResolvedTyVars' nev+  BuiltinFlat {} -> pure Set.empty+  Datatype _ args -> Set.unions <$> traverse allResolvedTyVars' args++incAbstractionDB :: ValT AbstractTy -> ValT AbstractTy+incAbstractionDB = mapValT $ \case+  Abstraction (BoundAt db indx) ->+    let db' = fromJust . preview asInt $ review asInt db + 1+     in Abstraction (BoundAt db' indx)+  other -> other++-- 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' (DataDeclaration tn numVars ctors _)+  | V.null ctors = lift Nothing+  | otherwise = do+      ctors' <- traverse mkBBCtor ctors+      lift $ ThunkT . CompT bbfCount . CompTBody . flip NEV.snoc topLevelOut <$> NEV.fromVector ctors'+  where+    topLevelOut = Abstraction $ BoundAt Z outIx++    outIx :: Index "tyvar"+    outIx = fromJust . preview intIndex $ review intCount numVars++    bbfCount = fromJust . preview intCount $ review intCount numVars + 1++    mkBBCtor :: Constructor AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)+    mkBBCtor (Constructor _ args)+      | V.null args = pure topLevelOut+      | otherwise = do+          elimArgs <- fmap incAbstractionDB <$> traverse fixArg args+          elimArgs' <- lift . NEV.fromVector $ elimArgs+          let out = Abstraction $ BoundAt (S Z) outIx+          pure . ThunkT . CompT count0 . CompTBody . flip NEV.snoc out $ elimArgs'++    fixArg :: ValT AbstractTy -> ExceptT BBFError Maybe (ValT AbstractTy)+    fixArg arg = do+      let isDirectRecursiveTy = runReader (isRecursiveChildOf tn arg) 0+      if isDirectRecursiveTy+        then pure $ Abstraction (BoundAt Z outIx)+        else case arg of+          Datatype tn' dtArgs+            | tn == tn' -> throwError $ InvalidRecursion tn arg+            | otherwise -> do+                dtArgs' <- traverse fixArg dtArgs+                pure . Datatype tn' $ dtArgs'+          _ -> pure arg++{- Note (Sean, 14/05/25): Re  DeBruijn indices:++     - None of the existing variable DeBruijn or position indices change at all b/c the binding context of the+       `forall` we're introducing replaces the binding context of the datatype declaration and only extends it.++     - The only special thing we have to keep track of is the (DeBruijn) index of the `out` variable, but this doesn't require+       any fancy scope tracking: It will always be Z for the top-level result and `S Z` wherever it occurs in a+       transformed constructor. It won't ever occur any "deeper" than that (because we don't nest these, and a constructor gets exactly one+       `out`)++     - Actually this is slightly false, we need to "bump" all of the indices inside constructor arms by one (because+       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)+-}

@@ -19,6 +19,7 @@ import Data.List.NonEmpty (NonEmpty) import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum)) import Data.Word (Word32)+import Optics.Core (Prism', prism) import Test.QuickCheck (Arbitrary)  -- | A DeBruijn index.@@ -75,13 +76,12 @@  {-# COMPLETE Z, S #-} --- | Convert a DeBruijn index into a (non-negative) 'Int'.+-- | Construct a DeBruijn from an Int, or deconstruct a Debruijn into an Int ----- @since 1.0.0-asInt :: DeBruijn -> Int-asInt (DeBruijn i) = fromIntegral i+-- @since 1.1.0+asInt :: Prism' Int DeBruijn+asInt = prism (\(DeBruijn x) -> fromIntegral x) (\x -> if x >= 0 then Right . DeBruijn $ fromIntegral x else Left x)  -- Helpers- reduce :: DeBruijn -> Maybe DeBruijn reduce (DeBruijn x) = DeBruijn (x - 1) <$ guard (x > 0)

@@ -0,0 +1,263 @@+-- | This module define a "kind-checking" pass. This requires some explanation, since we don't have+--     an *explicit* notion of kinds in Covenant:+--+--     With the addition of type constructors for datatypes into ValT comes a new set of things that can+--     "go wrong". In particular:+--       - Someone may try to use a type constructor which is not defined anywhere+--       - A type may be applied to an incorrect number of arguments+--       - The "count" - the number of bound tyvars in the `ValT.Datatype` representation - may be incorrect (i.e. inconsistent with the count in the declaration)+--+--     The checks to detect these errors are entirely independent from the checks performed during typechecking or renaming, so we do them in a separate pass.+module Covenant.Internal.KindCheck+  ( checkDataDecls,+    checkValT,+    KindCheckError (..),+    EncodingArgErr (..),+    cycleCheck,+    checkEncodingArgs,+  )+where++import Control.Monad (unless)+import Control.Monad.Except (ExceptT, MonadError (throwError), runExceptT)+import Control.Monad.Reader+  ( MonadReader (local),+    ReaderT (ReaderT),+    asks,+    runReaderT,+  )+import Covenant.Data (everythingOf)+import Covenant.Index (Count, intCount)+import Covenant.Internal.Strategy+  ( DataEncoding (SOP),+  )+import Covenant.Internal.Type+  ( AbstractTy,+    CompT (CompT),+    CompTBody (CompTBody),+    Constructor (Constructor),+    DataDeclaration (DataDeclaration, OpaqueData),+    TyName,+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+    checkStrategy,+    datatype,+  )+import Data.Foldable (traverse_)+import Data.Functor.Identity (Identity, runIdentity)+import Data.Kind (Type)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as M+import Data.Maybe (mapMaybe)+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Vector (Vector)+import Data.Vector qualified as V+import Optics.Core (A_Lens, LabelOptic (labelOptic), folded, lens, preview, review, to, toListOf, view, (%))++{- TODO: Explicitly separate the kind checker into two check functions:+     - One which kind checks `ValT`s to ensure:+       1. All TyCons in the ValT exist+       2. All TyCons in the ValT have the correct arity++     - One which checks *datatype declarations* to ensure:+       1. Everything satisfies the above ValT checks+       2. No thunk arguments to ctors!+       3. No mutual recursion (cycles)+-}++data KindCheckError+  = UnknownType TyName+  | IncorrectNumArgs TyName (Count "tyvar") (Vector (ValT AbstractTy)) -- first is expected (from the decl), second is actual+  | ThunkConstructorArg (CompT AbstractTy) -- no polymorphic function args to ctors+  | MutualRecursionDetected (Set TyName)+  | InvalidStrategy TyName+  | EncodingMismatch (EncodingArgErr AbstractTy)+  deriving stock (Show, Eq)++newtype KindCheckContext a = KindCheckContext (Map TyName (DataDeclaration a))++instance+  (k ~ A_Lens, a ~ Map TyName (DataDeclaration c), b ~ Map TyName (DataDeclaration c)) =>+  LabelOptic "kindCheckContext" k (KindCheckContext c) (KindCheckContext c) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(KindCheckContext x) -> x)+      (\(KindCheckContext _) x' -> KindCheckContext x')++newtype KindCheckM t a = KindCheckM (ReaderT (KindCheckContext t) (ExceptT KindCheckError Identity) a)+  deriving+    (Functor, Applicative, Monad, MonadReader (KindCheckContext t), MonadError KindCheckError)+    via (ReaderT (KindCheckContext t) (ExceptT KindCheckError Identity))++runKindCheckM :: forall (t :: Type) (a :: Type). Map TyName (DataDeclaration t) -> KindCheckM t a -> Either KindCheckError a+runKindCheckM dtypes (KindCheckM act) = runIdentity . runExceptT $ runReaderT act (KindCheckContext dtypes)++lookupDeclaration :: forall (t :: Type). TyName -> KindCheckM t (DataDeclaration t)+lookupDeclaration tn = do+  types <- asks (view #kindCheckContext)+  case M.lookup tn types of+    Nothing -> throwError $ UnknownType tn+    Just decl -> pure decl++{- This sanity checks datatype declarations using the criteria enumerated above.+-}++-- | Checks that all the data declarations in the argument \'make sense\'.+-- Specifically:+--+-- * The strategy declared for the datatype is valid for it+-- * There are no mutually recursive datatype declarations+-- * Constructor arguments are not thunks+-- * The number of type variables in any constructor isn't greater than we+-- expect+--+-- @since 1.1.0+checkDataDecls :: Map TyName (DataDeclaration AbstractTy) -> Either KindCheckError ()+checkDataDecls decls = runKindCheckM decls $ traverse_ checkDataDecl (M.elems decls)++checkDataDecl :: DataDeclaration AbstractTy -> KindCheckM AbstractTy ()+checkDataDecl OpaqueData {} = pure ()+checkDataDecl decl@(DataDeclaration tn _ ctors _) = do+  unless (checkStrategy decl) $ throwError (InvalidStrategy tn)+  cycleCheck' mempty decl+  let allCtorArgs = view #constructorArgs =<< ctors+  traverse_ (checkKinds CheckDataDecl) allCtorArgs+  checkEncodingArgsInDataDecl decl++data KindCheckMode = CheckDataDecl | CheckValT+  deriving stock (Show, Eq, Ord)++-- This isn't really a "kind checker" in the normal sense and just checks that none of the three failure conditions above obtain+checkKinds :: KindCheckMode -> ValT AbstractTy -> KindCheckM AbstractTy ()+checkKinds mode = \case+  Abstraction _ -> pure ()+  ThunkT compT@(CompT _ (CompTBody nev))+    | mode == CheckDataDecl -> throwError $ ThunkConstructorArg compT+    | otherwise -> traverse_ (checkKinds mode) nev+  BuiltinFlat {} -> pure ()+  Datatype tn args ->+    lookupDeclaration tn >>= \case+      OpaqueData {} -> pure ()+      DataDeclaration _ numVars _ _ -> do+        let numArgsActual = V.length args+            numArgsExpected = review intCount numVars+        unless (numArgsActual == numArgsExpected) $ throwError (IncorrectNumArgs tn numVars args)+        traverse_ (checkKinds mode) args++-- | This is for checking type annotations in the ASG, *not* datatypes+checkValT :: Map TyName (DataDeclaration AbstractTy) -> ValT AbstractTy -> Maybe KindCheckError+checkValT dtypes = either Just (const Nothing) . runKindCheckM dtypes . checkKinds CheckValT++-- | Verifies that no types in the argument are mutually recursive.+--+-- @since 1.1.0+cycleCheck :: forall (a :: Type). (Ord a) => Map TyName (DataDeclaration a) -> Maybe KindCheckError+cycleCheck decls = either Just (const Nothing) $ runKindCheckM decls go+  where+    go =+      local (\_ -> KindCheckContext decls) $+        traverse_ (cycleCheck' mempty) =<< asks (view (#kindCheckContext % to M.elems))++{- This is a bit odd b/c we don't want to fail for auto-recursive types, so we need to be careful+   *not* to mark the current decl being examined as "visited" until we've "descended" into the dependencies+   (I think?)+-}+cycleCheck' :: forall (a :: Type). (Ord a) => Set TyName -> DataDeclaration a -> KindCheckM a ()+cycleCheck' _ OpaqueData {} = pure ()+cycleCheck' visited (DataDeclaration tn _ ctors _) = traverse_ (checkCtor visited tn) ctors+  where+    checkCtor :: Set TyName -> TyName -> Constructor a -> KindCheckM a ()+    checkCtor vs tn' (Constructor _ args) = do+      let allComponents = Set.toList . Set.unions $ everythingOf <$> V.toList args+          -- every type constructor in any part of a constructor arg, *except* the tycon of the decl+          -- we're examining, since autorecursion is fine/necessary+          allTyCons = Set.filter (/= tn') . Set.fromList . mapMaybe (fmap fst . preview datatype) $ allComponents+          alreadyVisitedArgTys = Set.intersection allTyCons vs+      unless (null alreadyVisitedArgTys) $ throwError (MutualRecursionDetected alreadyVisitedArgTys)+      let newVisited = Set.insert tn' vs+      nextRound <- traverse lookupDeclaration (Set.toList allTyCons)+      traverse_ (cycleCheck' newVisited) nextRound++{- Arguably the closest thing to a real kind checker in the module.++   Checks whether the arguments to type constructors (ValT 'Datatype's) conform with their encoding.++-}++-- First arg is the name of the type constructor w/ a bad argument, second arg is the bad argument.+data EncodingArgErr a = EncodingArgMismatch TyName (ValT a)+  deriving stock (Show, Eq)++-- | Verifies that a datatype (third argument) is valid according to its stated+-- encoding, as provided by the first two arguments (projection and metadata).+--+-- = Note+--+-- If the datatype being validated refers to other datatypes, we assume that+-- they exist in the metadata 'Map'. Thus, we must ensure this holds or the+-- check will fail.+--+-- @since 1.1.0+checkEncodingArgs ::+  forall (a :: Type) (info :: Type).+  (info -> DataEncoding) -> -- this lets us not care about whether we're doing this w/ a DataDeclaration or DatatypeInfo+  Map TyName info ->+  ValT a ->+  Either (EncodingArgErr a) ()+checkEncodingArgs getEncoding tyDict = \case+  Abstraction {} -> pure ()+  BuiltinFlat {} -> pure ()+  ThunkT (CompT _ (CompTBody args)) -> traverse_ go args+  Datatype tn args -> do+    let encoding = getEncoding $ tyDict M.! tn+    case encoding of+      -- Might as well check all the way down+      SOP -> do+        {- NOTE Sean 7/2/25: We are *temporarily* disallowing thunk arguments to SOPs to speed up development and+                             create consistency. We disallow Thunk arguments to constructors in datatype declarations,+                             and while we could very well allow them outside of those declarations, it creates a strange situation+                             where the same function might be safe/unsafe depending on whether it is used on a ValT inside of a data+                             declaration vs (e.g.) a type annotation in the ASG.++                             To remove this restriction, delete the `traverse_ isValidSOPArg args` line below+        -}+        traverse_ go args+        traverse_ (isValidSOPArg tn) args++      -- Both explicit data encodings and builtins should be "morally data encoded"+      _ -> do+        traverse_ go args+        traverse_ (isValidDataArg tn) args+  where+    go :: ValT a -> Either (EncodingArgErr a) ()+    go = checkEncodingArgs getEncoding tyDict++    isValidDataArg :: TyName -> ValT a -> Either (EncodingArgErr a) ()+    isValidDataArg tn = \case+      Abstraction {} -> pure ()+      BuiltinFlat {} -> pure ()+      thunk@ThunkT {} -> throwError $ EncodingArgMismatch tn thunk+      dt@(Datatype tn' args') -> do+        let encoding = getEncoding $ tyDict M.! tn'+        case encoding of+          SOP -> throwError $ EncodingArgMismatch tn dt+          _ -> traverse_ go args'++    isValidSOPArg :: TyName -> ValT a -> Either (EncodingArgErr a) ()+    isValidSOPArg tn = \case+      Abstraction {} -> pure ()+      BuiltinFlat {} -> pure ()+      thunk@ThunkT {} -> throwError $ EncodingArgMismatch tn thunk+      Datatype tn' args' -> traverse_ (isValidSOPArg tn') args'++checkEncodingArgsInDataDecl :: DataDeclaration AbstractTy -> KindCheckM AbstractTy ()+checkEncodingArgsInDataDecl decl =+  asks (view #kindCheckContext) >>= \tyDict ->+    case traverse (checkEncodingArgs (view #datatypeEncoding) tyDict) allConstructorArgs of+      Left encErr -> throwError $ EncodingMismatch encErr+      Right _ -> pure ()+  where+    allConstructorArgs :: Vector (ValT AbstractTy)+    allConstructorArgs = V.concat $ toListOf (#datatypeConstructors % folded % #constructorArgs) decl

@@ -0,0 +1,706 @@+module Covenant.Internal.Ledger+  ( ledgerTypes,+    -- For testing+    DeclBuilder (Decl),+    CtorBuilder (Ctor),+    mkDecl,+    maybeT,+    pair,+    list,+    tree,+    weirderList,+  )+where++import Covenant.DeBruijn (DeBruijn (Z))+import Covenant.Index (Count, count0, count1, count2, ix0, ix1)+import Covenant.Internal.Strategy+  ( DataEncoding (BuiltinStrategy, PlutusData),+    InternalStrategy (InternalAssocMapStrat, InternalDataStrat, InternalListStrat, InternalPairStrat),+    PlutusDataStrategy (ConstrData, NewtypeData),+  )+import Covenant.Internal.Type+  ( AbstractTy (BoundAt),+    BuiltinFlatT (BoolT, ByteStringT, IntegerT),+    Constructor (Constructor),+    ConstructorName (ConstructorName),+    DataDeclaration (DataDeclaration),+    TyName (TyName),+    ValT (Abstraction, BuiltinFlat, Datatype),+  )+import Data.Coerce (coerce)+import Data.Vector qualified as Vector++-- All the ledger types. Just putting them in a list for now but they'll probably end up in some other kind of container eventually+ledgerTypes :: [DataDeclaration AbstractTy]+ledgerTypes =+  [ list,+    pair,+    plutusData,+    datum,+    redeemer,+    scriptHash,+    datumHash,+    redeemerHash,+    credential,+    stakingCredential,+    pubKeyHash,+    address,+    maybeT,+    posixTime,+    interval,+    upperBound,+    lowerBound,+    extended,+    ledgerBytes,+    assocMap,+    currencySymbol,+    tokenName,+    value,+    lovelace,+    rational,+    mintValue,+    txId,+    txOutRef,+    txOut,+    outputDatum,+    txInInfo,+    dRepCredential,+    dRep,+    delegatee,+    coldCommitteeCredential,+    hotCommitteeCredential,+    txCert,+    voter,+    vote,+    governanceActionId,+    committee,+    constitution,+    changedParameters,+    protocolVersion,+    governanceAction,+    proposalProcedure,+    scriptPurpose,+    scriptInfo,+    txInfo,+    scriptContext+  ]++-- Builtins. These aren't "real" ADTs and their unique encoding strategies indicate special handling++-- Note (Koz, 11/07/25): This has a Haddock, and is versioned, because+-- Covenant.Test exposes it. If we ever stop doing this, we can remove this+-- Haddock.++-- | The onchain list type.+--+-- @since 1.1.0+list :: DataDeclaration AbstractTy+list =+  mkDecl $+    Decl+      "List"+      count1+      [ Ctor "Nil" [],+        Ctor "Cons" [Abstraction (BoundAt Z ix0), tycon "List" [Abstraction (BoundAt Z ix0)]]+      ]+      (BuiltinStrategy InternalListStrat)++pair :: DataDeclaration AbstractTy+pair = mkDecl $ Decl "Pair" count2 [Ctor "Pair" [a, b]] (BuiltinStrategy InternalPairStrat)++-- Make sure this matches up with chooseData+plutusData :: DataDeclaration AbstractTy+plutusData =+  mkDecl $+    Decl+      "Data"+      count0+      [ Ctor "Constr" [BuiltinFlat IntegerT, tycon "List" [tycon "Data" []]],+        Ctor "Map" [tycon "List" [tycon "Pair" [tycon "Data" [], tycon "Data" []]]],+        Ctor "List" [tycon "List" [tycon "Data" []]],+        Ctor "I" [BuiltinFlat IntegerT],+        Ctor "B" [BuiltinFlat ByteStringT]+      ]+      (BuiltinStrategy InternalDataStrat)++-- Newtypes and Hash Types (from V1)++datum :: DataDeclaration AbstractTy+datum = mkDecl $ Decl "Datum" count0 [Ctor "Datum" [tycon "Data" []]] (PlutusData NewtypeData)++redeemer :: DataDeclaration AbstractTy+redeemer = mkDecl $ Decl "Redeemer" count0 [Ctor "Redeemer" [tycon "Data" []]] (PlutusData NewtypeData)++scriptHash :: DataDeclaration AbstractTy+scriptHash = mkDecl $ Decl "ScriptHash" count0 [Ctor "ScriptHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData)++datumHash :: DataDeclaration AbstractTy+datumHash = mkDecl $ Decl "DatumHash" count0 [Ctor "DatumHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData)++redeemerHash :: DataDeclaration AbstractTy+redeemerHash = mkDecl $ Decl "RedeemerHash" count0 [Ctor "RedeemerHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData)++-- Credential + Staking Credential (from V1)+credential :: DataDeclaration AbstractTy+credential =+  mkDecl $+    Decl+      "Credential"+      count0+      [ Ctor "PubKeyCredential" [tycon "PubKeyHash" []],+        Ctor "ScriptCredential" [tycon "ScriptHash" []]+      ]+      (PlutusData ConstrData)++stakingCredential :: DataDeclaration AbstractTy+stakingCredential =+  mkDecl $+    Decl+      "StakingCredential"+      count0+      [ Ctor "StakingHash" [tycon "Credential" []],+        Ctor "StakingPtr" [BuiltinFlat IntegerT, BuiltinFlat IntegerT, BuiltinFlat IntegerT]+      ]+      (PlutusData ConstrData)++-- PubKeyHash (from V1)+pubKeyHash :: DataDeclaration AbstractTy+pubKeyHash = mkDecl $ Decl "PubKeyHash" count0 [Ctor "PubKeyHash" [BuiltinFlat ByteStringT]] (PlutusData NewtypeData)++-- Address (from V1)+address :: DataDeclaration AbstractTy+address =+  mkDecl $+    Decl+      "Address"+      count0+      [ Ctor "Address" [tycon "Credential" [], tycon "Maybe" [tycon "StakingCredential" []]]+      ]+      (PlutusData ConstrData)++-- PlutusTX types, from https://github.com/IntersectMBO/plutus/blob/master/plutus-tx/src/PlutusTx/IsData/Instances.hs+maybeT :: DataDeclaration AbstractTy+maybeT =+  mkDecl $+    Decl+      "Maybe"+      count1+      [ Ctor "Just" [Abstraction (BoundAt Z ix0)],+        Ctor "Nothing" []+      ]+      (PlutusData ConstrData)++-- Time & Intervals (V1)++posixTime :: DataDeclaration AbstractTy+posixTime = mkSimpleNewtype "POSIXTime" (BuiltinFlat IntegerT)++interval :: DataDeclaration AbstractTy+interval =+  mkDecl $+    Decl+      "Interval"+      count1+      [ Ctor+          "Interval"+          [ tycon "LowerBound" [a],+            tycon "UpperBound" [a]+          ]+      ]+      (PlutusData ConstrData)++upperBound :: DataDeclaration AbstractTy+upperBound =+  mkDecl $+    Decl+      "UpperBound"+      count1+      [ Ctor "UpperBound" [tycon "Extended" [a], BuiltinFlat BoolT]+      ]+      (PlutusData ConstrData)++lowerBound :: DataDeclaration AbstractTy+lowerBound =+  mkDecl $+    Decl+      "LowerBound"+      count1+      [ Ctor "LowerBound" [tycon "Extended" [a], BuiltinFlat BoolT]+      ]+      (PlutusData ConstrData)++extended :: DataDeclaration AbstractTy+extended =+  mkDecl $+    Decl+      "Extended"+      count1+      [ Ctor "NegInf" [],+        Ctor "Finite" [a],+        Ctor "PosInf" []+      ]+      (PlutusData ConstrData)++-- LedgerBytes (V1)++ledgerBytes :: DataDeclaration AbstractTy+ledgerBytes = mkSimpleNewtype "LedgerBytes" (BuiltinFlat ByteStringT)++-- Value & Friends (should be V1). Also AssocMap (v1)++-- NOTE Sean 5/28: This is "magical" like List/Pair/Data due to the fact that we cannot use an opaque+--                 (because opaques do not take type parameters)+assocMap :: DataDeclaration AbstractTy+assocMap =+  mkDecl $+    Decl+      "Map"+      count2+      [Ctor "Map" [tycon "List" [tycon "Pair" [a, b]]]]+      (BuiltinStrategy InternalAssocMapStrat)++currencySymbol :: DataDeclaration AbstractTy+currencySymbol = mkSimpleNewtype "CurrencySymbol" (BuiltinFlat ByteStringT)++tokenName :: DataDeclaration AbstractTy+tokenName = mkSimpleNewtype "TokenName" (BuiltinFlat ByteStringT)++value :: DataDeclaration AbstractTy+value =+  mkSimpleNewtype+    "Value"+    ( tycon+        "Map"+        [ tycon "CurrencySymbol" [],+          tycon "Map" [tycon "TokenName" [], BuiltinFlat IntegerT]+        ]+    )++lovelace :: DataDeclaration AbstractTy+lovelace = mkSimpleNewtype "Lovelace" (BuiltinFlat IntegerT)++rational :: DataDeclaration AbstractTy+rational =+  mkDecl $+    Decl+      "Rational"+      count0+      [ Ctor "Rational" [tycon "Pair" [BuiltinFlat IntegerT, BuiltinFlat IntegerT]]+      ]+      (PlutusData NewtypeData)++-- MintValue (V3)++mintValue :: DataDeclaration AbstractTy+mintValue =+  mkDecl $+    Decl+      "MintValue"+      count0+      [ Ctor+          "UnsafeMintValue"+          [ tycon+              "Map"+              [ tycon "CurrencySymbol" [],+                tycon "Map" [tycon "TokenName" [], BuiltinFlat IntegerT]+              ]+          ]+      ]+      (PlutusData NewtypeData)++-- TxId (v3)+txId :: DataDeclaration AbstractTy+txId = mkSimpleNewtype "TxId" (BuiltinFlat ByteStringT)++-- TxOutRef (v3)+txOutRef :: DataDeclaration AbstractTy+txOutRef =+  mkDecl $+    Decl+      "TxOutRef"+      count0+      [ Ctor "TxOutRef" [tycon "TxId" [], BuiltinFlat IntegerT]+      ]+      (PlutusData ConstrData)++-- TxOut (v2)+txOut :: DataDeclaration AbstractTy+txOut =+  mkDecl $+    Decl+      "TxOut"+      count0+      [ Ctor+          "TxOut"+          [ tycon "Address" [],+            tycon "Value" [],+            tycon "OutputDatum" [],+            tycon "Maybe" [tycon "ScriptHash" []]+          ]+      ]+      (PlutusData ConstrData)++-- OutputDatum (v2)+outputDatum :: DataDeclaration AbstractTy+outputDatum =+  mkDecl $+    Decl+      "OutputDatum"+      count0+      [ Ctor "NoOutputDatum" [],+        Ctor "OutputDatumHash" [tycon "DatumHash" []],+        Ctor "OutputDatum" [tycon "OutputDatum" []]+      ]+      (PlutusData ConstrData)++-- txInInfo (V3)+txInInfo :: DataDeclaration AbstractTy+txInInfo =+  mkDecl $+    Decl+      "TxInInfo"+      count0+      [ Ctor+          "TxInInfo"+          [ tycon "TxOutRef" [],+            tycon "TxOut" []+          ]+      ]+      (PlutusData ConstrData)++-- DRepCredential (v3)+dRepCredential :: DataDeclaration AbstractTy+dRepCredential = mkSimpleNewtype "DRepCredential" (tycon "Credential" [])++-- DRep (v3)+dRep :: DataDeclaration AbstractTy+dRep =+  mkDecl $+    Decl+      "DRep"+      count0+      [ Ctor "DRep" [tycon "DRepCredential" []],+        Ctor "DRepAlwaysAbstain" [],+        Ctor "DRepAlwaysNoConfidence" []+      ]+      (PlutusData ConstrData)++-- delegatee (v3)+delegatee :: DataDeclaration AbstractTy+delegatee =+  mkDecl $+    Decl+      "Delegatee"+      count0+      [ Ctor "DelegStake" [tycon "PubKeyHash" []],+        Ctor "DelegVote" [tycon "DRep" []],+        Ctor "DelegStakeVoke" [tycon "PubKeyHash" [], tycon "DRep" []]+      ]+      (PlutusData ConstrData)++coldCommitteeCredential :: DataDeclaration AbstractTy+coldCommitteeCredential = mkSimpleNewtype "ColdCommitteeCredential" (tycon "Credential" [])++hotCommitteeCredential :: DataDeclaration AbstractTy+hotCommitteeCredential = mkSimpleNewtype "HotCommitteeCredential" (tycon "Credential" [])++-- txCert (v3)+txCert :: DataDeclaration AbstractTy+txCert =+  mkDecl $+    Decl+      "TxCert"+      count0+      [ Ctor "TxCertRegStaking" [tycon "Credential" [], tycon "Maybe" [tycon "Lovelace" []]],+        Ctor "TxCertUnRegStaking" [tycon "Credential" [], tycon "Maybe" [tycon "Lovelace" []]],+        Ctor "TxCertDelegStaking" [tycon "Credential" [], tycon "Delegatee" []],+        Ctor "TxCertRegDeleg" [tycon "Credential" [], tycon "Delegatee" [], tycon "Lovelace" []],+        Ctor "TxCertRegDRep" [tycon "DRepCredential" [], tycon "Lovelace" []],+        Ctor "TxCertUpdateDRep" [tycon "DRepCredential" []],+        Ctor "TxCertUnRegDRep" [tycon "DRepCredential" [], tycon "Lovelace" []],+        Ctor "TxCertPoolRegister" [tycon "PubKeyHash" [], tycon "PubKeyHash" []],+        Ctor "TxCertPoolRetire" [tycon "PubKeyHash" [], BuiltinFlat IntegerT],+        Ctor "TxCertAuthHotCommittee" [tycon "ColdCommitteeCredential" [], tycon "HotCommitteeCredential" []],+        Ctor "TxCertResignColdCommittee" [tycon "ColdCommitteeCredential" []]+      ]+      (PlutusData ConstrData)++-- voter (v3)+voter :: DataDeclaration AbstractTy+voter =+  mkDecl $+    Decl+      "Voter"+      count0+      [ Ctor "CommitteeVoter" [tycon "HotCommitteeCredential" []],+        Ctor "DRepVoter" [tycon "DRepCredential" []],+        Ctor "StakePoolVoter" [tycon "PubKeyHash" []]+      ]+      (PlutusData ConstrData)++-- vote (v3)+vote :: DataDeclaration AbstractTy+vote =+  mkDecl $+    Decl+      "Vote"+      count0+      [ Ctor "VoteNo" [],+        Ctor "VoteYes" [],+        Ctor "Abstain" []+      ]+      (PlutusData ConstrData)++-- GovernanceActionID (v3)+governanceActionId :: DataDeclaration AbstractTy+governanceActionId =+  mkDecl $+    Decl+      "GovernanceActionId"+      count0+      [ Ctor+          "GovernanceActionId"+          [ tycon "TxId" [],+            BuiltinFlat IntegerT+          ]+      ]+      (PlutusData ConstrData)++-- Committee (v3)+committee :: DataDeclaration AbstractTy+committee =+  mkDecl $+    Decl+      "Committee"+      count0+      [ Ctor+          "Committee"+          [ tycon "Map" [tycon "ColdCommitteeCredential" [], BuiltinFlat IntegerT],+            tycon "Rational" []+          ]+      ]+      (PlutusData ConstrData)++-- constitution (V3)+constitution :: DataDeclaration AbstractTy+constitution = mkSimpleNewtype "Constitution" (tycon "Maybe" [tycon "ScriptHash" []])++-- changedParameters (V3)+changedParameters :: DataDeclaration AbstractTy+changedParameters = mkSimpleNewtype "ChangedParameters" (tycon "Data" [])++-- ProtocolVersion (V3)+protocolVersion :: DataDeclaration AbstractTy+protocolVersion =+  mkDecl $+    Decl+      "ProtocolVersion"+      count0+      [ Ctor "ProtocolVersion" [BuiltinFlat IntegerT, BuiltinFlat IntegerT]+      ]+      (PlutusData ConstrData)++-- GovernanceAction (v3)+governanceAction :: DataDeclaration AbstractTy+governanceAction =+  mkDecl $+    Decl+      "GovernanceAction"+      count0+      [ Ctor+          "ParameterChange"+          [ tycon "Maybe" [tycon "GovernanceActionId" []],+            tycon "ChangedParameters" [],+            tycon "Maybe" [tycon "ScriptHash" []]+          ],+        Ctor+          "HardForkInitiation"+          [ tycon "Maybe" [tycon "GovernanceActionId" []],+            tycon "ProtocolVersion" []+          ],+        Ctor+          "TreasuryWithdrawals"+          [ tycon "Map" [tycon "Credential" [], tycon "Lovelace" []],+            tycon "Maybe" [tycon "ScriptHash" []]+          ],+        Ctor "NoConfidence" [tycon "Maybe" [tycon "GovernanceActionId" []]],+        Ctor+          "UpdateCommittee"+          [ tycon "Maybe" [tycon "GovernanceActionId" []],+            tycon "List" [tycon "ColdCommitteeCredential" []],+            tycon "Map" [tycon "ColdCommitteeCredential" [], BuiltinFlat IntegerT],+            tycon "Rational" []+          ],+        Ctor "NewConstitution" [tycon "Maybe" [tycon "GovernanceActionId" []], tycon "Constitution" []],+        Ctor "InfoAction" []+      ]+      (PlutusData ConstrData)++-- ProposalProcedure (v3)+proposalProcedure :: DataDeclaration AbstractTy+proposalProcedure =+  mkDecl $+    Decl+      "ProposalProcedure"+      count0+      [ Ctor+          "ProposalProcedure"+          [ tycon "Lovelace" [],+            tycon "Credential" [],+            tycon "GovernanceAction" []+          ]+      ]+      (PlutusData ConstrData)++-- scriptPurpose (v3)+scriptPurpose :: DataDeclaration AbstractTy+scriptPurpose =+  mkDecl $+    Decl+      "ScriptPurpose"+      count0+      [ Ctor "Minting" [tycon "CurrencySymbol" []],+        Ctor "Spending" [tycon "TxOutRef" []],+        Ctor "Rewarding" [tycon "Credential" []],+        Ctor "Certifying" [BuiltinFlat IntegerT, tycon "TxCert" []],+        Ctor "Voting" [tycon "Voter" []],+        Ctor "Proposing" [BuiltinFlat IntegerT, tycon "ProposalProcedure" []]+      ]+      (PlutusData ConstrData)++-- ScriptInfo (V3)+scriptInfo :: DataDeclaration AbstractTy+scriptInfo =+  mkDecl $+    Decl+      "ScriptInfo"+      count0+      [ Ctor "MintingScript" [tycon "CurrencySymbol" []],+        Ctor "SpendingScript" [tycon "TxOutRef" [], tycon "Maybe" [tycon "Datum" []]],+        Ctor "RewardingScript" [tycon "Credential" []],+        Ctor "CertifyingScript" [BuiltinFlat IntegerT, tycon "TxCert" []],+        Ctor "VotingScript" [tycon "Voter" []],+        Ctor "ProposingScript" [BuiltinFlat IntegerT, tycon "ProposalProcedure" []]+      ]+      (PlutusData ConstrData)++-- This is a TypeSyn, so not a declaration, but it's *annoying* to type the ValT version out+posixTimeRange :: ValT AbstractTy+posixTimeRange = tycon "Interval" [tycon "POSIXTime" []]++-- txInfo (v3)+txInfo :: DataDeclaration AbstractTy+txInfo =+  mkDecl $+    Decl+      "TxInfo"+      count0+      [ Ctor+          "TxInfo"+          [ tycon "List" [tycon "TxInInfo" []],+            tycon "List" [tycon "TxInInfo" []],+            tycon "List" [tycon "TxOut" []],+            tycon "Lovelace" [],+            tycon "MintValue" [],+            tycon "List" [tycon "TxCert" []],+            tycon "Map" [tycon "Credential" [], tycon "Lovelace" []],+            posixTimeRange,+            tycon "List" [tycon "PubKeyHash" []],+            tycon "Map" [tycon "ScriptPurpose" [], tycon "Redeemer" []],+            tycon "Map" [tycon "DatumHash" [], tycon "Datum" []],+            tycon "TxId" [],+            tycon "Map" [tycon "Voter" [], tycon "Map" [tycon "GovernanceActionId" [], tycon "Vote" []]],+            tycon "List" [tycon "ProposalProcedure" []],+            tycon "Maybe" [tycon "Lovelace" []],+            tycon "Maybe" [tycon "Lovelace" []]+          ]+      ]+      (PlutusData ConstrData)++-- scriptContext (v3)+scriptContext :: DataDeclaration AbstractTy+scriptContext =+  mkDecl $+    Decl+      "ScriptContext"+      count0+      [ Ctor+          "ScriptContext"+          [ tycon "TxInfo" [],+            tycon "Redeemer" [],+            tycon "ScriptInfo" []+          ]+      ]+      (PlutusData ConstrData)++-- Helpers++-- Variants of DataDeclaration and Constructor that use Lists to avoid a slew of Vector.fromList cluttering up the module++data DeclBuilder = Decl TyName (Count "tyvar") [CtorBuilder] DataEncoding++data CtorBuilder = Ctor ConstructorName [ValT AbstractTy]++mkDecl :: DeclBuilder -> DataDeclaration AbstractTy+mkDecl (Decl tn cnt ctors enc) = DataDeclaration tn cnt (Vector.fromList . fmap mkCtor $ ctors) enc+  where+    mkCtor :: CtorBuilder -> Constructor AbstractTy+    mkCtor (Ctor cnm fields) = Constructor cnm (Vector.fromList fields)++tycon :: TyName -> [ValT AbstractTy] -> ValT AbstractTy+tycon tn vals = Datatype tn (Vector.fromList vals)++{- This is shorthand for a non-polymorphic newtype (i.e. a single ctor / arg type with a newtype strategy) where+   the name of the constructor is the same as the name of the type.++   This is a *very* common case and this seems useful to save extra typing.++-}+mkSimpleNewtype :: TyName -> ValT AbstractTy -> DataDeclaration AbstractTy+mkSimpleNewtype tn val = mkDecl $ Decl tn count0 [Ctor (coerce tn) [val]] (PlutusData NewtypeData)++-- obviously should not export these, solely exist to improve readability of declarations.+-- Since everything here is data-encodeable the DB index *should* always be Z & I don't think anything uses more than+-- 2 tyvars++a :: ValT AbstractTy+a = Abstraction (BoundAt Z ix0)++b :: ValT AbstractTy+b = Abstraction (BoundAt Z ix1)++-- For tests, much easier to define this here w/ the helpers++-- Note (Koz, 11/07/25): Same as for `list`.++-- | A datatype equivalent to+--+-- @data Tree a = Bin (Tree a) (Tree a) | Tip a@+--+-- @since 1.1.0+tree :: DataDeclaration AbstractTy+tree =+  mkDecl $+    Decl+      "Tree"+      count1+      [ Ctor "Bin" [tycon "Tree" [a], tycon "Tree" [a]],+        Ctor "Tip" [a]+      ]+      (PlutusData ConstrData)++-- | A datatype equivalent to+--+-- @data WeirderList a = Uncons (Maybe (a, WeirderList a))@+--+-- @since 1.1.0+weirderList :: DataDeclaration AbstractTy+weirderList =+  mkDecl $+    Decl+      "WeirderList"+      count1+      [ Ctor "Uncons" [tycon "Maybe" [tycon "Pair" [a, tycon "WeirderList" [a]]]]+      ]+      (PlutusData ConstrData)

@@ -0,0 +1,169 @@+module Covenant.Internal.PrettyPrint+  ( ScopeBoundary (..),+    PrettyContext (..),+    PrettyM,+    runPrettyM,+    bindVars,+    mkForall,+    lookupAbstraction,+  )+where++import Control.Monad.Reader+  ( MonadReader (local),+    Reader,+    asks,+    runReader,+  )+import Covenant.Index+  ( Count,+    Index,+    intCount,+    intIndex,+  )+import Data.Kind (Type)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Vector (Vector)+import Data.Vector qualified as Vector+import GHC.Exts (fromListN)+import Optics.At ()+import Optics.Core+  ( A_Lens,+    LabelOptic (labelOptic),+    ix,+    lens,+    over,+    preview,+    review,+    set,+    view,+    (%),+  )+import Prettyprinter+  ( Doc,+    Pretty (pretty),+    hsep,+    (<+>),+  )++newtype ScopeBoundary = ScopeBoundary Int+  deriving (Show, Eq, Ord, Num, Real, Enum, Integral) via Int++-- Keeping the field names for clarity even if we don't use them+data PrettyContext (ann :: Type)+  = PrettyContext+  { _boundIdents :: Map ScopeBoundary (Vector (Doc ann)),+    _currentScope :: ScopeBoundary,+    _varStream :: [Doc ann]+  }++instance+  (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) =>+  LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(PrettyContext x _ _) -> x)+      (\(PrettyContext _ y z) x -> PrettyContext x y z)++instance+  (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) =>+  LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(PrettyContext _ x _) -> x)+      (\(PrettyContext x _ z) y -> PrettyContext x y z)++instance+  (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) =>+  LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(PrettyContext _ _ x) -> x)+      (\(PrettyContext x y _) z -> PrettyContext x y z)++-- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail+newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a)+  deriving+    ( Functor,+      Applicative,+      Monad,+      MonadReader (PrettyContext ann)+    )+    via (Reader (PrettyContext ann))++runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a+runPrettyM (PrettyM ma) = runReader ma (PrettyContext mempty 0 infiniteVars)+  where+    -- Lazily generated infinite list of variables. Will start with a, b, c...+    -- and cycle around to a1, b2, c3 etc.+    -- We could do something more sophisticated but this should work.+    infiniteVars :: [Doc ann]+    infiniteVars =+      let aToZ = ['a' .. 'z']+          intStrings = ("" <$ aToZ) <> map (show @Integer) [0 ..]+       in zipWith (\x xs -> pretty (x : xs)) aToZ intStrings++bindVars ::+  forall (ann :: Type) (a :: Type).+  Count "tyvar" ->+  (Vector (Doc ann) -> PrettyM ann a) ->+  PrettyM ann a+bindVars count' act+  | count == 0 = crossBoundary (act Vector.empty)+  | otherwise = crossBoundary $ do+      here <- asks (view #currentScope)+      withFreshVarNames count $ \newBoundVars ->+        local (over #boundIdents (Map.insert here newBoundVars)) (act newBoundVars)+  where+    -- Increment the current scope+    crossBoundary :: PrettyM ann a -> PrettyM ann a+    crossBoundary = local (over #currentScope (+ 1))+    count :: Int+    count = review intCount count'++mkForall ::+  forall (ann :: Type).+  Vector (Doc ann) ->+  Doc ann ->+  Doc ann+mkForall tvars funTyBody =+  if Vector.null tvars+    then funTyBody+    else "forall" <+> hsep (Vector.toList tvars) <> "." <+> funTyBody++lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann)+lookupAbstraction offset argIndex = do+  let scopeOffset = ScopeBoundary offset+  let argIndex' = review intIndex argIndex+  here <- asks (view #currentScope)+  asks (preview (#boundIdents % ix (here + scopeOffset) % ix argIndex')) >>= \case+    Nothing ->+      -- TODO: actual error reporting+      error $+        "Internal error: The encountered a variable at arg index "+          <> show argIndex'+          <> " with true level "+          <> show scopeOffset+          <> " but could not locate the corresponding pretty form at scope level "+          <> show here+    Just res' -> pure res'++-- Helpers++-- Generate N fresh var names and use the supplied monadic function to do something with them.+withFreshVarNames ::+  forall (ann :: Type) (a :: Type).+  Int ->+  (Vector (Doc ann) -> PrettyM ann a) ->+  PrettyM ann a+withFreshVarNames n act = do+  stream <- asks (view #varStream)+  let (used, rest) = splitAt n stream+  local (set #varStream rest) . act . fromListN n $ used

@@ -3,8 +3,10 @@     RenameError (..),     runRenameM,     renameValT,+    renameDataDecl,     renameCompT,     undoRename,+    renameDatatypeInfo,   ) where @@ -26,15 +28,19 @@     gets,     modify,   )+import Covenant.Data (DatatypeInfo (DatatypeInfo)) import Covenant.DeBruijn (DeBruijn (S, Z), asInt) import Covenant.Index (Count, Index, intCount, intIndex) import Covenant.Internal.Type   ( AbstractTy (BoundAt),     CompT (CompT),     CompTBody (CompTBody),+    Constructor (Constructor),+    DataDeclaration (DataDeclaration, OpaqueData),     Renamed (Rigid, Unifiable, Wildcard),-    ValT (Abstraction, BuiltinFlat, ThunkT),+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),   )+import Data.Bitraversable (Bitraversable (bitraverse)) import Data.Coerce (coerce) import Data.Kind (Type) import Data.Tuple.Optics (_1)@@ -107,7 +113,7 @@  -- | Ways in which the renamer can fail. ----- @since 1.0.0+-- @since 1.1.0 data RenameError   = -- | An attempt to reference an abstraction in a scope where this     -- abstraction doesn't exist. First field is the true level, second is@@ -115,18 +121,6 @@     --     -- @since 1.0.0     InvalidAbstractionReference Int (Index "tyvar")-  | -- | A value type specifies an abstraction that never gets used-    -- anywhere. For example, the type @forall a b . [a]@ has @b@-    -- irrelevant.-    ---    -- @since 1.0.0-    IrrelevantAbstraction-  | -- | A computation type specifies an abstraction which is not used-    -- by any argument. For example, the type @forall a b . a -> !(b -> !a)@-    -- has @b@ undetermined.-    ---    -- @since 1.0.0-    UndeterminedAbstraction   deriving stock (Eq, Show)  -- | A \'renaming monad\' which allows us to convert type representations from@@ -183,9 +177,6 @@     Vector.generateM       (NonEmpty.length xs - 1)       (\i -> coerce . renameValT $ xs NonEmpty.! i)-  -- Check that we don't overdetermine anything-  ourAbstractions <- gets (view (#tracker % to Vector.head % _1))-  unless (Vector.and ourAbstractions) (throwError UndeterminedAbstraction)   -- Check result type   renamedResult <- coerce . renameValT . NonEmpty.last $ xs   -- Roll back state@@ -201,7 +192,32 @@   Abstraction t -> Abstraction <$> renameAbstraction t   ThunkT t -> ThunkT <$> renameCompT t   BuiltinFlat t -> pure . BuiltinFlat $ t+  -- Assumes kind-checking has occurred+  Datatype tn xs -> RenameM $ do+    -- We don't step or un-step the scope here b/c a TyCon which appears as a ValT _cannot_ bind variables.+    -- This Vector here doesn't represent a function, but a product, so we there is no "return" type to treat specially (I think!)+    renamedXS <- Vector.mapM (coerce . renameValT) xs+    pure $ Datatype tn renamedXS +-- @since 1.1.0+renameDataDecl :: DataDeclaration AbstractTy -> RenameM (DataDeclaration Renamed)+renameDataDecl (OpaqueData tn manual) = pure $ OpaqueData tn manual+renameDataDecl (DataDeclaration tn cnt ctors strat) = RenameM $ do+  modify (stepUpScope cnt)+  renamedCtors <- Vector.mapM (coerce . renameCtor) ctors+  modify dropDownScope+  pure $ DataDeclaration tn cnt renamedCtors strat+  where+    renameCtor :: Constructor AbstractTy -> RenameM (Constructor Renamed)+    renameCtor (Constructor cn args) = Constructor cn <$> traverse renameValT args++renameDatatypeInfo :: DatatypeInfo AbstractTy -> Either RenameError (DatatypeInfo Renamed)+renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM $ do+  ogDecl' <- renameDataDecl ogDecl+  baseFStuff' <- traverse (bitraverse renameDataDecl renameValT) baseFStuff+  bb' <- traverse renameValT bb+  pure $ DatatypeInfo ogDecl' baseFStuff' bb'+ -- A way of 'undoing' the renaming process. This is meant to be used only after -- applications, and assumes that what is being un-renamed is the result of a -- computation.@@ -218,6 +234,7 @@       ThunkT (CompT abses (CompTBody xs)) ->         ThunkT . CompT abses . CompTBody <$> local (+ 1) (traverse go xs)       BuiltinFlat t' -> pure . BuiltinFlat $ t'+      Datatype tn args -> Datatype tn <$> traverse go args  -- Helpers @@ -231,8 +248,8 @@  renameAbstraction :: AbstractTy -> RenameM Renamed renameAbstraction (BoundAt scope index) = RenameM $ do-  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - asInt scope)-  scopeInfo <- gets (\x -> view #tracker x Vector.!? asInt scope)+  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - review asInt scope)+  scopeInfo <- gets (\x -> view #tracker x Vector.!? review asInt scope)   let asIntIx = review intIndex index   case scopeInfo of     -- This variable is bound in a scope that encloses the renaming scope. Thus,@@ -274,4 +291,4 @@ -- we've seen this variable. noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState noteUsed scope index =-  set (#tracker % ix (asInt scope) % _1 % ix (review intIndex index)) True+  set (#tracker % ix (review asInt scope) % _1 % ix (review intIndex index)) True

@@ -0,0 +1,100 @@+module Covenant.Internal.Strategy+  ( DataEncoding (..),+    PlutusDataStrategy (..),+    InternalStrategy (..),+    PlutusDataConstructor (..),+  )+where++-- | 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+    )++-- 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.++-- | Specifics of how a @Data@-encoded datatype is represented.+--+-- @since 1.1.0+data PlutusDataStrategy+  = -- | The type is encoded as an @Integer@, corresponding to which \'arm\'+    -- of the datatype we want.+    --+    -- @since 1.1.0+    EnumData+  | -- | The type is encoded as a list of its fields.+    --+    -- @since 1.1.0+    ProductListData+  | -- | The type is encoded using @Constr@.+    --+    -- @since 1.1.0+    ConstrData+  | -- | The type \'borrows\' the encoding of whatever it wraps.+    --+    -- @since 1.1.0+    NewtypeData+  deriving stock+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq,+      -- | @since 1.1.0+      Ord+    )++-- | The constructors of the onchain @Data@ type. Needed for other definitions+-- here.+--+-- @since 1.1.0+data PlutusDataConstructor+  = PlutusI+  | PlutusB+  | PlutusConstr+  | PlutusList+  | PlutusMap+  deriving stock+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq,+      -- | @since 1.1.0+      Ord+    )++data InternalStrategy+  = InternalListStrat+  | InternalPairStrat+  | InternalDataStrat+  | InternalAssocMapStrat+  | -- This exists solely so I can get a 'DataEncoding' out of an opaque, it's not really used+    InternalOpaqueStrat+  deriving stock+    ( Show,+      Eq,+      Ord+    )

@@ -19,10 +19,11 @@ import Covenant.Constant (AConstant) import Covenant.DeBruijn (DeBruijn) import Covenant.Index (Index)+import Covenant.Internal.KindCheck (EncodingArgErr) import Covenant.Internal.Rename (RenameError) import Covenant.Internal.Type (AbstractTy, CompT, ValT) import Covenant.Internal.Unification (TypeAppError)-import Covenant.Prim (OneArgFunc, ThreeArgFunc, TwoArgFunc)+import Covenant.Prim (OneArgFunc, SixArgFunc, ThreeArgFunc, TwoArgFunc) import Data.Kind (Type) import Data.Vector (Vector) import Data.Word (Word64)@@ -117,6 +118,10 @@     --     -- @since 1.0.0     WrongReturnType (ValT AbstractTy) (ValT AbstractTy)+  | -- @since 1.1.0++    -- | Wraps an encoding argument mismatch error from KindCheck+    EncodingError (EncodingArgErr AbstractTy)   deriving stock     ( -- | @since 1.0.0       Eq,@@ -150,7 +155,8 @@ typeId ::   forall (m :: Type -> Type).   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>-  Id -> m ASGNodeType+  Id ->+  m ASGNodeType typeId i = do   lookedUp <- lookupRef i   case lookedUp of@@ -199,7 +205,8 @@ typeRef ::   forall (m :: Type -> Type).   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>-  Ref -> m ASGNodeType+  Ref ->+  m ASGNodeType typeRef = \case   AnArg arg -> pure . ValNodeType . typeArg $ arg   AnId i -> typeId i@@ -211,6 +218,7 @@   = Builtin1Internal OneArgFunc   | Builtin2Internal TwoArgFunc   | Builtin3Internal ThreeArgFunc+  | Builtin6Internal SixArgFunc   | LamInternal Id   | ForceInternal Ref   | ReturnInternal Ref

@@ -1,57 +1,99 @@+{-# LANGUAGE OverloadedLists #-}+{-# LANGUAGE PatternSynonyms #-}+ module Covenant.Internal.Type   ( AbstractTy (..),     Renamed (..),     CompT (..),     CompTBody (..),+    DataDeclaration (..),+    Constructor (..),+    ConstructorName (..),     ValT (..),     BuiltinFlatT (..),+    TyName (..),+    runConstructorName,+    abstraction,+    thunkT,+    builtinFlat,+    datatype,+    checkStrategy,+    naturalBaseFunctor,+    negativeBaseFunctor,+    byteStringBaseFunctor,   ) where -import Control.Monad.Reader-  ( MonadReader (local),-    Reader,-    asks,-    runReader,-  )-import Covenant.DeBruijn (DeBruijn)+import Covenant.DeBruijn (DeBruijn (Z)) import Covenant.Index   ( Count,     Index,+    count1,     intCount,     intIndex,+    ix0,   )+import Covenant.Internal.PrettyPrint+  ( PrettyM,+    bindVars,+    lookupAbstraction,+    mkForall,+    runPrettyM,+  )+import Covenant.Internal.Strategy+  ( DataEncoding+      ( BuiltinStrategy,+        PlutusData,+        SOP+      ),+    InternalStrategy+      ( InternalAssocMapStrat,+        InternalDataStrat,+        InternalListStrat,+        InternalOpaqueStrat,+        InternalPairStrat+      ),+    PlutusDataConstructor,+    PlutusDataStrategy+      ( ConstrData,+        EnumData,+        NewtypeData,+        ProductListData+      ),+  )+import Covenant.Util (pattern ConsV, pattern NilV) import Data.Functor.Classes (Eq1 (liftEq)) import Data.Kind (Type)-import Data.Map.Strict (Map)-import Data.Map.Strict qualified as Map+import Data.Set (Set)+import Data.String (IsString)+import Data.Text (Text) import Data.Vector (Vector) import Data.Vector qualified as Vector import Data.Vector.NonEmpty (NonEmptyVector) import Data.Vector.NonEmpty qualified as NonEmpty import Data.Word (Word64)-import GHC.Exts (fromListN)-import Optics.At () import Optics.Core-  ( A_Lens,+  ( A_Fold,+    A_Lens,     LabelOptic (labelOptic),-    ix,+    Prism',+    folding,     lens,-    over,     preview,+    prism,     review,-    set,-    view,-    (%),   ) import Prettyprinter   ( Doc,     Pretty (pretty),     hsep,+    indent,     parens,+    vcat,     viaShow,     (<+>),   )+import Test.QuickCheck.Instances.Text ()  -- | A type abstraction, using a combination of a DeBruijn index (to indicate -- which scope it refers to) and a positional index (to indicate which bound@@ -150,6 +192,23 @@ instance Pretty (CompT Renamed) where   pretty = runPrettyM . prettyCompTWithContext +-- | The name of a data type. This refers specifically to non-\'flat\' types+-- either provided by the ledger, or defined by the user.+--+-- @since 1.1.0+newtype TyName = TyName Text+  deriving+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq,+      -- | @since 1.1.0+      Ord,+      -- | @since 1.1.0+      IsString+    )+    via Text+ -- | A value type, with abstractions indicated by the type argument. In pretty -- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or -- 'Renamed' (after renaming).@@ -162,6 +221,9 @@     ThunkT (CompT a)   | -- | A builtin type without any nesting.     BuiltinFlat BuiltinFlatT+  | -- | An applied type constructor for a non-\'flat\' data type.+    -- | @since 1.1.0+    Datatype TyName (Vector (ValT a))   deriving stock     ( -- | @since 1.0.0       Eq,@@ -184,9 +246,36 @@     BuiltinFlat t1 -> \case       BuiltinFlat t2 -> t1 == t2       _ -> False+    Datatype tn1 args1 -> \case+      Datatype tn2 args2 -> tn1 == tn2 && liftEq (liftEq f) args1 args2+      _ -> False +-- | /Do not/ use this instance to write other 'Pretty' instances. It exists to+-- ensure readable tests without having to expose a lot of internals.+--+-- @since 1.0.0+instance Pretty (ValT Renamed) where+  pretty = runPrettyM . prettyValTWithContext++abstraction :: forall (a :: Type). Prism' (ValT a) a+abstraction = prism Abstraction (\case (Abstraction a) -> Right a; other -> Left other)++thunkT :: forall (a :: Type). Prism' (ValT a) (CompT a)+thunkT = prism ThunkT (\case (ThunkT compT) -> Right compT; other -> Left other)++builtinFlat :: forall (a :: Type). Prism' (ValT a) BuiltinFlatT+builtinFlat = prism BuiltinFlat (\case (BuiltinFlat bi) -> Right bi; other -> Left other)++datatype :: forall (a :: Type). Prism' (ValT a) (TyName, Vector (ValT a))+datatype =+  prism+    (uncurry Datatype)+    (\case (Datatype tn args) -> Right (tn, args); other -> Left other)+ -- | All builtin types that are \'flat\': that is, do not have other types -- \'nested inside them\'.+--+-- @since 1.0.0 data BuiltinFlatT   = UnitT   | BoolT@@ -205,151 +294,217 @@       Show     ) --- Helpers+-- | The name of a data type constructor.+--+-- @since 1.1.0+newtype ConstructorName = ConstructorName Text+  deriving+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq,+      -- | @since 1.1.0+      Ord,+      -- | @since 1.1.0+      IsString+    )+    via Text -newtype ScopeBoundary = ScopeBoundary Int-  deriving (Show, Eq, Ord, Num) via Int+-- | @since 1.1.0+runConstructorName :: ConstructorName -> Text+runConstructorName (ConstructorName nm) = nm --- Keeping the field names for clarity even if we don't use them-data PrettyContext (ann :: Type)-  = PrettyContext-  { _boundIdents :: Map ScopeBoundary (Vector (Doc ann)),-    _currentScope :: ScopeBoundary,-    _varStream :: [Doc ann]-  }+-- | A single constructor of a data type, with its fields.+--+-- @since 1.1.0+data Constructor (a :: Type)+  = Constructor ConstructorName (Vector (ValT a))+  deriving stock+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq+    ) +-- | @since 1.1.0+instance Eq1 Constructor where+  liftEq f (Constructor nm args) (Constructor nm' args') =+    nm == nm' && liftEq (liftEq f) args args'++-- | @since 1.1.0 instance-  (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) =>-  LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b+  (k ~ A_Lens, a ~ ConstructorName, b ~ ConstructorName) =>+  LabelOptic "constructorName" k (Constructor c) (Constructor c) a b   where   {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(Constructor n _) -> n) (\(Constructor _ args) n -> Constructor n args)++-- | @since 1.1.0+instance+  (k ~ A_Lens, a ~ Vector (ValT c), b ~ Vector (ValT c)) =>+  LabelOptic "constructorArgs" k (Constructor c) (Constructor c) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(Constructor _ args) -> args) (\(Constructor n _) args -> Constructor n args)++-- | Description of a non-\'flat\' type, together with how it is encoded.+--+-- @since 1.1.0+data DataDeclaration a+  = -- | A \'standard\' datatype, with its constructors and encoding.+    --+    -- @since 1.1.0+    DataDeclaration TyName (Count "tyvar") (Vector (Constructor a)) DataEncoding+  | -- | An \'opaque\' datatype, with the permitted constructors of+    -- @Data@ we can use to build and tear it down.+    --+    -- @since 1.1.0+    OpaqueData TyName (Set PlutusDataConstructor)+  deriving stock+    ( -- | @since 1.1.0+      Show,+      -- | @since 1.1.0+      Eq+    )++-- | @since 1.1.0+instance Pretty (DataDeclaration Renamed) where+  pretty = runPrettyM . prettyDataDeclWithContext++-- | @since 1.1.0+instance+  (k ~ A_Lens, a ~ TyName, b ~ TyName) =>+  LabelOptic "datatypeName" k (DataDeclaration c) (DataDeclaration c) a b+  where+  {-# INLINEABLE labelOptic #-}   labelOptic =     lens-      (\(PrettyContext x _ _) -> x)-      (\(PrettyContext _ y z) x -> PrettyContext x y z)+      (\case OpaqueData tn _ -> tn; DataDeclaration tn _ _ _ -> tn)+      (\decl tn -> case decl of OpaqueData _ x -> OpaqueData tn x; DataDeclaration _ x y z -> DataDeclaration tn x y z) +-- | @since 1.1.0 instance-  (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) =>-  LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b+  (k ~ A_Fold, a ~ Count "tyvar", b ~ Count "tyvar") =>+  LabelOptic "datatypeBinders" k (DataDeclaration c) (DataDeclaration c) a b   where   {-# INLINEABLE labelOptic #-}   labelOptic =-    lens-      (\(PrettyContext _ x _) -> x)-      (\(PrettyContext x _ z) y -> PrettyContext x y z)+    folding $ \case+      DataDeclaration _ cnt _ _ -> Just cnt+      _ -> Nothing +-- | @since 1.1.0 instance-  (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) =>-  LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b+  (k ~ A_Fold, a ~ Vector (Constructor c), b ~ Vector (Constructor c)) =>+  LabelOptic "datatypeConstructors" k (DataDeclaration c) (DataDeclaration c) a b   where   {-# INLINEABLE labelOptic #-}   labelOptic =+    folding $ \case+      DataDeclaration _ _ ctors _ -> Just ctors+      _ -> Nothing++-- | @since 1.1.0+instance+  (k ~ A_Lens, a ~ DataEncoding, b ~ DataEncoding) =>+  LabelOptic "datatypeEncoding" k (DataDeclaration c) (DataDeclaration c) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =     lens-      (\(PrettyContext _ _ x) -> x)-      (\(PrettyContext x y _) z -> PrettyContext x y z)+      (\case OpaqueData {} -> BuiltinStrategy InternalOpaqueStrat; DataDeclaration _ _ _ enc -> enc)+      (\decl enc -> case decl of OpaqueData tn x -> OpaqueData tn x; DataDeclaration tn x y _ -> DataDeclaration tn x y enc) --- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail-newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a)-  deriving-    ( Functor,-      Applicative,-      Monad,-      MonadReader (PrettyContext ann)-    )-    via (Reader (PrettyContext ann))+checkStrategy :: forall (a :: Type). DataDeclaration a -> Bool+checkStrategy = \case+  OpaqueData _ _ -> True+  DataDeclaration tn _ ctors strat -> case strat of+    SOP -> True+    BuiltinStrategy internalStrat -> case internalStrat of+      InternalListStrat -> tn == "List"+      InternalPairStrat -> tn == "Pair"+      InternalDataStrat -> tn == "Data"+      InternalAssocMapStrat -> tn == "Map"+      InternalOpaqueStrat -> False+    PlutusData plutusStrat -> case plutusStrat of+      ConstrData -> True+      EnumData -> all (\(Constructor _ args) -> null args) ctors+      ProductListData -> length ctors == 1+      NewtypeData -> case ctors of+        ConsV x NilV -> case preview #constructorArgs x of+          Just (ConsV _ NilV) -> True+          _ -> False+        _ -> False -runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a-runPrettyM (PrettyM ma) = runReader ma (PrettyContext mempty 0 infiniteVars)+naturalBaseFunctor :: DataDeclaration AbstractTy+naturalBaseFunctor = DataDeclaration "Natural_F" count1 constrs SOP   where-    -- Lazily generated infinite list of variables. Will start with a, b, c...-    -- and cycle around to a1, b2, c3 etc.-    -- We could do something more sophisticated but this should work.-    infiniteVars :: [Doc ann]-    infiniteVars =-      let aToZ = ['a' .. 'z']-          intStrings = ("" <$ aToZ) <> map (show @Integer) [0 ..]-       in zipWith (\x xs -> pretty (x : xs)) aToZ intStrings+    constrs :: Vector (Constructor AbstractTy)+    constrs =+      [ Constructor "ZeroNat_F" [],+        Constructor "SuccNat_F" [Abstraction . BoundAt Z $ ix0]+      ] +negativeBaseFunctor :: DataDeclaration AbstractTy+negativeBaseFunctor = DataDeclaration "Negative_F" count1 constrs SOP+  where+    constrs :: Vector (Constructor AbstractTy)+    constrs =+      [ Constructor "ZeroNeg_F" [],+        Constructor "PredNeg_F" [Abstraction . BoundAt Z $ ix0]+      ]++byteStringBaseFunctor :: DataDeclaration AbstractTy+byteStringBaseFunctor = DataDeclaration "ByteString_F" count1 constrs SOP+  where+    constrs :: Vector (Constructor AbstractTy)+    constrs =+      [ Constructor "EmptyByteString_F" [],+        Constructor "ConsByteString_F" [BuiltinFlat IntegerT, Abstraction . BoundAt Z $ ix0]+      ]++-- Helpers+ prettyCompTWithContext :: forall (ann :: Type). CompT Renamed -> PrettyM ann (Doc ann) prettyCompTWithContext (CompT count (CompTBody funArgs))-  | review intCount count == 0 = prettyFunTy funArgs+  | review intCount count == 0 = prettyFunTy' funArgs   | otherwise = bindVars count $ \newVars -> do-      funTy <- prettyFunTy funArgs+      funTy <- prettyFunTy' funArgs       pure $ mkForall newVars funTy -prettyFunTy ::+prettyFunTy' ::   forall (ann :: Type).   NonEmptyVector (ValT Renamed) ->   PrettyM ann (Doc ann)-prettyFunTy args = case NonEmpty.uncons args of-  (arg, rest) -> Vector.foldl' go (("!" <>) <$> prettyArg arg) rest-  where-    go ::-      PrettyM ann (Doc ann) ->-      ValT Renamed ->-      PrettyM ann (Doc ann)-    go acc t = (\x y -> x <+> "->" <+> y) <$> prettyArg t <*> acc-    prettyArg :: ValT Renamed -> PrettyM ann (Doc ann)-    prettyArg vt =-      let prettyVT = prettyValTWithContext vt-       in if isSimpleValT vt-            then prettyVT-            else parens <$> prettyVT--bindVars ::-  forall (ann :: Type) (a :: Type).-  Count "tyvar" ->-  (Vector (Doc ann) -> PrettyM ann a) ->-  PrettyM ann a-bindVars count' act-  | count == 0 = crossBoundary (act Vector.empty)-  | otherwise = crossBoundary $ do-      here <- asks (view #currentScope)-      withFreshVarNames count $ \newBoundVars ->-        local (over #boundIdents (Map.insert here newBoundVars)) (act newBoundVars)-  where-    -- Increment the current scope-    crossBoundary :: PrettyM ann a -> PrettyM ann a-    crossBoundary = local (over #currentScope (+ 1))-    count :: Int-    count = review intCount count'--mkForall ::-  forall (ann :: Type).-  Vector (Doc ann) ->-  Doc ann ->-  Doc ann-mkForall tvars funTyBody =-  if Vector.null tvars-    then funTyBody-    else "forall" <+> hsep (Vector.toList tvars) <> "." <+> funTyBody---- I.e. can we omit parens and get something unambiguous? This might be overly aggressive w/ parens but that's OK-isSimpleValT :: forall (a :: Type). ValT a -> Bool-isSimpleValT = \case-  ThunkT thunk -> isSimpleCompT thunk-  _ -> True-  where-    isSimpleCompT :: CompT a -> Bool-    isSimpleCompT (CompT count (CompTBody args)) =-      review intCount count == 0 && NonEmpty.length args == 1+prettyFunTy' args = case NonEmpty.unsnoc args of+  (rest, resTy) -> do+    resTy' <- ("!" <>) <$> prettyValTWithContext resTy+    case Vector.uncons rest of+      Nothing -> pure resTy'+      Just (firstArg, otherArgs) -> do+        prettyArg1 <- prettyValTWithContext firstArg+        argsWithoutResult <- Vector.foldM (\acc x -> (\z -> acc <+> "->" <+> z) <$> prettyValTWithContext x) prettyArg1 otherArgs+        pure . parens $ argsWithoutResult <+> "->" <+> resTy'  prettyValTWithContext :: forall (ann :: Type). ValT Renamed -> PrettyM ann (Doc ann) prettyValTWithContext = \case   Abstraction abstr -> prettyRenamedWithContext abstr   ThunkT compT -> prettyCompTWithContext compT   BuiltinFlat biFlat -> pure $ viaShow biFlat+  Datatype (TyName tn) args -> do+    args' <- traverse prettyValTWithContext args+    let tn' = pretty tn+    case Vector.toList args' of+      [] -> pure tn'+      argsList -> pure . parens $ tn' <+> hsep argsList --- Generate N fresh var names and use the supplied monadic function to do something with them.-withFreshVarNames ::-  forall (ann :: Type) (a :: Type).-  Int ->-  (Vector (Doc ann) -> PrettyM ann a) ->-  PrettyM ann a-withFreshVarNames n act = do-  stream <- asks (view #varStream)-  let (used, rest) = splitAt n stream-  local (set #varStream rest) . act . fromListN n $ used+prettyCtorWithContext :: forall (ann :: Type). Constructor Renamed -> PrettyM ann (Doc ann)+prettyCtorWithContext (Constructor ctorNm ctorArgs)+  | Vector.null ctorArgs = pure $ pretty (runConstructorName ctorNm)+  | otherwise = do+      let ctorNm' = pretty (runConstructorName ctorNm)+      args' <- Vector.toList <$> traverse prettyValTWithContext ctorArgs+      pure $ ctorNm' <+> hsep args'  prettyRenamedWithContext :: forall (ann :: Type). Renamed -> PrettyM ann (Doc ann) prettyRenamedWithContext = \case@@ -357,19 +512,21 @@   Unifiable i -> lookupAbstraction 0 i   Wildcard w64 offset i -> pure $ pretty offset <> "_" <> viaShow w64 <> "#" <> pretty (review intIndex i) -lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann)-lookupAbstraction offset argIndex = do-  let scopeOffset = ScopeBoundary offset-  let argIndex' = review intIndex argIndex-  here <- asks (view #currentScope)-  asks (preview (#boundIdents % ix (here + scopeOffset) % ix argIndex')) >>= \case-    Nothing ->-      -- TODO: actual error reporting-      error $-        "Internal error: The encountered a variable at arg index "-          <> show argIndex'-          <> " with true level "-          <> show scopeOffset-          <> " but could not locate the corresponding pretty form at scope level "-          <> show here-    Just res' -> pure res'+prettyDataDeclWithContext :: forall (ann :: Type). DataDeclaration Renamed -> PrettyM ann (Doc ann)+prettyDataDeclWithContext (OpaqueData (TyName tn) _) = pure . pretty $ tn+prettyDataDeclWithContext (DataDeclaration (TyName tn) numVars ctors _) = bindVars numVars $ \boundVars -> do+  let tn' = pretty tn+  ctors' <- traverse prettyCtorWithContext ctors+  let prettyCtors = indent 2 . vcat . prefix "| " . Vector.toList $ ctors'+  if Vector.null ctors+    then pure $ "data" <+> tn' <+> hsep (Vector.toList boundVars)+    else pure $ "data" <+> tn' <+> hsep (Vector.toList boundVars) <+> "=" <+> prettyCtors+  where+    -- I don't think there's a library fn that does this? This is for the `|` in a sum type.+    prefix :: Doc ann -> [Doc ann] -> [Doc ann]+    prefix _ [] = []+    prefix _ [x] = [x]+    prefix sep (x : xs) = x : goPrefix xs+      where+        goPrefix [] = []+        goPrefix (y : ys) = (sep <> y) : goPrefix ys

@@ -3,22 +3,29 @@ module Covenant.Internal.Unification   ( TypeAppError (..),     checkApp,+    runUnifyM,+    UnifyM,   ) where -import Control.Monad (foldM, unless)+import Control.Monad (foldM, unless, when) import Data.Ord (comparing) #if __GLASGOW_HASKELL__==908 import Data.Foldable (foldl') #endif-import Control.Monad.Except (catchError, throwError)+import Control.Monad.Except (MonadError, catchError, throwError)+import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask)+import Covenant.Data (DatatypeInfo) import Covenant.Index (Index, intCount, intIndex)+import Covenant.Internal.Rename (RenameError, renameDatatypeInfo) import Covenant.Internal.Type-  ( BuiltinFlatT,+  ( AbstractTy,+    BuiltinFlatT,     CompT (CompT),     CompTBody (CompTBody),     Renamed (Rigid, Unifiable, Wildcard),-    ValT (Abstraction, BuiltinFlat, ThunkT),+    TyName,+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),   ) import Data.Kind (Type) import Data.Map (Map)@@ -27,13 +34,17 @@ import Data.Maybe (fromJust, mapMaybe) import Data.Set (Set) import Data.Set qualified as Set+import Data.Text (Text) import Data.Vector (Vector) import Data.Vector qualified as Vector+import Data.Vector.NonEmpty (NonEmptyVector) import Data.Vector.NonEmpty qualified as NonEmpty import Data.Word (Word64)-import Optics.Core (preview)+import Optics.Core (ix, preview, view) --- | @since 1.0.0+-- | Possible errors resulting from applications of arguments to functions.+--+-- @since 1.0.0 data TypeAppError   = -- | The final type after all arguments are applied is @forall a . a@.     LeakingUnifiable (Index "tyvar")@@ -42,10 +53,29 @@   | -- | We were given too many arguments.     ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed)))   | -- | We weren't given enough arguments.-    InsufficientArgs (CompT Renamed)+    --+    -- @since 1.1.0+    InsufficientArgs Int (CompT Renamed) [Maybe (ValT Renamed)]   | -- | The expected type (first field) and actual type (second field) do not     -- unify.     DoesNotUnify (ValT Renamed) (ValT Renamed)+  | -- | No datatype info associated with requested TyName+    --+    -- @since 1.1.0+    NoDatatypeInfo TyName+  | -- | No BB form. The only datatypes which should lack one are those isomorphic to `Void`.+    --+    -- @since 1.1.0+    NoBBForm TyName+  | -- | Datatype renaming failed.+    --+    -- @since 1.1.0+    DatatypeInfoRenameFailed TyName RenameError+  | -- | Something happened that definitely should not have. For right now, this means: The BB form of a datatype isn't a thunk+    --   (but it might be useful to keep this around as a catchall for things that really shouldn't happen).+    --+    -- @since 1.1.0+    ImpossibleHappened Text   deriving stock     ( -- | @since 1.0.0       Eq,@@ -53,17 +83,68 @@       Show     ) --- | @since 1.0.0-checkApp :: CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed)-checkApp f@(CompT _ (CompTBody xs)) =+{- This will probably only get used directly in testing and we'll use capabilities w/ the class everywhere else? -}+newtype UnifyM a = UnifyM (ReaderT (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError) a)+  deriving+    ( -- | @since 1.1.0+      Functor,+      Applicative,+      Monad,+      MonadReader (Map TyName (DatatypeInfo AbstractTy)),+      MonadError TypeAppError+    )+    via (ReaderT (Map TyName (DatatypeInfo AbstractTy)) (Either TypeAppError))++runUnifyM :: Map TyName (DatatypeInfo AbstractTy) -> UnifyM a -> Either TypeAppError a+runUnifyM tyDict (UnifyM act) = runReaderT act tyDict++lookupDatatypeInfo ::+  TyName ->+  UnifyM (DatatypeInfo Renamed)+lookupDatatypeInfo tn =+  ask >>= \tyDict -> case preview (ix tn) tyDict of+    Nothing -> throwError $ NoDatatypeInfo tn+    Just dti -> either (throwError . DatatypeInfoRenameFailed tn) pure $ renameDatatypeInfo dti++lookupBBForm :: TyName -> UnifyM (ValT Renamed)+lookupBBForm tn =+  lookupDatatypeInfo tn >>= \dti -> case view #bbForm dti of+    Nothing -> throwError $ NoBBForm tn+    Just bbForm -> pure bbForm++-- | 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.+--+-- @since 1.0.0+checkApp ::+  Map TyName (DatatypeInfo AbstractTy) ->+  CompT Renamed ->+  [Maybe (ValT Renamed)] ->+  Either TypeAppError (ValT Renamed)+checkApp tyDict f args = runUnifyM tyDict $ checkApp' f args++checkApp' ::+  CompT Renamed ->+  [Maybe (ValT Renamed)] ->+  UnifyM (ValT Renamed)+checkApp' f@(CompT _ (CompTBody xs)) ys = do   let (curr, rest) = NonEmpty.uncons xs-   in go curr (Vector.toList rest)+      numArgsExpected = NonEmpty.length xs - 1+      numArgsActual = length ys+  when (numArgsActual < numArgsExpected) $+    throwError $+      InsufficientArgs numArgsActual f ys+  when (numArgsExpected > numArgsActual) $+    throwError $+      ExcessArgs f (Vector.fromList ys)+  go curr (Vector.toList rest) ys   where     go ::       ValT Renamed ->       [ValT Renamed] ->       [Maybe (ValT Renamed)] ->-      Either TypeAppError (ValT Renamed)+      UnifyM (ValT Renamed)     go currParam restParams args = case restParams of       [] -> case args of         -- If we got here, currParam is the resulting type after all@@ -71,7 +152,7 @@         [] -> fixUp currParam         _ -> throwError . ExcessArgs f . Vector.fromList $ args       _ -> case args of-        [] -> throwError . InsufficientArgs $ f+        [] -> throwError $ InsufficientArgs (length args) f args         (currArg : restArgs) -> do           newRestParams <- case currArg of             -- An error argument unifies with anything, as it's effectively@@ -82,7 +163,7 @@               subs <- catchError (unify currParam currArg') (promoteUnificationError currParam currArg')               pure . Map.foldlWithKey' applySub restParams $ subs           case newRestParams of-            [] -> throwError . InsufficientArgs $ f+            [] -> throwError $ InsufficientArgs (length args) f args             (currParam' : restParams') -> go currParam' restParams' restArgs  -- Helpers@@ -109,6 +190,7 @@   ThunkT (CompT abstractions (CompTBody xs)) ->     ThunkT . CompT abstractions . CompTBody . fmap (substitute index toSub) $ xs   BuiltinFlat t -> BuiltinFlat t+  Datatype tn args -> Datatype tn $ substitute index toSub <$> args  -- Because unification is inherently recursive, if we find an error deep within -- a type, the message will signify only the _part_ that fails to unify, not the@@ -117,17 +199,16 @@ -- function, which effectively allows us to rename the types reported in -- unification errors to whatever types 'wrap' them. promoteUnificationError ::-  forall (a :: Type).   ValT Renamed ->   ValT Renamed ->   TypeAppError ->-  Either TypeAppError a+  UnifyM a promoteUnificationError topLevelExpected topLevelActual =-  Left . \case+  throwError . \case     DoesNotUnify _ _ -> DoesNotUnify topLevelExpected topLevelActual     err -> err -fixUp :: ValT Renamed -> Either TypeAppError (ValT Renamed)+fixUp :: ValT Renamed -> UnifyM (ValT Renamed) fixUp = \case   -- We have a result that's effectively `forall a . a` but not an error   Abstraction (Unifiable index) -> throwError . LeakingUnifiable $ index@@ -162,11 +243,12 @@     _ -> Set.empty   BuiltinFlat _ -> Set.empty   ThunkT (CompT _ (CompTBody xs)) -> NonEmpty.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty xs+  Datatype _ args -> Vector.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty args  unify ::   ValT Renamed ->   ValT Renamed ->-  Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+  UnifyM (Map (Index "tyvar") (ValT Renamed)) unify expected actual =   catchError     ( case expected of@@ -177,15 +259,16 @@           Wildcard scopeId1 _ index1 -> expectWildcard scopeId1 index1         ThunkT t1 -> expectThunk t1         BuiltinFlat t1 -> expectFlatBuiltin t1+        Datatype tn xs -> expectDatatype tn xs     )     (promoteUnificationError expected actual)   where-    unificationError :: forall (a :: Type). Either TypeAppError a-    unificationError = Left . DoesNotUnify expected $ actual-    noSubUnify :: forall (k :: Type) (a :: Type). Either TypeAppError (Map k a)+    unificationError :: forall (a :: Type). UnifyM a+    unificationError = throwError . DoesNotUnify expected $ actual+    noSubUnify :: forall (k :: Type) (a :: Type). UnifyM (Map k a)     noSubUnify = pure Map.empty     expectRigid ::-      Int -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+      Int -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))     -- Rigids behave identically to concrete types: they can unify with     -- themselves, or any other abstraction, but nothing else. No substitutional     -- rewrites are needed.@@ -197,7 +280,7 @@       Abstraction _ -> noSubUnify       _ -> unificationError     expectWildcard ::-      Word64 -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+      Word64 -> Index "tyvar" -> UnifyM (Map (Index "tyvar") (ValT Renamed))     -- Wildcards can unify with unifiables, as well as themselves, but nothing     -- else. No substitutional rewrites are needed.     expectWildcard scopeId1 index1 = case actual of@@ -207,7 +290,7 @@           then noSubUnify           else unificationError       _ -> unificationError-    expectThunk :: CompT Renamed -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+    expectThunk :: CompT Renamed -> UnifyM (Map (Index "tyvar") (ValT Renamed))     -- Thunks unify unconditionally with wildcards or unifiables. They unify     -- conditionally with other thunks, provided that we can unify each argument     -- with its counterpart in the same position, as well as their result types,@@ -221,7 +304,7 @@           (foldM (\acc (l, r) -> unify l r >>= reconcile acc) Map.empty . NonEmpty.zip t1 $ t2)           (promoteUnificationError expected actual)       _ -> unificationError-    expectFlatBuiltin :: BuiltinFlatT -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+    expectFlatBuiltin :: BuiltinFlatT -> UnifyM (Map (Index "tyvar") (ValT Renamed))     -- 'Flat' builtins are always concrete. They can unify with themselves,     -- unifiables or wildcards, but nothing else. No substitutional rewrites are     -- needed.@@ -233,10 +316,38 @@           then noSubUnify           else unificationError       _ -> unificationError+    expectDatatype :: TyName -> Vector (ValT Renamed) -> UnifyM (Map (Index "tyvar") (ValT Renamed))+    -- Datatypes unify with wildcards or unifiables, or other "suitable" instances of the same datatype.+    -- Suitability with other datatypes is determined by converting to BB form, then concretifying+    -- 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`+    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+    concretify :: ValT Renamed -> Vector (ValT Renamed) -> UnifyM (ValT Renamed)+    concretify (ThunkT (CompT count (CompTBody fn))) args = fixUp $ ThunkT (CompT count (CompTBody newFn))+      where+        indexedArgs :: [(Index "tyvar", ValT Renamed)]+        indexedArgs = Vector.toList $ Vector.imap (\i x -> (fromJust . preview intIndex $ i, x)) args+        newFn :: NonEmptyVector (ValT Renamed)+        newFn = go indexedArgs <$> fn+        go :: [(Index "tyvar", ValT Renamed)] -> ValT Renamed -> ValT Renamed+        go subs arg = foldl' (\val (i, concrete) -> substitute i concrete val) arg subs+    concretify _ _ = throwError $ ImpossibleHappened "bbForm is not a thunk"     reconcile ::       Map (Index "tyvar") (ValT Renamed) ->       Map (Index "tyvar") (ValT Renamed) ->-      Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+      UnifyM (Map (Index "tyvar") (ValT Renamed))     -- Note (Koz, 14/04/2025): This utter soup means the following:     --     -- - If the old map and the new map don't have any overlapping assignments,@@ -248,4 +359,13 @@       Merge.mergeA         Merge.preserveMissing         Merge.preserveMissing-        (Merge.zipWithAMatched $ \_ l r -> l <$ unless (l == r) unificationError)+        (Merge.zipWithAMatched combineBindings)+    combineBindings :: Index "tyvar" -> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed)+    combineBindings _ old new =+      if old == new+        then pure old+        else case old of+          Abstraction (Unifiable _) -> pure new+          _ -> case new of+            Abstraction (Unifiable _) -> pure old+            _ -> unificationError

@@ -7,12 +7,6 @@ -- Contains definitions relating to Plutus primitive functions in Covenant -- programs. ----- = Note------ In the 1.0.0 release, we didn't include non-flat builtin types, specifically--- pairs, lists and @Data@. Thus, the primops that operate on, or produce, these--- are not currently included.--- -- @since 1.0.0 module Covenant.Prim   ( OneArgFunc (..),@@ -21,20 +15,23 @@     typeTwoArgFunc,     ThreeArgFunc (..),     typeThreeArgFunc,-    -- SixArgFunc (..),-    -- typeSixArgFunc,+    SixArgFunc (..),+    typeSixArgFunc,   ) where -import Covenant.DeBruijn (DeBruijn (Z))-import Covenant.Index (ix0)+import Covenant.DeBruijn (DeBruijn (S, Z))+import Covenant.Index (ix0, ix1) import Covenant.Type   ( AbstractTy,-    CompT (Comp0, Comp1),+    CompT (Comp0, Comp1, Comp2),     CompTBody (ReturnT, (:--:>)),-    ValT,+    ValT (ThunkT),     boolT,     byteStringT,+    dataType1T,+    dataType2T,+    dataTypeT,     g1T,     g2T,     integerT,@@ -55,10 +52,7 @@ -- to directly \'lift\' empty list constants into itself. Secondly, while these -- primitives /could/ still be used instead of direct lifts, there is never a -- reason to prefer them, as they are less efficient than embedding a constant--- directly. Thirdly, their naive typings would end up with overdetermined type--- variables - consider the typing of @MkNilData@:------ @forall a . () -> ![a]@+-- directly. -- -- For all of these reasons, we do not represent these primitives in the ASG. --@@ -70,22 +64,37 @@   | Blake2b_256   | EncodeUtf8   | DecodeUtf8-  | --  | FstPair-    --  |  SndPair-    --  | HeadList-    --  | TailList-    --  | NullList-    --  | MapData-    --  | ListData-    --  | IData-    --  | BData-    --  | UnConstrData-    --  | UnMapData-    --  | UnListData-    --  | UnIData-    --  | UnBData-    --  | SerialiseData-    BLS12_381_G1_neg+  | -- | @since 1.1.0+    FstPair+  | -- | @since 1.1.0+    SndPair+  | -- | @since 1.1.0+    HeadList+  | -- | @since 1.1.0+    TailList+  | -- | @since 1.1.0+    NullList+  | -- | @since 1.1.0+    MapData+  | -- | @since 1.1.0+    ListData+  | -- | @since 1.1.0+    IData+  | -- | @since 1.1.0+    BData+  | -- | @since 1.1.0+    UnConstrData+  | -- | @since 1.1.0+    UnMapData+  | -- | @since 1.1.0+    UnListData+  | -- | @since 1.1.0+    UnIData+  | -- | @since 1.1.0+    UnBData+  | -- | @since 1.1.0+    SerialiseData+  | BLS12_381_G1_neg   | BLS12_381_G1_compress   | BLS12_381_G1_uncompress   | BLS12_381_G2_neg@@ -119,21 +128,21 @@         Blake2b_256,         EncodeUtf8,         DecodeUtf8,-        -- FstPair,-        -- SndPair,-        -- HeadList,-        -- TailList,-        -- NullList,-        -- MapData,-        -- ListData,-        -- IData,-        -- BData,-        -- UnConstrData,-        -- UnMapData,-        -- UnListData,-        -- UnIData,-        -- UnBData,-        -- SerialiseData,+        FstPair,+        SndPair,+        HeadList,+        TailList,+        NullList,+        MapData,+        ListData,+        IData,+        BData,+        UnConstrData,+        UnMapData,+        UnListData,+        UnIData,+        UnBData,+        SerialiseData,         BLS12_381_G1_neg,         BLS12_381_G1_compress,         BLS12_381_G1_uncompress,@@ -159,6 +168,21 @@   Blake2b_256 -> hashingT   EncodeUtf8 -> Comp0 $ stringT :--:> ReturnT byteStringT   DecodeUtf8 -> Comp0 $ byteStringT :--:> ReturnT stringT+  FstPair -> Comp2 $ pairT aT bT :--:> ReturnT aT+  SndPair -> Comp2 $ pairT aT bT :--:> ReturnT bT+  HeadList -> Comp1 $ listT aT :--:> ReturnT aT+  TailList -> Comp1 $ listT aT :--:> ReturnT (listT aT)+  NullList -> Comp1 $ listT aT :--:> ReturnT boolT+  MapData -> Comp0 $ listT (pairT dataT dataT) :--:> ReturnT dataT+  ListData -> Comp0 $ listT dataT :--:> ReturnT dataT+  IData -> Comp0 $ integerT :--:> ReturnT dataT+  BData -> Comp0 $ byteStringT :--:> ReturnT dataT+  UnConstrData -> Comp0 $ dataT :--:> ReturnT (pairT integerT (listT dataT))+  UnMapData -> Comp0 $ dataT :--:> ReturnT (listT (pairT dataT dataT))+  UnListData -> Comp0 $ dataT :--:> ReturnT (listT dataT)+  UnIData -> Comp0 $ dataT :--:> ReturnT integerT+  UnBData -> Comp0 $ dataT :--:> ReturnT byteStringT+  SerialiseData -> Comp0 $ dataT :--:> ReturnT byteStringT   BLS12_381_G1_neg -> Comp0 $ g1T :--:> ReturnT g1T   BLS12_381_G1_compress -> Comp0 $ g1T :--:> ReturnT byteStringT   BLS12_381_G1_uncompress -> Comp0 $ byteStringT :--:> ReturnT g1T@@ -199,11 +223,15 @@   | EqualsString   | ChooseUnit   | Trace-  | -- | MkCons-    -- | ConstrData-    -- | EqualsData-    -- | MkPairData-    BLS12_381_G1_add+  | -- | @since 1.1.0+    MkCons+  | -- | @since 1.1.0+    ConstrData+  | -- | @since 1.1.0+    EqualsData+  | -- | @since 1.1.0+    MkPairData+  | BLS12_381_G1_add   | BLS12_381_G1_scalarMul   | BLS12_381_G1_equal   | BLS12_381_G1_hashToGroup@@ -255,10 +283,10 @@         EqualsString,         ChooseUnit,         Trace,-        -- MkCons,-        -- ConstrData,-        -- EqualsData,-        -- MkPairData,+        MkCons,+        ConstrData,+        EqualsData,+        MkPairData,         BLS12_381_G1_add,         BLS12_381_G1_scalarMul,         BLS12_381_G1_equal,@@ -300,8 +328,12 @@   LessThanEqualsByteString -> compareT byteStringT   AppendString -> combineT stringT   EqualsString -> compareT stringT-  ChooseUnit -> Comp1 $ unitT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)-  Trace -> Comp1 $ stringT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)+  ChooseUnit -> Comp1 $ unitT :--:> aT :--:> ReturnT aT+  Trace -> Comp1 $ stringT :--:> aT :--:> ReturnT aT+  MkCons -> Comp1 $ aT :--:> listT aT :--:> ReturnT (listT aT)+  ConstrData -> Comp0 $ integerT :--:> listT dataT :--:> ReturnT dataT+  EqualsData -> compareT dataT+  MkPairData -> Comp0 $ dataT :--:> dataT :--:> ReturnT (pairT dataT dataT)   BLS12_381_G1_add -> combineT g1T   BLS12_381_G1_scalarMul -> Comp0 $ integerT :--:> g1T :--:> ReturnT g1T   BLS12_381_G1_equal -> compareT g1T@@ -332,14 +364,16 @@   | VerifyEcdsaSecp256k1Signature   | VerifySchnorrSecp256k1Signature   | IfThenElse-  | -- | ChooseList-    -- | CaseList-    IntegerToByteString+  | -- | @since 1.1.0+    ChooseList+  | -- | @since 1.1.0+    CaseList+  | IntegerToByteString   | AndByteString   | OrByteString   | XorByteString-  | -- | WriteBits-    ExpModInteger+  | WriteBits+  | ExpModInteger   deriving stock     ( -- | @since 1.0.0       Eq,@@ -360,13 +394,13 @@         VerifyEcdsaSecp256k1Signature,         VerifySchnorrSecp256k1Signature,         IfThenElse,-        -- ChooseList,-        -- CaseList,+        ChooseList,+        CaseList,         IntegerToByteString,         AndByteString,         OrByteString,         XorByteString,-        -- WriteBits,+        WriteBits,         ExpModInteger       ] @@ -378,18 +412,23 @@   VerifyEd25519Signature -> signatureT   VerifyEcdsaSecp256k1Signature -> signatureT   VerifySchnorrSecp256k1Signature -> signatureT-  IfThenElse ->-    Comp1 $-      boolT-        :--:> tyvar Z ix0-        :--:> tyvar Z ix0-        :--:> ReturnT (tyvar Z ix0)+  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   AndByteString -> bitwiseT   OrByteString -> bitwiseT   XorByteString -> bitwiseT+  WriteBits ->+    Comp0 $+      byteStringT :--:> listT integerT :--:> boolT :--:> ReturnT byteStringT   ExpModInteger ->     Comp0 $       integerT@@ -412,10 +451,9 @@           :--:> byteStringT           :--:> ReturnT byteStringT -{- -- | All six-argument primitives provided by Plutus. ----- @since 1.0.0+-- @since 1.1.0 data SixArgFunc   = ChooseData   | CaseData@@ -430,8 +468,54 @@  -- | Does not shrink. ----- @since 1.0.0+-- @since 1.1.0 instance Arbitrary SixArgFunc where   {-# INLINEABLE arbitrary #-}   arbitrary = elements [ChooseData, CaseData]--}++-- | Produce the type of a six-argument primop.+--+-- @since 1.1.0+typeSixArgFunc :: SixArgFunc -> CompT AbstractTy+typeSixArgFunc = \case+  ChooseData ->+    Comp1 $+      dataT+        :--:> aT+        :--:> aT+        :--:> aT+        :--:> 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++dataT :: ValT AbstractTy+dataT = dataTypeT "Data"++listT :: ValT AbstractTy -> ValT AbstractTy+listT = dataType1T "List"++pairT :: ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy+pairT = dataType2T "Pair"++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,21 +1,124 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE PolyKinds #-}+ -- | -- Module: Covenant.Test -- Copyright: (C) MLabs 2025 -- License: Apache 2.0 -- Maintainer: koz@mlabs.city, sean@mlabs.city ----- Utilities designed to help test Covenant itself.+-- Various utilities designed to help test Covenant. --+-- = Note+--+-- This is probably not that useful to end users of Covenant, but needs to be+-- exposed so the tests can use this functionality.+-- -- @since 1.0.0 module Covenant.Test-  ( Concrete (Concrete),+  ( -- * QuickCheck data wrappers+    Concrete (Concrete),+    DataDeclFlavor (ConcreteDecl, ConcreteNestedDecl, SimpleRecursive, Poly1, Poly1PolyThunks),+    DataDeclSet (DataDeclSet),++    -- * Functions++    -- ** Lifted QuickCheck functions+    chooseInt,+    scale,++    -- ** 'DataDeclSet' functionality+    prettyDeclSet,++    -- ** Test helpers+    checkApp,+    failLeft,+    tyAppTestDatatypes,+    list,+    tree,+    weirderList,+    unsafeTyCon,++    -- ** Datatype checks+    cycleCheck,+    checkDataDecls,+    checkEncodingArgs,++    -- ** Renaming++    -- *** Types+    RenameError (..),+    RenameM,++    -- *** Introduction+    renameValT,+    renameCompT,+    renameDataDecl,++    -- *** Elimination+    runRenameM,   ) where +#if __GLASGOW_HASKELL__==908+import Data.Foldable (foldl')+#endif import Control.Applicative ((<|>))-import Covenant.Index (count0)-import Covenant.Type-  ( AbstractTy,+import Control.Monad (void)+import Control.Monad.State.Strict+  ( MonadState (get, put),+    State,+    evalState,+    gets,+    modify,+  )+import Control.Monad.Trans (MonadTrans (lift))+import Covenant.Data+  ( DatatypeInfo,+    mkDatatypeInfo,+    noPhantomTyVars,+  )+import Covenant.DeBruijn (DeBruijn (Z), asInt)+import Covenant.Index+  ( Count,+    count0,+    count1,+    count2,+    intCount,+    intIndex,+    ix0,+    ix1,+  )+import Covenant.Internal.KindCheck+  ( checkDataDecls,+    checkEncodingArgs,+    cycleCheck,+  )+import Covenant.Internal.Ledger+  ( CtorBuilder (Ctor),+    DeclBuilder (Decl),+    list,+    maybeT,+    mkDecl,+    pair,+    tree,+    weirderList,+  )+import Covenant.Internal.PrettyPrint (ScopeBoundary)+import Covenant.Internal.Rename+  ( RenameError (InvalidAbstractionReference),+    RenameM,+    renameCompT,+    renameDataDecl,+    renameValT,+    runRenameM,+  )+import Covenant.Internal.Strategy+  ( DataEncoding (PlutusData, SOP),+    PlutusDataStrategy (ConstrData),+  )+import Covenant.Internal.Type+  ( AbstractTy (BoundAt),     BuiltinFlatT       ( BLS12_381_G1_ElementT,         BLS12_381_G2_ElementT,@@ -26,21 +129,61 @@         StringT,         UnitT       ),-    CompT (Comp0, CompN),+    Constructor (Constructor),+    ConstructorName (ConstructorName),+    DataDeclaration (DataDeclaration, OpaqueData),+    TyName (TyName),+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+    runConstructorName,+  )+import Covenant.Internal.Unification (checkApp)+import Covenant.Type+  ( CompT (Comp0, CompN),     CompTBody (ArgsAndResult),-    ValT (Abstraction, BuiltinFlat, ThunkT),   )+import Covenant.Util (prettyStr) import Data.Coerce (coerce)+import Data.Kind (Type)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as M+import Data.Maybe (fromJust, mapMaybe)+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Text (Text)+import Data.Text qualified as T+import Data.Vector (Vector) import Data.Vector qualified as Vector+import GHC.Exts (fromListN)+import GHC.Word (Word32)+import Optics.Core+  ( A_Lens,+    LabelOptic (labelOptic),+    folded,+    lens,+    over,+    preview,+    review,+    set,+    toListOf,+    view,+    (%),+  ) import Test.QuickCheck   ( Arbitrary (arbitrary, shrink),+    Arbitrary1 (liftArbitrary, liftShrink),     Gen,     elements,-    liftArbitrary,-    oneof,+    frequency,     sized,+    suchThat,+    vectorOf,   )+import Test.QuickCheck qualified as QC (chooseInt)+import Test.QuickCheck.GenT (GenT, MonadGen)+import Test.QuickCheck.GenT qualified as GT+import Test.QuickCheck.Instances.Containers () import Test.QuickCheck.Instances.Vector ()+import Test.Tasty.HUnit (assertFailure)  -- | Wrapper for 'ValT' to provide an 'Arbitrary' instance to generate only -- value types without any type variables.@@ -77,16 +220,16 @@                   BLS12_381_MlResultT                 ]         | otherwise =-            oneof-              [ pure . BuiltinFlat $ UnitT,-                pure . BuiltinFlat $ BoolT,-                pure . BuiltinFlat $ IntegerT,-                pure . BuiltinFlat $ StringT,-                pure . BuiltinFlat $ ByteStringT,-                pure . BuiltinFlat $ BLS12_381_G1_ElementT,-                pure . BuiltinFlat $ BLS12_381_G2_ElementT,-                pure . BuiltinFlat $ BLS12_381_MlResultT,-                ThunkT . Comp0 <$> (ArgsAndResult <$> liftArbitrary (go (size `quot` 4)) <*> go (size `quot` 4))+            frequency+              [ (10, pure . BuiltinFlat $ UnitT),+                (10, pure . BuiltinFlat $ BoolT),+                (10, pure . BuiltinFlat $ IntegerT),+                (10, pure . BuiltinFlat $ StringT),+                (10, pure . BuiltinFlat $ ByteStringT),+                (10, pure . BuiltinFlat $ BLS12_381_G1_ElementT),+                (10, pure . BuiltinFlat $ BLS12_381_G2_ElementT),+                (10, pure . BuiltinFlat $ BLS12_381_MlResultT),+                (2, ThunkT . Comp0 <$> (ArgsAndResult <$> liftArbitrary (go (size `quot` 4)) <*> go (size `quot` 4)))               ]   {-# INLINEABLE shrink #-}   shrink (Concrete v) =@@ -102,3 +245,614 @@           pure (ArgsAndResult args' result) <|> pure (ArgsAndResult args result')       -- Can't shrink this       BuiltinFlat _ -> []+      Datatype tn args ->+        Datatype tn <$> do+          let argsList = Vector.toList args+          (fmap (Vector.fromList . coerce) . shrink . fmap Concrete) argsList++-- | A \'description type\' designed for use with 'DataDeclSet' to describe what+-- kind of types it contains.+--+-- @since 1.1.0+data DataDeclFlavor+  = -- | All constructor arguments are concrete and the declaration is monomorphic.+    --+    -- @since 1.1.0+    ConcreteDecl+  | -- | As 'ConcreteDecl', but can re-use already generated concrete declarations+    -- in the context to make nested types.+    --+    -- @since 1.1.0+    ConcreteNestedDecl+  | -- | Recursive, monomorphic type (such as @data IntList = End | More Int IntList@).+    --+    -- @since 1.1.0+    SimpleRecursive+  | -- | Polymorphic types in one variable, which may or may not be recursive.+    --+    -- @since 1.1.0+    Poly1+  | -- | As 'Poly1', but may have further polymorphism via thunks.+    --+    -- @since 1.1.0+    Poly1PolyThunks++-- | Helper type to generate datatype definitions. Specifically, this stores+-- already-generated datatype declarations for our (re)use when generating.+--+-- @since 1.1.0+newtype DataDeclSet (flavor :: DataDeclFlavor) = DataDeclSet [DataDeclaration AbstractTy]++-- @since 1.1.0+instance Arbitrary (DataDeclSet 'ConcreteDecl) where+  arbitrary = coerce $ genDataList genConcreteDataDecl+  shrink = coerce . shrinkDataDecls . coerce++-- @since 1.1.0+instance Arbitrary (DataDeclSet 'ConcreteNestedDecl) where+  arbitrary = coerce $ genDataList genNestedConcrete+  shrink = coerce . shrinkDataDecls . coerce++-- @since 1.1.0+instance Arbitrary (DataDeclSet 'SimpleRecursive) where+  arbitrary = coerce $ genDataList genArbitraryRecursive+  shrink = coerce . shrinkDataDecls . coerce++-- @since 1.1.0+instance Arbitrary (DataDeclSet 'Poly1) where+  arbitrary = coerce $ genDataList genPolymorphic1Decl+  shrink = coerce . shrinkDataDecls . coerce++instance Arbitrary (DataDeclSet 'Poly1PolyThunks) where+  arbitrary = coerce . runDataGenM $ do+    -- If we don't have this we can't generate ctor args of the sort we want here.+    -- I *think* we're very unlikely to get 10 unsuitable decls out of this+    void $ GT.vectorOf 10 genPolymorphic1Decl+    void $ GT.listOf genNonConcreteDecl+    decls <- M.elems <$> gets (view #decls) -- simpler to just pluck them from the monadic context+    pure $ filter noPhantomTyVars decls -- TODO/FIXME: We shouldn't have to filter here, better to catch things earlier+  shrink = coerce . shrinkDataDecls . coerce++-- | Prettyprinter for 'DataDeclSet'.+--+-- @since 1.1.0+prettyDeclSet :: forall (a :: DataDeclFlavor). DataDeclSet a -> String+prettyDeclSet (DataDeclSet decls) =+  concatMap (\x -> (prettyStr . unsafeRename . renameDataDecl $ x) <> "\n\n") decls++-- | The same as 'QC.chooseInt', but lifted to work in any 'MonadGen'.+--+-- @since 1.1.0+chooseInt ::+  forall (m :: Type -> Type).+  (MonadGen m) => (Int, Int) -> m Int+chooseInt bounds = GT.liftGen $ QC.chooseInt bounds++-- | The same as 'QC.scale', but lifted to work in any 'MonadGen'.+--+-- @since 1.1.0+scale ::+  forall (m :: Type -> Type) (a :: Type).+  (MonadGen m) => (Int -> Int) -> m a -> m a+scale f g = GT.sized (\n -> GT.resize (f n) g)++-- | If the argument is a 'Right', pass the assertion; otherwise, fail the+-- assertion.+--+-- @since 1.1.0+failLeft ::+  forall (a :: Type) (b :: Type).+  (Show a) =>+  Either a b ->+  IO b+failLeft = either (assertFailure . show) pure++-- | Small collection of datatypes needed to test type application logic.+--+-- @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+  where+    unsafeMkDatatypeInfo d = case mkDatatypeInfo d of+      Left err -> error (show err)+      Right res -> res++-- | Helper for tests to quickly construct 'Datatype's. This is unsafe, as it+-- allows construction of nonsensical renamings.+--+-- @since 1.1.0+unsafeTyCon :: TyName -> [ValT a] -> ValT a+unsafeTyCon tn args = Datatype tn (Vector.fromList args)++-- Helpers++{- The state used by our datatype generators.+-}+data DataGen = DataGen+  { -- Keeps track of decls we've already generated. Used for "nested" generators and also essential for ValT generation (when we get around to implementing it)+    _dgDecls :: Map TyName (DataDeclaration AbstractTy),+    -- All used constructor names. Have to track separately, even though the information eventually ends up in the previous field, to avoid duplicate constructors in the same type.+    _dgCtors :: Set ConstructorName,+    -- Current scope. Needed for generating polymorphic `ValT`s for arguments to constructors . (That's not implemented yet but we 100% will need this )+    _dgCurrentScope :: ScopeBoundary,+    -- NOTE: Needs to maintain the invariant that the Word32 is always >0, since we will use this to select in scope variables for polymorphic args to ctors. (Again, not implemented yet)+    _dgBoundVars :: Map ScopeBoundary Word32,+    -- We need this for recursive types. We can't lookup the arity in dgDecls if we want to recurse b/c it won't be there until we've finished generating the whole decl+    _dgArities :: Map TyName (Count "tyvar")+  }++instance+  (k ~ A_Lens, a ~ Map TyName (DataDeclaration AbstractTy), b ~ Map TyName (DataDeclaration AbstractTy)) =>+  LabelOptic "decls" k DataGen DataGen a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(DataGen a _ _ _ _) -> a) (\(DataGen _ b c d e) a -> DataGen a b c d e)++instance+  (k ~ A_Lens, a ~ Set ConstructorName, b ~ Set ConstructorName) =>+  LabelOptic "constructors" k DataGen DataGen a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(DataGen _ b _ _ _) -> b) (\(DataGen a _ c d e) b -> DataGen a b c d e)++instance+  (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) =>+  LabelOptic "currentScope" k DataGen DataGen a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(DataGen _ _ c _ _) -> c) (\(DataGen a b _ d e) c -> DataGen a b c d e)++instance+  (k ~ A_Lens, a ~ Map ScopeBoundary Word32, b ~ Map ScopeBoundary Word32) =>+  LabelOptic "boundVars" k DataGen DataGen a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(DataGen _ _ _ d _) -> d) (\(DataGen a b c _ e) d -> DataGen a b c d e)++instance+  (k ~ A_Lens, a ~ Map TyName (Count "tyvar"), b ~ Map TyName (Count "tyvar")) =>+  LabelOptic "arities" k DataGen DataGen a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens (\(DataGen _ _ _ _ e) -> e) (\(DataGen a b c d _) e -> DataGen a b c d e)++{-  Monadic stack for generating monomorphic datatype declarations. Not every generator uses every part of the state, but+    it ought to suffice for generating *any* datatype declaration we choose.++    In theory this could be a reader but it becomes super awkward to work, StateT is easier++    While we don't have any generators for polymorphic `ValT`s yet, the scope stuff will be necessary there.+-}+newtype DataGenM a = DataGenM (GenT (State DataGen) a)+  deriving newtype (Functor, Applicative, Monad)+  deriving (MonadGen) via GenT (State DataGen)++instance MonadState DataGen DataGenM where+  get = DataGenM $ lift get+  put = DataGenM . lift . put++{- N.B. We don't need this *yet* but we will need it to generate constructors which take polymorphic functions as arguments.+-}+bindVars :: Count "tyvar" -> DataGenM ()+bindVars count'+  | count == 0 = crossBoundary+  | otherwise = do+      crossBoundary+      here <- gets (view #currentScope)+      modify $ over #boundVars (M.insert here $ fromIntegral count)+  where+    count :: Int+    count = review intCount count'++    crossBoundary :: DataGenM ()+    crossBoundary = modify $ over #currentScope (+ 1)++-- performs action in the deeper scope then resets.+withBoundVars :: forall (a :: Type). Count "tyvar" -> DataGenM a -> DataGenM a+withBoundVars count act = do+  oldScope <- gets (view #currentScope)+  bindVars count+  res <- act+  modify $ set #currentScope oldScope+  pure res++runDataGenM :: forall (a :: Type). DataGenM a -> Gen a+runDataGenM (DataGenM ma) = (\x -> evalState x (DataGen M.empty Set.empty 0 M.empty M.empty)) <$> GT.runGenT ma++-- Stupid helper, saves us from forgetting to update part of the state+returnDecl :: DataDeclaration AbstractTy -> DataGenM (DataDeclaration AbstractTy)+returnDecl od@(OpaqueData tn _) = modify (over #decls (M.insert tn od)) >> pure od+returnDecl decl@(DataDeclaration tyNm arity _ _) = do+  modify $ over #decls (M.insert tyNm decl)+  logArity tyNm arity+  pure decl++{- We need this outside of `returnDecl` to construct recursive polymorphic types, i.e. types where an argument to+   a constructor is the parent type applied to the type variables bound at the start of the declaration.+-}+logArity :: TyName -> Count "tyvar" -> DataGenM ()+logArity tn cnt = modify $ over #arities (M.insert tn cnt)++newtype ConcreteDataDecl = ConcreteDataDecl (DataDeclaration AbstractTy)+  deriving (Eq) via (DataDeclaration AbstractTy)+  deriving stock (Show)++{- These should never be used in a DataGenM context, we should always use the fresh generators below-}+anyCtorName :: Gen ConstructorName+anyCtorName = ConstructorName <$> genValidCtorName+  where+    genValidCtorName :: Gen Text+    genValidCtorName = do+      let caps = ['A' .. 'Z']+          lower = ['a' .. 'z']+      nmLen <- chooseInt (1, 6) -- should be more than enough to ensure `suchThat` doesn't run into clashes all the time+      x <- elements caps+      xs <- vectorOf nmLen $ elements (caps <> lower)+      pure . T.pack $ (x : xs)++anyTyName :: Gen TyName+anyTyName = TyName . runConstructorName <$> anyCtorName++{- These ensure that we don't ever duplicate type names or constructor names. We need the DataGenM state+   to ensure that, so these should *always* be used when writing generators, and the arbitrary instances should be avoided.+-}+freshConstructorName :: DataGenM ConstructorName+freshConstructorName = do+  datatypes <- gets (M.elems . view #decls)+  let allCtorNames = Set.fromList $ toListOf (folded % #datatypeConstructors % folded % #constructorName) datatypes+  thisName <- GT.liftGen $ anyCtorName `suchThat` (`Set.notMember` allCtorNames)+  modify $ over #constructors (Set.insert thisName)+  pure thisName++freshTyName :: DataGenM TyName+freshTyName = do+  datatypes <- gets (M.elems . view #decls)+  let allDataTypeNames = Set.fromList $ toListOf (folded % #datatypeName) datatypes+  GT.liftGen $ anyTyName `suchThat` (`Set.notMember` allDataTypeNames)++newtype ConcreteConstructor = ConcreteConstructor (Constructor AbstractTy)+  deriving (Eq) via (Constructor AbstractTy)+  deriving stock (Show)++notAThunk :: Concrete -> Bool+notAThunk (Concrete valT) = case valT of+  ThunkT _ -> False+  _ -> True++genConcreteConstructor :: DataGenM ConcreteConstructor+genConcreteConstructor = ConcreteConstructor <$> go+  where+    go :: DataGenM (Constructor AbstractTy)+    go = do+      ctorNm <- freshConstructorName+      numArgs <- chooseInt (0, 5)+      args <- GT.liftGen $ Vector.replicateM numArgs (arbitrary @Concrete `suchThat` notAThunk)+      pure $ Constructor ctorNm (coerce <$> args)++genConcreteDataDecl :: DataGenM ConcreteDataDecl+genConcreteDataDecl =+  ConcreteDataDecl <$> do+    tyNm <- freshTyName+    numArgs <- chooseInt (0, 5)+    ctors <- coerce <$> Vector.replicateM numArgs genConcreteConstructor+    let decl = DataDeclaration tyNm count0 ctors SOP+    returnDecl decl++{- Concrete datatypes which may contain other concrete datatypes as constructor args. (Still no TyVars)++   For example, if you have (in the DataGen context) an already generated:++   data Foo = Foo Integer++   this can generate a datatype like:++   data Bar = Bar Foo | Baz String++   I.e. it generates datatype declarations that use previously generated datatype declarations.++   This isn't useful unless you generate a *set* (or some other collection of them) in the DataGen monad,+   since generating them one at a time will always give you the same thing as a ConcreteDataDecl.+-}+newtype NestedConcreteDataDecl = NestedConcreteDataDecl (DataDeclaration AbstractTy)+  deriving (Eq) via (DataDeclaration AbstractTy)+  deriving stock (Show)++newtype NestedConcreteCtor = NestedConcreteCtor (Constructor AbstractTy)++genNestedConcrete :: DataGenM NestedConcreteDataDecl+genNestedConcrete =+  NestedConcreteDataDecl <$> do+    tyNm <- freshTyName+    res <- GT.oneof [nullary tyNm, nonNestedConcrete tyNm, nested tyNm]+    returnDecl res+  where+    nullary :: TyName -> DataGenM (DataDeclaration AbstractTy)+    nullary tyNm = do+      ctorNm <- freshConstructorName+      pure $ DataDeclaration tyNm count0 (Vector.singleton (Constructor ctorNm Vector.empty)) SOP++    nonNestedConcrete :: TyName -> DataGenM (DataDeclaration AbstractTy)+    nonNestedConcrete tyNm = do+      numCtors <- chooseInt (0, 5)+      ctors <- fmap coerce <$> Vector.replicateM numCtors genConcreteConstructor+      pure $ DataDeclaration tyNm count0 ctors SOP++    nested :: TyName -> DataGenM (DataDeclaration AbstractTy)+    nested tyNm = do+      numCtors <- chooseInt (0, 5)+      ctors <- Vector.replicateM numCtors nestedCtor+      pure $ DataDeclaration tyNm count0 (coerce <$> ctors) SOP++{- It's useful to have access to these outside of the above function because sometimes we want to mix and match+   "simpler" constructors like this with the more complex sorts we generate below.+-}+nestedCtor :: DataGenM NestedConcreteCtor+nestedCtor = do+  -- We want this: Not very much hinges on the # of args to each constructor and having finite bounds like this makes the output easier to read+  numArgs <- chooseInt (0, 5)+  args <- Vector.replicateM numArgs nestedCtorArg+  ctorNm <- freshConstructorName+  pure . coerce $ Constructor ctorNm args++nestedCtorArg :: DataGenM (ValT AbstractTy)+nestedCtorArg = do+  userTyNames <- gets (M.keys . view #decls)+  if null userTyNames+    then coerce <$> GT.liftGen (arbitrary @Concrete)+    else do+      let userTypes = (`Datatype` Vector.empty) <$> userTyNames+      GT.liftGen $ frequency [(8, elements userTypes), (2, coerce <$> arbitrary @Concrete)]++newtype RecursiveConcreteDataDecl = RecursiveConcreteDataDecl (DataDeclaration AbstractTy)+  deriving (Eq) via (DataDeclaration AbstractTy)+  deriving stock (Show)++{- Non-polymorphic recursive types, i.e. things like:++   data IntList = Empty | ConsInt Int IntList++   The general idea is that we construct a base case constructor (Nil or Empty) and then+   construct a recursive constructor. We can expand this later (e.g. to have multiple recursive constructors, or a polymorphic variant)+   but this will be enough to handle initial testing w/ the base functor / BBF stuff (and we have to ensure we have things like this to test that)+-}+genArbitraryRecursive :: DataGenM RecursiveConcreteDataDecl+genArbitraryRecursive =+  RecursiveConcreteDataDecl <$> do+    tyNm <- freshTyName+    baseCtor <- coerce <$> genConcreteConstructor -- any concrete ctor - or any ctor that doesn't contain the parent type - will suffice as a base case+    numRecCtors <- chooseInt (1, 5)+    recCtor <- GT.vectorOf numRecCtors $ genRecCtor tyNm+    returnDecl $ DataDeclaration tyNm count0 (Vector.fromList (baseCtor : recCtor)) SOP+  where+    genRecCtor :: TyName -> DataGenM (Constructor AbstractTy)+    genRecCtor tyNm = do+      ctorNm <- freshConstructorName+      let thisType = Datatype tyNm Vector.empty+      numNonRecArgs <- chooseInt (1, 5) -- need at least one to avoid "bad" types+      args <- coerce $ GT.vectorOf numNonRecArgs nestedCtorArg+      pure $ Constructor ctorNm (Vector.fromList (thisType : args))++{- Single variable polymorphic datatypes. That is, things like:++   data Foo a = Nope | Yup a++   data Snowk a = Start | More (Snowk a) a+-}+newtype Polymorphic1 = Polymorphic1 (DataDeclaration AbstractTy)+  deriving (Eq) via (DataDeclaration AbstractTy)+  deriving stock (Show)++{- Generator for single variable polymorphic datatypes, no polymorphic *functions* as arguments to the datatypes yet (that requires something different).++   When run multiple times in the monadic context, will reuse single variable declarations that are "in scope" (i.e. have already been generated and are+   known in the DataGenM state).++   TODO: Rework this to generate declarations with an arbitrary number of tyvar arguments. Doing so would be fairly simple (but isn't needed ATM)+-}+genPolymorphic1Decl :: DataGenM Polymorphic1+genPolymorphic1Decl =+  Polymorphic1+    <$> GT.suchThat+      ( do+          -- this is a hack to save avoid reworking generator logic. It should be fine cuz we're not super likely to get phantoms anyway+          tyNm <- freshTyName+          logArity tyNm count1+          numCtors <- chooseInt (1, 5)+          polyCtors <- concat <$> GT.vectorOf numCtors (genPolyCtor tyNm)+          let result = DataDeclaration tyNm count1 (Vector.fromList polyCtors) SOP+          returnDecl result+      )+      noPhantomTyVars+  where+    -- We return a single constructor UNLESS we're generating a recursive type, in which case we have to return 2 to ensure a base case+    genPolyCtor :: TyName -> DataGenM [Constructor AbstractTy]+    genPolyCtor thisTy = do+      ctorNm <- freshConstructorName+      numArgs <- chooseInt (1, 5)+      argsRaw <- GT.vectorOf numArgs polyArg+      let recCase = Datatype thisTy (Vector.singleton (Abstraction (BoundAt Z ix0)))+      if recCase `elem` argsRaw+        then do+          baseCtorNm <- freshConstructorName+          let baseCtor = Constructor baseCtorNm mempty+              recCtor = Constructor ctorNm (fromListN numArgs argsRaw)+          pure [baseCtor, recCtor]+        else pure [Constructor ctorNm (fromListN numArgs argsRaw)]+      where+        arityOne :: Count "tyvar" -> Bool+        arityOne c = c == count1++        polyArg :: DataGenM (ValT AbstractTy)+        polyArg = do+          -- first we choose a type with an arity >=1. We have to have at least one of those because we've added the parent type to the arity map+          availableArity1 <- gets (M.keys . M.filter arityOne . view #arities)+          someTyCon1 <- GT.elements availableArity1+          GT.oneof+            [ pure $ Abstraction (BoundAt Z ix0),+              pure $ Datatype someTyCon1 (Vector.singleton (Abstraction (BoundAt Z ix0))),+              GT.liftGen (coerce <$> arbitrary @Concrete)+            ]++{- Non-concrete ValTs. This needs to be scope- and context-sensitive in order to generate ThunkTs that *use* (but never *bind*) variables.++This will give us things like:++  data Foo a b = Foo Int Bool a (a -> (Int -> b) -> b -> b)+-}++newtype NonConcrete = NonConcrete (ValT AbstractTy)+  deriving+    ( -- | @since 1.0.0+      Eq+    )+    via (ValT AbstractTy)+  deriving stock+    ( -- | @since 1.0.0+      Show+    )++genNonConcrete :: DataGenM NonConcrete+genNonConcrete = NonConcrete <$> GT.sized go+  where+    -- smaller to make output more readable+    genConcrete :: DataGenM Concrete+    genConcrete = GT.liftGen $ scale (`quot` 8) (arbitrary @Concrete)++    go :: Int -> DataGenM (ValT AbstractTy)+    go = helper++    -- A polymorphic tycon applied to *either* an in-scope type variable *or* a concrete type.+    -- TODO: Conceivably this could recursively call `helper` to generate "fancier" tycon arguments+    --       but that shouldn't matter much for now & runs the risk of generating unusably large output w/o+    --       careful implementation.+    appliedTyCon :: Int -> DataGenM (ValT AbstractTy)+    appliedTyCon size = do+      currentScope <- gets (view #currentScope)+      tyConsWithArity <- M.toList <$> gets (view #arities)+      boundVars <- M.toList <$> gets (view #boundVars)+      -- We *have* to have some variables bound for this to work. We can't meaningfully return a `Maybe` here+      -- Also we have to have some Arity >= 1 TyCon around+      -- I.e. we cannot run this generator in a "fresh" DataGenM stack and have to both pre-generate+      -- some fresh polymorphic types *and* ensure that we only use this in a context where we have bound variables.+      (thisTyCon, thisArity) <- GT.elements tyConsWithArity+      let arityInt = review intCount thisArity+      let resolvedArgs = concatMap (resolveArgs currentScope) boundVars+      let choices+            | size <= 0 = [coerce <$> genConcrete]+            | otherwise = [coerce <$> genConcrete, GT.elements resolvedArgs]+      tyConArgs <- GT.vectorOf arityInt $ GT.oneof choices+      pure $ Datatype thisTyCon (Vector.fromList tyConArgs)++    resolveArgs :: ScopeBoundary -> (ScopeBoundary, Word32) -> [ValT AbstractTy]+    resolveArgs currentScope (varScope, numIndices) =+      let resolvedScope :: DeBruijn+          resolvedScope = fromJust . preview asInt . fromIntegral $ currentScope - varScope+       in mapMaybe (fmap (Abstraction . BoundAt resolvedScope) . preview intIndex) [0 .. (fromIntegral numIndices - 1)]++    helper :: Int -> DataGenM (ValT AbstractTy)+    helper size = do+      GT.oneof [coerce <$> genConcrete, appliedTyCon size]++-- NOTE: We have to call this with a "driver" which pre-generates suitable (i.e. polymorphic) data declarations, see notes in `genNonConcrete`+genNonConcreteDecl :: DataGenM (DataDeclaration AbstractTy)+genNonConcreteDecl = flip GT.suchThat noPhantomTyVars . withBoundVars count1 $ do+  -- we need to bind the vars before we're done constructing the type+  tyNm <- freshTyName+  numArgs <- chooseInt (1, 5)+  ctors <- Vector.replicateM numArgs genNonConcreteCtor+  let decl = DataDeclaration tyNm count1 ctors SOP+  returnDecl decl+  where+    genNonConcreteCtor :: DataGenM (Constructor AbstractTy)+    genNonConcreteCtor = do+      ctorNm <- freshConstructorName+      numArgs <- chooseInt (0, 5)+      args <- GT.vectorOf numArgs genNonConcrete+      pure $ Constructor ctorNm (coerce . Vector.fromList $ args)++{-+   Misc Helpers and the Arbitrary instances+-}++{- NOTE: This is supposed to be a "generic" shrinker for datatypes. It *should* return two paths:+                - One that shrinks the number of constructors+                - One that shrinks the constructors++              This is why I had to add handling for `datatype` into `Concrete`. To use `shrink` recursively+              on the structural components, we need some kind of instance to pivot off of. Since we want to avoid+              writing a generic Arbitrary instance for Constructor or DataDeclaration, this seems like the+              simplest solution.+-}+shrinkDataDecl :: DataDeclaration AbstractTy -> [DataDeclaration AbstractTy]+shrinkDataDecl OpaqueData {} = []+shrinkDataDecl (DataDeclaration nm cnt ctors strat)+  | Vector.null ctors = []+  | otherwise = filter noPhantomTyVars $ smallerNumCtors <|> smallerCtorArgs+  where+    smallerNumCtors :: [DataDeclaration AbstractTy]+    smallerNumCtors = Vector.toList $ (\cs -> DataDeclaration nm cnt cs strat) <$> Vector.init (subVectors ctors)+    smallerCtorArgs = (\cs -> DataDeclaration nm cnt cs strat) <$> shrinkCtorsNumArgs ctors++    -- need a fn which takes a single ctor and just shrinks the args+    -- this is difficult to keep track of: THIS ONE GIVES US IDENTICALLY NAMED CTORS WITH DIFFERENT ARG LISTS+    shrinkNumArgs :: Constructor AbstractTy -> [Constructor AbstractTy]+    shrinkNumArgs (Constructor ctorNm args) =+      let smallerArgs :: [Vector (ValT AbstractTy)]+          smallerArgs = coerce $ shrink (fmap Concrete args)+       in fmap (Constructor ctorNm) smallerArgs++    shrinkCtorsNumArgs :: Vector (Constructor AbstractTy) -> [Vector (Constructor AbstractTy)]+    shrinkCtorsNumArgs cs =+      let -- the inner lists exhaust the arg-deletion possibilities for each constructor+          cs' = Vector.toList $ shrinkNumArgs <$> cs+          go [] = []+          go (x : xs) = (:) <$> x <*> xs+       in Vector.fromList <$> go cs'++-- Helper, should probably exist in Data.Vector but doesn't+subVectors :: forall (a :: Type). Vector a -> Vector (Vector a)+subVectors xs = Vector.cons Vector.empty (nonEmptySubVectors xs)++nonEmptySubVectors :: forall (a :: Type). Vector a -> Vector (Vector a)+nonEmptySubVectors v = case Vector.uncons v of+  Nothing -> Vector.empty+  Just (x, xs) ->+    let f :: Vector a -> Vector (Vector a) -> Vector (Vector a)+        f ys r = ys `Vector.cons` ((x `Vector.cons` ys) `Vector.cons` r)+     in Vector.singleton x `Vector.cons` foldr f Vector.empty (nonEmptySubVectors xs)++shrinkDataDecls :: [DataDeclaration AbstractTy] -> [[DataDeclaration AbstractTy]]+shrinkDataDecls decls = liftShrink shrinkDataDecl decls <|> (shrinkDataDecl <$> decls)++genDataList :: forall (a :: Type). DataGenM a -> Gen [a]+genDataList = runDataGenM . GT.listOf++-- For convenience. Don't remove this, necessary for efficient development on future work+unsafeRename :: forall (a :: Type). RenameM a -> a+unsafeRename act = case runRenameM act of+  Left err -> error $ show err+  Right res -> res++eitherT :: DataDeclaration AbstractTy+eitherT =+  mkDecl $+    Decl+      "Either"+      count2+      [ Ctor "Left" [Abstraction (BoundAt Z ix0)],+        Ctor "Right" [Abstraction (BoundAt Z ix1)]+      ]+      (PlutusData ConstrData)++unitT :: DataDeclaration AbstractTy+unitT =+  mkDecl $+    Decl+      "Unit"+      count0+      [Ctor "Unit" []]+      (PlutusData ConstrData)++testDatatypes :: [DataDeclaration AbstractTy]+testDatatypes = [maybeT, eitherT, unitT, pair]

@@ -22,6 +22,9 @@      -- * Value types     ValT (..),+    dataTypeT,+    dataType1T,+    dataType2T,     BuiltinFlatT (..),     byteStringT,     integerT,@@ -33,22 +36,25 @@     mlResultT,     unitT, -    -- * Renaming--    -- ** Types-    RenameError (..),-    RenameM,--    -- ** Introduction-    renameValT,-    renameCompT,--    -- ** Elimination-    runRenameM,--    -- * Type application-    TypeAppError (..),-    checkApp,+    -- * Data declarations+    TyName (TyName),+    ConstructorName (ConstructorName),+    Constructor (Constructor),+    PlutusDataStrategy+      ( EnumData,+        ProductListData,+        ConstrData,+        NewtypeData+      ),+    DataEncoding (SOP, PlutusData, BuiltinStrategy),+    PlutusDataConstructor+      ( PlutusI,+        PlutusB,+        PlutusConstr,+        PlutusList,+        PlutusMap+      ),+    DataDeclaration (DataDeclaration, OpaqueData),   ) where @@ -63,16 +69,21 @@     count3,     intCount,   )-import Covenant.Internal.Rename-  ( RenameError-      ( InvalidAbstractionReference,-        IrrelevantAbstraction,-        UndeterminedAbstraction+import Covenant.Internal.Strategy+  ( DataEncoding (BuiltinStrategy, PlutusData, SOP),+    PlutusDataConstructor+      ( PlutusB,+        PlutusConstr,+        PlutusI,+        PlutusList,+        PlutusMap       ),-    RenameM,-    renameCompT,-    renameValT,-    runRenameM,+    PlutusDataStrategy+      ( ConstrData,+        EnumData,+        NewtypeData,+        ProductListData+      ),   ) import Covenant.Internal.Type   ( AbstractTy (BoundAt),@@ -88,18 +99,12 @@       ),     CompT (CompT),     CompTBody (CompTBody),+    Constructor (Constructor),+    ConstructorName (ConstructorName),+    DataDeclaration (DataDeclaration, OpaqueData),     Renamed (Rigid, Unifiable, Wildcard),-    ValT (Abstraction, BuiltinFlat, ThunkT),-  )-import Covenant.Internal.Unification-  ( TypeAppError-      ( DoesNotUnify,-        ExcessArgs,-        InsufficientArgs,-        LeakingUnifiable,-        LeakingWildcard-      ),-    checkApp,+    TyName (TyName),+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),   ) import Data.Coerce (coerce) import Data.Kind (Type)@@ -107,6 +112,7 @@ import Data.Vector qualified as Vector import Data.Vector.NonEmpty (NonEmptyVector) import Data.Vector.NonEmpty qualified as NonEmpty+import GHC.Exts (fromListN) import Optics.Core (preview)  -- | The body of a computation type that doesn't take any arguments and produces@@ -249,6 +255,24 @@ -- @since 1.0.0 tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy tyvar db = Abstraction . BoundAt db++-- | Helper for referring to compound data types with no type variables.+--+-- @since 1.1.0+dataTypeT :: forall (a :: Type). TyName -> ValT a+dataTypeT tn = Datatype tn Vector.empty++-- | Helper for referring to compound data types with one type variable.+--+-- @since 1.1.0+dataType1T :: TyName -> ValT AbstractTy -> ValT AbstractTy+dataType1T tn = Datatype tn . Vector.singleton++-- | Helper for referring to compound data types with two type variables.+--+-- @since 1.1.0+dataType2T :: TyName -> ValT AbstractTy -> ValT AbstractTy -> ValT AbstractTy+dataType2T tn v1 v2 = Datatype tn . fromListN 2 $ [v1, v2]  -- | Helper for defining the value type of builtin bytestrings. --

@@ -9,12 +9,16 @@ module Covenant.Util   ( pattern NilV,     pattern ConsV,+    prettyStr,   ) where  import Data.Kind (Type)+import Data.Text qualified as Text import Data.Vector.Generic (Vector) import Data.Vector.Generic qualified as Vector+import Prettyprinter (Pretty (pretty), defaultLayoutOptions, layoutPretty)+import Prettyprinter.Render.Text (renderStrict)  -- | A pattern matching helper for vectors (of all types), corresponding to @[]@ -- for lists. This pattern is bidirectional, which means it can be used just@@ -43,3 +47,14 @@ pattern ConsV x xs <- (Vector.uncons -> Just (x, xs))  {-# COMPLETE NilV, ConsV #-}++-- | Shorthand to transform any 'Pretty' into a 'String' using the default+-- layout.+--+-- @since 1.1.0+prettyStr :: forall (a :: Type). (Pretty a) => a -> String+prettyStr =+  Text.unpack+    . renderStrict+    . layoutPretty defaultLayoutOptions+    . pretty

@@ -65,6 +65,7 @@ import Covenant.Util (pattern ConsV, pattern NilV) import Data.Coerce (coerce) import Data.Kind (Type)+import Data.Map qualified as M import Data.Maybe (fromJust) import Data.Vector qualified as Vector import Optics.Core (preview, review)@@ -120,20 +121,20 @@ unitEmptyASG = do   let builtUp = pure ()   let expected = Left EmptyASG-  let actual = runASGBuilder builtUp+  let actual = runASGBuilder M.empty builtUp   assertEqual "" expected actual  unitSingleError :: IO () unitSingleError = do   let builtUp = err   let expected = Left TopLevelError-  let actual = runASGBuilder builtUp+  let actual = runASGBuilder M.empty builtUp   assertEqual "" expected actual  unitForceError :: IO () unitForceError = do   let builtUp = err >>= \i -> force (AnId i)-  let result = runASGBuilder builtUp+  let result = runASGBuilder M.empty builtUp   case result of     Left (TypeError _ ForceError) -> pure ()     _ -> assertFailure $ "Unexpected result: " <> show result@@ -141,7 +142,7 @@ unitThunkError :: IO () unitThunkError = do   let builtUp = err >>= thunk-  let result = runASGBuilder builtUp+  let result = runASGBuilder M.empty builtUp   case result of     Left (TypeError _ ThunkError) -> pure ()     _ -> assertFailure $ "Unexpected result: " <> show result@@ -235,7 +236,9 @@   where     mkComps ::       forall (a :: Type).-      (a -> ASGBuilder Id) -> a -> (ASGBuilder Id, ASGBuilder Id)+      (a -> ASGBuilder Id) ->+      a ->+      (ASGBuilder Id, ASGBuilder Id)     mkComps f x =       let comp = f x           forceThunkComp = do@@ -431,12 +434,12 @@ failWrongError err' = failWithCounterExample ("Unexpected error: " <> show err')  withCompilationFailure :: ASGBuilder Id -> (CovenantError -> Property) -> Property-withCompilationFailure comp cb = case runASGBuilder comp of+withCompilationFailure comp cb = case runASGBuilder M.empty comp of   Left err' -> cb err'   Right asg -> failWithCounterExample ("Unexpected success: " <> show asg)  withCompilationSuccess :: ASGBuilder Id -> (ASG -> Property) -> Property-withCompilationSuccess comp cb = case runASGBuilder comp of+withCompilationSuccess comp cb = case runASGBuilder M.empty comp of   Left err' -> failWithCounterExample ("Unexpected failure: " <> show err')   Right asg -> cb asg 

@@ -0,0 +1,46 @@+module Main (main) where++import Control.Monad.Reader (runReader)+import Covenant.Data+  ( allComponentTypes,+    hasRecursive,+    mkBaseFunctor,+  )+import Covenant.Test+  ( DataDeclFlavor (Poly1PolyThunks),+    DataDeclSet (DataDeclSet),+    prettyDeclSet,+  )+import Covenant.Type ()+import Data.Map.Strict qualified as M+import Optics.Core (view)+import Test.QuickCheck+  ( Arbitrary (arbitrary, shrink),+    Property,+  )+import Test.Tasty (defaultMain, testGroup)+import Test.Tasty.QuickCheck (forAllShrinkShow, testProperty)++main :: IO ()+main =+  defaultMain . testGroup "BaseFunctors" $+    [testProperty "All recursion is replaced in base functor transform" baseFunctorsContainNoRecursion]++baseFunctorsContainNoRecursion :: Property+baseFunctorsContainNoRecursion = forAllShrinkShow (arbitrary @(DataDeclSet 'Poly1PolyThunks)) shrink prettyDeclSet $ \(DataDeclSet decls) ->+  let declMap = M.fromList $ (\x -> (view #datatypeName x, x)) <$> decls+      baseFunctorResults = flip runReader 0 . mkBaseFunctor <$> declMap+   in M.foldlWithKey'+        ( \acc tyNm origDecl ->+            let isTyRecursive = any (\x -> runReader (hasRecursive tyNm x) 0) (allComponentTypes origDecl)+                mBaseFDecl = baseFunctorResults M.! tyNm+             in case mBaseFDecl of+                  -- if we didn't make a base functor then the original type must NOT be recursive+                  Nothing -> not isTyRecursive && acc+                  Just baseFDecl ->+                    -- If we did make a base functor, it should contain no recursion+                    let recursionInBaseF = any (\x -> runReader (hasRecursive (view #datatypeName baseFDecl) x) 0) (allComponentTypes baseFDecl)+                     in not recursionInBaseF && acc+        )+        True+        declMap

@@ -0,0 +1,156 @@+{-# LANGUAGE ViewPatterns #-}++module Main (main) where++-- import Data.Either (isRight)++import Control.Exception (throwIO)+import Control.Monad ((<=<))+import Covenant.Data+  ( mkBBF,+  )+import Covenant.DeBruijn (DeBruijn (S, Z))+import Covenant.Index (ix0, ix1)+import Covenant.Test+  ( DataDeclFlavor (Poly1PolyThunks),+    DataDeclSet (DataDeclSet),+    failLeft,+    list,+    prettyDeclSet,+    renameCompT,+    renameValT,+    runRenameM,+    tree,+    tyAppTestDatatypes,+    unsafeTyCon,+    weirderList,+  )+import Covenant.Type+  ( AbstractTy (BoundAt),+    CompT (Comp0, Comp1, Comp2),+    CompTBody (ReturnT, (:--:>)),+    ValT (Abstraction, ThunkT),+    tyvar,+  )+import Data.Map qualified as M+import Data.Maybe (catMaybes, fromJust)+import Optics.Core (view)+import Test.QuickCheck+  ( Arbitrary (arbitrary, shrink),+    Property,+  )+import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup)+import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)+import Test.Tasty.QuickCheck (QuickCheckTests, forAllShrinkShow, testProperty)++main :: IO ()+main =+  defaultMain . adjustOption moreTests . testGroup "BB" $+    [ testProperty "All BBF transformations rename properly" bbFormRenames,+      testMonotypeBB,+      bbfList,+      bbfTree,+      bbfWeirderList+    ]+  where+    -- These tests are suuuuppeeerr inefficient, it'd be ideal to run more but it'll take too long+    moreTests :: QuickCheckTests -> QuickCheckTests+    moreTests = max 500++{- This is the only reasonable property I can think of, and is ultimately more of a test of the+   "ensure there aren't any phantom type variables" than it is of the bb transform.++   Fortunately the transform itself is fairly straightforward and isn't likely to contain major errors.+-}+bbFormRenames :: Property+bbFormRenames = forAllShrinkShow (arbitrary @(DataDeclSet 'Poly1PolyThunks)) shrink prettyDeclSet $ \(DataDeclSet decls) ->+  case traverse mkBBF decls of+    Left _ -> False+    Right (catMaybes -> bbfDecls) ->+      let results =+            mapM+              ( \valT -> case runRenameM . renameValT $ valT of+                  Left err -> Left (err, valT)+                  Right res -> Right res+              )+              bbfDecls+       in case results of -- all (isRight . runRenameM . renameValT) bbfDecls+            Right {} -> True+            Left err -> error (show err)++bbfList :: TestTree+bbfList = testCase "bbfList" $ do+  let bbf = mkBBF list+  bbf' <- either (assertFailure . show) (maybe (assertFailure "no bbf for list") pure) bbf+  assertEqual "bbfList" expectedListBBF bbf'+  where+    expectedListBBF =+      ThunkT+        ( Comp2+            ( tyvar Z ix1+                :--:> ThunkT+                  ( Comp0+                      ( tyvar (S Z) ix0+                          :--:> tyvar (S Z) ix1+                          :--:> ReturnT (tyvar (S Z) ix1)+                      )+                  )+                :--:> ReturnT (tyvar Z ix1)+            )+        )++bbfTree :: TestTree+bbfTree = testCase "bbfTree" $ do+  let bbf = mkBBF tree+  bbf' <- either (assertFailure . show) (maybe (assertFailure "no bbf for tree") pure) bbf+  assertEqual "bbfList" expectedTreeBBF bbf'+  where+    expectedTreeBBF =+      ThunkT+        ( Comp2+            ( ThunkT+                ( Comp0+                    ( tyvar (S Z) ix1+                        :--:> tyvar (S Z) ix1+                        :--:> ReturnT (tyvar (S Z) ix1)+                    )+                )+                :--:> ThunkT+                  ( Comp0+                      ( tyvar (S Z) ix0+                          :--:> ReturnT (tyvar (S Z) ix1)+                      )+                  )+                :--:> ReturnT (tyvar Z ix1)+            )+        )++bbfWeirderList :: TestTree+bbfWeirderList = testCase "bbfWeirderList" $ do+  let bbf = mkBBF weirderList+  bbf' <- either (assertFailure . show) (maybe (assertFailure "no bbf for tree") pure) bbf+  assertEqual "bbfWeirderTree" expectedWeirdBBF bbf'+  where+    -- forall a r. (Maybe (a,r) -> r) -> r+    expectedWeirdBBF =+      ThunkT+        ( Comp2+            ( ThunkT+                ( Comp0+                    ( unsafeTyCon "Maybe" [unsafeTyCon "Pair" [tyvar (S Z) ix0, tyvar (S Z) ix1]]+                        :--:> ReturnT (tyvar (S Z) ix1)+                    )+                )+                :--:> ReturnT (tyvar Z ix1)+            )+        )++-- Simple datatype unification unit test. Checks whether `data Unit = Unit` has the expected BB form+testMonotypeBB :: TestTree+testMonotypeBB = testCase "unitBbf" $ do+  let expected = Comp1 $ Abstraction (BoundAt Z ix0) :--:> ReturnT (Abstraction $ BoundAt Z ix0)+  expected' <- failLeft . runRenameM . renameCompT $ expected+  actual <- case fromJust . (view #bbForm <=< M.lookup "Unit") $ tyAppTestDatatypes of+    ThunkT inner -> either (throwIO . userError . show) pure . runRenameM $ renameCompT inner+    _ -> assertFailure "BB form not a thunk!"+  assertEqual "unit bbf" expected' actual

@@ -0,0 +1,159 @@+module Main (main) where++import Covenant.ASG (defaultDatatypes)+import Covenant.Data ()+import Covenant.DeBruijn (DeBruijn (Z))+import Covenant.Index (count0, count1, ix0)+import Covenant.Test+  ( checkDataDecls,+    checkEncodingArgs,+    cycleCheck,+    unsafeTyCon,+  )+import Covenant.Type+  ( AbstractTy (BoundAt),+    BuiltinFlatT (IntegerT),+    CompT (Comp1),+    CompTBody (ReturnT, (:--:>)),+    Constructor (Constructor),+    DataDeclaration (DataDeclaration, OpaqueData),+    DataEncoding (PlutusData, SOP),+    PlutusDataStrategy (ConstrData),+    TyName,+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+    tyvar,+  )+import Data.Map.Strict qualified as M+import Data.Vector qualified as V+import Optics.Core (view)+import Test.Tasty (TestTree, defaultMain, testGroup)+import Test.Tasty.ExpectedFailure (expectFail)+import Test.Tasty.HUnit (assertFailure, testCase)++main :: IO ()+main =+  defaultMain . testGroup "DatatypeCycleCheck" $+    [ testCase "singleNonRec" $ runCycleCheck [maybee],+      testCase "singleSelfRec" $ runCycleCheck [intList],+      expectFail $ testCase "mutRecShouldFail" (runCycleCheck [mutRec1, mutRec2]),+      checkLedgerTypes,+      simpleEncodingMismatch,+      nestedThunkArg,+      noThunkArgsToSOPTyCons,+      goodSOPArg+    ]++checkLedgerTypes :: TestTree+checkLedgerTypes =+  testCase "kindCheckLedgerTypes"+    . either (assertFailure . show) pure+    . checkDataDecls+    . fmap (view #originalDecl)+    $ defaultDatatypes++encodingCheck :: String -> [DataDeclaration AbstractTy] -> ValT AbstractTy -> TestTree+encodingCheck testNm tyDict valT =+  testCase testNm $+    either (assertFailure . show) pure $+      checkEncodingArgs (view #datatypeEncoding) (mkTyDict tyDict) valT++shouldFailEncodingCheck :: String -> [DataDeclaration AbstractTy] -> ValT AbstractTy -> TestTree+shouldFailEncodingCheck tnm tyDict valT = expectFail $ encodingCheck tnm tyDict valT++simpleEncodingMismatch :: TestTree+simpleEncodingMismatch = shouldFailEncodingCheck "simpleEncodingMismatch" [maybee, intList] encodingMismatch++noThunkArgsToSOPTyCons :: TestTree+noThunkArgsToSOPTyCons =+  shouldFailEncodingCheck "no thunk args to SOP tycons (for now)" [maybeSOP] badSOPThunk++nestedThunkArg :: TestTree+nestedThunkArg = shouldFailEncodingCheck "nestedThunkArg" [maybee] badThunkArg++goodSOPArg :: TestTree+goodSOPArg = encodingCheck "goodSOP" [maybeSOP] goodSOP++mkTyDict :: forall a. [DataDeclaration a] -> M.Map TyName (DataDeclaration a)+mkTyDict = foldr (\decl acc -> M.insert (view #datatypeName decl) decl acc) M.empty++runCycleCheck :: [DataDeclaration AbstractTy] -> IO ()+runCycleCheck decls = case cycleCheck declMap of+  Nothing -> pure ()+  Just err -> assertFailure $ show err+  where+    declMap =+      foldr+        ( \dd acc -> case dd of+            OpaqueData {} -> acc+            DataDeclaration tn _ _ _ -> M.insert tn dd acc+        )+        M.empty+        decls++maybee :: DataDeclaration AbstractTy+maybee = DataDeclaration "Maybe" count1 (V.fromList ctors) (PlutusData ConstrData)+  where+    ctors =+      [ Constructor "Nothing" V.empty,+        Constructor "Just" (V.singleton (Abstraction $ BoundAt Z ix0))+      ]++maybeSOP :: DataDeclaration AbstractTy+maybeSOP = DataDeclaration "MaybeSOP" count1 (V.fromList ctors) SOP+  where+    ctors =+      [ Constructor "Nothing" V.empty,+        Constructor "Just" (V.singleton (Abstraction $ BoundAt Z ix0))+      ]++intList :: DataDeclaration AbstractTy+intList = DataDeclaration "IntList" count0 (V.fromList ctors) SOP+  where+    ctors =+      [ Constructor "Empty" V.empty,+        Constructor "More" (V.fromList intListMore)+      ]++    intListMore :: [ValT AbstractTy]+    intListMore = [BuiltinFlat IntegerT, Datatype "IntList" V.empty]++-- DATA ENCODED MAYBE, SOP ENCODED INTLIST+-- Maybe IntList+encodingMismatch :: ValT AbstractTy+encodingMismatch = Datatype "Maybe" (V.fromList [Datatype "IntList" V.empty])++-- forall a. (a -> a)+identitee :: ValT AbstractTy+identitee = ThunkT $ Comp1 (tyvar Z ix0 :--:> ReturnT (tyvar Z ix0))++-- DATA ENCODED MAYBE+-- Maybe (Maybe (forall a. a -> a))+badThunkArg :: ValT AbstractTy+badThunkArg = unsafeTyCon "Maybe" [unsafeTyCon "Maybe" [identitee]]++-- SOP ENCODED MAYBE+-- Maybe (Maybe (Maybe Integer))+goodSOP :: ValT AbstractTy+goodSOP =+  unsafeTyCon+    "MaybeSOP"+    [ unsafeTyCon "MaybeSOP" [unsafeTyCon "MaybeSOP" [BuiltinFlat IntegerT]]+    ]++-- NOTE Sean 7/2/2025: We are *temporarily* forbidding thunk arguments even to SOP encoded type constructors.+--                     This is not strictly necessary, and we can go back and change that if we have time, but it+--                     does greatly simplify getting a proof-of-concept off the ground.+-- SOP ENCODED MAYBE+-- Maybe (forall a. a -> a)+badSOPThunk :: ValT AbstractTy+badSOPThunk = unsafeTyCon "MaybeSOP" [identitee]++mutRec1 :: DataDeclaration AbstractTy+mutRec1 = DataDeclaration "MutRec1" count0 (V.fromList ctors) SOP+  where+    ctors = [Constructor "MutRec1" (V.singleton (Datatype "MutRec2" V.empty))]++mutRec2 :: DataDeclaration AbstractTy+mutRec2 = DataDeclaration "MutRec2" count0 (V.fromList ctors) SOP+  where+    ctors = [Constructor "MutRec2" (V.fromList [Datatype "MutRec1" V.empty])]

@@ -1,20 +1,56 @@+{-# LANGUAGE PatternSynonyms #-}+ module Main (main) where +import Covenant.ASG (defaultDatatypes) import Covenant.Prim-  ( typeOneArgFunc,+  ( OneArgFunc+      ( BData,+        FstPair,+        HeadList,+        IData,+        ListData,+        MapData,+        NullList,+        SerialiseData,+        SndPair,+        TailList,+        UnBData,+        UnConstrData,+        UnIData,+        UnListData,+        UnMapData+      ),+    SixArgFunc (CaseData, ChooseData),+    ThreeArgFunc (CaseList, ChooseList),+    TwoArgFunc (ConstrData, EqualsData, MkCons, MkPairData),+    typeOneArgFunc,+    typeSixArgFunc,     typeThreeArgFunc,     typeTwoArgFunc,   )+import Covenant.Test+  ( checkApp,+    renameCompT,+    renameValT,+    runRenameM,+  ) import Covenant.Type   ( AbstractTy (BoundAt),-    CompT,+    CompT (Comp0),     Renamed (Unifiable),+    ValT (Datatype, ThunkT),     arity,-    renameCompT,-    runRenameM,+    boolT,+    byteStringT,+    integerT,+    pattern ReturnT,+    pattern (:--:>),   ) import Data.Functor.Classes (liftEq)+import Data.Functor.Identity (Identity (Identity)) import Data.Kind (Type)+import Data.Vector qualified as Vector import Test.QuickCheck   ( Arbitrary (arbitrary),     Property,@@ -24,6 +60,7 @@     (===),   ) import Test.Tasty (defaultMain, testGroup)+import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) import Test.Tasty.QuickCheck (testProperty)  main :: IO ()@@ -35,15 +72,53 @@         "Arity"         [ testProperty "One-argument primops take one argument" prop1Arg,           testProperty "Two-argument primops take two arguments" prop2Args,-          testProperty "Three-argument primops take three arguments" prop3Args-          --         testProperty "Six-argument primops take six arguments" prop6Args+          testProperty "Three-argument primops take three arguments" prop3Args,+          testProperty "Six-argument primops take six arguments" prop6Args         ],       testGroup         "Renaming"         [ testProperty "One-argument primops rename correctly" prop1Rename,           testProperty "Two-argument primops rename correctly" prop2Rename,-          testProperty "Three-argument primops rename correctly" prop3Rename-          -- testProperty "Six-argument primops rename correctly" prop6Rename+          testProperty "Three-argument primops rename correctly" prop3Rename,+          testProperty "Six-argument primops rename correctly" prop6Rename+        ],+      testGroup+        "Application with data types"+        [ testGroup+            "One argument"+            [ testCase "FstPair" unitFstPair,+              testCase "SndPair" unitSndPair,+              testCase "HeadList" unitHeadList,+              testCase "TailList" unitTailList,+              testCase "NullList" unitNullList,+              testCase "MapData" unitMapData,+              testCase "ListData" unitListData,+              testCase "IData" unitIData,+              testCase "BData" unitBData,+              testCase "UnConstrData" unitUnConstrData,+              testCase "UnMapData" unitUnMapData,+              testCase "UnListData" unitUnListData,+              testCase "UnIData" unitUnIData,+              testCase "UnBData" unitUnBData,+              testCase "SerialiseData" unitSerialiseData+            ],+          testGroup+            "Two arguments"+            [ testCase "MkCons" unitMkCons,+              testCase "ConstrData" unitConstrData,+              testCase "EqualsData" unitEqualsData,+              testCase "MkPairData" unitMkPairData+            ],+          testGroup+            "Three arguments"+            [ testCase "ChooseList" unitChooseList,+              testCase "CaseList" unitCaseList+            ],+          testGroup+            "Six arguments"+            [ testCase "ChooseData" unitChooseData,+              testCase "CaseData" unitCaseData+            ]         ]     ] @@ -67,14 +142,137 @@ prop3Rename :: Property prop3Rename = mkRenameProp typeThreeArgFunc -{- prop6Args :: Property prop6Args = mkArgProp typeSixArgFunc 6  prop6Rename :: Property prop6Rename = mkRenameProp typeSixArgFunc--} +unitFstPair :: IO ()+unitFstPair = withRenamedComp (typeOneArgFunc FstPair) $ \renamedFunT ->+  withRenamedVals [Datatype "Pair" . Vector.fromList $ [integerT, byteStringT]] $+    tryAndApply integerT renamedFunT++unitSndPair :: IO ()+unitSndPair = withRenamedComp (typeOneArgFunc SndPair) $ \renamedFunT ->+  withRenamedVals [Datatype "Pair" . Vector.fromList $ [integerT, byteStringT]] $+    tryAndApply byteStringT renamedFunT++unitHeadList :: IO ()+unitHeadList = withRenamedComp (typeOneArgFunc HeadList) $ \renamedFunT ->+  withRenamedVals [Datatype "List" . Vector.singleton $ integerT] $+    tryAndApply integerT renamedFunT++unitTailList :: IO ()+unitTailList = withRenamedComp (typeOneArgFunc TailList) $ \renamedFunT ->+  withRenamedVals (Identity . Datatype "List" . Vector.singleton $ integerT) $ \(Identity renamedArgT) ->+    tryAndApply renamedArgT renamedFunT [renamedArgT]++unitNullList :: IO ()+unitNullList = withRenamedComp (typeOneArgFunc NullList) $ \renamedFunT ->+  withRenamedVals [Datatype "List" . Vector.singleton $ integerT] $+    tryAndApply boolT renamedFunT++unitMapData :: IO ()+unitMapData = withRenamedComp (typeOneArgFunc MapData) $ \renamedFunT ->+  let pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT]+   in withRenamedVals [Datatype "List" . Vector.singleton $ pairDataT] $+        tryAndApply dataT renamedFunT++unitListData :: IO ()+unitListData = withRenamedComp (typeOneArgFunc ListData) $ \renamedFunT ->+  withRenamedVals [Datatype "List" . Vector.singleton $ dataT] $+    tryAndApply dataT renamedFunT++unitIData :: IO ()+unitIData = withRenamedComp (typeOneArgFunc IData) $ \renamedFunT ->+  withRenamedVals [integerT] $ tryAndApply dataT renamedFunT++unitBData :: IO ()+unitBData = withRenamedComp (typeOneArgFunc BData) $ \renamedFunT ->+  withRenamedVals [byteStringT] $ tryAndApply dataT renamedFunT++unitUnConstrData :: IO ()+unitUnConstrData = withRenamedComp (typeOneArgFunc UnConstrData) $ \renamedFunT ->+  withRenamedVals (Identity dataT) $ \(Identity renamedArgT) ->+    let listDataT = Datatype "List" . Vector.singleton $ dataT+        returnT = Datatype "Pair" . Vector.fromList $ [integerT, listDataT]+     in tryAndApply returnT renamedFunT [renamedArgT]++unitUnMapData :: IO ()+unitUnMapData = withRenamedComp (typeOneArgFunc UnMapData) $ \renamedFunT ->+  withRenamedVals (Identity dataT) $ \(Identity renamedArgT) ->+    let pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT]+        listPairDataT = Datatype "List" . Vector.singleton $ pairDataT+     in tryAndApply listPairDataT renamedFunT [renamedArgT]++unitUnListData :: IO ()+unitUnListData = withRenamedComp (typeOneArgFunc UnListData) $ \renamedFunT ->+  withRenamedVals [dataT] $+    tryAndApply (Datatype "List" . Vector.singleton $ dataT) renamedFunT++unitUnIData :: IO ()+unitUnIData = withRenamedComp (typeOneArgFunc UnIData) $ \renamedFunT ->+  withRenamedVals [dataT] $ tryAndApply integerT renamedFunT++unitUnBData :: IO ()+unitUnBData = withRenamedComp (typeOneArgFunc UnBData) $ \renamedFunT ->+  withRenamedVals [dataT] $ tryAndApply byteStringT renamedFunT++unitSerialiseData :: IO ()+unitSerialiseData = withRenamedComp (typeOneArgFunc SerialiseData) $ \renamedFunT ->+  withRenamedVals [dataT] $ tryAndApply byteStringT renamedFunT++unitMkCons :: IO ()+unitMkCons = withRenamedComp (typeTwoArgFunc MkCons) $ \renamedFunT ->+  let listT = Datatype "List" . Vector.singleton $ integerT+   in withRenamedVals [integerT, listT] $ tryAndApply listT renamedFunT++unitConstrData :: IO ()+unitConstrData = withRenamedComp (typeTwoArgFunc ConstrData) $ \renamedFunT ->+  let listT = Datatype "List" . Vector.singleton $ dataT+   in withRenamedVals [integerT, listT] $ tryAndApply dataT renamedFunT++unitEqualsData :: IO ()+unitEqualsData = withRenamedComp (typeTwoArgFunc EqualsData) $ \renamedFunT ->+  withRenamedVals [dataT, dataT] $ tryAndApply boolT renamedFunT++unitMkPairData :: IO ()+unitMkPairData = withRenamedComp (typeTwoArgFunc MkPairData) $ \renamedFunT ->+  let pairDataT = Datatype "Pair" . Vector.fromList $ [dataT, dataT]+   in withRenamedVals [dataT, dataT] $ tryAndApply pairDataT renamedFunT++unitChooseList :: IO ()+unitChooseList = withRenamedComp (typeThreeArgFunc ChooseList) $ \renamedFunT ->+  let listT = Datatype "List" . Vector.singleton $ integerT+   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  mkArgProp ::@@ -106,3 +304,33 @@ eqRenamedVar (BoundAt _ ix) = \case   Unifiable ix' -> ix == ix'   _ -> False++withRenamedComp ::+  CompT AbstractTy ->+  (CompT Renamed -> IO ()) ->+  IO ()+withRenamedComp t f = case runRenameM . renameCompT $ t of+  Left err -> assertFailure $ "Could not rename: " <> show err+  Right t' -> f t'++withRenamedVals ::+  forall (t :: Type -> Type).+  (Traversable t) =>+  t (ValT AbstractTy) ->+  (t (ValT Renamed) -> IO ()) ->+  IO ()+withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of+  Left err -> assertFailure $ "Could not rename: " <> show err+  Right vals' -> f vals'++tryAndApply ::+  ValT Renamed ->+  CompT Renamed ->+  [ValT Renamed] ->+  IO ()+tryAndApply expected f xs = case checkApp defaultDatatypes f . fmap Just $ xs of+  Left err -> assertFailure $ "Could not apply: " <> show err+  Right res -> assertEqual "" expected res++dataT :: forall (a :: Type). ValT a+dataT = Datatype "Data" Vector.empty

@@ -8,7 +8,13 @@   ( ix0,     ix1,   )-import Covenant.Test (Concrete (Concrete))+import Covenant.Test+  ( Concrete (Concrete),+    RenameError (InvalidAbstractionReference),+    renameCompT,+    renameValT,+    runRenameM,+  ) import Covenant.Type   ( BuiltinFlatT       ( BLS12_381_G1_ElementT,@@ -20,16 +26,9 @@         StringT,         UnitT       ),-    CompT (Comp0, Comp1, Comp2),-    RenameError-      ( InvalidAbstractionReference,-        UndeterminedAbstraction-      ),+    CompT (Comp1, Comp2),     Renamed (Unifiable, Wildcard),     ValT (Abstraction, BuiltinFlat, ThunkT),-    renameCompT,-    renameValT,-    runRenameM,     tyvar,     pattern ReturnT,     pattern (:--:>),@@ -64,11 +63,6 @@       testCase "forall a b . a -> b -> !a" testConstT,       testCase "forall a . a -> !(forall b . b -> !a)" testConstT2,       testGroup-        "Overdeterminance"-        [ testCase "forall a b . a -> !(b -> !a)" testDodgyConstT,-          testCase "forall a b . a -> !a" testDodgyIdT-        ],-      testGroup         "Non-existent abstractions"         [ testCase "forall a . b -> !a" testIndexingIdT         ]@@ -138,29 +132,6 @@   let result = runRenameM . renameCompT $ constT   assertRight (assertEqual "" expected) result --- Checks that `forall a b . a -> !a` triggers the undetermined variable checker.-testDodgyIdT :: IO ()-testDodgyIdT = do-  let idT = Comp2 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)-  let result = runRenameM . renameCompT $ idT-  case result of-    Left UndeterminedAbstraction -> assertBool "" True-    Left _ -> assertBool "wrong renaming error" False-    _ -> assertBool "renaming succeeded when it should have failed" False---- Checks that `forall a b. a -> !(b -> !a)` triggers the undetermined variable checker.-testDodgyConstT :: IO ()-testDodgyConstT = do-  let constT =-        Comp2 $-          tyvar Z ix0-            :--:> ReturnT (ThunkT . Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix0))-  let result = runRenameM . renameCompT $ constT-  case result of-    Left UndeterminedAbstraction -> assertBool "" True-    Left _ -> assertBool "wrong renaming error" False-    _ -> assertBool "renaming succeeded when it should have failed" False- -- Checks that `forall a . b -> !a` triggers the variable indexing checker. testIndexingIdT :: IO () testIndexingIdT = do@@ -170,7 +141,6 @@     Left (InvalidAbstractionReference trueLevel ix) -> do       assertEqual "" trueLevel 1       assertEqual "" ix ix1-    Left _ -> assertBool "wrong renaming error" False     _ -> assertBool "renaming succeeded when it should have failed" False  -- Helpers

@@ -4,39 +4,47 @@  import Control.Applicative ((<|>)) import Control.Monad (guard)+import Covenant.ASG+  ( TypeAppError+      ( DoesNotUnify,+        ExcessArgs,+        InsufficientArgs+      ),+  ) import Covenant.DeBruijn (DeBruijn (S, Z), asInt) import Covenant.Index   ( Index,     ix0,     ix1,+    ix2,   )-import Covenant.Test (Concrete (Concrete))-import Covenant.Type-  ( AbstractTy,-    CompT (Comp0, Comp1, Comp2),-    Renamed (Rigid, Wildcard),-    TypeAppError-      ( DoesNotUnify,-        ExcessArgs,-        InsufficientArgs-      ),-    ValT-      ( Abstraction,-        ThunkT-      ),+import Covenant.Test+  ( Concrete (Concrete),     checkApp,-    integerT,+    failLeft,     renameCompT,     renameValT,     runRenameM,+    tyAppTestDatatypes,+  )+import Covenant.Type+  ( AbstractTy,+    BuiltinFlatT (BoolT, IntegerT, UnitT),+    CompT (Comp0, Comp1, Comp2, Comp3),+    Renamed (Rigid, Unifiable, Wildcard),+    ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+    integerT,     tyvar,     pattern ReturnT,     pattern (:--:>),   )+import Covenant.Util (prettyStr) import Data.Coerce (coerce) import Data.Functor.Identity (Identity (Identity)) import Data.Kind (Type)+import Data.Map qualified as M import Data.Vector qualified as Vector+import Optics.Core (review) import Test.QuickCheck   ( Gen,     Property,@@ -53,7 +61,7 @@     vectorOf,     (===),   )-import Test.Tasty (adjustOption, defaultMain, testGroup)+import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup) import Test.Tasty.HUnit (assertEqual, assertFailure, testCase) import Test.Tasty.QuickCheck (QuickCheckTests, testProperty) @@ -77,7 +85,21 @@           testProperty "concrete expected, rigid actual" propUnifyConcreteRigid,           testProperty "unifiable expected, rigid actual" propUnifyUnifiableRigid,           testProperty "rigid expected, rigid actual" propUnifyRigid,-          testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid+          testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid,+          testProperty "thunk with unifiable result" propThunkWithUnifiableResult+        ],+      testGroup+        "Datatypes"+        [ testEitherConcrete,+          polymorphicApplicationM,+          polymorphicApplicationE,+          polymorphicApplicationP,+          unifyMaybe,+          testCase "nested datatypes" unitNestedDatatypes,+          testProperty "thunk with datatype argument" propThunkWithDatatype,+          testProperty "concrete thunk with datatype argument" propConcreteThunkWithDatatype,+          testProperty "thunk with unifiable and datatype argument" propThunkUnifiableWithDatatype,+          testProperty "thunk with unifiable datatype" propThunkUnifiableDatatype         ]     ]   where@@ -100,7 +122,7 @@         [] -> discard -- should be impossible         _ : extraArgs ->           let expected = Left . ExcessArgs renamedIdT . Vector.fromList . fmap Just $ extraArgs-              actual = checkApp renamedIdT (fmap Just renamedExcessArgs)+              actual = checkApp M.empty renamedIdT (fmap Just renamedExcessArgs)            in expected === actual   where     -- Note (Koz, 14/04/2025): The default size of 100 makes it rather painful@@ -126,8 +148,8 @@ unitInsufficientArgs :: IO () unitInsufficientArgs = do   renamedIdT <- failLeft . runRenameM . renameCompT $ idT-  let expected = Left . InsufficientArgs $ renamedIdT-  let actual = checkApp renamedIdT []+  let expected = Left $ InsufficientArgs 0 renamedIdT []+  let actual = checkApp M.empty renamedIdT []   assertEqual "" expected actual  -- Try to apply `forall a . a -> !a` to a random concrete type. Result should be@@ -137,7 +159,7 @@   withRenamedComp idT $ \renamedIdT ->     withRenamedVals (Identity t) $ \(Identity t') ->       let expected = Right t'-          actual = checkApp renamedIdT [Just t']+          actual = checkApp M.empty renamedIdT [Just t']        in expected === actual  -- Try to apply `forall a b . a -> b -> !a` to two identical concrete types.@@ -147,7 +169,7 @@   withRenamedComp const2T $ \renamedConst2T ->     withRenamedVals (Identity t) $ \(Identity t') ->       let expected = Right t'-          actual = checkApp renamedConst2T [Just t', Just t']+          actual = checkApp M.empty renamedConst2T [Just t', Just t']        in expected === actual  -- Try to apply `forall a b . a -> b -> !a` to two random _different_ concrete@@ -160,7 +182,7 @@       withRenamedVals (Identity t1) $ \(Identity t1') ->         withRenamedVals (Identity t2) $ \(Identity t2') ->           let expected = Right t1'-              actual = checkApp renamedConst2T [Just t1', Just t2']+              actual = checkApp M.empty renamedConst2T [Just t1', Just t2']            in expected === actual  -- Randomly pick a concrete type `A`, then pick a type `b` which is either `A`@@ -174,14 +196,14 @@       case mtB of         Nothing ->           let expected = Right integerT-              actual = checkApp f [Just tA']+              actual = checkApp M.empty f [Just tA']            in expected === actual         Just tB ->           if tA == tB             then discard             else withRenamedVals (Identity tB) $ \(Identity arg) ->               let expected = Left . DoesNotUnify tA' $ arg-                  actual = checkApp f [Just arg]+                  actual = checkApp M.empty f [Just arg]                in expected === actual   where     -- This ensures that our cases occur with equal frequency.@@ -210,9 +232,9 @@       -- be based on `S scope`, since that's what's in the computation type.       -- However, we actually have to reduce it by 1, as we have a 'scope       -- stepdown' for `f` even though we bind no variables.-      let trueLevel = negate . asInt $ scope+      let trueLevel = negate . review asInt $ scope           expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t'-          actual = checkApp f [Just t']+          actual = checkApp M.empty f [Just t']        in expected === actual  -- Randomly pick a concrete type A, then try to apply `(forall a . a ->@@ -225,7 +247,7 @@          in withRenamedVals (Identity argT) $ \(Identity argT') ->               let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT                   expected = Left . DoesNotUnify lhs $ argT'-                  actual = checkApp f [Just argT']+                  actual = checkApp M.empty f [Just argT']                in expected === actual  -- Randomly generate a concrete type A, then try to apply@@ -237,7 +259,7 @@     withRenamedVals (Identity t) $ \(Identity t') ->       withRenamedVals (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) ->         let expected = Right t'-            actual = checkApp f [Just arg]+            actual = checkApp M.empty f [Just arg]          in expected === actual  -- Randomly generate a concrete type A, and a rigid type B, then try to apply `A@@ -247,9 +269,9 @@   withRenamedComp (Comp0 $ aT :--:> ReturnT integerT) $ \f ->     withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) ->       withRenamedVals (Identity aT) $ \(Identity aT') ->-        let level = negate . asInt $ scope+        let level = negate . review asInt $ scope             expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index-            actual = checkApp f [Just arg]+            actual = checkApp M.empty f [Just arg]          in expected === actual  -- Randomly generate a rigid type A, then try to apply `forall a . a -> !a` to@@ -259,7 +281,7 @@   withRenamedComp idT $ \f ->     withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) ->       let expected = Right arg-          actual = checkApp f [Just arg]+          actual = checkApp M.empty f [Just arg]        in expected === actual  -- Randomly generate a scope S and an index I, then another scope S' and another@@ -271,7 +293,7 @@ propUnifyRigid :: Property propUnifyRigid = forAllShrink gen shr $ \testData ->   withTestData testData $ \(f, arg, expected) ->-    let actual = checkApp f [Just arg]+    let actual = checkApp M.empty f [Just arg]      in expected === actual   where     gen :: Gen (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))@@ -312,7 +334,7 @@           Nothing -> withRenamedVals (Identity . tyvar db $ index) $ \(Identity arg) ->             f (fun, arg, Right integerT)           Just rest ->-            let level = negate . asInt $ db+            let level = negate . review asInt $ db                 lhs = Abstraction . Rigid level $ index              in case rest of                   Left db2 -> withRenamedVals (Identity . tyvar db2 $ index) $ \(Identity arg) ->@@ -330,9 +352,204 @@          in withRenamedVals (Identity argT) $ \(Identity argT') ->               let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT                   expected = Left . DoesNotUnify lhs $ argT'-                  actual = checkApp f [Just argT']+                  actual = checkApp M.empty f [Just argT']                in expected === actual +-- Randomly pick concrete types A and B, then try to apply to `forall a . ((A -> B ->+-- !a) -> !a)` the argument `(A -> B -> !A)`. Result should unify and produce+-- `A`.+propThunkWithUnifiableResult :: Property+propThunkWithUnifiableResult = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) ->+  let funThunkArgT = ThunkT $ Comp0 $ aT :--:> bT :--:> ReturnT (tyvar (S Z) ix0)+      funT = Comp1 $ funThunkArgT :--:> ReturnT (tyvar Z ix0)+      thunkT = ThunkT $ Comp0 $ aT :--:> bT :--:> ReturnT aT+   in withRenamedComp funT $ \f ->+        withRenamedVals (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals (Identity aT) $ \(Identity aT') ->+            let expected = Right aT'+                actual = checkApp M.empty f [Just argT]+             in expected === actual++-- Tries to apply some concrete types to `defaultLeft`, checks that the return type is+-- correct after unification (via checkApp)+testEitherConcrete :: TestTree+testEitherConcrete = testCase "testEitherConcrete" $ do+  -- a == unit+  -- b == bool+  -- c == integer+  let arg1 = BuiltinFlat IntegerT+      arg2 = ThunkT (Comp0 $ BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT))+      arg3 = Datatype "Either" . Vector.fromList $ [BuiltinFlat UnitT, BuiltinFlat BoolT]++      expected = BuiltinFlat IntegerT+  defaultLeftRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft+  actual <-+    either (assertFailure . show) pure $+      checkApp+        tyAppTestDatatypes+        defaultLeftRenamed+        (pure <$> [arg1, arg2, arg3])+  assertEqual "testEitherConcrete" expected actual++-- Tries to apply arguments containing a mixture of concrete and abstract types to the BB form for maybe,+-- then checks whether the application types as the (concrete) return type.+-- note: The order of args is wrong for a Plutus "Maybe" (but that doesn't matter). BB form is:+-- forall a r. r -> (a -> r) -> r+-- (Plutus defines 'Maybe' incorrectly, i.e., with the 'Just' ctor first)+polymorphicApplicationM :: TestTree+polymorphicApplicationM = testCase "polyAppMaybe" $ do+  let testFn =+        Comp1 $+          ( ThunkT . Comp1 $+              tyvar Z ix0+                :--:> ThunkT (Comp0 (tyvar (S (S Z)) ix0 :--:> ReturnT (tyvar (S Z) ix0)))+                :--:> ReturnT (tyvar Z ix0)+          )+            :--:> ReturnT (BuiltinFlat IntegerT)+      testArg =+        ThunkT . Comp1 $+          tyvar Z ix0+            :--:> ThunkT (Comp0 (BuiltinFlat BoolT :--:> ReturnT (tyvar (S Z) ix0)))+            :--:> ReturnT (tyvar Z ix0)+  fnRenamed <- failLeft . runRenameM . renameCompT $ testFn+  argRenamed <- failLeft . runRenameM . renameValT $ testArg+  result <-+    either (assertFailure . show) pure $+      checkApp tyAppTestDatatypes fnRenamed [Just argRenamed]+  assertEqual "polyAppMaybe" result (BuiltinFlat IntegerT)++-- Applies a mixture of polymorphic and concrete arguments to `defaultLeft` and checks that the  return+-- type is what we expected after unification+polymorphicApplicationE :: TestTree+polymorphicApplicationE = testCase "polyAppEither" $ do+  -- a = a' (arbitrary unifiable)+  -- b = Bool+  -- c = Integer+  let arg1 = Abstraction $ Unifiable ix0+      arg2 = ThunkT (Comp0 $ BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT))+      arg3 = Datatype "Either" . Vector.fromList $ [arg1, BuiltinFlat BoolT]+  fnRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft+  actual <-+    either (assertFailure . show) pure $+      checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3])+  assertEqual "polyAppEither" actual (BuiltinFlat IntegerT)++-- Applies a mixture of polymorphic and concrete arguments to `defaultPair` and checks that the return type+-- is what we expected after unification+polymorphicApplicationP :: TestTree+polymorphicApplicationP = testCase "polyAppPair" $ do+  -- a = a' (arbitrary unifiable)+  -- b = Bool+  -- c = Integer+  let arg1 = Abstraction $ Unifiable ix0+      arg2 = BuiltinFlat BoolT+      arg3 = ThunkT $ Comp0 $ Abstraction (Rigid 1 ix0) :--:> BuiltinFlat BoolT :--:> ReturnT (BuiltinFlat IntegerT)+      arg4 = Datatype "Pair" (Vector.fromList [arg1, BuiltinFlat BoolT])+  fnRenamed <- failLeft . runRenameM . renameCompT $ defaultPair+  actual <-+    either (assertFailure . show) pure $+      checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3, arg4])+  assertEqual "polyAppPair" actual (BuiltinFlat IntegerT)++-- Checks whether `forall a. Maybe a -> Integer` unifies properly with `Maybe Bool -> Integer`+unifyMaybe :: TestTree+unifyMaybe = testCase "unifyMaybe" $ do+  let testFn =+        Comp1 $+          Datatype "Maybe" (Vector.fromList [tyvar Z ix0])+            :--:> ReturnT (BuiltinFlat IntegerT)+      testArg = Datatype "Maybe" (Vector.fromList [BuiltinFlat BoolT])+  fnRenamed <- failLeft . runRenameM . renameCompT $ testFn+  result <-+    either (assertFailure . catchInsufficientArgs) pure $+      checkApp tyAppTestDatatypes fnRenamed [Just testArg]+  assertEqual "unifyMaybe" result (BuiltinFlat IntegerT)+  where+    catchInsufficientArgs :: TypeAppError -> String+    catchInsufficientArgs = \case+      InsufficientArgs _ fn _ -> prettyStr fn+      other -> show other++-- Checks that `forall a . Maybe a -> Maybe (Maybe a)`, when applied to `Maybe+-- Integer`, produces `Maybe (Maybe Integer)`+unitNestedDatatypes :: IO ()+unitNestedDatatypes = do+  let fn =+        Comp1 $+          Datatype "Maybe" (Vector.singleton $ tyvar Z ix0)+            :--:> ReturnT (Datatype "Maybe" (Vector.singleton . Datatype "Maybe" . Vector.singleton $ tyvar Z ix0))+  fnRenamed <- failLeft . runRenameM . renameCompT $ fn+  let arg = Datatype "Maybe" . Vector.singleton $ integerT+  let expected = Datatype "Maybe" . Vector.singleton . Datatype "Maybe" . Vector.singleton $ integerT+  case checkApp tyAppTestDatatypes fnRenamed [Just arg] of+    Left err -> assertFailure . show $ err+    Right res -> assertEqual "type mismatch" expected res++-- Randomly pick concrete types A and B, then try to apply to `forall a. ((A ->+-- Maybe B -> !a) -> !a)` the argument `(A -> Maybe B -> !A)`. Result should+-- unify and produce `A`.+propThunkWithDatatype :: Property+propThunkWithDatatype = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) ->+  let maybeT = Datatype "Maybe" (Vector.singleton bT)+      funThunkArg = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT (tyvar (S Z) ix0)+      funT = Comp1 $ funThunkArg :--:> ReturnT (tyvar Z ix0)+      thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT+   in withRenamedComp funT $ \f ->+        withRenamedVals (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals (Identity aT) $ \(Identity aT') ->+            let expected = Right aT'+                actual = checkApp tyAppTestDatatypes f [Just argT]+             in expected === actual++-- Randomly pick concrete types A and B, then try to apply to `((A -> Maybe B ->+-- !A) -> !A)` the argument `(A -> Maybe B -> !A)`. Result should unify and+-- produce `A`.+propConcreteThunkWithDatatype :: Property+propConcreteThunkWithDatatype = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) ->+  let maybeT = Datatype "Maybe" (Vector.singleton bT)+      funThunkArg = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT+      funT = Comp0 $ funThunkArg :--:> ReturnT aT+      thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT+   in withRenamedComp funT $ \f ->+        withRenamedVals (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals (Identity aT) $ \(Identity aT') ->+            let expected = Right aT'+                actual = checkApp tyAppTestDatatypes f [Just argT]+             in expected === actual++-- Randomly pick concrete types A and B, then try to apply to `forall a. ((a -> Maybe B+-- -> !A) -> !A)` the argument `(A -> Maybe B -> !A)`. Result should unify and+-- produce `A`.+propThunkUnifiableWithDatatype :: Property+propThunkUnifiableWithDatatype = forAllShrink arbitrary shrink $ \(Concrete aT, Concrete bT) ->+  let maybeT = Datatype "Maybe" (Vector.singleton bT)+      funThunkArg = ThunkT $ Comp1 $ tyvar (S Z) ix0 :--:> maybeT :--:> ReturnT aT+      funT = Comp1 $ funThunkArg :--:> ReturnT aT+      thunkT = ThunkT $ Comp0 $ aT :--:> maybeT :--:> ReturnT aT+   in withRenamedComp funT $ \f ->+        withRenamedVals (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals (Identity aT) $ \(Identity aT') ->+            let expected = Right aT'+                actual = checkApp tyAppTestDatatypes f [Just argT]+             in expected === actual++-- Randomly pick concrete type A, then try to apply to `forall a . ((Maybe A ->+-- !a) -> !a)` the argument `(Maybe A -> !A)`. Result should unify and produce+-- `A`.+propThunkUnifiableDatatype :: Property+propThunkUnifiableDatatype = forAllShrink arbitrary shrink $ \(Concrete aT) ->+  let -- maybeTUnifiable = Datatype "Maybe" . Vector.singleton $ tyvar (S Z) ix0+      maybeTConcrete = Datatype "Maybe" . Vector.singleton $ aT+      funThunkArg = ThunkT $ Comp0 $ maybeTConcrete :--:> ReturnT (tyvar (S Z) ix0)+      funT = Comp1 $ funThunkArg :--:> ReturnT (tyvar Z ix0)+      thunkT = ThunkT $ Comp0 $ maybeTConcrete :--:> ReturnT aT+   in withRenamedComp funT $ \f ->+        withRenamedVals (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals (Identity aT) $ \(Identity aT') ->+            let expected = Right aT'+                actual = checkApp tyAppTestDatatypes f [Just argT]+             in expected === actual+ -- Helpers  -- `forall a. a -> !a`@@ -343,12 +560,25 @@ const2T :: CompT AbstractTy const2T = Comp2 $ tyvar Z ix0 :--:> tyvar Z ix1 :--:> ReturnT (tyvar Z ix0) -failLeft ::-  forall (a :: Type) (b :: Type).-  (Show a) =>-  Either a b ->-  IO b-failLeft = either (assertFailure . show) pure+-- forall a b c. c -> (b -> !c) -> Either a b -> !c+-- ...I hope+defaultLeft :: CompT AbstractTy+defaultLeft =+  Comp3 $+    tyvar Z ix2+      :--:> ThunkT (Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix2))+      :--:> Datatype "Either" (Vector.fromList [tyvar Z ix0, tyvar Z ix1])+      :--:> ReturnT (tyvar Z ix2)++-- forall a b c. a -> b -> (a -> b -> !c) -> Pair a b -> c+defaultPair :: CompT AbstractTy+defaultPair =+  Comp3 $+    tyvar Z ix0+      :--:> tyvar Z ix1+      :--:> ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix2))+      :--:> Datatype "Pair" (Vector.fromList [tyvar Z ix0, tyvar Z ix1])+      :--:> ReturnT (tyvar Z ix2)  withRenamedComp ::   CompT AbstractTy ->