diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,32 @@
 Unreleased
 ==========
+<!-- Append new entries here -->
+
+0.2.0
+=====
+* [!346](https://gitlab.com/morley-framework/morley/-/merge_requests/346)
+  Added `docStorage` and `contractGeneralDefault`.
+* [!306](https://gitlab.com/morley-framework/morley/-/merge_requests/306)
+  Deprecated `mapMigrationCode` in favor of `MapLorentzInstr`.
+* [!326](https://gitlab.com/morley-framework/morley/-/merge_requests/326)
+Updated contract registry (`Lorentz.ContractRegistry`):
+  + Now it can print initial storage apart from contract and documentation.
+  + Some extra fields were added to `ContractInfo`.
+  + Logic is captured in the `runContractRegistry` function.
+  + If you don't specify output file, we will use a file with name constructed from contract name. Pass `-` if you want `stdout`.
+* [!245](https://gitlab.com/morley-framework/morley/-/merge_requests/245) Added `HasTypeAnn` instance for `FutureContract arg`.
+* [!294](https://gitlab.com/morley-framework/morley/-/merge_requests/294)
+  + Added `Paths_*` modules to `autogen-modules` in cabal files.  Removed `-O0`
+  + from default GHC options. Please set `ghc-options` in your `stack.yaml` or
+  `cabal.project.local`.
+* [!271](https://gitlab.com/morley-framework/morley/merge_requests/271) Renamed
+  'Contract' to 'ContractCode', and appended "Code" to the names of two functions:
+  'convertContract' and 'printTypedContract'
+* [!267](https://gitlab.com/morley-framework/morley/-/merge_requests/267)
+  + Retain type annotations in entrypoints derivation.
+  + Remove overlappable `HasTypeAnn` instance defined for nearly each type.
+    Add `default` `getTypeAnn` method definition instead and manually define `HasTypeAnn` instance for each type instead (trivially).
+    When you create a new data type with `IsoValue` instance, you usually have to derive `HasTypeAnn` as well.
 
 0.1.0
 =====
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,12 +1,208 @@
 # Morley Lorentz EDSL
 
+## Table of contents
+
+* [Overview](#overview)
+* [Writing contracts in Lorentz](#writing-contracts-in-lorentz)
+* [Lorentz contract example](#lorentz-example)
+* [FAQ](#faq)
+
+## Overview
+
 Lorentz is a powerful meta-programming tool which allows one to write Michelson contracts directly in Haskell.
 
 Haskell's type checker and automatic type inference facilitate contracts implementation and reduce boilerplate related to types.
 Adoption of Algebraic Data Types makes work with complex objects safe and convenient.
-Later Lorentz contract can be dumped as a plain textual Michelson contract using functions from [`Michelson.Printer`](/src/Michelson/Printer.hs).
+Later Lorentz contract can be dumped as a plain textual Michelson contract using functions from [`Michelson.Printer`](../morley/src/Michelson/Printer.hs).
 
+As an addition, you can optimize the transpiled Michelson contract before printing
+using functions from [`Michelson.Optimizer`](../morley/src/Michelson/Optimizer.hs).
+E.g. this optimizer will replace `IF {} {}` with `DROP`. For more possible optimizations
+please refer to the module mentioned earlier.
+
 You can find Lorentz instructions in [`Lorentz`](src/Lorentz.hs) modules.
 
-Examples of using Lorentz eDSL reside in the [`morley-ledgers`](/morley-ledgers) package.
-For more information, refer to that package's [README](/morley-ledgers/README.md).
+Examples of using Lorentz eDSL reside in the [`morley-ledgers`](../morley-ledgers) package.
+For more information, refer to that package's [README](/code/morley-ledgers/README.md).
+
+Also, to get more information about Lorentz you can read our [blogpost](https://serokell.io/blog/lorentz-implementing-smart-contract-edsl-in-haskell).
+
+## Writing contracts in Lorentz
+
+Basically, Lorentz function is just the haskell function that transforms one
+stack to another, this can be presented as the following operator:
+```haskell
+(inp :: [Kind.Type]) :-> (out :: [Kind.Type])
+```
+
+In order to list types on the stack, we will use `&` operator:
+```haskell
+(a :: Kind.Type) & (b :: [Kind.Type]) = a ': b
+```
+For example, `Natural & Integer & Bool & '[]`.
+
+Such design provides a nice code decomposition ability.
+
+Contract code in Lorentz is Lorentz function with specific type:
+```haskell
+type ContractOut storage = '[([Operation], storage)]
+type ContractCode parameter storage = '[(parameter, storage)] :-> ContractOut storage
+```
+
+Lorentz reimplements all existing [instructions](./src/Lorentz/Instr.hs) and
+[macros](./src/Lorentz/Macro.hs) from Michelson.
+
+Apart from reimplementing existing Michelson functionality, Lorentz provides bunch of
+additional features:
+
+* Pattern-matching on ADTs.
+```haskell
+data TrafficLight
+  = Red
+  | Yellow
+  | Green
+  deriving stock Generic
+  deriving anyclass IsoValue
+
+showTrafficLight :: TrafficLight & s :-> MText & s
+showTrafficLight = caseT
+  ( #cRed /-> push [mt|Red|]
+  , #cYellow /-> push [mt|Yellow|]
+  , #cGreen /-> push [mt|Green|]
+  )
+```
+* `RebindableSyntax` for Lorentz instructions, including `do` notation and `if` operator
+
+```haskell
+sumIsGt10 :: Integer & Integer & s :-> Bool & s
+sumIsGt10 = do
+  add
+  dip $ push @Integer 10
+  gt
+
+foo :: Integer & s :-> Integer & s
+foo = do
+  dup
+  sumIsGt10
+  if Holds
+  then do push @Integer 1
+  else do push @Integer -1
+```
+* Records with getters.
+
+```haskell
+data UserInfo = UserInfo
+  { firstName :: MText
+  , secondName :: MText
+  , userId :: Natural
+  } deriving stock Generic
+    deriving anyclass IsoValue
+
+getFullName :: UserInfo & s :-> MText & s
+getFullName = do
+  getField #firstName
+  dip $ toField #secondName
+  concat
+```
+
+* Automatic contracts documentation generation.
+
+  Lorentz provides primitives for embedding documentation in the contract code and
+  functions to produce documentation in Markdown, they can be found in
+  [`Lorentz.Doc`](./src/Lorentz/Doc.hs) and [`Michelson.Doc`](../morley/src/Michelson/Doc.hs) modules.
+  Documentation examples can be found [here](https://gitlab.com/morley-framework/morley/-/tree/autodoc/master/morley-ledgers/autodoc)
+  and [here](https://gitlab.com/morley-framework/morley/-/tree/autodoc/master/morley-multisig/autodoc).
+
+<a name="lorentz-example"></a>
+## Sample smart contract written in Lorentz
+
+Example contract with autodoc:
+```haskell
+data MeasurementMethod
+  = ParrotStep
+  | MonkeyStep
+  | ElephantStep
+  deriving stock Generic
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+
+instance TypeHasDoc MeasurementMethod where
+  typeDocName _ = "MeasurmentMethod"
+  typeDocMdDescription =
+    "This type defines the way of measuring boa length. \
+    \Single boa constrictor corresponds to 38 parrot steps, 31 monkey step \
+    \and 9 elephant steps."
+
+data Parameter
+  = MeasureBoaConstrictor ("method" :! MeasurementMethod)
+  | Zero ()
+  deriving stock Generic
+  deriving anyclass IsoValue
+
+instance ParameterHasEntryPoints Parameter where
+  type ParameterEntryPointsDerivation Parameter = EpdPlain
+
+type Storage = Natural
+
+measureBoaConstrictor :: ContractCode Parameter Storage
+measureBoaConstrictor = contractName "Boa constrictor measurement" $ do
+  doc $ DDescription "This contract measures boa constrictor."
+  unpair
+  dip drop
+  entryCase @Parameter (Proxy @PlainEntryPointsKind)
+    ( #cMeasureBoaConstrictor /-> do
+        doc $ DDescription "Measure the boa constrictor with given method."
+        fromNamed #method
+        caseT @MeasurementMethod
+          ( #cParrotStep /-> push @Natural 38
+          , #cMonkeyStep /-> push @Natural 31
+          , #cElephantStep /-> push @Natural 9
+          )
+    , #cZero /-> do
+        doc $ DDescription "Put zero to the storage."
+        drop; push @Natural 0
+    )
+  nil; pair
+```
+
+### Generated documentation
+
+Generated documentation for this contract can be found [here](./doc/sampleAutodoc.md).
+
+### Transpiled Michelson contract
+
+```
+parameter (or (or :method %measureBoaConstrictor unit
+                                                 (or unit
+                                                     unit))
+              (unit %zero));
+storage nat;
+code { CAST (pair (or (or unit (or unit unit)) unit) nat);
+       DUP;
+       CAR;
+       DIP { CDR };
+       DIP { DROP };
+       IF_LEFT { IF_LEFT { DROP;
+                           PUSH nat 38 }
+                         { IF_LEFT { DROP;
+                                     PUSH nat 31 }
+                                   { DROP;
+                                     PUSH nat 9 } } }
+               { DROP;
+                 PUSH nat 0 };
+       NIL operation;
+       PAIR };
+```
+
+## FAQ
+
+<!-- This question should be removed once https://gitlab.com/morley-framework/morley/issues/79 is resolved -->
+* Q: I added a new parameter case to contract and GHC went mad.
+
+  A: Ensure that your number of entry points does not exceed the limit set in [`Util.TypeTuple.Instances`](../morley/src/Util/TypeTuple/Instances.hs).
+
+* Q: I added one more datatype that is used in the contract and GHC reports with errors related
+     to `Rep` type family.
+
+  A: Make sure your datatype derives `Generic` instance and all primitive types used in it have `IsPrimitiveValue`
+     set to `True`.
diff --git a/lorentz.cabal b/lorentz.cabal
--- a/lorentz.cabal
+++ b/lorentz.cabal
@@ -1,13 +1,13 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.32.0.
+-- This file has been generated from package.yaml by hpack version 0.33.0.
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 7990f612989602be8cc01109be8cbf14f3b33c3346292f6f58d3c293094c3f8d
+-- hash: 19874377999eb866131159c713da07469cac8c7698406c41b9e7758fd1104672
 
 name:           lorentz
-version:        0.1.0
+version:        0.2.0
 synopsis:       EDSL for the Michelson Language
 description:    Lorentz is a powerful meta-programming tool which allows one to write Michelson contracts directly in Haskell. It has the same instructions as Michelson, but operates on Haskell values and allows one to use Haskell features.
 category:       Language
@@ -30,6 +30,7 @@
 library
   exposed-modules:
       Lorentz
+      Lorentz.Address
       Lorentz.ADT
       Lorentz.Arith
       Lorentz.Base
@@ -50,6 +51,8 @@
       Lorentz.Errors
       Lorentz.Errors.Common
       Lorentz.Errors.Numeric
+      Lorentz.Errors.Numeric.Contract
+      Lorentz.Errors.Numeric.Doc
       Lorentz.Ext
       Lorentz.Extensible
       Lorentz.Instr
@@ -66,7 +69,6 @@
       Lorentz.Test
       Lorentz.Test.Consumer
       Lorentz.Test.Doc
-      Lorentz.Test.Import
       Lorentz.Test.Integrational
       Lorentz.Test.Unit
       Lorentz.TestScenario
@@ -86,13 +88,18 @@
       Lorentz.UStore.Types
       Lorentz.Value
       Lorentz.Zip
+  other-modules:
+      Paths_lorentz
+  autogen-modules:
+      Paths_lorentz
   hs-source-dirs:
       src
   default-extensions: ApplicativeDo AllowAmbiguousTypes BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MonadFailDesugaring MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances 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 -O0
+  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:
       HUnit
     , QuickCheck
+    , aeson-pretty
     , base-noprelude >=4.7 && <5
     , bimap
     , bytestring
@@ -103,18 +110,18 @@
     , fmt
     , formatting
     , ghc-prim
-    , hspec
     , interpolate
     , lens
     , morley
     , morley-prelude >=0.3.0
+    , mtl
     , named
     , optparse-applicative
     , pretty-terminal
     , singletons
-    , tasty
     , template-haskell
     , text
+    , tezos-bake-monitor-lib
     , unordered-containers
     , vinyl
   default-language: Haskell2010
@@ -128,9 +135,13 @@
       Test.Lorentz.Base
       Test.Lorentz.Conditionals
       Test.Lorentz.DeadCode
+      Test.Lorentz.Doc.Positions
       Test.Lorentz.EntryPoints
+      Test.Lorentz.EntryPoints.Doc
       Test.Lorentz.Errors
+      Test.Lorentz.Errors.Numeric
       Test.Lorentz.Extensible
+      Test.Lorentz.Interpreter
       Test.Lorentz.Macro
       Test.Lorentz.Pack
       Test.Lorentz.Print
@@ -148,10 +159,11 @@
       Test.Tasty.TypeSpec
       Test.Util.TypeSpec
       Tree
+      Paths_lorentz
   hs-source-dirs:
       test
   default-extensions: ApplicativeDo AllowAmbiguousTypes BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MonadFailDesugaring MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances ViewPatterns DerivingStrategies
-  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 -O0 -threaded -with-rtsopts=-N
+  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 -threaded -with-rtsopts=-N
   build-tool-depends:
       tasty-discover:tasty-discover
   build-depends:
@@ -163,6 +175,7 @@
     , constraints
     , containers
     , data-default
+    , filepath
     , first-class-families
     , fmt
     , formatting
diff --git a/src/Lorentz/ADT.hs b/src/Lorentz/ADT.hs
--- a/src/Lorentz/ADT.hs
+++ b/src/Lorentz/ADT.hs
@@ -37,7 +37,6 @@
 import Data.Constraint (Dict(..))
 import qualified Data.Kind as Kind
 import Data.Vinyl.Core (RMap(..), Rec(..))
-import Data.Vinyl.Derived (Label)
 import GHC.TypeLits (AppendSymbol, Symbol)
 import Named ((:!), (:?), arg, argDef, argF)
 
@@ -47,6 +46,7 @@
 import Michelson.Typed.Haskell.Instr
 import Michelson.Typed.Haskell.Value
 import Util.TypeTuple
+import Util.Label (Label)
 
 -- | Allows field access and modification.
 type HasField dt fname =
@@ -197,7 +197,7 @@
 -- To construct a case branch use '/->' operator.
 case_
   :: forall dt out inp.
-     ( InstrCaseC dt inp out
+     ( InstrCaseC dt
      , RMap (CaseClauses dt)
      )
   => Rec (CaseClauseL inp out) (CaseClauses dt) -> dt & inp :-> out
@@ -224,7 +224,7 @@
 caseT = case_ @dt . recFromTuple
 
 type CaseTC dt out inp clauses =
-  ( InstrCaseC dt inp out
+  ( InstrCaseC dt
   , RMap (CaseClauses dt)
   , RecFromTuple clauses
   , clauses ~ Rec (CaseClauseL inp out) (CaseClauses dt)
diff --git a/src/Lorentz/Address.hs b/src/Lorentz/Address.hs
new file mode 100644
--- /dev/null
+++ b/src/Lorentz/Address.hs
@@ -0,0 +1,211 @@
+{- |
+
+This module introduces several types for safe work with @address@ and
+@contract@ types. All available types for that are represented in the following
+table:
+
++------------------------+------------+-------------------+----------------------+
+| Type                   | Type safe? | What it refers to | Michelson reflection |
++========================+============+===================+======================+
+| Address                | No         | Whole contract    | address              |
++------------------------+------------+-------------------+----------------------+
+| EpAddress              | No         | Entrypoint        | address              |
++------------------------+------------+-------------------+----------------------+
+| TAddress               | Yes        | Whole contract    | address              |
++------------------------+------------+-------------------+----------------------+
+| FutureContract         | Yes        | Entrypoint        | address              |
++------------------------+------------+-------------------+----------------------+
+| ContractRef            | Yes        | Entrypoint        | contract             |
++------------------------+------------+-------------------+----------------------+
+
+This module also provides functions for converting between these types in Haskell
+and Michelson worlds.
+In the latter you can additionally use coercions and dedicated instructions from
+"Lorentz.Instr".
+
+-}
+module Lorentz.Address
+  ( TAddress (..)
+  , FutureContract (..)
+
+    -- ** Conversions
+  , callingTAddress
+  , callingDefTAddress
+  , ToAddress (..)
+  , ToTAddress (..)
+  , ToTAddress_
+  , toTAddress_
+  , ToContractRef (..)
+  , FromContractRef (..)
+  , convertContractRef
+
+    -- * Re-exports
+  , Address
+  , EpAddress (..)
+  , ContractRef (..)
+  , M.coerceContractRef
+  ) where
+
+import Data.Kind as Kind
+import Data.Type.Bool (type (&&), Not)
+
+import Lorentz.Base
+import Lorentz.Constraints
+import qualified Lorentz.EntryPoints.Core as Ep
+import Lorentz.TypeAnns
+import Michelson.Typed (ContractRef(..), IsoValue(..))
+import qualified Michelson.Typed as M
+import Michelson.Typed.EntryPoints (EpAddress(..))
+import Tezos.Address (Address)
+import Util.Type
+import Util.TypeLits
+
+-- | Address which remembers the parameter type of the contract it refers to.
+--
+-- It differs from Michelson's @contract@ type because it cannot contain
+-- entrypoint, and it always refers to entire contract parameter even if this
+-- contract has explicit default entrypoint.
+newtype TAddress p = TAddress { unTAddress :: Address }
+  deriving stock Generic
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+-- | Turn 'TAddress' to 'ContractRef' in /Haskell/ world.
+--
+-- This is an analogy of @address@ to @contract@ convertion in Michelson world,
+-- thus you have to supply an entrypoint (or call the default one explicitly).
+callingTAddress
+  :: forall cp mname.
+     (NiceParameterFull cp)
+  => TAddress cp
+  -> Ep.EntryPointRef mname
+  -> ContractRef (Ep.GetEntryPointArgCustom cp mname)
+callingTAddress (TAddress addr) epRef =
+  withDict (niceParameterEvi @cp) $
+  case Ep.parameterEntryPointCallCustom @cp epRef of
+    epc@M.EntryPointCall{} -> ContractRef addr (M.SomeEpc epc)
+
+-- | Specification of 'callTAddress' to call the default entrypoint.
+callingDefTAddress
+  :: forall cp.
+     (NiceParameterFull cp)
+  => TAddress cp
+  -> ContractRef (Ep.GetDefaultEntryPointArg cp)
+callingDefTAddress taddr = callingTAddress taddr Ep.CallDefault
+
+-- | Something coercible to 'TAddress cp'.
+type ToTAddress_ cp addr = (ToTAddress cp addr, ToT addr ~ ToT Address)
+
+-- | Cast something appropriate to 'TAddress'.
+toTAddress_
+  :: forall cp addr s.
+     (ToTAddress_ cp addr)
+  => addr : s :-> TAddress cp : s
+toTAddress_ = I M.Nop
+
+-- | Address associated with value of @contract arg@ type.
+--
+-- Places where 'ContractRef' can appear are now severely limited,
+-- this type gives you type-safety of 'ContractRef' but still can be used
+-- everywhere.
+-- This type is not a full-featured one rather a helper; in particular, once
+-- pushing it on stack, you cannot return it back to Haskell world.
+--
+-- Note that it refers to an entrypoint of the contract, not just the contract
+-- as a whole. In this sense this type differs from 'TAddress'.
+--
+-- Unlike with 'ContractRef', having this type you still cannot be sure that
+-- the referred contract exists and need to perform a lookup before calling it.
+newtype FutureContract arg = FutureContract { unFutureContract :: ContractRef arg }
+
+instance IsoValue (FutureContract arg) where
+  type ToT (FutureContract arg) = ToT EpAddress
+  toVal (FutureContract contract) = toVal $ M.contractRefToAddr contract
+  fromVal = error "Fetching 'FutureContract' back from Michelson is impossible"
+
+instance HasTypeAnn (FutureContract a) where
+  getTypeAnn = M.starNotes
+
+-- | Convert something to 'Address' in /Haskell/ world.
+--
+-- Use this when you want to access state of the contract and are not interested
+-- in calling it.
+class ToAddress a where
+  toAddress :: a -> Address
+
+instance ToAddress Address where
+  toAddress = id
+
+instance ToAddress EpAddress where
+  toAddress = eaAddress
+
+instance ToAddress (TAddress cp) where
+  toAddress = unTAddress
+
+instance ToAddress (FutureContract cp) where
+  toAddress = toAddress . unFutureContract
+
+instance ToAddress (ContractRef cp) where
+  toAddress = crAddress
+
+-- | Convert something referring to a contract (not specific entrypoint)
+-- to 'TAddress' in /Haskell/ world.
+class ToTAddress (cp :: Kind.Type) (a :: Kind.Type) where
+  toTAddress :: a -> TAddress cp
+
+instance ToTAddress cp Address where
+  toTAddress = TAddress
+
+instance (cp ~ cp') => ToTAddress cp (TAddress cp') where
+  toTAddress = id
+
+-- | Convert something to 'ContractRef' in /Haskell/ world.
+class ToContractRef (cp :: Kind.Type) (contract :: Kind.Type) where
+  toContractRef :: HasCallStack => contract -> ContractRef cp
+
+instance (cp ~ cp') => ToContractRef cp (ContractRef cp') where
+  toContractRef = id
+
+instance (NiceParameter cp, cp ~ cp') => ToContractRef cp (FutureContract cp') where
+  toContractRef = unFutureContract
+
+instance ( FailWhen cond msg
+         , cond ~
+            ( Ep.CanHaveEntryPoints cp &&
+              Not (Ep.ParameterEntryPointsDerivation cp == Ep.EpdNone)
+            )
+         , msg ~
+            ( 'Text "Cannot apply `ToContractRef` to `TAddress`" ':$$:
+              'Text "Consider using call(Def)TAddress first`" ':$$:
+              'Text "(or if you know your parameter type is primitive," ':$$:
+              'Text " make sure typechecker also knows about that)" ':$$:
+              'Text "For parameter `" ':<>: 'ShowType cp ':<>: 'Text "`"
+            )
+         , cp ~ arg, NiceParameter arg
+           -- These constraints should naturally derive from ones above,
+           -- but proving that is not worth the effort
+         , NiceParameterFull cp, Ep.GetDefaultEntryPointArg cp ~ cp
+         ) =>
+         ToContractRef arg (TAddress cp) where
+  toContractRef = callingDefTAddress
+
+-- | Convert something from 'ContractAddr' in /Haskell/ world.
+class FromContractRef (cp :: Kind.Type) (contract :: Kind.Type) where
+  fromContractRef :: ContractRef cp -> contract
+
+instance (cp ~ cp') => FromContractRef cp (ContractRef cp') where
+  fromContractRef = id
+
+instance (cp ~ cp') => FromContractRef cp (FutureContract cp') where
+  fromContractRef = FutureContract . fromContractRef
+
+instance FromContractRef cp EpAddress where
+  fromContractRef = M.contractRefToAddr
+
+instance FromContractRef cp Address where
+  fromContractRef = crAddress
+
+convertContractRef
+  :: forall cp contract2 contract1.
+     (ToContractRef cp contract1, FromContractRef cp contract2)
+  => contract1 -> contract2
+convertContractRef = fromContractRef @cp . toContractRef
diff --git a/src/Lorentz/Arith.hs b/src/Lorentz/Arith.hs
--- a/src/Lorentz/Arith.hs
+++ b/src/Lorentz/Arith.hs
@@ -84,7 +84,7 @@
   type ArithResHs Or Bool Bool = Bool
 
 instance ArithOpHs And Integer Natural where
-  type ArithResHs And Integer Natural = Integer
+  type ArithResHs And Integer Natural = Natural
 instance ArithOpHs And Natural Natural where
   type ArithResHs And Natural Natural = Natural
 instance ArithOpHs And Bool Bool where
diff --git a/src/Lorentz/Base.hs b/src/Lorentz/Base.hs
--- a/src/Lorentz/Base.hs
+++ b/src/Lorentz/Base.hs
@@ -21,9 +21,10 @@
   , transformBytesLorentz
   , optimizeLorentz
   , optimizeLorentzWithConf
+  , MapLorentzInstr (..)
 
   , ContractOut
-  , Contract
+  , ContractCode
   , SomeContract (..)
   , Lambda
   ) where
@@ -35,14 +36,15 @@
 import Fmt (Buildable(..))
 
 import Lorentz.Constraints
-import Lorentz.Value
 import Michelson.ErrorPos (InstrCallStack)
 import Michelson.Optimizer (OptimizerConf, optimizeWithConf)
 import Michelson.Parser (ParserException, parseExpandValue)
 import Michelson.Preprocess (transformBytes, transformStrings)
-import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeVerifyValue)
+import Michelson.Text (MText)
+import Michelson.TypeCheck (TCError, runTypeCheckIsolated, typeCheckValue)
 import Michelson.Typed
-  (Instr(..), RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr, rfMerge)
+  (Instr(..), IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr, rfMapAnyInstr,
+  rfMerge)
 import qualified Michelson.Untyped as U
 
 -- | Alias for instruction which hides inner types representation via 'T'.
@@ -104,12 +106,12 @@
 infixr 1 %>
 
 type ContractOut st = '[([Operation], st)]
-type Contract cp st = '[(cp, st)] :-> ContractOut st
+type ContractCode cp st = '[(cp, st)] :-> ContractOut st
 
 data SomeContract where
   SomeContract
     :: (NiceParameterFull cp, NiceStorage st)
-    => Contract cp st
+    => ContractCode cp st
     -> SomeContract
 
 type (&) (a :: Kind.Type) (b :: [Kind.Type]) = a ': b
@@ -163,7 +165,7 @@
       first ParseLorentzTypecheckError .
       runTypeCheckIsolated .
       usingReaderT (def @InstrCallStack) .
-      typeVerifyValue
+      typeCheckValue
 
 -- | Lorentz version of 'transformStrings'.
 transformStringsLorentz ::
@@ -191,3 +193,11 @@
   :: inp :-> out
   -> inp :-> out
 optimizeLorentz = optimizeLorentzWithConf def
+
+-- | Applicable for wrappers over Lorentz code.
+class MapLorentzInstr instr where
+  -- | Modify all the code under given entity.
+  mapLorentzInstr :: (forall i o. (i :-> o) -> (i :-> o)) -> instr -> instr
+
+instance MapLorentzInstr (i :-> o) where
+  mapLorentzInstr f = f
diff --git a/src/Lorentz/Coercions.hs b/src/Lorentz/Coercions.hs
--- a/src/Lorentz/Coercions.hs
+++ b/src/Lorentz/Coercions.hs
@@ -2,6 +2,7 @@
 module Lorentz.Coercions
   ( -- * Safe coercions
     CanCastTo (..)
+  , castDummyG
   , checkedCoerce
   , Coercible_
   , checkedCoerce_
@@ -28,14 +29,17 @@
 import Control.Lens (Wrapped(..))
 import qualified Data.Coerce as Coerce
 import Data.Constraint (Dict(..), (\\))
-import Data.Vinyl.Derived (Label)
+import qualified GHC.Generics as G
 import Named (NamedF)
 import Unsafe.Coerce (unsafeCoerce)
 
+import Lorentz.Address
 import Lorentz.Base
 import Lorentz.Instr
 import Lorentz.Value
+import Lorentz.Zip
 import Michelson.Typed
+import Util.Label (Label)
 
 ----------------------------------------------------------------------------
 -- Unsafe coercions
@@ -106,36 +110,29 @@
 ----------------------------------------------------------------------------
 
 -- | Explicitly allowed coercions.
+--
+-- @a `CanCastTo` b@ proclaims that @a@ can be casted to @b@ without violating
+-- any invariants of @b@.
+--
+-- This relation is reflexive; it /may/ be symmetric or not.
+-- It tends to be composable: casting complex types usually requires permission
+-- to cast their respective parts; for such types consider using 'castDummyG'
+-- as implementation of the method of this typeclass.
+--
+-- For cases when a cast from @a@ to @b@ requires some validation, consider
+-- rather making a dedicated function which performs the necessary checks and
+-- then calls @forcedCoerce@.
 class a `CanCastTo` b where
   -- | An optional method which helps passing -Wredundant-constraints check.
-  castDummy :: ()
-  castDummy = ()
+  -- Also, you can set specific implementation for it with specific sanity checks.
+  castDummy :: Proxy a -> Proxy b -> ()
+  castDummy _ _ = ()
 
 -- | Coercion in Haskell world which respects 'CanCastTo'.
 checkedCoerce :: forall a b. (CanCastTo a b, Coerce.Coercible a b) => a -> b
 checkedCoerce = Coerce.coerce
   where _useCast = castDummy @a @b
 
--- Incoherent instance are generally evil because arbitrary instance can be
--- picked, but in our case this is exactly what we want: permit cast if
--- /any/ instance matches.
-instance {-# INCOHERENT #-} CanCastTo a a where
-  castDummy = castDummy @a @a
-
-instance CanCastTo a b => CanCastTo [a] [b] where
-  castDummy = castDummy @a @b
-
-instance (CanCastTo a1 a2, CanCastTo b1 b2) =>
-         CanCastTo (a1, b1) (a2, b2) where
-  castDummy = castDummy @a1 @a2 `seq` castDummy @b1 @b2
-
-instance (CanCastTo i1 i2, CanCastTo o1 o2) =>
-         CanCastTo (Lambda i1 o1) (Lambda i2 o2)
-  -- That's magic, having default impl for 'castDummy' disables
-  -- -Wredundant-constraints automatically
-
-instance CanCastTo a b => CanCastTo (Maybe a) (Maybe b)
-
 -- | Coercion from @a@ to @b@ is permitted and safe.
 type Castable_ a b = (MichelsonCoercible a b, CanCastTo a b)
 
@@ -165,6 +162,62 @@
 allowCheckedCoerce :: forall a b. Dict (CanCastTo a b, CanCastTo b a)
 allowCheckedCoerce =
   Dict \\ allowCheckedCoerceTo @a @b \\ allowCheckedCoerceTo @b @a
+
+-- Incoherent instances are generally evil because arbitrary instance can be
+-- picked, but in our case this is exactly what we want: permit cast if
+-- /any/ instance matches.
+instance {-# INCOHERENT #-} CanCastTo a a where
+
+instance CanCastTo a b =>
+         CanCastTo [a] [b]
+instance CanCastTo a b =>
+         CanCastTo (Maybe a) (Maybe b)
+instance (CanCastTo l1 l2, CanCastTo r1 r2) =>
+         CanCastTo (Either l1 r1) (Either l2 r2)
+instance CanCastTo k1 k2 =>
+         CanCastTo (Set k1) (Set k2)
+instance (CanCastTo k1 k2, CanCastTo v1 v2) =>
+         CanCastTo (Map k1 v1) (Map k2 v2)
+instance (CanCastTo k1 k2, CanCastTo v1 v2) =>
+         CanCastTo (BigMap k1 v1) (BigMap k2 v2)
+instance ( CanCastTo (ZippedStack i1) (ZippedStack i2)
+         , CanCastTo (ZippedStack o1) (ZippedStack o2)
+         ) =>
+         CanCastTo (i1 :-> o1) (i2 :-> o2)
+instance (CanCastTo a1 a2) =>
+         CanCastTo (ContractRef a1) (ContractRef a2)
+
+instance (CanCastTo a b, f ~ g) => CanCastTo (NamedF f a n) (NamedF g b m)
+
+instance (CanCastTo a1 a2, CanCastTo b1 b2) =>
+         CanCastTo (a1, b1) (a2, b2)
+instance (CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2) =>
+         CanCastTo (a1, b1, c1) (a2, b2, c2)
+instance (CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2, CanCastTo d1 d2) =>
+         CanCastTo (a1, b1, c1, d1) (a2, b2, c2, d2)
+instance ( CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2, CanCastTo d1 d2
+         , CanCastTo e1 e2 ) =>
+         CanCastTo (a1, b1, c1, d1, e1) (a2, b2, c2, d2, e2)
+instance ( CanCastTo a1 a2, CanCastTo b1 b2, CanCastTo c1 c2, CanCastTo d1 d2
+         , CanCastTo e1 e2, CanCastTo f1 f2 ) =>
+         CanCastTo (a1, b1, c1, d1, e1, f1) (a2, b2, c2, d2, e2, f2)
+
+-- | Implementation of 'castDummy' for types composed from smaller types.
+-- It helps to ensure that all necessary constraints are requested in instance
+-- head.
+castDummyG
+  :: (Generic a, Generic b, GCanCastTo (G.Rep a) (G.Rep b))
+  => Proxy a -> Proxy b -> ()
+castDummyG (_ :: Proxy a) (_ :: Proxy b) = ()
+  where _dummy = Dict @(Generic a, Generic b, GCanCastTo (G.Rep a) (G.Rep b))
+
+type family GCanCastTo x y :: Constraint where
+  GCanCastTo (G.M1 _ _ x) (G.M1 _ _ y) = GCanCastTo x y
+  GCanCastTo (xl G.:+: xr) (yl G.:+: yr) = (GCanCastTo xl yl, GCanCastTo xr yr)
+  GCanCastTo (xl G.:*: xr) (yl G.:*: yr) = (GCanCastTo xl yl, GCanCastTo xr yr)
+  GCanCastTo G.U1 G.U1 = ()
+  GCanCastTo G.V1 G.V1 = ()
+  GCanCastTo (G.Rec0 a) (G.Rec0 b) = CanCastTo a b
 
 {- Note about potential use of 'Coercible'.
 
diff --git a/src/Lorentz/ContractRegistry.hs b/src/Lorentz/ContractRegistry.hs
--- a/src/Lorentz/ContractRegistry.hs
+++ b/src/Lorentz/ContractRegistry.hs
@@ -1,32 +1,61 @@
 -- | This module contains various datatypes and functions which are
--- common for contract registry packages (e.g. morley-ledgers and morley-multisig).
+-- common for contract registry packages (e.g. @morley-ledgers@ and
+-- @morley-multisig@).
+
 module Lorentz.ContractRegistry
-  ( ContractInfo (..)
+  ( -- * Registry types
+    ContractInfo (..)
   , ContractRegistry (..)
-  , getContract
-  , printContractFromRegistryDoc
   , (?::)
-  -- Common CLI stuff
+
+  -- * Things to do in @main@
   , CmdLnArgs (..)
   , argParser
+  , runContractRegistry
+
+  -- * Building blocks
+  , getContract
+  , printContractFromRegistryDoc
   ) where
 
+import Data.Aeson.Encode.Pretty (encodePretty, encodePrettyToTextBuilder)
+import qualified Data.ByteString.Lazy.Char8 as BS (putStrLn)
+import Data.Constraint ((\\))
 import qualified Data.Map as Map
-import qualified Data.Text.Lazy.IO as TL
-import Fmt (Buildable(..), blockListF, nameF, (+|), (|+))
+import Data.Text.Lazy.Builder (toLazyText)
+import Fmt (Buildable(..), blockListF, nameF, pretty, (+|), (|+))
 import qualified Options.Applicative as Opt
+import Tezos.V005.Micheline (Expression)
 
 import Lorentz.Base
 import Lorentz.Constraints
 import Lorentz.Doc
+import Lorentz.Print
+import Lorentz.Run
+import Michelson.Printer (printTypedFullContract)
+import Michelson.Typed (FullContract(..), IsoValue(..), Notes)
+import Morley.Micheline
 import Util.IO
 
 data ContractInfo =
   forall cp st.
     (NiceParameterFull cp, NiceStorage st) =>
   ContractInfo
-  { ciContract :: Contract cp st
+  { ciContract :: ContractCode cp st
   , ciIsDocumented :: Bool
+  , ciStorageParser :: Maybe (Opt.Parser st)
+  -- ^ Specifies how to parse initial storage value.
+  --
+  -- Normally you pass some user data and call a function that
+  -- constructs storage from that data.
+  --
+  -- If storage is simple and can be easilly constructed manually, you
+  -- can use 'Nothing'.
+  , ciCompilationOptions :: CompilationOptions
+  -- ^ How to compile this contract.
+  , ciStorageNotes :: Notes (ToT st)
+  -- ^ A temporary approach to add annotations to storage.
+  -- TODO [#20]: invent something better.
   }
 
 (?::) :: Text -> a -> (Text, a)
@@ -46,28 +75,31 @@
   build registry =
     nameF "Available contracts" (blockListF $ keys (unContractRegistry registry))
 
-printContractFromRegistryDoc :: Text -> ContractRegistry -> Maybe FilePath -> IO ()
-printContractFromRegistryDoc name contracts mOutput = do
+printContractFromRegistryDoc :: Text -> ContractRegistry -> DGitRevision -> Maybe FilePath -> IO ()
+printContractFromRegistryDoc name contracts gitRev mOutput = do
   ContractInfo{..} <- either die pure $ getContract name contracts
-  let writeFunc = case mOutput of
-        Nothing -> TL.putStrLn
-        Just "def" -> writeFileUtf8 $ toString name <> ".md"
-        Just output -> writeFileUtf8 output
   if ciIsDocumented
-  then writeFunc $ contractDocToMarkdown $ buildLorentzDoc ciContract
+  then
+     writeFunc (toString name <> ".md") mOutput $
+       contractDocToMarkdown $ buildLorentzDocWithGitRev gitRev ciContract
   else die "This contract is not documented"
 
+data SomeNiceStorage where
+  SomeNiceStorage :: NiceStorage st => st -> SomeNiceStorage
+
+-- | 'ContractRegistry' actions parsed from CLI.
 data CmdLnArgs
   = List
-  | Print Text (Maybe FilePath) Bool
-  | Document Text (Maybe FilePath)
+  | Print Text (Maybe FilePath) Bool Bool
+  | Document Text (Maybe FilePath) DGitRevision
+  | PrintStorage SomeNiceStorage Bool
 
-argParser :: Opt.Parser CmdLnArgs
-argParser = Opt.subparser $ mconcat
+argParser :: ContractRegistry -> DGitRevision -> Opt.Parser CmdLnArgs
+argParser registry gitRev = Opt.subparser $ mconcat $
   [ listSubCmd
   , printSubCmd
   , documentSubCmd
-  ]
+  ] <> mapMaybe storageSubCmd (Map.toList $ unContractRegistry registry)
   where
     mkCommandParser commandName parser desc =
       Opt.command commandName $
@@ -81,12 +113,12 @@
 
     printSubCmd =
       mkCommandParser "print"
-      (Print <$> printOptions <*> outputOptions <*> onelineOption)
+      (Print <$> printOptions <*> outputOptions <*> onelineOption <*> michelineOption)
       "Dump a contract in form of Michelson code"
 
     documentSubCmd =
       mkCommandParser "document"
-      (Document <$> printOptions <*> outputOptions)
+      (Document <$> printOptions <*> outputOptions <*> pure gitRev)
       "Dump contract documentation in Markdown"
 
     printOptions = Opt.strOption $ mconcat
@@ -100,10 +132,58 @@
       [ Opt.short 'o'
       , Opt.long "output"
       , Opt.metavar "FILEPATH"
-      , Opt.help "File to use as output. If not specified, stdout is used."
+      , Opt.help $
+        "File to use as output. If not specified, the file name " <>
+        "will be constructed from the contract name." <>
+        "Pass - to use stdout."
       ]
 
     onelineOption :: Opt.Parser Bool
     onelineOption = Opt.switch (
       Opt.long "oneline" <>
       Opt.help "Force single line output")
+
+    michelineOption :: Opt.Parser Bool
+    michelineOption = Opt.switch (
+      Opt.long "micheline" <>
+      Opt.help "Print using low-level Micheline representation")
+
+    storageSubCmd ::
+      (Text, ContractInfo) -> Maybe $ Opt.Mod Opt.CommandFields CmdLnArgs
+    storageSubCmd (toString -> name, ContractInfo {..}) = do
+      storageParser <- ciStorageParser
+      pure $ mkCommandParser ("storage-" <> name)
+        (PrintStorage . SomeNiceStorage <$> storageParser <*> michelineOption)
+        ("Print initial storage for the contract '" <> name <> "'")
+
+-- | Run an action operating with 'ContractRegistry'.
+runContractRegistry :: ContractRegistry -> CmdLnArgs -> IO ()
+runContractRegistry registry = \case
+  List -> pretty registry
+  Print name mOutput forceOneLine useMicheline ->
+    case getContract name registry of
+      Left err ->
+        die err
+      Right ContractInfo{..} ->
+        let compiledContract  =
+              (compileLorentzContractWithOptions ciCompilationOptions ciContract)
+                {fcStoreNotes = ciStorageNotes} in
+        writeFunc (toString name <> ".tz") mOutput $
+          if useMicheline
+          then toLazyText $ encodePrettyToTextBuilder $ toExpression compiledContract
+          else printTypedFullContract forceOneLine $ compiledContract
+  Document name mOutput gitRev -> do
+    printContractFromRegistryDoc name registry gitRev mOutput
+  PrintStorage (SomeNiceStorage (storage :: st)) useMicheline ->
+    if useMicheline
+    then BS.putStrLn $ encodePretty $ toExpressionHelper storage
+    else putStrLn $ printLorentzValue True storage
+  where
+    toExpressionHelper :: forall st'. NiceStorage st' => st' -> Expression
+    toExpressionHelper = toExpression . toVal \\ niceStorageEvi @st'
+
+writeFunc :: FilePath -> Maybe FilePath -> LText -> IO ()
+writeFunc defName = \case
+  Nothing -> writeFileUtf8 defName
+  Just "-" -> putStrLn
+  Just output -> writeFileUtf8 output
diff --git a/src/Lorentz/Doc.hs b/src/Lorentz/Doc.hs
--- a/src/Lorentz/Doc.hs
+++ b/src/Lorentz/Doc.hs
@@ -3,9 +3,13 @@
 module Lorentz.Doc
   ( doc
   , docGroup
+  , docStorage
   , buildLorentzDoc
+  , buildLorentzDocWithGitRev
   , renderLorentzDoc
   , contractName
+  , contractGeneral
+  , contractGeneralDefault
   , cutLorentzNonDoc
 
     -- * Re-exports
@@ -27,6 +31,7 @@
   , mkDGitRevision
   , morleyRepoSettings
   , DComment (..)
+  , DAnchor (..)
   , DType (..)
   , docDefinitionRef
   , contractDocToMarkdown
@@ -65,13 +70,18 @@
 
 -- | Put a document item.
 doc :: DocItem di => di -> s :-> s
-doc = I . Ext . DOC_ITEM . SomeDocItem
+doc = I . docInstr
 
 -- | Group documentation built in the given piece of code
 -- into block dedicated to one thing, e.g. to one entrypoint.
 docGroup :: DocGrouping -> (inp :-> out) -> (inp :-> out)
 docGroup gr = iMapAnyCode (DocGroup gr)
 
+-- | Insert documentation of the contract storage type. The type
+-- should be passed using type applications.
+docStorage :: forall storage s. TypeHasDoc storage => s :-> s
+docStorage = doc $ DStorageType $ DType $ Proxy @storage
+
 -- | Give a name to given contract. Apply it to the whole contract code.
 contractName :: Text -> (inp :-> out) -> (inp :-> out)
 contractName name = docGroup (SomeDocItem . DName name)
@@ -79,6 +89,23 @@
 buildLorentzDoc :: inp :-> out -> ContractDoc
 buildLorentzDoc (iAnyCode -> code) = buildInstrDoc code
 
+-- | Takes an instruction that inserts documentation items with
+-- general information about the contract. Inserts it into general
+-- section. See 'DGeneralInfoSection'.
+contractGeneral :: (inp :-> out) -> (inp :-> out)
+contractGeneral = docGroup (SomeDocItem . DGeneralInfoSection)
+
+-- | Inserts general information about the contract using the default format.
+--
+-- Currently we only include git revision. It is unknown in the
+-- library code and is supposed to be updated in an executable.
+contractGeneralDefault :: s :-> s
+contractGeneralDefault = contractGeneral $ doc DGitRevisionUnknown
+
+buildLorentzDocWithGitRev :: DGitRevision -> inp :-> out -> ContractDoc
+buildLorentzDocWithGitRev gitRev (iAnyCode -> code) =
+  buildInstrDocWithGitRev gitRev code
+
 renderLorentzDoc :: inp :-> out -> LText
 renderLorentzDoc = contractDocToMarkdown . buildLorentzDoc
 
@@ -94,7 +121,7 @@
          TypeHasDoc (i :-> o) where
   typeDocName _ = "Code (extended lambda)"
   typeDocMdReference tp wp =
-    let DocItemRef (DocItemId ctorDocItemId) = docItemRef (DType tp)
+    let DocItemRef ctorDocItemId = docItemRef (DType tp)
         refToThis = mdLocalRef (mdTicked "Code") ctorDocItemId
     in applyWithinParens wp $
       mconcat $ intersperse " " [refToThis, refToStack @i, refToStack @o]
diff --git a/src/Lorentz/Empty.hs b/src/Lorentz/Empty.hs
--- a/src/Lorentz/Empty.hs
+++ b/src/Lorentz/Empty.hs
@@ -17,13 +17,14 @@
 import Lorentz.Base
 import Lorentz.Doc
 import Lorentz.Errors
+import Lorentz.TypeAnns (HasTypeAnn)
 import Lorentz.Value
 import Michelson.Typed.Haskell.Doc
 
 -- | Replacement for uninhabited type.
 newtype Empty = Empty ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 instance TypeHasDoc Empty where
   typeDocMdDescription =
diff --git a/src/Lorentz/EntryPoints.hs b/src/Lorentz/EntryPoints.hs
--- a/src/Lorentz/EntryPoints.hs
+++ b/src/Lorentz/EntryPoints.hs
@@ -12,7 +12,6 @@
   , AllParameterEntryPoints
   , LookupParameterEntryPoint
   , parameterEntryPointsToNotes
-  , flattenEntryPoints
   , GetEntryPointArg
   , parameterEntryPointCall
   , GetDefaultEntryPointArg
@@ -25,9 +24,12 @@
   , GetEntryPointArgCustom
   , HasEntryPointArg (..)
   , HasDefEntryPointArg
+  , HasEntryPointOfType
+  , ParameterContainsEntryPoints
   , TrustEpName (..)
   , parameterEntryPointCallCustom
   , RequireAllUniqueEntryPoints
+  , (:>)
 
     -- * Implementations
   , EpdNone
diff --git a/src/Lorentz/EntryPoints/Core.hs b/src/Lorentz/EntryPoints/Core.hs
--- a/src/Lorentz/EntryPoints/Core.hs
+++ b/src/Lorentz/EntryPoints/Core.hs
@@ -5,12 +5,16 @@
   ( CanHaveEntryPoints
   , EntryPointsDerivation (..)
   , EpConstructionRes (..)
+  , EpCallingDesc (..)
+  , EpCallingStep (..)
   , RequireAllUniqueEntryPoints
   , ParameterHasEntryPoints (..)
   , ParameterDeclaresEntryPoints
   , GetParameterEpDerivation
   , pepNotes
   , pepCall
+  , pepDescs
+  , pepDescsWithDef
   , AllParameterEntryPoints
   , LookupParameterEntryPoint
   , parameterEntryPointsToNotes
@@ -18,7 +22,6 @@
   , parameterEntryPointCall
   , GetDefaultEntryPointArg
   , parameterEntryPointCallDefault
-  , flattenEntryPoints
   , ForbidExplicitDefaultEntryPoint
   , NoExplicitDefaultEntryPoint
   , sepcCallRootChecked
@@ -29,8 +32,11 @@
   , TrustEpName (..)
   , HasEntryPointArg (..)
   , HasDefEntryPointArg
+  , HasEntryPointOfType
+  , ParameterContainsEntryPoints
   , parameterEntryPointCallCustom
   , EpdNone
+  , (:>)
 
     -- * Internals
   , RequireAllUniqueEntryPoints'
@@ -38,22 +44,21 @@
 
 import Data.Constraint (Dict(..), (\\))
 import qualified Data.Kind as Kind
-import Data.Map (Map, insert)
-import Data.Singletons (SingI, sing)
 import Data.Typeable (typeRep)
-import Data.Vinyl.Derived (Label)
+import Data.Vinyl (Rec(..))
 import Fcf (Eval, Exp)
 import qualified Fcf
 import qualified Fcf.Utils as Fcf
 import Fmt (pretty)
 
 import Michelson.Typed
-import qualified Michelson.Untyped as U
+import Util.Label
 import Util.Type
 import Util.TypeLits
 
 import Lorentz.Constraints.Scopes
 import Lorentz.EntryPoints.Helpers
+import Lorentz.TypeAnns (HasTypeAnn, getTypeAnn)
 
 -- | Defines a generalized way to declare entrypoints for various parameter types.
 --
@@ -62,11 +67,20 @@
 -- Also keep in mind, that in presence of explicit default entrypoint, all other
 -- 'Or' arms should be callable, though you can put this burden on user if very
 -- necessary.
+--
+-- Methods of this typeclass aim to better type-safety when making up an
+-- implementation and they may be not too convenient to use; users should
+-- exploit their counterparts.
 class EntryPointsDerivation deriv cp where
   -- | Name and argument of each entrypoint.
   -- This may include intermediate ones, even root if necessary.
   --
   -- Touching this type family is costly (@O(N^2)@), don't use it often.
+  --
+  -- Note [order of entrypoints children]:
+  -- If this contains entrypoints referring to indermediate nodes (not leaves)
+  -- in @or@ tree, then each such entrypoint should be mentioned eariler than
+  -- all of its children.
   type EpdAllEntryPoints deriv cp :: [(Symbol, Kind.Type)]
 
   -- | Get entrypoint argument by name.
@@ -87,10 +101,13 @@
   -- This method is implementation detail, for actual entrypoint lookup
   -- use 'parameterEntryPointCall'.
   epdCall
-    :: (KnownSymbol name, ParameterScope (ToT cp))
+    :: ParameterScope (ToT cp)
     => Label name
     -> EpConstructionRes (ToT cp) (Eval (EpdLookupEntryPoint deriv cp name))
 
+  -- | Description of how each of the entrypoints is constructed.
+  epdDescs :: Rec EpCallingDesc (EpdAllEntryPoints deriv cp)
+
 type RequireAllUniqueEntryPoints' deriv cp =
   RequireAllUnique
     "entrypoint name"
@@ -108,6 +125,29 @@
   EpConstructionFailed
     :: EpConstructionRes param 'Nothing
 
+-- | How one of the entrypoints is called.
+--
+-- Type arguments are name of the constructor which eventually gave
+-- name to the entrypoint and this entrypoint's argument.
+data EpCallingDesc (info :: (Symbol, Kind.Type)) where
+  EpCallingDesc ::
+    { epcdArg :: Proxy (arg :: Kind.Type)
+      -- ^ Entrypoint argument type.
+    , epcdEntrypoint :: EpName
+      -- ^ Name of assigned entrypoint.
+    , epcdSteps :: [EpCallingStep]
+      -- ^ If we emulated entrypoints calling via just wrapping an argument into
+      -- constructors until getting the full parameter, how would it look like.
+      -- Steps are enlisted in reversed order - top-level constructors go last.
+    } -> EpCallingDesc '(name, arg)
+
+deriving stock instance Show (EpCallingDesc info)
+
+data EpCallingStep
+  -- | Wrap into constructor with given name.
+  = EpsWrapIn Text
+  deriving (Show, Eq)
+
 -- | Which entrypoints given parameter declares.
 --
 -- Note that usually this function should not be used as constraint, use
@@ -151,14 +191,46 @@
 -- It hides derivations stuff inside, and treats primitive types specially
 -- like 'GetParameterEpDerivation' does.
 pepCall
-  :: forall cp name deriv.
-     ( ParameterDeclaresEntryPoints cp, ParameterScope (ToT cp)
-     , KnownSymbol name, deriv ~ GetParameterEpDerivation cp
-     )
+  :: forall cp name.
+     (ParameterDeclaresEntryPoints cp, ParameterScope (ToT cp))
   => Label name
-  -> EpConstructionRes (ToT cp) (Eval (EpdLookupEntryPoint deriv cp name))
+  -> EpConstructionRes (ToT cp) (Eval (LookupParameterEntryPoint cp name))
 pepCall = epdCall @(GetParameterEpDerivation cp) @cp
 
+-- | Version of 'epdDescs' which we actually use in code.
+-- It hides derivations stuff inside, and treats primitive types specially
+-- like 'GetParameterEpDerivation' does.
+pepDescs
+  :: forall cp.
+     (ParameterDeclaresEntryPoints cp)
+  => Rec EpCallingDesc (AllParameterEntryPoints cp)
+pepDescs = epdDescs @(GetParameterEpDerivation cp) @cp
+
+-- | Descriptions of how each of the entrypoints is constructed.
+--
+-- Similar to 'pepDescs', but includes default entrypoint disregard whether it is
+-- explicit or not, while 'pepDescs' includes it only if it is explicit.
+-- Also this returns list, not 'Rec', for simplicity.
+--
+-- Note that [order of entrypoints children] property still holds here.
+pepDescsWithDef
+  :: forall cp.
+     (ParameterDeclaresEntryPoints cp)
+  => [Some1 EpCallingDesc]
+pepDescsWithDef = addDefaultIfImplicit $ pepDescs @cp
+  where
+    addDefaultIfImplicit descsRec =
+      let descs = recordToSomeList descsRec
+          hasDef =
+            any (\(Some1 EpCallingDesc{..}) -> epcdEntrypoint == DefEpName) descs
+      in if hasDef
+         then descs
+         else Some1 EpCallingDesc
+              { epcdArg = Proxy @cp
+              , epcdEntrypoint = DefEpName
+              , epcdSteps = []
+              } : descs
+
 -- Derived methods and type families
 ----------------------------------------------------------------------------
 
@@ -203,17 +275,14 @@
 -- To call default entrypoint properly use 'parameterEntryPointCallDefault'.
 parameterEntryPointCall
   :: forall cp name.
-     ( ParameterDeclaresEntryPoints cp
-     , KnownSymbol name
-     )
+     ParameterDeclaresEntryPoints cp
   => Label name
   -> EntryPointCall cp (GetEntryPointArg cp name)
-parameterEntryPointCall label =
+parameterEntryPointCall label@Label =
   withDict (niceParameterEvi @cp) $
   case pepCall @cp label of
     EpConstructed liftSeq -> EntryPointCall
-      { epcName = epNameFromParamAnn (ctorNameToAnn @name)
-               ?: error "Empty constructor-entrypoint name"
+      { epcName = ctorNameToEp @name
       , epcParamProxy = Proxy
       , epcLiftSequence = liftSeq
       }
@@ -332,41 +401,6 @@
   Call | (_ :: Proxy ('Just name)) <- Proxy @mname ->
     parameterEntryPointCall @cp (fromLabel @name)
 
--- | Flatten a provided list of notes to a map of its entrypoints
--- and its corresponding utype.
---
--- It is obtained by constructing `insert k1 v1 (insert k2 v2 ... mempty)`
--- pipe using `Endo` so that it is more concise rather than stacking composition
--- of monoidal endomorphisms explicitly. Note that here no duplicates can appear
--- in returned map for `ParamNotes` even if they may appear inside passed `Notes` tree.
-flattenEntryPoints :: SingI t => ParamNotes t -> Map EpName U.Type
-flattenEntryPoints (unParamNotes -> notes) = appEndo (gatherEPs (sing, notes)) mempty
-  where
-    gatherEPs
-      :: forall n.
-         (Sing n, Notes n)
-      -> Endo (Map EpName U.Type)
-    gatherEPs = \case
-      (STOr ls rs, NTOr _ fn1 fn2 ln rn) -> mconcat
-        [ Endo . maybe id (uncurry insert) . psi ln $ epNameFromParamAnn fn1
-        , Endo . maybe id (uncurry insert) . psi rn $ epNameFromParamAnn fn2
-        , gatherEPs (ls, ln)
-        , gatherEPs (rs, rn)
-        ]
-      _ -> mempty
-
-    psi
-      :: forall n.
-         SingI n
-      => Notes n
-      -> Maybe EpName
-      -> Maybe (EpName, U.Type)
-    psi n x = tensor x $ mkUType sing n
-
-    -- Tensorial strength criteria
-    tensor :: Functor f => f a -> b -> f (a,b)
-    tensor fa b = fmap (,b) fa
-
 -- | Universal entrypoint lookup.
 type family GetEntryPointArgCustom cp mname :: Kind.Type where
   GetEntryPointArgCustom cp 'Nothing = GetDefaultEntryPointArg cp
@@ -426,6 +460,26 @@
   HasEntryPointArg cp TrustEpName arg where
   useHasEntryPointArg (TrustEpName epName) = (Dict, epName) \\ niceParameterEvi @arg
 
+-- | Checks that the given parameter consists of some specific entrypoint. Similar as
+-- `HasEntryPointArg` but ensures that the argument matches the following datatype.
+type HasEntryPointOfType param con exp
+  = (GetEntryPointArgCustom param ('Just con) ~ exp, ParameterDeclaresEntryPoints param)
+
+-- | A helper datatype which prettifies interface for `ParameterContainsEntryPoints`.
+data NamedEp = NamedEp Symbol Kind.Type
+type n :> ty = 'NamedEp n ty
+infixr 0 :>
+
+-- | Check that the given entrypoint has some fields inside.
+-- This interface allows for an abstraction of contract parameter so
+-- that it requires some *minimal* specification, but not a concrete one.
+type family
+    ParameterContainsEntryPoints param (fields :: [NamedEp]) :: Constraint
+  where
+  ParameterContainsEntryPoints _ '[] = ()
+  ParameterContainsEntryPoints param ((n :> ty) ': rest) =
+    (HasEntryPointOfType param n ty, ParameterContainsEntryPoints param rest)
+
 ----------------------------------------------------------------------------
 -- Trivial implementation
 ----------------------------------------------------------------------------
@@ -433,8 +487,9 @@
 -- | No entrypoints declared, parameter type will serve as argument type
 -- of the only existing entrypoint (default one).
 data EpdNone
-instance SingI (ToT cp) => EntryPointsDerivation EpdNone cp where
+instance (HasTypeAnn cp) => EntryPointsDerivation EpdNone cp where
   type EpdAllEntryPoints EpdNone cp = '[]
   type EpdLookupEntryPoint EpdNone cp = Fcf.ConstFn 'Nothing
-  epdNotes = starNotes
+  epdNotes = getTypeAnn @cp
   epdCall _ = EpConstructionFailed
+  epdDescs = RNil
diff --git a/src/Lorentz/EntryPoints/Doc.hs b/src/Lorentz/EntryPoints/Doc.hs
--- a/src/Lorentz/EntryPoints/Doc.hs
+++ b/src/Lorentz/EntryPoints/Doc.hs
@@ -1,13 +1,17 @@
 -- | Utilities for declaring and documenting entry points.
 module Lorentz.EntryPoints.Doc
   ( DEntryPoint (..)
+  , DEntryPointReference (..)
   , EntryArrow (..)
   , PlainEntryPointsKind
   , diEntryPointToMarkdown
   , DEntryPointArg (..)
   , DType (..)
   , DeriveCtorFieldDoc (..)
+  , ParamBuilder (..)
+  , ParamBuildingDesc (..)
   , ParamBuildingStep (..)
+  , mkPbsWrapIn
   , clarifyParamBuildingSteps
   , constructDEpArg
   , emptyDEpArg
@@ -18,32 +22,43 @@
   , documentEntryPoint
   , entryCase
   , entryCase_
+  , finalizeParamCallingDoc
+  , areFinalizedParamBuildingSteps
+  , entryCaseSimple_
+  , entryCaseSimple
+  , RequireFlatParamEps
+  , RequireFlatEpDerivation
   ) where
 
 import Control.Lens.Cons (_head)
 import Data.Char (toLower)
+import Data.Constraint (Dict(..))
 import qualified Data.Kind as Kind
-import Data.Singletons (sing)
 import Data.Vinyl.Core (RMap, Rec(..), rappend)
-import Data.Vinyl.Derived (Label)
-import Fmt (build)
+import Fmt (Buildable(..), listF)
 import GHC.Generics ((:+:))
 import qualified GHC.Generics as G
 import GHC.TypeLits (AppendSymbol, KnownSymbol, symbolVal)
+import qualified Text.Show
 
 import Lorentz.ADT
 import Lorentz.Base
-import Lorentz.Constraints.Scopes
+import Lorentz.Constraints
 import Lorentz.Doc
+import Lorentz.EntryPoints.Core
+import Lorentz.EntryPoints.Helpers
+import Lorentz.EntryPoints.Impl
 import Lorentz.TypeAnns
 import Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)
-import Michelson.Typed (mkUType)
+import Michelson.Typed (pattern DefEpName, EpName, mkUType)
 import Michelson.Typed.Doc
 import Michelson.Typed.Haskell.Doc
 import Michelson.Typed.Haskell.Instr
 import qualified Michelson.Untyped as Untyped
+import Util.Label (Label)
 import Util.Markdown
 import Util.Type
+import Util.TypeLits
 import Util.TypeTuple
 
 -- | Gathers information about single entrypoint.
@@ -74,41 +89,104 @@
   docItemSectionName = Just "Entrypoints"
   docItemToMarkdown = diEntryPointToMarkdown
 
--- | During incremental assembly of parameter building steps -
--- current representation of parameter.
-type CurrentParam = Markdown
+data DEntryPointReference = DEntryPointReference Text Anchor
 
+instance DocItem DEntryPointReference where
+  type DocItemPosition DEntryPointReference = 13
+  docItemSectionName = Nothing
+  docItemToMarkdown _ (DEntryPointReference name anchor) =
+    "Copies behaviour of " <>
+    mdLocalRef (mdTicked $ build name) anchor <>
+    " entrypoint."
+
+-- | When describing the way of parameter construction - piece of incremental
+-- builder for this description.
+newtype ParamBuilder = ParamBuilder
+  { unParamBuilder :: Markdown -> Markdown
+    -- ^ Argument stands for previously constructed parameter piece, and
+    -- returned value - a piece constructed after our step.
+  }
+
+-- | Show what given 'ParamBuilder' does on a sample.
+pbSample :: ParamBuilder -> Markdown
+pbSample (ParamBuilder b) = b "·"
+
+instance Buildable ParamBuilder where
+  build = pbSample
+
+instance Show ParamBuilder where
+  show (ParamBuilder pb) =
+    -- Using @'x'@ symbol here because unicode does not render well in 'show'
+    "ParamBuilder " <> show (pb "x")
+
+instance Eq ParamBuilder where
+  (==) = (==) `on` pbSample
+
+data ParamBuildingDesc = ParamBuildingDesc
+  { pbdEnglish :: Markdown
+    -- ^ Plain english description of this step.
+  , pbdHaskell :: ParamBuilder
+    -- ^ How to construct parameter in Haskell code.
+  , pbdMichelson :: ParamBuilder
+    -- ^ How to construct parameter working on raw Michelson.
+  } deriving stock (Show, Eq)
+
 -- | Describes a parameter building step.
 --
 -- This can be wrapping into (Haskell) constructor, or a more complex
 -- transformation.
-data ParamBuildingStep = ParamBuildingStep
-  { pbsEnglish :: Markdown
-    -- ^ Plain english description of this step.
-  , pbsHaskell :: CurrentParam -> Markdown
-    -- ^ How to construct parameter in Haskell code.
-  , pbsMichelson :: CurrentParam -> Markdown
-    -- ^ How to construct parameter working on raw Michelson.
-  }
+data ParamBuildingStep
+    -- | Wraps something into constructor with given name.
+    -- Constructor should be the one which corresponds to an entrypoint
+    -- defined via field annotation, for more complex cases use 'PbsCustom'.
+  = PbsWrapIn Text ParamBuildingDesc
+    -- | Directly call an entrypoint marked with a field annotation.
+  | PbsCallEntrypoint EpName
+    -- | Other action.
+  | PbsCustom ParamBuildingDesc
+    -- | This entrypoint cannot be called, which is possible when an explicit
+    -- default entrypoint is present. This is not a true entrypoint but just some
+    -- intermediate node in @or@ tree and neither it nor any of its parents
+    -- are marked with a field annotation.
+    --
+    -- It contains dummy 'ParamBuildingStep's which were assigned before
+    -- entrypoints were taken into account.
+  | PbsUncallable [ParamBuildingStep]
+  deriving stock (Show, Eq)
 
+instance Buildable ParamBuildingStep where
+  build = \case
+    PbsWrapIn ctor _desc -> "Wrap in `" <> build ctor <> "`"
+    PbsCallEntrypoint ep -> "Call entrypoint " <> build ep
+    PbsCustom desc -> "Custom: \"" <> pbdEnglish desc <> "\""
+    PbsUncallable steps -> "Uncallable; dummy steps: " <> listF steps
+
+-- | Make a 'ParamBuildingStep' that tells about wrapping an argument into
+-- a constructor with given name and uses given 'ParamBuilder' as description of
+-- Michelson part.
+mkPbsWrapIn :: Text -> ParamBuilder -> ParamBuildingStep
+mkPbsWrapIn ctorName michDesc =
+  PbsWrapIn ctorName ParamBuildingDesc
+    { pbdEnglish = "Wrap into " <> mdTicked (build ctorName) <> " constructor."
+    , pbdHaskell = ParamBuilder $ \p -> build ctorName <> " (" <> p <> ")"
+    , pbdMichelson = michDesc
+    }
+
 -- | Describes argument of an entrypoint.
 data DEntryPointArg =
   DEntryPointArg
   { epaArg :: Maybe DType
     -- ^ Argument of the entrypoint. Pass 'Nothing' if no argument is required.
-  , epaHasAnnotation :: Bool
-    -- ^ Whether this entrypoint has a field annotation (and thus is
-    -- callable using the standard "lightweigth entrypoints"
-    -- mechanism) or is a virtual entrypoint which requires
-    -- constructing a value of the full parameter type.
   , epaBuilding :: [ParamBuildingStep]
     -- ^ Describes a way to lift an entrypoint argument into full parameter
     -- which can be passed to the contract.
     --
-    -- Steps are supposed to be applied in the order in which they are given.
+    -- Steps are supposed to be applied in the order opposite to one in which
+    -- they are given.
     -- E.g. suppose that an entrypoint is called as @Run (Service1 arg)@;
-    -- then the first step should describe wrapping into @Service1@ constructor,
-    -- and the second step should be about wrapping into @Run@ constructor.
+    -- then the first step (actual last) should describe wrapping into @Run@
+    -- constructor, and the second step (actual first) should be about wrapping
+    -- into @Service1@ constructor.
   , epaType :: Untyped.Type
     -- ^ Untyped representation of entrypoint, used for printing its michelson
     -- type representation.
@@ -120,24 +198,22 @@
      , HasTypeAnn arg
      , KnownValue arg
      )
-  => Bool -> DEntryPointArg
-constructDEpArg epaHasAnnotation = DEntryPointArg
+  => DEntryPointArg
+constructDEpArg = DEntryPointArg
   { epaArg = Just $ DType (Proxy @arg)
-  , epaHasAnnotation = epaHasAnnotation
   , epaBuilding = []
   , epaType = mkDEpUType @arg
   }
 
-emptyDEpArg :: Bool -> DEntryPointArg
-emptyDEpArg epaHasAnnotation = DEntryPointArg
+emptyDEpArg :: DEntryPointArg
+emptyDEpArg = DEntryPointArg
   { epaArg = Nothing
-  , epaHasAnnotation = epaHasAnnotation
   , epaBuilding = []
   , epaType = Untyped.Type Untyped.TUnit Untyped.noAnn
   }
 
 mkDEpUType :: forall t. (KnownValue t, HasTypeAnn t) => Untyped.Type
-mkDEpUType = mkUType sing (getTypeAnn @t)
+mkDEpUType = mkUType (getTypeAnn @t)
 
 mkDEntryPointArgSimple
   :: forall t.
@@ -148,25 +224,33 @@
   => DEntryPointArg
 mkDEntryPointArgSimple = DEntryPointArg
   { epaArg = Just $ DType (Proxy @t)
-  , epaHasAnnotation = False
   , epaBuilding = []
   , epaType = mkDEpUType @t
   }
 
 -- | Go over contract code and update every occurrence of 'DEntryPointArg'
+-- documentation item, modifying param building steps.
+modifyParamBuildingSteps
+  :: ([ParamBuildingStep] -> [ParamBuildingStep])
+  -> (inp :-> out)
+  -> (inp :-> out)
+modifyParamBuildingSteps f =
+  iMapAnyCode $
+  modifyInstrDoc (\di -> Just di{ epaBuilding = f (epaBuilding di) })
+
+-- | Go over contract code and update every occurrence of 'DEntryPointArg'
 -- documentation item, adding the given step to its "how to build parameter"
 -- description.
 clarifyParamBuildingSteps :: ParamBuildingStep -> (inp :-> out) -> (inp :-> out)
 clarifyParamBuildingSteps pbs =
-  iMapAnyCode $
-  modifyInstrDoc (\di -> di{ epaBuilding = epaBuilding di ++ [pbs] })
+  modifyParamBuildingSteps (pbs :)
 
 instance DocItem DEntryPointArg where
   type DocItemPosition DEntryPointArg = 20
   docItemSectionName = Nothing
-  docItemDependencies (DEntryPointArg mdty _ _ _) =
+  docItemDependencies (DEntryPointArg mdty _ _) =
     [SomeDocDefinitionItem dty | Just dty <- pure mdty]
-  docItemToMarkdown _ (DEntryPointArg mdty hasAnnotation psteps et) =
+  docItemToMarkdown _ (DEntryPointArg mdty psteps et) =
     mconcat . Prelude.map (<> "\n\n") $
       [ mdSubsection "Argument" $
           case mdty of
@@ -182,37 +266,39 @@
               ],
           mdSpoiler "How to call this entrypoint" $
             "\n0. Construct an argument for the entrypoint.\n" <>
-            mconcat howToCall
+            howToCall
       ]
     where
-      howToCall
-        | hasAnnotation = howToCallAnnotatedEntrypoint
-        | otherwise = howToCallVirtualEntrypoint
-
-      -- TODO: currently we always set @hasAnnotation@ to @True@,
-      -- hence this case in unreachable.  It is still useful, we
-      -- should set @hasAnnotation@ properly and improve handling of
-      -- this case.  Specifically, for virtual entrypoints we should
-      -- wrap them into constructors until we reach one having a field
-      -- annotation. As soon as it is reached, we can call the
-      -- contract by an entrypoint name.
-      howToCallVirtualEntrypoint =
-        [ mconcat . Prelude.intersperse "\n" $
-            psteps <&> \ParamBuildingStep{..} ->
-              mconcat . Prelude.intersperse "\n" $
-              [ -- Markdown re-enumerates enumerated lists automatically
-                "1. " <> pbsEnglish
-              , "  + " <>
-                mdSubsection "In Haskell" (mdTicked $ pbsHaskell "·")
-              , "  + " <>
-                mdSubsection "In Michelson" (mdTicked $ pbsMichelson "·")
-              ]
-        , "\n\nPass resulting value as parameter to the contract.\n"
-        ]
+      howToCall =
+        mconcat . Prelude.intersperse "\n" $
+        -- Markdown re-enumerates enumerated lists automatically
+        Prelude.map ("1. " <>) $
+          reverse psteps <&> \case
+            PbsWrapIn _ pbd ->
+              renderPbDesc pbd
+            PbsCallEntrypoint ep -> case ep of
+              DefEpName ->
+                "Call the contract (default entrypoint) with the constructed \
+                \argument."
+              _ ->
+                "Call contract's " <> mdTicked (build ep) <> " entrypoint \
+                \passing the constructed argument."
+            PbsCustom pbd ->
+              renderPbDesc pbd
+            PbsUncallable _ ->
+              "Feel sad: this entrypoint *cannot* be called and is enlisted \
+              \here only to describe the parameter structure."
+              -- We could hide such entrypoints, but then in case of incorrect
+              -- use of 'entryCase's or a bug in documentation, understanding
+              -- what's going on would be hard
 
-      howToCallAnnotatedEntrypoint =
-        [ "1. Make a transfer to the contract passing this entrypoint's name " <>
-          "and the constructed value as an argument."
+      renderPbDesc ParamBuildingDesc{..} =
+        mconcat . Prelude.intersperse "\n" $
+        [ pbdEnglish
+        , "    + " <>
+          mdSubsection "In Haskell" (mdTicked $ pbSample pbdHaskell)
+        , "    + " <>
+          mdSubsection "In Michelson" (mdTicked $ pbSample pbdMichelson)
         ]
 
 -- | Pick a type documentation from 'CtorField'.
@@ -224,14 +310,14 @@
   =>
     DeriveCtorFieldDoc con 'NoFields
   where
-  deriveCtorFieldDoc = emptyDEpArg True
+  deriveCtorFieldDoc = emptyDEpArg
 
 instance
     (TypeHasDoc ty, HasTypeAnn ty, KnownValue ty, KnownSymbol con)
   =>
     DeriveCtorFieldDoc con ('OneField ty)
   where
-  deriveCtorFieldDoc = constructDEpArg @ty True
+  deriveCtorFieldDoc = constructDEpArg @ty
 
 -- | Add necessary documentation to entry points.
 documentEntryPoints
@@ -239,7 +325,7 @@
      DocumentEntryPoints kind a
   => Rec (CaseClauseL inp out) (CaseClauses a)
   -> Rec (CaseClauseL inp out) (CaseClauses a)
-documentEntryPoints = gDocumentEntryPoints @kind @(G.Rep a) id
+documentEntryPoints = gDocumentEntryPoints @kind @(G.Rep a) (ParamBuilder id)
 
 -- | Constraint for 'documentEntryPoints'.
 type DocumentEntryPoints kind a =
@@ -253,7 +339,7 @@
   --
   -- First argument is accumulator for Michelson description of the building step.
   gDocumentEntryPoints
-    :: (Markdown -> Markdown)
+    :: ParamBuilder
     -> Rec (CaseClauseL inp out) (GCaseClauses x)
     -> Rec (CaseClauseL inp out) (GCaseClauses x)
 
@@ -264,14 +350,14 @@
          , RSplit (GCaseClauses x) (GCaseClauses y)
          ) =>
          GDocumentEntryPoints kind (x :+: y) where
-  gDocumentEntryPoints michDesc clauses =
+  gDocumentEntryPoints (ParamBuilder michDesc) clauses =
     let (lclauses, rclauses) = rsplit @CaseClauseParam @(GCaseClauses x) clauses
     in gDocumentEntryPoints @kind @x
-         (\a -> michDesc $ "Left (" <> a <> ")")
+         (ParamBuilder $ \a -> michDesc $ "Left (" <> a <> ")")
          lclauses
        `rappend`
        gDocumentEntryPoints @kind @y
-         (\a -> michDesc $ "Right (" <> a <> ")")
+         (ParamBuilder $ \a -> michDesc $ "Right (" <> a <> ")")
          rclauses
 
 instance ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
@@ -282,25 +368,22 @@
          GDocumentEntryPoints kind (G.C1 ('G.MetaCons ctor _1 _2) x) where
   gDocumentEntryPoints michDesc (CaseClauseL clause :& RNil) =
     let entryPointName = toText $ symbolVal (Proxy @ctor)
-        psteps = ParamBuildingStep
-          { pbsEnglish = "Wrap into " <> mdTicked (build entryPointName) <> " constructor."
-          , pbsHaskell = \p -> build entryPointName <> " (" <> p <> ")"
-          , pbsMichelson = michDesc
-          }
+        psteps = mkPbsWrapIn entryPointName michDesc
         addDoc instr =
           clarifyParamBuildingSteps psteps $
           docGroup (SomeDocItem . DEntryPoint @kind entryPointName) $
           doc (deriveCtorFieldDoc @ctor @cf) # instr
     in CaseClauseL (addDoc clause) :& RNil
 
--- | Like 'case_', to be used for pattern-matching on parameter.
+-- | Like 'case_', to be used for pattern-matching on a parameter
+-- or its part.
 --
 -- Modifies documentation accordingly. Including description of
 -- entrypoints' arguments, thus for them you will need to supply
 -- 'TypeHasDoc' instance.
 entryCase_
   :: forall dt entryPointKind out inp.
-     ( InstrCaseC dt inp out
+     ( InstrCaseC dt
      , RMap (CaseClauses dt)
      , DocumentEntryPoints entryPointKind dt
      )
@@ -335,7 +418,7 @@
 documentEntryPoint instr =
   let entryPointName = toText $ symbolVal (Proxy @epName) in
     docGroup (SomeDocItem . DEntryPoint @kind entryPointName) $
-    doc (constructDEpArg @param True) # instr
+    doc (constructDEpArg @param) # instr
 
 -- | Provides arror for convenient entrypoint documentation
 class EntryArrow kind name body where
@@ -353,3 +436,125 @@
          , KnownValue param
          ) => EntryArrow kind name body where
   (#->) _ = documentEntryPoint @kind @epName
+
+-- | Modify param building steps with respect to entrypoints that given
+-- parameter declares.
+--
+-- Each contract with entrypoints should eventually call this function,
+-- otherwise, in case if contract uses built-in entrypoints feature,
+-- the resulting parameter building steps in the generated documentation
+-- will not consider entrypoints and thus may be incorrect.
+--
+-- Calling this twice over the same code is also prohibited.
+finalizeParamCallingDoc
+  :: forall cp inp out.
+     (NiceParameterFull cp, RequireSumType cp, HasCallStack)
+  => (cp : inp :-> out) -> (cp : inp :-> out)
+finalizeParamCallingDoc = modifyParamBuildingSteps modifySteps
+  where
+    -- We do not actually need it, requiring this constraint only to avoid
+    -- misapplication of our function.
+    _needSumType :: Dict (RequireSumType cp)
+    _needSumType = Dict
+
+    epDescs :: [Some1 EpCallingDesc]
+    epDescs =
+      -- Reversing the list because if element @e1@ of this list is prefix of
+      -- another element @e2@, we want @e2@ to appear eariler than @e1@ to
+      -- match against it first. But without reverse exactly the opposite
+      -- holds due to [order of entrypoints children] property.
+      reverse $ pepDescsWithDef @cp
+
+    modifySteps :: [ParamBuildingStep] -> [ParamBuildingStep]
+    modifySteps pbs
+      | areFinalizedParamBuildingSteps pbs =
+          error "Applying finalization second time"
+      | otherwise =
+          fromMaybe [PbsUncallable pbs] . listToMaybe . catMaybes $
+          epDescs <&> \epDesc -> tryShortcut epDesc pbs
+
+    -- Further we check whether given 'EpCallingStep's form prefix of
+    -- 'ParamBuildingStep's; if so, we can apply only part of building
+    -- steps and then call the entrypoint directly
+
+    match :: [EpCallingStep] -> [ParamBuildingStep] -> Bool
+    match cSteps pbSteps =
+      and $ zip cSteps (prolong pbSteps) <&> \case
+        (EpsWrapIn ctor, Just (PbsWrapIn ctor2 _)) | ctor == ctor2 -> True
+        _ -> False
+      where
+        prolong :: [a] -> [Maybe a]
+        prolong l = map Just l ++ repeat Nothing
+
+    tryShortcut
+      :: Some1 EpCallingDesc
+      -> [ParamBuildingStep]
+      -> Maybe [ParamBuildingStep]
+    tryShortcut (Some1 EpCallingDesc{ epcdSteps = cSteps, epcdEntrypoint = ep })
+                pbSteps
+      | match cSteps pbSteps =
+          let truncated = drop (length cSteps) pbSteps
+              callEpStep = PbsCallEntrypoint ep
+          in Just $ callEpStep : truncated
+      | otherwise = Nothing
+
+-- | Whether 'finalizeParamCallingDoc' has already been applied to these steps.
+areFinalizedParamBuildingSteps :: [ParamBuildingStep] -> Bool
+areFinalizedParamBuildingSteps =
+  -- Currently, 'finalizeParamCallingDoc' puts either 'PbsCallEntrypoint' or
+  -- 'PbsUncallable' to list, and only it, and we rely on this behaviour here.
+  -- If something changes so that these heuristics do not work, we can always
+  -- insert special markers which would tell us whether finalization has been
+  -- applied.
+  let
+    hasFinalizationTraces = \case
+      PbsWrapIn{} -> False
+      PbsCallEntrypoint{} -> True
+      PbsCustom{} -> False
+      PbsUncallable{} -> True
+  in any hasFinalizationTraces
+
+entryCaseSimple_
+  :: forall cp out inp.
+     ( InstrCaseC cp
+     , RMap (CaseClauses cp)
+     , DocumentEntryPoints PlainEntryPointsKind cp
+     , NiceParameterFull cp
+     , RequireFlatParamEps cp
+     )
+  => Rec (CaseClauseL inp out) (CaseClauses cp)
+  -> cp & inp :-> out
+entryCaseSimple_ =
+  finalizeParamCallingDoc . entryCase_ (Proxy @PlainEntryPointsKind)
+  where
+    _reqFlat = Dict @(RequireFlatEpDerivation cp (GetParameterEpDerivation cp))
+
+-- | Version of 'entryCase' for contracts with flat parameter, use it when you
+-- need only one 'entryCase' all over the contract implementation.
+--
+-- This method calls 'finalizeParamCallingDoc' inside.
+entryCaseSimple
+  :: forall cp out inp clauses.
+     ( CaseTC cp out inp clauses
+     , DocumentEntryPoints PlainEntryPointsKind cp
+     , NiceParameterFull cp
+     , RequireFlatParamEps cp
+     )
+  => IsoRecTuple clauses -> cp & inp :-> out
+entryCaseSimple = entryCaseSimple_ . recFromTuple
+
+type family RequireFlatParamEps cp :: Constraint where
+  RequireFlatParamEps cp =
+    ( RequireFlatEpDerivation cp (GetParameterEpDerivation cp)
+    , RequireSumType cp
+    )
+
+-- Checking this is not strictly necessary, but let's try it
+type family RequireFlatEpDerivation cp deriv :: Constraint where
+  RequireFlatEpDerivation _ EpdNone = ()
+  RequireFlatEpDerivation _ EpdPlain = ()
+  RequireFlatEpDerivation cp deriv = TypeError
+    ( 'Text "Parameter is not flat" ':$$:
+      'Text "For parameter `" ':<>: 'ShowType cp ':<>: 'Text "`" ':$$:
+      'Text "With entrypoints derivation way `" ':<>: 'ShowType deriv ':<>: 'Text "`"
+    )
diff --git a/src/Lorentz/EntryPoints/Helpers.hs b/src/Lorentz/EntryPoints/Helpers.hs
--- a/src/Lorentz/EntryPoints/Helpers.hs
+++ b/src/Lorentz/EntryPoints/Helpers.hs
@@ -1,5 +1,6 @@
 module Lorentz.EntryPoints.Helpers
   ( ctorNameToAnn
+  , ctorNameToEp
   , CanHaveEntryPoints
   , ShouldHaveEntryPoints (..)
   , RequireSumType
@@ -9,7 +10,7 @@
 
 import Michelson.Typed.Haskell
 import Michelson.Typed.T
-import Michelson.Untyped (FieldAnn, ann)
+import Michelson.Untyped (EpName, FieldAnn, ann, epNameFromParamAnn)
 import Util.Text
 import Util.Type
 import Util.TypeLits
@@ -17,6 +18,11 @@
 ctorNameToAnn :: forall ctor. (KnownSymbol ctor, HasCallStack) => FieldAnn
 ctorNameToAnn = ann . headToLower $ (symbolValT' @ctor)
 
+ctorNameToEp :: forall ctor. (KnownSymbol ctor, HasCallStack) => EpName
+ctorNameToEp =
+  epNameFromParamAnn (ctorNameToAnn @ctor)
+  ?: error "Empty constructor-entrypoint name"
+
 -- | A special type which wraps over a primitive type and states that it has
 -- entrypoints (one).
 --
@@ -43,4 +49,6 @@
   RequireSumType a =
     If (CanHaveEntryPoints a)
        (() :: Constraint)
-       (TypeError ('Text "Expected Michelson sum type"))
+       (TypeError ('Text "Expected Michelson sum type" ':$$:
+                   'Text "In type `" ':<>: 'ShowType a ':<>: 'Text "`"
+                  ))
diff --git a/src/Lorentz/EntryPoints/Impl.hs b/src/Lorentz/EntryPoints/Impl.hs
--- a/src/Lorentz/EntryPoints/Impl.hs
+++ b/src/Lorentz/EntryPoints/Impl.hs
@@ -1,30 +1,38 @@
 -- | Common implementations of entrypoints.
 module Lorentz.EntryPoints.Impl
-  ( EpdPlain
+  ( -- * Ways to implement 'ParameterHasEntryPoints'
+    EpdPlain
   , EpdRecursive
   , EpdDelegate
+
+  -- * Implementation details
+  , PlainEntryPointsC
+  , EPTree (..)
+  , BuildEPTree
   ) where
 
 import qualified Data.Kind as Kind
-import Data.Singletons (SingI (..))
-import Data.Singletons.Prelude (Sing (STrue, SFalse))
+import Data.Singletons (SingI(..))
+import Data.Singletons.Prelude (Sing(SFalse, STrue))
 import Data.Singletons.Prelude.Eq ((%==))
 import Data.Type.Bool (If)
+import Data.Vinyl.Core (Rec(..), (<+>))
+import Data.Vinyl.Recursive (rmap)
+import Fcf (Eval, Exp)
+import qualified Fcf
 import qualified GHC.Generics as G
 import Util.TypeLits
-import Fcf (Exp, Eval)
-import qualified Fcf
 
+import Lorentz.Value
 import Michelson.Typed
 import Michelson.Typed.Haskell.Instr.Sum (IsPrimitiveValue)
 import Michelson.Typed.Haskell.Value (GValueType, GenericIsoValue)
 import Michelson.Untyped (FieldAnn, noAnn)
-import Lorentz.Value
+import Util.Fcf (type (<|>), Over2, TyEqSing)
 import Util.Type
-import Util.Fcf (Over2, type (<|>), TyEqSing)
 
-import Lorentz.EntryPoints.Helpers
 import Lorentz.EntryPoints.Core
+import Lorentz.EntryPoints.Helpers
 import Lorentz.TypeAnns
 
 -- | Implementation of 'ParameterHasEntryPoints' which fits for case when
@@ -41,6 +49,7 @@
   type EpdLookupEntryPoint EpdPlain cp = PlainLookupEntryPointExt EpdPlain cp
   epdNotes = plainEpdNotesExt @EpdPlain @cp
   epdCall = plainEpdCallExt @EpdPlain @cp
+  epdDescs = plainEpdDescsExt @EpdPlain @cp
 
 -- | Extension of 'EpdPlain' on parameters being defined as several nested
 -- datatypes.
@@ -61,6 +70,7 @@
   type EpdLookupEntryPoint EpdRecursive cp = PlainLookupEntryPointExt EpdRecursive cp
   epdNotes = plainEpdNotesExt @EpdRecursive @cp
   epdCall = plainEpdCallExt @EpdRecursive @cp
+  epdDescs = plainEpdDescsExt @EpdRecursive @cp
 
 -- | Extension of 'EpdPlain' on parameters being defined as several nested
 -- datatypes.
@@ -83,6 +93,7 @@
   type EpdLookupEntryPoint EpdDelegate cp = PlainLookupEntryPointExt EpdDelegate cp
   epdNotes = plainEpdNotesExt @EpdDelegate @cp
   epdCall = plainEpdCallExt @EpdDelegate @cp
+  epdDescs = plainEpdDescsExt @EpdDelegate @cp
 
 type PlainAllEntryPointsExt mode cp = AllEntryPoints mode (BuildEPTree mode cp) cp
 
@@ -96,11 +107,17 @@
 
 plainEpdCallExt
   :: forall mode cp name.
-     (PlainEntryPointsC mode cp, ParameterScope (ToT cp), KnownSymbol name)
+     (PlainEntryPointsC mode cp, ParameterScope (ToT cp))
   => Label name
   -> EpConstructionRes (ToT cp) (Eval (LookupEntryPoint mode (BuildEPTree mode cp) cp name))
 plainEpdCallExt = mkEpLiftSequence @mode @(BuildEPTree mode cp) @cp
 
+plainEpdDescsExt
+  :: forall mode cp.
+     (PlainEntryPointsC mode cp)
+  => Rec EpCallingDesc (PlainAllEntryPointsExt mode cp)
+plainEpdDescsExt = mkEpDescs @mode @(BuildEPTree mode cp) @cp
+
 type PlainEntryPointsC mode cp =
   ( GenericIsoValue cp
   , EntryPointsNotes mode (BuildEPTree mode cp) cp
@@ -162,12 +179,19 @@
 mkEpLiftSequence
   :: forall mode ep a name.
       ( EntryPointsNotes mode ep a, ParameterScope (ToT a)
-      , GenericIsoValue a, KnownSymbol name
+      , GenericIsoValue a
       )
   => Label name
   -> EpConstructionRes (ToT a) (Eval (LookupEntryPoint mode ep a name))
 mkEpLiftSequence = gMkEpLiftSequence @mode @ep @(G.Rep a)
 
+-- | Makes up descriptions of entrypoints calling.
+mkEpDescs
+  :: forall mode ep a.
+      (EntryPointsNotes mode ep a)
+  => Rec EpCallingDesc (AllEntryPoints mode ep a)
+mkEpDescs = gMkDescs @mode @ep @(G.Rep a)
+
 -- | Fetches information about all entrypoints - leaves of 'Or' tree.
 type AllEntryPoints mode ep a = GAllEntryPoints mode ep (G.Rep a)
 
@@ -186,15 +210,19 @@
   gMkEntryPointsNotes :: HasCallStack => (Notes (GValueType x), FieldAnn)
 
   gMkEpLiftSequence
-    :: (KnownSymbol name, ParameterScope (GValueType x))
+    :: ParameterScope (GValueType x)
     => Label name
     -> EpConstructionRes (GValueType x) (Eval (GLookupEntryPoint mode ep x name))
 
+  gMkDescs
+    :: Rec EpCallingDesc (GAllEntryPoints mode ep x)
+
 instance GEntryPointsNotes mode ep x => GEntryPointsNotes mode ep (G.D1 i x) where
   type GAllEntryPoints mode ep (G.D1 i x) = GAllEntryPoints mode ep x
   type GLookupEntryPoint mode ep (G.D1 i x) = GLookupEntryPoint mode ep x
   gMkEntryPointsNotes = gMkEntryPointsNotes @mode @ep @x
   gMkEpLiftSequence = gMkEpLiftSequence @mode @ep @x
+  gMkDescs = gMkDescs @mode @ep @x
 
 instance (GEntryPointsNotes mode epx x, GEntryPointsNotes mode epy y) =>
          GEntryPointsNotes mode ('EPNode epx epy) (x G.:+: y) where
@@ -216,6 +244,8 @@
               case gMkEpLiftSequence @mode @epy @y label of
                 EpConstructed liftSeq -> EpConstructed (EplWrapRight liftSeq)
                 EpConstructionFailed -> EpConstructionFailed
+  gMkDescs =
+    gMkDescs @mode @epx @x <+> gMkDescs @mode @epy @y
 
 instance ( GHasTypeAnn x, KnownSymbol ctor
          , ToT (GExtractField x) ~ GValueType x
@@ -227,12 +257,18 @@
     JustOnEq ctor (GExtractField x)
   gMkEntryPointsNotes =
     (gGetTypeAnn @x, ctorNameToAnn @ctor)
-  gMkEpLiftSequence (_ :: Label name) =
+  gMkEpLiftSequence (Label :: Label name) =
     case sing @ctor %== sing @name of
       STrue -> EpConstructed EplArgHere
       SFalse -> EpConstructionFailed
+  gMkDescs = addDescStep @ctor $
+    EpCallingDesc
+    { epcdArg = Proxy
+    , epcdEntrypoint = ctorNameToEp @ctor
+    , epcdSteps = []
+    } :& RNil
 
-instance (ep ~ 'EPNode epx epy, GEntryPointsNotes mode ep x) =>
+instance (ep ~ 'EPNode epx epy, GEntryPointsNotes mode ep x, KnownSymbol ctor) =>
          GEntryPointsNotes mode ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) where
   type GAllEntryPoints mode ('EPNode epx epy) (G.C1 ('G.MetaCons ctor _1 _2) x) =
     GAllEntryPoints mode ('EPNode epx epy) x
@@ -240,6 +276,7 @@
     GLookupEntryPoint mode ('EPNode epx epy) x
   gMkEntryPointsNotes = gMkEntryPointsNotes @mode @ep @x
   gMkEpLiftSequence = gMkEpLiftSequence @mode @ep @x
+  gMkDescs = addDescStep @ctor $ gMkDescs @mode @ep @x
 
 instance ( ep ~ 'EPDelegate, GEntryPointsNotes mode ep x
          , KnownSymbol ctor, ToT (GExtractField x) ~ GValueType x
@@ -252,16 +289,23 @@
   gMkEntryPointsNotes =
     let (notes, _rootAnn) = gMkEntryPointsNotes @mode @ep @x
     in (notes, ctorNameToAnn @ctor)
-  gMkEpLiftSequence (label :: Label name) =
+  gMkEpLiftSequence label@(Label :: Label name) =
     case sing @ctor %== sing @name of
       STrue -> EpConstructed EplArgHere
       SFalse -> gMkEpLiftSequence @mode @ep @x label
+  gMkDescs = addDescStep @ctor $
+    EpCallingDesc
+    { epcdArg = Proxy
+    , epcdEntrypoint = ctorNameToEp @ctor
+    , epcdSteps = []
+    } :& gMkDescs @mode @ep @x
 
 instance GEntryPointsNotes mode ep x => GEntryPointsNotes mode ep (G.S1 i x) where
   type GAllEntryPoints mode ep (G.S1 i x) = GAllEntryPoints mode ep x
   type GLookupEntryPoint mode ep (G.S1 i x) = GLookupEntryPoint mode ep x
   gMkEntryPointsNotes = gMkEntryPointsNotes @mode @ep @x
   gMkEpLiftSequence = gMkEpLiftSequence @mode @ep @x
+  gMkDescs = gMkDescs @mode @ep @x
 
 instance (EntryPointsNotes EpdRecursive ep a, GenericIsoValue a) =>
          GEntryPointsNotes EpdRecursive ep (G.Rec0 a) where
@@ -269,6 +313,7 @@
   type GLookupEntryPoint EpdRecursive ep (G.Rec0 a) = LookupEntryPoint EpdRecursive ep a
   gMkEntryPointsNotes = (mkEntryPointsNotes @EpdRecursive @ep @a, noAnn)
   gMkEpLiftSequence = mkEpLiftSequence @EpdRecursive @ep @a
+  gMkDescs = mkEpDescs @EpdRecursive @ep @a
 
 instance (ParameterDeclaresEntryPoints a) =>
          GEntryPointsNotes EpdDelegate 'EPDelegate (G.Rec0 a) where
@@ -277,12 +322,14 @@
   gMkEntryPointsNotes = (pepNotes @a, noAnn)
   -- TODO [#35]: should use field ann ^^^^^ returned by 'epdNotes'
   gMkEpLiftSequence = pepCall @a
+  gMkDescs = pepDescs @a
 
 instance GEntryPointsNotes mode 'EPLeaf G.U1 where
   type GAllEntryPoints mode 'EPLeaf G.U1 = '[]
   type GLookupEntryPoint mode 'EPLeaf G.U1 = Fcf.ConstFn 'Nothing
   gMkEntryPointsNotes = (starNotes, noAnn)
   gMkEpLiftSequence _ = EpConstructionFailed
+  gMkDescs = RNil
 
 instance Each [Typeable, SingI] [GValueType x, GValueType y] =>
          GEntryPointsNotes mode 'EPLeaf (x G.:*: y) where
@@ -290,6 +337,7 @@
   type GLookupEntryPoint mode 'EPLeaf (x G.:*: y) = Fcf.ConstFn 'Nothing
   gMkEntryPointsNotes = (starNotes, noAnn)
   gMkEpLiftSequence _ = EpConstructionFailed
+  gMkDescs = RNil
 
 -- Return 'Just' iff given entries of type @k1@ are equal.
 type family JustOnEq (a :: k1) (b :: k2) :: k1 -> Exp (Maybe k2) where
@@ -304,3 +352,12 @@
   GExtractField (G.S1 _ x) = GExtractField x
   GExtractField (G.Rec0 a) = a
   GExtractField G.U1 = ()
+
+addDescStep
+  :: forall ctor eps.
+      KnownSymbol ctor
+  => Rec EpCallingDesc eps -> Rec EpCallingDesc eps
+addDescStep =
+  let step = EpsWrapIn $ symbolValT' @ctor
+  in rmap $ \EpCallingDesc{..} ->
+       EpCallingDesc{ epcdSteps = step : epcdSteps, .. }
diff --git a/src/Lorentz/EntryPoints/Manual.hs b/src/Lorentz/EntryPoints/Manual.hs
--- a/src/Lorentz/EntryPoints/Manual.hs
+++ b/src/Lorentz/EntryPoints/Manual.hs
@@ -29,6 +29,7 @@
     EpdLookupEntryPoint deriv cp
   epdNotes = epdNotes @deriv @cp
   epdCall = epdCall @deriv @cp
+  epdDescs = epdDescs @deriv @cp
 
 instance ( NiceParameter cp
          , EntryPointsDerivation epd cp
diff --git a/src/Lorentz/Errors.hs b/src/Lorentz/Errors.hs
--- a/src/Lorentz/Errors.hs
+++ b/src/Lorentz/Errors.hs
@@ -10,6 +10,7 @@
   , isoErrorFromVal
   , ErrorHasDoc (..)
   , typeDocMdDescriptionReferToError
+  , customErrorDocHaskellRepGeneral
 
   , UnspecifiedError (..)
 
@@ -38,7 +39,9 @@
   , CustomErrorNoIsoValue
   , deriveCustomError
 
-  , errorsDocumentation
+    -- * Internals
+  , errorTagToText
+  , errorTagToMText
   ) where
 
 import qualified Data.Char as C
@@ -48,7 +51,6 @@
 import Data.Singletons (SingI(..), demote)
 import Data.Type.Equality (type (==))
 import Data.Typeable (cast)
-import Data.Vinyl.Derived (Label)
 import Fmt (Buildable, build, fmt, pretty, (+|), (+||), (|+), (||+))
 import GHC.TypeLits (ErrorMessage(..), KnownSymbol, Symbol, TypeError, symbolVal)
 import qualified Language.Haskell.TH as TH
@@ -65,6 +67,7 @@
 import Michelson.Typed.Sing
 import Michelson.Typed.T
 import Michelson.Typed.Value
+import Util.Label (Label)
 import Util.Markdown
 import Util.Type
 import Util.Typeable
@@ -104,7 +107,7 @@
   => Value t -> Either Text e
 isoErrorFromVal e = fromVal <$> gcastE e
 
-class ErrorHasDoc e where
+class Typeable e => ErrorHasDoc (e :: Kind.Type) where
   -- | Name of error as it appears in the corresponding section title.
   errorDocName :: Text
 
@@ -128,6 +131,23 @@
   -- | Which definitions documentation for this error mentions.
   errorDocDependencies :: [SomeDocDefinitionItem]
 
+  -- | Constraints which we require in a particular instance.
+  -- You are not oblidged to often instantiate this correctly, it is only useful
+  -- for some utilities.
+  type ErrorRequirements e :: Constraint
+  type ErrorRequirements e = ()
+
+  -- | Captured constraints which we require in a particular instance.
+  -- This is a way to encode a bidirectional instance in the nowaday Haskell,
+  -- for @class MyConstraint => ErrorHasDoc MyType@ instance it lets deducing
+  -- @MyConstraint@ by @ErrorHasDoc MyType@.
+  --
+  -- You are not oblidged to always instantiate, it is only useful for some
+  -- utilities which otherwise would not compile.
+  errorDocRequirements :: Dict (ErrorRequirements e)
+  default errorDocRequirements :: ErrorRequirements e => Dict (ErrorRequirements e)
+  errorDocRequirements = Dict
+
 -- | Helper for managing descriptions.
 pickFirstSentence :: Markdown -> Markdown
 pickFirstSentence = build . toText . go . fmt
@@ -151,7 +171,7 @@
 instance ErrorHasDoc MText where
   errorDocName = "InternalError"
   errorDocMdCause =
-    "Internal error occured."
+    "Some internal error occured."
   errorDocHaskellRep =
     "Textual error message, see " <>
     typeDocMdReference (Proxy @MText) (WithinParens False) <> "."
@@ -216,6 +236,8 @@
 Note that this relation is defined globally rather than on per-contract basis,
 so define errors accordingly. If your error has argument specific to your
 contract, call it such that error name reflects its belonging to this contract.
+
+This is the basic [error format].
 -}
 
 {- About global registry of errors:
@@ -289,24 +311,36 @@
   errorDocMdCauseInEntrypoint = customErrDocMdCauseInEntrypoint @tag
   errorDocClass = customErrClass @tag
   errorDocHaskellRep =
-    let hasArg = demote @(ToT (ErrorArg tag)) /= TUnit
-        name = build $ errorTagToText @tag
-    in mconcat $ catMaybes
-      [ Just $
-          ( if hasArg
-            then mdTicked ("(\"" <> name <> "\", " <> "<error argument>" <> ")")
-            else mdTicked ("(\"" <> name <> "\", ())")
-          ) <> "."
-      , guard hasArg $>
-          ("\n\nProvided error argument will be of type "
-          <> typeDocMdReference (Proxy @(ErrorArg tag)) (WithinParens False)
-          <> (maybe "" (\txt -> " and stand for " <> txt) (customErrArgumentSemantics @tag))
-          <> "."
-          )
-      ]
+    customErrorDocHaskellRepGeneral (show $ errorTagToText @tag) (Proxy @tag)
 
+  type ErrorRequirements (CustomError tag) = (CustomErrorHasDoc tag, SingI (ToT (ErrorArg tag)))
+  errorDocRequirements = Dict
+
+-- | Description of error representation in Haskell.
+customErrorDocHaskellRepGeneral
+  :: ( SingI (ToT (ErrorArg tag)), IsError (CustomError tag)
+     , TypeHasDoc (ErrorArg tag), CustomErrorHasDoc tag
+     )
+  => Text -> Proxy tag -> Markdown
+customErrorDocHaskellRepGeneral tagName (_ :: Proxy tag) =
+  let hasArg = demote @(ToT (ErrorArg tag)) /= TUnit
+      tagName' = build tagName
+  in mconcat $ catMaybes
+    [ Just $
+        ( if hasArg
+          then mdTicked ("(" <> tagName' <> ", " <> "<error argument>" <> ")")
+          else mdTicked ("(" <> tagName' <> ", ())")
+        ) <> "."
+    , guard hasArg $>
+        ("\n\nProvided error argument will be of type "
+        <> typeDocMdReference (Proxy @(ErrorArg tag)) (WithinParens False)
+        <> (maybe "" (\txt -> " and stand for " <> txt) (customErrArgumentSemantics @tag))
+        <> "."
+        )
+    ]
+
 -- | Demote error tag to term level.
-errorTagToMText :: KnownSymbol tag => Label tag -> MText
+errorTagToMText :: Label tag -> MText
 errorTagToMText l =
   -- Now tags come not from constructor names, but from labels,
   -- we have to lead the first letter to upper case to preserve
@@ -379,7 +413,8 @@
     reifyTypeEquality @arg @() $
       errorFromVal v <&> \(CustomError l ()) -> CustomError l
 
-instance ErrorHasDoc (CustomError tag) => ErrorHasDoc (arg -> CustomError tag) where
+instance (Typeable arg, ErrorHasDoc (CustomError tag)) =>
+         ErrorHasDoc (arg -> CustomError tag) where
   errorDocName = errorDocName @(CustomError tag)
   errorDocMdCauseInEntrypoint = errorDocMdCauseInEntrypoint @(CustomError tag)
   errorDocMdCause = errorDocMdCause @(CustomError tag)
@@ -461,7 +496,7 @@
 
 -- | Mentions that contract uses given error.
 data DError where
-  DError :: IsError e => Proxy e -> DError
+  DError :: ErrorHasDoc e => Proxy e -> DError
 
 instance Eq DError where
   DError e1 == DError e2 = e1 `eqParam1` e2
@@ -487,16 +522,16 @@
     ]
   docItemDependencies (DError (_ :: Proxy e)) = errorDocDependencies @e
 
-errorDocMdReference :: forall e. IsError e => Markdown
+errorDocMdReference :: forall e. ErrorHasDoc e => Markdown
 errorDocMdReference =
-  let DocItemRef (DocItemId anchor) = docItemRef $ DError (Proxy @e)
-  in mdLocalRef (mdTicked . build $ errorDocName @e) anchor
+  let DocItemRef docItemId = docItemRef $ DError (Proxy @e)
+  in mdLocalRef (mdTicked . build $ errorDocName @e) docItemId
 
 -- | Documentation for custom errors.
 
 -- | Mentions that entrypoint throws given error.
 data DThrows where
-  DThrows :: IsError e => Proxy e -> DThrows
+  DThrows :: ErrorHasDoc e => Proxy e -> DThrows
 
 instance Eq DThrows where
   DThrows e1 == DThrows e2 = eqParam1 e1 e2
@@ -523,7 +558,11 @@
 -- | This is to be included on top of @Errors@ section of the generated
 -- documentation.
 errorsDocumentation :: Markdown
-errorsDocumentation = [md|
+errorsDocumentation =
+  -- Note: this description should remain general enough to fit into all our
+  -- error formats, seek for [error format] to find all the relevant
+  -- declarations.
+  [md|
   Our contract implies the possibility of error scenarios, this section enlists
   all values which the contract can produce via calling `FAILWITH` instruction
   on them. In case of error, no changes to contract state will be applied.
@@ -536,7 +575,7 @@
   appears in the list first will be thrown.
 
   Most of the errors are represented according to the same
-  `(error name, error argument)` pattern. See the list of errors below
+  `(error tag, error argument)` pattern. See the list of errors below
   for details.
 
   We distinquish several error classes:
diff --git a/src/Lorentz/Errors/Numeric.hs b/src/Lorentz/Errors/Numeric.hs
--- a/src/Lorentz/Errors/Numeric.hs
+++ b/src/Lorentz/Errors/Numeric.hs
@@ -1,174 +1,6 @@
--- | By default we represent error tags using strings. This module
--- makes it possible to use numbers instead.
---
--- There are two possible ways to use it:
--- 1. If you have just one Lorentz instruction (potentially a big one),
--- just use 'useNumericErrors' function. It will change error representation
--- there and return a map that can be used to interpret new error codes.
--- 2. If your contract consists of multiple parts, start with gathering all
--- error tags ('gatherErrorTags'). Then build 'ErrorTagMap' using
--- 'addNewErrorTags'. Pass empty map if you are building from scratch
--- (you can use 'buildErrorTagMap' shortcut) or an existing
--- map if you have one (e. g. you are upgrading a contract).
-
 module Lorentz.Errors.Numeric
-  ( ErrorTagMap
-  , ErrorTagExclusions
-  , gatherErrorTags
-  , addNewErrorTags
-  , buildErrorTagMap
-  , excludeErrorTags
-  , applyErrorTagMap
-  , applyErrorTagMapWithExclusions
-  , useNumericErrors
-
-  , errorFromValNumeric
+  ( module Exports
   ) where
 
-import Data.Bimap (Bimap)
-import qualified Data.Bimap as Bimap
-import Data.Default (def)
-import qualified Data.HashSet as HS
-import Data.Singletons (SingI, sing)
-import Fmt (pretty)
-
-import Lorentz.Base
-import Lorentz.Errors
-import Michelson.Analyzer
-import Michelson.FailPattern
-import Michelson.Text (MText)
-import Michelson.Typed
-
--- | This is a bidirectional map with correspondence between numeric
--- and textual error tags.
-type ErrorTagMap = Bimap Natural MText
-
--- | Tags excluded from map.
-type ErrorTagExclusions = HashSet MText
-
--- | Find all textual error tags that are used in typical
--- @FAILWITH@ patterns within given instruction.
--- Map them to natural numbers.
-gatherErrorTags :: inp :-> out -> HashSet MText
-gatherErrorTags = HS.fromMap . void . arErrorTags . analyze . iAnyCode
-
--- | Add more error tags to an existing 'ErrorTagMap'. It is useful when
--- your contract consists of multiple parts (e. g. in case of contract
--- upgrade), you have existing map for some part and want to add tags
--- from another part to it.
--- You can pass empty map as existing one if you just want to build
--- 'ErrorTagMap' from a set of textual tags. See 'buildErrorTagMap'.
-addNewErrorTags :: ErrorTagMap -> HashSet MText -> ErrorTagMap
-addNewErrorTags existingMap newTags =
-  foldl' (flip $ uncurry Bimap.tryInsert) existingMap newItems
-  where
-    firstUnusedNumeric
-      | Bimap.null existingMap = 0
-      | otherwise = fst (Bimap.findMax existingMap) + 1
-
-    newItems :: [(Natural, MText)]
-    newItems = zip [firstUnusedNumeric .. ] (toList newTags)
-
--- | Build 'ErrorTagMap' from a set of textual tags.
-buildErrorTagMap :: HashSet MText -> ErrorTagMap
-buildErrorTagMap = addNewErrorTags Bimap.empty
-
--- | Remove some error tags from map.
--- This way you say to remain these string tags intact, while others will be
--- converted to numbers when this map is applied.
---
--- Note that later you have to apply this map using
--- 'applyErrorTagMapWithExclusions', otherwise an error would be raised.
-excludeErrorTags
-  :: HasCallStack
-  => ErrorTagExclusions -> ErrorTagMap -> ErrorTagMap
-excludeErrorTags toExclude errMap =
-  foldl' (flip deleteExistingR) errMap toExclude
-  where
-    deleteExistingR k m = case Bimap.lookupR k m of
-      Just _ -> Bimap.deleteR k m
-      Nothing ->
-        error $ "Tag " <> show k <> " does not appear in the contract"
-
--- | For each typical 'FAILWITH' that uses a string to represent error
--- tag this function changes error tag to be a number using the
--- supplied conversion map.
--- It assumes that supplied map contains all such strings
--- (and will error out if it does not).
--- It will always be the case if you gather all error tags using
--- 'gatherErrorTags' and build 'ErrorTagMap' from them using 'addNewErrorTags'.
-applyErrorTagMap :: HasCallStack => ErrorTagMap -> inp :-> out -> inp :-> out
-applyErrorTagMap errorTagMap = applyErrorTagMapWithExclusions errorTagMap mempty
-
--- | Similar to 'applyErrorTagMap', but for case when you have excluded some
--- tags from map via 'excludeErrorTags'.
--- Needed, because both 'excludeErrorTags' and this function do not tolerate
--- unknown errors in contract code (for your safety).
-applyErrorTagMapWithExclusions
-  :: HasCallStack
-  => ErrorTagMap -> ErrorTagExclusions -> inp :-> out -> inp :-> out
-applyErrorTagMapWithExclusions errorTagMap exclusions =
-  iMapAnyCode (applyErrorTagMapWithExcT errorTagMap exclusions)
-
--- | This function implements the simplest scenario of using this
--- module's functionality:
--- 1. Gather all error tags from a single instruction.
--- 2. Turn them into error conversion map.
--- 3. Apply this conversion.
-useNumericErrors ::
-  HasCallStack => inp :-> out -> (inp :-> out, ErrorTagMap)
-useNumericErrors instr = (applyErrorTagMap errorTagMap instr, errorTagMap)
-  where
-    errorTagMap = buildErrorTagMap $ gatherErrorTags instr
-
--- This function works with 'Michelson.Typed' representation, not with Lorentz.
-applyErrorTagMapWithExcT ::
-     HasCallStack
-  => ErrorTagMap
-  -> ErrorTagExclusions
-  -> Instr inp out
-  -> Instr inp out
-applyErrorTagMapWithExcT errorTagMap exclusions instr =
-  dfsModifyInstr dfsSettings step instr
-  where
-    dfsSettings :: DfsSettings ()
-    dfsSettings = def
-      { dsGoToValues = True
-      }
-
-    tagToNatValue :: HasCallStack => MText -> SomeConstrainedValue ConstantScope'
-    tagToNatValue tag =
-      case (HS.member tag exclusions, Bimap.lookupR tag errorTagMap) of
-        (True, _) -> SomeConstrainedValue (VC $ CvString tag)
-        -- It will be applied to textual tags detected by 'modifyTypicalFailWith'.
-        -- Here we assume that all of them are discovered by the analyzer.
-        -- If this error ever happens, it means that someone used
-        -- 'applyErrorTagMap' with incomplete 'ErrorTagMap' or there is an
-        -- internal bug somewhere.
-        (False, Nothing) -> error $ "Can't find a tag: " <> pretty tag
-        (False, Just n) -> SomeConstrainedValue (VC $ CvNat n)
-
-    step :: HasCallStack => Instr inp out -> Instr inp out
-    step = modifyTypicalFailWith tagToNatValue
-
--- | If you apply numeric error representation in your contract, 'errorFromVal'
--- will stop working because it doesn't know about this
--- transformation.
--- This function takes this transformation into account.
--- If a number is used as a tag, but it is not found in the passed
--- map, we conservatively preserve that number (because this whole
--- approach is rather a heuristic).
-errorFromValNumeric ::
-  (Typeable t, SingI t, IsError e) => ErrorTagMap -> Value t -> Either Text e
-errorFromValNumeric errorTagMap v =
-  case v of
-    VC (CvNat tag)
-      | Just textualTag <- Bimap.lookup tag errorTagMap ->
-        errorFromVal . VC . CvString $ textualTag
-    VPair (VC (CvNat tag), something)
-      | Just textualTag <- Bimap.lookup tag errorTagMap
-      , _ :: Value pair <- v ->
-        case sing @pair of
-          STPair {} ->
-            errorFromVal $ VPair (VC $ CvString textualTag, something)
-    _ -> errorFromVal v
+import Lorentz.Errors.Numeric.Contract as Exports
+import Lorentz.Errors.Numeric.Doc as Exports
diff --git a/src/Lorentz/Errors/Numeric/Contract.hs b/src/Lorentz/Errors/Numeric/Contract.hs
new file mode 100644
--- /dev/null
+++ b/src/Lorentz/Errors/Numeric/Contract.hs
@@ -0,0 +1,174 @@
+-- | By default we represent error tags using strings. This module
+-- makes it possible to use numbers instead. It introduces new [error format].
+--
+-- There are two possible ways to use it:
+-- 1. If you have just one Lorentz instruction (potentially a big one),
+-- just use 'useNumericErrors' function. It will change error representation
+-- there and return a map that can be used to interpret new error codes.
+-- 2. If your contract consists of multiple parts, start with gathering all
+-- error tags ('gatherErrorTags'). Then build 'ErrorTagMap' using
+-- 'addNewErrorTags'. Pass empty map if you are building from scratch
+-- (you can use 'buildErrorTagMap' shortcut) or an existing
+-- map if you have one (e. g. you are upgrading a contract).
+
+module Lorentz.Errors.Numeric.Contract
+  ( ErrorTagMap
+  , ErrorTagExclusions
+  , gatherErrorTags
+  , addNewErrorTags
+  , buildErrorTagMap
+  , excludeErrorTags
+  , applyErrorTagMap
+  , applyErrorTagMapWithExclusions
+  , useNumericErrors
+
+  , errorFromValNumeric
+  ) where
+
+import Data.Bimap (Bimap)
+import qualified Data.Bimap as Bimap
+import Data.Default (def)
+import qualified Data.HashSet as HS
+import Data.Singletons (SingI, sing)
+import Fmt (pretty)
+
+import Lorentz.Base
+import Lorentz.Errors
+import Michelson.Analyzer
+import Michelson.FailPattern
+import Michelson.Text (MText)
+import Michelson.Typed
+
+-- | This is a bidirectional map with correspondence between numeric
+-- and textual error tags.
+type ErrorTagMap = Bimap Natural MText
+
+-- | Tags excluded from map.
+type ErrorTagExclusions = HashSet MText
+
+-- | Find all textual error tags that are used in typical
+-- @FAILWITH@ patterns within given instruction.
+-- Map them to natural numbers.
+gatherErrorTags :: inp :-> out -> HashSet MText
+gatherErrorTags = HS.fromMap . void . arErrorTags . analyze . iAnyCode
+
+-- | Add more error tags to an existing 'ErrorTagMap'. It is useful when
+-- your contract consists of multiple parts (e. g. in case of contract
+-- upgrade), you have existing map for some part and want to add tags
+-- from another part to it.
+-- You can pass empty map as existing one if you just want to build
+-- 'ErrorTagMap' from a set of textual tags. See 'buildErrorTagMap'.
+addNewErrorTags :: ErrorTagMap -> HashSet MText -> ErrorTagMap
+addNewErrorTags existingMap newTags =
+  foldl' (flip $ uncurry Bimap.tryInsert) existingMap newItems
+  where
+    firstUnusedNumeric
+      | Bimap.null existingMap = 0
+      | otherwise = fst (Bimap.findMax existingMap) + 1
+
+    newItems :: [(Natural, MText)]
+    newItems = zip [firstUnusedNumeric .. ] (toList newTags)
+
+-- | Build 'ErrorTagMap' from a set of textual tags.
+buildErrorTagMap :: HashSet MText -> ErrorTagMap
+buildErrorTagMap = addNewErrorTags Bimap.empty
+
+-- | Remove some error tags from map.
+-- This way you say to remain these string tags intact, while others will be
+-- converted to numbers when this map is applied.
+--
+-- Note that later you have to apply this map using
+-- 'applyErrorTagMapWithExclusions', otherwise an error would be raised.
+excludeErrorTags
+  :: HasCallStack
+  => ErrorTagExclusions -> ErrorTagMap -> ErrorTagMap
+excludeErrorTags toExclude errMap =
+  foldl' (flip deleteExistingR) errMap toExclude
+  where
+    deleteExistingR k m = case Bimap.lookupR k m of
+      Just _ -> Bimap.deleteR k m
+      Nothing ->
+        error $ "Tag " <> show k <> " does not appear in the contract"
+
+-- | For each typical 'FAILWITH' that uses a string to represent error
+-- tag this function changes error tag to be a number using the
+-- supplied conversion map.
+-- It assumes that supplied map contains all such strings
+-- (and will error out if it does not).
+-- It will always be the case if you gather all error tags using
+-- 'gatherErrorTags' and build 'ErrorTagMap' from them using 'addNewErrorTags'.
+applyErrorTagMap :: HasCallStack => ErrorTagMap -> inp :-> out -> inp :-> out
+applyErrorTagMap errorTagMap = applyErrorTagMapWithExclusions errorTagMap mempty
+
+-- | Similar to 'applyErrorTagMap', but for case when you have excluded some
+-- tags from map via 'excludeErrorTags'.
+-- Needed, because both 'excludeErrorTags' and this function do not tolerate
+-- unknown errors in contract code (for your safety).
+applyErrorTagMapWithExclusions
+  :: HasCallStack
+  => ErrorTagMap -> ErrorTagExclusions -> inp :-> out -> inp :-> out
+applyErrorTagMapWithExclusions errorTagMap exclusions =
+  iMapAnyCode (applyErrorTagMapWithExcT errorTagMap exclusions)
+
+-- | This function implements the simplest scenario of using this
+-- module's functionality:
+-- 1. Gather all error tags from a single instruction.
+-- 2. Turn them into error conversion map.
+-- 3. Apply this conversion.
+useNumericErrors ::
+  HasCallStack => inp :-> out -> (inp :-> out, ErrorTagMap)
+useNumericErrors instr = (applyErrorTagMap errorTagMap instr, errorTagMap)
+  where
+    errorTagMap = buildErrorTagMap $ gatherErrorTags instr
+
+-- This function works with 'Michelson.Typed' representation, not with Lorentz.
+applyErrorTagMapWithExcT ::
+     HasCallStack
+  => ErrorTagMap
+  -> ErrorTagExclusions
+  -> Instr inp out
+  -> Instr inp out
+applyErrorTagMapWithExcT errorTagMap exclusions instr =
+  dfsModifyInstr dfsSettings step instr
+  where
+    dfsSettings :: DfsSettings ()
+    dfsSettings = def
+      { dsGoToValues = True
+      }
+
+    tagToNatValue :: HasCallStack => MText -> SomeConstrainedValue ConstantScope'
+    tagToNatValue tag =
+      case (HS.member tag exclusions, Bimap.lookupR tag errorTagMap) of
+        (True, _) -> SomeConstrainedValue (VC $ CvString tag)
+        -- It will be applied to textual tags detected by 'modifyTypicalFailWith'.
+        -- Here we assume that all of them are discovered by the analyzer.
+        -- If this error ever happens, it means that someone used
+        -- 'applyErrorTagMap' with incomplete 'ErrorTagMap' or there is an
+        -- internal bug somewhere.
+        (False, Nothing) -> error $ "Can't find a tag: " <> pretty tag
+        (False, Just n) -> SomeConstrainedValue (VC $ CvNat n)
+
+    step :: HasCallStack => Instr inp out -> Instr inp out
+    step = modifyTypicalFailWith tagToNatValue
+
+-- | If you apply numeric error representation in your contract, 'errorFromVal'
+-- will stop working because it doesn't know about this
+-- transformation.
+-- This function takes this transformation into account.
+-- If a number is used as a tag, but it is not found in the passed
+-- map, we conservatively preserve that number (because this whole
+-- approach is rather a heuristic).
+errorFromValNumeric ::
+  (Typeable t, SingI t, IsError e) => ErrorTagMap -> Value t -> Either Text e
+errorFromValNumeric errorTagMap v =
+  case v of
+    VC (CvNat tag)
+      | Just textualTag <- Bimap.lookup tag errorTagMap ->
+        errorFromVal . VC . CvString $ textualTag
+    VPair (VC (CvNat tag), something)
+      | Just textualTag <- Bimap.lookup tag errorTagMap
+      , _ :: Value pair <- v ->
+        case sing @pair of
+          STPair {} ->
+            errorFromVal $ VPair (VC $ CvString textualTag, something)
+    _ -> errorFromVal v
diff --git a/src/Lorentz/Errors/Numeric/Doc.hs b/src/Lorentz/Errors/Numeric/Doc.hs
new file mode 100644
--- /dev/null
+++ b/src/Lorentz/Errors/Numeric/Doc.hs
@@ -0,0 +1,229 @@
+-- | Autodoc for numeric errors.
+module Lorentz.Errors.Numeric.Doc
+  ( DDescribeErrorTagMap (..)
+  , applyErrorTagToErrorsDoc
+  , applyErrorTagToErrorsDocWith
+  , NumericErrorDocHandler
+  , NumericErrorDocHandlerError
+  , customErrorDocHandler
+  , voidResultDocHandler
+  , baseErrorDocHandlers
+
+    -- * Internals
+  , NumericErrorWrapper
+  ) where
+
+import Control.Monad.Cont (callCC, runCont)
+import qualified Data.Bimap as Bimap
+import Data.Constraint (Dict(..))
+import qualified Data.Kind as Kind
+import Data.Typeable ((:~:)(..), eqT)
+import Data.Typeable (typeRep)
+import Fmt (build, pretty)
+import GHC.TypeNats (KnownNat, Nat, natVal, someNatVal)
+
+import Lorentz.Base
+import Lorentz.Doc
+import Lorentz.Errors
+import Lorentz.Errors.Numeric.Contract
+import Lorentz.Macro
+import Michelson.Text (MText)
+import Michelson.Typed
+import Util.Markdown
+import Util.Typeable
+
+-- | Adds a section which explains error tag mapping.
+data DDescribeErrorTagMap = DDescribeErrorTagMap
+  { detmSrcLoc :: Text
+    -- ^ Describes where the error tag map is defined in Haskell code.
+  } deriving (Eq, Ord)
+
+instance DocItem DDescribeErrorTagMap where
+  type DocItemPosition DDescribeErrorTagMap = 4090
+  type DocItemPlacement DDescribeErrorTagMap = 'DocItemInDefinitions
+  docItemSectionName = Just "About error tags mapping"
+  docItemRef DDescribeErrorTagMap{..} = DocItemRef $
+    DocItemId $ "error-mapping-" <> detmSrcLoc
+  docItemToMarkdown _ DDescribeErrorTagMap{..} = [md|
+    This contract uses numeric representation of error tags.
+    Nevertheless, the original Lorentz code operates with string tags which are
+    later mapped to naturals.
+
+    If you need to handle errors produced by this contract, we recommend
+    converting numeric tags back to strings first, preserving textual tags which
+    are already present, and then pattern-match on textual tags.
+    This conversion can be performed with the help of the error tag map defined
+    at `#{detmSrcLoc}`.
+
+    Note that some errors can still use a textual tag, for instance to
+    satisfy rules of an interface.
+
+    In [TM-376](https://issues.serokell.io/issue/TM-376) we are going to provide
+    more type-safe and convenient mechanisms for errors handling.
+    |]
+    -- TODO [TM-376]: update the comment above on how to work with our errors
+    -- from Haskell
+
+-- | Anchor which refers to the section describing error tag mapping.
+dDescribeErrorTagMapAnchor :: Anchor
+dDescribeErrorTagMapAnchor = Anchor "about-error-tags-mapping"
+
+-- | Errors for 'NumericErrorDocHandler'
+data NumericErrorDocHandlerError
+  = EheNotApplicable
+    -- ^ Given handler is not suitable, probably another one will fit.
+  | EheConversionUnnecessary
+    -- ^ Given handler suits and tells that given error should remain unchanged.
+
+data SomeErrorWithDoc = forall err. ErrorHasDoc err => SomeErrorWithDoc (Proxy err)
+
+-- | Handler which changes documentation for one particular error type.
+newtype NumericErrorDocHandler =
+  NumericErrorDocHandler
+  { _unNumericErrorDocHandler
+      :: forall givenErr.
+         (ErrorHasDoc givenErr)
+      => ErrorTagMap
+      -> Proxy givenErr
+      -> Either NumericErrorDocHandlerError SomeErrorWithDoc
+  }
+
+-- | Modify documentation generated for given code so that all 'CustomError'
+-- mention not their textual error tag rather respective numeric one from the
+-- given map.
+--
+-- If some documented error is not present in the map, it remains unmodified.
+-- This function may fail with 'error' if contract uses some uncommon errors,
+-- see 'applyErrorTagToErrorsDocWith' for details.
+applyErrorTagToErrorsDoc
+  :: HasCallStack
+  => ErrorTagMap -> inp :-> out -> inp :-> out
+applyErrorTagToErrorsDoc = applyErrorTagToErrorsDocWith baseErrorDocHandlers
+
+-- | Extended version of 'applyErrorTagToErrorsDoc' which accepts error
+-- handlers.
+--
+-- In most cases that function should be enough for your purposes, but it uses
+-- a fixed set of base handlers which may be not enough in case when you define
+-- your own errors. In this case define and pass all the necessary handlers to
+-- this function.
+--
+-- It fails with 'error' if some of the errors used in the contract cannot be
+-- handled with given handlers.
+applyErrorTagToErrorsDocWith
+  :: HasCallStack
+  => [NumericErrorDocHandler]
+  -> ErrorTagMap
+  -> inp :-> out
+  -> inp :-> out
+applyErrorTagToErrorsDocWith handlers errorTagMap =
+  iMapAnyCode $ modifyInstrDoc @_ @DThrows $
+  \(DThrows ep) ->
+    flip runCont id $
+    callCC $ \quitWith -> do
+      forM_ handlers $ \(NumericErrorDocHandler handler) ->
+        case handler errorTagMap ep of
+          Left EheNotApplicable -> pass
+          Left EheConversionUnnecessary -> quitWith Nothing
+          Right (SomeErrorWithDoc nep) -> quitWith $ Just (DThrows nep)
+      error $ "No handler found for error " <> show (typeRep ep)
+
+mkGeneralNumericWrapper
+  :: forall err.
+     (ErrorHasDoc err, ErrorHasNumericDoc err)
+  => ErrorTagMap
+  -> MText
+  -> Either NumericErrorDocHandlerError SomeErrorWithDoc
+mkGeneralNumericWrapper errorTagMap strTag = do
+  numErrTag <- Bimap.lookupR strTag errorTagMap
+              & maybeToRight EheConversionUnnecessary
+  SomeNat (_ :: Proxy numTag) <- pure $ someNatVal numErrTag
+  return $ SomeErrorWithDoc $ Proxy @(NumericErrorWrapper numTag err)
+
+-- | Handler for all 'CustomError's.
+customErrorDocHandler :: NumericErrorDocHandler
+customErrorDocHandler = NumericErrorDocHandler $
+  \errorTagMap (_ :: Proxy givenErr) ->
+    join . maybeToRight EheNotApplicable $
+    eqTypeIgnoringPhantom @CustomError @givenErr $ \Refl (_ :: Proxy strTag) ->
+      case errorDocRequirements @(CustomError strTag) of
+        Dict -> do
+          let strTag = errorTagToMText (fromLabel @strTag)
+          mkGeneralNumericWrapper @givenErr errorTagMap strTag
+
+-- | Handler for 'VoidResult'.
+voidResultDocHandler :: NumericErrorDocHandler
+voidResultDocHandler = NumericErrorDocHandler $
+  \errorTagMap (_ :: Proxy givenErr) ->
+    join . maybeToRight EheNotApplicable $
+    eqTypeIgnoringPhantom @VoidResult @givenErr $ \Refl (_ :: Proxy res) -> do
+      mkGeneralNumericWrapper @givenErr errorTagMap voidResultTag
+
+-- | Handler for textual error messages.
+textErrorDocHandler :: NumericErrorDocHandler
+textErrorDocHandler = NumericErrorDocHandler $
+  \_errorTagMap (_ :: Proxy givenErr) ->
+    case eqT @givenErr @MText of
+      Nothing -> Left EheNotApplicable
+      Just Refl -> pure $ SomeErrorWithDoc $ Proxy @NumericTextError
+
+-- | Handlers for most common errors defined in Lorentz.
+baseErrorDocHandlers :: [NumericErrorDocHandler]
+baseErrorDocHandlers =
+  [ customErrorDocHandler
+  , voidResultDocHandler
+  , textErrorDocHandler
+  ]
+
+-- | Pseudo error which stands for textual errors converted to numeric codes.
+data NumericTextError
+
+instance ErrorHasDoc NumericTextError where
+  errorDocName = errorDocName @MText
+  errorDocMdCause = errorDocMdCause @MText
+  errorDocMdCauseInEntrypoint = errorDocMdCauseInEntrypoint @MText
+  errorDocClass = errorDocClass @MText
+  errorDocDependencies = [SomeDocDefinitionItem (DType $ Proxy @Natural)]
+  errorDocHaskellRep =
+    "Numeric code for an error message, see also " <>
+    mdLocalRef "error tags mapping" dDescribeErrorTagMapAnchor <> "."
+
+-- | Some error with a numeric tag attached.
+data NumericErrorWrapper (numTag :: Nat) (err :: Kind.Type)
+
+instance ( ErrorHasDoc err
+         , KnownNat numTag, ErrorHasNumericDoc err
+         ) =>
+         ErrorHasDoc (NumericErrorWrapper numTag err) where
+  errorDocName = errorDocName @err
+  errorDocMdCause = errorDocMdCause @err
+  errorDocMdCauseInEntrypoint = errorDocMdCauseInEntrypoint @err
+  errorDocClass = errorDocClass @err
+  errorDocDependencies = errorDocDependencies @err
+  errorDocHaskellRep =
+    case errorDocRequirements @err of
+      Dict -> mconcat
+        [ let numTag = pretty (natVal $ Proxy @numTag) <> " :: nat"
+          in numericErrorDocHaskellRep @err numTag
+        , "\n\n"
+        , mdSubsection "Respective textual tag" $
+            mdTicked (build $ numericErrorDocTextualTag @err)
+        ]
+
+-- | Helper typeclass which overloads representation for errors.
+class ErrorHasNumericDoc err where
+  -- | Error representation with respect to tags being changed to numeric ones.
+  numericErrorDocHaskellRep :: ErrorRequirements err => Text -> Markdown
+  numericErrorDocTextualTag :: ErrorRequirements err => Text
+
+instance ErrorHasNumericDoc (CustomError tag) where
+  numericErrorDocHaskellRep numTag =
+    customErrorDocHaskellRepGeneral numTag (Proxy @tag)
+  numericErrorDocTextualTag = errorTagToText @tag
+
+instance ErrorHasDoc (VoidResult res) =>
+         ErrorHasNumericDoc (VoidResult res) where
+  numericErrorDocHaskellRep numTag =
+    case errorDocRequirements @(VoidResult res) of
+      Dict -> mdTicked $ "(" <> build numTag <> ", " <> "<return value>" <> ")"
+  numericErrorDocTextualTag = toText voidResultTag
diff --git a/src/Lorentz/Extensible.hs b/src/Lorentz/Extensible.hs
--- a/src/Lorentz/Extensible.hs
+++ b/src/Lorentz/Extensible.hs
@@ -55,7 +55,6 @@
 import qualified Data.Kind as Kind
 import qualified Data.Text as T
 import Data.Typeable (Proxy(..))
-import Data.Vinyl.Derived (Label)
 import Data.Vinyl.TypeLevel (type (++))
 import Fmt (Buildable(build), (+||), (|+), (||+))
 import GHC.Generics ((:+:)(..))
@@ -66,16 +65,18 @@
 import Lorentz.Base
 import Lorentz.Coercions
 import Lorentz.Constraints
+import Lorentz.TypeAnns
 import Lorentz.Instr
 import Lorentz.Pack
 import Michelson.Typed
+import Util.Label (Label)
 import Util.Markdown
 import Util.Type
 import Util.TypeLits
 
 newtype Extensible x = Extensible (Natural, ByteString)
   deriving stock (Generic, Eq, Show)
-  deriving anyclass (IsoValue)
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 instance Wrapped (Extensible x)
 
@@ -263,6 +264,11 @@
       \where `idx` is a natural number which designates constructor used to \
       \make up given value, and `param` is the argument carried in that \
       \constructor.\n\n"
+    , "To unwrap value from its `Extensible` representation in Haskell, one should use \
+      \`fromExtVal` function provided by `Lorentz.Extensible` module. \
+      \This function tries to unwrap an event and may fail if the representation is \
+      \invalid (i.e. if it fails to find the corresponding constructor or if the \
+      \parameter can not be unpacked.\n\n"
     , "Value must be one of:\n\n"
     , mconcat $
         Prelude.map (<> "\n\n") $
diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs
--- a/src/Lorentz/Instr.hs
+++ b/src/Lorentz/Instr.hs
@@ -4,8 +4,11 @@
   , dropN
   , dup
   , swap
+  , ConstraintDIGLorentz
   , digPeano
   , dig
+  , ConstraintDUGLorentz
+  , dugPeano
   , dug
   , push
   , some
@@ -103,6 +106,7 @@
 import Data.Singletons (SingI, sing)
 import qualified GHC.TypeNats as GHC (Nat)
 
+import Lorentz.Address
 import Lorentz.Arith
 import Lorentz.Base
 import Lorentz.Constraints
@@ -179,11 +183,19 @@
       '[ Bool, Integer, Integer, Integer ]
     _example = dig @3
 
+-- | Version of `dug` which uses Peano number.
+-- It is inteded for internal usage in Lorentz.
+dugPeano ::
+  forall (n :: Peano) inp out a.
+  ( ConstraintDUGLorentz n inp out a
+  ) => inp :-> out
+dugPeano = I (DUG $ sing @n)
+
 dug ::
   forall (n :: GHC.Nat) inp out a.
   ( ConstraintDUGLorentz (ToPeano n) inp out a
   ) => inp :-> out
-dug = I (DUG $ sing @(ToPeano n))
+dug = dugPeano @(ToPeano n)
   where
     _example ::
       '[ Bool, Integer, Integer, Integer ] :->
@@ -459,16 +471,6 @@
 int :: Natural & s :-> Integer & s
 int = I INT
 
--- | Cast something appropriate to 'TAddress'.
--- TODO [TM-280]: try to move somewhere
-toTAddress_
-  :: (ToTAddress_ cp addr)
-  => addr : s :-> TAddress cp : s
-toTAddress_ = I Nop
-
--- | Something coercible to 'TAddress cp'.
-type ToTAddress_ cp addr = (ToTAddress cp addr, ToT addr ~ ToT Address)
-
 -- | Get a reference to the current contract.
 --
 -- Note that, similar to 'CONTRACT' instruction, in Michelson 'SELF' instruction
@@ -575,7 +577,7 @@
 
 createContract
   :: forall p g s. (NiceStorage g, NiceParameterFull p)
-  => Contract p g
+  => ContractCode p g
   -> Maybe KeyHash & Mutez & g & s
   :-> Operation & Address & s
 createContract cntrc =
diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs
--- a/src/Lorentz/Macro.hs
+++ b/src/Lorentz/Macro.hs
@@ -54,6 +54,12 @@
   , assertUsing
 
   -- * Syntactic Conveniences
+  , ConstraintDuupXLorentz
+  , ConstraintReplaceNLorentz
+  , ConstraintUpdateNLorentz
+  , DuupX (..)
+  , ReplaceN (..)
+  , UpdateN (..)
   , dropX
   , cloneX
   , duupX
@@ -80,6 +86,8 @@
   , mapInsertNew
   , deleteMap
   , setDelete
+  , replaceN
+  , updateN
 
   -- * Additional Morley macros
   , View (..)
@@ -91,6 +99,7 @@
   , unwrapView
   , void_
   , mkVoid
+  , voidResultTag
 
   -- * Buildable utils for additional Morley macros
   , buildView
@@ -99,6 +108,8 @@
   -- * Macros for working with @address@ and @contract@-like types
   , addressToEpAddress
   , pushContractRef
+
+
   ) where
 
 import Prelude hiding (compare, drop, some, swap)
@@ -115,12 +126,14 @@
 import Lorentz.Base
 import Lorentz.Coercions
 import Lorentz.Constraints
+import Lorentz.TypeAnns
 import Lorentz.Doc
 import Lorentz.Errors
 import Lorentz.Ext (stackType)
 import Lorentz.Instr
 import Lorentz.Value
-import Michelson.Typed (ConstraintDIG', ConstraintDIPN', T, typeDocDependencies')
+import Michelson.Typed
+  (ConstraintDIG', ConstraintDIPN', ConstraintDUG', T, typeDocDependencies')
 import Michelson.Typed.Arith
 import Michelson.Typed.Haskell.Value
 import Util.Markdown
@@ -501,6 +514,112 @@
 setDelete :: IsComparable e => e & Set e & s :-> Set e & s
 setDelete = dip (push False) # update
 
+-- | Kind-agnostic constraint for replaceN
+type ReplaceNConstraint' kind (n :: Peano)
+  (s :: [kind]) (a :: kind) (mid :: [kind]) (tail :: [kind]) =
+  ( tail ~ Drop ('S n) s
+  , ConstraintDIPN' kind ('S n) (a ': s) mid (a ': tail) tail
+  , ConstraintDUG' kind n mid s a
+  )
+
+-- | Constraint for replaceN that combines kind-agnostic constraint for
+-- Lorentz (Haskell) types and for our typed Michelson.
+type ConstraintReplaceNLorentz (n :: Peano)
+  (s :: [Kind.Type]) (a :: Kind.Type)
+  (mid :: [Kind.Type]) (tail :: [Kind.Type]) =
+  ( ReplaceNConstraint' T n (ToTs s) (ToT a) (ToTs mid) (ToTs tail)
+  , ReplaceNConstraint' Kind.Type n s a mid tail
+  )
+
+class ReplaceN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) mid tail where
+  replaceNImpl :: a ': s :-> s
+
+instance {-# OVERLAPPING #-} (s ~ (a ': xs)) => ReplaceN ('S 'Z) s a mid tail where
+  replaceNImpl = swap # drop
+
+instance {-# OVERLAPPABLE #-} (ConstraintReplaceNLorentz ('S n) s a mid tail) =>
+  ReplaceN ('S ('S n)) s a mid tail where
+  replaceNImpl =
+    -- 'stackType' helps GHC deduce types
+    dipNPeano @('S ('S n)) (stackType @(a ': tail) # drop) # dugPeano @('S n)
+
+-- | Replace nth element (0-indexed) with the one on the top of the stack.
+-- For example, `replaceN @3` replaces the 3rd element with the 0th one.
+-- `replaceN @0` is not a valid operation (and it is not implemented).
+-- `replaceN @1` is equivalent to `swap # drop` (and is the only one implemented
+-- like this).
+-- In all other cases `replaceN @n` will drop the nth element (`dipN @n drop`)
+-- and then put the 0th one in its place (`dug @(n-1)`).
+replaceN :: forall (n :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.Type]).
+  ( ConstraintReplaceNLorentz (ToPeano (n - 1)) s a s1 tail
+  , ReplaceN (ToPeano n) s a s1 tail
+  )
+  => a ': s :-> s
+replaceN = replaceNImpl @(ToPeano n) @s @a @s1 @tail
+  where
+    _example ::
+      '[ Integer, (), Integer, Bool ] :->
+      '[ (), Integer, Bool ]
+    _example = replaceN @2
+
+-- | Kind-agnostic constraint for updateN
+type UpdateNConstraint' kind (n :: Peano)
+  (s :: [kind]) (a :: kind) (b :: kind) (mid :: [kind]) (tail :: [kind]) =
+  ( tail ~ Drop ('S n) s
+  , ConstraintDUG' kind n (a ': s) mid a
+  , ConstraintDIPN' kind n mid s (a ': b ': tail) (b ': tail)
+  )
+
+-- | Constraint for updateN that combines kind-agnostic constraint for
+-- Lorentz (Haskell) types and for our typed Michelson.
+type ConstraintUpdateNLorentz (n :: Peano)
+  (s :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.Type)
+  (mid :: [Kind.Type]) (tail :: [Kind.Type]) =
+  ( UpdateNConstraint' T n (ToTs s) (ToT a) (ToT b) (ToTs mid) (ToTs tail)
+  , UpdateNConstraint' Kind.Type n s a b mid tail
+  )
+
+class UpdateN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.Type) mid tail where
+  updateNImpl
+    :: '[a, b] :-> '[b]
+    -> a ': s :-> s
+
+instance {-# OVERLAPPING #-} (s ~ (b ': tail)) => UpdateN ('S 'Z) s a b mid tail where
+  updateNImpl instr = framed instr
+
+instance {-# OVERLAPPING #-} (s ~ (x ': b ': tail)) => UpdateN ('S ('S 'Z)) s a b mid tail where
+  updateNImpl instr = swap # dip (framed instr)
+
+instance {-# OVERLAPPABLE #-} (ConstraintUpdateNLorentz ('S ('S n)) s a b mid tail) =>
+  UpdateN ('S ('S ('S n))) s a b mid tail where
+  updateNImpl instr =
+    -- 'stackType' helps GHC deduce types
+    dugPeano @('S ('S n)) # dipNPeano @('S ('S n)) (framed instr # stackType @(b ': tail))
+
+-- | Replaces the nth element (0-indexed) with the result of the given "updating"
+-- instruction (binary with the return type equal to the second argument) applied
+-- to the 0th element and the nth element itself.
+-- For example, `updateN @3 cons` replaces the 3rd element with the result of
+-- `cons` applied to the topmost element and the 3rd one.
+-- `updateN @0 instr` is not a valid operation (and it is not implemented).
+-- `updateN @1 instr` is equivalent to `instr` (and so is implemented).
+-- `updateN @2 instr` is equivalent to `swap # dip instr` (and so is implemented).
+-- In all other cases `updateN @n instr` will put the topmost element right above
+-- the nth one (`dug @(n-1)`) and then apply the function to them in place
+-- (`dipN @(n-1) instr`).
+updateN :: forall (n :: GHC.Nat) a b (s :: [Kind.Type]) (mid :: [Kind.Type]) (tail :: [Kind.Type]).
+  ( ConstraintUpdateNLorentz (ToPeano (n - 1)) s a b mid tail
+  , UpdateN (ToPeano n) s a b mid tail
+  )
+  => '[a, b] :-> '[b]
+  -> a ': s :-> s
+updateN instr = updateNImpl @(ToPeano n) @s @a @b @mid @tail instr
+  where
+    _example ::
+      '[ Integer, (), (), [Integer], Bool ] :->
+      '[ (), (), [Integer], Bool ]
+    _example = updateN @3 cons
+
 ----------------------------------------------------------------------------
 -- Additional Morley macros
 ----------------------------------------------------------------------------
@@ -510,8 +629,10 @@
   { viewParam :: a
   , viewCallbackTo :: ContractRef r
   } deriving stock (Eq, Show, Generic)
-    deriving anyclass IsoValue
+    deriving anyclass (IsoValue, HasTypeAnn)
 
+instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (View a1 r1) (View a2 r2)
+
 instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (View a r) where
   typeDocMdDescription =
     "`View a r` accepts an argument of type `a` and callback contract \
@@ -571,8 +692,10 @@
   , voidResProxy :: Lambda b b
     -- ^ Type of result reported via 'failWith'.
   } deriving stock (Generic, Show)
-    deriving anyclass IsoValue
+    deriving anyclass (IsoValue, HasTypeAnn)
 
+instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (Void_ a1 r1) (Void_ a2 r2)
+
 instance Each [Typeable, TypeHasDoc] [a, r] => TypeHasDoc (Void_ a r) where
   typeDocName _ = "Void"
   typeDocMdDescription =
@@ -644,7 +767,7 @@
     \update), this is the simplest way to return something to the caller in \
     \read-only entrypoints."
   errorDocHaskellRep =
-    mdTicked ("(\"" <> pretty (voidResultTag) <> "\", " <> "<return value>" <> ")")
+    mdTicked ("(\"" <> pretty voidResultTag <> "\", " <> "<return value>" <> ")")
   errorDocDependencies =
     typeDocDependencies' (Proxy @MText) <> typeDocDependencies' (Proxy @r)
 
diff --git a/src/Lorentz/Pack.hs b/src/Lorentz/Pack.hs
--- a/src/Lorentz/Pack.hs
+++ b/src/Lorentz/Pack.hs
@@ -2,6 +2,7 @@
 module Lorentz.Pack
   ( lPackValue
   , lUnpackValue
+  , lEncodeValue
   ) where
 
 import Data.Constraint ((\\))
@@ -24,3 +25,8 @@
   => ByteString -> Either UnpackError a
 lUnpackValue =
   fmap fromVal . unpackValue' \\ niceUnpackedValueEvi @a
+
+lEncodeValue
+  :: forall a. (NicePrintedValue a)
+  => a -> ByteString
+lEncodeValue = encodeValue' . toVal \\ nicePrintedValueEvi @a
diff --git a/src/Lorentz/Print.hs b/src/Lorentz/Print.hs
--- a/src/Lorentz/Print.hs
+++ b/src/Lorentz/Print.hs
@@ -26,6 +26,6 @@
 printLorentzContract
   :: forall cp st.
      (NiceParameterFull cp, NiceStorage st)
-  => Bool -> Contract cp st -> LText
+  => Bool -> ContractCode cp st -> LText
 printLorentzContract forceSingleLine =
   printTypedFullContract forceSingleLine . compileLorentzContract
diff --git a/src/Lorentz/Rebinded.hs b/src/Lorentz/Rebinded.hs
--- a/src/Lorentz/Rebinded.hs
+++ b/src/Lorentz/Rebinded.hs
@@ -29,7 +29,6 @@
 
 import Prelude hiding (drop, swap, (>>), (>>=))
 
-import Data.Vinyl.Derived (Label)
 import Named ((:!))
 
 import Lorentz.Arith
@@ -38,6 +37,7 @@
 import Lorentz.Instr
 import Lorentz.Macro
 import Michelson.Typed.Arith
+import Util.Label (Label)
 
 -- | Aliases for '(#)' used by do-blocks.
 (>>) :: (a :-> b) -> (b :-> c) -> (a :-> c)
diff --git a/src/Lorentz/Run.hs b/src/Lorentz/Run.hs
--- a/src/Lorentz/Run.hs
+++ b/src/Lorentz/Run.hs
@@ -1,5 +1,6 @@
 module Lorentz.Run
   ( CompilationOptions(..)
+  , defaultCompilationOptions
   , compileLorentz
   , compileLorentzContract
   , compileLorentzContractWithOptions
@@ -29,7 +30,7 @@
 compileLorentzContract
   :: forall cp st.
      (NiceParameterFull cp, NiceStorage st)
-  => Contract cp st -> FullContract (ToT cp) (ToT st)
+  => ContractCode cp st -> FullContract (ToT cp) (ToT st)
 compileLorentzContract =
   compileLorentzContractWithOptions defaultCompilationOptions
 
@@ -54,14 +55,14 @@
 compileLorentzContractWithOptions
   :: forall cp st.
      (NiceParameterFull cp, NiceStorage st)
-  => CompilationOptions -> Contract cp st -> FullContract (ToT cp) (ToT st)
+  => CompilationOptions -> ContractCode cp st -> FullContract (ToT cp) (ToT st)
 compileLorentzContractWithOptions CompilationOptions{..} contract =
   FullContract
   { fcCode = if (isStar (unParamNotes cpNotes) || coDisableInitialCast)
       then -- If contract parameter type has no annotations or explicitly asked, we drop CAST.
         compileLorentz contract
       else -- Perform CAST otherwise.
-        compileLorentz (I CAST # contract :: Contract cp st)
+        compileLorentz (I CAST # contract :: ContractCode cp st)
   , fcParamNotesSafe = cpNotes
   , fcStoreNotes = starNotes
   } \\ niceParameterEvi @cp
diff --git a/src/Lorentz/Store.hs b/src/Lorentz/Store.hs
--- a/src/Lorentz/Store.hs
+++ b/src/Lorentz/Store.hs
@@ -74,10 +74,9 @@
 import qualified Data.Map as Map
 import Data.Type.Bool (If, type (||))
 import Data.Type.Equality (type (==))
-import Data.Vinyl.Derived (Label)
 import GHC.Generics ((:+:))
 import qualified GHC.Generics as G
-import GHC.TypeLits (AppendSymbol, ErrorMessage(..), KnownSymbol, Symbol, TypeError)
+import GHC.TypeLits (AppendSymbol, ErrorMessage(..), Symbol, TypeError)
 import GHC.TypeNats (type (+), Nat)
 import Type.Reflection ((:~:)(Refl))
 
@@ -92,6 +91,7 @@
 import Michelson.Typed.Haskell.Instr.Sum
 import Michelson.Typed.Haskell.Value
 import Michelson.Typed.Instr
+import Util.Label (Label)
 
 {-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
 
@@ -335,7 +335,7 @@
 -- | Insert a key-value pair, but fail if it will overwrite some existing entry.
 storeInsertNew
   :: forall store name s.
-     (StoreInsertC store name, KnownSymbol name)
+     StoreInsertC store name
   => Label name
   -> (forall s0 any. GetStoreKey store name : s0 :-> any)
   -> GetStoreKey store name
@@ -551,7 +551,7 @@
 -- | Insert a key-value pair, but fail if it will overwrite some existing entry.
 storageInsertNew
   :: forall store name fields s.
-     (StoreInsertC store name, KnownSymbol name)
+     StoreInsertC store name
   => Label name
   -> (forall s0 any. GetStoreKey store name : s0 :-> any)
   -> GetStoreKey store name
diff --git a/src/Lorentz/StoreClass.hs b/src/Lorentz/StoreClass.hs
--- a/src/Lorentz/StoreClass.hs
+++ b/src/Lorentz/StoreClass.hs
@@ -33,8 +33,6 @@
   , composeStoreSubmapOps
   ) where
 
-import Data.Vinyl.Derived (Label)
-
 import Lorentz.ADT
 import Lorentz.Base
 import Lorentz.Constraints
@@ -42,6 +40,7 @@
 import qualified Lorentz.Macro as L
 import Lorentz.Value
 import Michelson.Typed.Haskell
+import Util.Label (Label)
 
 ----------------------------------------------------------------------------
 -- Fields
diff --git a/src/Lorentz/Test/Consumer.hs b/src/Lorentz/Test/Consumer.hs
--- a/src/Lorentz/Test/Consumer.hs
+++ b/src/Lorentz/Test/Consumer.hs
@@ -10,5 +10,5 @@
 import Lorentz.Macro
 
 -- | Remembers parameters it was called with, last goes first.
-contractConsumer :: Contract cp [cp]
+contractConsumer :: ContractCode cp [cp]
 contractConsumer = unpair # cons # nil # pair
diff --git a/src/Lorentz/Test/Doc.hs b/src/Lorentz/Test/Doc.hs
--- a/src/Lorentz/Test/Doc.hs
+++ b/src/Lorentz/Test/Doc.hs
@@ -6,18 +6,40 @@
     -- * Individual test predicates
   , testDeclaresParameter
   , testEachEntrypointIsDescribed
+  , testParamBuildingStepsAreFinalized
+  , testAllEntrypointsAreCallable
 
   , module Michelson.Doc.Test
   ) where
 
-import Fmt (pretty)
+import Fmt (Buildable(..), blockListF, fmt, nameF, pretty)
 import Test.HUnit (assertBool, assertFailure)
 
 import Lorentz.EntryPoints.Doc
 import Michelson.Doc
 import Michelson.Doc.Test
+import Util.Markdown
 import Util.Typeable
 
+-- | All ways of describing an entrypoint behaviour.
+data DocEpDescription
+  = DocEpDescription DDescription
+  | DocEpReference DEntryPointReference
+
+instance Buildable DocEpDescription where
+  build = \case
+    DocEpDescription (DDescription txt) ->
+      "description: " <> txt
+    DocEpReference (DEntryPointReference name (Anchor anchor)) ->
+      "reference \"" <> build name <> "\" (" <> build anchor <> ")"
+
+-- | Extract 'DocEpDescription's of a documentation block.
+lookupDocEpDescription :: DocBlock -> [DocEpDescription]
+lookupDocEpDescription block = mconcat
+  [ map DocEpDescription . maybe [] toList $ lookupDocBlockSection block
+  , map DocEpReference . maybe [] toList $ lookupDocBlockSection block
+  ]
+
 -- | Check that contract documents its parameter.
 testDeclaresParameter :: DocTest
 testDeclaresParameter =
@@ -36,6 +58,24 @@
         SomeDocItem (castIgnoringPhantom -> Just DEntryPoint{}) -> True
         _ -> False
 
+-- | Check that no group contains two 'DDescription' or 'DEntryPointReference'
+-- items.
+--
+-- This is a stricter version of 'testNoAdjacentDescriptions' test.
+testNoAdjacentEpDescriptions :: DocTest
+testNoAdjacentEpDescriptions =
+  mkDocTest "No two 'DDescription' appear under the same group" $
+  \contractDoc ->
+    sequence_ . forEachContractLayer contractDoc $ \_ block ->
+      case lookupDocEpDescription block of
+        ds@(_ : _ : _) ->
+          assertFailure . fmt $
+             nameF "Found multiple adjacent entrypoint descriptions" $
+             blockListF $ map (quotes . build) (toList ds)
+        _ -> pass
+    where
+      quotes t = "\"" <> t <> "\""
+
 -- | It's a common issue to forget to describe an entrypoint.
 testEachEntrypointIsDescribed :: DocTest
 testEachEntrypointIsDescribed =
@@ -45,17 +85,72 @@
       runMaybeT $ do
         SomeDocItem docItem <- MaybeT . pure $ mDocItem
         dep@DEntryPoint{} <- MaybeT . pure $ castIgnoringPhantom docItem
-        Nothing <- pure $ lookupDocBlockSection @DDescription block
+        [] <- pure $ lookupDocEpDescription block
         MaybeT . assertFailure $
           "Entrypoint '" <> pretty (depName dep) <> "' does not contain \
-          \description.\n\
-          \Put `doc $ DDescription \"text\"` in the entrypoint logic to fix this."
+          \any description.\n\
+          \Put e.g. `doc $ DDescription \"text\"` in the entrypoint logic to \
+          \fix this."
 
+-- | Check that 'finalizeParamCallingDoc' is applied to the contract as it
+-- always should.
+testParamBuildingStepsAreFinalized :: DocTest
+testParamBuildingStepsAreFinalized =
+  mkDocTest "'finalizeParamCallingDoc' is applied" $
+  \contractDoc ->
+    sequence_ . forEachContractDocItem contractDoc $ \DEntryPointArg{..} ->
+      unless (areFinalizedParamBuildingSteps epaBuilding) $
+        assertFailure
+          "Found unfinalized param building steps, \
+          \'How to call this entrypoint' section may be incorrect.\n\
+          \Have you applied 'finalizeParamCallingDoc' to your contract?"
+
+-- | Check that all documented entrypoints are callable.
+--
+-- Sometimes having such an entrypoint is fine, e.g. when you have an explicit
+-- default entrypoint deep in one arm then other arms (entire arms, not
+-- individual entrypoints within them) are uncallable unless also assigned a
+-- field annotation; for example see [doc for uncallable entrypoints] note.
+-- If this is your case, exclude this test suite with 'excludeDocTest'.
+-- But such situations are rare.
+--
+-- More often, this test failure indicates that entrypoints are documented
+-- incorrectly, e.g. `caseT` is used in some place instead of `entryCase`.
+-- Check whether printed building steps are correct.
+--
+-- NB: another, simplified example of case when disabling this test is
+-- justified:
+--
+-- @
+-- data SubParam1 = Do1 | Default
+-- data SubParam2 = Do2 | Do3
+-- data Param = Arm1 SubParam1 | Arm2 SubParam2
+--   -- ^ with entrypoints derived via 'EpdRecursive'
+-- @
+--
+-- In this case entire @Arm1@ and @Arm2@ are not true entrypoints, only @Default@
+-- and @Do{1,2,3}@ are, but @Arm1@ and @Arm2@ will still appear in documentation
+-- as entrypoints.
+testAllEntrypointsAreCallable :: DocTest
+testAllEntrypointsAreCallable =
+  mkDocTest "All entrypoints are callable" $
+  \contractDoc ->
+    sequence_ . forEachContractDocItem contractDoc $ \DEntryPointArg{..} ->
+      forM_ epaBuilding $ \case
+        PbsUncallable pbs ->
+          assertFailure . fmt $
+            "Found an uncallable entrypoint.\n\
+            \Dummy parameter building steps for it: " <> blockListF (reverse pbs)
+        _ -> pass
+
 -- | Tests all properties.
 testLorentzDoc :: [DocTest]
 testLorentzDoc = mconcat
   [ testDocBasic
   , [ testDeclaresParameter
+    , testNoAdjacentEpDescriptions
     , testEachEntrypointIsDescribed
+    , testParamBuildingStepsAreFinalized
+    , testAllEntrypointsAreCallable
     ]
   ]
diff --git a/src/Lorentz/Test/Import.hs b/src/Lorentz/Test/Import.hs
deleted file mode 100644
--- a/src/Lorentz/Test/Import.hs
+++ /dev/null
@@ -1,27 +0,0 @@
--- | Mirrors 'Michelson.Test.Import' module in a Lorentz way.
-
-module Lorentz.Test.Import
-  ( testTreesWithContractL
-  , specWithContractL
-  ) where
-
-import Data.Singletons (SingI)
-import Test.Hspec (Spec)
-import Test.Tasty (TestTree)
-
-import qualified Lorentz.Base as L
-import Michelson.Test.Import (specWithContract, testTreesWithContract)
-import Michelson.Typed (ToT)
-import qualified Michelson.Untyped as U
-
--- | Like 'testTreesWithContract' but for Lorentz types.
-testTreesWithContractL
-  :: (Each [Typeable, SingI] [ToT cp, ToT st], HasCallStack)
-  => FilePath -> ((U.Contract, L.Contract cp st) -> IO [TestTree]) -> IO [TestTree]
-testTreesWithContractL file testImpl = testTreesWithContract file (testImpl . second L.I)
-
--- | Like 'specWithContract', but for Lorentz types.
-specWithContractL
-  :: (Each [Typeable, SingI] [ToT cp, ToT st], HasCallStack)
-  => FilePath -> ((U.Contract, L.Contract cp st) -> Spec) -> Spec
-specWithContractL file mkSpec = specWithContract file (mkSpec . second L.I)
diff --git a/src/Lorentz/Test/Integrational.hs b/src/Lorentz/Test/Integrational.hs
--- a/src/Lorentz/Test/Integrational.hs
+++ b/src/Lorentz/Test/Integrational.hs
@@ -73,7 +73,6 @@
 import Data.Default (Default(..))
 import Data.Singletons (SingI)
 import Data.Typeable (gcast)
-import Data.Vinyl.Derived (Label)
 import Fmt (Buildable, listF, (+|), (|+))
 import Named ((:!), arg)
 
@@ -90,10 +89,11 @@
 import Michelson.Runtime.GState
 import Michelson.Test.Integrational
 import qualified Michelson.Test.Integrational as I
-import Michelson.TypeCheck (typeVerifyValue)
+import Michelson.TypeCheck (typeCheckValue)
 import qualified Michelson.Typed as T
 import qualified Michelson.Untyped as U
 import Tezos.Core
+import Util.Label (Label)
 import Util.Named ((.!))
 
 ----------------------------------------------------------------------------
@@ -110,7 +110,7 @@
 lOriginate
   :: forall cp st.
      (NiceParameterFull cp, NiceStorage st)
-  => L.Contract cp st
+  => L.ContractCode cp st
   -> Text
   -> st
   -> Mutez
@@ -124,7 +124,7 @@
 -- | Originate a contract with empty balance and default storage.
 lOriginateEmpty
   :: (NiceParameterFull cp, NiceStorage st, Default st)
-  => L.Contract cp st
+  => L.ContractCode cp st
   -> Text
   -> IntegrationalScenarioM (TAddress cp)
 lOriginateEmpty contract name = lOriginate contract name def (unsafeMkMutez 0)
@@ -201,7 +201,7 @@
     typeCheck uval =
       evaluatingState initSt . runExceptT $
       usingReaderT def $
-      typeVerifyValue uval
+      typeCheckValue uval
     initSt = error "Typechecker state unavailable"
 
 -- | Similar to 'expectStorage', but for Lorentz values.
diff --git a/src/Lorentz/Test/Unit.hs b/src/Lorentz/Test/Unit.hs
--- a/src/Lorentz/Test/Unit.hs
+++ b/src/Lorentz/Test/Unit.hs
@@ -7,7 +7,7 @@
 
 import Lorentz hiding (contract)
 import Michelson.Test.Unit (matchContractEntryPoints)
-import Michelson.Typed (convertFullContract)
+import Michelson.Typed (convertFullContract, flattenEntryPoints)
 
 -- | Expect the given contract to have some specific entrypoints.
 expectContractEntrypoints
@@ -16,7 +16,7 @@
      , NiceParameterFull contractEps
      , NiceStorage st
      )
-  => Contract contractEps st -> Assertion
+  => ContractCode contractEps st -> Assertion
 expectContractEntrypoints contract =
   withDict (niceParameterEvi @expectedEps) $
   withDict (niceParameterEvi @contractEps) $
diff --git a/src/Lorentz/TypeAnns.hs b/src/Lorentz/TypeAnns.hs
--- a/src/Lorentz/TypeAnns.hs
+++ b/src/Lorentz/TypeAnns.hs
@@ -10,8 +10,6 @@
 import qualified GHC.Generics as G
 import Named (NamedF)
 
-import Lorentz.Base ((:->))
-import Lorentz.Zip
 import Michelson.Text
 import Michelson.Typed
   (BigMap, ContractRef(..), EpAddress, Notes(..), Operation, T(..), ToCT, ToT, starNotes)
@@ -32,8 +30,8 @@
 class HasTypeAnn a where
   getTypeAnn :: Notes (ToT a)
 
-instance {-# OVERLAPPABLE #-} (GHasTypeAnn (G.Rep a), GValueType (G.Rep a) ~ ToT a)
-  => HasTypeAnn a where
+  default getTypeAnn
+    :: (GHasTypeAnn (G.Rep a), GValueType (G.Rep a) ~ ToT a) => Notes (ToT a)
   getTypeAnn = gGetTypeAnn @(G.Rep a)
 
 instance (HasTypeAnn a, KnownSymbol name)
@@ -69,6 +67,8 @@
 instance (HasTypeAnn a) => HasTypeAnn (Maybe a) where
   getTypeAnn = NTOption noAnn (getTypeAnn @a)
 
+instance HasTypeAnn ()
+
 instance HasTypeAnn Integer where
   getTypeAnn = starNotes
 
@@ -123,16 +123,17 @@
 instance HasTypeAnn Operation where
   getTypeAnn = starNotes
 
+instance (HasTypeAnn a, HasTypeAnn b) => HasTypeAnn (a, b)
+instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c) => HasTypeAnn (a, b, c)
+instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d) => HasTypeAnn (a, b, c, d)
+instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d, HasTypeAnn e)
+  => HasTypeAnn (a, b, c, d, e)
+instance (HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d, HasTypeAnn e, HasTypeAnn f)
+  => HasTypeAnn (a, b, c, d, e, f)
 instance
-    ( HasTypeAnn (ZippedStack i)
-    , HasTypeAnn (ZippedStack o)
-    )
-  =>
-    HasTypeAnn (i :-> o)
-  where
-  getTypeAnn = NTLambda noAnn
-    (getTypeAnn @(ZippedStack i))
-    (getTypeAnn @(ZippedStack o))
+  ( HasTypeAnn a, HasTypeAnn b, HasTypeAnn c, HasTypeAnn d, HasTypeAnn e
+  , HasTypeAnn f, HasTypeAnn g)
+  => HasTypeAnn (a, b, c, d, e, f, g)
 
 -- A Generic HasTypeAnn implementation
 class GHasTypeAnn a where
diff --git a/src/Lorentz/UParam.hs b/src/Lorentz/UParam.hs
--- a/src/Lorentz/UParam.hs
+++ b/src/Lorentz/UParam.hs
@@ -46,7 +46,6 @@
 import Data.Constraint ((\\))
 import qualified Data.Kind as Kind
 import Data.Vinyl.Core (Rec(..))
-import Data.Vinyl.Derived (Label)
 import Data.Vinyl.TypeLevel (type (++))
 import qualified Fcf
 import Fmt (Buildable(..))
@@ -58,18 +57,20 @@
 import Lorentz.ADT
 import Lorentz.Base
 import Lorentz.Coercions
-import Lorentz.EntryPoints.Doc
 import Lorentz.Constraints
+import Lorentz.EntryPoints.Doc
 import Lorentz.Errors
 import Lorentz.Instr as L
 import Lorentz.Macro
 import Lorentz.Pack
+import Lorentz.TypeAnns (HasTypeAnn)
 import Michelson.Text
 import Michelson.Typed
+import Util.Label (Label)
+import Util.Markdown
 import Util.Type
 import Util.TypeLits
 import Util.TypeTuple
-import Util.Markdown
 
 -- | An entrypoint is described by two types: its name and type of argument.
 type EntryPointKind = (Symbol, Kind.Type)
@@ -84,7 +85,7 @@
 -- to one of entry points from @entries@ list.
 newtype UParam (entries :: [EntryPointKind]) = UParamUnsafe (MText, ByteString)
   deriving stock (Generic, Eq, Show)
-  deriving anyclass (IsoValue)
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 instance Wrapped (UParam entries)
 
@@ -133,7 +134,7 @@
 
 -- | Construct a 'UParam' safely.
 mkUParam
-  :: ( KnownSymbol name, NicePackedValue a
+  :: ( NicePackedValue a
      , LookupEntryPoint name entries ~ a
      , RequireUniqueEntryPoints entries
      )
@@ -407,11 +408,11 @@
 pbsUParam :: forall ctorName. KnownSymbol ctorName => ParamBuildingStep
 pbsUParam =
   let ctor = build $ symbolValT' @ctorName
-  in ParamBuildingStep
-      { pbsEnglish =
+  in PbsCustom ParamBuildingDesc
+      { pbdEnglish =
           "Wrap into *UParam* as " <> mdTicked ctor <> " entrypoint."
-      , pbsHaskell =
+      , pbdHaskell = ParamBuilder $
           \a -> "mkUParam #" <> ctor <> " (" <> a <> ")"
-      , pbsMichelson =
+      , pbdMichelson = ParamBuilder $
           \a -> "Pair \"" <> ctor <> "\" (pack (" <> a <> "))"
       }
diff --git a/src/Lorentz/UStore/Instr.hs b/src/Lorentz/UStore/Instr.hs
--- a/src/Lorentz/UStore/Instr.hs
+++ b/src/Lorentz/UStore/Instr.hs
@@ -27,7 +27,6 @@
 import qualified Data.Kind as Kind
 import GHC.Generics ((:*:), (:+:))
 import qualified GHC.Generics as G
-import Data.Vinyl.Derived (Label)
 import GHC.TypeLits (KnownSymbol, Symbol)
 import Type.Reflection ((:~:)(Refl))
 
@@ -41,6 +40,7 @@
 import Lorentz.UStore.Common
 import Michelson.Text
 import Michelson.Typed.Haskell.Value
+import Util.Label (Label)
 
 -- Helpers
 ----------------------------------------------------------------------------
diff --git a/src/Lorentz/UStore/Lift.hs b/src/Lorentz/UStore/Lift.hs
--- a/src/Lorentz/UStore/Lift.hs
+++ b/src/Lorentz/UStore/Lift.hs
@@ -9,7 +9,6 @@
   , UStoreFieldsAreUnique
   ) where
 
-import Data.Vinyl.Derived (Label)
 import Data.Type.Bool (If)
 import qualified Data.Kind as Kind
 import GHC.TypeLits (Symbol, TypeError, ErrorMessage (..))
@@ -22,6 +21,7 @@
 import Lorentz.Instr
 import Lorentz.UStore.Types
 import Michelson.Typed.Haskell
+import Util.Label (Label)
 import Util.Type
 
 -- | Get all fields names accessible in given 'UStore' template.
diff --git a/src/Lorentz/UStore/Migration/Base.hs b/src/Lorentz/UStore/Migration/Base.hs
--- a/src/Lorentz/UStore/Migration/Base.hs
+++ b/src/Lorentz/UStore/Migration/Base.hs
@@ -99,18 +99,19 @@
 import qualified Data.Kind as Kind
 import Data.Singletons (SingI(..), demote)
 import qualified Data.Typeable as Typeable
-import Data.Vinyl.Derived (Label)
 import Fmt (Buildable(..), Builder, fmt)
 
 import Lorentz.Base
 import Lorentz.Coercions
 import Lorentz.Doc
+import Lorentz.TypeAnns (HasTypeAnn)
 import Lorentz.Instr (nop)
 import Lorentz.Run
 import Lorentz.UStore.Types
 import Lorentz.Value
 import Michelson.Typed (ExtInstr(..), Instr(..), T(..))
 import Michelson.Typed.Util
+import Util.Label (Label, labelToText)
 import Util.Lens
 import Util.TypeLits
 
@@ -150,7 +151,7 @@
   MigrationScript
   { unMigrationScript :: Lambda UStore_ UStore_
   } deriving stock (Show, Generic)
-    deriving anyclass IsoValue
+    deriving anyclass (IsoValue, HasTypeAnn)
 
 instance Wrapped (MigrationScript oldStore newStore)
 
@@ -188,6 +189,11 @@
   :: ('[UStore newStore] :-> '[UStore newStore]) -> MigrationScript oldStore newStore
 manualWithNewUStore = manualWithUStore
 
+-- | Modify code under given 'MigrationScript'.
+--
+-- Avoid using this function when constructing a batched migration because
+-- batching logic should know size of the code precisely, consider mapping
+-- 'UStoreMigration' instead.
 manualMapMigrationScript
   :: (('[UStore_] :-> '[UStore_]) -> ('[UStore_] :-> '[UStore_]))
   -> MigrationScript oldStore newStore
@@ -208,7 +214,7 @@
     -- ^ Some sort of addition: "init", "set", "overwrite", e.t.c.
   | DDelAction
     -- ^ Removal.
-  deriving stock (Show)
+  deriving stock Show
 
 instance Buildable DMigrationActionType where
   build = \case
@@ -226,7 +232,7 @@
     -- ^ Name of affected field of 'UStore'.
   , manFieldType :: T
     -- ^ Type of affected field of 'UStore' in new storage version.
-  } deriving stock (Show)
+  } deriving stock Show
 
 -- Sad that we need to write this useless documentation instance, probably it's
 -- worth generalizing @doc_group@ and @doc_item@ instructions so that they
@@ -239,15 +245,15 @@
 -- | Add description of action, it will be used in rendering migration plan and
 -- some batching implementations.
 attachMigrationActionName
-  :: (KnownSymbol fieldName, SingI (ToT fieldTy))
+  :: SingI (ToT fieldTy)
   => DMigrationActionType
   -> Label fieldName
   -> Proxy fieldTy
   -> s :-> s
-attachMigrationActionName action (_ :: Label fieldName) (_ :: Proxy fieldTy) =
+attachMigrationActionName action label (_ :: Proxy fieldTy) =
   doc $ DMigrationActionDesc
   { manAction = action
-  , manField = symbolValT' @fieldName
+  , manField = labelToText label
   , manFieldType = demote @(ToT fieldTy)
   }
 
@@ -282,14 +288,18 @@
 migrationToLambda (UStoreMigration atoms) =
   checkedCoerce_ # foldMap (unMigrationScript . maScript) atoms # checkedCoerce_
 
+instance MapLorentzInstr (UStoreMigration os ns) where
+  mapLorentzInstr f (UStoreMigration atoms) =
+    UStoreMigration $
+      atoms & traversed . maScriptL . _Wrapped' %~ f
+
 -- | Modify all code in migration.
 mapMigrationCode
   :: (forall i o. (i :-> o) -> (i :-> o))
   -> UStoreMigration os ns
   -> UStoreMigration os ns
-mapMigrationCode f (UStoreMigration atoms) =
-  UStoreMigration $
-    atoms & traversed . maScriptL . _Wrapped' %~ f
+mapMigrationCode = mapLorentzInstr
+{-# DEPRECATED mapMigrationCode "Use 'hoistLorentzInstr' instead" #-}
 
 -- | A bunch of migration atoms produced by migration writer.
 newtype MigrationBlocks (oldTemplate :: Kind.Type) (newTemplate :: Kind.Type)
diff --git a/src/Lorentz/UStore/Migration/Batching.hs b/src/Lorentz/UStore/Migration/Batching.hs
--- a/src/Lorentz/UStore/Migration/Batching.hs
+++ b/src/Lorentz/UStore/Migration/Batching.hs
@@ -86,7 +86,7 @@
     chooseType = \case
       [] -> SlbtUnknown
       xs | all isLambda xs -> SlbtLambda
-      xs | all (not . isAddLambda) xs -> SlbtData
+      xs | (not . any isAddLambda) xs -> SlbtData
          | otherwise -> SlbtCustom
 
     isLambda :: DMigrationActionDesc -> Bool
diff --git a/src/Lorentz/UStore/Migration/Blocks.hs b/src/Lorentz/UStore/Migration/Blocks.hs
--- a/src/Lorentz/UStore/Migration/Blocks.hs
+++ b/src/Lorentz/UStore/Migration/Blocks.hs
@@ -22,8 +22,6 @@
   , ($:)
   ) where
 
-import Data.Vinyl.Derived (Label)
-
 import Lorentz.Base
 import Lorentz.Coercions
 import Lorentz.Instr (dip)
@@ -31,6 +29,7 @@
 import Lorentz.UStore.Migration.Base
 import Lorentz.UStore.Migration.Diff
 import Lorentz.UStore.Types
+import Util.Label (Label)
 import Util.Type
 import Util.TypeLits
 
diff --git a/src/Lorentz/UStore/Migration/Diff.hs b/src/Lorentz/UStore/Migration/Diff.hs
--- a/src/Lorentz/UStore/Migration/Diff.hs
+++ b/src/Lorentz/UStore/Migration/Diff.hs
@@ -16,11 +16,11 @@
   ) where
 
 import qualified Data.Kind as Kind
-import GHC.Generics ((:*:), (:+:))
-import Fcf (Eval, Exp, Pure, Fst, type (=<<), type (***))
+import Fcf (type (***), type (=<<), Eval, Exp, Fst, Pure)
 import qualified Fcf
 import Fcf.Data.List (Cons)
 import Fcf.Utils (TError)
+import GHC.Generics ((:*:), (:+:))
 import qualified GHC.Generics as G
 
 import Lorentz.UStore.Types
diff --git a/src/Lorentz/UStore/Types.hs b/src/Lorentz/UStore/Types.hs
--- a/src/Lorentz/UStore/Types.hs
+++ b/src/Lorentz/UStore/Types.hs
@@ -35,21 +35,22 @@
 
 import Data.Default (Default)
 import Control.Lens (Wrapped)
-import Data.Vinyl.Derived (Label)
 import qualified Data.Kind as Kind
 import Data.Type.Equality (type (==))
 import GHC.Generics ((:*:)(..), (:+:)(..))
 import qualified GHC.Generics as G
-import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError, KnownSymbol)
+import GHC.TypeLits (ErrorMessage(..), Symbol, TypeError)
 import Test.QuickCheck (Arbitrary)
 
 import Lorentz.Pack
 import Lorentz.Doc
+import Lorentz.TypeAnns (HasTypeAnn)
 import Lorentz.Polymorphic
+import Michelson.Text (labelToMText)
 import Michelson.Typed.T
 import Michelson.Typed.Haskell.Value
-import Lorentz.UStore.Common
 import Lorentz.Value
+import Util.Label (Label)
 import Util.Type
 
 -- | Gathers multple fields and 'BigMap's under one object.
@@ -65,6 +66,7 @@
   } deriving stock (Eq, Show, Generic)
     deriving newtype (Default, Semigroup, Monoid, IsoValue,
                       MemOpHs, GetOpHs, UpdOpHs)
+    deriving anyclass HasTypeAnn
 
 instance Wrapped (UStore a)
 
@@ -132,16 +134,16 @@
 -- | Version of 'mkFieldMarkerUKey' which accepts label.
 mkFieldMarkerUKeyL
   :: forall marker field.
-     (KnownUStoreMarker marker, KnownSymbol field)
+     KnownUStoreMarker marker
   => Label field -> ByteString
-mkFieldMarkerUKeyL _ =
-  mkFieldMarkerUKey @marker (fieldNameToMText @field)
+mkFieldMarkerUKeyL label =
+  mkFieldMarkerUKey @marker (labelToMText label)
 
 -- | Shortcut for 'mkFieldMarkerUKey' which accepts not marker but store template
 -- and name of entry.
 mkFieldUKey
   :: forall (store :: Kind.Type) field.
-     (KnownSymbol field, KnownUStoreMarker (GetUStoreFieldMarker store field))
+     KnownUStoreMarker (GetUStoreFieldMarker store field)
   => Label field -> ByteString
 mkFieldUKey = mkFieldMarkerUKeyL @(GetUStoreFieldMarker store field)
 
diff --git a/src/Lorentz/Value.hs b/src/Lorentz/Value.hs
--- a/src/Lorentz/Value.hs
+++ b/src/Lorentz/Value.hs
@@ -1,33 +1,6 @@
 -- | Re-exports typed Value, CValue, some core types, some helpers and
 -- defines aliases for constructors of typed values.
 --
-
-{-
-TODO [TM-280]: Move this mess somewhere (in the last MR)
-
-This module also introduces several types for safe work with @address@ and
-@contract@ types, all available types for that are represented in the following
-table:
-
-+------------------------+------------+-------------------+----------------------+
-| Type                   | Type safe? | What it refers to | Michelson reflection |
-+========================+============+===================+======================+
-| Address                | No         | Whole contract    | address              |
-+------------------------+------------+-------------------+----------------------+
-| EpAddress              | No         | Entrypoint        | address              |
-+------------------------+------------+-------------------+----------------------+
-| TAddress               | Yes        | Whole contract    | address              |
-+------------------------+------------+-------------------+----------------------+
-| FutureContract         | Yes        | Entrypoint        | address              |
-+------------------------+------------+-------------------+----------------------+
-| ContractRef            | Yes        | Entrypoint        | contract             |
-+------------------------+------------+-------------------+----------------------+
-
-This module also provides functions for converting between this types in Haskell
-world.
-In Michelson world, you can use coercions and dedicated instructions from
-"Lorentz.Instr".
--}
 module Lorentz.Value
   ( Value
   , IsoValue (..)
@@ -86,162 +59,18 @@
   ) where
 
 import Data.Default (Default(..))
-import Data.Type.Bool (type (&&), Not)
-import Data.Kind as Kind
-import Data.Vinyl.Derived (Label(..))
 
-import Lorentz.Constraints
+import Lorentz.Address
 import Michelson.Text
 import Michelson.Typed
   (ContractRef(..), EntryPointCall, IsoCValue(..), IsoValue(..), SomeEntryPointCall, Value)
 import qualified Michelson.Typed as M
 import Michelson.Typed.CValue (CValue(..))
-import qualified Lorentz.EntryPoints.Core as Ep
 import Michelson.Typed.EntryPoints (EpAddress(..))
 import Tezos.Address (Address)
 import Tezos.Core
   (ChainId, Mutez, Timestamp, timestampFromSeconds, timestampFromUTCTime, timestampQuote, toMutez)
 import Tezos.Crypto (KeyHash, PublicKey, Signature)
-import Util.TypeLits
-import Util.Type
+import Util.Label (Label(..))
 
 type List = []
-
--- TODO (this MR): Add appropriate 'CanCastTo' instances
-
--- | Address which remembers the parameter type of the contract it refers to.
---
--- It differs from Michelson's @contract@ type because it cannot contain
--- entrypoint, and it always refers to entire contract parameter even if this
--- contract has explicit default entrypoint.
-newtype TAddress p = TAddress { unTAddress :: Address }
-  deriving stock Generic
-  deriving anyclass IsoValue
-
--- | Turn 'TAddress' to 'ContractRef' in /Haskell/ world.
---
--- This is an analogy of @address@ to @contract@ convertion in Michelson world,
--- thus you have to supply an entrypoint (or call the default one explicitly).
-callingTAddress
-  :: forall cp mname.
-     (NiceParameterFull cp)
-  => TAddress cp
-  -> Ep.EntryPointRef mname
-  -> ContractRef (Ep.GetEntryPointArgCustom cp mname)
-callingTAddress (TAddress addr) epRef =
-  withDict (niceParameterEvi @cp) $
-  case Ep.parameterEntryPointCallCustom @cp epRef of
-    epc@M.EntryPointCall{} -> ContractRef addr (M.SomeEpc epc)
-
--- | Specification of 'callTAddress' to call the default entrypoint.
-callingDefTAddress
-  :: forall cp.
-     (NiceParameterFull cp)
-  => TAddress cp
-  -> ContractRef (Ep.GetDefaultEntryPointArg cp)
-callingDefTAddress taddr = callingTAddress taddr Ep.CallDefault
-
--- | Address associated with value of @contract arg@ type.
---
--- Places where 'ContractRef' can appear are now severely limited,
--- this type gives you type-safety of 'ContractRef' but still can be used
--- everywhere.
--- This type is not a full-featured one rather a helper; in particular, once
--- pushing it on stack, you cannot return it back to Haskell world.
---
--- Note that it refers to an entrypoint of the contract, not just the contract
--- as a whole. In this sense this type differs from 'TAddress'.
---
--- Unlike with 'ContractRef', having this type you still cannot be sure that
--- the referred contract exists and need to perform a lookup before calling it.
-newtype FutureContract arg = FutureContract { unFutureContract :: ContractRef arg }
-
-instance IsoValue (FutureContract arg) where
-  type ToT (FutureContract arg) = ToT EpAddress
-  toVal (FutureContract contract) = toVal $ M.contractRefToAddr contract
-  fromVal = error "Fetching 'FutureContract' back from Michelson is impossible"
-
--- | Convert something to 'Address' in /Haskell/ world.
---
--- Use this when you want to access state of the contract and are not interested
--- in calling it.
-class ToAddress a where
-  toAddress :: a -> Address
-
-instance ToAddress Address where
-  toAddress = id
-
-instance ToAddress EpAddress where
-  toAddress = eaAddress
-
-instance ToAddress (TAddress cp) where
-  toAddress = unTAddress
-
-instance ToAddress (FutureContract cp) where
-  toAddress = toAddress . unFutureContract
-
-instance ToAddress (ContractRef cp) where
-  toAddress = crAddress
-
--- | Convert something referring to a contract (not specific entrypoint)
--- to 'TAddress' in /Haskell/ world.
-class ToTAddress (cp :: Kind.Type) (a :: Kind.Type) where
-  toTAddress :: a -> TAddress cp
-
-instance ToTAddress cp Address where
-  toTAddress = TAddress
-
-instance (cp ~ cp') => ToTAddress cp (TAddress cp') where
-  toTAddress = id
-
--- | Convert something to 'ContractRef' in /Haskell/ world.
-class ToContractRef (cp :: Kind.Type) (contract :: Kind.Type) where
-  toContractRef :: HasCallStack => contract -> ContractRef cp
-
-instance (cp ~ cp') => ToContractRef cp (ContractRef cp') where
-  toContractRef = id
-
-instance (NiceParameter cp, cp ~ cp') => ToContractRef cp (FutureContract cp') where
-  toContractRef = unFutureContract
-
-instance ( FailWhen cond msg
-         , cond ~
-            ( Ep.CanHaveEntryPoints cp &&
-              Not (Ep.ParameterEntryPointsDerivation cp == Ep.EpdNone)
-            )
-         , msg ~
-            ( 'Text "Cannot apply `ToContractRef` to `TAddress`" ':$$:
-              'Text "Consider using call(Def)TAddress first`" ':$$:
-              'Text "(or if you know your parameter type is primitive," ':$$:
-              'Text " make sure typechecker also knows about that)" ':$$:
-              'Text "For parameter `" ':<>: 'ShowType cp ':<>: 'Text "`"
-            )
-         , cp ~ arg, NiceParameter arg
-           -- These constraints should naturally derive from ones above,
-           -- but prooving that does not worth the effort
-         , NiceParameterFull cp, Ep.GetDefaultEntryPointArg cp ~ cp
-         ) =>
-         ToContractRef arg (TAddress cp) where
-  toContractRef = callingDefTAddress
-
--- | Convert something from 'ContractAddr' in /Haskell/ world.
-class FromContractRef (cp :: Kind.Type) (contract :: Kind.Type) where
-  fromContractRef :: ContractRef cp -> contract
-
-instance (cp ~ cp') => FromContractRef cp (ContractRef cp') where
-  fromContractRef = id
-
-instance (cp ~ cp') => FromContractRef cp (FutureContract cp') where
-  fromContractRef = FutureContract . fromContractRef
-
-instance FromContractRef cp EpAddress where
-  fromContractRef = M.contractRefToAddr
-
-instance FromContractRef cp Address where
-  fromContractRef = crAddress
-
-convertContractRef
-  :: forall cp contract2 contract1.
-     (ToContractRef cp contract1, FromContractRef cp contract2)
-  => contract1 -> contract2
-convertContractRef = fromContractRef @cp . toContractRef
diff --git a/src/Lorentz/Zip.hs b/src/Lorentz/Zip.hs
--- a/src/Lorentz/Zip.hs
+++ b/src/Lorentz/Zip.hs
@@ -18,7 +18,9 @@
 import qualified Data.Kind as Kind
 
 import Lorentz.Base
+import Lorentz.TypeAnns
 import Michelson.Typed
+import Michelson.Untyped (noAnn)
 
 -- | Zipping stack into tuple and back.
 class ZipInstr (s :: [Kind.Type]) where
@@ -71,3 +73,14 @@
   type ToT (inp :-> out) = 'TLambda (ToT (ZippedStack inp)) (ToT (ZippedStack out))
   toVal i = VLam . unLorentzInstr $ zippingStack i
   fromVal (VLam i) = zipInstr ## LorentzInstr i ## unzipInstr
+
+instance
+    ( HasTypeAnn (ZippedStack i)
+    , HasTypeAnn (ZippedStack o)
+    )
+  =>
+    HasTypeAnn (i :-> o)
+  where
+  getTypeAnn = NTLambda noAnn
+    (getTypeAnn @(ZippedStack i))
+    (getTypeAnn @(ZippedStack o))
diff --git a/test/Test/DocTest.hs b/test/Test/DocTest.hs
--- a/test/Test/DocTest.hs
+++ b/test/Test/DocTest.hs
@@ -15,7 +15,7 @@
 import Michelson.Doc
 
 -- A bad contract because it uses 'caseT' instead of 'entryCase'
-contract1 :: L.Contract (Either Integer Natural) Integer
+contract1 :: L.ContractCode (Either Integer Natural) Integer
 contract1 = L.car # L.caseT
   ( #cLeft /->
       L.doc (DDescription "Handles left") #
@@ -28,7 +28,7 @@
 contractDoc1 :: ContractDoc
 contractDoc1 = L.buildLorentzDoc contract1
 
-contract2 :: L.Contract (Either Integer Natural) Integer
+contract2 :: L.ContractCode (Either Integer Natural) Integer
 contract2 = L.car # L.entryCase (Proxy @PlainEntryPointsKind)
   ( #cLeft /-> L.nop
   , #cRight /-> L.int
diff --git a/test/Test/Lorentz/Doc/Positions.hs b/test/Test/Lorentz/Doc/Positions.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Lorentz/Doc/Positions.hs
@@ -0,0 +1,38 @@
+-- | Tests on ordering of documentation items.
+module Test.Lorentz.Doc.Positions
+  ( test_Errors
+  ) where
+
+import Data.Typeable (typeRep)
+import Fmt (pretty)
+import Test.HUnit (Assertion, assertFailure)
+import Test.Tasty (TestTree)
+import Test.Tasty.HUnit (testCase)
+
+import Lorentz.Errors
+import Lorentz.Errors.Numeric
+import Michelson.Doc
+
+-- | Test that one doc item goes before another doc item in generated
+-- documentation.
+(<.)
+  :: forall d1 d2.
+      (DocItem d1, DocItem d2)
+  => Proxy d1 -> Proxy d2 -> Assertion
+dp1 <. dp2 =
+  unless (p1 < p2) $
+    assertFailure $
+      "Doc item " <> show (typeRep dp1) <> " with position " <> pretty p1 <> " \
+      \goes before doc item " <> show (typeRep dp2) <> " with position " <> pretty p2
+  where
+    p1 = docItemPosition @d1
+    p2 = docItemPosition @d2
+
+test_Errors :: [TestTree]
+test_Errors =
+  [ testCase "Error tag mapping is described before errors" $
+      -- This is required because when @Errors@ section is modified
+      -- to mention numeric error tags, it needs some clarification
+      -- provided by @About error tag mapping@ section.
+      Proxy @DDescribeErrorTagMap <. Proxy @DError
+  ]
diff --git a/test/Test/Lorentz/EntryPoints.hs b/test/Test/Lorentz/EntryPoints.hs
--- a/test/Test/Lorentz/EntryPoints.hs
+++ b/test/Test/Lorentz/EntryPoints.hs
@@ -19,7 +19,7 @@
 import Test.TypeSpec (Is, TypeSpec(..))
 import Test.Util.TypeSpec (ExactlyIs)
 
-import Lorentz ((:!), ( # ), (/->))
+import Lorentz ((:!), ( # ), (/->), HasTypeAnn)
 import qualified Lorentz as L
 import Lorentz.Constraints
 import Lorentz.EntryPoints
@@ -39,7 +39,7 @@
   | Do3 MyEntryPoints2
   | Do4 MyParams
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints1a
   = Do1a Integer
@@ -47,92 +47,98 @@
   | Do3a MyEntryPoints2
   | Do4a MyParams
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints2
   = Do10
   | Do11 Natural
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints3
   = Do12 ("tuplearg" :! ("TL" :! Integer, "TR" :!  Natural), "boolarg" :! Bool)
   | Do13 ("integerarg" :! Integer, "boolarg" :! Bool)
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints4
   = Do14 ("viewarg1" :! L.View ("owner" :! L.Address) Natural)
   | Do15 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints5
   = Do16 ("maybearg" :! Maybe ("maybeinner" :! Natural))
   | Do17 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints6
   = Do18 ("lambdaarg" :! L.Lambda Natural Natural)
   | Do19 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints7
   = Do20 ("listarg" :! [("balance" :! Natural , "address" :! L.Address)])
   | Do21 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints8
   = Do22 ("maparg" :! (Map Natural ("balance" :! Natural , "address" :! L.Address)))
   | Do23 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints9
   = Do24 ("maybearg" L.:? ("maybeinner" :! Natural))
   | Do25 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPoints10
   = Do26 ("bigmaparg" :! L.Lambda (BigMap Natural ("balance" :! Natural , "address" :! L.Address)) ())
   | Do27 ()
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
+data MyEntryPoints11
+  = Do28 ("kek" :! Natural, "pek" :! Integer)
+  | Do29
+  deriving stock Generic
+  deriving anyclass (IsoValue, HasTypeAnn)
+
 data MyEntryPointsWithDef
   = Default Integer
   | NonDefault Natural
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyParams = MyParams
   { param1 :: ()
   , param2 :: ByteString
   }
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 -- Normally this cannot declare entrypoints because this is not a sum type.
 -- But we will declare them forcibly
 data MySingleEntryPoint = Dos1 Integer
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPointsDelegated
   = Dod1
   | Dod2 MyEntryPointsSubDelegated
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 data MyEntryPointsSubDelegated
   = Dosd1
   | Dosd2
   deriving stock Generic
-  deriving anyclass IsoValue
+  deriving anyclass (IsoValue, HasTypeAnn)
 
 instance ParameterHasEntryPoints MyEntryPoints1 where
   type ParameterEntryPointsDerivation MyEntryPoints1 = EpdRecursive
@@ -167,6 +173,9 @@
 instance ParameterHasEntryPoints MyEntryPoints10 where
   type ParameterEntryPointsDerivation MyEntryPoints10 = EpdPlain
 
+instance ParameterHasEntryPoints MyEntryPoints11 where
+  type ParameterEntryPointsDerivation MyEntryPoints11 = EpdNone
+
 instance ParameterHasEntryPoints MyEntryPointsWithDef where
   type ParameterEntryPointsDerivation MyEntryPointsWithDef = EpdPlain
 
@@ -179,7 +188,7 @@
 instance ParameterHasEntryPoints MyEntryPointsSubDelegated where
   type ParameterEntryPointsDerivation MyEntryPointsSubDelegated = EpdNone
 
-dummyContract :: L.Contract param ()
+dummyContract :: L.ContractCode param ()
 dummyContract = L.drop L.# L.unit L.# L.nil L.# L.pair
 
 -- | Helper datatype which contains field annotations from 'NTOr'.
@@ -338,6 +347,13 @@
           @?=
           TANodePair noAnn (TALeaf noAnn) (TANodeLambda noAnn (TALeaf noAnn) (TALeaf noAnn))
       ]
+  , testCase "EpdNone case (type annotations are preserved)" $
+      (paramAnnTree $ compileLorentzContract (dummyContract @MyEntryPoints11))
+      @?=
+      (TANodeOr noAnn
+        (TANodePair noAnn (TALeaf (ann "kek")) (TALeaf (ann "pek")))
+        (TALeaf noAnn)
+      )
   ]
   where
     paramAnnTree :: FullContract cp st -> TypeAnnTree cp
@@ -390,9 +406,9 @@
      )
   => EntryPointRef mname
   -> arg
-  -> L.Contract (TAddress cp) ()
+  -> L.ContractCode (TAddress cp) ()
 callerContract epRef arg =
-  L.car # L.contractCalling @cp epRef #
+  L.car # L.contractCalling epRef #
   L.assertSome [mt|Contract lookup failed|] #
   L.push (toMutez 1) # L.push arg # L.transferTokens #
   L.dip (L.unit # L.nil) # L.cons # L.pair
diff --git a/test/Test/Lorentz/EntryPoints/Doc.hs b/test/Test/Lorentz/EntryPoints/Doc.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Lorentz/EntryPoints/Doc.hs
@@ -0,0 +1,231 @@
+-- | Tests on autodoc for entrypoints.
+module Test.Lorentz.EntryPoints.Doc
+  ( test_ParamBuildingSteps_are_correct
+  , test_Finalization_check
+  , unit_Uncallables_detection
+  ) where
+
+import Control.Spoon (teaspoon)
+import Test.HUnit (Assertion, assertBool, (@?=))
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase)
+
+import Lorentz ((:->), (/->))
+import qualified Lorentz as L
+import Lorentz.Doc
+import Lorentz.EntryPoints
+import Lorentz.EntryPoints.Doc
+import Lorentz.Test.Doc
+import Lorentz.TypeAnns
+import Lorentz.Value
+import Michelson.Untyped (EpName(..))
+
+-- Parameters
+----------------------------------------------------------------------------
+
+data MySub
+  = Dos1
+  | Dos2
+  deriving stock (Generic)
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+instance TypeHasDoc MySub where
+  typeDocMdDescription = "MySub"
+
+mySubImpl :: '[MySub] :-> '[]
+mySubImpl = L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDos1 /-> L.nop
+  , #cDos2 /-> L.nop
+  )
+
+data MyPlainEps
+  = Do1 Integer
+  | Do2 MySub
+  deriving stock (Generic)
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+instance TypeHasDoc MyPlainEps where
+  typeDocMdDescription = "MyPlainEps"
+
+instance ParameterHasEntryPoints MyPlainEps where
+  type ParameterEntryPointsDerivation MyPlainEps = EpdPlain
+
+myPlainImplDumb :: '[MyPlainEps] :-> '[]
+myPlainImplDumb = L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDo1 /-> L.drop
+  , #cDo2 /-> mySubImpl
+  )
+
+myPlainImpl :: '[MyPlainEps] :-> '[]
+myPlainImpl = finalizeParamCallingDoc myPlainImplDumb
+
+data MyRecursiveEps
+  = Dor1 Integer
+  | Dor2 MySub
+  deriving stock (Generic)
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+instance ParameterHasEntryPoints MyRecursiveEps where
+  type ParameterEntryPointsDerivation MyRecursiveEps = EpdRecursive
+
+myRecursiveImpl :: '[MyRecursiveEps] :-> '[]
+myRecursiveImpl = finalizeParamCallingDoc $
+  L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDor1 /-> L.drop
+  , #cDor2 /-> mySubImpl
+  )
+
+data MyDelegateEps
+  = Dod1 Integer
+  | Dod2 MyPlainEps
+  deriving stock (Generic)
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+instance ParameterHasEntryPoints MyDelegateEps where
+  type ParameterEntryPointsDerivation MyDelegateEps = EpdDelegate
+
+myDelegateImpl :: '[MyDelegateEps] :-> '[]
+myDelegateImpl = finalizeParamCallingDoc $
+  L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDod1 /-> L.drop
+  , #cDod2 /-> myPlainImplDumb
+  )
+
+myDelegateImplFinalizedTwice :: '[MyDelegateEps] :-> '[]
+myDelegateImplFinalizedTwice = finalizeParamCallingDoc $
+  L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDod1 /-> L.drop
+  , #cDod2 /-> myPlainImpl
+  )
+
+data MyDefEps
+  = Do0
+  | Default
+  deriving stock (Generic)
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+instance TypeHasDoc MyDefEps where
+  typeDocMdDescription = "MyDefEps"
+
+instance ParameterHasEntryPoints MyDefEps where
+  type ParameterEntryPointsDerivation MyDefEps = EpdPlain
+
+myDefImplDumb :: '[MyDefEps] :-> '[]
+myDefImplDumb =
+  L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDo0 /-> L.nop
+  , #cDefault /-> L.nop
+  )
+
+myDefImpl :: '[MyDefEps] :-> '[]
+myDefImpl = finalizeParamCallingDoc myDefImplDumb
+
+data MyRecursiveDefEps
+  = Dord1 MySub
+  | Dord2 MyDefEps
+  deriving stock (Generic)
+  deriving anyclass (IsoValue, HasTypeAnn)
+
+instance ParameterHasEntryPoints MyRecursiveDefEps where
+  type ParameterEntryPointsDerivation MyRecursiveDefEps = EpdRecursive
+
+myRecursiveDefImpl :: '[MyRecursiveDefEps] :-> '[]
+myRecursiveDefImpl = finalizeParamCallingDoc $
+  L.entryCase (Proxy @PlainEntryPointsKind)
+  ( #cDord1 /-> mySubImpl
+  , #cDord2 /-> myDefImplDumb
+  )
+
+-- Tests
+----------------------------------------------------------------------------
+
+-- Similar to 'ParamBuildingSteps', but without details irrelevant for testing
+data ParamBuildingType
+    -- | Wrap into constructor with given name
+    -- NB: starts with capital letter
+  = PbtWrapIn Text
+    -- | Call given entrypoint
+    -- NB: starts with lowercase letter
+  | PbtCallEntrypoint Text
+    -- | Does something weird
+  | PbtCustom
+    -- | Entrypoint cannot be called
+  | PbtUncallable
+  deriving stock (Show, Eq)
+
+pbsType :: ParamBuildingStep -> ParamBuildingType
+pbsType = \case
+  PbsWrapIn ctor _ -> PbtWrapIn ctor
+  PbsCallEntrypoint (unEpName -> ep) -> PbtCallEntrypoint ep
+  PbsCustom _ -> PbtCustom
+  PbsUncallable _ -> PbtUncallable
+
+getAllBuildingSteps :: (i :-> o) -> [[ParamBuildingType]]
+getAllBuildingSteps instr =
+  forEachContractDocItem (L.buildLorentzDoc instr) (map pbsType . epaBuilding)
+
+test_ParamBuildingSteps_are_correct :: [TestTree]
+test_ParamBuildingSteps_are_correct =
+  [ testCase "Simple entrypoints without direct calling" $
+      getAllBuildingSteps myPlainImplDumb
+        @?= [ [PbtWrapIn "Do1"]
+            , [PbtWrapIn "Do2"]
+            , [PbtWrapIn "Do2", PbtWrapIn "Dos1"]
+            , [PbtWrapIn "Do2", PbtWrapIn "Dos2"]
+            ]
+
+  , testCase "Simple entrypoints" $
+      getAllBuildingSteps myPlainImpl
+        @?= [ [PbtCallEntrypoint "do1"]
+            , [PbtCallEntrypoint "do2"]
+            , [PbtCallEntrypoint "do2", PbtWrapIn "Dos1"]
+            , [PbtCallEntrypoint "do2", PbtWrapIn "Dos2"]
+            ]
+  , testCase "Recursive entrypoints" $
+      getAllBuildingSteps myRecursiveImpl
+        @?= [ [PbtCallEntrypoint "dor1"]
+            , [PbtCallEntrypoint "", PbtWrapIn "Dor2"]
+            , [PbtCallEntrypoint "dos1"]
+            , [PbtCallEntrypoint "dos2"]
+            ]
+  , testCase "Delegate entrypoints" $
+      getAllBuildingSteps myDelegateImpl
+        @?= [ [PbtCallEntrypoint "dod1"]
+            , [PbtCallEntrypoint "dod2"]
+            , [PbtCallEntrypoint "do1"]
+            , [PbtCallEntrypoint "do2"]
+            , [PbtCallEntrypoint "do2", PbtWrapIn "Dos1"]
+            , [PbtCallEntrypoint "do2", PbtWrapIn "Dos2"]
+            ]
+
+  , testGroup "With explicit default"
+    [ testCase "Simple" $
+        getAllBuildingSteps myDefImpl
+          @?= [ [PbtCallEntrypoint "do0"]
+              , [PbtCallEntrypoint ""]
+              ]
+    , testCase "Recursive" $
+        getAllBuildingSteps myRecursiveDefImpl
+          @?= [ [PbtUncallable]  -- Dord1 itself
+              , [PbtCallEntrypoint "dos1"]
+              , [PbtCallEntrypoint "dos2"]
+              , [PbtUncallable]  -- Dord2 itself
+              , [PbtCallEntrypoint "do0"]
+              , [PbtCallEntrypoint ""]
+              ]
+    ]
+  ]
+
+test_Finalization_check :: [TestTree]
+test_Finalization_check =
+  [ testCase "Cannot apply second time" $
+      assertBool "Finalization unexpectedly didn't fail second time" $
+        isNothing $ teaspoon myDelegateImplFinalizedTwice
+  ]
+
+-- | Note [doc for uncallable entrypoints]:
+-- This test is a proof of that sometimes not all entrypoints are callable.
+unit_Uncallables_detection :: Assertion
+unit_Uncallables_detection =
+  expectDocTestFailure testAllEntrypointsAreCallable $
+    buildLorentzDoc myRecursiveDefImpl
diff --git a/test/Test/Lorentz/Errors.hs b/test/Test/Lorentz/Errors.hs
--- a/test/Test/Lorentz/Errors.hs
+++ b/test/Test/Lorentz/Errors.hs
@@ -136,5 +136,5 @@
   validate . Left $
     lExpectErrorNumeric errorTagMap (== VoidResult False)
 
-voidSample :: Contract (Void_ Bool Bool) ()
+voidSample :: ContractCode (Void_ Bool Bool) ()
 voidSample = car # void_ L.not
diff --git a/test/Test/Lorentz/Errors/Numeric.hs b/test/Test/Lorentz/Errors/Numeric.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Lorentz/Errors/Numeric.hs
@@ -0,0 +1,67 @@
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Lorentz.Errors.Numeric
+  ( test_Documentation
+  ) where
+
+import qualified Data.Kind as Kind
+import Data.Typeable (eqT)
+import Test.HUnit (assertFailure)
+import Test.Tasty (TestTree)
+import Test.Tasty.HUnit (testCase)
+
+import qualified Lorentz as L
+import Lorentz.Base
+import Lorentz.Doc
+import Lorentz.Errors
+import Lorentz.Value
+import Lorentz.Errors.Numeric
+import Michelson.Doc (lookupDocBlockSection)
+
+type instance ErrorArg "myError" = ()
+type instance ErrorArg "myNonMappedError" = ()
+
+instance CustomErrorHasDoc "myError" where
+  customErrClass = ErrClassActionException
+  customErrDocMdCause = "An error happened"
+
+instance CustomErrorHasDoc "myNonMappedError" where
+  customErrClass = ErrClassActionException
+  customErrDocMdCause = "A non-mapped error happened"
+
+contract :: Lambda () ()
+contract =
+  L.push True #
+  L.if_ (L.failCustom_ #myError)
+        (L.failCustom_ #myNonMappedError)
+
+errorTagMap :: ErrorTagMap
+errorTagMap =
+  excludeErrorTags (one [mt|MyNonMappedError|]) $
+  buildErrorTagMap $ gatherErrorTags contract
+
+test_Documentation :: [TestTree]
+test_Documentation =
+  [ testCase "Documentation is updated" $ do
+      let docum = buildLorentzDoc $ applyErrorTagToErrorsDoc errorTagMap contract
+          contents = cdContents docum
+          dThrows = lookupDocBlockSection @DThrows contents
+                 ?: error "Suddenly found no DThrow doc items"
+
+      let
+        throws :: forall (e :: Kind.Type). Typeable e => DThrows -> Bool
+        throws (DThrows (_ :: Proxy e')) = isJust $ eqT @e @e'
+
+        anyThrows :: forall (e :: Kind.Type). Typeable e => Bool
+        anyThrows = any (throws @e) dThrows
+
+      when (anyThrows @(CustomError "myError")) $
+        assertFailure "Old 'myError' remained"
+      unless (anyThrows @(NumericErrorWrapper 0 (CustomError "myError"))) $
+        assertFailure "Mapped 'myError' does not appear in the result with tag 0"
+
+      unless (anyThrows @(CustomError "myNonMappedError")) $
+        assertFailure "Old 'myNonMappedError' is not remained"
+      when (anyThrows @(NumericErrorWrapper 1 (CustomError "myNonMappedError"))) $
+        assertFailure "'myNonMappedError' appears mapped in the result"
+  ]
diff --git a/test/Test/Lorentz/Interpreter.hs b/test/Test/Lorentz/Interpreter.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Lorentz/Interpreter.hs
@@ -0,0 +1,119 @@
+module Test.Lorentz.Interpreter
+  ( test_Entry_points_lookup
+  , test_Entry_points_calling
+  ) where
+
+import qualified Data.Map as Map
+import System.FilePath ((</>))
+import Test.Tasty (TestTree, testGroup)
+import Test.Tasty.HUnit (testCase)
+import Util.Named ((.!))
+
+import Lorentz.Test.Integrational
+import Michelson.Interpret (ContractEnv(..))
+import Michelson.Test (contractProp, testTreesWithTypedContract)
+import Michelson.Test.Dummy (dummyContractEnv)
+import Michelson.Test.Integrational (genesisAddress, integrationalTestExpectation, validate)
+import Michelson.Test.Unit
+import Michelson.Text
+import Michelson.Typed (IsoValue(..))
+import qualified Michelson.Typed as T
+import qualified Michelson.Untyped as U
+import Tezos.Address
+import Tezos.Core
+
+test_Entry_points_lookup :: IO [TestTree]
+test_Entry_points_lookup =
+  testTreesWithTypedContract (dir </> "call1.mtz") $ \call1 ->
+  testTreesWithTypedContract (dir </> "call2.mtz") $ \call2 ->
+  testTreesWithTypedContract (dir </> "call3.mtz") $ \call3 ->
+  testTreesWithTypedContract (dir </> "call4.mtz") $ \call4 ->
+  testTreesWithTypedContract (dir </> "call5.mtz") $ \call5 ->
+  testTreesWithTypedContract (dir </> "call6.mtz") $ \call6 ->
+  testTreesWithTypedContract (dir </> "call7.mtz") $ \call7 ->
+  pure
+  [ testGroup "Calling contract without default entrypoint"
+    [ testCase "Calling default entrypoint refers to the root" $
+        checkProp call1 validateSuccess (addr "simple")
+    , testCase "Calling some entrypoint refers this entrypoint" $
+        checkProp call7 validateSuccess (addr "simple")
+    ]
+  , testGroup "Calling contract with default entrypoint"
+    [ testCase "Calling default entrypoint works" $
+        checkProp call2 validateSuccess (addr "def")
+    ]
+  , testGroup "Common failures"
+    [ testCase "Fails on type mismatch" $
+        checkProp call1 validateFailure (addr "def")
+    , testCase "Fails on entrypoint not found" $
+        checkProp call3 validateFailure (addr "simple")
+    ]
+  , testGroup "Referring entrypoints groups"
+    [ testCase "Can refer entrypoint group" $
+        checkProp call4 validateSuccess (addr "complex")
+    , testCase "Works with annotations" $
+        checkProp call5 validateSuccess (addr "complex")
+    , testCase "Does not work on annotations mismatch in 'contract' type argument" $
+        checkProp call6 validateFailure (addr "complex")
+    ]
+  ]
+  where
+    checkProp contract validator callee =
+      contractProp @Address @()
+        contract validator
+        dummyContractEnv{ ceContracts = Map.fromList env }
+        callee ()
+    validateFailure = validateMichelsonFailsWith ()
+
+    dir = entrypointsDir
+    contractSimpleTy =
+      U.Type (U.TOr (U.ann "a") (U.ann "b") (U.Type U.Tint U.noAnn) (U.Type U.Tnat U.noAnn))
+             U.noAnn
+    contractComplexTy =
+      U.Type (U.TOr (U.ann "s") (U.ann "t") (U.Type U.Tstring U.noAnn) contractSimpleTy)
+             U.noAnn
+    contractWithDefTy =
+      U.Type (U.TOr (U.ann "a") (U.ann "default") (U.Type U.Tnat U.noAnn) (U.Type U.Tstring U.noAnn))
+             U.noAnn
+    addr = mkContractAddressRaw
+    env =
+      [ (mkContractHashRaw "simple", contractSimpleTy)
+      , (mkContractHashRaw "complex", contractComplexTy)
+      , (mkContractHashRaw "def", contractWithDefTy)
+      ]
+
+test_Entry_points_calling :: IO [TestTree]
+test_Entry_points_calling =
+  testTreesWithTypedContract (dir </> "call1.mtz") $
+    \(call1 :: T.FullContract (ToT Address) (ToT ())) ->
+  testTreesWithTypedContract (dir </> "contract1.mtz") $
+    \(contract1 :: T.FullContract (ToT (Either Integer MText)) (ToT Integer)) ->
+  testTreesWithTypedContract (dir </> "self1.mtz") $
+    \(self1 :: T.FullContract (ToT (Either Integer ())) (ToT Integer)) ->
+  pure
+  [ testCase "Calling some entrypoint in CONTRACT" $
+      integrationalTestExpectation $ do
+        callerRef <- tOriginate call1 "caller" (toVal ()) (toMutez 100)
+        targetRef <- tOriginate contract1 "target" (toVal @Integer 0) (toMutez 100)
+
+        tTransfer (#from .! genesisAddress) (#to .! callerRef) (toMutez 1)
+          T.DefEpName (toVal targetRef)
+
+        validate . Right $
+          tExpectStorageConst targetRef (toVal @Integer 5)
+
+  , testCase "Calling some entrypoint in SELF" $
+      integrationalTestExpectation $ do
+        contractRef <- tOriginate self1 "self" (toVal @Integer 0) (toMutez 100)
+
+        tTransfer (#from .! genesisAddress) (#to .! contractRef) (toMutez 1)
+          T.DefEpName (toVal $ Right @Integer ())
+
+        validate . Right $
+          tExpectStorageConst contractRef (toVal @Integer 5)
+  ]
+  where
+    dir = entrypointsDir
+
+entrypointsDir :: FilePath
+entrypointsDir = ".." </> ".." </> "contracts" </> "entrypoints"
diff --git a/test/Test/Lorentz/Macro.hs b/test/Test/Lorentz/Macro.hs
--- a/test/Test/Lorentz/Macro.hs
+++ b/test/Test/Lorentz/Macro.hs
@@ -6,6 +6,8 @@
 
 module Test.Lorentz.Macro
   ( unit_duupX
+  , unit_replaceN
+  , unit_updateN
   , test_execute
   ) where
 
@@ -26,6 +28,33 @@
   where
     duupX3 :: [Bool, Integer, (), Bool] :-> [(), Bool, Integer, (), Bool]
     duupX3 = dipN @2 dup # dig @2
+
+unit_replaceN :: Assertion
+unit_replaceN = do
+  replaceN @1 @?= swap # drop
+  replaceN @2 @?= replaceN2
+  replaceN @3 @?= replaceN3
+  where
+    replaceN2 :: [(), Integer, (), Bool] :-> [Integer, (), Bool]
+    replaceN2 = dipN @2 drop # dug @1
+
+    replaceN3 :: [Bool, Integer, (), Bool] :-> [Integer, (), Bool]
+    replaceN3 = dipN @3 drop # dug @2
+
+unit_updateN :: Assertion
+unit_updateN = do
+  updateN @1 cons @?= updateN1
+  updateN @2 cons @?= updateN2
+  updateN @3 cons @?= updateN3
+  where
+    updateN1 :: [Bool, [Bool], Integer, ()] :-> [[Bool], Integer, ()]
+    updateN1 = cons
+
+    updateN2 :: [Bool, Integer, [Bool], ()] :-> [Integer, [Bool], ()]
+    updateN2 = swap # dip cons
+
+    updateN3 :: [Bool, Integer, (), [Bool]] :-> [Integer, (), [Bool]]
+    updateN3 = dug @2 # dipN @2 cons
 
 test_execute :: [TestTree]
 test_execute =
diff --git a/test/Test/Lorentz/Pack.hs b/test/Test/Lorentz/Pack.hs
--- a/test/Test/Lorentz/Pack.hs
+++ b/test/Test/Lorentz/Pack.hs
@@ -5,13 +5,13 @@
   ) where
 
 import Prelude hiding (drop, swap)
-import Test.HUnit (Assertion, (@?=), assertFailure)
+import Test.HUnit (Assertion, assertFailure, (@?=))
 import Test.Tasty (TestTree)
 import Test.Tasty.HUnit (testCase)
 
 import Lorentz
-import Michelson.Typed.Instr (Instr (..))
-import Michelson.Typed.Util (DfsSettings (..), dfsFoldInstr)
+import Michelson.Typed.Instr (Instr(..))
+import Michelson.Typed.Util (DfsSettings(..), dfsFoldInstr)
 
 test_lambda_roundtrip :: [TestTree]
 test_lambda_roundtrip =
diff --git a/test/Test/Lorentz/Print.hs b/test/Test/Lorentz/Print.hs
--- a/test/Test/Lorentz/Print.hs
+++ b/test/Test/Lorentz/Print.hs
@@ -15,7 +15,7 @@
 import Lorentz hiding (contract, unpack)
 import qualified Lorentz as L
 import Michelson.Printer.Util (buildRenderDoc)
-import Michelson.Typed hiding (Contract)
+import Michelson.Typed hiding (ContractCode)
 import Michelson.Untyped (para)
 
 data MyEntryPoints1
@@ -28,7 +28,7 @@
 instance ParameterHasEntryPoints MyEntryPoints1 where
   type ParameterEntryPointsDerivation MyEntryPoints1 = EpdPlain
 
-contract :: Contract MyEntryPoints1 ()
+contract :: ContractCode MyEntryPoints1 ()
 contract = drop # unit # nil # pair
 
 test_Print_parameter_annotations :: [TestTree]
@@ -49,7 +49,7 @@
         code = drop # lambda (drop # unit)
      in printLorentzValue True code
         @?=
-        "{ DROP; LAMBDA int unit       { DROP;UNIT } }"
+        "{ DROP; LAMBDA  int  unit  { DROP;UNIT } }"
   ]
 
 data TestParam
@@ -64,7 +64,7 @@
 unit_Erase_annotations :: Assertion
 unit_Erase_annotations =
   let
-    myContract :: Contract TestParam ()
+    myContract :: ContractCode TestParam ()
     myContract = cdr # nil # L.pair
     expected = "parameter (or (pair %testCon1 (nat :a) (bool :b)) (unit %testCon2));storage unit;code { CAST (pair (or (pair nat bool) unit) unit);CDR;NIL operation;PAIR };"
   in assertEqual
diff --git a/test/Test/Util/TypeSpec.hs b/test/Test/Util/TypeSpec.hs
--- a/test/Test/Util/TypeSpec.hs
+++ b/test/Test/Util/TypeSpec.hs
@@ -2,10 +2,10 @@
   ( ExactlyIs
   ) where
 
-import Test.TypeSpec.Core
 import Data.Singletons.Prelude.Eq (DefaultEq)
+import Test.TypeSpec.Core
 import Util.Type (If)
-import Util.TypeLits (ErrorMessage (..))
+import Util.TypeLits (ErrorMessage(..))
 
 -- | Like 'Is' but ensures that arguments match in kind.
 data ExactlyIs (actual :: k) (expected :: k)
