morley 1.18.0 → 1.19.0

raw patch · 77 files changed

+4046/−2281 lines, 77 filesdep +constraints-extrasdep +dependent-sum-templatedep +somePVP ok

version bump matches the API change (PVP)

Dependencies added: constraints-extras, dependent-sum-template, some, type-errors

API changes (from Hackage documentation)

Files

• CHANGES.md +139/−0
• README.md +8/−0
• app/Main.hs +22/−27
• app/REPL.hs +2/−1
• morley.cabal +19/−4
• src/Morley/AsRPC.hs +191/−68
• src/Morley/CLI.hs +27/−1
• src/Morley/Micheline/Class.hs +40/−16
• src/Morley/Micheline/Expression.hs +4/−4
• src/Morley/Michelson/Doc.hs +4/−4
• src/Morley/Michelson/Interpret.hs +83/−49
• src/Morley/Michelson/Optimizer.hs +3/−34
• src/Morley/Michelson/Parser.hs +1/−1
• src/Morley/Michelson/Parser/Instr.hs +9/−1
• src/Morley/Michelson/Parser/Value.hs +7/−1
• src/Morley/Michelson/Printer.hs +6/−8
• src/Morley/Michelson/Printer/Util.hs +7/−9
• src/Morley/Michelson/Runtime.hs +123/−82
• src/Morley/Michelson/Runtime/Dummy.hs +22/−3
• src/Morley/Michelson/Runtime/GState.hs +82/−22
• src/Morley/Michelson/Runtime/Import.hs +3/−3
• src/Morley/Michelson/Runtime/RunCode.hs +164/−0
• src/Morley/Michelson/Text.hs +6/−6
• src/Morley/Michelson/TypeCheck.hs +1/−0
• src/Morley/Michelson/TypeCheck/Error.hs +49/−37
• src/Morley/Michelson/TypeCheck/Ext.hs +21/−19
• src/Morley/Michelson/TypeCheck/Helpers.hs +124/−138
• src/Morley/Michelson/TypeCheck/Instr.hs +350/−201
• src/Morley/Michelson/TypeCheck/TypeCheck.hs +124/−67
• src/Morley/Michelson/TypeCheck/TypeCheckedOp.hs +19/−18
• src/Morley/Michelson/TypeCheck/TypeCheckedSeq.hs +11/−11
• src/Morley/Michelson/TypeCheck/Types.hs +15/−15
• src/Morley/Michelson/TypeCheck/Value.hs +60/−76
• src/Morley/Michelson/Typed/Arith.hs +13/−13
• src/Morley/Michelson/Typed/ClassifiedInstr.hs +24/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/HasAnns.hs +139/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/IsAlwaysFailing.hs +138/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/IsMichelson.hs +137/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Classifiers/NumChildren.hs +58/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/InstrEnum.hs +47/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/MainImpl.hs +47/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/TH.hs +85/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/Types.hs +86/−0
• src/Morley/Michelson/Typed/ClassifiedInstr/Internal/WithClassifiedInstr.hs +67/−0
• src/Morley/Michelson/Typed/Convert.hs +150/−156
• src/Morley/Michelson/Typed/Entrypoints.hs +29/−7
• src/Morley/Michelson/Typed/Existential.hs +13/−18
• src/Morley/Michelson/Typed/Haskell/Instr/Product.hs +80/−75
• src/Morley/Michelson/Typed/Haskell/Instr/Sum.hs +41/−47
• src/Morley/Michelson/Typed/Haskell/LooseSum.hs +7/−5
• src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs +22/−28
• src/Morley/Michelson/Typed/Haskell/Value.hs +6/−5
• src/Morley/Michelson/Typed/Instr.hs +79/−44
• src/Morley/Michelson/Typed/Operation.hs +1/−1
• src/Morley/Michelson/Typed/Scope.hs +71/−106
• src/Morley/Michelson/Typed/T.hs +2/−1
• src/Morley/Michelson/Typed/Util.hs +113/−523
• src/Morley/Michelson/Typed/Value.hs +55/−15
• src/Morley/Michelson/Untyped/Entrypoints.hs +18/−2
• src/Morley/Michelson/Untyped/Instr.hs +24/−12
• src/Morley/Michelson/Untyped/Value.hs +2/−0
• src/Morley/Tezos/Address.hs +152/−104
• src/Morley/Tezos/Address/Alias.hs +163/−36
• src/Morley/Tezos/Address/Kinds.hs +3/−0
• src/Morley/Tezos/Core.hs +1/−1
• src/Morley/Tezos/Crypto.hs +71/−33
• src/Morley/Tezos/Crypto/Secp256k1.hs +21/−2
• src/Morley/Tezos/Crypto/Timelock.hs +4/−0
• src/Morley/Util/Constrained.hs +70/−0
• src/Morley/Util/MismatchError.hs +2/−2
• src/Morley/Util/Peano.hs +44/−0
• src/Morley/Util/Sing.hs +9/−0
• src/Morley/Util/TH.hs +57/−5
• src/Morley/Util/Type.hs +117/−102
• src/Morley/Util/TypeTuple/Class.hs +1/−0
• src/Morley/Util/TypeTuple/Instances.hs +11/−0
• src/Morley/Util/TypeTuple/TH.hs +20/−12

@@ -1,6 +1,145 @@ <!-- Unreleased: append new entries here -->  +1.19.0+======+* [!1273](https://gitlab.com/morley-framework/morley/-/merge_requests/1273)+  Add LAMBDA_REC and Lambda_rec support+  + Typed instructions `AnnLAMBDA` and newly introduced `AnnLAMBDA_REC` do not+    carry `VLam` any more, instead they carry `RemFail` directly.+  + New data type `LambdaCode'` introduced, with two constructors, for plain and+    recursive lambdas, respecively.+  + `VLam` now contains `LambdaCode'` instead of `RemFail`.+  + New function `mkVLamRec` for constructing recursive lambda values+    introduced.+* [!1278](https://gitlab.com/morley-framework/morley/-/merge_requests/1278)+  Deprecate `OPEN_CHEST`, related types and values+* [!1281](https://gitlab.com/morley-framework/morley/-/merge_requests/1281)+  Use the new binaries names, `octez-client` and `octez-node`+* [!1270](https://gitlab.com/morley-framework/morley/-/merge_requests/1270)+  Add lima protocol TICKET instruction, rename old one to TICKET_DEPRECATED+  + The `TICKET` instruction was renamed to `TICKET_DEPRECATED`+  + A new `TICKET` instruction was added which no longer allows zero amount+    tickets. It now returns `Some Ticket` and `None` in case of zero amount+    supplied.+* [!1288](https://gitlab.com/morley-framework/morley/-/merge_requests/1288)+  Fix toExpression in nested right pair combs with variable annotations+  + Conversion to Micheline would lose variable annotations on nested right pair+    combs. This issue has been fixed.+* [!1271](https://gitlab.com/morley-framework/morley/-/merge_requests/1271)+  Deprecate `AssertTypesEqual`+  + Use `FailUnlessEqual` instead.+* [!1193](https://gitlab.com/morley-framework/morley/-/merge_requests/1193)+  Use `nest` from `Text.PrettyPrint.Leijen` in instructions rendering instead+  of `Morley.Michelson.Printer.Util.spaces`+* [!1265](https://gitlab.com/morley-framework/morley/-/merge_requests/1265)+  Add parser for ConstrainedAddress `parseConstrainedAddress`+  + Better address parser error reporting+  + Added `FromJSON` instance for `ConstrainedAddress`+* [!1248](https://gitlab.com/morley-framework/morley/-/merge_requests/1248)+  Add `HasAnnotation` deriving to `deriveRPC`+  + New datatype `Morley.AsRPC.DeriveRPCOptions`+  + New helper `Morley.AsRPC.deriveRPCWithOptions`+  + `deriveRPCWithStrategy`, `deriveManyRPC`, `deriveManyRPCWithStrategy` are+    deprecated in favor of `deriveRPCWithOptions`+  + `deriveRPC` now behaves as `deriveManyRPC`, and additionally tries to derive+    `HasAnnotation`. It will error out if `HasAnnotation` is not in scope.+* [!1258](https://gitlab.com/morley-framework/morley/-/merge_requests/1258)+  Support implicit delegation in interpreter+  + Reworked delegate tracking in morley interpreter.+  + Added `unImplicitAddress :: ImplicitAddress -> KeyHash` utility to+    `Morley.Tezos.Address`.+* [!1188](https://gitlab.com/morley-framework/morley/-/merge_requests/1188)+  Straighten out detSecretKey's behavior+  + Add `Morley.Tezos.Crypto.KeyType` enum type encoding secret/public key type.+  + Refactor `HashTag` to use `KeyType`.+  + `detSecretKey` now chooses key type based on the seed, not seed _length_.+  + Add `detSecretKey'` allowing to choose what key type to use.+* [!1230](https://gitlab.com/morley-framework/morley/-/merge_requests/1230)+  Fix secp256k1 signatures+  + Roughly half of all secp256k1 created by Morley were rejected by network due+    to an implementation mismatch. This has been fixed.+* [!1260](https://gitlab.com/morley-framework/morley/-/merge_requests/1260)+  Refactor `SomeAddressOrAlias`+    + Changed the definition of `SomeAddressOrAlias` to be able to parse+      address/aliases of a contract, implicit account, or both.+      A prefix of `implicit:` or `contract:` can be used to disambiguate.+    + Changed the parser of `AddressOrAlias kind` to accept the `implicit:`+      and `contract:` prefixes.+    + Replaced the `morley transfer --to-implicit` and `--to-contract` options+      with a single `--to` option.+* [!1255](https://gitlab.com/morley-framework/morley/-/merge_requests/1255)+  Simplify some machinery using instances from `some`+* [!1138](https://gitlab.com/morley-framework/morley/-/merge_requests/1138)+  Generalize typechecking to work with arbitrary instruction wrapper instead of+  `ExpandedOp`.+  * Renames:+    + `TcInstrHandler` to `TcInstr`;+    + `typeCheckOpImpl` to `typeCheckExpandedOp`;+    + `TCError` to `TcError` and `TCTypeError` to `TcTypeError`;+    + `SomeInstr` to `SomeTcInstr`;+  * Some functions/types (`TCError`, `typeCheck*`) now have primed (`'`)+    versions that are generalized over `ExpandedOp`. Those functions now+    accept the typechecker for `ExpandedOp`.+* [!1240](https://gitlab.com/morley-framework/morley/-/merge_requests/1240)+  Add `MichelsonExt` to `MichelsonFailed` to allow extensible failure.+* [!1206](https://gitlab.com/morley-framework/morley/-/merge_requests/1206)+  Add `tupleFromRec`+* [!1243](https://gitlab.com/morley-framework/morley/-/merge_requests/1243)+  Add `run_code` emulation to Morley+  + `Morley.Michelson.Runtime` now provides `runCode` function, mimicing the+    functionality of RPC `run_code` endpoint+* [!1241](https://gitlab.com/morley-framework/morley/-/merge_requests/1241)+  Add classified typed instruction machinery+  + See `Morley.Michelson.Typed.ClassifiedInstr` haddocks for more information.+* [!1242](https://gitlab.com/morley-framework/morley/-/merge_requests/1242)+  Add `Constrained` utility existential+  + New utility module `Morley.Util.Constrained` introduced, defining an+    existential `Constrained`, similar to `Some` from `some`, but capturing+    additional constraints on the GADT argument+  + `ConstrainedAddress` reimplemented in terms of `Constrained`+  + `MkConstrainedAddress` kept as a pattern synonym, but deprecated+  + Types and pattern synonyms from `Morley.Michelson.Typed.Existential`+    reimplemented in terms of `Constrained`+* [!1245](https://gitlab.com/morley-framework/morley/-/merge_requests/1245)+  Remove Guard from Morley.Util.Type+  + See [#865](https://gitlab.com/morley-framework/morley/-/issues/865) for+    an alternative+* [!1237](https://gitlab.com/morley-framework/morley/-/merge_requests/1237)+  Track delegate registration in interpreter+* [!1178](https://gitlab.com/morley-framework/morley/-/merge_requests/1178)+  Add `HasNoNestedBigMaps t` constraint to `WellTyped` requirement for `Contract t`.+  + This is indirectly enforced by the network, but was missing. Useful to avoid+    redundant checks.+* [!1228](https://gitlab.com/morley-framework/morley/-/merge_requests/1228)+  Handle implicit default entrypoint in `mkEntrypointsMap`+  + Add a new enum type `HandleImplicitDefaultEp` to signal how to handle+    implicit default entrypoint.+  + Change `mkEntrypointsMap` to accept `HandleImplicitDefaultEp` as its first+    argument. The old behaviour corresponds to calling it with+    `WithoutImplicitDefaultEp`.+  + Change `flattenEntrypoints` to accept `HandleImplicitDefaultEp`, similar to+    `mkEntrypointsMap`.+* [!1195](https://gitlab.com/morley-framework/morley/-/merge_requests/1195)+  Improve `Forbid` constraints to carry type equality evidence+* [!1222](https://gitlab.com/morley-framework/morley/-/merge_requests/1222)+  Change the constraints on `instrCase` in+  `Morley.Michelson.Typed.Haskell.Instr.Sum` and on `instrConstruct`,+  `instrConstructStack`, and `instrDeconstruct` in+  `Morley.Michelson.Typed.Haskell.Instr.Product`. Code using these functions+  in surprisingly polymorphic ways may need minor adjustments. Applications of+  these functions should now be faster to typecheck and also faster to run.+* [!1216](https://gitlab.com/morley-framework/morley/-/merge_requests/1216)+  Add `LazyTake`, a "lazier" version of `Take`+  + Use `LazyTake` to improve type inference for various functions.+  + Rearrange `ConstraintDIG'` and `ConstraintDUG'` to reveal a bidirectional+    functional dependency.+  + Remove the `KnownList inp` constraint from `ConstraintDig'`.+* [!1215](https://gitlab.com/morley-framework/morley/-/merge_requests/1215)+  Output values associated with operations in `emulate transfer` etc+* [!1198](https://gitlab.com/morley-framework/morley/-/merge_requests/1198)+  Add equalities to `ConstraintDIPN'` to offer more fundeps.+ 1.18.0 ====== * [!1212](https://gitlab.com/morley-framework/morley/-/merge_requests/1212)

@@ -10,6 +10,14 @@  ## Morley executable +### Dependencies++To install using stack or cabal, you need to install [libsodium](https://doc.libsodium.org) first.++If installing into a non-standard location, after its installation is complete, add+the directory containing `libsodium.so` to your `LD_LIBRARY_PATH` environment+variable. Otherwise, compilation with stack or cabal will fail.+ ### How to install  There are three ways to get Morley executable:

@@ -30,7 +30,6 @@ import Morley.Michelson.Untyped qualified as U import Morley.Tezos.Address import Morley.Tezos.Address.Alias-import Morley.Tezos.Address.Kinds import Morley.Tezos.Core (Mutez, Timestamp(..), tz) import Morley.Tezos.Crypto import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes, createChestAndChestKey)@@ -127,7 +126,7 @@     typecheckSubCmd =       mkCommandParser "typecheck"         (TypeCheck <$> typeCheckOptions) $-        ("Typecheck passed contract")+        ("Typecheck passed contract.")      printSubCmd =       mkCommandParser "print"@@ -135,35 +134,35 @@              <*> (#output <:?> outputOption)              <*> (#singleLine <:!> onelineOption))       ("Parse a Morley contract and print corresponding Michelson " <>-       "contract that can be parsed by the OCaml reference client: tezos-client")+       "contract that can be parsed by the OCaml reference client: `octez-client`.")      emulateSubCmd =       mkCommandParser "emulate"       (subparser $ runSubCmd                 <> originateSubCmd                 <> transferSubCmd)-      ("Set of commands to run in an emulated environment")+      ("Set of commands to run in an emulated environment.")      runSubCmd =       mkCommandParser "run"       (Run <$> runOptions) $       "Run passed contract. \-      \It's originated first and then a transaction is sent to it"+      \It's originated first and then a transaction is sent to it."      replSubCmd =       mkCommandParser "repl"       (pure REPL)-      "Start a Morley REPL"+      "Start a Morley REPL."      originateSubCmd =       mkCommandParser "originate"       (Originate <$> originateOptions)-      "Originate passed contract. Add it to passed DB"+      "Originate passed contract. Add it to passed DB."      transferSubCmd =       mkCommandParser "transfer"       (Transfer <$> transferOptions)-      "Transfer tokens to given address"+      "Transfer tokens to given address."      optimizeSubCmd =       mkCommandParser "optimize"@@ -184,25 +183,25 @@     verboseFlag = switch $       short 'v' <>       long "verbose" <>-      help "Whether output should be verbose"+      help "Whether output should be verbose."      writeFlag :: Opt.Parser Bool     writeFlag = switch $       long "write" <>-      help "Whether updated DB should be written to DB file"+      help "Whether updated DB should be written to DB file."      dryRunFlag :: Opt.Parser Bool     dryRunFlag = switch $       long "dry-run" <>-      help "Do not write updated DB to DB file"+      help "Do not write updated DB to DB file."      typeCheckOptionsOption :: Opt.Parser TypeCheck.TypeCheckOptions     typeCheckOptionsOption = do       tcVerbose <- verboseFlag       tcStrict <- fmap not . switch $         long "typecheck-lax" <>-        help "Whether actions permitted in `tezos-client run` but forbidden in \-             \e.g. `tezos-client originate` should be allowed here"+        help "Whether actions permitted in `octez-client run` but forbidden in \+             \e.g. `octez-client originate` should be allowed here."       return TypeCheck.TypeCheckOptions{..}      typeCheckOptions :: Opt.Parser TypeCheckOptions@@ -232,7 +231,7 @@         <*> dbPathOption         <*> typeCheckOptionsOption         <*> valueOption Nothing (#name :! "storage")-            (#help :! "Initial storage of a running contract")+            (#help :! "Initial storage of a running contract.")         <*> txDataOption         <*> verboseFlag         <*> nowOption@@ -240,7 +239,7 @@         <*> minBlockTimeOption         <*> maxStepsOption         <*> mutezOption (Just defaultBalance)-            (#name :! "balance") (#help :! "Initial balance of this contract")+            (#name :! "balance") (#help :! "Initial balance of this contract.")         <*> writeFlag      originateOptions :: Opt.Parser OriginateOptions@@ -250,16 +249,16 @@         <*> dbPathOption         <*> typeCheckOptionsOption         <*> addressOption (Just genesisAddress)-            (#name :! "originator") (#help :! "Contract's originator")+            (#name :! "originator") (#help :! "Contract's originator.")         <*> optional (aliasOption "alias")         <*> optional             (keyHashOption Nothing-              (#name :! "delegate") (#help :! "Contract's optional delegate")+              (#name :! "delegate") (#help :! "Contract's optional delegate.")             )         <*> valueOption Nothing-            (#name :! "storage") (#help :! "Initial storage of an originating contract")+            (#name :! "storage") (#help :! "Initial storage of an originating contract.")         <*> mutezOption (Just defaultBalance)-            (#name :! "balance") (#help :! "Initial balance of an originating contract")+            (#name :! "balance") (#help :! "Initial balance of an originating contract.")         <*> verboseFlag      transferOptions :: Opt.Parser TransferOptions@@ -267,14 +266,10 @@       toDBPath <- dbPathOption       toTcOptions <- typeCheckOptionsOption       toDestination <--        SomeAddressOrAlias <$> addressOrAliasOption @'AddressKindImplicit-          Nothing-          (#name :! "to-implicit")-          (#help :! "Address or alias of the transfer's destination implicit address (tz1/tz2/tz3)")-        <|> SomeAddressOrAlias <$> addressOrAliasOption @'AddressKindContract+        someAddressOrAliasOption           Nothing-          (#name :! "to-contract")-          (#help :! "Address or alias of the transfer's destination contract (KT1)")+          (#name :! "to")+          (#help :! "Address or alias of the transfer's destination.")       toTxData <- txDataOption       toNow <- nowOption       toLevel <- levelOption@@ -359,7 +354,7 @@             michelsonContract             ! #verbose ooVerbose         putTextLn $ "Originated contract " <> pretty addr-      Transfer TransferOptions {toDestination=SomeAddressOrAlias toDestination, ..} -> do+      Transfer TransferOptions {..} -> do         transfer toNow toLevel toMinBlockTime toMaxSteps toDBPath toTcOptions toDestination toTxData           ! #verbose toVerbose           ! #dryRun toDryRun

@@ -39,7 +39,8 @@ import Morley.Michelson.Runtime.Dummy import Morley.Michelson.Runtime.Import (readValue) import Morley.Michelson.TypeCheck-  (SomeInstr(..), SomeInstrOut(..), TypeCheckOptions(..), runTypeCheckIsolated, typeCheckingWith)+  (SomeTcInstr(..), SomeTcInstrOut(..), TypeCheckOptions(..), runTypeCheckIsolated,+  typeCheckingWith) import Morley.Michelson.TypeCheck.Instr (typeCheckList, typeCheckParameter) import Morley.Michelson.TypeCheck.Types (HST(..)) import Morley.Michelson.Typed qualified as T

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           morley-version:        1.18.0+version:        1.19.0 synopsis:       Developer tools for the Michelson Language description:    A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective. category:       Language@@ -69,6 +69,7 @@       Morley.Michelson.Runtime.Dummy       Morley.Michelson.Runtime.GState       Morley.Michelson.Runtime.Import+      Morley.Michelson.Runtime.RunCode       Morley.Michelson.Runtime.TxData       Morley.Michelson.Text       Morley.Michelson.TypeCheck@@ -86,6 +87,16 @@       Morley.Michelson.Typed.AnnotatedValue       Morley.Michelson.Typed.Annotation       Morley.Michelson.Typed.Arith+      Morley.Michelson.Typed.ClassifiedInstr+      Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.HasAnns+      Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsAlwaysFailing+      Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsMichelson+      Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.NumChildren+      Morley.Michelson.Typed.ClassifiedInstr.Internal.InstrEnum+      Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl+      Morley.Michelson.Typed.ClassifiedInstr.Internal.TH+      Morley.Michelson.Typed.ClassifiedInstr.Internal.Types+      Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr       Morley.Michelson.Typed.Contract       Morley.Michelson.Typed.Convert       Morley.Michelson.Typed.Doc@@ -139,6 +150,7 @@       Morley.Util.Binary       Morley.Util.ByteString       Morley.Util.CLI+      Morley.Util.Constrained       Morley.Util.CustomGeneric       Morley.Util.Default       Morley.Util.Exception@@ -223,7 +235,7 @@       UndecidableInstances       UndecidableSuperClasses       ViewPatterns-  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages+  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode   build-depends:       Diff     , MonadRandom@@ -236,10 +248,12 @@     , binary     , bytestring     , constraints >=0.11+    , constraints-extras     , containers     , crypto-sodium >=0.0.5.0     , cryptonite     , data-default+    , dependent-sum-template     , elliptic-curve     , first-class-families >=0.5.0.0     , fmt >=0.6.3.0@@ -261,6 +275,7 @@     , show-type     , singletons     , singletons-base+    , some     , syb     , template-haskell     , text@@ -269,6 +284,7 @@     , th-reify-many     , time     , timerep+    , type-errors     , uncaught-exception     , unordered-containers     , vector@@ -337,7 +353,7 @@       UndecidableInstances       UndecidableSuperClasses       ViewPatterns-  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages+  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode   build-depends:       MonadRandom     , aeson@@ -350,7 +366,6 @@     , megaparsec >=7.0.0     , morley     , morley-prelude-    , named     , optparse-applicative     , singletons     , text

@@ -6,6 +6,8 @@ module Morley.AsRPC   ( TAsRPC   , HasRPCRepr(..)+  , deriveRPCWithOptions+  , DeriveRPCOptions(..)   , deriveRPC   , deriveRPCWithStrategy   , deriveManyRPC@@ -28,6 +30,7 @@  import Control.Lens.Plated (universe) import Data.Constraint (Dict(..), (***), (:-)(Sub), (\\))+import Data.Default (Default(..)) import Data.Generics (everything, mkQ) import Data.List qualified as List ((\\)) import Data.Map qualified as Map@@ -37,8 +40,9 @@ import Language.Haskell.TH   (Con(InfixC, NormalC, RecC), Cxt, Dec(DataD, NewtypeD, TySynD, TySynInstD),   DerivStrategy(AnyclassStrategy), Info(TyConI), Kind, Loc(loc_module), Name, Q, TyLit(StrTyLit),-  TySynEqn(..), TyVarBndr(..), Type(..), cxt, instanceD, location, mkName, nameBase, ppr, reify,-  reifyInstances, standaloneDerivWithStrategyD)+  TySynEqn(..), TyVarBndr(..), Type(..), conT, cxt, instanceD, location, lookupTypeName, mkName,+  nameBase, normalB, ppr, reify, reifyInstances, standaloneDerivWithStrategyD, valD, varE, varP)+import Language.Haskell.TH qualified as TH import Language.Haskell.TH.ReifyMany (reifyManyTyCons) import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames) @@ -54,6 +58,7 @@ import Morley.Util.CustomGeneric   (GenericStrategy, customGeneric', deriveFullType, haskellBalanced,   mangleGenericStrategyConstructors, mangleGenericStrategyFields, reifyDataType)+import Morley.Util.Interpolate (itu) import Morley.Util.Named hiding (Name) import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail) @@ -270,67 +275,134 @@ -- Derive RPC repr ---------------------------------------------------------------------------- --- | Derive an RPC representation for a type, as well as instances for 'Generic', 'IsoValue' and 'HasRPCRepr'.------ > data ExampleStorage a b = ExampleStorage--- >   { esField1 :: Integer--- >   , esField2 :: [BigMap Integer MText]--- >   , esField3 :: a--- >   }--- >   deriving stock Generic--- >   deriving anyclass IsoValue--- >--- > deriveRPC "ExampleStorage"------ Will generate:------ > data ExampleStorageRPC a b = ExampleStorageRPC--- >   { esField1RPC :: AsRPC Integer--- >   , esField2RPC :: AsRPC [BigMap Integer MText]--- >   , esField3RPC :: AsRPC a--- >   }--- >--- > instance HasRPCRepr a => HasRPCRepr (ExampleStorage a b) where--- >   type AsRPC (ExampleStorage a b) = ExampleStorageRPC a b--- > deriving anyclass instance (IsoValue (AsRPC a), IsoValue (AsRPC b)) => IsoValue (ExampleStorageRPC a b)--- > instance Generic (ExampleStorageRPC a b) where--- >   ...+-- | 'deriveRPCWithOptions' using default 'DeriveRPCOptions'. deriveRPC :: String -> Q [Dec]-deriveRPC typeStr = deriveRPCWithStrategy typeStr haskellBalanced+deriveRPC typeStr = deriveRPCWithOptions typeStr def --- | Recursively enumerate @data@, @newtype@ and @type@ declarations,--- and derives an RPC representation for each type that doesn't yet have one.------ You can also pass in a list of types for which you _don't_ want--- an RPC representation to be derived.------ In this example, 'deriveManyRPC' will generate an RPC--- representation for @A@ and @B@,--- but not for @C@ (because we explicitly said we don't want one)--- or @D@ (because it already has one).------ > data B = B--- > data C = C--- > data D = D--- > deriveRPC "D"--- >--- > data A = A B C D--- > deriveManyRPC "A" ["C"]+-- | Options for 'deriveRPCWithOptions'.+data DeriveRPCOptions = DeriveRPCOptions+  { droRecursive :: Bool+    -- ^ Recursively enumerate @data@, @newtype@ and @type@ declarations, and+    -- derives an RPC representation for each type that doesn't yet have one.+    -- @True@ by default.+  , droRecursiveSkipTypes :: [String]+    -- ^ List of types for which you _don't_ want an RPC representation to be+    -- derived. This is ignored if @droRecursive@ is @False@.+  , droHasAnnotation :: Bool+    -- ^ Derive @HasAnnotation@. The class and its methods must be in scope,+    -- otherwise a compilation error is raised. @True@ by default.+  , droStrategy :: GenericStrategy+    -- ^ Custom Generic deriving strategy. 'haskellBalanced' by default.+  }++instance Default DeriveRPCOptions where+  def = DeriveRPCOptions+    { droRecursive = True+    , droRecursiveSkipTypes = []+    , droHasAnnotation = True+    , droStrategy = haskellBalanced+    }++{- | Derive an RPC representation for a type, as well as instances for+'Generic', 'IsoValue', 'HasRPCRepr' and optionally @HasAnnotation@.++> data ExampleStorage a b = ExampleStorage+>   { esField1 :: Integer+>   , esField2 :: [BigMap Integer MText]+>   , esField3 :: a+>   }+>   deriving stock Generic+>   deriving anyclass IsoValue+>+> deriveRPC "ExampleStorage"++Will generate:++> data ExampleStorageRPC a b = ExampleStorageRPC+>   { esField1RPC :: AsRPC Integer+>   , esField2RPC :: AsRPC [BigMap Integer MText]+>   , esField3RPC :: AsRPC a+>   }+>+> instance HasRPCRepr a => HasRPCRepr (ExampleStorage a b) where+>   type AsRPC (ExampleStorage a b) = ExampleStorageRPC a b+> deriving anyclass instance (IsoValue (AsRPC a), IsoValue (AsRPC b)) => IsoValue (ExampleStorageRPC a b)+> instance Generic (ExampleStorageRPC a b) where+>   ...++When 'droHasAnnotation' is @True@, it will also generate a @HasAnnotation@ (from+@Lorentz@) instance like:++> instance With [HasAnnotation, HasRPCRepr] ExampleStorage+>   => HasAnnotation ExampleStorageRPC where+>   getAnnotation = notesAsRPC . getAnnotation @ExampleStorage+>   annOptions = annOptions @ExampleStorage++Note that if the type doesn't contain type variables or only contains phantom+type variables, 'HasRPCRepr' constraint is omitted, as it would be redundant.++@HasAnnotation@ and its methods must be in scope.++When 'droRecursive' is @True@, recursively enumerate @data@, @newtype@ and+@type@ declarations, and derive an RPC representation for each type that doesn't+yet have one.++You can also pass in a list of types for which you _don't_ want+an RPC representation to be derived in 'droRecursiveSkipTypes'.++In this example, this will generate an RPC representation for @A@ and @B@, but+not for @C@ (because we explicitly said we don't want one) or @D@ (because it+already has one).++> data B = B+> data C = C+> data D = D+> deriveRPC "D"+>+> data A = A B C D+> deriveRPCWithOptions "A" def{droRecursive=True, droRecursiveSkipTypes=["C"]}+-}+deriveRPCWithOptions :: String -> DeriveRPCOptions -> Q [Dec]+deriveRPCWithOptions typeStr opts@DeriveRPCOptions{droRecursive}+  | droRecursive = deriveManyRPCWithStrategy' typeStr opts+  | otherwise = do+      typeName <- lookupTypeNameOrFail typeStr+      whenM (isTypeAlias typeName) $ fail $ typeStr <> " is a 'type' alias but not 'data' or 'newtype'."+      deriveRPCWithStrategy' typeName opts++-- | Same as 'deriveRPCWithOptions' with 'droRecursive' set to @True@ and+-- 'droHasAnnotation' set to @False@. Accepts 'droRecursiveSkipTypes' as second+-- argument. deriveManyRPC :: String -> [String] -> Q [Dec]-deriveManyRPC typeStr skipTypes =-  deriveManyRPCWithStrategy typeStr skipTypes haskellBalanced+deriveManyRPC typeStr droRecursiveSkipTypes = deriveRPCWithOptions typeStr DeriveRPCOptions+  { droRecursive = True+  , droHasAnnotation = False+  , droStrategy = haskellBalanced+  , droRecursiveSkipTypes+  }+{-# DEPRECATED deriveManyRPC "Use deriveRPCWithOptions instead" #-}  -- | Same as 'deriveManyRPC', but uses a custom strategy for deriving a 'Generic' instance. deriveManyRPCWithStrategy :: String -> [String] -> GenericStrategy -> Q [Dec]-deriveManyRPCWithStrategy typeStr skipTypes gs = do-  skipTypeNames <- traverse lookupTypeNameOrFail skipTypes+deriveManyRPCWithStrategy typeStr skipTypes strategy = deriveRPCWithOptions typeStr DeriveRPCOptions+  { droRecursive = True+  , droHasAnnotation = False+  , droRecursiveSkipTypes=skipTypes+  , droStrategy = strategy+  }+{-# DEPRECATED deriveManyRPCWithStrategy "Use deriveRPCWithOptions instead" #-}++deriveManyRPCWithStrategy' :: String -> DeriveRPCOptions -> Q [Dec]+deriveManyRPCWithStrategy' typeStr opts@DeriveRPCOptions{droRecursiveSkipTypes} = do+  skipTypeNames <- traverse lookupTypeNameOrFail droRecursiveSkipTypes   typeName <- lookupTypeNameOrFail typeStr   whenM (isTypeAlias typeName) $ fail $ typeStr <> " is a 'type' alias but not 'data' or 'newtype'."   allTypeNames <- findWithoutInstance typeName-  join <$> forM (allTypeNames List.\\ skipTypeNames) \name -> deriveRPCWithStrategy' name gs+  join <$> forM (allTypeNames List.\\ skipTypeNames) \name ->+    deriveRPCWithStrategy' name opts   where -    -- | Recursively enumerate @data@, @newtype@ and @type@ declarations,+    -- Recursively enumerate @data@, @newtype@ and @type@ declarations,     -- and returns the names of only @data@ and @newtype@ of those that     -- don't yet have an 'AsRPC' instance. Type aliases don't need instances     -- and respectively there is no need to derive 'AsRPC' for them.@@ -356,7 +428,7 @@         Just typ ->           not . null <$> reifyInstances ''AsRPC [typ] -    -- | Given a type name, return the corresponding type expression+    -- Given a type name, return the corresponding type expression     -- (applied to any type variables, if necessary).     --     -- For example, assuming a data type like @data F a b = ...@ exists in the type environment,@@ -374,13 +446,16 @@  -- | Same as 'deriveRPC', but uses a custom strategy for deriving a 'Generic' instance. deriveRPCWithStrategy :: String -> GenericStrategy -> Q [Dec]-deriveRPCWithStrategy typeStr gs = do-  typeName <- lookupTypeNameOrFail typeStr-  whenM (isTypeAlias typeName) $ fail $ typeStr <> " is a 'type' alias but not 'data' or 'newtype'."-  deriveRPCWithStrategy' typeName gs+deriveRPCWithStrategy name gs = deriveRPCWithOptions name DeriveRPCOptions+  { droHasAnnotation = False+  , droRecursive = False+  , droRecursiveSkipTypes = []+  , droStrategy = gs+  }+{-# DEPRECATED deriveRPCWithStrategy "Use deriveRPCWithOptions instead" #-} -deriveRPCWithStrategy' :: Name -> GenericStrategy -> Q [Dec]-deriveRPCWithStrategy' typeName gs = do+deriveRPCWithStrategy' :: Name -> DeriveRPCOptions -> Q [Dec]+deriveRPCWithStrategy' typeName DeriveRPCOptions{..} = do   (_, decCxt, mKind, tyVars, constructors) <- reifyDataType typeName    -- TODO [#722]: use `reifyInstances` to check that 'AsRPC' exists for `fieldType`@@ -412,17 +487,18 @@   -- RPC type after stripping RPC suffix. Fix for #811   let     gs' = mangleGenericStrategyFields dropRPCSuffix $-            mangleGenericStrategyConstructors dropRPCSuffix gs+            mangleGenericStrategyConstructors dropRPCSuffix droStrategy    mconcat <$> sequence     [ pure . one $ typeDecOfRPC     , one <$> mkAsRPCInstance fieldTypes derivedType derivedTypeRPC     , mkIsoValueInstance fieldTypesRPC derivedTypeRPC     , customGeneric' (Just repTypeRPC) typeNameRPC derivedTypeRPC constructorsRPC gs'+    , annotationInstance fieldTypes derivedType derivedTypeRPC     ]    where-    -- | Given the field type @FieldType a b@, returns @AsRPC (FieldType a b)@.+    -- Given the field type @FieldType a b@, returns @AsRPC (FieldType a b)@.     convertFieldType :: Type -> Type     convertFieldType tp = ConT ''AsRPC `AppT` tp @@ -435,7 +511,7 @@     convertName :: Name -> Name     convertName = mkName . convertNameStr . nameBase -    -- | Given the constructor+    -- Given the constructor     -- @C { f :: Int }@,     -- returns the constructor     -- @CRPC { fRPC :: AsRPC Int }@.@@ -453,7 +529,7 @@         InfixC (second convertFieldType fieldType1) (convertName conName) (second convertFieldType fieldType2)       constr -> fail $ "Unsupported constructor for '" <> show typeName <> "': " <> show (ppr constr) -    -- | Get a list of all the unique types of all the fields of all the given constructors.+    -- Get a list of all the unique types of all the fields of all the given constructors.     getFieldTypes :: [Con] -> Q [Type]     getFieldTypes constrs = ordNub . join <$> forM constrs \case       RecC _ fields -> pure $ fields <&> \(_, _, fieldType) -> fieldType@@ -472,7 +548,7 @@         _ -> fail $ "Only newtypes and data types are supported, but '" <>           show tyName <> "' is:\n" <> show (ppr typeInfo) -    -- | Traverse a 'Rep' type and:+    -- Traverse a 'Rep' type and:     --     -- 1. Inspect its metadata and append @RPC@ to the type/constructor/field names.     -- 2. Convert field types (e.g. @T@ becomes @AsRPC T@).@@ -511,7 +587,7 @@           VarT v -> VarT $ fromMaybe v $ Map.lookup v varMap           x -> x -    -- | Lookup the generic 'Rep' type instance for the given type.+    -- Lookup the generic 'Rep' type instance for the given type.     reifyRepInstance :: Name -> Type -> Q TySynEqn     reifyRepInstance name tp =       reifyInstances ''G.Rep [tp] >>= \case@@ -519,7 +595,7 @@         (_:_) -> fail $ "Found multiple instances of 'Generic' for '" <> show name <> "'."         [] -> fail $ "Type '" <> show name <> "' must implement 'Generic'." -    -- | Given the type @Foo a b = Foo (Bar a)@, generate an 'IsoValue' instance like:+    -- Given the type @Foo a b = Foo (Bar a)@, generate an 'IsoValue' instance like:     --     -- > deriving anyclass instance IsoValue (AsRPC (Bar a)) => IsoValue (FooRPC a b)     --@@ -534,7 +610,7 @@           cxt $ filter hasTyVar fieldTypes <&> \fieldType ->             [t|IsoValue $(pure fieldType)|] -    -- | Given the type @Foo a b = Foo (Bar a)@, generate an 'HasRPCRepr' instance like:+    -- Given the type @Foo a b = Foo (Bar a)@, generate an 'HasRPCRepr' instance like:     --     -- > instance HasRPCRepr (Bar a) => HasRPCRepr (Foo a b) where     -- >   type AsRPC (Foo a b) = FooRPC a b@@ -552,7 +628,54 @@           cxt $ filter hasTyVar fieldTypes <&> \fieldType ->             [t|HasRPCRepr $(pure fieldType)|] -    -- | Checks if the given type has any type variables.+    -- When @HasAnnotation@ and its methods are in scope, given the type @ty@+    -- where @AsRPC ty = tyRPC@, generate a @HasAnnotation@ instance like:+    --+    -- > instance With [HasAnnotation, HasRPCRepr] ty => HasAnnotation tyRPC where+    -- >   getAnnotation = notesAsRPC . getAnnotation @ty+    -- >   annOptions = annOptions @ty+    --+    -- Note that if @ty@ doesn't contain type variables or only contains phantom+    -- type variables, 'HasRPCRepr' constraint is omitted, as it would be+    -- redundant.+    --+    -- Will fail if @HasAnnotation@ or its methods are not in scope.+    annotationInstance :: [Type] -> Type -> Type -> Q [Dec]+    annotationInstance _ _ _ | not droHasAnnotation = pure []+    annotationInstance fields (pure -> ty) (pure -> tyRPC) = pure <$> do+      let noHasAnnError :: Text -> Q b+          noHasAnnError reason =+            -- NB: weird indentation is due to how GHC formats multiline TH+            -- errors (it doesn't)+            fail [itu|+              #{reason}+                  Did you mean to derive 'HasAnnotation' instances? If not, use:+                      deriveRPCWithOptions "#{tyBase}" def{droHasAnnotation=False}+              |]+            where tyBase = nameBase typeName+      hasAnnNm <- maybe (noHasAnnError "'HasAnnotation' is not in scope.") pure =<<+        lookupTypeName "HasAnnotation"+      methodNames <- reify hasAnnNm >>= \case+        TH.ClassI (TH.ClassD _ _ _ _ decs) _ ->+          pure $ flip mapMaybe decs \case+            TH.SigD name _ -> Just name+            _ -> Nothing+        x -> noHasAnnError $+          "Expected 'HasAnnotation' to be a class, but instead found " <> show (ppr x)+      getAnnNm <- find (\nm -> nameBase nm == "getAnnotation") methodNames &+        maybe (noHasAnnError "Did not find 'getAnnotation' method on 'HasAnnotation'") pure+      annOptNm <- find (\nm -> nameBase nm == "annOptions") methodNames &+        maybe (noHasAnnError "Did not find 'annOptions' method on 'HasAnnotation'") pure+      let hasAnn = conT hasAnnNm+          constraints+            | any hasTyVar fields = [[t| With '[$hasAnn, HasRPCRepr] $ty |]]+            | otherwise = [[t| $hasAnn $ty |]]+      instanceD (sequence constraints) [t|$hasAnn $tyRPC|]+          [ valD (varP getAnnNm) (normalB [|notesAsRPC . $(varE getAnnNm) @($ty)|]) []+          , valD (varP annOptNm) (normalB [|$(varE annOptNm) @($ty)|]) []+          ]++    -- Checks if the given type has any type variables.     hasTyVar :: Type -> Bool     hasTyVar ty =       flip any (universe ty) \case

@@ -23,6 +23,7 @@   , addressOption   , aliasOption   , addressOrAliasOption+  , someAddressOrAliasOption   , onelineOption   , entrypointOption   , mTextOption@@ -31,10 +32,12 @@   ) where  import Data.Singletons (SingI)+import Fmt (pretty) import Options.Applicative   (footerDoc, fullDesc, header, help, helper, info, long, metavar, option, progDesc, strOption,   switch) import Options.Applicative qualified as Opt+import Options.Applicative.Help qualified as Pretty import Options.Applicative.Help.Pretty (Doc) import Text.Read (read) @@ -50,6 +53,7 @@ import Morley.Tezos.Core (Mutez, Timestamp, parseTimestamp, timestampFromSeconds) import Morley.Tezos.Crypto import Morley.Util.CLI+import Morley.Util.Interpolate (itu) import Morley.Util.Named  ----------------------------------------------------------------------------@@ -157,6 +161,28 @@   -> Opt.Parser (AddressOrAlias kind) addressOrAliasOption = mkCLOptionParser +-- | Generic parser to read an option of 'SomeAddressOrAlias' type.+someAddressOrAliasOption+  :: Maybe SomeAddressOrAlias+  -> "name" :! String+  -> "help" :! String+  -> Opt.Parser SomeAddressOrAlias+someAddressOrAliasOption defValue (arg #name -> name) (arg #help -> hInfo) =+  Opt.option (getReader @SomeAddressOrAlias) $ mconcat+    [ Opt.metavar (getMetavar @SomeAddressOrAlias)+    , Opt.long name+    -- Note: `Opt.help` ignores newlines, so we use `Opt.helpDoc` + `vsep` instead.+    -- We use `paragraph` to word-wrap the help text.+    , Opt.helpDoc $ Just $ Pretty.vsep $ (Pretty.extractChunk . Pretty.paragraph) <$>+      [ hInfo+      , [itu|+        When using an alias that is assigned to both a contract and an implicit account,+        use the prefix '#{contractPrefix}:' or '#{implicitPrefix}:' to disambiguate.+        |]+      ]+    , maybeAddDefault pretty defValue+    ]+ -- | Parser for transaction parameters. txDataOption :: Opt.Parser TxData txDataOption =@@ -172,7 +198,7 @@     mkTxData :: ImplicitAddress -> U.Value -> Mutez -> EpName -> TxData     mkTxData addr param amount epName =       TxData-        { tdSenderAddress = MkConstrainedAddress addr+        { tdSenderAddress = Constrained addr         , tdParameter = TxUntypedParam param         , tdEntrypoint = epName         , tdAmount = amount

@@ -22,8 +22,8 @@ import Morley.Michelson.TypeCheck (TypeCheckOptions(..), typeCheckingWith) import Morley.Michelson.TypeCheck.Instr (typeCheckValue) import Morley.Michelson.Typed-  (Contract, HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType, rfAnyInstr,-  toUType)+  (Contract, HasNoOp, Instr, LambdaCode'(..), Notes(..), T(..), Value, Value'(..), fromUType,+  mkUType, rfAnyInstr, toUType) import Morley.Michelson.Typed.Convert (convertContract, instrToOpsOptimized, untypeValueOptimized) import Morley.Michelson.Untyped qualified as Untyped import Morley.Michelson.Untyped.Annotation@@ -63,6 +63,7 @@     Untyped.ValueSeq vs -> toExpression vs     Untyped.ValueMap elts -> toExpression $ eltToExpr <$> elts     Untyped.ValueLambda ops -> toExpression ops+    Untyped.ValueLamRec ops -> expressionPrim' "Lambda_rec" [toExpression ops] []     where       eltToExpr :: Untyped.Elt ExpandedOp -> Expression       eltToExpr (Untyped.Elt l r) = expressionPrim' "Elt"@@ -90,8 +91,7 @@     Untyped.TOperation -> expressionPrim' "operation" [] []     Untyped.TContract arg -> expressionPrim' "contract" [toExpression arg] []     Untyped.TTicket arg -> expressionPrim' "ticket" [toExpression arg] []-    t@Untyped.TPair{} -> expressionPrim' "pair"-      (rightCombedPairToList (Ty t noAnn) (noAnn, noAnn)) []+    t@Untyped.TPair{} -> expressionPrim' "pair" (rightCombedPairToList t) []     Untyped.TOr fa1 fa2 l r ->       let exprL = addTrimmedAnns (toExpression l) [] [fa1] []           exprR = addTrimmedAnns (toExpression r) [] [fa2] []@@ -126,15 +126,15 @@       addAnns e anns =         e & _ExpressionPrim . mpaAnnotsL <>~ anns -      rightCombedPairToList :: Ty -> (FieldAnn, VarAnn) -> [Expression]-      rightCombedPairToList ty (fa, va) = case (ty, fa) of-        (Ty (Untyped.TPair fa1 fa2 va1 va2 l r) (Untyped.Annotation ""), Untyped.Annotation "") ->-          let annsL = mkAnns [] [fa1] [va1]-              exprL = toExpression l `addAnns` annsL-          in exprL : (rightCombedPairToList r (fa2, va2))-        _ ->-          let anns = mkAnns [] [fa] [va]-          in one $ toExpression ty `addAnns` anns+      rightCombedPairToList :: Untyped.T -> [Expression]+      rightCombedPairToList t =+        let go ty (fa, va)+              | Ty (Untyped.TPair faL faR vaL vaR l r) ta <- ty+              , ta == noAnn, fa == noAnn, va == noAnn+              = toExpression l `addAnns` mkAnns [] [faL] [vaL] : go r (faR, vaR)+              | otherwise+              = one $ toExpression ty `addAnns` mkAnns [] [fa] [va]+        in go (Ty t noAnn) (noAnn, noAnn)  instance ToExpression Ty where   toExpression (Ty t ta) = addTrimmedAnns (toExpression t) [ta] [] []@@ -157,6 +157,8 @@ instance ToExpression ViewName where   toExpression (ViewName s) = expressionString s +-- Note: On adding new expressions here, you must also add the symmetric (reading) case+-- to FromExp x (InstrAbstract op) as well. instance ToExpression ExpandedInstr where   toExpression = \case     PUSH va ty v -> expressionPrim' "PUSH" [toExpression ty, toExpression v] $@@ -218,6 +220,11 @@                             , toExpression tyout                             , toExpression ops                             ] $ mkAnns [] [] [va]+    LAMBDA_REC va tyin tyout ops ->+      expressionPrim' "LAMBDA_REC" [ toExpression tyin+                            , toExpression tyout+                            , toExpression ops+                            ] $ mkAnns [] [] [va]     EXEC va -> expressionPrim' "EXEC" [] $ mkAnns [] [] [va]     APPLY va -> expressionPrim' "APPLY" [] $ mkAnns [] [] [va]     DIP ops -> expressionPrim' "DIP" [toExpression ops] []@@ -285,6 +292,7 @@     LEVEL va -> expressionPrim' "LEVEL" [] $ mkAnns [] [] [va]     SELF_ADDRESS va -> expressionPrim' "SELF_ADDRESS" [] $ mkAnns [] [] [va]     TICKET va -> expressionPrim' "TICKET" [] $ mkAnns [] [] [va]+    TICKET_DEPRECATED va -> expressionPrim' "TICKET_DEPRECATED" [] $ mkAnns [] [] [va]     READ_TICKET va -> expressionPrim' "READ_TICKET" [] $ mkAnns [] [] [va]     SPLIT_TICKET va -> expressionPrim' "SPLIT_TICKET" [] $ mkAnns [] [] [va]     JOIN_TICKETS va -> expressionPrim' "JOIN_TICKETS" [] $ mkAnns [] [] [va]@@ -393,6 +401,8 @@       arg' <- fromExp arg       pure $ Untyped.ValueSome arg'     ExpPrim' _ "None" [] [] -> pure Untyped.ValueNone+    ExpPrim' _ "Lambda_rec" [args] [] -> fmap Untyped.ValueLamRec $+      fromExp args >>= maybeToRight (FromExpError e "Expected at least one instruction") . nonEmpty     ExpSeq _ [] -> pure Untyped.ValueNil     ExpSeq _ (h : t) ->       case fromExp @x @op h of@@ -433,6 +443,8 @@     ExpSeq _ s -> SeqEx <$> traverse fromExp s     e          -> PrimEx <$> fromExp e +-- Note: On adding new expressions here, you must also add the symmetric (writing) case+-- to ToExpression as well. instance FromExp x op =>          FromExp x (InstrAbstract op) where   fromExp e = let annSet = getAnnSet e in case e of@@ -599,6 +611,13 @@       ops' <- fromExp @x @[op] ops       let va = firstAnn @VarTag annSet       pure $ LAMBDA va inp' out' ops'+    ExpPrim' _ "LAMBDA_REC" [inp, out, ops] _ -> do+      checkAnnsCount e annSet (0, 0, 1)+      inp' <- fromExp @x @Ty inp+      out' <- fromExp @x @Ty out+      ops' <- fromExp @x @[op] ops+      let va = firstAnn @VarTag annSet+      pure $ LAMBDA_REC va inp' out' ops'     ExpPrim' _ "EXEC" [] anns -> mkInstrWithVarAnn EXEC anns     ExpPrim' _ "APPLY" [] anns -> mkInstrWithVarAnn APPLY anns     ExpPrim' _ "DIP" [ops] [] -> do@@ -698,7 +717,10 @@     ExpPrim' _ "SELF_ADDRESS" [] anns ->       mkInstrWithVarAnn SELF_ADDRESS anns     ExpPrim' _ "NEVER" [] [] -> pure NEVER-    ExpPrim' _ "TICKET" [] anns -> mkInstrWithVarAnn TICKET anns+    ExpPrim' _ "TICKET_DEPRECATED" [] anns ->+      mkInstrWithVarAnn TICKET_DEPRECATED anns+    ExpPrim' _ "TICKET" [] anns ->+      mkInstrWithVarAnn TICKET anns     ExpPrim' _ "READ_TICKET" [] anns ->       mkInstrWithVarAnn READ_TICKET anns     ExpPrim' _ "SPLIT_TICKET" [] anns ->@@ -952,8 +974,10 @@ -- not just lambdas (i.e. instructions with one input and one output). instance (SingI inp, SingI out) => FromExp RegularExp (Instr '[inp] '[out]) where   fromExp expr =-    fromExpression @(Value ('TLambda inp out)) expr <&> \case-      VLam instr -> rfAnyInstr instr+    fromExpression @(Value ('TLambda inp out)) expr >>= \case+      VLam (LambdaCode instr) -> pure $ rfAnyInstr instr+      VLam LambdaCodeRec{} -> Left $ FromExpError expr+        "Expected block of code, found Lambda_rec"  instance FromExp x ViewName where   fromExp e = case e of

