covenant 1.1.0 → 1.2.0

raw patch · 17 files changed

+1946/−473 lines, 17 filesdep +smashPVP ok

version bump matches the API change (PVP)

Dependencies added: smash

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−1
• covenant.cabal +5/−2
• src/Covenant/ASG.hs +760/−91
• src/Covenant/Data.hs +1/−0
• src/Covenant/Index.hs +7/−0
• src/Covenant/Internal/KindCheck.hs +12/−2
• src/Covenant/Internal/Rename.hs +163/−66
• src/Covenant/Internal/Term.hs +153/−9
• src/Covenant/Internal/Type.hs +17/−3
• src/Covenant/Internal/Unification.hs +70/−25
• src/Covenant/Test.hs +79/−5
• src/Covenant/Type.hs +1/−7
• test/asg/Main.hs +498/−112
• test/bb/Main.hs +3/−5
• test/primops/Main.hs +3/−3
• test/renaming/Main.hs +11/−10
• test/type-applications/Main.hs +153/−132

@@ -4,7 +4,16 @@  The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/). -## UNRELEASED+## 1.2.0 -- 2025-08-27++* Helper function for safely retrieving an in-scope type variable when constructing the ASG  +* Removed Return nodes, associated pattern synonyms, and the `ret` ASGBuilder function+* Reworked the renamer to be context sensitive+* Added new error types for un-renaming+* Modified ASG helper functions and updated tests to conform with renamer rework+* Added support for introduction forms (ValNode stuff, ASG helper function, tests)+* Added support for catamorphism elimination forms+* Added support for pattern matching elimination form  ## 1.1.0 -- 2025-07-11 

@@ -1,6 +1,6 @@ cabal-version: 3.0 name: covenant-version: 1.1.0+version: 1.2.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.@@ -84,6 +84,7 @@     nonempty-vector ==0.2.4,     optics-core ==0.4.1.1,     prettyprinter ==1.7.1,+    smash ==0.1.0.0,     tasty ==1.5.3,     tasty-expected-failure ==0.12.3,     tasty-hunit ==0.10.2,@@ -92,7 +93,8 @@  common bench-lang   import: lang-  ghc-options: -O2+  ghc-options:+    -O2  -- Primary library library@@ -135,6 +137,7 @@     prettyprinter ==1.7.1,     quickcheck-instances ==0.3.32,     quickcheck-transformer ==0.3.1.2,+    smash ==0.1.0.0,     tasty-hunit ==0.10.2,     text >=2.1.1 && <2.2,     transformers >=0.6.1.0 && <0.7.0.0,

