packages feed

covenant (empty) → 1.0.0

raw patch · 22 files changed

+5081/−0 lines, 22 filesdep +QuickCheckdep +accdep +base

Dependencies added: QuickCheck, acc, base, bimap, bytestring, containers, covenant, enummapset, mtl, nonempty-vector, optics-core, optics-extra, optics-th, prettyprinter, quickcheck-instances, quickcheck-transformer, tasty, tasty-hunit, tasty-quickcheck, text, transformers, vector

Files

+ CHANGELOG.md view
@@ -0,0 +1,11 @@+# Changelog for `covenant`++All notable changes to this project will be documented in this file.++The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.1.0/).++## UNRELEASED++## 1.0.0 -- 08-05-2025++Initial version
+ LICENSE view
@@ -0,0 +1,201 @@+                                 Apache License+                           Version 2.0, January 2004+                        http://www.apache.org/licenses/++   TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION++   1. Definitions.++      "License" shall mean the terms and conditions for use, reproduction,+      and distribution as defined by Sections 1 through 9 of this document.++      "Licensor" shall mean the copyright owner or entity authorized by+      the copyright owner that is granting the License.++      "Legal Entity" shall mean the union of the acting entity and all+      other entities that control, are controlled by, or are under common+      control with that entity. For the purposes of this definition,+      "control" means (i) the power, direct or indirect, to cause the+      direction or management of such entity, whether by contract or+      otherwise, or (ii) ownership of fifty percent (50%) or more of the+      outstanding shares, or (iii) beneficial ownership of such entity.++      "You" (or "Your") shall mean an individual or Legal Entity+      exercising permissions granted by this License.++      "Source" form shall mean the preferred form for making modifications,+      including but not limited to software source code, documentation+      source, and configuration files.++      "Object" form shall mean any form resulting from mechanical+      transformation or translation of a Source form, including but+      not limited to compiled object code, generated documentation,+      and conversions to other media types.++      "Work" shall mean the work of authorship, whether in Source or+      Object form, made available under the License, as indicated by a+      copyright notice that is included in or attached to the work+      (an example is provided in the Appendix below).++      "Derivative Works" shall mean any work, whether in Source or Object+      form, that is based on (or derived from) the Work and for which the+      editorial revisions, annotations, elaborations, or other modifications+      represent, as a whole, an original work of authorship. For the purposes+      of this License, Derivative Works shall not include works that remain+      separable from, or merely link (or bind by name) to the interfaces of,+      the Work and Derivative Works thereof.++      "Contribution" shall mean any work of authorship, including+      the original version of the Work and any modifications or additions+      to that Work or Derivative Works thereof, that is intentionally+      submitted to Licensor for inclusion in the Work by the copyright owner+      or by an individual or Legal Entity authorized to submit on behalf of+      the copyright owner. For the purposes of this definition, "submitted"+      means any form of electronic, verbal, or written communication sent+      to the Licensor or its representatives, including but not limited to+      communication on electronic mailing lists, source code control systems,+      and issue tracking systems that are managed by, or on behalf of, the+      Licensor for the purpose of discussing and improving the Work, but+      excluding communication that is conspicuously marked or otherwise+      designated in writing by the copyright owner as "Not a Contribution."++      "Contributor" shall mean Licensor and any individual or Legal Entity+      on behalf of whom a Contribution has been received by Licensor and+      subsequently incorporated within the Work.++   2. Grant of Copyright License. Subject to the terms and conditions of+      this License, each Contributor hereby grants to You a perpetual,+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable+      copyright license to reproduce, prepare Derivative Works of,+      publicly display, publicly perform, sublicense, and distribute the+      Work and such Derivative Works in Source or Object form.++   3. Grant of Patent License. Subject to the terms and conditions of+      this License, each Contributor hereby grants to You a perpetual,+      worldwide, non-exclusive, no-charge, royalty-free, irrevocable+      (except as stated in this section) patent license to make, have made,+      use, offer to sell, sell, import, and otherwise transfer the Work,+      where such license applies only to those patent claims licensable+      by such Contributor that are necessarily infringed by their+      Contribution(s) alone or by combination of their Contribution(s)+      with the Work to which such Contribution(s) was submitted. If You+      institute patent litigation against any entity (including a+      cross-claim or counterclaim in a lawsuit) alleging that the Work+      or a Contribution incorporated within the Work constitutes direct+      or contributory patent infringement, then any patent licenses+      granted to You under this License for that Work shall terminate+      as of the date such litigation is filed.++   4. Redistribution. You may reproduce and distribute copies of the+      Work or Derivative Works thereof in any medium, with or without+      modifications, and in Source or Object form, provided that You+      meet the following conditions:++      (a) You must give any other recipients of the Work or+          Derivative Works a copy of this License; and++      (b) You must cause any modified files to carry prominent notices+          stating that You changed the files; and++      (c) You must retain, in the Source form of any Derivative Works+          that You distribute, all copyright, patent, trademark, and+          attribution notices from the Source form of the Work,+          excluding those notices that do not pertain to any part of+          the Derivative Works; and++      (d) If the Work includes a "NOTICE" text file as part of its+          distribution, then any Derivative Works that You distribute must+          include a readable copy of the attribution notices contained+          within such NOTICE file, excluding those notices that do not+          pertain to any part of the Derivative Works, in at least one+          of the following places: within a NOTICE text file distributed+          as part of the Derivative Works; within the Source form or+          documentation, if provided along with the Derivative Works; or,+          within a display generated by the Derivative Works, if and+          wherever such third-party notices normally appear. The contents+          of the NOTICE file are for informational purposes only and+          do not modify the License. You may add Your own attribution+          notices within Derivative Works that You distribute, alongside+          or as an addendum to the NOTICE text from the Work, provided+          that such additional attribution notices cannot be construed+          as modifying the License.++      You may add Your own copyright statement to Your modifications and+      may provide additional or different license terms and conditions+      for use, reproduction, or distribution of Your modifications, or+      for any such Derivative Works as a whole, provided Your use,+      reproduction, and distribution of the Work otherwise complies with+      the conditions stated in this License.++   5. Submission of Contributions. Unless You explicitly state otherwise,+      any Contribution intentionally submitted for inclusion in the Work+      by You to the Licensor shall be under the terms and conditions of+      this License, without any additional terms or conditions.+      Notwithstanding the above, nothing herein shall supersede or modify+      the terms of any separate license agreement you may have executed+      with Licensor regarding such Contributions.++   6. Trademarks. This License does not grant permission to use the trade+      names, trademarks, service marks, or product names of the Licensor,+      except as required for reasonable and customary use in describing the+      origin of the Work and reproducing the content of the NOTICE file.++   7. Disclaimer of Warranty. Unless required by applicable law or+      agreed to in writing, Licensor provides the Work (and each+      Contributor provides its Contributions) on an "AS IS" BASIS,+      WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or+      implied, including, without limitation, any warranties or conditions+      of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A+      PARTICULAR PURPOSE. You are solely responsible for determining the+      appropriateness of using or redistributing the Work and assume any+      risks associated with Your exercise of permissions under this License.++   8. Limitation of Liability. In no event and under no legal theory,+      whether in tort (including negligence), contract, or otherwise,+      unless required by applicable law (such as deliberate and grossly+      negligent acts) or agreed to in writing, shall any Contributor be+      liable to You for damages, including any direct, indirect, special,+      incidental, or consequential damages of any character arising as a+      result of this License or out of the use or inability to use the+      Work (including but not limited to damages for loss of goodwill,+      work stoppage, computer failure or malfunction, or any and all+      other commercial damages or losses), even if such Contributor+      has been advised of the possibility of such damages.++   9. Accepting Warranty or Additional Liability. While redistributing+      the Work or Derivative Works thereof, You may choose to offer,+      and charge a fee for, acceptance of support, warranty, indemnity,+      or other liability obligations and/or rights consistent with this+      License. However, in accepting such obligations, You may act only+      on Your own behalf and on Your sole responsibility, not on behalf+      of any other Contributor, and only if You agree to indemnify,+      defend, and hold each Contributor harmless for any liability+      incurred by, or claims asserted against, such Contributor by reason+      of your accepting any such warranty or additional liability.++   END OF TERMS AND CONDITIONS++   APPENDIX: How to apply the Apache License to your work.++      To apply the Apache License to your work, attach the following+      boilerplate notice, with the fields enclosed by brackets "[]"+      replaced with your own identifying information. (Don't include+      the brackets!)  The text should be enclosed in the appropriate+      comment syntax for the file format. We also recommend that a+      file or class name and description of purpose be included on the+      same "printed page" as the copyright notice for easier+      identification within third-party archives.++   Copyright [yyyy] [name of copyright owner]++   Licensed under the Apache License, Version 2.0 (the "License");+   you may not use this file except in compliance with the License.+   You may obtain a copy of the License at++       http://www.apache.org/licenses/LICENSE-2.0++   Unless required by applicable law or agreed to in writing, software+   distributed under the License is distributed on an "AS IS" BASIS,+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.+   See the License for the specific language governing permissions and+   limitations under the License.
+ README.md view
@@ -0,0 +1,35 @@+# Covenant++# What is this?++Covenant is a standalone IR, designed as a target for front-end DSLs for writing+Cardano scripts. It uses [call-by-push-value][cbpv] and is+[Turner-total][turner-total], which gives it a high degree of analyzability.+Furthermore, it uses a fully hash-consed structure.++# How do I use this?++This is currently a work-in-progress. Begin with the documentation in+`Covenant.ASG` and `Covenant.Type`.++# What do I need?++Our policy is to support the latest three GHC versions; see the Cabal file's+`tested-with` field to see which exact versions are supported. This is enforced+using `get-tested` in our CI.++We support only [Tier 1 platforms](https://gitlab.haskell.org/ghc/ghc/-/wikis/platforms#tier-1-platforms). +Covenant is developed using the lowest supported version.++# License++Covenant is licensed under Apache 2.0. Please see the `LICENSE` file for more+information. ++# References++* [Catalyst proposal for+  Covenant](https://projectcatalyst.io/funds/13/f13-cardano-open-developers/mlabs-static-analysis-with-covenant)++[cbpv]: https://www.cs.bham.ac.uk/~pbl/papers/thesisqmwphd.pdf+[turner-total]: https://www.jucs.org/jucs_10_7/total_functional_programming/jucs_10_07_0751_0768_turner.pdf
+ covenant.cabal view
@@ -0,0 +1,162 @@+cabal-version: 3.0+name: covenant+version: 1.0.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.++homepage: https://github.com/mlabs-haskell/covenant+license: Apache-2.0+license-file: LICENSE+author: Koz Ross, Sean Hunter+maintainer: koz@mlabs.city, sean@mlabs.city+bug-reports: https://github.com/mlabs-haskell/covenant/issues+copyright: (C) MLabs 2024+category: Covenant+tested-with: ghc ==9.8.4 || ==9.10.1 || ==9.12.1+build-type: Simple+extra-source-files:+  CHANGELOG.md+  README.md++-- Common sections+common lang+  ghc-options:+    -Wall+    -Wcompat+    -Wredundant-bang-patterns+    -Wredundant-strictness-flags+    -Wmissing-deriving-strategies+    -Woperator-whitespace+    -Wambiguous-fields+    -Wmisplaced-pragmas+    -Wmissing-export-lists+    -Wmissing-import-lists++  default-extensions:+    BangPatterns+    BinaryLiterals+    DataKinds+    DeriveTraversable+    DerivingVia+    DuplicateRecordFields+    EmptyCase+    FlexibleContexts+    FlexibleInstances+    GeneralizedNewtypeDeriving+    HexFloatLiterals+    ImportQualifiedPost+    InstanceSigs+    KindSignatures+    LambdaCase+    MultiParamTypeClasses+    NoFieldSelectors+    NoStarIsType+    NumericUnderscores+    OverloadedLabels+    OverloadedStrings+    PackageImports+    ScopedTypeVariables+    StandaloneDeriving+    TupleSections+    TypeApplications+    TypeFamilies+    TypeOperators+    UndecidableInstances++  build-depends: base >=4.19.0.0 && <5+  default-language: Haskell2010++common test-lang+  import: lang+  ghc-options:+    -O2+    -threaded+    -rtsopts+    -with-rtsopts=-N++  build-depends:+    QuickCheck ==2.15.0.1,+    covenant,+    tasty ==1.5.3,+    tasty-hunit ==0.10.2,+    tasty-quickcheck ==0.11.1,++common bench-lang+  import: lang+  ghc-options: -O2++-- Primary library+library+  import: lang+  exposed-modules:+    Control.Monad.Action+    Control.Monad.HashCons+    Covenant.ASG+    Covenant.Constant+    Covenant.DeBruijn+    Covenant.Index+    Covenant.Prim+    Covenant.Test+    Covenant.Type+    Covenant.Util++  other-modules:+    Covenant.Internal.Rename+    Covenant.Internal.Term+    Covenant.Internal.Type+    Covenant.Internal.Unification++  build-depends:+    QuickCheck ==2.15.0.1,+    acc ==0.2.0.3,+    bimap ==0.5.0,+    bytestring >=0.12.1.0 && <0.13,+    containers >=0.6.8 && <0.8,+    enummapset ==0.7.3.0,+    mtl >=2.3.1 && <3,+    nonempty-vector ==0.2.4,+    optics-core ==0.4.1.1,+    optics-extra ==0.4.2.1,+    optics-th ==0.4.1,+    prettyprinter ==1.7.1,+    quickcheck-instances ==0.3.32,+    quickcheck-transformer ==0.3.1.2,+    text >=2.1.1 && <2.2,+    transformers >=0.6.1.0 && <0.7.0.0,+    vector ==0.13.2.0,++  hs-source-dirs: src++-- Tests+test-suite renaming+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  hs-source-dirs: test/renaming++test-suite type-applications+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  build-depends: vector+  hs-source-dirs: test/type-applications++test-suite primops+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  build-depends: nonempty-vector+  hs-source-dirs: test/primops++test-suite asg+  import: test-lang+  type: exitcode-stdio-1.0+  main-is: Main.hs+  build-depends:+    optics-core,+    vector,++  hs-source-dirs: test/asg++-- Benchmarks
+ src/Control/Monad/Action.hs view
@@ -0,0 +1,287 @@+{-# LANGUAGE FunctionalDependencies #-}++-- | Module: Control.Monad.Action+--+-- Monoid actions, and the update monad, as well as an @mtl@-style capability+-- type class.+--+-- = A note on functional dependencies+--+-- To ensure easy inference, we make use of functional dependencies (either+-- directly or by an equivalent mechanism on associated type families) on both+-- the 'Action' and 'MonadUpdate' type classes. Specifically, we insist that:+--+-- 1. Any monoidal action determines the state it acts on; and+-- 2. Any particular stack that implements 'MonadUpdate' determines what its+-- action is.+--+-- This means that any given action can act on _exactly_ one state, and that any+-- given stack has at most one state we can act upon. The second restriction+-- above is in line with the other similar @mtl@-style capability type classes+-- (such as @MonadReader@, @MonadState@ etc), while the first is a reasonable+-- choice given that we want to have both good inference and also the ability+-- for different actions to act on the same state. Given that actions are likely+-- to be fairly application-specific, we don't see this as a significant+-- limitation.+module Control.Monad.Action+  ( -- * Monoid actions++    -- ** Class+    Action (..),++    -- ** Wrapper+    Actionable,+    actionable,++    -- * Action monad++    -- ** Transformer+    UpdateT (..),+    runUpdateT,++    -- ** Capability type class+    MonadUpdate (..),+  )+where++import Acc (Acc)+import Control.Monad.Trans (MonadTrans (lift))+import Control.Monad.Trans.Except (ExceptT)+import Control.Monad.Trans.Maybe (MaybeT)+import Control.Monad.Trans.RWS.CPS (RWST)+import Control.Monad.Trans.Reader (ReaderT)+import Control.Monad.Trans.State.Strict (StateT)+import Control.Monad.Trans.Writer.CPS (WriterT)+import Data.Functor (void)+import Data.Kind (Type)+import Data.Monoid (Endo, appEndo)++-- | Describes (left) [monoidal actions on a+-- set](https://en.wikipedia.org/wiki/Semigroup_action). In this case, the type+-- @StateOf a@ is \'the state being acted on\' (or \'the state\'), while @a@ is+-- \'the thing doing the acting\' (or \'the action\').+--+-- = Laws+--+-- Briefly, any instance of @'Action' a@ defines a [monoid+-- homomorphism](https://en.wikipedia.org/wiki/Monoid#Monoid_homomorphisms)+-- between @a@ and @'Endo' (StateOf a)@ (which is essentially @StateOf a ->+-- StateOf a)@. In Haskell terms, this means the following laws must hold:+--+-- 1. @'act' 'mempty'@ @=@ @'mempty'@+-- 2. @'act' x '<>' 'act' y@ @=@ @'act' (x '<>' y)@+--+-- @since 1.0.0+class (Monoid a) => Action (a :: Type) where+  type StateOf a :: Type+  act :: a -> Endo (StateOf a)++-- | Often, we want to take a type that doesn't (naturally) form a 'Monoid' and+-- use it as an action. This can be done using a range of \'free monoid+-- constructions\', including lists. However, these aren't optimal due to the+-- append-heavy (and concatenation-heavy) workloads we typically need from+-- actions.+--+-- 'Actionable' is such a \'free monoid construction\' which \'promotes\' any+-- @a@ into a 'Semigroup' and a 'Monoid'. It is fairly opaque, providing only+-- the instances we really need, but it's designed for efficient appending and+-- concatenation.+--+-- To use 'Actionable', you want to do something like this:+--+-- @+-- data MyState = ...+--+-- data MyType = ...+--+-- newtype MyAction = MyAction (Actionable MyType)+--  deriving (Semigroup, Monoid) via (Actionable MyType)+--+-- instance Action MyAction where+--    type StateOf MyAction = MyState+--    act (MyAction acts) = foldMap go acts+--    where+--      go :: MyType -> Endo MyState+--      go x = Endo $ \oldState -> ...+-- @+--+-- To \'inject\' your type into an 'Actionable', use 'actionable'.+--+-- @since 1.0.0+newtype Actionable a = Actionable (Acc a)+  deriving+    ( -- | @since 1.0.0+      Semigroup,+      -- | @since 1.0.0+      Monoid+    )+    via Acc a+  deriving+    ( -- | @since 1.0.0+      Foldable+    )+    via Acc++-- | Wrap a value into an 'Actionable'.+--+-- @since 1.0.0+actionable :: a -> Actionable a+actionable = Actionable . pure++-- | A transformer implementing the \'update monad\' pattern, as described+-- [here](https://www.schoolofhaskell.com/user/edwardk/heap-of-successes).+--+-- We leave the state implicit, as it is uniquely determined by the @act@ type,+-- together with the 'Action' type class requirement.+--+-- = Important note+--+-- This implementation is not suitable for any @m@ that throws exceptions. This+-- includes @IO@, @ST@ and anything stacked atop them. For the reasons why, see+-- [here](https://github.com/haskell-effectful/effectful/blob/master/transformers.md#statet).+--+-- @since 1.0.0+newtype UpdateT (act :: Type) (m :: Type -> Type) (a :: Type)+  = UpdateT (StateOf act -> m (act, a))+  deriving stock+    ( -- | @since 1.0.0+      Functor+    )++-- | @since 1.0.0+instance (Action act, Monad m) => Applicative (UpdateT act m) where+  {-# INLINEABLE pure #-}+  pure x = UpdateT $ \_ -> pure (mempty, x)+  {-# INLINEABLE (<*>) #-}+  UpdateT fs <*> UpdateT xs = UpdateT $ \s -> do+    (act1, f) <- fs s+    let s' = appEndo (act act1) s+    (act2, x) <- xs s'+    pure (act1 <> act2, f x)++-- | @since 1.0.0+instance (Action act, Monad m) => Monad (UpdateT act m) where+  {-# INLINEABLE (>>=) #-}+  UpdateT xs >>= f = UpdateT $ \s -> do+    (act1, x) <- xs s+    let s' = appEndo (act act1) s+    let (UpdateT applied) = f x+    (act2, y) <- applied s'+    pure (act1 <> act2, y)++-- | @since 1.0.0+instance (Action act) => MonadTrans (UpdateT act) where+  {-# INLINEABLE lift #-}+  lift comp = UpdateT $ \_ -> (mempty,) <$> comp++-- | As 'runUpdate', except that it produces the results in the \'inner monad\'+-- of 'UpdateT'.+--+-- @since 1.0.0+runUpdateT ::+  forall (act :: Type) (m :: Type -> Type) (a :: Type).+  (Functor m, Action act) =>+  UpdateT act m a ->+  StateOf act ->+  m (StateOf act, act, a)+runUpdateT (UpdateT comp) s =+  (\(act1, res) -> (appEndo (act act1) s, act1, res)) <$> comp s++-- | An @mtl@-style capability type class describing update monads in general,+-- irrespective of their states and/or actions.+--+-- = Laws+--+-- 1. @'send' x 'Control.Applicative.*>' 'send' y@ @=@ @'send' (x '<>' y)@+--+-- If you define 'update' or 'request', ensure the following also hold:+--+-- 2. @'update' 'mempty'@ @=@ @'pure' ()@+-- 3. @'request' 'Control.Applicative.*>' 'request'@ @=@ @'request'@+-- 4. @'update'@ @=@ @'void' '.' 'send'@+-- 5. @'request'@ @=@ @'send' 'mempty'@+--+-- Laws 4 and 5 form the default definitions of 'update' and 'request'+-- respectively, which obey all these laws.+--+-- @since 1.0.0+class (Action act, Monad m) => MonadUpdate act m | m -> act where+  -- | Performs the given action on the state, returning the result.+  --+  -- @since 1.0.0+  send :: act -> m (StateOf act)++  -- | Performs the given action, returning nothing.+  --+  -- @since 1.0.0+  {-# INLINEABLE update #-}+  update :: act -> m ()+  update = void . send++  -- | Retrieves the state without doing anything to it.+  --+  -- @since 1.0.0+  {-# INLINEABLE request #-}+  request :: m (StateOf act)+  request = send (mempty :: act)++  {-# MINIMAL send #-}++-- | @since 1.0.0+instance (Action act, Monad m) => MonadUpdate act (UpdateT act m) where+  {-# INLINEABLE send #-}+  send x = UpdateT $ \s -> pure (x, appEndo (act x) s)++-- | @since 1.0.0+instance (MonadUpdate act m) => MonadUpdate act (ReaderT r m) where+  {-# INLINEABLE send #-}+  send = lift . send+  {-# INLINEABLE update #-}+  update = lift . update+  {-# INLINEABLE request #-}+  request = lift request++-- | @since 1.0.0+instance (MonadUpdate act m) => MonadUpdate act (MaybeT m) where+  {-# INLINEABLE send #-}+  send = lift . send+  {-# INLINEABLE update #-}+  update = lift . update+  {-# INLINEABLE request #-}+  request = lift request++-- | @since 1.0.0+instance (MonadUpdate act m) => MonadUpdate act (StateT s m) where+  {-# INLINEABLE send #-}+  send = lift . send+  {-# INLINEABLE update #-}+  update = lift . update+  {-# INLINEABLE request #-}+  request = lift request++-- | @since 1.0.0+instance (MonadUpdate act m) => MonadUpdate act (WriterT w m) where+  {-# INLINEABLE send #-}+  send = lift . send+  {-# INLINEABLE update #-}+  update = lift . update+  {-# INLINEABLE request #-}+  request = lift request++-- | @since 1.0.0+instance (MonadUpdate act m) => MonadUpdate act (RWST r w s m) where+  {-# INLINEABLE send #-}+  send = lift . send+  {-# INLINEABLE update #-}+  update = lift . update+  {-# INLINEABLE request #-}+  request = lift request++-- | @since 1.0.0+instance (MonadUpdate act m) => MonadUpdate act (ExceptT e m) where+  {-# INLINEABLE send #-}+  send = lift . send+  {-# INLINEABLE update #-}+  update = lift . update+  {-# INLINEABLE request #-}+  request = lift request
+ src/Control/Monad/HashCons.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE FunctionalDependencies #-}++-- | Module: Control.Monad.HashCons+--+-- Provides a transformer, and a capability type class in the style of @mtl@,+-- for hash consing. See the Covenant wiki for how this works.+module Control.Monad.HashCons+  ( -- * Transformer+    HashConsT,+    runHashConsT,+    hashCons,+    lookupRef_,++    -- * Capability type class+    MonadHashCons (..),+  )+where++import Control.Monad.State.Strict+  ( StateT,+    get,+    modify,+    runStateT,+  )+import Control.Monad.Trans (MonadTrans (lift))+import Control.Monad.Trans.Except (ExceptT)+import Control.Monad.Trans.Maybe (MaybeT)+import Control.Monad.Trans.RWS.CPS (RWST)+import Control.Monad.Trans.Reader (ReaderT)+import Control.Monad.Trans.Writer.CPS (WriterT)+import Data.Bimap (Bimap)+import Data.Bimap qualified as Bimap+import Data.Kind (Type)++-- | A transformer implementing hash consing capabilities, with references of+-- type @r@ and referents of type @e@. It is assumed that values of type @e@+-- contain values of type @r@ in their capacity as references, though this is+-- not a requirement of this transformer.+--+-- = Important note+--+-- This implementation is not suitable for any @m@ that throws exceptions. This+-- includes @IO@, @ST@ and anything stacked atop them. For the reasons why, see+-- [here](https://github.com/haskell-effectful/effectful/blob/master/transformers.md#statet).+--+-- @since 1.0.0+newtype HashConsT (r :: Type) (e :: Type) (m :: Type -> Type) (a :: Type)+  = HashConsT (StateT (Bimap r e) m a)+  deriving+    ( -- | @since 1.0.0+      Functor,+      -- | @since 1.0.0+      Applicative,+      -- | @since 1.0.0+      Monad+    )+    via (StateT (Bimap r e) m)+  deriving+    ( -- | @since 1.0.0+      MonadTrans+    )+    via StateT (Bimap r e)++-- | Execute the computation described, returning both the result and the unique+-- pairings of @r@ and @e@ produced as part of it.+--+-- @since 1.0.0+runHashConsT ::+  forall (r :: Type) (e :: Type) (m :: Type -> Type) (a :: Type).+  HashConsT r e m a ->+  m (a, Bimap r e)+runHashConsT (HashConsT comp) = runStateT comp Bimap.empty++-- | Given a value of type @e@, produce the unique value of type @r@ acting as a+-- reference to it. This @r@ will be cached, ensuring any future requests for+-- the reference for this value of type @e@ will be the same.+--+-- @since 1.0.0+hashCons ::+  forall (r :: Type) (e :: Type) (m :: Type -> Type).+  (Ord r, Ord e, Bounded r, Enum r, Monad m) =>+  e ->+  HashConsT r e m r+hashCons x = HashConsT $ do+  binds <- get+  case Bimap.lookupR x binds of+    Nothing ->+      if Bimap.null binds+        then minBound <$ modify (Bimap.insert minBound x)+        else do+          let largestOldRef = fst . Bimap.findMax $ binds+          let newRef = succ largestOldRef+          newRef <$ modify (Bimap.insert newRef x)+    Just ref -> pure ref++-- | Given a value of type @r@, fetch the cached @e@ value, if it exists.+--+-- @since 1.0.0+lookupRef_ ::+  forall (r :: Type) (e :: Type) (m :: Type -> Type).+  (Monad m, Ord e, Ord r) =>+  r ->+  HashConsT r e m (Maybe e)+lookupRef_ r = HashConsT (Bimap.lookup r <$> get)++-- | An @mtl@-style capability type class for hash consing capability, using+-- references of type @r@ and values of type @e@.+--+-- = Laws+--+-- 1. @'refTo' x '>>' 'refTo' x@ @=@ @'refTo' x@+-- 2. @'liftA2' ('/=') ('refTo' x) ('refTo' y)@ @=@ @'refTo' x '*>' 'refTo' y '*>' 'pure' (x '/=' y)@+-- 3. @'refTo' x '>>=' (\\r -> 'lookupRef' r '>>=' (\\y -> 'pure' (y, r)))@ @=@ @('Just' x, ) '<$>' 'refTo' x@+--+-- @since 1.0.0+class+  (Eq e, Eq r, Monad m) =>+  MonadHashCons (r :: Type) (e :: Type) (m :: Type -> Type)+    | m -> e r+  where+  -- | Produce the unique value of type @r@ that acts as a reference for the+  -- given value of type @e@.+  --+  -- @since 1.0.0+  refTo :: e -> m r++  -- | Given a value of type @r@, fetch the cached value of type @e@.+  --+  -- @since 1.0.0+  lookupRef :: r -> m (Maybe e)++-- | @since 1.0.0+instance (Ord r, Ord e, Bounded r, Enum r, Monad m) => MonadHashCons r e (HashConsT r e m) where+  {-# INLINEABLE refTo #-}+  refTo = hashCons+  {-# INLINEABLE lookupRef #-}+  lookupRef = lookupRef_++-- | @since 1.0.0+instance (Ord r, Ord e, MonadHashCons r e m) => MonadHashCons r e (MaybeT m) where+  {-# INLINEABLE refTo #-}+  refTo e = lift (refTo e)+  {-# INLINEABLE lookupRef #-}+  lookupRef r = lift (lookupRef r)++-- | @since 1.0.0+instance (MonadHashCons r e m) => MonadHashCons r e (ReaderT r' m) where+  {-# INLINEABLE refTo #-}+  refTo e = lift (refTo e)+  {-# INLINEABLE lookupRef #-}+  lookupRef r = lift (lookupRef r)++-- | @since 1.0.0+instance (MonadHashCons r e m) => MonadHashCons r e (StateT s m) where+  {-# INLINEABLE refTo #-}+  refTo e = lift (refTo e)+  {-# INLINEABLE lookupRef #-}+  lookupRef r = lift (lookupRef r)++-- | @since 1.0.0+instance (MonadHashCons r e m) => MonadHashCons r e (WriterT w m) where+  {-# INLINEABLE refTo #-}+  refTo e = lift (refTo e)+  {-# INLINEABLE lookupRef #-}+  lookupRef r = lift (lookupRef r)++-- | @since 1.0.0+instance (MonadHashCons r e m) => MonadHashCons r e (RWST r' w s m) where+  {-# INLINEABLE refTo #-}+  refTo e = lift (refTo e)+  {-# INLINEABLE lookupRef #-}+  lookupRef r = lift (lookupRef r)++-- | @since 1.0.0+instance (MonadHashCons r e m) => MonadHashCons r e (ExceptT e' m) where+  {-# INLINEABLE refTo #-}+  refTo e = lift (refTo e)+  {-# INLINEABLE lookupRef #-}+  lookupRef r = lift (lookupRef r)
+ src/Covenant/ASG.hs view
@@ -0,0 +1,621 @@+{-# LANGUAGE PatternSynonyms #-}++-- |+-- Module: Covenant.ASG+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- The Covenant ASG, and ways to programmatically build it.+--+-- = Note+--+-- We use the term \'ASG\' to refer to \'abstract syntax graph\'. This is+-- because Covenant uses hash consing to ensure duplicate nodes do not exist,+-- thus producing a DAG structure, rather than a tree.+--+-- @since 1.0.0+module Covenant.ASG+  ( -- * The ASG itself++    -- ** Types+    ASG,++    -- ** Functions+    topLevelNode,+    nodeAt,++    -- * ASG components++    -- ** Types+    Id,+    Ref (..),+    Arg,+    CompNodeInfo+      ( Builtin1,+        Builtin2,+        Builtin3,+        Lam,+        Force,+        Return+      ),+    ValNodeInfo (Lit, App, Thunk),+    ASGNode (..),++    -- ** Functions+    typeASGNode,++    -- * ASG builder++    -- ** Types+    CovenantError (..),+    ScopeInfo,+    ASGBuilder,+    CovenantTypeError+      ( BrokenIdReference,+        ForceCompType,+        ForceNonThunk,+        ForceError,+        ThunkValType,+        ThunkError,+        ApplyToValType,+        ApplyToError,+        ApplyCompType,+        RenameFunctionFailed,+        RenameArgumentFailed,+        NoSuchArgument,+        ReturnCompType,+        LambdaResultsInValType,+        LambdaResultsInNonReturn,+        ReturnWrapsError,+        ReturnWrapsCompType,+        WrongReturnType,+        UnificationError+      ),+    RenameError+      ( InvalidAbstractionReference,+        IrrelevantAbstraction,+        UndeterminedAbstraction+      ),++    -- ** Introducers+    arg,+    builtin1,+    builtin2,+    builtin3,+    force,+    ret,+    lam,+    err,+    lit,+    thunk,+    app,++    -- ** Elimination+    runASGBuilder,+  )+where++import Control.Monad.Except+  ( ExceptT,+    MonadError (throwError),+    runExceptT,+  )+import Control.Monad.HashCons+  ( HashConsT,+    MonadHashCons (lookupRef, refTo),+    runHashConsT,+  )+import Control.Monad.Reader+  ( MonadReader (local),+    ReaderT,+    asks,+    runReaderT,+  )+import Covenant.Constant (AConstant, typeConstant)+import Covenant.DeBruijn (DeBruijn, asInt)+import Covenant.Index (Index, count0, intIndex)+import Covenant.Internal.Rename+  ( RenameError+      ( InvalidAbstractionReference,+        IrrelevantAbstraction,+        UndeterminedAbstraction+      ),+    renameCompT,+    renameValT,+    runRenameM,+    undoRename,+  )+import Covenant.Internal.Term+  ( ASGNode (ACompNode, AValNode, AnError),+    ASGNodeType (CompNodeType, ErrorNodeType, ValNodeType),+    Arg (Arg),+    CompNodeInfo+      ( Builtin1Internal,+        Builtin2Internal,+        Builtin3Internal,+        ForceInternal,+        LamInternal,+        ReturnInternal+      ),+    CovenantTypeError+      ( ApplyCompType,+        ApplyToError,+        ApplyToValType,+        BrokenIdReference,+        ForceCompType,+        ForceError,+        ForceNonThunk,+        LambdaResultsInNonReturn,+        LambdaResultsInValType,+        NoSuchArgument,+        RenameArgumentFailed,+        RenameFunctionFailed,+        ReturnCompType,+        ReturnWrapsCompType,+        ReturnWrapsError,+        ThunkError,+        ThunkValType,+        UnificationError,+        WrongReturnType+      ),+    Id,+    Ref (AnArg, AnId),+    ValNodeInfo (AppInternal, LitInternal, ThunkInternal),+    typeASGNode,+    typeId,+    typeRef,+  )+import Covenant.Internal.Type+  ( AbstractTy,+    CompT (CompT),+    CompTBody (CompTBody),+    Renamed,+    ValT (ThunkT),+  )+import Covenant.Internal.Unification (checkApp)+import Covenant.Prim+  ( OneArgFunc,+    ThreeArgFunc,+    TwoArgFunc,+    typeOneArgFunc,+    typeThreeArgFunc,+    typeTwoArgFunc,+  )+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.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Maybe (fromJust)+import Data.Vector (Vector)+import Data.Vector qualified as Vector+import Data.Vector.NonEmpty qualified as NonEmpty+import Optics.Core+  ( A_Lens,+    LabelOptic (labelOptic),+    ix,+    lens,+    over,+    preview,+    review,+    (%),+  )++-- | A fully-assembled Covenant ASG.+--+-- @since 1.0.0+newtype ASG = ASG (Id, Map Id ASGNode)+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Show+    )++-- Note (Koz, 24/04/25): The `topLevelNode` and `nodeAt` functions use `fromJust`,+-- because we can guarantee it's impossible to miss. For an end user, the only+-- way to get hold of an `Id` is by inspecting a node, and since we control how+-- these are built and assigned, and users can't change them, it's safe.+--+-- It is technically possible to escape this safety regime by having two+-- different `ASG`s and mixing up their `Id`s. However, this is both vanishingly+-- unlikely and probably not worth trying to protect against, given the nuisance+-- of having to work in `Maybe` all the time.++-- | Retrieves the top-level node of an ASG.+--+-- @since 1.0.0+topLevelNode :: ASG -> ASGNode+topLevelNode asg@(ASG (rootId, _)) = nodeAt rootId asg++-- | Given an 'Id' and an ASG, produces the node corresponding to that 'Id'.+--+-- = Important note+--+-- This is only safe to use if the 'Id' comes from a node in the argument 'ASG'.+-- 'Id's valid in one ASG are not likely to be valid in another. \'Mixing+-- and matching\' 'Id's from different ASGs will at best produce unexpected+-- results, and at worst will crash. You have been warned.+--+-- @since 1.0.0+nodeAt :: Id -> ASG -> ASGNode+nodeAt i (ASG (_, mappings)) = fromJust . Map.lookup i $ mappings++-- | A tracker for scope-related information while building an ASG+-- programmatically. Currently only tracks available arguments.+--+-- = Important note+--+-- This is a fairly low-level type, designed specifically for ASG construction.+-- While you can do arbitrary things with it, changing things in it outside of+-- 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)))+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Show+    )++-- | Gives access to the argument information for the current, and all+-- enclosing, scopes. The \'outer\' 'Vector' is a stack of scopes, with lower+-- indexes corresponding to closer scopes: index 0 is our scope, 1 is our+-- 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+instance+  (k ~ A_Lens, a ~ Vector (Vector (ValT AbstractTy)), b ~ Vector (Vector (ValT AbstractTy))) =>+  LabelOptic "argumentInfo" k ScopeInfo ScopeInfo a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic = lens coerce (\_ v -> ScopeInfo v)++-- | A Plutus primop with one argument.+--+-- @since 1.0.0+pattern Builtin1 :: OneArgFunc -> CompNodeInfo+pattern Builtin1 f <- Builtin1Internal f++-- | A Plutus primop with two arguments.+--+-- @since 1.0.0+pattern Builtin2 :: TwoArgFunc -> CompNodeInfo+pattern Builtin2 f <- Builtin2Internal f++-- | A Plutus primop with three arguments.+--+-- @since 1.0.0+pattern Builtin3 :: ThreeArgFunc -> CompNodeInfo+pattern Builtin3 f <- Builtin3Internal f++-- | Force a thunk back into the computation it wraps.+--+-- @since 1.0.0+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++{-# COMPLETE Builtin1, Builtin2, Builtin3, Force, Return, Lam #-}++-- | A compile-time literal of a flat builtin type.+--+-- @since 1.0.0+pattern Lit :: AConstant -> ValNodeInfo+pattern Lit c <- LitInternal c++-- | An application of a computation (the 'Id' field) to some arguments (the+-- 'Vector' field).+--+-- @since 1.0.0+pattern App :: Id -> Vector Ref -> ValNodeInfo+pattern App f args <- AppInternal f args++-- | Wrap a computation into a value (essentially delaying it).+--+-- @since 1.0.0+pattern Thunk :: Id -> ValNodeInfo+pattern Thunk i <- ThunkInternal i++{-# COMPLETE Lit, App, Thunk #-}++-- | Any problem that might arise when building an ASG programmatically.+--+-- @since 1.0.0+data CovenantError+  = -- | There was a type error when assembling the ASG. This provides the+    -- hash-consed state up to the point of the error.+    --+    -- @since 1.0.0+    TypeError (Bimap Id ASGNode) CovenantTypeError+  | -- | We tried to generate an ASG with no nodes in it.+    --+    -- @since 1.0.0+    EmptyASG+  | -- | We tried to generate as ASG whose top-level node is an error.+    --+    -- @since 1.0.0+    TopLevelError+  | -- | We tried to generate an ASG whose top-level node is a value.+    --+    -- @since 1.0.0+    TopLevelValue (Bimap Id ASGNode) (ValT AbstractTy) ValNodeInfo+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Show+    )++-- | A concrete monadic stack, providing the minimum amount of functionality+-- needed to build an ASG using the combinators given in this module.+--+-- @since 1.0.0+newtype ASGBuilder (a :: Type)+  = ASGBuilder (ReaderT ScopeInfo (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.0.0+      MonadReader ScopeInfo,+      -- | @since 1.0.0+      MonadError CovenantTypeError,+      -- | @since 1.0.0+      MonadHashCons Id ASGNode+    )+    via ReaderT ScopeInfo (ExceptT CovenantTypeError (HashConsT Id ASGNode Identity))++-- | Executes an 'ASGBuilder' to make a \'finished\' ASG.+--+-- @since 1.0.0+runASGBuilder ::+  forall (a :: Type).+  ASGBuilder a ->+  Either CovenantError ASG+runASGBuilder (ASGBuilder comp) =+  case runIdentity . runHashConsT . runExceptT . runReaderT comp . ScopeInfo $ Vector.empty of+    (result, bm) -> case result of+      Left err' -> Left . TypeError bm $ err'+      Right _ -> case Bimap.size bm of+        0 -> Left EmptyASG+        _ -> do+          let (i, rootNode') = Bimap.findMax bm+          case rootNode' of+            AnError -> Left TopLevelError+            ACompNode _ _ -> pure . ASG $ (i, Bimap.toMap bm)+            AValNode t info -> Left . TopLevelValue bm t $ info++-- | Given a scope and a positional argument index, construct that argument.+-- Will fail if that argument doesn't exist in the specified scope, or if the+-- specified scope doesn't exist.+--+-- @since 1.0.0+arg ::+  forall (m :: Type -> Type).+  (MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>+  DeBruijn ->+  Index "arg" ->+  m Arg+arg scope index = do+  let scopeAsInt = asInt scope+  let indexAsInt = review intIndex index+  lookedUp <- asks (preview (#argumentInfo % ix scopeAsInt % ix indexAsInt))+  case lookedUp of+    Nothing -> throwError . NoSuchArgument scope $ index+    Just t -> pure . Arg scope index $ t++-- | Construct a node corresponding to the given Plutus primop.+--+-- @since 1.0.0+builtin1 ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m) =>+  OneArgFunc ->+  m Id+builtin1 bi = do+  let node = ACompNode (typeOneArgFunc bi) . Builtin1Internal $ bi+  refTo node++-- | As 'builtin1', but for two-argument primops.+--+-- @since 1.0.0+builtin2 ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m) =>+  TwoArgFunc ->+  m Id+builtin2 bi = do+  let node = ACompNode (typeTwoArgFunc bi) . Builtin2Internal $ bi+  refTo node++-- | As 'builtin1', but for three-argument primops.+--+-- @since 1.0.0+builtin3 ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m) =>+  ThreeArgFunc ->+  m Id+builtin3 bi = do+  let node = ACompNode (typeThreeArgFunc bi) . Builtin3Internal $ bi+  refTo node++-- | Given a reference to a thunk, turn it back into a computation. Will fail if+-- the reference isn't a thunk.+--+-- @since 1.0.0+force ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  Ref ->+  m Id+force r = do+  refT <- typeRef r+  case refT of+    ValNodeType t -> case t of+      ThunkT compT -> refTo . ACompNode compT . ForceInternal $ r+      _ -> throwError . ForceNonThunk $ t+    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.+--+-- = Important note+--+-- This combinator works slightly differently to the others in this module. This+-- is required because, due to hash consing, an ASG is typically built+-- \'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@.+--+-- @since 1.0.0+lam ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m, MonadReader ScopeInfo m) =>+  CompT AbstractTy ->+  m Id ->+  m Id+lam expectedT@(CompT _ (CompTBody xs)) bodyComp = do+  let (args, resultT) = NonEmpty.unsnoc xs+  bodyId <- local (over #argumentInfo (Vector.cons args)) bodyComp+  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++-- | Construct the error node.+--+-- @since 1.0.0+err ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m) =>+  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:+--+-- * 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+--+-- @since 1.0.0+app ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  Id ->+  Vector Ref ->+  m Id+app fId argRefs = do+  lookedUp <- typeId fId+  case lookedUp of+    CompNodeType fT -> case runRenameM . renameCompT $ fT of+      Left err' -> throwError . RenameFunctionFailed fT $ err'+      Right renamedFT -> do+        renamedArgs <- traverse renameArg argRefs+        case checkApp renamedFT . Vector.toList $ renamedArgs of+          Left err' -> throwError . UnificationError $ err'+          Right result -> do+            let restored = undoRename result+            refTo . AValNode restored . AppInternal fId $ argRefs+    ValNodeType t -> throwError . ApplyToValType $ t+    ErrorNodeType -> throwError ApplyToError++-- | Construct a node corresponding to the given constant.+--+-- @since 1.0.0+lit ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m) =>+  AConstant ->+  m Id+lit c = refTo . AValNode (typeConstant c) . LitInternal $ c++-- | Given an 'Id' referring to a computation, build a thunk wrapping it. Will+-- fail if the 'Id' does not refer to a computation node.+--+-- @since 1.0.0+thunk ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  Id ->+  m Id+thunk i = do+  idT <- typeId i+  case idT of+    CompNodeType t -> refTo . AValNode (ThunkT t) . ThunkInternal $ i+    ValNodeType t -> throwError . ThunkValType $ t+    ErrorNodeType -> throwError ThunkError++-- Helpers++renameArg ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError 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
+ src/Covenant/Constant.hs view
@@ -0,0 +1,83 @@+-- |+-- Module: Covenant.Constant+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- Representation of Plutus constants in Covenant.+--+-- @since 1.0.0+module Covenant.Constant+  ( -- * Types+    AConstant (..),++    -- * Functions+    typeConstant,+  )+where++import Covenant.Internal.Type+  ( BuiltinFlatT (BoolT, ByteStringT, IntegerT, StringT, UnitT),+    ValT (BuiltinFlat),+  )+import Data.ByteString (ByteString)+import Data.Kind (Type)+import Data.Text (Text)+import Test.QuickCheck+  ( Arbitrary (arbitrary, shrink),+    oneof,+  )+import Test.QuickCheck.Instances.ByteString ()+import Test.QuickCheck.Instances.Text ()+import Test.QuickCheck.Instances.Vector ()++-- | A Plutus constant term.+--+-- @since 1.0.0+data AConstant+  = AUnit+  | ABoolean Bool+  | AnInteger Integer+  | AByteString ByteString+  | AString Text+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | @since 1.0.0+instance Arbitrary AConstant where+  {-# INLINEABLE arbitrary #-}+  arbitrary =+    oneof+      [ pure AUnit,+        ABoolean <$> arbitrary,+        AnInteger <$> arbitrary,+        AByteString <$> arbitrary,+        AString <$> arbitrary+      ]+  {-# INLINEABLE shrink #-}+  shrink = \case+    AUnit -> []+    ABoolean b -> ABoolean <$> shrink b+    AnInteger i -> AnInteger <$> shrink i+    AByteString bs -> AByteString <$> shrink bs+    AString t -> AString <$> shrink t++-- | Produce the type of a given constant.+--+-- @since 1.0.0+typeConstant ::+  forall (a :: Type).+  AConstant -> ValT a+typeConstant =+  BuiltinFlat . \case+    AUnit -> UnitT+    ABoolean _ -> BoolT+    AnInteger _ -> IntegerT+    AByteString _ -> ByteStringT+    AString _ -> StringT
+ src/Covenant/DeBruijn.hs view
@@ -0,0 +1,87 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module: Covenant.DeBruijn+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- DeBruijn indexing type and helpers. These are mainly used for scope tracking.+module Covenant.DeBruijn+  ( DeBruijn (Z, S),+    asInt,+  )+where++import Control.Monad (guard)+import Data.Coerce (coerce)+import Data.List.NonEmpty (NonEmpty)+import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum))+import Data.Word (Word32)+import Test.QuickCheck (Arbitrary)++-- | A DeBruijn index.+--+-- @since 1.0.0+newtype DeBruijn = DeBruijn Word32+  deriving+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Arbitrary+    )+    via Word32+  deriving stock+    ( -- | @since 1.0.0+      Show+    )++-- | Enables some manner of arithmetic with 'DeBruijn's. In this case, '<>' is+-- analogous to '+', while @'stimes' b@ is analogous to scalar multiplication by+-- @b@. Note that 'DeBruijn's cannot be scaled by negative numbers.+--+-- @since 1.0.0+instance Semigroup DeBruijn where+  {-# INLINEABLE (<>) #-}+  DeBruijn x <> DeBruijn y = DeBruijn (x + y)+  {-# INLINEABLE sconcat #-}+  sconcat = DeBruijn . sum . coerce @(NonEmpty DeBruijn) @(NonEmpty Word32)+  {-# INLINEABLE stimes #-}+  stimes b = DeBruijn . coerce . stimes b . coerce @_ @(Sum Word32)++-- | @since 1.0.0+instance Monoid DeBruijn where+  {-# INLINEABLE mempty #-}+  mempty = Z++-- | The zero index.+--+-- @since 1.0.0+pattern Z :: DeBruijn+pattern Z <- DeBruijn 0+  where+    Z = DeBruijn 0++-- | Successor to an index.+--+-- @since 1.0.0+pattern S :: DeBruijn -> DeBruijn+pattern S x <- (reduce -> Just x)+  where+    S (DeBruijn x) = DeBruijn (x + 1)++{-# COMPLETE Z, S #-}++-- | Convert a DeBruijn index into a (non-negative) 'Int'.+--+-- @since 1.0.0+asInt :: DeBruijn -> Int+asInt (DeBruijn i) = fromIntegral i++-- Helpers++reduce :: DeBruijn -> Maybe DeBruijn+reduce (DeBruijn x) = DeBruijn (x - 1) <$ guard (x > 0)
+ src/Covenant/Index.hs view
@@ -0,0 +1,172 @@+{-# LANGUAGE RoleAnnotations #-}++-- |+-- Module: Covenant.Index+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- Positional indexes, starting from 0, and cardinality indicators.+--+-- @since 1.0.0+module Covenant.Index+  ( Index,+    Count,+    intIndex,+    intCount,+    ix0,+    count0,+    ix1,+    count1,+    ix2,+    count2,+    ix3,+    count3,+  )+where++import Data.Bits (toIntegralSized)+import Data.Coerce (coerce)+import Data.List.NonEmpty (NonEmpty)+import Data.Semigroup (Semigroup (sconcat, stimes), Sum (Sum))+import Data.Word (Word32)+import GHC.TypeLits (Symbol)+import Optics.Prism (Prism', prism)+import Test.QuickCheck (Arbitrary)++-- | A positional index, starting from zero. The label allows distinguishing+-- different flavours of indices.+--+-- @since 1.0.0+newtype Index (ofWhat :: Symbol) = Index Word32+  deriving+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Arbitrary+    )+    via Word32+  deriving stock+    ( -- | @since 1.0.0+      Show+    )++type role Index nominal++-- | Enables some manner of arithmetic with 'Index'ess. In this case, '<>' is+-- analogous to '+', while @'stimes' b@ is analogous to scalar multiplication by+-- @b@. Note that 'Index'es cannot be scaled by negative numbers.+--+-- @since 1.0.0+instance Semigroup (Index ofWhat) where+  {-# INLINEABLE (<>) #-}+  Index x <> Index y = Index (x + y)+  {-# INLINEABLE sconcat #-}+  sconcat = Index . sum . coerce @(NonEmpty (Index ofWhat)) @(NonEmpty Word32)+  {-# INLINEABLE stimes #-}+  stimes b = Index . coerce . stimes b . coerce @_ @(Sum Word32)++-- | @since 1.0.0+instance Monoid (Index ofWhat) where+  {-# INLINEABLE mempty #-}+  mempty = Index 0++-- | Helper to construct, and convert, 'Index'es and 'Int's. This is needed+-- because unfortunately, the standard Haskell practice is to use 'Int' for+-- indexes.+--+-- To use this, do one of the following:+--+-- * Construct with @'preview'@: for example, @'preview' intIndex 1@.+-- * Destruct with @'review'@.+--+-- @since 1.0.0+intIndex :: forall (ofWhat :: Symbol). Prism' Int (Index ofWhat)+intIndex =+  prism+    (fromIntegral . coerce @_ @Word32)+    (\i -> maybe (Left i) (Right . Index) . toIntegralSized $ i)++-- | Helper for the first index.+--+-- @since 1.0.0+ix0 :: forall (ofWhat :: Symbol). Index ofWhat+ix0 = Index 0++-- | Helper for the second index.+--+-- @since 1.0.0+ix1 :: forall (ofWhat :: Symbol). Index ofWhat+ix1 = Index 1++-- | Helper for the third index.+--+-- @since 1.0.0+ix2 :: forall (ofWhat :: Symbol). Index ofWhat+ix2 = Index 2++-- | Helper for the fourth index.+--+-- @since 1.0.0+ix3 :: forall (ofWhat :: Symbol). Index ofWhat+ix3 = Index 3++-- | An indicator of the cardinality of something. Meant to be paired with+-- 'Index' to specify which unique something you mean.+--+-- @since 1.0.0+newtype Count (ofWhat :: Symbol) = Count Word32+  deriving+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord+    )+    via Word32+  deriving stock+    ( -- | @since 1.0.0+      Show+    )++type role Count nominal++-- | Helper to construct, and convert, 'Count's and 'Int's. This is needed+-- because unfortunately, sizes of things are usually 'Int's in Haskell.+--+-- To use this, do one of the following:+--+-- * Construct with @'preview'@: for example, @'preview' intCount 1@.+-- * Destruct with @'review'@.+--+-- @since 1.0.0+intCount :: forall (ofWhat :: Symbol). Prism' Int (Count ofWhat)+intCount =+  prism+    (fromIntegral . coerce @_ @Word32)+    (\i -> maybe (Left i) (Right . Count) . toIntegralSized $ i)++-- | Helper for a count of zero items.+--+-- @since 1.0.0+count0 :: forall (ofWhat :: Symbol). Count ofWhat+count0 = Count 0++-- | Helper for a count of one item.+--+-- @since 1.0.0+count1 :: forall (ofWhat :: Symbol). Count ofWhat+count1 = Count 1++-- | Helper for a count of two items.+--+-- @since 1.0.0+count2 :: forall (ofWhat :: Symbol). Count ofWhat+count2 = Count 2++-- | Helper for a count of three items.+--+-- @since 1.0.0+count3 :: forall (ofWhat :: Symbol). Count ofWhat+count3 = Count 3
+ src/Covenant/Internal/Rename.hs view
@@ -0,0 +1,277 @@+module Covenant.Internal.Rename+  ( RenameM,+    RenameError (..),+    runRenameM,+    renameValT,+    renameCompT,+    undoRename,+  )+where++import Control.Monad (unless)+import Control.Monad.Except+  ( ExceptT,+    runExceptT,+    throwError,+  )+import Control.Monad.Reader+  ( Reader,+    asks,+    local,+    runReader,+  )+import Control.Monad.State.Strict+  ( State,+    evalState,+    gets,+    modify,+  )+import Covenant.DeBruijn (DeBruijn (S, Z), asInt)+import Covenant.Index (Count, Index, intCount, intIndex)+import Covenant.Internal.Type+  ( AbstractTy (BoundAt),+    CompT (CompT),+    CompTBody (CompTBody),+    Renamed (Rigid, Unifiable, Wildcard),+    ValT (Abstraction, BuiltinFlat, ThunkT),+  )+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 Optics.Core+  ( A_Lens,+    LabelOptic (labelOptic),+    ix,+    lens,+    over,+    review,+    set,+    to,+    view,+    (%),+  )++-- Used during renaming. Contains a source of fresh indices for wildcards, as+-- well as tracking:+--+-- 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))+  deriving stock (Eq, Show)++-- Note (Koz, 11/04/2025): We need this field as a source of unique identifiers+-- when renaming wildcards. Wildcards are special in that they can unify with+-- anything (possibly _several_ anythings) except different wildcards in the+-- same scope as each other. For example, consider the computation type below:+--+-- (forall a b . a -> b -> !Int) -> (forall c . c -> !Int) -> String -> !Int+--+-- In particular, `a` and `c` would be defined the same way: `BoundAt Z ix0`.+-- However, while `c` and `b` could unify just fine, `a` and `b` could not.+-- Furthermore, they are identically scoped (in the sense that they're both+-- enclosed the same way), which means that, unlike rigid variables, we cannot+-- uniquely identify them just by their scoping.+--+-- Thus, we have to have to have a way to uniquely label any wildcard in such a+-- way that wildcards in the same scope, at the same level, are tagged+-- separately from wildcards in a _different_ scope at the same level. See the+-- functions `stepUpScope` and `dropDownScope` to see how we achieve this.+instance+  (k ~ A_Lens, a ~ Word64, b ~ Word64) =>+  LabelOptic "idSource" k RenameState RenameState a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(RenameState x _) -> x)+      (\(RenameState _ y) x' -> RenameState x' y)++-- 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)) =>+  LabelOptic "tracker" k RenameState RenameState a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(RenameState _ y) -> y)+      (\(RenameState x _) y' -> RenameState x y')++-- | Ways in which the renamer can fail.+--+-- @since 1.0.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.+    --+    -- @since 1.0.0+    InvalidAbstractionReference Int (Index "tyvar")+  | -- | A value type specifies an abstraction that never gets used+    -- anywhere. For example, the type @forall a b . [a]@ has @b@+    -- irrelevant.+    --+    -- @since 1.0.0+    IrrelevantAbstraction+  | -- | A computation type specifies an abstraction which is not used+    -- by any argument. For example, the type @forall a b . a -> !(b -> !a)@+    -- has @b@ undetermined.+    --+    -- @since 1.0.0+    UndeterminedAbstraction+  deriving stock (Eq, Show)++-- | A \'renaming monad\' which allows us to convert type representations from+-- ones that use /relative/ abstraction labelling to /absolute/ abstraction+-- labelling.+--+-- = Why this is necessary+--+-- Consider the following 'AbstractTy': @'BoundAtScope' 1 0@. The meaning of+-- this is relative to where in a type it is positioned: it could be bound by a+-- scope higher than our own, or something we can unify with. Because its+-- meaning (namely, what it refers to) is situational, type checking becomes+-- more difficult, although it has other advantages.+--+-- This monad allows us to convert this relative form into an absolute one. More+-- specifically, the renamer does two things:+--+-- * Ensures that any given abstraction refers to one, and /only/ one, thing;+-- and+-- * Indicates which abstractions are unifiable, and which are (effectively)+-- constant or fixed.+--+-- @since 1.0.0+newtype RenameM (a :: Type)+  = RenameM (ExceptT RenameError (State RenameState) a)+  deriving+    ( -- | @since 1.0.0+      Functor,+      -- | @since 1.0.0+      Applicative,+      -- | @since 1.0.0+      Monad+    )+    via (ExceptT RenameError (State RenameState))++-- | Execute a renaming computation.+--+-- @since 1.0.0+runRenameM ::+  forall (a :: Type).+  RenameM a ->+  Either RenameError a+runRenameM (RenameM comp) = evalState (runExceptT comp) . RenameState 0 $ Vector.empty++-- | Rename a computation type.+--+-- @since 1.0.0+renameCompT :: CompT AbstractTy -> RenameM (CompT Renamed)+renameCompT (CompT abses (CompTBody xs)) = RenameM $ do+  -- Step up a scope+  modify (stepUpScope abses)+  -- Rename, but only the arguments+  renamedArgs <-+    Vector.generateM+      (NonEmpty.length xs - 1)+      (\i -> coerce . renameValT $ xs NonEmpty.! i)+  -- Check that we don't overdetermine anything+  ourAbstractions <- gets (view (#tracker % to Vector.head % _1))+  unless (Vector.and ourAbstractions) (throwError UndeterminedAbstraction)+  -- Check result type+  renamedResult <- coerce . renameValT . NonEmpty.last $ xs+  -- Roll back state+  modify dropDownScope+  -- Rebuild and return+  pure . CompT abses . CompTBody . NonEmpty.snocV renamedArgs $ renamedResult++-- | Rename a value type.+--+-- @since 1.0.0+renameValT :: ValT AbstractTy -> RenameM (ValT Renamed)+renameValT = \case+  Abstraction t -> Abstraction <$> renameAbstraction t+  ThunkT t -> ThunkT <$> renameCompT t+  BuiltinFlat t -> pure . BuiltinFlat $ t++-- 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+  where+    go :: ValT Renamed -> Reader Int (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+      ThunkT (CompT abses (CompTBody xs)) ->+        ThunkT . CompT abses . CompTBody <$> local (+ 1) (traverse go xs)+      BuiltinFlat t' -> pure . BuiltinFlat $ t'++-- 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++renameAbstraction :: AbstractTy -> RenameM Renamed+renameAbstraction (BoundAt scope index) = RenameM $ do+  trueLevel <- gets (\x -> view (#tracker % to Vector.length) x - asInt scope)+  scopeInfo <- gets (\x -> view #tracker x Vector.!? asInt scope)+  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++-- 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+      -- Label (speculatively) the current scope 'step' with a unique value.+      entry = (Vector.replicate absesI False, fresh)+   in -- Ensure that our source of fresh identifiers is incremented+      over #tracker (Vector.cons entry) . set #idSource (fresh + 1) $ x++-- Stop tracking the last scope we added.+--+-- Note that, while we 'throw away' the information about (used) variables in+-- the scope, we do _not_ roll back the `idSource`. This is in fact why we have+-- to be in `State` rather than `Reader`: that change has to be persistent to+-- 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 (asInt scope) % _1 % ix (review intIndex index)) True
+ src/Covenant/Internal/Term.hs view
@@ -0,0 +1,291 @@+module Covenant.Internal.Term+  ( CovenantTypeError (..),+    Id (..),+    typeId,+    Arg (..),+    typeArg,+    Ref (..),+    typeRef,+    CompNodeInfo (..),+    ValNodeInfo (..),+    ASGNode (..),+    typeASGNode,+    ASGNodeType (..),+  )+where++import Control.Monad.Except (MonadError (throwError))+import Control.Monad.HashCons (MonadHashCons (lookupRef))+import Covenant.Constant (AConstant)+import Covenant.DeBruijn (DeBruijn)+import Covenant.Index (Index)+import Covenant.Internal.Rename (RenameError)+import Covenant.Internal.Type (AbstractTy, CompT, ValT)+import Covenant.Internal.Unification (TypeAppError)+import Covenant.Prim (OneArgFunc, ThreeArgFunc, TwoArgFunc)+import Data.Kind (Type)+import Data.Vector (Vector)+import Data.Word (Word64)++-- | An error that can arise during the construction of an ASG by programmatic+-- means.+--+-- @since 1.0.0+data CovenantTypeError+  = -- | An 'Id' has no corresponding node. This error should not arise under+    -- normal circumstances: the most likely explanation is that you're using an+    -- 'Id' that was made by a different ASG builder computation.+    --+    -- @since 1.0.0+    BrokenIdReference Id+  | -- | Computation-typed nodes can't be forced, but we tried anyway.+    --+    -- @since 1.0.0+    ForceCompType (CompT AbstractTy)+  | -- | Value-typed nodes that aren't thunks can't be forced, but we tried anyway.+    --+    -- @since 1.0.0+    ForceNonThunk (ValT AbstractTy)+  | -- | Error nodes can't be forced, but we tried anyway.+    --+    -- @since 1.0.0+    ForceError+  | -- | Value-typed nodes can't be thunked, but we tried anyway.+    --+    -- @since 1.0.0+    ThunkValType (ValT AbstractTy)+  | -- | Error nodes can't be thunked, but we tried anyway.+    --+    -- @since 1.0.0+    ThunkError+  | -- | Arguments can't be applied to a value-typed node, but we tried anyway.+    --+    -- @since 1.0.0+    ApplyToValType (ValT AbstractTy)+  | -- | Arguments can't be applied to error nodes, but we tried anyway.+    --+    -- @since 1.0.0+    ApplyToError+  | -- | Computation-typed nodes can't be applied as arguments, but we tried anyway.+    --+    -- @since 1.0.0+    ApplyCompType (CompT AbstractTy)+  | -- | Renaming the function in an application failed.+    --+    -- @since 1.0.0+    RenameFunctionFailed (CompT AbstractTy) RenameError+  | -- | Renaming an argument in an application failed.+    --+    -- @since 1.0.0+    RenameArgumentFailed (ValT AbstractTy) RenameError+  | -- | We failed to unify an expected argument type with the type of the+    -- argument we were actually given.+    --+    -- @since 1.0.0+    UnificationError TypeAppError+  | -- | An argument was requested that doesn't exist.+    --+    -- @since 1.0.0+    NoSuchArgument DeBruijn (Index "arg")+  | -- | Can't return a computation-typed node, but we tried anyway.+    --+    -- @since 1.0.0+    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)+  | -- | The body of a lambda results in a computation-typed node which isn't+    -- a return, which isn't allowed.+    --+    -- @since 1.0.0+    LambdaResultsInNonReturn (CompT AbstractTy)+  | -- | A lambda body's return is wrapping an error, instead of being directly+    -- an error. This should not happen under normal circumstances and is most+    -- certainly a bug.+    --+    -- @since 1.0.0+    ReturnWrapsError+  | -- | We tried to return a computation-typed node, but this isn't allowed.+    --+    -- @since 1.0.0+    ReturnWrapsCompType (CompT AbstractTy)+  | -- | The result of an application is not what the computation being+    -- applied expected.+    --+    -- First field is the expected type, the second is what we actually got.+    --+    -- @since 1.0.0+    WrongReturnType (ValT AbstractTy) (ValT AbstractTy)+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Show+    )++-- | A unique identifier for a node in a Covenant program.+--+-- @since 1.0.0+newtype Id = Id Word64+  deriving+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Bounded,+      -- | Needed for internal reasons, even though this type class is terrible.+      --+      -- @since 1.0.0+      Enum+    )+    via Word64+  deriving stock+    ( -- | @since 1.0.0+      Show+    )++-- Get the type of an `Id`, or fail.+typeId ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  Id -> m ASGNodeType+typeId i = do+  lookedUp <- lookupRef i+  case lookedUp of+    Nothing -> throwError . BrokenIdReference $ i+    Just node -> pure . typeASGNode $ node++-- | An argument passed to a function in a Covenant program.+--+-- @since 1.0.0+data Arg = Arg DeBruijn (Index "arg") (ValT AbstractTy)+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- Helper to get the type of an argument.+typeArg :: Arg -> ValT AbstractTy+typeArg (Arg _ _ t) = t++-- | A general reference in a Covenant program.+--+-- @since 1.0.0+data Ref+  = -- | A function argument.+    --+    -- @since 1.0.0+    AnArg Arg+  | -- | A link to an ASG node.+    --+    -- @since 1.0.0+    AnId Id+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- Helper for getting a type for any reference.+typeRef ::+  forall (m :: Type -> Type).+  (MonadHashCons Id ASGNode m, MonadError CovenantTypeError m) =>+  Ref -> m ASGNodeType+typeRef = \case+  AnArg arg -> pure . ValNodeType . typeArg $ arg+  AnId i -> typeId i++-- | Computation-term-specific node information.+--+-- @since 1.0.0+data CompNodeInfo+  = Builtin1Internal OneArgFunc+  | Builtin2Internal TwoArgFunc+  | Builtin3Internal ThreeArgFunc+  | LamInternal Id+  | ForceInternal Ref+  | ReturnInternal Ref+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | Value-term-specific node information.+--+-- @since 1.0.0+data ValNodeInfo+  = LitInternal AConstant+  | AppInternal Id (Vector Ref)+  | ThunkInternal Id+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | A single node in a Covenant ASG. Where appropriate, these carry their+-- types.+--+-- @since 1.0.0+data ASGNode+  = -- | A computation-typed node.+    --+    -- @since 1.0.0+    ACompNode (CompT AbstractTy) CompNodeInfo+  | -- | A value-typed node+    --+    -- @since 1.0.0+    AValNode (ValT AbstractTy) ValNodeInfo+  | -- | An error node.+    --+    -- @since 1.0.0+    AnError+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | Produces the type of any ASG node.+--+-- @since 1.0.0+typeASGNode :: ASGNode -> ASGNodeType+typeASGNode = \case+  ACompNode t _ -> CompNodeType t+  AValNode t _ -> ValNodeType t+  AnError -> ErrorNodeType++-- | Helper data type representing the type of any ASG node whatsoever.+--+-- @since 1.0.0+data ASGNodeType+  = CompNodeType (CompT AbstractTy)+  | ValNodeType (ValT AbstractTy)+  | ErrorNodeType+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )
+ src/Covenant/Internal/Type.hs view
@@ -0,0 +1,375 @@+module Covenant.Internal.Type+  ( AbstractTy (..),+    Renamed (..),+    CompT (..),+    CompTBody (..),+    ValT (..),+    BuiltinFlatT (..),+  )+where++import Control.Monad.Reader+  ( MonadReader (local),+    Reader,+    asks,+    runReader,+  )+import Covenant.DeBruijn (DeBruijn)+import Covenant.Index+  ( Count,+    Index,+    intCount,+    intIndex,+  )+import Data.Functor.Classes (Eq1 (liftEq))+import Data.Kind (Type)+import Data.Map.Strict (Map)+import Data.Map.Strict qualified as Map+import Data.Vector (Vector)+import Data.Vector qualified as Vector+import Data.Vector.NonEmpty (NonEmptyVector)+import Data.Vector.NonEmpty qualified as NonEmpty+import Data.Word (Word64)+import GHC.Exts (fromListN)+import Optics.At ()+import Optics.Core+  ( A_Lens,+    LabelOptic (labelOptic),+    ix,+    lens,+    over,+    preview,+    review,+    set,+    view,+    (%),+  )+import Prettyprinter+  ( Doc,+    Pretty (pretty),+    hsep,+    parens,+    viaShow,+    (<+>),+  )++-- | A type abstraction, using a combination of a DeBruijn index (to indicate+-- which scope it refers to) and a positional index (to indicate which bound+-- variable in that scope it refers to).+--+-- = Important note+--+-- This is a /relative/ representation: any given 'AbstractTy' could refer to+-- different things when placed in different positions in the ASG. This stems+-- from how DeBruijn indices behave: 'Z' refers to \'our immediate enclosing+-- scope\', @'S' 'Z'@ to \'one scope outside our immediate enclosing scope\',+-- etc. This can mean different things depending on what these scope(s) are.+--+-- @since 1.0.0+data AbstractTy = BoundAt DeBruijn (Index "tyvar")+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | A type abstraction that has undergone renaming from a specific context.+--+-- @since 1.0.0+data Renamed+  = -- | Set by an enclosing scope, and thus is essentially a+    -- concrete type, we just don't know which. First field is its \'true+    -- level\', second field is the positional index in that scope.+    Rigid Int (Index "tyvar")+  | -- | Can be unified with something, but must be consistent: that is, only one+    -- unification for every instance. Field is this variable's positional index;+    -- we don't need to track the scope, as only one scope contains unifiable+    -- bindings.+    Unifiable (Index "tyvar")+  | -- | /Must/ unify with everything, except with other distinct wildcards in the+    -- same scope. First field is a unique /scope/ identifier; second is its+    -- \'true level\' simialr to @'Rigid'@; third is the positional index within+    -- its scope. We must have unique identifiers for wildcard scopes, as+    -- wildcards unify with everything /except/ other wildcards in the /same/+    -- scope, and child scopes aren't unique.+    Wildcard Word64 Int (Index "tyvar")+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | The \'body\' of a computation type, consisting of the types of its+-- arguments and the type of its result.+--+-- @since 1.0.0+newtype CompTBody (a :: Type) = CompTBody (NonEmptyVector (ValT a))+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | @since 1.0.0+instance Eq1 CompTBody where+  {-# INLINEABLE liftEq #-}+  liftEq f (CompTBody xs) (CompTBody ys) =+    liftEq (liftEq f) xs ys++-- | A computation type, with abstractions indicated by the type argument. In+-- pretty much any case imaginable, this would be either 'AbstractTy' (in the+-- ASG), or 'Renamed' (after renaming).+--+-- @since 1.0.0+data CompT (a :: Type) = CompT (Count "tyvar") (CompTBody a)+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | @since 1.0.0+instance Eq1 CompT where+  {-# INLINEABLE liftEq #-}+  liftEq f (CompT abses1 xs) (CompT abses2 ys) =+    abses1 == abses2 && liftEq f xs ys++-- | @since 1.0.0+instance Pretty (CompT Renamed) where+  pretty = runPrettyM . prettyCompTWithContext++-- | A value type, with abstractions indicated by the type argument. In pretty+-- much any case imaginable, this would be either 'AbstractTy' (in the ASG) or+-- 'Renamed' (after renaming).+--+-- @since 1.0.0+data ValT (a :: Type)+  = -- | An abstract type.+    Abstraction a+  | -- | A suspended computation.+    ThunkT (CompT a)+  | -- | A builtin type without any nesting.+    BuiltinFlat BuiltinFlatT+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | @since 1.0.0+instance Eq1 ValT where+  {-# INLINEABLE liftEq #-}+  liftEq f = \case+    Abstraction abs1 -> \case+      Abstraction abs2 -> f abs1 abs2+      _ -> False+    ThunkT t1 -> \case+      ThunkT t2 -> liftEq f t1 t2+      _ -> False+    BuiltinFlat t1 -> \case+      BuiltinFlat t2 -> t1 == t2+      _ -> False++-- | All builtin types that are \'flat\': that is, do not have other types+-- \'nested inside them\'.+data BuiltinFlatT+  = UnitT+  | BoolT+  | IntegerT+  | StringT+  | ByteStringT+  | BLS12_381_G1_ElementT+  | BLS12_381_G2_ElementT+  | BLS12_381_MlResultT+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- Helpers++newtype ScopeBoundary = ScopeBoundary Int+  deriving (Show, Eq, Ord, Num) via Int++-- Keeping the field names for clarity even if we don't use them+data PrettyContext (ann :: Type)+  = PrettyContext+  { _boundIdents :: Map ScopeBoundary (Vector (Doc ann)),+    _currentScope :: ScopeBoundary,+    _varStream :: [Doc ann]+  }++instance+  (k ~ A_Lens, a ~ Map ScopeBoundary (Vector (Doc ann)), b ~ Map ScopeBoundary (Vector (Doc ann))) =>+  LabelOptic "boundIdents" k (PrettyContext ann) (PrettyContext ann) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(PrettyContext x _ _) -> x)+      (\(PrettyContext _ y z) x -> PrettyContext x y z)++instance+  (k ~ A_Lens, a ~ ScopeBoundary, b ~ ScopeBoundary) =>+  LabelOptic "currentScope" k (PrettyContext ann) (PrettyContext ann) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(PrettyContext _ x _) -> x)+      (\(PrettyContext x _ z) y -> PrettyContext x y z)++instance+  (k ~ A_Lens, a ~ [Doc ann], b ~ [Doc ann]) =>+  LabelOptic "varStream" k (PrettyContext ann) (PrettyContext ann) a b+  where+  {-# INLINEABLE labelOptic #-}+  labelOptic =+    lens+      (\(PrettyContext _ _ x) -> x)+      (\(PrettyContext x y _) z -> PrettyContext x y z)++-- Maybe make a newtype with error reporting since this can fail, but do later since *should't* fail+newtype PrettyM (ann :: Type) (a :: Type) = PrettyM (Reader (PrettyContext ann) a)+  deriving+    ( Functor,+      Applicative,+      Monad,+      MonadReader (PrettyContext ann)+    )+    via (Reader (PrettyContext ann))++runPrettyM :: forall (ann :: Type) (a :: Type). PrettyM ann a -> a+runPrettyM (PrettyM ma) = runReader ma (PrettyContext mempty 0 infiniteVars)+  where+    -- Lazily generated infinite list of variables. Will start with a, b, c...+    -- and cycle around to a1, b2, c3 etc.+    -- We could do something more sophisticated but this should work.+    infiniteVars :: [Doc ann]+    infiniteVars =+      let aToZ = ['a' .. 'z']+          intStrings = ("" <$ aToZ) <> map (show @Integer) [0 ..]+       in zipWith (\x xs -> pretty (x : xs)) aToZ intStrings++prettyCompTWithContext :: forall (ann :: Type). CompT Renamed -> PrettyM ann (Doc ann)+prettyCompTWithContext (CompT count (CompTBody funArgs))+  | review intCount count == 0 = prettyFunTy funArgs+  | otherwise = bindVars count $ \newVars -> do+      funTy <- prettyFunTy funArgs+      pure $ mkForall newVars funTy++prettyFunTy ::+  forall (ann :: Type).+  NonEmptyVector (ValT Renamed) ->+  PrettyM ann (Doc ann)+prettyFunTy args = case NonEmpty.uncons args of+  (arg, rest) -> Vector.foldl' go (("!" <>) <$> prettyArg arg) rest+  where+    go ::+      PrettyM ann (Doc ann) ->+      ValT Renamed ->+      PrettyM ann (Doc ann)+    go acc t = (\x y -> x <+> "->" <+> y) <$> prettyArg t <*> acc+    prettyArg :: ValT Renamed -> PrettyM ann (Doc ann)+    prettyArg vt =+      let prettyVT = prettyValTWithContext vt+       in if isSimpleValT vt+            then prettyVT+            else parens <$> prettyVT++bindVars ::+  forall (ann :: Type) (a :: Type).+  Count "tyvar" ->+  (Vector (Doc ann) -> PrettyM ann a) ->+  PrettyM ann a+bindVars count' act+  | count == 0 = crossBoundary (act Vector.empty)+  | otherwise = crossBoundary $ do+      here <- asks (view #currentScope)+      withFreshVarNames count $ \newBoundVars ->+        local (over #boundIdents (Map.insert here newBoundVars)) (act newBoundVars)+  where+    -- Increment the current scope+    crossBoundary :: PrettyM ann a -> PrettyM ann a+    crossBoundary = local (over #currentScope (+ 1))+    count :: Int+    count = review intCount count'++mkForall ::+  forall (ann :: Type).+  Vector (Doc ann) ->+  Doc ann ->+  Doc ann+mkForall tvars funTyBody =+  if Vector.null tvars+    then funTyBody+    else "forall" <+> hsep (Vector.toList tvars) <> "." <+> funTyBody++-- I.e. can we omit parens and get something unambiguous? This might be overly aggressive w/ parens but that's OK+isSimpleValT :: forall (a :: Type). ValT a -> Bool+isSimpleValT = \case+  ThunkT thunk -> isSimpleCompT thunk+  _ -> True+  where+    isSimpleCompT :: CompT a -> Bool+    isSimpleCompT (CompT count (CompTBody args)) =+      review intCount count == 0 && NonEmpty.length args == 1++prettyValTWithContext :: forall (ann :: Type). ValT Renamed -> PrettyM ann (Doc ann)+prettyValTWithContext = \case+  Abstraction abstr -> prettyRenamedWithContext abstr+  ThunkT compT -> prettyCompTWithContext compT+  BuiltinFlat biFlat -> pure $ viaShow biFlat++-- Generate N fresh var names and use the supplied monadic function to do something with them.+withFreshVarNames ::+  forall (ann :: Type) (a :: Type).+  Int ->+  (Vector (Doc ann) -> PrettyM ann a) ->+  PrettyM ann a+withFreshVarNames n act = do+  stream <- asks (view #varStream)+  let (used, rest) = splitAt n stream+  local (set #varStream rest) . act . fromListN n $ used++prettyRenamedWithContext :: forall (ann :: Type). Renamed -> PrettyM ann (Doc ann)+prettyRenamedWithContext = \case+  Rigid offset index -> lookupAbstraction offset index+  Unifiable i -> lookupAbstraction 0 i+  Wildcard w64 offset i -> pure $ pretty offset <> "_" <> viaShow w64 <> "#" <> pretty (review intIndex i)++lookupAbstraction :: forall (ann :: Type). Int -> Index "tyvar" -> PrettyM ann (Doc ann)+lookupAbstraction offset argIndex = do+  let scopeOffset = ScopeBoundary offset+  let argIndex' = review intIndex argIndex+  here <- asks (view #currentScope)+  asks (preview (#boundIdents % ix (here + scopeOffset) % ix argIndex')) >>= \case+    Nothing ->+      -- TODO: actual error reporting+      error $+        "Internal error: The encountered a variable at arg index "+          <> show argIndex'+          <> " with true level "+          <> show scopeOffset+          <> " but could not locate the corresponding pretty form at scope level "+          <> show here+    Just res' -> pure res'
+ src/Covenant/Internal/Unification.hs view
@@ -0,0 +1,251 @@+{-# LANGUAGE CPP #-}++module Covenant.Internal.Unification+  ( TypeAppError (..),+    checkApp,+  )+where++import Control.Monad (foldM, unless)+import Data.Ord (comparing)+#if __GLASGOW_HASKELL__==908+import Data.Foldable (foldl')+#endif+import Control.Monad.Except (catchError, throwError)+import Covenant.Index (Index, intCount, intIndex)+import Covenant.Internal.Type+  ( BuiltinFlatT,+    CompT (CompT),+    CompTBody (CompTBody),+    Renamed (Rigid, Unifiable, Wildcard),+    ValT (Abstraction, BuiltinFlat, ThunkT),+  )+import Data.Kind (Type)+import Data.Map (Map)+import Data.Map.Merge.Strict qualified as Merge+import Data.Map.Strict qualified as Map+import Data.Maybe (fromJust, mapMaybe)+import Data.Set (Set)+import Data.Set qualified as Set+import Data.Vector (Vector)+import Data.Vector qualified as Vector+import Data.Vector.NonEmpty qualified as NonEmpty+import Data.Word (Word64)+import Optics.Core (preview)++-- | @since 1.0.0+data TypeAppError+  = -- | The final type after all arguments are applied is @forall a . a@.+    LeakingUnifiable (Index "tyvar")+  | -- | A wildcard (thus, a skolem) escaped its scope.+    LeakingWildcard Word64 Int (Index "tyvar")+  | -- | We were given too many arguments.+    ExcessArgs (CompT Renamed) (Vector (Maybe (ValT Renamed)))+  | -- | We weren't given enough arguments.+    InsufficientArgs (CompT Renamed)+  | -- | The expected type (first field) and actual type (second field) do not+    -- unify.+    DoesNotUnify (ValT Renamed) (ValT Renamed)+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Show+    )++-- | @since 1.0.0+checkApp :: CompT Renamed -> [Maybe (ValT Renamed)] -> Either TypeAppError (ValT Renamed)+checkApp f@(CompT _ (CompTBody xs)) =+  let (curr, rest) = NonEmpty.uncons xs+   in go curr (Vector.toList rest)+  where+    go ::+      ValT Renamed ->+      [ValT Renamed] ->+      [Maybe (ValT Renamed)] ->+      Either TypeAppError (ValT Renamed)+    go currParam restParams args = case restParams of+      [] -> case args of+        -- If we got here, currParam is the resulting type after all+        -- substitutions have been applied.+        [] -> fixUp currParam+        _ -> throwError . ExcessArgs f . Vector.fromList $ args+      _ -> case args of+        [] -> throwError . InsufficientArgs $ f+        (currArg : restArgs) -> do+          newRestParams <- case currArg of+            -- An error argument unifies with anything, as it's effectively+            -- `forall a . a`. Furthermore, it requires no substitutional+            -- changes. Thus, we can just skip it.+            Nothing -> pure restParams+            Just currArg' -> do+              subs <- catchError (unify currParam currArg') (promoteUnificationError currParam currArg')+              pure . Map.foldlWithKey' applySub restParams $ subs+          case newRestParams of+            [] -> throwError . InsufficientArgs $ f+            (currParam' : restParams') -> go currParam' restParams' restArgs++-- Helpers++applySub ::+  [ValT Renamed] ->+  Index "tyvar" ->+  ValT Renamed ->+  [ValT Renamed]+applySub acc index sub = fmap (substitute index sub) acc++substitute ::+  Index "tyvar" ->+  ValT Renamed ->+  ValT Renamed ->+  ValT Renamed+substitute index toSub = \case+  Abstraction t -> case t of+    Unifiable ourIndex ->+      if ourIndex == index+        then toSub+        else Abstraction t+    _ -> Abstraction t+  ThunkT (CompT abstractions (CompTBody xs)) ->+    ThunkT . CompT abstractions . CompTBody . fmap (substitute index toSub) $ xs+  BuiltinFlat t -> BuiltinFlat t++-- Because unification is inherently recursive, if we find an error deep within+-- a type, the message will signify only the _part_ that fails to unify, not the+-- entire type. While potentially useful, this can be quite confusing,+-- especially with generated types. Thus, we use `catchError` with this+-- function, which effectively allows us to rename the types reported in+-- unification errors to whatever types 'wrap' them.+promoteUnificationError ::+  forall (a :: Type).+  ValT Renamed ->+  ValT Renamed ->+  TypeAppError ->+  Either TypeAppError a+promoteUnificationError topLevelExpected topLevelActual =+  Left . \case+    DoesNotUnify _ _ -> DoesNotUnify topLevelExpected topLevelActual+    err -> err++fixUp :: ValT Renamed -> Either TypeAppError (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+  -- This can be a problem, as we might be referring to unifiables that don't+  -- exist anymore+  ThunkT (CompT _ (CompTBody xs)) -> do+    -- Figure out how many variables the thunk has to introduce now+    let remainingUnifiables = NonEmpty.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty xs+    let requiredIntroductions = Set.size remainingUnifiables+    -- We know that the size of a set can't be negative, but GHC doesn't.+    let asCount = fromJust . preview intCount $ requiredIntroductions+    -- Make enough indexes for us to use in one go+    let indexesToUse = mapMaybe (preview intIndex) [0, 1 .. requiredIntroductions - 1]+    -- Construct a mapping between old, possibly non-contiguous, unifiables and+    -- our new ones+    let renames =+          zipWith+            (\i replacement -> (i, Abstraction . Unifiable $ replacement))+            (Set.toList remainingUnifiables)+            indexesToUse+    let fixed = fmap (\t -> foldl' (\acc (i, r) -> substitute i r acc) t renames) xs+    pure . ThunkT . CompT asCount . CompTBody $ fixed+  t -> pure t++collectUnifiables :: ValT Renamed -> Set (Index "tyvar")+collectUnifiables = \case+  Abstraction t -> case t of+    Unifiable index -> Set.singleton index+    _ -> Set.empty+  BuiltinFlat _ -> Set.empty+  ThunkT (CompT _ (CompTBody xs)) -> NonEmpty.foldl' (\acc t -> acc <> collectUnifiables t) Set.empty xs++unify ::+  ValT Renamed ->+  ValT Renamed ->+  Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+unify expected actual =+  catchError+    ( case expected of+        Abstraction t1 -> case t1 of+          -- Unifiables unify with everything, and require a substitutional rewrite.+          Unifiable index1 -> pure . Map.singleton index1 $ actual+          Rigid level1 index1 -> expectRigid level1 index1+          Wildcard scopeId1 _ index1 -> expectWildcard scopeId1 index1+        ThunkT t1 -> expectThunk t1+        BuiltinFlat t1 -> expectFlatBuiltin t1+    )+    (promoteUnificationError expected actual)+  where+    unificationError :: forall (a :: Type). Either TypeAppError a+    unificationError = Left . DoesNotUnify expected $ actual+    noSubUnify :: forall (k :: Type) (a :: Type). Either TypeAppError (Map k a)+    noSubUnify = pure Map.empty+    expectRigid ::+      Int -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+    -- Rigids behave identically to concrete types: they can unify with+    -- themselves, or any other abstraction, but nothing else. No substitutional+    -- rewrites are needed.+    expectRigid level1 index1 = case actual of+      Abstraction (Rigid level2 index2) ->+        if level1 == level2 && index1 == index2+          then noSubUnify+          else unificationError+      Abstraction _ -> noSubUnify+      _ -> unificationError+    expectWildcard ::+      Word64 -> Index "tyvar" -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+    -- Wildcards can unify with unifiables, as well as themselves, but nothing+    -- else. No substitutional rewrites are needed.+    expectWildcard scopeId1 index1 = case actual of+      Abstraction (Unifiable _) -> noSubUnify+      Abstraction (Wildcard scopeId2 _ index2) ->+        if scopeId1 /= scopeId2 || index1 == index2+          then noSubUnify+          else unificationError+      _ -> unificationError+    expectThunk :: CompT Renamed -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+    -- Thunks unify unconditionally with wildcards or unifiables. They unify+    -- conditionally with other thunks, provided that we can unify each argument+    -- with its counterpart in the same position, as well as their result types,+    -- without conflicts.+    expectThunk (CompT _ (CompTBody t1)) = case actual of+      Abstraction (Rigid _ _) -> unificationError+      Abstraction _ -> noSubUnify+      ThunkT (CompT _ (CompTBody t2)) -> do+        unless (comparing NonEmpty.length t1 t2 == EQ) unificationError+        catchError+          (foldM (\acc (l, r) -> unify l r >>= reconcile acc) Map.empty . NonEmpty.zip t1 $ t2)+          (promoteUnificationError expected actual)+      _ -> unificationError+    expectFlatBuiltin :: BuiltinFlatT -> Either TypeAppError (Map (Index "tyvar") (ValT Renamed))+    -- 'Flat' builtins are always concrete. They can unify with themselves,+    -- unifiables or wildcards, but nothing else. No substitutional rewrites are+    -- needed.+    expectFlatBuiltin t1 = case actual of+      Abstraction (Rigid _ _) -> unificationError+      Abstraction _ -> noSubUnify+      BuiltinFlat t2 ->+        if t1 == t2+          then noSubUnify+          else unificationError+      _ -> unificationError+    reconcile ::+      Map (Index "tyvar") (ValT Renamed) ->+      Map (Index "tyvar") (ValT Renamed) ->+      Either TypeAppError (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 $ \_ l r -> l <$ unless (l == r) unificationError)
+ src/Covenant/Prim.hs view
@@ -0,0 +1,437 @@+-- |+-- Module: Covenant.Prim+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- Contains definitions relating to Plutus primitive functions in Covenant+-- programs.+--+-- = Note+--+-- In the 1.0.0 release, we didn't include non-flat builtin types, specifically+-- pairs, lists and @Data@. Thus, the primops that operate on, or produce, these+-- are not currently included.+--+-- @since 1.0.0+module Covenant.Prim+  ( OneArgFunc (..),+    typeOneArgFunc,+    TwoArgFunc (..),+    typeTwoArgFunc,+    ThreeArgFunc (..),+    typeThreeArgFunc,+    -- SixArgFunc (..),+    -- typeSixArgFunc,+  )+where++import Covenant.DeBruijn (DeBruijn (Z))+import Covenant.Index (ix0)+import Covenant.Type+  ( AbstractTy,+    CompT (Comp0, Comp1),+    CompTBody (ReturnT, (:--:>)),+    ValT,+    boolT,+    byteStringT,+    g1T,+    g2T,+    integerT,+    mlResultT,+    stringT,+    tyvar,+    unitT,+  )+import Test.QuickCheck (Arbitrary (arbitrary), elements)++-- | All one-argument primitives provided by Plutus.+--+-- = Note+--+-- We exclude the @MkNilData@ and @MkNilPairData@ primitives from this list for+-- several reasons. For clarity, we list these below. Firstly, the reason why+-- these primitives still exist at all is historical: Plutus now has the ability+-- to directly \'lift\' empty list constants into itself. Secondly, while these+-- primitives /could/ still be used instead of direct lifts, there is never a+-- reason to prefer them, as they are less efficient than embedding a constant+-- directly. Thirdly, their naive typings would end up with overdetermined type+-- variables - consider the typing of @MkNilData@:+--+-- @forall a . () -> ![a]@+--+-- For all of these reasons, we do not represent these primitives in the ASG.+--+-- @since 1.0.0+data OneArgFunc+  = LengthOfByteString+  | Sha2_256+  | Sha3_256+  | Blake2b_256+  | EncodeUtf8+  | DecodeUtf8+  | --  | FstPair+    --  |  SndPair+    --  | HeadList+    --  | TailList+    --  | NullList+    --  | MapData+    --  | ListData+    --  | IData+    --  | BData+    --  | UnConstrData+    --  | UnMapData+    --  | UnListData+    --  | UnIData+    --  | UnBData+    --  | SerialiseData+    BLS12_381_G1_neg+  | BLS12_381_G1_compress+  | BLS12_381_G1_uncompress+  | BLS12_381_G2_neg+  | BLS12_381_G2_compress+  | BLS12_381_G2_uncompress+  | Keccak_256+  | Blake2b_224+  | ComplementByteString+  | CountSetBits+  | FindFirstSetBit+  | Ripemd_160+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | Does not shrink.+--+-- @since 1.0.0+instance Arbitrary OneArgFunc where+  {-# INLINEABLE arbitrary #-}+  arbitrary =+    elements+      [ LengthOfByteString,+        Sha2_256,+        Sha3_256,+        Blake2b_256,+        EncodeUtf8,+        DecodeUtf8,+        -- FstPair,+        -- SndPair,+        -- HeadList,+        -- TailList,+        -- NullList,+        -- MapData,+        -- ListData,+        -- IData,+        -- BData,+        -- UnConstrData,+        -- UnMapData,+        -- UnListData,+        -- UnIData,+        -- UnBData,+        -- SerialiseData,+        BLS12_381_G1_neg,+        BLS12_381_G1_compress,+        BLS12_381_G1_uncompress,+        BLS12_381_G2_neg,+        BLS12_381_G2_compress,+        BLS12_381_G2_uncompress,+        Keccak_256,+        Blake2b_224,+        ComplementByteString,+        CountSetBits,+        FindFirstSetBit,+        Ripemd_160+      ]++-- | Produce the type of a single-argument primop.+--+-- @since 1.0.0+typeOneArgFunc :: OneArgFunc -> CompT AbstractTy+typeOneArgFunc = \case+  LengthOfByteString -> Comp0 $ byteStringT :--:> ReturnT integerT+  Sha2_256 -> hashingT+  Sha3_256 -> hashingT+  Blake2b_256 -> hashingT+  EncodeUtf8 -> Comp0 $ stringT :--:> ReturnT byteStringT+  DecodeUtf8 -> Comp0 $ byteStringT :--:> ReturnT stringT+  BLS12_381_G1_neg -> Comp0 $ g1T :--:> ReturnT g1T+  BLS12_381_G1_compress -> Comp0 $ g1T :--:> ReturnT byteStringT+  BLS12_381_G1_uncompress -> Comp0 $ byteStringT :--:> ReturnT g1T+  BLS12_381_G2_neg -> Comp0 $ g2T :--:> ReturnT g2T+  BLS12_381_G2_compress -> Comp0 $ g2T :--:> ReturnT byteStringT+  BLS12_381_G2_uncompress -> Comp0 $ byteStringT :--:> ReturnT g2T+  Keccak_256 -> hashingT+  Blake2b_224 -> hashingT+  ComplementByteString -> Comp0 $ byteStringT :--:> ReturnT byteStringT+  CountSetBits -> Comp0 $ byteStringT :--:> ReturnT integerT+  FindFirstSetBit -> Comp0 $ byteStringT :--:> ReturnT integerT+  Ripemd_160 -> hashingT+  where+    hashingT :: CompT AbstractTy+    hashingT = Comp0 $ byteStringT :--:> ReturnT byteStringT++-- | All two-argument primitives provided by Plutus.+--+-- @since 1.0.0+data TwoArgFunc+  = AddInteger+  | SubtractInteger+  | MultiplyInteger+  | DivideInteger+  | QuotientInteger+  | RemainderInteger+  | ModInteger+  | EqualsInteger+  | LessThanInteger+  | LessThanEqualsInteger+  | AppendByteString+  | ConsByteString+  | IndexByteString+  | EqualsByteString+  | LessThanByteString+  | LessThanEqualsByteString+  | AppendString+  | EqualsString+  | ChooseUnit+  | Trace+  | -- | MkCons+    -- | ConstrData+    -- | EqualsData+    -- | MkPairData+    BLS12_381_G1_add+  | BLS12_381_G1_scalarMul+  | BLS12_381_G1_equal+  | BLS12_381_G1_hashToGroup+  | BLS12_381_G2_add+  | BLS12_381_G2_scalarMul+  | BLS12_381_G2_equal+  | BLS12_381_G2_hashToGroup+  | BLS12_381_millerLoop+  | BLS12_381_mulMlResult+  | BLS12_381_finalVerify+  | ByteStringToInteger+  | ReadBit+  | ReplicateByte+  | ShiftByteString+  | RotateByteString+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | Does not shrink.+--+-- @since 1.0.0+instance Arbitrary TwoArgFunc where+  {-# INLINEABLE arbitrary #-}+  arbitrary =+    elements+      [ AddInteger,+        SubtractInteger,+        MultiplyInteger,+        DivideInteger,+        QuotientInteger,+        RemainderInteger,+        ModInteger,+        EqualsInteger,+        LessThanInteger,+        LessThanEqualsInteger,+        AppendByteString,+        ConsByteString,+        IndexByteString,+        EqualsByteString,+        LessThanByteString,+        LessThanEqualsByteString,+        AppendString,+        EqualsString,+        ChooseUnit,+        Trace,+        -- MkCons,+        -- ConstrData,+        -- EqualsData,+        -- MkPairData,+        BLS12_381_G1_add,+        BLS12_381_G1_scalarMul,+        BLS12_381_G1_equal,+        BLS12_381_G1_hashToGroup,+        BLS12_381_G2_add,+        BLS12_381_G2_scalarMul,+        BLS12_381_G2_equal,+        BLS12_381_G2_hashToGroup,+        BLS12_381_millerLoop,+        BLS12_381_mulMlResult,+        BLS12_381_finalVerify,+        ByteStringToInteger,+        ReadBit,+        ReplicateByte,+        ShiftByteString,+        RotateByteString+      ]++-- | Produce the type of a two-argument primop.+--+-- @since 1.0.0+typeTwoArgFunc :: TwoArgFunc -> CompT AbstractTy+typeTwoArgFunc = \case+  AddInteger -> combineT integerT+  SubtractInteger -> combineT integerT+  MultiplyInteger -> combineT integerT+  DivideInteger -> combineT integerT+  QuotientInteger -> combineT integerT+  RemainderInteger -> combineT integerT+  ModInteger -> combineT integerT+  EqualsInteger -> compareT integerT+  LessThanInteger -> compareT integerT+  LessThanEqualsInteger -> compareT integerT+  AppendByteString -> combineT byteStringT+  ConsByteString -> Comp0 $ integerT :--:> byteStringT :--:> ReturnT byteStringT+  IndexByteString -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT integerT+  EqualsByteString -> compareT byteStringT+  LessThanByteString -> compareT byteStringT+  LessThanEqualsByteString -> compareT byteStringT+  AppendString -> combineT stringT+  EqualsString -> compareT stringT+  ChooseUnit -> Comp1 $ unitT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)+  Trace -> Comp1 $ stringT :--:> tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)+  BLS12_381_G1_add -> combineT g1T+  BLS12_381_G1_scalarMul -> Comp0 $ integerT :--:> g1T :--:> ReturnT g1T+  BLS12_381_G1_equal -> compareT g1T+  BLS12_381_G1_hashToGroup -> Comp0 $ byteStringT :--:> byteStringT :--:> ReturnT g1T+  BLS12_381_G2_add -> combineT g2T+  BLS12_381_G2_scalarMul -> Comp0 $ integerT :--:> g2T :--:> ReturnT g2T+  BLS12_381_G2_equal -> compareT g2T+  BLS12_381_G2_hashToGroup -> Comp0 $ byteStringT :--:> byteStringT :--:> ReturnT g2T+  BLS12_381_millerLoop -> Comp0 $ g1T :--:> g2T :--:> ReturnT mlResultT+  BLS12_381_mulMlResult -> combineT mlResultT+  BLS12_381_finalVerify -> Comp0 $ mlResultT :--:> mlResultT :--:> ReturnT boolT+  ByteStringToInteger -> Comp0 $ boolT :--:> byteStringT :--:> ReturnT integerT+  ReadBit -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT boolT+  ReplicateByte -> Comp0 $ integerT :--:> integerT :--:> ReturnT byteStringT+  ShiftByteString -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT byteStringT+  RotateByteString -> Comp0 $ byteStringT :--:> integerT :--:> ReturnT byteStringT+  where+    combineT :: ValT AbstractTy -> CompT AbstractTy+    combineT t = Comp0 $ t :--:> t :--:> ReturnT t+    compareT :: ValT AbstractTy -> CompT AbstractTy+    compareT t = Comp0 $ t :--:> t :--:> ReturnT boolT++-- | All three-argument primitives provided by Plutus.+--+-- @since 1.0.0+data ThreeArgFunc+  = VerifyEd25519Signature+  | VerifyEcdsaSecp256k1Signature+  | VerifySchnorrSecp256k1Signature+  | IfThenElse+  | -- | ChooseList+    -- | CaseList+    IntegerToByteString+  | AndByteString+  | OrByteString+  | XorByteString+  | -- | WriteBits+    ExpModInteger+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | Does not shrink.+--+-- @since 1.0.0+instance Arbitrary ThreeArgFunc where+  {-# INLINEABLE arbitrary #-}+  arbitrary =+    elements+      [ VerifyEd25519Signature,+        VerifyEcdsaSecp256k1Signature,+        VerifySchnorrSecp256k1Signature,+        IfThenElse,+        -- ChooseList,+        -- CaseList,+        IntegerToByteString,+        AndByteString,+        OrByteString,+        XorByteString,+        -- WriteBits,+        ExpModInteger+      ]++-- | Produce the type of a three-argument primop.+--+-- @since 1.0.0+typeThreeArgFunc :: ThreeArgFunc -> CompT AbstractTy+typeThreeArgFunc = \case+  VerifyEd25519Signature -> signatureT+  VerifyEcdsaSecp256k1Signature -> signatureT+  VerifySchnorrSecp256k1Signature -> signatureT+  IfThenElse ->+    Comp1 $+      boolT+        :--:> tyvar Z ix0+        :--:> tyvar Z ix0+        :--:> ReturnT (tyvar Z ix0)+  IntegerToByteString ->+    Comp0 $+      boolT :--:> integerT :--:> integerT :--:> ReturnT byteStringT+  AndByteString -> bitwiseT+  OrByteString -> bitwiseT+  XorByteString -> bitwiseT+  ExpModInteger ->+    Comp0 $+      integerT+        :--:> integerT+        :--:> integerT+        :--:> ReturnT integerT+  where+    signatureT :: CompT AbstractTy+    signatureT =+      Comp0 $+        byteStringT+          :--:> byteStringT+          :--:> byteStringT+          :--:> ReturnT boolT+    bitwiseT :: CompT AbstractTy+    bitwiseT =+      Comp0 $+        boolT+          :--:> byteStringT+          :--:> byteStringT+          :--:> ReturnT byteStringT++{-+-- | All six-argument primitives provided by Plutus.+--+-- @since 1.0.0+data SixArgFunc+  = ChooseData+  | CaseData+  deriving stock+    ( -- | @since 1.0.0+      Eq,+      -- | @since 1.0.0+      Ord,+      -- | @since 1.0.0+      Show+    )++-- | Does not shrink.+--+-- @since 1.0.0+instance Arbitrary SixArgFunc where+  {-# INLINEABLE arbitrary #-}+  arbitrary = elements [ChooseData, CaseData]+-}
+ src/Covenant/Test.hs view
@@ -0,0 +1,104 @@+-- |+-- Module: Covenant.Test+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- Utilities designed to help test Covenant itself.+--+-- @since 1.0.0+module Covenant.Test+  ( Concrete (Concrete),+  )+where++import Control.Applicative ((<|>))+import Covenant.Index (count0)+import Covenant.Type+  ( AbstractTy,+    BuiltinFlatT+      ( BLS12_381_G1_ElementT,+        BLS12_381_G2_ElementT,+        BLS12_381_MlResultT,+        BoolT,+        ByteStringT,+        IntegerT,+        StringT,+        UnitT+      ),+    CompT (Comp0, CompN),+    CompTBody (ArgsAndResult),+    ValT (Abstraction, BuiltinFlat, ThunkT),+  )+import Data.Coerce (coerce)+import Data.Vector qualified as Vector+import Test.QuickCheck+  ( Arbitrary (arbitrary, shrink),+    Gen,+    elements,+    liftArbitrary,+    oneof,+    sized,+  )+import Test.QuickCheck.Instances.Vector ()++-- | Wrapper for 'ValT' to provide an 'Arbitrary' instance to generate only+-- value types without any type variables.+--+-- @since 1.0.0+newtype Concrete = Concrete (ValT AbstractTy)+  deriving+    ( -- | @since 1.0.0+      Eq+    )+    via (ValT AbstractTy)+  deriving stock+    ( -- | @since 1.0.0+      Show+    )++-- | @since 1.0.0+instance Arbitrary Concrete where+  {-# INLINEABLE arbitrary #-}+  arbitrary = Concrete <$> sized go+    where+      go :: Int -> Gen (ValT AbstractTy)+      go size+        | size <= 0 =+            BuiltinFlat+              <$> elements+                [ UnitT,+                  BoolT,+                  IntegerT,+                  StringT,+                  ByteStringT,+                  BLS12_381_G1_ElementT,+                  BLS12_381_G2_ElementT,+                  BLS12_381_MlResultT+                ]+        | otherwise =+            oneof+              [ pure . BuiltinFlat $ UnitT,+                pure . BuiltinFlat $ BoolT,+                pure . BuiltinFlat $ IntegerT,+                pure . BuiltinFlat $ StringT,+                pure . BuiltinFlat $ ByteStringT,+                pure . BuiltinFlat $ BLS12_381_G1_ElementT,+                pure . BuiltinFlat $ BLS12_381_G2_ElementT,+                pure . BuiltinFlat $ BLS12_381_MlResultT,+                ThunkT . Comp0 <$> (ArgsAndResult <$> liftArbitrary (go (size `quot` 4)) <*> go (size `quot` 4))+              ]+  {-# INLINEABLE shrink #-}+  shrink (Concrete v) =+    Concrete <$> case v of+      -- impossible+      Abstraction _ -> []+      ThunkT (CompN _ (ArgsAndResult args result)) ->+        ThunkT . CompN count0 <$> do+          let argsList = Vector.toList args+          argsList' <- fmap coerce . shrink . fmap Concrete $ argsList+          result' <- fmap coerce . shrink . Concrete $ result+          let args' = Vector.fromList argsList'+          pure (ArgsAndResult args' result) <|> pure (ArgsAndResult args result')+      -- Can't shrink this+      BuiltinFlat _ -> []
+ src/Covenant/Type.hs view
@@ -0,0 +1,334 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}++-- |+-- Module: Covenant.Type+-- Copyright: (C) MLabs 2025+-- License: Apache 2.0+-- Maintainer: koz@mlabs.city, sean@mlabs.city+--+-- Covenant's type system and various ways to construct types.+--+-- @since 1.0.0+module Covenant.Type+  ( -- * Type abstractions+    AbstractTy (..),+    Renamed (..),++    -- * Computation types+    CompT (Comp0, Comp1, Comp2, Comp3, CompN),+    CompTBody (ReturnT, (:--:>), ArgsAndResult),+    arity,++    -- * Value types+    ValT (..),+    BuiltinFlatT (..),+    byteStringT,+    integerT,+    stringT,+    tyvar,+    boolT,+    g1T,+    g2T,+    mlResultT,+    unitT,++    -- * Renaming++    -- ** Types+    RenameError (..),+    RenameM,++    -- ** Introduction+    renameValT,+    renameCompT,++    -- ** Elimination+    runRenameM,++    -- * Type application+    TypeAppError (..),+    checkApp,+  )+where++import Control.Monad (guard)+import Covenant.DeBruijn (DeBruijn)+import Covenant.Index+  ( Count,+    Index,+    count0,+    count1,+    count2,+    count3,+    intCount,+  )+import Covenant.Internal.Rename+  ( RenameError+      ( InvalidAbstractionReference,+        IrrelevantAbstraction,+        UndeterminedAbstraction+      ),+    RenameM,+    renameCompT,+    renameValT,+    runRenameM,+  )+import Covenant.Internal.Type+  ( AbstractTy (BoundAt),+    BuiltinFlatT+      ( BLS12_381_G1_ElementT,+        BLS12_381_G2_ElementT,+        BLS12_381_MlResultT,+        BoolT,+        ByteStringT,+        IntegerT,+        StringT,+        UnitT+      ),+    CompT (CompT),+    CompTBody (CompTBody),+    Renamed (Rigid, Unifiable, Wildcard),+    ValT (Abstraction, BuiltinFlat, ThunkT),+  )+import Covenant.Internal.Unification+  ( TypeAppError+      ( DoesNotUnify,+        ExcessArgs,+        InsufficientArgs,+        LeakingUnifiable,+        LeakingWildcard+      ),+    checkApp,+  )+import Data.Coerce (coerce)+import Data.Kind (Type)+import Data.Vector (Vector)+import Data.Vector qualified as Vector+import Data.Vector.NonEmpty (NonEmptyVector)+import Data.Vector.NonEmpty qualified as NonEmpty+import Optics.Core (preview)++-- | The body of a computation type that doesn't take any arguments and produces+-- the a result of the given value type. Use this just as you would a+-- data constructor.+--+-- = Example+--+-- * @'ReturnT' 'integerT'@ is @!Integer@+--+-- @since 1.0.0+pattern ReturnT :: forall (a :: Type). ValT a -> CompTBody a+pattern ReturnT x <- CompTBody (returnHelper -> Just x)+  where+    ReturnT x = CompTBody (NonEmpty.singleton x)++-- | Given a type of argument, and the body of another computation type,+-- construct a copy of the body, adding an extra argument of the argument type.+-- Use this just as you would a data constructor.+--+-- = Note+--+-- Together with 'ReturnT', these two patterns provide an exhaustive pattern+-- match.+--+-- = Example+--+-- * @'integerT' :--:> ReturnT 'byteStringT'@ is @Integer -> !ByteString@+--+-- @since 1.0.0+pattern (:--:>) ::+  forall (a :: Type).+  ValT a ->+  CompTBody a ->+  CompTBody a+pattern x :--:> xs <- CompTBody (arrowHelper -> Just (x, xs))+  where+    x :--:> xs = CompTBody (NonEmpty.cons x (coerce xs))++infixr 1 :--:>++-- | A view of a computation type as a 'Vector' of its argument types, together+-- with its result type. Can be used as a data constructor, and is an exhaustive+-- match.+--+-- = Example+--+-- * @'ArgsAndResult' ('Vector.fromList' ['integerT', 'integerT']) 'integerT'@+--   is @Integer -> Integer -> !Integer@+--+-- @since 1.0.0+pattern ArgsAndResult ::+  forall (a :: Type).+  Vector (ValT a) ->+  ValT a ->+  CompTBody a+pattern ArgsAndResult args result <- (argsAndResultHelper -> (args, result))+  where+    ArgsAndResult args result = CompTBody (NonEmpty.snocV args result)++{-# 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.+--+-- @since 1.0.0+pattern Comp0 ::+  forall (a :: Type).+  CompTBody a ->+  CompT a+pattern Comp0 xs <- (countHelper 0 -> Just xs)+  where+    Comp0 xs = CompT count0 xs++-- | A computation type that binds one type variable (that+-- is, something whose type is @forall a . ... -> ...)@. Use this like a data+-- constructor.+--+-- @since 1.0.0+pattern Comp1 ::+  forall (a :: Type).+  CompTBody a ->+  CompT a+pattern Comp1 xs <- (countHelper 1 -> Just xs)+  where+    Comp1 xs = CompT count1 xs++-- | A computation type that binds two type variables (that+-- is, something whose type is @forall a b . ... -> ...)@. Use this like a data+-- constructor.+--+-- @since 1.0.0+pattern Comp2 ::+  forall (a :: Type).+  CompTBody a ->+  CompT a+pattern Comp2 xs <- (countHelper 2 -> Just xs)+  where+    Comp2 xs = CompT count2 xs++-- | A computation type that binds three type variables+-- (that is, something whose type is @forall a b c . ... -> ...)@. Use this like+-- a data constructor.+--+-- @since 1.0.0+pattern Comp3 ::+  forall (a :: Type).+  CompTBody a ->+  CompT a+pattern Comp3 xs <- (countHelper 3 -> Just xs)+  where+    Comp3 xs = CompT count3 xs++-- | A general way to construct and deconstruct computations which bind an+-- arbitrary number of type variables. Use this like a data constructor. Unlike+-- the other @Comp@ patterns, 'CompN' is exhaustive if matched on.+--+-- @since 1.0.0+pattern CompN ::+  Count "tyvar" ->+  CompTBody AbstractTy ->+  CompT AbstractTy+pattern CompN count xs <- CompT count xs+  where+    CompN count xs = CompT count xs++{-# COMPLETE CompN #-}++-- | Helper for defining type variables.+--+-- @since 1.0.0+tyvar :: DeBruijn -> Index "tyvar" -> ValT AbstractTy+tyvar db = Abstraction . BoundAt db++-- | Helper for defining the value type of builtin bytestrings.+--+-- @since 1.0.0+byteStringT :: forall (a :: Type). ValT a+byteStringT = BuiltinFlat ByteStringT++-- | Helper for defining the value type of builtin integers.+--+-- @since 1.0.0+integerT :: forall (a :: Type). ValT a+integerT = BuiltinFlat IntegerT++-- | Helper for defining the value type of builtin strings.+--+-- @since 1.0.0+stringT :: forall (a :: Type). ValT a+stringT = BuiltinFlat StringT++-- | Helper for defining the value type of builtin booleans.+--+-- @since 1.0.0+boolT :: forall (a :: Type). ValT a+boolT = BuiltinFlat BoolT++-- | Helper for defining the value type of BLS12-381 G1 curve points.+--+-- @since 1.0.0+g1T :: forall (a :: Type). ValT a+g1T = BuiltinFlat BLS12_381_G1_ElementT++-- | Helper for defining the value type of BLS12-381 G2 curve points.+--+-- @since 1.0.0+g2T :: forall (a :: Type). ValT a+g2T = BuiltinFlat BLS12_381_G2_ElementT++-- | Helper for defining the value type of BLS12-381 multiplication results.+--+-- @since 1.0.0+mlResultT :: forall (a :: Type). ValT a+mlResultT = BuiltinFlat BLS12_381_MlResultT++-- | Helper for defining the value type of the builtin unit type.+--+-- @since 1.0.0+unitT :: forall (a :: Type). ValT a+unitT = BuiltinFlat UnitT++-- Helpers++returnHelper ::+  forall (a :: Type).+  NonEmptyVector (ValT a) ->+  Maybe (ValT a)+returnHelper xs = case NonEmpty.uncons xs of+  (y, ys) ->+    if Vector.length ys == 0+      then pure y+      else Nothing++arrowHelper ::+  forall (a :: Type).+  NonEmptyVector (ValT a) ->+  Maybe (ValT a, CompTBody a)+arrowHelper xs = case NonEmpty.uncons xs of+  (y, ys) -> (y,) . CompTBody <$> NonEmpty.fromVector ys++argsAndResultHelper ::+  forall (a :: Type).+  CompTBody a ->+  (Vector (ValT a), ValT a)+argsAndResultHelper (CompTBody xs) = NonEmpty.unsnoc xs++countHelper ::+  forall (a :: Type).+  Int ->+  CompT a ->+  Maybe (CompTBody a)+countHelper expected (CompT actual xs) = do+  expectedCount <- preview intCount expected+  guard (expectedCount == actual)+  pure xs
+ src/Covenant/Util.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE ViewPatterns #-}++-- | Module: Covenant.Util+--+-- Various helpers that don't fit anywhere else.+--+-- @since 1.0.0+module Covenant.Util+  ( pattern NilV,+    pattern ConsV,+  )+where++import Data.Kind (Type)+import Data.Vector.Generic (Vector)+import Data.Vector.Generic qualified as Vector++-- | A pattern matching helper for vectors (of all types), corresponding to @[]@+-- for lists. This pattern is bidirectional, which means it can be used just+-- like a data constructor.+--+-- @since 1.0.0+pattern NilV :: forall (a :: Type) (v :: Type -> Type). (Vector v a) => v a+pattern NilV <- (Vector.uncons -> Nothing)+  where+    NilV = Vector.empty++-- | A pattern matching helper for vectors (of all types), corresponding to @x :+-- xs@-style matches. This is a read-only pattern, which means you can match+-- with it, but not construct; this is done because @cons@ for vectors is+-- inefficient and should thus be used consciously, using appropriate functions.+--+-- Together with 'NilV', 'ConsV' provides an exhaustive match.+--+-- @since 1.0.0+pattern ConsV ::+  forall (a :: Type) (v :: Type -> Type).+  (Vector v a) =>+  a ->+  v a ->+  v a+pattern ConsV x xs <- (Vector.uncons -> Just (x, xs))++{-# COMPLETE NilV, ConsV #-}
+ test/asg/Main.hs view
@@ -0,0 +1,467 @@+{-# LANGUAGE PatternSynonyms #-}++module Main (main) where++import Control.Applicative ((<|>))+import Control.Monad (guard)+import Covenant.ASG+  ( ASG,+    ASGBuilder,+    ASGNode (ACompNode, AValNode),+    CompNodeInfo+      ( Builtin1,+        Builtin2,+        Builtin3,+        Return+      ),+    CovenantError (EmptyASG, TopLevelError, TopLevelValue, TypeError),+    CovenantTypeError+      ( ApplyCompType,+        ApplyToError,+        ApplyToValType,+        ForceCompType,+        ForceError,+        ForceNonThunk,+        LambdaResultsInValType,+        NoSuchArgument,+        ReturnCompType,+        ThunkError,+        ThunkValType+      ),+    Id,+    Ref (AnArg, AnId),+    ValNodeInfo (Lit),+    app,+    arg,+    builtin1,+    builtin2,+    builtin3,+    err,+    force,+    lam,+    lit,+    nodeAt,+    ret,+    runASGBuilder,+    thunk,+    topLevelNode,+  )+import Covenant.Constant (typeConstant)+import Covenant.DeBruijn (DeBruijn (Z))+import Covenant.Index (Index, intIndex, ix0)+import Covenant.Prim+  ( typeOneArgFunc,+    typeThreeArgFunc,+    typeTwoArgFunc,+  )+import Covenant.Test (Concrete (Concrete))+import Covenant.Type+  ( AbstractTy,+    CompT (Comp0, CompN),+    CompTBody (ArgsAndResult, ReturnT),+    ValT,+    arity,+  )+import Covenant.Util (pattern ConsV, pattern NilV)+import Data.Coerce (coerce)+import Data.Kind (Type)+import Data.Maybe (fromJust)+import Data.Vector qualified as Vector+import Optics.Core (preview, review)+import Test.QuickCheck+  ( Gen,+    Property,+    arbitrary,+    conjoin,+    counterexample,+    forAllShrinkShow,+    liftShrink,+    listOf,+    property,+    shrink,+    (===),+  )+import Test.Tasty (adjustOption, defaultMain, testGroup)+import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)+import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)++main :: IO ()+main =+  defaultMain . adjustOption moreTests . testGroup "ASG" $+    [ testCase "empty ASG does not compile" unitEmptyASG,+      testCase "single error does not compile" unitSingleError,+      testCase "forcing an error does not compile" unitForceError,+      testCase "thunking an error does not compile" unitThunkError,+      testProperty "toplevel constant does not compile" propTopLevelConstant,+      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,+      testProperty "applying arguments to a value does not compile" propApplyToVal,+      testProperty "applying arguments to an error does not compile" propApplyToError,+      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+    ]+  where+    moreTests :: QuickCheckTests -> QuickCheckTests+    moreTests = max 10_000++-- Units++unitEmptyASG :: IO ()+unitEmptyASG = do+  let builtUp = pure ()+  let expected = Left EmptyASG+  let actual = runASGBuilder builtUp+  assertEqual "" expected actual++unitSingleError :: IO ()+unitSingleError = do+  let builtUp = err+  let expected = Left TopLevelError+  let actual = runASGBuilder builtUp+  assertEqual "" expected actual++unitForceError :: IO ()+unitForceError = do+  let builtUp = err >>= \i -> force (AnId i)+  let result = runASGBuilder builtUp+  case result of+    Left (TypeError _ ForceError) -> pure ()+    _ -> assertFailure $ "Unexpected result: " <> show result++unitThunkError :: IO ()+unitThunkError = do+  let builtUp = err >>= thunk+  let result = runASGBuilder builtUp+  case result of+    Left (TypeError _ ThunkError) -> pure ()+    _ -> assertFailure $ "Unexpected result: " <> show result++-- Properties++propTopLevelConstant :: Property+propTopLevelConstant = forAllShrinkShow arbitrary shrink show $ \c ->+  let builtUp = lit c+   in withCompilationFailure builtUp $ \case+        TopLevelValue _ t info -> case info of+          Lit c' ->+            conjoin+              [ typeConstant c === t,+                c' === c+              ]+          _ -> failUnexpectedValNodeInfo info+        err' -> failWithCounterExample ("Unexpected failure type: " <> show err')++propTopLevelBuiltin1 :: Property+propTopLevelBuiltin1 = forAllShrinkShow arbitrary shrink show $ \bi1 ->+  let builtUp = builtin1 bi1+   in withCompilationSuccess builtUp $ \asg ->+        withToplevelCompNode asg $ \t info ->+          case info of+            Builtin1 bi ->+              conjoin+                [ t === typeOneArgFunc bi1,+                  bi === bi1+                ]+            _ -> failUnexpectedCompNodeInfo info++propTopLevelBuiltin2 :: Property+propTopLevelBuiltin2 = forAllShrinkShow arbitrary shrink show $ \bi2 ->+  let builtUp = builtin2 bi2+   in withCompilationSuccess builtUp $ \asg ->+        withToplevelCompNode asg $ \t info ->+          case info of+            Builtin2 bi ->+              conjoin+                [ t === typeTwoArgFunc bi2,+                  bi === bi2+                ]+            _ -> failUnexpectedCompNodeInfo info++propTopLevelBuiltin3 :: Property+propTopLevelBuiltin3 = forAllShrinkShow arbitrary shrink show $ \bi3 ->+  let builtUp = builtin3 bi3+   in withCompilationSuccess builtUp $ \asg ->+        withToplevelCompNode asg $ \t info ->+          case info of+            Builtin3 bi ->+              conjoin+                [ t === typeThreeArgFunc bi3,+                  bi === bi3+                ]+            _ -> 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+propForceThunk = forAllShrinkShow arbitrary shrink show $ \x ->+  let (comp, forceThunkComp) = case x of+        Left bi1 -> mkComps builtin1 bi1+        Right (Left bi2) -> mkComps builtin2 bi2+        Right (Right bi3) -> mkComps builtin3 bi3+   in withCompilationSuccess comp $ \expectedASG ->+        withCompilationSuccess forceThunkComp $ \forceThunkASG ->+          withToplevelCompNode expectedASG $ \expectedT _ ->+            withToplevelCompNode forceThunkASG $ \actualT _ ->+              expectedT === actualT+  where+    mkComps ::+      forall (a :: Type).+      (a -> ASGBuilder Id) -> a -> (ASGBuilder Id, ASGBuilder Id)+    mkComps f x =+      let comp = f x+          forceThunkComp = do+            i <- comp+            thunkI <- thunk i+            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)+      expectedT = case x of+        Left bi1 -> typeOneArgFunc bi1+        Right (Left bi2) -> typeTwoArgFunc bi2+        Right (Right bi3) -> typeThreeArgFunc bi3+   in withCompilationFailure comp $ \case+        TypeError _ (ForceCompType actualT) -> expectedT === actualT+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++propForceNonThunk :: Property+propForceNonThunk = forAllShrinkShow arbitrary shrink show $ \c ->+  let comp = do+        i <- lit c+        force (AnId i)+   in withCompilationFailure comp $ \case+        TypeError _ (ForceNonThunk actualT) -> typeConstant c === actualT+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++propThunkValType :: Property+propThunkValType = forAllShrinkShow arbitrary shrink show $ \c ->+  let comp = do+        i <- lit c+        thunk i+   in withCompilationFailure comp $ \case+        TypeError _ (ThunkValType actualT) -> typeConstant c === actualT+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++propApplyToVal :: Property+propApplyToVal = forAllShrinkShow arbitrary shrink show $ \c args ->+  let comp = do+        args' <- traverse (fmap AnId . lit) args+        i <- lit c+        app i args'+   in withCompilationFailure comp $ \case+        TypeError _ (ApplyToValType t) -> typeConstant c === t+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++propApplyToError :: Property+propApplyToError = forAllShrinkShow arbitrary shrink show $ \args ->+  let comp = do+        args' <- traverse (fmap AnId . lit) args+        i <- err+        app i args'+   in withCompilationFailure comp $ \case+        TypeError _ ApplyToError -> property True+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++-- We use only builtins for this test, and specifically a one-argument builtin+-- for the thing being applied to, but this should still demonstrate the+-- behaviour as we expect+propApplyComp :: Property+propApplyComp = forAllShrinkShow arbitrary shrink show $ \f arg1 ->+  let t = case arg1 of+        Left bi1 -> typeOneArgFunc bi1+        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')+   in withCompilationFailure comp $ \case+        TypeError _ (ApplyCompType actualT) -> t === actualT+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++propNonExistentArg :: Property+propNonExistentArg = forAllShrinkShow arbitrary shrink show $ \(db, index) ->+  let comp = arg db index >>= \i -> ret (AnArg i)+   in withCompilationFailure comp $ \case+        TypeError _ (NoSuchArgument db' index') -> conjoin [db === db', index === index']+        TypeError _ err' -> failWrongTypeError err'+        err' -> failWrongError err'++-- Generate a lambda taking an arbitrary (positive) number of arguments, plus a+-- positional index, then return that argument in the body. The type of the+-- lambda we get back should match.+propExistingArg :: Property+propExistingArg = forAllShrinkShow gen shr show $ \(t, index) ->+  let comp = lam t $ do+        arg1 <- arg Z index+        ret (AnArg arg1)+   in withCompilationSuccess comp $ \asg ->+        withToplevelCompNode asg $ \t' _ ->+          t' === t+  where+    gen :: Gen (CompT AbstractTy, Index "arg")+    gen = do+      Concrete argT <- arbitrary+      prefixArgs <- listOf (arbitrary @Concrete)+      suffixArgs <- listOf (arbitrary @Concrete)+      -- We know that lengths can't be negative, but GHC doesn't+      let index = fromJust . preview intIndex $ length prefixArgs+      let args = Vector.fromList $ coerce prefixArgs <> [argT] <> coerce suffixArgs+      pure (Comp0 $ ArgsAndResult args argT, index)+    -- We shrink only in the index and the number of arguments, as shrinking the+    -- argument types themselves doesn't change anything+    shr :: (CompT AbstractTy, Index "arg") -> [(CompT AbstractTy, Index "arg")]+    shr (t@(CompN _ (ArgsAndResult args _)), index)+      | arity t <= 1 = []+      | index == ix0 = do+          args' <- liftShrink (const []) . fmap Concrete $ args+          case args' of+            NilV -> [] -- no arguments left to use+            ConsV (Concrete res') _ -> pure (Comp0 (ArgsAndResult (coerce args') res'), index)+      | otherwise =+          let shrinkOnIndex = do+                index' <- shrink index+                let indexAsInt = review intIndex index+                case args Vector.!? indexAsInt of+                  Nothing -> [] -- Should be impossible+                  Just res' -> pure (Comp0 (ArgsAndResult args res'), index')+              shrinkOnArgs = do+                args' <- liftShrink (const []) . fmap Concrete $ args+                let indexAsInt = review intIndex index+                guard (indexAsInt < Vector.length args')+                case args' Vector.!? indexAsInt of+                  Nothing -> [] -- Should be impossible+                  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'++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'++-- Helpers++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 comp cb = case runASGBuilder comp of+  Left err' -> cb err'+  Right asg -> failWithCounterExample ("Unexpected success: " <> show asg)++withCompilationSuccess :: ASGBuilder Id -> (ASG -> Property) -> Property+withCompilationSuccess comp cb = case runASGBuilder comp of+  Left err' -> failWithCounterExample ("Unexpected failure: " <> show err')+  Right asg -> cb asg++withToplevelCompNode :: ASG -> (CompT AbstractTy -> CompNodeInfo -> Property) -> Property+withToplevelCompNode asg cb = case topLevelNode asg of+  ACompNode t info -> cb t info+  node -> failWithCounterExample ("Unexpected toplevel node: " <> show node)++failWithCounterExample :: String -> Property+failWithCounterExample msg = counterexample msg . property $ False++failUnexpectedCompNodeInfo :: CompNodeInfo -> Property+failUnexpectedCompNodeInfo info =+  failWithCounterExample ("Unexpected CompNodeInfo: " <> show info)++failUnexpectedValNodeInfo :: ValNodeInfo -> Property+failUnexpectedValNodeInfo info =+  failWithCounterExample ("Unexpected ValNodeInfo: " <> show info)++withExpectedId :: Ref -> (Id -> Property) -> Property+withExpectedId r cb = case r of+  AnId i -> cb i+  AnArg arg' -> failWithCounterExample ("Unexpected argument: " <> show arg')++withExpectedValNode :: Id -> ASG -> (ValT AbstractTy -> ValNodeInfo -> Property) -> Property+withExpectedValNode i asg cb = case nodeAt i asg of+  AValNode t info -> cb t info+  node -> failWithCounterExample ("Unexpected node: " <> show node)
+ test/primops/Main.hs view
@@ -0,0 +1,108 @@+module Main (main) where++import Covenant.Prim+  ( typeOneArgFunc,+    typeThreeArgFunc,+    typeTwoArgFunc,+  )+import Covenant.Type+  ( AbstractTy (BoundAt),+    CompT,+    Renamed (Unifiable),+    arity,+    renameCompT,+    runRenameM,+  )+import Data.Functor.Classes (liftEq)+import Data.Kind (Type)+import Test.QuickCheck+  ( Arbitrary (arbitrary),+    Property,+    counterexample,+    forAll,+    property,+    (===),+  )+import Test.Tasty (defaultMain, testGroup)+import Test.Tasty.QuickCheck (testProperty)++main :: IO ()+main =+  defaultMain . testGroup "Primops" $+    [ -- Since there are so few primops, we don't increase the test count+      -- beyond the default 100, as it would just be redundant.+      testGroup+        "Arity"+        [ testProperty "One-argument primops take one argument" prop1Arg,+          testProperty "Two-argument primops take two arguments" prop2Args,+          testProperty "Three-argument primops take three arguments" prop3Args+          --         testProperty "Six-argument primops take six arguments" prop6Args+        ],+      testGroup+        "Renaming"+        [ testProperty "One-argument primops rename correctly" prop1Rename,+          testProperty "Two-argument primops rename correctly" prop2Rename,+          testProperty "Three-argument primops rename correctly" prop3Rename+          -- testProperty "Six-argument primops rename correctly" prop6Rename+        ]+    ]++-- Test cases and properties++prop1Arg :: Property+prop1Arg = mkArgProp typeOneArgFunc 1++prop1Rename :: Property+prop1Rename = mkRenameProp typeOneArgFunc++prop2Args :: Property+prop2Args = mkArgProp typeTwoArgFunc 2++prop2Rename :: Property+prop2Rename = mkRenameProp typeTwoArgFunc++prop3Args :: Property+prop3Args = mkArgProp typeThreeArgFunc 3++prop3Rename :: Property+prop3Rename = mkRenameProp typeThreeArgFunc++{-+prop6Args :: Property+prop6Args = mkArgProp typeSixArgFunc 6++prop6Rename :: Property+prop6Rename = mkRenameProp typeSixArgFunc+-}++-- Helpers++mkArgProp ::+  forall (a :: Type).+  (Show a, Arbitrary a) =>+  (a -> CompT AbstractTy) ->+  Int ->+  Property+mkArgProp typingFun targetArity = forAll arbitrary $ \f ->+  let t = typingFun f+   in arity t === targetArity++mkRenameProp ::+  forall (a :: Type).+  (Show a, Arbitrary a) =>+  (a -> CompT AbstractTy) ->+  Property+mkRenameProp typingFun = forAll arbitrary $ \f ->+  let t = typingFun f+      result = runRenameM . renameCompT $ t+   in case result of+        Left err -> counterexample (show err) False+        Right renamed -> property $ liftEq eqRenamedVar t renamed++-- In our context, the _only_ variables we have are unifiable. If we see+-- anything else, we know we've messed up somewhere. Furthermore, the indexes+-- should 'line up'.+eqRenamedVar :: AbstractTy -> Renamed -> Bool+eqRenamedVar (BoundAt _ ix) = \case+  Unifiable ix' -> ix == ix'+  _ -> False
+ test/renaming/Main.hs view
@@ -0,0 +1,185 @@+{-# LANGUAGE OverloadedLists #-}+{-# LANGUAGE PatternSynonyms #-}++module Main (main) where++import Covenant.DeBruijn (DeBruijn (S, Z))+import Covenant.Index+  ( ix0,+    ix1,+  )+import Covenant.Test (Concrete (Concrete))+import Covenant.Type+  ( BuiltinFlatT+      ( BLS12_381_G1_ElementT,+        BLS12_381_G2_ElementT,+        BLS12_381_MlResultT,+        BoolT,+        ByteStringT,+        IntegerT,+        StringT,+        UnitT+      ),+    CompT (Comp0, Comp1, Comp2),+    RenameError+      ( InvalidAbstractionReference,+        UndeterminedAbstraction+      ),+    Renamed (Unifiable, Wildcard),+    ValT (Abstraction, BuiltinFlat, ThunkT),+    renameCompT,+    renameValT,+    runRenameM,+    tyvar,+    pattern ReturnT,+    pattern (:--:>),+  )+import Data.Functor.Classes (liftEq)+import Data.Kind (Type)+import Test.QuickCheck+  ( Arbitrary (arbitrary, shrink),+    Property,+    forAllShrinkShow,+  )+import Test.Tasty (adjustOption, defaultMain, testGroup)+import Test.Tasty.HUnit (assertBool, assertEqual, testCase)+import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)++main :: IO ()+main =+  defaultMain . adjustOption moreTests . testGroup "Renaming" $+    [ testGroup+        "Builtin flat types"+        [ testCase "UnitT" $ testFlat UnitT,+          testCase "BoolT" $ testFlat BoolT,+          testCase "IntegerT" $ testFlat IntegerT,+          testCase "StringT" $ testFlat StringT,+          testCase "ByteStringT" $ testFlat ByteStringT,+          testCase "G1ElementT" $ testFlat BLS12_381_G1_ElementT,+          testCase "G2ElementT" $ testFlat BLS12_381_G2_ElementT,+          testCase "MlResultT" $ testFlat BLS12_381_MlResultT+        ],+      testProperty "Nested concrete types" propNestedConcrete,+      testCase "forall a . a -> !a" testIdT,+      testCase "forall a b . a -> b -> !a" testConstT,+      testCase "forall a . a -> !(forall b . b -> !a)" testConstT2,+      testGroup+        "Overdeterminance"+        [ testCase "forall a b . a -> !(b -> !a)" testDodgyConstT,+          testCase "forall a b . a -> !a" testDodgyIdT+        ],+      testGroup+        "Non-existent abstractions"+        [ testCase "forall a . b -> !a" testIndexingIdT+        ]+    ]+  where+    -- Note (Koz, 26/02/2025): By default, QuickCheck runs only 100 tests per+    -- property, which is far to few. Using the method below, we can ensure that+    -- we run a decent number of tests, while also permitting more than this to+    -- be set via the CLI if we want.+    moreTests :: QuickCheckTests -> QuickCheckTests+    moreTests = max 10_000++-- Tests and properties++-- Checks that the given 'flat' type renames to itself.+testFlat :: BuiltinFlatT -> IO ()+testFlat t = do+  let input = BuiltinFlat t+  let result = runRenameM . 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+   in case result of+        Left _ -> False+        Right actual -> liftEq (\_ _ -> False) t actual++-- Checks that `forall a . a -> !a` correctly renames.+testIdT :: IO ()+testIdT = do+  let idT = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)+  let expected =+        Comp1 $+          Abstraction (Unifiable ix0)+            :--:> ReturnT (Abstraction (Unifiable ix0))+  let result = runRenameM . renameCompT $ idT+  assertRight (assertEqual "" expected) result++-- Checks that `forall a b . a -> b -> !a` correctly renames.+testConstT :: IO ()+testConstT = do+  let constT = Comp2 $ tyvar Z ix0 :--:> tyvar Z ix1 :--:> ReturnT (tyvar Z ix0)+  let expected =+        Comp2 $+          Abstraction (Unifiable ix0)+            :--:> Abstraction (Unifiable ix1)+            :--:> ReturnT (Abstraction (Unifiable ix0))+  let result = runRenameM . renameCompT $ constT+  assertRight (assertEqual "" expected) result++-- Checks that `forall a . a -> !(forall b . b -> !a)` correctly renames.+testConstT2 :: IO ()+testConstT2 = do+  let constT =+        Comp1 $ tyvar Z ix0 :--:> ReturnT (ThunkT . Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar (S Z) ix0))+  let expected =+        Comp1 $+          Abstraction (Unifiable ix0)+            :--:> ReturnT+              ( ThunkT . Comp1 $+                  Abstraction (Wildcard 1 2 ix0)+                    :--:> ReturnT (Abstraction (Unifiable ix0))+              )+  let result = runRenameM . renameCompT $ constT+  assertRight (assertEqual "" expected) result++-- Checks that `forall a b . a -> !a` triggers the undetermined variable checker.+testDodgyIdT :: IO ()+testDodgyIdT = do+  let idT = Comp2 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)+  let result = runRenameM . renameCompT $ idT+  case result of+    Left UndeterminedAbstraction -> assertBool "" True+    Left _ -> assertBool "wrong renaming error" False+    _ -> assertBool "renaming succeeded when it should have failed" False++-- Checks that `forall a b. a -> !(b -> !a)` triggers the undetermined variable checker.+testDodgyConstT :: IO ()+testDodgyConstT = do+  let constT =+        Comp2 $+          tyvar Z ix0+            :--:> ReturnT (ThunkT . Comp0 $ tyvar (S Z) ix1 :--:> ReturnT (tyvar (S Z) ix0))+  let result = runRenameM . renameCompT $ constT+  case result of+    Left UndeterminedAbstraction -> assertBool "" True+    Left _ -> assertBool "wrong renaming error" False+    _ -> assertBool "renaming succeeded when it should have failed" False++-- Checks that `forall a . b -> !a` triggers the variable indexing checker.+testIndexingIdT :: IO ()+testIndexingIdT = do+  let t = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix1)+  let result = runRenameM . renameCompT $ t+  case result of+    Left (InvalidAbstractionReference trueLevel ix) -> do+      assertEqual "" trueLevel 1+      assertEqual "" ix ix1+    Left _ -> assertBool "wrong renaming error" False+    _ -> assertBool "renaming succeeded when it should have failed" False++-- Helpers++assertRight ::+  forall (a :: Type) (b :: Type).+  (b -> IO ()) ->+  Either a b ->+  IO ()+assertRight f = \case+  Left _ -> assertBool "renamer errored" False+  Right actual -> f actual
+ test/type-applications/Main.hs view
@@ -0,0 +1,369 @@+{-# LANGUAGE PatternSynonyms #-}++module Main (main) where++import Control.Applicative ((<|>))+import Control.Monad (guard)+import Covenant.DeBruijn (DeBruijn (S, Z), asInt)+import Covenant.Index+  ( Index,+    ix0,+    ix1,+  )+import Covenant.Test (Concrete (Concrete))+import Covenant.Type+  ( AbstractTy,+    CompT (Comp0, Comp1, Comp2),+    Renamed (Rigid, Wildcard),+    TypeAppError+      ( DoesNotUnify,+        ExcessArgs,+        InsufficientArgs+      ),+    ValT+      ( Abstraction,+        ThunkT+      ),+    checkApp,+    integerT,+    renameCompT,+    renameValT,+    runRenameM,+    tyvar,+    pattern ReturnT,+    pattern (:--:>),+  )+import Data.Coerce (coerce)+import Data.Functor.Identity (Identity (Identity))+import Data.Kind (Type)+import Data.Vector qualified as Vector+import Test.QuickCheck+  ( Gen,+    Property,+    arbitrary,+    counterexample,+    discard,+    elements,+    forAllShrink,+    getSize,+    liftShrink,+    oneof,+    shrink,+    suchThat,+    vectorOf,+    (===),+  )+import Test.Tasty (adjustOption, defaultMain, testGroup)+import Test.Tasty.HUnit (assertEqual, assertFailure, testCase)+import Test.Tasty.QuickCheck (QuickCheckTests, testProperty)++main :: IO ()+main =+  defaultMain . adjustOption moreTests . testGroup "Type application" $+    [ testProperty "Too many arguments to id" propTooManyArgs,+      testCase "id on no arguments" unitInsufficientArgs,+      testGroup+        "Substitution"+        [ testProperty "id applied to concrete" propIdConcrete,+          testProperty "two-arg const to same concretes" propConst2Same,+          testProperty "two-arg const to different concretes" propConst2Different+        ],+      testGroup+        "Unification"+        [ testProperty "concrete expected, concrete actual" propUnifyConcrete,+          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,+          testProperty "rigid expected, rigid actual" propUnifyRigid,+          testProperty "wildcard expected, rigid actual" propUnifyWildcardRigid+        ]+    ]+  where+    -- Note (Koz, 26/02/2025): By default, QuickCheck runs only 100 tests per+    -- property, which is far too few. Using the method below, we can ensure that+    -- we run a decent number of tests, while also permitting more than this to+    -- be set via the CLI if we want.+    moreTests :: QuickCheckTests -> QuickCheckTests+    moreTests = max 10_000++-- 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 ->+      case renamedExcessArgs of+        [] -> discard -- should be impossible+        _ : extraArgs ->+          let expected = Left . ExcessArgs renamedIdT . Vector.fromList . fmap Just $ extraArgs+              actual = checkApp renamedIdT (fmap Just renamedExcessArgs)+           in expected === actual+  where+    -- Note (Koz, 14/04/2025): The default size of 100 makes it rather painful+    -- to generate excess arguments, as the generator used for concrete types+    -- is recursive. Furthermore, we need to ensure the list has at least two+    -- elements, which forces too many restarts. Thus, we roll our own.+    gen :: Gen [ValT AbstractTy]+    gen = do+      size <- getSize+      lenIncrease <- elements [0, 1 .. size `quot` 4]+      Concrete firstTy <- arbitrary+      Concrete secondTy <- arbitrary+      ([firstTy, secondTy] <>) <$> vectorOf lenIncrease (coerce @Concrete <$> arbitrary)+    shr :: [ValT AbstractTy] -> [[ValT AbstractTy]]+    shr = \case+      [] -> []+      [_] -> []+      [_, _] -> []+      xs -> liftShrink (coerce . shrink . Concrete) xs++-- Try to apply `forall a . a -> !a` to zero arguments. Result should indicate+-- insufficient arguments.+unitInsufficientArgs :: IO ()+unitInsufficientArgs = do+  renamedIdT <- failLeft . runRenameM . renameCompT $ idT+  let expected = Left . InsufficientArgs $ renamedIdT+  let actual = checkApp renamedIdT []+  assertEqual "" expected actual++-- Try to apply `forall a . a -> !a` to a random concrete type. Result should be+-- that type.+propIdConcrete :: Property+propIdConcrete = forAllShrink arbitrary shrink $ \(Concrete t) ->+  withRenamedComp idT $ \renamedIdT ->+    withRenamedVals (Identity t) $ \(Identity t') ->+      let expected = Right t'+          actual = checkApp renamedIdT [Just t']+       in expected === actual++-- Try to apply `forall a b . a -> b -> !a` to two identical concrete types.+-- Result should be that type.+propConst2Same :: Property+propConst2Same = forAllShrink arbitrary shrink $ \(Concrete t) ->+  withRenamedComp const2T $ \renamedConst2T ->+    withRenamedVals (Identity t) $ \(Identity t') ->+      let expected = Right t'+          actual = checkApp renamedConst2T [Just t', Just t']+       in expected === actual++-- Try to apply `forall a b . a -> b -> !a` to two random _different_ concrete+-- types. Result should be the choice for `a`.+propConst2Different :: Property+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') ->+          let expected = Right t1'+              actual = checkApp renamedConst2T [Just t1', Just t2']+           in expected === actual++-- Randomly pick a concrete type `A`, then pick a type `b` which is either `A`+-- or a type different from `A` (50% of the time each way). Then try to apply `A+-- -> !Integer` to `b`. Result should unify be `Integer` if `b ~ A`, and a+-- unification error otherwise.+propUnifyConcrete :: Property+propUnifyConcrete = forAllShrink gen shr $ \(tA, mtB) ->+  withRenamedComp (Comp0 $ tA :--:> ReturnT integerT) $ \f ->+    withRenamedVals (Identity tA) $ \(Identity tA') ->+      case mtB of+        Nothing ->+          let expected = Right integerT+              actual = checkApp f [Just tA']+           in expected === actual+        Just tB ->+          if tA == tB+            then discard+            else withRenamedVals (Identity tB) $ \(Identity arg) ->+              let expected = Left . DoesNotUnify tA' $ arg+                  actual = checkApp f [Just arg]+               in expected === actual+  where+    -- This ensures that our cases occur with equal frequency.+    gen :: Gen (ValT AbstractTy, Maybe (ValT AbstractTy))+    gen = do+      Concrete x <- arbitrary+      (x,) <$> oneof [pure Nothing, Just . coerce <$> arbitrary @Concrete]+    -- We don't want to 'shrink out of case'; if we have a `Just`, we want to+    -- keep it a `Just`.+    shr :: (ValT AbstractTy, Maybe (ValT AbstractTy)) -> [(ValT AbstractTy, Maybe (ValT AbstractTy))]+    shr (x, my) = do+      Concrete x' <- shrink (Concrete x)+      case my of+        Nothing -> pure (x', Nothing)+        Just y -> do+          Concrete y' <- shrink (Concrete y)+          pure (x', my) <|> pure (x, Just y')++-- Randomly pick a rigid type A and concrete type B, then try to apply `A ->+-- !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 . asInt $ scope+          expected = Left . DoesNotUnify (Abstraction . Rigid trueLevel $ ix) $ t'+          actual = checkApp 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 ->+        let argT = ThunkT . Comp0 $ t :--:> ReturnT integerT+         in withRenamedVals (Identity argT) $ \(Identity argT') ->+              let lhs = ThunkT . Comp1 $ Abstraction (Wildcard 1 2 ix0) :--:> ReturnT integerT+                  expected = Left . DoesNotUnify lhs $ argT'+                  actual = checkApp f [Just argT']+               in expected === actual++-- Randomly generate a concrete type A, then try to apply+-- `(forall a . a -> !A) -> !A` to `forall a . (a -> !A)`. Result should unify+-- 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 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 . asInt $ scope+            expected = Left . DoesNotUnify aT' . Abstraction . Rigid level $ index+            actual = checkApp 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 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.+propUnifyRigid :: Property+propUnifyRigid = forAllShrink gen shr $ \testData ->+  withTestData testData $ \(f, arg, expected) ->+    let actual = checkApp f [Just arg]+     in expected === actual+  where+    gen :: Gen (DeBruijn, Index "tyvar", Maybe (Either DeBruijn (Index "tyvar")))+    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 . 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)++-- 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 ->+        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+                  expected = Left . DoesNotUnify lhs $ argT'+                  actual = checkApp f [Just argT']+               in expected === actual++-- Helpers++-- `forall a. a -> !a`+idT :: CompT AbstractTy+idT = Comp1 $ tyvar Z ix0 :--:> ReturnT (tyvar Z ix0)++-- `forall a b . a -> b -> !a+const2T :: CompT AbstractTy+const2T = Comp2 $ tyvar Z ix0 :--:> tyvar Z ix1 :--:> ReturnT (tyvar Z ix0)++failLeft ::+  forall (a :: Type) (b :: Type).+  (Show a) =>+  Either a b ->+  IO b+failLeft = either (assertFailure . show) pure++withRenamedComp ::+  CompT AbstractTy ->+  (CompT Renamed -> Property) ->+  Property+withRenamedComp t f = case runRenameM . renameCompT $ t of+  Left err -> counterexample (show err) False+  Right t' -> f t'++withRenamedVals ::+  forall (t :: Type -> Type).+  (Traversable t) =>+  t (ValT AbstractTy) ->+  (t (ValT Renamed) -> Property) ->+  Property+withRenamedVals vals f = case runRenameM . traverse renameValT $ vals of+  Left err -> counterexample (show err) False+  Right vals' -> f vals'