@@ -101,9 +101,9 @@   --   * "parameter" is at index 0 on the list, so it gets packed to `0x0300`   --   * "storage" is at index 1, so it gets packed to `0x0301`   ---  -- You can ask `tezos-client` which code corresponds to a given instruction/type/constructor.+  -- You can ask `octez-client` which code corresponds to a given instruction/type/constructor.   ---  -- > tezos-client convert data 'storage' from michelson to binary+  -- > octez-client convert data 'storage' from michelson to binary   -- > 0x0301   --   -- Whenever new instructions/types/constructors are added to the protocol,@@ -131,8 +131,8 @@   "DIG", "DUG", "EMPTY_BIG_MAP", "APPLY", "chain_id", "CHAIN_ID", "LEVEL", "SELF_ADDRESS",   "never", "NEVER", "UNPAIR", "VOTING_POWER", "TOTAL_VOTING_POWER", "KECCAK", "SHA3", "PAIRING_CHECK",   "bls12_381_g1", "bls12_381_g2", "bls12_381_fr", "sapling_state", "sapling_transaction_deprecated", "SAPLING_EMPTY_STATE", "SAPLING_VERIFY_UPDATE", "ticket",-  "TICKET", "READ_TICKET", "SPLIT_TICKET", "JOIN_TICKETS", "GET_AND_UPDATE", "chest", "chest_key", "OPEN_CHEST",-  "VIEW", "view", "constant", "SUB_MUTEZ", "tx_rollup_l2_address", "MIN_BLOCK_TIME", "sapling_transaction", "EMIT"+  "TICKET_DEPRECATED", "READ_TICKET", "SPLIT_TICKET", "JOIN_TICKETS", "GET_AND_UPDATE", "chest", "chest_key", "OPEN_CHEST",+  "VIEW", "view", "constant", "SUB_MUTEZ", "tx_rollup_l2_address", "MIN_BLOCK_TIME", "sapling_transaction", "EMIT", "Lambda_rec", "LAMBDA_REC", "TICKET"   ]  -- | Type for Micheline Expression with extension points.

@@ -775,16 +775,16 @@     \Michelson representation to make interactions outside of Haskell possible.\n\n\     \There are multiple ways to interact with this contract:\n\n\     \* Use this contract in your Haskell application, thus all operation submissions \-    \should be handled separately, e.g. via calling `tezos-client`, which will communicate \-    \with the `tezos-node`. In order to be able to call `tezos-client` you'll need to be able \+    \should be handled separately, e.g. via calling `octez-client`, which will communicate \+    \with the `octez-node`. In order to be able to call `octez-client` you'll need to be able \     \to construct Michelson values from Haskell.\n\n\     \  The easiest way to do that is to serialize Haskell value using `lPackValue` function \     \from [`Lorentz.Pack`](https://gitlab.com/morley-framework/morley/-/blob/2441e26bebd22ac4b30948e8facbb698d3b25c6d/code/lorentz/src/Lorentz/Pack.hs) \     \module, encode resulting bytestring to hexadecimal representation using `encodeHex` function. \     \Resulting hexadecimal encoded bytes sequence can be decoded back to Michelson value via \-    \`tezos-client unpack michelson data`.\n\n\+    \`octez-client unpack michelson data`.\n\n\     \  Reverse conversion from Michelson value to the \-    \Haskell value can be done by serializing Michelson value using `tezos-client hash data` command, \+    \Haskell value can be done by serializing Michelson value using `octez-client hash data` command, \     \resulting `Raw packed data` should be decoded from the hexadecimal representation using `decodeHex` \     \and deserialized to the Haskell value via `lUnpackValue` function from \     \[`Lorentz.Pack`](https://gitlab.com/morley-framework/morley/-/blob/2441e26bebd22ac4b30948e8facbb698d3b25c6d/code/lorentz/src/Lorentz/Pack.hs).\n\n\

@@ -7,7 +7,7 @@   ( ContractEnv (..)   , InterpreterState (..)   , MichelsonFailed (..)-  , MichelsonFailureWithStack (..)+  , MichelsonFailureWithStack(..)   , RemainingSteps (..)   , SomeItStack (..)   , MorleyLogs (..)@@ -76,7 +76,6 @@ import Morley.Util.Peano (LongerThan, Peano) import Morley.Util.PeanoNatural (PeanoNatural(..)) import Morley.Util.Sing (eqParamSing)-import Morley.Util.TH import Morley.Util.Type import Morley.Util.Typeable @@ -166,20 +165,23 @@   -- ^ Minimum time between blocks   } --- | Represents @[FAILED]@ state of a Michelson program. Contains--- value that was on top of the stack when @FAILWITH@ was called.-data MichelsonFailed where-  MichelsonFailedWith :: (SingI t, ConstantScope t) => T.Value t -> MichelsonFailed+-- | Errors that can be thrown by the interpreter. The @ext@ type variable+-- allow the downstreams consumer to add additional exceptions.+data MichelsonFailed ext where+  MichelsonFailedWith :: (SingI t, ConstantScope t) => T.Value t -> MichelsonFailed ext+    -- ^ Represents @[FAILED]@ state of a Michelson program. Contains+    -- value that was on top of the stack when @FAILWITH@ was called.   MichelsonArithError     :: (Typeable n, Typeable m)-    => ArithError (Value n) (Value m) -> MichelsonFailed-  MichelsonGasExhaustion :: MichelsonFailed-  MichelsonFailedTestAssert :: Text -> MichelsonFailed-  MichelsonUnsupported :: Text -> MichelsonFailed+    => ArithError (Value n) (Value m) -> MichelsonFailed ext+  MichelsonGasExhaustion :: MichelsonFailed ext+  MichelsonFailedTestAssert :: Text -> MichelsonFailed ext+  MichelsonUnsupported :: Text -> MichelsonFailed ext+  MichelsonExt :: ext -> MichelsonFailed ext -deriving stock instance Show MichelsonFailed+deriving stock instance Show ext => Show (MichelsonFailed ext) -instance Eq MichelsonFailed where+instance Eq ext => Eq (MichelsonFailed ext) where   MichelsonFailedWith v1 == MichelsonFailedWith v2 = v1 `eqParamSing` v2   MichelsonFailedWith _ == _ = False   MichelsonArithError ae1 == MichelsonArithError ae2 = ae1 `eqParam2` ae2@@ -190,8 +192,10 @@   MichelsonFailedTestAssert _ == _ = False   MichelsonUnsupported i1 == MichelsonUnsupported i2 = i1 == i2   MichelsonUnsupported _ == _ = False+  MichelsonExt i1 == MichelsonExt i2 = i1 == i2+  MichelsonExt _ == _ = False -instance Buildable MichelsonFailed where+instance Buildable ext => Buildable (MichelsonFailed ext) where   build =     \case       MichelsonFailedWith v ->@@ -202,22 +206,23 @@       MichelsonFailedTestAssert t -> build t       MichelsonUnsupported instr ->         build instr <> " instruction is not supported."+      MichelsonExt x -> build x --- | Carries a 'MichelsonFailed' error and the 'ErrorSrcPos' at which it was raised-data MichelsonFailureWithStack = MichelsonFailureWithStack-  { mfwsFailed :: MichelsonFailed+-- | Carries a 'MichelsonFailed' @ext@ error and the 'ErrorSrcPos' at which it was raised+data MichelsonFailureWithStack ext = MichelsonFailureWithStack+  { mfwsFailed :: MichelsonFailed ext   , mfwsErrorSrcPos :: ErrorSrcPos   } deriving stock (Show, Generic, Eq) -instance Buildable MichelsonFailureWithStack where+instance Buildable ext => Buildable (MichelsonFailureWithStack ext) where   build (MichelsonFailureWithStack err loc) = build err <> " at " <> build loc -newtype InterpretError = InterpretError (MichelsonFailureWithStack, MorleyLogs)+newtype InterpretError ext = InterpretError (MichelsonFailureWithStack ext, MorleyLogs)   deriving stock (Generic) -deriving stock instance Show InterpretError+deriving stock instance Show ext => Show (InterpretError ext) -instance Buildable InterpretError where+instance Buildable ext => Buildable (InterpretError ext) where   build (InterpretError (mf, _)) = prettyLn mf  data InterpretResult where@@ -245,11 +250,11 @@   }  type ContractReturn st =-  (Either MichelsonFailureWithStack ([Operation], T.Value st), (InterpreterState, MorleyLogs))+  (Either (MichelsonFailureWithStack Void) ([Operation], T.Value st), (InterpreterState, MorleyLogs))  handleContractReturn   :: (StorageScope st)-  => ContractReturn st -> Either InterpretError InterpretResult+  => ContractReturn st -> Either (InterpretError Void) InterpretResult handleContractReturn (ei, (s, l)) =   bimap (InterpretError . (, l)) (constructIR . (, s, l)) ei @@ -314,7 +319,7 @@   :: ContractEnv   -> Instr inp out   -> Rec T.Value inp-  -> Either MichelsonFailureWithStack (Rec T.Value out)+  -> Either (MichelsonFailureWithStack Void) (Rec T.Value out) interpretInstr = fmap mapToValue ... interpretInstrAnnotated  -- | Interpret an instruction in vacuum, putting no extra constraints on@@ -325,7 +330,7 @@   :: ContractEnv   -> Instr inp out   -> Rec T.Value inp-  -> Either MichelsonFailureWithStack (Rec StkEl out)+  -> Either (MichelsonFailureWithStack Void) (Rec StkEl out) interpretInstrAnnotated env instr inpSt =   fst $   runEvalOp@@ -341,14 +346,14 @@   SomeItStack :: T.ExtInstr inp -> Rec StkEl inp -> SomeItStack  type EvalOp =-  ExceptT MichelsonFailureWithStack $+  ExceptT (MichelsonFailureWithStack Void) $   RWS ContractEnv MorleyLogsBuilder InterpreterState  runEvalOp   :: EvalOp a   -> ContractEnv   -> InterpreterState-  -> (Either MichelsonFailureWithStack a, (InterpreterState, MorleyLogs))+  -> (Either (MichelsonFailureWithStack Void) a, (InterpreterState, MorleyLogs)) runEvalOp act env initSt =   let (res, is, logs) = runRWS (runExceptT act) env initSt   in (res, (is, buildMorleyLogs logs))@@ -386,20 +391,22 @@ instance InterpreterStateMonad m => InterpreterStateMonad (ExceptT e m) where   stateInterpreterState = lift . stateInterpreterState -type EvalM m =+type EvalM' ext m =   ( MonadReader ContractEnv m   , InterpreterStateMonad m   , MonadWriter MorleyLogsBuilder m-  , MonadError MichelsonFailureWithStack m+  , MonadError (MichelsonFailureWithStack ext) m   ) +type EvalM m = EvalM' Void m+ type InstrRunner m =   forall inp out.      Instr inp out   -> Rec StkEl inp   -> m (Rec StkEl out) -throwMichelson :: EvalM m => MichelsonFailed -> m a+throwMichelson :: EvalM' ext m => MichelsonFailed ext -> m a throwMichelson mf = asks ceErrorSrcPos >>= throwError . MichelsonFailureWithStack mf  -- | Function to change amount of remaining steps stored in State monad.@@ -422,7 +429,10 @@ runInstrNoGas = runInstrImpl runInstrNoGas  -- | Function to interpret Michelson instruction(s) against given stack.-runInstrImpl :: forall m. EvalM m => InstrRunner m -> InstrRunner m+-- The @ext@ type variable specifies additional exceptions that can be thrown from the inner+-- runner function (via 'MichelsonExt'). In Morley, it's set to 'Void', but downstream consumers+-- may use other type here.+runInstrImpl :: forall ext m. EvalM' ext m => InstrRunner m -> InstrRunner m runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r' runInstrImpl runner (WithLoc ics i) r = local (\env -> env{ceErrorSrcPos = ics}) $ runner i r runInstrImpl runner (Meta _ i) r = runner i r@@ -470,9 +480,8 @@        => PeanoNatural n -> Rec StkEl inp -> Rec StkEl out     go Zero stack = stack     go (Succ n') (b :& r) =-      case klist @inp of-        KCons _ Proxy -> case go n' r of-          (a :& resTail) -> a :& b :& resTail+      case go n' r of+        a :& resTail -> a :& b :& resTail runInstrImpl _ (DUG s) input0 =   pure $ go s input0   where@@ -599,12 +608,24 @@ runInstrImpl runner (LOOP_LEFT ops) (StkEl (VOr (Left a)) :& r) = do   res <- runner ops (StkEl a :& r)   runner (LOOP_LEFT ops) res-runInstrImpl _ (AnnLAMBDA _ lam) r = pure $ StkEl lam :& r-runInstrImpl runner AnnEXEC{} (a :& StkEl (VLam (T.rfAnyInstr -> lBody)) :& r) = do-  res <- runner lBody (a :& RNil)-  pure $ res <+> r-runInstrImpl _ AnnAPPLY{} (StkEl (a :: T.Value a) :& StkEl (VLam lBody) :& r) = do-  pure $ StkEl (VLam (T.rfMapAnyInstr doApply lBody)) :& r+runInstrImpl _ (AnnLAMBDA _ lam) r = pure $ StkEl (mkVLam lam) :& r+runInstrImpl _ (AnnLAMBDA_REC _ lam) r = pure $ StkEl (mkVLamRec lam) :& r+runInstrImpl runner AnnEXEC{} (a :& self@(StkEl (VLam code)) :& r) =+  case code of+    LambdaCode (T.rfAnyInstr -> lBody) -> do+      res <- runner lBody (a :& RNil)+      pure $ res <+> r+    LambdaCodeRec (T.rfAnyInstr -> lBody) -> do+      res <- runner lBody (a :& self :& RNil)+      pure $ res <+> r+runInstrImpl _ i@AnnAPPLY{} (StkEl (a :: T.Value a) :& StkEl (VLam code) :& r)+  | _ :: Instr (a : 'TLambda ('TPair a b) c : s) ('TLambda b c : s) <- i+  , _ :: LambdaCode' Instr ('TPair a b) c <- code+  = case code of+      LambdaCode lBody -> pure $ StkEl (VLam $ LambdaCode (T.rfMapAnyInstr doApply lBody)) :& r+      LambdaCodeRec lBody ->+        let res = RfNormal $ PUSH a `Seq` PAIR `Seq` LAMBDA_REC lBody `Seq` SWAP `Seq` EXEC+        in pure $ StkEl (VLam $ LambdaCode res) :& r   where     doApply :: Instr ('TPair a i ': s) o -> Instr (i ': s) o     doApply b = PUSH a `Seq` PAIR `Seq` Nested b@@ -687,7 +708,7 @@     mkViewEnv :: ContractAddress -> ContractState -> ContractEnv -> ContractEnv     mkViewEnv calledAddr viewedContractState ContractEnv{..} = ContractEnv       { ceBalance = csBalance viewedContractState-      , ceSender = MkConstrainedAddress ceSelf+      , ceSender = Constrained ceSelf       , ceSelf = calledAddr       , ceSource       , ceAmount = zeroMutez@@ -703,7 +724,7 @@       pure $ StkEl (VContract (MkAddress ceSelf) sepc) :& r runInstrImpl _ (AnnCONTRACT (Anns2' _ (_ :: T.Notes a)) instrEpName) (StkEl (VAddress epAddr) :& r) = do   ContractEnv{..} <- ask-  T.EpAddress' (MkConstrainedAddress addr) addrEpName <- pure epAddr+  T.EpAddress' (Constrained addr) addrEpName <- pure epAddr   let mepName =         case (instrEpName, addrEpName) of           (DefEpName, DefEpName) -> Just DefEpName@@ -765,7 +786,7 @@               globalCounter   let resEpAddr = EpAddress resAddr DefEpName   let resOp = CreateContract-        (MkConstrainedAddress originator) (unwrapMbKeyHash mbKeyHash) m g contract globalCounter+        (Constrained originator) (unwrapMbKeyHash mbKeyHash) m g contract globalCounter   pure $ StkEl (VOp (OpCreateContract resOp))       :& StkEl (VAddress resEpAddr)       :& r@@ -805,10 +826,10 @@   let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]   pure $ StkEl (VBool $ checkPairing pairs') :& r runInstrImpl _ AnnSOURCE{} r = do-  ContractEnv{ceSource=MkConstrainedAddress ceSource} <- ask+  ContractEnv{ceSource=Constrained ceSource} <- ask   pure $ StkEl (VAddress $ EpAddress ceSource DefEpName) :& r runInstrImpl _ AnnSENDER{} r = do-  ContractEnv{ceSender=MkConstrainedAddress ceSender} <- ask+  ContractEnv{ceSender=Constrained ceSender} <- ask   pure $ StkEl (VAddress $ EpAddress ceSender DefEpName) :& r runInstrImpl _ AnnADDRESS{} (StkEl (VContract a sepc) :& r) =   pure $ StkEl (VAddress $ EpAddress' a (sepcName sepc)) :& r@@ -823,6 +844,12 @@   pure $ StkEl (VAddress $ EpAddress ceSelf DefEpName) :& r runInstrImpl _ AnnTICKET{} (StkEl dat :& StkEl (VNat am) :& r) = do   ContractEnv{..} <- ask+  let result = VOption do+        guard (am /= 0)+        pure $ VTicket (MkAddress ceSelf) dat am+  pure $ StkEl (result) :& r+runInstrImpl _ AnnTICKET_DEPRECATED{} (StkEl dat :& StkEl (VNat am) :& r) = do+  ContractEnv{..} <- ask   pure $ StkEl (VTicket (MkAddress ceSelf) dat am) :& r runInstrImpl _ AnnREAD_TICKET{} (te@(StkEl (VTicket addr dat am)) :& r) = do   pure $@@ -865,7 +892,7 @@  -- | Evaluates an arithmetic operation and either fails or proceeds. runArithOp-  :: (ArithOp aop n m, EvalM monad)+  :: (ArithOp aop n m, EvalM' ext monad)   => proxy aop   -> StkEl n   -> StkEl m@@ -909,7 +936,7 @@ unwrapMbKeyHash :: Maybe (T.Value 'T.TKeyHash) -> Maybe KeyHash unwrapMbKeyHash mbKeyHash = mbKeyHash <&> \(VKeyHash keyHash) -> keyHash -interpretExt :: EvalM m => InstrRunner m -> SomeItStack -> m ()+interpretExt :: EvalM' ext m => InstrRunner m -> SomeItStack -> m () interpretExt _ (SomeItStack (T.PRINT (T.PrintComment pc)) st) = do   let getEl (Left l) = l       getEl (Right str) = withStackElem str st (pretty . seValue)@@ -943,7 +970,7 @@       (e :& _, Zero) -> cont e       (_ :& es, Succ n) -> loop (es, n) -assignBigMapIds' :: EvalM m => Value t -> m (Value t)+assignBigMapIds' :: EvalM' ext m => Value t -> m (Value t) assignBigMapIds' val = do   bigMapCounter0 <- view isBigMapCounterL <$> getInterpreterState   let (storageWithIds, bigMapCounter1) = runState (assignBigMapIds True val) bigMapCounter0@@ -971,6 +998,13 @@ incrementCounter = modifyInterpreterState $ \iState ->       iState { isGlobalCounter = isGlobalCounter iState + 1 } -(deriveGADTNFData ''MichelsonFailed)+instance NFData ext => NFData (MichelsonFailed ext) where+  rnf = \case+    MichelsonFailedWith x -> rnf x+    MichelsonArithError x -> rnf x+    MichelsonGasExhaustion -> ()+    MichelsonFailedTestAssert x -> rnf x+    MichelsonUnsupported x -> rnf x+    MichelsonExt x -> rnf x -instance NFData MichelsonFailureWithStack+instance NFData ext => NFData (MichelsonFailureWithStack ext)