@@ -1,3 +1,4 @@+{-# LANGUAGE CPP #-} {-# LANGUAGE PatternSynonyms #-}  -- |@@ -37,11 +38,11 @@         Builtin3,         Builtin6,         Lam,-        Force,-        Return+        Force       ),-    ValNodeInfo (Lit, App, Thunk),+    ValNodeInfo (Lit, App, Thunk, Cata, DataConstructor, Match),     ASGNode (..),+    ASGNodeType (..),      -- ** Functions     typeASGNode,@@ -50,36 +51,54 @@      -- ** Types     CovenantError (..),-    ScopeInfo,+    ScopeInfo (..),     ASGBuilder,     TypeAppError (..),     RenameError (..),+    UnRenameError (..),+    EncodingArgErr (..),     CovenantTypeError (..),+    BoundTyVar,      -- ** Introducers+    boundTyVar,     arg,     builtin1,     builtin2,     builtin3,     builtin6,     force,-    ret,     lam,     err,     lit,     thunk,+    dataConstructor,++    -- ** Eliminators     app,+    cata,+    match, -    -- ** Elimination+    -- ** Helpers+    ctor,+    lazyLam,+    dtype,      -- *** Environment     defaultDatatypes,      -- *** Function     runASGBuilder,+    -- only for tests+    ASGEnv (..),   ) where +#if __GLASGOW_HASKELL__==908+import Data.Foldable (foldl')+#endif++import Control.Monad (foldM, join, unless, zipWithM) import Control.Monad.Except   ( ExceptT,     MonadError (throwError),@@ -98,15 +117,18 @@   ) 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.DeBruijn (DeBruijn (S, Z), asInt)+import Covenant.Index (Count, Index, count0, intCount, intIndex, wordCount)+import Covenant.Internal.KindCheck (EncodingArgErr (EncodingArgMismatch), checkEncodingArgs) import Covenant.Internal.Ledger (ledgerTypes) import Covenant.Internal.Rename   ( RenameError-      ( InvalidAbstractionReference+      ( InvalidAbstractionReference,+        InvalidScopeReference       ),+    UnRenameError (NegativeDeBruijn, UnRenameWildCard),     renameCompT,+    renameDatatypeInfo,     renameValT,     runRenameM,     undoRename,@@ -121,21 +143,45 @@         Builtin3Internal,         Builtin6Internal,         ForceInternal,-        LamInternal,-        ReturnInternal+        LamInternal       ),     CovenantTypeError       ( ApplyCompType,         ApplyToError,         ApplyToValType,         BrokenIdReference,+        CataAlgebraWrongArity,+        CataApplyToNonValT,+        CataNoBaseFunctorForType,+        CataNoSuchType,+        CataNonRigidAlgebra,+        CataNotAnAlgebra,+        CataUnsuitable,+        CataWrongBuiltinType,+        CataWrongValT,+        ConstructorDoesNotExistForType,+        DatatypeInfoRenameError,         EncodingError,+        FailedToRenameInstantiation,         ForceCompType,         ForceError,         ForceNonThunk,+        IntroFormErrorNodeField,+        IntroFormWrongNumArgs,+        InvalidOpaqueField,+        LambdaResultsInCompType,         LambdaResultsInNonReturn,-        LambdaResultsInValType,+        MatchErrorAsHandler,+        MatchNoBBForm,+        MatchNoDatatypeInfo,+        MatchNonDatatypeScrutinee,+        MatchNonThunkBBF,+        MatchNonValTy,+        MatchPolymorphicHandler,+        MatchRenameBBFail,+        MatchRenameTyConArgFail,         NoSuchArgument,+        OutOfScopeTyVar,         RenameArgumentFailed,         RenameFunctionFailed,         ReturnCompType,@@ -143,24 +189,29 @@         ReturnWrapsError,         ThunkError,         ThunkValType,+        TypeDoesNotExist,+        UndeclaredOpaquePlutusDataCtor,+        UndoRenameFailure,         UnificationError,         WrongReturnType       ),     Id,     Ref (AnArg, AnId),-    ValNodeInfo (AppInternal, LitInternal, ThunkInternal),+    ValNodeInfo (AppInternal, CataInternal, DataConstructorInternal, LitInternal, MatchInternal, ThunkInternal),     typeASGNode,     typeId,     typeRef,   ) import Covenant.Internal.Type-  ( AbstractTy,+  ( AbstractTy (BoundAt),+    BuiltinFlatT (ByteStringT, IntegerT),     CompT (CompT),     CompTBody (CompTBody),-    DataDeclaration,+    DataDeclaration (DataDeclaration),     Renamed,     TyName,-    ValT (ThunkT),+    ValT (BuiltinFlat, Datatype, ThunkT),+    arity,   ) import Covenant.Internal.Unification   ( TypeAppError@@ -174,7 +225,13 @@         NoBBForm,         NoDatatypeInfo       ),+    UnifyM,     checkApp,+    fixUp,+    reconcile,+    runUnifyM,+    substitute,+    unify,   ) import Covenant.Prim   ( OneArgFunc,@@ -186,27 +243,50 @@     typeThreeArgFunc,     typeTwoArgFunc,   )+import Covenant.Type+  ( CompT (Comp0),+    CompTBody (ReturnT),+    Constructor,+    ConstructorName,+    DataDeclaration (OpaqueData),+    PlutusDataConstructor (PlutusB, PlutusConstr, PlutusI, PlutusList, PlutusMap),+    Renamed (Unifiable),+    TyName (TyName),+    ValT (Abstraction),+    tyvar,+  ) import Data.Bimap (Bimap) import Data.Bimap qualified as Bimap import Data.Coerce (coerce) import Data.Functor.Identity (Identity, runIdentity) import Data.Kind (Type)+import Data.List (find) import Data.Map.Strict (Map) import Data.Map.Strict qualified as Map-import Data.Maybe (fromJust)+import Data.Maybe (fromJust, isJust, mapMaybe)+import Data.Set qualified as Set+import Data.Text qualified as T import Data.Vector (Vector) import Data.Vector qualified as Vector import Data.Vector.NonEmpty qualified as NonEmpty+import Data.Void (Void, vacuous)+import Data.Wedge (Wedge, wedge)+import Data.Word (Word32) import Optics.Core   ( A_Lens,     LabelOptic (labelOptic),+    at,+    folded,     ix,     lens,     over,     preview,     review,+    toListOf,     view,     (%),+    _1,+    _2,   )  -- | A fully-assembled Covenant ASG.@@ -249,8 +329,14 @@ nodeAt :: Id -> ASG -> ASGNode nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings +-- | The environment used when \'building up\' an 'ASG'. This type is exposed+-- only for testing, or debugging, and should /not/ be used in general by those+-- who just want to build an 'ASG'.+--+-- @since 1.2.0 data ASGEnv = ASGEnv ScopeInfo (Map TyName (DatatypeInfo AbstractTy)) +-- | @since 1.2.0 instance   (k ~ A_Lens, a ~ ScopeInfo, b ~ ScopeInfo) =>   LabelOptic "scopeInfo" k ASGEnv ASGEnv a b@@ -261,6 +347,7 @@       (\(ASGEnv si _) -> si)       (\(ASGEnv _ dti) si -> ASGEnv si dti) +-- | @since 1.2.0 instance   (k ~ A_Lens, a ~ Map TyName (DatatypeInfo AbstractTy), b ~ Map TyName (DatatypeInfo AbstractTy)) =>   LabelOptic "datatypeInfo" k ASGEnv ASGEnv a b@@ -281,8 +368,8 @@ -- the functionality provided by this module is not recommended, unless you know -- /exactly/ what you're doing. ----- @since 1.0.0-newtype ScopeInfo = ScopeInfo (Vector (Vector (ValT AbstractTy)))+-- @since 1.2.0+newtype ScopeInfo = ScopeInfo (Vector (Word32, Vector (ValT AbstractTy)))   deriving stock     ( -- | @since 1.0.0       Eq,@@ -296,9 +383,9 @@ -- enclosing scope, 2 is the enclosing scope of our enclosing scope, etc. The -- \'inner\' 'Vector's are positional lists of argument types. ----- @since 1.0.0+-- @since 1.2.0 instance-  (k ~ A_Lens, a ~ Vector (Vector (ValT AbstractTy)), b ~ Vector (Vector (ValT AbstractTy))) =>+  (k ~ A_Lens, a ~ Vector (Word32, Vector (ValT AbstractTy)), b ~ Vector (Word32, Vector (ValT AbstractTy))) =>   LabelOptic "argumentInfo" k ScopeInfo ScopeInfo a b   where   {-# INLINEABLE labelOptic #-}@@ -334,19 +421,13 @@ pattern Force :: Ref -> CompNodeInfo pattern Force r <- ForceInternal r --- | Produce the result of a computation.------ @since 1.0.0-pattern Return :: Ref -> CompNodeInfo-pattern Return r <- ReturnInternal r- -- | A lambda. ----- @since 1.0.0-pattern Lam :: Id -> CompNodeInfo-pattern Lam i <- LamInternal i+-- @since 1.2.0+pattern Lam :: Ref -> CompNodeInfo+pattern Lam r <- LamInternal r -{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Return, Lam #-}+{-# COMPLETE Builtin1, Builtin2, Builtin3, Builtin6, Force, Lam #-}  -- | A compile-time literal of a flat builtin type. --@@ -367,8 +448,26 @@ pattern Thunk :: Id -> ValNodeInfo pattern Thunk i <- ThunkInternal i -{-# COMPLETE Lit, App, Thunk #-}+-- | \'Tear down\' a self-recursive value with an algebra.+--+-- @since 1.0.0+pattern Cata :: Ref -> Ref -> ValNodeInfo+pattern Cata algebraRef valRef <- CataInternal algebraRef valRef +-- | Inject (zero or more) fields into a data constructor+--+-- @since 1.2.0+pattern DataConstructor :: TyName -> ConstructorName -> Vector Ref -> ValNodeInfo+pattern DataConstructor tyName ctorName fields <- DataConstructorInternal tyName ctorName fields++-- | Deconstruct a value of a data type using the supplied handlers for each arm+--+-- @since 1.2.0+pattern Match :: Ref -> Vector Ref -> ValNodeInfo+pattern Match scrutinee handlers <- MatchInternal scrutinee handlers++{-# COMPLETE Lit, App, Thunk, Cata, DataConstructor, Match #-}+ -- | Any problem that might arise when building an ASG programmatically. -- -- @since 1.0.0@@ -467,7 +566,7 @@ arg scope index = do   let scopeAsInt = review asInt scope   let indexAsInt = review intIndex index-  lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % ix indexAsInt))+  lookedUp <- asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % _2 % ix indexAsInt))   case lookedUp of     Nothing -> throwError . NoSuchArgument scope $ index     Just t -> pure . Arg scope index $ t@@ -538,24 +637,6 @@     CompNodeType t -> throwError . ForceCompType $ t     ErrorNodeType -> throwError ForceError --- | Given the result of a function body (either a value or an error), construct--- the return for it. Will fail if that reference aims at a computation node.------ @since 1.0.0-ret ::-  forall (m :: Type -> Type).-  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>-  Ref ->-  m Id-ret r = do-  refT <- typeRef r-  case refT of-    ValNodeType t -> do-      let t' = CompT count0 . CompTBody . NonEmpty.singleton $ t-      refTo . ACompNode t' . ReturnInternal $ r-    CompNodeType t -> throwError . ReturnCompType $ t-    ErrorNodeType -> err- -- | Given a desired type, and a computation which will construct a lambda body -- when executed (with the scope extended with the arguments the functions can -- expect), construct a lambda.@@ -567,37 +648,34 @@ -- \'bottom-up\', whereas function arguments (and their scopes) are necessarily -- top-down. Thus, we need to \'delay\' the construction of a lambda's body to -- ensure that proper scoped argument information can be given to it, hence why--- the argument being passed is an @m Id@.+-- the argument being passed is an @m Ref@. ----- @since 1.0.0+-- @since 1.2.0 lam ::   forall (m :: Type -> Type).   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>   CompT AbstractTy ->-  m Id ->+  m Ref ->   m Id-lam expectedT@(CompT _ (CompTBody xs)) bodyComp = do+lam expectedT@(CompT cnt (CompTBody xs)) bodyComp = do   let (args, resultT) = NonEmpty.unsnoc xs-  bodyId <- local (over (#scopeInfo % #argumentInfo) (Vector.cons args)) bodyComp-  bodyNode <- lookupRef bodyId-  case bodyNode of-    Nothing -> throwError . BrokenIdReference $ bodyId-    -- This unifies with anything, so we're fine-    Just AnError -> refTo . ACompNode expectedT . LamInternal $ bodyId-    Just (ACompNode t specs) -> case specs of-      ReturnInternal r -> do-        rT <- typeRef r-        case rT of-          -- Note (Koz, 17/04/2025): I am not 100% sure about this, but I can't-          -- see how anything else would make sense.-          ValNodeType actualT ->-            if resultT == actualT-              then refTo . ACompNode expectedT . LamInternal $ bodyId-              else throwError . WrongReturnType resultT $ actualT-          ErrorNodeType -> throwError ReturnWrapsError -- Should be impossible-          CompNodeType t' -> throwError . ReturnWrapsCompType $ t'-      _ -> throwError . LambdaResultsInNonReturn $ t-    Just (AValNode t _) -> throwError . LambdaResultsInValType $ t+      cntW = view wordCount cnt+  bodyRef <- local (over (#scopeInfo % #argumentInfo) (Vector.cons (cntW, args))) bodyComp+  case bodyRef of+    AnArg (Arg _ _ argTy) -> do+      if argTy == resultT+        then refTo . ACompNode expectedT . LamInternal $ bodyRef+        else throwError . WrongReturnType resultT $ argTy+    AnId bodyId ->+      lookupRef bodyId >>= \case+        Nothing -> throwError . BrokenIdReference $ bodyId+        -- This unifies with anything, so we're fine+        Just AnError -> refTo . ACompNode expectedT . LamInternal . AnId $ bodyId+        Just (AValNode ty _) -> do+          if ty == resultT+            then refTo . ACompNode expectedT . LamInternal . AnId $ bodyId+            else throwError . WrongReturnType resultT $ ty+        Just (ACompNode t _) -> throwError $ LambdaResultsInCompType t  -- | Construct the error node. --@@ -608,37 +686,245 @@   m Id err = refTo AnError --- | Given an 'Id' referring to a computation, and a 'Vector' of 'Ref's to the--- desired arguments, construct the application of the arguments to that--- computation. This can fail for a range of reasons:+-- | Performs both term and type application. More precisely, given: --+-- * An 'Id' referring to a computation; and+-- * A 'Vector' of 'Ref's for the desired term arguments to the computation, in+--   order; and+-- * A 'Vector' of (optional) type arguments to the computation, also in order.+--+-- we produce the result of that application.+--+-- This can fail for a range of reasons:+-- -- * Type mismatch between what the computation expects and what it's given -- * Too many or too few arguments -- * Not a computation type for 'Id' argument -- * Not value types for 'Ref's+-- * Renaming failures (likely due to a malformed function or argument type) ----- @since 1.0.0+-- = Note+--+-- We use the 'Wedge' data type to designate type arguments, as it can represent+-- the three possibilities we need:+--+-- * \'Infer this argument\', specified as 'Nowhere'.+-- * \'Use this type variable in our scope\', specified as 'Here'.+-- * \'Use this concrete type\', specified as 'There'.+--+-- @since 1.2.0 app ::   forall (m :: Type -> Type).   (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>   Id ->   Vector Ref ->+  Vector (Wedge BoundTyVar (ValT Void)) ->   m Id-app fId argRefs = do+app fId argRefs instTys = do   lookedUp <- typeId fId+  let rawSubs = mkSubstitutions instTys+  subs <- renameSubs rawSubs+  scopeInfo <- askScope   case lookedUp of-    CompNodeType fT -> case runRenameM . renameCompT $ fT of+    CompNodeType fT -> case runRenameM scopeInfo . renameCompT $ fT of       Left err' -> throwError . RenameFunctionFailed fT $ err'       Right renamedFT -> do+        instantiatedFT <- instantiate subs renamedFT         renamedArgs <- traverse renameArg argRefs         tyDict <- asks (view #datatypeInfo)-        result <- either (throwError . UnificationError) pure $ checkApp tyDict renamedFT (Vector.toList renamedArgs)-        let restored = undoRename result+        result <- either (throwError . UnificationError) pure $ checkApp tyDict instantiatedFT (Vector.toList renamedArgs)+        restored <- undoRenameM result         checkEncodingWithInfo tyDict restored         refTo . AValNode restored . AppInternal fId $ argRefs     ValNodeType t -> throwError . ApplyToValType $ t     ErrorNodeType -> throwError ApplyToError+  where+    mkSubstitutions :: Vector (Wedge BoundTyVar (ValT Void)) -> [(Index "tyvar", ValT AbstractTy)]+    mkSubstitutions =+      Vector.ifoldl'+        ( \acc i' w ->+            let i = fromJust . preview intIndex $ i'+             in wedge+                  acc+                  (\(BoundTyVar dbIx posIx) -> (i, tyvar dbIx posIx) : acc)+                  (\v -> (i, vacuous v) : acc)+                  w+        )+        [] +    renameSubs :: [(Index "tyvar", ValT AbstractTy)] -> m [(Index "tyvar", ValT Renamed)]+    renameSubs subs =+      askScope >>= \scope -> case traverse (traverse (runRenameM scope . renameValT)) subs of+        Left err' -> throwError $ FailedToRenameInstantiation err'+        Right res -> pure res++    instantiate :: [(Index "tyvar", ValT Renamed)] -> CompT Renamed -> m (CompT Renamed)+    instantiate [] fn = pure fn+    instantiate subs fn = do+      instantiated <- liftUnifyM . fixUp $ foldr (\(i, t) f -> substitute i t f) (ThunkT fn) subs+      case instantiated of+        ThunkT res -> pure res+        other ->+          throwError . UnificationError . ImpossibleHappened $+            "Impossible happened: Result of tyvar instantiation should be a thunk, but is: "+              <> T.pack (show other)++-- | Introduce a data constructor.+--+-- The first argument is a type name (for example, @\"Maybe\"@). The second+-- argument is a constructor of that type (for example, @\"Just\"@ or+-- @\"Nothing\"@). The third argument are the values to \'fill in\' all the fields+-- of the constructor requested.+--+-- = Note+--+-- 'dataConstructor' yields thunks, which must be forced, and then possibly have+-- type arguments applied to them. The reason for this is subtle, but important.+-- Consider the @Nothing@ constructor of @Maybe@: as this has no fields, we+-- cannot use the field type to determine what the type argument to @Maybe@+-- should be in this case. As datatype terms are values, they do not bind type+-- variables, and thus, we cannot have a return type that makes sense in this+-- case.+--+-- We resolve this problem by returning a thunk. In the case of our example,+-- @Nothing@ would produce @<forall a . !Maybe a>@.+--+-- @since 1.2.0+dataConstructor ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  TyName ->+  ConstructorName ->+  Vector Ref ->+  m Id+dataConstructor tyName ctorName fields = do+  thisTyInfo <- lookupDatatypeInfo+  let thisTyDecl = view #originalDecl thisTyInfo+  renamedFieldTypes <-+    traverse renameArg fields+      >>= ( \case+              Nothing -> throwError $ IntroFormErrorNodeField tyName ctorName fields+              Just ok -> pure ok+          )+        . sequence+  {- The procedures for handling a typed declared as Opaque and a "normal" type are totally different.++     For Opaque types, we just have to check that the "ConstructorName" we get corresponds to a constructor of+     PlutusData, then validate that the arguments conform with that PlutusData constructor.+  -}+  case thisTyDecl of+    OpaqueData _ opaqueCtorSet -> do+      checkOpaqueArgs opaqueCtorSet renamedFieldTypes+      refTo $ AValNode (Datatype tyName mempty) (DataConstructorInternal tyName ctorName fields)+    DataDeclaration _ count ctors _ -> do+      -- First we check that the arity of the constructor is equal to the number of fields in the decl.+      checkFieldArity (Vector.length fields) thisTyInfo+      -- Then we resolve the supplied field Refs, rename, and throw an error if we're passed an error node.++      -- Then we construct the return type.+      resultThunk <- mkResultThunk count ctors renamedFieldTypes+      -- Then we undo the renaming.+      restored <- undoRenameM resultThunk+      -- Then we check the compatibility of the arguments with the datatype's encoding.+      asks (view #datatypeInfo) >>= \dti -> checkEncodingWithInfo dti restored+      -- Finally, if nothing has thrown an error, we return a reference to our result node, decorated with the+      -- return type we constructed.+      refTo $ AValNode restored (DataConstructorInternal tyName ctorName fields)+  where+    {- Constructs the result type of the introduction form. Arguments are:+         1. The count (number of tyvars) from the data declaration.+         2. The vector of constructors from the data declaration.+         3. The (renamed and resolved) vector of supplied arguments.++       The procedure goes like:+         1. Extract the argument types from the constructor in the declaration. Any tyvars here+            *have* to be Unifiable (unless something has slipped past the kind checker) -+            data declarations have atomic, independent scopes.+         2. Unify those with the actual, supplied field types, yielding a set of substitutions.+         3. Construct a fully abstract (i.e. parameterized only by unifiable type variables) representation of the+            type constructor.+         4. Apply those substitutions to the abstract type constructor.+         5. Wrap the "concretified" type constructor in a thunk and use `fixUp` to sort out the `Count` and+            indices.+    -}+    mkResultThunk :: Count "tyvar" -> Vector (Constructor Renamed) -> Vector (ValT Renamed) -> m (ValT Renamed)+    mkResultThunk count' declCtors fieldArgs' = do+      declCtorFields <- Vector.toList . view #constructorArgs <$> findConstructor declCtors+      subs <- unifyFields declCtorFields fieldArgs+      let tyConAbstractArgs = mapMaybe (fmap (Abstraction . Unifiable) . preview intIndex) [0, 1 .. (count - 1)]+          tyConAbstract = Datatype tyName (Vector.fromList tyConAbstractArgs)+      let tyConConcrete = Map.foldlWithKey' (\acc i t -> substitute i t acc) tyConAbstract subs+      liftUnifyM . fixUp . ThunkT . Comp0 . ReturnT $ tyConConcrete+      where+        count :: Int+        count = review intCount count'++        fieldArgs :: [ValT Renamed]+        fieldArgs = Vector.toList fieldArgs'++    {- Unifies the declaration fields (which may be abstract) with the supplied fields+       (which will be "concrete", in the sense that "they have to be rigid if they're tyvars").++       Returns a (reconciled) set of substitutions which can be applied to a fully-abstract (i.e.+       parameterized only by Unifiable tyVars) to yield the concrete, applied type constructor.+    -}+    unifyFields :: [ValT Renamed] -> [ValT Renamed] -> m (Map (Index "tyvar") (ValT Renamed))+    unifyFields declFields suppliedFields = liftUnifyM $ do+      rawSubs <- zipWithM unify declFields suppliedFields+      foldM reconcile Map.empty rawSubs++    {- Checks that the number of fields supplied as arguments is equal to the+       number of fields in the corresponding constructor of the data declaration.++       This is needed because `zipWithM unifyFields` won't throw an error in the case that they are not equal.+    -}+    checkFieldArity :: Int -> DatatypeInfo Renamed -> m ()+    checkFieldArity actualNumFields dtInfo = do+      let ctors = toListOf (#originalDecl % #datatypeConstructors % folded) dtInfo+      expectedNumFields <- Vector.length . view #constructorArgs <$> findConstructor ctors+      unless (actualNumFields == expectedNumFields) $+        throwError $+          IntroFormWrongNumArgs tyName ctorName actualNumFields++    checkOpaqueArgs :: Set.Set PlutusDataConstructor -> Vector (ValT Renamed) -> m ()+    checkOpaqueArgs declCtors fieldArgs' = case ctorName of+      "I" -> opaqueCheck PlutusI [BuiltinFlat IntegerT]+      "B" -> opaqueCheck PlutusB [BuiltinFlat ByteStringT]+      "List" -> opaqueCheck PlutusList [Datatype "List" (Vector.fromList [Datatype "Data" mempty])]+      "Map" -> opaqueCheck PlutusMap [Datatype "Map" (Vector.fromList [Datatype "Data" mempty, Datatype "Data" mempty])]+      "Constr" -> opaqueCheck PlutusConstr [BuiltinFlat IntegerT, Datatype "List" (Vector.fromList [Datatype "Data" mempty])]+      _ -> throwError $ UndeclaredOpaquePlutusDataCtor declCtors ctorName+      where+        fieldArgs :: [ValT Renamed]+        fieldArgs = Vector.toList fieldArgs'+        opaqueCheck :: PlutusDataConstructor -> [ValT Renamed] -> m ()+        opaqueCheck setMustHaveThis fieldShouldBeThis = do+          unless (setMustHaveThis `Set.member` declCtors) $ throwError (UndeclaredOpaquePlutusDataCtor declCtors ctorName)+          unless (fieldArgs == fieldShouldBeThis) $ throwError (InvalidOpaqueField declCtors ctorName fieldArgs)++    -- convenience helpers++    -- Looks up a constructor in a foldable container of constructors (which is probably always a vector but w/e)+    -- Exists to avoid duplicating this code in a few places.+    findConstructor ::+      forall (t :: Type -> Type) (a :: Type).+      (Foldable t) =>+      t (Constructor a) ->+      m (Constructor a)+    findConstructor xs = case find (\x -> view #constructorName x == ctorName) xs of+      Nothing -> throwError $ ConstructorDoesNotExistForType tyName ctorName+      Just ctor' -> pure ctor'++    -- Looks up the DatatypeInfo for the type argument supplied+    -- and also renames (and rethrows the rename error if renaming fails)+    lookupDatatypeInfo :: m (DatatypeInfo Renamed)+    lookupDatatypeInfo =+      asks (preview (#datatypeInfo % ix tyName)) >>= \case+        Nothing -> throwError $ TypeDoesNotExist tyName+        Just infoAbstract -> case renameDatatypeInfo infoAbstract of+          Left e -> throwError $ DatatypeInfoRenameError e+          Right infoRenamed -> pure infoRenamed+ -- | Construct a node corresponding to the given constant. -- -- @since 1.0.0@@ -665,20 +951,260 @@     ValNodeType t -> throwError . ThunkValType $ t     ErrorNodeType -> throwError ThunkError +-- | Given a 'Ref' to an algebra (that is, something taking a base functor and+-- producing some result), and a 'Ref' to a value associated with that base+-- functor, build a catamorphism to tear it down. This can fail for a range of+-- reasons:+--+-- * First 'Ref' is not a thunk taking one argument+-- * The argument to the thunk isn't a base functor, or isn't a suitable base+--   functor for the second argument+-- * Second argument is not a value type+--+-- = Note+--+-- 'cata' cannot work with /non-rigid/ algebras; that is, all algebras must be+-- functions that bind no type variables of their own.+--+-- @since 1.1.0+cata ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  Ref ->+  Ref ->+  m Id+cata rAlg rVal =+  typeRef rVal >>= \case+    ValNodeType valT ->+      typeRef rAlg >>= \case+        t@(ValNodeType (ThunkT algT)) -> case algT of+          Comp0 (CompTBody nev) -> do+            let algebraArity = arity algT+            unless (algebraArity == 1) (throwError . CataAlgebraWrongArity $ algebraArity)+            case nev NonEmpty.! 0 of+              Datatype bfName bfTyArgs -> do+                -- If we got this far, we know at minimum that we have somewhat+                -- sensical arguments. Now we have to make sure that we have a+                -- suitable type for the algebra, and a suitable thing to tear+                -- down.+                --+                -- After verifying this, we use `tryApply` so the unification+                -- machinery can produce the type we expect with proper+                -- concretifications.+                unless (Vector.length bfTyArgs > 0) (throwError . CataNotAnAlgebra $ t)+                let lastTyArg = Vector.last bfTyArgs+                unless (nev NonEmpty.! 1 == lastTyArg) (throwError . CataNotAnAlgebra $ t)+                appliedArgT <- case valT of+                  BuiltinFlat bT -> case bT of+                    ByteStringT -> do+                      unless (bfName == "ByteString_F") (throwError . CataUnsuitable algT $ valT)+                      pure $ Datatype "ByteString_F" . Vector.singleton $ lastTyArg+                    IntegerT -> do+                      let isSuitableBaseFunctor = bfName == "Natural_F" || bfName == "Negative_F"+                      unless isSuitableBaseFunctor (throwError . CataUnsuitable algT $ valT)+                      pure $ Datatype bfName . Vector.singleton $ lastTyArg+                    _ -> throwError . CataWrongBuiltinType $ bT+                  Datatype tyName tyVars -> do+                    lookedUp <- asks (view (#datatypeInfo % at tyName))+                    case lookedUp of+                      Nothing -> throwError . CataNoSuchType $ tyName+                      Just info -> case view #baseFunctor info of+                        Just (DataDeclaration actualBfName _ _ _, _) -> do+                          unless (bfName == actualBfName) (throwError . CataUnsuitable algT $ valT)+                          let lastTyArg' = stepDownDB lastTyArg+                          pure . Datatype bfName . Vector.snoc tyVars $ lastTyArg'+                        _ -> throwError . CataNoBaseFunctorForType $ tyName+                  _ -> throwError . CataWrongValT $ valT+                resultT <- tryApply algT appliedArgT+                refTo . AValNode resultT . CataInternal rAlg $ rVal+              _ -> throwError . CataNotAnAlgebra $ t+          _ -> throwError . CataNonRigidAlgebra $ algT+        t -> throwError . CataNotAnAlgebra $ t+    t -> throwError . CataApplyToNonValT $ t++-- | Perform a pattern match. The first argument is the value to be matched on,+-- and the second argument is a 'Vector' of \'handlers\' for each possible+-- \'arm\' of the type of the value to be matched on.+--+-- All handlers must be thunks, and must all return the same (concrete) result.+-- Polymorphic \'handlers\' (that is, thunks whose computation binds type+-- variables of its own) will fail to compile.+--+-- @since 1.2.0+match ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  Ref ->+  Vector Ref ->+  m Id+match scrutinee handlers = do+  scrutNodeTy <- typeRef scrutinee+  case scrutNodeTy of+    ValNodeType scrutTy@(Datatype tn args) ->+      isRecursive scrutTy >>= \case+        True -> goRecursive tn args+        False -> goNonRecursive tn args+    ValNodeType other -> throwError $ MatchNonDatatypeScrutinee other+    other -> throwError $ MatchNonValTy other+  where+    isRecursive :: ValT AbstractTy -> m Bool+    isRecursive (Datatype tyName _) = do+      datatypeInfoExists <- asks (isJust . preview (#datatypeInfo % ix tyName))+      if datatypeInfoExists+        then asks (isJust . join . preview (#datatypeInfo % ix tyName % #baseFunctor))+        else throwError $ MatchNoDatatypeInfo tyName+    isRecursive _ = pure False++    goRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id+    goRecursive tn@(TyName rawTn) tyConArgs = do+      -- This fromJust is safe b/c the presence of absence of base functor data is the condition that+      -- determines whether we're in this branch or the non-recursive one+      rawBFBB <- asks (snd . fromJust . join . preview (#datatypeInfo % ix tn % #baseFunctor))+      bfbb <- instantiateBFBB rawBFBB+      handlers' <- Vector.toList <$> traverse cleanupHandler handlers+      tyDict <- asks (view #datatypeInfo)+      case checkApp tyDict bfbb (Just <$> handlers') of+        Right appliedBfbb -> do+          result <- undoRenameM appliedBfbb+          refTo $ AValNode result (MatchInternal scrutinee handlers)+        Left err' -> throwError . UnificationError $ err'+      where+        instantiateBFBB :: ValT AbstractTy -> m (CompT Renamed)+        instantiateBFBB bfbb = do+          -- we have a BFBB like:+          -- listBB :: forall a r . r -> <a -> r -> !r> -> !r+          -- And we need to:+          --   1. Instantiate all of the type arguments to the original datatype (e.g. the 'a' in List a)+          --      into the BFBB+          --   2. Instantiate the *last* tyvar bound by the BBBF to the type of the original datatype+          --      giving us, e.g. ListF a (List a)+          scope <- askScope+          renamedBFBB <- case runRenameM scope (renameValT bfbb) of+            Left err' -> throwError $ MatchRenameBBFail err'+            Right res -> pure res+          -- The type constructor for the base-functor variant of the scrutinee type.+          let scrut = Datatype tn tyConArgs+          let scrutF = Datatype (TyName $ rawTn <> "_F") (Vector.snoc tyConArgs scrut)+          -- These are arguments to the original type constructor plus the snoc'd original type.+          -- E.g. if we have:+          --      Scrutinee: List Int+          --   this should be:+          --   [Int, List Int]+          let bfInstArgs = Vector.snoc tyConArgs scrutF+          renamedArgs <- case runRenameM scope (traverse renameValT bfInstArgs) of+            Left err' -> throwError $ MatchRenameTyConArgFail err'+            Right res -> pure res+          let subs :: Vector (Index "tyvar", ValT Renamed)+              subs = Vector.imap (\i v -> (fromJust . preview intIndex $ i, v)) renamedArgs+              subbed = foldl' (\bbf (i, v) -> substitute i v bbf) renamedBFBB subs+          case subbed of+            ThunkT bfComp -> pure bfComp+            other -> throwError $ MatchNonThunkBBF other++    -- Unwraps a thunk handler if it is a handler for a nullary constructor.+    cleanupHandler :: Ref -> m (ValT Renamed)+    cleanupHandler r =+      renameArg r >>= \case+        Nothing ->+          throwError $ MatchErrorAsHandler r+        Just hVal -> case hVal of+          hdlr@(ThunkT (CompT cnt (ReturnT v)))+            | cnt == count0 -> pure v+            | otherwise -> throwError $ MatchPolymorphicHandler hdlr+          other -> pure other++    goNonRecursive :: TyName -> Vector (ValT AbstractTy) -> m Id+    goNonRecursive tn tyConArgs = do+      rawBBF <- asks (fromJust . preview (#datatypeInfo % ix tn % #bbForm))+      (instantiatedBBF :: CompT Renamed) <- instantiateBB rawBBF tyConArgs+      handlers' <- Vector.toList <$> traverse cleanupHandler handlers+      tyDict <- asks (view #datatypeInfo)+      case checkApp tyDict instantiatedBBF (Just <$> handlers') of+        Right appliedBBF -> do+          result <- undoRenameM appliedBBF+          refTo $ AValNode result (MatchInternal scrutinee handlers)+        Left err' -> throwError . UnificationError $ err'+      where+        instantiateBB :: Maybe (ValT AbstractTy) -> Vector (ValT AbstractTy) -> m (CompT Renamed)+        instantiateBB Nothing _ = throwError $ MatchNoBBForm tn+        instantiateBB (Just bb) tyArgs = do+          scope <- askScope+          renamedBB <- case runRenameM scope (renameValT bb) of+            Left err' -> throwError $ MatchRenameBBFail err'+            Right res -> pure res+          renamedArgs <- case runRenameM scope (traverse renameValT tyArgs) of+            Left err' -> throwError $ MatchRenameTyConArgFail err'+            Right res -> pure res+          let subs :: Vector (Index "tyvar", ValT Renamed)+              subs = Vector.imap (\i v -> (fromJust . preview intIndex $ i, v)) renamedArgs+              subbed = foldl' (\bbf (i, v) -> substitute i v bbf) renamedBB subs+          case subbed of+            ThunkT bbComp -> pure bbComp+            other -> throwError $ MatchNonThunkBBF other+ -- Helpers +-- Note (Koz, 13/08/2025): We need this procedure specifically for `cata`. The+-- reason for this has to do with how we construct the 'base functor form' of+-- the value to be torn down by the catamorphism, in order to use the+-- unification machinery to get the type of the final result.+--+-- To be specific, suppose we have `<List_F r (Maybe r) -> !Maybe r>` as our algebra+-- argument (where `r` is some rigid), and `List r` as the value to be torn+-- down. If we assume the rigid is bound one scope away, `r`'s DeBruijn index+-- will be `S Z` for+-- the value to be torn down, but `S (S Z)` for the algebra argument. The way+-- our approach works is:+--+-- 1. Look at the algebra argument, specifically the base functor type. Take its+--    last type argument, which we will call `last`.+-- 2. Determine the base functor for the value to be torn down. Cook up a new+--    instance of the base functor type, copying all the type arguments from the+--    value to be torn down in the same order. Then put `last` at the end.+-- 3. Force the algebra argument thunk, then try and apply the result of Step 2+--    to that.+--+-- Following the steps above for our example, we would proceed as follows:+--+-- 1. Set `last` as `Maybe r`.+-- 2. Cook up `List_F r (Maybe r)`. Note that this matches what the algebra+--    expects.+-- 3. Use the unifier with `List_F r (Maybe r) -> !Maybe r`, applying the+--    argument `List_F r (Maybe r)` from Step 2.+--+-- However, if `last` is a rigid, we have an 'off by one error'. To see why,+-- consider the form of the algebra argument:+--+-- `ThunkT . Comp0 $ Datatype "List_F" [tyvar (S (S Z)) ix0, ....`+--+-- However, `tyvar (S (S Z)) ix0` is not valid in the scope of the value to be+-- torn down: that same rigid would have DeBruijn index `S Z` there instead.+-- This applies the same if the tyvar is part of a datatype.+--+-- As we prohibit non-rigid algebras, this requires us to lower the DeBruijn+-- index by one for our process.+stepDownDB :: ValT AbstractTy -> ValT AbstractTy+stepDownDB = \case+  Abstraction (BoundAt db i) -> case db of+    -- This is impossible, so we just return it unmodified+    Z -> Abstraction (BoundAt db i)+    (S db') -> Abstraction (BoundAt db' i)+  Datatype tyName tyArgs -> Datatype tyName . fmap stepDownDB $ tyArgs+  x -> x+ renameArg ::   forall (m :: Type -> Type).-  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>   Ref ->   m (Maybe (ValT Renamed)) renameArg r =-  typeRef r >>= \case-    CompNodeType t -> throwError . ApplyCompType $ t-    ValNodeType t -> case runRenameM . renameValT $ t of-      Left err' -> throwError . RenameArgumentFailed t $ err'-      Right renamed -> pure . Just $ renamed-    ErrorNodeType -> pure Nothing+  askScope >>= \scope ->+    typeRef r >>= \case+      CompNodeType t -> throwError . ApplyCompType $ t+      ValNodeType t -> case runRenameM scope . renameValT $ t of+        Left err' -> throwError . RenameArgumentFailed t $ err'+        Right renamed -> pure . Just $ renamed+      ErrorNodeType -> pure Nothing  checkEncodingWithInfo ::   forall (a :: Type) (m :: Type -> Type).@@ -689,3 +1215,146 @@ checkEncodingWithInfo tyDict valT = case checkEncodingArgs (view (#originalDecl % #datatypeEncoding)) tyDict valT of   Left encErr -> throwError $ EncodingError encErr   Right {} -> pure ()++tryApply ::+  forall (m :: Type -> Type).+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  CompT AbstractTy ->+  ValT AbstractTy ->+  m (ValT AbstractTy)+tryApply algebraT argT =+  askScope >>= \scope -> case runRenameM scope . renameCompT $ algebraT of+    Left err' -> throwError . RenameFunctionFailed algebraT $ err'+    Right renamedAlgebraT -> case runRenameM scope . renameValT $ argT of+      Left err' -> throwError . RenameArgumentFailed argT $ err'+      Right renamedArgT -> do+        tyDict <- asks (view #datatypeInfo)+        case checkApp tyDict renamedAlgebraT [Just renamedArgT] of+          Left err' -> throwError . UnificationError $ err'+          Right resultT -> undoRenameM resultT++-- Putting this here to reduce chance of annoying manual merge (will move later)++-- | Wrapper around an `Arg` that we know represents an in-scope type variable.+-- @since 1.2.0+data BoundTyVar = BoundTyVar DeBruijn (Index "tyvar")+  deriving stock+    ( -- @since 1.2.0+      Show,+      -- @since 1.2.0+      Eq,+      -- @since 1.2.0+      Ord+    )++-- | Given a DeBruijn index (designating scope) and positional index (designating+-- which variable in that scope we are interested in), retrieve an in-scope type+-- variable.+--+-- This will error if we request a type variable in a scope that doesn't exist,+-- or at a position that doesn't exist in that scope.+--+-- @since 1.2.0+boundTyVar ::+  forall (m :: Type -> Type).+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  DeBruijn ->+  Index "tyvar" ->+  m BoundTyVar+boundTyVar scope index = do+  let scopeAsInt = review asInt scope+      indexAsWord :: Word32+      indexAsWord = fromIntegral $ review intIndex index+  tyVarInScope <-+    asks (preview (#scopeInfo % #argumentInfo % ix scopeAsInt % _1)) >>= \case+      Nothing -> pure False+      Just varsBoundAtScope ->+        -- varsBoundAtScope is the count of the CompT binding context verbatim+        if varsBoundAtScope <= 0+          then pure False+          else pure $ indexAsWord < varsBoundAtScope+  if tyVarInScope+    then pure (BoundTyVar scope index)+    else throwError $ OutOfScopeTyVar scope index++-- To avoid annoying code duplication++-- Helper to avoid having to manually catch and rethrow the error+undoRenameM ::+  forall (m :: Type -> Type).+  (MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  ValT Renamed ->+  m (ValT AbstractTy)+undoRenameM val = do+  scope <- asks (fmap fst . view (#scopeInfo % #argumentInfo))+  case undoRename scope val of+    Left err' -> throwError $ UndoRenameFailure err'+    Right renamed -> pure renamed++askScope ::+  forall (m :: Type -> Type).+  (MonadReader ASGEnv m) =>+  m (Vector Word32)+askScope = asks (fmap fst . view (#scopeInfo % #argumentInfo))++-- Runs a UnifyM computation in our abstract monad. Again, largely to avoid superfluous code+-- duplication.+liftUnifyM ::+  forall (m :: Type -> Type) (a :: Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  UnifyM a ->+  m a+liftUnifyM act = do+  tyDict <- asks (view #datatypeInfo)+  case runUnifyM tyDict act of+    Left e -> throwError $ UnificationError e+    Right res -> pure res++-- Utility functions for ASG construction. These are not strictly necessary, but are extremely convenient.++-- | Constructs a datatype value at given constructor. This is different to+-- 'dataConstructor', as it doesn't produce a thunk.+--+-- The third argument is a 'Vector' of values to \'fill in\' all the fields+-- required by the stated constructor. The fourth argument is a 'Vector' of+-- \'type instantiations\', which allow \'concretification\' of any lingering+-- polymorphic type variables which are not determined by the field values given+-- as the third argument.+--+-- = Example+--+-- Consider @Left 3@. In this case, the field only determines the first type+-- argument to the @Either@ data type, and if we used 'dataConstructor', we+-- would be left with a thunk of type @<forall a . !Either Integer a>@. Using+-- 'ctor', we can immediately specify what @a@ should be, and unwrap the thunk.+--+-- @since 1.2.0+ctor ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  TyName ->+  ConstructorName ->+  Vector.Vector Ref ->+  Vector.Vector (Wedge BoundTyVar (ValT Void)) ->+  m Id+ctor tn cn args instTys = do+  dataThunk <- dataConstructor tn cn args+  dataForced <- force (AnId dataThunk)+  app dataForced mempty instTys++-- | As 'lam', but produces a thunk value instead of a computation.+--+-- @since 1.2.0+lazyLam ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ASGEnv m) =>+  CompT AbstractTy ->+  m Ref ->+  m Id+lazyLam expected bodyComp = lam expected bodyComp >>= thunk++-- | Helper to avoid using 'Vector.fromList' when defining data types.+--+-- @since 1.2.0+dtype :: TyName -> [ValT AbstractTy] -> ValT AbstractTy+dtype tn = Datatype tn . Vector.fromList

@@ -35,6 +35,7 @@     isRecursiveChildOf,     hasRecursive,     everythingOf,+    mapValT,   ) where 

