diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,30 @@
+1.10.0
+======
+* [!692](https://gitlab.com/morley-framework/morley/-/merge_requests/692)
+  The `ToJSON` instance for Micheline `Expression` now produces more compact JSON values,
+  by omitting the `"annots"` and `"args"` fields when these lists are empty.
+* [!673](https://gitlab.com/morley-framework/morley/-/merge_requests/673)
+  + Removed `TextException`.
+  Migration guide: use `StringException` or `throwString` from `safe-exceptions`.
+  + Removed `displayUncaughtException`.
+  Migration guide: use `uncaught-exception` library.
+  + Added `Util.Main` module, consider using it in your `Main.hs`.
+* [!657](https://gitlab.com/morley-framework/morley/-/merge_requests/657)
+  Make `namedParser` handle complex-worded options neatly.
+* [!678](https://gitlab.com/morley-framework/morley/-/merge_requests/678)
+  Added `FromExpression` instances for `Michelson.Untyped.Type`, `Michelson.Typed.T`,
+  and `Michelson.Typed.Instr`.
+* [!607](https://gitlab.com/morley-framework/morley/-/merge_requests/607)
+  Removed `parse` from the executable.
+* [!659](https://gitlab.com/morley-framework/morley/-/merge_requests/659)
+  Remove `Michelson.Interpret.MichelsonAmbigousEpRef` exception constructor.
+* [!664](https://gitlab.com/morley-framework/morley/-/merge_requests/664)
+  Added `Tezos.Crypto.Sign`.
+* [!638](https://gitlab.com/morley-framework/morley/-/merge_requests/638)
+  Added `Morley.Micheline.Json.TezosMutez`.
+* [!638](https://gitlab.com/morley-framework/morley/-/merge_requests/638)
+  Added `Tezos.Core.prettyTez`.
+
 1.9
 =====
 * [!653](https://gitlab.com/morley-framework/morley/-/merge_requests/653)
diff --git a/app/Main.hs b/app/Main.hs
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -10,7 +10,6 @@
 import qualified Data.Text.Lazy.IO.Utf8 as Utf8 (writeFile)
 import Data.Version (showVersion)
 import Fmt (pretty)
-import Main.Utf8 (withUtf8)
 import Named (arg, argF, (!))
 import Options.Applicative
   (command, execParser, footerDoc, fullDesc, header, help, helper, info, infoOption, long,
@@ -18,14 +17,11 @@
 import qualified Options.Applicative as Opt
 import Options.Applicative.Help.Pretty (Doc, linebreak)
 import Paths_morley (version)
-import Text.Pretty.Simple (pPrint)
 
 import Michelson.Analyzer (analyze)
-import Michelson.Macro (expandContract)
 import Michelson.Optimizer (optimize)
 import Michelson.Printer (printSomeContract, printUntypedContract)
-import Michelson.Runtime
-  (TxData(..), originateContract, prepareContract, readAndParseContract, runContract, transfer)
+import Michelson.Runtime (TxData(..), originateContract, prepareContract, runContract, transfer)
 import Michelson.Runtime.GState (genesisAddress)
 import Michelson.TypeCheck (tcVerbose, typeCheckContract)
 import Michelson.TypeCheck.Types (SomeContract(..), mapSomeContract)
@@ -37,7 +33,7 @@
 import Tezos.Core (Mutez, Timestamp(..), unsafeMkMutez)
 import Tezos.Crypto
 import Util.CLI (outputOption)
-import Util.Exception (displayUncaughtException)
+import Util.Main (wrapMain)
 import Util.Named
 
 ----------------------------------------------------------------------------
@@ -45,8 +41,7 @@
 ----------------------------------------------------------------------------
 
 data CmdLnArgs
-  = Parse (Maybe FilePath) Bool
-  | Print ("input" :? FilePath) ("output" :? FilePath) ("singleLine" :! Bool)
+  = Print ("input" :? FilePath) ("output" :? FilePath) ("singleLine" :! Bool)
   | Optimize OptimizeOptions
   | Analyze AnalyzeOptions
   | TypeCheck TypeCheckOptions
@@ -104,7 +99,6 @@
 
 argParser :: Opt.Parser CmdLnArgs
 argParser = subparser $
-  parseSubCmd <>
   printSubCmd <>
   typecheckSubCmd <>
   runSubCmd <>
@@ -119,11 +113,6 @@
       info (helper <*> parser) $
       progDesc desc
 
-    parseSubCmd =
-      mkCommandParser "parse"
-      (uncurry Parse <$> parseOptions)
-      "Parse passed contract"
-
     typecheckSubCmd =
       mkCommandParser "typecheck"
         (TypeCheck <$> typeCheckOptions) $
@@ -189,13 +178,6 @@
       <$> optional contractFileOption
       <*> verboseFlag
 
-    parseOptions :: Opt.Parser (Maybe FilePath, Bool)
-    parseOptions = (,)
-      <$> optional contractFileOption
-      <*> switch (
-        long "expand-macros" <>
-        help "Whether expand macros after parsing or not")
-
     defaultBalance :: Mutez
     defaultBalance = unsafeMkMutez 4000000
 
@@ -258,7 +240,7 @@
 ----------------------------------------------------------------------------
 
 main :: IO ()
-main = displayUncaughtException $ withUtf8 $ do
+main = wrapMain $ do
   cmdLnArgs <- execParser programInfo
   run cmdLnArgs
   where
@@ -275,11 +257,6 @@
 
     run :: CmdLnArgs -> IO ()
     run args = case args of
-      Parse mFilename hasExpandMacros -> do
-        contract <- readAndParseContract mFilename
-        if hasExpandMacros
-          then pPrint $ expandContract contract
-          else pPrint contract
       Print (argF #input -> mInputFile)
             (argF #output -> mOutputFile)
             (arg #singleLine -> forceSingleLine) -> do
diff --git a/app/REPL.hs b/app/REPL.hs
--- a/app/REPL.hs
+++ b/app/REPL.hs
@@ -26,19 +26,18 @@
 import System.Console.Haskeline
 import Text.Megaparsec (parse)
 
-import Michelson.Interpret (ContractEnv(..), interpretInstr)
+import Michelson.Interpret (interpretInstr)
 import Michelson.Macro (ParsedOp, expandList)
 import Michelson.Parser (errorBundlePretty, ops, parseExpandValue, type_)
 import Michelson.Parser.Types (noLetEnv)
 import Michelson.Printer (printDoc, printTypedValue)
 import Michelson.Printer.Util (doesntNeedParens)
-import Michelson.Runtime.GState (genesisAddress)
+import Michelson.Runtime.Dummy
 import Michelson.TypeCheck (SomeInstr(..), SomeInstrOut(..), getWTP, runTypeCheckIsolated)
 import Michelson.TypeCheck.Instr (typeCheckList, typeCheckParameter)
 import Michelson.TypeCheck.Types (HST(..), NotWellTyped(..))
 import qualified Michelson.Typed as T
 import qualified Michelson.Untyped as U
-import Tezos.Core (Timestamp(..), dummyChainId, unsafeMkMutez)
 
 data SomeStack = forall t. Typeable t => SomeStack
   { stValues :: (Rec T.Value t)
@@ -107,21 +106,6 @@
                 _ :/ (AnyOutInstr _) -> putTextLn "Encountered a FAILWITH instruction"
             Left err -> printErr $ show err
           Nothing -> printErr "Casting stack failed"
-
-dummyContractEnv :: ContractEnv
-dummyContractEnv = ContractEnv
-  { ceNow = Timestamp 100
-  , ceMaxSteps = 100500
-  , ceBalance = unsafeMkMutez 100
-  , ceContracts = mempty
-  , ceSelf = genesisAddress
-  , ceSource = genesisAddress
-  , ceSender = genesisAddress
-  , ceAmount = unsafeMkMutez 100
-  , ceChainId = dummyChainId
-  , ceOperationHash = Nothing
-  , ceGlobalCounter = 0
-  }
 
 printHelp :: ReplM ()
 printHelp = putTextLn "REPL starts with an empty stack. At each instruction entered,\
diff --git a/morley.cabal b/morley.cabal
--- a/morley.cabal
+++ b/morley.cabal
@@ -1,11 +1,11 @@
-cabal-version: 2.2
+cabal-version: 2.0
 
 -- This file has been generated from package.yaml by hpack version 0.34.2.
 --
 -- see: https://github.com/sol/hpack
 
 name:           morley
-version:        1.9
+version:        1.10.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
@@ -64,6 +64,7 @@
       Michelson.Printer
       Michelson.Printer.Util
       Michelson.Runtime
+      Michelson.Runtime.Dummy
       Michelson.Runtime.GState
       Michelson.Runtime.TxData
       Michelson.Text
@@ -140,6 +141,7 @@
       Util.Instances
       Util.Label
       Util.Lens
+      Util.Main
       Util.Markdown
       Util.Named
       Util.Num
@@ -158,7 +160,7 @@
       Paths_morley
   hs-source-dirs:
       src
-  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
+  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
   ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude
   build-depends:
       aeson
@@ -186,17 +188,19 @@
     , named
     , optparse-applicative
     , parser-combinators >=1.0.0
+    , scientific
     , semigroups >=0.19.1
     , show-type
     , singletons
     , syb
     , template-haskell
     , text
+    , text-manipulate
     , th-lift
     , th-lift-instances
     , time
     , timerep
-    , transformers-compat ==0.6.5
+    , uncaught-exception
     , unordered-containers
     , vector
     , vinyl
@@ -215,7 +219,7 @@
       Paths_morley
   hs-source-dirs:
       app
-  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
+  default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
   ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude
   build-depends:
       aeson
@@ -229,7 +233,6 @@
     , morley-prelude
     , named
     , optparse-applicative
-    , pretty-simple
     , text
     , vinyl
     , with-utf8
diff --git a/src/Michelson/Doc.hs b/src/Michelson/Doc.hs
--- a/src/Michelson/Doc.hs
+++ b/src/Michelson/Doc.hs
@@ -30,6 +30,7 @@
   , deIsAtomic
   , subDocToMarkdown
   , docItemToBlock
+  , docItemSectionRef
   , lookupDocBlockSection
   , contractDocToMarkdown
   , contractDocToToc
@@ -50,8 +51,6 @@
   , DConversionInfo (..)
   ) where
 
-import Control.Lens.Cons (_head)
-import Data.Char (toLower)
 import qualified Data.Map as M
 import qualified Data.Map.Merge.Strict as M
 import qualified Data.Set as S
@@ -368,21 +367,51 @@
         content =
           mconcat $ resItems <&> \di ->
             docItemToMarkdownFull (headerLevelDelta hl) di
+        anchor = maybe "" mdAnchor (docItemSectionAnchor @di)
     in if null resItems
        then ""
-       else sectionNameFull <> sectionDescFull <> content
+       else anchor <> sectionNameFull <> sectionDescFull <> content
 
+-- | Anchor for all the sections (referring them as to headers may cause
+-- colissions).
+newtype SectionAnchor = SectionAnchor
+  { _unSectionAnchor :: Text
+    -- ^ Section name
+  }
+
+instance ToAnchor SectionAnchor where
+  toAnchor (SectionAnchor t) = Anchor ("section-" <> t)
+
+-- | Make an anchor that is to be attached to the given section.
+docItemSectionAnchor :: forall di. DocItem di => Maybe SectionAnchor
+docItemSectionAnchor = do
+  case docItemSectionNameStyle @di of
+    DocSectionNameBig -> pass
+    DocSectionNameSmall -> mzero
+  SectionAnchor <$> docItemSectionName @di
+
+-- | Reference to the given section.
+--
+-- Will return @Nothing@ if sections of given doc item type are not
+-- assumed to be referred outside.
+docItemSectionRef :: forall di. DocItem di => Maybe Markdown
+docItemSectionRef = do
+  name <- docItemSectionName @di
+  anchor <- docItemSectionAnchor @di
+  return $ mdLocalRef (build name) anchor
+
 -- | Render a part of table of contents from 'DocBlock'.
 docBlockToToc :: HeaderLevel -> DocBlock -> Markdown
 docBlockToToc hl block =
   mconcat $ M.elems block <&> \(DocSection items@((_ :: DocElem di) :| _)) ->
     let sectionName = docItemSectionName @di
         (sectionNameFull, headerLevelDelta) =
-          case sectionName of
-            Nothing -> ("", id)
-            Just "Table of contents" -> ("", id)
-            Just sn ->
-              (mdToc hl (build sn) (over _head toLower $ sn), nextHeaderLevel)
+          case (sectionName, docItemSectionAnchor @di) of
+            (_, Nothing) -> ("", id)
+            (Nothing, _) -> ("", id)
+            (Just "Table of contents", _) -> ("", id)
+            (Just sn, Just anchor) ->
+              (mdToc hl (build sn) anchor, nextHeaderLevel)
         resItems = docItemsOrder $ map deItem (toList items)
         content =
           mconcat $ resItems <&> docItemToToc (headerLevelDelta hl)
@@ -681,7 +710,7 @@
     \this contract from Haskell, but for each Haskell type we also mention its \
     \Michelson representation to make interactions outside of Haskell possible.\n\n\
     \There are multiple ways to interact with this contract:\n\n\
-    \* Use this contract in your Haskell application, thus all operation submission\
+    \* Use this contract in your Haskell application, thus all operation submissions \
     \should be handled separately, e.g. via calling `tezos-client`, which will communicate \
     \with the `tezos-node`. In order to be able to call `tezos-client` you'll need to be able \
     \to construct Michelson values from Haskell.\n\n\
@@ -695,5 +724,5 @@
     \resulting `Raw packed data` should be decoded from the hexadecimal representation using `decodeHex` \
     \and deserialized to the Haskell value via `lUnpackValue` function from \
     \[`Lorentz.Pack`](https://gitlab.com/morley-framework/morley/-/blob/2441e26bebd22ac4b30948e8facbb698d3b25c6d/code/lorentz/src/Lorentz/Pack.hs).\n\n\
-    \* Contruct values for this contract directly on Michelson level using types provided in the \
+    \* Construct values for this contract directly on Michelson level using types provided in the \
     \documentation."
diff --git a/src/Michelson/Interpret.hs b/src/Michelson/Interpret.hs
--- a/src/Michelson/Interpret.hs
+++ b/src/Michelson/Interpret.hs
@@ -7,6 +7,7 @@
 module Michelson.Interpret
   ( ContractEnv (..)
   , InterpreterState (..)
+  , isMorleyLogsL
   , MichelsonFailed (..)
   , RemainingSteps (..)
   , SomeItStack (..)
@@ -22,6 +23,7 @@
   , InterpretError (..)
   , InterpretResult (..)
   , EvalM
+  , InterpreterStateMonad (..)
   , InstrRunner
   , runInstr
   , runInstrNoGas
@@ -35,13 +37,14 @@
 
 import Prelude hiding (EQ, GT, LT)
 
+import Control.Lens (makeLensesFor)
 import Control.Monad.Except (MonadError, throwError)
 import Data.Default (Default(..))
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Data.Singletons (Sing)
 import Data.Vinyl (Rec(..), (<+>))
-import Fmt (Buildable(build), Builder, genericF)
+import Fmt (Buildable(build), Builder, blockListF, prettyLn)
 
 import Michelson.Interpret.Pack (packValue')
 import Michelson.Interpret.Unpack (UnpackError, unpackValue')
@@ -96,7 +99,6 @@
     => ArithError (Value' instr n) (Value' instr m) -> MichelsonFailed
   MichelsonGasExhaustion :: MichelsonFailed
   MichelsonFailedTestAssert :: Text -> MichelsonFailed
-  MichelsonAmbigousEpRef :: EpName -> EpAddress -> MichelsonFailed
 
 deriving stock instance Show MichelsonFailed
 
@@ -109,9 +111,6 @@
   MichelsonGasExhaustion == _ = False
   MichelsonFailedTestAssert t1 == MichelsonFailedTestAssert t2 = t1 == t2
   MichelsonFailedTestAssert _ == _ = False
-  MichelsonAmbigousEpRef ep1 epAddr1 == MichelsonAmbigousEpRef ep2 epAddr2 =
-    ep1 == ep2 && epAddr1 == epAddr2
-  MichelsonAmbigousEpRef _ _ == _ = False
 
 instance Buildable MichelsonFailed where
   build =
@@ -122,9 +121,6 @@
       MichelsonGasExhaustion ->
         "Gas limit exceeded on contract execution"
       MichelsonFailedTestAssert t -> build t
-      MichelsonAmbigousEpRef instrEp epAddr ->
-        "Ambigous entrypoint reference. `CONTRACT %" <> build instrEp <> "` \
-        \called over address " <> build epAddr
     where
       formatValue :: forall t . SingI t => Value t -> Builder
       formatValue v =
@@ -138,7 +134,7 @@
 deriving stock instance Show InterpretError
 
 instance Buildable InterpretError where
-  build = genericF
+  build (InterpretError (mf, logs)) = prettyLn mf <> "MorleyLogs are:\n" <> build logs
 
 data InterpretResult where
   InterpretResult
@@ -167,8 +163,11 @@
   { unMorleyLogs :: [Text]
     -- ^ Logs in reverse order.
   } deriving stock (Eq, Show, Generic)
-    deriving newtype (Default, Buildable)
+    deriving newtype Default
 
+instance Buildable MorleyLogs where
+  build (MorleyLogs logs) = blockListF $ reverse logs
+
 instance NFData MorleyLogs
 
 noMorleyLogs :: MorleyLogs
@@ -268,9 +267,30 @@
 runEvalOp act env initSt =
   flip runState initSt $ usingReaderT env $ runExceptT act
 
+class Monad m => InterpreterStateMonad m where
+  getInterpreterState :: m InterpreterState
+  getInterpreterState = stateInterpreterState (\s -> (s, s))
+
+  putInterpreterState :: InterpreterState -> m ()
+  putInterpreterState s = stateInterpreterState (\_ -> ((), s))
+
+  stateInterpreterState :: (InterpreterState -> (a, InterpreterState)) -> m a
+  stateInterpreterState f = do
+    s <- getInterpreterState
+    let (a, s') = f s
+    a <$ putInterpreterState s'
+
+  modifyInterpreterState :: (InterpreterState -> InterpreterState) -> m ()
+  modifyInterpreterState f = stateInterpreterState (((), ) . f)
+
+instance InterpreterStateMonad (ExceptT MichelsonFailed $
+                              ReaderT ContractEnv $
+                                 State InterpreterState) where
+  stateInterpreterState f = lift $ lift $ state f
+
 type EvalM m =
   ( MonadReader ContractEnv m
-  , MonadState InterpreterState m
+  , InterpreterStateMonad m
   , MonadError MichelsonFailed m
   )
 
@@ -283,16 +303,17 @@
 -- | Function to change amount of remaining steps stored in State monad
 runInstr :: EvalM m => InstrRunner m
 runInstr i@(Seq _i1 _i2) r = runInstrImpl runInstr i r
+runInstr i@(WithLoc _ _) r = runInstrImpl runInstr i r
 runInstr i@(InstrWithNotes _ _i1) r = runInstrImpl runInstr i r
 runInstr i@(InstrWithVarNotes _ _i1) r = runInstrImpl runInstr i r
 runInstr i@Nop r = runInstrImpl runInstr i r
 runInstr i@(Nested _) r = runInstrImpl runInstr i r
 runInstr i r = do
-  rs <- gets isRemainingSteps
+  rs <- isRemainingSteps <$> getInterpreterState
   if rs == 0
   then throwError $ MichelsonGasExhaustion
   else do
-    modify (\s -> s {isRemainingSteps = rs - 1})
+    modifyInterpreterState (\s -> s {isRemainingSteps = rs - 1})
     runInstrImpl runInstr i r
 
 runInstrNoGas :: EvalM m => InstrRunner m
@@ -301,7 +322,7 @@
 -- | Function to interpret Michelson instruction(s) against given stack.
 runInstrImpl :: EvalM m => InstrRunner m -> InstrRunner m
 runInstrImpl runner (Seq i1 i2) r = runner i1 r >>= \r' -> runner i2 r'
-runInstrImpl runner (WithLoc _ i) r = runInstrImpl runner i r
+runInstrImpl runner (WithLoc _ i) r = runner i r
 runInstrImpl runner (InstrWithNotes _ i) r = runner i r
 runInstrImpl runner (InstrWithVarNotes _ i) r = runner i r
 runInstrImpl runner (FrameInstr (_ :: Proxy s) i) r = do
@@ -463,20 +484,25 @@
 runInstrImpl _ (CONTRACT (nt :: T.Notes a) instrEpName) (VAddress epAddr :& r) = do
   ContractEnv{..} <- ask
   let T.EpAddress addr addrEpName = epAddr
-  epName <- case (instrEpName, addrEpName) of
-    (DefEpName, DefEpName) -> pure DefEpName
-    (DefEpName, en) -> pure en
-    (en, DefEpName) -> pure en
-    _ -> throwError $ MichelsonAmbigousEpRef instrEpName epAddr
+  let mepName =
+        case (instrEpName, addrEpName) of
+          (DefEpName, DefEpName) -> Just DefEpName
+          (DefEpName, en) -> Just en
+          (en, DefEpName) -> Just en
+          _ -> Nothing
 
-  pure $ case addr of
-    KeyAddress _ ->
-      castContract addr epName T.tyImplicitAccountParam :& r
-    ContractAddress ca ->
-      case Map.lookup ca ceContracts of
-        Just (SomeParamType _ paramNotes) ->
-          castContract addr epName paramNotes :& r
-        Nothing -> VOption Nothing :& r
+  pure $ case mepName of
+    Nothing ->
+      VOption Nothing :& r
+    Just epName ->
+      case addr of
+        KeyAddress _ ->
+          castContract addr epName T.tyImplicitAccountParam :& r
+        ContractAddress ca ->
+          case Map.lookup ca ceContracts of
+            Just (SomeParamType _ paramNotes) ->
+              castContract addr epName paramNotes :& r
+            Nothing -> VOption Nothing :& r
   where
   castContract
     :: forall p. T.ParameterScope p
@@ -497,10 +523,10 @@
   (VOption mbKeyHash :& VMutez m :& g :& r) = do
   originator <- ceSelf <$> ask
 
-  originationNonce <- gets isOriginationNonce
+  originationNonce <- isOriginationNonce <$> getInterpreterState
   globalCounter <- asks ceGlobalCounter
   opHash <- ceOperationHash <$> ask
-  modify $ \iState ->
+  modifyInterpreterState $ \iState ->
     iState { isOriginationNonce = OriginationIndex $ (unOriginationIndex $ isOriginationNonce iState) + 1 }
   let ops = cCode contract
   let resAddr =
@@ -594,7 +620,7 @@
 interpretExt (SomeItStack (T.PRINT (T.PrintComment pc)) st) = do
   let getEl (Left l) = l
       getEl (Right str) = withStackElem str st show
-  modify (\s -> s {isMorleyLogs = MorleyLogs $ mconcat (map getEl pc) : unMorleyLogs (isMorleyLogs s)})
+  modifyInterpreterState (\s -> s {isMorleyLogs = MorleyLogs $ mconcat (map getEl pc) : unMorleyLogs (isMorleyLogs s)})
 
 interpretExt (SomeItStack (T.TEST_ASSERT (T.TestAssert nm pc instr)) st) = do
   ost <- runInstrNoGas instr st
@@ -624,3 +650,4 @@
       (_ :& es, SS n) -> loop (es, n)
 
 (deriveGADTNFData ''MichelsonFailed)
+makeLensesFor [("isMorleyLogs", "isMorleyLogsL")] ''InterpreterState
diff --git a/src/Michelson/Interpret/Pack.hs b/src/Michelson/Interpret/Pack.hs
--- a/src/Michelson/Interpret/Pack.hs
+++ b/src/Michelson/Interpret/Pack.hs
@@ -134,7 +134,11 @@
   "\x0a" <> encodeAsList bs
 
 encodeEpName :: EpName -> LByteString
-encodeEpName = encodeUtf8 . unAnnotation . epNameToRefAnn
+encodeEpName = encodeUtf8 . unAnnotation . epNameToRefAnn . canonicalize
+  where
+    canonicalize :: EpName -> EpName
+    canonicalize (EpNameUnsafe "default") = DefEpName
+    canonicalize epName                   = epName
 
 -- | Encode some map.
 encodeMap :: (SingI v, HasNoOp v, SingI k, HasNoOp k) => Map (Value k) (Value v) -> LByteString
@@ -384,9 +388,16 @@
 
 -- | Encode an instruction with variable annotations
 encodeVarNotedInstr :: Instr inp out -> NonEmpty VarAnn -> LByteString
-encodeVarNotedInstr i vns = case i of
-  InstrWithNotes n a -> encodeNotedInstr a n (toList vns)
-  _ -> encodeWithAnns [] [] (toList vns) $ encodeInstr i
+encodeVarNotedInstr i (toList -> vns) = case i of
+  InstrWithNotes n a -> encodeNotedInstr a n vns
+  -- AnnPAIR, AnnCAR and AnnCDR are checked here because their cases on
+  -- `encodeInstr` increment them to \x04 when they have a field annotation, but
+  -- they would also get increment due to variable annotations, resulting in an
+  -- incorrect \x05 code.
+  AnnPAIR tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns "\x03\x42"
+  AnnCAR fn -> encodeWithAnns [] [fn] vns "\x03\x16"
+  AnnCDR fn -> encodeWithAnns [] [fn] vns "\x03\x17"
+  _ -> encodeWithAnns [] [] vns $ encodeInstr i
 
 -- | Encode an instruction with Annotations
 encodeNotedInstr
diff --git a/src/Michelson/Interpret/Unpack.hs b/src/Michelson/Interpret/Unpack.hs
--- a/src/Michelson/Interpret/Unpack.hs
+++ b/src/Michelson/Interpret/Unpack.hs
@@ -21,7 +21,9 @@
   , unpackValue'
   , unpackInstr'
 
+  -- * Internals
   , decodeContract
+  , decodeType
   ) where
 
 import Prelude hiding (EQ, Ordering(..), get)
@@ -55,7 +57,7 @@
 import Michelson.Typed.Scope (UnpackedValScope)
 import Michelson.Untyped
 import Tezos.Core
-import Tezos.Crypto
+import Tezos.Crypto hiding (sign)
 import Util.Binary
 import Util.Num
 
diff --git a/src/Michelson/Optimizer.hs b/src/Michelson/Optimizer.hs
--- a/src/Michelson/Optimizer.hs
+++ b/src/Michelson/Optimizer.hs
@@ -106,6 +106,7 @@
     `orSimpleRule` adjacentDrops
     `orSimpleRule` specificPush
     `orSimpleRule` pairUnpair
+    `orSimpleRule` unpairMisc
     `orSimpleRule` swapBeforeCommutative
 
 -- | We do not enable 'pushPack' rule by default because it is
@@ -326,6 +327,12 @@
   UNPAIR_c (Seq PAIR c) -> Just c
   UNPAIR_c      PAIR    -> Just Nop
 
+  _ -> Nothing
+
+unpairMisc :: Rule
+unpairMisc = \case
+  Seq UNPAIR SWAP -> Just (DUP `Seq` CDR `Seq` DIP CAR)
+  Seq UNPAIR (Seq SWAP c) -> Just (DUP `Seq` CDR `Seq` DIP CAR `Seq` c)
   _ -> Nothing
 
 commuteArith ::
diff --git a/src/Michelson/Parser/Macro.hs b/src/Michelson/Parser/Macro.hs
--- a/src/Michelson/Parser/Macro.hs
+++ b/src/Michelson/Parser/Macro.hs
@@ -96,7 +96,12 @@
   a <- upairMacInner
   symbol' "R"
   (vns, fns) <- permute2Def (some note) (some note)
-  return $ UNPAIR (Macro.mapUnpairLeaves (zip vns fns) a)
+  return $ UNPAIR (Macro.mapUnpairLeaves (padAnnotations vns fns) a)
+  where
+    padAnnotations []       []       = []
+    padAnnotations []       (f : fs) = (noAnn, f) : padAnnotations [] fs
+    padAnnotations (v : vs) []       = (v, noAnn) : padAnnotations vs []
+    padAnnotations (v : vs) (f : fs) = (v, f    ) : padAnnotations vs fs
 
 cadrMac :: Parser Macro
 cadrMac = lexeme $ do
diff --git a/src/Michelson/Runtime/Dummy.hs b/src/Michelson/Runtime/Dummy.hs
new file mode 100644
--- /dev/null
+++ b/src/Michelson/Runtime/Dummy.hs
@@ -0,0 +1,66 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | Dummy data to be used in tests or demos where it's not essential.
+
+module Michelson.Runtime.Dummy
+  ( dummyNow
+  , dummyMaxSteps
+  , dummyContractEnv
+  , dummyOrigination
+  ) where
+
+import Michelson.Interpret (ContractEnv(..), RemainingSteps)
+import Michelson.Runtime.GState (genesisAddress)
+import Michelson.Typed (ParameterScope, StorageScope)
+import qualified Michelson.Typed as T
+import Michelson.Typed.Origination (OriginationOperation(..))
+import Tezos.Core (Timestamp(..), dummyChainId, unsafeMkMutez)
+
+-- | Dummy timestamp, can be used to specify current `NOW` value or
+-- maybe something else.
+dummyNow :: Timestamp
+dummyNow = Timestamp 100
+
+-- | Dummy value for maximal number of steps a contract can
+-- make. Intentionally quite large, because most likely if you use
+-- dummy value you don't want the interpreter to stop due to gas
+-- exhaustion. On the other hand, it probably still prevents the
+-- interpreter from working for eternity.
+dummyMaxSteps :: RemainingSteps
+dummyMaxSteps = 100500
+
+-- | Dummy 'ContractEnv' with some reasonable hardcoded values. You
+-- can override values you are interested in using record update
+-- syntax.
+dummyContractEnv :: ContractEnv
+dummyContractEnv = ContractEnv
+  { ceNow = dummyNow
+  , ceMaxSteps = dummyMaxSteps
+  , ceBalance = unsafeMkMutez 100
+  , ceContracts = mempty
+  , ceSelf = genesisAddress
+  , ceSource = genesisAddress
+  , ceSender = genesisAddress
+  , ceAmount = unsafeMkMutez 100
+  , ceChainId = dummyChainId
+  , ceOperationHash = Nothing
+  , ceGlobalCounter = 0
+  }
+
+-- | 'OriginationOperation' with most data hardcoded to some
+-- reasonable values. Contract and initial values must be passed
+-- explicitly, because otherwise it hardly makes sense.
+dummyOrigination
+  :: (ParameterScope cp, StorageScope st)
+  => T.Value st
+  -> T.Contract cp st
+  -> OriginationOperation
+dummyOrigination storage contract = OriginationOperation
+  { ooOriginator = genesisAddress
+  , ooDelegate = Nothing
+  , ooBalance = unsafeMkMutez 100
+  , ooStorage = storage
+  , ooContract = contract
+  }
diff --git a/src/Michelson/TypeCheck/Helpers.hs b/src/Michelson/TypeCheck/Helpers.hs
--- a/src/Michelson/TypeCheck/Helpers.hs
+++ b/src/Michelson/TypeCheck/Helpers.hs
@@ -271,24 +271,76 @@
   Un.SeqEx sq                      -> typeCheckSeq sq
   where
     -- If we know source location from the untyped instruction, keep it in the typed one.
+    typeCheckPrimWithLoc :: InstrCallStack -> Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
     typeCheckPrimWithLoc loc op = local (const loc)
       (wrapWithLoc loc <$> typeCheckPrim op)
 
+    typeCheckPrim :: Un.ExpandedInstr -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
     typeCheckPrim op = tcInstr op inputStack <&> mapSeq addNotes
 
-    typeCheckSeqWithLoc loc = local (const loc) . typeCheckSeq
+    typeCheckSeqWithLoc :: InstrCallStack -> [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
+    typeCheckSeqWithLoc loc = fmap (wrapWithLoc loc) . local (const loc) . typeCheckSeq
 
+    typeCheckSeq :: [Un.ExpandedOp] -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
     typeCheckSeq sq = typeCheckImpl tcInstr sq inputStack
                   <&> mapSeq (addNotes . mapSomeInstr Nested)
 
+    addNotes :: SomeInstr inp -> SomeInstr inp
     addNotes (inp :/ i ::: out) = inp :/ wrapWithNotes out i ::: out
     addNotes i = i
 
     wrapWithNotes :: HST d -> Instr c d -> Instr c d
-    wrapWithNotes outputStack instr = case outputStack of
-      -- do not wrap in notes if the notes are "star"
-      ((n, _, _) ::& _) | isStar n -> instr
-      ((n, _, _) ::& _) -> InstrWithNotes (PackedNotes n) instr
+    wrapWithNotes outputStack instr = case instr of
+      -- Abstractions for instructions:
+      Nop -> instr'
+      Seq _ _ -> instr'
+      Nested _ -> instr'
+      DocGroup _ _ -> instr'
+      Ext _ -> instr'
+      FrameInstr _ _ -> instr'
+      WithLoc _ _ -> instr'
+      -- These two shouldn't happen, since annotations are added here.
+      InstrWithNotes _ _ -> instr'
+      InstrWithVarNotes _ _ -> instr'
+
+      -- Instructions that don't produce notes:
+      DROP -> instr'
+      SWAP -> instr'
+      DIG _ -> instr'
+      DUG _ -> instr'
+      IF_NONE _ _ -> instr'
+      IF_LEFT _ _ -> instr'
+      IF_CONS _ _ -> instr'
+      ITER _ -> instr'
+      IF _ _ -> instr'
+      LOOP _ -> instr'
+      LOOP_LEFT _ -> instr'
+      DIP _ -> instr'
+      DIPN _ _ -> instr'
+      FAILWITH -> instr'
+
+      -- Instructions that produce at most two notes:
+      CREATE_CONTRACT _ -> case outputStack of
+        ((np, _, vp) ::& (_, _, vs) ::& _) ->
+          let withNotes = if isStar np then id else InstrWithNotes (PackedNotes np)
+              withVarNotes = if vp == Un.noAnn && vs == Un.noAnn then id else InstrWithVarNotes (vp :| [vs])
+           in withNotes . withVarNotes $ instr
+
+      -- Instructions that produce at most one note:
+      _ -> case outputStack of
+        ((n, _, v) ::& _) ->
+          let withNotes = if isStar n then id else InstrWithNotes (PackedNotes n)
+              withVarNotes = if v == Un.noAnn then id else InstrWithVarNotes (one v)
+           in withNotes . withVarNotes $ instr
+        SNil -> instr
+      where
+        instr' = addNotesNoVarAnn outputStack instr
+
+    addNotesNoVarAnn :: HST d -> Instr c d -> Instr c d
+    addNotesNoVarAnn outputStack instr = case outputStack of
+      ((n, _, _) ::& _)
+        | isStar n -> instr
+        | otherwise -> InstrWithNotes (PackedNotes n) instr
       SNil -> instr
 
 -- | Like 'typeCheckImpl' but doesn't add a stack type comment after the
@@ -421,7 +473,7 @@
 wrapWithLoc loc = mapSeq $ \someInstr -> case someInstr of
   (_ :/ WithLoc{} ::: _) -> someInstr
   (inp :/ instr ::: out) -> inp :/ WithLoc loc instr ::: out
-  _ -> someInstr
+  (inp :/ AnyOutInstr instr) -> inp :/ (AnyOutInstr $ WithLoc loc instr)
 
 -- | Check whether given types are structurally equal and annotations converge.
 matchTypes
diff --git a/src/Michelson/TypeCheck/Instr.hs b/src/Michelson/TypeCheck/Instr.hs
--- a/src/Michelson/TypeCheck/Instr.hs
+++ b/src/Michelson/TypeCheck/Instr.hs
@@ -344,8 +344,8 @@
         (_, (_ ::& iTail)) -> do
           go (n - 1) iTail <&> \case TCDropHelper s out -> TCDropHelper (SS s) out
 
-  (U.DUP _vn, a ::& rs) -> workOnInstr uInstr $
-    pure (inp :/ DUP ::: (a ::& a::& rs))
+  (U.DUP vn1, a@(n, d, _vn2) ::& rs) -> workOnInstr uInstr $
+    pure (inp :/ DUP ::: ((n, d, vn1) ::& a ::& rs))
 
   (U.DUP _vn, SNil) -> notEnoughItemsOnStack
 
@@ -508,7 +508,7 @@
   (U.IF_CONS mp mq, (STList{}, ns, Dict, vn) ::&+ rs) -> do
     case ns of
       NTList _ (an :: Notes t1) -> withWTPInstr' @t1 $ do
-        let ait = (an, Dict, vn <> "hd") ::& (ns, Dict, vn <> "tl") ::& rs
+        let ait = (an, Dict, vn) ::& (ns, Dict, vn) ::& rs
         genericIf IF_CONS U.IF_CONS mp mq ait rs inp
 
   (U.IF_CONS _ _, _ ::& _) ->
diff --git a/src/Michelson/Typed/Convert.hs b/src/Michelson/Typed/Convert.hs
--- a/src/Michelson/Typed/Convert.hs
+++ b/src/Michelson/Typed/Convert.hs
@@ -157,11 +157,11 @@
     Ext _ -> instrToOps i
     WithLoc _ i0 -> instrToOps (InstrWithNotes n i0)
     InstrWithNotes _ _ -> instrToOps i
-    InstrWithVarNotes _ _ -> instrToOps i
     -- For inner instruction, filter out values that we don't want to apply
     -- annotations to and delegate it's conversion to this function itself.
     -- If none of the above, convert a single instruction and copy annotations
     -- to it.
+    InstrWithVarNotes n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n n0]
     _ -> [U.PrimEx $ handleInstrAnnotate i n]
   InstrWithVarNotes n i -> case i of
     Nop -> instrToOps i
@@ -170,201 +170,211 @@
     DocGroup _ _ -> instrToOps i
     Ext _ -> instrToOps i
     WithLoc _ i0 -> instrToOps (InstrWithVarNotes n i0)
-    InstrWithNotes _ _ -> instrToOps i
+    InstrWithNotes n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n0 n]
     InstrWithVarNotes _ _ -> instrToOps i
     _ -> [U.PrimEx $ handleInstrVarNotes i n]
   i -> [U.PrimEx $ handleInstr i]
   where
+    handleInstrAnnotateWithVarNotes
+      :: forall inp' out'
+       . HasCallStack
+      => Instr inp' out'
+      -> PackedNotes out'
+      -> NonEmpty U.VarAnn
+      -> U.ExpandedInstr
+    handleInstrAnnotateWithVarNotes ins' (PackedNotes notes') varAnns =
+      let x = handleInstr ins' in addVarNotes (addInstrNote x notes') varAnns
+
     handleInstrAnnotate
       :: forall inp' out' . HasCallStack
       => Instr inp' out' -> PackedNotes out' -> U.ExpandedInstr
     handleInstrAnnotate ins' (PackedNotes notes') = let
       x = handleInstr ins' in addInstrNote x notes'
-      where
-        addInstrNote
-          :: forall t. (SingI t, HasCallStack)
-          => U.ExpandedInstr -> Notes t -> U.ExpandedInstr
-        addInstrNote ins nte = case (sing @t, ins, nte) of
-            (_, U.PUSH va _ v, _) -> U.PUSH va (mkUType nte) v
-            (_, U.SOME _ va, NTOption ta _) -> U.SOME ta va
-            (STOption _, U.NONE _ va _, NTOption ta nt) -> U.NONE ta va (mkUType nt)
-            (_, U.UNIT _ va, NTUnit ta) -> U.UNIT ta va
-            (_, U.PAIR ta va f1 f2, _) -> U.PAIR ta va f1 f2
-            (_, U.CAR va f1, _) -> U.CAR va f1
-            (_, U.CDR va f1, _) -> U.CDR va f1
-            (STOr _ _, U.LEFT _ va _ _ _, NTOr ta f1 f2 _ n2) ->
-              U.LEFT ta va f1 f2 (mkUType n2)
-            (STOr _ _, U.RIGHT _ va _ _ _, NTOr ta f1 f2 n1 _) ->
-              U.RIGHT ta va f1 f2 (mkUType n1)
-            (STList _, U.NIL _ va _, NTList ta n) -> U.NIL ta va (mkUType n)
-            (STSet _, U.EMPTY_SET _ va _, NTSet ta1 n) ->
-              U.EMPTY_SET ta1 va (mkUType n)
-            (STMap _ _, U.EMPTY_MAP _ va _ _, NTMap ta1 k n) ->
-              U.EMPTY_MAP ta1 va (mkUType k) (mkUType n)
-            (STBigMap _ _, U.EMPTY_BIG_MAP _ va _ _, NTBigMap ta1 k n) ->
-              U.EMPTY_BIG_MAP ta1 va (mkUType k) (mkUType n)
-            (STLambda _ _, U.LAMBDA va _ _ ops, NTLambda _ n1 n2) ->
-              U.LAMBDA va (mkUType n1) (mkUType n2) ops
-            (_, U.CAST va _, n) -> U.CAST va (mkUType n)
-            (STOption _, U.UNPACK _ va _, NTOption ta nt) -> U.UNPACK ta va (mkUType nt)
-            (STOption (STContract _), U.CONTRACT va fa _, NTOption _ (NTContract _ nt)) ->
-              U.CONTRACT va fa (mkUType nt)
-            (_, U.CONTRACT va fa t, NTOption _ _) -> U.CONTRACT va fa t
-            (_, a@(U.APPLY {}), _) -> a
-            (_, a@(U.CHAIN_ID {}), _) -> a
-            (_, a@(U.EXT _), _) -> a
-            (_, a@(U.DROP), _) -> a
-            (_, a@(U.DROPN _), _) -> a
-            (_, a@(U.DUP _), _) -> a
-            (_, a@(U.SWAP), _) -> a
-            (_, a@(U.DIG {}), _) -> a
-            (_, a@(U.DUG {}), _) -> a
-            (_, a@(U.IF_NONE _ _), _) -> a
-            (_, a@(U.CONS _), _) -> a
-            (_, a@(U.IF_LEFT _ _), _) -> a
-            (_, a@(U.IF_CONS _ _), _) -> a
-            (_, a@(U.SIZE _), _) -> a
-            (_, a@(U.MAP _ _), _) -> a
-            (_, a@(U.ITER _), _) -> a
-            (_, a@(U.MEM _), _) -> a
-            (_, a@(U.GET _), _) -> a
-            (_, a@(U.UPDATE _), _) -> a
-            (_, a@(U.IF _ _), _) -> a
-            (_, a@(U.LOOP _), _) -> a
-            (_, a@(U.LOOP_LEFT _), _) -> a
-            (_, a@(U.EXEC _), _) -> a
-            (_, a@(U.DIP _), _) -> a
-            (_, a@(U.DIPN {}), _) -> a
-            (_, a@(U.FAILWITH), _) -> a
-            (_, a@(U.RENAME _), _) -> a
-            (_, a@(U.PACK _), _) -> a
-            (_, a@(U.CONCAT _), _) -> a
-            (_, a@(U.SLICE _), _) -> a
-            (_, a@(U.ISNAT _), _) -> a
-            (_, a@(U.ADD _), _) -> a
-            (_, a@(U.SUB _), _) -> a
-            (_, a@(U.MUL _), _) -> a
-            (_, a@(U.EDIV _), _) -> a
-            (_, a@(U.ABS _), _) -> a
-            (_, a@(U.NEG _), _) -> a
-            (_, a@(U.LSL _), _) -> a
-            (_, a@(U.LSR _), _) -> a
-            (_, a@(U.OR _), _) -> a
-            (_, a@(U.AND _), _) -> a
-            (_, a@(U.XOR _), _) -> a
-            (_, a@(U.NOT _), _) -> a
-            (_, a@(U.COMPARE _), _) -> a
-            (_, a@(U.EQ _), _) -> a
-            (_, a@(U.NEQ _), _) -> a
-            (_, a@(U.LT _), _) -> a
-            (_, a@(U.GT _), _) -> a
-            (_, a@(U.LE _), _) -> a
-            (_, a@(U.GE _), _) -> a
-            (_, a@(U.INT _), _) -> a
-            (_, a@(U.SELF _ _), _) -> a
-            (_, a@(U.TRANSFER_TOKENS _), _) -> a
-            (_, a@(U.SET_DELEGATE _), _) -> a
-            (_, a@(U.CREATE_CONTRACT {}), _) -> a
-            (_, a@(U.IMPLICIT_ACCOUNT _), _) -> a
-            (_, a@(U.NOW _), _) -> a
-            (_, a@(U.AMOUNT _), _) -> a
-            (_, a@(U.BALANCE _), _) -> a
-            (_, a@(U.CHECK_SIGNATURE _), _) -> a
-            (_, a@(U.SHA256 _), _) -> a
-            (_, a@(U.SHA512 _), _) -> a
-            (_, a@(U.BLAKE2B _), _) -> a
-            (_, a@(U.HASH_KEY _), _) -> a
-            (_, a@(U.SOURCE _), _) -> a
-            (_, a@(U.SENDER _), _) -> a
-            (_, a@(U.ADDRESS _), _) -> a
-            (_, b, c) -> error $ "addInstrNote: Unexpected instruction/annotation combination: " <> show (b, c)
 
+    addInstrNote
+      :: forall t. (SingI t, HasCallStack)
+      => U.ExpandedInstr -> Notes t -> U.ExpandedInstr
+    addInstrNote ins nte = case (sing @t, ins, nte) of
+        (_, U.PUSH va _ v, _) -> U.PUSH va (mkUType nte) v
+        (_, U.SOME _ va, NTOption ta _) -> U.SOME ta va
+        (STOption _, U.NONE _ va _, NTOption ta nt) -> U.NONE ta va (mkUType nt)
+        (_, U.UNIT _ va, NTUnit ta) -> U.UNIT ta va
+        (_, U.PAIR ta va f1 f2, _) -> U.PAIR ta va f1 f2
+        (_, U.CAR va f1, _) -> U.CAR va f1
+        (_, U.CDR va f1, _) -> U.CDR va f1
+        (STOr _ _, U.LEFT _ va _ _ _, NTOr ta f1 f2 _ n2) ->
+          U.LEFT ta va f1 f2 (mkUType n2)
+        (STOr _ _, U.RIGHT _ va _ _ _, NTOr ta f1 f2 n1 _) ->
+          U.RIGHT ta va f1 f2 (mkUType n1)
+        (STList _, U.NIL _ va _, NTList ta n) -> U.NIL ta va (mkUType n)
+        (STSet _, U.EMPTY_SET _ va _, NTSet ta1 n) ->
+          U.EMPTY_SET ta1 va (mkUType n)
+        (STMap _ _, U.EMPTY_MAP _ va _ _, NTMap ta1 k n) ->
+          U.EMPTY_MAP ta1 va (mkUType k) (mkUType n)
+        (STBigMap _ _, U.EMPTY_BIG_MAP _ va _ _, NTBigMap ta1 k n) ->
+          U.EMPTY_BIG_MAP ta1 va (mkUType k) (mkUType n)
+        (STLambda _ _, U.LAMBDA va _ _ ops, NTLambda _ n1 n2) ->
+          U.LAMBDA va (mkUType n1) (mkUType n2) ops
+        (_, U.CAST va _, n) -> U.CAST va (mkUType n)
+        (STOption _, U.UNPACK _ va _, NTOption ta nt) -> U.UNPACK ta va (mkUType nt)
+        (STOption (STContract _), U.CONTRACT va fa _, NTOption _ (NTContract _ nt)) ->
+          U.CONTRACT va fa (mkUType nt)
+        (_, U.CONTRACT va fa t, NTOption _ _) -> U.CONTRACT va fa t
+        (_, a@(U.APPLY {}), _) -> a
+        (_, a@(U.CHAIN_ID {}), _) -> a
+        (_, a@(U.EXT _), _) -> a
+        (_, a@(U.DROP), _) -> a
+        (_, a@(U.DROPN _), _) -> a
+        (_, a@(U.DUP _), _) -> a
+        (_, a@(U.SWAP), _) -> a
+        (_, a@(U.DIG {}), _) -> a
+        (_, a@(U.DUG {}), _) -> a
+        (_, a@(U.IF_NONE _ _), _) -> a
+        (_, a@(U.CONS _), _) -> a
+        (_, a@(U.IF_LEFT _ _), _) -> a
+        (_, a@(U.IF_CONS _ _), _) -> a
+        (_, a@(U.SIZE _), _) -> a
+        (_, a@(U.MAP _ _), _) -> a
+        (_, a@(U.ITER _), _) -> a
+        (_, a@(U.MEM _), _) -> a
+        (_, a@(U.GET _), _) -> a
+        (_, a@(U.UPDATE _), _) -> a
+        (_, a@(U.IF _ _), _) -> a
+        (_, a@(U.LOOP _), _) -> a
+        (_, a@(U.LOOP_LEFT _), _) -> a
+        (_, a@(U.EXEC _), _) -> a
+        (_, a@(U.DIP _), _) -> a
+        (_, a@(U.DIPN {}), _) -> a
+        (_, a@(U.FAILWITH), _) -> a
+        (_, a@(U.RENAME _), _) -> a
+        (_, a@(U.PACK _), _) -> a
+        (_, a@(U.CONCAT _), _) -> a
+        (_, a@(U.SLICE _), _) -> a
+        (_, a@(U.ISNAT _), _) -> a
+        (_, a@(U.ADD _), _) -> a
+        (_, a@(U.SUB _), _) -> a
+        (_, a@(U.MUL _), _) -> a
+        (_, a@(U.EDIV _), _) -> a
+        (_, a@(U.ABS _), _) -> a
+        (_, a@(U.NEG _), _) -> a
+        (_, a@(U.LSL _), _) -> a
+        (_, a@(U.LSR _), _) -> a
+        (_, a@(U.OR _), _) -> a
+        (_, a@(U.AND _), _) -> a
+        (_, a@(U.XOR _), _) -> a
+        (_, a@(U.NOT _), _) -> a
+        (_, a@(U.COMPARE _), _) -> a
+        (_, a@(U.EQ _), _) -> a
+        (_, a@(U.NEQ _), _) -> a
+        (_, a@(U.LT _), _) -> a
+        (_, a@(U.GT _), _) -> a
+        (_, a@(U.LE _), _) -> a
+        (_, a@(U.GE _), _) -> a
+        (_, a@(U.INT _), _) -> a
+        (_, a@(U.SELF _ _), _) -> a
+        (_, a@(U.TRANSFER_TOKENS _), _) -> a
+        (_, a@(U.SET_DELEGATE _), _) -> a
+        (_, a@(U.CREATE_CONTRACT {}), _) -> a
+        (_, a@(U.IMPLICIT_ACCOUNT _), _) -> a
+        (_, a@(U.NOW _), _) -> a
+        (_, a@(U.AMOUNT _), _) -> a
+        (_, a@(U.BALANCE _), _) -> a
+        (_, a@(U.CHECK_SIGNATURE _), _) -> a
+        (_, a@(U.SHA256 _), _) -> a
+        (_, a@(U.SHA512 _), _) -> a
+        (_, a@(U.BLAKE2B _), _) -> a
+        (_, a@(U.HASH_KEY _), _) -> a
+        (_, a@(U.SOURCE _), _) -> a
+        (_, a@(U.SENDER _), _) -> a
+        (_, a@(U.ADDRESS _), _) -> a
+        (_, b, c) -> error $ "addInstrNote: Unexpected instruction/annotation combination: " <> show (b, c)
+
     handleInstrVarNotes :: forall inp' out' . HasCallStack
       => Instr inp' out' -> NonEmpty U.VarAnn -> U.ExpandedInstr
     handleInstrVarNotes ins' varAnns =
       let x = handleInstr ins' in addVarNotes x varAnns
-      where
-        addVarNotes
-          :: HasCallStack
-          => U.ExpandedInstr -> NonEmpty U.VarAnn -> U.ExpandedInstr
-        addVarNotes ins varNotes = case varNotes of
-          va1 :| [va2] -> case ins of
-            U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va1 va2 c
-            _ -> error $
-              "addVarNotes: Cannot add two var annotations to instr: " <> show ins
-          va :| [] -> case ins of
-            U.DUP _ -> U.DUP va
-            U.PUSH _ t v -> U.PUSH va t v
-            U.SOME ta _ -> U.SOME ta va
-            U.NONE ta _ t -> U.NONE ta va t
-            U.UNIT ta _ -> U.UNIT ta va
-            U.PAIR ta _ fa1 fa2 -> U.PAIR ta va fa1 fa2
-            U.CAR _ fa -> U.CAR va fa
-            U.CDR _ fa -> U.CDR va fa
-            U.LEFT ta _ fa1 fa2 t -> U.LEFT ta va fa1 fa2 t
-            U.RIGHT ta _ fa1 fa2 t -> U.RIGHT ta va fa1 fa2 t
-            U.NIL ta _ t -> U.NIL ta va t
-            U.CONS _ -> U.CONS va
-            U.SIZE _ -> U.SIZE va
-            U.EMPTY_SET ta _ c -> U.EMPTY_SET ta va c
-            U.EMPTY_MAP ta _ c t -> U.EMPTY_MAP ta va c t
-            U.EMPTY_BIG_MAP ta _ c t -> U.EMPTY_BIG_MAP ta va c t
-            U.MAP _ ops -> U.MAP va ops
-            U.MEM _ -> U.MEM va
-            U.GET _ -> U.GET va
-            U.UPDATE _ -> U.UPDATE va
-            U.LAMBDA _ t1 t2 ops -> U.LAMBDA va t1 t2 ops
-            U.EXEC _ -> U.EXEC va
-            U.APPLY _ -> U.APPLY va
-            U.CAST _ t -> U.CAST va t
-            U.RENAME _ -> U.RENAME va
-            U.PACK _ -> U.PACK va
-            U.UNPACK ta _ t -> U.UNPACK ta va t
-            U.CONCAT _ -> U.CONCAT va
-            U.SLICE _ -> U.SLICE va
-            U.ISNAT _ -> U.ISNAT va
-            U.ADD _ -> U.ADD va
-            U.SUB _ -> U.SUB va
-            U.MUL _ -> U.MUL va
-            U.EDIV _ -> U.EDIV va
-            U.ABS _ -> U.ABS va
-            U.NEG _ -> U.NEG va
-            U.LSL _ -> U.LSL va
-            U.LSR _ -> U.LSR va
-            U.OR _ -> U.OR va
-            U.AND _ -> U.AND va
-            U.XOR _ -> U.XOR va
-            U.NOT _ -> U.NOT va
-            U.COMPARE _ -> U.COMPARE va
-            U.EQ _ -> U.EQ va
-            U.NEQ _ -> U.NEQ va
-            U.LT _ -> U.LT va
-            U.GT _ -> U.GT va
-            U.LE _ -> U.LE va
-            U.GE _ -> U.GE va
-            U.INT _ -> U.INT va
-            U.SELF _ fa -> U.SELF va fa
-            U.CONTRACT _ fa t -> U.CONTRACT va fa t
-            U.TRANSFER_TOKENS _ -> U.TRANSFER_TOKENS va
-            U.SET_DELEGATE _ -> U.SET_DELEGATE va
-            U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va U.noAnn c
-            U.IMPLICIT_ACCOUNT _ -> U.IMPLICIT_ACCOUNT va
-            U.NOW _ -> U.NOW va
-            U.AMOUNT _ -> U.AMOUNT va
-            U.BALANCE _ -> U.BALANCE va
-            U.CHECK_SIGNATURE _ -> U.CHECK_SIGNATURE va
-            U.SHA256 _ -> U.SHA256 va
-            U.SHA512 _ -> U.SHA512 va
-            U.BLAKE2B _ -> U.BLAKE2B va
-            U.HASH_KEY _ -> U.HASH_KEY va
-            U.SOURCE _ -> U.SOURCE va
-            U.SENDER _ -> U.SENDER va
-            U.ADDRESS _ -> U.ADDRESS va
-            U.CHAIN_ID _ -> U.CHAIN_ID va
-            _ -> error $
-              "addVarNotes: Cannot add single var annotation to instr: " <> (show ins)
-          _ -> error $
-            "addVarNotes: Trying to add more than two var annotations to instr: " <> (show ins)
+
+    addVarNotes
+      :: HasCallStack
+      => U.ExpandedInstr -> NonEmpty U.VarAnn -> U.ExpandedInstr
+    addVarNotes ins varNotes = case varNotes of
+      va1 :| [va2] -> case ins of
+        U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va1 va2 c
+        _ -> error $
+          "addVarNotes: Cannot add two var annotations to instr: " <> show ins
+      va :| [] -> case ins of
+        U.DUP _ -> U.DUP va
+        U.PUSH _ t v -> U.PUSH va t v
+        U.SOME ta _ -> U.SOME ta va
+        U.NONE ta _ t -> U.NONE ta va t
+        U.UNIT ta _ -> U.UNIT ta va
+        U.PAIR ta _ fa1 fa2 -> U.PAIR ta va fa1 fa2
+        U.CAR _ fa -> U.CAR va fa
+        U.CDR _ fa -> U.CDR va fa
+        U.LEFT ta _ fa1 fa2 t -> U.LEFT ta va fa1 fa2 t
+        U.RIGHT ta _ fa1 fa2 t -> U.RIGHT ta va fa1 fa2 t
+        U.NIL ta _ t -> U.NIL ta va t
+        U.CONS _ -> U.CONS va
+        U.SIZE _ -> U.SIZE va
+        U.EMPTY_SET ta _ c -> U.EMPTY_SET ta va c
+        U.EMPTY_MAP ta _ c t -> U.EMPTY_MAP ta va c t
+        U.EMPTY_BIG_MAP ta _ c t -> U.EMPTY_BIG_MAP ta va c t
+        U.MAP _ ops -> U.MAP va ops
+        U.MEM _ -> U.MEM va
+        U.GET _ -> U.GET va
+        U.UPDATE _ -> U.UPDATE va
+        U.LAMBDA _ t1 t2 ops -> U.LAMBDA va t1 t2 ops
+        U.EXEC _ -> U.EXEC va
+        U.APPLY _ -> U.APPLY va
+        U.CAST _ t -> U.CAST va t
+        U.RENAME _ -> U.RENAME va
+        U.PACK _ -> U.PACK va
+        U.UNPACK ta _ t -> U.UNPACK ta va t
+        U.CONCAT _ -> U.CONCAT va
+        U.SLICE _ -> U.SLICE va
+        U.ISNAT _ -> U.ISNAT va
+        U.ADD _ -> U.ADD va
+        U.SUB _ -> U.SUB va
+        U.MUL _ -> U.MUL va
+        U.EDIV _ -> U.EDIV va
+        U.ABS _ -> U.ABS va
+        U.NEG _ -> U.NEG va
+        U.LSL _ -> U.LSL va
+        U.LSR _ -> U.LSR va
+        U.OR _ -> U.OR va
+        U.AND _ -> U.AND va
+        U.XOR _ -> U.XOR va
+        U.NOT _ -> U.NOT va
+        U.COMPARE _ -> U.COMPARE va
+        U.EQ _ -> U.EQ va
+        U.NEQ _ -> U.NEQ va
+        U.LT _ -> U.LT va
+        U.GT _ -> U.GT va
+        U.LE _ -> U.LE va
+        U.GE _ -> U.GE va
+        U.INT _ -> U.INT va
+        U.SELF _ fa -> U.SELF va fa
+        U.CONTRACT _ fa t -> U.CONTRACT va fa t
+        U.TRANSFER_TOKENS _ -> U.TRANSFER_TOKENS va
+        U.SET_DELEGATE _ -> U.SET_DELEGATE va
+        U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va U.noAnn c
+        U.IMPLICIT_ACCOUNT _ -> U.IMPLICIT_ACCOUNT va
+        U.NOW _ -> U.NOW va
+        U.AMOUNT _ -> U.AMOUNT va
+        U.BALANCE _ -> U.BALANCE va
+        U.CHECK_SIGNATURE _ -> U.CHECK_SIGNATURE va
+        U.SHA256 _ -> U.SHA256 va
+        U.SHA512 _ -> U.SHA512 va
+        U.BLAKE2B _ -> U.BLAKE2B va
+        U.HASH_KEY _ -> U.HASH_KEY va
+        U.SOURCE _ -> U.SOURCE va
+        U.SENDER _ -> U.SENDER va
+        U.ADDRESS _ -> U.ADDRESS va
+        U.CHAIN_ID _ -> U.CHAIN_ID va
+        _ -> error $
+          "addVarNotes: Cannot add single var annotation to instr: " <> (show ins) <> " with " <> show va
+      _ -> error $
+        "addVarNotes: Trying to add more than two var annotations to instr: " <> (show ins)
 
     handleInstr :: Instr inp out -> U.ExpandedInstr
     handleInstr = \case
diff --git a/src/Michelson/Typed/Haskell/Doc.hs b/src/Michelson/Typed/Haskell/Doc.hs
--- a/src/Michelson/Typed/Haskell/Doc.hs
+++ b/src/Michelson/Typed/Haskell/Doc.hs
@@ -709,16 +709,24 @@
   typeDocHaskellRep _ _ = Nothing
 
 instance TypeHasDoc Address where
-  typeDocName _ = "Address (no entrypoint)"
-  typeDocMdDescription =
-    "This is similar to Michelson Address, but does not retain entrypoint name \
-    \if it refers to a contract."
+  typeDocName _ = "Address"
+  typeDocMdDescription = [md|
+    Address primitive.
+
+    Unlike Michelson's `address`, it is assumed not to contain an entrypoint name,
+    even if it refers to a contract; this won't be checked, so passing an entrypoint
+    name may result in unexpected errors.
+    |]
   typeDocDependencies _ = []
   typeDocHaskellRep _ _ = Nothing
 
 instance TypeHasDoc EpAddress where
-  typeDocName _ = "Address"
-  typeDocMdDescription = "Address primitive."
+  typeDocName _ = "EntrypointAddress"
+  typeDocMdDescription = [md|
+    Address primitive.
+
+    This exactly matches the Michelson's `address`, and can refer to a specific entrypoint.
+    |]
   typeDocDependencies _ = []
   typeDocHaskellRep _ _ = Nothing
 
@@ -731,6 +739,12 @@
 instance TypeHasDoc Signature where
   typeDocName _ = "Signature"
   typeDocMdDescription = "Signature primitive."
+  typeDocDependencies _ = []
+  typeDocHaskellRep _ _ = Nothing
+
+instance TypeHasDoc ChainId where
+  typeDocName _ = "ChainId"
+  typeDocMdDescription = "Identifier of the current chain."
   typeDocDependencies _ = []
   typeDocHaskellRep _ _ = Nothing
 
diff --git a/src/Michelson/Typed/Instr.hs b/src/Michelson/Typed/Instr.hs
--- a/src/Michelson/Typed/Instr.hs
+++ b/src/Michelson/Typed/Instr.hs
@@ -128,8 +128,8 @@
   -- top type on the result stack.
   --
   -- As of now, when converting from untyped representation,
-  -- we only preserve field annotations and type annotations.
-  -- Variable annotations are not preserved.
+  -- we only preserve field annotations and type annotations in @PackedNotes@.
+  -- Variable annotations are preserved in @InstrWithVarNotes@.
   --
   -- This can wrap only instructions with at least one non-failing execution
   -- branch.
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
@@ -16,9 +16,11 @@
 import Fmt (Buildable(..), pretty)
 
 import Michelson.Interpret.Pack (encodeValue', packCode', packNotedT', packT')
-import Michelson.Interpret.Unpack (UnpackError, decodeContract, unpackInstr', unpackValue')
+import Michelson.Interpret.Unpack
+  (UnpackError, decodeContract, decodeType, unpackInstr', unpackValue')
 import Michelson.Typed
-  (Contract(..), HasNoOp, Instr(..), Notes(..), T(..), Value, pnNotes, pnRootAnn)
+  (Contract(..), HasNoOp, Instr(..), KnownT, Notes(..), T(..), Value, Value'(..), fromUType,
+  pattern AsUType, pnNotes, pnRootAnn, rfAnyInstr)
 import Michelson.Typed.Instr (mapEntriesOrdered)
 import Michelson.Typed.Scope (UnpackedValScope)
 import qualified Michelson.Untyped as Untyped
@@ -44,6 +46,9 @@
 instance SingI t => ToExpression (Notes t) where
   toExpression = decodeExpression . packNotedT'
 
+instance ToExpression Untyped.Type where
+  toExpression (AsUType notes) = toExpression notes
+
 instance (SingI t, HasNoOp t) => ToExpression (Value t) where
   toExpression = decodeExpression . encodeValue'
 
@@ -108,3 +113,21 @@
   fromExpression =
     first FromExpressionError . launchGet decodeContract .
     LBS.fromStrict . encodeExpression
+
+instance FromExpression Untyped.Type where
+  fromExpression =
+    first FromExpressionError .
+    launchGet decodeType .
+    LBS.fromStrict .
+    encodeExpression
+
+instance FromExpression T where
+  fromExpression =
+    second fromUType . fromExpression @Untyped.Type
+
+-- Note: we should generalize this to work for any instruction,
+-- not just lambdas (i.e. instructions with one input and one output).
+instance (KnownT inp, KnownT out) => FromExpression (Instr '[inp] '[out]) where
+  fromExpression expr =
+    fromExpression @(Value ('TLambda inp out)) expr <&> \case
+      VLam instr -> rfAnyInstr instr
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
@@ -17,10 +17,9 @@
   ) where
 
 import Data.Aeson
-  (FromJSON, ToJSON, parseJSON, toEncoding, toJSON, withObject, withText, (.!=), (.:), (.:?))
-import Data.Aeson.Casing (aesonPrefix, snakeCase)
+  (FromJSON, ToJSON, object, parseJSON, toEncoding, toJSON, withObject, withText, (.!=), (.:),
+  (.:?), (.=))
 import qualified Data.Aeson.Encoding.Internal as Aeson
-import Data.Aeson.TH (deriveToJSON)
 import qualified Data.Aeson.Types as Aeson
 import qualified Data.HashMap.Strict as HashMap
 import qualified Data.Sequence as Seq
@@ -106,6 +105,13 @@
     <*> v .:? "args" .!= mempty
     <*> v .:? "annots" .!= mempty
 
+instance ToJSON MichelinePrimAp where
+  toJSON MichelinePrimAp {..} = object $ catMaybes
+    [ Just ("prim" .= mpaPrim)
+    , if mpaArgs == mempty then Nothing else Just ("args" .= mpaArgs)
+    , if mpaAnnots == mempty then Nothing else Just ("annots" .= mpaAnnots)
+    ]
+
 annotFromText :: MonadFail m => Text -> m Annotation
 annotFromText txt = case result of
     Just a -> pure a
@@ -155,5 +161,3 @@
   toEncoding (ExpressionString x) = Aeson.pairs (Aeson.pair "string" (toEncoding x))
   toEncoding (ExpressionInt x) = Aeson.pairs (Aeson.pair "int" (toEncoding $ StringEncode x))
   toEncoding (ExpressionBytes x) = Aeson.pairs (Aeson.pair "bytes" (toEncoding $ HexJSONByteString x))
-
-deriveToJSON (aesonPrefix snakeCase) ''MichelinePrimAp
diff --git a/src/Morley/Micheline/Json.hs b/src/Morley/Micheline/Json.hs
--- a/src/Morley/Micheline/Json.hs
+++ b/src/Morley/Micheline/Json.hs
@@ -9,7 +9,7 @@
   ( StringEncode (..)
   , TezosBigNum
   , TezosInt64
-  , parseMutezJson
+  , TezosMutez (..)
   ) where
 
 import Data.Aeson (FromJSON, ToJSON, parseJSON, toEncoding, toJSON)
@@ -54,6 +54,10 @@
   toJSON (StringEncode x) = Aeson.String $ show x
   toEncoding (StringEncode x) = AE.int64Text x
 
-parseMutezJson :: TezosInt64 -> Aeson.Parser Mutez
-parseMutezJson (StringEncode i) =
-  either (fail . toString) pure $ mkMutez' i
+newtype TezosMutez = TezosMutez { unTezosMutez :: Mutez }
+  deriving stock (Show)
+
+instance FromJSON TezosMutez where
+  parseJSON v = do
+    StringEncode i <- parseStringEncodedIntegral @Int64 v
+    either (fail . toString) (pure . TezosMutez) $ mkMutez' i
diff --git a/src/Tezos/Core.hs b/src/Tezos/Core.hs
--- a/src/Tezos/Core.hs
+++ b/src/Tezos/Core.hs
@@ -21,6 +21,7 @@
   , divModMutezInt
   , zeroMutez
   , oneMutez
+  , prettyTez
 
     -- * Timestamp
   , Timestamp (..)
@@ -51,6 +52,7 @@
 import qualified Data.Aeson as Aeson
 import Data.Aeson.TH (deriveJSON)
 import Data.Data (Data(..))
+import Data.Scientific
 import qualified Data.Text as T
 import Data.Time.Clock (UTCTime)
 import Data.Time.Clock.POSIX (POSIXTime, getPOSIXTime, posixSecondsToUTCTime, utcTimeToPOSIXSeconds)
@@ -179,6 +181,18 @@
 
 oneMutez :: Mutez
 oneMutez = Mutez 1
+
+-- |
+-- >>> prettyTez (toMutez 420)
+-- "0.00042 ꜩ"
+-- >>> prettyTez (toMutez 42000000)
+-- "42 ꜩ"
+prettyTez :: Mutez -> Text
+prettyTez ((/ 1000000) . fromIntegral . unMutez -> s) =
+  case floatingOrInteger s of
+    Left (_ :: Float)    -> toText $ formatScientific Fixed Nothing s
+    Right (n :: Integer) -> pretty n
+  <> " ꜩ"
 
 ----------------------------------------------------------------------------
 -- Timestamp
diff --git a/src/Tezos/Crypto.hs b/src/Tezos/Crypto.hs
--- a/src/Tezos/Crypto.hs
+++ b/src/Tezos/Crypto.hs
@@ -50,6 +50,7 @@
   , parseSignatureRaw
   , signatureLengthBytes
   , checkSignature
+  , sign
 
   -- * Formatting
   , CryptoParseError (..)
@@ -84,6 +85,7 @@
   , keyHashDecoders
   ) where
 
+import Crypto.Random (MonadRandom)
 import Data.Aeson (FromJSON(..), ToJSON(..))
 import qualified Data.Aeson as Aeson
 import qualified Data.Aeson.Encoding as Aeson
@@ -281,6 +283,13 @@
         & fmap (\sig -> P256.checkSignature pk sig bytes)
         & fromRight False
     _ -> False
+
+sign :: MonadRandom m => SecretKey -> ByteString -> m Signature
+sign sk bs =
+  case sk of
+    SecretKeyEd25519 sk'   -> pure $ SignatureEd25519 $ Ed25519.sign sk' bs
+    SecretKeySecp256k1 sk' -> SignatureSecp256k1 <$> Secp256k1.sign sk' bs
+    SecretKeyP256 sk'      -> SignatureP256 <$> P256.sign sk' bs
 
 ----------------------------------------------------------------------------
 -- Formatting
diff --git a/src/Util/CLI.hs b/src/Util/CLI.hs
--- a/src/Util/CLI.hs
+++ b/src/Util/CLI.hs
@@ -28,6 +28,7 @@
   ) where
 
 import qualified Data.Kind as Kind
+import Data.Text.Manipulate (toSpinal)
 import Fmt (Buildable, pretty)
 import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
 import Named (Name(..), arg)
@@ -162,6 +163,9 @@
     mods
 
 -- | Create a 'Opt.Parser' for a value using its type-level name.
+--
+-- This expects type-level name to be in camelCase as appropriate for Haskell
+-- and transforms the variable inside.
 namedParser ::
      forall (a :: Kind.Type) (name :: Symbol).
      (Buildable a, HasCLReader a, KnownSymbol name)
@@ -171,7 +175,7 @@
 namedParser defValue hInfo =
   option ((Name @name) <.!> getReader) $
     mconcat
-    [ long name
+    [ long (toString . toSpinal . toText $ name)
     , metavar (getMetavar @a)
     , help hInfo
     , maybeAddDefault pretty (Name @name <.!> defValue)
diff --git a/src/Util/Exception.hs b/src/Util/Exception.hs
--- a/src/Util/Exception.hs
+++ b/src/Util/Exception.hs
@@ -5,20 +5,8 @@
 module Util.Exception
   ( -- * General simple helpers
     throwLeft
-
-  , -- * Common exceptions
-    TextException (..)
-
-    -- * Better printing of exceptions
-  , DisplayExceptionInShow(..)
-  , displayUncaughtException
   ) where
 
-import Control.Exception (throwIO)
-import Fmt (Buildable(..), pretty)
-import System.Exit (ExitCode(..))
-import qualified Text.Show
-
 -- | If monadic action returns a 'Left' value, it will be
 -- thrown. Otherwise the returned value will be returned as is.
 throwLeft :: (MonadThrow m, Exception e) => m (Either e a) -> m a
@@ -26,54 +14,3 @@
   (>>= \case
       Left e -> throwM e
       Right x -> return x)
-
-----------------------------------------------------------------------------
--- Common exceptions
-----------------------------------------------------------------------------
-
-data TextException = TextException Text
-instance Exception TextException
-
-instance Buildable TextException where
-  build (TextException desc) = build desc
-
-instance Show TextException where
-  show = pretty
-
-----------------------------------------------------------------------------
--- Better printing of exceptions at executable-level
-----------------------------------------------------------------------------
-
-newtype DisplayExceptionInShow = DisplayExceptionInShow { unDisplayExceptionInShow :: SomeException }
-
-instance Show DisplayExceptionInShow where
-  show (DisplayExceptionInShow se) = displayException se
-
-instance Exception DisplayExceptionInShow
-
--- | Customise default uncaught exception handling. The problem with
--- the default handler is that it uses `show` to display uncaught
--- exceptions, but `displayException` may provide more reasonable
--- output. We do not modify uncaught exception handler, but simply
--- wrap uncaught exceptions (only synchronous ones) into
--- 'DisplayExceptionInShow'.
---
--- Some exceptions (currently we are aware only of 'ExitCode') are
--- handled specially by default exception handler, so we don't wrap
--- them.
-displayUncaughtException :: IO () -> IO ()
-displayUncaughtException = mapIOExceptions wrapUnlessExitCode
-  where
-    -- We can't use `mapException` here, because it only works with
-    -- exceptions inside pure values, not with `IO` exceptions.
-    -- Note: it doesn't catch async exceptions.
-    mapIOExceptions :: (SomeException -> SomeException) -> IO a -> IO a
-    mapIOExceptions f action = action `catchAny` (throwIO . f)
-
-    -- We don't wrap `ExitCode` because it seems to be handled specially.
-    -- Application exit code depends on the value stored in `ExitCode`.
-    wrapUnlessExitCode :: SomeException -> SomeException
-    wrapUnlessExitCode e =
-      case fromException @ExitCode e of
-        Just _ -> e
-        Nothing -> toException $ DisplayExceptionInShow e
diff --git a/src/Util/Main.hs b/src/Util/Main.hs
new file mode 100644
--- /dev/null
+++ b/src/Util/Main.hs
@@ -0,0 +1,25 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | Functions supposed to be used in the @Main@ module.
+
+module Util.Main
+  ( wrapMain
+  ) where
+
+import Control.Exception.Uncaught (withDisplayExceptionHandler)
+import Main.Utf8 (withUtf8)
+
+-- | Some defaults in Haskell are debatable and we typically want
+-- to customize them in our applications.
+-- Some customizations are done at the level of @main@.
+-- Currently we have two of them:
+--
+-- 1. 'withUtf8' from the @with-utf8@ package.
+-- 2. 'withDisplayExceptionHandler' from the @uncaught-exception@ package.
+--
+-- This function is supposed to apply all @main@ customizations that we
+-- typcally want to do.
+wrapMain :: IO () -> IO ()
+wrapMain = withUtf8 . withDisplayExceptionHandler
diff --git a/src/Util/Markdown.hs b/src/Util/Markdown.hs
--- a/src/Util/Markdown.hs
+++ b/src/Util/Markdown.hs
@@ -26,6 +26,7 @@
   , md
   ) where
 
+import Data.Char (isAscii)
 import qualified Data.String.Interpolate.IsString as Interpolate
 import Data.String.Interpolate.Util (unindent)
 import Fmt (Builder, build, (+|), (|+))
@@ -49,6 +50,10 @@
   fromString = Anchor . fromString . ("manual-" <>)
 
 -- | Picking anchor for various things.
+--
+-- What you want here is potentially adding some prefix to ensure anchors uniqueness.
+-- It is not necessary to preprocess the text to fit anchor format - that will happen
+-- when the anchor is embedded into 'Markdown'.
 class ToAnchor anchor where
   toAnchor :: anchor -> Anchor
 
@@ -88,18 +93,22 @@
 mdEscapeAnchorS :: String -> Markdown
 mdEscapeAnchorS = \case
   [] -> ""
-  ' ' : s -> "-" <> mdEscapeAnchorS s
-  '(' : s -> "lparen" <> mdEscapeAnchorS s
-  ')' : s -> "rparen" <> mdEscapeAnchorS s
-  '[' : s -> "lbracket" <> mdEscapeAnchorS s
-  ']' : s -> "rbracket" <> mdEscapeAnchorS s
-  '{' : s -> "lbrace" <> mdEscapeAnchorS s
-  '}' : s -> "rbrace" <> mdEscapeAnchorS s
-  ',' : s -> "comma" <> mdEscapeAnchorS s
-  ';' : s -> "semicolon" <> mdEscapeAnchorS s
-  ':' : s -> "colon" <> mdEscapeAnchorS s
-  '#' : s -> "hash" <> mdEscapeAnchorS s
-  c : s -> build (toText [c]) <> mdEscapeAnchorS s
+  c : s -> escapeChar c <> mdEscapeAnchorS s
+  where
+    escapeChar = \case
+      ' ' -> "-"
+      '(' -> "lparen"
+      ')' -> "rparen"
+      '[' -> "lbracket"
+      ']' -> "rbracket"
+      '{' -> "lbrace"
+      '}' -> "rbrace"
+      ',' -> "comma"
+      ';' -> "semicolon"
+      ':' -> "colon"
+      '#' -> "hash"
+      c | not (isAscii c) -> "c" <> build (fromEnum c)
+        | otherwise -> build [c]
 
 -- | Turn text into valid anchor. Human-readability is not preserved.
 mdEscapeAnchor :: ToAnchor anchor => anchor -> Markdown