@@ -27,11 +27,10 @@ import Prelude hiding (EQ, GT, LT)  import Control.Lens (makeLensesFor)-import Data.Constraint (Dict(..), (\\))+import Data.Constraint (Dict(..)) import Data.Default (Default(def)) import Data.Singletons (sing) import Data.Type.Equality ((:~:)(Refl))-import Unsafe.Coerce (unsafeCoerce)  import Morley.Michelson.Interpret.Pack (packValue') import Morley.Michelson.Typed.Aliases (Value)@@ -42,9 +41,7 @@ import Morley.Michelson.Typed.T import Morley.Michelson.Typed.Util (DfsSettings(..), dfsModifyInstr) import Morley.Michelson.Typed.Value-import Morley.Util.Peano import Morley.Util.PeanoNatural-import Morley.Util.Type  ---------------------------------------------------------------------------- -- High level@@ -395,39 +392,11 @@ digDug = Rule \case   (DIG (x :: PeanoNatural n) :: Instr inp t) :# (DUG y :: Instr t out) :# xs     | Just Refl <- eqPeanoNat x y-    -> Just xs \\ digDugProof @inp @out @t @n (singPeanoNat x)+    -> Just xs   (DIG (x :: PeanoNatural n) :: Instr inp t) :# (DUG y :: Instr t out)     | Just Refl <- eqPeanoNat x y-    -> Just Nop \\ digDugProof @inp @out @t @n (singPeanoNat x)+    -> Just Nop   _ -> Nothing--digDugProof-  :: forall inp out t n a.-     ( KnownList inp-     , inp ~ (Take n inp ++ (a ': Drop ('S n) inp))-     , t ~ (a ': Take n inp ++ Drop ('S n) inp)-     , out ~ (Take n (Drop ('S 'Z) t) ++ (a ': Drop ('S n) t))-     )-  => SingNat n -> inp :~: out-{-# RULES "digDugProof" forall n. digDugProof n = unsafeCoerce Refl #-}-{-# INLINE[1] digDugProof #-}-digDugProof n = Refl-  \\ lemma1 n inpS-  \\ lemma2 n inpS-  where-    inpS = klist @inp-    lemma1 :: forall xs m. SingNat m -> KList xs -> Take m xs :~: Take m (Take m xs ++ Drop ('S m) xs)-    lemma1 = \case-      SZ -> const Refl-      SS m -> \case-        KNil -> Refl-        KCons _ (Proxy :: Proxy ys) -> Refl \\ lemma1 m (klist @ys)-    lemma2 :: forall xs m. SingNat m -> KList xs -> Drop ('S m) xs :~: Drop m (Take m xs ++ Drop ('S m) xs)-    lemma2 = \case-      SZ -> const Refl-      SS m -> \case-        KNil -> Refl-        KCons _ (Proxy :: Proxy ys) -> lemma2 m (klist @ys)  -- TODO [#299]: optimize sequences of more than 2 DROPs. -- | Sequences of @DROP@s can be turned into single @DROP n@.

@@ -146,7 +146,7 @@     Nothing ->       fail $ "Duplicate contract field: " <> pretty result   where-    -- | @ensureNotDuplicate@ provides a better message and point to the correct line+    -- @ensureNotDuplicate@ provides a better message and point to the correct line     -- when the parser fails.     contractTuple = fmap reverse . executingStateT [] $ do       (`sepEndBy` lift semicolon) $ do

@@ -49,10 +49,11 @@   , sourceOp, senderOp, chainIdOp, sha3Op, keccakOp, neverOp   , votingPowerOp, totalVotingPowerOp, try unpairNOp   , unpairOp-  , ticketOp, readTicketOp, splitTicketOp, joinTicketsOp+  , ticketOp, ticketDeprecatedOp, readTicketOp, splitTicketOp, joinTicketsOp   , openChestOp   , saplingEmptyStateOp, saplingVerifyUpdateOp, minBlockTimeOp   , emitOp+  , lambdaRecOp opParser   ]  -- | Parse a sequence of instructions.@@ -137,6 +138,10 @@ lambdaOp opParser =   word "LAMBDA" LAMBDA <*> noteDef <*> type_ <*> type_ <*> ops' opParser +lambdaRecOp :: Parser ParsedOp -> Parser ParsedInstr+lambdaRecOp opParser =+  word "LAMBDA_REC" LAMBDA_REC <*> noteDef <*> type_ <*> type_ <*> ops' opParser+ neverOp :: Parser ParsedInstr neverOp = word "NEVER" NEVER -- Generic comparison@@ -459,6 +464,9 @@  ticketOp :: Parser ParsedInstr ticketOp = word "TICKET" TICKET <*> noteDef++ticketDeprecatedOp :: Parser ParsedInstr+ticketDeprecatedOp = word "TICKET_DEPRECATED" TICKET_DEPRECATED <*> noteDef  readTicketOp :: Parser ParsedInstr readTicketOp = word "READ_TICKET" READ_TICKET <*> noteDef

@@ -42,7 +42,7 @@   [ stringLiteral, bytesLiteral, intLiteral, unitValue   , trueValue, falseValue, pairValueCore opParser, leftValue opParser   , rightValue opParser, someValue opParser, noneValue, nilValue-  , seqOrLambda opParser, mapValue opParser+  , seqOrLambda opParser, mapValue opParser, lambdaRecValue opParser   ]  seqOrLambda :: Parser ParsedOp -> Parser ParsedValue@@ -119,6 +119,12 @@  lambdaValue :: Parser ParsedOp -> Parser ParsedValue lambdaValue opParser = U.ValueLambda <$> ops1+  where+    ops1 :: Parser (NonEmpty ParsedOp)+    ops1 = braces $ sepEndBy1 opParser semicolon++lambdaRecValue :: Parser ParsedOp -> Parser ParsedValue+lambdaRecValue opParser = word "Lambda_rec" U.ValueLamRec <*> ops1   where     ops1 :: Parser (NonEmpty ParsedOp)     ops1 = braces $ sepEndBy1 opParser semicolon

@@ -13,7 +13,6 @@   , printUntypedValue   ) where -import Data.Constraint (withDict) import Data.Singletons (SingI) import Data.Text.Lazy qualified as TL @@ -22,40 +21,39 @@ import Morley.Michelson.Untyped qualified as U  -- | Convert an untyped contract into a textual representation which--- will be accepted by the OCaml reference client: tezos-client.+-- will be accepted by the OCaml reference client: @octez-client@. printUntypedContract :: (RenderDoc op) => Bool -> U.Contract' op -> TL.Text printUntypedContract forceSingleLine = printDoc forceSingleLine . renderDoc doesntNeedParens  -- | Convert a typed contract into a textual representation which--- will be accepted by the OCaml reference client: tezos-client.+-- will be accepted by the OCaml reference client: @octez-client@. printTypedContractCode :: (SingI p, SingI s) => Bool -> T.ContractCode p s -> TL.Text printTypedContractCode forceSingleLine =   printUntypedContract forceSingleLine . T.convertContractCode  -- | Convert typed contract into a textual representation which--- will be accepted by the OCaml reference client: tezos-client.+-- will be accepted by the OCaml reference client: @octez-client@. printTypedContract :: Bool -> T.Contract p s -> TL.Text printTypedContract forceSingleLine fc@T.Contract{} =   printUntypedContract forceSingleLine $ T.convertContract fc  -- | Convert typed value into a textual representation which--- will be accepted by the OCaml reference client: tezos-client.+-- will be accepted by the OCaml reference client: @octez-client@. printTypedValue   :: forall t.       (T.ProperUntypedValBetterErrors t)   => Bool -> T.Value t -> TL.Text printTypedValue forceSingleLine =-  withDict (T.properUntypedValEvi @t) $   printUntypedValue forceSingleLine . T.untypeValue  -- | Convert untyped value into a textual representation which--- will be accepted by the OCaml reference client: tezos-client.+-- will be accepted by the OCaml reference client: @octez-client@. printUntypedValue :: (RenderDoc op) => Bool -> U.Value' op -> TL.Text printUntypedValue forceSingleLine =   printDoc forceSingleLine . renderDoc doesntNeedParens  -- | Convert 'T.SomeContract' into a textual representation which--- will be accepted by the OCaml reference client: tezos-client.+-- will be accepted by the OCaml reference client: @octez-client@. printSomeContract :: Bool -> T.SomeContract -> TL.Text printSomeContract forceSingleLine (T.SomeContract fc) =   printTypedContract forceSingleLine fc