@@ -22,6 +22,7 @@     count2,     ix3,     count3,+    wordCount,   ) where @@ -31,6 +32,7 @@ import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum)) import Data.Word (Word32) import GHC.TypeLits (Symbol)+import Optics.Core (Lens', lens) import Optics.Prism (Prism', prism) import Test.QuickCheck (Arbitrary) @@ -146,6 +148,11 @@   prism     (fromIntegral . coerce @_ @Word32)     (\i -> maybe (Left i) (Right . Count) . toIntegralSized $ i)++-- | We use the Word32 directly during renaming, and a Lens is more appropriate+-- than a Prism if we're working with Word32s+wordCount :: forall (ofWhat :: Symbol). Lens' (Count ofWhat) Word32+wordCount = lens (\(Count x) -> x) (\_ w -> Count w)  -- | Helper for a count of zero items. --

@@ -186,8 +186,18 @@  -} --- 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)+-- | Indicates that we tried to instantiate a polymorphic data type using a type+-- whose encoding is incompatible. The most common case of this is when we have+-- a \'polymorphic\' data type that uses some kind of @Data@ encoding and we try+-- to instantiate it with a type which has a SOP encoding.+--+-- @since 1.2.0+data EncodingArgErr a+  = -- | First field is a constructor name for the type we tried to instantiate,+    -- second field is the bad instantiator.+    --+    -- @since 1.2.0+    EncodingArgMismatch TyName (ValT a)   deriving stock (Show, Eq)  -- | Verifies that a datatype (third argument) is valid according to its stated

