diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,56 @@
 <!-- Unreleased: append new entries here -->
 
 
+1.18.0
+======
+* [!1212](https://gitlab.com/morley-framework/morley/-/merge_requests/1212)
+  Implement `EMIT` and other Kathmandu changes
+  + Update michelson primitives for the new protocol
+  + Add support for parsing/typechecking/serializing `EMIT` instruction
+  + Support `EMIT` on the emulator
+* [!1202](https://gitlab.com/morley-framework/morley/-/merge_requests/1202)
+  Make error messages less confusing when types are ambiguous.
+  + Use `FailUnless` and similar rather than `If` to reduce the prevalence
+    of confusing type errors.
+  + Remove `TypeErrorUnless` in favor of `FailUnless`.
+* [!1207](https://gitlab.com/morley-framework/morley/-/merge_requests/1207)
+  Rename our custom `SingI1` to `SingIOne` to avoid confusion with
+  `singletons`, remove its method, and reduce it to just one polymorphic
+  instance.
+* [!1203](https://gitlab.com/morley-framework/morley/-/merge_requests/1203)
+  Remove `Morley.Util.Type.reifyTypeEquality`
+* [!1185](https://gitlab.com/morley-framework/morley/-/merge_requests/1185)
+  Refactor typechecker monad
+* [!1192](https://gitlab.com/morley-framework/morley/-/merge_requests/1192)
+  Refactor aliases storage in Cleveland
+  + Added `Morley.Util.Bimap.Bimap`
+  + Changed the type of `GState.gsImplicitAddressAliases` to `Bimap ImplicitAlias Address`
+  + Changed the type of `GState.gsContractAddressAliases` to `Bimap ContractAlias Address`
+  * Deleted `GSAddImplicitAddressAlias`
+* [!1177](https://gitlab.com/morley-framework/morley/-/merge_requests/1177)
+  Distinguish implicit/contract aliases and addresses on the type level
+* [!1190](https://gitlab.com/morley-framework/morley/-/merge_requests/1190)
+  Remove some `SingI` constraints from some `WithDeMorganScope` instances.
+* [!1186](https://gitlab.com/morley-framework/morley/-/merge_requests/1186)
+  Make `ITER{FAILWITH;}` typecheck
+* [!1176](https://gitlab.com/morley-framework/morley/-/merge_requests/1176)
+  Render Michelson values on multiple lines
+* [!1168](https://gitlab.com/morley-framework/morley/-/merge_requests/1168)
+  Support a mix of RPC and non-RPC representations in `runCode`
+  + Deleted `WellTypedIsoValue`
+  + Added `IsoValue` constraint to `WellTypedToT`, `HasNoOpToT`, `HasNoBigMapToT`, `KnownIsoT`.
+  + Added `typeCheckValueRunCodeCompat` to simulate the typechecking behavior of the
+    tezos RPC's `run_code` endpoint.
+  + Changed the return type of `typeCheckValue` from `TypeCheckInstr` to `TypeCheckResult`.
+  + Delete `runTypeCheckInstrIsolated`
+  + Restrict the type of `runTypeCheckIsolated`
+  + Delete `MaybeRPC`
+* [!1137](https://gitlab.com/morley-framework/morley/-/merge_requests/1137)
+  Support a delimiting but otherwise empty escape `\&` in
+  `Morley.Util.Interpolate`
+* [!1175](https://gitlab.com/morley-framework/morley/-/merge_requests/1175)
+  Use tagged decoder for Address
+
 1.17.0
 ======
 * [!1173](https://gitlab.com/morley-framework/morley/-/merge_requests/1173)
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -28,8 +28,9 @@
 import Morley.Michelson.TypeCheck.Types (mapSomeContract)
 import Morley.Michelson.Typed (Contract'(..), SomeContract(..), unContractCode)
 import Morley.Michelson.Untyped qualified as U
-import Morley.Tezos.Address (Address)
-import Morley.Tezos.Address.Alias (AddressOrAlias, Alias)
+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)
@@ -92,8 +93,8 @@
   { ooContractFile :: Maybe FilePath
   , ooDBPath :: FilePath
   , ooTcOptions :: TypeCheck.TypeCheckOptions
-  , ooOriginator :: Address
-  , ooAlias :: Maybe Alias
+  , ooOriginator :: ImplicitAddress
+  , ooAlias :: Maybe ContractAlias
   , ooDelegate :: Maybe KeyHash
   , ooStorageValue :: U.Value
   , ooBalance :: Mutez
@@ -103,7 +104,7 @@
 data TransferOptions = TransferOptions
   { toDBPath :: FilePath
   , toTcOptions :: TypeCheck.TypeCheckOptions
-  , toDestination :: AddressOrAlias
+  , toDestination :: SomeAddressOrAlias
   , toTxData :: TxData
   , toNow :: Maybe Timestamp
   , toLevel :: Maybe Natural
@@ -265,10 +266,15 @@
     transferOptions = do
       toDBPath <- dbPathOption
       toTcOptions <- typeCheckOptionsOption
-      toDestination <- addressOrAliasOption
-        Nothing
-        (#name :! "to")
-        (#help :! "Address or alias of the transfer's destination")
+      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
+          Nothing
+          (#name :! "to-contract")
+          (#help :! "Address or alias of the transfer's destination contract (KT1)")
       toTxData <- txDataOption
       toNow <- nowOption
       toLevel <- levelOption
@@ -353,7 +359,7 @@
             michelsonContract
             ! #verbose ooVerbose
         putTextLn $ "Originated contract " <> pretty addr
-      Transfer TransferOptions {..} -> do
+      Transfer TransferOptions {toDestination=SomeAddressOrAlias toDestination, ..} -> do
         transfer toNow toLevel toMinBlockTime toMaxSteps toDBPath toTcOptions toDestination toTxData
           ! #verbose toVerbose
           ! #dryRun toDryRun
diff --git a/morley.cabal b/morley.cabal
--- a/morley.cabal
+++ b/morley.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           morley
-version:        1.17.0
+version:        1.18.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
@@ -124,6 +124,7 @@
       Morley.Michelson.Untyped.View
       Morley.Tezos.Address
       Morley.Tezos.Address.Alias
+      Morley.Tezos.Address.Kinds
       Morley.Tezos.Core
       Morley.Tezos.Crypto
       Morley.Tezos.Crypto.BLS12381
@@ -134,6 +135,7 @@
       Morley.Tezos.Crypto.Timelock
       Morley.Tezos.Crypto.Util
       Morley.Util.Aeson
+      Morley.Util.Bimap
       Morley.Util.Binary
       Morley.Util.ByteString
       Morley.Util.CLI
@@ -150,6 +152,7 @@
       Morley.Util.Main
       Morley.Util.Markdown
       Morley.Util.MismatchError
+      Morley.Util.MultiReader
       Morley.Util.Named
       Morley.Util.Peano
       Morley.Util.PeanoNatural
@@ -191,6 +194,7 @@
       GADTs
       GeneralizedNewtypeDeriving
       ImportQualifiedPost
+      InstanceSigs
       LambdaCase
       MultiParamTypeClasses
       MultiWayIf
@@ -304,6 +308,7 @@
       GADTs
       GeneralizedNewtypeDeriving
       ImportQualifiedPost
+      InstanceSigs
       LambdaCase
       MultiParamTypeClasses
       MultiWayIf
diff --git a/src/Morley/AsRPC.hs b/src/Morley/AsRPC.hs
--- a/src/Morley/AsRPC.hs
+++ b/src/Morley/AsRPC.hs
@@ -6,7 +6,6 @@
 module Morley.AsRPC
   ( TAsRPC
   , HasRPCRepr(..)
-  , MaybeRPC(..)
   , deriveRPC
   , deriveRPCWithStrategy
   , deriveManyRPC
@@ -43,13 +42,12 @@
 import Language.Haskell.TH.ReifyMany (reifyManyTyCons)
 import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames)
 
-import Morley.Micheline (ToExpression(..))
 import Morley.Michelson.Text (MText)
 import Morley.Michelson.Typed
   (BigMap, BigMapId, ContractPresence(ContractAbsent), ContractRef, EpAddress, HasNoBigMap,
   HasNoContract, HasNoNestedBigMaps, HasNoOp, IsoValue, Notes(..), OpPresence(..), Operation,
   SingI(sing), SingT(..), StorageScope, T(..), ToT, Value, Value'(..), WellTyped,
-  checkContractTypePresence, checkOpPresence, toVal, withDict)
+  checkContractTypePresence, checkOpPresence, withDict)
 import Morley.Tezos.Address (Address, TxRollupL2Address)
 import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
 import Morley.Tezos.Crypto
@@ -62,8 +60,7 @@
 {-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}
 
 -- $setup
--- >>> import Morley.Michelson.Typed (T(..), BigMap, mkBigMap)
--- >>> import Morley.Michelson.Typed.Haskell.Value (BigMapId(..))
+-- >>> import Morley.Michelson.Typed
 -- >>> import Morley.Michelson.Text (MText)
 
 ----------------------------------------------------------------------------
@@ -268,28 +265,6 @@
   type AsRPC ChestKey = ChestKey
 instance HasRPCRepr TxRollupL2Address where
   type AsRPC TxRollupL2Address = TxRollupL2Address
-
-----------------------------------------------------------------------------
--- MaybeRPC
-----------------------------------------------------------------------------
-
--- | Represents a value that may or may not be in its RPC representation.
---
--- >>> :t NotRPC @(BigMap Integer MText) (mkBigMap @[(Integer, MText)] [])
--- ...
---   :: MaybeRPC (BigMap Integer MText)
---
--- >>> :t IsRPC @(BigMap Integer MText) (BigMapId 1)
--- ...
---   :: MaybeRPC (BigMap Integer MText)
-data MaybeRPC v where
-  NotRPC :: IsoValue  v => v -> MaybeRPC v
-  IsRPC :: (SingI (ToT v), IsoValue (AsRPC v), HasRPCRepr v) => AsRPC v -> MaybeRPC v
-
-instance HasNoOp (ToT v) => ToExpression (MaybeRPC v) where
-  toExpression = \case
-    NotRPC v -> toExpression (toVal v)
-    IsRPC v -> withDict (rpcHasNoOpEvi @(ToT v)) $ toExpression (toVal v)
 
 ----------------------------------------------------------------------------
 -- Derive RPC repr
diff --git a/src/Morley/CLI.hs b/src/Morley/CLI.hs
--- a/src/Morley/CLI.hs
+++ b/src/Morley/CLI.hs
@@ -30,6 +30,7 @@
   , timeOption
   ) where
 
+import Data.Singletons (SingI)
 import Options.Applicative
   (footerDoc, fullDesc, header, help, helper, info, long, metavar, option, progDesc, strOption,
   switch)
@@ -44,8 +45,8 @@
 import Morley.Michelson.Text (MText)
 import Morley.Michelson.Untyped (EpName)
 import Morley.Michelson.Untyped qualified as U
-import Morley.Tezos.Address (Address)
-import Morley.Tezos.Address.Alias (AddressOrAlias(..), Alias(..))
+import Morley.Tezos.Address
+import Morley.Tezos.Address.Alias
 import Morley.Tezos.Core (Mutez, Timestamp, parseTimestamp, timestampFromSeconds)
 import Morley.Tezos.Crypto
 import Morley.Util.CLI
@@ -141,18 +142,19 @@
   help "Path to DB with data which is used instead of real blockchain data" <>
   Opt.showDefault
 
-aliasOption :: String -> Opt.Parser Alias
-aliasOption key = fmap Alias . Opt.strOption $
+aliasOption :: (SingI kind, L1AddressKind kind) => String -> Opt.Parser (Alias kind)
+aliasOption key = fmap mkAlias . Opt.strOption $
   long key <>
   metavar "ALIAS" <>
   help "An alias to be associated with the originated contract's address, e.g: 'alice', 'bob'"
 
 -- | Generic parser to read an option of 'AddressOrAlias' type.
 addressOrAliasOption
-  :: Maybe AddressOrAlias
+  :: (SingI kind, L1AddressKind kind)
+  => Maybe (AddressOrAlias kind)
   -> "name" :! String
   -> "help" :! String
-  -> Opt.Parser AddressOrAlias
+  -> Opt.Parser (AddressOrAlias kind)
 addressOrAliasOption = mkCLOptionParser
 
 -- | Parser for transaction parameters.
@@ -167,10 +169,10 @@
       (#name :! "amount") (#help :! "Amount sent by a transaction")
     <*> entrypointOption (#name :! "entrypoint") (#help :! "Entrypoint to call")
   where
-    mkTxData :: Address -> U.Value -> Mutez -> EpName -> TxData
+    mkTxData :: ImplicitAddress -> U.Value -> Mutez -> EpName -> TxData
     mkTxData addr param amount epName =
       TxData
-        { tdSenderAddress = addr
+        { tdSenderAddress = MkConstrainedAddress addr
         , tdParameter = TxUntypedParam param
         , tdEntrypoint = epName
         , tdAmount = amount
@@ -196,9 +198,9 @@
   Maybe Mutez -> "name" :! String -> "help" :! String -> Opt.Parser Mutez
 mutezOption = mkCLOptionParser
 
--- | Generic parser to read an option of 'Address' type.
-addressOption ::
-  Maybe Address -> "name" :! String -> "help" :! String -> Opt.Parser Address
+-- | Generic parser to read an option of 'KindedAddress' type.
+addressOption :: SingI kind =>
+  Maybe (KindedAddress kind) -> "name" :! String -> "help" :! String -> Opt.Parser (KindedAddress kind)
 addressOption = mkCLOptionParser
 
 -- | @--oneline@ flag.
diff --git a/src/Morley/Micheline/Class.hs b/src/Morley/Micheline/Class.hs
--- a/src/Morley/Micheline/Class.hs
+++ b/src/Morley/Micheline/Class.hs
@@ -14,14 +14,12 @@
 
 import Control.Lens ((<>~))
 import Data.Bits (Bits)
-import Data.Default (def)
 import Data.Singletons (SingI(..), demote)
 import Fmt (Buildable(..), indentF, pretty, unlinesF)
 
 import Morley.Micheline.Expression
 import Morley.Michelson.Text (mkMText, unMText)
-import Morley.Michelson.TypeCheck
-  (TypeCheckMode(..), TypeCheckOptions(..), runTypeCheck, typeCheckingWith)
+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,
@@ -296,6 +294,7 @@
     SAPLING_EMPTY_STATE va n -> expressionPrim' "SAPLING_EMPTY_STATE" [integralToExpr n] $ mkAnns [] [] [va]
     SAPLING_VERIFY_UPDATE va -> expressionPrim' "SAPLING_VERIFY_UPDATE" [] $ mkAnns [] [] [va]
     MIN_BLOCK_TIME va -> expressionPrim' "MIN_BLOCK_TIME" [] $ mkAnnsFromAny va
+    EMIT va tag ty -> expressionPrim' "EMIT" (toExpression <$> maybeToList ty) $ mkAnns [] [tag] [va]
 
 instance ToExpression Untyped.Contract where
   toExpression contract
@@ -366,8 +365,6 @@
     Left e -> Left e
     where
       typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $
-        (runTypeCheck $ TypeCheckValue (uv, demote @t)) $
-        usingReaderT def $
         typeCheckValue uv
 
 instance FromExp x op => FromExp x (Untyped.Value' op) where
@@ -718,6 +715,12 @@
     ExpPrim' _ "SAPLING_VERIFY_UPDATE" [] anns ->
       mkInstrWithVarAnn SAPLING_VERIFY_UPDATE anns
     ExpPrim' _ "MIN_BLOCK_TIME" [] anns -> pure $ mkInstrWithAnyAnns MIN_BLOCK_TIME anns
+    ExpPrim' _ "EMIT" mty _ -> do
+      checkAnnsCount e annSet (0, 1, 1)
+      let tag = firstAnn @FieldTag annSet
+          va = firstAnn @VarTag annSet
+      ty' <- maybe (pure Nothing) (fmap Just . fromExp @x @Ty) $ listToMaybe mty
+      pure $ EMIT va tag ty'
     _ -> Left $ FromExpError e "Expected an instruction"
 
     where
diff --git a/src/Morley/Micheline/Expression.hs b/src/Morley/Micheline/Expression.hs
--- a/src/Morley/Micheline/Expression.hs
+++ b/src/Morley/Micheline/Expression.hs
@@ -132,7 +132,7 @@
   "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"
+  "VIEW", "view", "constant", "SUB_MUTEZ", "tx_rollup_l2_address", "MIN_BLOCK_TIME", "sapling_transaction", "EMIT"
   ]
 
 -- | Type for Micheline Expression with extension points.
diff --git a/src/Morley/Michelson/Interpret.hs b/src/Morley/Michelson/Interpret.hs
--- a/src/Morley/Michelson/Interpret.hs
+++ b/src/Morley/Michelson/Interpret.hs
@@ -65,8 +65,9 @@
 import Morley.Michelson.Typed qualified as T
 import Morley.Michelson.Typed.Operation
   (OperationHash(..), OriginationOperation(..), mkContractAddress, mkOriginationOperationHash)
-import Morley.Tezos.Address (Address(..), GlobalCounter(..))
-import Morley.Tezos.Address.Alias (Alias)
+import Morley.Michelson.Untyped (unAnnotation)
+import Morley.Tezos.Address
+import Morley.Tezos.Address.Alias
 import Morley.Tezos.Core (ChainId, Mutez, Timestamp, zeroMutez)
 import Morley.Tezos.Crypto
   (KeyHash, OpeningResult(..), blake2b, checkSignature, hashKey, keccak, mkTLTime, openChest,
@@ -138,14 +139,16 @@
   -- ^ Number of steps after which execution unconditionally terminates.
   , ceBalance :: Mutez
   -- ^ Current amount of mutez of the current contract.
-  , ceContracts :: Map Address AddressState
+  , ceContracts :: Map ContractAddress ContractState
   -- ^ Information stored about the existing contracts.
-  , ceSelf :: Address
+  , ceSelf :: ContractAddress
   -- ^ Address of the interpreted contract.
-  , ceSource :: Address
-  -- ^ The contract that initiated the current transaction.
-  , ceSender :: Address
-  -- ^ The contract that initiated the current internal transaction.
+  , ceSource :: L1Address
+  -- ^ The contract that initiated the current transaction. Note that this
+  -- contract should in normal operation be an implicit account.
+  , ceSender :: L1Address
+  -- ^ The contract that initiated the current internal transaction. This may
+  -- either be an implicit account or a smart contract.
   , ceAmount :: Mutez
   -- ^ Amount of the current transaction.
   , ceVotingPowers :: VotingPowers
@@ -663,8 +666,8 @@
                     (StkEl (arg :: Value arg) :& StkEl (VAddress epAddr) :& r) = do
   ContractEnv{..} <- ask
   res :: Value ('TOption ret) <- VOption <$> runMaybeT do
-    let EpAddress addr _ = epAddr
-    Just (ASContract viewedContractState) <- pure $ Map.lookup addr ceContracts
+    EpAddress addr@ContractAddress{} _ <- pure epAddr
+    Just viewedContractState <- pure $ Map.lookup addr ceContracts
     ContractState
       { csContract = viewedContract
       , csStorage = viewedContractStorage
@@ -681,10 +684,10 @@
     return res
   pure (StkEl res :& r)
   where
-    mkViewEnv :: Address -> ContractState -> ContractEnv -> ContractEnv
+    mkViewEnv :: ContractAddress -> ContractState -> ContractEnv -> ContractEnv
     mkViewEnv calledAddr viewedContractState ContractEnv{..} = ContractEnv
       { ceBalance = csBalance viewedContractState
-      , ceSender = ceSelf
+      , ceSender = MkConstrainedAddress ceSelf
       , ceSelf = calledAddr
       , ceSource
       , ceAmount = zeroMutez
@@ -697,10 +700,10 @@
   ContractEnv{..} <- ask
   case Proxy @out of
     (_ :: Proxy ('TContract cp ': s)) -> do
-      pure $ StkEl (VContract ceSelf sepc) :& r
+      pure $ StkEl (VContract (MkAddress ceSelf) sepc) :& r
 runInstrImpl _ (AnnCONTRACT (Anns2' _ (_ :: T.Notes a)) instrEpName) (StkEl (VAddress epAddr) :& r) = do
   ContractEnv{..} <- ask
-  let T.EpAddress addr addrEpName = epAddr
+  T.EpAddress' (MkConstrainedAddress addr) addrEpName <- pure epAddr
   let mepName =
         case (instrEpName, addrEpName) of
           (DefEpName, DefEpName) -> Just DefEpName
@@ -711,27 +714,25 @@
   let withNotes v = StkEl v :& r
   withNotes <$> case mepName of
     Nothing -> pure $ VOption Nothing
-    Just epName ->
-      case addr of
-        KeyAddress{} -> pure $ castContract addr epName T.tyImplicitAccountParam
-        ContractAddress{} -> pure $
-          case Map.lookup addr ceContracts of
-            Just (ASSimple _) -> error "Broken addresses map"
-            Just (ASContract ContractState{..}) ->
-              castContract addr epName (cParamNotes csContract)
-            Nothing -> VOption Nothing
-        TransactionRollupAddress{} ->
-          -- TODO [#838]: support transaction rollups on the emulator
-          throwMichelson $ MichelsonUnsupported "txr1 addresses with CONTRACT"
+    Just epName -> case addr of
+      ImplicitAddress{} -> pure $ castContract addr epName T.tyImplicitAccountParam
+      ContractAddress{} -> pure $
+        case Map.lookup addr ceContracts of
+          Just ContractState{..} ->
+            castContract addr epName (cParamNotes csContract)
+          Nothing -> VOption Nothing
+      TxRollupAddress{} ->
+        -- TODO [#838]: support transaction rollups on the emulator
+        throwMichelson $ MichelsonUnsupported "txr1 addresses with CONTRACT"
   where
   castContract
-    :: forall p. T.ParameterScope p
-    => Address -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))
+    :: forall p kind. (T.ParameterScope p)
+    => KindedAddress kind -> EpName -> T.ParamNotes p -> T.Value ('TOption ('TContract a))
   castContract addr epName param = VOption $ do
     -- As we are within Maybe monad, pattern-match failure results in Nothing
     MkEntrypointCallRes (_ :: Notes a') epc <- T.mkEntrypointCall epName param
     Right Refl <- pure $ eqType @a @a'
-    return $ VContract addr (T.SomeEpc epc)
+    return $ VContract (MkAddress addr) (T.SomeEpc epc)
 
 runInstrImpl _ AnnTRANSFER_TOKENS{}
   (StkEl p :& StkEl (VMutez mutez) :& StkEl contract :& r) = do
@@ -755,18 +756,21 @@
           Just hash -> mkContractAddress hash globalCounter
           Nothing ->
             mkContractAddress
-              (mkOriginationOperationHash (createOrigOp originator Nothing mbKeyHash m contract g globalCounter))
+              (mkOriginationOperationHash $
+                  createOrigOp originator Nothing mbKeyHash m contract g globalCounter
+              )
               -- If opHash is Nothing it means that interpreter is running in some kind of test
               -- context, therefore we generate dummy contract address with its own origination
               -- operation.
               globalCounter
   let resEpAddr = EpAddress resAddr DefEpName
-  let resOp = CreateContract originator (unwrapMbKeyHash mbKeyHash) m g contract globalCounter
+  let resOp = CreateContract
+        (MkConstrainedAddress originator) (unwrapMbKeyHash mbKeyHash) m g contract globalCounter
   pure $ StkEl (VOp (OpCreateContract resOp))
       :& StkEl (VAddress resEpAddr)
       :& r
 runInstrImpl _ AnnIMPLICIT_ACCOUNT{} (StkEl (VKeyHash k) :& r) =
-  pure $ (StkEl (VContract (KeyAddress k) sepcPrimitive)) :& r
+  pure $ (StkEl (VContract (MkAddress $ ImplicitAddress k) sepcPrimitive)) :& r
 runInstrImpl _ AnnNOW{} r = do
   ContractEnv{..} <- ask
   pure $ StkEl (VTimestamp ceNow) :& r
@@ -801,13 +805,13 @@
   let pairs' = [ (g1, g2) | VPair (VBls12381G1 g1, VBls12381G2 g2) <- pairs ]
   pure $ StkEl (VBool $ checkPairing pairs') :& r
 runInstrImpl _ AnnSOURCE{} r = do
-  ContractEnv{..} <- ask
+  ContractEnv{ceSource=MkConstrainedAddress ceSource} <- ask
   pure $ StkEl (VAddress $ EpAddress ceSource DefEpName) :& r
 runInstrImpl _ AnnSENDER{} r = do
-  ContractEnv{..} <- ask
+  ContractEnv{ceSender=MkConstrainedAddress ceSender} <- ask
   pure $ StkEl (VAddress $ EpAddress ceSender DefEpName) :& r
 runInstrImpl _ AnnADDRESS{} (StkEl (VContract a sepc) :& r) =
-  pure $ StkEl (VAddress $ EpAddress a (sepcName sepc)) :& r
+  pure $ StkEl (VAddress $ EpAddress' a (sepcName sepc)) :& r
 runInstrImpl _ AnnCHAIN_ID{} r = do
   ContractEnv{..} <- ask
   pure $ StkEl (VChainId ceChainId) :& r
@@ -819,11 +823,11 @@
   pure $ StkEl (VAddress $ EpAddress ceSelf DefEpName) :& r
 runInstrImpl _ AnnTICKET{} (StkEl dat :& StkEl (VNat am) :& r) = do
   ContractEnv{..} <- ask
-  pure $ StkEl (VTicket ceSelf dat am) :& r
+  pure $ StkEl (VTicket (MkAddress ceSelf) dat am) :& r
 runInstrImpl _ AnnREAD_TICKET{} (te@(StkEl (VTicket addr dat am)) :& r) = do
   pure $
     StkEl
-      (VPair (VAddress (EpAddress addr DefEpName), (VPair (dat, VNat am))))
+      (VPair (VAddress (EpAddress' addr DefEpName), (VPair (dat, VNat am))))
     :& te :& r
 runInstrImpl _ AnnSPLIT_TICKET{}
     (StkEl tv@(VTicket addr dat am) :&
@@ -853,6 +857,11 @@
 runInstrImpl _ AnnMIN_BLOCK_TIME{} r = do
   ContractEnv{..} <- ask
   pure $ StkEl (VNat ceMinBlockTime) :& r
+runInstrImpl _ (AnnEMIT _ (unAnnotation -> emTag) mNotes) ((StkEl emValue) :& r) = do
+  incrementCounter
+  emCounter <- isGlobalCounter <$> getInterpreterState
+  let emNotes = fromMaybe starNotes mNotes
+  pure $ StkEl (VOp (OpEmit Emit{..})) :& r
 
 -- | Evaluates an arithmetic operation and either fails or proceeds.
 runArithOp
@@ -877,9 +886,9 @@
   unpackValue' bs
 
 createOrigOp
-  :: (ParameterScope param, StorageScope store)
-  => Address
-  -> Maybe Alias
+  :: (ParameterScope param, StorageScope store, L1AddressKind kind)
+  => KindedAddress kind
+  -> Maybe ContractAlias
   -> Maybe (T.Value 'T.TKeyHash)
   -> Mutez
   -> Contract param store
diff --git a/src/Morley/Michelson/Interpret/Unpack.hs b/src/Morley/Michelson/Interpret/Unpack.hs
--- a/src/Morley/Michelson/Interpret/Unpack.hs
+++ b/src/Morley/Michelson/Interpret/Unpack.hs
@@ -80,4 +80,4 @@
   when (tag /= 0x05) . Left . UnpackError $
     "Unexpected tag: '" <> (show tag) <> "'. '0x05' tag expected."
   expr <- eitherDecodeExpression bs'
-  either (Left . UnpackError . pretty) Right $ fromExpression @t expr
+  first (UnpackError . pretty) $ fromExpression @t expr
diff --git a/src/Morley/Michelson/Parser/Instr.hs b/src/Morley/Michelson/Parser/Instr.hs
--- a/src/Morley/Michelson/Parser/Instr.hs
+++ b/src/Morley/Michelson/Parser/Instr.hs
@@ -52,6 +52,7 @@
   , ticketOp, readTicketOp, splitTicketOp, joinTicketsOp
   , openChestOp
   , saplingEmptyStateOp, saplingVerifyUpdateOp, minBlockTimeOp
+  , emitOp
   ]
 
 -- | Parse a sequence of instructions.
@@ -470,3 +471,6 @@
 
 openChestOp :: Parser ParsedInstr
 openChestOp = word "OPEN_CHEST" OPEN_CHEST <*> noteDef
+
+emitOp :: Parser ParsedInstr
+emitOp = word "EMIT" (uncurry EMIT) <*> notesVF <*> optional type_
diff --git a/src/Morley/Michelson/Printer/Util.hs b/src/Morley/Michelson/Printer/Util.hs
--- a/src/Morley/Michelson/Printer/Util.hs
+++ b/src/Morley/Michelson/Printer/Util.hs
@@ -24,16 +24,20 @@
   , needsParens
   , doesntNeedParens
   , addParens
+  , addParensMultiline
   , assertParensNotNeeded
   ) where
 
+import Prelude hiding (group)
+
 import Control.Exception (assert)
 import Data.Text.Lazy qualified as LT
 import Data.Text.Lazy.Builder (Builder)
 import Fmt (Buildable, pretty)
 import Text.PrettyPrint.Leijen.Text
-  (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, encloseSep, hcat, isEmpty, lbracket,
-  parens, punctuate, rbracket, renderOneLine, renderPretty, semi, space, text, vcat, (<+>))
+  (Doc, SimpleDoc, align, braces, displayB, displayT, enclose, encloseSep, hcat, hsep, isEmpty,
+  lbracket, parens, punctuate, rbracket, renderOneLine, renderPretty, semi, sep, space, text, (<+>),
+  (<//>))
 
 -- | Environment carried during recursive rendering.
 newtype RenderContext = RenderContext
@@ -91,22 +95,16 @@
 renderOps :: (RenderDoc op) => Bool -> NonEmpty op -> Doc
 renderOps oneLine = renderOpsList oneLine . toList
 
--- | Join a non-empty list of 'Doc' by spaces
-spacecat :: NonEmpty Doc -> Doc
-spacecat = foldr (<+>) mempty
-
 -- | Render a comma-separated list of items in braces
 renderOpsList :: (RenderDoc op) => Bool -> [op] -> Doc
 renderOpsList oneLine ops =
   braces $ enclose space space $ renderOpsListNoBraces oneLine ops
 
--- | Render a comma-separated list of items without braces
+-- | Render a semi-colon-separated list of items without braces
 renderOpsListNoBraces :: RenderDoc op => Bool -> [op] -> Doc
-renderOpsListNoBraces oneLine ops =
-  cat' $ punctuate semi $
-    renderDoc doesntNeedParens <$> filter isRenderable ops
-  where
-    cat' = if oneLine then maybe "" spacecat . nonEmpty else align . vcat
+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
@@ -128,7 +126,6 @@
 buildRenderDocExtended :: RenderDoc a => a -> Builder
 buildRenderDocExtended = printDocB False . renderDoc doesntNeedParens
 
-
 -- | Here using a page width of 80 and a ribbon width of 1.0
 -- https://hackage.haskell.org/package/wl-pprint-1.2.1/docs/Text-PrettyPrint-Leijen.html
 doRender :: Bool -> Doc -> SimpleDoc
@@ -154,6 +151,12 @@
 addParens = \case
   RenderContext True -> parens
   RenderContext False -> id
+
+-- | Add parentheses if needed, multiline if necessary.
+addParensMultiline :: RenderContext -> Doc -> Doc
+addParensMultiline pn doc = case pn of
+  RenderContext True -> "(" <> doc <//> ")"
+  RenderContext False -> doc
 
 -- | Ensure parentheses are not required, for case when you cannot
 -- sensibly wrap your expression into them.
diff --git a/src/Morley/Michelson/Runtime.hs b/src/Morley/Michelson/Runtime.hs
--- a/src/Morley/Michelson/Runtime.hs
+++ b/src/Morley/Michelson/Runtime.hs
@@ -18,7 +18,6 @@
 
   -- * Re-exports
   , ContractState (..)
-  , AddressState (..)
   , VotingPowers
   , mkVotingPowers
   , mkVotingPowersFromMap
@@ -55,11 +54,14 @@
 
 import Control.Lens (assign, at, makeLenses, (.=), (<>=))
 import Control.Monad.Except (Except, liftEither, runExcept, throwError)
+import Data.Constraint (Dict(..), (\\))
 import Data.Default (def)
 import Data.HashSet qualified as HS
 import Data.Semigroup.Generic (GenericSemigroupMonoid(..))
+import Data.Singletons (demote)
 import Data.Text.IO (getContents)
 import Data.Text.IO.Utf8 qualified as Utf8 (readFile)
+import Data.Type.Equality (pattern Refl)
 import Fmt (Buildable(build), blockListF, fmt, fmtLn, indentF, nameF, pretty, (+|), (|+))
 import Text.Megaparsec (parse)
 
@@ -79,8 +81,9 @@
 import Morley.Michelson.Typed.Operation
 import Morley.Michelson.Untyped (Contract)
 import Morley.Michelson.Untyped qualified as U
-import Morley.Tezos.Address (Address(..), GlobalCounter(..), isKeyAddress)
-import Morley.Tezos.Address.Alias (AddressOrAlias(..), Alias)
+import Morley.Tezos.Address
+import Morley.Tezos.Address.Alias
+import Morley.Tezos.Address.Kinds
 import Morley.Tezos.Core
   (Mutez, Timestamp(..), getCurrentTime, unsafeAddMutez, unsafeSubMutez, zeroMutez)
 import Morley.Tezos.Crypto (KeyHash, parseHash)
@@ -105,6 +108,8 @@
   -- ^ Transfer tokens to the address.
   | SetDelegateOp SetDelegateOperation
   -- ^ Set the delegate of a contract.
+  | EmitOp EmitOperation
+  -- ^ Emit contract event.
   deriving stock (Show)
 
 instance Buildable ExecutorOp where
@@ -118,6 +123,11 @@
     SetDelegateOp SetDelegateOperation{..} ->
       "Set delegate of contract " +| sdoContract |+
       " to " +| maybe "<nobody>" build sdoDelegate |+ ""
+    EmitOp (EmitOperation source T.Emit{..}) ->
+      "Emit event " +| emTag |+
+        " from contract " +| source |+
+        " with type " +| emNotes |+
+        " and value " +| emValue |+ ""
 
 -- | Result of a single execution of interpreter.
 data ExecutorRes = ExecutorRes
@@ -143,7 +153,7 @@
 data ExecutorState = ExecutorState
   { _esGState :: GState
   , _esRemainingSteps :: RemainingSteps
-  , _esSourceAddress :: Maybe Address
+  , _esSourceAddress :: Maybe L1Address
   , _esLog :: ExecutorLog
   , _esOperationHash :: ~OperationHash
   , _esPrevCounters :: HashSet GlobalCounter
@@ -171,7 +181,7 @@
   | EEInterpreterFailed a
                         InterpretError
   -- ^ Interpretation of Michelson contract failed.
-  | EEUnknownAddressAlias Alias
+  | EEUnknownAddressAlias SomeAlias
   -- ^ Given alias doesn't refer to any address.
   | EEUnknownSender a
   -- ^ Sender address is unknown.
@@ -199,13 +209,18 @@
   -- ^ Type of parameter in transfer to an implicit account is not Unit.
   | EEOperationReplay ExecutorOp
   -- ^ An attempt to perform the operation duplicated with @DUP@ instruction.
-  deriving stock (Show, Functor)
+  | EEGlobalOperationSourceNotImplicit Address
+  -- ^ Attempted to initiate global operation from a non-implicit address.
+  | EEGlobalEmitOp
+  -- ^ Trying to run emit operation as a global operation, which should be impossible.
+  deriving stock (Show, Functor, Foldable, Traversable)
 
 instance (Buildable a) => Buildable (ExecutorError' a) where
   build =
     \case
-      EEUnknownAddressAlias alias ->
-        "The alias " +| alias |+ " doesn't have any associated addresses"
+      EEUnknownAddressAlias (SomeAlias (alias :: Alias kind)) ->
+        ("The alias " +| alias |+ " doesn't have any associated " +| demote @kind |+ " addresses")
+        \\ aliasKindSanity alias
       EEUnknownContract addr -> "The contract is not originated " +| addr |+ ""
       EEInterpreterFailed addr err ->
         "Michelson interpreter failed for contract " +| addr |+ ": " +| err |+ ""
@@ -230,6 +245,10 @@
         "Bad contract parameter for: " +| addr |+ ""
       EEOperationReplay op ->
         "Operation replay attempt:\n" +| indentF 2 (build op) |+ ""
+      EEGlobalOperationSourceNotImplicit addr ->
+        "Attempted to initiate global operation from a non-implicit address " +| addr |+ ""
+      EEGlobalEmitOp ->
+        "Attempted to run emit event as a global operation, this should be impossible."
 
 type ExecutorError = ExecutorError' Address
 
@@ -274,14 +293,14 @@
 originateContract
   :: FilePath
   -> TypeCheckOptions
-  -> Address
-  -> Maybe Alias
+  -> ImplicitAddress
+  -> Maybe ContractAlias
   -> Maybe KeyHash
   -> Mutez
   -> U.Value
   -> U.Contract
   -> "verbose" :! Bool
-  -> IO Address
+  -> IO ContractAddress
 originateContract dbPath tcOpts originator mbAlias delegate balance uStorage uContract verbose = do
   origination <- either throwM pure . typeCheckingWith tcOpts $
     mkOrigination <$> typeCheckContractAndStorage uContract uStorage
@@ -325,8 +344,8 @@
     -- Here we are safe to bypass executeGlobalOperations for origination,
     -- since origination can't generate more operations.
     addr <- executeGlobalOrigination origination
-    let transferOp = TransferOp $ TransferOperation addr txData 1
-    executeGlobalOperations tcOpts [transferOp]
+    let transferOp = TransferOp $ TransferOperation (MkAddress addr) txData 1
+    void $ executeGlobalOperations tcOpts [transferOp]
     getContractStorage addr
   return newSt
   where
@@ -349,30 +368,29 @@
       , ooAlias = Nothing
       }
 
-    getContractStorage :: Address -> ExecutorM SomeStorage
+    getContractStorage :: ContractAddress -> ExecutorM SomeStorage
     getContractStorage addr = do
-      addrs <- use (esGState . gsAddressesL)
+      addrs <- use (esGState . gsContractAddressesL)
       case addrs ^. at addr of
         Nothing -> error $ pretty addr <> " is unknown"
-        Just (ASSimple {}) -> error $ pretty addr <> " is a simple address"
-        Just (ASContract (ContractState{..})) -> return $ SomeStorage csStorage
+        Just ContractState{..} -> return $ SomeStorage csStorage
 
 -- | Send a transaction to given address with given parameters.
-transfer ::
-     Maybe Timestamp
+transfer
+  :: Maybe Timestamp
   -> Maybe Natural
   -> Maybe Natural
   -> Word64
   -> FilePath
   -> TypeCheckOptions
-  -> AddressOrAlias
+  -> AddressOrAlias kind
   -> 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 <- resolveAddress destination
+    destAddr <- MkAddress <$> resolveAddress destination
     executeGlobalOperations tcOpts [TransferOp $ TransferOperation destAddr txData 0]
 
 ----------------------------------------------------------------------------
@@ -478,27 +496,31 @@
         mapM_ putTextLn logs
       putTextLn "" -- extra break line to separate logs from two sequence contracts
 
--- | Resolves 'AddressOrAlias' type to 'Address'
-resolveAddress :: AddressOrAlias -> ExecutorM Address
+-- | Resolves 'AddressOrAlias' type to 'KindedAddress' of the appropriate kind.
+resolveAddress
+  :: forall kind. AddressOrAlias kind
+  -> ExecutorM (KindedAddress kind)
 resolveAddress (AddressResolved addr) = pure addr
 resolveAddress (AddressAlias alias) = do
-  addrAliases <- use $ esGState . gsAddressAliasesL
-  case lookupAddress alias addrAliases of
+  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 alias
+    Nothing -> throwError $ EEUnknownAddressAlias $ SomeAlias alias
 
--- | Execute a list of global operations, discarding their results.
+-- | Execute a list of global operations, returning a list of generated events.
 executeGlobalOperations
   :: TypeCheckOptions
   -> [ExecutorOp]
-  -> ExecutorM ()
-executeGlobalOperations tcOpts = mapM_ $ \op ->
-  executeMany (#isGlobalOp :! True) [op]
+  -> 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.
-    executeMany :: "isGlobalOp" :! Bool -> [ExecutorOp] -> ExecutorM ()
+    executeMany :: "isGlobalOp" :! Bool -> [ExecutorOp] -> ExecutorM [EmitOperation]
     executeMany isGlobalOp = \case
-        [] -> pass
+        [] -> pure []
         (op:opsTail) -> do
           case op of
             OriginateOp origination -> do
@@ -510,16 +532,19 @@
             TransferOp transferOperation -> do
               moreOps <- executeTransfer isGlobalOp Nothing tcOpts transferOperation
               executeMany (#isGlobalOp :! False) $ moreOps <> opsTail
+            EmitOp emitOperation -> do
+              liftM2 (:) (executeEmit isGlobalOp emitOperation) $
+                executeMany (#isGlobalOp :! False) opsTail
 
 -- | Execute a global origination operation.
-executeGlobalOrigination :: OriginationOperation -> ExecutorM Address
+executeGlobalOrigination :: OriginationOperation -> ExecutorM ContractAddress
 executeGlobalOrigination = executeOrigination ! #isGlobalOp True
 
 -- | Execute an origination operation.
 executeOrigination
   :: "isGlobalOp" :! Bool
   -> OriginationOperation
-  -> ExecutorM Address
+  -> ExecutorM ContractAddress
 executeOrigination (arg #isGlobalOp -> isGlobalOp) origination@(OriginationOperation{..}) = do
   when isGlobalOp $ do
     beginGlobalOperation
@@ -538,11 +563,12 @@
   let contractState = ContractState ooBalance ooContract storageWithIds ooDelegate
 
   let originatorAddress = ooOriginator
-  originatorBalance <- case gsAddresses gs ^. at originatorAddress of
-    Nothing -> throwError (EEUnknownManager originatorAddress)
-    Just (asBalance -> oldBalance)
+
+  originatorBalance <- case lookupBalance originatorAddress gs of
+    Nothing -> throwError $ EEUnknownManager $ MkAddress ooOriginator
+    Just oldBalance
       | oldBalance < ooBalance ->
-        throwError $ EENotEnoughFunds originatorAddress oldBalance
+        throwError $ EENotEnoughFunds (MkAddress ooOriginator) oldBalance
       | otherwise ->
         -- Subtraction is safe because we have checked its
         -- precondition in guard.
@@ -551,8 +577,8 @@
     address = mkContractAddress opHash ooCounter
     updates =
       catMaybes
-        [ liftA2 GSAddAddressAlias ooAlias (Just address)
-        , Just $ GSAddAddress address (ASContract contractState)
+        [ liftA2 GSAddContractAddressAlias ooAlias (Just address)
+        , Just $ GSAddContractAddress address contractState
         , Just $ GSSetBalance originatorAddress originatorBalance
         , Just GSIncrementCounter
         , if bigMapCounter0 == bigMapCounter1
@@ -573,7 +599,7 @@
   :: "isGlobalOp" :! Bool
   -> SetDelegateOperation
   -> ExecutorM ()
-executeDelegation (arg #isGlobalOp -> isGlobalOp) delegation@(SetDelegateOperation{..}) = do
+executeDelegation (arg #isGlobalOp -> isGlobalOp) delegation@SetDelegateOperation{..} = do
   when isGlobalOp $ do
     beginGlobalOperation
     assign esOperationHash $ mkDelegationOperationHash delegation
@@ -591,6 +617,16 @@
 
       return ()
 
+-- | Execute delegation operation.
+executeEmit
+  :: "isGlobalOp" :! Bool
+  -> EmitOperation
+  -> ExecutorM EmitOperation
+executeEmit (arg #isGlobalOp -> isGlobalOp) op = do
+  when isGlobalOp $ throwError EEGlobalEmitOp
+  checkOperationReplay $ EmitOp op
+  pure op
+
 -- | Execute a transfer operation.
 executeTransfer
   :: "isGlobalOp" :! Bool
@@ -604,7 +640,10 @@
   -> TransferOperation
   -> ExecutorM [ExecutorOp]
 executeTransfer (arg #isGlobalOp -> isGlobalOp)
-  overrideBalanceMb tcOpts transferOperation@(TransferOperation addr txData _) = do
+  overrideBalanceMb tcOpts
+    transferOperation@(
+      TransferOperation (MkAddress (addr :: KindedAddress kind))
+        txData@TxData{tdSenderAddress=MkConstrainedAddress senderAddr,..} _) = do
     when isGlobalOp $
       beginGlobalOperation
 
@@ -613,186 +652,214 @@
     mbt <- view eeMinBlockTime
     gs <- use esGState
     remainingSteps <- use esRemainingSteps
-    mSourceAddr <- use esSourceAddress
+    sourceAddr <- fromMaybe (tdSenderAddress txData) <$> use esSourceAddress
 
     let globalCounter = gsCounter gs
-    let addresses = gsAddresses gs
-    let senderAddr = tdSenderAddress txData
-    let sourceAddr = fromMaybe senderAddr mSourceAddr
-    let isZeroTransfer = tdAmount txData == zeroMutez
+    let addresses :: Map (KindedAddress kind) (AddressStateFam kind)
+        addresses = case addr of
+          ImplicitAddress{} -> gsImplicitAddresses gs
+          ContractAddress{} -> gsContractAddresses gs
+          TxRollupAddress{} -> gsTxRollupAddresses gs
+    let isZeroTransfer = tdAmount == zeroMutez
+    let senderBalance = lookupBalance senderAddr gs
 
     checkOperationReplay $ TransferOp transferOperation
 
     -- Implicit addresses can't be senders with a balance of 0tz even when the transfer amount
     -- is zero.
-    when (isKeyAddress senderAddr && isNothing overrideBalanceMb) $
-      case addresses ^. at senderAddr of
-        Nothing -> throwError $ EEEmptyImplicitContract senderAddr
-        Just (asBalance -> balance) | balance == zeroMutez ->
-          throwError $ EEEmptyImplicitContract senderAddr
-        _ -> pass
+    case isImplicitAddress senderAddr of
+      Nothing -> do
+        when (isGlobalOp && not isZeroTransfer) $
+          throwError $ EETransactionFromContract (MkAddress senderAddr) tdAmount
 
-    when (badParamToImplicitAccount addr $ tdParameter txData) $
-      throwError $ EEWrongParameterType addr
+      Just Refl -> do
+        when (isNothing overrideBalanceMb) $
+          case senderBalance of
+            Nothing -> throwError $ EEEmptyImplicitContract $ MkAddress senderAddr
+            Just balance | balance == zeroMutez ->
+              throwError $ EEEmptyImplicitContract $ MkAddress senderAddr
+            _ -> pass
 
-    -- Transferring 0 XTZ to a key address is prohibited.
-    when (isZeroTransfer && isKeyAddress addr) $
-      throwError $ EEZeroTransaction addr
+    case isImplicitAddress addr of
+      Nothing -> pass
+      Just Refl -> do
+        when (badParamToImplicitAccount tdParameter) $
+          throwError $ EEWrongParameterType $ MkAddress addr
+
+        -- Transferring 0 XTZ to a key address is prohibited.
+        when (isZeroTransfer) $
+          throwError $ EEZeroTransaction $ MkAddress addr
+
     mDecreaseSenderBalance <-
       if isNothing overrideBalanceMb && not isZeroTransfer
-        then case addresses ^. at senderAddr of
-          Nothing -> throwError $ EEUnknownSender senderAddr
-          Just (asBalance -> balance)
-            | balance < tdAmount txData ->
-              throwError $ EENotEnoughFunds senderAddr balance
-            | otherwise ->
+        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.
-              return $ Just $ GSSetBalance senderAddr (balance `unsafeSubMutez` tdAmount txData)
+              let newBal = balance `unsafeSubMutez` tdAmount
+              pure $ Just $ GSSetBalance senderAddr newBal
         else pure Nothing
-    when (not (isKeyAddress senderAddr) && isGlobalOp && not isZeroTransfer) $
-      throwError $ EETransactionFromContract senderAddr $ tdAmount txData
-    let onlyUpdates updates = return (updates, [], Nothing, remainingSteps)
-    (otherUpdates, sideEffects, maybeInterpretRes :: Maybe InterpretResult, newRemSteps)
-        <- case (addresses ^. at addr, addr) of
-      (Nothing, TransactionRollupAddress _) ->
-        -- TODO [#838]: support transaction rollups on the emulator
-        throwError $ EEUnknownContract addr
-      (Nothing, ContractAddress _) ->
-        throwError $ EEUnknownContract addr
-      (Nothing, KeyAddress _) -> do
-        let
-          transferAmount = tdAmount txData
-          addrState = ASSimple transferAmount
-          upd = GSAddAddress addr addrState
 
-        onlyUpdates [upd]
-      (Just (ASSimple oldBalance), _) -> 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 txData)
-              overrideBalanceMb
-          upd = GSSetBalance addr newBalance
-        onlyUpdates [upd]
-      (Just (ASContract (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 txData)
-              overrideBalanceMb
-          epName = tdEntrypoint txData
+    let commonFinishup
+          :: Dict (L1AddressKind kind)
+          -- NB: this is a Dict and not a constraint because GHC desugars these
+          -- let-bindings such that it expects this constraint at the definition
+          -- site.
+          -> [GStateUpdate]
+          -> [T.Operation]
+          -> Maybe InterpretResult
+          -> RemainingSteps
+          -> ExecutorM [ExecutorOp]
+        commonFinishup Dict otherUpdates sideEffects maybeInterpretRes newRemSteps = do
+          let
+            -- According to the reference implementation, counter is incremented for transfers as well.
+            updates = (maybe id (:) mDecreaseSenderBalance otherUpdates) ++ [GSIncrementCounter]
 
-        T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)
-          <- T.mkEntrypointCall epName (T.cParamNotes csContract)
-             & maybe (throwError $ EEUnknownEntrypoint epName) pure
+          newGState <- liftEither $ first EEFailedToApplyUpdates $ applyUpdates updates gs
 
-        -- If the parameter has already been typechecked, simply check if
-        -- its type matches the contract's entrypoint's type.
-        -- Otherwise (e.g. if it was parsed from stdin via the CLI),
-        -- we need to typecheck the parameter.
-        typedParameter <-
-          case tdParameter txData of
-            TxTypedParam (typedVal :: T.Value t) -> do
-              T.castM @t @epArg typedVal (throwError . EEUnexpectedParameterType addr)
-            TxUntypedParam untypedVal ->
-              liftEither $ first (EEIllTypedParameter addr) $ typeCheckingWith tcOpts $
-                typeVerifyParameter @epArg existingContracts untypedVal
+          esGState .= newGState
+          esRemainingSteps .= newRemSteps
+          esSourceAddress .= Just sourceAddr
 
-        let bigMapCounter0 = gs ^. gsBigMapCounterL
-        let (typedParameterWithIds, bigMapCounter1) = runState (assignBigMapIds False typedParameter) bigMapCounter0
+          esLog <>= ExecutorLog updates (maybe mempty (one . (MkAddress addr, )) maybeInterpretRes)
 
-        -- I'm not entirely sure why we need to pattern match on `()` here,
-        -- but, if we don't, we get a compiler error that I suspect is somehow related
-        -- to the existential types we're matching on a few lines above.
-        --
-        -- • Couldn't match type ‘a0’
-        --                  with ‘(InterpretResult, RemainingSteps, [Operation], [GStateUpdate])’
-        --     ‘a0’ is untouchable inside the constraints: StorageScope st1
-        () <- when isGlobalOp $
-          esOperationHash .= mkTransferOperationHash
-            addr
-            typedParameterWithIds
-            (tdEntrypoint txData)
-            (tdAmount txData)
+          mapM (convertOp addr) $ sideEffects
+        onlyUpdates :: Dict (L1AddressKind kind) -> [GStateUpdate] -> ExecutorM [ExecutorOp]
+        onlyUpdates dict updates = commonFinishup dict updates [] Nothing remainingSteps
 
-        opHash <- use esOperationHash
-        let
-          contractEnv = ContractEnv
-            { ceNow = now
-            , ceMaxSteps = remainingSteps
-            , ceBalance = newBalance
-            , ceContracts = gsAddresses gs
-            , ceSelf = addr
-            , ceSource = sourceAddr
-            , ceSender = senderAddr
-            , ceAmount = tdAmount txData
-            , ceVotingPowers = gsVotingPowers gs
-            , ceChainId = gsChainId gs
-            , ceOperationHash = Just opHash
-            , ceLevel = level
-            , ceErrorSrcPos = def
-            , ceMinBlockTime = mbt
-            }
+    case addr of
+      TxRollupAddress{} ->
+        -- TODO [#838]: support transaction rollups on the emulator
+        throwError $ EEUnknownContract (MkAddress addr)
+      ImplicitAddress{} -> case addresses ^. at addr of
+        Nothing -> do
+          let
+            transferAmount = tdAmount
+            addrState = transferAmount
+            upd = GSAddImplicitAddress addr addrState
 
-        iur@InterpretResult
-          { iurOps = sideEffects
-          , iurNewStorage = newValue
-          , iurNewState = InterpreterState newRemainingSteps globalCounter2 bigMapCounter2
-          }
-          <- liftEither $ first (EEInterpreterFailed addr) $
-             handleContractReturn $
-                interpret
-                  csContract
-                  epc
-                  typedParameterWithIds
-                  csStorage
-                  (gsCounter gs)
-                  bigMapCounter1
-                  contractEnv
+          onlyUpdates Dict [upd]
+        Just oldBalance -> 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
+            upd = GSSetBalance addr newBalance
+          onlyUpdates Dict [upd]
+      ContractAddress{} -> case addresses ^. at addr of
+        Nothing -> throwError $ EEUnknownContract (MkAddress addr)
+        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
+            epName = tdEntrypoint
 
-        let
-          updBalance
-            | newBalance == csBalance = Nothing
-            | otherwise = Just $ GSSetBalance addr newBalance
-          updStorage
-            | SomeValue newValue == SomeValue csStorage = Nothing
-            | otherwise = Just $ GSSetStorageValue addr newValue
-          updBigMapCounter
-            | bigMapCounter0 == bigMapCounter2 = Nothing
-            | otherwise = Just $ GSSetBigMapCounter bigMapCounter2
-          updGlobalCounter
-            | globalCounter == globalCounter2 = Nothing
-            | otherwise = Just $ GSUpdateCounter globalCounter2
-          updates = catMaybes
-            [ updBalance
-            , updStorage
-            , updBigMapCounter
-            , updGlobalCounter
-            ]
-        return (updates, sideEffects, Just iur, newRemainingSteps)
+          T.MkEntrypointCallRes _ (epc :: EntrypointCallT cp epArg)
+            <- T.mkEntrypointCall epName (T.cParamNotes csContract)
+              & maybe (throwError $ EEUnknownEntrypoint epName) pure
 
-    let
-      -- According to the reference implementation, counter is incremented for transfers as well.
-      updates = (maybe id (:) mDecreaseSenderBalance otherUpdates) ++ [GSIncrementCounter]
+          -- If the parameter has already been typechecked, simply check if
+          -- its type matches the contract's entrypoint's type.
+          -- Otherwise (e.g. if it was parsed from stdin via the CLI),
+          -- we need to typecheck the parameter.
+          typedParameter <-
+            case tdParameter of
+              TxTypedParam (typedVal :: T.Value t) ->
+                T.castM @t @epArg typedVal $
+                  throwError . EEUnexpectedParameterType (MkAddress addr)
+              TxUntypedParam untypedVal ->
+                liftEither $ first (EEIllTypedParameter $ MkAddress addr) $
+                  typeCheckingWith tcOpts $
+                    typeVerifyParameter @epArg existingContracts untypedVal
 
-    newGState <- liftEither $ first EEFailedToApplyUpdates $ applyUpdates updates gs
+          let bigMapCounter0 = gs ^. gsBigMapCounterL
+          let (typedParameterWithIds, bigMapCounter1) = runState (assignBigMapIds False typedParameter) bigMapCounter0
 
-    esGState .= newGState
-    esRemainingSteps .= newRemSteps
-    esSourceAddress .= Just sourceAddr
+          -- I'm not entirely sure why we need to pattern match on `()` here,
+          -- but, if we don't, we get a compiler error that I suspect is somehow related
+          -- to the existential types we're matching on a few lines above.
+          --
+          -- • Couldn't match type ‘a0’
+          --                  with ‘(InterpretResult, RemainingSteps, [Operation], [GStateUpdate])’
+          --     ‘a0’ is untouchable inside the constraints: StorageScope st1
+          () <- when isGlobalOp $
+            esOperationHash .= mkTransferOperationHash
+              addr
+              typedParameterWithIds
+              tdEntrypoint
+              tdAmount
 
-    esLog <>= ExecutorLog updates (maybe mempty (one . (addr, )) maybeInterpretRes)
+          opHash <- use esOperationHash
+          let
+            contractEnv = ContractEnv
+              { ceNow = now
+              , ceMaxSteps = remainingSteps
+              , ceBalance = newBalance
+              , ceContracts = gsContractAddresses gs
+              , ceSelf = addr
+              , ceSource = sourceAddr
+              , ceSender = MkConstrainedAddress senderAddr
+              , ceAmount = tdAmount
+              , ceVotingPowers = gsVotingPowers gs
+              , ceChainId = gsChainId gs
+              , ceOperationHash = Just opHash
+              , ceLevel = level
+              , ceErrorSrcPos = def
+              , ceMinBlockTime = mbt
+              }
 
-    return $ convertOp addr <$> sideEffects
+          iur@InterpretResult
+            { iurOps = sideEffects
+            , iurNewStorage = newValue
+            , iurNewState = InterpreterState newRemainingSteps globalCounter2 bigMapCounter2
+            }
+            <- liftEither $ first (EEInterpreterFailed (MkAddress addr)) $
+              handleContractReturn $
+                  interpret
+                    csContract
+                    epc
+                    typedParameterWithIds
+                    csStorage
+                    (gsCounter gs)
+                    bigMapCounter1
+                    contractEnv
 
+          let
+            updBalance
+              | newBalance == csBalance = Nothing
+              | otherwise = Just $ GSSetBalance addr newBalance
+            updStorage
+              | SomeValue newValue == SomeValue csStorage = Nothing
+              | otherwise = Just $ GSSetStorageValue addr newValue
+            updBigMapCounter
+              | bigMapCounter0 == bigMapCounter2 = Nothing
+              | otherwise = Just $ GSSetBigMapCounter bigMapCounter2
+            updGlobalCounter
+              | globalCounter == globalCounter2 = Nothing
+              | otherwise = Just $ GSUpdateCounter globalCounter2
+            updates = catMaybes
+              [ updBalance
+              , updStorage
+              , updBigMapCounter
+              , updGlobalCounter
+              ]
+          commonFinishup Dict updates sideEffects (Just iur) newRemainingSteps
+
+
 ----------------------------------------------------------------------------
 -- Simple helpers
 ----------------------------------------------------------------------------
@@ -804,21 +871,22 @@
       OriginateOp OriginationOperation{..} -> ooCounter
       TransferOp TransferOperation{..} -> toCounter
       SetDelegateOp SetDelegateOperation{..} -> sdoCounter
+      EmitOp (EmitOperation _ T.Emit{..}) -> emCounter
   prevCounters <- use esPrevCounters
   when (opCounter `HS.member` prevCounters) $
     throwError $ EEOperationReplay op
   esPrevCounters <>= one opCounter
 
 -- The argument is the address of the contract that generated this operation.
-convertOp :: Address -> T.Operation -> ExecutorOp
+convertOp :: L1AddressKind kind => KindedAddress kind -> T.Operation -> ExecutorM ExecutorOp
 convertOp interpretedAddr =
   \case
     OpTransferTokens tt ->
-      case ttContract tt of
+      pure $ case ttContract tt of
         T.VContract destAddress sepc ->
           let txData =
                 TxData
-                  { tdSenderAddress = interpretedAddr
+                  { tdSenderAddress = MkConstrainedAddress interpretedAddr
                   , tdEntrypoint = T.sepcName sepc
                   , tdParameter = TxTypedParam (ttTransferArgument tt)
                   , tdAmount = ttAmount tt
@@ -830,31 +898,34 @@
                   , toCounter = ttCounter tt
                   }
           in TransferOp transferOperation
-    OpSetDelegate T.SetDelegate{..} -> SetDelegateOp SetDelegateOperation
-      { sdoContract = interpretedAddr
-      , sdoDelegate = sdMbKeyHash
-      , sdoCounter = sdCounter
-      }
-    OpCreateContract cc ->
-      let origination = OriginationOperation
-            { ooOriginator = ccOriginator cc
-            , ooDelegate = ccDelegate cc
-            , ooBalance = ccBalance cc
-            , ooStorage = ccStorageVal cc
-            , ooContract = ccContract cc
-            , ooCounter = ccCounter cc
-            , ooAlias = Nothing
-            }
-       in OriginateOp origination
+    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, ..} ->
+      pure $ OriginateOp OriginationOperation
+        { ooOriginator = ccOriginator
+        , ooDelegate = ccDelegate
+        , ooBalance = ccBalance
+        , ooStorage = ccStorageVal
+        , ooContract = ccContract
+        , ooCounter = ccCounter
+        , ooAlias = Nothing
+        }
+    OpEmit emit -> case interpretedAddr of
+      ContractAddress{} -> pure $ EmitOp $ EmitOperation interpretedAddr emit
+      _ -> throwError $ EEUnknownContract $ MkAddress interpretedAddr
 
 -- | Reset source address before executing a global operation.
 beginGlobalOperation :: ExecutorM ()
 beginGlobalOperation =
   esSourceAddress .= Nothing
 
--- | Return True if address is an implicit account yet the param is not Unit.
-badParamToImplicitAccount :: Address -> TxParam -> Bool
-badParamToImplicitAccount (ContractAddress _) _                       = False
-badParamToImplicitAccount (KeyAddress _) (TxTypedParam T.VUnit)       = False
-badParamToImplicitAccount (KeyAddress _) (TxUntypedParam U.ValueUnit) = False
-badParamToImplicitAccount _ _                                         = True
+-- | Return True if the param is not Unit.
+badParamToImplicitAccount :: TxParam -> Bool
+badParamToImplicitAccount (TxTypedParam T.VUnit)       = False
+badParamToImplicitAccount (TxUntypedParam U.ValueUnit) = False
+badParamToImplicitAccount _ = True
diff --git a/src/Morley/Michelson/Runtime/Dummy.hs b/src/Morley/Michelson/Runtime/Dummy.hs
--- a/src/Morley/Michelson/Runtime/Dummy.hs
+++ b/src/Morley/Michelson/Runtime/Dummy.hs
@@ -13,6 +13,7 @@
   , dummyGlobalCounter
   , dummyOrigination
   , dummyMinBlockTime
+  , dummySelf
   ) where
 
 import Data.Default (def)
@@ -22,7 +23,7 @@
 import Morley.Michelson.Typed (ParameterScope, StorageScope)
 import Morley.Michelson.Typed qualified as T
 import Morley.Michelson.Typed.Operation (OriginationOperation(..))
-import Morley.Tezos.Address (GlobalCounter(..))
+import Morley.Tezos.Address
 import Morley.Tezos.Core (Timestamp(..), dummyChainId, tz)
 
 -- | Dummy timestamp, can be used to specify current @NOW@ value or
@@ -50,6 +51,9 @@
 dummyGlobalCounter :: GlobalCounter
 dummyGlobalCounter = 0
 
+dummySelf :: ContractAddress
+dummySelf = [ta|KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB|]
+
 -- | Dummy 'ContractEnv' with some reasonable hardcoded values. You
 -- can override values you are interested in using record update
 -- syntax.
@@ -59,9 +63,9 @@
   , ceMaxSteps = dummyMaxSteps
   , ceBalance = [tz|100u|]
   , ceContracts = mempty
-  , ceSelf = genesisAddress
-  , ceSource = genesisAddress
-  , ceSender = genesisAddress
+  , ceSelf = dummySelf
+  , ceSource = MkConstrainedAddress genesisAddress
+  , ceSender = MkConstrainedAddress genesisAddress
   , ceAmount = [tz|100u|]
   , ceVotingPowers = dummyVotingPowers
   , ceChainId = dummyChainId
diff --git a/src/Morley/Michelson/Runtime/GState.hs b/src/Morley/Michelson/Runtime/GState.hs
--- a/src/Morley/Michelson/Runtime/GState.hs
+++ b/src/Morley/Michelson/Runtime/GState.hs
@@ -7,10 +7,6 @@
   (
     -- * Auxiliary types
     ContractState (..)
-  , AddressState (..)
-  , AddressAliases (..)
-  , lookupAddress
-  , asBalance
   , VotingPowers (..)
   , vpPick
   , vpTotal
@@ -23,11 +19,14 @@
   -- * GState
   , GState (..)
   , gsChainIdL
-  , gsAddressesL
-  , gsAddressAliasesL
+  , gsImplicitAddressesL
+  , gsContractAddressesL
+  , gsImplicitAddressAliasesL
+  , gsContractAddressAliasesL
   , gsVotingPowersL
   , gsCounterL
   , gsBigMapCounterL
+  , addressesL
   , genesisAddresses
   , genesisKeyHashes
   , genesisAddress
@@ -51,6 +50,8 @@
   , applyUpdate
   , applyUpdates
   , extractAllContracts
+  , lookupBalance
+  , AddressStateFam
   ) where
 
 import Control.Lens (at, makeLenses, (?~))
@@ -58,8 +59,6 @@
 import Data.Aeson qualified as Aeson
 import Data.Aeson.Encode.Pretty qualified as Aeson
 import Data.Aeson.TH (deriveJSON)
-import Data.Bimap (Bimap)
-import Data.Bimap qualified as Bimap (empty, fromList, insert, lookup, toList)
 import Data.ByteString.Lazy qualified as LBS
 import Data.Default (def)
 import Data.Map.Strict qualified as Map
@@ -73,13 +72,16 @@
 import Morley.Michelson.Typed.Existential (SomeContractAndStorage(..))
 import Morley.Michelson.Typed.Scope
 import Morley.Michelson.Untyped (Contract, Value)
-import Morley.Tezos.Address (Address(..), GlobalCounter(..))
-import Morley.Tezos.Address.Alias (Alias)
+import Morley.Tezos.Address
+import Morley.Tezos.Address.Alias
+import Morley.Tezos.Address.Kinds
 import Morley.Tezos.Core (ChainId, Mutez, divModMutezInt, dummyChainId)
 import Morley.Tezos.Crypto
 import Morley.Util.Aeson
+import Morley.Util.Bimap (Bimap)
+import Morley.Util.Bimap qualified as Bimap
 import Morley.Util.Lens
-import Morley.Util.Peano
+import Morley.Util.Peano (ToPeano, type (>))
 import Morley.Util.Sing (eqI, eqParamSing, eqParamSing2)
 import Morley.Util.SizedList qualified as SL
 import Morley.Util.SizedList.Types
@@ -97,6 +99,8 @@
   -- ^ Delegate associated with this contract.
   }
 
+makeLensesWith postfixLFields ''ContractState
+
 deriving stock instance Show ContractState
 
 instance Eq ContractState where
@@ -137,30 +141,6 @@
     "\n  Contract: " +| T.convertContract csContract |+
     "\n  Delegate: " +| csDelegate |+ ""
 
--- | State of an arbitrary address.
-data AddressState
-  = ASSimple Mutez
-  -- ^ For contracts without code we store only its balance.
-  | ASContract ContractState
-  -- ^ For contracts with code we store more state represented by
-  -- 'ContractState'.
-  deriving stock (Show, Eq, Generic)
-
-instance Buildable AddressState where
-  build =
-    \case
-      ASSimple balance -> "Balance = " +| balance |+ ""
-      ASContract cs -> build cs
-
-deriveJSON morleyAesonOptions ''AddressState
-
--- | Extract balance from 'AddressState'.
-asBalance :: AddressState -> Mutez
-asBalance =
-  \case
-    ASSimple b -> b
-    ASContract cs -> csBalance cs
-
 -- | Distribution of voting power among the contracts.
 --
 -- Voting power reflects the ability of bakers to accept, deny or pass new
@@ -208,29 +188,23 @@
 data GState = GState
   { gsChainId :: ChainId
   -- ^ Identifier of chain.
-  , gsAddresses :: Map Address AddressState
-  -- ^ All known addresses and their state.
+  , gsImplicitAddresses :: Map ImplicitAddress Mutez
+  -- ^ All known implicit addresses and their state (i.e. balance)
+  , gsContractAddresses :: Map ContractAddress ContractState
+  -- ^ All known contract addresses and their state.
+  , gsTxRollupAddresses :: Map TxRollupAddress ()
+  -- ^ All known transaction rollup addresses and their state.
   , gsVotingPowers :: VotingPowers
   -- ^ Voting power distribution.
   , gsCounter :: GlobalCounter
   -- ^ Ever increasing operation counter.
   , gsBigMapCounter :: BigMapCounter
-  , gsAddressAliases :: AddressAliases
-  -- ^ Addresses with the associated aliases/names.
+  , gsImplicitAddressAliases :: Bimap ImplicitAlias ImplicitAddress
+  -- ^ Implicit addresses with the associated aliases/names.
+  , gsContractAddressAliases :: Bimap ContractAlias ContractAddress
+  -- ^ Contract addresses with the associated aliases/names.
   } deriving stock (Show, Eq)
 
-newtype AddressAliases = AddressAliases (Bimap Alias Address)
-  deriving stock (Eq, Show)
-
-instance FromJSON AddressAliases where
-  parseJSON = fmap (AddressAliases . Bimap.fromList) . parseJSON
-
-instance ToJSON AddressAliases where
-  toJSON (AddressAliases aa) = toJSON $ Bimap.toList aa
-
-lookupAddress :: Alias -> AddressAliases -> Maybe Address
-lookupAddress alias (AddressAliases aa) = Bimap.lookup alias aa
-
 makeLensesWith postfixLFields ''GState
 
 deriveJSON morleyAesonOptions ''GState
@@ -256,15 +230,15 @@
 genesisKeyHashes = hashKey . toPublic <$> genesisSecrets
 
 -- | Initially these addresses have a lot of money.
-genesisAddresses :: GenesisList Address
-genesisAddresses = KeyAddress <$> genesisKeyHashes
+genesisAddresses :: GenesisList ImplicitAddress
+genesisAddresses = ImplicitAddress <$> genesisKeyHashes
 
 -- | One of genesis key hashes.
 genesisKeyHash :: KeyHash
 genesisKeyHash = SL.head genesisKeyHashes
 
 -- | One of genesis addresses.
-genesisAddress :: Address
+genesisAddress :: ImplicitAddress
 genesisAddress = SL.head genesisAddresses
 
 -- | Secret key assotiated with 'genesisAddress'.
@@ -272,7 +246,7 @@
 genesisSecretKey = SL.head genesisSecrets
 
 -- | More genesis addresses
-genesisAddress1, genesisAddress2, genesisAddress3 :: Address
+genesisAddress1, genesisAddress2, genesisAddress3 :: ImplicitAddress
 _ :< genesisAddress1 :< genesisAddress2 :< genesisAddress3
   :< _ = genesisAddresses
 
@@ -282,7 +256,9 @@
 --
 -- Note that @'genesisAddress' == genesisAddressN \@0@, @'genesisAddress1' == genesisAddressN \@1@,
 -- etc.
-genesisAddressN :: forall n. (SingIPeano n, ToPeano GenesisAddressesNum > ToPeano n ~ 'True) => Address
+genesisAddressN
+  :: forall n. (SingIPeano n, ToPeano GenesisAddressesNum > ToPeano n ~ 'True)
+  => ImplicitAddress
 genesisAddressN = SL.index @n genesisAddresses
 
 -- | Dummy 'VotingPowers'. We give all the voting power to two genesis addreses
@@ -298,16 +274,19 @@
 initGState =
   GState
   { gsChainId = dummyChainId
-  , gsAddresses = Map.fromList
-    [ (genesis, ASSimple money)
+  , gsImplicitAddresses = Map.fromList
+    [ (genesis, money)
     | let (money, _) = maxBound @Mutez `divModMutezInt` genesisAddressesNum
                     ?: error "Number of genesis addresses is 0"
     , genesis <- toList genesisAddresses
     ]
+  , gsContractAddresses = Map.empty
+  , gsTxRollupAddresses = Map.empty
   , gsVotingPowers = dummyVotingPowers
   , gsCounter = GlobalCounter 0
   , gsBigMapCounter = BigMapCounter 0
-  , gsAddressAliases = AddressAliases $ Bimap.empty
+  , gsImplicitAddressAliases = Bimap.empty
+  , gsContractAddressAliases = Bimap.empty
   }
 
 data GStateParseError =
@@ -342,23 +321,26 @@
 
 -- | Updates that can be applied to 'GState'.
 data GStateUpdate where
-  GSAddAddress :: Address -> AddressState -> GStateUpdate
-  GSAddAddressAlias :: Alias -> Address -> GStateUpdate
-  GSSetStorageValue :: StorageScope st => Address -> T.Value st -> GStateUpdate
-  GSSetBalance :: Address -> Mutez -> GStateUpdate
+  GSAddImplicitAddress :: ImplicitAddress -> Mutez -> GStateUpdate
+  GSAddContractAddress :: ContractAddress -> ContractState -> GStateUpdate
+  GSAddContractAddressAlias :: ContractAlias -> ContractAddress -> GStateUpdate
+  GSSetStorageValue :: StorageScope st => ContractAddress -> T.Value st -> GStateUpdate
+  GSSetBalance :: L1AddressKind kind => KindedAddress kind -> Mutez -> GStateUpdate
   GSIncrementCounter :: GStateUpdate
   GSUpdateCounter :: GlobalCounter -> GStateUpdate
   GSSetBigMapCounter :: BigMapCounter -> GStateUpdate
-  GSSetDelegate :: Address -> Maybe KeyHash -> GStateUpdate
+  GSSetDelegate :: ContractAddress -> Maybe KeyHash -> GStateUpdate
 
 deriving stock instance Show GStateUpdate
 
 instance Buildable GStateUpdate where
   build =
     \case
-      GSAddAddress addr st ->
-        "Add address " +| addr |+ " with state " +| st |+ ""
-      GSAddAddressAlias alias addr ->
+      GSAddImplicitAddress addr st ->
+        "Add implicit address " +| addr |+ " with balance " +| st |+ ""
+      GSAddContractAddress addr st ->
+        "Add contract address " +| addr |+ " with state " +| st |+ ""
+      GSAddContractAddressAlias alias addr ->
         "Add an alias " +| alias |+ " for address " +| addr |+ ""
       GSSetStorageValue addr tVal ->
         "Set storage value of address " +| addr |+ " to " +| T.untypeValue tVal |+ ""
@@ -377,8 +359,8 @@
 data GStateUpdateError
   = GStateAddressExists Address
   | GStateUnknownAddress Address
-  | GStateNotContract Address
-  | GStateStorageNotMatch Address
+  | GStateStorageNotMatch ContractAddress
+  | GStateTxRollup TxRollupAddress GStateUpdate
   deriving stock (Show)
 
 instance Buildable GStateUpdateError where
@@ -386,20 +368,22 @@
     \case
       GStateAddressExists addr -> "Address already exists: " <> build addr
       GStateUnknownAddress addr -> "Unknown address: " <> build addr
-      GStateNotContract addr -> "Address doesn't have contract: " <> 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 |+ ""
 
 -- | Apply 'GStateUpdate' to 'GState'.
 applyUpdate :: GStateUpdate -> GState -> Either GStateUpdateError GState
 applyUpdate =
   \case
-    GSAddAddress addr st -> addAddress addr st
-    GSAddAddressAlias alias addr -> Right . addAddressAlias alias addr
+    GSAddImplicitAddress addr st -> addImplicitAddress addr st
+    GSAddContractAddress addr st -> addContractAddress addr st
+    GSAddContractAddressAlias alias addr -> Right . addContractAddressAlias alias addr
     GSSetStorageValue addr newValue ->
       setStorageValue addr newValue
-    GSSetBalance addr newBalance -> setBalance addr newBalance
+    GSSetBalance addr newBalance -> addr `setBalance` newBalance
     GSIncrementCounter -> Right . over gsCounterL (+1)
     GSUpdateCounter newCounter -> Right . set gsCounterL newCounter
     GSSetBigMapCounter bmCounter -> Right . set gsBigMapCounterL bmCounter
@@ -410,67 +394,92 @@
 applyUpdates = flip (foldM (flip applyUpdate))
 
 -- | Add an address if it hasn't been added before.
-addAddress :: Address -> AddressState -> GState -> Either GStateUpdateError GState
-addAddress addr st gs
-    | addr `Map.member` (gsAddresses gs) = Left $ GStateAddressExists addr
-    | otherwise = Right $ gs & gsAddressesL . at addr ?~ st
+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
 
+-- | Add an address if it hasn't been added before.
+addContractAddress :: ContractAddress -> ContractState -> GState -> Either GStateUpdateError GState
+addContractAddress addr st gs
+  | addr `Map.member` (gsContractAddresses gs) = Left $ GStateAddressExists (MkAddress addr)
+  | otherwise = Right $ gs & gsContractAddressesL . at addr ?~ st
+
 -- | Add an alias for given address, overwriting any existing address for the same alias.
-addAddressAlias :: Alias -> Address -> GState -> GState
-addAddressAlias alias addr = gsAddressAliasesL %~ insertAddressAlias
-  where
-    insertAddressAlias (AddressAliases aa) =
-      AddressAliases $ Bimap.insert alias addr aa
+addContractAddressAlias :: ContractAlias -> ContractAddress -> GState -> GState
+addContractAddressAlias alias addr = gsContractAddressAliasesL . at alias ?~ addr
 
 -- | Update storage value associated with given address.
 setStorageValue :: forall st. (StorageScope st) =>
-     Address -> T.Value st -> GState -> Either GStateUpdateError GState
+     ContractAddress -> T.Value st -> GState -> Either GStateUpdateError GState
 setStorageValue addr newValue = updateAddressState addr modifier
   where
-    modifier :: AddressState -> Either GStateUpdateError AddressState
-    modifier (ASSimple _) = Left (GStateNotContract addr)
-    modifier (ASContract ContractState{csStorage = _ :: T.Value st', ..}) = do
+    modifier :: ContractState -> Either GStateUpdateError ContractState
+    modifier ContractState{csStorage = _ :: T.Value st', ..} = do
       case eqI @st @st' of
-        Just Refl -> Right $ ASContract $ ContractState{csStorage = newValue, ..}
+        Just Refl -> Right $ ContractState{csStorage = newValue, ..}
         _ -> Left $ GStateStorageNotMatch addr
 
 -- | Update balance value associated with given address.
-setBalance :: Address -> Mutez -> GState -> Either GStateUpdateError GState
-setBalance addr newBalance = updateAddressState addr $ Right . \case
-  ASSimple _ -> ASSimple newBalance
-  ASContract cs -> ASContract (cs {csBalance = newBalance})
+setBalance
+  :: forall kind. L1AddressKind kind
+  => KindedAddress kind
+  -> Mutez
+  -> GState
+  -> Either GStateUpdateError GState
+setBalance addr newBalance = updateAddressState addr $
+  Right . set (balanceLens addr) newBalance
 
+lookupBalance :: forall kind. L1AddressKind kind => KindedAddress kind -> GState -> Maybe Mutez
+lookupBalance addr = preview $ addressesL addr . at addr . traverse . balanceLens addr
+
+balanceLens
+  :: forall kind. L1AddressKind kind
+  => KindedAddress kind
+  -> Lens' (AddressStateFam kind) Mutez
+balanceLens = \case
+  ImplicitAddress{} -> id
+  ContractAddress{} -> csBalanceL
+  where _ = usingImplicitOrContractKind @kind ()
+
 -- | Set delegate for a given address
-setDelegate :: Address -> Maybe KeyHash -> GState -> Either GStateUpdateError GState
-setDelegate addr key = updateAddressState addr \case
-  ASSimple _ -> Left $ GStateNotContract addr
-  ASContract cs -> Right $ ASContract cs{csDelegate = key}
+setDelegate :: ContractAddress -> Maybe KeyHash -> GState -> Either GStateUpdateError GState
+setDelegate addr key = updateAddressState addr $ pure . (csDelegateL .~ key)
 
-updateAddressState ::
-     Address
-  -> (AddressState -> Either GStateUpdateError AddressState)
+type family AddressStateFam kind where
+  AddressStateFam 'AddressKindImplicit = Mutez
+  AddressStateFam 'AddressKindContract = ContractState
+  -- TODO [#838]: support transaction rollups on the emulator
+  AddressStateFam 'AddressKindTxRollup = ()
+
+updateAddressState
+  :: forall kind. KindedAddress kind
+  -> (AddressStateFam kind -> Either GStateUpdateError (AddressStateFam kind))
   -> GState
   -> Either GStateUpdateError GState
 updateAddressState addr f gs =
-  case addresses ^. at addr of
-    Nothing -> Left (GStateUnknownAddress addr)
+  let addrL :: Lens' GState (Maybe (AddressStateFam kind))
+      addrL = addressesL addr . at addr
+  in case gs ^. addrL of
+    Nothing -> Left $ GStateUnknownAddress $ MkAddress addr
     Just as -> do
       newState <- f as
-      return $ gs { gsAddresses = addresses & at addr .~ Just newState }
-  where
-    addresses = gsAddresses gs
+      return $ gs & addrL .~ Just newState
 
+addressesL
+  :: KindedAddress kind
+  -> Lens' GState (Map (KindedAddress kind) (AddressStateFam kind))
+addressesL = \case
+  ImplicitAddress{} -> gsImplicitAddressesL
+  ContractAddress{} -> gsContractAddressesL
+  TxRollupAddress{} -> gsTxRollupAddressesL
+
 -- | Retrieve all contracts stored in GState
 extractAllContracts :: GState -> TcOriginatedContracts
-extractAllContracts = Map.fromList . mapMaybe extractContract . toPairs . gsAddresses
+extractAllContracts = Map.fromList . mapMaybe extractContract . toPairs . gsContractAddresses
  where
     extractContract
-      :: (Address, AddressState) -> Maybe (ContractHash, SomeParamType)
+      :: (ContractAddress, ContractState) -> Maybe (ContractHash, SomeParamType)
     extractContract =
-      \case (KeyAddress _, ASSimple {}) -> Nothing
-            (KeyAddress _, _) -> error "broken GState"
-            (ContractAddress ca, ASContract (ContractState{..})) ->
+      \case (ContractAddress ca, ContractState{..}) ->
               Just (ca, SomeParamType $ T.cParamNotes $ csContract)
-            (ContractAddress _, _) -> error "broken GState"
-            -- TODO [#838]: support transaction rollups on the emulator
-            (TransactionRollupAddress _, _) -> error "broken GState"
diff --git a/src/Morley/Michelson/Runtime/TxData.hs b/src/Morley/Michelson/Runtime/TxData.hs
--- a/src/Morley/Michelson/Runtime/TxData.hs
+++ b/src/Morley/Michelson/Runtime/TxData.hs
@@ -18,7 +18,7 @@
 import Morley.Michelson.Typed qualified as T
 import Morley.Michelson.Untyped (EpName)
 import Morley.Michelson.Untyped qualified as U
-import Morley.Tezos.Address (Address)
+import Morley.Tezos.Address
 import Morley.Tezos.Core (Mutez)
 import Morley.Util.Lens (postfixLFields)
 
@@ -31,7 +31,7 @@
 
 -- | Data associated with a particular transaction.
 data TxData = TxData
-  { tdSenderAddress :: Address
+  { tdSenderAddress :: L1Address
   , tdParameter :: TxParam
   , tdEntrypoint :: EpName
   , tdAmount :: Mutez
diff --git a/src/Morley/Michelson/TypeCheck.hs b/src/Morley/Michelson/TypeCheck.hs
--- a/src/Morley/Michelson/TypeCheck.hs
+++ b/src/Morley/Michelson/TypeCheck.hs
@@ -12,6 +12,7 @@
   , typeCheckStorage
   , typeCheckTopLevelType
   , typeCheckValue
+  , typeCheckValueRunCodeCompat
   , typeVerifyContract
   , typeVerifyParameter
   , typeVerifyStorage
diff --git a/src/Morley/Michelson/TypeCheck/Error.hs b/src/Morley/Michelson/TypeCheck/Error.hs
--- a/src/Morley/Michelson/TypeCheck/Error.hs
+++ b/src/Morley/Michelson/TypeCheck/Error.hs
@@ -27,7 +27,7 @@
 import Morley.Michelson.TypeCheck.Types (SomeHST(..))
 import Morley.Michelson.Typed qualified as T
 import Morley.Michelson.Untyped qualified as U
-import Morley.Tezos.Address (Address)
+import Morley.Tezos.Address
 import Morley.Tezos.Crypto (CryptoParseError)
 import Morley.Tezos.Crypto.BLS12381 qualified as BLS
 import Morley.Util.MismatchError
@@ -54,6 +54,7 @@
   | FailwithArgument
   | TicketsJoin
   | ViewBlock
+  | EmitArgument
   deriving stock (Show, Eq, Generic)
   deriving anyclass (NFData)
 
@@ -79,6 +80,7 @@
     FailwithArgument -> "argument to FAILWITH"
     TicketsJoin -> "join of two tickets"
     ViewBlock -> "top-level view block"
+    EmitArgument -> "argument to EMIT"
 
 data TopLevelType
   = TltParameterType
@@ -132,8 +134,10 @@
   -- ^ There are not enough items on stack to perform a certain instruction.
   | IllegalEntrypoint T.EpNameFromRefAnnError
   -- ^ Invalid entrypoint name provided
-  | UnknownContract Address
+  | UnknownContract ContractAddress
   -- ^ Contract with given address is not originated.
+  | TxRollupContract TxRollupAddress
+  -- ^ Provided txr1 address as contract.
   | EntrypointNotFound T.EpName
   -- ^ Given entrypoint is not present.
   | IllegalParamDecl T.ParamEpError
@@ -158,6 +162,13 @@
   -- ^ Empty block of code, like ITER body.
   | AnyError
   -- ^ Generic error when instruction does not match something sensible.
+  | InvalidBigMapId Integer
+  -- ^ A big_map with the given ID was not found.
+  | UnexpectedBigMapType
+  -- ^ We found a big_map with the given big_map ID, but
+  -- its key and/or value types are not the same as the requested types.
+      Integer -- ^ The big_map ID we used to lookup a big_map value.
+      (MismatchError T.T)
   deriving stock (Show, Eq, Generic)
   deriving anyclass (NFData)
 
@@ -194,6 +205,8 @@
       "Not enough items on stack"
     UnknownContract addr ->
       "Contract is not registered:" <+> (renderAnyBuildable addr)
+    TxRollupContract addr ->
+      "txr1 address can not be used as a contract:" <+> (renderAnyBuildable addr)
     IllegalEntrypoint err -> renderDoc context err
     EntrypointNotFound ep ->
       "No such entrypoint" <+> enclose "`" "`" (renderAnyBuildable ep)
@@ -208,6 +221,11 @@
       "Cannot use a terminate instruction (like FAILWITH) in this block"
     EmptyCode -> "Code block is empty"
     AnyError -> "Some of the arguments have invalid types"
+    InvalidBigMapId bigMapId ->
+      "No big_map with ID" <+> renderAnyBuildable bigMapId <+> "was found."
+    UnexpectedBigMapType bigMapId mismatchError ->
+      "A big_map with the ID" <+> renderAnyBuildable bigMapId <+> "was found, but it does not have the expected type."
+      <$$> renderDoc context mismatchError
 
 -- | Type check error
 data TCError
diff --git a/src/Morley/Michelson/TypeCheck/Helpers.hs b/src/Morley/Michelson/TypeCheck/Helpers.hs
--- a/src/Morley/Michelson/TypeCheck/Helpers.hs
+++ b/src/Morley/Michelson/TypeCheck/Helpers.hs
@@ -269,7 +269,7 @@
   mapMSeq appendTypeComment tcSeq
   where
     appendTypeComment packedI@(inp :/ iAndOut) = do
-      verbose <- lift (asks tcVerbose)
+      verbose <- asks' tcVerbose
       pure case (verbose, iAndOut) of
         (True, i ::: out) -> inp :/ Seq i (stackTypeComment out) ::: out
         (True, AnyOutInstr i) -> inp :/ AnyOutInstr (Seq i noStackTypeComment)
@@ -279,7 +279,7 @@
 prependStackTypeComment
   :: SomeInstr inp -> TypeCheckInstrNoExcept (SomeInstr inp)
 prependStackTypeComment packedInstr@(inp :/ _) = do
-  verbose <- lift (asks tcVerbose)
+  verbose <- asks' tcVerbose
   pure if verbose && (not (isNop' packedInstr))
     then mapSomeInstr (Seq (stackTypeComment inp)) packedInstr
     else packedInstr
diff --git a/src/Morley/Michelson/TypeCheck/Instr.hs b/src/Morley/Michelson/TypeCheck/Instr.hs
--- a/src/Morley/Michelson/TypeCheck/Instr.hs
+++ b/src/Morley/Michelson/TypeCheck/Instr.hs
@@ -38,6 +38,7 @@
     , typeCheckStorage
     , typeCheckTopLevelType
     , typeCheckValue
+    , typeCheckValueRunCodeCompat
     , typeVerifyContract
     , typeVerifyParameter
     , typeVerifyStorage
@@ -47,7 +48,6 @@
 
 import Prelude hiding (EQ, GT, LT)
 
-import Control.Lens ((.=))
 import Control.Monad.Except (MonadError, catchError, liftEither, throwError)
 import Data.Constraint ((\\))
 import Data.Default (def)
@@ -74,7 +74,7 @@
 import Morley.Util.MismatchError
 import Morley.Util.Peano
 import Morley.Util.PeanoNatural
-import Morley.Util.Sing (SingI1(..))
+import Morley.Util.Sing (SingIOne, withSingIOne)
 import Morley.Util.Type (knownListFromSingI, onFirst, type (++))
 
 import Morley.Michelson.Untyped qualified as U
@@ -199,7 +199,7 @@
 
     onFailedCodeTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck a
     onFailedCodeTypeCheck ops err = do
-      verbose <- asks tcVerbose
+      verbose <- asks' tcVerbose
       throwError if verbose
         then TCIncompletelyTyped err U.Contract
              { contractParameter = wholeParam
@@ -212,7 +212,7 @@
 
     onFailedFullTypeCheck :: [TypeCheckedOp] -> [U.View' TypeCheckedOp] -> TCError -> TypeCheck a
     onFailedFullTypeCheck ops views err = do
-      verbose <- asks tcVerbose
+      verbose <- asks' tcVerbose
       throwError if verbose
         then TCIncompletelyTyped err U.Contract
              { contractParameter = wholeParam
@@ -278,7 +278,7 @@
     onFailedViewsTypeCheck
       :: U.View -> [TypeCheckedOp] -> TCError -> TypeCheck a
     onFailedViewsTypeCheck v viewOps err = do
-      verbose <- asks tcVerbose
+      verbose <- asks' tcVerbose
       throwError if verbose
         then TCIncompletelyTypedView err v{ U.viewCode = viewOps }
         else err
@@ -306,7 +306,7 @@
     onFailedViewsTypeCheck
       :: Seq (U.View' TypeCheckedOp) -> U.View' TypeCheckedOp -> TCError -> TypeCheck a
     onFailedViewsTypeCheck processedViews v err = do
-      verbose <- asks tcVerbose
+      verbose <- asks' tcVerbose
       throwError if verbose
         then TCIncompletelyTyped err tcCotract
              { U.contractViews = toList (processedViews |> v)
@@ -326,7 +326,7 @@
   => [U.ExpandedOp]
   -> HST inp
   -> TypeCheck (SomeInstr inp)
-typeCheckList = throwingTCError' ... typeCheckListNoExcept
+typeCheckList = throwingTCError ... typeCheckListNoExcept
 
 -- | Function @typeCheckListNoExcept@ converts list of Michelson instructions
 -- given in representation from @Morley.Michelson.Type@ module to representation in a
@@ -354,14 +354,24 @@
 typeCheckValue
   :: forall t. SingI t
   => U.Value
-  -> TypeCheckInstr (Value t)
+  -> TypeCheckResult (Value t)
 typeCheckValue value = do
-  mode <- use tcModeL
-  tcModeL .= TypeCheckValue (value, demote @t)
-  res <- typeCheckValImpl @t Nothing typeCheckInstr value
-  tcModeL .= mode
-  pure res
+  runTypeCheck (TypeCheckValue (value, demote @t) Nothing) $
+    usingReaderT def $
+      typeCheckValImpl Nothing typeCheckInstr value
 
+-- | Simulates the typechecking behavior of the RPC's @/run_code@ endpoint.
+--
+-- If an integer is found where a big_map is expected,
+-- 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 bigMapFinder val =
+  runTypeCheck (TypeCheckValue (val, demote @t) (Just bigMapFinder)) $
+    usingReaderT def $
+      typeCheckValImpl Nothing typeCheckInstr val
+
 typeVerifyParameter
   :: SingI t
   => TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)
@@ -376,7 +386,7 @@
   :: forall t. SingI t
   => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)
 typeVerifyTopLevelType mOriginatedContracts valueU =
-  runTypeCheck (TypeCheckValue (valueU, demote @t)) $ usingReaderT def $
+  runTypeCheck (TypeCheckValue (valueU, demote @t) Nothing) $ usingReaderT def $
     typeCheckValImpl mOriginatedContracts typeCheckInstr valueU
 
 -- | Like 'typeCheckValue', but for values to be used as parameter.
@@ -596,7 +606,10 @@
 
   (U.PUSH vn mt mval, i) -> workOnInstr uInstr $
     withUType mt $ \(nt :: Notes t) -> do
-      val <- typeCheckValue @t mval
+      -- Locally switch 'TypeCheckMode' to 'TypeCheckValue'.
+      val <- local' (tcModeL .~ TypeCheckValue (mval, demote @t) Nothing) $
+        typeCheckValImpl @t Nothing typeCheckInstr mval
+
       proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing
         $ checkScope @(ConstantScope t)
       case proofScope of
@@ -1356,9 +1369,9 @@
   (U.VIEW{}, _) -> notEnoughItemsOnStack
 
   (U.SELF vn fn, _) -> workOnInstr uInstr $ withNotInView uInstr do
-    mode <- gets tcMode
+    mode <- asks' tcMode
     case mode of
-      TypeCheckValue (value, ty) ->
+      TypeCheckValue (value, ty) _ ->
         tcFailedOnValue value ty "The SELF instruction cannot appear in a lambda" Nothing
       TypeCheckContract (SomeParamType notescp) -> do
         let epName = U.epNameFromSelfAnn fn
@@ -1605,6 +1618,22 @@
     failWithErr $ UnexpectedType $ ("sapling_transaction" :| ["sapling_state"]) :| []
   (U.SAPLING_VERIFY_UPDATE _, _) -> notEnoughItemsOnStack
 
+  (U.EMIT{}, SNil) -> notEnoughItemsOnStack
+
+  (U.EMIT va tag mty, ((_ :: SingT t2), Dict) ::& rs) ->
+    workOnInstr uInstr do
+      Dict <- onScopeCheckInstrErr @t2 uInstr (SomeHST inp) Nothing $
+        checkScope @(PackedValScope t2)
+      case mty of
+        Just (AsUType (ty :: Notes t1)) -> do
+          Refl <- errM $ eqType @t1 @t2
+          pure $ inp :/ AnnEMIT (Anns1 va) tag (Just ty) ::: ((sing, Dict) ::& rs)
+        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 = onTypeCheckInstrErr uInstr (SomeHST inp) (Just EmitArgument)
+
   where
     withWTPInstr'
       :: forall t inp. SingI t
@@ -1629,7 +1658,7 @@
     notEnoughItemsOnStack' = failWithErr' NotEnoughItemsOnStack
 
     withNotInView :: U.ExpandedInstr -> (IsNotInView => TypeCheckInstr r) -> TypeCheckInstr r
-    withNotInView instr act = gets tcMode >>= \case
+    withNotInView instr act = asks' tcMode >>= \case
       -- we provide the not-in-view constraint in the isolated mode
       TypeCheckTest -> giveNotInView act
       _ -> view tcieNotInView >>= \case
@@ -1676,7 +1705,7 @@
   :: forall c rs.
     ( MapOp c
     , WellTyped (MapOpInp c)
-    , SingI1 (MapOpRes c)
+    , SingIOne (MapOpRes c)
     )
   => ([TypeCheckedOp] -> TypeCheckedInstr)
   -> SingT (MapOpInp c)
@@ -1696,7 +1725,7 @@
             Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)
               $ eqHST rs rs'
             x <- mkRes bn rs'
-            pure $ i :/ withSingI1 @(MapOpRes c) @v' (AnnMAP (Anns1 anns) sub ::: x)
+            pure $ i :/ withSingIOne @(MapOpRes c) @v' (AnnMAP (Anns1 anns) sub ::: x)
           _ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration)
       AnyOutInstr _ ->
         typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails
@@ -1720,8 +1749,8 @@
     subI ::: o -> do
       Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) $ eqHST o rs
       pure $ i :/ ITER subI ::: o
-    AnyOutInstr _ ->
-      typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails
+    AnyOutInstr subI ->
+      pure $ i :/ ITER subI ::: rs
 
 lamImpl
   :: forall it ot ts .
diff --git a/src/Morley/Michelson/TypeCheck/TypeCheck.hs b/src/Morley/Michelson/TypeCheck/TypeCheck.hs
--- a/src/Morley/Michelson/TypeCheck/TypeCheck.hs
+++ b/src/Morley/Michelson/TypeCheck/TypeCheck.hs
@@ -5,6 +5,7 @@
   ( TcInstrHandler
   , TcOriginatedContracts
   , TypeCheckEnv(..)
+  , BigMapFinder
   , TypeCheckOptions(..)
   , TypeCheck
   , TypeCheckNoExcept
@@ -13,19 +14,18 @@
   , TypeCheckInstr
   , TypeCheckInstrNoExcept
   , runTypeCheckIsolated
-  , runTypeCheckInstrIsolated
   , typeCheckingWith
   , liftNoExcept
-  , liftNoExcept'
   , throwingTCError
-  , throwingTCError'
   , preserving
   , preserving'
   , guarding
   , guarding_
   , tcEither
+  , ask'
+  , asks'
+  , local'
 
-  , tcExtFramesL
   , tcModeL
   , TypeCheckMode(..)
   , SomeParamType(..)
@@ -36,8 +36,7 @@
   ) where
 
 import Control.Lens (makeLenses)
-import Control.Monad.Except (Except, mapExceptT, runExcept, throwError)
-import Control.Monad.Reader (mapReaderT)
+import Control.Monad.Except (Except, MonadError, runExcept, throwError)
 import Data.Constraint (Dict)
 import Data.Default (Default(..))
 import Fmt (Buildable, build, pretty)
@@ -49,29 +48,40 @@
   tcsEither)
 import Morley.Michelson.TypeCheck.Types
 import Morley.Michelson.Typed qualified as T
+import Morley.Michelson.Typed.Existential (SomeVBigMap)
 import Morley.Michelson.Untyped qualified as U
 import Morley.Tezos.Address (ContractHash)
 import Morley.Util.Lens
+import Morley.Util.MultiReader
 
-type TypeCheck =
-  (ReaderT TypeCheckOptions
-    (ExceptT TCError
-      (State TypeCheckEnv)))
+-- | Environments avaliable during typecheck.
+type TCEnvs = '[TypeCheckEnv, TypeCheckOptions]
 
--- | A non-throwing alternative for @TypeCheck@. Mainly meant to be used for
--- construction of a partially typed tree (see @TypeCheckedSeq@).
-type TypeCheckNoExcept =
-  (ReaderT TypeCheckOptions
-    (State TypeCheckEnv))
+-- | A full type-check monad carrying intermediary context (via 'TypeCheckEnv'),
+-- general 'TypeCheckOptions' and throwing 'TCError'.
+type TypeCheck = MultiReaderT TCEnvs (Except TCError)
 
+-- | 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
+
 -- | 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 = ReaderT TypeCheckOptions (Except TCError)
 
+-- | Environments available during instr typecheck
+type TCInstrEnvs = TypeCheckInstrEnv ': TCEnvs
+
+-- | Version of 'TypeCheck' additionally carrying instruction-specific
+-- 'TypeCheckInstrEnv'
+type TypeCheckInstr = MultiReaderT TCInstrEnvs (Except TCError)
+
+-- | Version of 'TypeCheckNoExcept' additionally carrying instruction-specific
+-- 'TypeCheckInstrEnv'
+type TypeCheckInstrNoExcept = MultiReaderT TCInstrEnvs Identity
+
 data SomeParamType = forall t. (T.ParameterScope t) =>
   SomeParamType (T.ParamNotes t)
 
@@ -108,16 +118,29 @@
 -- | Typechecking mode that tells the type checker whether it is typechecking
 -- contract code in actual contract, lambda, or test.
 data TypeCheckMode
-  = TypeCheckValue (U.Value, T.T)
+  = TypeCheckValue
+    -- ^ We're typechecking a value.
+      (U.Value, T.T)
+      (Maybe BigMapFinder)
+      -- ^ When this is a `Just`, we simulate the typechecking behavior of the RPC's @/run_code@ endpoint.
+      --
+      -- If an integer is found where a big_map is expected,
+      -- we use 'BigMapFinder' to 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.
   | TypeCheckContract SomeParamType
+    -- ^ We're typechecking a contract.
   | TypeCheckTest
+    -- ^ We're typechecking a set of instructions in a "test" environment like a REPL,
+    -- where the instruction @SELF@ would not make sense.
 
 -- | The typechecking state
 data TypeCheckEnv = TypeCheckEnv
-  { tcExtFrames :: ~TcExtFrames
-  , tcMode :: ~TypeCheckMode
+  { tcMode :: ~TypeCheckMode
   }
 
+type BigMapFinder = Natural -> Maybe SomeVBigMap
+
 data TypeCheckOptions = TypeCheckOptions
   { tcVerbose :: Bool
     -- ^ Whether to add stack type comments after every
@@ -139,11 +162,16 @@
 instance Default TypeCheckOptions where
   def = TypeCheckOptions{ tcVerbose = False, tcStrict = True }
 
+data TypeCheckInstrEnv = TypeCheckInstrEnv
+  { _tcieErrorPos :: ErrorSrcPos
+  , _tcieNotInView :: Maybe (Dict T.IsNotInView)
+  }
+
 makeLensesWith postfixLFields ''TypeCheckEnv
+makeLenses ''TypeCheckInstrEnv
 
 runTypeCheck :: TypeCheckMode -> TypeCheck a -> TypeCheckResult a
-runTypeCheck mode =
-  mapReaderT $ mapExceptT $ evaluatingStateT (TypeCheckEnv [] mode)
+runTypeCheck = usingReaderT . TypeCheckEnv
 
 -- | Run type checker as if it worked isolated from other world -
 -- no access to environment of the current contract is allowed.
@@ -153,65 +181,35 @@
 -- 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 a -> TypeCheckResult a
+runTypeCheckIsolated :: TypeCheck (SomeInstr t) -> TypeCheckResult (SomeInstr t)
 runTypeCheckIsolated = runTypeCheck TypeCheckTest
 
 typeCheckingWith :: TypeCheckOptions -> TypeCheckResult a -> Either TCError a
 typeCheckingWith options = runExcept . usingReaderT options
 
-type TypeCheckInstr =
-  ReaderT TypeCheckInstrEnv TypeCheck
-
-type TypeCheckInstrNoExcept =
-  ReaderT TypeCheckInstrEnv TypeCheckNoExcept
-
-data TypeCheckInstrEnv = TypeCheckInstrEnv
-  { _tcieErrorPos :: ErrorSrcPos
-  , _tcieNotInView :: Maybe (Dict T.IsNotInView)
-  }
-
-makeLenses ''TypeCheckInstrEnv
-
 instance Default TypeCheckInstrEnv where
   def = TypeCheckInstrEnv def Nothing
 
--- | Similar to 'runTypeCheckIsolated', but for 'TypeCheckInstr.'
-runTypeCheckInstrIsolated :: TypeCheckInstr a -> TypeCheckResult a
-runTypeCheckInstrIsolated = runTypeCheckIsolated . flip runReaderT def
-
-liftNoExcept :: TypeCheckInstrNoExcept a -> TypeCheckInstr a
-liftNoExcept action = (pure action)
-                 <**> (usingReaderT <$> ask)
-                 <**> (usingReaderT <$> lift ask)
-                 <**> (evaluatingState <$> get)
-
-liftNoExcept' :: TypeCheckNoExcept a -> TypeCheck a
-liftNoExcept' action = (pure action)
-                  <**> (usingReaderT <$> ask)
-                  <**> (evaluatingState <$> get)
+liftNoExcept
+  :: forall m e (a :: Type). MonadMultiReaderT m Identity
+  => m a
+  -> ChangeMultiReaderBase m (Except e) a
+liftNoExcept action = mapMultiReaderT (pure @(Except e) . runIdentity) action
 
 throwingTCError
-  :: TypeCheckInstrNoExcept (TypeCheckedSeq inp) -> TypeCheckInstr (SomeInstr inp)
-throwingTCError action = liftNoExcept action
-  >>= tcsEither (const throwError) (pure)
-
-throwingTCError'
-  :: TypeCheckNoExcept (TypeCheckedSeq inp) -> TypeCheck (SomeInstr inp)
-throwingTCError' action = liftNoExcept' action
-  >>= tcsEither (const throwError) (pure)
+  :: ( MonadMultiReaderT m Identity
+     , m' ~ ChangeMultiReaderBase m (Except TCError)
+     , MonadError TCError m'
+     )
+  => m (TypeCheckedSeq inp) -> m' (SomeInstr inp)
+throwingTCError action = liftNoExcept @_ @TCError 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
-tcEither onErr onOk action = do
-  res <- (pure action)
-    <**> (usingReaderT <$> ask)
-    <**> (usingReaderT <$> lift ask)
-    <**> (pure runExceptT)
-    <**> (evaluatingState <$> get)
-  either onErr onOk res
+tcEither onErr onOk action = either onErr onOk =<< mapMultiReaderT (pure . runExcept) action
 
 -- | Perform a throwing action on an acquired instruction. Preserve the acquired
 -- result by embedding it into a type checking tree with a specified parent
diff --git a/src/Morley/Michelson/TypeCheck/Types.hs b/src/Morley/Michelson/TypeCheck/Types.hs
--- a/src/Morley/Michelson/TypeCheck/Types.hs
+++ b/src/Morley/Michelson/TypeCheck/Types.hs
@@ -8,7 +8,6 @@
     , SomeInstrOut (..)
     , SomeInstr (..)
     , BoundVars (..)
-    , TcExtFrames
     , withWTPm
     , unsafeWithWTP
     , mapSomeContract
@@ -174,9 +173,6 @@
 
 noBoundVars :: BoundVars
 noBoundVars = BoundVars Map.empty Nothing
-
--- | State for type checking @nop@
-type TcExtFrames = [BoundVars]
 
 -- | Given a type and an action that requires evidence that the type is well typed,
 --  generate the evidence and execute the action, or else fail with an error.
diff --git a/src/Morley/Michelson/TypeCheck/Value.hs b/src/Morley/Michelson/TypeCheck/Value.hs
--- a/src/Morley/Michelson/TypeCheck/Value.hs
+++ b/src/Morley/Michelson/TypeCheck/Value.hs
@@ -20,14 +20,13 @@
 import Morley.Michelson.TypeCheck.Error (TCError(..), TCTypeError(..))
 import Morley.Michelson.TypeCheck.Helpers
 import Morley.Michelson.TypeCheck.TypeCheck
-  (SomeParamType(..), TcInstrHandler, TcOriginatedContracts, TypeCheckInstr, TypeCheckOptions(..),
-  tcieErrorPos, tcieNotInView, throwingTCError)
 import Morley.Michelson.TypeCheck.Types
-import Morley.Michelson.Typed (EpAddress(..), Notes(..), SingT(..), Value'(..))
+import Morley.Michelson.Typed
+  (EpAddress(..), Notes(..), SingT(..), SomeVBigMap(..), Value'(..), castM)
 import Morley.Michelson.Typed qualified as T
 import Morley.Michelson.Typed.Contract (giveNotInView)
 import Morley.Michelson.Untyped qualified as U
-import Morley.Tezos.Address (Address(..), TxRollupL2Address(..))
+import Morley.Tezos.Address
 import Morley.Tezos.Core
 import Morley.Tezos.Crypto
 import Morley.Tezos.Crypto.BLS12381 qualified as BLS
@@ -65,225 +64,241 @@
 typeCheckValImpl mOriginatedContracts tcDo uv = doTypeCheckVal (uv, sing @ty)
   where
     doTypeCheckVal :: forall tz. (U.Value, Sing tz) -> TypeCheckInstr (T.Value tz)
-    doTypeCheckVal (uvalue, sng) = case (uvalue, sng) of
-      (U.ValueInt i, STInt) -> pure $ T.VInt i
-      (v@(U.ValueInt i), t@STNat)
-        | i >= 0 -> pure $ VNat (fromInteger i)
-        | otherwise -> tcFailedOnValue v (fromSing t) "" (Just NegativeNat)
-      (v@(U.ValueInt i), t@STMutez) -> case mkMutez i of
-        Right m -> pure $ VMutez m
-        Left err -> tcFailedOnValue v (fromSing t) err (Just InvalidTimestamp)
-      (U.ValueString s, STString) -> pure $ VString s
-      (v@(U.ValueString s), t@STAddress) -> case T.parseEpAddress (unMText s) of
-        Right addr -> pure $ VAddress addr
-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)
-      (v@(U.ValueBytes b), t@STAddress) -> case T.parseEpAddressRaw (U.unInternalByteString b) of
-        Right addr -> pure $ VAddress addr
-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)
-      (v@(U.ValueString s), t@STKeyHash) -> case parseHash (unMText s)  of
-        Right kHash -> pure $ VKeyHash kHash
-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
-      (v@(U.ValueBytes b), t@STKeyHash) ->
-        case parseKeyHashRaw (U.unInternalByteString b) of
+    doTypeCheckVal (uvalue, sng) = do
+      typeCheckMode <- asks' tcMode
+      case (uvalue, sng) of
+        (U.ValueInt i, STInt) -> pure $ T.VInt i
+        (v@(U.ValueInt i), t@STNat)
+          | i >= 0 -> pure $ VNat (fromInteger i)
+          | otherwise -> tcFailedOnValue v (fromSing t) "" (Just NegativeNat)
+        (v@(U.ValueInt i), t@STMutez) -> case mkMutez i of
+          Right m -> pure $ VMutez m
+          Left err -> tcFailedOnValue v (fromSing t) err (Just InvalidTimestamp)
+
+        -- If `tcBigMaps` is a `Just`, then we simulate the behavior of the RPC
+        -- @/run_code@ endpoint.
+        -- If a value contains a natural number where a big_map is expected,
+        -- we assume that number represents a big_map ID and replace it with
+        -- the corresponding big_map value (if it exists and has the expected key/value types).
+        (U.ValueInt bigMapId, STBigMap {}) | TypeCheckValue _ (Just bigMapFinder) <- typeCheckMode -> do
+          let bigMapMaybe = bigMapFinder =<< fromIntegralMaybe @Integer @Natural bigMapId
+          case bigMapMaybe of
+            Just (SomeVBigMap (bigMap@VBigMap{} :: T.Value actualT)) ->
+              withSingI sng $ castM @actualT @tz bigMap $
+                tcFailedOnValue uvalue (fromSing sng) "" . Just . UnexpectedBigMapType bigMapId
+            Nothing ->
+              tcFailedOnValue uvalue (fromSing sng) "" (Just (InvalidBigMapId bigMapId))
+        (U.ValueString s, STString) -> pure $ VString s
+        (v@(U.ValueString s), t@STAddress) -> case T.parseEpAddress (unMText s) of
+          Right addr -> pure $ VAddress addr
+          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)
+        (v@(U.ValueBytes b), t@STAddress) -> case T.parseEpAddressRaw (U.unInternalByteString b) of
+          Right addr -> pure $ VAddress addr
+          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidAddress err)
+        (v@(U.ValueString s), t@STKeyHash) -> case parseHash (unMText s)  of
           Right kHash -> pure $ VKeyHash kHash
           Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
-      (v@(U.ValueString s), t@STTxRollupL2Address) -> case parseHash (unMText s)  of
-        Right kHash -> pure $ VTxRollupL2Address $ TxRollupL2Address kHash
-        Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
-      (v@(U.ValueBytes b), t@STTxRollupL2Address) ->
-        case parseKeyHashL2Raw (U.unInternalByteString b) of
+        (v@(U.ValueBytes b), t@STKeyHash) ->
+          case parseKeyHashRaw (U.unInternalByteString b) of
+            Right kHash -> pure $ VKeyHash kHash
+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
+        (v@(U.ValueString s), t@STTxRollupL2Address) -> case parseHash (unMText s)  of
           Right kHash -> pure $ VTxRollupL2Address $ TxRollupL2Address kHash
           Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
-      (U.ValueInt i, STBls12381Fr) ->
-        pure $ VBls12381Fr (fromIntegralOverflowing @Integer @Bls12381Fr i)
-      (v@(U.ValueBytes b), t@STBls12381Fr) ->
-        case BLS.fromMichelsonBytes (U.unInternalByteString b) of
-          Right val -> pure $ VBls12381Fr val
-          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
-      (v@(U.ValueBytes b), t@STBls12381G1) ->
-        case BLS.fromMichelsonBytes (U.unInternalByteString b) of
-          Right val -> pure $ VBls12381G1 val
-          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
-      (v@(U.ValueBytes b), t@STBls12381G2) ->
-        case BLS.fromMichelsonBytes (U.unInternalByteString b) of
-          Right val -> pure $ VBls12381G2 val
-          Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
-      (v@(U.ValueString s), t@STTimestamp) -> case parseTimestamp $ unMText s of
-        Just tstamp -> pure $ VTimestamp tstamp
-        Nothing -> tcFailedOnValue v (fromSing t) "" (Just InvalidTimestamp)
-      (U.ValueInt i, STTimestamp) -> pure $ VTimestamp (timestampFromSeconds i)
-      (U.ValueBytes (U.InternalByteString s), STBytes) -> pure $ VBytes s
-      (U.ValueTrue, STBool) -> pure $ VBool True
-      (U.ValueFalse, STBool) -> pure $ VBool False
+        (v@(U.ValueBytes b), t@STTxRollupL2Address) ->
+          case parseKeyHashL2Raw (U.unInternalByteString b) of
+            Right kHash -> pure $ VTxRollupL2Address $ TxRollupL2Address kHash
+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidKeyHash err)
+        (U.ValueInt i, STBls12381Fr) ->
+          pure $ VBls12381Fr (fromIntegralOverflowing @Integer @Bls12381Fr i)
+        (v@(U.ValueBytes b), t@STBls12381Fr) ->
+          case BLS.fromMichelsonBytes (U.unInternalByteString b) of
+            Right val -> pure $ VBls12381Fr val
+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
+        (v@(U.ValueBytes b), t@STBls12381G1) ->
+          case BLS.fromMichelsonBytes (U.unInternalByteString b) of
+            Right val -> pure $ VBls12381G1 val
+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
+        (v@(U.ValueBytes b), t@STBls12381G2) ->
+          case BLS.fromMichelsonBytes (U.unInternalByteString b) of
+            Right val -> pure $ VBls12381G2 val
+            Left err -> tcFailedOnValue v (fromSing t) "" (Just $ InvalidBls12381Object err)
+        (v@(U.ValueString s), t@STTimestamp) -> case parseTimestamp $ unMText s of
+          Just tstamp -> pure $ VTimestamp tstamp
+          Nothing -> tcFailedOnValue v (fromSing t) "" (Just InvalidTimestamp)
+        (U.ValueInt i, STTimestamp) -> pure $ VTimestamp (timestampFromSeconds i)
+        (U.ValueBytes (U.InternalByteString s), STBytes) -> pure $ VBytes s
+        (U.ValueTrue, STBool) -> pure $ VBool True
+        (U.ValueFalse, STBool) -> pure $ VBool False
 
-      (U.ValueString (parsePublicKey . unMText -> Right s), STKey) ->
-        pure $ T.VKey s
-      (U.ValueBytes (parsePublicKeyRaw . U.unInternalByteString -> Right s), STKey) ->
-        pure $ VKey s
+        (U.ValueString (parsePublicKey . unMText -> Right s), STKey) ->
+          pure $ T.VKey s
+        (U.ValueBytes (parsePublicKeyRaw . U.unInternalByteString -> Right s), STKey) ->
+          pure $ VKey s
 
-      (U.ValueString (parseSignature . unMText -> Right s), STSignature) ->
-        pure $ VSignature s
-      (U.ValueBytes (parseSignatureRaw . U.unInternalByteString  -> Right s), STSignature) ->
-        pure $ VSignature s
+        (U.ValueString (parseSignature . unMText -> Right s), STSignature) ->
+          pure $ VSignature s
+        (U.ValueBytes (parseSignatureRaw . U.unInternalByteString  -> Right s), STSignature) ->
+          pure $ VSignature s
 
-      (U.ValueString (parseChainId . unMText -> Right ci), STChainId) ->
-        pure $ VChainId ci
-      (U.ValueBytes (mkChainId . U.unInternalByteString -> Right ci), STChainId) ->
-        pure $ VChainId ci
+        (U.ValueString (parseChainId . unMText -> Right ci), STChainId) ->
+          pure $ VChainId ci
+        (U.ValueBytes (mkChainId . U.unInternalByteString -> Right ci), STChainId) ->
+          pure $ VChainId ci
 
-      (cv@(U.ValueString (T.parseEpAddress . unMText -> Right addr))
-        , STContract pc) -> typecheckContractValue cv addr pc
-      (cv@(U.ValueBytes (T.parseEpAddressRaw . U.unInternalByteString -> Right addr))
-        , STContract pc) -> typecheckContractValue cv addr pc
+        (cv@(U.ValueString (T.parseEpAddress . unMText -> Right addr))
+          , STContract pc) -> typecheckContractValue cv addr pc
+        (cv@(U.ValueBytes (T.parseEpAddressRaw . U.unInternalByteString -> Right addr))
+          , STContract pc) -> typecheckContractValue cv addr pc
 
-      (cv, s@(STTicket vt)) -> lift (asks tcStrict) >>= \case
-        -- Note [Tickets forging]
-        -- Normally, ticket values cannot be constructed manually (i.e. forged)
-        -- 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
-        -- manually constructed ticket value as parameter or initial storage.
-        True ->
-          tcFailedOnValue cv (fromSing sng)
-            "ticket values cannot be forged in real operations"
-            Nothing
-        False -> case cv of
-          U.ValuePair addrV (U.ValuePair datV amV) -> withComparable vt cv s $ do
-            addrValue <- doTypeCheckVal (addrV, STAddress)
-            dat <- doTypeCheckVal (datV, vt)
-            amountValue <- doTypeCheckVal (amV, STNat)
-            case (addrValue, amountValue) of
-              (VAddress (EpAddress addr ep), VNat am) -> do
-                unless (U.isDefEpName ep) $
-                  tcFailedOnValue cv (fromSing sng)
-                    "it is pointless to provide an address with entrypoint as a \
-                    \ticketer, we do not support that"
-                    Nothing
-                -- ↑ Tezos allows passing addresses with entrypoint, but it is
-                -- not possible to sanely work with them after that anyway,
-                -- since @TICKET@ instruction (the only valid way of constructing
-                -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.
-                return $ VTicket addr dat am
-          _ ->
+        (cv, s@(STTicket vt)) -> asks' tcStrict >>= \case
+          -- Note [Tickets forging]
+          -- Normally, ticket values cannot be constructed manually (i.e. forged)
+          -- 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
+          -- manually constructed ticket value as parameter or initial storage.
+          True ->
             tcFailedOnValue cv (fromSing sng)
-              "ticket type expects a value of type `(pair address <data> nat)`"
+              "ticket values cannot be forged in real operations"
               Nothing
+          False -> case cv of
+            U.ValuePair addrV (U.ValuePair datV amV) -> withComparable vt cv s $ do
+              addrValue <- doTypeCheckVal (addrV, STAddress)
+              dat <- doTypeCheckVal (datV, vt)
+              amountValue <- doTypeCheckVal (amV, STNat)
+              case (addrValue, amountValue) of
+                (VAddress (EpAddress' addr ep), VNat am) -> do
+                  unless (U.isDefEpName ep) $
+                    tcFailedOnValue cv (fromSing sng)
+                      "it is pointless to provide an address with entrypoint as a \
+                      \ticketer, we do not support that"
+                      Nothing
+                  -- ↑ Tezos allows passing addresses with entrypoint, but it is
+                  -- not possible to sanely work with them after that anyway,
+                  -- since @TICKET@ instruction (the only valid way of constructing
+                  -- tickets in real run) uses @SELF_ADDRESS@ result as ticketer.
+                  pure $ VTicket addr dat am
+            _ ->
+              tcFailedOnValue cv (fromSing sng)
+                "ticket type expects a value of type `(pair address <data> nat)`"
+                Nothing
 
-      (U.ValueUnit, STUnit) -> pure $ VUnit
-      (U.ValuePair ml mr, STPair lt rt) -> do
-        l <- doTypeCheckVal (ml, lt)
-        r <- doTypeCheckVal (mr, rt)
-        pure $ VPair (l, r)
-      (U.ValueLeft ml, STOr lt rt) -> do
-        l <- doTypeCheckVal (ml, lt)
-        withSingI lt $ withSingI rt $ pure $ VOr (Left l)
-      (U.ValueRight mr, STOr lt rt) -> do
-        r <- doTypeCheckVal (mr, rt)
-        withSingI lt $ withSingI rt $ pure $ VOr (Right r)
-      (U.ValueSome mv, STOption op) -> do
-        v <- doTypeCheckVal (mv, op)
-        withSingI op $ pure $ VOption (Just v)
-      (U.ValueNone, STOption op) -> do
-        withSingI op $ pure $ VOption Nothing
+        (U.ValueUnit, STUnit) -> pure $ VUnit
+        (U.ValuePair ml mr, STPair lt rt) -> do
+          l <- doTypeCheckVal (ml, lt)
+          r <- doTypeCheckVal (mr, rt)
+          pure $ VPair (l, r)
+        (U.ValueLeft ml, STOr lt rt) -> do
+          l <- doTypeCheckVal (ml, lt)
+          withSingI lt $ withSingI rt $ pure $ VOr (Left l)
+        (U.ValueRight mr, STOr lt rt) -> do
+          r <- doTypeCheckVal (mr, rt)
+          withSingI lt $ withSingI rt $ pure $ VOr (Right r)
+        (U.ValueSome mv, STOption op) -> do
+          v <- doTypeCheckVal (mv, op)
+          withSingI op $ pure $ VOption (Just v)
+        (U.ValueNone, STOption op) -> do
+          withSingI op $ pure $ VOption Nothing
 
-      (U.ValueNil, STList l) -> withSingI l $
-        pure $ T.VList []
+        (U.ValueNil, STList l) -> withSingI l $
+          pure $ T.VList []
 
-      -- If ValueSeq contains at least 2 elements, it can be type checked as a
-      -- right combed pair.
-      (U.ValueSeq vals@(_ :| (_ : _)), STPair _ _) ->
-        doTypeCheckVal (seqToRightCombedPair vals, sng)
+        -- If ValueSeq contains at least 2 elements, it can be type checked as a
+        -- right combed pair.
+        (U.ValueSeq vals@(_ :| (_ : _)), STPair _ _) ->
+          doTypeCheckVal (seqToRightCombedPair vals, sng)
 
-      (U.ValueSeq (toList -> mels), STList l) -> do
-        els <- typeCheckValsImpl (mels, l)
-        withSingI l $ pure $ VList els
+        (U.ValueSeq (toList -> mels), STList l) -> do
+          els <- typeCheckValsImpl (mels, l)
+          withSingI l $ pure $ VList els
 
-      (U.ValueNil, STSet s) -> do
-        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"
-            instrPos (Just $ UnsupportedTypeForScope (fromSing s) T.BtNotComparable)
+        (U.ValueNil, STSet s) -> do
+          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"
+              instrPos (Just $ UnsupportedTypeForScope (fromSing s) T.BtNotComparable)
 
-      (sq@(U.ValueSeq (toList -> mels)), s@(STSet vt)) -> withComparable vt sq s $ do
-        instrPos <- view tcieErrorPos
+        (sq@(U.ValueSeq (toList -> mels)), s@(STSet vt)) -> withComparable vt sq s $ do
+          instrPos <- view tcieErrorPos
 
-        els <- typeCheckValsImpl (mels, vt)
-        elsS <- liftEither $ S.fromDistinctAscList <$> ensureDistinctAsc id els
-                  `onFirst` \msg -> TCFailedOnValue sq (fromSing vt) msg instrPos Nothing
-        withSingI vt $ pure $ VSet elsS
+          els <- typeCheckValsImpl (mels, vt)
+          elsS <- liftEither $ S.fromDistinctAscList <$> ensureDistinctAsc id els
+                    `onFirst` \msg -> TCFailedOnValue sq (fromSing vt) msg instrPos Nothing
+          withSingI vt $ pure $ VSet elsS
 
-      (v@U.ValueNil, s@(STMap st vt)) ->
-        withSingI st $ withSingI vt $ withComparable st v s $ pure $ T.VMap M.empty
+        (v@U.ValueNil, s@(STMap st vt)) ->
+          withSingI st $ withSingI vt $ withComparable st v s $ pure $ T.VMap M.empty
 
-      (sq@(U.ValueMap (toList -> mels)), s@(STMap kt vt)) ->
-        withComparable kt sq s $ do
-          keyOrderedElts <- typeCheckMapVal mels sq kt vt
-          withSingI kt $ withSingI vt $
-            pure $ VMap (M.fromDistinctAscList keyOrderedElts)
+        (sq@(U.ValueMap (toList -> mels)), s@(STMap kt vt)) ->
+          withComparable kt sq s $ do
+            keyOrderedElts <- typeCheckMapVal mels sq kt vt
+            withSingI kt $ withSingI vt $
+              pure $ VMap (M.fromDistinctAscList keyOrderedElts)
 
-      (v@U.ValueNil, s@(STBigMap st1 st2)) ->
-        withSingI st1 $ withSingI st2 $ withComparable st1 v s $ withBigMapAbsence st2 v s $
-          pure $ VBigMap Nothing M.empty
+        (v@U.ValueNil, s@(STBigMap st1 st2)) ->
+          withSingI st1 $ withSingI st2 $ withComparable st1 v s $ withBigMapAbsence st2 v s $
+            pure $ VBigMap Nothing M.empty
 
-      (sq@(U.ValueMap (toList -> mels)), s@(STBigMap kt vt)) ->
-        withComparable kt sq s $ withBigMapAbsence vt sq s $ do
-          keyOrderedElts <- typeCheckMapVal mels sq kt vt
-          withSingI kt $ withSingI vt $
-            pure $ VBigMap Nothing (M.fromDistinctAscList keyOrderedElts)
+        (sq@(U.ValueMap (toList -> mels)), s@(STBigMap kt vt)) ->
+          withComparable kt sq s $ withBigMapAbsence vt sq s $ do
+            keyOrderedElts <- typeCheckMapVal mels sq kt vt
+            withSingI kt $ withSingI vt $
+              pure $ VBigMap Nothing (M.fromDistinctAscList keyOrderedElts)
 
-      -- `{ {} }` can be typechecked either as `VLam` or `VList`.
-      (U.ValueLambda s, STList l) ->
-        case emptyLambdaAsList s of
-          Just xs -> doTypeCheckVal (xs, sng)
-          Nothing -> tcFailedOnValue uvalue (fromSing l) "" Nothing
+        -- `{ {} }` can be typechecked either as `VLam` or `VList`.
+        (U.ValueLambda s, STList l) ->
+          case emptyLambdaAsList s of
+            Just xs -> doTypeCheckVal (xs, sng)
+            Nothing -> tcFailedOnValue uvalue (fromSing l) "" Nothing
 
-      (U.ValueSeq s, STLambda _ _) -> case emptyListAsLambda s of
-        Just xs -> doTypeCheckVal (xs, sng)
-        Nothing -> tcFailedOnValue uvalue (fromSing sng) "" Nothing
+        (U.ValueSeq s, STLambda _ _) -> case emptyListAsLambda s of
+          Just xs -> doTypeCheckVal (xs, sng)
+          Nothing -> tcFailedOnValue uvalue (fromSing sng) "" Nothing
 
-      (v, STLambda (var :: Sing it) (b :: Sing ot)) -> withSingI var $ withSingI b $ do
-        mp <- case v of
-          U.ValueNil       -> pure []
-          U.ValueLambda mp -> pure $ toList mp
-          _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing
-        _ :/ instr <-
-          withWTP @it uvalue $ throwingTCError $
-            typeCheckImpl
-              -- lambdas can contain operations forbidden inside views, hence
-              -- we invent a "not in view" constraint here.
-              (giveNotInView $ local (set tcieNotInView $ Just Dict) ... tcDo)
-              mp
-              ((sing @it, Dict) ::& SNil)
-        case instr of
-          lam ::: (lo :: HST lo) -> withWTP @ot uvalue $ do
-            case eqHST1 @ot lo of
-              Right Refl -> do
-                pure $ T.mkVLam (T.RfNormal lam)
-              Left m ->
-                tcFailedOnValue v (demote @ty)
-                        "wrong output type of lambda's value:" (Just m)
-          AnyOutInstr lam ->
-            pure $ T.mkVLam (T.RfAlwaysFails lam)
+        (v, STLambda (var :: Sing it) (b :: Sing ot)) -> withSingI var $ withSingI b $ do
+          mp <- case v of
+            U.ValueNil       -> pure []
+            U.ValueLambda mp -> pure $ toList mp
+            _ -> tcFailedOnValue v (demote @ty) "unexpected value" Nothing
+          _ :/ instr <-
+            withWTP @it uvalue $ throwingTCError $
+              typeCheckImpl
+                -- lambdas can contain operations forbidden inside views, hence
+                -- we invent a "not in view" constraint here.
+                (giveNotInView $ local (set tcieNotInView $ Just Dict) ... tcDo)
+                mp
+                ((sing @it, Dict) ::& SNil)
+          case instr of
+            lam ::: (lo :: HST lo) -> withWTP @ot uvalue $ do
+              case eqHST1 @ot lo of
+                Right Refl -> do
+                  pure $ T.mkVLam (T.RfNormal lam)
+                Left m ->
+                  tcFailedOnValue v (demote @ty)
+                          "wrong output type of lambda's value:" (Just m)
+            AnyOutInstr lam ->
+              pure $ T.mkVLam (T.RfAlwaysFails lam)
 
-      (v@(U.ValueBytes (U.InternalByteString bs)), STChest) ->
-        case chestFromBytes bs of
-          Right res -> pure $ VChest res
-          Left err -> tcFailedOnValue v T.TChest err Nothing
+        (v@(U.ValueBytes (U.InternalByteString bs)), STChest) ->
+          case chestFromBytes bs of
+            Right res -> pure $ VChest res
+            Left err -> tcFailedOnValue v T.TChest err Nothing
 
-      (v@(U.ValueBytes (U.InternalByteString bs)), STChestKey) ->
-        case chestKeyFromBytes bs of
-          Right res -> pure $ VChestKey res
-          Left err -> tcFailedOnValue v T.TChestKey err Nothing
+        (v@(U.ValueBytes (U.InternalByteString bs)), STChestKey) ->
+          case chestKeyFromBytes bs of
+            Right res -> pure $ VChestKey res
+            Left err -> tcFailedOnValue v T.TChestKey err Nothing
 
-      (v, t@(STSaplingState _)) -> tcFailedOnValue v (fromSing t)
-        "sapling_state is not supported" Nothing
+        (v, t@(STSaplingState _)) -> tcFailedOnValue v (fromSing t)
+          "sapling_state is not supported" Nothing
 
-      (v, t@(STSaplingTransaction _)) -> tcFailedOnValue v (fromSing t)
-        "sapling_transaction is not supported" Nothing
+        (v, t@(STSaplingTransaction _)) -> tcFailedOnValue v (fromSing t)
+          "sapling_transaction is not supported" Nothing
 
-      (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing
+        (v, t) -> tcFailedOnValue v (fromSing t) "unknown value" Nothing
 
     seqToRightCombedPair :: (NonEmpty $ U.Value) -> U.Value
     seqToRightCombedPair (x :| [y]) = U.ValuePair x y
@@ -364,9 +379,9 @@
             "Unsupported type in type argument of 'contract' type" instrPos $
               Just $ UnsupportedTypeForScope (fromSing pc) reason
       case addr of
-        KeyAddress _ -> do
+        ImplicitAddress _ -> do
           Refl <- ensureTypeMatches @'T.TUnit
-          pure $ VContract addr T.sepcPrimitive
+          pure $ VContract (MkAddress addr) T.sepcPrimitive
         ContractAddress ca -> case mOriginatedContracts of
           Nothing -> liftEither . Left $ unsupportedType T.BtHasContract
           Just originatedContracts -> case M.lookup ca originatedContracts of
@@ -378,13 +393,13 @@
                   EntrypointNotFound epName
                 Just (T.MkEntrypointCallRes (_ :: Notes t') epc) -> do
                   Refl <- ensureTypeMatches @t'
-                  pure $ VContract addr (T.SomeEpc epc)
+                  pure $ VContract (MkAddress addr) (T.SomeEpc epc)
             Nothing ->
               throwError $ TCFailedOnValue cv (demote @ty) "Contract literal unknown"
                 instrPos (Just $ UnknownContract addr)
-        TransactionRollupAddress _ ->
+        TxRollupAddress _ ->
           throwError $ TCFailedOnValue cv (demote @ty) "txr1 address passed as contract"
-                instrPos (Just $ UnknownContract addr)
+                instrPos (Just $ TxRollupContract addr)
 
 withComparable
   :: forall a (t :: T.T) ty. Sing a
diff --git a/src/Morley/Michelson/Typed/Convert.hs b/src/Morley/Michelson/Typed/Convert.hs
--- a/src/Morley/Michelson/Typed/Convert.hs
+++ b/src/Morley/Michelson/Typed/Convert.hs
@@ -48,7 +48,7 @@
 import Morley.Michelson.Typed.View
 import Morley.Michelson.Untyped qualified as U
 import Morley.Michelson.Untyped.Annotation (Annotation(unAnnotation))
-import Morley.Tezos.Address hiding (ta)
+import Morley.Tezos.Address
 import Morley.Tezos.Core
   (ChainId(unChainId), mformatChainId, parseChainId, timestampFromSeconds, timestampToSeconds, tz,
   unMutez)
@@ -204,15 +204,15 @@
   (VContract addr sepc, _) ->
     case opts of
       Readable  ->
-        U.ValueString . mformatEpAddress $ EpAddress addr (sepcName sepc)
+        U.ValueString . mformatEpAddress $ EpAddress' addr (sepcName sepc)
       _         -> U.ValueBytes . U.InternalByteString . encodeEpAddress $
-        EpAddress addr (sepcName sepc)
+        EpAddress' addr (sepcName sepc)
   (VChest c, _) -> U.ValueBytes . U.InternalByteString $ chestBytes c
   (VChestKey c, _) -> U.ValueBytes . U.InternalByteString $ chestKeyBytes c
   (VTicket s v a, STTicket vt) ->
     case valueTypeSanity v of
       Dict ->
-        let us = untypeValueImpl opts STAddress $ VAddress (EpAddress s DefEpName)
+        let us = untypeValueImpl opts STAddress $ VAddress (EpAddress' s DefEpName)
             uv = untypeValueImpl opts vt v
             ua = untypeValueImpl opts STNat $ VNat a
         in case opts of
@@ -277,13 +277,13 @@
     encodeEpAddress (EpAddress addr epName) =
       encodeAddress addr <> encodeEpName epName
 
-    encodeAddress :: Address -> ByteString
+    encodeAddress :: KindedAddress kind -> ByteString
     encodeAddress = \case
-      KeyAddress keyHash ->
+      ImplicitAddress keyHash ->
         "\x00" <> hashToBytes keyHash
       ContractAddress hash ->
         "\x01" <> hashToBytes hash <> "\x00"
-      TransactionRollupAddress hash ->
+      TxRollupAddress hash ->
         "\x02" <> hashToBytes hash <> "\x00"
 
     encodeEpName :: EpName -> ByteString
@@ -470,6 +470,7 @@
         annotateInstr ann U.SAPLING_EMPTY_STATE (singPeanoVal s)
       AnnSAPLING_VERIFY_UPDATE ann -> annotateInstr ann U.SAPLING_VERIFY_UPDATE
       AnnMIN_BLOCK_TIME ann -> U.MIN_BLOCK_TIME ann
+      AnnEMIT va tag ty -> annotateInstr va U.EMIT tag $ mkUType <$> ty
 
 untypeStackRef :: StackRef s -> U.StackRef
 untypeStackRef (StackRef n) = U.StackRef (fromPeanoNatural n)
@@ -582,7 +583,7 @@
       dat <- sampleTypedValue t
       VNat amount <- sampleTypedValue STNat
       case cmpProof of
-        Dict -> return $ VTicket (eaAddress sampleAddress) dat amount
+        Dict -> return $ VTicket (MkAddress sampleCTAddress) dat amount
     STPair t1 t2 -> withSingI t1 $ withSingI t2 $ do
       val1 <- sampleTypedValue t1
       val2 <- sampleTypedValue t2
@@ -610,7 +611,8 @@
           pure $ mkVLam $ RfNormal (DROP `Seq` PUSH val)
         _ -> pure $ mkVLam $ RfAlwaysFails (PUSH (VString [mt|lambda sample|]) `Seq` FAILWITH)
     where
-      sampleAddress = (unsafe . parseEpAddress) "KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB"
+      sampleCTAddress = [ta|KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB|]
+      sampleAddress = unsafe . parseEpAddress $ formatAddress sampleCTAddress
       samplePublicKey = fromRight (error "impossible") $ parsePublicKey
         "edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V"
       sampleSignature = fromRight (error "impossible") $ parseSignature
@@ -645,7 +647,7 @@
     (VTicket s v a, STTicket tv) -> renderDocSing
       needsParens
       OpPresent
-      (VPair (VAddress (EpAddress s DefEpName), VPair (v, VNat a))
+      (VPair (VAddress (EpAddress' s DefEpName), VPair (v, VNat a))
         , STPair STAddress (STPair tv STNat))
     val@(VPair (_, (VPair (_, _))), _) ->
       U.renderValuesList id $ renderLinearizedRightCombValuePair val
diff --git a/src/Morley/Michelson/Typed/Entrypoints.hs b/src/Morley/Michelson/Typed/Entrypoints.hs
--- a/src/Morley/Michelson/Typed/Entrypoints.hs
+++ b/src/Morley/Michelson/Typed/Entrypoints.hs
@@ -3,7 +3,7 @@
 
 -- | Utilities for lightweight entrypoints support.
 module Morley.Michelson.Typed.Entrypoints
-  ( EpAddress (..)
+  ( EpAddress (.., EpAddress)
   , ParseEpAddressError (..)
   , formatEpAddress
   , mformatEpAddress
@@ -72,13 +72,18 @@
 ----------------------------------------------------------------------------
 
 -- | Address with optional entrypoint name attached to it.
-data EpAddress = EpAddress
+data EpAddress = EpAddress'
   { eaAddress :: Address
     -- ^ Address itself
   , eaEntrypoint :: EpName
     -- ^ Entrypoint name (might be empty)
   } deriving stock (Show, Eq, Ord, Generic)
 
+pattern EpAddress :: KindedAddress kind -> EpName -> EpAddress
+pattern EpAddress addr name = EpAddress' (MkAddress addr) name
+
+{-# COMPLETE EpAddress #-}
+
 instance Buildable EpAddress where
   build = build . formatEpAddress
 
@@ -130,14 +135,14 @@
   in case mannotTxt of
     "" -> do
       addr <- first ParseEpAddressBadAddress $ parseAddress addrTxt
-      return $ EpAddress addr DefEpName
+      return $ EpAddress' addr DefEpName
     annotTxt' -> do
       addr <- first ParseEpAddressBadAddress $ parseAddress addrTxt
       annot <- first ParseEpAddressBadRefAnn $ case T.stripPrefix "%" annotTxt' of
         Nothing -> error "impossible"
         Just a -> mkAnnotation a
       epName <- first ParseEpAddressRefAnnError $ epNameFromRefAnn annot
-      return $ EpAddress addr epName
+      return $ EpAddress' addr epName
 
 -- | Parses byte representation of entrypoint address.
 --
@@ -162,7 +167,7 @@
   decodedEntrypoint <- first (ParseEpAddressBadEntryopint raw) $ decodeUtf8' eps
   decodedAnnotation <- first ParseEpAddressBadRefAnn $ mkAnnotation decodedEntrypoint
   eaEntrypoint <- first ParseEpAddressRefAnnError $ epNameFromRefAnn decodedAnnotation
-  pure $ EpAddress {..}
+  pure $ EpAddress' {..}
 
 -- ParamNotes
 ----------------------------------------------------------------------------
diff --git a/src/Morley/Michelson/Typed/Existential.hs b/src/Morley/Michelson/Typed/Existential.hs
--- a/src/Morley/Michelson/Typed/Existential.hs
+++ b/src/Morley/Michelson/Typed/Existential.hs
@@ -14,6 +14,7 @@
   , SomeContract (..)
   , SomeContractAndStorage (..)
   , SomeIsoValue (..)
+  , SomeVBigMap(..)
   ) where
 
 import Fmt (Buildable(..))
@@ -96,3 +97,6 @@
        -> SomeContractAndStorage
 
 deriving stock instance Show SomeContractAndStorage
+
+data SomeVBigMap where
+  SomeVBigMap :: forall k v. Value ('TBigMap k v) -> SomeVBigMap
diff --git a/src/Morley/Michelson/Typed/Haskell/Doc.hs b/src/Morley/Michelson/Typed/Haskell/Doc.hs
--- a/src/Morley/Michelson/Typed/Haskell/Doc.hs
+++ b/src/Morley/Michelson/Typed/Haskell/Doc.hs
@@ -759,6 +759,12 @@
     |]
   typeDocDependencies _ = []
   typeDocHaskellRep _ _ = Nothing
+  typeDocMichelsonRep _ = (Nothing, TKeyHash)
+  typeDocMdReference tp _ =
+    customTypeDocMdReference
+      (typeDocName tp, DType tp)
+      []
+      (WithinParens False)
 
 instance TypeHasDoc EpAddress where
   typeDocName _ = "EntrypointAddress"
diff --git a/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs b/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs
--- a/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs
+++ b/src/Morley/Michelson/Typed/Haskell/Instr/Product.hs
@@ -2,7 +2,6 @@
 -- SPDX-License-Identifier: LicenseRef-MIT-OA
 
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
-{-# LANGUAGE InstanceSigs #-}
 
 -- | Instructions working on product types derived from Haskell ones.
 module Morley.Michelson.Typed.Haskell.Instr.Product
diff --git a/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs b/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs
--- a/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs
+++ b/src/Morley/Michelson/Typed/Haskell/ValidateDescription.hs
@@ -10,10 +10,12 @@
   ) where
 
 import Data.Singletons (Demote)
-import Data.Type.Bool (If, type (||))
+import Data.Type.Bool (type (||))
 import GHC.Generics qualified as G
 import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
 
+import Morley.Util.Type (FailUnless, FailUnlessElse)
+
 -- | Description of constructors and fields of some datatype.
 --
 -- This type is just two nested maps represented as associative lists. It is supposed to
@@ -85,24 +87,21 @@
 -- otherwise.
 type family HasAllFields (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where
   HasAllFields conName fields typ =
-    If
+    FailUnlessElse
       (HasConstructor conName (G.Rep typ))
-      (HasAllFieldsImpl conName fields typ)
-      (TypeError
-        ('Text "No constructor " ':<>: 'ShowType conName ':<>: 'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "." )
+      ('Text "No constructor " ':<>: 'ShowType conName ':<>:
+      'Text " in type " ':<>: 'ShowType typ ':<>: 'Text "."
       )
+      (HasAllFieldsImpl conName fields typ)
 
 -- | Actual recursive implementation of 'HasAllFields'.
 type family HasAllFieldsImpl (conName :: Symbol) (fields :: [(Symbol, Symbol)]) (typ :: Type) :: Constraint where
   HasAllFieldsImpl _ '[] _ = ()
   HasAllFieldsImpl conName ( '(fieldName, _) ': rest ) typ =
-    ( If
+    ( FailUnless
         (HasField conName fieldName (G.Rep typ))
-        (() :: Constraint)
-        (TypeError
-          ('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>:
-           'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "."
-          )
+        ('Text "No field " ':<>: 'ShowType fieldName ':<>: 'Text " in constructor " ':<>:
+        'ShowType conName ':<>: 'Text " of type " ':<>: 'ShowType typ ':<>: 'Text "."
         )
     , HasAllFieldsImpl conName rest typ
     )
diff --git a/src/Morley/Michelson/Typed/Haskell/Value.hs b/src/Morley/Michelson/Typed/Haskell/Value.hs
--- a/src/Morley/Michelson/Typed/Haskell/Value.hs
+++ b/src/Morley/Michelson/Typed/Haskell/Value.hs
@@ -12,7 +12,6 @@
   , GIsoValue (GValueType)
   , ToT'
   , GenericIsoValue
-  , WellTypedIsoValue
   , WellTypedToT
   , HasNoOpToT
 
@@ -56,7 +55,7 @@
 import Morley.Michelson.Typed.Scope
 import Morley.Michelson.Typed.T
 import Morley.Michelson.Typed.Value
-import Morley.Tezos.Address (Address, TxRollupL2Address)
+import Morley.Tezos.Address
 import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
 import Morley.Tezos.Crypto
   (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)
@@ -68,7 +67,7 @@
 -- Complex values isomorphism
 ----------------------------------------------------------------------------
 
-type KnownIsoT a = SingI (ToT a)
+type KnownIsoT a = (IsoValue a, SingI (ToT a))
 
 -- | Isomorphism between Michelson values and plain Haskell types.
 --
@@ -173,7 +172,7 @@
 
 instance IsoValue Address where
   type ToT Address = 'TAddress
-  toVal addr = VAddress $ EpAddress addr DefEpName
+  toVal addr = VAddress $ EpAddress' addr DefEpName
   fromVal (VAddress x) = eaAddress x
 
 instance IsoValue EpAddress where
@@ -272,11 +271,9 @@
 
 type SomeEntrypointCall arg = SomeEntrypointCallT (ToT arg)
 
-type WellTypedToT a = WellTyped (ToT a)
-type WellTypedIsoValue a = (WellTyped (ToT a), IsoValue a)
-
-type HasNoOpToT a = HasNoOp (ToT a)
-type HasNoBigMapToT a = HasNoBigMap (ToT a)
+type WellTypedToT a = (IsoValue a, WellTyped (ToT a))
+type HasNoOpToT a = (IsoValue a, HasNoOp (ToT a))
+type HasNoBigMapToT a = (IsoValue a, HasNoBigMap (ToT a))
 
 -- | Since @Contract@ name is used to designate contract code, lets call
 -- analogy of 'TContract' type as follows.
@@ -303,7 +300,7 @@
 coerceContractRef ContractRef{..} = ContractRef{..}
 
 contractRefToAddr :: ContractRef cp -> EpAddress
-contractRefToAddr ContractRef{..} = EpAddress crAddress (sepcName crEntrypoint)
+contractRefToAddr ContractRef{..} = EpAddress' crAddress (sepcName crEntrypoint)
 
 -- | Ticket type.
 data Ticket (arg :: Type) = Ticket
diff --git a/src/Morley/Michelson/Typed/Instr.hs b/src/Morley/Michelson/Typed/Instr.hs
--- a/src/Morley/Michelson/Typed/Instr.hs
+++ b/src/Morley/Michelson/Typed/Instr.hs
@@ -98,6 +98,7 @@
           , SAPLING_EMPTY_STATE
           , SAPLING_VERIFY_UPDATE
           , MIN_BLOCK_TIME
+          , EMIT
           )
   , castInstr
   , pattern (:#)
@@ -159,8 +160,8 @@
 import Morley.Util.PeanoNatural
 import Morley.Util.Sing (eqI)
 import Morley.Util.TH
-import Morley.Util.Type (If, KnownList, type (++))
-import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)), TypeErrorUnless)
+import Morley.Util.Type (FailUnless, If, KnownList, type (++))
+import Morley.Util.TypeLits (ErrorMessage(ShowType, Text, (:$$:), (:<>:)))
 
 {-# ANN module ("HLint: ignore Language.Haskell.TH should be imported post-qualified or with an explicit import list" :: Text) #-}
 
@@ -217,7 +218,7 @@
 
 type ConstraintPairN (n :: Peano) (inp :: [T]) =
   ( RequireLongerOrSameLength inp n
-  , TypeErrorUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n ≥ 2")
+  , FailUnless (n >= ToPeano 2) ('Text "'PAIR n' expects n ≥ 2")
   )
 
 type PairN (n :: Peano) (s :: [T]) = (RightComb (Take n s) ': Drop n s)
@@ -232,10 +233,10 @@
   RightComb (x ': xs) = 'TPair x (RightComb xs)
 
 type ConstraintUnpairN (n :: Peano) (pair :: T) =
-  ( TypeErrorUnless (n >= ToPeano 2)
+  ( FailUnless (n >= ToPeano 2)
       ('Text "'UNPAIR n' expects n ≥ 2")
 
-  , TypeErrorUnless (CombedPairLeafCountIsAtLeast n pair)
+  , FailUnless (CombedPairLeafCountIsAtLeast n pair)
       (If (IsPair pair)
         ('Text "'UNPAIR "
           ':<>: 'ShowType (FromPeano n)
@@ -265,7 +266,7 @@
   UnpairN ('S n)       ('TPair x y) = x : UnpairN n y
 
 type ConstraintGetN (ix :: Peano) (pair :: T) =
-  ( TypeErrorUnless (CombedPairNodeIndexIsValid ix pair)
+  ( FailUnless (CombedPairNodeIndexIsValid ix pair)
       (If (IsPair pair)
         ('Text "'GET "
           ':<>: 'ShowType (FromPeano ix)
@@ -288,7 +289,7 @@
   GetN ('S ('S n)) ('TPair _ right) = GetN n right
 
 type ConstraintUpdateN (ix :: Peano) (pair :: T) =
-  ( TypeErrorUnless (CombedPairNodeIndexIsValid ix pair)
+  ( FailUnless (CombedPairNodeIndexIsValid ix pair)
       (If (IsPair pair)
         ('Text "'UPDATE "
           ':<>: 'ShowType (FromPeano ix)
@@ -810,6 +811,12 @@
     -> Instr ('TSaplingTransaction n : 'TSaplingState n ': s)
              ('TOption ('TPair 'TBytes ('TPair 'TInt ('TSaplingState n))) ': s)
   AnnMIN_BLOCK_TIME :: [AnyAnn] -> Instr s ('TNat ': s)
+  AnnEMIT
+    :: PackedValScope t
+    => AnnVar
+    -> FieldAnn
+    -> Maybe (Notes t)
+    -> Instr (t ': s) ('TOperation : s)
 
 castInstr
   :: forall inp1 out1 inp2 out2.
diff --git a/src/Morley/Michelson/Typed/Operation.hs b/src/Morley/Michelson/Typed/Operation.hs
--- a/src/Morley/Michelson/Typed/Operation.hs
+++ b/src/Morley/Michelson/Typed/Operation.hs
@@ -6,6 +6,7 @@
   , OriginationOperation (..)
   , TransferOperation (..)
   , SetDelegateOperation (..)
+  , EmitOperation (..)
   , mkContractAddress
   , mkOriginationOperationHash
   , mkTransferOperationHash
@@ -16,15 +17,15 @@
 import Data.ByteString.Lazy qualified as BSL
 
 import Morley.Michelson.Interpret.Pack (toBinary, toBinary')
-import Morley.Michelson.Runtime.TxData (TxData(..))
-import Morley.Michelson.Typed (EpName, unContractCode)
+import Morley.Michelson.Runtime.TxData (TxData)
+import Morley.Michelson.Typed (Emit, EpName(..), Instr, unContractCode)
 import Morley.Michelson.Typed.Aliases (Contract, Value)
 import Morley.Michelson.Typed.Contract (cCode)
 import Morley.Michelson.Typed.Entrypoints (EpAddress(..))
 import Morley.Michelson.Typed.Haskell.Value (IsoValue(..))
-import Morley.Michelson.Typed.Scope (ParameterScope, StorageScope)
-import Morley.Tezos.Address (Address(ContractAddress), GlobalCounter(..))
-import Morley.Tezos.Address.Alias (Alias)
+import Morley.Michelson.Typed.Scope (PackedValScope, ParameterScope, StorageScope)
+import Morley.Tezos.Address
+import Morley.Tezos.Address.Alias
 import Morley.Tezos.Core (Mutez(..))
 import Morley.Tezos.Crypto (Hash(..), HashTag(..), KeyHash, blake2b, blake2b160)
 
@@ -47,10 +48,10 @@
 
 -- | Data necessary to originate a contract.
 data OriginationOperation =
-  forall cp st.
-  (StorageScope st, ParameterScope cp) =>
+  forall cp st kind.
+  (StorageScope st, ParameterScope cp, L1AddressKind kind) =>
   OriginationOperation
-  { ooOriginator :: Address
+  { ooOriginator :: KindedAddress kind
   -- ^ Originator of the contract.
   , ooDelegate :: Maybe KeyHash
   -- ^ Optional delegate.
@@ -64,7 +65,7 @@
   -- ^ The value of the global counter at the time the operation was created.
   -- We store it here so that the resulting addresses of @CREATE_CONTRACT@ and
   -- performing of origination operation are the same.
-  , ooAlias :: Maybe Alias
+  , ooAlias :: Maybe ContractAlias
   -- ^ An alias to be associated with the originated contract's address.
 
   -- In Tezos each operation also has a special field called @counter@, see here:
@@ -112,7 +113,7 @@
 mkContractAddress
   :: OperationHash
   -> GlobalCounter
-  -> Address
+  -> ContractAddress
 mkContractAddress (OperationHash opHash) (GlobalCounter counter) =
   ContractAddress
   $ Hash HashContract
@@ -133,7 +134,7 @@
 
 mkTransferOperationHash
   :: ParameterScope t
-  => Address
+  => KindedAddress kind
   -> Value t
   -> EpName
   -> Mutez
@@ -157,7 +158,7 @@
 
 -- | Set contract's delegate
 data SetDelegateOperation = SetDelegateOperation
-  { sdoContract :: Address
+  { sdoContract :: ContractAddress
   -- ^ The contract we're setting delegate of
   , sdoDelegate :: Maybe KeyHash
   -- ^ The delegate we're setting
@@ -173,3 +174,10 @@
     --
     -- https://gitlab.com/tezos/tezos/-/blob/685227895f48a2564a9de3e1e179e7cd741d52fb/src/proto_010_PtGRANAD/lib_protocol/operation_repr.ml#L354
     packedOperation = packMaybe (toBinary' . toVal) sdoDelegate
+
+data EmitOperation = forall t. PackedValScope t => EmitOperation
+  { eoSource :: ContractAddress
+  , eoEmit :: Emit Instr t
+  }
+
+deriving stock instance Show EmitOperation
diff --git a/src/Morley/Michelson/Typed/Scope.hs b/src/Morley/Michelson/Typed/Scope.hs
--- a/src/Morley/Michelson/Typed/Scope.hs
+++ b/src/Morley/Michelson/Typed/Scope.hs
@@ -132,15 +132,19 @@
   , SingI (..)
   ) where
 
+import Data.Bool.Singletons (SBool(..))
 import Data.Constraint (Dict(..), withDict, (:-)(..), (\\))
-import Data.Singletons (Sing, SingI(..), fromSing, withSingI)
+import Data.Singletons
+  (SLambda(..), Sing, SingI(..), fromSing, type (@@), type (~>), type Apply, withSingI, (@@))
 import Data.Type.Bool (Not, type (&&), type (||))
 import Fmt (Buildable(..))
 import GHC.TypeLits (ErrorMessage(..), TypeError)
 
+import Data.Type.Equality ((:~:)(..))
 import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc)
 import Morley.Michelson.Typed.Sing (SingT(..))
 import Morley.Michelson.Typed.T (T(..))
+import Unsafe.Coerce (unsafeCoerce)
 
 ----------------------------------------------------------------------------
 -- Constraints
@@ -1031,62 +1035,114 @@
 --
 -- Because of the De Morgan laws @not (a or b)@ implies @(not a) and (not b)@
 -- or in our case: @pair@ does not contain @x@ -> @a@ and @b@ don't contain @x@.
---
--- GHC is however not able to prove this, so we need to use another (impossible)
--- 'error' to forcefully "prove" the two scopes.
 class WithDeMorganScope (c :: T -> Constraint) t a b where
   withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret
 
--- | Helper to build a 'WithDeMorganScope' by using a 'CheckScope' that we know
--- cannot fail.
-mkWithDeMorgan
-  :: forall scope a b ret. (CheckScope (scope a), CheckScope (scope b))
-  => ((scope a, scope b) => ret) -> ret
-mkWithDeMorgan f = fromRight (error "impossible") $ do
-  Dict <- checkScope @(scope a)
-  Dict <- checkScope @(scope b)
-  pure f
+-- | Produce evidence that the first argument of a disjunction
+-- is false if the whole disjunction is false.
+orL :: forall a b. (a || b) ~ 'False => Sing a -> a :~: 'False
+orL SFalse = Refl
+{-# NOINLINE [1] orL #-}
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoOp 'TPair a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoOp @a @b
+-- This rule is *slightly* illegitimate, because the right hand side is lazier
+-- than the left hand side. In context, this is fine, and we really *want* to
+-- do it so we have at least some hope of avoiding building singletons that we
+-- don't end up using. We'd get a totally legitimate rule if we used a SingI
+-- constraint instead of a Sing argument, but then we'd need to use withSingI,
+-- which for some reason doesn't use the newfangled GHC machinery for such and
+-- therefore risks gumming up optimization. Of course, we could roll our own
+-- withSingI, but that's very hairy and GHC version dependent (the
+-- never-really-documented magicDict was recently replaced by withDict, which
+-- is documented in ... the type checker source code, apparently).
+{-# RULES
+"orL" forall s. orL s = unsafeCoerce Refl
+ #-}
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoContract 'TPair a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoContract @a @b
+-- | When a class looks like
+--
+-- @
+-- class (SomeTypeFamily t ~ 'False, ...) => TheClass t
+-- instance (SomeTypeFamily t ~ 'False, ...) => TheClass t
+-- @
+--
+-- and the additional constraints are satisfied by the instance constraints of
+-- the 'WithDeMorganScope' instance for @TheClass@, we can use
+-- `simpleWithDeMorgan` to define 'withDeMorganScope' for the instance.
+simpleWithDeMorgan
+  :: forall sym a b ret.
+     ((sym @@ a || sym @@ b) ~ 'False, SingI sym, SingI a)
+  => (((sym @@ a) ~ 'False, (sym @@ b) ~ 'False) => ret) -> ret
+-- Note: If the "orL" rule fires (which it should), we won't actually calculate
+-- the (likely recursive) `sing @sym @@ sing @a` at all. If we're lucky, GHC
+-- might not build the `SingI a` dictionary either.
+simpleWithDeMorgan f
+  | Refl <- orL @(sym @@ a) @(sym @@ b) (sing @sym @@ sing @a)
+  = f
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoTicket 'TPair a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoTicket @a @b
+data ContainsOpSym :: T ~> Bool
+type instance Apply ContainsOpSym x = ContainsOp x
+instance SingI ContainsOpSym where
+  sing = SLambda $ \t -> case checkOpPresence t of
+    OpPresent -> STrue
+    OpAbsent -> SFalse
+instance SingI a => WithDeMorganScope HasNoOp 'TPair a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @a @b f
+instance SingI a => WithDeMorganScope HasNoOp 'TOr a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @a @b f
+instance SingI k => WithDeMorganScope HasNoOp 'TMap k v where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @k @v f
+instance SingI k => WithDeMorganScope HasNoOp 'TBigMap k v where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsOpSym @k @v f
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoBigMap 'TPair a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a @b
+data ContainsContractSym :: T ~> Bool
+type instance Apply ContainsContractSym x = ContainsContract x
+instance SingI ContainsContractSym where
+  sing = SLambda $ \t -> case checkContractTypePresence t of
+    ContractPresent -> STrue
+    ContractAbsent -> SFalse
+instance SingI a => WithDeMorganScope HasNoContract 'TPair a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsContractSym @a @b f
+instance SingI a => WithDeMorganScope HasNoContract 'TOr a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsContractSym @a @b f
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a @b
+data ContainsTicketSym :: T ~> Bool
+type instance Apply ContainsTicketSym x = ContainsTicket x
+instance SingI ContainsTicketSym where
+  sing = SLambda $ \t -> case checkTicketPresence t of
+    TicketPresent -> STrue
+    TicketAbsent -> SFalse
+instance SingI a => WithDeMorganScope HasNoTicket 'TPair a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsTicketSym @a @b f
+instance SingI a => WithDeMorganScope HasNoTicket 'TOr a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsTicketSym @a @b f
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoOp 'TOr a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoOp @a @b
+data ContainsBigMapSym :: T ~> Bool
+type instance Apply ContainsBigMapSym x = ContainsBigMap x
+instance SingI ContainsBigMapSym where
+  sing = SLambda $ \t -> case checkBigMapPresence t of
+    BigMapPresent -> STrue
+    BigMapAbsent -> SFalse
+instance SingI a => WithDeMorganScope HasNoBigMap 'TPair a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsBigMapSym @a @b f
+instance SingI a => WithDeMorganScope HasNoBigMap 'TOr a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsBigMapSym @a @b f
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoContract 'TOr a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoContract @a @b
+data ContainsNestedBigMapsSym :: T ~> Bool
+type instance Apply ContainsNestedBigMapsSym x = ContainsNestedBigMaps x
+instance SingI ContainsNestedBigMapsSym where
+  sing = SLambda $ \t -> case checkNestedBigMapsPresence t of
+    NestedBigMapsPresent -> STrue
+    NestedBigMapsAbsent -> SFalse
+instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b f
+instance SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where
+  withDeMorganScope f = simpleWithDeMorgan @ContainsNestedBigMapsSym @a @b f
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoTicket 'TOr a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoTicket @a @b
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoBigMap 'TOr a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoBigMap @a @b
 
-instance (SingI a, SingI b) => WithDeMorganScope HasNoNestedBigMaps 'TOr a b where
-  withDeMorganScope = mkWithDeMorgan @HasNoNestedBigMaps @a @b
-
-instance (SingI k, SingI v) => WithDeMorganScope HasNoOp 'TMap k v where
-  withDeMorganScope = mkWithDeMorgan @HasNoOp @k @v
-
-instance (SingI k, SingI v) => WithDeMorganScope HasNoOp 'TBigMap k v where
-  withDeMorganScope = mkWithDeMorgan @HasNoOp @k @v
-
 instance
   ( WithDeMorganScope HasNoOp t a b
   , WithDeMorganScope HasNoNestedBigMaps t a b
-  , SingI a, SingI b
   , WellTyped a, WellTyped b
   ) => WithDeMorganScope ParameterScope t a b where
   withDeMorganScope f =
@@ -1097,7 +1153,6 @@
   ( WithDeMorganScope HasNoOp t a b
   , WithDeMorganScope HasNoNestedBigMaps t a b
   , WithDeMorganScope HasNoContract t a b
-  , SingI a, SingI b
   , WellTyped a, WellTyped b
   ) => WithDeMorganScope StorageScope t a b where
   withDeMorganScope f =
@@ -1111,7 +1166,6 @@
   , WithDeMorganScope HasNoContract t a b
   , WithDeMorganScope HasNoTicket t a b
   , WithDeMorganScope HasNoSaplingState t a b
-  , SingI a, SingI b
   , WellTyped a, WellTyped b
   ) => WithDeMorganScope ConstantScope t a b where
   withDeMorganScope f =
@@ -1126,7 +1180,6 @@
   , WithDeMorganScope HasNoBigMap t a b
   , WithDeMorganScope HasNoTicket t a b
   , WithDeMorganScope HasNoSaplingState t a b
-  , SingI a, SingI b
   , WellTyped a, WellTyped b
   ) => WithDeMorganScope PackedValScope t a b where
   withDeMorganScope f =
@@ -1138,7 +1191,6 @@
 instance
   ( WithDeMorganScope PackedValScope t a b
   , WithDeMorganScope ConstantScope t a b
-  , SingI a, SingI b
   , WellTyped a, WellTyped b
   ) => WithDeMorganScope UnpackedValScope t a b where
   withDeMorganScope f =
diff --git a/src/Morley/Michelson/Typed/Sing.hs b/src/Morley/Michelson/Typed/Sing.hs
--- a/src/Morley/Michelson/Typed/Sing.hs
+++ b/src/Morley/Michelson/Typed/Sing.hs
@@ -25,7 +25,7 @@
 import Morley.Michelson.Printer.Util (RenderDoc(..))
 import Morley.Michelson.Typed.T (T(..))
 import Morley.Util.MismatchError
-import Morley.Util.Sing (SingI1(..), castSing, eqI, genSingletonsType)
+import Morley.Util.Sing (castSing, eqI, genSingletonsType)
 import Morley.Util.TH (deriveGADTNFData)
 
 -- | 'SingI' and 'Data.Singletons.TH.SDecide' instances for the 'T' kind.
@@ -45,15 +45,6 @@
 ---------------------------------------------
 -- Singleton-related helpers for T
 ----------------------------------------------
-instance SingI1 'TList where
-  withSingI1 x = x
-
-instance SingI1 'TOption where
-  withSingI1 x = x
-
-instance SingI k => SingI1 ('TMap k) where
-  withSingI1 x = x
-
 castSingE
   :: forall (a :: T) (b :: T) t. (SingI a, SingI b)
   => t a -> Either Text (t b)
diff --git a/src/Morley/Michelson/Typed/Util.hs b/src/Morley/Michelson/Typed/Util.hs
--- a/src/Morley/Michelson/Typed/Util.hs
+++ b/src/Morley/Michelson/Typed/Util.hs
@@ -261,6 +261,7 @@
     AnnSAPLING_EMPTY_STATE{} -> recursion0 i
     AnnSAPLING_VERIFY_UPDATE{} -> recursion0 i
     AnnMIN_BLOCK_TIME{} -> recursion0 i
+    AnnEMIT{} -> recursion0 i
   where
     recursion0 ::
       forall a b. Instr a b -> m (Instr a b)
@@ -454,6 +455,7 @@
     i@AnnSAPLING_EMPTY_STATE{} -> RfNormal i
     i@AnnSAPLING_VERIFY_UPDATE{} -> RfNormal i
     i@AnnMIN_BLOCK_TIME{} -> RfNormal i
+    i@AnnEMIT{} -> RfNormal i
 
 -- | There are many ways to represent a sequence of more than 2 instructions.
 -- E. g. for @i1; i2; i3@ it can be @Seq i1 $ Seq i2 i3@ or @Seq (Seq i1 i2) i3@.
@@ -938,6 +940,7 @@
   AnnSAPLING_EMPTY_STATE{} -> True
   AnnSAPLING_VERIFY_UPDATE{} -> True
   AnnMIN_BLOCK_TIME{} -> True
+  AnnEMIT{} -> True
 
 -- | A wrapper around either typechecked 'Anns' or unchecked 'NonEmpty' of
 -- 'AnyAnn'. Annotations on some instructions aren't typechecked, hence these
@@ -1069,3 +1072,7 @@
   AnnSAPLING_EMPTY_STATE anns _ -> pure $ SomeAnns anns
   AnnSAPLING_VERIFY_UPDATE anns -> pure $ SomeAnns anns
   AnnMIN_BLOCK_TIME anns -> SomeUncheckedAnns <$> nonEmpty anns
+  AnnEMIT anns tag ty -> pure $
+    case ty of
+      Just ty' -> SomeAnns $ tag `AnnsCons` ty' `AnnsTyCons` anns
+      Nothing -> SomeAnns $ tag `AnnsCons` anns
diff --git a/src/Morley/Michelson/Typed/Value.hs b/src/Morley/Michelson/Typed/Value.hs
--- a/src/Morley/Michelson/Typed/Value.hs
+++ b/src/Morley/Michelson/Typed/Value.hs
@@ -9,6 +9,7 @@
   , Operation' (..)
   , SetDelegate (..)
   , TransferTokens (..)
+  , Emit(..)
   , Value' (..)
   , RemFail (..)
   , mkVLam
@@ -31,11 +32,12 @@
 import Fmt (Buildable(build), Builder, (+|), (|+))
 
 import Morley.Michelson.Text (MText)
+import Morley.Michelson.Typed.Annotation (Notes)
 import Morley.Michelson.Typed.Contract
 import Morley.Michelson.Typed.Entrypoints
 import Morley.Michelson.Typed.Scope
 import Morley.Michelson.Typed.T (T(..))
-import Morley.Tezos.Address (Address, GlobalCounter(..), TxRollupL2Address)
+import Morley.Tezos.Address
 import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
 import Morley.Tezos.Crypto
   (Bls12381Fr, Bls12381G1, Bls12381G2, Chest, ChestKey, KeyHash, PublicKey, Signature)
@@ -58,6 +60,7 @@
        , Typeable instr, ParameterScope cp, StorageScope st)
     => CreateContract instr cp st
     -> Operation' instr
+  OpEmit :: PackedValScope t => Emit instr t -> Operation' instr
 
 instance Buildable (Operation' instr) where
   build =
@@ -65,6 +68,7 @@
       OpTransferTokens tt -> build tt
       OpSetDelegate sd -> build sd
       OpCreateContract cc -> build cc
+      OpEmit em -> build em
 
 deriving stock instance Show (Operation' instr)
 
@@ -76,6 +80,8 @@
     (OpSetDelegate _, _) -> False
     (OpCreateContract cc1, OpCreateContract cc2) -> cc1 `eqParamMixed3` cc2
     (OpCreateContract _, _) -> False
+    (OpEmit em1, OpEmit em2) -> em1 `eqParamSing` em2
+    (OpEmit _, _) -> False
 
 data TransferTokens instr p = TransferTokens
   { ttTransferArgument :: Value' instr p
@@ -104,7 +110,7 @@
     , forall i o. Eq (instr i o)
     )
   => CreateContract
-  { ccOriginator :: Address
+  { ccOriginator :: L1Address
   , ccDelegate :: Maybe KeyHash
   , ccBalance :: Mutez
   , ccStorageVal :: Value' instr st
@@ -121,6 +127,19 @@
 deriving stock instance Show (CreateContract instr cp st)
 deriving stock instance Eq (CreateContract instr cp st)
 
+data Emit instr t = PackedValScope t => Emit
+  { emTag :: Text
+  , emNotes :: Notes t
+  , emValue :: Value' instr t
+  , emCounter :: GlobalCounter
+  }
+
+deriving stock instance Show (Emit instr t)
+deriving stock instance Eq (Emit instr t)
+
+instance Buildable (Emit instr t) where
+  build Emit{..} = "Emit contract event with tag " +| emTag |+ " and type " +| emNotes |+ ""
+
 -- | Wrapper over instruction which remembers whether this instruction
 -- always fails or not.
 data RemFail (instr :: k -> k -> Type) (i :: k) (o :: k) where
@@ -266,10 +285,10 @@
 -- | Make value of @contract@ type which refers to the given address and
 -- does not call any entrypoint.
 addressToVContract
-  :: forall t instr.
+  :: forall t instr kind.
       (ParameterScope t, ForbidOr t)
-  => Address -> Value' instr ('TContract t)
-addressToVContract addr = VContract addr sepcPrimitive
+  => KindedAddress kind -> Value' instr ('TContract t)
+addressToVContract addr = VContract (MkAddress addr) sepcPrimitive
 
 buildVContract :: Value' instr ('TContract arg) -> Builder
 buildVContract = \case
@@ -364,6 +383,10 @@
   , deriveGADTNFData ''Operation'
   , deriveGADTNFData ''Value'
   ]
+
+instance NFData (Emit instr t) where
+  rnf (Emit a b c d) =
+    rnf a `seq` rnf b `seq` rnf c `seq` rnf d
 
 instance NFData (TransferTokens instr p)
 
diff --git a/src/Morley/Michelson/Untyped/Instr.hs b/src/Morley/Michelson/Untyped/Instr.hs
--- a/src/Morley/Michelson/Untyped/Instr.hs
+++ b/src/Morley/Michelson/Untyped/Instr.hs
@@ -10,14 +10,15 @@
   , flattenExpandedOp
   ) where
 
-import Prelude hiding (EQ, GT, LT)
+import Prelude hiding (EQ, GT, LT, group)
 
 import Data.Aeson.TH (deriveJSON)
 import Data.Data (Data(..))
 import Fmt (Buildable(build), (+|), (|+))
 import Generics.SYB (everywhere, mkT)
 import Text.PrettyPrint.Leijen.Text
-  (Doc, align, braces, enclose, indent, integer, line, nest, space, text, (<$$>), (<+>))
+  (Doc, align, braces, enclose, group, indent, integer, nest, space, text, (<$$>), (<+>))
+import Text.PrettyPrint.Leijen.Text qualified as PP
 
 import Morley.Michelson.ErrorPos (ErrorSrcPos)
 import Morley.Michelson.Printer.Util
@@ -212,6 +213,7 @@
   | SAPLING_EMPTY_STATE VarAnn Natural
   | SAPLING_VERIFY_UPDATE VarAnn
   | MIN_BLOCK_TIME    [AnyAnn]
+  | EMIT              VarAnn FieldAnn (Maybe Ty)
   deriving stock (Eq, Functor, Data, Generic, Show)
 
 instance NFData op => NFData (InstrAbstract op)
@@ -227,20 +229,10 @@
     DIG n                   -> "DIG" <+> text (show n)
     DUG n                   -> "DUG" <+> text (show n)
     PUSH va t v             ->
-      let renderConsecutively =
-            "PUSH" <+> renderAnnot va <+> renderTy t <+> renderDoc needsParens v
-          renderAligned = "PUSH" <+> renderAnnot va <$$> (spaces 2 <> renderTy t)
-                                <$$> spaces 2 <> nest 3 (renderDoc needsParens v)
-      in case v of
-        ValueNil      -> renderConsecutively
-        ValueInt{}    -> renderConsecutively
-        ValueString{} -> renderConsecutively
-        ValueBytes{}  -> renderConsecutively
-        ValueUnit     -> renderConsecutively
-        ValueTrue     -> renderConsecutively
-        ValueFalse    -> renderConsecutively
-        ValueNone     -> renderConsecutively
-        _             -> renderAligned
+      group $ nest 2 $
+        text "PUSH" <+> renderAnnot va
+        PP.<$> renderTy t
+        PP.<$> renderDoc needsParens v
     SOME ta va              -> "SOME" <+> renderAnnots [ta] [] [va]
     NONE ta va t            -> "NONE" <+> renderAnnots [ta] [] [va] <+> renderTy t
     UNIT ta va              -> "UNIT" <+> renderAnnots [ta] [] [va]
@@ -276,7 +268,7 @@
     EXEC va                 -> "EXEC" <+> renderAnnot va
     APPLY va                -> "APPLY" <+> renderAnnot va
     DIP s                   -> "DIP" <+> nest 5 (renderOps s)
-    DIPN n s                -> "DIP" <+> text (show n) <> line <> indent 4 (renderOps s)
+    DIPN n s                -> "DIP" <+> text (show n) PP.<$> indent 4 (renderOps s)
     FAILWITH                -> "FAILWITH"
     CAST va t               -> "CAST" <+> renderAnnot va <+> renderTy t
     RENAME va               -> "RENAME" <+> renderAnnot va
@@ -314,32 +306,33 @@
     CREATE_CONTRACT va1 va2 contract -> let
       body = enclose space space $ align $ (renderDoc doesntNeedParens contract)
       in "CREATE_CONTRACT" <+> renderAnnots [] [] [va1, va2] <$$> (indent 2 $ braces $ body)
-    IMPLICIT_ACCOUNT va     -> "IMPLICIT_ACCOUNT" <+> renderAnnot va
-    NOW va                  -> "NOW" <+> renderAnnot va
-    AMOUNT va               -> "AMOUNT" <+> renderAnnot va
-    BALANCE va              -> "BALANCE" <+> renderAnnot va
-    VOTING_POWER va         -> "VOTING_POWER" <+> renderAnnot va
-    TOTAL_VOTING_POWER va   -> "TOTAL_VOTING_POWER" <+> renderAnnot va
-    CHECK_SIGNATURE va      -> "CHECK_SIGNATURE" <+> renderAnnot va
-    SHA256 va               -> "SHA256" <+> renderAnnot va
-    SHA512 va               -> "SHA512" <+> renderAnnot va
-    BLAKE2B va              -> "BLAKE2B" <+> renderAnnot va
-    SHA3 va                 -> "SHA3" <+> renderAnnot va
-    KECCAK va               -> "KECCAK" <+> renderAnnot va
-    HASH_KEY va             -> "HASH_KEY" <+> renderAnnot va
-    PAIRING_CHECK va        -> "PAIRING_CHECK" <+> renderAnnot va
-    SOURCE va               -> "SOURCE" <+> renderAnnot va
-    SENDER va               -> "SENDER" <+> renderAnnot va
-    ADDRESS va              -> "ADDRESS" <+> renderAnnot va
-    CHAIN_ID va             -> "CHAIN_ID" <+> renderAnnot va
-    LEVEL va                -> "LEVEL" <+> renderAnnot va
-    SELF_ADDRESS va         -> "SELF_ADDRESS" <+> renderAnnot va
-    NEVER                   -> "NEVER"
-    TICKET va               -> "TICKET" <+> renderAnnot va
-    READ_TICKET va          -> "READ_TICKET" <+> renderAnnot va
-    SPLIT_TICKET va         -> "SPLIT_TICKET" <+> renderAnnot va
-    JOIN_TICKETS va         -> "JOIN_TICKETS" <+> renderAnnot va
-    OPEN_CHEST va           -> "OPEN_CHEST" <+> renderAnnot va
+    IMPLICIT_ACCOUNT va      -> "IMPLICIT_ACCOUNT" <+> renderAnnot va
+    NOW va                   -> "NOW" <+> renderAnnot va
+    AMOUNT va                -> "AMOUNT" <+> renderAnnot va
+    BALANCE va               -> "BALANCE" <+> renderAnnot va
+    VOTING_POWER va          -> "VOTING_POWER" <+> renderAnnot va
+    TOTAL_VOTING_POWER va    -> "TOTAL_VOTING_POWER" <+> renderAnnot va
+    CHECK_SIGNATURE va       -> "CHECK_SIGNATURE" <+> renderAnnot va
+    SHA256 va                -> "SHA256" <+> renderAnnot va
+    SHA512 va                -> "SHA512" <+> renderAnnot va
+    BLAKE2B va               -> "BLAKE2B" <+> renderAnnot va
+    SHA3 va                  -> "SHA3" <+> renderAnnot va
+    KECCAK va                -> "KECCAK" <+> renderAnnot va
+    HASH_KEY va              -> "HASH_KEY" <+> renderAnnot va
+    PAIRING_CHECK va         -> "PAIRING_CHECK" <+> renderAnnot va
+    SOURCE va                -> "SOURCE" <+> renderAnnot va
+    SENDER va                -> "SENDER" <+> renderAnnot va
+    ADDRESS va               -> "ADDRESS" <+> renderAnnot va
+    CHAIN_ID va              -> "CHAIN_ID" <+> renderAnnot va
+    LEVEL va                 -> "LEVEL" <+> renderAnnot va
+    SELF_ADDRESS va          -> "SELF_ADDRESS" <+> renderAnnot va
+    NEVER                    -> "NEVER"
+    TICKET va                -> "TICKET" <+> renderAnnot va
+    READ_TICKET va           -> "READ_TICKET" <+> renderAnnot va
+    SPLIT_TICKET va          -> "SPLIT_TICKET" <+> renderAnnot va
+    JOIN_TICKETS va          -> "JOIN_TICKETS" <+> renderAnnot va
+    OPEN_CHEST va            -> "OPEN_CHEST" <+> renderAnnot va
+    EMIT va fa ty            -> "EMIT" <+> renderAnnots [] [fa] [va] <+> maybe mempty renderTy ty
     SAPLING_EMPTY_STATE va n -> "SAPLING_EMPTY_STATE" <+> renderAnnot va <+> (integer $ toInteger n)
     SAPLING_VERIFY_UPDATE va -> "SAPLING_VERIFY_UPDATE" <+> renderAnnot va
     MIN_BLOCK_TIME anns      -> "MIN_BLOCK_TIME" <+> renderAnyAnns anns
diff --git a/src/Morley/Michelson/Untyped/Value.hs b/src/Morley/Michelson/Untyped/Value.hs
--- a/src/Morley/Michelson/Untyped/Value.hs
+++ b/src/Morley/Michelson/Untyped/Value.hs
@@ -19,6 +19,8 @@
   , renderElt'
   ) where
 
+import Prelude hiding (group)
+
 import Data.Aeson (FromJSON(..), ToJSON(..), withText)
 import Data.Aeson.TH (deriveJSON)
 import Data.Data (Data(..))
@@ -26,10 +28,12 @@
 import Fmt (Buildable(build))
 import Text.Hex (decodeHex, encodeHex)
 import Text.PrettyPrint.Leijen.Text
-  (Doc, braces, dquotes, enclose, semi, space, text, textStrict, (<+>))
+  (Doc, align, dquotes, encloseSep, group, hang, lbrace, rbrace, semi, sep, softline, space, text,
+  textStrict, (<+>))
+import Text.PrettyPrint.Leijen.Text qualified as PP
 
 import Morley.Michelson.Printer.Util
-  (RenderContext, RenderDoc(..), addParens, buildRenderDoc, doesntNeedParens, needsParens,
+  (RenderContext, RenderDoc(..), addParensMultiline, buildRenderDoc, doesntNeedParens, needsParens,
   renderOps)
 import Morley.Michelson.Text
 import Morley.Util.Aeson
@@ -99,13 +103,18 @@
 
 -- | Helper functions to render @Value@s
 renderSome, renderLeft, renderRight :: RenderContext -> (RenderContext -> Doc) -> Doc
-renderSome  pn render = addParens pn $ "Some"  <+> render needsParens
-renderLeft  pn render = addParens pn $ "Left"  <+> render needsParens
-renderRight pn render = addParens pn $ "Right" <+> render needsParens
+renderSome  pn render = renderContainer pn $ "Some" PP.<$> render needsParens
+renderLeft  pn render = renderContainer pn $ "Left" PP.<$> render needsParens
+renderRight pn render = renderContainer pn $ "Right" PP.<$> render needsParens
 
+-- | Helper function to format container values such as @Some@ and @Right@.
+renderContainer :: RenderContext -> Doc -> Doc
+renderContainer pn doc = addParensMultiline pn $ group $ hang 2 $ doc
+
 -- | Helper function to render @Pair@ @Value@
 renderPair :: RenderContext -> (RenderContext -> Doc) -> (RenderContext -> Doc) -> Doc
-renderPair pn l r = addParens pn $ "Pair" <+> l needsParens <+> r needsParens
+renderPair pn l r = addParensMultiline pn $ hang 2 $
+  sep ["Pair", l needsParens, r needsParens]
 
 -- | Helper function to render @Elt@
 renderElt' :: (RenderContext -> Doc) -> (RenderContext -> Doc) -> Doc
@@ -126,9 +135,8 @@
 -- given a rendering function for a single item.
 renderValuesList :: (e -> Doc) -> NonEmpty e -> Doc
 renderValuesList renderElem (toList -> es) =
-  braces . enclose space space $
-    mconcat . intersperse (semi <> space) $
-      renderElem <$> es
+  align $ encloseSep (lbrace <> space) (softline <> rbrace) (semi <> space) $
+    renderElem <$> es
 
 instance (RenderDoc op) => Buildable (Value' op) where
   build = buildRenderDoc
diff --git a/src/Morley/Tezos/Address.hs b/src/Morley/Tezos/Address.hs
--- a/src/Morley/Tezos/Address.hs
+++ b/src/Morley/Tezos/Address.hs
@@ -7,11 +7,19 @@
 
 module Morley.Tezos.Address
   ( ContractHash
-  , Address (..)
+  , KindedAddress (..)
   , TxRollupL2Address (..)
   , mkKeyAddress
   , detGenKeyAddress
-  , isKeyAddress
+  , isImplicitAddress
+  , ImplicitAddress
+  , ContractAddress
+  , TxRollupAddress
+  , L1Address
+  , L1AddressKind
+  , ConstrainAddressKind
+  , Address
+  , ConstrainedAddress(.., MkAddress)
 
   , GlobalCounter(..)
   , mkContractHashHack
@@ -22,16 +30,27 @@
   , formatAddress
   , mformatAddress
   , parseAddressRaw
+  , parseKindedAddress
   , parseAddress
   , ta
+
+  -- * Utilities
+  , addressKindSanity
+  , usingImplicitOrContractKind
   ) where
 
+import Control.Monad.Except (mapExceptT, throwError)
 import Data.Aeson (FromJSON(..), FromJSONKey, ToJSON(..), ToJSONKey)
 import Data.Aeson qualified as Aeson
 import Data.Aeson.Encoding qualified as Aeson
 import Data.Aeson.Types qualified as AesonTypes
+import Data.Binary.Get qualified as Get
 import Data.ByteString qualified as BS
+import Data.ByteString.Lazy qualified as LBS
+import Data.Constraint (Dict(..), (\\))
+import Data.Singletons (SingI(..))
 import Data.Text (strip)
+import Data.Type.Equality ((:~:)(..))
 import Fmt (Buildable(build), hexF, pretty)
 import Instances.TH.Lift ()
 import Language.Haskell.TH.Quote qualified as TH
@@ -41,42 +60,158 @@
 
 import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDoc, renderAnyBuildable)
 import Morley.Michelson.Text
+import Morley.Tezos.Address.Kinds
 import Morley.Tezos.Crypto
+import Morley.Util.Binary
 import Morley.Util.CLI
+import Morley.Util.Sing
 import Morley.Util.TypeLits
 
--- | Data type corresponding to address structure in Tezos.
-data Address
-  = KeyAddress KeyHash
-  -- ^ @tz1@, @tz2@ or @tz3@ address which is a hash of a public key.
-  | ContractAddress ContractHash
-  -- ^ @KT@ address which corresponds to a callable contract.
-  | TransactionRollupAddress TxRollupHash
-  -- ^ @txr1@ address which corresponds to a transaction rollup.
-  deriving stock (Show, Eq, Ord, Generic, Lift)
+-- | A "kinded" address. This type carries 'AddressKind' on the type-level.
+-- Useful in the internal API, not as much when we have to interact with the
+-- network. See 'Address' for a type that is isomorphic to a Michelson
+-- @address@.
+data KindedAddress (kind :: AddressKind) where
+  -- | @tz1@, @tz2@ or @tz3@ address which is a hash of a public key.
+  ImplicitAddress :: KeyHash -> KindedAddress 'AddressKindImplicit
+  -- | @KT1@ address which corresponds to a callable contract.
+  ContractAddress :: ContractHash -> KindedAddress 'AddressKindContract
+  -- | @txr1@ address which corresponds to a transaction rollup.
+  TxRollupAddress :: TxRollupHash -> KindedAddress 'AddressKindTxRollup
 
-instance NFData Address
+deriving stock instance Show (KindedAddress kind)
+deriving stock instance Eq (KindedAddress kind)
+deriving stock instance Ord (KindedAddress kind)
+deriving stock instance Lift (KindedAddress kind)
 
+instance NFData (KindedAddress kind) where
+  rnf = \case
+    ImplicitAddress x -> rnf x
+    ContractAddress x -> rnf x
+    TxRollupAddress x -> rnf x
+
+-- | A type only allowing v'ImplicitAddress'
+type ImplicitAddress = KindedAddress 'AddressKindImplicit
+
+-- | A type only allowing v'ContractAddress'
+type ContractAddress = KindedAddress 'AddressKindContract
+
+-- | A type only allowing v'TxRollupAddress'
+type TxRollupAddress = KindedAddress 'AddressKindTxRollup
+
+-- | Data type corresponding to @address@ structure in Tezos.
+type Address =
+  ConstrainedAddress '[ 'AddressKindImplicit, 'AddressKindContract, 'AddressKindTxRollup ]
+
+type family ConstrainAddressKindHelper (ks :: [AddressKind]) kind where
+  ConstrainAddressKindHelper (x ': _) x = 'True
+  ConstrainAddressKindHelper (_ ': xs) x = ConstrainAddressKindHelper xs x
+  ConstrainAddressKindHelper '[] _ = 'False
+
+type family CheckConstrainAddressKindError k b :: Constraint where
+  CheckConstrainAddressKindError _ 'True = ()
+  CheckConstrainAddressKindError k 'False =
+    TypeError ('ShowType k ':<>: 'Text "is forbidden in this context")
+
+-- | Constrain address kind to be one of the kinds in the list.
+type ConstrainAddressKind ks k =
+  ( CheckConstrainAddressKindError k (ConstrainAddressKindHelper ks k)
+  , ConstrainAddressKindHelper ks k ~ 'True)
+
+-- | An existential of 'KindedAddress' constrained by its type argument.
+data ConstrainedAddress (ks :: [AddressKind]) =
+  forall kind. ConstrainAddressKind ks kind => MkConstrainedAddress (KindedAddress kind)
+
+-- | A convenience synonym for 'ConstrainedAddress' allowing only implicit and
+-- contract addresses.
+--
+-- 'L1Address' is named as such because in addition to implicit and contract
+-- addresses, Michelson's @address@ type can contain @txr1@ addresses,
+-- identifying transaction rollups. While @txr1@ are technically also level-1
+-- (level-2 being @tx_rollup_l2_address@, i.e. @tz4@), in practice it's a
+-- level-1 identifier for a bundle of level-2 operations. Hence, to keep type
+-- names concise, we use 'L1Address'.
+type L1Address =
+  ConstrainedAddress '[ 'AddressKindImplicit, 'AddressKindContract ]
+
+-- | Convenience synonym for 'ConstrainAddressKind' allowing only implicit and
+-- contract addresses.
+--
+-- For a note on the naming convention, refer to 'L1Address'.
+type L1AddressKind kind =
+  ConstrainAddressKind '[ 'AddressKindImplicit, 'AddressKindContract ] kind
+
+-- | A trick to avoid bogus redundant constraint warnings
+usingImplicitOrContractKind :: forall kind a. L1AddressKind kind => a -> a
+usingImplicitOrContractKind = id
+  where _ = Dict :: Dict (L1AddressKind kind)
+
+-- | 'MkConstrainedAddress' specialized to 'Address'
+pattern MkAddress :: KindedAddress kind -> Address
+pattern MkAddress x <- MkConstrainedAddress x
+  where MkAddress x = case x of
+          ImplicitAddress{} -> MkConstrainedAddress x
+          ContractAddress{} -> MkConstrainedAddress x
+          TxRollupAddress{} -> MkConstrainedAddress x
+
+{-# COMPLETE MkAddress #-}
+
+deriving stock instance Show (ConstrainedAddress c)
+instance Eq (ConstrainedAddress c) where
+  MkConstrainedAddress (addr1 :: KindedAddress kind1)
+    == MkConstrainedAddress (addr2 :: KindedAddress kind2) =
+    case eqI @kind1 @kind2 \\ addressKindSanity addr1 \\ addressKindSanity addr2 of
+      Just Refl -> addr1 == addr2
+      Nothing -> False
+instance Ord (ConstrainedAddress c) where
+  compare (MkConstrainedAddress (a1 :: KindedAddress kind1))
+          (MkConstrainedAddress (a2 :: KindedAddress kind2)) =
+    case (a1, a2) of
+      (k1, k2)
+        | Just Refl <- eqI @kind1 @kind2 \\ addressKindSanity k1 \\ addressKindSanity k2
+        -> compare k1 k2
+      (ImplicitAddress{}, _) -> LT
+      (ContractAddress{}, ImplicitAddress{}) -> GT
+      (ContractAddress{}, _) -> LT
+      (TxRollupAddress{}, ImplicitAddress{}) -> GT
+      (TxRollupAddress{}, ContractAddress{}) -> GT
+      (TxRollupAddress{}, _) -> LT
+deriving stock instance Lift (ConstrainedAddress c)
+
+instance NFData (ConstrainedAddress c) where
+  rnf (MkConstrainedAddress x) = rnf x
+
+instance Buildable (ConstrainedAddress c) where
+  build (MkConstrainedAddress x) = build x
+
+-- | Given any (non-bottom) 'KindedAddress', prove that @kind@ is well-defined
+-- (i.e. has a 'SingI' instance)
+addressKindSanity :: KindedAddress kind -> Dict (SingI kind)
+addressKindSanity = \case
+  ImplicitAddress{} -> Dict
+  ContractAddress{} -> Dict
+  TxRollupAddress{} -> Dict
+
 -- | @tz4@ level-2 public key hash address, used with transaction rollups, corresponds
 -- to @tx_rollup_l2_address@ Michelson type.
 newtype TxRollupL2Address = TxRollupL2Address KeyHashL2
   deriving stock (Show, Eq, Ord, Generic, Lift)
   deriving newtype NFData
 
--- | Returns @True@ if given address is implicit.
-isKeyAddress :: Address -> Bool
-isKeyAddress = \case
-  KeyAddress _      -> True
-  ContractAddress _ -> False
-  TransactionRollupAddress _ -> False
+-- | Checks if the provided 'KindedAddress' is an implicit address and returns
+-- proof of the fact if it is.
+isImplicitAddress :: KindedAddress kind -> Maybe (kind :~: 'AddressKindImplicit)
+isImplicitAddress = \case
+  ImplicitAddress{} -> Just Refl
+  _ -> Nothing
 
--- | Smart constructor for 'KeyAddress'.
-mkKeyAddress :: PublicKey -> Address
-mkKeyAddress = KeyAddress . hashKey
+-- | Smart constructor for t'ImplicitAddress'.
+mkKeyAddress :: PublicKey -> ImplicitAddress
+mkKeyAddress = ImplicitAddress . hashKey
 
--- | Deterministically generate a random 'KeyAddress' and discard its
+-- | Deterministically generate a random t'ImplicitAddress' and discard its
 -- secret key.
-detGenKeyAddress :: ByteString -> Address
+detGenKeyAddress :: ByteString -> ImplicitAddress
 detGenKeyAddress = mkKeyAddress . toPublic . detSecretKey
 
 -- | Represents the network's global counter.
@@ -110,17 +245,17 @@
 -- Formatting/parsing
 ----------------------------------------------------------------------------
 
-formatAddress :: Address -> Text
+formatAddress :: KindedAddress kind -> Text
 formatAddress =
   \case
-    KeyAddress h -> formatHash h
+    ImplicitAddress h -> formatHash h
     ContractAddress h -> formatHash h
-    TransactionRollupAddress h -> formatHash h
+    TxRollupAddress h -> formatHash h
 
-mformatAddress :: Address -> MText
+mformatAddress :: KindedAddress kind -> MText
 mformatAddress = unsafe . mkMText . formatAddress
 
-instance Buildable Address where
+instance Buildable (KindedAddress kind) where
   build = build . formatAddress
 
 instance Buildable TxRollupL2Address where
@@ -152,36 +287,45 @@
         mconcat $ "Address failed to parse: " : intersperse ", "
           (toList $ renderDoc context <$> pkErr)
 
--- | Parse an address from its human-readable textual representation
--- used by Tezos (e. g. "tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU"). Or
--- fail if it's invalid.
-parseAddress :: Text -> Either ParseAddressError Address
-parseAddress addressText =
-  let implicit = tryParse KeyAddress parseHash handleCrypto
-      contract = tryParse ContractAddress parseHash handleCrypto
-      txr = tryParse TransactionRollupAddress parseHash handleCrypto
-  in implicit `merge` contract `merge` txr
+-- | Parse an address of a particular kind from its human-readable textual
+-- representation used by Tezos (e. g. "tz1faswCTDciRzE4oJ9jn2Vm2dvjeyA9fUzU").
+-- Or fail if it's invalid.
+parseKindedAddress :: forall kind. SingI kind => Text -> Either ParseAddressError (KindedAddress kind)
+parseKindedAddress addressText = case sing @kind of
+  SAddressKindContract -> tryParse ContractAddress
+  SAddressKindImplicit -> tryParse ImplicitAddress
+  SAddressKindTxRollup -> tryParse TxRollupAddress
   where
     handleCrypto = \case
       CryptoParseWrongBase58Check -> ParseAddressWrongBase58Check
       x -> ParseAddressAllFailed $ pure x
+    tryParse :: AllHashTags hkind => (Hash hkind -> b) -> Either ParseAddressError b
+    tryParse ctor = bimap handleCrypto ctor $ parseHash addressText
+
+-- | Parse an address of arbitrary kind from its human-readable textual
+-- representation, or fail if it's invalid.
+parseAddress :: Text -> Either ParseAddressError Address
+parseAddress x =
+          (MkAddress <$> parseKindedAddress @'AddressKindImplicit x)
+  `merge` (MkAddress <$> parseKindedAddress @'AddressKindContract x)
+  `merge` (MkAddress <$> parseKindedAddress @'AddressKindTxRollup x)
+  where
     merge :: Semigroup a => Either a b -> Either a b -> Either a b
     merge (Left xs) (Left ys) = Left $ xs <> ys
     merge r@Right{} _ = r
     merge _ r@Right{} = r
-    tryParse :: (t -> b) -> (Text -> Either t1 t) -> (t1 -> a) -> Either a b
-    tryParse ctor parser handler =
-      case parser addressText of
-        Left err -> Left $ handler err
-        Right res -> Right $ ctor res
 
 data ParseAddressRawError
   = ParseAddressRawWrongSize ByteString
   -- ^ Raw bytes representation of an address has invalid length.
-  | ParseAddressRawInvalidPrefix ByteString
+  | ParseAddressRawInvalidPrefix Word8
   -- ^ Raw bytes representation of an address has incorrect prefix.
-  | ParseAddressRawMalformedSeparator ByteString
+  | ParseAddressRawMalformedSeparator Word8
   -- ^ Raw bytes representation of an address does not end with "\00".
+  | ParseAddressRawBinaryError Text
+  -- ^ General binary decoding error.
+  | ParseAddressCryptoError CryptoParseError
+  -- ^ Crypto error in parsing key hash.
   deriving stock (Eq, Show, Generic)
 
 instance NFData ParseAddressRawError
@@ -193,8 +337,10 @@
         "Invalid prefix for raw address" <+> (dquotes $ renderAnyBuildable $ hexF prefix) <+> "provided"
       ParseAddressRawWrongSize addr -> "Given raw address+" <+>
         (renderAnyBuildable $ hexF addr) <+> "has invalid length" <+> int (length addr)
-      ParseAddressRawMalformedSeparator addr -> "Given raw address+" <+> (renderAnyBuildable $ hexF addr) <+>
+      ParseAddressRawMalformedSeparator addr -> "Given raw address" <+> (renderAnyBuildable $ hexF addr) <+>
         "does not end with" <+> dquotes (backslash <> "00")
+      ParseAddressRawBinaryError err -> "Binary error during decoding address:" <+> renderAnyBuildable err
+      ParseAddressCryptoError err -> "Key hash decoding error:" <+> renderAnyBuildable err
 
 instance Buildable ParseAddressRawError where
   build = buildRenderDoc
@@ -203,32 +349,29 @@
 -- (e.g "01521139f84791537d54575df0c74a8084cc68861c00")) . Or fail otherwise
 -- if it's invalid.
 parseAddressRaw :: ByteString -> Either ParseAddressRawError Address
-parseAddressRaw bytes =
-  case BS.splitAt 1 bytes of
-    -- key hash address
-    ("\00", rest) -> checkHashLength (BS.drop 1 rest) >> case BS.splitAt 1 rest of
-      ("\00", addr) -> pure $ KeyAddress $ Hash HashEd25519 addr
-      ("\01", addr) -> pure $ KeyAddress $ Hash HashSecp256k1 addr
-      ("\02", addr) -> pure $ KeyAddress $ Hash HashP256 addr
-      (x, _) -> Left $ ParseAddressRawInvalidPrefix x
-    (pfx, rest) -> do
-      (address, sep) <- maybe (Left $ ParseAddressRawWrongSize rest) pure $ BS.unsnoc rest
-      checkHashLength address
-      unless (sep == 0x00) $
-        Left $ ParseAddressRawMalformedSeparator rest
-      case pfx of
-        -- contract address
-        "\01" -> pure $ ContractAddress $ Hash HashContract address
-        -- transaction rollup address
-        "\02" -> pure $ TransactionRollupAddress $ Hash HashTXR address
-        x -> Left $ ParseAddressRawInvalidPrefix x
+parseAddressRaw bytes
+  -- NB: conveniently, the byte count is the same for 'KeyAddress',
+  -- 'ContractAddress' and 'TransactionRollupAddress'. However, with
+  -- 'KeyAddress' it's two tag bytes, while with the other two it's one tag byte
+  -- and one separator byte.
+  | BS.length bytes /= hashLengthBytes + 2 = Left $ ParseAddressRawWrongSize bytes
+  | otherwise
+  = either (Left . ParseAddressRawBinaryError . fromString . view _3) (view _3)
+  $ flip Get.runGetOrFail (LBS.fromStrict bytes) $ runExceptT
+  $ decodeWithTagM "address" (throwError . ParseAddressRawInvalidPrefix)
+      [ 0x00 ##: MkAddress . ImplicitAddress <$> keyHash
+      , 0x01 ##: MkAddress . ContractAddress <$> sepHash HashContract
+      , 0x02 ##: MkAddress . TxRollupAddress <$> sepHash HashTXR
+      ]
   where
-    checkHashLength addr
-      | length addr /= hashLengthBytes
-      = Left $ ParseAddressRawWrongSize addr
-      | otherwise = pass
+    sep = lift Get.getWord8 >>= \case
+      0x00 -> pass
+      x -> throwError $ ParseAddressRawMalformedSeparator x
+    keyHash = mapExceptT (fmap $ first ParseAddressCryptoError) decodeKeyHash
+    sepHash :: HashTag kind -> ExceptT ParseAddressRawError Get.Get (Hash kind)
+    sepHash kind = Hash kind <$> lift (getByteStringCopy hashLengthBytes) <* sep
 
--- | QuasyQuoter for constructing Tezos addresses.
+-- | QuasiQuoter for constructing Tezos addresses.
 --
 -- Validity of result will be checked at compile time.
 ta :: TH.QuasiQuoter
@@ -236,13 +379,13 @@
   { TH.quoteExp = \s ->
       case parseAddress . strip $ toText s of
         Left   err -> fail $ pretty err
-        Right addr -> TH.lift addr
+        Right (MkAddress addr) -> TH.lift addr
   , TH.quotePat = \_ ->
-      fail "Cannot use this QuasyQuotation at pattern position"
+      fail "Cannot use this QuasiQuotation at pattern position"
   , TH.quoteType = \_ ->
-      fail "Cannot use this QuasyQuotation at type position"
+      fail "Cannot use this QuasiQuotation at type position"
   , TH.quoteDec = \_ ->
-      fail "Cannot use this QuasyQuotation at declaration position"
+      fail "Cannot use this QuasiQuotation at declaration position"
   }
 
 
@@ -250,7 +393,7 @@
     TypeError ('Text "There is no instance defined for (IsString Address)" ':$$:
                'Text "Consider using QuasiQuotes: `[ta|some text...|]`"
               ) =>
-    IsString Address where
+    IsString (KindedAddress kind) where
   fromString = error "impossible"
 
 
@@ -258,24 +401,41 @@
 -- Unsafe
 ----------------------------------------------------------------------------
 
-instance HasCLReader Address where
+instance SingI kind => HasCLReader (KindedAddress kind) where
   getReader = eitherReader parseAddrDo
     where
       parseAddrDo addr =
-        either (Left . mappend "Failed to parse address: " . pretty) Right $
-        parseAddress $ toText addr
+        first (mappend "Failed to parse address: " . pretty) $
+        parseKindedAddress $ toText addr
   getMetavar = "ADDRESS"
 
 ----------------------------------------------------------------------------
 -- Aeson instances
 ----------------------------------------------------------------------------
 
-instance ToJSON Address where
+instance ToJSON (KindedAddress kind) where
   toJSON = Aeson.String . formatAddress
   toEncoding = Aeson.text . formatAddress
 
-instance ToJSONKey Address where
+instance ToJSONKey (KindedAddress kind) where
   toJSONKey = AesonTypes.toJSONKeyText formatAddress
+
+instance SingI kind => FromJSON (KindedAddress kind) where
+  parseJSON =
+    Aeson.withText "Address" $
+    either (fail . pretty) pure . parseKindedAddress
+
+instance SingI kind => FromJSONKey (KindedAddress kind) where
+  fromJSONKey =
+    AesonTypes.FromJSONKeyTextParser
+      (either (fail . pretty) pure . parseKindedAddress)
+
+instance ToJSON (ConstrainedAddress c) where
+  toJSON (MkConstrainedAddress addr) = toJSON addr
+  toEncoding (MkConstrainedAddress addr) = toEncoding addr
+
+instance ToJSONKey (ConstrainedAddress c) where
+  toJSONKey = AesonTypes.toJSONKeyText \(MkConstrainedAddress addr) -> formatAddress addr
 
 instance FromJSON Address where
   parseJSON =
diff --git a/src/Morley/Tezos/Address/Alias.hs b/src/Morley/Tezos/Address/Alias.hs
--- a/src/Morley/Tezos/Address/Alias.hs
+++ b/src/Morley/Tezos/Address/Alias.hs
@@ -4,43 +4,118 @@
 module Morley.Tezos.Address.Alias
   ( AddressOrAlias(..)
   , Alias(..)
+  , SomeAlias(..)
+  , SomeAddressOrAlias(..)
+  , ImplicitAlias
+  , ContractAlias
+  , ImplicitAddressOrAlias
+  , ContractAddressOrAlias
+  , unAlias
+  , mkAlias
+  , aliasKindSanity
   )
   where
 
-import Data.Aeson (FromJSON, ToJSON)
-import Fmt (Buildable(..))
+import Data.Aeson (FromJSON(..), ToJSON(..))
+import Data.Constraint (Dict(..), (\\))
+import Data.Singletons (SingI(..), demote)
+import Data.Type.Equality ((:~:)(..))
+import Fmt (Buildable(..), nameF, pretty, (+|), (|+))
 import Options.Applicative qualified as Opt
 
-import Morley.Tezos.Address (Address, parseAddress)
+import Morley.Tezos.Address
+import Morley.Tezos.Address.Kinds
 import Morley.Util.CLI (HasCLReader(..))
+import Morley.Util.Sing
 
 -- | @tezos-client@ can associate addresses with textual aliases.
 -- This type denotes such an alias.
-newtype Alias = Alias
-  { unAlias :: Text
-    -- ^ Extract 'Text' from 'Alias'.
-  }
-  deriving stock (Show, Eq, Ord)
-  deriving newtype (Buildable, ToJSON, FromJSON)
+data Alias (kind :: AddressKind) where
+  ImplicitAlias :: Text -> Alias 'AddressKindImplicit
+  ContractAlias :: Text -> Alias 'AddressKindContract
 
+-- | A type only allowing v'ImplicitAlias' values.
+type ImplicitAlias = Alias 'AddressKindImplicit
+
+-- | A type only allowing v'ContractAlias' values.
+type ContractAlias = Alias 'AddressKindContract
+
+deriving stock instance Show (Alias kind)
+deriving stock instance Eq (Alias kind)
+deriving stock instance Ord (Alias kind)
+
+-- | Get raw alias text from 'Alias'
+unAlias :: Alias kind -> Text
+unAlias = \case
+  ImplicitAlias x -> x
+  ContractAlias x -> x
+
+-- | Construct an 'Alias' from alias 'Text'.
+mkAlias :: forall kind. (SingI kind, L1AddressKind kind) => Text -> Alias kind
+mkAlias = usingImplicitOrContractKind @kind $ case sing @kind of
+  SAddressKindImplicit -> ImplicitAlias
+  SAddressKindContract -> ContractAlias
+
+instance Buildable (Alias kind) where
+  build = build . unAlias
+
+instance ToJSON (Alias kind) where
+  toJSON = toJSON . unAlias
+
+instance (SingI kind, L1AddressKind kind) => FromJSON (Alias kind) where
+  parseJSON = fmap mkAlias . parseJSON
+
+-- | Existential wrapper over 'Alias'.
+data SomeAlias = forall kind. SomeAlias (Alias kind)
+
+deriving stock instance Show SomeAlias
+
+instance Buildable SomeAlias where
+  build (SomeAlias x) = build x
+
+-- | Given an 'Alias', prove it's @kind@ is well-defined (i.e. it has a 'SingI'
+-- instance and satisfies 'L1AddressKind' constraint)
+aliasKindSanity :: Alias kind -> Dict (L1AddressKind kind, SingI kind)
+aliasKindSanity = \case
+  ImplicitAlias{} -> Dict
+  ContractAlias{} -> Dict
+
 -- | Representation of an address that @tezos-client@ uses. It can be
 -- an address itself or a textual alias.
-data AddressOrAlias
-  = AddressResolved Address
+data AddressOrAlias kind
+  = AddressResolved (KindedAddress kind)
   -- ^ Address itself, can be used as is.
-  | AddressAlias Alias
+  | AddressAlias (Alias kind)
   -- ^ Address alias, should be resolved by @tezos-client@.
   deriving stock (Show, Eq, Ord)
 
-instance HasCLReader AddressOrAlias where
+instance (SingI kind, L1AddressKind kind) => HasCLReader (AddressOrAlias kind) where
   getReader =
-    Opt.str <&> \addrOrAlias ->
+    Opt.str >>= \addrOrAlias ->
       case parseAddress addrOrAlias of
-        Right addr -> AddressResolved addr
-        Left _ -> AddressAlias (Alias addrOrAlias)
+        Right (MkAddress (addr :: KindedAddress kind')) ->
+          case eqI @kind @kind' \\ addressKindSanity addr of
+            Just Refl -> pure $ AddressResolved addr
+            Nothing -> Opt.readerError $ pretty $ nameF "Unexpected address kind" $
+              "expected " +| demote @kind |+ " address, but got " +| addr |+ ""
+        Left _ -> pure $ AddressAlias (mkAlias addrOrAlias)
   getMetavar = "ADDRESS OR ALIAS"
 
-instance Buildable AddressOrAlias where
+instance Buildable (AddressOrAlias kind) where
   build = \case
     AddressResolved addr -> build addr
     AddressAlias alias -> build alias
+
+-- | Convenience type synonym.
+type ImplicitAddressOrAlias = AddressOrAlias 'AddressKindImplicit
+
+-- | Convenience type synonym.
+type ContractAddressOrAlias = AddressOrAlias 'AddressKindContract
+
+-- | Existential over 'AddressOrAlias'.
+data SomeAddressOrAlias = forall kind. SomeAddressOrAlias (AddressOrAlias kind)
+
+instance Buildable SomeAddressOrAlias where
+  build (SomeAddressOrAlias x) = build x
+
+deriving stock instance Show SomeAddressOrAlias
diff --git a/src/Morley/Tezos/Address/Kinds.hs b/src/Morley/Tezos/Address/Kinds.hs
new file mode 100644
--- /dev/null
+++ b/src/Morley/Tezos/Address/Kinds.hs
@@ -0,0 +1,33 @@
+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
+-- SPDX-License-Identifier: LicenseRef-MIT-OA
+
+-- NB: 'genSingletonsType' creates some unused synonyms and GHC complains. To
+-- minimize the impact of this option, this is in a separate module.
+{-# OPTIONS_GHC -Wno-unused-top-binds #-}
+
+-- | Address kinds.
+module Morley.Tezos.Address.Kinds
+  ( AddressKind(..)
+  , SingAddressKind(..)
+  ) where
+
+import Fmt (Buildable(..))
+
+import Morley.Util.Sing
+
+-- | Address "kind"
+data AddressKind
+  = AddressKindImplicit
+  -- ^ an implicit address, @tz1@-@tz3@
+  | AddressKindContract
+  -- ^ a contract address, @KT1@
+  | AddressKindTxRollup
+  -- ^ a transaction rollup address, @txr1@
+
+instance Buildable AddressKind where
+  build = \case
+    AddressKindImplicit -> "implicit"
+    AddressKindContract -> "contract"
+    AddressKindTxRollup -> "transaction rollup"
+
+genSingletonsType ''AddressKind
diff --git a/src/Morley/Tezos/Crypto.hs b/src/Morley/Tezos/Crypto.hs
--- a/src/Morley/Tezos/Crypto.hs
+++ b/src/Morley/Tezos/Crypto.hs
@@ -84,6 +84,7 @@
   , hashLengthBytes
   , formatSecretKey
   , parseSecretKey
+  , decodeKeyHash
 
   -- * Hashing
   , hashKey
@@ -110,9 +111,10 @@
   , decodeBase58CheckWithPrefix
   , keyDecoders
   , keyHashDecoders
-  , allHashTags
+  , AllHashTags(..)
   ) where
 
+import Control.Monad.Except (throwError)
 import Crypto.Random (MonadRandom)
 import Data.Aeson (FromJSON(..), FromJSONKey, ToJSON(..), ToJSONKey)
 import Data.Aeson qualified as Aeson
@@ -123,6 +125,7 @@
 import Data.ByteString qualified as BS
 import Data.ByteString.Lazy qualified as LBS
 import Data.Text qualified as T
+import Data.Text.Internal.Builder (Builder)
 import Fmt (Buildable, build, hexF, pretty)
 import Instances.TH.Lift ()
 import Language.Haskell.TH.Syntax (Lift)
@@ -382,10 +385,8 @@
     ])
 
 parsePublicKeyRaw :: ByteString -> Either Text PublicKey
-parsePublicKeyRaw ba =
-  case Get.runGetOrFail (decodeWithTag "key" keyDecoders) (LBS.fromStrict ba) of
-    Right (_, _, result) -> Right result
-    Left (_, _, err) -> Left (toText err)
+parsePublicKeyRaw ba = bimap (toText . view _3) (view _3) $
+  Get.runGetOrFail (decodeWithTag "key" keyDecoders) (LBS.fromStrict ba)
 
 formatSignature :: Signature -> Text
 formatSignature = \case
@@ -469,12 +470,12 @@
 instance ToJSONKey (Hash kind) where
   toJSONKey = AesonTypes.toJSONKeyText formatHash
 
-instance AllTags kind => FromJSON (Hash kind) where
+instance AllHashTags kind => FromJSON (Hash kind) where
   parseJSON =
     Aeson.withText "Hash" $
     either (fail . pretty) pure . parseHash
 
-instance AllTags kind => FromJSONKey (Hash kind) where
+instance AllHashTags kind => FromJSONKey (Hash kind) where
   fromJSONKey =
     AesonTypes.FromJSONKeyTextParser $
     either (fail . pretty) pure . parseHash
@@ -487,19 +488,19 @@
 type KeyHashTag = HashTag 'HashKindPublicKey
 
 -- | List all 'HashTag's for a given 'HashKind'.
-class AllTags kind where
+class AllHashTags kind where
   allHashTags :: NonEmpty (HashTag kind)
 
-instance AllTags 'HashKindPublicKey where
+instance AllHashTags 'HashKindPublicKey where
   allHashTags = HashEd25519 :| [HashSecp256k1, HashP256]
 
-instance AllTags 'HashKindContract where
+instance AllHashTags 'HashKindContract where
   allHashTags = pure HashContract
 
-instance AllTags 'HashKindL2PublicKey where
+instance AllHashTags 'HashKindL2PublicKey where
   allHashTags = pure HashBLS
 
-instance AllTags 'HashKindTxRollup where
+instance AllHashTags 'HashKindTxRollup where
   allHashTags = pure HashTXR
 
 -- | Blake2b_160 hash of something.
@@ -550,7 +551,7 @@
   build = build . formatHash
 
 parseHash
-  :: AllTags kind
+  :: AllHashTags kind
   => Text
   -> Either CryptoParseError (Hash kind)
 parseHash txt =
@@ -565,24 +566,25 @@
 
   in firstRight $ map parse allHashTags
 
+parseKeyHashHelper
+  :: Int
+  -> Builder
+  -> ExceptT CryptoParseError Get.Get a
+  -> ByteString
+  -> Either CryptoParseError a
+parseKeyHashHelper expectedLength name decoder ba
+  | BS.length ba /= expectedLength
+  = Left $ CryptoParseUnexpectedLength name (BS.length ba)
+  | otherwise
+  = either (Left . CryptoParseBinaryError . toText . view _3) (view _3)
+  $ flip Get.runGetOrFail (LBS.fromStrict ba) $ runExceptT decoder
+
 parseKeyHashRaw :: ByteString -> Either CryptoParseError KeyHash
-parseKeyHashRaw ba =
-  if (BS.length ba - 1 == hashLengthBytes) then
-    case Get.runGetOrFail (decodeWithTag "key_hash" keyHashDecoders) (LBS.fromStrict ba) of
-      Right (_, _, result) -> Right result
-      Left (_, _, err) -> Left $ CryptoParseBinaryError (toText err)
-  else
-    Left $ CryptoParseUnexpectedLength "key_hash" (BS.length ba)
+parseKeyHashRaw = parseKeyHashHelper (hashLengthBytes + 1) "key_hash" decodeKeyHash
 
 parseKeyHashL2Raw :: ByteString -> Either CryptoParseError KeyHashL2
-parseKeyHashL2Raw ba =
-  if (BS.length ba == hashLengthBytes) then
-    case Get.runGetOrFail (Hash HashBLS <$> getByteStringCopy hashLengthBytes)
-          (LBS.fromStrict ba) of
-      Right (_, _, result) -> Right result
-      Left (_, _, err) -> Left $ CryptoParseBinaryError (toText err)
-  else
-    Left $ CryptoParseUnexpectedLength "tx_rollup_l2_address" (BS.length ba)
+parseKeyHashL2Raw = parseKeyHashHelper hashLengthBytes "tx_rollup_l2_address" $
+  lift $ Hash HashBLS <$> getByteStringCopy hashLengthBytes
 
 -- | Magic constants used by Tezos to encode hashes with proper prefixes.
 hashTagBytes :: HashTag kind -> ByteString
@@ -601,7 +603,7 @@
     HashTXR -> "\001\128\120\031"
     -- https://gitlab.com/tezos/tezos/-/blob/0ca82c9dc361a6f223e81221c86bdb95d1a8d91c/src/proto_014_PtKathma/lib_protocol/tx_rollup_prefixes.ml#L35
 
-instance AllTags kind => HasCLReader (Hash kind) where
+instance AllHashTags kind => HasCLReader (Hash kind) where
   getReader = eitherReader (first pretty . parseHash . toText)
   getMetavar = "KEY_HASH"
 
@@ -615,11 +617,15 @@
       (fmap PublicKeyP256 . P256.mkPublicKey)
   ]
 
-keyHashDecoders :: [TaggedDecoder KeyHash]
+keyHashDecoders :: (Monad (t Get.Get), MonadTrans t) => [TaggedDecoderM t KeyHash]
 keyHashDecoders =
-  [ 0x00 #: Hash HashEd25519 <$> getPayload
-  , 0x01 #: Hash HashSecp256k1 <$> getPayload
-  , 0x02 #: Hash HashP256 <$> getPayload
+  [ 0x00 ##: Hash HashEd25519 <$> getPayload
+  , 0x01 ##: Hash HashSecp256k1 <$> getPayload
+  , 0x02 ##: Hash HashP256 <$> getPayload
   ]
   where
-    getPayload = getByteStringCopy hashLengthBytes
+    getPayload = lift $ getByteStringCopy hashLengthBytes
+
+decodeKeyHash :: ExceptT CryptoParseError Get.Get KeyHash
+decodeKeyHash =
+  decodeWithTagM "key_hash" (throwError . CryptoParseWrongTag . BS.singleton) keyHashDecoders
diff --git a/src/Morley/Util/Bimap.hs b/src/Morley/Util/Bimap.hs
new file mode 100644
--- /dev/null
+++ b/src/Morley/Util/Bimap.hs
@@ -0,0 +1,63 @@
+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
+-- SPDX-License-Identifier: LicenseRef-MIT-OA
+
+module Morley.Util.Bimap
+  ( Bimap(..)
+  , empty
+    -- * Optics
+  , flipped
+  ) where
+
+import Prelude hiding (empty)
+
+import Control.Lens (At(..), Index, Iso, IxValue, Ixed(..), iso)
+import Data.Aeson (FromJSON(..), ToJSON(..))
+import Data.Bimap qualified as Bimap
+import Data.Coerce (coerce)
+import GHC.Exts (IsList)
+
+newtype Bimap a b = Bimap { unBimap :: Bimap.Bimap a b }
+  deriving newtype (Show, Eq, Ord, IsList)
+
+empty :: Bimap a b
+empty = coerce Bimap.empty
+
+type instance Index (Bimap k _) = k
+type instance IxValue (Bimap _ v) = v
+
+-- | Left-biased 'Ixed' instance.
+-- It assumes the left value @a@ is the key (just like the @Ix (Map k v)@ instance).
+--
+-- To flip this assumption, use the 'flipped' optic.
+instance (Ord k, Ord v) => Ixed (Bimap k v) where
+  ix :: k -> Traversal' (Bimap k v) v
+  ix k handler (Bimap bmap) =
+    case Bimap.lookup k bmap of
+     Just v -> handler v <&> \v' -> Bimap $ Bimap.insert k v' bmap
+     Nothing -> pure $ Bimap bmap
+
+-- | Left-biased 'At' instance.
+-- It assumes the left value @a@ is the key (just like the @At (Map k v)@ instance).
+--
+-- To flip this assumption, use the 'flipped' optic.
+instance (Ord k, Ord v) => At (Bimap k v) where
+  at :: k -> Lens' (Bimap k v) (Maybe v)
+  at k handler (Bimap bmap) =
+    handler currentValueMaybe <&> \newValueMaybe ->
+      Bimap $
+        case (currentValueMaybe, newValueMaybe) of
+          (Nothing, Nothing) -> bmap
+          (Just _, Nothing) -> Bimap.delete k bmap
+          (_, Just newValue) -> Bimap.insert k newValue bmap
+    where
+      currentValueMaybe = Bimap.lookup k bmap
+
+-- | Isomorphism between @Bimap a b@ and @Bimap b a@.
+flipped :: Iso (Bimap a1 b1) (Bimap a2 b2) (Bimap b1 a1) (Bimap b2 a2)
+flipped = iso (coerce Bimap.twist) (coerce Bimap.twist)
+
+instance (Ord a, Ord b, FromJSON a, FromJSON b) => FromJSON (Bimap a b) where
+  parseJSON = fmap (Bimap . Bimap.fromList) . parseJSON
+
+instance (ToJSON a, ToJSON b) => ToJSON (Bimap a b) where
+  toJSON = toJSON . Bimap.toList . unBimap
diff --git a/src/Morley/Util/Binary.hs b/src/Morley/Util/Binary.hs
--- a/src/Morley/Util/Binary.hs
+++ b/src/Morley/Util/Binary.hs
@@ -7,10 +7,13 @@
   ( UnpackError (..)
   , ensureEnd
   , launchGet
-  , TaggedDecoder(..)
+  , TaggedDecoder
+  , TaggedDecoderM(..)
   , (#:)
+  , (##:)
   , decodeBytesLike
   , decodeWithTag
+  , decodeWithTagM
   , getByteStringCopy
   , getRemainingByteStringCopy
   , unknownTag
@@ -54,19 +57,27 @@
     Left (_remainder, _offset, err) -> Left . UnpackError $ toText err
     Right (_remainder, _offset, res) -> Right res
 
--- | Describes how 'decodeWithTag' should decode tag-dependent data.
+-- | Specialization of 'TaggedDecoderM' to 'IdentityT' transformer.
+type TaggedDecoder a = TaggedDecoderM IdentityT a
+
+-- | Describes how 'decodeWithTagM' should decode tag-dependent data.
 -- We expect bytes of such structure: 'tdTag' followed by a bytestring
 -- which will be parsed with 'tdDecoder'.
-data TaggedDecoder a = TaggedDecoder
+data TaggedDecoderM t a = TaggedDecoder
   { tdTag :: Word8
-  , tdDecoder :: Get a
+  , tdDecoder :: t Get a
   }
 
--- | Alias for 'TaggedDecoder' constructor.
+-- | Alias for v'TaggedDecoder' constructor specialized to 'Get'
 (#:) :: Word8 -> Get a -> TaggedDecoder a
-(#:) = TaggedDecoder
+(#:) t = TaggedDecoder t . lift
 infixr 0 #:
 
+-- | Alias for v'TaggedDecoder' constructor.
+(##:) :: Word8 -> t Get a -> TaggedDecoderM t a
+(##:) = TaggedDecoder
+infixr 0 ##:
+
 -- | Get a bytestring of the given length leaving no references to the
 -- original data in serialized form.
 getByteStringCopy :: Int -> Get ByteString
@@ -92,14 +103,30 @@
 unknownTag desc tag =
   fail . fmt $ "Unknown " <> build desc <> " tag: 0x" <> hexF tag
 
--- Common decoder for the case when packed data starts with a tag (1
--- byte) that specifies how to decode remaining data.
+-- | Common decoder for the case when packed data starts with a tag (1 byte)
+-- that specifies how to decode remaining data.
+--
+-- This is a version of 'decodeWithTagM' specialized to naked 'Get' monad.
 decodeWithTag :: String -> [TaggedDecoder a] -> Get a
-decodeWithTag what decoders = do
-  tag <- Get.label (what <> " tag") Get.getWord8
+decodeWithTag what decoders =
+  runIdentityT $ decodeWithTagM what (lift . unknownTag what) decoders
+
+-- | Common decoder for the case when packed data starts with a tag (1 byte)
+-- that specifies how to decode remaining data.
+--
+-- This is a general version of 'decodeWithTag' that allows 'Get' to be wrapped
+-- in a monad transformer.
+decodeWithTagM
+  :: (MonadTrans t, Monad (t Get))
+  => String
+  -> (Word8 -> t Get a)
+  -> [TaggedDecoderM t a]
+  -> t Get a
+decodeWithTagM what unknownTagFail decoders = do
+  tag <- lift $ Get.label (what <> " tag") Get.getWord8
   -- Number of decoders is usually small, so linear runtime lookup should be ok.
   case List.find ((tag ==) . tdTag) decoders of
-    Nothing -> unknownTag what tag
+    Nothing -> unknownTagFail tag
     Just TaggedDecoder{..} -> tdDecoder
 
 decodeBytesLike
diff --git a/src/Morley/Util/Interpolate/Internal.hs b/src/Morley/Util/Interpolate/Internal.hs
--- a/src/Morley/Util/Interpolate/Internal.hs
+++ b/src/Morley/Util/Interpolate/Internal.hs
@@ -62,6 +62,7 @@
 
 unescape :: String -> Q String
 unescape ('\\':'#':xs) = ('\\':) . ('#':) <$> unescape xs
+unescape ('\\':'&':xs) = unescape xs
 unescape xs@('\\':c:cs) = case readP_to_S lexChar xs of
   (ch, rest):_ -> (ch :) <$> unescape rest
   [] -> do
diff --git a/src/Morley/Util/MultiReader.hs b/src/Morley/Util/MultiReader.hs
new file mode 100644
--- /dev/null
+++ b/src/Morley/Util/MultiReader.hs
@@ -0,0 +1,98 @@
+-- SPDX-FileCopyrightText: 2022 Oxhead Alpha
+-- SPDX-License-Identifier: LicenseRef-MIT-OA
+
+-- | A poor man's extensible reader effects via nested 'ReaderT'.
+module Morley.Util.MultiReader
+  ( MultiReaderT
+  , MonadMultiReaderT
+  , ChangeMultiReaderBase
+  , asks'
+  , ask'
+  , local'
+  , mapMultiReaderT
+  ) where
+
+import Control.Monad.Reader (mapReaderT)
+import GHC.TypeLits (ErrorMessage(..), TypeError)
+
+import Morley.Util.Peano
+
+-- | Convenience type family to build a stack of multiple 'ReaderT'.
+type family MultiReaderT (xs :: [Type]) (m :: Type -> Type) :: Type -> Type where
+  MultiReaderT (x ': xs) m = ReaderT x (MultiReaderT xs m)
+  MultiReaderT '[] m = m
+
+-- | Convenience constraint synonym.
+--
+-- Required for `asks'`, `ask'`, `local'` and 'mapMultiReaderT'
+type MonadMultiReaderT m base =
+  (m ~ MultiReaderT (MultiReaderIso m) base, MonadMultiReaderMap (MultiReaderIso m))
+
+-- | Replace the base monad for a nested 'ReaderT' stack.
+type ChangeMultiReaderBase m newBase = MultiReaderT (MultiReaderIso m) newBase
+
+-- | Find the index of the first occurrence of the first argument in the second
+-- argument as a Peano number.
+--
+-- Essentially a type-level version of 'find'.
+--
+-- Raises a type error if the element is not found.
+type family MultiReaderDepth (r :: Type) (rs :: [Type]) :: Peano where
+  MultiReaderDepth r (r ': _) = 'Z
+  MultiReaderDepth r (_ ': rs) = 'S (MultiReaderDepth r rs)
+  MultiReaderDepth r '[] = TypeError (
+    'Text "MultiReaderT does not have a reader environment" ':$$:
+    'ShowType r ':$$: 'Text "anywhere in the stack."
+    )
+
+-- | Given a transformer stack of nested 'ReaderT', get a list of environments.
+-- This type family is essentially a witness of isomorphism between a stack of
+-- 'ReaderT' and a type-level list of reader environments.
+--
+-- This is useful because 'MultiReaderT' can't have an injectivity annotation.
+type family MultiReaderIso (m :: Type -> Type) :: [Type] where
+  MultiReaderIso (ReaderT r m) = r ': MultiReaderIso m
+  MultiReaderIso _ = '[]
+
+-- | Typeclass implementing versions of 'ask' and 'local' that aren't
+-- constrained by a functional dependency.
+class (Monad m, n ~ MultiReaderDepth r (MultiReaderIso m))
+  => MultiReader (n :: Peano) r m where
+  -- | Unconstrained version of 'ask'. Lifts the appropriate number of times
+  -- depending on the type @r@.
+  ask' :: m r
+
+  -- | Unconstrained version of 'local'. Maps the appropriate number of times
+  -- depending on the type @r@.
+  local' :: (r -> r) -> m a -> m a
+
+instance (Monad m) => MultiReader 'Z x (ReaderT x m) where
+  ask' = ask
+  local' = local
+
+instance
+  ( MultiReader n r m, Monad m, 'S n ~ MultiReaderDepth r (x ': MultiReaderIso m) )
+  => MultiReader ('S n) r (ReaderT x m) where
+  ask' = lift ask'
+  local' = mapReaderT . local'
+
+-- | Class implementing 'mapReaderT' over a stack of 'ReaderT'.
+class MonadMultiReaderMap xs where
+  -- | 'mapReaderT', only it maps over the whole nested 'ReaderT' stack, and not
+  -- just one level.
+  mapMultiReaderT
+    :: ( m' ~ MultiReaderT xs m
+       , n' ~ MultiReaderT xs n
+       , xs ~ MultiReaderIso m'
+       )
+    => (m a -> n b) -> m' a -> n' b
+
+instance MonadMultiReaderMap '[] where
+  mapMultiReaderT f = f
+
+instance (MonadMultiReaderMap xs) => MonadMultiReaderMap (x ': xs) where
+  mapMultiReaderT f = mapReaderT (mapMultiReaderT f)
+
+-- | Unconstrained version of 'asks'. @asks' f = fmap f ask'@.
+asks' :: forall m r (a :: Type) n. MultiReader n r m => (r -> a) -> m a
+asks' f = f <$> ask'
diff --git a/src/Morley/Util/Peano.hs b/src/Morley/Util/Peano.hs
--- a/src/Morley/Util/Peano.hs
+++ b/src/Morley/Util/Peano.hs
@@ -95,7 +95,7 @@
 import Unsafe.Coerce (unsafeCoerce)
 
 import Morley.Util.Sing (genSingletonsType)
-import Morley.Util.Type (If, MockableConstraint(..))
+import Morley.Util.Type (FailUnless, MockableConstraint(..))
 
 -- This is very obviously a false positive.
 {-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
@@ -130,7 +130,7 @@
 -- isomorphism)
 type IsoNatPeano (n :: GHC.Nat) (p :: Peano) = (n ~ FromPeano p, ToPeano n ~ p)
 
--- | A synonym for @SingI (ToPeano n)@. Essentialy requires that we can construct a 'Peano'
+-- | A synonym for @SingI (ToPeano n)@. Essentially requires that we can construct a 'Peano'
 -- singleton for a given 'Nat'
 type SingIPeano (n :: GHC.Nat) = SingI (ToPeano n)
 
@@ -327,15 +327,14 @@
 -- type family is internal.
 type family RequireLongerThan' (l :: [k]) (a :: Nat) :: Constraint where
   RequireLongerThan' l a =
-    If (IsLongerThan l a)
-       (() :: Constraint)
-       (TypeError
-          ('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:
-           'Text " is not accessible" ':$$:
-           'Text "Current stack has size of only " ':<>:
-           'ShowType (LengthWithTail l) ':<>:
-           'Text ":" ':$$: 'ShowType l
-           ))
+    FailUnless
+      (IsLongerThan l a)
+      ('Text "Stack element #" ':<>: 'ShowType (FromPeano a) ':<>:
+       'Text " is not accessible" ':$$:
+       'Text "Current stack has size of only " ':<>:
+       'ShowType (LengthWithTail l) ':<>:
+       'Text ":" ':$$: 'ShowType l
+       )
 
 class (RequireLongerThan' l a, LongerThan l a) =>
   RequireLongerThan (l :: [k]) (a :: Peano)
@@ -349,14 +348,13 @@
 -- GHC and also producess good error messages.
 type family RequireLongerOrSameLength' (l :: [k]) (a :: Peano) :: Constraint where
   RequireLongerOrSameLength' l a =
-    If (IsLongerOrSameLength l a)
-       (() :: Constraint)
-       (TypeError
-          ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
-           'Text "Current stack has size of only " ':<>:
-           'ShowType (LengthWithTail l) ':<>:
-           'Text ":" ':$$: 'ShowType l
-           ))
+    FailUnless
+      (IsLongerOrSameLength l a)
+      ('Text "Expected stack with length >= " ':<>: 'ShowType (FromPeano a) ':$$:
+       'Text "Current stack has size of only " ':<>:
+       'ShowType (LengthWithTail l) ':<>:
+       'Text ":" ':$$: 'ShowType l
+       )
 
 -- | We can have
 -- `RequireLongerOrSameLength = (RequireLongerOrSameLength' l a, LongerOrSameLength l a)`,
diff --git a/src/Morley/Util/Sing.hs b/src/Morley/Util/Sing.hs
--- a/src/Morley/Util/Sing.hs
+++ b/src/Morley/Util/Sing.hs
@@ -8,7 +8,8 @@
   , eqParamSing3
   , eqParamMixed3
   , castSing
-  , SingI1(..)
+  , SingIOne
+  , withSingIOne
   , genSingletonsType
   ) where
 
@@ -115,9 +116,16 @@
   Refl <- sing @a `decideEquality` sing @b
   return ca
 
--- Second-order analogue of 'SingI'
-class SingI1 f where
-  withSingI1 :: forall x r. SingI x => (SingI (f x) => r) -> r
+-- | A second-order analogue of 'SingI'. This serves the same purpose as the
+-- @"Data.Singletons".'Data.Singletons.SingIOne'@ class. However, the @singletons@
+-- version requires a separate instance for each type in order to support GHC
+-- versions that don't offer @QuantifiedConstraints@. We only need one instance
+-- for all types.
+class (forall x. SingI x => SingI (f x)) => SingIOne f
+instance (forall x. SingI x => SingI (f x)) => SingIOne f
+
+withSingIOne :: forall f x r. (SingIOne f, SingI x) => (SingI (f x) => r) -> r
+withSingIOne f = f
 
 -- | Helper function to generate 'SingI' and 'Data.Singletons.TH.SDecide' instances
 -- using @Sing@ as prefix for the type names and @S@ for constructors'.
diff --git a/src/Morley/Util/Type.hs b/src/Morley/Util/Type.hs
--- a/src/Morley/Util/Type.hs
+++ b/src/Morley/Util/Type.hs
@@ -12,9 +12,16 @@
   , IsElem
   , type (/)
   , type (//)
+  , AssertTypesEqual
+  , FailUnlessEqual
+  , FailUnlessEqualElse
   , Guard
   , FailWhen
+  , FailWhenElse
+  , FailWhenElsePoly
   , FailUnless
+  , FailUnlessElse
+  , FailUnlessElsePoly
   , failUnlessEvi
   , failWhenEvi
   , AllUnique
@@ -29,8 +36,6 @@
   , Some1 (..)
   , recordToSomeList
 
-  , reifyTypeEquality
-
   , ConcatListOfTypesAssociativity
   , listOfTypesConcatAssociativityAxiom
 
@@ -41,6 +46,7 @@
   ) where
 
 import Data.Constraint (Dict(..), (:-)(..), (\\))
+import Data.Eq.Singletons (DefaultEq)
 import Data.Singletons (SingI(sing))
 import Data.Type.Bool (If, Not, type (&&))
 import Data.Type.Equality (type (==))
@@ -52,6 +58,9 @@
 import Prelude.Singletons (SList(..))
 import Unsafe.Coerce (unsafeCoerce)
 
+-- $setup
+-- >>> import GHC.TypeLits (ErrorMessage (..))
+
 -- | Equality constraint in form of a typeclass.
 class a ~ b => IsEq a b
 instance a ~ b => IsEq a b
@@ -76,13 +85,153 @@
   Guard 'False _ = 'Nothing
   Guard 'True a = 'Just a
 
+-- | Constrain two types to be equal. If they are found not to be, produce
+-- an error message. If they are shown to be equal, impose an additional
+-- given constraint.
+--
+-- >>> :k! FailUnlessEqualElse Int Int ('Text "This should not result in a failure") ()
+-- FailUnlessEqualElse Int Int ('Text "This should not result in a failure") () :: Constraint
+-- = (() :: Constraint, Int ~ Int)
+--
+-- >>> :k! FailUnlessEqualElse Bool Int ('Text "This should result in a failure") ()
+-- FailUnlessEqualElse Bool Int ('Text "This should result in a failure") () :: Constraint
+-- = ((TypeError ...), Bool ~ Int)
+--
+-- the @~@ constraint might seem redundant, but, without it, GHC would reject
+--
+-- @
+-- foo :: FailUnlessEqualElse a b MyError () => a -> b
+-- foo = id
+-- @
+--
+-- GHC needs to \"see\" the type equality @~@ in order to actually \"learn\"
+-- something from a type family's result.
+--
+-- We use 'DefaultEq' here, rather than 'Data.Type.Equality.==', so this will
+-- work with type variables known to be equal, even if nothing is known about
+-- them concretely. For example, the following will compile:
+--
+-- @
+-- foo :: FailUnlessEqualElse a b MyError () => a -> b
+-- foo x = x
+--
+-- bar :: a -> a
+-- bar = foo
+-- @
+--
+-- If we used @(==)@, then bar would be rejected.
+--
+-- @(==)@ has its place (see the comments below it in "Data.Type.Equality")
+-- but I don't think it has anything to offer us here. In particular, the equality
+-- constraint we bundle up seems to win us all the reasoning power that @(==)@ would
+-- provide and more. The following adaptation of the example in the
+-- @Data.Type.Equality@ comments compiles:
+--
+-- @
+-- foo :: FailUnlessEqualElse (Maybe a) (Maybe b) ('Text "yo") ()
+--          :- FailUnlessEqualElse a b ('Text "heya") ()
+-- foo = Sub Dict
+-- @
+--
+-- In this example, the entire consequent follows from the equality constraint
+-- in the antecedent; the `FailUnlessElsePoly` part of it is irrelevant, so we
+-- don't need to be able to reason from it. If we /were/ reasoning solely using
+-- @(==)@, @foo@ would be rejected because the error messages are different.
+type FailUnlessEqualElse :: forall k. k -> k -> ErrorMessage -> Constraint -> Constraint
+type FailUnlessEqualElse a b err els =
+  ( FailUnlessElsePoly (a `DefaultEq` b) err els
+  , a ~ b
+  )
+
+-- | Constrain two types to be equal, and produce an error message if
+-- they are found not to be.
+--
+-- >>> :k! FailUnlessEqual Int Int ('Text "This should not result in a failure")
+-- FailUnlessEqual Int Int ('Text "This should not result in a failure") :: Constraint
+-- = (() :: Constraint, Int ~ Int)
+--
+-- >>> :k! FailUnlessEqual Bool Int ('Text "This should result in a failure")
+-- FailUnlessEqual Bool Int ('Text "This should result in a failure") :: Constraint
+-- = ((TypeError ...), Bool ~ Int)
+type FailUnlessEqual :: forall k. k -> k -> ErrorMessage -> Constraint
+type FailUnlessEqual a b err = FailUnlessEqualElse a b err ()
+
+-- | An old name for 'FailUnlessEqual'.
+type AssertTypesEqual :: forall k. k -> k -> ErrorMessage -> Constraint
+type AssertTypesEqual a b err = FailUnlessEqual a b err
+
+-- | A version of 'FailWhenElsePoly' that imposes an equality constraint on its
+-- 'Bool' argument.
+type FailWhenElse :: Bool -> ErrorMessage -> Constraint -> Constraint
+type FailWhenElse cond msg els = FailUnlessEqualElse cond 'False msg els
+
 -- | Fail with given error if the condition does not hold.
-type family FailUnless (cond :: Bool) (msg :: ErrorMessage) :: Constraint where
-  FailUnless 'True _ = ()
-  FailUnless 'False msg = TypeError msg
+-- Otherwise, return the third argument.
+--
+-- There is a subtle difference between @FailWhenElsePoly@ and the
+-- following type definition:
+--
+-- @
+-- type FailWhenElsePolyAlternative cond msg els =
+--   If cond
+--      (TypeError msg)
+--      els
+-- @
+--
+-- If @cond@ cannot be fully reduced (e.g., it's a stuck type family
+-- application or an ambiguous type) then:
+--
+-- * @FailWhenElsePoly@ will state that the constraint cannot be deduced (and
+--   this error message will be suppressed if there are also custom type
+--   errors).
+--
+-- * @FailWhenElsePolyAlternative@ will fail with the given error message,
+--   @err@.
+--
+-- For example:
+--
+-- @
+-- -- Partial function
+-- type family IsZero (n :: Peano) :: Bool where
+--   IsZero ('S _) = 'False
+--
+-- f1 :: (IsZero n ~ 'True, FailWhenElsePoly (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()
+-- f1 = ()
+--
+-- f1 :: (IsZero n ~ 'True, FailWhenElsePolyAlternative (IsZero n) ('Text "Expected zero") (() :: Constraint)) => ()
+-- f1 = ()
+--
+-- f1res == f1 @'Z
+-- --  • Couldn't match type ‘IsZero 'Z’ with ‘'True’
+--
+-- f2res == f2 @'Z
+-- --  • Expected zero
+-- @
+--
+-- As you can see, the error message in @f2res@ is misleading (because the type argument
+-- actually _is_ zero), so it's preferable to fail with the standard GHC error message.
+type FailWhenElsePoly :: forall k. Bool -> ErrorMessage -> k -> k
+type family FailWhenElsePoly cond msg els where
+  FailWhenElsePoly 'True msg _els = TypeError msg
+  FailWhenElsePoly 'False _ els = els
 
+-- | A version of 'FailUnlessElsePoly' that imposes an equality constraint on its
+-- 'Bool' argument.
+type FailUnlessElse :: Bool -> ErrorMessage -> Constraint -> Constraint
+type FailUnlessElse b msg els = FailWhenElse (Not b) msg els
+
+-- | Fail with given error if the condition does not hold. Otherwise,
+-- return the third argument.
+type FailUnlessElsePoly :: forall k. Bool -> ErrorMessage -> k -> k
+type FailUnlessElsePoly b e k = FailWhenElsePoly (Not b) e k
+
+-- | Fail with given error if the condition does not hold.
+type FailUnless :: Bool -> ErrorMessage -> Constraint
+type FailUnless cond msg = FailUnlessElse cond msg ()
+
 -- | Fail with given error if the condition holds.
-type FailWhen cond msg = FailUnless (Not cond) msg
+type FailWhen :: Bool -> ErrorMessage -> Constraint
+type FailWhen cond msg = FailWhenElse cond msg ()
 
 -- | A natural conclusion from the fact that an error has not occurred.
 failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)
@@ -97,15 +246,15 @@
 
 type RequireAllUnique desc l = RequireAllUnique' desc l l
 
-type family RequireAllUnique' (desc :: Symbol) (l :: [k]) (origL ::[k]) :: Constraint where
+type family RequireAllUnique' (desc :: Symbol) (l :: [k]) (origL :: [k]) :: Constraint where
   RequireAllUnique' _ '[] _ = ()
   RequireAllUnique' desc (x : xs) origL =
-    If (IsElem x xs)
-       (TypeError ('Text "Duplicated " ':<>: 'Text desc ':<>: 'Text ":" ':$$:
-                   'ShowType x ':$$:
-                   'Text "Full list: " ':<>:
-                   'ShowType origL
-                  )
+    FailWhenElse
+       (IsElem x xs)
+       ('Text "Duplicated " ':<>: 'Text desc ':<>: 'Text ":" ':$$:
+        'ShowType x ':$$:
+        'Text "Full list: " ':<>:
+        'ShowType origL
        )
        (RequireAllUnique' desc xs origL)
 
@@ -129,10 +278,6 @@
 
 instance (c x, ReifyList c xs) => ReifyList c (x ': xs) where
   reifyList reifyElem = reifyElem (Proxy @x) : reifyList @_ @c @xs reifyElem
-
--- | Reify type equality from boolean equality.
-reifyTypeEquality :: forall a b x. (a == b) ~ 'True => (a ~ b => x) -> x
-reifyTypeEquality x = x \\ unsafeProvideConstraint @(a ~ b)
 
 -- | Similar to @SingI []@, but does not require individual elements to be also
 -- instance of @SingI@.
diff --git a/src/Morley/Util/TypeLits.hs b/src/Morley/Util/TypeLits.hs
--- a/src/Morley/Util/TypeLits.hs
+++ b/src/Morley/Util/TypeLits.hs
@@ -15,87 +15,15 @@
   , TypeError
   , ErrorMessage (..)
 
-  , TypeErrorUnless
   , AssertTypesEqual
   ) where
 
-import Data.Type.Equality (type (==))
 import GHC.TypeLits (AppendSymbol, ErrorMessage(..), KnownSymbol, Symbol, TypeError, symbolVal)
 
+import Morley.Util.Type (AssertTypesEqual)
+
 symbolValT :: forall s. KnownSymbol s => Proxy s -> Text
 symbolValT = toText . symbolVal
 
 symbolValT' :: forall s. KnownSymbol s => Text
 symbolValT' = symbolValT (Proxy @s)
-
--- | Conditional type error.
---
--- There is a very subtle difference between 'TypeErrorUnless' and the following type family:
---
--- > type family TypeErrorUnlessAlternative (cond :: Bool) (err :: ErrorMessage) :: Constraint where
--- >   TypeErrorUnlessAlternative cond err =
--- >     ( If cond
--- >         (() :: Constraint)
--- >         (TypeError err)
--- >     , cond ~ 'True
--- >     )
---
--- If @cond@ cannot be fully reduced (e.g. it's a stuck type family), then:
---
--- * @TypeErrorUnless@ will state that the constraint cannot be deduced.
--- * @TypeErrorUnlessAlternative@ will fail with the given error message @err@.
---
--- For example:
---
--- > -- Partial function
--- > type family IsZero (n :: Peano) :: Bool where
--- >   IsZero ('S _) = 'False
--- >
--- > f1 :: TypeErrorUnless (IsZero n) ('Text "Expected zero") => ()
--- > f1 = ()
--- >
--- > f2 :: TypeErrorUnlessAlternative (IsZero n) ('Text "Expected zero") => ()
--- > f2 = ()
--- >
--- >
--- > f1res = f1 @'Z
--- > -- • Couldn't match type ‘IsZero 'Z’ with ‘'True’
--- >
--- > f2res = f2 @'Z
--- > -- • Expected zero
---
--- As you can see, the error message in @f2res@ is misleading (because the type argument
--- actually _is_ zero), so it's preferable to fail with the standard GHC error message.
-type TypeErrorUnless (cond :: Bool) (err :: ErrorMessage) =
-  ( TypeErrorUnlessHelper cond err
-  -- Note: the '~' constraint below might seem redundant, but, without it,
-  -- GHC would warn that the following pattern match is not exhaustive (even though it is):
-  --
-  -- > f :: TypeErrorUnless (n >= ToPeano 2) "some err msg" => Sing n -> ()
-  -- > f = \case
-  -- >   SS (SS SZ) -> ()
-  -- >   SS (SS _) -> ()
-  --
-  -- GHC needs to "see" the type equality '~' in order to actually "learn" something from a
-  -- type family's result.
-  , cond ~ 'True
-  )
-
-type family TypeErrorUnlessHelper (cond :: Bool) (err :: ErrorMessage) :: Constraint where
-  TypeErrorUnlessHelper 'True _ = ()
-  TypeErrorUnlessHelper 'False err = TypeError err
-
--- | Condition Error helper to check if two types are equal
---
--- >>> :k! AssertTypesEqual Int Int ('Text "This should not result in a failure")
--- AssertTypesEqual Int Int ('Text "This should not result in a failure") :: Constraint
--- = (() :: Constraint, Int ~ Int)
---
--- >>> :k! AssertTypesEqual Bool Int ('Text "This should result in a failure")
--- AssertTypesEqual Bool Int ('Text "This should result in a failure") :: Constraint
--- = ((TypeError ...), Bool ~ Int)
-type AssertTypesEqual a b (err :: ErrorMessage) =
-  ( TypeErrorUnlessHelper (a == b) err
-  -- The reasons for the constraint below are the same as those in @TypeErrorUnless@ constructor
-  , a ~ b
-  )