@@ -2,7 +2,7 @@ -- SPDX-License-Identifier: LicenseRef-MIT-OA  -- | Utilities for rendering Michelson code in a format compatible with--- Tezos software (e.g @tezos-client@)+-- Octez software (e.g @octez-client@) module Morley.Michelson.Printer.Util   ( RenderDoc(..)   , Prettier(..)@@ -13,7 +13,6 @@   , renderOpsList   , renderOpsListNoBraces   , renderAnyBuildable-  , spaces   , wrapInParens   , buildRenderDoc   , buildRenderDocExtended@@ -35,9 +34,9 @@ import Data.Text.Lazy.Builder (Builder) import Fmt (Buildable, pretty) import Text.PrettyPrint.Leijen.Text-  (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, encloseSep, hcat, hsep, isEmpty,-  lbracket, parens, punctuate, rbracket, renderOneLine, renderPretty, semi, sep, space, text, (<+>),-  (<//>))+  (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, encloseSep, hsep, isEmpty, lbracket,+  parens, punctuate, rbracket, renderOneLine, renderPretty, semi, sep, space, text, textStrict,+  (<+>), (<//>))  -- | Environment carried during recursive rendering. newtype RenderContext = RenderContext@@ -64,6 +63,9 @@   isRenderable :: a -> Bool   isRenderable _ = True +instance RenderDoc Text where+  renderDoc _ = textStrict+ -- | Renders a list of 'RenderDoc' elements surrounded with square brackets, -- separated by a comma and a space. renderDocList :: RenderDoc a => RenderContext -> [a] -> Doc@@ -105,10 +107,6 @@ renderOpsListNoBraces oneLine =   align . (if oneLine then hsep else sep) . punctuate semi .     fmap (renderDoc doesntNeedParens) . filter isRenderable---- | Create a specific number of spaces.-spaces :: Int -> Doc-spaces x = hcat $ replicate x space  -- | Wrap documents in parentheses if there are two or more in the list. wrapInParens :: RenderContext -> NonEmpty Doc -> Doc

@@ -9,6 +9,11 @@     originateContract   , runContract   , transfer+  , runCode+  , RunCodeParameters(..)+  , runCodeParameters+  , resolveRunCodeBigMaps+  , mkBigMapFinder    -- * Other helpers   , parseContract@@ -52,7 +57,7 @@   , elUpdates   ) where -import Control.Lens (assign, at, makeLenses, (.=), (<>=))+import Control.Lens (assign, at, each, ix, makeLenses, to, (.=), (<>=)) import Control.Monad.Except (Except, liftEither, runExcept, throwError) import Data.Constraint (Dict(..), (\\)) import Data.Default (def)@@ -66,16 +71,17 @@ import Text.Megaparsec (parse)  import Morley.Michelson.Interpret-  (ContractEnv(..), InterpretError(..), InterpretResult(..), InterpreterState(..), MorleyLogs(..),+  (ContractEnv(..), InterpretError, InterpretResult(..), InterpreterState(..), MorleyLogs(..),   RemainingSteps(..), assignBigMapIds, handleContractReturn, interpret) import Morley.Michelson.Macro (ParsedOp, expandContract) import Morley.Michelson.Parser qualified as P import Morley.Michelson.Runtime.Dummy import Morley.Michelson.Runtime.GState+import Morley.Michelson.Runtime.RunCode import Morley.Michelson.Runtime.TxData import Morley.Michelson.TypeCheck import Morley.Michelson.Typed-  (CreateContract(..), EntrypointCallT, EpName, Operation'(..), SomeConstrainedValue(..),+  (Constrained(..), CreateContract(..), EntrypointCallT, EpName, Operation'(..),   SomeContractAndStorage(..), SomeStorage, TransferTokens(..), untypeValue) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Operation@@ -87,6 +93,7 @@ import Morley.Tezos.Core   (Mutez, Timestamp(..), getCurrentTime, unsafeAddMutez, unsafeSubMutez, zeroMutez) import Morley.Tezos.Crypto (KeyHash, parseHash)+import Morley.Util.Interpolate (itu) import Morley.Util.MismatchError import Morley.Util.Named @@ -178,11 +185,17 @@ data ExecutorError' a   = EEUnknownContract a   -- ^ The interpreted contract hasn't been originated.-  | EEInterpreterFailed a-                        InterpretError+  | EEInterpreterFailed a (InterpretError Void)   -- ^ Interpretation of Michelson contract failed.   | EEUnknownAddressAlias SomeAlias-  -- ^ Given alias doesn't refer to any address.+  -- ^ The given alias isn't associated with any address+  -- OR is associated with an address of an unexpected kind+  -- (e.g. we expected an implicit address and found a contract address, or vice-versa).+  | EEUnknownL1AddressAlias Text+  -- ^ The given alias is not associated with any address.+  | EEAmbiguousAlias Text ImplicitAddress ContractAddress+  -- ^ The given alias is ambiguous, i.e. it is associated with __both__ an+  -- implicit address and a contract address.   | EEUnknownSender a   -- ^ Sender address is unknown.   | EEUnknownManager a@@ -190,13 +203,13 @@   | EENotEnoughFunds a Mutez   -- ^ Sender doesn't have enough funds.   | EEEmptyImplicitContract a-  -- ^ Sender is an implicit address with the balance of 0. We mimic tezos-client in calling it-  -- "Empty implicit contract".+  -- ^ Sender is an implicit address with the balance of 0. We mimic+  -- @octez-client@ in calling it "Empty implicit contract".   | EEZeroTransaction a   -- ^ Sending 0tz towards an address.   | EEFailedToApplyUpdates GStateUpdateError   -- ^ Failed to apply updates to GState.-  | EEIllTypedParameter a TCError+  | EEIllTypedParameter a TcError   -- ^ Contract parameter is ill-typed.   | EEUnexpectedParameterType a (MismatchError T.T)   -- ^ Contract parameter is well-typed, but its type does@@ -219,8 +232,18 @@   build =     \case       EEUnknownAddressAlias (SomeAlias (alias :: Alias kind)) ->-        ("The alias " +| alias |+ " doesn't have any associated " +| demote @kind |+ " addresses")-        \\ aliasKindSanity alias+        [itu|The alias '#{alias}' is not associated to a #{kind} address|]+        where+          kind = demote @kind \\ aliasKindSanity alias :: AddressKind+      EEUnknownL1AddressAlias aliasText ->+        [itu|The alias '#{aliasText}' is not associated with any address|]+      EEAmbiguousAlias aliasText implicitAddr contractAddr ->+        [itu|+        The alias '#{aliasText}' is assigned to both:+          * a contract address: #{contractAddr}+          * and an implicit address: #{implicitAddr}+        Use '#{contractPrefix}:#{aliasText}' or '#{implicitPrefix}:#{aliasText}' to disambiguate.+        |]       EEUnknownContract addr -> "The contract is not originated " +| addr |+ ""       EEInterpreterFailed addr err ->         "Michelson interpreter failed for contract " +| addr |+ ": " +| err |+ ""@@ -375,6 +398,28 @@         Nothing -> error $ pretty addr <> " is unknown"         Just ContractState{..} -> return $ SomeStorage csStorage +-- | Construct 'BigMapFinder' using the current executor context.+mkBigMapFinder :: ExecutorM BigMapFinder+mkBigMapFinder = do+  pureState <- get++  pure \bigMapId ->+    pureState ^?+      esGState . gsContractAddressesL . each . to getContractStorage .+        to (getBigMapsWithId bigMapId) . each+  where+    getContractStorage :: ContractState -> T.SomeValue+    getContractStorage (ContractState _ _ storage _) = T.SomeValue storage++    getBigMapsWithId :: Natural -> T.SomeValue -> [T.SomeVBigMap]+    getBigMapsWithId bigMapId (T.SomeValue val) =+      T.dfsFoldMapValue+        (\v -> case v of+            T.VBigMap (Just bigMapId') _ | bigMapId' == bigMapId -> [T.SomeVBigMap v]+            _ -> []+        )+        val+ -- | Send a transaction to given address with given parameters. transfer   :: Maybe Timestamp@@ -383,14 +428,14 @@   -> Word64   -> FilePath   -> TypeCheckOptions-  -> AddressOrAlias kind+  -> SomeAddressOrAlias   -> TxData   -> "verbose" :! Bool   -> "dryRun" :? Bool   -> IO () transfer maybeNow maybeLevel maybeMinBlockTime maxSteps dbPath tcOpts destination txData verbose dryRun = do   void $ runExecutorMWithDB maybeNow maybeLevel maybeMinBlockTime dbPath (RemainingSteps maxSteps) verbose dryRun $ do-    destAddr <- MkAddress <$> resolveAddress destination+    destAddr <- resolveAddress destination     executeGlobalOperations tcOpts [TransferOp $ TransferOperation destAddr txData 0]  ----------------------------------------------------------------------------@@ -496,19 +541,30 @@         mapM_ putTextLn logs       putTextLn "" -- extra break line to separate logs from two sequence contracts --- | Resolves 'AddressOrAlias' type to 'KindedAddress' of the appropriate kind.+-- | Resolves 'SomeAddressOrAlias' type to an address. resolveAddress-  :: forall kind. AddressOrAlias kind-  -> ExecutorM (KindedAddress kind)-resolveAddress (AddressResolved addr) = pure addr-resolveAddress (AddressAlias alias) = do-  let s :: SingAddressKind kind = T.sing @kind \\ aliasKindSanity alias-  addrMb <- use $ case s of-    SAddressKindImplicit -> esGState . gsImplicitAddressAliasesL . at alias-    SAddressKindContract -> esGState . gsContractAddressAliasesL . at alias-  case addrMb of-    Just addr -> pure addr-    Nothing -> throwError $ EEUnknownAddressAlias $ SomeAlias alias+  :: SomeAddressOrAlias+  -- TODO [#905] or [#889]: Change the return type to `L1Address`+  -> ExecutorM Address+resolveAddress = \case+  SAOAKindUnspecified aliasText -> do+    implicitAddrMb <- preuse $ esGState . gsImplicitAddressAliasesL . ix (ImplicitAlias aliasText)+    contractAddrMb <- preuse $ esGState . gsContractAddressAliasesL . ix (ContractAlias aliasText)+    case (implicitAddrMb, contractAddrMb) of+      (Nothing, Nothing) -> throwError $ EEUnknownL1AddressAlias aliasText+      (Just implicitAddr, Nothing) -> pure $ Constrained implicitAddr+      (Nothing, Just contractAddr) -> pure $ Constrained contractAddr+      (Just implicitAddr, Just contractAddr) -> throwError $ EEAmbiguousAlias aliasText implicitAddr contractAddr+  SAOAKindSpecified (AddressResolved (addr@ContractAddress{})) -> pure $ Constrained addr+  SAOAKindSpecified (AddressResolved (addr@ImplicitAddress{})) -> pure $ Constrained addr+  SAOAKindSpecified (AddressAlias alias) -> do+    addrMb <- preuse $+      case alias of+        ImplicitAlias{} -> esGState . gsImplicitAddressAliasesL . ix alias . to Constrained+        ContractAlias{} -> esGState . gsContractAddressAliasesL . ix alias . to Constrained+    case addrMb of+      Just addr -> pure addr+      Nothing -> throwError $ EEUnknownAddressAlias $ SomeAlias alias  -- | Execute a list of global operations, returning a list of generated events. executeGlobalOperations@@ -517,7 +573,7 @@   -> ExecutorM [EmitOperation] executeGlobalOperations tcOpts = concatMapM $ \op -> executeMany (#isGlobalOp :! True) [op]   where-    -- | Execute a list of operations and additional operations they return, until there are none.+    -- Execute a list of operations and additional operations they return, until there are none.     executeMany :: "isGlobalOp" :! Bool -> [ExecutorOp] -> ExecutorM [EmitOperation]     executeMany isGlobalOp = \case         [] -> pure []@@ -530,7 +586,7 @@               executeDelegation isGlobalOp operation               executeMany (#isGlobalOp :! False) opsTail             TransferOp transferOperation -> do-              moreOps <- executeTransfer isGlobalOp Nothing tcOpts transferOperation+              moreOps <- executeTransfer isGlobalOp tcOpts transferOperation               executeMany (#isGlobalOp :! False) $ moreOps <> opsTail             EmitOp emitOperation -> do               liftM2 (:) (executeEmit isGlobalOp emitOperation) $@@ -608,7 +664,9 @@    gs <- use esGState -  let updates = [GSSetDelegate sdoContract sdoDelegate]+  Constrained address <- pure sdoContract++  let updates = [GSSetDelegate address sdoDelegate]   case applyUpdates updates gs of     Left err -> throwError $ EEFailedToApplyUpdates err     Right newGS -> do@@ -630,20 +688,13 @@ -- | Execute a transfer operation. executeTransfer   :: "isGlobalOp" :! Bool-  -> Maybe Mutez-  -- ^ Whether to override the destination's balance.-  ---  -- When it's a `Just`, the destination's balance will be set to the given amount-  -- and no tz will be debited from the sender's account.-  -- This is useful to emulate the behaviour of the Tezos RPC's @/run_code@ endpoint.   -> TypeCheckOptions   -> TransferOperation   -> ExecutorM [ExecutorOp]-executeTransfer (arg #isGlobalOp -> isGlobalOp)-  overrideBalanceMb tcOpts+executeTransfer (arg #isGlobalOp -> isGlobalOp) tcOpts     transferOperation@(       TransferOperation (MkAddress (addr :: KindedAddress kind))-        txData@TxData{tdSenderAddress=MkConstrainedAddress senderAddr,..} _) = do+        txData@TxData{tdSenderAddress=Constrained senderAddr,..} _) = do     when isGlobalOp $       beginGlobalOperation @@ -673,12 +724,11 @@           throwError $ EETransactionFromContract (MkAddress senderAddr) tdAmount        Just Refl -> do-        when (isNothing overrideBalanceMb) $-          case senderBalance of-            Nothing -> throwError $ EEEmptyImplicitContract $ MkAddress senderAddr-            Just balance | balance == zeroMutez ->-              throwError $ EEEmptyImplicitContract $ MkAddress senderAddr-            _ -> pass+        case senderBalance of+          Nothing -> throwError $ EEEmptyImplicitContract $ MkAddress senderAddr+          Just balance | balance == zeroMutez ->+            throwError $ EEEmptyImplicitContract $ MkAddress senderAddr+          _ -> pass      case isImplicitAddress addr of       Nothing -> pass@@ -690,19 +740,17 @@         when (isZeroTransfer) $           throwError $ EEZeroTransaction $ MkAddress addr -    mDecreaseSenderBalance <--      if isNothing overrideBalanceMb && not isZeroTransfer-        then case senderBalance of-          Nothing -> throwError $ EEUnknownSender $ MkAddress senderAddr-          Just balance-            | balance < tdAmount ->-              throwError $ EENotEnoughFunds (MkAddress senderAddr) balance-            | otherwise -> do-              -- Subtraction is safe because we have checked its-              -- precondition in guard.-              let newBal = balance `unsafeSubMutez` tdAmount-              pure $ Just $ GSSetBalance senderAddr newBal-        else pure Nothing+    mDecreaseSenderBalance <- case senderBalance of+      _ | isZeroTransfer -> pure Nothing+      Nothing -> throwError $ EEUnknownSender $ MkAddress senderAddr+      Just balance+        | balance < tdAmount ->+          throwError $ EENotEnoughFunds (MkAddress senderAddr) balance+        | otherwise -> do+          -- Subtraction is safe because we have checked its+          -- precondition in guard.+          let newBal = balance `unsafeSubMutez` tdAmount+          pure $ Just $ GSSetBalance senderAddr newBal      let commonFinishup           :: Dict (L1AddressKind kind)@@ -743,15 +791,13 @@             upd = GSAddImplicitAddress addr addrState            onlyUpdates Dict [upd]-        Just oldBalance -> do+        Just ImplicitState{..} -> do           let-            -- Calculate the account's new balance, unless `overrideBalanceMb` is used.-            -- Note: `unsafeAddMutez` can't overflow if global state is correct (because we can't-            -- create money out of nowhere)-            newBalance =-              fromMaybe-                (oldBalance `unsafeAddMutez` tdAmount)-                overrideBalanceMb+            -- Calculate the account's new balance.+            --+            -- Note: `unsafeAddMutez` can't overflow if global state is correct+            -- (because we can't create money out of nowhere)+            newBalance = isBalance `unsafeAddMutez` tdAmount             upd = GSSetBalance addr newBalance           onlyUpdates Dict [upd]       ContractAddress{} -> case addresses ^. at addr of@@ -759,13 +805,11 @@         Just ContractState{..} -> do           let             existingContracts = extractAllContracts gs-            newBalance =-              -- Calculate the contract's new balance, unless `overrideBalanceMb` is used.-              -- Note: `unsafeAddMutez` can't overflow if global state is correct (because we can't-              -- create money out of nowhere)-              fromMaybe-                (csBalance `unsafeAddMutez` tdAmount)-                overrideBalanceMb+            -- Calculate the contract's new balance.+            --+            -- Note: `unsafeAddMutez` can't overflow if global state is+            -- correct (because we can't create money out of nowhere)+            newBalance = csBalance `unsafeAddMutez` tdAmount             epName = tdEntrypoint            T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)@@ -812,7 +856,7 @@               , ceContracts = gsContractAddresses gs               , ceSelf = addr               , ceSource = sourceAddr-              , ceSender = MkConstrainedAddress senderAddr+              , ceSender = Constrained senderAddr               , ceAmount = tdAmount               , ceVotingPowers = gsVotingPowers gs               , ceChainId = gsChainId gs@@ -859,7 +903,6 @@               ]           commonFinishup Dict updates sideEffects (Just iur) newRemainingSteps - ---------------------------------------------------------------------------- -- Simple helpers ----------------------------------------------------------------------------@@ -886,7 +929,7 @@         T.VContract destAddress sepc ->           let txData =                 TxData-                  { tdSenderAddress = MkConstrainedAddress interpretedAddr+                  { tdSenderAddress = Constrained interpretedAddr                   , tdEntrypoint = T.sepcName sepc                   , tdParameter = TxTypedParam (ttTransferArgument tt)                   , tdAmount = ttAmount tt@@ -898,14 +941,12 @@                   , toCounter = ttCounter tt                   }           in TransferOp transferOperation-    OpSetDelegate T.SetDelegate{..} -> case interpretedAddr of-      addr@ContractAddress{} -> pure $ SetDelegateOp SetDelegateOperation-        { sdoContract = addr-        , sdoDelegate = sdMbKeyHash-        , sdoCounter = sdCounter-        }-      _ -> throwError $ EEUnknownContract $ MkAddress interpretedAddr-    OpCreateContract CreateContract{ccOriginator=MkConstrainedAddress ccOriginator, ..} ->+    OpSetDelegate T.SetDelegate{..} -> pure $ SetDelegateOp SetDelegateOperation+      { sdoContract = Constrained interpretedAddr+      , sdoDelegate = sdMbKeyHash+      , sdoCounter = sdCounter+      }+    OpCreateContract CreateContract{ccOriginator=Constrained ccOriginator, ..} ->       pure $ OriginateOp OriginationOperation         { ooOriginator = ccOriginator         , ooDelegate = ccDelegate

@@ -14,12 +14,14 @@   , dummyOrigination   , dummyMinBlockTime   , dummySelf+  , dummyContractState   ) where  import Data.Default (def)  import Morley.Michelson.Interpret (ContractEnv(..), RemainingSteps)-import Morley.Michelson.Runtime.GState (BigMapCounter, dummyVotingPowers, genesisAddress)+import Morley.Michelson.Runtime.GState+  (BigMapCounter, ContractState(..), dummyVotingPowers, genesisAddress) import Morley.Michelson.Typed (ParameterScope, StorageScope) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Operation (OriginationOperation(..))@@ -64,8 +66,8 @@   , ceBalance = [tz|100u|]   , ceContracts = mempty   , ceSelf = dummySelf-  , ceSource = MkConstrainedAddress genesisAddress-  , ceSender = MkConstrainedAddress genesisAddress+  , ceSource = Constrained genesisAddress+  , ceSender = Constrained genesisAddress   , ceAmount = [tz|100u|]   , ceVotingPowers = dummyVotingPowers   , ceChainId = dummyChainId@@ -92,4 +94,21 @@   , ooContract = contract   , ooCounter = counter   , ooAlias = Nothing+  }++-- | Construct dummy 'ContractState' for the given parameter type. This can be+-- useful with @runCode@. The state constructed doesn't have any views, and uses+-- @unit@ for storage.+dummyContractState :: T.ParameterScope t => T.ParamNotes t -> ContractState+dummyContractState notes = ContractState+  { csContract = T.Contract+      { cCode = T.mkContractCode $ T.CDR T.:# T.NIL T.:# T.PAIR+      , cParamNotes = notes+      , cStoreNotes = T.starNotes+      , cEntriesOrder = def+      , cViews = def+      }+  , csDelegate = Nothing+  , csBalance = [tz|100u|]+  , csStorage = T.VUnit   }

@@ -8,6 +8,9 @@     -- * Auxiliary types     ContractState (..)   , VotingPowers (..)+  , ImplicitState (..)+  , isBalanceL+  , isDelegateL   , vpPick   , vpTotal   , mkVotingPowers@@ -63,11 +66,12 @@ import Data.Default (def) import Data.Map.Strict qualified as Map import Data.Type.Equality ((:~:)(..))-import Fmt (Buildable(build), pretty, (+|), (|+))+import Fmt (Buildable(build), nameF, pretty, unlinesF, (+|), (|+)) import System.IO.Error (IOError, isDoesNotExistError)  import Morley.Michelson.TypeCheck-  (SomeParamType(..), TcOriginatedContracts, typeCheckContractAndStorage, typeCheckingWith)+  (SomeParamType(..), TcOriginatedContracts, tcStrict, typeCheckContractAndStorage,+  typeCheckingWith) import Morley.Michelson.Typed qualified as T import Morley.Michelson.Typed.Existential (SomeContractAndStorage(..)) import Morley.Michelson.Typed.Scope@@ -86,6 +90,25 @@ import Morley.Util.SizedList qualified as SL import Morley.Util.SizedList.Types +data ImplicitState = ImplicitState+  { isBalance :: Mutez+    -- ^ Implicit address balance.+  , isDelegate :: Maybe KeyHash+    -- ^ Delegate, if set. Implicit address can have a delegate set to itself,+    -- then it's considered "registered delegate" and can be set as delegate for+    -- other addresses. It's impossible to "unregister" a delegate, so once+    -- delegate is set to the address itself, it can't be changed.+  } deriving stock (Show, Eq)++deriveJSON morleyAesonOptions ''ImplicitState+makeLensesWith postfixLFields ''ImplicitState++instance Buildable ImplicitState where+  build ImplicitState{..} = nameF "Implicit state" $ unlinesF+    [ nameF "Balance" $ build isBalance+    , nameF "Delegate" $ build isDelegate+    ]+ -- | State of a contract with code. data ContractState =   forall cp st. (ParameterScope cp, StorageScope st) => ContractState@@ -129,7 +152,7 @@       (uStorage :: Value) <- o .: "storage"       (uContract :: Contract) <- o .: "contract"       (delegate :: Maybe KeyHash) <- o .:? "delegate"-      case typeCheckingWith def $ typeCheckContractAndStorage uContract uStorage of+      case typeCheckingWith def{ tcStrict=False } $ typeCheckContractAndStorage uContract uStorage of         Right (SomeContractAndStorage contract storage) ->           pure $ ContractState balance contract storage delegate         Left err -> fail $ "Unable to parse `ContractState`: " <> pretty err@@ -188,7 +211,7 @@ data GState = GState   { gsChainId :: ChainId   -- ^ Identifier of chain.-  , gsImplicitAddresses :: Map ImplicitAddress Mutez+  , gsImplicitAddresses :: Map ImplicitAddress ImplicitState   -- ^ All known implicit addresses and their state (i.e. balance)   , gsContractAddresses :: Map ContractAddress ContractState   -- ^ All known contract addresses and their state.@@ -261,7 +284,7 @@   => ImplicitAddress genesisAddressN = SL.index @n genesisAddresses --- | Dummy 'VotingPowers'. We give all the voting power to two genesis addreses+-- | Dummy 'VotingPowers'. We give all the voting power to two genesis addresses -- as the addresses holding lot of money. Only two addresses are involved for -- simplicity. dummyVotingPowers :: VotingPowers@@ -275,7 +298,7 @@   GState   { gsChainId = dummyChainId   , gsImplicitAddresses = Map.fromList-    [ (genesis, money)+    [ (genesis, ImplicitState money Nothing)     | let (money, _) = maxBound @Mutez `divModMutezInt` genesisAddressesNum                     ?: error "Number of genesis addresses is 0"     , genesis <- toList genesisAddresses@@ -329,7 +352,7 @@   GSIncrementCounter :: GStateUpdate   GSUpdateCounter :: GlobalCounter -> GStateUpdate   GSSetBigMapCounter :: BigMapCounter -> GStateUpdate-  GSSetDelegate :: ContractAddress -> Maybe KeyHash -> GStateUpdate+  GSSetDelegate :: L1AddressKind kind => KindedAddress kind -> Maybe KeyHash -> GStateUpdate  deriving stock instance Show GStateUpdate @@ -354,25 +377,32 @@       GSSetBigMapCounter inc ->         "Increment internal big_map counter by: " +| build inc       GSSetDelegate addr key ->-        "Set delegate for contract " +| addr |+ " to " +| maybe "<nobody>" build key+        "Set delegate for " +| addr |+ " to " +| maybe "<nobody>" build key  data GStateUpdateError   = GStateAddressExists Address   | GStateUnknownAddress Address   | GStateStorageNotMatch ContractAddress   | GStateTxRollup TxRollupAddress GStateUpdate+  | GStateNotDelegate ImplicitAddress+  | GStateCantDeleteDelegate ImplicitAddress+  | GStateAlreadySetDelegate L1Address (Maybe KeyHash)   deriving stock (Show)  instance Buildable GStateUpdateError where-  build =-    \case-      GStateAddressExists addr -> "Address already exists: " <> build addr-      GStateUnknownAddress addr -> "Unknown address: " <> build addr-      GStateStorageNotMatch addr ->-        "Storage type does not match the contract in run-time state\-        \ when updating new storage value to address: " <> build addr-      GStateTxRollup addr op ->-        "Transaction rollup address " +| addr |+ " doesn't support this operation: " +| op |+ ""+  build = \case+    GStateAddressExists addr -> "Address already exists: " <> build addr+    GStateUnknownAddress addr -> "Unknown address: " <> build addr+    GStateStorageNotMatch addr ->+      "Storage type does not match the contract in run-time state\+      \ when updating new storage value to address: " <> build addr+    GStateTxRollup addr op ->+      "Transaction rollup address " +| addr |+ " doesn't support this operation: " +| op |+ ""+    GStateNotDelegate addr -> "Address " +| addr |+ " is not registered as delegate."+    GStateCantDeleteDelegate addr ->+      "Delegate deletion is forbidden for " +| addr |+ ""+    GStateAlreadySetDelegate addr kh ->+      "Already set delegate for " +| addr |+ " to " <> maybe "<nothing>" build kh  -- | Apply 'GStateUpdate' to 'GState'. applyUpdate :: GStateUpdate -> GState -> Either GStateUpdateError GState@@ -397,7 +427,7 @@ addImplicitAddress :: ImplicitAddress -> Mutez -> GState -> Either GStateUpdateError GState addImplicitAddress addr st gs   | addr `Map.member` (gsImplicitAddresses gs) = Left $ GStateAddressExists (MkAddress addr)-  | otherwise = Right $ gs & gsImplicitAddressesL . at addr ?~ st+  | otherwise = Right $ gs & gsImplicitAddressesL . at addr ?~ ImplicitState st Nothing  -- | Add an address if it hasn't been added before. addContractAddress :: ContractAddress -> ContractState -> GState -> Either GStateUpdateError GState@@ -438,16 +468,46 @@   => KindedAddress kind   -> Lens' (AddressStateFam kind) Mutez balanceLens = \case-  ImplicitAddress{} -> id+  ImplicitAddress{} -> isBalanceL   ContractAddress{} -> csBalanceL   where _ = usingImplicitOrContractKind @kind () +-- | Check if address delegate is set to itself, i.e. it's "registered delegate"+-- in network terms. "Registered delegates" can't change their delegate. On the+-- other hand, those can be set as delegates for other addresses.+isRegisteredDelegate :: ImplicitAddress -> GState -> Bool+isRegisteredDelegate addr@(ImplicitAddress kh) gs =+  gs ^? gsImplicitAddressesL . at addr . traverse . isDelegateL == Just (Just kh)+ -- | Set delegate for a given address-setDelegate :: ContractAddress -> Maybe KeyHash -> GState -> Either GStateUpdateError GState-setDelegate addr key = updateAddressState addr $ pure . (csDelegateL .~ key)+setDelegate+  :: forall kind. L1AddressKind kind+  => KindedAddress kind -> Maybe KeyHash -> GState -> Either GStateUpdateError GState+setDelegate addr newDelegate gs+  | Just oldDelegate@Just{} <- gs ^? addressesL addr . at addr . traverse . delegateLens+  , oldDelegate == newDelegate+  -- network fails when new delegate == old delegate == Just kh, so we do likewise+  -- note it _doesn't_ fail when new == old == Nothing+  = Left $ GStateAlreadySetDelegate (Constrained addr) newDelegate+  | ImplicitAddress{} <- addr+  , isRegisteredDelegate addr gs+  -- implicit addresses that are registered delegates can't change delegates+  = Left $ GStateCantDeleteDelegate addr+  | Just kh <- newDelegate+  , let keyAddr = ImplicitAddress kh+  , not $ isRegisteredDelegate keyAddr gs+  -- can't set delegate to an address not registered as delegate+  , MkAddress keyAddr /= MkAddress addr -- but implicit contract can set delegate to itself+  = Left $ GStateNotDelegate keyAddr+  | otherwise = updateAddressState addr (pure . (delegateLens .~ newDelegate)) gs+  where+    delegateLens :: Lens' (AddressStateFam kind) (Maybe KeyHash)+    delegateLens = case addr of+      ContractAddress{} -> csDelegateL+      ImplicitAddress{} -> isDelegateL  type family AddressStateFam kind where-  AddressStateFam 'AddressKindImplicit = Mutez+  AddressStateFam 'AddressKindImplicit = ImplicitState   AddressStateFam 'AddressKindContract = ContractState   -- TODO [#838]: support transaction rollups on the emulator   AddressStateFam 'AddressKindTxRollup = ()

@@ -33,7 +33,7 @@ import Morley.Michelson.Parser.Types (MichelsonSource(..)) import Morley.Michelson.Runtime (parseExpandContract) import Morley.Michelson.TypeCheck-  (TCError, typeCheckContract, typeCheckTopLevelType, typeCheckingWith, typeVerifyContract,+  (TcError, typeCheckContract, typeCheckTopLevelType, typeCheckingWith, typeVerifyContract,   typeVerifyTopLevelType) import Morley.Michelson.Typed (Contract, SingI, SomeContract(..), SomeValue, Value) import Morley.Michelson.Untyped qualified as U@@ -112,7 +112,7 @@ -- | Error type for 'importContract' function. data ContractReadError   = CREParse MichelsonSource ParserException-  | CRETypeCheck MichelsonSource TCError+  | CRETypeCheck MichelsonSource TcError   deriving stock (Show, Eq)  instance Buildable ContractReadError where@@ -189,7 +189,7 @@ -- | Error type for 'importValue' function. data ValueReadError   = VREParse MichelsonSource ParserException-  | VRETypeCheck MichelsonSource TCError+  | VRETypeCheck MichelsonSource TcError   deriving stock (Show, Eq)  instance Buildable ValueReadError where

@@ -0,0 +1,164 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++-- | Emulation of @run_code@.++module Morley.Michelson.Runtime.RunCode+  ( runCode+  , RunCodeParameters(..)+  , runCodeParameters+  , resolveRunCodeBigMaps+  ) where++import Data.Default (def)+import Data.Map qualified as Map++import Morley.Michelson.Interpret (ContractEnv(..), InterpretError(..), assignBigMapIds, interpret)+import Morley.Michelson.Runtime.Dummy+import Morley.Michelson.Runtime.GState+import Morley.Michelson.TypeCheck+import Morley.Michelson.Typed qualified as T+import Morley.Michelson.Typed.Operation+import Morley.Michelson.Untyped qualified as U+import Morley.Tezos.Address+import Morley.Tezos.Core (ChainId, Mutez, Timestamp(..), dummyChainId, zeroMutez)+import Morley.Tezos.Crypto (KeyHash)++----------------------------------------------------------------------------+-- Auxiliary types+----------------------------------------------------------------------------++-- | Data required for calling 'runCode'.+type RunCodeParameters :: T.T -> T.T -> T.T -> Type+data RunCodeParameters cp epArg st = RunCodeParameters+  { rcScript :: T.Contract cp st+    -- ^ Contract code to run+  , rcStorage :: T.Value st+    -- ^ Initial contract storage+  , rcInput :: T.Value epArg+    -- ^ Parameter to call the contract+  , rcEntryPoint :: T.EntrypointCallT cp epArg+    -- ^ Entrypoint to call. Use 'T.mkEntrypointCall' to construct.+  , rcAmount :: Mutez+    -- ^ Transfer amount+  , rcBalance :: Mutez+    -- ^ Contract initial balance+  , rcChainId :: ChainId+    -- ^ Chain id+  , rcNow :: Timestamp+    -- ^ The result of @NOW@ instruction+  , rcLevel :: Natural+    -- ^ The result of @LEVEL@ instruction+  , rcMinBlockTime :: Natural+    -- ^ The result of @MIN_BLOCK_TIME@ instruction+  , rcSource :: L1Address+    -- ^ Transfer source+  , rcSender :: L1Address+    -- ^ Transfer sender+  , rcKnownContracts :: Map ContractAddress ContractState+    -- ^ Known contracts and their state. If you only know parameter types and+    -- don't need to run contract's views, you can use 'dummyContractState' to+    -- construct the state.+  , rcSelf :: Maybe ContractAddress+    -- ^ Address returned by the @SELF@ instruction, will be auto-generated if+    -- 'Nothing'+  , rcDelegate :: Maybe KeyHash+    -- ^ Contract's delegate+  , rcVotingPowers :: VotingPowers+    -- ^ Voting powers+  }++-- | Construct 'RunCodeParameters' with some reasonable defaults.+--+-- Prepare untyped storage and parameter with 'resolveRunCodeBigMaps'.+--+-- Use 'T.mkEntrypointCall' or 'T.mkDefEntrypointCall' to construct the entrypoint+-- call specification.+runCodeParameters+  :: T.Contract cp st -- ^ Contract to run+  -> T.Value st -- ^ Contract storage+  -> T.EntrypointCallT cp epArg -- ^ Entrypoint call specification+  -> T.Value epArg -- ^ Entrypoint argument+  -> RunCodeParameters cp epArg st+runCodeParameters rcScript rcStorage rcEntryPoint rcInput = RunCodeParameters+  { rcAmount = zeroMutez+  , rcBalance = zeroMutez+  , rcChainId = dummyChainId+  , rcNow = dummyNow+  , rcLevel = dummyLevel+  , rcMinBlockTime = dummyMinBlockTime+  , rcSource = Constrained genesisAddress+  , rcSender = Constrained genesisAddress+  , rcKnownContracts = mempty+  , rcSelf = Nothing+  , rcDelegate = Nothing+  , rcVotingPowers = dummyVotingPowers+  , ..+  }++-- | Emulate @run_code@ RPC endpoint to an extent. Unlike @runContract@, runs+-- the contract through the emulator directly, without doing any operations.+-- This includes not doing the origination operation, and not applying the+-- operations produced by the transfer.+runCode+  :: RunCodeParameters cp epArg st+  -> Either (InterpretError Void) ([T.Operation], T.Value st)+runCode (RunCodeParameters+  -- NB: explicit match to ensure all fields are consumed; ugly, but there are no real alternatives+  rcScript@T.Contract{}+  rcStorage+  rcInput+  rcEntryPoint+  rcAmount+  rcBalance+  rcChainId+  rcNow+  rcLevel+  rcMinBlockTime+  rcSource+  rcSender+  rcKnownContracts+  rcSelf+  rcDelegate+  rcVotingPowers+  ) = toInterpreterRes $+    interpret rcScript rcEntryPoint input storage dummyGlobalCounter bigMapCtr contractEnv+  where+    selfState = ContractState+      { csBalance = rcBalance+      , csContract = rcScript+      , csStorage = rcStorage+      , csDelegate = rcDelegate+      }+    dummyOriginationHash = mkOriginationOperationHash $+      dummyOrigination rcStorage rcScript dummyGlobalCounter+    self = fromMaybe+      (mkContractAddress dummyOriginationHash dummyGlobalCounter)+      rcSelf+    ((input, storage), bigMapCtr) = usingState dummyBigMapCounter $+      (,) <$> assignBigMapIds False rcInput <*> assignBigMapIds False rcStorage+    toInterpreterRes (eith, (_, logs)) = first (InterpretError . (, logs)) eith+    contractEnv = ContractEnv+      { ceNow = rcNow+      , ceBalance = rcBalance+      , ceSelf = self+      , ceAmount = rcAmount+      , ceMinBlockTime = rcMinBlockTime+      , ceContracts = Map.insert self selfState rcKnownContracts+      , ceMaxSteps = dummyMaxSteps+      , ceSource = rcSource+      , ceSender = rcSender+      , ceChainId = rcChainId+      , ceOperationHash = Nothing+      , ceLevel = rcLevel+      , ceErrorSrcPos = def+      , ceVotingPowers = rcVotingPowers+      }++-- | Given an untyped value, possibly containing @big_map@ ids, typecheck it,+-- resolving ids to the corresponding @big_map@s.+--+-- 'BigMapFinder' can be constructed using 'Morley.Michelson.Runtime.mkBigMapFinder'.+resolveRunCodeBigMaps+  :: T.SingI t => BigMapFinder -> U.Value -> Either TcError (T.Value t)+resolveRunCodeBigMaps = typeCheckingWith def{tcStrict=False} ... typeCheckValueRunCodeCompat

@@ -8,7 +8,7 @@ -- -- When writting a Michelson contract, you can only mention characters with -- codes from @[32 .. 126]@ range in string literals. Same restriction applies--- to string literals passed to @tezos-client@.+-- to string literals passed to @octez-client@. -- -- However, Michelson allows some control sequences: @"\n"@. You have to write -- it exactly in this form, and internally it will be transformed to line feed@@ -42,6 +42,7 @@ import Fmt (Buildable) import Language.Haskell.TH qualified as TH import Language.Haskell.TH.Quote qualified as TH+import Type.Errors (DelayError)  import Morley.Util.CLI import Morley.Util.Label (Label(..), labelToText)@@ -174,11 +175,10 @@     [] -> Right []  -- | A type error asking to use 'MText' instead of t'Text'.-type family DoNotUseTextError where-  DoNotUseTextError = TypeError-    ( 'Text "`Text` is not isomorphic to Michelson strings," ':$$:-      'Text "consider using `MText` type instead"-    )+type DoNotUseTextError = DelayError+  ( 'Text "`Text` is not isomorphic to Michelson strings," ':$$:+    'Text "consider using `MText` type instead"+  )  -- | Create a 'MText' from type-level string. --

@@ -13,6 +13,7 @@   , typeCheckTopLevelType   , typeCheckValue   , typeCheckValueRunCodeCompat+  , typeCheckExpandedOp   , typeVerifyContract   , typeVerifyParameter   , typeVerifyStorage

@@ -6,8 +6,9 @@ module Morley.Michelson.TypeCheck.Error   ( TypeContext (..)   , TopLevelType (..)-  , TCTypeError (..)-  , TCError (..)+  , TcTypeError (..)+  , TcError+  , TcError' (..)   , ExtError (..)   , StackSize (..)   , pairWithNodeIndex@@ -35,7 +36,7 @@ -- | Contexts where type error can occur. data TypeContext   = LambdaArgument-  | LambdaCode+  | LambdaCodeCtx   | DipCode   | ConsArgument   | ComparisonArguments@@ -61,7 +62,7 @@ instance RenderDoc TypeContext where   renderDoc _ = \case     LambdaArgument -> "argument to some lambda"-    LambdaCode -> "code in LAMBDA"+    LambdaCodeCtx -> "code in LAMBDA"     DipCode -> "code in DIP"     ConsArgument -> "argument to CONS"     ComparisonArguments -> "arguments to comparison function"@@ -102,8 +103,8 @@ -- | Data type that represents various errors -- which are related to type system. -- These errors are used to specify info about type check errors--- in @TCError@ data type.-data TCTypeError+-- in @TcError@ data type.+data TcTypeError   = TypeEqError (MismatchError T.T)   -- ^ Type equality error   | StackEqError (MismatchError [T.T])@@ -123,10 +124,14 @@   | UnexpectedTopLevelType TopLevelType (MismatchError T.T)   -- ^ Error that happens when the caller expected one top-level type, but   -- the contract has another type specified.-  | InvalidInstruction U.ExpandedInstr Text+  | InvalidInstruction (U.InstrAbstract ()) Text   -- ^ Some instruction is invalid or used in an invalid way.   -- For example, @PAIR 0@ or @PAIR 1@, or a @SELF@ instruction was used in a @LAMBDA@.+  --   -- The 'Text' argument is a user-readable explanation of why this instruction is invalid.+  --+  -- Since this makes sense only for primitive instructions, we keep+  -- @U.InstrAbstract@ with @()@ type argument.   | InvalidValueType T.T   -- ^ Error that happens when a `U.Value` is never a valid source for this type   -- (e.g. @timestamp@ cannot be obtained from a `U.ValueTrue`)@@ -172,10 +177,10 @@   deriving stock (Show, Eq, Generic)   deriving anyclass (NFData) -instance Buildable TCTypeError where+instance Buildable TcTypeError where   build = buildRenderDocExtended -instance RenderDoc TCTypeError where+instance RenderDoc TcTypeError where   renderDoc context = \case     TypeEqError merr ->       "Types not equal:" <$> renderDoc context merr@@ -197,7 +202,7 @@       "Unexpected" <+> renderDoc context tyDesc <+> "type."       <$$> renderDoc doesntNeedParens mmerr     InvalidInstruction instr reason ->-      "Invalid instruction" <+> (renderDoc context instr)+      "Invalid instruction" <+> (renderDoc context (instr $> ("..." :: Text)))       <$$> "Reason:" <+> textStrict reason     InvalidValueType t ->       "Value type is never a valid" <+> enclose "`" "`" (renderDoc context t)@@ -227,65 +232,72 @@       "A big_map with the ID" <+> renderAnyBuildable bigMapId <+> "was found, but it does not have the expected type."       <$$> renderDoc context mismatchError +instance Exception TcTypeError+ -- | Type check error-data TCError-  = TCFailedOnInstr U.ExpandedInstr SomeHST ErrorSrcPos (Maybe TypeContext) (Maybe TCTypeError)-  | TCFailedOnValue U.Value T.T Text ErrorSrcPos (Maybe TCTypeError)-  | TCContractError Text (Maybe TCTypeError)-  | TCViewError Text U.ViewName (Maybe TCTypeError)-  | TCUnreachableCode ErrorSrcPos (NonEmpty U.ExpandedOp)-  | TCExtError SomeHST ErrorSrcPos ExtError-  | TCIncompletelyTyped TCError (U.Contract' TypeCheckedOp)-  | TCIncompletelyTypedView TCError (U.View' TypeCheckedOp)+data TcError' op+  = TcFailedOnInstr (U.InstrAbstract op) SomeHST ErrorSrcPos (Maybe TypeContext) (Maybe TcTypeError)+  | TcFailedOnValue (U.Value' op) T.T Text ErrorSrcPos (Maybe TcTypeError)+  | TcContractError Text (Maybe TcTypeError)+  | TcViewError Text U.ViewName (Maybe TcTypeError)+  | TcUnreachableCode ErrorSrcPos (NonEmpty op)+  | TcExtError SomeHST ErrorSrcPos ExtError+  | TcIncompletelyTyped (TcError' op) (U.Contract' (TypeCheckedOp op))+  | TcIncompletelyTypedView (TcError' op) (U.View' (TypeCheckedOp op))+  | TcDeprecatedType Text T.T   deriving stock (Show, Eq, Generic) -instance NFData TCError+type TcError = TcError' U.ExpandedOp -instance Buildable TCError where+instance (NFData op, NFData (TypeCheckedOp op)) => NFData (TcError' op)++instance RenderDoc op => Buildable (TcError' op) where   build = buildRenderDocExtended -instance RenderDoc TCError where+instance RenderDoc op => RenderDoc (TcError' op) where   renderDoc context = \case-    TCFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTCTypeError -> line+    TcFailedOnInstr instr (SomeHST t) ics mbTCTypeContext mbTcTypeError -> line       <> "Error checking expression:"       <> surroundWithNewLines (renderDoc context instr)       <> "against input stack type:"       <> surroundWithNewLines (renderDoc context t)       <> maybe "" (\c -> "Error in" <+> renderDoc context c) mbTCTypeContext-      <> maybe "" (\e -> ":" <+> (renderDoc context e) <> "." <$$> line) mbTCTypeError+      <> maybe "" (\e -> ":" <+> (renderDoc context e) <> "." <$$> line) mbTcTypeError       <> (renderDoc context ics)-    TCFailedOnValue v t custom ics mbTCTypeError ->+    TcFailedOnValue v t custom ics mbTcTypeError ->       "Error checking value"       <$$> (renderDoc context v) <+> "against type"       <+> (renderDoc context t) <> (bool (":" <+> (renderAnyBuildable custom)) "." (null custom))-      <+> (maybe "" (\e -> line <> (renderDoc context e) <> line) mbTCTypeError)+      <+> (maybe "" (\e -> line <> (renderDoc context e) <> line) mbTcTypeError)       <+> (renderDoc context ics)-    TCContractError msg typeError ->+    TcContractError msg typeError ->       "Error occurred during contract typecheck:"       <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)-    TCViewError msg viewName typeError ->+    TcViewError msg viewName typeError ->       "Error occurred during typecheck of view " <> renderDoc context viewName <> ":"       <$$> (renderAnyBuildable msg) <> (maybe "" (\e -> " " <> (renderDoc context e)) typeError)-    TCUnreachableCode ics instrs ->+    TcUnreachableCode ics instrs ->       "Unreachable code:" <$$> buildTruncated 3 (toList instrs) <> "."       <+> (renderDoc context ics)-    TCExtError (SomeHST t) ics e ->+    TcExtError (SomeHST t) ics e ->       "Error occurred during Morley extension typecheck:" <>       (renderAnyBuildable e) <+> "on stack" <+> (renderDoc context t) <> "."       <+> (renderDoc context ics)-    TCIncompletelyTyped err contract ->+    TcIncompletelyTyped err contract ->       line       <> renderDoc doesntNeedParens contract       <$> renderDoc context err-    TCIncompletelyTypedView err _view ->+    TcIncompletelyTypedView err _view ->       line       <> renderDoc context err+    TcDeprecatedType err ty ->+      "Found deprecated type:" <+> renderDoc doesntNeedParens ty <$> renderDoc doesntNeedParens err     where     buildTruncated k l       | null (drop k l) = renderDocList context l       | otherwise = (renderDocList context (take k l)) <> " ..." -    -- | Helper to format a line using empty lines at the end and at the beginning,+    -- Helper to format a line using empty lines at the end and at the beginning,     -- and 4-space indents for the line itself     surroundWithNewLines :: Doc -> Doc     surroundWithNewLines l =@@ -293,7 +305,7 @@       <$$> indent 4 l       <$$> line -instance Exception TCError where+instance Exception TcError where   displayException = pretty  newtype StackSize = StackSize Natural@@ -307,8 +319,8 @@ -- | Various type errors possible when checking Morley extension commands data ExtError =     LengthMismatch U.StackTypePattern-  | TypeMismatch U.StackTypePattern Int TCTypeError-  | StkRestMismatch U.StackTypePattern SomeHST SomeHST TCTypeError+  | TypeMismatch U.StackTypePattern Int TcTypeError+  | StkRestMismatch U.StackTypePattern SomeHST SomeHST TcTypeError   | TestAssertError Text   | InvalidStackReference U.StackRef StackSize   deriving stock (Show, Eq, Generic)@@ -358,7 +370,7 @@   0 -> "'a"   ix -> pairWithElems (minPairLength ix)   where-    -- | Given a node index @ix@, calculates the minimum number of+    -- Given a node index @ix@, calculates the minimum number of     -- elements a pair must have for that index to be valid.     minPairLength :: Word -> Word     minPairLength = \case

@@ -27,22 +27,24 @@ -- | Perform some, possibly throwing, action presumably making use of a supplied -- external instruction. In case of an error, return @IllTypedSeq@ wrapping the -- thrown error and the instruction. If the action successfully returns--- @SomeInstr@, wrap it in a @WellTypedSeq@.+-- @SomeTcInstr@, wrap it in a @WellTypedSeq@. workOnInstr-  :: U.ExpandedExtInstr-  -> TypeCheckInstr (SomeInstr s)-  -> TypeCheckInstrNoExcept (TypeCheckedSeq s)+  :: IsInstrOp op+  => U.ExtInstrAbstract op+  -> TypeCheckInstr op (SomeTcInstr s)+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op s) workOnInstr ext = tcEither-  (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx $ U.EXT ext])+  (\err -> pure $ IllTypedSeq err [NonTypedInstr $ liftInstr $ U.EXT ext])   (pure . WellTypedSeq)  typeCheckExt-  :: forall s. SingI s-  => TcInstrHandler-  -> U.ExpandedExtInstr+  :: forall s op.+     (SingI s, IsInstrOp op)+  => TcInstrBase op+  -> U.ExtInstrAbstract op   -> HST s-  -> TypeCheckInstrNoExcept (TypeCheckedSeq s)-typeCheckExt tcInstr ext hst = do+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)+typeCheckExt tcOp ext hst = do   instrPos <- view tcieErrorPos   case ext of     U.STACKTYPE s -> workOnInstr ext $@@ -51,24 +53,24 @@       verifyPrint pc <&> \tpc -> toSomeInstr (T.PRINT tpc)     U.UTEST_ASSERT U.TestAssert{..} -> do       let cons = U.EXT . U.UTEST_ASSERT . U.TestAssert tassName tassComment-      preserving (typeCheckImpl tcInstr tassInstrs hst) cons $ \(_ :/ si) -> case si of-        AnyOutInstr _ -> throwError $ TCExtError (SomeHST hst) instrPos $ TestAssertError+      preserving (typeCheckImpl tcOp tassInstrs hst) cons $ \(_ :/ si) -> case si of+        AnyOutInstr _ -> throwError $ TcExtError (SomeHST hst) instrPos $ TestAssertError                          "TEST_ASSERT has to return Bool, but it always fails"         instr ::: (((_ :: (T.SingT b, Dict (T.WellTyped b))) ::& _)) -> do           Refl <- liftEither $ first-            (const $ TCExtError (SomeHST hst) instrPos $+            (const $ TcExtError (SomeHST hst) instrPos $               TestAssertError "TEST_ASSERT has to return Bool, but returned something else")             (eqType @b @'T.TBool)           tcom <- verifyPrint tassComment           pure . toSomeInstr $ T.TEST_ASSERT $ T.TestAssert tassName tcom instr         _ ->-          throwError $ TCExtError (SomeHST hst) instrPos $+          throwError $ TcExtError (SomeHST hst) instrPos $             TestAssertError "TEST_ASSERT has to return Bool, but the stack is empty"      U.UCOMMENT t ->       pure $ WellTypedSeq $ toSomeInstr $ T.COMMENT_ITEM $ T.JustComment t   where-    verifyPrint :: U.PrintComment -> TypeCheckInstr (T.PrintComment s)+    verifyPrint :: U.PrintComment -> TypeCheckInstr op (T.PrintComment s)     verifyPrint (U.PrintComment pc) = do       let checkStRef (Left txt)             = pure $ Left txt           checkStRef (Right (U.StackRef i)) = Right <$> createStackRef i hst@@ -77,10 +79,10 @@     toSomeInstr ext' = hst :/ T.Ext ext' ::: hst     stackTypeSomeInstr s = hst :/ T.Ext (T.STACKTYPE s) ::: hst -liftExtError :: SingI s => HST s -> Either ExtError a -> TypeCheckInstr a+liftExtError :: SingI s => HST s -> Either ExtError a -> TypeCheckInstr op a liftExtError hst ei = do   instrPos <- view tcieErrorPos-  liftEither $ first (TCExtError (SomeHST hst) instrPos) ei+  liftEither $ first (TcExtError (SomeHST hst) instrPos) ei  -- | Check that a @StackTypePattern@ matches the type of the current stack checkStackType@@ -122,7 +124,7 @@ -- -- Fails when index is too large for the given stack. createStackRef-  :: (MonadError TCError m, MonadReader TypeCheckInstrEnv m, SingI s)+  :: (MonadError (TcError' op) m, MonadReader TypeCheckInstrEnv m, SingI s)   => Natural -> HST s -> m (T.StackRef s) createStackRef idx hst =   case doCreate (hst, idx) of@@ -130,7 +132,7 @@     Nothing -> do       instrPos <- view tcieErrorPos       throwError $-        TCExtError (SomeHST hst) instrPos $+        TcExtError (SomeHST hst) instrPos $           InvalidStackReference (U.StackRef idx) (StackSize $ lengthHST hst)   where     doCreate :: forall s. (HST s, Natural) -> Maybe (T.StackRef s)

@@ -16,6 +16,8 @@     , typeCheckInstrErr'     , typeCheckImpl     , typeCheckImplStripped+    , mapSeq+    , wrapWithLoc      , memImpl     , getImpl@@ -40,12 +42,13 @@ import Control.Monad.Except (MonadError, catchError, throwError) import Data.Constraint (Dict(..), withDict) import Data.Default (def)+import Data.Generics (listify) import Data.Singletons (Sing, SingI(sing), demote, fromSing) import Data.Singletons.Decide ((:~:)(Refl)) import Fmt (Buildable, (+|), (|+))  import Morley.Michelson.ErrorPos (ErrorSrcPos)-import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..), TypeContext(..))+import Morley.Michelson.TypeCheck.Error (TcError'(..), TcTypeError(..), TypeContext(..)) import Morley.Michelson.TypeCheck.TypeCheck import Morley.Michelson.TypeCheck.TypeCheckedSeq (IllTypedInstr(..), TypeCheckedSeq(..)) import Morley.Michelson.TypeCheck.Types@@ -70,7 +73,7 @@ -- | Check whether the given stack types are equal. eqHST   :: forall as bs. (SingI as, SingI bs)-  => HST as -> HST bs -> Either TCTypeError (as :~: bs)+  => HST as -> HST bs -> Either TcTypeError (as :~: bs) eqHST (hst :: HST xs) (hst' :: HST ys) = do   case eqI @as @bs of     Nothing -> Left $ StackEqError MkMismatchError {meActual = hstToTs hst, meExpected = hstToTs hst'}@@ -80,7 +83,7 @@ -- given type. This function is a specialized version of `eqHST`. eqHST1   :: forall t st. (SingI st, WellTyped t)-  => HST st -> Either TCTypeError (st :~: '[t])+  => HST st -> Either TcTypeError (st :~: '[t]) eqHST1 hst = do   let hst' = sing @t -:& SNil   case eqI @'[t] @st of@@ -110,52 +113,52 @@ handleError = flip catchError  -- | Function @eqType@ is a simple wrapper around @Data.Singletons.decideEquality@ suited--- for use within @Either TCTypeError a@ applicative.+-- for use within @Either TcTypeError a@ applicative. eqType   :: forall (a :: T) (b :: T). (Each '[SingI] [a, b])-  => Either TCTypeError (a :~: b)+  => Either TcTypeError (a :~: b) eqType =   requireEq @a @b $ Left ... TypeEqError  onTypeCheckInstrErr-  :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)-  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext-  -> Either TCTypeError a -> m a+  :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)+  => Un.InstrAbstract op -> SomeHST -> Maybe TypeContext+  -> Either TcTypeError a -> m a onTypeCheckInstrErr instr hst mContext ei = do   either (typeCheckInstrErr' instr hst mContext) return ei  onScopeCheckInstrErr-  :: forall (t :: T) m a.-      (MonadReader TypeCheckInstrEnv m, MonadError TCError m, SingI t)-  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext+  :: forall (t :: T) op m a.+      (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m, SingI t)+  => Un.InstrAbstract op -> SomeHST -> Maybe TypeContext   -> Either BadTypeForScope a -> m a onScopeCheckInstrErr instr hst mContext = \case   Right a -> return a   Left e -> do     pos <- view tcieErrorPos-    throwError $ TCFailedOnInstr instr hst pos mContext $+    throwError $ TcFailedOnInstr instr hst pos mContext $       Just $ UnsupportedTypeForScope (demote @t) e  typeCheckInstrErr-  :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)-  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext+  :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)+  => Un.InstrAbstract op -> SomeHST -> Maybe TypeContext   -> m a typeCheckInstrErr instr hst mContext = do   pos <- view tcieErrorPos-  throwError $ TCFailedOnInstr instr hst pos mContext Nothing+  throwError $ TcFailedOnInstr instr hst pos mContext Nothing  typeCheckInstrErr'-  :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m)-  => Un.ExpandedInstr -> SomeHST -> Maybe TypeContext-  -> TCTypeError -> m a+  :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)+  => Un.InstrAbstract op -> SomeHST -> Maybe TypeContext+  -> TcTypeError -> m a typeCheckInstrErr' instr hst mContext err = do   pos <- view tcieErrorPos-  throwError $ TCFailedOnInstr instr hst pos mContext (Just err)+  throwError $ TcFailedOnInstr instr hst pos mContext (Just err)  withCompareableCheck-  :: forall a m v ts. (SingI ts, MonadReader TypeCheckInstrEnv m, MonadError TCError m)+  :: forall a m v ts op. (SingI ts, MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m)   => Sing a-  -> Un.ExpandedInstr+  -> Un.InstrAbstract op   -> HST ts   -> (Comparable a => v)   -> m v@@ -163,68 +166,38 @@   Just d@Dict -> pure $ withDict d act   Nothing -> typeCheckInstrErr instr (SomeHST i) $ Just ComparisonArguments -typeCheckOpImpl-  :: forall inp. SingI inp-  => TcInstrHandler-  -> Un.ExpandedOp-  -> HST inp-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-typeCheckOpImpl tcInstr op' hst = case op' of-  Un.WithSrcEx _ op@Un.WithSrcEx{} -> typeCheckOpImpl tcInstr op hst-  Un.WithSrcEx loc (Un.PrimEx op)  -> typeCheckPrimWithLoc loc op-  Un.WithSrcEx loc (Un.SeqEx sq)   -> typeCheckSeqWithLoc loc sq-  Un.PrimEx op                     -> typeCheckPrim op-  Un.SeqEx sq                      -> typeCheckSeq sq-  where-    -- If we know source location from the untyped instruction, keep it in the typed one.-    typeCheckPrimWithLoc :: ErrorSrcPos -> Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-    typeCheckPrimWithLoc loc op = local (set tcieErrorPos loc)-      (wrapWithLoc loc <$> typeCheckPrim op)--    typeCheckPrim :: Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-    typeCheckPrim op = tcInstr op hst--    typeCheckSeqWithLoc :: ErrorSrcPos -> [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-    typeCheckSeqWithLoc loc = fmap (wrapWithLoc loc) . local (set tcieErrorPos loc) . typeCheckSeq--    typeCheckSeq :: [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-    typeCheckSeq sq = typeCheckImpl tcInstr sq hst-                  <&> mapSeq (mapSomeInstr Nested)- -- | Like 'typeCheckImpl' but doesn't add a stack type comment after the -- sequence. typeCheckImplNoLastTypeComment-  :: forall inp . SingI inp-  => TcInstrHandler-  -> [Un.ExpandedOp]-  -> HST inp-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+  :: IsInstrOp op+  => TcInstrBase op+  -> TcInstr op [op] typeCheckImplNoLastTypeComment _ [] inputStack   = pure (WellTypedSeq (inputStack :/ Nop ::: inputStack))-typeCheckImplNoLastTypeComment tcInstr [op] inputStack = do-  typeCheckOpImpl tcInstr op inputStack+typeCheckImplNoLastTypeComment tcOp [op] inputStack = do+  tcOp op inputStack       >>= mapMSeq prependStackTypeComment-typeCheckImplNoLastTypeComment tcInstr (op : ops) inputStack = do-  done <- typeCheckOpImpl tcInstr op inputStack+typeCheckImplNoLastTypeComment tcOp (op : ops) inputStack = do+  done <- tcOp op inputStack       >>= mapMSeq prependStackTypeComment-  continueTypeChecking tcInstr done ops+  continueTypeChecking tcOp done ops  continueTypeChecking-  :: forall inp. ()-  => TcInstrHandler-  -> TypeCheckedSeq inp-  -> [Un.ExpandedOp]-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-continueTypeChecking tcInstr done rest = case done of+  :: forall op inp. (IsInstrOp op)+  => TcInstrBase op+  -> TypeCheckedSeq op inp+  -> [op]+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)+continueTypeChecking tcOp done rest = case done of   WellTypedSeq instr -> handleFirst instr   MixedSeq i e left -> pure (MixedSeq i e (left <> map NonTypedInstr rest))   IllTypedSeq e left -> pure (IllTypedSeq e (left <> map NonTypedInstr rest))   where-    handleFirst :: SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+    handleFirst :: SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)     handleFirst packedInstr@(inputStack :/ instrAndOutputStack) = do       case instrAndOutputStack of         instr ::: outputStack -> do-          nextPiece <- typeCheckImplNoLastTypeComment tcInstr rest outputStack+          nextPiece <- typeCheckImplNoLastTypeComment tcOp rest outputStack           let combiner = combine inputStack instr           pure case nextPiece of             WellTypedSeq nextInstr -> WellTypedSeq (combiner nextInstr)@@ -234,39 +207,35 @@           [] -> WellTypedSeq packedInstr           op : ops -> (MixedSeq                         packedInstr-                        (TCUnreachableCode (extractOpPos op) (op :| ops))+                        (TcUnreachableCode (extractOpPos op) (op :| ops))                         (map NonTypedInstr ops))      combine inp Nop (_ :/ nextPart) = inp :/ nextPart     combine inp i1 (_ :/ nextPart) = inp :/ mapSomeInstrOut (Seq i1) nextPart -    extractOpPos :: Un.ExpandedOp -> ErrorSrcPos-    extractOpPos (Un.WithSrcEx loc _) = loc-    extractOpPos _ = def+    extractOpPos :: op -> ErrorSrcPos+    extractOpPos = fromMaybe def . pickErrorSrcPos  -- | Like 'typeCheckImpl' but without the first and the last stack type -- comments. Useful to reduce duplication of stack type comments. typeCheckImplStripped-  :: forall inp . SingI inp-  => TcInstrHandler-  -> [Un.ExpandedOp]-  -> HST inp-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-typeCheckImplStripped tcInstr [] inp-  = typeCheckImplNoLastTypeComment tcInstr [] inp-typeCheckImplStripped tcInstr (op : ops) inp = do-  done <- typeCheckOpImpl tcInstr op inp-  continueTypeChecking tcInstr done ops+  :: IsInstrOp op+  => TcInstrBase op+  -> TcInstr op [op]+typeCheckImplStripped tcOp [] inp+  = typeCheckImplNoLastTypeComment tcOp [] inp+typeCheckImplStripped tcOp (op : ops) inp = do+  done <- tcOp op inp+  continueTypeChecking tcOp done ops  typeCheckImpl-  :: forall inp . SingI inp-  => TcInstrHandler-  -> [Un.ExpandedOp]-  -> HST inp-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-typeCheckImpl tcInstr ops inputStack = do-  tcSeq <- typeCheckImplNoLastTypeComment tcInstr ops inputStack-  mapMSeq appendTypeComment tcSeq+  :: forall op. IsInstrOp op+  => TcInstrBase op+  -> TcInstr op [op]+typeCheckImpl tcOp ops inputStack = do+  checkBadTypes inputStack & tcEither+    (\err -> pure $ IllTypedSeq err $ NonTypedInstr <$> ops)+    (\_ -> typeCheckImplNoLastTypeComment tcOp ops inputStack >>= mapMSeq appendTypeComment)   where     appendTypeComment packedI@(inp :/ iAndOut) = do       verbose <- asks' tcVerbose@@ -274,17 +243,34 @@         (True, i ::: out) -> inp :/ Seq i (stackTypeComment out) ::: out         (True, AnyOutInstr i) -> inp :/ AnyOutInstr (Seq i noStackTypeComment)         _ -> packedI+    checkBadTypes :: HST a -> TypeCheckInstr op' ()+    checkBadTypes x = do+      isStrict <- asks' tcStrict+      when isStrict $ doCheckBadTypes x+    doCheckBadTypes :: HST a -> TypeCheckInstr op' ()+    doCheckBadTypes = \case+      SNil -> pure ()+      (_ :: Sing t, _) ::& _+        | ty : _ <- listify isTimeLockTy (demote @t) -> timelockDeprecated ty+      _ ::& xs -> doCheckBadTypes xs+    isTimeLockTy :: T -> Bool+    isTimeLockTy TChest = True+    isTimeLockTy TChestKey = True+    isTimeLockTy _ = False+    timelockDeprecated :: T -> TypeCheckInstr op' a+    timelockDeprecated = throwError . TcDeprecatedType+      "Timelock mechanism is affected by a vulnerability."   prependStackTypeComment-  :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)+  :: SomeTcInstr inp -> TypeCheckInstrNoExcept op (SomeTcInstr inp) prependStackTypeComment packedInstr@(inp :/ _) = do   verbose <- asks' tcVerbose   pure if verbose && (not (isNop' packedInstr))     then mapSomeInstr (Seq (stackTypeComment inp)) packedInstr     else packedInstr -isNop' :: SomeInstr inp -> Bool+isNop' :: SomeTcInstr inp -> Bool isNop' (_ :/ i ::: _) = isNop i isNop' (_ :/ AnyOutInstr i) = isNop i @@ -299,18 +285,18 @@  mapMSeq   :: Applicative f-  => (SomeInstr inp -> f (SomeInstr inp'))-  -> TypeCheckedSeq inp-  -> f (TypeCheckedSeq inp')+  => (SomeTcInstr inp -> f (SomeTcInstr inp'))+  -> TypeCheckedSeq op inp+  -> f (TypeCheckedSeq op inp') mapMSeq f v = case v of   WellTypedSeq instr -> f instr <&> WellTypedSeq   MixedSeq instr err tail' -> f instr <&> \instr' -> MixedSeq instr' err tail'   IllTypedSeq err tail' -> pure $ IllTypedSeq err tail'  mapSeq-  :: (SomeInstr inp -> SomeInstr inp')-  -> TypeCheckedSeq inp-  -> TypeCheckedSeq inp'+  :: (SomeTcInstr inp -> SomeTcInstr inp')+  -> TypeCheckedSeq op inp+  -> TypeCheckedSeq op inp' mapSeq f = runIdentity . mapMSeq (Identity . f)  stackTypeComment :: HST st -> Instr st st@@ -319,7 +305,7 @@ noStackTypeComment :: Instr st st noStackTypeComment = Ext (COMMENT_ITEM (StackTypeComment Nothing)) -wrapWithLoc :: ErrorSrcPos -> TypeCheckedSeq inp -> TypeCheckedSeq inp+wrapWithLoc :: ErrorSrcPos -> TypeCheckedSeq op inp -> TypeCheckedSeq op inp wrapWithLoc loc = mapSeq $ \someInstr -> case someInstr of   (_ :/ WithLoc{} ::: _) -> someInstr   (inp :/ instr ::: out) -> inp :/ WithLoc loc instr ::: out@@ -331,17 +317,17 @@  -- | Generic implementation for MEMeration memImpl-  :: forall c memKey rs inp m .+  :: forall c memKey rs inp m op .     ( MemOp c     , SingI (MemOpKey c)     , inp ~ (memKey : c : rs)     , SingI rs     , MonadReader TypeCheckInstrEnv m-    , MonadError TCError m+    , MonadError (TcError' op) m     )   => HST inp   -> VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) memImpl inputHST@(_ ::& _ ::& hstTail) varAnn =   case eqType @memKey @(MemOpKey c) of     Right Refl ->@@ -353,18 +339,18 @@     uInstr = Un.MEM varAnn  getImpl-  :: forall c getKey rs inp m .+  :: forall c getKey rs inp m op .     ( GetOp c, SingI (GetOpKey c)     , WellTyped (GetOpVal c)     , inp ~ (getKey : c : rs)     , SingI rs     , MonadReader TypeCheckInstrEnv m-    , MonadError TCError m+    , MonadError (TcError' op) m     )   => HST inp   -> SingT (GetOpVal c)   -> VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) getImpl inputHST@(_ ::& _ ::& hstTail) valueSing varAnn =   case eqType @getKey @(GetOpKey c) of     Right Refl ->@@ -376,17 +362,17 @@     uInstr = Un.GET varAnn  updImpl-  :: forall c updKey updParams rs inp m .+  :: forall c updKey updParams rs inp m op .     ( UpdOp c     , SingI (UpdOpKey c), SingI (UpdOpParams c)     , SingI rs     , inp ~ (updKey : updParams : c : rs)     , MonadReader TypeCheckInstrEnv m-    , MonadError TCError m+    , MonadError (TcError' op) m     )   => HST inp   -> VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) updImpl inputHST@(_ ::& _ ::& cTuple ::& hstTail) varAnn =   case (eqType @updKey @(UpdOpKey c), eqType @updParams @(UpdOpParams c)) of     (Right Refl, Right Refl) ->@@ -400,7 +386,7 @@     uInstr = Un.UPDATE varAnn  getUpdImpl-  :: forall c updKey updParams rs inp m .+  :: forall c updKey updParams rs inp m op .     ( UpdOp c, GetOp c     , SingI (UpdOpKey c)     , SingI (GetOpVal c)@@ -409,11 +395,11 @@     , GetOpKey c ~ UpdOpKey c     , UpdOpParams c ~ 'TOption (GetOpVal c)     , MonadReader TypeCheckInstrEnv m-    , MonadError TCError m+    , MonadError (TcError' op) m     )   => HST inp   -> VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) getUpdImpl inputHST@(_ ::& hst1 ::& cTuple ::& hstTail) varAnn =   case (eqType @updKey @(UpdOpKey c), eqType @updParams @(UpdOpParams c)) of     (Right Refl, Right Refl) ->@@ -430,7 +416,7 @@   :: (SizeOp c, inp ~ (c ': rs), Monad m)   => HST inp   -> VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) sizeImpl i@(_ ::& rs) vn =   pure $ i :/ AnnSIZE (Anns1 vn) ::: ((sing, Dict) ::& rs) @@ -438,7 +424,7 @@   :: (SliceOp c, inp ~ ('TNat ': 'TNat ': c ': rs), Monad m)   => HST inp   -> Un.VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) sliceImpl i@(_ ::& _ ::& (cn, Dict) ::& rs) vn = do   let rn = STOption cn   pure $ i :/ AnnSLICE (Anns1 vn) ::: ((rn, Dict) ::& rs)@@ -447,7 +433,7 @@   :: (ConcatOp c, WellTyped c, inp ~ ('TList c : rs), Monad m)   => HST inp   -> Un.VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) concatImpl' i@((STList n, Dict) ::& rs) vn = do   pure $ i :/ AnnCONCAT' (Anns1 vn) ::: ((n, Dict) ::& rs) @@ -458,14 +444,14 @@      )   => HST inp   -> Un.VarAnn-  -> m (SomeInstr inp)+  -> m (SomeTcInstr inp) concatImpl i@((cn1, _) ::& (_, _) ::& rs) vn = do   pure $ i :/ AnnCONCAT (Anns1 vn) ::: ((cn1, Dict) ::& rs)  -- | Helper function to construct instructions for binary arithmetic -- operations. arithImpl-  :: forall aop inp m n s t.+  :: forall aop inp m n s t op.      ( WellTyped (ArithRes aop n m)      , inp ~ (n ': m ': s)      , MonadReader TypeCheckInstrEnv t@@ -473,24 +459,24 @@   => (Anns '[VarAnn] -> Instr inp (ArithRes aop n m ': s))   -> HST inp   -> VarAnn-  -> Un.ExpandedInstr-  -> t (SomeInstr inp)+  -> Un.InstrAbstract op+  -> t (SomeTcInstr inp) arithImpl mkInstr i@(_ ::& _ ::& rs) vn _ =   pure $ i :/ mkInstr (Anns1 vn) ::: ((sing, Dict) ::& rs)  addImpl-  :: forall a b inp rs m.+  :: forall a b inp rs m op.      ( Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)      , SingI rs      , MonadReader TypeCheckInstrEnv m-     , MonadError TCError m+     , MonadError (TcError' op) m      )   => Sing a -> Sing b   -> HST inp   -> VarAnn-  -> Un.ExpandedInstr-  -> m (SomeInstr inp)+  -> Un.InstrAbstract op+  -> m (SomeTcInstr inp) addImpl t1 t2 = case (t1, t2) of   (STInt, STInt) -> arithImpl @Add AnnADD   (STInt, STNat) -> arithImpl @Add AnnADD@@ -506,18 +492,18 @@     NotNumericTypes (demote @a) (demote @b)  edivImpl-  :: forall a b inp rs m.+  :: forall a b inp rs m op.      ( SingI rs      , Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)      , MonadReader TypeCheckInstrEnv m-     , MonadError TCError m+     , MonadError (TcError' op) m      )   => Sing a -> Sing b   -> HST inp   -> VarAnn-  -> Un.ExpandedInstr-  -> m (SomeInstr inp)+  -> Un.InstrAbstract op+  -> m (SomeTcInstr inp) edivImpl t1 t2 = case (t1, t2) of   (STInt, STInt) -> edivImplDo   (STInt, STNat) -> edivImplDo@@ -538,24 +524,24 @@      )   => HST inp   -> VarAnn-  -> Un.ExpandedInstr-  -> t (SomeInstr inp)+  -> Un.InstrAbstract op+  -> t (SomeTcInstr inp) edivImplDo i@(_ ::& _ ::& rs) vn _ =   pure $ i :/ AnnEDIV (Anns1 vn) ::: ((sing, Dict) ::& rs)  subImpl-  :: forall a b inp rs m.+  :: forall a b inp rs m op.      ( Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)      , SingI rs      , MonadReader TypeCheckInstrEnv m-     , MonadError TCError m+     , MonadError (TcError' op) m      )   => Sing a -> Sing b   -> HST inp   -> VarAnn-  -> Un.ExpandedInstr-  -> m (SomeInstr inp)+  -> Un.InstrAbstract op+  -> m (SomeTcInstr inp) subImpl t1 t2 = case (t1, t2) of   (STInt, STInt) -> arithImpl @Sub AnnSUB   (STInt, STNat) -> arithImpl @Sub AnnSUB@@ -563,24 +549,24 @@   (STNat, STNat) -> arithImpl @Sub AnnSUB   (STTimestamp, STTimestamp) -> arithImpl @Sub AnnSUB   (STMutez, STMutez) -> \i _ uInstr -> typeCheckInstrErr' uInstr (SomeHST i) (Just ArithmeticOperation) $-    InvalidInstruction uInstr "Use of SUB on `mutez` operands is deprecated; use SUB_MUTEZ"+    InvalidInstruction (uInstr $> ()) "Use of SUB on `mutez` operands is deprecated; use SUB_MUTEZ"   (STTimestamp, STInt) -> arithImpl @Sub AnnSUB   _ -> \i _ uInstr -> typeCheckInstrErr' uInstr (SomeHST i) (Just ArithmeticOperation) $     NotNumericTypes (demote @a) (demote @b)  mulImpl-  :: forall a b inp rs m.+  :: forall a b inp rs m op.      ( Each '[SingI] [a, b]      , inp ~ (a ': b ': rs)      , SingI rs      , MonadReader TypeCheckInstrEnv m-     , MonadError TCError m+     , MonadError (TcError' op) m      )   => Sing a -> Sing b   -> HST inp   -> VarAnn-  -> Un.ExpandedInstr-  -> m (SomeInstr inp)+  -> Un.InstrAbstract op+  -> m (SomeTcInstr inp) mulImpl t1 t2 = case (t1, t2) of   (STInt, STInt) -> arithImpl @Mul AnnMUL   (STInt, STNat) -> arithImpl @Mul AnnMUL@@ -607,7 +593,7 @@      )   => Instr inp (UnaryArithRes aop n ': s)   -> HST inp-  -> t (SomeInstr inp)+  -> t (SomeTcInstr inp) unaryArithImpl mkInstr i@(_ ::& rs) = do   pure $ i :/ mkInstr ::: ((sing, Dict) ::& rs) @@ -621,6 +607,6 @@      )   => Instr inp (UnaryArithRes aop n ': s)   -> HST inp-  -> t (SomeInstr inp)+  -> t (SomeTcInstr inp) unaryArithImplAnnotated mkInstr i@((n, _) ::& rs) = do   pure $ i :/ mkInstr ::: ((n, Dict) ::& rs)

@@ -18,18 +18,20 @@ -- -- Function @typeCheck@ takes list of instructions and returns value of type -- @Instr inp out@ along with @HST inp@ and @HST out@ all wrapped into--- @SomeInstr@ data type. This wrapping is done to satisfy Haskell type+-- @SomeTcInstr@ data type. This wrapping is done to satisfy Haskell type -- system (which has no support for dependent types). -- Functions @typeCheckInstr@, @typeCheckValue@ behave similarly. -- -- When a recursive call is made within @typeCheck@, @typeCheckInstr@ or--- @typeCheckValue@, result of a call is unwrapped from @SomeInstr@ and type+-- @typeCheckValue@, result of a call is unwrapped from @SomeTcInstr@ and type -- information from @HST inp@ and @HST out@ is being used to assert that -- recursive call returned instruction of expected type -- (error is thrown otherwise). module Morley.Michelson.TypeCheck.Instr     ( typeCheckContract+    , typeCheckContract'     , typeCheckContractAndStorage+    , typeCheckContractAndStorage'     , typeCheckInstr     , typeCheckList     , tcList@@ -37,13 +39,20 @@     , typeCheckParameter     , typeCheckStorage     , typeCheckTopLevelType+    , typeCheckTopLevelType'+    , typeCheckViews+    , typeCheckView'+    , typeCheckViews'     , typeCheckValue     , typeCheckValueRunCodeCompat+    , typeCheckExpandedOp     , typeVerifyContract+    , typeVerifyContract'     , typeVerifyParameter     , typeVerifyStorage     , typeVerifyTopLevelType     , typeVerifyView+    , typeVerifyView'     ) where  import Prelude hiding (EQ, GT, LT)@@ -54,11 +63,12 @@ import Data.Generics (everything, mkQ) import Data.Sequence ((|>)) import Data.Sequence qualified as Seq-import Data.Singletons (Sing, SomeSing(..), demote, withSingI, withSomeSing)+import Data.Singletons (Sing, SomeSing(..), demote, withSingI) import Data.Type.Equality (TestEquality(..)) import Data.Typeable ((:~:)(..)) import Fmt (pretty) +import Morley.Michelson.ErrorPos (ErrorSrcPos) import Morley.Michelson.TypeCheck.Error import Morley.Michelson.TypeCheck.Ext import Morley.Michelson.TypeCheck.Helpers@@ -84,66 +94,87 @@ -- | Type check a contract and verify that the given storage -- is of the type expected by the contract. typeCheckContractAndStorage-  :: U.Contract -> U.Value -> TypeCheckResult SomeContractAndStorage-typeCheckContractAndStorage uContract uStorage = do-  SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract uContract-  storage <- typeVerifyStorage @st uStorage+  :: U.Contract -> U.Value -> TypeCheckResult U.ExpandedOp SomeContractAndStorage+typeCheckContractAndStorage = typeCheckContractAndStorage' typeCheckExpandedOp++typeCheckContractAndStorage'+  :: IsInstrOp op+  => TcInstrBase op -> U.Contract' op -> U.Value' op -> TypeCheckResult op SomeContractAndStorage+typeCheckContractAndStorage' tcOp uContract uStorage = do+  SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract' tcOp uContract+  storage <- typeVerifyStorage' @st tcOp uStorage   pure $ SomeContractAndStorage contract storage  typeCheckContract   :: U.Contract-  -> TypeCheckResult SomeContract-typeCheckContract c = do-  paramType <- liftEither $ mkSomeParamType (U.contractParameter c)-  runTypeCheck (TypeCheckContract paramType) $ typeCheckContractImpl c+  -> TypeCheckResult U.ExpandedOp SomeContract+typeCheckContract = typeCheckContract' typeCheckExpandedOp +typeCheckContract'+  :: IsInstrOp op+  => TcInstrBase op+  -> U.Contract' op+  -> TypeCheckResult op SomeContract+typeCheckContract' tcOp c = do+  paramType <- liftEither $ first (TcContractError "illegal parameter declaration: " . Just ) $+    mkSomeParamType (U.contractParameter c)+  runTypeCheck (TypeCheckContract paramType) $ doTypeCheckContract' tcOp c+ typeVerifyContract   :: forall cp st.      (SingI cp, SingI st)-  => U.Contract -> TypeCheckResult (Contract cp st)-typeVerifyContract uContract = do+  => U.Contract -> TypeCheckResult U.ExpandedOp (Contract cp st)+typeVerifyContract = typeVerifyContract' typeCheckExpandedOp++typeVerifyContract'+  :: forall cp st op.+     (SingI cp, SingI st, IsInstrOp op)+  => TcInstrBase op -> U.Contract' op -> TypeCheckResult op (Contract cp st)+typeVerifyContract' tcOp uContract = do   SomeContract tContract@(Contract{} :: Contract cp' st') <--    typeCheckContract uContract+    typeCheckContract' tcOp uContract   Refl <- requireEq @cp' @cp (mkErr TltParameterType)   Refl <- requireEq @st' @st (mkErr TltStorageType)   return tContract   where-    mkErr :: TopLevelType -> MismatchError T -> TypeCheckResult any+    mkErr :: TopLevelType -> MismatchError T -> TypeCheckResult op any     mkErr tyDesc merr =-      throwError $ TCContractError "error in contract type" $ Just $+      throwError $ TcContractError "error in contract type" $ Just $           UnexpectedTopLevelType tyDesc merr -withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a+withWTP :: forall t a op. SingI t => (WellTyped t => TypeCheck op a) -> TypeCheck op a withWTP fn = case getWTP @t of   Right Dict -> fn-  Left err -> throwError $ TCContractError (pretty err) Nothing+  Left err -> throwError $ TcContractError (pretty err) Nothing -withWTPInstr_ :: forall t a. SingI t => U.ExpandedInstr -> SomeHST -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a+withWTPInstr_ :: forall t op a. SingI t => U.InstrAbstract op -> SomeHST -> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a withWTPInstr_ v t fn = case getWTP @t of   Right Dict -> fn   Left (NotWellTyped badType cause) -> do     loc <- view tcieErrorPos-    throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType cause)+    throwError $ TcFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType cause)  withWTPInstr'_-  :: forall t inp. SingI t-  => U.ExpandedInstr+  :: forall t op inp. (SingI t, IsInstrOp op)+  => U.InstrAbstract op   -> SomeHST-  -> (WellTyped t => TypeCheckInstrNoExcept (TypeCheckedSeq inp))-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+  -> (WellTyped t => TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) withWTPInstr'_ v t fn = case getWTP @t of   Right Dict -> fn   Left (NotWellTyped badType cause) -> do     loc <- view tcieErrorPos-    let err = TCFailedOnInstr v t loc Nothing+    let err = TcFailedOnInstr v t loc Nothing               (Just $ UnsupportedTypeForScope badType cause)-    pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx v]+    pure $ IllTypedSeq err [NonTypedInstr $ liftInstr v] -typeCheckContractImpl-  :: U.Contract-  -> TypeCheck SomeContract-typeCheckContractImpl uContract@(U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder uViews) = do-  _ <- maybe (throwError $ TCContractError "no instructions in contract code" $ Just EmptyCode)+doTypeCheckContract'+  :: IsInstrOp op+  => TcInstrBase op+  -> U.Contract' op+  -> TypeCheck op SomeContract+doTypeCheckContract' tcOp uContract@(U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder uViews) = do+  _ <- maybe (throwError $ TcContractError "no instructions in contract code" $ Just EmptyCode)                 pure (nonEmpty pCode)   withUType mParam $ \(paramNote :: Notes param) ->     withUType mStorage $ \(storageNote :: Notes st) -> do@@ -160,14 +191,14 @@             usingReaderT def $             liftNoExcept $             typeCheckImpl-              (giveNotInView $ local (set tcieNotInView $ Just Dict) ... typeCheckInstr)+              (giveNotInView $ local (set tcieNotInView $ Just Dict) ... tcOp)               pCode               inp           instr@(_ :/ instrOut) <-             tcsEither onFailedCodeTypeCheck pure codeRes            -- typecheck views-          views <- typeCheckViewsImpl+          views <- typeCheckViews' tcOp             uContract{ U.contractCode = [someInstrToOp instr], U.contractViews = [] }             storageNote uViews @@ -177,31 +208,31 @@             cParamNotes <-               liftEither $               mkParamNotes paramNote rootAnn `onFirst`-                  (TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)+                  (TcContractError "invalid parameter declaration: " . Just . IllegalParamDecl)             let cEntriesOrder = entriesOrder             cViews <- liftEither $-              mkViewsSet views `onFirst` \e -> TCContractError (pretty e) Nothing+              mkViewsSet views `onFirst` \e -> TcContractError (pretty e) Nothing             case instrOut of               instr' ::: out -> liftEither $ do                 case eqHST1 @('TPair ('TList 'TOperation) st) out of                   Right Refl ->                     pure $ SomeContract Contract{ cCode = ContractCode instr', .. }                   Left err ->-                    Left $ TCContractError "contract output type violates convention:" $ Just err+                    Left $ TcContractError "contract output type violates convention:" $ Just err               AnyOutInstr instr' ->                 pure $ SomeContract Contract{ cCode = ContractCode instr', .. }    where-    hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a+    hasTypeError :: forall (t :: T) a op. SingI t => Text -> BadTypeForScope -> TypeCheck op a     hasTypeError name reason = throwError $-      TCContractError ("contract " <> name <> " type error") $+      TcContractError ("contract " <> name <> " type error") $       Just $ UnsupportedTypeForScope (demote @t) reason -    onFailedCodeTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck a+    onFailedCodeTypeCheck :: [TypeCheckedOp op] -> TcError' op -> TypeCheck op a     onFailedCodeTypeCheck ops err = do       verbose <- asks' tcVerbose       throwError if verbose-        then TCIncompletelyTyped err U.Contract+        then TcIncompletelyTyped err U.Contract              { contractParameter = wholeParam              , contractStorage = mStorage              , contractCode = ops@@ -210,11 +241,11 @@              }         else err -    onFailedFullTypeCheck :: [TypeCheckedOp] -> [U.View' TypeCheckedOp] -> TCError -> TypeCheck a+    onFailedFullTypeCheck :: [TypeCheckedOp op] -> [U.View' (TypeCheckedOp op)] -> TcError' op -> TypeCheck op a     onFailedFullTypeCheck ops views err = do       verbose <- asks' tcVerbose       throwError if verbose-        then TCIncompletelyTyped err U.Contract+        then TcIncompletelyTyped err U.Contract              { contractParameter = wholeParam              , contractStorage = mStorage              , contractCode = ops@@ -226,22 +257,33 @@ typeVerifyView   :: forall arg ret st.      (SingI arg, SingI ret, WellTyped st)-  => Notes st -> U.View -> TypeCheckResult (View arg st ret)-typeVerifyView notes v = do+  => Notes st -> U.View -> TypeCheckResult U.ExpandedOp (View arg st ret)+typeVerifyView = typeVerifyView' typeCheckExpandedOp++typeVerifyView'+  :: forall arg ret st op.+     (SingI arg, SingI ret, WellTyped st, IsInstrOp op)+  => TcInstrBase op -> Notes st -> U.View' op -> TypeCheckResult op (View arg st ret)+typeVerifyView' tcOp notes v = do   SomeView (tcView@View{} :: View arg' st' ret') <--    runTypeCheck TypeCheckTest $ typeCheckViewImpl notes v+    runTypeCheck TypeCheckTest $ typeCheckView' tcOp notes v   Refl <- requireEq @arg' @arg (mkErr TltParameterType)   Refl <- requireEq @st' @st (mkErr TltStorageType)   Refl <- requireEq @ret' @ret (mkErr TltParameterType)   return tcView   where-    mkErr :: TopLevelType -> MismatchError T -> TypeCheckResult any+    mkErr :: TopLevelType -> MismatchError T -> TypeCheckResult op any     mkErr tyDesc merr =-      throwError $ TCContractError "error in view type" $ Just $+      throwError $ TcContractError "error in view type" $ Just $           UnexpectedTopLevelType tyDesc merr -typeCheckViewImpl :: WellTyped st => Notes st -> U.View -> TypeCheck (SomeView st)-typeCheckViewImpl storageNote+typeCheckView'+  :: (WellTyped st, IsInstrOp op)+  => TcInstrBase op+  -> Notes st+  -> U.View' op+  -> TypeCheck op (SomeView st)+typeCheckView' tcOp storageNote   uView@U.View   { U.viewArgument = AsUType (argNote :: Notes param)   , U.viewReturn = AsUType (returnNote :: Notes ret)@@ -259,7 +301,7 @@     codeRes <-       usingReaderT def $       liftNoExcept $-      typeCheckImpl typeCheckInstr uInstr inp+      typeCheckImpl tcOp uInstr inp     _ :/ instrOut <-       tcsEither (onFailedViewsTypeCheck uView) pure codeRes @@ -269,50 +311,63 @@     case instrOut of       instr ::: out -> liftEither do         Refl <- eqHST1 @ret out-          `onFirst` (TCViewError "view return type mismatch:" viewName . Just)+          `onFirst` (TcViewError "view return type mismatch:" viewName . Just)         return $ SomeView View{ vCode = instr, .. }       AnyOutInstr instr ->         return $ SomeView View{ vCode = instr, .. }    where     onFailedViewsTypeCheck-      :: U.View -> [TypeCheckedOp] -> TCError -> TypeCheck a+      :: U.View' op -> [TypeCheckedOp op] -> TcError' op -> TypeCheck op a     onFailedViewsTypeCheck v viewOps err = do       verbose <- asks' tcVerbose       throwError if verbose-        then TCIncompletelyTypedView err v{ U.viewCode = viewOps }+        then TcIncompletelyTypedView err v{ U.viewCode = viewOps }         else err -    hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a+    hasTypeError :: forall (t :: T) a op. SingI t => Text -> BadTypeForScope -> TypeCheck op a     hasTypeError desc reason = throwError $-      TCViewError (desc <> " type error in view") viewName $+      TcViewError (desc <> " type error in view") viewName $       Just $ UnsupportedTypeForScope (demote @t) reason -typeCheckViewsImpl-  :: (WellTyped st)-  => U.Contract' TypeCheckedOp -> Notes st -> [U.View] -> TypeCheck [SomeView st]-typeCheckViewsImpl tcCotract storageNote cViews =+typeCheckViews'+  :: forall st op.+     (WellTyped st, IsInstrOp op)+  => TcInstrBase op+  -> U.Contract' (TypeCheckedOp op)+  -> Notes st+  -> [U.View' op]+  -> TypeCheck op [SomeView st]+typeCheckViews' doTypeCheckOp tcContract storageNote cViews =   let myfoldM l acc f = foldM f acc l in-  fmap (map snd . toList) $ myfoldM cViews (Seq.Empty :: Seq (U.View, SomeView st))+  fmap (map snd . toList) $ myfoldM cViews (Seq.Empty :: Seq (U.View' op, SomeView st))     \processedViews uView -> do-      resView <- typeCheckViewImpl storageNote uView+      resView <- typeCheckView' doTypeCheckOp storageNote uView       pure $ processedViews |> (uView, resView)       `catchError` \case-        TCIncompletelyTypedView err view' ->+        TcIncompletelyTypedView err view' ->           let tcViews = map (uncurry someViewToOp) processedViews           in onFailedViewsTypeCheck tcViews view' err         err -> throwError err   where     onFailedViewsTypeCheck-      :: Seq (U.View' TypeCheckedOp) -> U.View' TypeCheckedOp -> TCError -> TypeCheck a+      :: Seq (U.View' (TypeCheckedOp op)) -> U.View' (TypeCheckedOp op) -> TcError' op -> TypeCheck op a     onFailedViewsTypeCheck processedViews v err = do       verbose <- asks' tcVerbose       throwError if verbose-        then TCIncompletelyTyped err tcCotract+        then TcIncompletelyTyped err tcContract              { U.contractViews = toList (processedViews |> v)              }         else err +typeCheckViews+  :: WellTyped st+  => U.Contract' (TypeCheckedOp U.ExpandedOp)+  -> Notes st+  -> [U.View]+  -> TypeCheck U.ExpandedOp [SomeView st]+typeCheckViews = typeCheckViews' typeCheckExpandedOp+ -- | Function @typeCheckList@ converts list of Michelson instructions -- given in representation from @Morley.Michelson.Type@ module to representation -- in strictly typed GADT.@@ -325,8 +380,8 @@   :: (SingI inp)   => [U.ExpandedOp]   -> HST inp-  -> TypeCheck (SomeInstr inp)-typeCheckList = throwingTCError ... typeCheckListNoExcept+  -> TypeCheck U.ExpandedOp (SomeTcInstr inp)+typeCheckList = throwingTcError ... typeCheckListNoExcept typeCheckExpandedOp  -- | Function @typeCheckListNoExcept@ converts list of Michelson instructions -- given in representation from @Morley.Michelson.Type@ module to representation in a@@ -335,9 +390,9 @@ -- Types are checked along the way. It is necessary to embed well typed node as -- well as type checking errors into the tree. typeCheckListNoExcept-  :: (SingI inp)-  => [U.ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp)-typeCheckListNoExcept = usingReaderT def ... typeCheckImpl typeCheckInstr+  :: (SingI inp, IsInstrOp op)+  => TcInstrBase op -> [op] -> HST inp -> TypeCheckNoExcept op (TypeCheckedSeq op inp)+typeCheckListNoExcept tcOp = usingReaderT def ... typeCheckImpl tcOp  -- | Function @typeCheckValue@ converts a single Michelson value -- given in representation from @Morley.Michelson.Untyped@ module hierarchy to@@ -354,11 +409,11 @@ typeCheckValue   :: forall t. SingI t   => U.Value-  -> TypeCheckResult (Value t)+  -> TypeCheckResult U.ExpandedOp (Value t) typeCheckValue value = do   runTypeCheck (TypeCheckValue (value, demote @t) Nothing) $     usingReaderT def $-      typeCheckValImpl Nothing typeCheckInstr value+      typeCheckValImpl Nothing typeCheckExpandedOp value  -- | Simulates the typechecking behavior of the RPC's @/run_code@ endpoint. --@@ -366,48 +421,62 @@ -- we check if a big_map exists with that ID. -- If it does, and if the big_map's value and key have the expected types, we replace the -- big_map ID with the corresponding big_map value.-typeCheckValueRunCodeCompat :: forall t. SingI t => BigMapFinder -> U.Value -> TypeCheckResult (Value t)+typeCheckValueRunCodeCompat :: forall t. SingI t => BigMapFinder -> U.Value -> TypeCheckResult U.ExpandedOp (Value t) typeCheckValueRunCodeCompat bigMapFinder val =   runTypeCheck (TypeCheckValue (val, demote @t) (Just bigMapFinder)) $     usingReaderT def $-      typeCheckValImpl Nothing typeCheckInstr val+      typeCheckValImpl Nothing typeCheckExpandedOp val  typeVerifyParameter   :: SingI t-  => TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)+  => TcOriginatedContracts -> U.Value -> TypeCheckResult U.ExpandedOp (Value t) typeVerifyParameter originatedContracts = typeVerifyTopLevelType (Just originatedContracts)  typeVerifyStorage   :: SingI t-  => U.Value -> TypeCheckResult (Value t)-typeVerifyStorage = typeVerifyTopLevelType Nothing+  => U.Value -> TypeCheckResult U.ExpandedOp (Value t)+typeVerifyStorage = typeVerifyStorage' typeCheckExpandedOp +typeVerifyStorage'+  :: (SingI t, IsInstrOp op)+  => TcInstrBase op -> U.Value' op -> TypeCheckResult op (Value t)+typeVerifyStorage' tcOp = typeVerifyTopLevelType' tcOp Nothing+ typeVerifyTopLevelType   :: forall t. SingI t-  => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)-typeVerifyTopLevelType mOriginatedContracts valueU =+  => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult U.ExpandedOp (Value t)+typeVerifyTopLevelType = typeVerifyTopLevelType' typeCheckExpandedOp++typeVerifyTopLevelType'+  :: forall t op. (SingI t, IsInstrOp op)+  => TcInstrBase op -> Maybe TcOriginatedContracts -> U.Value' op -> TypeCheckResult op (Value t)+typeVerifyTopLevelType' tcOp mOriginatedContracts valueU =   runTypeCheck (TypeCheckValue (valueU, demote @t) Nothing) $ usingReaderT def $-    typeCheckValImpl mOriginatedContracts typeCheckInstr valueU+    typeCheckValImpl mOriginatedContracts tcOp valueU  -- | Like 'typeCheckValue', but for values to be used as parameter. -- -- Also accepts a 'TcOriginatedContracts' in order to be able to type-check -- @contract p@ values (which can only be part of a parameter). typeCheckParameter-  :: TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult SomeValue+  :: TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult U.ExpandedOp SomeValue typeCheckParameter originatedContracts = typeCheckTopLevelType (Just originatedContracts)  -- | Like 'typeCheckValue', but for values to be used as storage. typeCheckStorage-  :: U.Ty -> U.Value -> TypeCheckResult SomeValue+  :: U.Ty -> U.Value -> TypeCheckResult U.ExpandedOp SomeValue typeCheckStorage = typeCheckTopLevelType Nothing  typeCheckTopLevelType-  :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult SomeValue-typeCheckTopLevelType mOriginatedContracts typeU valueU =-  withSomeSing (fromUType typeU) $ \(s :: Sing t) ->-    withSingI s $ SomeValue <$> typeVerifyTopLevelType @t mOriginatedContracts valueU+  :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult U.ExpandedOp SomeValue+typeCheckTopLevelType = typeCheckTopLevelType' typeCheckExpandedOp +typeCheckTopLevelType'+  :: IsInstrOp op+  => TcInstrBase op -> Maybe TcOriginatedContracts -> U.Ty -> U.Value' op -> TypeCheckResult op SomeValue+typeCheckTopLevelType' tcOp mOriginatedContracts (AsUType (_ :: Notes t)) valueU =+  SomeValue <$> typeVerifyTopLevelType' @t tcOp mOriginatedContracts valueU+ -- | Helper data type we use to typecheck DUPN. data TCDupNHelper inp where   TCDupNHelper ::@@ -479,18 +548,17 @@ -- | Helper function to convert a simple throwing typechecking action into a -- non-throwing one, embedding possible errors into the type checking tree. workOnInstr-  :: U.ExpandedInstr-  -> TypeCheckInstr (SomeInstr s)-  -> TypeCheckInstrNoExcept (TypeCheckedSeq s)+  :: IsInstrOp op+  => U.InstrAbstract op+  -> TypeCheckInstr op (SomeTcInstr s)+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op s) workOnInstr instr = tcEither-  (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx instr])+  (\err -> pure $ IllTypedSeq err [NonTypedInstr $ liftInstr instr])   (pure . WellTypedSeq) --- | Less verbose version of `typeCheckImpl typeCheckInstr`.-tcList-  :: (SingI inp)-  => [U.ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-tcList = typeCheckImpl typeCheckInstr+-- | Alias for 'typeCheckImpl'.+tcList :: IsInstrOp op => TcInstrBase op -> TcInstr op [op]+tcList = typeCheckImpl  -- | Function @typeCheckInstr@ converts a single Michelson instruction -- given in representation from @Morley.Michelson.Type@ module to representation@@ -505,10 +573,10 @@ -- If there was no match on a given pair of instruction and input stack, -- that is interpreted as input of wrong type and type check finishes with -- error.-typeCheckInstr :: TcInstrHandler-typeCheckInstr uInstr inp = case (uInstr, inp) of+typeCheckInstr :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op (U.InstrAbstract op)+typeCheckInstr tcOp uInstr inp = case (uInstr, inp) of   (U.EXT ext, si) ->-    typeCheckExt typeCheckInstr ext si+    typeCheckExt tcOp ext si    (U.DROP, _ ::& rs) -> workOnInstr uInstr $ pure $ inp :/ DROP ::: rs @@ -521,7 +589,7 @@       go :: forall inp. SingI inp         => Word         -> HST inp-        -> TypeCheckInstr (TCDropHelper inp)+        -> TypeCheckInstr op (TCDropHelper inp)       go = curry \case         (0, i) -> pure (TCDropHelper Zero i) @@ -544,15 +612,15 @@       go :: forall inp. SingI inp         => Word         -> HST inp-        -> TypeCheckInstr (TCDupNHelper inp)+        -> TypeCheckInstr op (TCDupNHelper inp)       go = curry \case         (_, SNil) -> notEnoughItemsOnStack'          (0, _) ->-          typeCheckInstrErr' uInstr (SomeHST inp) Nothing (InvalidInstruction uInstr "'DUP n' expects n > 0")+          typeCheckInstrErr' uInstr (SomeHST inp) Nothing (InvalidInstruction (void uInstr) "'DUP n' expects n > 0")          -- Don't bind whatever variable annotation is here because DUP n doesn't-        -- duplicate variable annotations. This is consistent with tezos-client.+        -- duplicate variable annotations. This is consistent with @octez-client@.         (1, i@((an :: SingT a, dict) ::& _)) -> do           Dict <-             onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing $@@ -574,7 +642,7 @@       go :: forall inp. SingI inp         => Word         -> HST inp-        -> TypeCheckInstr (TCDigHelper inp)+        -> TypeCheckInstr op (TCDigHelper inp)       go = curry \case         -- Even 'DIG 0' is invalid on empty stack (so it is not strictly `Nop`).         (_, SNil) -> notEnoughItemsOnStack'@@ -591,7 +659,7 @@       go :: forall inp. SingI inp         => Word         -> HST inp-        -> TypeCheckInstr (TCDugHelper inp)+        -> TypeCheckInstr op (TCDugHelper inp)       go = curry \case         (0, i@(_ ::& _)) -> pure (TCDugHelper Zero i) @@ -608,7 +676,7 @@     withUType mt $ \(nt :: Notes t) -> do       -- Locally switch 'TypeCheckMode' to 'TypeCheckValue'.       val <- local' (tcModeL .~ TypeCheckValue (mval, demote @t) Nothing) $-        typeCheckValImpl @t Nothing typeCheckInstr mval+        typeCheckValImpl @t Nothing tcOp mval        proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing         $ checkScope @(ConstantScope t)@@ -634,7 +702,7 @@    (U.IF_NONE mp mq, (STOption (asing :: SingT a), Dict) ::& rs) ->     withWTPInstr' @a $-      genericIf IF_NONE U.IF_NONE mp mq rs ((asing, Dict) ::& rs) inp+      genericIf tcOp IF_NONE U.IF_NONE mp mq rs ((asing, Dict) ::& rs) inp    (U.IF_NONE _ _, _ ::& _) ->     failWithErr $ UnexpectedType $ ("option 'a" :| []) :| []@@ -663,11 +731,11 @@     go nTotal inp <&> \case       TCPairNHelper s out -> inp :/ AnnPAIRN (Anns1 varAnn) s ::: out     where-      go :: forall inp. Word -> HST inp -> TypeCheckInstr (TCPairNHelper inp)+      go :: forall inp. Word -> HST inp -> TypeCheckInstr op (TCPairNHelper inp)       go n hst         | n < 2 =             typeCheckInstrErr' uInstr (SomeHST inp) Nothing-              (InvalidInstruction uInstr "'PAIR n' expects n ≥ 2")+              (InvalidInstruction (void uInstr) "'PAIR n' expects n ≥ 2")         | n == 2 =             case hst of               (an :: SingT a, _) ::& (bn :: SingT b, _) ::& hstTail -> do@@ -691,11 +759,11 @@       TCUnpairNHelper s out ->         inp :/ UNPAIRN s ::: out     where-      go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr (TCUnpairNHelper (x : xs))+      go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr op (TCUnpairNHelper (x : xs))       go n hst         | n < 2 =             typeCheckInstrErr' uInstr (SomeHST inp) Nothing-              (InvalidInstruction uInstr "UNPAIR expects an argument of at least 2.")+              (InvalidInstruction (void uInstr) "UNPAIR expects an argument of at least 2.")         | n == 2 =             case hst of               (STPair aT bT, Dict) ::& rest -> do@@ -713,7 +781,7 @@                       (aT, Dict) ::& out               _ -> unexpectedType -      unexpectedType :: TypeCheckInstr a+      unexpectedType :: TypeCheckInstr op a       unexpectedType = failWithErr' $ UnexpectedType $ (pairWithElems nTotal :| []) :| []    (U.CAR vn fn, (STPair lt _, Dict) ::& rs) -> workOnInstr uInstr $@@ -755,7 +823,7 @@           let             ait = (lt, Dict) ::& rs             bit = (rt, Dict) ::& rs-          genericIf IF_LEFT U.IF_LEFT mp mq ait bit inp+          genericIf tcOp IF_LEFT U.IF_LEFT mp mq ait bit inp    (U.IF_LEFT _ _, _ ::& _) ->     failWithErr $ UnexpectedType $ ("or 'a 'b" :| []) :| []@@ -779,7 +847,7 @@   (U.IF_CONS mp mq, (ns@(STList (an :: SingT t1)), Dict) ::& rs) -> do     withWTPInstr' @t1 $ do       let ait = (an, Dict) ::& (ns, Dict) ::& rs-      genericIf IF_CONS U.IF_CONS mp mq ait rs inp+      genericIf tcOp IF_CONS U.IF_CONS mp mq ait rs inp    (U.IF_CONS _ _, _ ::& _) ->     failWithErr $ UnexpectedType $ ("list 'a" :| []) :| []@@ -824,17 +892,17 @@    (U.MAP vn mp, (STList (vns :: SingT t1), Dict) ::& _) -> withSingI vns $ do     withWTPInstr' @t1 $-      mapImpl (U.MAP vn) vns vn uInstr mp inp+      mapImpl tcOp (U.MAP vn) vns vn uInstr mp inp         (\(rn :: SingT t) hst -> withWTPInstr @t $ pure $ (STList rn, Dict) ::& hst)    (U.MAP vn mp, (STOption (vns :: SingT t1), Dict) ::& _) -> withSingI vns $ do     withWTPInstr' @t1 $-      mapImpl (U.MAP vn) vns vn uInstr mp inp+      mapImpl tcOp (U.MAP vn) vns vn uInstr mp inp         (\(rn :: SingT t) hst -> withWTPInstr @t $ pure $ (STOption rn, Dict) ::& hst)    (U.MAP vn mp, (STMap (k :: SingT k) (v :: SingT v1), Dict) ::& _) -> withSingI k $ withSingI v $ do     withWTPInstr' @('TPair k v1) $-      mapImpl (U.MAP vn) (STPair k v) vn uInstr mp inp+      mapImpl tcOp (U.MAP vn) (STPair k v) vn uInstr mp inp           (\(rn :: SingT v) hst -> withWTPInstr @('TMap k v) $ pure $ (STMap k rn, Dict) ::& hst)    (U.MAP _ _, _ ::& _) ->@@ -848,14 +916,14 @@    (U.ITER is, (STSet (s :: Sing t1), _) ::& _) -> withSingI s $ do     withWTPInstr' @t1 $-      iterImpl s uInstr is inp+      iterImpl tcOp s uInstr is inp    (U.ITER is, (STList (l :: Sing t1), _) ::& _) -> withSingI l $ do     withWTPInstr' @t1 $-      iterImpl l uInstr is inp+      iterImpl tcOp l uInstr is inp    (U.ITER is, (STMap (k :: SingT a) (v :: SingT b), _) ::& _) -> withSingI k $ withSingI v $ do-    withWTPInstr' @('TPair a b) $ iterImpl (STPair k v) uInstr is inp+    withWTPInstr' @('TPair a b) $ iterImpl tcOp (STPair k v) uInstr is inp    (U.ITER _, _ ::& _) ->     failWithErr $ UnexpectedType@@ -909,7 +977,7 @@       TCGetNHelper s out ->         inp :/ AnnGETN (Anns1 getNVarAnn) s ::: out     where-      go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr (TCGetNHelper (x : xs))+      go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr op (TCGetNHelper (x : xs))       go 0 ((a, Dict) ::& rest) =         pure $ TCGetNHelper Zero ((a, Dict) ::& rest)       go 1 ((STPair leftNotes _, Dict) ::& rest) =@@ -943,7 +1011,7 @@       TCUpdateNHelper s out ->         inp :/ AnnUPDATEN (Anns1 updateNVarAnn) s ::: out     where-      go :: forall val pair rest. Word -> HST (val : pair : rest) -> TypeCheckInstr (TCUpdateNHelper (val : pair : rest))+      go :: forall val pair rest. Word -> HST (val : pair : rest) -> TypeCheckInstr op (TCUpdateNHelper (val : pair : rest))       go 0 ((valNotes, Dict) ::& (_, _) ::& rest) =         pure $ TCUpdateNHelper Zero $           (valNotes, Dict) ::& rest@@ -976,7 +1044,7 @@   (U.GET_AND_UPDATE _, _) -> notEnoughItemsOnStack    (U.IF mp mq, (STBool{}, _) ::& rs) ->-    genericIf IF U.IF mp mq rs rs inp+    genericIf tcOp IF U.IF mp mq rs rs inp    (U.IF _ _, _ ::& _) ->     failWithErr $ UnexpectedType $ ("bool" :| []) :| []@@ -984,7 +1052,7 @@   (U.IF _ _, SNil) -> notEnoughItemsOnStack    (U.LOOP is, (STBool{}, _) ::& (rs :: HST rs)) -> do-    preserving (tcList is rs) U.LOOP $ \(_ :/ tp) ->+    preserving (tcList tcOp is rs) U.LOOP $ \(_ :/ tp) ->       case tp of         subI ::: (o :: HST o) -> do           case eqHST o (sing @'TBool -:& rs) of@@ -1002,7 +1070,7 @@   (U.LOOP_LEFT is, (os@(STOr (an :: SingT t) (bn :: SingT b)), Dict) ::& rs) -> do     withWTPInstr' @t $ withWTPInstr' @b $ do       let ait = (an, Dict) ::& rs-      preserving (tcList is ait) U.LOOP_LEFT $ \(_ :/ tp) ->+      preserving (tcList tcOp is ait) U.LOOP_LEFT $ \(_ :/ tp) ->         case tp of           subI ::: o -> do             case (eqHST o (os -:& rs), o) of@@ -1024,15 +1092,24 @@     -- litter our main typechecking logic     withWTPInstr' @t $       withWTPInstr' @u $-        lamImpl (U.LAMBDA vn p1 p2) (Anns3'' vn ins ons) uInstr is (notesSing ins) (notesSing ons) i+        lamImpl tcOp is (notesSing ins) (notesSing ons)+          (U.LAMBDA vn p1 p2) (Anns3'' vn ins ons) uInstr i +  (U.LAMBDA_REC vn p1@(AsUType (ins :: Notes t)) p2@(AsUType (ons :: Notes u)) is, i) -> do+    -- further processing is extracted into another function just not to+    -- litter our main typechecking logic+    withWTPInstr' @t $+      withWTPInstr' @u $+        lamRecImpl tcOp is (notesSing ins) (notesSing ons)+          (U.LAMBDA_REC vn p1 p2) (Anns3'' vn ins ons) uInstr i+   (U.EXEC vn, ((_ :: SingT t1), _)                               ::& ( STLambda (v :: SingT t1') (b :: SingT t2'), _)                               ::& rs) -> withSingI v $ withSingI b $ workOnInstr uInstr $ do     Refl <- errM $ eqType @t1 @t1'     withWTPInstr @t2' $ pure $ inp :/ AnnEXEC (Anns1 vn) ::: ((b, Dict) ::& rs)       where-        errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a+        errM :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Either TcTypeError a -> m a         errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)    (U.EXEC _, _ ::& _ ::& _) ->@@ -1060,7 +1137,7 @@   (U.APPLY _, _) -> notEnoughItemsOnStack    (U.DIP is, a ::& s) -> do-    typeCheckDipBody U.DIP uInstr is s+    typeCheckDipBody tcOp U.DIP uInstr is s       (IllTypedSeq)       (\subI t -> WellTypedSeq $ inp :/ DIP subI ::: (a ::& t)) @@ -1074,15 +1151,15 @@       go :: forall inp. SingI inp         => Word         -> HST inp-        -> TypeCheckInstrNoExcept (TCDipHelper inp)+        -> TypeCheckInstrNoExcept op (TCDipHelper op inp)       go n curHST = case (n, curHST) of-        (0, _) -> typeCheckDipBody (U.DIPN nTotal) uInstr instructions curHST+        (0, _) -> typeCheckDipBody tcOp (U.DIPN nTotal) uInstr instructions curHST           (TCDipHelperErr)           (TCDipHelperOk Zero)         (_, SNil) -> do           pos <- view tcieErrorPos-          let err = TCFailedOnInstr uInstr (SomeHST inp) pos Nothing (Just NotEnoughItemsOnStack)-          pure $ TCDipHelperErr err [NonTypedInstr $ U.PrimEx uInstr]+          let err = TcFailedOnInstr uInstr (SomeHST inp) pos Nothing (Just NotEnoughItemsOnStack)+          pure $ TCDipHelperErr err [NonTypedInstr $ liftInstr uInstr]         (_, hstHead ::& hstTail) ->           go (n - 1) hstTail <&> \case           TCDipHelperOk s subI out -> TCDipHelperOk (Succ s) subI (hstHead ::& out)@@ -1101,7 +1178,7 @@       withWTPInstr @t $         pure $ inp :/ AnnCAST (Anns2' vn castToNotes) ::: ((notesSing castToNotes, Dict) ::& rs)     where-      errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a+      errM :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Either TcTypeError a -> m a       errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just Cast)    (U.CAST _ _, _) -> notEnoughItemsOnStack@@ -1385,7 +1462,7 @@                   withWTPInstr @('TContract t1) $                     pure $ inp :/ AnnSELF @arg (Anns1 vn) (SomeEpc epc) ::: ((notesSing ntRes, Dict) ::& inp)       TypeCheckTest ->-        failWithErr' $ InvalidInstruction uInstr "'SELF' appears in test typechecking"+        failWithErr' $ InvalidInstruction (void uInstr) "'SELF' appears in test typechecking"   (U.CONTRACT vn fn mt, (STAddress{}, _) ::& rs) -> workOnInstr uInstr $     withUType mt $ \(tns :: Notes t) -> do       proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)@@ -1433,7 +1510,7 @@     ::& (STMutez{}, _)     ::& (_ :: SingT g, Dict) ::& rs) -> workOnInstr uInstr $ withNotInView uInstr do       (SomeContract contr@(Contract _ _ (_ :: Notes st) _ _))-        <- lift $ typeCheckContractImpl contract+        <- lift $ doTypeCheckContract' tcOp contract       Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just ContractStorage) $         eqType @g @st       pure@@ -1559,6 +1636,14 @@     failWithErr $ UnexpectedType $ ("a'" :| ["nat"]) :| []   (U.TICKET _, _) -> notEnoughItemsOnStack +  (U.TICKET_DEPRECATED vn, (stVal :: Sing v, _) ::& (STNat{}, _) ::& rs) -> workOnInstr uInstr $+    withWTPInstr @v $+    withCompareableCheck stVal uInstr inp $+      inp :/ AnnTICKET_DEPRECATED (Anns1 vn) ::: ((sing, Dict) ::& rs)+  (U.TICKET_DEPRECATED _, _ ::& _ ::& _) ->+    failWithErr $ UnexpectedType $ ("a'" :| ["nat"]) :| []+  (U.TICKET_DEPRECATED _, _) -> notEnoughItemsOnStack+   (U.READ_TICKET vn, ticket@(STTicket{}, Dict) ::& rs) -> workOnInstr uInstr $       pure $ inp :/ AnnREAD_TICKET (Anns1 vn) ::: ((sing, Dict) ::& ticket ::& rs)   (U.READ_TICKET _, _ ::& _) ->@@ -1589,6 +1674,10 @@       ::& (STNat, Dict)       ::& rs) ->       workOnInstr uInstr $ do+        isStrict <- asks' tcStrict+        when isStrict $+          typeCheckInstrErr' uInstr (SomeHST inp) Nothing $+            InvalidInstruction (void uInstr) "OPEN_CHEST temporarily deprecated"         pure $ inp :/ AnnOPEN_CHEST (Anns1 vn) ::: (           (STOr STBytes STBool, Dict)           ::& rs)@@ -1611,7 +1700,7 @@             pure $ inp :/ AnnSAPLING_VERIFY_UPDATE (Anns1 vn) ::: (               (STOption (STPair STBytes (STPair STInt (STSaplingState s1))), Dict)               ::& rs)-          Nothing -> failWithErr' $ InvalidInstruction uInstr+          Nothing -> failWithErr' $ InvalidInstruction (void uInstr)             "Memo sizes of two sapling states or transactions do not match."    (U.SAPLING_VERIFY_UPDATE _, _ ::& _ ::& _) ->@@ -1631,63 +1720,64 @@         Nothing ->           pure $ inp :/ AnnEMIT (Anns1 va) tag Nothing ::: ((sing, Dict) ::& rs)       where-        errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a+        errM :: (MonadReader TypeCheckInstrEnv m, MonadError (TcError' op) m) => Either TcTypeError a -> m a         errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just EmitArgument)    where     withWTPInstr'       :: forall t inp. SingI t-      => (WellTyped t => TypeCheckInstrNoExcept (TypeCheckedSeq inp))-      -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+      => (WellTyped t => TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))+      -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)     withWTPInstr' = withWTPInstr'_ @t uInstr (SomeHST inp)      withWTPInstr-      :: forall t a. SingI t => (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a+      :: forall t a. SingI t => (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op a     withWTPInstr = withWTPInstr_ @t uInstr (SomeHST inp) -    failWithErr :: TCTypeError -> TypeCheckInstrNoExcept (TypeCheckedSeq a)+    failWithErr :: TcTypeError -> TypeCheckInstrNoExcept op (TypeCheckedSeq op a)     failWithErr = workOnInstr uInstr . failWithErr' -    failWithErr' :: TCTypeError -> TypeCheckInstr a+    failWithErr' :: TcTypeError -> TypeCheckInstr op a     failWithErr' = typeCheckInstrErr' uInstr (SomeHST inp) Nothing -    notEnoughItemsOnStack :: TypeCheckInstrNoExcept (TypeCheckedSeq a)+    notEnoughItemsOnStack :: TypeCheckInstrNoExcept op (TypeCheckedSeq op a)     notEnoughItemsOnStack = failWithErr NotEnoughItemsOnStack -    notEnoughItemsOnStack' :: TypeCheckInstr a+    notEnoughItemsOnStack' :: TypeCheckInstr op a     notEnoughItemsOnStack' = failWithErr' NotEnoughItemsOnStack -    withNotInView :: U.ExpandedInstr -> (IsNotInView => TypeCheckInstr r) -> TypeCheckInstr r-    withNotInView instr act = asks' tcMode >>= \case+    withNotInView :: U.InstrAbstract op -> (IsNotInView => TypeCheckInstr op r) -> TypeCheckInstr op r+    withNotInView instr act = asks' (tcMode @op) >>= \case       -- we provide the not-in-view constraint in the isolated mode       TypeCheckTest -> giveNotInView act       _ -> view tcieNotInView >>= \case         Just Dict -> act         Nothing -> failWithErr' $-          InvalidInstruction instr "This instruction cannot be used on the top level of a view"+          InvalidInstruction (void instr) "This instruction cannot be used on the top level of a view"  -- | Helper function for two-branch if where each branch is given a single -- value. genericIf-  :: forall bti bfi cond rs .-    (SingI bti, SingI bfi)-  => (forall s'.+  :: forall bti bfi cond rs op .+    (SingI bti, SingI bfi, IsInstrOp op)+  => TcInstrBase op+  -> (forall s'.         Instr bti s' ->         Instr bfi s' ->         Instr (cond ': rs) s'      )-  -> (forall op. [op] -> [op] -> U.InstrAbstract op)-  -> [U.ExpandedOp]-  -> [U.ExpandedOp]+  -> (forall op1. [op1] -> [op1] -> U.InstrAbstract op1)+  -> [op]+  -> [op]   -> HST bti   -> HST bfi   -> HST (cond ': rs)-  -> TypeCheckInstrNoExcept (TypeCheckedSeq (cond ': rs))-genericIf cons mCons mbt mbf bti bfi i@(_ ::& _) = do+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op (cond ': rs))+genericIf tcOp cons mCons mbt mbf bti bfi i@(_ ::& _) = do   let cons1 opsT = mCons opsT (map (IllTypedOp . NonTypedInstr) mbf)-  preserving' (tcList mbt bti) cons1 $ \tInstr@(_ :/ pinstr) -> do+  preserving' (tcList tcOp mbt bti) cons1 $ \tInstr@(_ :/ pinstr) -> do     let cons2 opsF = mCons [someInstrToOp tInstr] opsF-    preserving (tcList mbf bfi) cons2 $ \(_ :/ qinstr) -> do+    preserving (tcList tcOp mbf bfi) cons2 $ \(_ :/ qinstr) -> do       fmap (i :/) $ case (pinstr, qinstr) of         (p ::: po, q ::: qo) -> do           let instr = mCons mbt mbf@@ -1702,22 +1792,24 @@           pure $ AnyOutInstr (cons p q)  mapImpl-  :: forall c rs.+  :: forall c rs op.     ( MapOp c     , WellTyped (MapOpInp c)     , SingIOne (MapOpRes c)+    , IsInstrOp op     )-  => ([TypeCheckedOp] -> TypeCheckedInstr)+  => TcInstrBase op+  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)   -> SingT (MapOpInp c)   -> VarAnn-  -> U.ExpandedInstr-  -> [U.ExpandedOp]+  -> U.InstrAbstract op+  -> [op]   -> HST (c ': rs)   -> (forall v'. (SingI v') =>-        SingT v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs)))-  -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs))-mapImpl cons vn anns instr mp i@(_ ::& rs) mkRes = do-  preserving (tcList mp ((vn, Dict) ::& rs)) cons $ \(_ :/ subp) ->+        SingT v' -> HST rs -> TypeCheckInstr op (HST (MapOpRes c v' ': rs)))+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op (c ': rs))+mapImpl tcOp cons vn anns instr mp i@(_ ::& rs) mkRes = do+  preserving (tcList tcOp mp ((vn, Dict) ::& rs)) cons $ \(_ :/ subp) ->     case subp of       sub ::: subo ->         case subo of@@ -1731,20 +1823,22 @@         typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails  iterImpl-  :: forall c rs .+  :: forall c rs op .     ( IterOp c     , WellTyped (IterOpEl c)+    , IsInstrOp op     )-  => SingT (IterOpEl c)-  -> U.ExpandedInstr-  -> [U.ExpandedOp]+  => TcInstrBase op+  -> SingT (IterOpEl c)+  -> U.InstrAbstract op+  -> [op]   -> HST (c ': rs)-  -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs))-iterImpl en instr mp i@((_, _) ::& rs) = do+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op (c ': rs))+iterImpl tcOp en instr mp i@((_, _) ::& rs) = do   let tcAction = case mp of         [] -> workOnInstr instr           (typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode)-        _ -> typeCheckImpl typeCheckInstr mp ((en, Dict) ::& rs)+        _ -> typeCheckImpl tcOp mp ((en, Dict) ::& rs)   preserving tcAction U.ITER $ \(_ :/ subp) -> case subp of     subI ::: o -> do       Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) $ eqHST o rs@@ -1752,24 +1846,56 @@     AnyOutInstr subI ->       pure $ i :/ ITER subI ::: rs +type LamTC it ot ts op+  =  [op]+  -> SingT it+  -> SingT ot+  ->  ([TypeCheckedOp op] -> TypeCheckedInstr op)+  -> Anns '[VarAnn, Notes it, Notes ot]+  -> U.InstrAbstract op+  -> HST ts+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op ts)+ lamImpl-  :: forall it ot ts .+  :: forall it ot ts op .     ( WellTyped it, WellTyped ot     , SingI ts+    , IsInstrOp op     )-  => ([TypeCheckedOp] -> TypeCheckedInstr)-  -> Anns '[VarAnn, Notes it, Notes ot]-  -> U.ExpandedInstr-  -> [U.ExpandedOp]-  -> SingT it-  -> SingT ot-  -> HST ts-  -> TypeCheckInstrNoExcept (TypeCheckedSeq ts)-lamImpl cons anns instr is ins ons i =+  => TcInstrBase op+  -> LamTC it ot ts op+lamImpl tcOp is ins = lamCommon AnnLAMBDA+  (giveNotInView $ local (set tcieNotInView $ Just Dict) $ tcList tcOp is ((ins, Dict) ::& SNil))+  is ins++lamRecImpl+  :: forall it ot ts op .+    ( WellTyped it, WellTyped ot+    , SingI ts+    , IsInstrOp op+    )+  => TcInstrBase op+  -> LamTC it ot ts op+lamRecImpl tcOp is ins ons = lamCommon AnnLAMBDA_REC+  (giveNotInView $+      local (set tcieNotInView $ Just Dict) $+        tcList tcOp is ((ins, Dict) ::& (STLambda ins ons, Dict) ::& SNil))+  is ins ons++lamCommon+  :: forall it ot ts op inp .+    ( WellTyped it, WellTyped ot+    , SingI ts+    , IsInstrOp op+    )+  => (Anns '[VarAnn, Notes it, Notes ot] -> RemFail Instr inp '[ot] -> Instr ts ('TLambda it ot : ts))+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)+  -> LamTC it ot ts op+lamCommon tyCon tcInstr is ins ons cons anns instr i =   guarding_ instr     (whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr -> do-      let err = InvalidInstruction selfInstr "SELF instruction cannot be used in a LAMBDA"-      typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) err) $+      let err = InvalidInstruction (void selfInstr) "SELF instruction cannot be used in a LAMBDA"+      typeCheckInstrErr' instr (SomeHST i) (Just LambdaCodeCtx) err) $     preserving tcInstr cons $ \(_ :/ lamI) -> do       let lamNotes onsr = STLambda ins onsr       let lamSt onsr = (lamNotes onsr, Dict) ::& i@@ -1777,44 +1903,67 @@         lam ::: lo -> do           case eqHST1 @ot lo of             Right Refl -> do-                pure (AnnLAMBDA anns (VLam $ RfNormal lam) ::: lamSt ons)-            Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) m+                pure (tyCon anns (RfNormal lam) ::: lamSt ons)+            Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCodeCtx) m         AnyOutInstr lam ->-          pure (AnnLAMBDA anns (VLam $ RfAlwaysFails lam) ::: lamSt ons)+          pure (tyCon anns (RfAlwaysFails lam) ::: lamSt ons)   where-    tcInstr = giveNotInView $ local (set tcieNotInView $ Just Dict) $ tcList is ((ins, Dict) ::& SNil)-    hasSelf :: U.ExpandedOp -> First U.ExpandedInstr+    hasSelf :: op -> First (U.InstrAbstract op)     hasSelf = everything (<>)       (mkQ (First Nothing)        (\case-           selfInstr@(U.SELF{} :: U.InstrAbstract U.ExpandedOp) -> First $ Just selfInstr+           selfInstr@(U.SELF{} :: U.InstrAbstract op) -> First $ Just selfInstr            _ -> First Nothing        )       ) +typeCheckExpandedOp :: TcInstrBase U.ExpandedOp+typeCheckExpandedOp = \case+  U.WithSrcEx _ op@U.WithSrcEx{} -> typeCheckExpandedOp op+  U.WithSrcEx loc (U.PrimEx op)  -> typeCheckPrimWithLoc loc op+  U.WithSrcEx loc (U.SeqEx sq)   -> typeCheckSeqWithLoc loc sq+  U.PrimEx op                    -> typeCheckPrim op+  U.SeqEx sq                     -> typeCheckSeq sq+  where+    -- If we know source location from the untyped instruction, keep it in the typed one.+    typeCheckPrimWithLoc :: ErrorSrcPos -> TcInstr U.ExpandedOp U.ExpandedInstr+    typeCheckPrimWithLoc loc op hst = local (set tcieErrorPos loc)+      (wrapWithLoc loc <$> typeCheckPrim op hst)++    typeCheckPrim :: TcInstr U.ExpandedOp U.ExpandedInstr+    typeCheckPrim = typeCheckInstr typeCheckExpandedOp++    typeCheckSeqWithLoc :: ErrorSrcPos -> TcInstr U.ExpandedOp [U.ExpandedOp]+    typeCheckSeqWithLoc loc op = fmap (wrapWithLoc loc) . local (set tcieErrorPos loc) . typeCheckSeq op++    typeCheckSeq :: TcInstr U.ExpandedOp [U.ExpandedOp]+    typeCheckSeq sq hst = typeCheckImpl typeCheckExpandedOp sq hst+                      <&> mapSeq (mapSomeInstr Nested)+ ---------------------------------------------------------------------------- -- Helpers for DIP (n) typechecking ----------------------------------------------------------------------------  -- Helper data type we use to typecheck DIPN.-data TCDipHelper inp where+data TCDipHelper op inp where   TCDipHelperOk ::-    forall (n :: Peano) inp out s s'.+    forall (n :: Peano) inp out s s' op.     (SingI out, ConstraintDIPN n inp out s s') =>-    PeanoNatural n -> Instr s s' -> HST out -> TCDipHelper inp-  TCDipHelperErr :: TCError -> [IllTypedInstr] -> TCDipHelper inp+    PeanoNatural n -> Instr s s' -> HST out -> TCDipHelper op inp+  TCDipHelperErr :: TcError' op -> [IllTypedInstr op] -> TCDipHelper op inp  typeCheckDipBody-  :: SingI inp-  => ([TypeCheckedOp] -> TypeCheckedInstr)-  -> U.ExpandedInstr-  -> [U.ExpandedOp]+  :: (SingI inp, IsInstrOp op)+  => TcInstrBase op+  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)+  -> U.InstrAbstract op+  -> [op]   -> HST inp-  -> (TCError -> [IllTypedInstr] -> r)+  -> (TcError' op -> [IllTypedInstr op] -> r)   -> (forall out. SingI out => Instr inp out -> HST out -> r)-  -> TypeCheckInstrNoExcept r-typeCheckDipBody cons mainInstr instructions inputHST onErr onOk = do-  listRes <- tcList instructions inputHST+  -> TypeCheckInstrNoExcept op r+typeCheckDipBody tcOp cons mainInstr instructions inputHST onErr onOk = do+  listRes <- tcList tcOp instructions inputHST   pos <- view tcieErrorPos   pure $ listRes & tcsEither     (\tcOps err -> onErr err [SemiTypedInstr $ cons tcOps])@@ -1825,7 +1974,7 @@         -- if output stack of code block within @DIP@ occurs to be any, an         -- error "FAILWITH must be at tail position" is raised.         -- It is not allowed even in `DIP 0`.-          let err = TCFailedOnInstr mainInstr+          let err = TcFailedOnInstr mainInstr                                     (SomeHST inputHST)                                     pos                                     (Just DipCode)