@@ -1,3 +1,5 @@+{-# LANGUAGE MultiWayIf #-}+ module Covenant.Internal.Rename   ( RenameM,     RenameError (..),@@ -7,17 +9,21 @@     renameCompT,     undoRename,     renameDatatypeInfo,+    UnRenameM,+    UnRenameError (..),+    runUnRenameM,   ) where -import Control.Monad (unless) import Control.Monad.Except   ( ExceptT,+    MonadError,     runExceptT,     throwError,   ) import Control.Monad.Reader-  ( Reader,+  ( MonadReader,+    Reader,     asks,     local,     runReader,@@ -29,8 +35,8 @@     modify,   ) import Covenant.Data (DatatypeInfo (DatatypeInfo))-import Covenant.DeBruijn (DeBruijn (S, Z), asInt)-import Covenant.Index (Count, Index, intCount, intIndex)+import Covenant.DeBruijn (DeBruijn (Z), asInt)+import Covenant.Index (Count, Index, intIndex, wordCount) import Covenant.Internal.Type   ( AbstractTy (BoundAt),     CompT (CompT),@@ -43,17 +49,16 @@ import Data.Bitraversable (Bitraversable (bitraverse)) import Data.Coerce (coerce) import Data.Kind (Type)-import Data.Tuple.Optics (_1) import Data.Vector (Vector) import Data.Vector qualified as Vector import Data.Vector.NonEmpty qualified as NonEmpty-import Data.Word (Word64)+import Data.Word (Word32, Word64) import Optics.Core   ( A_Lens,     LabelOptic (labelOptic),-    ix,     lens,     over,+    preview,     review,     set,     to,@@ -62,12 +67,14 @@   )  -- Used during renaming. Contains a source of fresh indices for wildcards, as--- well as tracking:+-- well as: ----- 1. How many variables are bound by each scope;--- 2. Which of these variables have been noted as used; and--- 3. A unique identifier for each scope (for wildcards).-data RenameState = RenameState Word64 (Vector (Vector Bool, Word64))+-- 1. The first Word64 argument is the "source of freshness" for WildCards+-- 2. The second Word64 argument is the inherited scope size+-- 3. The *size* of the vector tracks the current scope size (the enclosing scope is inherited, but it may grow during renaming)+-- 4. The first element of the tuple in the vector is the *count* of TyVars bound in each scope. (Note: It is therefore 1 greater than the index)+-- 5. The second element of the tuple in the vector is the unique identifier for wildcards in each scope.+data RenameState = RenameState Word64 Word32 (Vector (Word32, Word64))   deriving stock (Eq, Show)  -- Note (Koz, 11/04/2025): We need this field as a source of unique identifiers@@ -94,35 +101,65 @@   {-# INLINEABLE labelOptic #-}   labelOptic =     lens-      (\(RenameState x _) -> x)-      (\(RenameState _ y) x' -> RenameState x' y)+      (\(RenameState x _ _) -> x)+      (\(RenameState _ b c) a' -> RenameState a' b c) --- The 'outer' vector represents a stack of scopes. Each entry is a combination--- of a vector of used variables (length is equal to the number of variables--- bound by that scope), together with a unique identifier not only for that--- scope, but also the `step` into that scope, as required by wildcard renaming. instance-  (k ~ A_Lens, a ~ Vector (Vector Bool, Word64), b ~ Vector (Vector Bool, Word64)) =>+  (k ~ A_Lens, a ~ Word32, b ~ Word32) =>+  LabelOptic "inheritedScope" k RenameState RenameState a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(RenameState _ x _) -> x)+      (\(RenameState a _ c) b' -> RenameState a b' c)++instance+  (k ~ A_Lens, a ~ Vector (Word32, Word64), b ~ Vector (Word32, Word64)) =>   LabelOptic "tracker" k RenameState RenameState a b   where   {-# INLINEABLE labelOptic #-}   labelOptic =     lens-      (\(RenameState _ y) -> y)-      (\(RenameState x _) y' -> RenameState x y')+      (\(RenameState _ _ y) -> y)+      (\(RenameState x y _) z' -> RenameState x y z')  -- | Ways in which the renamer can fail. -- -- @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-    -- the index that was requested.+    -- abstraction doesn't exist, but where the scope itself /does/ exist.+    -- Put another way: This gets thrown when the argument index of an+    -- abstraction inconsistent with the `Count` of the scope its DB index refers to.+    -- First field is the true level, second is the index that was requested.     ---    -- @since 1.0.0+    -- @since 1.2.0     InvalidAbstractionReference Int (Index "tyvar")+  | -- | An abstraction refers to a scope which does not exist. That is: The abstraction's+    -- DeBruijn index points to a scope "higher than" the top-level scope.+    --+    -- @since 1.2.0+    InvalidScopeReference Int (Index "tyvar")   deriving stock (Eq, Show) +-- | Ways in which the un-renamer can fail.+--+-- @since 1.2.0+data UnRenameError+  = -- | We tried to un-rename a wildcard. This means something has gone very wrong internally.+    -- @since 1.2.0+    UnRenameWildCard Renamed+  | -- | We received a negative DeBruijn in our true level calculation. This is impossible, and indicates another+    --   internal malfunction or bug+    NegativeDeBruijn Int+  deriving stock+    ( -- | @since 1.2.0+      Eq,+      -- | @since 1.2.0+      Show+    )+ -- | A \'renaming monad\' which allows us to convert type representations from -- ones that use /relative/ abstraction labelling to /absolute/ abstraction -- labelling.@@ -156,15 +193,74 @@     )     via (ExceptT RenameError (State RenameState)) +-- | The portions of the RenameState needed for unrenaming. Lacks the unique indicator for+-- wildcards, since trying to un-rename a wildcard is an error.+data UnRenameCxt = UnRenameCxt Word32 (Vector Word32)+  deriving stock+    ( -- @since 1.2.0+      Show,+      -- @since 1.2.0+      Eq,+      -- @since 1.2.0+      Ord+    )++instance+  (k ~ A_Lens, a ~ Word32, b ~ Word32) =>+  LabelOptic "inheritedScopeSize" k UnRenameCxt UnRenameCxt a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(UnRenameCxt x _) -> x)+      (\(UnRenameCxt _ y) x' -> UnRenameCxt x' y)++instance+  (k ~ A_Lens, a ~ Vector Word32, b ~ Vector Word32) =>+  LabelOptic "scopeInfo" k UnRenameCxt UnRenameCxt a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(UnRenameCxt _ y) -> y)+      (\(UnRenameCxt x _) y' -> UnRenameCxt x y')++-- | @since 1.2.0+newtype UnRenameM (a :: Type) = UnRenameM (ExceptT UnRenameError (Reader UnRenameCxt) a)+  deriving+    ( -- | @since 1.2.0+      Functor,+      -- | @since 1.2.0+      Applicative,+      -- | @since 1.2.0+      Monad,+      -- | @since 1.2.0+      MonadReader UnRenameCxt,+      -- | @since 1.2.0+      MonadError UnRenameError+    )+    via (ExceptT UnRenameError (Reader UnRenameCxt))+ -- | Execute a renaming computation. ----- @since 1.0.0+-- @since 1.2.0 runRenameM ::   forall (a :: Type).+  Vector Word32 ->   RenameM a ->   Either RenameError a-runRenameM (RenameM comp) = evalState (runExceptT comp) . RenameState 0 $ Vector.empty+runRenameM scopeInfo (RenameM comp) =+  evalState (runExceptT comp)+    . RenameState 0 (fromIntegral $ Vector.length scopeInfo)+    $ Vector.map (,0) scopeInfo +runUnRenameM ::+  forall (a :: Type).+  UnRenameM a ->+  Vector Word32 ->+  Either UnRenameError a+runUnRenameM (UnRenameM comp) inherited = runReader (runExceptT comp) $ UnRenameCxt (fromIntegral $ Vector.length inherited) inherited+ -- | Rename a computation type. -- -- @since 1.0.0@@ -211,8 +307,10 @@     renameCtor :: Constructor AbstractTy -> RenameM (Constructor Renamed)     renameCtor (Constructor cn args) = Constructor cn <$> traverse renameValT args +-- REVIEW: I am not sure if we really want the scope arg to runRenameM to be `mempty`.+--         If something breaks w/ BB forms or datatypes, look here. renameDatatypeInfo :: DatatypeInfo AbstractTy -> Either RenameError (DatatypeInfo Renamed)-renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM $ do+renameDatatypeInfo (DatatypeInfo ogDecl baseFStuff bb) = runRenameM mempty $ do   ogDecl' <- renameDataDecl ogDecl   baseFStuff' <- traverse (bitraverse renameDataDecl renameValT) baseFStuff   bb' <- traverse renameValT bb@@ -221,60 +319,65 @@ -- 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.-undoRename :: ValT Renamed -> ValT AbstractTy-undoRename t = runReader (go t) 1+--+-- @since 1.2.0+undoRename :: Vector Word32 -> ValT Renamed -> Either UnRenameError (ValT AbstractTy)+undoRename scope t = runUnRenameM (go t) scope   where-    go :: ValT Renamed -> Reader Int (ValT AbstractTy)+    go :: ValT Renamed -> UnRenameM (ValT AbstractTy)     go = \case       Abstraction t' ->         Abstraction <$> case t' of-          Unifiable index -> BoundAt <$> trueLevelToDB 1 <*> pure index-          Rigid trueLevel index -> BoundAt <$> trueLevelToDB trueLevel <*> pure index-          Wildcard _ trueLevel index -> BoundAt <$> trueLevelToDB trueLevel <*> pure index+          Rigid trueLevel index -> do+            db <- unTrueLevel trueLevel+            pure $ BoundAt db index+          w@(Wildcard {}) -> throwError $ UnRenameWildCard w+          Unifiable index -> pure $ BoundAt Z index       ThunkT (CompT abses (CompTBody xs)) ->-        ThunkT . CompT abses . CompTBody <$> local (+ 1) (traverse go xs)+        ThunkT+          . CompT abses+          . CompTBody+          <$> local (over #scopeInfo (Vector.cons $ view wordCount abses)) (traverse go xs)       BuiltinFlat t' -> pure . BuiltinFlat $ t'       Datatype tn args -> Datatype tn <$> traverse go args --- Helpers--trueLevelToDB :: Int -> Reader Int DeBruijn-trueLevelToDB trueLevel = asks (go . subtract trueLevel)-  where-    go :: Int -> DeBruijn-    go = \case-      0 -> Z-      n -> S . go $ n - 1+    unTrueLevel :: Int -> UnRenameM DeBruijn+    unTrueLevel tl = do+      trackerLen <- asks (Vector.length . view #scopeInfo)+      inheritedSize <- asks (fromIntegral . view #inheritedScopeSize)+      let db = trackerLen - 1 - inheritedSize - tl+      case preview asInt db of+        Nothing -> throwError $ NegativeDeBruijn db+        Just res -> pure res  renameAbstraction :: AbstractTy -> RenameM Renamed renameAbstraction (BoundAt scope index) = RenameM $ do-  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - review asInt scope)+  inheritedScopeSize <- gets (fromIntegral . view #inheritedScope)+  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - 1 - inheritedScopeSize - 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,-    -- the variable is rigid.-    Nothing -> pure . Rigid trueLevel $ index-    Just (occursTracker, uniqueScopeId) -> case occursTracker Vector.!? asIntIx of-      Nothing -> throwError . InvalidAbstractionReference trueLevel $ index-      Just beenUsed -> do-        -- Note that this variable has occurred-        unless beenUsed (modify (noteUsed scope index))-        pure $-          if trueLevel == 1-            -- This is a unifiable variable-            then Unifiable index-            -- This is a wildcard variable-            else Wildcard uniqueScopeId trueLevel index+    Nothing -> throwError . InvalidScopeReference trueLevel $ index+    Just (occursTracker, uniqueScopeId) ->+      if+        | not (checkVarIxExists asIntIx occursTracker) -> throwError . InvalidAbstractionReference trueLevel $ index+        | trueLevel == 0 -> pure $ Unifiable index+        | trueLevel < 0 -> pure $ Rigid trueLevel index+        | otherwise -> pure $ Wildcard uniqueScopeId trueLevel index+  where+    checkVarIxExists :: Int -> Word32 -> Bool+    checkVarIxExists i wCount = fromIntegral i < wCount +-- Helpers+ -- Given a number of abstractions bound by a scope, modify the state to track -- that scope. stepUpScope :: Count "tyvar" -> RenameState -> RenameState stepUpScope abses x =   let fresh = view #idSource x-      absesI = review intCount abses+      absesW = view wordCount abses       -- Label (speculatively) the current scope 'step' with a unique value.-      entry = (Vector.replicate absesI False, fresh)+      entry = (absesW, fresh)    in -- Ensure that our source of fresh identifiers is incremented       over #tracker (Vector.cons entry) . set #idSource (fresh + 1) $ x @@ -286,9 +389,3 @@ -- achieve our goal of renaming wildcards. dropDownScope :: RenameState -> RenameState dropDownScope = over #tracker Vector.tail---- Given a pair of DeBruijn index and positional index for a variable, note that--- we've seen this variable.-noteUsed :: DeBruijn -> Index "tyvar" -> RenameState -> RenameState-noteUsed scope index =-  set (#tracker % ix (review asInt scope) % _1 % ix (review intIndex index)) True

@@ -20,11 +20,19 @@ 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.Rename (RenameError, UnRenameError)+import Covenant.Internal.Type+  ( AbstractTy,+    BuiltinFlatT,+    CompT,+    TyName,+    ValT,+  ) import Covenant.Internal.Unification (TypeAppError) import Covenant.Prim (OneArgFunc, SixArgFunc, ThreeArgFunc, TwoArgFunc)+import Covenant.Type (ConstructorName, PlutusDataConstructor, Renamed) import Data.Kind (Type)+import Data.Set qualified as Set import Data.Vector (Vector) import Data.Word (Word64) @@ -94,8 +102,8 @@     ReturnCompType (CompT AbstractTy)   | -- | The body of a lambda results in a value-typed node, which isn't allowed.     ---    -- @since 1.0.0-    LambdaResultsInValType (ValT AbstractTy)+    -- @since 1.2.0+    LambdaResultsInCompType (CompT AbstractTy)   | -- | The body of a lambda results in a computation-typed node which isn't     -- a return, which isn't allowed.     --@@ -118,10 +126,141 @@     --     -- @since 1.0.0     WrongReturnType (ValT AbstractTy) (ValT AbstractTy)-  | -- @since 1.1.0--    -- | Wraps an encoding argument mismatch error from KindCheck+  | -- | Wraps an encoding argument mismatch error from KindCheck+    --+    -- @since 1.1.0     EncodingError (EncodingArgErr AbstractTy)+  | -- | The first argument to a catamorphism wasn't an algebra, as+    -- it had the wrong arity.+    --+    -- @since 1.2.0+    CataAlgebraWrongArity Int+  | -- | The first argument to a catamorphism wasn't an algebra.+    --+    -- @since 1.1.0+    CataNotAnAlgebra ASGNodeType+  | -- | The second argument to a catamorphism wasn't a value type.+    --+    -- @since 1.1.0+    CataApplyToNonValT ASGNodeType+  | -- The algebra given to this catamorphism is not rigid (that is, its+    -- computation type binds variables).+    --+    -- @since 1.2.0+    CataNonRigidAlgebra (CompT AbstractTy)+  | -- | The second argument to a catamorphism is a builtin type, but not one+    -- we can eliminate with a catamorphism.+    --+    -- @since 1.1.0+    CataWrongBuiltinType BuiltinFlatT+  | -- | The second argument to a catamorphism is a value type, but not one we+    -- can eliminate with a catamorphism. Usually, this means it's a variable.+    --+    -- @since 1.1.0+    CataWrongValT (ValT AbstractTy)+  | -- | We requested a catamorphism for a type that doesn't exist.+    --+    -- @since 1.2.0+    CataNoSuchType TyName+  | -- | We requested a catamorphism for a type without a base functor.+    --+    -- @since 1.2.0+    CataNoBaseFunctorForType TyName+  | -- | The provided algebra is not suitable for the given type.+    --+    -- @since 1.1.0+    CataUnsuitable (CompT AbstractTy) (ValT AbstractTy)+  | -- | Someone attempted to construct a tyvar using a DB index or argument position+    --   which refers to a scope (or argument) that does not exist.+    --+    -- @since 1.2.0+    OutOfScopeTyVar DeBruijn (Index "tyvar")+  | -- | We failed to rename an "instantiation type" supplied to 'Covenant.ASG.app'.+    --+    -- @since 1.2.0+    FailedToRenameInstantiation RenameError+  | -- | Un-renaming failed.+    --+    -- @since 1.2.0+    UndoRenameFailure UnRenameError+  | -- | We tried to look up the 'DatatypeInfo' corresponding to a 'TyName' and came up empty handed.+    --+    -- @since 1.2.0+    TypeDoesNotExist TyName+  | -- | We tried to rename a 'DatatypeInfo' and failed.+    --+    -- @since 1.2.0+    DatatypeInfoRenameError RenameError+  | -- | We tried to look up a constructor for a given type. The type exists, but the constructor does not.+    --+    -- @since 1.2.0+    ConstructorDoesNotExistForType TyName ConstructorName+  | -- | When using the helper function to construct an introduction form, the type and constructor exist but the+    --   number of fields provided as an argument does not match the number of declared fields.+    --   The 'Int' is the /incorrect/ number of /supplied/ fields.+    --+    -- @since 1.2.0+    IntroFormWrongNumArgs TyName ConstructorName Int+  | -- | The user passed an error node as an argument to a datatype into form. We return the arguments given+    --   to 'Covenant.ASG.dataConstructor' in the error.+    --+    -- @since 1.2.0+    IntroFormErrorNodeField TyName ConstructorName (Vector Ref)+  | -- | The user tried to construct an introduction form using a Plutus @Data@ constructor not found in the+    --   opaque datatype declaration.+    --+    -- @since 1.2.0+    UndeclaredOpaquePlutusDataCtor (Set.Set PlutusDataConstructor) ConstructorName+  | -- | The user tried to construct an introduction form with a valid Plutus @Data@ constructor, but+    --   supplied a 'Covenant.ASG.Ref' to a field of the wrong type.+    --+    -- @since 1.2.0+    InvalidOpaqueField (Set.Set PlutusDataConstructor) ConstructorName [ValT Renamed]+  | -- The user tried to match on (i.e. use as a scrutinee) a node that wasn't a value.+    --+    -- @since 1.2.0+    MatchNonValTy ASGNodeType+  | -- | Internal error: we found a base functor Boehm-Berrarducci form that isn't a thunk after instantiation+    --   during pattern matching.Somehow we got a BFBB that is something other than a thunk after instantiation during pattern matching.+    --+    --   This should not normally happen: let us know if you see this error!+    --+    -- @since 1.2.0+    MatchNonThunkBBF (ValT Renamed)+  | -- | We encountered a rename error during pattern matching. This will refer+    -- to either the Boehm-Berrarducci form, or the base functor Boehm-Berrarducci form, depending on what type we tried to match.+    --+    -- @since 1.2.0+    MatchRenameBBFail RenameError+  | -- | This indicates that we encountered an error when renaming the arguments to the type constructor of the+    --   /scrutinee type/ during pattern matching. That is, if we're matching on @Either a b@, this means that+    --   either @a@ or @b@ failed to rename.+    --+    --  This should not normally happen: let us know if you see this error!+    --+    -- @since 1.2.0+    MatchRenameTyConArgFail RenameError+  | -- | A user tried to use a polymorphic handler in a pattern match, which is not currently allowed.+    --+    -- @since 1.2.0+    MatchPolymorphicHandler (ValT Renamed)+  | -- | We tried to use an error node as a pattern match handler.+    --+    -- @since 1.2.0+    MatchErrorAsHandler Ref+  | -- | The non-recursive branch of a pattern match needs a Boehm-Berrarducci form for the given type+    -- name, but it doesn't exist.+    --+    -- @since 1.2.0+    MatchNoBBForm TyName+  | -- | Someone tried to match on something that isn't a datatype.+    --+    -- @since 1.2.0+    MatchNonDatatypeScrutinee (ValT AbstractTy)+  | -- | The scrutinee is a datatype, be don't have it in our datatype dictionary.+    --+    -- @since 1.2.0+    MatchNoDatatypeInfo TyName   deriving stock     ( -- | @since 1.0.0       Eq,@@ -219,9 +358,8 @@   | Builtin2Internal TwoArgFunc   | Builtin3Internal ThreeArgFunc   | Builtin6Internal SixArgFunc-  | LamInternal Id+  | LamInternal Ref   | ForceInternal Ref-  | ReturnInternal Ref   deriving stock     ( -- | @since 1.0.0       Eq,@@ -238,6 +376,12 @@   = LitInternal AConstant   | AppInternal Id (Vector Ref)   | ThunkInternal Id+  | -- | @since 1.1.0+    CataInternal Ref Ref+  | -- | @since 1.2.0+    DataConstructorInternal TyName ConstructorName (Vector Ref)+  | -- | @since 1.2.0+    MatchInternal Ref (Vector Ref)   deriving stock     ( -- | @since 1.0.0       Eq,

@@ -21,6 +21,7 @@     naturalBaseFunctor,     negativeBaseFunctor,     byteStringBaseFunctor,+    arity,   ) where @@ -158,7 +159,9 @@       -- | @since 1.0.0       Ord,       -- | @since 1.0.0-      Show+      Show,+      -- | @since 1.2.0+      Functor     )  -- | @since 1.0.0@@ -179,7 +182,9 @@       -- | @since 1.0.0       Ord,       -- | @since 1.0.0-      Show+      Show,+      -- | @since 1.2.0+      Functor     )  -- | @since 1.0.0@@ -192,6 +197,13 @@ instance Pretty (CompT Renamed) where   pretty = runPrettyM . prettyCompTWithContext +-- | Determine the arity of a computation type: that is, how many arguments a+-- function of this type must be given.+--+-- @since 1.0.0+arity :: forall (a :: Type). CompT a -> Int+arity (CompT _ (CompTBody xs)) = NonEmpty.length xs - 1+ -- | The name of a data type. This refers specifically to non-\'flat\' types -- either provided by the ledger, or defined by the user. --@@ -230,7 +242,9 @@       -- | @since 1.0.0       Ord,       -- | @since 1.0.0-      Show+      Show,+      -- | @since 1.2.0+      Functor     )  -- | @since 1.0.0

@@ -1,10 +1,16 @@ {-# LANGUAGE CPP #-}+{-# LANGUAGE MultiWayIf #-}  module Covenant.Internal.Unification   ( TypeAppError (..),     checkApp,     runUnifyM,     UnifyM,+    -- These are exported for use with ASG helpers, largely (but not exclusively) the intro forms helper+    unify,+    substitute,+    fixUp,+    reconcile,   ) where @@ -15,7 +21,7 @@ #endif import Control.Monad.Except (MonadError, catchError, throwError) import Control.Monad.Reader (MonadReader, ReaderT (runReaderT), ask)-import Covenant.Data (DatatypeInfo)+import Covenant.Data (DatatypeInfo, mkDatatypeInfo) import Covenant.Index (Index, intCount, intIndex) import Covenant.Internal.Rename (RenameError, renameDatatypeInfo) import Covenant.Internal.Type@@ -24,8 +30,11 @@     CompT (CompT),     CompTBody (CompTBody),     Renamed (Rigid, Unifiable, Wildcard),-    TyName,+    TyName (TyName),     ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+    byteStringBaseFunctor,+    naturalBaseFunctor,+    negativeBaseFunctor,   ) import Data.Kind (Type) import Data.Map (Map)@@ -35,6 +44,7 @@ import Data.Set (Set) import Data.Set qualified as Set import Data.Text (Text)+import Data.Text qualified as Text import Data.Vector (Vector) import Data.Vector qualified as Vector import Data.Vector.NonEmpty (NonEmptyVector)@@ -76,6 +86,9 @@     --     -- @since 1.1.0     ImpossibleHappened Text+  | -- Could not reconcile two assignments with the same index+    -- @since 1.2.0+    CouldNotReconcile (Index "tyvar") (ValT Renamed) (ValT Renamed)   deriving stock     ( -- | @since 1.0.0       Eq,@@ -101,10 +114,42 @@ lookupDatatypeInfo ::   TyName ->   UnifyM (DatatypeInfo Renamed)-lookupDatatypeInfo tn =+lookupDatatypeInfo tn@(TyName rawTyName) =   ask >>= \tyDict -> case preview (ix tn) tyDict of-    Nothing -> throwError $ NoDatatypeInfo tn-    Just dti -> either (throwError . DatatypeInfoRenameFailed tn) pure $ renameDatatypeInfo dti+    Nothing -> checkForBaseFunctor tyDict+    Just dti -> renamedToUnify . renameDatatypeInfo $ dti+  where+    checkForBaseFunctor :: Map TyName (DatatypeInfo AbstractTy) -> UnifyM (DatatypeInfo Renamed)+    checkForBaseFunctor tyDict = case Text.stripSuffix "_F" rawTyName of+      Nothing -> throwError . NoDatatypeInfo $ tn+      Just rawTyNameStub ->+        if+          -- Note (Koz, 12/08/2025): None of these specific cases should _ever_+          -- fail. Thus, `fromRight` is safe here.+          | rawTyNameStub == "Natural" ->+              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ naturalBaseFunctor+          | rawTyNameStub == "Negative" ->+              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ negativeBaseFunctor+          | rawTyNameStub == "ByteString" ->+              renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ byteStringBaseFunctor+          -- We have something that _looks_ like a base functor, but not a+          -- special builtin case. We thus need to ask the environment for the+          -- recursive type it stands for, if it exists.+          | otherwise -> do+              let standinTyName = TyName rawTyNameStub+              case preview (ix standinTyName) tyDict of+                -- Now we have _truly_ missed.+                Nothing -> throwError . NoDatatypeInfo $ tn+                Just dti -> case view #baseFunctor dti of+                  Nothing -> throwError . NoDatatypeInfo $ tn+                  -- Since this is generated, it can't fail to rename+                  Just (bfDd, _) -> renamedToUnify . renameDatatypeInfo . fromRight . mkDatatypeInfo $ bfDd+    renamedToUnify :: Either RenameError (DatatypeInfo Renamed) -> UnifyM (DatatypeInfo Renamed)+    renamedToUnify = either (throwError . DatatypeInfoRenameFailed tn) pure+    fromRight :: forall a b. (Show a) => Either a b -> b+    fromRight = \case+      Left err -> error . show $ err+      Right x -> x  lookupBBForm :: TyName -> UnifyM (ValT Renamed) lookupBBForm tn =@@ -210,8 +255,6 @@  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   -- We're doing the equivalent of failing the `ST` trick   Abstraction (Wildcard scopeId trueLevel index) -> throwError . LeakingWildcard scopeId trueLevel $ index   -- We may have a result with fewer unifiables than we started with@@ -344,28 +387,30 @@         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) ->-      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,-    --   just union them.-    -- - Otherwise, for any assignment to a unifiable that is present in both-    --   maps, ensure they assign to the same thing; if they do, it's fine,-    --   otherwise we have a problem.-    reconcile =-      Merge.mergeA-        Merge.preserveMissing-        Merge.preserveMissing-        (Merge.zipWithAMatched combineBindings)++reconcile ::+  Map (Index "tyvar") (ValT Renamed) ->+  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,+--   just union them.+-- - Otherwise, for any assignment to a unifiable that is present in both+--   maps, ensure they assign to the same thing; if they do, it's fine,+--   otherwise we have a problem.+reconcile =+  Merge.mergeA+    Merge.preserveMissing+    Merge.preserveMissing+    (Merge.zipWithAMatched combineBindings)+  where     combineBindings :: Index "tyvar" -> ValT Renamed -> ValT Renamed -> UnifyM (ValT Renamed)-    combineBindings _ old new =+    combineBindings i old new =       if old == new         then pure old         else case old of           Abstraction (Unifiable _) -> pure new           _ -> case new of             Abstraction (Unifiable _) -> pure old-            _ -> unificationError+            _ -> throwError $ CouldNotReconcile i old new

@@ -57,6 +57,12 @@      -- *** Elimination     runRenameM,+    undoRename,++    -- ** ASG+    DebugASGBuilder (..),+    debugASGBuilder,+    typeIdTest,   ) where @@ -65,6 +71,9 @@ #endif import Control.Applicative ((<|>)) import Control.Monad (void)+import Control.Monad.Error.Class (MonadError)+import Control.Monad.HashCons (HashConsT, MonadHashCons, runHashConsT)+import Control.Monad.Reader (MonadReader, ReaderT, runReaderT) import Control.Monad.State.Strict   ( MonadState (get, put),     State,@@ -73,6 +82,8 @@     modify,   ) import Control.Monad.Trans (MonadTrans (lift))+import Control.Monad.Trans.Except (ExceptT, runExceptT)+import Covenant.ASG (ASGEnv (ASGEnv), ASGNode, CovenantError (TypeError), CovenantTypeError, Id, ScopeInfo (ScopeInfo)) import Covenant.Data   ( DatatypeInfo,     mkDatatypeInfo,@@ -106,17 +117,19 @@   ) import Covenant.Internal.PrettyPrint (ScopeBoundary) import Covenant.Internal.Rename-  ( RenameError (InvalidAbstractionReference),+  ( RenameError (InvalidAbstractionReference, InvalidScopeReference),     RenameM,     renameCompT,     renameDataDecl,     renameValT,     runRenameM,+    undoRename,   ) import Covenant.Internal.Strategy   ( DataEncoding (PlutusData, SOP),     PlutusDataStrategy (ConstrData),   )+import Covenant.Internal.Term (ASGNodeType (CompNodeType, ValNodeType), typeId) import Covenant.Internal.Type   ( AbstractTy (BoundAt),     BuiltinFlatT@@ -143,6 +156,7 @@   ) import Covenant.Util (prettyStr) import Data.Coerce (coerce)+import Data.Functor.Identity (Identity (runIdentity)) import Data.Kind (Type) import Data.Map.Strict (Map) import Data.Map.Strict qualified as M@@ -325,7 +339,9 @@ -- @since 1.1.0 chooseInt ::   forall (m :: Type -> Type).-  (MonadGen m) => (Int, Int) -> m Int+  (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'.@@ -333,7 +349,10 @@ -- @since 1.1.0 scale ::   forall (m :: Type -> Type) (a :: Type).-  (MonadGen m) => (Int -> Int) -> m a -> m a+  (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@@ -828,9 +847,64 @@ genDataList :: forall (a :: Type). DataGenM a -> Gen [a] genDataList = runDataGenM . GT.listOf +-- ASG Stuff++-- | This is a @newtype@ over 'ASGBuilder' to clearly indicate that it should be used only for testing, as it is+-- useful to have a variant of the 'ASGBuilder' monad which has a \'runner\'.+--+-- @since 1.2.0+newtype DebugASGBuilder (a :: Type)+  = DebugASGBuilder (ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity)) a)+  deriving+    ( -- | @since 1.0.0+      Functor,+      -- | @since 1.0.0+      Applicative,+      -- | @since 1.0.0+      Monad,+      -- | @since 1.1.0+      MonadReader ASGEnv,+      -- | @since 1.0.0+      MonadError CovenantTypeError,+      -- | @since 1.0.0+      MonadHashCons Id ASGNode+    )+    via ReaderT ASGEnv (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))++-- | \'Runner\' for 'DebugASGBuilder'.+--+-- @since 1.2.0+debugASGBuilder ::+  forall (a :: Type).+  Map TyName (DatatypeInfo AbstractTy) ->+  DebugASGBuilder a ->+  Either CovenantError a+debugASGBuilder tyDict (DebugASGBuilder 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 a -> pure a++-- | Looks up the type of a node, wrapping computation node types into a thunk.+--+-- This is /only/ for use in testing!+--+-- @since 1.2.0+typeIdTest ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  Id ->+  m (ValT AbstractTy)+typeIdTest i =+  typeId i >>= \case+    ValNodeType t -> pure t+    -- FIXME: This is quick & dirty but I need it for something+    CompNodeType t -> pure $ ThunkT t+    other -> error $ "Expected a ValT but got: " <> show other+ -- 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+unsafeRename act = case runRenameM mempty act of   Left err -> error $ show err   Right res -> res @@ -855,4 +929,4 @@       (PlutusData ConstrData)  testDatatypes :: [DataDeclaration AbstractTy]-testDatatypes = [maybeT, eitherT, unitT, pair]+testDatatypes = [maybeT, eitherT, unitT, pair, list]

@@ -105,6 +105,7 @@     Renamed (Rigid, Unifiable, Wildcard),     TyName (TyName),     ValT (Abstraction, BuiltinFlat, Datatype, ThunkT),+    arity,   ) import Data.Coerce (coerce) import Data.Kind (Type)@@ -176,13 +177,6 @@ {-# COMPLETE ArgsAndResult #-}  {-# COMPLETE ReturnT, (:--:>) #-}---- | Determine the arity of a computation type: that is, how many arguments a--- function of this type must be given.------ @since 1.0.0-arity :: forall (a :: Type). CompT a -> Int-arity (CompT _ (CompTBody xs)) = NonEmpty.length xs - 1  -- | A computation type that does not bind any type variables. Use this like a -- data constructor.

@@ -1,30 +1,36 @@+{-# LANGUAGE OverloadedLists #-} {-# LANGUAGE PatternSynonyms #-}  module Main (main) where  import Control.Applicative ((<|>))-import Control.Monad (guard)+import Control.Monad (guard, void) import Covenant.ASG   ( ASG,     ASGBuilder,-    ASGNode (ACompNode, AValNode),+    ASGNode (ACompNode, AValNode, AnError),     CompNodeInfo       ( Builtin1,         Builtin2,-        Builtin3,-        Return+        Builtin3       ),-    CovenantError (EmptyASG, TopLevelError, TopLevelValue, TypeError),+    CovenantError+      ( EmptyASG,+        TopLevelError,+        TopLevelValue,+        TypeError+      ),     CovenantTypeError       ( ApplyCompType,         ApplyToError,         ApplyToValType,+        CataNoBaseFunctorForType,+        CataNonRigidAlgebra,         ForceCompType,         ForceError,         ForceNonThunk,-        LambdaResultsInValType,         NoSuchArgument,-        ReturnCompType,+        OutOfScopeTyVar,         ThunkError,         ThunkValType       ),@@ -33,34 +39,54 @@     ValNodeInfo (Lit),     app,     arg,+    boundTyVar,     builtin1,     builtin2,     builtin3,+    cata,+    ctor,+    dataConstructor,+    defaultDatatypes,+    dtype,     err,     force,     lam,+    lazyLam,     lit,-    nodeAt,-    ret,+    match,     runASGBuilder,     thunk,     topLevelNode,   )-import Covenant.Constant (typeConstant)-import Covenant.DeBruijn (DeBruijn (Z))-import Covenant.Index (Index, intIndex, ix0)+import Covenant.Constant+  ( AConstant (AUnit, AnInteger),+    typeConstant,+  )+import Covenant.DeBruijn (DeBruijn (S, Z))+import Covenant.Index (Index, intIndex, ix0, ix1) import Covenant.Prim   ( typeOneArgFunc,     typeThreeArgFunc,     typeTwoArgFunc,   )-import Covenant.Test (Concrete (Concrete))+import Covenant.Test+  ( Concrete (Concrete),+    DebugASGBuilder,+    debugASGBuilder,+    tyAppTestDatatypes,+    typeIdTest,+  ) import Covenant.Type   ( AbstractTy,-    CompT (Comp0, CompN),-    CompTBody (ArgsAndResult, ReturnT),-    ValT,+    BuiltinFlatT (IntegerT, UnitT),+    CompT (Comp0, Comp1, Comp2, CompN),+    CompTBody (ArgsAndResult, ReturnT, (:--:>)),+    ValT (BuiltinFlat, Datatype, ThunkT),     arity,+    boolT,+    byteStringT,+    integerT,+    tyvar,   ) import Covenant.Util (pattern ConsV, pattern NilV) import Data.Coerce (coerce)@@ -68,6 +94,7 @@ import Data.Map qualified as M import Data.Maybe (fromJust) import Data.Vector qualified as Vector+import Data.Wedge (Wedge (Here, Nowhere, There), wedgeLeft) import Optics.Core (preview, review) import Test.QuickCheck   ( Gen,@@ -82,8 +109,8 @@     shrink,     (===),   )-import Test.Tasty (adjustOption, defaultMain, testGroup)-import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)+import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup)+import Test.Tasty.HUnit (Assertion, assertEqual, assertFailure, testCase) import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)  main :: IO ()@@ -97,9 +124,7 @@       testProperty "toplevel one-arg builtin compiles and has the right type" propTopLevelBuiltin1,       testProperty "toplevel two-arg builtin compiles and has the right type" propTopLevelBuiltin2,       testProperty "toplevel three-arg builtin compiles and has the right type" propTopLevelBuiltin3,-      testProperty "toplevel return compiles and has the right type" propTopLevelReturn,       testProperty "forcing a thunk has the same type as what the thunk wraps" propForceThunk,-      testProperty "applying zero arguments to a return has the same type as what the return wraps" propApplyReturn,       testProperty "forcing a computation type does not compile" propForceComp,       testProperty "forcing a non-thunk value type does not compile" propForceNonThunk,       testProperty "thunking a value type does not compile" propThunkValType,@@ -108,8 +133,33 @@       testProperty "passing computations as arguments does not compile" propApplyComp,       testProperty "requesting a non-existent argument does not compile" propNonExistentArg,       testProperty "requesting an argument that exists compiles" propExistingArg,-      testProperty "returning a computation from a lambda does not compile" propReturnComp,-      testProperty "a lambda body having a value type does not compile" propLambdaValBody+      testCase "db indices are well behaved (non-datatype case)" newLamTest1,+      testCase "db indices are well behaved (datatype case)" newLamTest2,+      testCase "calling down an in-scope tyvar works" boundTyVarHappy,+      testCase "calling down an out-of-scope tyvar fails" boundTyVarShouldFail,+      nothingIntro,+      justConcreteIntro,+      justRigidIntro,+      justNothingIntro,+      testGroup+        "Catamorphisms"+        [ testCase "Natural_F can tear down an Integer" unitCataNaturalF,+          testCase "Negative_F can tear down an Integer" unitCataNegativeF,+          testCase "ByteString_F can tear down a ByteString" unitCataByteStringF,+          testCase "Non-recursive type cata should fail" unitCataMaybeF,+          testCase "Cata with non-rigid algebra should fail" unitCataNonRigidF,+          testCase "<List_F Integer Bool -> !Bool> with List Integer should be Bool" unitCataListInteger,+          testCase "<List_F Integer r -> !r> with List Integer should be r" unitCataListIntegerRigid,+          testCase "<List_F r Integer -> !Integer> with List r should be Integer" unitCataListRigid,+          testCase "<List_F r (Maybe r) -> !Maybe r> with List r should be Maybe r" unitCataListMaybeRigid,+          testCase "introduction then cata elimination" unitCataIntroThenEliminate+        ],+      testGroup+        "Matching"+        [ matchMaybe,+          matchList,+          maybeToList+        ]     ]   where     moreTests :: QuickCheckTests -> QuickCheckTests@@ -147,11 +197,182 @@     Left (TypeError _ ThunkError) -> pure ()     _ -> assertFailure $ "Unexpected result: " <> show result +-- Construct a function of type `<Natural_F Bool -> !Bool> -> Integer -> !Bool`, whose+-- body performs a cata over its second argument using its first argument. This+-- should compile, and type as expected.+unitCataNaturalF :: IO ()+unitCataNaturalF = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "Natural_F" [boolT] :--:> ReturnT boolT+  let ty = Comp0 $ thunkTy :--:> integerT :--:> ReturnT boolT+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `<Negative_F Bool -> !Bool> -> Integer -> !Bool`, whose+-- body performs a cata over its second argument using its first argument. This+-- should compile, and type as expected.+unitCataNegativeF :: IO ()+unitCataNegativeF = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "Negative_F" [boolT] :--:> ReturnT boolT+  let ty = Comp0 $ thunkTy :--:> integerT :--:> ReturnT boolT+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `<ByteString_F Integer -> !Integer> -> ByteString+-- -> !Bool`, whose body performs a cata over its second argument using its+-- first argument. This should compile, and type as expected.+unitCataByteStringF :: IO ()+unitCataByteStringF = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "ByteString_F" [integerT] :--:> ReturnT integerT+  let ty = Comp0 $ thunkTy :--:> byteStringT :--:> ReturnT integerT+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `forall a . <Maybe_F a Integer -> !Integer> -> Maybe+-- a -> !Integer`, whose body performs a cata over its second argument+-- using its first argument. This should fail to compile, indicating that+-- `Maybe` doesn't have a base functor.+unitCataMaybeF :: IO ()+unitCataMaybeF = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "Maybe_F" [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT+  let ty = Comp1 $ thunkTy :--:> Datatype "Maybe" [tyvar Z ix0] :--:> ReturnT integerT+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationFailureUnit comp $ \case+    TypeError _ (CataNoBaseFunctorForType tyName) -> assertEqual "" "Maybe" tyName+    err' -> assertFailure $ "Failed with unexpected type of error: " <> show err'++-- Construct a function of type `<forall a . ListF a (Maybe a) -> !Maybe a> -> List+-- Integer -> !Maybe Integer`, whose body performs a cata over its second+-- argument using its first argument. This should fail to compile due to a+-- non-rigid algebra.+unitCataNonRigidF :: IO ()+unitCataNonRigidF = do+  let nonRigidCompT = Comp1 $ Datatype "List_F" [tyvar Z ix0, Datatype "Maybe" [tyvar Z ix0]] :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])+  let thunkTy = ThunkT nonRigidCompT+  let ty = Comp0 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT (Datatype "Maybe" [integerT])+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationFailureUnit comp $ \case+    TypeError _ (CataNonRigidAlgebra t) -> assertEqual "" nonRigidCompT t+    err' -> assertFailure $ "Failed with unexpected type of error: " <> show err'++-- Construct a function of type `<List_F Integer Bool -> !Bool> -> List Integer+-- -> !Bool`, whose body performs a cata over its second argument using its+-- first argument. This should compile, and type as expected.+unitCataListInteger :: IO ()+unitCataListInteger = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [integerT, boolT] :--:> ReturnT boolT+  let ty = Comp0 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT boolT+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `forall a . <List_F Integer a -> !a> -> List+-- Integer -> !a`, whose body performs a cata over its second argument using its+-- first argument. This should compile, and type as expected.+unitCataListIntegerRigid :: IO ()+unitCataListIntegerRigid = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [integerT, tyvar (S Z) ix0] :--:> ReturnT (tyvar (S Z) ix0)+  let ty = Comp1 $ thunkTy :--:> Datatype "List" [integerT] :--:> ReturnT (tyvar Z ix0)+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `forall a . <List_F a Integer -> !Integer> -> List+-- a -> !Integer`, whose body performs a cata over its second argument using its+-- first argument. This should compile, and type as expected.+unitCataListRigid :: IO ()+unitCataListRigid = do+  let thunkTy = ThunkT $ Comp0 $ Datatype "List_F" [tyvar (S Z) ix0, integerT] :--:> ReturnT integerT+  let ty = Comp1 $ thunkTy :--:> Datatype "List" [tyvar Z ix0] :--:> ReturnT integerT+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `forall a . <List_F a (Maybe a) -> !Maybe a> ->+-- List a -> !Maybe a`, whose body performs a cata over its second argument+-- using its first argument. This should compile, and type as expected.+unitCataListMaybeRigid :: IO ()+unitCataListMaybeRigid = do+  let thunkTy =+        ThunkT $+          Comp0 $+            Datatype "List_F" [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix0]]+              :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix0])+  let ty =+        Comp1 $+          thunkTy+            :--:> Datatype "List" [tyvar Z ix0]+            :--:> ReturnT (Datatype "Maybe" [tyvar Z ix0])+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        result <- cata (AnArg alg) (AnArg x)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty++-- Construct a function of type `forall a b . <List_F a (Maybe b) -> !Maybe b> ->+-- a -> !Maybe b`. In its body, we construct a singleton list, then eliminate it+-- using a cata with the first argument as the algebra. THis should compile and+-- type as expected.+unitCataIntroThenEliminate :: IO ()+unitCataIntroThenEliminate = do+  let thunkTy =+        ThunkT $+          Comp0 $+            Datatype "List_F" [tyvar (S Z) ix0, Datatype "Maybe" [tyvar (S Z) ix1]]+              :--:> ReturnT (Datatype "Maybe" [tyvar (S Z) ix1])+  let ty =+        Comp2 $+          thunkTy+            :--:> tyvar Z ix0+            :--:> ReturnT (Datatype "Maybe" [tyvar Z ix1])+  let comp = lam ty $ do+        alg <- arg Z ix0+        x <- arg Z ix1+        nilThunk <- dataConstructor "List" "Nil" []+        nilForced <- force (AnId nilThunk)+        aT <- boundTyVar Z ix0+        nilApplied <- app nilForced [] [Here aT]+        singleThunk <- dataConstructor "List" "Cons" [AnArg x, AnId nilApplied]+        singleForced <- force (AnId singleThunk)+        singleApplied <- app singleForced [] [Nowhere]+        result <- cata (AnArg alg) (AnId singleApplied)+        pure . AnId $ result+  withCompilationSuccessUnit comp $ matchesType ty+ -- Properties  propTopLevelConstant :: Property propTopLevelConstant = forAllShrinkShow arbitrary shrink show $ \c ->-  let builtUp = lit c+  let builtUp = AnId <$> lit c    in withCompilationFailure builtUp $ \case         TopLevelValue _ t info -> case info of           Lit c' ->@@ -201,25 +422,6 @@                 ]             _ -> failUnexpectedCompNodeInfo info -propTopLevelReturn :: Property-propTopLevelReturn = forAllShrinkShow arbitrary shrink show $ \c ->-  let builtUp = lit c >>= \i -> ret (AnId i)-   in withCompilationSuccess builtUp $ \asg ->-        withToplevelCompNode asg $ \t info ->-          case info of-            Return r -> withExpectedId r $ \i ->-              withExpectedValNode i asg $ \t' info' ->-                case info' of-                  Lit c' ->-                    let cT = typeConstant c-                     in conjoin-                          [ c' === c,-                            cT === t',-                            t === Comp0 (ReturnT cT)-                          ]-                  _ -> failUnexpectedValNodeInfo info'-            _ -> failUnexpectedCompNodeInfo info- -- We use builtins only for this test, but this should demonstrate the -- properties well enough propForceThunk :: Property@@ -247,30 +449,15 @@             force (AnId thunkI)        in (comp, forceThunkComp) --- As we can't build toplevel value ASGs, this has to be a bit roundabout-propApplyReturn :: Property-propApplyReturn = forAllShrinkShow arbitrary shrink show $ \c ->-  let comp = do-        i <- lit c-        ret (AnId i)-      applyReturnComp = do-        i <- comp-        applied <- app i Vector.empty-        ret (AnId applied)-   in withCompilationSuccess comp $ \expectedASG ->-        withCompilationSuccess applyReturnComp $ \applyReturnASG ->-          withToplevelCompNode expectedASG $ \expectedT _ ->-            withToplevelCompNode applyReturnASG $ \actualT _ ->-              expectedT === actualT- propForceComp :: Property propForceComp = forAllShrinkShow arbitrary shrink show $ \x ->-  let comp = do-        i <- case x of-          Left bi1 -> builtin1 bi1-          Right (Left bi2) -> builtin2 bi2-          Right (Right bi3) -> builtin3 bi3-        force (AnId i)+  let comp =+        AnId <$> do+          i <- case x of+            Left bi1 -> builtin1 bi1+            Right (Left bi2) -> builtin2 bi2+            Right (Right bi3) -> builtin3 bi3+          force (AnId i)       expectedT = case x of         Left bi1 -> typeOneArgFunc bi1         Right (Left bi2) -> typeTwoArgFunc bi2@@ -282,9 +469,10 @@  propForceNonThunk :: Property propForceNonThunk = forAllShrinkShow arbitrary shrink show $ \c ->-  let comp = do-        i <- lit c-        force (AnId i)+  let comp =+        AnId <$> do+          i <- lit c+          force (AnId i)    in withCompilationFailure comp $ \case         TypeError _ (ForceNonThunk actualT) -> typeConstant c === actualT         TypeError _ err' -> failWrongTypeError err'@@ -292,9 +480,10 @@  propThunkValType :: Property propThunkValType = forAllShrinkShow arbitrary shrink show $ \c ->-  let comp = do-        i <- lit c-        thunk i+  let comp =+        AnId <$> do+          i <- lit c+          thunk i    in withCompilationFailure comp $ \case         TypeError _ (ThunkValType actualT) -> typeConstant c === actualT         TypeError _ err' -> failWrongTypeError err'@@ -302,10 +491,11 @@  propApplyToVal :: Property propApplyToVal = forAllShrinkShow arbitrary shrink show $ \c args ->-  let comp = do-        args' <- traverse (fmap AnId . lit) args-        i <- lit c-        app i args'+  let comp =+        AnId <$> do+          args' <- traverse (fmap AnId . lit) args+          i <- lit c+          app i args' mempty    in withCompilationFailure comp $ \case         TypeError _ (ApplyToValType t) -> typeConstant c === t         TypeError _ err' -> failWrongTypeError err'@@ -313,10 +503,11 @@  propApplyToError :: Property propApplyToError = forAllShrinkShow arbitrary shrink show $ \args ->-  let comp = do-        args' <- traverse (fmap AnId . lit) args-        i <- err-        app i args'+  let comp =+        AnId <$> do+          args' <- traverse (fmap AnId . lit) args+          i <- err+          app i args' mempty    in withCompilationFailure comp $ \case         TypeError _ ApplyToError -> property True         TypeError _ err' -> failWrongTypeError err'@@ -332,13 +523,14 @@         Right (Left bi2) -> typeTwoArgFunc bi2         Right (Right bi3) -> typeThreeArgFunc bi3 -      comp = do-        i <- builtin1 f-        arg' <- case arg1 of-          Left bi1 -> builtin1 bi1-          Right (Left bi2) -> builtin2 bi2-          Right (Right bi3) -> builtin3 bi3-        app i (Vector.singleton . AnId $ arg')+      comp =+        AnId <$> do+          i <- builtin1 f+          arg' <- case arg1 of+            Left bi1 -> builtin1 bi1+            Right (Left bi2) -> builtin2 bi2+            Right (Right bi3) -> builtin3 bi3+          app i (Vector.singleton . AnId $ arg') mempty    in withCompilationFailure comp $ \case         TypeError _ (ApplyCompType actualT) -> t === actualT         TypeError _ err' -> failWrongTypeError err'@@ -346,7 +538,7 @@  propNonExistentArg :: Property propNonExistentArg = forAllShrinkShow arbitrary shrink show $ \(db, index) ->-  let comp = arg db index >>= \i -> ret (AnArg i)+  let comp = arg db index >>= \i -> pure $ AnArg i    in withCompilationFailure comp $ \case         TypeError _ (NoSuchArgument db' index') -> conjoin [db === db', index === index']         TypeError _ err' -> failWrongTypeError err'@@ -359,7 +551,7 @@ propExistingArg = forAllShrinkShow gen shr show $ \(t, index) ->   let comp = lam t $ do         arg1 <- arg Z index-        ret (AnArg arg1)+        pure (AnArg arg1)    in withCompilationSuccess comp $ \asg ->         withToplevelCompNode asg $ \t' _ ->           t' === t@@ -399,41 +591,217 @@                   Just (Concrete res') -> pure (Comp0 (ArgsAndResult (coerce args') res'), index)            in shrinkOnIndex <|> shrinkOnArgs -propReturnComp :: Property-propReturnComp = forAllShrinkShow arbitrary shrink show $ \x ->-  let t = case x of-        Left bi1 -> typeOneArgFunc bi1-        Right (Left bi2) -> typeTwoArgFunc bi2-        Right (Right bi3) -> typeThreeArgFunc bi3-      comp = do-        i <- case x of-          Left bi1 -> builtin1 bi1-          Right (Left bi2) -> builtin2 bi2-          Right (Right bi3) -> builtin3 bi3-        ret (AnId i)-   in withCompilationFailure comp $ \case-        TypeError _ (ReturnCompType actualT) -> t === actualT-        TypeError _ err' -> failWrongTypeError err'-        err' -> failWrongError err'+boundTyVarHappy :: Assertion+boundTyVarHappy = run $ do+  lam lamTy $ do+    arg1 <- AnArg <$> arg Z ix0+    void $ boundTyVar Z ix0+    pure arg1+  where+    lamTy :: CompT AbstractTy+    lamTy = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0) -propLambdaValBody :: Property-propLambdaValBody = forAllShrinkShow arbitrary shrink show $ \(Concrete t, c) ->-  let resultT = typeConstant c-      comp = lam (Comp0 (ArgsAndResult (Vector.singleton t) resultT)) $ lit c-   in withCompilationFailure comp $ \case-        TypeError _ (LambdaResultsInValType actualT) -> resultT === actualT-        TypeError _ err' -> failWrongTypeError err'-        err' -> failWrongError err'+    run :: forall (a :: Type). ASGBuilder a -> IO ()+    run act = case runASGBuilder M.empty act of+      Left err' -> assertFailure . show $ err'+      Right {} -> pure () +boundTyVarShouldFail :: Assertion+boundTyVarShouldFail = run $ boundTyVar Z ix0+  where+    run :: forall (a :: Type). (Show a) => ASGBuilder a -> IO ()+    run act = case runASGBuilder M.empty act of+      Left (TypeError _ (OutOfScopeTyVar db argpos)) ->+        if db == Z && argpos == ix0+          then pure ()+          else assertFailure $ "Expected OutOfScopeTyVar error for Z, ix0 but got: " <> show db <> ", " <> show argpos+      Left err' -> assertFailure $ "Expected an OutofScopeTyVar error, but got: " <> show err'+      Right x -> assertFailure $ "Expected boundTyVar to fail, but got: " <> show x++-- TODO: better name+newLamTest1 :: Assertion+newLamTest1 = case runASGBuilder M.empty fn of+  Left err' -> assertFailure (show err')+  Right {} -> pure ()+  where+    fn :: ASGBuilder Id+    fn = lam expected $ do+      f <- arg Z ix0 >>= force . AnArg+      a <- AnArg <$> arg Z ix1+      AnId <$> app f (Vector.singleton a) mempty++    expected :: CompT AbstractTy+    expected =+      Comp2 $+        ThunkT (Comp0 $ tyvar (S Z) ix0 :--:> ReturnT (tyvar (S Z) ix1))+          :--:> tyvar Z ix0+          :--:> ReturnT (tyvar Z ix1)++newLamTest2 :: Assertion+newLamTest2 = case runASGBuilder tyAppTestDatatypes fn of+  Left err' -> assertFailure (show err')+  Right {} -> pure ()+  where+    fn :: ASGBuilder Id+    fn = lam expected $ do+      f <- arg Z ix0 >>= force . AnArg+      a <- AnArg <$> arg Z ix1+      AnId <$> app f (Vector.singleton a) mempty++    expected :: CompT AbstractTy+    expected =+      Comp2 $+        ThunkT (Comp0 $ Datatype "Maybe" (Vector.singleton $ tyvar (S Z) ix0) :--:> ReturnT (tyvar (S Z) ix1))+          :--:> Datatype "Maybe" (Vector.singleton $ tyvar Z ix0)+          :--:> ReturnT (tyvar Z ix1)++-- Intro form tests++nothingIntro :: TestTree+nothingIntro =+  runIntroFormTest "nothing" expectNothingThunk $+    dataConstructor "Maybe" "Nothing" mempty >>= typeIdTest+  where+    expectNothingThunk :: ValT AbstractTy+    expectNothingThunk = ThunkT . Comp1 . ReturnT $ Datatype "Maybe" (Vector.fromList [tyvar Z ix0])++justConcreteIntro :: TestTree+justConcreteIntro = runIntroFormTest "justConcreteIntro" expected $ do+  argRef <- AnId <$> lit AUnit+  dataConstructor "Maybe" "Just" (Vector.singleton argRef) >>= typeIdTest+  where+    expected :: ValT AbstractTy+    expected = ThunkT . Comp0 . ReturnT $ Datatype "Maybe" (Vector.singleton $ BuiltinFlat UnitT)++justRigidIntro :: TestTree+justRigidIntro = runIntroFormTest "justRigidIntro" expected $ do+  lamId <- lam lamTy $ do+    arg1 <- AnArg <$> arg Z ix0+    justRigid <- dataConstructor "Maybe" "Just" (Vector.singleton arg1)+    pure (AnId justRigid)+  lamThunked <- thunk lamId+  typeIdTest lamThunked+  where+    lamTy :: CompT AbstractTy+    lamTy =+      Comp1 $+        tyvar Z ix0+          :--:> ReturnT+            ( ThunkT+                . Comp0+                . ReturnT+                $ Datatype "Maybe"+                $ Vector.singleton (tyvar (S Z) ix0)+            )++    expected :: ValT AbstractTy+    expected = ThunkT lamTy++justNothingIntro :: TestTree+justNothingIntro = runIntroFormTest "justNothingIntro" expectedThunk $ do+  thunkL <- lam expectedComp $ do+    nothingThunk <- dataConstructor "Maybe" "Nothing" mempty+    var <- boundTyVar Z ix0+    nothingForced <- force (AnId nothingThunk)+    nothingApplied <- app nothingForced mempty (Vector.singleton . wedgeLeft . Just $ var)+    justNothing <- dataConstructor "Maybe" "Just" (Vector.singleton (AnId nothingApplied))+    justNothingForced <- force (AnId justNothing)+    justNothingApplied <- app justNothingForced mempty (Vector.singleton Nowhere)+    pure (AnId justNothingApplied)+  typeIdTest thunkL+  where+    expectedComp :: CompT AbstractTy+    expectedComp =+      Comp1+        . ReturnT+        . Datatype "Maybe"+        . Vector.singleton+        . Datatype "Maybe"+        $ Vector.singleton+        $ tyvar Z ix0++    expectedThunk :: ValT AbstractTy+    expectedThunk = ThunkT expectedComp++-- pattern matching++{- Construct a pattern match on 'Maybe Unit' that returns an integer.++   This is effectively the simplest possible pattern matching test: The type is non-recursive and the+   parameters to the type constructor are all concrete.+-}+matchMaybe :: TestTree+matchMaybe = runIntroFormTest "matchMaybe" (BuiltinFlat IntegerT) $ do+  unit <- AnId <$> lit AUnit+  scrutinee <- ctor "Maybe" "Just" (Vector.singleton unit) (Vector.singleton Nowhere)+  nothingHandler <- lazyLam (Comp0 $ ReturnT (BuiltinFlat IntegerT)) (AnId <$> lit (AnInteger 0))+  justHandler <- lazyLam (Comp0 $ BuiltinFlat UnitT :--:> ReturnT (BuiltinFlat IntegerT)) (AnId <$> lit (AnInteger 1))+  result <- match (AnId scrutinee) (AnId <$> Vector.fromList [justHandler, nothingHandler])+  typeIdTest result++{- Construct a pattern match on 'List Unit' that returns an integer.++   A simple test for pattern matches on values of recursive types.+-}+matchList :: TestTree+matchList = runIntroFormTest "matchList" (BuiltinFlat IntegerT) $ do+  unit <- AnId <$> lit AUnit+  nilUnit <- ctor "List" "Nil" mempty (Vector.singleton $ There (BuiltinFlat UnitT))+  scrutinee <- ctor "List" "Cons" (Vector.fromList [unit, AnId nilUnit]) (Vector.singleton Nowhere)+  let nilHandlerTy = Comp0 $ ReturnT (BuiltinFlat IntegerT)+      consHandlerTy =+        Comp0 $+          BuiltinFlat UnitT+            :--:> Datatype "List_F" (Vector.fromList [BuiltinFlat UnitT, Datatype "List" (Vector.singleton $ BuiltinFlat UnitT)])+            :--:> ReturnT (BuiltinFlat IntegerT)+  nilHandler <- lazyLam nilHandlerTy (AnId <$> lit (AnInteger 0))+  consHandler <- lazyLam consHandlerTy (AnId <$> lit (AnInteger 0))+  result <- match (AnId scrutinee) (AnId <$> Vector.fromList [nilHandler, consHandler])+  typeIdTest result++{- This differs from the two above tests in that we're using pattern matching to construct the+   'maybeToList :: forall a. Maybe a -> List a' function. This is very useful, because if successful, it provides good evidence that:+     1. Pattern matching works on datatypes with rigid parameters.+     2. Pattern matching works inside the body of a lambda.+     3. Nothing breaks renaming anywhere.+-}+maybeToList :: TestTree+maybeToList = runIntroFormTest "maybeToList" maybeToListTy $ do+  thonk <- lazyLam maybeToListCompTy $ do+    let nothingHandlerTy = Comp0 $ ReturnT (dtype "List" [tyvar (S Z) ix0])+        justHandlerTy = Comp0 $ tyvar (S Z) ix0 :--:> ReturnT (dtype "List" [tyvar (S Z) ix0])+    nothingHandler <- lazyLam nothingHandlerTy $ do+      tvA <- boundTyVar (S Z) ix0+      AnId <$> ctor "List" "Nil" mempty (Vector.singleton (Here tvA))+    justHandler <- lazyLam justHandlerTy $ do+      tvA <- boundTyVar (S Z) ix0+      vA <- AnArg <$> arg Z ix0+      nil <- AnId <$> ctor "List" "Nil" mempty (Vector.singleton (Here tvA))+      AnId <$> ctor "List" "Cons" (Vector.fromList [vA, nil]) (Vector.singleton Nowhere)+    scrutinee <- AnArg <$> arg Z ix0+    AnId <$> match scrutinee (AnId <$> Vector.fromList [justHandler, nothingHandler])+  typeIdTest thonk+  where+    maybeToListCompTy :: CompT AbstractTy+    maybeToListCompTy = Comp1 (dtype "Maybe" [tyvar Z ix0] :--:> ReturnT (dtype "List" [tyvar Z ix0]))++    maybeToListTy :: ValT AbstractTy+    maybeToListTy = ThunkT maybeToListCompTy+ -- Helpers +runIntroFormTest :: String -> ValT AbstractTy -> DebugASGBuilder (ValT AbstractTy) -> TestTree+runIntroFormTest nm expectedTy act = testCase nm $ case debugASGBuilder tyAppTestDatatypes act of+  Left err' -> assertFailure ("ASG Error: " <> show err')+  Right actualTy -> assertEqual nm expectedTy actualTy+ failWrongTypeError :: CovenantTypeError -> Property failWrongTypeError err' = failWithCounterExample ("Unexpected type error: " <> show err')  failWrongError :: CovenantError -> Property failWrongError err' = failWithCounterExample ("Unexpected error: " <> show err') -withCompilationFailure :: ASGBuilder Id -> (CovenantError -> Property) -> Property+withCompilationFailure :: ASGBuilder Ref -> (CovenantError -> Property) -> Property withCompilationFailure comp cb = case runASGBuilder M.empty comp of   Left err' -> cb err'   Right asg -> failWithCounterExample ("Unexpected success: " <> show asg)@@ -459,6 +827,23 @@ failUnexpectedValNodeInfo info =   failWithCounterExample ("Unexpected ValNodeInfo: " <> show info) +withCompilationSuccessUnit :: ASGBuilder Id -> (ASG -> IO ()) -> IO ()+withCompilationSuccessUnit comp cb = case runASGBuilder defaultDatatypes comp of+  Left err' -> assertFailure $ "Did not compile: " <> show err'+  Right asg -> cb asg++withCompilationFailureUnit :: ASGBuilder Id -> (CovenantError -> IO ()) -> IO ()+withCompilationFailureUnit comp cb = case runASGBuilder defaultDatatypes comp of+  Left err' -> cb err'+  Right asg -> assertFailure $ "Unexpected compilation success: " <> show asg++matchesType :: CompT AbstractTy -> ASG -> IO ()+matchesType expectedTy asg = case topLevelNode asg of+  ACompNode actualTy _ -> assertEqual "" expectedTy actualTy+  u@(AValNode _ _) -> assertFailure $ "Got a value node: " <> show u+  AnError -> assertFailure "Got an error node"++{- NOTE: Not 100% sure I won't need these withExpectedId :: Ref -> (Id -> Property) -> Property withExpectedId r cb = case r of   AnId i -> cb i@@ -468,3 +853,4 @@ withExpectedValNode i asg cb = case nodeAt i asg of   AValNode t info -> cb t info   node -> failWithCounterExample ("Unexpected node: " <> show node)+--}

@@ -2,8 +2,6 @@  module Main (main) where --- import Data.Either (isRight)- import Control.Exception (throwIO) import Control.Monad ((<=<)) import Covenant.Data@@ -69,7 +67,7 @@     Right (catMaybes -> bbfDecls) ->       let results =             mapM-              ( \valT -> case runRenameM . renameValT $ valT of+              ( \valT -> case runRenameM mempty . renameValT $ valT of                   Left err -> Left (err, valT)                   Right res -> Right res               )@@ -149,8 +147,8 @@ testMonotypeBB :: TestTree testMonotypeBB = testCase "unitBbf" $ do   let expected = Comp1 $ Abstraction (BoundAt Z ix0) :--:> ReturnT (Abstraction $ BoundAt Z ix0)-  expected' <- failLeft . runRenameM . renameCompT $ expected+  expected' <- failLeft . runRenameM mempty . renameCompT $ expected   actual <- case fromJust . (view #bbForm <=< M.lookup "Unit") $ tyAppTestDatatypes of-    ThunkT inner -> either (throwIO . userError . show) pure . runRenameM $ renameCompT inner+    ThunkT inner -> either (throwIO . userError . show) pure . runRenameM mempty $ renameCompT inner     _ -> assertFailure "BB form not a thunk!"   assertEqual "unit bbf" expected' actual

@@ -292,7 +292,7 @@   Property mkRenameProp typingFun = forAll arbitrary $ \f ->   let t = typingFun f-      result = runRenameM . renameCompT $ t+      result = runRenameM mempty . renameCompT $ t    in case result of         Left err -> counterexample (show err) False         Right renamed -> property $ liftEq eqRenamedVar t renamed@@ -309,7 +309,7 @@   CompT AbstractTy ->   (CompT Renamed -> IO ()) ->   IO ()-withRenamedComp t f = case runRenameM . renameCompT $ t of+withRenamedComp t f = case runRenameM mempty . renameCompT $ t of   Left err -> assertFailure $ "Could not rename: " <> show err   Right t' -> f t' @@ -319,7 +319,7 @@   t (ValT AbstractTy) ->   (t (ValT Renamed) -> IO ()) ->   IO ()-withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of+withRenamedVals vals f = case runRenameM mempty . traverse renameValT $ vals of   Left err -> assertFailure $ "Could not rename: " <> show err   Right vals' -> f vals' 

@@ -81,14 +81,14 @@ testFlat :: BuiltinFlatT -> IO () testFlat t = do   let input = BuiltinFlat t-  let result = runRenameM . renameValT $ input+  let result = runRenameM mempty . renameValT $ input   assertRight (assertBool "" . liftEq (\_ _ -> False) input) result  -- Checks that for any 'fully concretified' type (nested or not), renaming -- changes nothing. propNestedConcrete :: Property propNestedConcrete = forAllShrinkShow arbitrary shrink show $ \(Concrete t) ->-  let result = runRenameM . renameValT $ t+  let result = runRenameM mempty . renameValT $ t    in case result of         Left _ -> False         Right actual -> liftEq (\_ _ -> False) t actual@@ -101,7 +101,7 @@         Comp1 $           Abstraction (Unifiable ix0)             :--:> ReturnT (Abstraction (Unifiable ix0))-  let result = runRenameM . renameCompT $ idT+  let result = runRenameM mempty . renameCompT $ idT   assertRight (assertEqual "" expected) result  -- Checks that `forall a b . a -> b -> !a` correctly renames.@@ -113,7 +113,7 @@           Abstraction (Unifiable ix0)             :--:> Abstraction (Unifiable ix1)             :--:> ReturnT (Abstraction (Unifiable ix0))-  let result = runRenameM . renameCompT $ constT+  let result = runRenameM mempty . renameCompT $ constT   assertRight (assertEqual "" expected) result  -- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames.@@ -126,22 +126,23 @@           Abstraction (Unifiable ix0)             :--:> ReturnT               ( ThunkT . Comp1 $-                  Abstraction (Wildcard 1 2 ix0)+                  Abstraction (Wildcard 1 1 ix0)                     :--:> ReturnT (Abstraction (Unifiable ix0))               )-  let result = runRenameM . renameCompT $ constT+  let result = runRenameM mempty . renameCompT $ constT   assertRight (assertEqual "" expected) result  -- Checks that `forall a . b -> !a` triggers the variable indexing checker. testIndexingIdT :: IO () testIndexingIdT = do-  let t = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix1)-  let result = runRenameM . renameCompT $ t+  let t = Comp1 $ tyvar Z ix1 :--:> ReturnT (tyvar Z ix0)+  let result = runRenameM mempty . renameCompT $ t+   case result of     Left (InvalidAbstractionReference trueLevel ix) -> do-      assertEqual "" trueLevel 1+      assertEqual "" trueLevel 0       assertEqual "" ix ix1-    _ -> assertBool "renaming succeeded when it should have failed" False+    _ -> assertBool ("renaming succeeded when it should have failed: " <> show result) False  -- Helpers 

@@ -3,7 +3,6 @@ module Main (main) where  import Control.Applicative ((<|>))-import Control.Monad (guard) import Covenant.ASG   ( TypeAppError       ( DoesNotUnify,@@ -14,6 +13,7 @@ import Covenant.DeBruijn (DeBruijn (S, Z), asInt) import Covenant.Index   ( Index,+    intIndex,     ix0,     ix1,     ix2,@@ -43,27 +43,35 @@ import Data.Functor.Identity (Identity (Identity)) import Data.Kind (Type) import Data.Map qualified as M+import Data.Maybe (fromJust)+import Data.Vector (Vector) import Data.Vector qualified as Vector-import Optics.Core (review)+import Data.Word (Word32)+import Optics.Core (preview, review) import Test.QuickCheck   ( Gen,     Property,     arbitrary,+    chooseInt,     counterexample,     discard,     elements,+    forAll,     forAllShrink,+    getNonZero,     getSize,+    liftArbitrary,     liftShrink,     oneof,     shrink,     suchThat,+    suchThatMap,     vectorOf,     (===),   ) import Test.Tasty (TestTree, adjustOption, defaultMain, testGroup) import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)-import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)+import Test.Tasty.QuickCheck (QuickCheckMaxSize, QuickCheckTests, testProperty)  main :: IO () main =@@ -79,13 +87,13 @@       testGroup         "Unification"         [ testProperty "concrete expected, concrete actual" propUnifyConcrete,-          testProperty "rigid expected, concrete actual" propUnifyRigidConcrete,+          adjustOption smallerTests . testProperty "rigid expected, concrete actual" $ propUnifyRigidConcrete,           testProperty "wildcard expected, concrete actual" propUnifyWildcardConcrete,           testProperty "wildcard expected, unifiable actual" propUnifyWildcardUnifiable,-          testProperty "concrete expected, rigid actual" propUnifyConcreteRigid,-          testProperty "unifiable expected, rigid actual" propUnifyUnifiableRigid,+          adjustOption smallerTests . testProperty "concrete expected, rigid actual" $ propUnifyConcreteRigid,+          adjustOption smallerTests . testProperty "unifiable expected, rigid actual" $ propUnifyUnifiableRigid,           testProperty "rigid expected, rigid actual" propUnifyRigid,-          testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid,+          adjustOption smallerTests . testProperty "wildcard expected, rigid actual" $ propUnifyWildcardRigid,           testProperty "thunk with unifiable result" propThunkWithUnifiableResult         ],       testGroup@@ -110,14 +118,20 @@     moreTests :: QuickCheckTests -> QuickCheckTests     moreTests = max 10_000 +    -- fewerTests :: QuickCheckTests -> QuickCheckTests+    -- fewerTests = const 100++    smallerTests :: QuickCheckMaxSize -> QuickCheckMaxSize+    smallerTests = (`div` 4)+ -- Units and properties  -- Try to apply more than one argument to `forall a . a -> !a`. -- Result should indicate excess arguments. propTooManyArgs :: Property propTooManyArgs = forAllShrink gen shr $ \excessArgs ->-  withRenamedComp idT $ \renamedIdT ->-    withRenamedVals excessArgs $ \renamedExcessArgs ->+  withRenamedComp mempty idT $ \renamedIdT ->+    withRenamedVals mempty excessArgs $ \renamedExcessArgs ->       case renamedExcessArgs of         [] -> discard -- should be impossible         _ : extraArgs ->@@ -147,7 +161,7 @@ -- insufficient arguments. unitInsufficientArgs :: IO () unitInsufficientArgs = do-  renamedIdT <- failLeft . runRenameM . renameCompT $ idT+  renamedIdT <- failLeft . runRenameM mempty . renameCompT $ idT   let expected = Left $ InsufficientArgs 0 renamedIdT []   let actual = checkApp M.empty renamedIdT []   assertEqual "" expected actual@@ -156,8 +170,8 @@ -- that type. propIdConcrete :: Property propIdConcrete = forAllShrink arbitrary shrink $ \(Concrete t) ->-  withRenamedComp idT $ \renamedIdT ->-    withRenamedVals (Identity t) $ \(Identity t') ->+  withRenamedComp mempty idT $ \renamedIdT ->+    withRenamedVals mempty (Identity t) $ \(Identity t') ->       let expected = Right t'           actual = checkApp M.empty renamedIdT [Just t']        in expected === actual@@ -166,8 +180,8 @@ -- Result should be that type. propConst2Same :: Property propConst2Same = forAllShrink arbitrary shrink $ \(Concrete t) ->-  withRenamedComp const2T $ \renamedConst2T ->-    withRenamedVals (Identity t) $ \(Identity t') ->+  withRenamedComp mempty const2T $ \renamedConst2T ->+    withRenamedVals mempty (Identity t) $ \(Identity t') ->       let expected = Right t'           actual = checkApp M.empty renamedConst2T [Just t', Just t']        in expected === actual@@ -178,9 +192,9 @@ propConst2Different = forAllShrink arbitrary shrink $ \(Concrete t1, Concrete t2) ->   if t1 == t2     then discard-    else withRenamedComp const2T $ \renamedConst2T ->-      withRenamedVals (Identity t1) $ \(Identity t1') ->-        withRenamedVals (Identity t2) $ \(Identity t2') ->+    else withRenamedComp mempty const2T $ \renamedConst2T ->+      withRenamedVals mempty (Identity t1) $ \(Identity t1') ->+        withRenamedVals mempty (Identity t2) $ \(Identity t2') ->           let expected = Right t1'               actual = checkApp M.empty renamedConst2T [Just t1', Just t2']            in expected === actual@@ -191,8 +205,8 @@ -- unification error otherwise. propUnifyConcrete :: Property propUnifyConcrete = forAllShrink gen shr $ \(tA, mtB) ->-  withRenamedComp (Comp0 $ tA :--:> ReturnT integerT) $ \f ->-    withRenamedVals (Identity tA) $ \(Identity tA') ->+  withRenamedComp mempty (Comp0 $ tA :--:> ReturnT integerT) $ \f ->+    withRenamedVals mempty (Identity tA) $ \(Identity tA') ->       case mtB of         Nothing ->           let expected = Right integerT@@ -201,7 +215,7 @@         Just tB ->           if tA == tB             then discard-            else withRenamedVals (Identity tB) $ \(Identity arg) ->+            else withRenamedVals mempty (Identity tB) $ \(Identity arg) ->               let expected = Left . DoesNotUnify tA' $ arg                   actual = checkApp M.empty f [Just arg]                in expected === actual@@ -226,26 +240,27 @@ -- !Integer` to `b`. Result should fail to unify. propUnifyRigidConcrete :: Property propUnifyRigidConcrete = forAllShrink arbitrary shrink $ \(Concrete t, scope, ix) ->-  withRenamedComp (Comp0 $ tyvar (S scope) ix :--:> ReturnT integerT) $ \f ->-    withRenamedVals (Identity t) $ \(Identity t') ->-      -- This is a little confusing, as we would expect that the true level will-      -- 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 . review asInt $ scope-          expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t'-          actual = checkApp M.empty f [Just t']-       in expected === actual+  let mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex ix + 1)+   in withRenamedComp mockScope (Comp0 $ tyvar (S scope) ix :--:> ReturnT integerT) $ \f ->+        withRenamedVals mockScope (Identity t) $ \(Identity t') ->+          -- This is a little confusing, as we would expect that the true level will+          -- 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 = ezTrueLevel mockScope scope ix+              expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t'+              actual = checkApp M.empty f [Just t']+           in expected === actual  -- Randomly pick a concrete type A, then try to apply `(forall a . a -> -- !Integer) -> !Integer` to `(A -> !Integer)`. Result should fail to unify. propUnifyWildcardConcrete :: Property propUnifyWildcardConcrete = forAllShrink arbitrary shrink $ \(Concrete t) ->   let thunk = ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT integerT-   in withRenamedComp (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->+   in withRenamedComp mempty (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->         let argT = ThunkT . Comp0 $ t :--:> ReturnT integerT-         in withRenamedVals (Identity argT) $ \(Identity argT') ->-              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT+         in withRenamedVals mempty (Identity argT) $ \(Identity argT') ->+              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 1 ix0) :--:> ReturnT integerT                   expected = Left . DoesNotUnify lhs $ argT'                   actual = checkApp M.empty f [Just argT']                in expected === actual@@ -255,102 +270,100 @@ -- to `A`. propUnifyWildcardUnifiable :: Property propUnifyWildcardUnifiable = forAllShrink arbitrary shrink $ \(Concrete t) ->-  withRenamedComp (Comp0 $ ThunkT (Comp1 $ tyvar Z ix0 :--:> ReturnT t) :--:> ReturnT t) $ \f ->-    withRenamedVals (Identity t) $ \(Identity t') ->-      withRenamedVals (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) ->-        let expected = Right t'-            actual = checkApp M.empty f [Just arg]-         in expected === actual+  let mockScope = Vector.singleton 1+   in withRenamedComp mockScope (Comp0 $ ThunkT (Comp1 $ tyvar Z ix0 :--:> ReturnT t) :--:> ReturnT t) $ \f ->+        withRenamedVals mockScope (Identity t) $ \(Identity t') ->+          withRenamedVals mockScope (Identity . ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT t) $ \(Identity arg) ->+            let expected = Right t'+                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 -- -> !Integer` to `B`. Result should fail to unify. propUnifyConcreteRigid :: Property propUnifyConcreteRigid = forAllShrink arbitrary shrink $ \(Concrete aT, scope, index) ->-  withRenamedComp (Comp0 $ aT :--:> ReturnT integerT) $ \f ->-    withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) ->-      withRenamedVals (Identity aT) $ \(Identity aT') ->-        let level = negate . review asInt $ scope-            expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index-            actual = checkApp M.empty f [Just arg]-         in expected === actual+  let mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex index + 1)+   in withRenamedComp mockScope (Comp0 $ aT :--:> ReturnT integerT) $ \f ->+        withRenamedVals mockScope (Identity $ tyvar scope index) $ \(Identity arg) ->+          withRenamedVals mockScope (Identity aT) $ \(Identity aT') ->+            let level = ezTrueLevel mockScope scope index+                expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index+                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 -- `A`. Result should unify to `A`. propUnifyUnifiableRigid :: Property propUnifyUnifiableRigid = forAllShrink arbitrary shrink $ \(scope, index) ->-  withRenamedComp idT $ \f ->-    withRenamedVals (Identity $ tyvar scope index) $ \(Identity arg) ->-      let expected = Right arg-          actual = checkApp M.empty f [Just arg]-       in expected === actual+  let mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex index + 1)+   in withRenamedComp mockScope idT $ \f ->+        withRenamedVals mockScope (Identity $ tyvar scope index) $ \(Identity arg) ->+          let expected = Right 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--- index I', that may or may not be different to S and/or I respectively. Let--- `T` be the rigid type that results from `S` and `I`, and `U` be the rigid--- type that results from `S'` and `I'`. Attempt to unify `T -> !Integer` with--- `U`. This should unify to `Integer` if, and only if, `T == U`; otherwise, it--- should fail to unify.+-- Randomly generate a scope stack of height at least 2, then two indexes `I`+-- and `J`, both valid in that scope stack. `I` and `J` may be different or the+-- same, with equal probability. Let `T` be the rigid type corresponding to some+-- variable index in the scope stack at the position for `I`, and `U` be the+-- rigid type corresponding to some variable index in the scope stack at the+-- position for `J`. Attempt to unify `T -> !Integer` with `U`. This should+-- unify to `Integer` if, and only if, `T == U`; otherwise, it should fail to+-- unify. propUnifyRigid :: Property-propUnifyRigid = forAllShrink gen shr $ \testData ->-  withTestData testData $ \(f, arg, expected) ->-    let actual = checkApp M.empty f [Just arg]-     in expected === actual+propUnifyRigid = forAll gen $ \(scopeStack, t, u, same) ->+  withRenamedComp scopeStack (Comp0 $ t :--:> ReturnT integerT) $ \fun ->+    withRenamedVals scopeStack (Identity u) $ \(Identity arg) ->+      case checkApp mempty fun [Just arg] of+        Left err -> counterexample ("Identical rigids, but got " <> show err) $ not same+        Right res -> counterexample ("Different rigids, but unified to " <> show res) same   where-    gen :: Gen (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))+    gen :: Gen (Vector Word32, ValT AbstractTy, ValT AbstractTy, Bool)     gen = do-      db <- arbitrary-      index <- arbitrary-      (db,index,)-        <$> oneof-          [ pure Nothing,-            Just . Left <$> suchThat arbitrary (db /=),-            Just . Right <$> suchThat arbitrary (index /=)-          ]-    shr ::-      (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) ->-      [(DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))]-    shr (db, index, mrest) = do-      db' <- shrink db-      index' <- shrink index-      case mrest of-        Nothing -> pure (db', index, Nothing) <|> pure (db, index', Nothing)-        Just (Left db2) -> do-          db2' <- shrink db2-          (db', index, Just (Left db2)) <$ guard (db' /= db2)-            <|> pure (db, index', Just (Left db2))-            <|> (db, index, Just (Left db2')) <$ guard (db /= db2')-        Just (Right index2) -> do-          index2' <- shrink index2-          pure (db', index, Just (Right index2))-            <|> (db, index', Just (Right index2)) <$ guard (index' /= index2)-            <|> (db, index, Just (Right index2')) <$ guard (index /= index2')-    withTestData ::-      (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar"))) ->-      ((CompT Renamed, ValT Renamed, Either TypeAppError (ValT Renamed)) -> Property) ->-      Property-    withTestData (db, index, mrest) f =-      withRenamedComp (Comp0 $ tyvar (S db) index :--:> ReturnT integerT) $ \fun ->-        case mrest of-          Nothing -> withRenamedVals (Identity . tyvar db $ index) $ \(Identity arg) ->-            f (fun, arg, Right integerT)-          Just rest ->-            let level = negate . review asInt $ db-                lhs = Abstraction . Rigid level $ index-             in case rest of-                  Left db2 -> withRenamedVals (Identity . tyvar db2 $ index) $ \(Identity arg) ->-                    f (fun, arg, Left . DoesNotUnify lhs $ arg)-                  Right index2 -> withRenamedVals (Identity . tyvar db $ index2) $ \(Identity arg) ->-                    f (fun, arg, Left . DoesNotUnify lhs $ arg)+      -- Note (Koz, 08/08/2025): We have to use this rather odd method to ensure+      -- that we never have any scope stack smaller than 2 elements. If we have+      -- an empty stack, we loop forever as we can't find a valid index, and if+      -- the scope stack is a singleton, we can never hit the 'different' case.+      --+      -- Furthermore, we must ensure every scope stack has at least 1 available+      -- variable, as otherwise, our subsequent generator can 'miss'.+      firstScope <- getNonZero <$> arbitrary+      secondScope <- getNonZero <$> arbitrary+      restOfScopes <- liftArbitrary (getNonZero <$> arbitrary)+      let scopeStack = Vector.cons firstScope . Vector.cons secondScope $ restOfScopes+      (t, u, same) <- genAbstractions scopeStack+      pure (scopeStack, t, u, same)+    genAbstractions :: Vector Word32 -> Gen (ValT AbstractTy, ValT AbstractTy, Bool)+    genAbstractions scopeStack = do+      let len = Vector.length scopeStack+      iPosition <- chooseInt (0, len - 1)+      jPosition <- suchThat (chooseInt (0, len - 1)) (/= iPosition)+      let iDB = fromJust . preview asInt $ iPosition+      let jDB = fromJust . preview asInt $ jPosition+      let iVarsAvailable = fromIntegral $ scopeStack Vector.! iPosition+      let jVarsAvailable = fromIntegral $ scopeStack Vector.! jPosition+      iIx <- suchThatMap (chooseInt (0, iVarsAvailable - 1)) (preview intIndex)+      jIx <- suchThatMap (chooseInt (0, jVarsAvailable - 1)) (preview intIndex)+      -- Note (Koz, 08/08/2025): We have to offset `t` by 1, because it's being+      -- bundled directly into a `Comp0`, which means that to refer to the same+      -- position in the scope stack, it needs to be one higher.+      elements+        [ -- 'Same' option.+          (tyvar (S iDB) iIx, tyvar iDB iIx, True),+          -- 'Different' option.+          (tyvar (S iDB) iIx, tyvar jDB jIx, False)+        ]  -- Randomly pick a rigid type A, then try to apply `(forall a . a -> !Integer) -- -> !Integer` to `(A -> !Integer)`. Result should fail to unify. propUnifyWildcardRigid :: Property propUnifyWildcardRigid = forAllShrink arbitrary shrink $ \(scope, index) ->   let thunk = ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT integerT-   in withRenamedComp (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->+      mockScope = Vector.replicate (review asInt scope + 1) (fromIntegral $ review intIndex index + 1)+   in withRenamedComp mockScope (Comp0 $ thunk :--:> ReturnT integerT) $ \f ->         let argT = ThunkT . Comp0 $ tyvar (S scope) index :--:> ReturnT integerT-         in withRenamedVals (Identity argT) $ \(Identity argT') ->-              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT+         in withRenamedVals mockScope (Identity argT) $ \(Identity argT') ->+              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 1 ix0) :--:> ReturnT integerT                   expected = Left . DoesNotUnify lhs $ argT'                   actual = checkApp M.empty f [Just argT']                in expected === actual@@ -363,9 +376,9 @@   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') ->+   in withRenamedComp mempty funT $ \f ->+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->             let expected = Right aT'                 actual = checkApp M.empty f [Just argT]              in expected === actual@@ -382,7 +395,7 @@       arg3 = Datatype "Either" . Vector.fromList $ [BuiltinFlat UnitT, BuiltinFlat BoolT]        expected = BuiltinFlat IntegerT-  defaultLeftRenamed <- failLeft . runRenameM . renameCompT $ defaultLeft+  defaultLeftRenamed <- failLeft . runRenameM mempty . renameCompT $ defaultLeft   actual <-     either (assertFailure . show) pure $       checkApp@@ -411,8 +424,8 @@           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+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ testFn+  argRenamed <- failLeft . runRenameM mempty . renameValT $ testArg   result <-     either (assertFailure . show) pure $       checkApp tyAppTestDatatypes fnRenamed [Just argRenamed]@@ -428,7 +441,7 @@   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+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ defaultLeft   actual <-     either (assertFailure . show) pure $       checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3])@@ -445,7 +458,7 @@       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+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ defaultPair   actual <-     either (assertFailure . show) pure $       checkApp tyAppTestDatatypes fnRenamed (pure <$> [arg1, arg2, arg3, arg4])@@ -459,7 +472,7 @@           Datatype "Maybe" (Vector.fromList [tyvar Z ix0])             :--:> ReturnT (BuiltinFlat IntegerT)       testArg = Datatype "Maybe" (Vector.fromList [BuiltinFlat BoolT])-  fnRenamed <- failLeft . runRenameM . renameCompT $ testFn+  fnRenamed <- failLeft . runRenameM mempty . renameCompT $ testFn   result <-     either (assertFailure . catchInsufficientArgs) pure $       checkApp tyAppTestDatatypes fnRenamed [Just testArg]@@ -478,7 +491,7 @@         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+  fnRenamed <- failLeft . runRenameM mempty . 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@@ -494,9 +507,9 @@       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') ->+   in withRenamedComp mempty funT $ \f ->+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->             let expected = Right aT'                 actual = checkApp tyAppTestDatatypes f [Just argT]              in expected === actual@@ -510,9 +523,9 @@       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') ->+   in withRenamedComp mempty funT $ \f ->+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->             let expected = Right aT'                 actual = checkApp tyAppTestDatatypes f [Just argT]              in expected === actual@@ -526,9 +539,9 @@       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') ->+   in withRenamedComp mempty funT $ \f ->+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->             let expected = Right aT'                 actual = checkApp tyAppTestDatatypes f [Just argT]              in expected === actual@@ -543,9 +556,9 @@       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') ->+   in withRenamedComp mempty funT $ \f ->+        withRenamedVals mempty (Identity thunkT) $ \(Identity argT) ->+          withRenamedVals mempty (Identity aT) $ \(Identity aT') ->             let expected = Right aT'                 actual = checkApp tyAppTestDatatypes f [Just argT]              in expected === actual@@ -581,19 +594,27 @@       :--:> ReturnT (tyvar Z ix2)  withRenamedComp ::+  Vector.Vector Word32 ->   CompT AbstractTy ->   (CompT Renamed -> Property) ->   Property-withRenamedComp t f = case runRenameM . renameCompT $ t of+withRenamedComp scope t f = case runRenameM scope . renameCompT $ t of   Left err -> counterexample (show err) False   Right t' -> f t'  withRenamedVals ::   forall (t :: Type -> Type).   (Traversable t) =>+  Vector.Vector Word32 ->   t (ValT AbstractTy) ->   (t (ValT Renamed) -> Property) ->   Property-withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of+withRenamedVals scope vals f = case runRenameM scope . traverse renameValT $ vals of   Left err -> counterexample (show err) False   Right vals' -> f vals'++ezTrueLevel :: Vector.Vector Word32 -> DeBruijn -> Index "tyvar" -> Int+ezTrueLevel inherited db ix = case runRenameM inherited . renameValT $ tyvar db ix of+  Left err' -> error ("ezTrueLevel: " <> show err')+  Right (Abstraction (Rigid res _)) -> res+  other -> error $ "ezTrueLevel didn't get a rigid, but got: " <> show other