@@ -2,7 +2,8 @@ -- SPDX-License-Identifier: LicenseRef-MIT-OA  module Morley.Michelson.TypeCheck.TypeCheck-  ( TcInstrHandler+  ( TcInstr+  , TcInstrBase   , TcOriginatedContracts   , TypeCheckEnv(..)   , BigMapFinder@@ -16,7 +17,8 @@   , runTypeCheckIsolated   , typeCheckingWith   , liftNoExcept-  , throwingTCError+  , throwingTcError+  , IsInstrOp (..)   , preserving   , preserving'   , guarding@@ -38,11 +40,13 @@ import Control.Lens (makeLenses) import Control.Monad.Except (Except, MonadError, runExcept, throwError) import Data.Constraint (Dict)+import Data.Data (Data) import Data.Default (Default(..))-import Fmt (Buildable, build, pretty)+import Data.Singletons (demote)+import Fmt (Buildable, build)  import Morley.Michelson.ErrorPos (ErrorSrcPos)-import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))+import Morley.Michelson.TypeCheck.Error (TcError'(..), TcTypeError(..)) import Morley.Michelson.TypeCheck.TypeCheckedSeq   (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp,   tcsEither)@@ -55,32 +59,32 @@ import Morley.Util.MultiReader  -- | Environments avaliable during typecheck.-type TCEnvs = '[TypeCheckEnv, TypeCheckOptions]+type TCEnvs op = '[TypeCheckEnv op, TypeCheckOptions]  -- | A full type-check monad carrying intermediary context (via 'TypeCheckEnv'),--- general 'TypeCheckOptions' and throwing 'TCError'.-type TypeCheck = MultiReaderT TCEnvs (Except TCError)+-- general 'TypeCheckOptions' and throwing 'TcError\''.+type TypeCheck op = MultiReaderT (TCEnvs op) (Except (TcError' op))  -- | A non-throwing alternative for 'TypeCheck'. Mainly meant to be used for -- construction of a partially typed tree (see 'TypeCheckedSeq').-type TypeCheckNoExcept = MultiReaderT TCEnvs Identity+type TypeCheckNoExcept op = MultiReaderT (TCEnvs op) Identity  -- | Monad for performing some typechecking operations with the same options. -- -- Unlike 'TypeCheck' monad, this does not carry the context of intra-contract -- or intra-value typechecking.-type TypeCheckResult = ReaderT TypeCheckOptions (Except TCError)+type TypeCheckResult op = ReaderT TypeCheckOptions (Except (TcError' op))  -- | Environments available during instr typecheck-type TCInstrEnvs = TypeCheckInstrEnv ': TCEnvs+type TCInstrEnvs op = TypeCheckInstrEnv ': TCEnvs op  -- | Version of 'TypeCheck' additionally carrying instruction-specific -- 'TypeCheckInstrEnv'-type TypeCheckInstr = MultiReaderT TCInstrEnvs (Except TCError)+type TypeCheckInstr op = MultiReaderT (TCInstrEnvs op) (Except (TcError' op))  -- | Version of 'TypeCheckNoExcept' additionally carrying instruction-specific -- 'TypeCheckInstrEnv'-type TypeCheckInstrNoExcept = MultiReaderT TCInstrEnvs Identity+type TypeCheckInstrNoExcept op = MultiReaderT (TCInstrEnvs op) Identity  data SomeParamType = forall t. (T.ParameterScope t) =>   SomeParamType (T.ParamNotes t)@@ -102,25 +106,22 @@ someParamToParameterType (SomeParamType T.UnsafeParamNotes{..}) =   U.ParameterType (T.AsUType pnNotes) pnRootAnn -mkSomeParamType :: U.ParameterType -> Either TCError SomeParamType-mkSomeParamType (U.ParameterType t ann) =-  T.withUType t $ \(notescp :: T.Notes t) -> do-    case T.checkScope @(T.ParameterScope t) of-      Right T.Dict ->-        case T.mkParamNotes notescp ann of-          Right paramNotes -> Right $ SomeParamType paramNotes-          Left err ->-            Left $ TCContractError "invalid parameter declaration: " $ Just $ IllegalParamDecl err-      Left err -> Left $ TCContractError ("Parameter type is invalid: " <> pretty err) Nothing+mkSomeParamType :: U.ParameterType -> Either TcTypeError SomeParamType+mkSomeParamType (U.ParameterType (T.AsUType (notescp :: T.Notes t)) ann) = do+  T.Dict <- T.checkScope @(T.ParameterScope t)+    & first (UnsupportedTypeForScope (demote @t))+  paramNotes <- T.mkParamNotes notescp ann+    & first IllegalParamDecl+  return $ SomeParamType paramNotes  type TcOriginatedContracts = Map ContractHash SomeParamType  -- | Typechecking mode that tells the type checker whether it is typechecking -- contract code in actual contract, lambda, or test.-data TypeCheckMode+data TypeCheckMode op   = TypeCheckValue     -- ^ We're typechecking a value.-      (U.Value, T.T)+      (U.Value' op, T.T)       (Maybe BigMapFinder)       -- ^ When this is a `Just`, we simulate the typechecking behavior of the RPC's @/run_code@ endpoint.       --@@ -135,8 +136,8 @@     -- where the instruction @SELF@ would not make sense.  -- | The typechecking state-data TypeCheckEnv = TypeCheckEnv-  { tcMode :: ~TypeCheckMode+data TypeCheckEnv op = TypeCheckEnv+  { tcMode :: ~(TypeCheckMode op)   }  type BigMapFinder = Natural -> Maybe SomeVBigMap@@ -144,13 +145,13 @@ data TypeCheckOptions = TypeCheckOptions   { tcVerbose :: Bool     -- ^ Whether to add stack type comments after every-    -- instruction a la tezos-client.+    -- instruction a la @octez-client@.   , tcStrict :: Bool     -- ^ Whether should we behave like in test run or real run     -- (real run is more strict).     ---    -- @tezos-client run@'s behaviour can slightly differ from the behaviour-    -- of @tezos-client originate@ and @tezos-client transfer@. For instance,+    -- @octez-client run@'s behaviour can slightly differ from the behaviour+    -- of @octez-client originate@ and @octez-client transfer@. For instance,     -- some values can be "forged" in test run, but not in a real one,     -- see: Note [Tickets forging].     --@@ -170,7 +171,7 @@ makeLensesWith postfixLFields ''TypeCheckEnv makeLenses ''TypeCheckInstrEnv -runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a+runTypeCheck :: TypeCheckMode op -> TypeCheck op a -> TypeCheckResult op a runTypeCheck = usingReaderT . TypeCheckEnv  -- | Run type checker as if it worked isolated from other world -@@ -181,10 +182,10 @@ -- whatever we typecheck does not depend on the parameter type of the -- contract which is being typechecked (because there is no contract -- that we are typechecking).-runTypeCheckIsolated :: TypeCheck (SomeInstr t) -> TypeCheckResult (SomeInstr t)+runTypeCheckIsolated :: TypeCheck op (SomeTcInstr t) -> TypeCheckResult op (SomeTcInstr t) runTypeCheckIsolated = runTypeCheck TypeCheckTest -typeCheckingWith :: TypeCheckOptions -> TypeCheckResult a -> Either TCError a+typeCheckingWith :: TypeCheckOptions -> TypeCheckResult op a -> Either (TcError' op) a typeCheckingWith options = runExcept . usingReaderT options  instance Default TypeCheckInstrEnv where@@ -196,32 +197,82 @@   -> ChangeMultiReaderBase m (Except e) a liftNoExcept action = mapMultiReaderT (pure @(Except e) . runIdentity) action -throwingTCError-  :: ( MonadMultiReaderT m Identity-     , m' ~ ChangeMultiReaderBase m (Except TCError)-     , MonadError TCError m'+throwingTcError+  :: forall op inp m m'.+     ( MonadMultiReaderT m Identity+     , m' ~ ChangeMultiReaderBase m (Except (TcError' op))+     , MonadError (TcError' op) m'      )-  => m (TypeCheckedSeq inp) -> m' (SomeInstr inp)-throwingTCError action = liftNoExcept @_ @TCError action >>= tcsEither (const throwError) (pure)+  => m (TypeCheckedSeq op inp) -> m' (SomeTcInstr inp)+throwingTcError action = liftNoExcept @_ @(TcError' op) action >>= tcsEither (const throwError) (pure)  tcEither-  :: (TCError -> TypeCheckInstrNoExcept a) -- ^ Call this if the action throws-  -> (b -> TypeCheckInstrNoExcept a) -- ^ Call this if it doesn't-  -> TypeCheckInstr b -- ^ The action to perform-  -> TypeCheckInstrNoExcept a -- ^ A non-throwing action+  :: (TcError' op -> TypeCheckInstrNoExcept op a) -- ^ Call this if the action throws+  -> (b -> TypeCheckInstrNoExcept op a) -- ^ Call this if it doesn't+  -> TypeCheckInstr op b -- ^ The action to perform+  -> TypeCheckInstrNoExcept op a -- ^ A non-throwing action tcEither onErr onOk action = either onErr onOk =<< mapMultiReaderT (pure . runExcept) action +-- | Operation types that appear in @AbstractInstr@.+--+-- 'Data' superclass constraint is used to search for particular sub-instructions.+class Data op => IsInstrOp op where+  -- | Lift a single instruction to operation.+  --+  -- This is used only in error messages.+  liftInstr :: U.InstrAbstract op -> op++  -- | Get callstack at this instruction, if any given.+  --+  -- This is used only in error messages.+  pickErrorSrcPos :: op -> Maybe ErrorSrcPos++  -- | Do our best to re-interpret an instruction as a value.+  --+  -- For instance, @{ {}, {} }@ may turn out to be represented both as nested+  -- @SeqEx@s and as nested @ValueList@ & @ValueNil@s.+  -- This function, along with 'tryValToOp', let us convert between these+  -- two forms.+  --+  -- TODO [#785]: try to remove these two functions+  tryOpToVal :: op -> Maybe (U.Value' op)++  -- | Do our best to re-interpret a value as an instruction.+  --+  -- This does the opposite to 'tryOpToVal'.+  --+  -- If a value is already a lambda, this can return 'Nothing'.+  tryValToOp :: U.Value' op -> Maybe op++instance IsInstrOp U.ExpandedOp where+  liftInstr = U.PrimEx++  pickErrorSrcPos = \case+    U.WithSrcEx cs _ -> Just cs+    _ -> Nothing++  tryOpToVal = \case+    U.SeqEx []      -> Just U.ValueNil+    U.SeqEx xs      -> U.ValueSeq . fromList <$> traverse tryOpToVal xs+    U.PrimEx {}     -> Nothing+    U.WithSrcEx _ i -> tryOpToVal i++  tryValToOp = \case+    U.ValueNil      -> Just $ U.SeqEx []+    U.ValueSeq xs   -> U.SeqEx . toList <$> traverse tryValToOp xs+    _               -> Nothing+ -- | Perform a throwing action on an acquired instruction. Preserve the acquired -- result by embedding it into a type checking tree with a specified parent -- instruction. preserving-  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)+  :: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)   -- ^ Acquiring computation-  -> ([TypeCheckedOp] -> TypeCheckedInstr)+  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)   -- ^ The parent instruction constructor-  -> (SomeInstr inp -> TypeCheckInstr (SomeInstr inp'))+  -> (SomeTcInstr inp -> TypeCheckInstr op (SomeTcInstr inp'))   -- ^ The throwing action-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp') preserving acquire con action = preserving' acquire con   (\instr -> action instr & tcEither     (\err -> pure $ IllTypedSeq err [SemiTypedInstr $ con [someInstrToOp instr]])@@ -231,13 +282,13 @@ -- acquired result even if the action does not succeed. Embed the result into a -- type checking tree with a specified parent instruction. preserving'-  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp)+  :: TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)   -- ^ Acquiring computation-  -> ([TypeCheckedOp] -> TypeCheckedInstr)+  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)   -- ^ The parent instruction constructor-  -> (SomeInstr inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp'))+  -> (SomeTcInstr inp -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp'))   -- ^ The action-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp')+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp') preserving' acquire con action =   acquire >>= tcsEither     (\tcOps err -> pure $ IllTypedSeq err [SemiTypedInstr $ con tcOps])@@ -247,31 +298,37 @@ -- otherwise embed the error into a type checking tree along with a specified -- untyped instruction. guarding-  :: U.ExpandedInstr -- ^ Untyped instruction-  -> TypeCheckInstr a -- ^ Acquiring computation-  -> (a -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)) -- ^ Follow-up action-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+  :: IsInstrOp op+  => U.InstrAbstract op -- ^ Untyped instruction+  -> TypeCheckInstr op a -- ^ Acquiring computation+  -> (a -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)) -- ^ Follow-up action+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) guarding instr cond action = do   cond & tcEither-    (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx instr])+    (\err -> pure $ IllTypedSeq err [NonTypedInstr $ liftInstr instr])     (action)  -- | Same as @guarding@ but doesn't pass an acquired result to a follow-up -- action. guarding_-  :: U.ExpandedInstr-  -> TypeCheckInstr a-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)-  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+  :: IsInstrOp op+  => U.InstrAbstract op+  -> TypeCheckInstr op a+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)+  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp) guarding_ instr cond action = guarding instr cond (const action) --- pva701: it's really painful to add arguments to TcInstrHandler--- due to necessity to refactor @typeCheckInstr@.--- Also functions which are being called from @typeCheckInstr@ would--- have to be refactored too.--- Therefore, I am using ReaderT over TypeCheck.-type TcInstrHandler+-- | Some type checker function.+--+-- It accepts untyped instructions to typecheck as @instr@ value, and @op@ type+-- stands for the basic operation type like @ExpandedOp@.+type TcInstr op instr    = forall inp. (T.SingI inp)-      => U.ExpandedInstr+      => instr       -> HST inp-      -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)+      -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)++-- | Type checker function for the operation like @ExpandedOp@.+-- Function of this type we carry in most of the other functions to let+-- them recurse.+type TcInstrBase op = TcInstr op op

@@ -14,58 +14,59 @@ import Data.Singletons (SingI)  import Morley.Michelson.Printer.Util (RenderDoc(..), renderOpsListNoBraces)-import Morley.Michelson.TypeCheck.Types (HST(..), SomeInstr(..), SomeInstrOut(..))+import Morley.Michelson.TypeCheck.Types (HST(..), SomeTcInstr(..), SomeTcInstrOut(..)) import Morley.Michelson.Typed.Aliases import Morley.Michelson.Typed.Convert (instrToOps) import Morley.Michelson.Typed.Instr (Instr, castInstr) import Morley.Michelson.Typed.View (SomeView'(..), View'(..)) import Morley.Michelson.Untyped qualified as U-import Morley.Michelson.Untyped.Instr (ExpandedOp, InstrAbstract(..))+import Morley.Michelson.Untyped.Instr (InstrAbstract(..)) import Morley.Util.TH (deriveGADTNFData)  -- | Represents a root of a partially typed operation tree.-type TypeCheckedInstr = InstrAbstract TypeCheckedOp+type TypeCheckedInstr op = InstrAbstract (TypeCheckedOp op)  -- | Represents nodes of a partially typed operation tree.-data TypeCheckedOp where+data TypeCheckedOp op where   -- | Constructs well-typed node.-  WellTypedOp :: (SingI inp, SingI out) => Instr inp out -> TypeCheckedOp+  WellTypedOp :: (SingI inp, SingI out) => Instr inp out -> TypeCheckedOp op   -- | Constructs ill-typed node which might in turn contain well-typed and   -- non-typed operations.-  IllTypedOp :: IllTypedInstr -> TypeCheckedOp+  IllTypedOp :: IllTypedInstr op -> TypeCheckedOp op -deriving stock instance Show TypeCheckedOp+deriving stock instance Show op => Show (TypeCheckedOp op)+deriving stock instance Functor TypeCheckedOp -instance Eq TypeCheckedOp where+instance Eq op => Eq (TypeCheckedOp op) where   WellTypedOp i1 == WellTypedOp i2 = castInstr i1 == Just i2   IllTypedOp i1 == IllTypedOp i2 = i1 == i2   _ == _ = False  -- | Represents a non-well-typed operation-data IllTypedInstr-  = SemiTypedInstr TypeCheckedInstr -- ^ Constructs a partialy typed operation.-  | NonTypedInstr ExpandedOp  -- ^ Constructs a completely untyped operation.-  deriving stock (Show, Eq, Generic)+data IllTypedInstr op+  = SemiTypedInstr (TypeCheckedInstr op) -- ^ Constructs a partialy typed operation.+  | NonTypedInstr op  -- ^ Constructs a completely untyped operation.+  deriving stock (Show, Eq, Generic, Functor) -deriving anyclass instance NFData TypeCheckedOp => NFData IllTypedInstr+deriving anyclass instance (NFData (TypeCheckedOp op), NFData op) => NFData (IllTypedInstr op) -instance RenderDoc TypeCheckedOp where+instance RenderDoc op => RenderDoc (TypeCheckedOp op) where   renderDoc _ (WellTypedOp instr) = renderOpsListNoBraces False (instrToOps instr)   renderDoc pn (IllTypedOp (SemiTypedInstr instr)) = renderDoc pn instr   renderDoc pn (IllTypedOp (NonTypedInstr op)) = renderDoc pn op --- | Makes a well-typed node out of `SomeInstr`-someInstrToOp :: SomeInstr inp -> TypeCheckedOp+-- | Makes a well-typed node out of `SomeTcInstr`+someInstrToOp :: SomeTcInstr inp -> TypeCheckedOp op someInstrToOp (hst :/ rest) = case hst of   SNil -> go rest   (::&){} -> go rest   where-    go :: forall inp. SingI inp => SomeInstrOut inp -> TypeCheckedOp+    go :: SingI inp => SomeTcInstrOut inp -> TypeCheckedOp op     go (i ::: _) = WellTypedOp i     go (AnyOutInstr i) = WellTypedOp (i @'[])  -- | Makes a view with well-typed code, taking the untyped and typechecked view.-someViewToOp :: U.View' op -> SomeView st -> U.View' TypeCheckedOp+someViewToOp :: U.View' op -> SomeView st -> U.View' (TypeCheckedOp op) someViewToOp U.View{..} (SomeView View{..}) = U.View   { U.viewCode = [WellTypedOp vCode]   , ..

@@ -6,7 +6,7 @@ -- -- It is needed to represent the fact that there can only be one well-typed node -- in a sequence and it is the first one. Also, it serves its role to remove--- @TCError@ usage from @TypeCheckedOp@.+-- @TcError@ usage from @TypeCheckedOp@. module Morley.Michelson.TypeCheck.TypeCheckedSeq   ( TypeCheckedInstr   , TypeCheckedOp(..)@@ -18,21 +18,21 @@   , someViewToOp   ) where -import Morley.Michelson.TypeCheck.Error (TCError)+import Morley.Michelson.TypeCheck.Error (TcError') import Morley.Michelson.TypeCheck.TypeCheckedOp   (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), someInstrToOp, someViewToOp)-import Morley.Michelson.TypeCheck.Types (SomeInstr(..))+import Morley.Michelson.TypeCheck.Types (SomeTcInstr(..))  -- | Represents a partiall typed sequence of instructions.-data TypeCheckedSeq inp+data TypeCheckedSeq op inp   -- | A fully well-typed sequence.-  = WellTypedSeq (SomeInstr inp)+  = WellTypedSeq (SomeTcInstr inp)   -- | A well-typed prefix followed by some error and semi-typed instructions.-  | MixedSeq (SomeInstr inp) TCError [IllTypedInstr]+  | MixedSeq (SomeTcInstr inp) (TcError' op) [IllTypedInstr op]   -- | There is no well-typed prefix, only an error and semi-typed instructions.-  | IllTypedSeq TCError [IllTypedInstr]+  | IllTypedSeq (TcError' op) [IllTypedInstr op] -seqToOps :: TypeCheckedSeq inp -> [TypeCheckedOp]+seqToOps :: TypeCheckedSeq op inp -> [TypeCheckedOp op] seqToOps = \case   WellTypedSeq instr -> [someInstrToOp instr]   MixedSeq instr _ tail' -> someInstrToOp instr : map IllTypedOp tail'@@ -40,10 +40,10 @@  -- | Case analysis for @TypeCheckedSeq@. tcsEither-  :: ([TypeCheckedOp] -> TCError -> a)+  :: ([TypeCheckedOp op] -> TcError' op -> a)      -- ^ On error, with all already typechecked operations-  -> (SomeInstr inp -> a) -- ^ On well-typed instruction-  -> TypeCheckedSeq inp -- ^ The sequence to dispatch on+  -> (SomeTcInstr inp -> a) -- ^ On well-typed instruction+  -> TypeCheckedSeq op inp -- ^ The sequence to dispatch on   -> a tcsEither onErr onInstr v = case v of   WellTypedSeq instr -> onInstr instr

@@ -5,8 +5,8 @@     ( HST (..)     , (-:&)     , SomeHST (..)-    , SomeInstrOut (..)-    , SomeInstr (..)+    , SomeTcInstrOut (..)+    , SomeTcInstr (..)     , BoundVars (..)     , withWTPm     , unsafeWithWTP@@ -109,7 +109,7 @@  -- | This data type keeps part of type check result - instruction and -- corresponding output stack.-data SomeInstrOut inp where+data SomeTcInstrOut inp where   -- | Type-check result with concrete output stack, most common case.   --   -- Output stack type is wrapped inside the type and @Typeable@@@ -118,7 +118,7 @@     :: SingI out     => Instr inp out     -> HST out-    -> SomeInstrOut inp+    -> SomeTcInstrOut inp    -- | Type-check result which matches against arbitrary output stack.   -- Information about annotations in the output stack is absent.@@ -129,37 +129,37 @@   -- lambda and immediatelly execute it - stack type is known).   AnyOutInstr     :: (forall out. Instr inp out)-    -> SomeInstrOut inp+    -> SomeTcInstrOut inp infix 9 ::: -deriving stock instance Show (SomeInstrOut inp)+deriving stock instance Show (SomeTcInstrOut inp) -instance Buildable (SomeInstrOut inp) where+instance Buildable (SomeTcInstrOut inp) where   build (i ::: out) = i |+ " :: " +| build out   build (AnyOutInstr i) = i |+ " :: *"  -- | Data type keeping the whole type check result: instruction and -- type representations of instruction's input and output.-data SomeInstr inp where-  (:/) :: HST inp -> SomeInstrOut inp -> SomeInstr inp+data SomeTcInstr inp where+  (:/) :: HST inp -> SomeTcInstrOut inp -> SomeTcInstr inp infix 8 :/ -deriving stock instance Show (SomeInstr inp)+deriving stock instance Show (SomeTcInstr inp)  mapSomeInstrOut   :: (forall out. Instr inp out -> Instr inp' out)-  -> SomeInstrOut inp-  -> SomeInstrOut inp'+  -> SomeTcInstrOut inp+  -> SomeTcInstrOut inp' mapSomeInstrOut f (i ::: out) = f i ::: out mapSomeInstrOut f (AnyOutInstr i) = AnyOutInstr (f i)  mapSomeInstr   :: (forall out. Instr inp out -> Instr inp out)-  -> SomeInstr inp-  -> SomeInstr inp+  -> SomeTcInstr inp+  -> SomeTcInstr inp mapSomeInstr f (inp :/ instrAndOut) = inp :/ mapSomeInstrOut f instrAndOut -instance Buildable (SomeInstr inp) where+instance Buildable (SomeTcInstr inp) where   build (inp :/ out) = inp |+ " -> " +| build out  mapSomeContract ::

@@ -17,7 +17,7 @@ import Prelude hiding (EQ, GT, LT)  import Morley.Michelson.Text-import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))+import Morley.Michelson.TypeCheck.Error (TcError'(..), TcTypeError(..)) import Morley.Michelson.TypeCheck.Helpers import Morley.Michelson.TypeCheck.TypeCheck import Morley.Michelson.TypeCheck.Types@@ -33,10 +33,10 @@ import Morley.Tezos.Crypto.Timelock (chestFromBytes, chestKeyFromBytes) import Morley.Util.Type (onFirst) -tcFailedOnValue :: U.Value -> T.T -> Text -> Maybe TCTypeError -> TypeCheckInstr a+tcFailedOnValue :: U.Value' op -> T.T -> Text -> Maybe TcTypeError -> TypeCheckInstr op a tcFailedOnValue v t msg err = do   loc <- view tcieErrorPos-  throwError $ TCFailedOnValue v t msg loc err+  throwError $ TcFailedOnValue v t msg loc err  -- | Function @typeCheckValImpl@ converts a single Michelson value -- given in representation from @Morley.Michelson.Type@ module to representation@@ -55,17 +55,17 @@ -- should contain the originated contracts when typechecking a parameter and -- 'Nothing' otherwise. typeCheckValImpl-  :: forall ty.-     SingI ty+  :: forall ty op.+     (SingI ty, IsInstrOp op)   => Maybe TcOriginatedContracts-  -> TcInstrHandler-  -> U.Value-  -> TypeCheckInstr (T.Value ty)+  -> TcInstrBase op+  -> U.Value' op+  -> TypeCheckInstr op (T.Value ty) typeCheckValImpl mOriginatedContracts tcDo uv = doTypeCheckVal (uv, sing @ty)   where-    doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)+    doTypeCheckVal :: forall tz. (U.Value' op, Sing tz) -> TypeCheckInstr op (T.Value tz)     doTypeCheckVal (uvalue, sng) = do-      typeCheckMode <- asks' tcMode+      typeCheckMode <- asks' (tcMode @op)       case (uvalue, sng) of         (U.ValueInt i, STInt) -> pure $ T.VInt i         (v@(U.ValueInt i), t@STNat)@@ -157,8 +157,11 @@           -- by design, and the only valid way to make a ticket is calling           -- @TICKET@ instruction.           ---          -- However @tezos-client run@ adds an exception, it allows passing a+          -- However @octez-client run@ adds an exception, it allows passing a           -- manually constructed ticket value as parameter or initial storage.+          --+          -- Since protocol lima zero amount tickets are no longer allowed+          -- event in "lax" mode, so we forbid them here is well. (see !1270)           True ->             tcFailedOnValue cv (fromSing sng)               "ticket values cannot be forged in real operations"@@ -169,6 +172,9 @@               dat <- doTypeCheckVal (datV, vt)               amountValue <- doTypeCheckVal (amV, STNat)               case (addrValue, amountValue) of+                (_, VNat 0) ->+                  tcFailedOnValue cv (fromSing sng) "ticket amount of 0 is not allowed"+                  Nothing                 (VAddress (EpAddress' addr ep), VNat am) -> do                   unless (U.isDefEpName ep) $                     tcFailedOnValue cv (fromSing sng)@@ -218,7 +224,7 @@           instrPos <- view tcieErrorPos           case T.getComparableProofS s of             Just Dict -> withSingI s $ pure (T.VSet S.empty)-            Nothing -> throwError $ TCFailedOnValue uvalue (fromSing s) "Non comparable types are not allowed in Sets"+            Nothing -> throwError $ TcFailedOnValue uvalue (fromSing s) "Non comparable types are not allowed in Sets"               instrPos (Just $ UnsupportedTypeForScope (fromSing s) T.BtNotComparable)          (sq@(U.ValueSeq (toList -> mels)), s@(STSet vt)) -> withComparable vt sq s $ do@@ -226,7 +232,7 @@            els <- typeCheckValsImpl (mels, vt)           elsS <- liftEither $ S.fromDistinctAscList <$> ensureDistinctAsc id els-                    `onFirst` \msg -> TCFailedOnValue sq (fromSing vt) msg instrPos Nothing+                    `onFirst` \msg -> TcFailedOnValue sq (fromSing vt) msg instrPos Nothing           withSingI vt $ pure $ VSet elsS          (v@U.ValueNil, s@(STMap st vt)) ->@@ -250,12 +256,12 @@          -- `{ {} }` can be typechecked either as `VLam` or `VList`.         (U.ValueLambda s, STList l) ->-          case emptyLambdaAsList s of-            Just xs -> doTypeCheckVal (xs, sng)+          case traverse tryOpToVal s of+            Just xs -> doTypeCheckVal (U.ValueSeq xs, sng)             Nothing -> tcFailedOnValue uvalue (fromSing l) "" Nothing -        (U.ValueSeq s, STLambda _ _) -> case emptyListAsLambda s of-          Just xs -> doTypeCheckVal (xs, sng)+        (U.ValueSeq s, STLambda _ _) -> case traverse tryValToOp s of+          Just xs -> doTypeCheckVal (U.ValueLambda xs, sng)           Nothing -> tcFailedOnValue uvalue (fromSing sng) "" Nothing          (v, STLambda (var :: Sing it) (b :: Sing ot)) -> withSingI var $ withSingI b $ do@@ -264,7 +270,7 @@             U.ValueLambda mp -> pure $ toList mp             _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing           _ :/ instr <--            withWTP @it uvalue $ throwingTCError $+            withWTP @it uvalue $ throwingTcError $               typeCheckImpl                 -- lambdas can contain operations forbidden inside views, hence                 -- we invent a "not in view" constraint here.@@ -282,12 +288,17 @@             AnyOutInstr lam ->               pure $ T.mkVLam (T.RfAlwaysFails lam) -        (v@(U.ValueBytes (U.InternalByteString bs)), STChest) ->+        (v@(U.ValueBytes (U.InternalByteString bs)), STChest) -> do+          isStrict <- asks' tcStrict+          when isStrict $ tcFailedOnValue v T.TChest "chest type temporarily deprecated" Nothing           case chestFromBytes bs of             Right res -> pure $ VChest res             Left err -> tcFailedOnValue v T.TChest err Nothing -        (v@(U.ValueBytes (U.InternalByteString bs)), STChestKey) ->+        (v@(U.ValueBytes (U.InternalByteString bs)), STChestKey) -> do+          isStrict <- asks' tcStrict+          when isStrict $+            tcFailedOnValue v T.TChestKey "chest_key type temporarily deprecated" Nothing           case chestKeyFromBytes bs of             Right res -> pure $ VChestKey res             Left err -> tcFailedOnValue v T.TChestKey err Nothing@@ -300,49 +311,22 @@          (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing -    seqToRightCombedPair :: (NonEmpty $ U.Value) -> U.Value+    seqToRightCombedPair :: (NonEmpty $ U.Value' op) -> U.Value' op     seqToRightCombedPair (x :| [y]) = U.ValuePair x y     seqToRightCombedPair (x :| xs) = U.ValuePair x $ seqToRightCombedPair (NE.fromList xs) -    -- Converts a lambda containing only empty 'SeqEx's (possibly nested)-    -- to a list of empty lists.-    emptyLambdaAsList :: NonEmpty U.ExpandedOp -> Maybe U.Value-    emptyLambdaAsList ops =-      let-        opToMaybeList :: U.ExpandedOp -> Maybe U.Value-        opToMaybeList = \case-          U.SeqEx []      -> Just U.ValueNil-          U.SeqEx xs      -> U.ValueSeq . NE.fromList <$> traverse opToMaybeList xs-          U.PrimEx {}     -> Nothing-          U.WithSrcEx _ i -> opToMaybeList i-      in-        U.ValueSeq <$> traverse opToMaybeList ops--    -- Converts a list containing only empty lists (possibly nested)-    -- to a lambda of empty 'SeqEx's.-    emptyListAsLambda :: NonEmpty U.Value -> Maybe U.Value-    emptyListAsLambda ops =-      let-        listToMaybeOp :: U.Value -> Maybe U.ExpandedOp-        listToMaybeOp = \case-          U.ValueNil      -> Just $ U.SeqEx []-          U.ValueSeq xs   -> U.SeqEx . toList <$> traverse listToMaybeOp xs-          _               -> Nothing-      in-        U.ValueLambda <$> traverse listToMaybeOp ops-     withWTP       :: forall t a. SingI t-      => U.Value-      -> (T.WellTyped t => TypeCheckInstr a)-      -> TypeCheckInstr a+      => U.Value' op+      -> (T.WellTyped t => TypeCheckInstr op a)+      -> TypeCheckInstr op a     withWTP uvalue fn = case T.getWTP @t of       Right Dict -> fn       Left err -> tcFailedOnValue uvalue (demote @ty) (pretty err) Nothing      typeCheckValsImpl-      :: ([U.Value], Sing t)-      -> TypeCheckInstr [T.Value t]+      :: ([U.Value' op], Sing t)+      -> TypeCheckInstr op [T.Value t]     typeCheckValsImpl (mvs, sng) =       fmap reverse $ foldM (\res mv -> (: res) <$> (doTypeCheckVal (mv, sng))) [] mvs @@ -351,31 +335,31 @@     -- It return list of pairs (key, value) with keys in ascending order     -- so it is safe to call @fromDistinctAscList@ on returned list     typeCheckMapVal-      :: [U.Elt U.ExpandedOp]-      -> U.Value+      :: [U.Elt op]+      -> U.Value' op       -> Sing kt       -> Sing vt-      -> TypeCheckInstr [(T.Value kt, T.Value vt)]+      -> TypeCheckInstr op [(T.Value kt, T.Value vt)]     typeCheckMapVal mels sq kt vt = withComparable kt sq kt $ do       instrPos <- view tcieErrorPos       ks <- typeCheckValsImpl (map (\(U.Elt k _) -> k) mels, kt)       vals <- typeCheckValsImpl (map (\(U.Elt _ v) -> v) mels, vt)       ksS <- liftEither $ ensureDistinctAsc id ks-            `onFirst` \msg -> TCFailedOnValue sq (fromSing kt) msg instrPos Nothing+            `onFirst` \msg -> TcFailedOnValue sq (fromSing kt) msg instrPos Nothing       pure $ zip ksS vals      typecheckContractValue       :: forall cp tz. (tz ~ 'T.TContract cp)-      => U.Value -> EpAddress -> Sing cp -> TypeCheckInstr (T.Value tz)+      => U.Value' op -> EpAddress -> Sing cp -> TypeCheckInstr op (T.Value tz)     typecheckContractValue cv (EpAddress addr epName) pc = do        instrPos <- view tcieErrorPos-      let ensureTypeMatches :: forall t'. SingI t' => TypeCheckInstr (cp :~: t')-          ensureTypeMatches = liftEither @_ @TypeCheckInstr $-            first (TCFailedOnValue cv (demote @ty) "wrong contract parameter" instrPos . Just) $+      let ensureTypeMatches :: forall t'. SingI t' => TypeCheckInstr op (cp :~: t')+          ensureTypeMatches = liftEither @_ @(TypeCheckInstr op) $+            first (TcFailedOnValue cv (demote @ty) "wrong contract parameter" instrPos . Just) $               (withSingI pc $ eqType @cp @t')-      let unsupportedType :: T.BadTypeForScope -> TCError-          unsupportedType reason = TCFailedOnValue cv (fromSing pc)+      let unsupportedType :: T.BadTypeForScope -> TcError' op+          unsupportedType reason = TcFailedOnValue cv (fromSing pc)             "Unsupported type in type argument of 'contract' type" instrPos $               Just $ UnsupportedTypeForScope (fromSing pc) reason       case addr of@@ -389,41 +373,41 @@               case T.mkEntrypointCall epName paramNotes of                 Nothing ->                   throwError $-                  TCFailedOnValue cv (demote @ty) "unknown entrypoint" instrPos . Just $+                  TcFailedOnValue cv (demote @ty) "unknown entrypoint" instrPos . Just $                   EntrypointNotFound epName                 Just (T.MkEntrypointCallRes (_ :: Notes t') epc) -> do                   Refl <- ensureTypeMatches @t'                   pure $ VContract (MkAddress addr) (T.SomeEpc epc)             Nothing ->-              throwError $ TCFailedOnValue cv (demote @ty) "Contract literal unknown"+              throwError $ TcFailedOnValue cv (demote @ty) "Contract literal unknown"                 instrPos (Just $ UnknownContract addr)         TxRollupAddress _ ->-          throwError $ TCFailedOnValue cv (demote @ty) "txr1 address passed as contract"+          throwError $ TcFailedOnValue cv (demote @ty) "txr1 address passed as contract"                 instrPos (Just $ TxRollupContract addr)  withComparable-  :: forall a (t :: T.T) ty. Sing a-  -> U.Value+  :: forall a (t :: T.T) ty op. Sing a+  -> U.Value' op   -> Sing t-  -> (T.Comparable a => TypeCheckInstr ty)-  -> TypeCheckInstr ty+  -> (T.Comparable a => TypeCheckInstr op ty)+  -> TypeCheckInstr op ty withComparable s uv t act = case T.getComparableProofS s of   Just Dict -> act   Nothing -> do     instrPos <- view tcieErrorPos     liftEither . Left $-      TCFailedOnValue uv (fromSing t) "Require a comparable type here" instrPos Nothing+      TcFailedOnValue uv (fromSing t) "Require a comparable type here" instrPos Nothing  withBigMapAbsence-  :: forall a (t :: T.T) ty. Sing a-  -> U.Value+  :: forall a (t :: T.T) ty op. Sing a+  -> U.Value' op   -> Sing t-  -> (T.HasNoBigMap a => TypeCheckInstr ty)-  -> TypeCheckInstr ty+  -> (T.HasNoBigMap a => TypeCheckInstr op ty)+  -> TypeCheckInstr op ty withBigMapAbsence s uv t act = case T.bigMapAbsense s of   Just Dict -> act   Nothing -> do     instrPos <- view tcieErrorPos     liftEither . Left $-      TCFailedOnValue uv (fromSing t) "Require a type which doesn't contain `big_map` here"+      TcFailedOnValue uv (fromSing t) "Require a type which doesn't contain `big_map` here"         instrPos Nothing

@@ -38,8 +38,9 @@   ) where  import Data.Bits (complement, shift, (.&.), (.|.))-import Data.Constraint (Dict(..))+import Data.Constraint (Bottom(..), Dict(..)) import Fmt (Buildable(build), (+|), (|+))+import Type.Errors (DelayError) import Unsafe qualified (fromIntegral)  import Morley.Michelson.Typed.Polymorphic@@ -272,16 +273,16 @@   type ArithRes Mul 'TBls12381G2 'TBls12381Fr = 'TBls12381G2   evalOp _ (VBls12381G2 i) (VBls12381Fr j) = Right $ VBls12381G2 (BLS.multiply j i)   commutativityProof = Nothing-instance Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G1 =>+instance (Bottom, Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G1) =>          ArithOp Mul 'TBls12381Fr 'TBls12381G1 where   type ArithRes Mul 'TBls12381Fr 'TBls12381G1 = 'TBls12381G1-  evalOp = error "impossible"-  commutativityProof = error "impossible"-instance Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G2 =>+  evalOp = no+  commutativityProof = no+instance (Bottom, Bls12381MulBadOrder BLS.Bls12381Fr BLS.Bls12381G2) =>          ArithOp Mul 'TBls12381Fr 'TBls12381G2 where   type ArithRes Mul 'TBls12381Fr 'TBls12381G2 = 'TBls12381G2-  evalOp = error "impossible"-  commutativityProof = error "impossible"+  evalOp = no+  commutativityProof = no  instance ArithOp EDiv 'TNat 'TInt where   type ArithRes EDiv 'TNat 'TInt = 'TOption ('TPair (EDivOpRes 'TNat 'TInt) (EModOpRes 'TNat 'TInt))@@ -302,12 +303,11 @@   type ArithRes EDiv 'TMutez 'TNat = 'TOption ('TPair (EDivOpRes 'TMutez 'TNat) (EModOpRes 'TMutez 'TNat))   evalOp _ i j = Right $ evalEDivOp i j -type family Bls12381MulBadOrder a1 a2 where-  Bls12381MulBadOrder a1 a2 = TypeError-    ('Text "Multiplication of "-       ':<>: 'ShowType a2 ':<>: 'Text " and "-       ':<>: 'ShowType a1 ':<>: 'Text " works only other way around"-    )+type Bls12381MulBadOrder a1 a2 = DelayError+  ('Text "Multiplication of "+      ':<>: 'ShowType a2 ':<>: 'Text " and "+      ':<>: 'ShowType a1 ':<>: 'Text " works only other way around"+  )  instance UnaryArithOp Abs 'TInt where   type UnaryArithRes Abs 'TInt = 'TNat

@@ -0,0 +1,24 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++-- | Machinery for typed instruction classification.+module Morley.Michelson.Typed.ClassifiedInstr+  ( withClassifiedInstr+  , ClassifiedInstr(..)++    -- * Classifications+  , NumChildren (..)+  , FailureType (..)+  , IsMichelson (..)+  , HasAnns (..)++    -- * Singletons+  , SingNumChildren (..)+  , SingFailureType (..)+  , SingIsMichelson (..)+  , SingHasAnns (..)+  ) where++import Morley.Michelson.Typed.ClassifiedInstr.Internal.MainImpl+import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types+import Morley.Michelson.Typed.ClassifiedInstr.Internal.WithClassifiedInstr

@@ -0,0 +1,139 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++{-# OPTIONS_HADDOCK not-home #-}++-- | Actual decision implementation for 'HasAnns'.+module Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.HasAnns+  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.HasAnns+  ) where++import Morley.Michelson.Typed.ClassifiedInstr.Internal.InstrEnum+import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types++-- | Decide whether instruction has annotations or not. All annotated+-- instructions should have @Ann@ prefix.+hasAnns :: InstrEnum -> HasAnns+hasAnns = \case+  WithLoc -> DoesNotHaveAnns+  Meta -> DoesNotHaveAnns+  FrameInstr -> DoesNotHaveAnns+  DocGroup -> DoesNotHaveAnns+  Nop -> DoesNotHaveAnns+  Ext -> DoesNotHaveAnns+  Seq -> DoesNotHaveAnns+  Nested -> DoesNotHaveAnns+  IF_NONE -> DoesNotHaveAnns+  IF_LEFT -> DoesNotHaveAnns+  IF_CONS -> DoesNotHaveAnns+  ITER -> DoesNotHaveAnns+  IF -> DoesNotHaveAnns+  LOOP -> DoesNotHaveAnns+  LOOP_LEFT -> DoesNotHaveAnns+  DIP  -> DoesNotHaveAnns+  DIPN  -> DoesNotHaveAnns+  FAILWITH  -> DoesNotHaveAnns+  NEVER  -> DoesNotHaveAnns+  DROP -> DoesNotHaveAnns+  DROPN -> DoesNotHaveAnns+  SWAP -> DoesNotHaveAnns+  DIG -> DoesNotHaveAnns+  DUG -> DoesNotHaveAnns+  UNPAIRN -> DoesNotHaveAnns+  ------------------------+  AnnMAP -> DoesHaveStandardAnns+  AnnCAR -> DoesHaveStandardAnns+  AnnCDR -> DoesHaveStandardAnns+  AnnDUP -> DoesHaveStandardAnns+  AnnDUPN -> DoesHaveStandardAnns+  AnnPUSH -> DoesHaveStandardAnns+  AnnSOME -> DoesHaveStandardAnns+  AnnNONE -> DoesHaveStandardAnns+  AnnUNIT -> DoesHaveStandardAnns+  AnnPAIR -> DoesHaveStandardAnns+  AnnUNPAIR -> DoesHaveStandardAnns+  AnnPAIRN -> DoesHaveStandardAnns+  AnnLEFT -> DoesHaveStandardAnns+  AnnRIGHT -> DoesHaveStandardAnns+  AnnNIL -> DoesHaveStandardAnns+  AnnCONS -> DoesHaveStandardAnns+  AnnSIZE -> DoesHaveStandardAnns+  AnnEMPTY_SET -> DoesHaveStandardAnns+  AnnEMPTY_MAP -> DoesHaveStandardAnns+  AnnEMPTY_BIG_MAP -> DoesHaveStandardAnns+  AnnMEM -> DoesHaveStandardAnns+  AnnGET -> DoesHaveStandardAnns+  AnnGETN -> DoesHaveStandardAnns+  AnnUPDATE -> DoesHaveStandardAnns+  AnnUPDATEN -> DoesHaveStandardAnns+  AnnGET_AND_UPDATE -> DoesHaveStandardAnns+  AnnLAMBDA -> DoesHaveStandardAnns+  AnnLAMBDA_REC -> DoesHaveStandardAnns+  AnnEXEC -> DoesHaveStandardAnns+  AnnAPPLY -> DoesHaveStandardAnns+  AnnCAST -> DoesHaveStandardAnns+  AnnRENAME -> DoesHaveStandardAnns+  AnnPACK -> DoesHaveStandardAnns+  AnnUNPACK -> DoesHaveStandardAnns+  AnnCONCAT -> DoesHaveStandardAnns+  AnnCONCAT' -> DoesHaveStandardAnns+  AnnSLICE -> DoesHaveStandardAnns+  AnnISNAT -> DoesHaveStandardAnns+  AnnADD -> DoesHaveStandardAnns+  AnnSUB -> DoesHaveStandardAnns+  AnnSUB_MUTEZ -> DoesHaveStandardAnns+  AnnMUL -> DoesHaveStandardAnns+  AnnEDIV -> DoesHaveStandardAnns+  AnnABS -> DoesHaveStandardAnns+  AnnNEG -> DoesHaveStandardAnns+  AnnLSL -> DoesHaveStandardAnns+  AnnLSR -> DoesHaveStandardAnns+  AnnOR -> DoesHaveStandardAnns+  AnnAND -> DoesHaveStandardAnns+  AnnXOR -> DoesHaveStandardAnns+  AnnNOT -> DoesHaveStandardAnns+  AnnCOMPARE -> DoesHaveStandardAnns+  AnnEQ -> DoesHaveStandardAnns+  AnnNEQ -> DoesHaveStandardAnns+  AnnLT -> DoesHaveStandardAnns+  AnnGT -> DoesHaveStandardAnns+  AnnLE -> DoesHaveStandardAnns+  AnnGE -> DoesHaveStandardAnns+  AnnINT -> DoesHaveStandardAnns+  AnnVIEW -> DoesHaveStandardAnns+  AnnSELF -> DoesHaveStandardAnns+  AnnCONTRACT -> DoesHaveStandardAnns+  AnnTRANSFER_TOKENS -> DoesHaveStandardAnns+  AnnSET_DELEGATE -> DoesHaveStandardAnns+  AnnCREATE_CONTRACT -> DoesHaveStandardAnns+  AnnIMPLICIT_ACCOUNT -> DoesHaveStandardAnns+  AnnNOW -> DoesHaveStandardAnns+  AnnAMOUNT -> DoesHaveStandardAnns+  AnnBALANCE -> DoesHaveStandardAnns+  AnnVOTING_POWER -> DoesHaveStandardAnns+  AnnTOTAL_VOTING_POWER -> DoesHaveStandardAnns+  AnnCHECK_SIGNATURE -> DoesHaveStandardAnns+  AnnSHA256 -> DoesHaveStandardAnns+  AnnSHA512 -> DoesHaveStandardAnns+  AnnBLAKE2B -> DoesHaveStandardAnns+  AnnSHA3 -> DoesHaveStandardAnns+  AnnKECCAK -> DoesHaveStandardAnns+  AnnHASH_KEY -> DoesHaveStandardAnns+  AnnPAIRING_CHECK -> DoesHaveStandardAnns+  AnnSOURCE -> DoesHaveStandardAnns+  AnnSENDER -> DoesHaveStandardAnns+  AnnADDRESS -> DoesHaveStandardAnns+  AnnCHAIN_ID -> DoesHaveStandardAnns+  AnnLEVEL -> DoesHaveStandardAnns+  AnnSELF_ADDRESS -> DoesHaveStandardAnns+  AnnTICKET -> DoesHaveStandardAnns+  AnnTICKET_DEPRECATED -> DoesHaveStandardAnns+  AnnREAD_TICKET -> DoesHaveStandardAnns+  AnnSPLIT_TICKET -> DoesHaveStandardAnns+  AnnJOIN_TICKETS -> DoesHaveStandardAnns+  AnnOPEN_CHEST -> DoesHaveStandardAnns+  AnnSAPLING_EMPTY_STATE -> DoesHaveStandardAnns+  AnnSAPLING_VERIFY_UPDATE -> DoesHaveStandardAnns+  ------------------------+  AnnMIN_BLOCK_TIME -> DoesHaveNonStandardAnns+  AnnEMIT -> DoesHaveNonStandardAnns

@@ -0,0 +1,138 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++{-# OPTIONS_HADDOCK not-home #-}++-- | Actual decision implementation for 'FailureType'.+module Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsAlwaysFailing+  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsAlwaysFailing+  ) where++import Morley.Michelson.Typed.ClassifiedInstr.Internal.InstrEnum+import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types++-- | Decide whether an instruction is always failing. Only 'NEVER' and+-- 'FAILWITH' are considered always failing.+isAlwaysFailing :: InstrEnum -> FailureType+isAlwaysFailing = \case+  NEVER -> AlwaysFailing+  FAILWITH -> AlwaysFailing+  --------------------+  WithLoc -> FailingNormal+  Meta -> FailingNormal+  FrameInstr -> FailingNormal+  DocGroup -> FailingNormal+  Nop -> FailingNormal+  Ext -> FailingNormal+  Seq -> FailingNormal+  Nested -> FailingNormal+  IF_NONE -> FailingNormal+  IF_LEFT -> FailingNormal+  IF_CONS -> FailingNormal+  AnnMAP -> FailingNormal+  ITER -> FailingNormal+  IF -> FailingNormal+  LOOP -> FailingNormal+  LOOP_LEFT -> FailingNormal+  DIP  -> FailingNormal+  DIPN  -> FailingNormal+  DROP -> FailingNormal+  DROPN -> FailingNormal+  SWAP -> FailingNormal+  DIG -> FailingNormal+  DUG -> FailingNormal+  UNPAIRN -> FailingNormal+  AnnCAR -> FailingNormal+  AnnCDR -> FailingNormal+  AnnDUP -> FailingNormal+  AnnDUPN -> FailingNormal+  AnnPUSH -> FailingNormal+  AnnSOME -> FailingNormal+  AnnNONE -> FailingNormal+  AnnUNIT -> FailingNormal+  AnnPAIR -> FailingNormal+  AnnUNPAIR -> FailingNormal+  AnnPAIRN -> FailingNormal+  AnnLEFT -> FailingNormal+  AnnRIGHT -> FailingNormal+  AnnNIL -> FailingNormal+  AnnCONS -> FailingNormal+  AnnSIZE -> FailingNormal+  AnnEMPTY_SET -> FailingNormal+  AnnEMPTY_MAP -> FailingNormal+  AnnEMPTY_BIG_MAP -> FailingNormal+  AnnMEM -> FailingNormal+  AnnGET -> FailingNormal+  AnnGETN -> FailingNormal+  AnnUPDATE -> FailingNormal+  AnnUPDATEN -> FailingNormal+  AnnGET_AND_UPDATE -> FailingNormal+  AnnLAMBDA -> FailingNormal+  AnnLAMBDA_REC -> FailingNormal+  AnnEXEC -> FailingNormal+  AnnAPPLY -> FailingNormal+  AnnCAST -> FailingNormal+  AnnRENAME -> FailingNormal+  AnnPACK -> FailingNormal+  AnnUNPACK -> FailingNormal+  AnnCONCAT -> FailingNormal+  AnnCONCAT' -> FailingNormal+  AnnSLICE -> FailingNormal+  AnnISNAT -> FailingNormal+  AnnADD -> FailingNormal+  AnnSUB -> FailingNormal+  AnnSUB_MUTEZ -> FailingNormal+  AnnMUL -> FailingNormal+  AnnEDIV -> FailingNormal+  AnnABS -> FailingNormal+  AnnNEG -> FailingNormal+  AnnLSL -> FailingNormal+  AnnLSR -> FailingNormal+  AnnOR -> FailingNormal+  AnnAND -> FailingNormal+  AnnXOR -> FailingNormal+  AnnNOT -> FailingNormal+  AnnCOMPARE -> FailingNormal+  AnnEQ -> FailingNormal+  AnnNEQ -> FailingNormal+  AnnLT -> FailingNormal+  AnnGT -> FailingNormal+  AnnLE -> FailingNormal+  AnnGE -> FailingNormal+  AnnINT -> FailingNormal+  AnnVIEW -> FailingNormal+  AnnSELF -> FailingNormal+  AnnCONTRACT -> FailingNormal+  AnnTRANSFER_TOKENS -> FailingNormal+  AnnSET_DELEGATE -> FailingNormal+  AnnCREATE_CONTRACT -> FailingNormal+  AnnIMPLICIT_ACCOUNT -> FailingNormal+  AnnNOW -> FailingNormal+  AnnAMOUNT -> FailingNormal+  AnnBALANCE -> FailingNormal+  AnnVOTING_POWER -> FailingNormal+  AnnTOTAL_VOTING_POWER -> FailingNormal+  AnnCHECK_SIGNATURE -> FailingNormal+  AnnSHA256 -> FailingNormal+  AnnSHA512 -> FailingNormal+  AnnBLAKE2B -> FailingNormal+  AnnSHA3 -> FailingNormal+  AnnKECCAK -> FailingNormal+  AnnHASH_KEY -> FailingNormal+  AnnPAIRING_CHECK -> FailingNormal+  AnnSOURCE -> FailingNormal+  AnnSENDER -> FailingNormal+  AnnADDRESS -> FailingNormal+  AnnCHAIN_ID -> FailingNormal+  AnnLEVEL -> FailingNormal+  AnnSELF_ADDRESS -> FailingNormal+  AnnTICKET -> FailingNormal+  AnnTICKET_DEPRECATED -> FailingNormal+  AnnREAD_TICKET -> FailingNormal+  AnnSPLIT_TICKET -> FailingNormal+  AnnJOIN_TICKETS -> FailingNormal+  AnnOPEN_CHEST -> FailingNormal+  AnnSAPLING_EMPTY_STATE -> FailingNormal+  AnnSAPLING_VERIFY_UPDATE -> FailingNormal+  AnnMIN_BLOCK_TIME -> FailingNormal+  AnnEMIT -> FailingNormal

@@ -0,0 +1,137 @@+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha+-- SPDX-License-Identifier: LicenseRef-MIT-OA++{-# OPTIONS_HADDOCK not-home #-}++-- | Actual decision implementation for 'IsMichelson'.+module Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsMichelson+  ( module Morley.Michelson.Typed.ClassifiedInstr.Internal.Classifiers.IsMichelson+  ) where++import Morley.Michelson.Typed.ClassifiedInstr.Internal.InstrEnum+import Morley.Michelson.Typed.ClassifiedInstr.Internal.Types++-- | Decide whether an instruction is coming from Michelson and whether it affects execution.+isMichelson :: InstrEnum -> IsMichelson+isMichelson = \case+  WithLoc -> Phantom+  Meta -> Phantom+  FrameInstr -> Phantom+  DocGroup -> Phantom+  Nop -> Additional+  Ext -> Additional+  Seq -> Structural+  Nested -> Structural+  --------------------+  IF_NONE -> FromMichelson+  IF_LEFT -> FromMichelson+  IF_CONS -> FromMichelson+  AnnMAP -> FromMichelson+  ITER -> FromMichelson+  IF -> FromMichelson+  LOOP -> FromMichelson+  LOOP_LEFT -> FromMichelson+  DIP  -> FromMichelson+  DIPN  -> FromMichelson+  FAILWITH  -> FromMichelson+  NEVER  -> FromMichelson+  DROP -> FromMichelson+  DROPN -> FromMichelson+  SWAP -> FromMichelson+  DIG -> FromMichelson+  DUG -> FromMichelson+  UNPAIRN -> FromMichelson+  AnnCAR -> FromMichelson+  AnnCDR -> FromMichelson+  AnnDUP -> FromMichelson+  AnnDUPN -> FromMichelson+  AnnPUSH -> FromMichelson+  AnnSOME -> FromMichelson+  AnnNONE -> FromMichelson+  AnnUNIT -> FromMichelson+  AnnPAIR -> FromMichelson+  AnnUNPAIR -> FromMichelson+  AnnPAIRN -> FromMichelson+  AnnLEFT -> FromMichelson+  AnnRIGHT -> FromMichelson+  AnnNIL -> FromMichelson+  AnnCONS -> FromMichelson+  AnnSIZE -> FromMichelson+  AnnEMPTY_SET -> FromMichelson+  AnnEMPTY_MAP -> FromMichelson+  AnnEMPTY_BIG_MAP -> FromMichelson+  AnnMEM -> FromMichelson+  AnnGET -> FromMichelson+  AnnGETN -> FromMichelson+  AnnUPDATE -> FromMichelson+  AnnUPDATEN -> FromMichelson+  AnnGET_AND_UPDATE -> FromMichelson+  AnnLAMBDA -> FromMichelson+  AnnLAMBDA_REC -> FromMichelson+  AnnEXEC -> FromMichelson+  AnnAPPLY -> FromMichelson+  AnnCAST -> FromMichelson+  AnnRENAME -> FromMichelson+  AnnPACK -> FromMichelson+  AnnUNPACK -> FromMichelson+  AnnCONCAT -> FromMichelson+  AnnCONCAT' -> FromMichelson+  AnnSLICE -> FromMichelson+  AnnISNAT -> FromMichelson+  AnnADD -> FromMichelson+  AnnSUB -> FromMichelson+  AnnSUB_MUTEZ -> FromMichelson+  AnnMUL -> FromMichelson+  AnnEDIV -> FromMichelson+  AnnABS -> FromMichelson+  AnnNEG -> FromMichelson+  AnnLSL -> FromMichelson+  AnnLSR -> FromMichelson+  AnnOR -> FromMichelson+  AnnAND -> FromMichelson+  AnnXOR -> FromMichelson+  AnnNOT -> FromMichelson+  AnnCOMPARE -> FromMichelson+  AnnEQ -> FromMichelson+  AnnNEQ -> FromMichelson+  AnnLT -> FromMichelson+  AnnGT -> FromMichelson+  AnnLE -> FromMichelson+  AnnGE -> FromMichelson+  AnnINT -> FromMichelson+  AnnVIEW -> FromMichelson+  AnnSELF -> FromMichelson+  AnnCONTRACT -> FromMichelson+  AnnTRANSFER_TOKENS -> FromMichelson+  AnnSET_DELEGATE -> FromMichelson+  AnnCREATE_CONTRACT -> FromMichelson+  AnnIMPLICIT_ACCOUNT -> FromMichelson+  AnnNOW -> FromMichelson+  AnnAMOUNT -> FromMichelson+  AnnBALANCE -> FromMichelson+  AnnVOTING_POWER -> FromMichelson+  AnnTOTAL_VOTING_POWER -> FromMichelson+  AnnCHECK_SIGNATURE -> FromMichelson+  AnnSHA256 -> FromMichelson+  AnnSHA512 -> FromMichelson+  AnnBLAKE2B -> FromMichelson+  AnnSHA3 -> FromMichelson+  AnnKECCAK -> FromMichelson+  AnnHASH_KEY -> FromMichelson+  AnnPAIRING_CHECK -> FromMichelson+  AnnSOURCE -> FromMichelson+  AnnSENDER -> FromMichelson+  AnnADDRESS -> FromMichelson+  AnnCHAIN_ID -> FromMichelson+  AnnLEVEL -> FromMichelson+  AnnSELF_ADDRESS -> FromMichelson+  AnnTICKET -> FromMichelson+  AnnTICKET_DEPRECATED -> FromMichelson+  AnnREAD_TICKET -> FromMichelson+  AnnSPLIT_TICKET -> FromMichelson+  AnnJOIN_TICKETS -> FromMichelson+  AnnOPEN_CHEST -> FromMichelson+  AnnSAPLING_EMPTY_STATE -> FromMichelson+  AnnSAPLING_VERIFY_UPDATE -> FromMichelson+  AnnMIN_BLOCK_TIME -> FromMichelson+  AnnEMIT -> FromMichelson