diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,6 +2,33 @@
 ==========
 <!-- Append new entries here -->
 
+0.11.0
+======
+* [!814](https://gitlab.com/morley-framework/morley/-/merge_requests/814)
+  + Added the usage of `Prelude.Type` instead of `Data.Kind.Type`,
+    as a result `Kind.Type` was replaced with just `Type`.
+* [!745](https://gitlab.com/morley-framework/morley/-/merge_requests/745)
+  + Generalize `st*` methods for working with storage.
+    Now it is possible to access nested fields and submaps like `stToField (#a :-| #b)`.
+    This should not require any changes unless you keep you own generic helpers over those methods.
+  + Existing `StoreHasSubmap (Big?)Map anyName k v` instance is replaced with two:
+    * `StoreHasSubmap (Big?)Map Self k v`
+    * `StoreHasSubmap store name k v` that delegates to `StoreHasField`.
+
+    Migration guide:
+    * If you have `StoreHasSubmap` instances for specific storage and name implemented via
+      `storeSubmapOpsDeeper`, remove them and make sure you have a similar `StoreHasField`
+      instance implemented via `storeFieldOpsADT`.
+    * If you have storage which is directly a map, use `this` instead of label to access the map.
+    * If you have an instance for a complex storage which is not represented as simple ADT,
+      turn this instance into overlappable one.
+* [!807](https://gitlab.com/morley-framework/morley/-/merge_requests/807)
+  + Add some instances to `BigMap` and `TAddress` types.
+* [!787](https://gitlab.com/morley-framework/morley/-/merge_requests/787)
+  + Added new Edo macros: `CAR k` and `CDR k` as `carN` and `cdrN`.
+* [!798](https://gitlab.com/morley-framework/morley/-/merge_requests/798)
+  + Added back the `UnaryArithOpHs Abs Integer` instance that was removed by accident.
+
 0.10.0
 ======
 * [!774](https://gitlab.com/morley-framework/morley/-/merge_requests/774)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -35,7 +35,7 @@
 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])
+(inp :: [Type]) :-> (out :: [Type])
 ```
 
 In order to list types on the stack, we will use `:` operator.
diff --git a/lorentz.cabal b/lorentz.cabal
--- a/lorentz.cabal
+++ b/lorentz.cabal
@@ -1,11 +1,11 @@
 cabal-version: 2.0
 
--- This file has been generated from package.yaml by hpack version 0.34.2.
+-- This file has been generated from package.yaml by hpack version 0.34.3.
 --
 -- see: https://github.com/sol/hpack
 
 name:           lorentz
-version:        0.10.0
+version:        0.11.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
@@ -13,7 +13,7 @@
 bug-reports:    https://gitlab.com/morley-framework/morley/-/issues
 author:         camlCase, Serokell, Tocqueville Group
 maintainer:     Serokell <hi@serokell.io>
-copyright:      2019-2020 Tocqueville Group
+copyright:      2019-2021 Tocqueville Group
 license:        MIT
 license-file:   LICENSE
 build-type:     Simple
@@ -70,6 +70,7 @@
       Lorentz.Run
       Lorentz.Run.Simple
       Lorentz.StoreClass
+      Lorentz.StoreClass.Extra
       Lorentz.UParam
       Lorentz.Util.TH
       Lorentz.Value
@@ -82,7 +83,7 @@
   hs-source-dirs:
       src
   default-extensions: AllowAmbiguousTypes ApplicativeDo BangPatterns BlockArguments ConstraintKinds DataKinds DefaultSignatures DeriveAnyClass DeriveDataTypeable DeriveFoldable DeriveFunctor DeriveGeneric DeriveTraversable DerivingStrategies DerivingVia EmptyCase FlexibleContexts FlexibleInstances GADTs GeneralizedNewtypeDeriving LambdaCase MultiParamTypeClasses MultiWayIf NamedFieldPuns NegativeLiterals NumericUnderscores NumDecimals OverloadedLabels OverloadedStrings PatternSynonyms PolyKinds QuasiQuotes RankNTypes RecordWildCards RecursiveDo ScopedTypeVariables StandaloneDeriving StrictData TemplateHaskell TupleSections TypeApplications TypeFamilies TypeOperators UndecidableInstances UndecidableSuperClasses ViewPatterns
-  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude
+  ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages
   build-depends:
       aeson-pretty
     , base-noprelude >=4.7 && <5
diff --git a/src/Lorentz/ADT.hs b/src/Lorentz/ADT.hs
--- a/src/Lorentz/ADT.hs
+++ b/src/Lorentz/ADT.hs
@@ -43,7 +43,6 @@
   ) where
 
 import Data.Constraint ((\\))
-import qualified Data.Kind as Kind
 import Data.Vinyl.Core (RMap(..), Rec(..))
 import GHC.TypeLits (AppendSymbol, Symbol)
 import Named ((:!), (:?), arg, argDef, argF)
@@ -70,12 +69,12 @@
   )
 
 -- | A pair of field name and type.
-data NamedField = NamedField Symbol Kind.Type
+data NamedField = NamedField Symbol Type
 type n := ty = 'NamedField n ty
 infixr 0 :=
 
 -- | Shortcut for multiple 'HasFieldOfType' constraints.
-type family HasFieldsOfType (dt :: Kind.Type) (fs :: [NamedField])
+type family HasFieldsOfType (dt :: Type) (fs :: [NamedField])
              :: Constraint where
   HasFieldsOfType _ '[] = ()
   HasFieldsOfType dt ((n := ty) ': fs) =
@@ -211,8 +210,8 @@
 wrapOne = case appendCtorFieldAxiom @(GetCtorField dt name) @st of
   Dict -> I . instrWrapOne @dt
 
--- | Lorentz analogy of 'CaseClause', it works on plain 'Kind.Type' types.
-data CaseClauseL (inp :: [Kind.Type]) (out :: [Kind.Type]) (param :: CaseClauseParam) where
+-- | Lorentz analogy of 'CaseClause', it works on plain 'Type' types.
+data CaseClauseL (inp :: [Type]) (out :: [Type]) (param :: CaseClauseParam) where
   CaseClauseL :: AppendCtorField x inp :-> out -> CaseClauseL inp out ('CaseClauseParam ctor x)
 
 -- | Provides "case" arrow which works on different wrappers for clauses.
diff --git a/src/Lorentz/Address.hs b/src/Lorentz/Address.hs
--- a/src/Lorentz/Address.hs
+++ b/src/Lorentz/Address.hs
@@ -50,8 +50,8 @@
   , M.coerceContractRef
   ) where
 
-import Data.Kind as Kind
-import Data.Type.Bool (type (&&), Not)
+import Data.Type.Bool (Not, type (&&))
+import Fmt (Buildable)
 
 import Lorentz.Annotation
 import Lorentz.Base
@@ -70,7 +70,8 @@
 -- 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 stock (Generic, Show)
+  deriving newtype (Eq, Ord, Buildable)
   deriving anyclass (IsoValue, HasAnnotation)
 
 -- | Turn 'TAddress' to 'ContractRef' in /Haskell/ world.
@@ -153,7 +154,7 @@
 
 -- | Convert something referring to a contract (not specific entrypoint)
 -- to 'TAddress' in /Haskell/ world.
-class ToTAddress (cp :: Kind.Type) (a :: Kind.Type) where
+class ToTAddress (cp :: Type) (a :: Type) where
   toTAddress :: a -> TAddress cp
 
 instance ToTAddress cp Address where
@@ -163,7 +164,7 @@
   toTAddress = id
 
 -- | Convert something to 'ContractRef' in /Haskell/ world.
-class ToContractRef (cp :: Kind.Type) (contract :: Kind.Type) where
+class ToContractRef (cp :: Type) (contract :: Type) where
   toContractRef :: HasCallStack => contract -> ContractRef cp
 
 instance (cp ~ cp') => ToContractRef cp (ContractRef cp') where
@@ -193,7 +194,7 @@
   toContractRef = callingDefTAddress
 
 -- | Convert something from 'ContractAddr' in /Haskell/ world.
-class FromContractRef (cp :: Kind.Type) (contract :: Kind.Type) where
+class FromContractRef (cp :: Type) (contract :: Type) where
   fromContractRef :: ContractRef cp -> contract
 
 instance (cp ~ cp') => FromContractRef cp (ContractRef cp') where
diff --git a/src/Lorentz/Annotation.hs b/src/Lorentz/Annotation.hs
--- a/src/Lorentz/Annotation.hs
+++ b/src/Lorentz/Annotation.hs
@@ -35,7 +35,7 @@
   (BigMap, ContractRef(..), EpAddress, KnownIsoT, Notes(..), Operation, ToT, insertTypeAnn,
   starNotes)
 import Michelson.Typed.Haskell.Value (GValueType)
-import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, ann, noAnn)
+import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, mkAnnotationUnsafe, noAnn)
 import Tezos.Address
 import Tezos.Core
 import Tezos.Crypto
@@ -75,7 +75,7 @@
 ----------------------------------------------------------------------------
 
 ctorNameToAnnWithOptions :: forall ctor. (KnownSymbol ctor, HasCallStack) => AnnOptions -> FieldAnn
-ctorNameToAnnWithOptions o = ann . fieldAnnModifier o $ headToLower $ (symbolValT' @ctor)
+ctorNameToAnnWithOptions o = mkAnnotationUnsafe . fieldAnnModifier o $ headToLower $ (symbolValT' @ctor)
 
 -- | Used in `GHasAnnotation` and `HasAnnotation` as a flag to track
 -- whether or not it directly follows an entrypoint to avoid introducing
@@ -114,7 +114,7 @@
     getAnnotation @a b
     where
       symbolAnn :: forall s. KnownSymbol s => TypeAnn
-      symbolAnn = ann $ symbolValT' @s
+      symbolAnn = mkAnnotationUnsafe $ symbolValT' @s
 
 instance (HasAnnotation (Maybe a), KnownSymbol name)
   => HasAnnotation (NamedF Maybe a name) where
diff --git a/src/Lorentz/Arith.hs b/src/Lorentz/Arith.hs
--- a/src/Lorentz/Arith.hs
+++ b/src/Lorentz/Arith.hs
@@ -9,26 +9,24 @@
   , ToIntegerArithOpHs
   ) where
 
-import qualified Data.Kind as Kind
-
 import Lorentz.Value
 import Michelson.Typed.Arith
 
 -- | Lifted 'ArithOp'.
 class ( ArithOp aop (ToT n) (ToT m)
       , ToT (ArithResHs aop n m) ~ ArithRes aop (ToT n) (ToT m)
-      ) => ArithOpHs (aop :: Kind.Type) (n :: Kind.Type) (m :: Kind.Type) where
-  type ArithResHs aop n m :: Kind.Type
+      ) => ArithOpHs (aop :: Type) (n :: Type) (m :: Type) where
+  type ArithResHs aop n m :: Type
 
 -- | Lifted 'UnaryArithOp'.
 class ( UnaryArithOp aop (ToT n)
       , ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)
-      ) => UnaryArithOpHs (aop :: Kind.Type) (n :: Kind.Type) where
-  type UnaryArithResHs aop n :: Kind.Type
+      ) => UnaryArithOpHs (aop :: Type) (n :: Type) where
+  type UnaryArithResHs aop n :: Type
 
 class ( ToIntArithOp (ToT n)
       ) =>
-      ToIntegerArithOpHs (n :: Kind.Type)
+      ToIntegerArithOpHs (n :: Type)
 
 instance ArithOpHs Add Natural Integer where
   type ArithResHs Add Natural Integer = Integer
@@ -132,6 +130,9 @@
 
 instance ArithOpHs Lsr Natural Natural where
   type ArithResHs Lsr Natural Natural = Natural
+
+instance UnaryArithOpHs Abs Integer where
+  type UnaryArithResHs Abs Integer = Natural
 
 instance UnaryArithOpHs Not Integer where
   type UnaryArithResHs Not Integer = Integer
diff --git a/src/Lorentz/Base.hs b/src/Lorentz/Base.hs
--- a/src/Lorentz/Base.hs
+++ b/src/Lorentz/Base.hs
@@ -33,7 +33,6 @@
   ) where
 
 import Data.Default (def)
-import qualified Data.Kind as Kind
 import qualified Data.List.NonEmpty as NE (fromList)
 import Fmt (Buildable(..))
 
@@ -50,7 +49,7 @@
 import qualified Michelson.Untyped as U
 
 -- | Alias for instruction which hides inner types representation via 'T'.
-newtype (inp :: [Kind.Type]) :-> (out :: [Kind.Type]) = LorentzInstr
+newtype (inp :: [Type]) :-> (out :: [Type]) = LorentzInstr
   { unLorentzInstr :: RemFail Instr (ToTs inp) (ToTs out)
   } deriving newtype (Show, Eq)
 infixr 1 :->
@@ -120,7 +119,7 @@
 --
 -- We discourage its use as this hinders reading error messages
 -- (the compiler inserts unnecessary parentheses and indentation).
-type (&) (a :: Kind.Type) (b :: [Kind.Type]) = a ': b
+type (&) (a :: Type) (b :: [Type]) = a ': b
 infixr 2 &
 
 (#) :: (a :-> b) -> (b :-> c) -> a :-> c
diff --git a/src/Lorentz/Bytes.hs b/src/Lorentz/Bytes.hs
--- a/src/Lorentz/Bytes.hs
+++ b/src/Lorentz/Bytes.hs
@@ -24,7 +24,6 @@
   , Keccak
   ) where
 
-import qualified Data.Kind as Kind
 import Fmt (Buildable(..))
 import qualified Type.Reflection as Refl
 import Util.Markdown
@@ -118,7 +117,7 @@
 
 -- | Open kind for hash algorithms, to make it more difficult to apply type
 -- arguments incorrectly.
-type HashAlgorithmKind = HashAlgoTag -> Kind.Type
+type HashAlgorithmKind = HashAlgoTag -> Type
 data HashAlgoTag
 
 -- | Hash of type @t@ evaluated from data of type @a@.
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
@@ -47,7 +47,6 @@
   ) where
 
 import Data.Constraint ((\\))
-import qualified Data.Kind as Kind
 import Data.Typeable (typeRep)
 import Data.Vinyl (Rec(..))
 import Fcf (Eval, Exp)
@@ -86,10 +85,10 @@
   -- 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)]
+  type EpdAllEntrypoints deriv cp :: [(Symbol, Type)]
 
   -- | Get entrypoint argument by name.
-  type EpdLookupEntrypoint deriv cp :: Symbol -> Exp (Maybe Kind.Type)
+  type EpdLookupEntrypoint deriv cp :: Symbol -> Exp (Maybe Type)
 
   -- | Construct parameter annotations corresponding to expected entrypoints set.
   --
@@ -121,7 +120,7 @@
   RequireAllUniqueEntrypoints' (ParameterEntrypointsDerivation cp) cp
 
 -- | Result of entrypoint lookup at term level.
-data EpConstructionRes (param :: T) (marg :: Maybe Kind.Type) where
+data EpConstructionRes (param :: T) (marg :: Maybe Type) where
   EpConstructed
     :: ParameterScope (ToT arg)
     => EpLiftSequence (ToT arg) param -> EpConstructionRes param ('Just arg)
@@ -132,9 +131,9 @@
 --
 -- 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
+data EpCallingDesc (info :: (Symbol, Type)) where
   EpCallingDesc ::
-    { epcdArg :: Proxy (arg :: Kind.Type)
+    { epcdArg :: Proxy (arg :: Type)
       -- ^ Entrypoint argument type.
     , epcdEntrypoint :: EpName
       -- ^ Name of assigned entrypoint.
@@ -159,7 +158,7 @@
       , RequireAllUniqueEntrypoints cp
       ) =>
       ParameterHasEntrypoints cp where
-  type ParameterEntrypointsDerivation cp :: Kind.Type
+  type ParameterEntrypointsDerivation cp :: Type
 
 -- | Parameter declares some entrypoints.
 --
@@ -238,16 +237,16 @@
 ----------------------------------------------------------------------------
 
 -- | Get all entrypoints declared for parameter.
-type family AllParameterEntrypoints (cp :: Kind.Type)
-             :: [(Symbol, Kind.Type)] where
+type family AllParameterEntrypoints (cp :: Type)
+             :: [(Symbol, Type)] where
   AllParameterEntrypoints cp =
     EpdAllEntrypoints (GetParameterEpDerivation cp) cp
 
 -- | Lookup for entrypoint type by name.
 --
 -- Does not treat default entrypoints in a special way.
-type family LookupParameterEntrypoint (cp :: Kind.Type)
-             :: Symbol -> Exp (Maybe Kind.Type) where
+type family LookupParameterEntrypoint (cp :: Type)
+             :: Symbol -> Exp (Maybe Type) where
   LookupParameterEntrypoint cp =
     EpdLookupEntrypoint (GetParameterEpDerivation cp) cp
 
@@ -404,7 +403,7 @@
     parameterEntrypointCall @cp (fromLabel @name)
 
 -- | Universal entrypoint lookup.
-type family GetEntrypointArgCustom cp mname :: Kind.Type where
+type family GetEntrypointArgCustom cp mname :: Type where
   GetEntrypointArgCustom cp 'Nothing = GetDefaultEntrypointArg cp
   GetEntrypointArgCustom cp ('Just name) = GetEntrypointArg cp name
 
@@ -468,7 +467,7 @@
   = (GetEntrypointArgCustom param ('Just con) ~ exp, ParameterDeclaresEntrypoints param)
 
 -- | A helper datatype which prettifies interface for `ParameterContainsEntrypoints`.
-data NamedEp = NamedEp Symbol Kind.Type
+data NamedEp = NamedEp Symbol Type
 type n :> ty = 'NamedEp n ty
 infixr 0 :>
 
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
@@ -46,7 +46,6 @@
 import Control.Lens.Cons (_head)
 import Data.Char (toLower)
 import Data.Constraint (Dict(..))
-import qualified Data.Kind as Kind
 import qualified Data.Map as Map
 import Data.Singletons (sing)
 import qualified Data.Text as T
@@ -86,7 +85,7 @@
 -- corresponding to various parts of a contract - specifying different @kind@
 -- type argument for each of those groups will allow you defining different
 -- 'DocItem' instances with appropriate custom descriptions for them.
-data DEntrypoint (kind :: Kind.Type) = DEntrypoint
+data DEntrypoint (kind :: Type) = DEntrypoint
   { depName :: Text
   , depSub :: SubDoc
   }
@@ -140,7 +139,7 @@
 --
 -- All such entrypoints will be placed under the same "entrypoints" section,
 -- and this instance defines characteristics of this section.
-class Typeable ep => EntrypointKindHasDoc (ep :: Kind.Type) where
+class Typeable ep => EntrypointKindHasDoc (ep :: Type) where
   -- | Position of the respective entrypoints section in the doc.
   -- This shares the same positions space with all other doc items.
   entrypointKindPos :: Natural
@@ -333,7 +332,7 @@
   , epaBuilding = []
   }
 
-mkDEpUType :: forall t. (KnownValue t, HasAnnotation t) => Untyped.Type
+mkDEpUType :: forall t. (KnownValue t, HasAnnotation t) => Untyped.Ty
 mkDEpUType = mkUType (getAnnotation @t FollowEntrypoint)
 
 mkDEntrypointArgSimple
@@ -461,7 +460,7 @@
 -- | Traverse entry points and add parameter building step (which describes
 -- necessity to wrap parameter into some constructor of the given datatype)
 -- to all parameters described within given code.
-class GDocumentEntrypoints (kind :: Kind.Type) (x :: Kind.Type -> Kind.Type) where
+class GDocumentEntrypoints (kind :: Type) (x :: Type -> Type) where
   -- | Add corresponding parameter building step.
   --
   -- First argument is accumulator for Michelson description of the building step.
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
@@ -10,17 +10,15 @@
   , RequireSumType
   ) where
 
-import qualified Data.Kind as Kind
-
 import Michelson.Typed.Haskell
 import Michelson.Typed.T
-import Michelson.Untyped (EpName, FieldAnn, ann, epNameFromParamAnn)
+import Michelson.Untyped (EpName, FieldAnn, mkAnnotationUnsafe, epNameFromParamAnn)
 import Util.Text
 import Util.Type
 import Util.TypeLits
 
 ctorNameToAnn :: forall ctor. (KnownSymbol ctor, HasCallStack) => FieldAnn
-ctorNameToAnn = ann . headToLower $ (symbolValT' @ctor)
+ctorNameToAnn = mkAnnotationUnsafe . headToLower $ (symbolValT' @ctor)
 
 ctorNameToEp :: forall ctor. (KnownSymbol ctor, HasCallStack) => EpName
 ctorNameToEp =
@@ -39,7 +37,7 @@
 deriving anyclass instance (WellTypedIsoValue r) => IsoValue (ShouldHaveEntrypoints r)
 
 -- | Used to understand whether a type can potentially declare any entrypoints.
-type family CanHaveEntrypoints (p :: Kind.Type) :: Bool where
+type family CanHaveEntrypoints (p :: Type) :: Bool where
   CanHaveEntrypoints (ShouldHaveEntrypoints _) = 'True
   CanHaveEntrypoints p = CanHaveEntrypointsT (ToT p)
 
@@ -50,7 +48,7 @@
 -- | Ensure that given type is a sum type.
 --
 -- This helps to prevent attempts to apply a function to, for instance, a pair.
-type family RequireSumType (a :: Kind.Type) :: Constraint where
+type family RequireSumType (a :: Type) :: Constraint where
   RequireSumType a =
     If (CanHaveEntrypoints a)
        (() :: Constraint)
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
@@ -16,7 +16,6 @@
   , BuildEPTree
   ) where
 
-import qualified Data.Kind as Kind
 import Data.Singletons.Prelude (SBool(SFalse, STrue))
 import Data.Singletons.Prelude.Eq ((%==))
 import Data.Vinyl.Core (Rec(..), (<+>))
@@ -29,7 +28,7 @@
 import Lorentz.Value
 import Michelson.Typed
 import Michelson.Typed.Haskell.Value (GValueType)
-import Michelson.Untyped (FieldAnn, ann, noAnn)
+import Michelson.Untyped (FieldAnn, mkAnnotationUnsafe, noAnn)
 import Util.Fcf (type (<|>), Over2, TyEqSing)
 import Util.Type
 
@@ -108,7 +107,7 @@
       '[ Fcf.Is (TyEqSing r) ('Just cp)
        , Fcf.Else (PlainLookupEntrypointExt deriv cp)
        ]
-  epdNotes = (plainEpdNotesExt @deriv @cp, ann (symbolValT' @r))
+  epdNotes = (plainEpdNotesExt @deriv @cp, mkAnnotationUnsafe (symbolValT' @r))
   epdCall label@(Label :: Label name) = case sing @r %== sing @name of
       STrue -> EpConstructed EplArgHere
       SFalse -> plainEpdCallExt @deriv @cp label
@@ -164,7 +163,7 @@
 -- | Build 'EPTree' by parameter type.
 type BuildEPTree mode a = GBuildEntrypointsTree mode (G.Rep a)
 
-type family GBuildEntrypointsTree (mode :: Kind.Type) (x :: Kind.Type -> Kind.Type)
+type family GBuildEntrypointsTree (mode :: Type) (x :: Type -> Type)
              :: EPTree where
   GBuildEntrypointsTree mode (G.D1 _ x) =
     GBuildEntrypointsTree mode x
@@ -225,9 +224,9 @@
 type LookupEntrypoint mode ep a = GLookupEntrypoint mode ep (G.Rep a)
 
 -- | Generic traversal for 'EntrypointsNotes'.
-class GEntrypointsNotes (mode :: Kind.Type) (ep :: EPTree) (x :: Kind.Type -> Kind.Type) where
-  type GAllEntrypoints mode ep x :: [(Symbol, Kind.Type)]
-  type GLookupEntrypoint mode ep x :: Symbol -> Exp (Maybe Kind.Type)
+class GEntrypointsNotes (mode :: Type) (ep :: EPTree) (x :: Type -> Type) where
+  type GAllEntrypoints mode ep x :: [(Symbol, Type)]
+  type GLookupEntrypoint mode ep x :: Symbol -> Exp (Maybe Type)
 
   {- | Returns:
     1. Notes corresponding to this level;
@@ -373,7 +372,7 @@
        ]
 
 -- Get field type under 'G.C1'.
-type family GExtractField (x :: Kind.Type -> Kind.Type) where
+type family GExtractField (x :: Type -> Type) where
   GExtractField (G.S1 _ x) = GExtractField x
   GExtractField (G.Rec0 a) = a
   GExtractField G.U1 = ()
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
@@ -8,8 +8,6 @@
   ( ParameterWrapper (..)
   ) where
 
-import qualified Data.Kind as Kind
-
 import Lorentz.Constraints
 import Lorentz.Entrypoints.Core
 import Lorentz.Wrappable (Wrappable)
@@ -17,7 +15,7 @@
 
 -- | Wrap parameter into this to locally assign a way to derive entrypoints for
 -- it.
-newtype ParameterWrapper (deriv :: Kind.Type) cp = ParameterWrapper { unParameterWraper :: cp }
+newtype ParameterWrapper (deriv :: Type) cp = ParameterWrapper { unParameterWraper :: cp }
   deriving stock Generic
   deriving anyclass (IsoValue, Wrappable)
 
diff --git a/src/Lorentz/Errors.hs b/src/Lorentz/Errors.hs
--- a/src/Lorentz/Errors.hs
+++ b/src/Lorentz/Errors.hs
@@ -49,7 +49,6 @@
   ) where
 
 import qualified Data.Char as C
-import qualified Data.Kind as Kind
 import qualified Data.List as L
 import Data.Singletons (demote)
 import Data.Typeable (cast)
@@ -107,7 +106,7 @@
   => Value t -> Either Text e
 isoErrorFromVal e = fromVal <$> gcastE e
 
-class Typeable e => ErrorHasDoc (e :: Kind.Type) where
+class Typeable e => ErrorHasDoc (e :: Type) where
   -- | Name of error as it appears in the corresponding section title.
   errorDocName :: Text
 
@@ -135,7 +134,7 @@
   -- You are not oblidged to often instantiate this correctly, it is only useful
   -- for some utilities.
   type ErrorRequirements e :: Constraint
-  type ErrorRequirements e = ()
+  type ErrorRequirements _ = ()
 
   -- | Captured constraints which we require in a particular instance.
   -- This is a way to encode a bidirectional instance in the nowaday Haskell,
@@ -279,7 +278,7 @@
 (and cons here is that each such tag will need to be declared first).
 
 -}
-type family ErrorArg (tag :: Symbol) :: Kind.Type
+type family ErrorArg (tag :: Symbol) :: Type
 
 -- | Material custom error.
 --
@@ -308,7 +307,7 @@
 -- | How 'CustomError' is actually represented in Michelson.
 type CustomErrorRep tag = CustomErrorArgRep (ErrorArg tag)
 
-type family CustomErrorArgRep (errArg :: Kind.Type) where
+type family CustomErrorArgRep (errArg :: Type) where
   CustomErrorArgRep NoErrorArg = MText
   CustomErrorArgRep UnitErrorArg = (MText, ())
   CustomErrorArgRep errArg = (MText, errArg)
@@ -478,7 +477,7 @@
       errorToVal (mkCustomError ()) cont
   errorFromVal v =
     reifyTypeEquality @arg @() $
-      errorFromVal v <&> \(CustomError l (a, ())) -> \b -> CustomError l (a, b)
+      errorFromVal v <&> \(CustomError l a) -> \b -> CustomError l (fst a, b)
 
 instance (Typeable arg, ErrorHasDoc (CustomError tag)) =>
          ErrorHasDoc (arg -> CustomError tag) where
diff --git a/src/Lorentz/Errors/Numeric/Doc.hs b/src/Lorentz/Errors/Numeric/Doc.hs
--- a/src/Lorentz/Errors/Numeric/Doc.hs
+++ b/src/Lorentz/Errors/Numeric/Doc.hs
@@ -19,7 +19,6 @@
 
 import Control.Monad.Cont (callCC, runCont)
 import qualified Data.Bimap as Bimap
-import qualified Data.Kind as Kind
 import Data.Typeable (typeRep)
 import Fmt (build, pretty)
 import GHC.TypeNats (Nat)
@@ -193,7 +192,7 @@
     mdLocalRef "error tags mapping" dDescribeErrorTagMapAnchor <> "."
 
 -- | Some error with a numeric tag attached.
-data NumericErrorWrapper (numTag :: Nat) (err :: Kind.Type)
+data NumericErrorWrapper (numTag :: Nat) (err :: Type)
 
 instance ( ErrorHasDoc err
          , KnownNat numTag, ErrorHasNumericDoc err
diff --git a/src/Lorentz/Extensible.hs b/src/Lorentz/Extensible.hs
--- a/src/Lorentz/Extensible.hs
+++ b/src/Lorentz/Extensible.hs
@@ -56,7 +56,6 @@
   ) where
 
 import Data.Char (isSpace)
-import qualified Data.Kind as Kind
 import qualified Data.Text as T
 import Fmt (Buildable(build), (+||), (|+), (||+))
 import GHC.Generics ((:+:)(..))
@@ -163,7 +162,7 @@
     'Ctor i name param ': EnumerateCtorsImpl ('Position (i + 1)) cs
 
 -- | Having a sum-type, yields a type-level list of its constructors
-type family GGetCtors (x :: Kind.Type -> Kind.Type) :: [CtorKind] where
+type family GGetCtors (x :: Type -> Type) :: [CtorKind] where
   GGetCtors (G.D1 _ x) = GGetCtors x
   GGetCtors (G.C1 ('G.MetaCons name _1 _2) (G.S1 _3 (G.Rec0 param)))
     = '[ '(name, 'OneField param) ]
@@ -172,7 +171,7 @@
   GGetCtors (x :+: y) = GGetCtors x ++ GGetCtors y
 
 -- | Generic implementation of toExtVal and fromExtVal
-class GExtVal t (x :: Kind.Type -> Kind.Type) where
+class GExtVal t (x :: Type -> Type) where
   gToExtVal :: x p -> Extensible t
   gFromExtVal :: Extensible t -> Either ExtConversionError (x p)
 
diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs
--- a/src/Lorentz/Instr.hs
+++ b/src/Lorentz/Instr.hs
@@ -131,7 +131,6 @@
   (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)
 
 import Data.Constraint ((\\))
-import qualified Data.Kind as Kind
 import Data.Singletons (SingI, sing)
 import qualified GHC.TypeNats as GHC (Nat)
 
@@ -149,7 +148,7 @@
   (CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG,
   ConstraintDUG', ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN,
   EntrypointCallT(..), ExtInstr(..), GetN, Instr(..), RemFail(..), SomeEntrypointCallT(..), UpdateN,
-  Value'(..), pattern CAR, pattern CDR, pattern PAIR, sepcName, starNotes)
+  Value'(..), pattern CAR, pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, sepcName, starNotes)
 import Michelson.Typed.Arith
 import Michelson.Typed.Haskell.Value
 import Util.Peano
@@ -182,7 +181,7 @@
 
 -- | Drop top @n@ elements from the stack.
 dropN ::
-  forall (n :: GHC.Nat) (s :: [Kind.Type]).
+  forall (n :: GHC.Nat) (s :: [Type]).
   -- Note: if we introduce `nPeano ~ ToPeano n` variable,
   -- GHC will complain that this constraint is redundant.
   ( SingI (ToPeano n), KnownPeano (ToPeano n)
@@ -198,10 +197,10 @@
 dup :: a : s :-> a : a : s
 dup = I DUP
 
-type ConstraintDUPNLorentz (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type])
-  (a :: Kind.Type) =
+type ConstraintDUPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
+  (a :: Type) =
   ( ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a)
-  , ConstraintDUPN' Kind.Type n inp out a
+  , ConstraintDUPN' Type n inp out a
   )
 
 dupNPeano ::
@@ -223,16 +222,16 @@
 swap = I SWAP
 
 -- See a comment about `ConstraintDIPNLorentz'.
-type ConstraintDIGLorentz (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type])
-  (a :: Kind.Type) =
+type ConstraintDIGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
+  (a :: Type) =
   ( ConstraintDIG n (ToTs inp) (ToTs out) (ToT a)
-  , ConstraintDIG' Kind.Type n inp out a
+  , ConstraintDIG' Type n inp out a
   )
 
-type ConstraintDUGLorentz (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type])
-  (a :: Kind.Type) =
+type ConstraintDUGLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
+  (a :: Type) =
   ( ConstraintDUG n (ToTs inp) (ToTs out) (ToT a)
-  , ConstraintDUG' Kind.Type n inp out a
+  , ConstraintDUG' Type n inp out a
   )
 
 -- | Version of `dig` which uses Peano number.
@@ -350,18 +349,18 @@
   => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s
 get = I GET
 
-type ConstraintPairGetLorentz (n :: GHC.Nat) (pair :: Kind.Type) =
+type ConstraintPairGetLorentz (n :: GHC.Nat) (pair :: Type) =
   ( ConstraintGetN (ToPeano n) (ToT pair)
   , ToT (PairGetHs (ToPeano n) pair) ~ GetN (ToPeano n) (ToT pair)
   )
 
-type family PairGetHs (ix :: Peano) (pair :: Kind.Type) :: Kind.Type where
+type family PairGetHs (ix :: Peano) (pair :: Type) :: Type where
   PairGetHs 'Z val                 = val
   PairGetHs ('S 'Z) (left, _)      = left
   PairGetHs ('S ('S n)) (_, right) = PairGetHs n right
 
 pairGet
-  :: forall (n :: GHC.Nat) (pair :: Kind.Type) (s :: [Kind.Type]).
+  :: forall (n :: GHC.Nat) (pair :: Type) (s :: [Type]).
      ConstraintPairGetLorentz n pair
   => pair : s :-> PairGetHs (ToPeano n) pair : s
 pairGet = I (GETN (peanoSing @n))
@@ -372,18 +371,18 @@
 update :: UpdOpHs c => UpdOpKeyHs c : UpdOpParamsHs c : c : s :-> c : s
 update = I UPDATE
 
-type ConstraintPairUpdateLorentz (n :: GHC.Nat) (val :: Kind.Type) (pair :: Kind.Type) =
+type ConstraintPairUpdateLorentz (n :: GHC.Nat) (val :: Type) (pair :: Type) =
   ( ConstraintUpdateN (ToPeano n) (ToT pair)
   , ToT (PairUpdateHs (ToPeano n) val pair) ~ UpdateN (ToPeano n) (ToT val) (ToT pair)
   )
 
-type family PairUpdateHs (ix :: Peano) (val :: Kind.Type) (pair :: Kind.Type) :: Kind.Type where
+type family PairUpdateHs (ix :: Peano) (val :: Type) (pair :: Type) :: Type where
   PairUpdateHs 'Z          val _             = val
   PairUpdateHs ('S 'Z)     val (_, right)    = (val, right)
   PairUpdateHs ('S ('S n)) val (left, right) = (left, PairUpdateHs n val right)
 
 pairUpdate
-  :: forall (n :: GHC.Nat) (val :: Kind.Type) (pair :: Kind.Type) (s :: [Kind.Type]).
+  :: forall (n :: GHC.Nat) (val :: Type) (pair :: Type) (s :: [Type]).
      ConstraintPairUpdateLorentz n val pair
   => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s
 pairUpdate = I (UPDATEN (peanoSing @n))
@@ -453,22 +452,22 @@
 -- 'ToTs' is not injective, hence 's0' is ambiguous.
 -- So we need both and we merge them into one to avoid a warning about
 -- a redundant constraint.
-type ConstraintDIPNLorentz (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type])
-  (s :: [Kind.Type]) (s' :: [Kind.Type]) =
+type ConstraintDIPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
+  (s :: [Type]) (s' :: [Type]) =
   ( ConstraintDIPN n (ToTs inp) (ToTs out) (ToTs s) (ToTs s')
-  , ConstraintDIPN' Kind.Type n inp out s s'
+  , ConstraintDIPN' Type n inp out s s'
   )
 
 -- | Version of `dipN` which uses Peano number.
 -- It is intended for internal usage in Lorentz.
 dipNPeano ::
-  forall (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type]) (s :: [Kind.Type]) (s' :: [Kind.Type]).
+  forall (n :: Peano) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
   ( ConstraintDIPNLorentz n inp out s s'
   ) => s :-> s' -> inp :-> out
 dipNPeano (iNonFailingCode -> a) = I (DIPN (sing @n) a)
 
 dipN ::
-  forall (n :: GHC.Nat) (inp :: [Kind.Type]) (out :: [Kind.Type]) (s :: [Kind.Type]) (s' :: [Kind.Type]).
+  forall (n :: GHC.Nat) (inp :: [Type]) (out :: [Type]) (s :: [Type]) (s' :: [Type]).
   ( ConstraintDIPNLorentz (ToPeano n) inp out s s'
   ) => s :-> s' -> inp :-> out
 dipN = dipNPeano @(ToPeano n)
@@ -828,7 +827,7 @@
   -> k : UpdOpParamsHs c : c : s :-> c : s
 updateNew mkErr = failingWhenPresent mkErr # update
 
-class LorentzFunctor (c :: Kind.Type -> Kind.Type) where
+class LorentzFunctor (c :: Type -> Type) where
   lmap :: KnownValue b => (a : s :-> b : s) -> (c a : s :-> c b : s)
 
 instance LorentzFunctor Maybe where
diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs
--- a/src/Lorentz/Macro.hs
+++ b/src/Lorentz/Macro.hs
@@ -2,6 +2,8 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
+{-# LANGUAGE NoStarIsType #-}
+
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
 
@@ -66,6 +68,8 @@
   , cloneX
   , duupX
   , framedN
+  , carN
+  , cdrN
   , caar
   , cadr
   , cdar
@@ -124,12 +128,11 @@
 
 import Prelude hiding (and, compare, drop, some, swap)
 
-import qualified Data.Kind as Kind
 import Data.Singletons (SingI(..))
 import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+))
 import Fmt.Internal.Tuple (TupleF)
 import qualified GHC.TypeLits as Lit
-import GHC.TypeNats (type (-))
+import GHC.TypeNats (type (-), type (+), type (*))
 import qualified GHC.TypeNats as GHC (Nat)
 
 import Lorentz.Annotation
@@ -326,7 +329,7 @@
 dropX = dipN @n @inp @out @s @s' drop
 
 class CloneX (n :: Peano) a s where
-  type CloneXT n a s :: [Kind.Type]
+  type CloneXT n a s :: [Type]
   cloneXImpl :: a : s :-> CloneXT n a s
 instance CloneX 'Z a s where
   type CloneXT 'Z a s = a : s
@@ -375,6 +378,33 @@
     -> Integer : Natural : () : s :-> ByteString : () : s
   _example = framedN @2
 
+carN
+  :: forall (n :: GHC.Nat) (pair :: Type) (s :: [Type]).
+     ConstraintPairGetLorentz (2 * n + 1) pair
+  => pair : s :-> PairGetHs (ToPeano (2 * n + 1)) pair : s
+carN = pairGet @(2 * n + 1)
+  where
+    _example :: '[ (String, (Integer, ())) ] :-> '[ String ]
+    _example = carN @0
+
+    _example' :: '[ (String, (Integer, ())) ] :-> '[ Integer ]
+    _example' = carN @1
+
+cdrN
+  :: forall (n :: GHC.Nat) (pair :: Type) (s :: [Type]).
+     ConstraintPairGetLorentz (2 * n) pair
+  => pair : s :-> PairGetHs (ToPeano (2 * n)) pair : s
+cdrN = pairGet @(2 * n)
+  where
+    _example :: '[ (String, (Integer, ())) ] :-> '[ (String, (Integer, ())) ]
+    _example = cdrN @0
+
+    _example' :: '[ (String, (Integer, ())) ] :-> '[ (Integer, ()) ]
+    _example' = cdrN @1
+
+    _example'' :: '[ (String, (Integer, ())) ] :-> '[ () ]
+    _example'' = cdrN @2
+
 papair :: a : b : c : s :-> ((a, b), c) : s
 papair = pair # pair
 
@@ -494,13 +524,13 @@
 -- | 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]) =
+  (s :: [Type]) (a :: Type)
+  (mid :: [Type]) (tail :: [Type]) =
   ( ReplaceNConstraint' T n (ToTs s) (ToT a) (ToTs mid) (ToTs tail)
-  , ReplaceNConstraint' Kind.Type n s a mid tail
+  , ReplaceNConstraint' Type n s a mid tail
   )
 
-class ReplaceN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) mid tail where
+class ReplaceN (n :: Peano) (s :: [Type]) (a :: Type) mid tail where
   replaceNImpl :: a ': s :-> s
 
 instance {-# OVERLAPPING #-} (s ~ (a ': xs)) => ReplaceN ('S 'Z) s a mid tail where
@@ -519,7 +549,7 @@
 -- 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]).
+replaceN :: forall (n :: GHC.Nat) a (s :: [Type]) (s1 :: [Type]) (tail :: [Type]).
   ( ConstraintReplaceNLorentz (ToPeano (n - 1)) s a s1 tail
   , ReplaceN (ToPeano n) s a s1 tail
   )
@@ -542,13 +572,13 @@
 -- | 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]) =
+  (s :: [Type]) (a :: Type) (b :: Type)
+  (mid :: [Type]) (tail :: [Type]) =
   ( UpdateNConstraint' T n (ToTs s) (ToT a) (ToT b) (ToTs mid) (ToTs tail)
-  , UpdateNConstraint' Kind.Type n s a b mid tail
+  , UpdateNConstraint' Type n s a b mid tail
   )
 
-class UpdateN (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) (b :: Kind.Type) mid tail where
+class UpdateN (n :: Peano) (s :: [Type]) (a :: Type) (b :: Type) mid tail where
   updateNImpl
     :: '[a, b] :-> '[b]
     -> a ': s :-> s
@@ -576,7 +606,7 @@
 -- 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]).
+updateN :: forall (n :: GHC.Nat) a b (s :: [Type]) (mid :: [Type]) (tail :: [Type]).
   ( ConstraintUpdateNLorentz (ToPeano (n - 1)) s a b mid tail
   , UpdateN (ToPeano n) s a b mid tail
   )
@@ -594,7 +624,7 @@
 ----------------------------------------------------------------------------
 
 -- | @view@ type synonym as described in A1.
-data View (a :: Kind.Type) (r :: Kind.Type) = View
+data View (a :: Type) (r :: Type) = View
   { viewParam :: a
   , viewCallbackTo :: ContractRef r
   } deriving stock (Eq, Show, Generic)
@@ -657,7 +687,7 @@
   transferTokens # nil # swap # cons # pair
 
 -- | @void@ type synonym as described in A1.
-data Void_ (a :: Kind.Type) (b :: Kind.Type) = Void_
+data Void_ (a :: Type) (b :: Type) = Void_
   { voidParam :: a
     -- ^ Entry point argument.
   , voidResProxy :: Lambda b b
@@ -804,7 +834,7 @@
 
 -- | Duplicate two topmost items on top of the stack.
 dupTop2 ::
-  forall (a :: Kind.Type) (b :: Kind.Type) (s :: [Kind.Type]).
+  forall (a :: Type) (b :: Type) (s :: [Type]).
   a ': b ': s :-> a ': b ': a ': b ': s
 dupTop2 = dupN @2 # dupN @2
 
diff --git a/src/Lorentz/Polymorphic.hs b/src/Lorentz/Polymorphic.hs
--- a/src/Lorentz/Polymorphic.hs
+++ b/src/Lorentz/Polymorphic.hs
@@ -19,8 +19,6 @@
   , IsoMapOpRes
   ) where
 
-import qualified Data.Kind as Kind
-
 import Lorentz.Constraints.Scopes (NiceComparable)
 import Michelson.Text
 import Michelson.Typed
@@ -34,7 +32,7 @@
 class ( MemOp (ToT c)
       , ToT (MemOpKeyHs c) ~ MemOpKey (ToT c)
       ) => MemOpHs c where
-  type MemOpKeyHs c :: Kind.Type
+  type MemOpKeyHs c :: Type
 
 instance NiceComparable e => MemOpHs (Set e) where
   type MemOpKeyHs (Set e) = e
@@ -56,8 +54,8 @@
       , ToT (MapOpInpHs c) ~ MapOpInp (ToT c)
       , ToT (MapOpResHs c ()) ~ MapOpRes (ToT c) (ToT ())
       ) => MapOpHs c where
-  type MapOpInpHs c :: Kind.Type
-  type MapOpResHs c :: Kind.Type -> Kind.Type
+  type MapOpInpHs c :: Type
+  type MapOpResHs c :: Type -> Type
 
 instance NiceComparable k => MapOpHs (Map k v) where
   type MapOpInpHs (Map k v) = (k, v)
@@ -71,7 +69,7 @@
 class ( IterOp (ToT c)
       , ToT (IterOpElHs c) ~ IterOpEl (ToT c)
       ) => IterOpHs c where
-  type IterOpElHs c :: Kind.Type
+  type IterOpElHs c :: Type
 
 instance NiceComparable k => IterOpHs (Map k v) where
   type IterOpElHs (Map k v) = (k, v)
@@ -99,8 +97,8 @@
       , ToT (UpdOpKeyHs c) ~ (UpdOpKey (ToT c))
       , ToT (UpdOpParamsHs c) ~ UpdOpParams (ToT c)
       ) => UpdOpHs c where
-  type UpdOpKeyHs c :: Kind.Type
-  type UpdOpParamsHs c :: Kind.Type
+  type UpdOpKeyHs c :: Type
+  type UpdOpParamsHs c :: Type
 
 instance NiceComparable k => UpdOpHs (Map k v) where
   type UpdOpKeyHs (Map k v) = k
@@ -119,8 +117,8 @@
       , ToT (GetOpKeyHs c) ~ (GetOpKey (ToT c))
       , ToT (GetOpValHs c) ~ GetOpVal (ToT c)
       ) => GetOpHs c where
-  type GetOpKeyHs c :: Kind.Type
-  type GetOpValHs c :: Kind.Type
+  type GetOpKeyHs c :: Type
+  type GetOpValHs c :: Type
 
 instance NiceComparable k => GetOpHs (Map k v) where
   type GetOpKeyHs (Map k v) = k
@@ -148,8 +146,8 @@
       , ToT (EDivOpResHs n m) ~ EDivOpRes (ToT n) (ToT m)
       , ToT (EModOpResHs n m) ~ EModOpRes (ToT n) (ToT m)
       ) => EDivOpHs n m where
-  type EDivOpResHs n m :: Kind.Type
-  type EModOpResHs n m :: Kind.Type
+  type EDivOpResHs n m :: Type
+  type EModOpResHs n m :: Type
 
 instance EDivOpHs Integer Integer where
   type EDivOpResHs Integer Integer = Integer
diff --git a/src/Lorentz/Referenced.hs b/src/Lorentz/Referenced.hs
--- a/src/Lorentz/Referenced.hs
+++ b/src/Lorentz/Referenced.hs
@@ -25,7 +25,6 @@
 
 import Prelude hiding (drop, swap)
 
-import qualified Data.Kind as Kind
 import GHC.TypeLits (ErrorMessage(..), TypeError)
 
 import Lorentz.Base
@@ -49,7 +48,7 @@
 ----------------------------------------------------------------------------
 
 -- | Allows duplicating stack elements referring them by type.
-class DupT (origSt :: [Kind.Type]) (a :: Kind.Type) (st :: [Kind.Type]) where
+class DupT (origSt :: [Type]) (a :: Type) (st :: [Type]) where
   dupTImpl :: st :-> a : st
 
 instance TypeError (StackElemNotFound origSt a) =>
@@ -84,9 +83,9 @@
 --
 -- Implemented with fun deps for conciseness; we can replace them
 -- with a type family anytime, but that would probably require more declarations.
-class DipT (origInp :: [Kind.Type]) (a :: Kind.Type)
-           (inp :: [Kind.Type]) (dipInp :: [Kind.Type])
-           (dipOut :: [Kind.Type]) (out :: [Kind.Type])
+class DipT (origInp :: [Type]) (a :: Type)
+           (inp :: [Type]) (dipInp :: [Type])
+           (dipOut :: [Type]) (out :: [Type])
            | inp a -> dipInp, dipOut inp a -> out where
   dipTImpl :: (dipInp :-> dipOut) -> (inp :-> out)
 
diff --git a/src/Lorentz/ReferencedByName.hs b/src/Lorentz/ReferencedByName.hs
--- a/src/Lorentz/ReferencedByName.hs
+++ b/src/Lorentz/ReferencedByName.hs
@@ -23,7 +23,6 @@
   ) where
 
 import Data.Constraint ((\\))
-import qualified Data.Kind as Kind
 import Data.Singletons (Sing)
 import Named (NamedF(..))
 
@@ -55,7 +54,7 @@
 data VarNamed = VarNamed Symbol | VarUnnamed | VarNameDummy
 
 -- | Get variable name.
-type family VarName (a :: Kind.Type) :: VarNamed where
+type family VarName (a :: Type) :: VarNamed where
   VarName (NamedF _ _ name) = 'VarNamed name
   VarName _ = 'VarUnnamed
 
@@ -68,7 +67,7 @@
   Assert 'VarNameDummy _ = AnyVN
   Assert vn _ = vn
 
-type family VarNamePretty' (x :: Kind.Type) (vn :: VarNamed) :: VarNamed where
+type family VarNamePretty' (x :: Type) (vn :: VarNamed) :: VarNamed where
   VarNamePretty' x vn = Assert vn
     (TypeError
       ('Text "Not clear which name `" ':<>: 'ShowType x ':<>: 'Text "` variable has" ':$$:
@@ -105,7 +104,7 @@
 and can easily add this constraint to his methods.
 
 -}
-class HasNamedVar (s :: [Kind.Type]) (name :: Symbol) (var :: Kind.Type)
+class HasNamedVar (s :: [Type]) (name :: Symbol) (var :: Type)
     | s name -> var where
 
   -- | 1-based position of the variable on stack.
@@ -116,7 +115,7 @@
   , RequireLongerOrSameLength s n, RequireLongerOrSameLength (ToTs s) n
   )
 
-data VarPosition (s :: [Kind.Type]) (name :: Symbol) (var :: Kind.Type) where
+data VarPosition (s :: [Type]) (name :: Symbol) (var :: Type) where
   VarPosition
     :: (ConstraintVarPosition s n)
     => (Sing (n :: Nat))
@@ -151,7 +150,7 @@
 -- | Version of 'HasNamedVar' for multiple variables.
 --
 -- >>> type HasContext = HasNamedVars s ["x" := Integer, "f" := Lambda MText MText]
-type family HasNamedVars (s :: [Kind.Type]) (vs :: [NamedField]) :: Constraint where
+type family HasNamedVars (s :: [Type]) (vs :: [NamedField]) :: Constraint where
   HasNamedVars _ '[] = ()
   HasNamedVars s ((n := ty) ': vs) = (HasNamedVar s n ty, HasNamedVars s vs)
 
diff --git a/src/Lorentz/StoreClass.hs b/src/Lorentz/StoreClass.hs
--- a/src/Lorentz/StoreClass.hs
+++ b/src/Lorentz/StoreClass.hs
@@ -3,6 +3,8 @@
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
 {-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
 
 {- | This module provides storage interfaces.
 
@@ -18,8 +20,19 @@
 
 -}
 module Lorentz.StoreClass
-  ( -- * Class
-    StoreHasField (..)
+  ( -- * Preliminary
+    FieldRefKind
+  , FieldRefTag
+  , KnownFieldRef (..)
+  , FieldName
+  , FieldRef
+  , FieldSymRef
+  , fieldNameToLabel
+  , fieldNameFromLabel
+  , FieldRefHasFinalName (..)
+
+    -- * Class
+  , StoreHasField (..)
   , StoreFieldOps (..)
   , StoreHasSubmap (..)
   , StoreSubmapOps (..)
@@ -38,6 +51,8 @@
     -- * Methods to work with storage
   , stToField
   , stGetField
+  , stToFieldNamed
+  , stGetFieldNamed
   , stSetField
   , stMem
   , stGet
@@ -75,20 +90,111 @@
 
     -- * Storage generation
   , mkStoreEp
+
+    -- * Complex field references
+  , (:-|)(..)
+
+  , SelfRef (..)
+  , this
+
+  , stNested
+
+  , FieldAlias
+  , stAlias
+  , FieldNickname
+  , stNickname
   ) where
 
+
+import qualified Data.Kind as Kind
 import Data.Map (singleton)
+import GHC.TypeLits (KnownSymbol, Symbol)
 
 import Lorentz.ADT
 import Lorentz.Base
-import Lorentz.Iso
+import Lorentz.Coercions
 import Lorentz.Constraints
 import Lorentz.Errors (failUnexpected)
 import qualified Lorentz.Instr as L
+import Lorentz.Iso
 import qualified Lorentz.Macro as L
 import Lorentz.Value
 import Michelson.Text (labelToMText)
 
+{- $doctest-setup
+
+>>> import Lorentz.Instr
+>>> import Lorentz.Value
+>>> import Lorentz.Run.Simple
+
+-}
+
+-- | Open kind for various field references.
+--
+-- The simplest field reference could be 'Label', pointing to a field
+-- by its name, but we also support more complex scenarios like deep
+-- fields identifiers.
+type FieldRefKind = FieldRefTag -> Kind.Type
+data FieldRefTag = FieldRefTag
+
+-- | For a type-level field reference - an associated term-level representation.
+--
+-- This is similar to 'Sing' + 'SingI' pair but has small differences:
+--
+-- * Dedicated to field references, thus term-level thing has 'FieldRefKind' kind.
+-- * The type of term-level value (@FieldRefObject ty@) determines the kind of
+--   the reference type.
+class KnownFieldRef (ty :: k) where
+  type FieldRefObject ty = (fr :: FieldRefKind) | fr -> ty
+  mkFieldRef :: FieldRefObject ty p
+
+-- | Some kind of reference to a field.
+--
+-- The idea behind this type is that in trivial case (@name :: Symbol@) it can
+-- be instantiated with a mere label, but it is generic enough to allow complex
+-- field references as well.
+type FieldRef name = FieldRefObject name 'FieldRefTag
+
+-- | The simplest field reference - just a name. Behaves similarly to 'Label'.
+data FieldName (n :: Symbol) (p :: FieldRefTag) =
+  KnownSymbol n => FieldName
+
+-- Thanks to @p@ type variable being of unique 'FieldRefKind' kind,
+-- this instance won't overlap with 'IsLabel' instances from other modules.
+instance (x ~ FieldName name, KnownSymbol name) =>
+         IsLabel name (x p) where
+  fromLabel = FieldName
+
+instance KnownSymbol name => KnownFieldRef (name :: Symbol) where
+  type FieldRefObject name = FieldName name
+  mkFieldRef = FieldName
+
+-- | Version of 'FieldRef' restricted to symbolic labels.
+--
+-- @FieldSymRef name ≡ FieldName name 'FieldRefTag@
+type FieldSymRef name = FieldRef (name :: Symbol)
+
+-- | Convert a symbolic 'FieldRef' to a label, useful for compatibility with
+-- other interfaces.
+fieldNameToLabel :: FieldSymRef n -> Label n
+fieldNameToLabel FieldName = Label
+
+-- | Convert a label to 'FieldRef', useful for compatibility with
+-- other interfaces.
+fieldNameFromLabel :: Label n -> FieldSymRef n
+fieldNameFromLabel Label = FieldName
+
+-- | Provides access to the direct name of the referred field.
+--
+-- This is used in 'stToFieldNamed'.
+class FieldRefHasFinalName fr where
+  type FieldRefFinalName fr :: Symbol
+  fieldRefFinalName :: FieldRef fr -> Label (FieldRefFinalName fr)
+
+instance FieldRefHasFinalName (name :: Symbol) where
+  type FieldRefFinalName name = name
+  fieldRefFinalName = fieldNameToLabel
+
 ----------------------------------------------------------------------------
 -- Fields
 ----------------------------------------------------------------------------
@@ -102,10 +208,10 @@
 data StoreFieldOps store fname ftype = StoreFieldOps
   { sopToField
       :: forall s.
-         Label fname -> store : s :-> ftype : s
+         FieldRef fname -> store : s :-> ftype : s
   , sopSetField
       :: forall s.
-         Label fname -> ftype : store : s :-> store : s
+         FieldRef fname -> ftype : store : s :-> store : s
   }
 
 -- Using fundeps here for the sake of less amount of boilerplate on user side,
@@ -114,22 +220,44 @@
 class StoreHasField store fname ftype | store fname -> ftype where
   storeFieldOps :: StoreFieldOps store fname ftype
 
+instance HasFieldOfType (a, b) fname ftype =>
+         StoreHasField (a, b) fname ftype where
+  storeFieldOps = storeFieldOpsADT
+
+instance HasFieldOfType (a, b, c) fname ftype =>
+         StoreHasField (a, b, c) fname ftype where
+  storeFieldOps = storeFieldOpsADT
+
 -- | Pick storage field.
 stToField
   :: StoreHasField store fname ftype
-  => Label fname -> store : s :-> ftype : s
+  => FieldRef fname -> store : s :-> ftype : s
 stToField = sopToField storeFieldOps
 
 -- | Get storage field, preserving the storage itself on stack.
 stGetField
   :: StoreHasField store fname ftype
-  => Label fname -> store : s :-> ftype : store : s
+  => FieldRef fname -> store : s :-> ftype : store : s
 stGetField l = L.dup # sopToField storeFieldOps l
 
+-- | Pick storage field retaining a name label attached.
+--
+-- For complex refs this tries to attach the immediate name of the referred field.
+stToFieldNamed
+  :: (StoreHasField store fname ftype, FieldRefHasFinalName fname)
+  => FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : s
+stToFieldNamed fr = stToField fr # toNamed (fieldRefFinalName fr)
+
+-- | Version of 'stToFieldNamed' that preserves the storage on stack.
+stGetFieldNamed
+  :: (StoreHasField store fname ftype, FieldRefHasFinalName fname)
+  => FieldRef fname -> store : s :-> (FieldRefFinalName fname :! ftype) : store : s
+stGetFieldNamed fr = L.dup # stToFieldNamed fr
+
 -- | Update storage field.
 stSetField
   :: StoreHasField store fname ftype
-  => Label fname -> ftype : store : s :-> store : s
+  => FieldRef fname -> ftype : store : s :-> store : s
 stSetField = sopSetField storeFieldOps
 
 ----------------------------------------------------------------------------
@@ -145,65 +273,75 @@
 data StoreSubmapOps store mname key value = StoreSubmapOps
   { sopMem
       :: forall s.
-         Label mname -> key : store : s :-> Bool : s
+         FieldRef mname -> key : store : s :-> Bool : s
   , sopGet
       :: forall s.
          (KnownValue value)
-      => Label mname -> key : store : s :-> Maybe value : s
+      => FieldRef mname -> key : store : s :-> Maybe value : s
   , sopUpdate
       :: forall s.
-         Label mname -> key : Maybe value : store : s :-> store : s
+         FieldRef mname -> key : Maybe value : store : s :-> store : s
 
     -- Methods below are derivatives of methods above, they can be provided
     -- if for given specific storage type more efficient implementation is
     -- available.
   , sopDelete
       :: forall s.
-         Label mname -> key : store : s :-> store : s
+         FieldRef mname -> key : store : s :-> store : s
   , sopInsert
       :: forall s.
-         Label mname -> key : value : store : s :-> store : s
+         FieldRef mname -> key : value : store : s :-> store : s
   }
 
 -- | Provides operations on submaps of storage.
 class StoreHasSubmap store mname key value | store mname -> key value where
   storeSubmapOps :: StoreSubmapOps store mname key value
 
+-- | Provides access to the submap via the respective field.
+--
+-- Tricky storages that consolidate submaps in a non-trivial way
+-- can define instances overlapping this one.
+instance ( StoreHasField store name submap
+         , StoreHasSubmap submap SelfRef key value
+         , KnownSymbol name
+         ) => StoreHasSubmap store (name :: Symbol) key value where
+  storeSubmapOps = storeSubmapOpsReferTo (fromLabel @name :-| this) storeSubmapOps
+
 -- | Check value presence in storage.
 stMem
   :: StoreHasSubmap store mname key value
-  => Label mname -> key : store : s :-> Bool : s
+  => FieldRef mname -> key : store : s :-> Bool : s
 stMem = sopMem storeSubmapOps
 
 -- | Get value in storage.
 stGet
   :: (StoreHasSubmap store mname key value, KnownValue value)
-  => Label mname -> key : store : s :-> Maybe value : s
+  => FieldRef mname -> key : store : s :-> Maybe value : s
 stGet = sopGet storeSubmapOps
 
 -- | Update a value in storage.
 stUpdate
   :: StoreHasSubmap store mname key value
-  => Label mname -> key : Maybe value : store : s :-> store : s
+  => FieldRef mname -> key : Maybe value : store : s :-> store : s
 stUpdate = sopUpdate storeSubmapOps
 
 -- | Delete a value in storage.
 stDelete
   :: forall store mname key value s.
      (StoreHasSubmap store mname key value)
-  => Label mname -> key : store : s :-> store : s
+  => FieldRef mname -> key : store : s :-> store : s
 stDelete = sopDelete storeSubmapOps
 
 -- | Add a value in storage.
 stInsert
   :: StoreHasSubmap store mname key value
-  => Label mname -> key : value : store : s :-> store : s
+  => FieldRef mname -> key : value : store : s :-> store : s
 stInsert = sopInsert storeSubmapOps
 
 -- | Add a value in storage, but fail if it will overwrite some existing entry.
 stInsertNew
   :: StoreHasSubmap store mname key value
-  => Label mname
+  => FieldRef mname
   -> (forall s0 any. key : s0 :-> any)
   -> key : value : store : s
   :-> store : s
@@ -211,42 +349,7 @@
   L.duupX @3 # L.duupX @2 # stMem l #
   L.if_ doFail (stInsert l)
 
--- Instances
 ----------------------------------------------------------------------------
-
--- | 'BigMap' can be used as standalone key-value storage,
--- name of submap is not accounted in this case.
-instance (key ~ key', value ~ value', NiceComparable key, KnownValue value) =>
-         StoreHasSubmap (BigMap key' value') name key value where
-  storeSubmapOps = StoreSubmapOps
-    { sopMem = \_label -> L.mem
-    , sopGet = \_label -> L.get
-    , sopUpdate = \_label -> L.update
-    , sopDelete = \_label -> L.deleteMap
-    , sopInsert = \_label -> L.mapInsert
-    }
-
--- | 'Map' can be used as standalone key-value storage if very needed.
-instance (key ~ key', value ~ value', NiceComparable key, KnownValue value) =>
-         StoreHasSubmap (Map key' value') name key value where
-  storeSubmapOps = StoreSubmapOps
-    { sopMem = \_label -> L.mem
-    , sopGet = \_label -> L.get
-    , sopUpdate = \_label -> L.update
-    , sopDelete = \_label -> L.deleteMap
-    , sopInsert = \_label -> L.mapInsert
-    }
-
-instance NiceComparable key => StoreHasSubmap (Set key) name key () where
-  storeSubmapOps = StoreSubmapOps
-    { sopMem = \_label -> L.mem
-    , sopGet = \_label -> L.mem # L.if_ (L.push $ Just ()) (L.push Nothing)
-    , sopUpdate = \_label -> L.dip L.isSome # L.update
-    , sopDelete = \_label -> L.setDelete
-    , sopInsert = \_label -> L.dip L.drop # L.setInsert
-    }
-
-----------------------------------------------------------------------------
 -- Stored Entrypoints
 ----------------------------------------------------------------------------
 
@@ -348,14 +451,14 @@
 -- keeping a pack of fields.
 storeFieldOpsADT
   :: HasFieldOfType dt fname ftype
-  => StoreFieldOps dt fname ftype
+  => StoreFieldOps dt (fname :: Symbol) ftype
 storeFieldOpsADT = StoreFieldOps
-  { sopToField = toField
-  , sopSetField = setField
+  { sopToField = toField . fieldNameToLabel
+  , sopSetField = setField . fieldNameToLabel
   }
 
 -- | Implementation of 'StoreHasEntrypoint' for a datatype keeping a pack of
--- fields, among which one has contains the entrypoint and another is what such
+-- fields, among which one contains the entrypoint and another is what such
 -- entrypoint operates on.
 storeEntrypointOpsADT
   :: ( HasFieldOfType store epmName (EntrypointsField epParam epStore)
@@ -366,7 +469,7 @@
   -> StoreEntrypointOps store epName epParam epStore
 storeEntrypointOpsADT mapLabel fieldLabel = StoreEntrypointOps
   { sopToEpLambda = \l -> toField mapLabel # pushStEp l # L.get # someStEp l
-  , sopSetEpLambda = \l -> L.dip (getField mapLabel) # setStEp mapLabel l # setField mapLabel
+  , sopSetEpLambda = \l -> L.dip (getField mapLabel) # setStEp this l # setField mapLabel
   , sopToEpStore = \_l -> toField fieldLabel
   , sopSetEpStore = \_l -> setField fieldLabel
   }
@@ -382,10 +485,15 @@
   => Label epmName -> Label epsName
   -> StoreEntrypointOps store epName epParam epStore
 storeEntrypointOpsFields mapLabel fieldLabel = StoreEntrypointOps
-  { sopToEpLambda = \l -> stToField mapLabel # pushStEp l # L.get # someStEp l
-  , sopSetEpLambda = \l -> L.dip (stGetField mapLabel) # setStEp mapLabel l # stSetField mapLabel
-  , sopToEpStore = \_l -> stToField fieldLabel
-  , sopSetEpStore = \_l -> stSetField fieldLabel
+  { sopToEpLambda = \l ->
+      stToField (fieldNameFromLabel mapLabel) # pushStEp l # L.get # someStEp l
+  , sopSetEpLambda = \l ->
+      L.dip (stGetField $ fieldNameFromLabel mapLabel) # setStEp this l #
+      stSetField (fieldNameFromLabel mapLabel)
+  , sopToEpStore = \_l ->
+      stToField $ fieldNameFromLabel fieldLabel
+  , sopSetEpStore = \_l ->
+      stSetField $ fieldNameFromLabel fieldLabel
   }
 
 -- | Implementation of 'StoreHasEntrypoint' for a datatype that has a 'StoreHasSubmap'
@@ -399,10 +507,10 @@
   => Label epmName -> Label epsName
   -> StoreEntrypointOps store epName epParam epStore
 storeEntrypointOpsSubmapField mapLabel fieldLabel = StoreEntrypointOps
-  { sopToEpLambda = \l -> pushStEp l # stGet mapLabel # someStEp l
-  , sopSetEpLambda = \l -> setStEp mapLabel l
-  , sopToEpStore = \_l -> stToField fieldLabel
-  , sopSetEpStore = \_l -> stSetField fieldLabel
+  { sopToEpLambda = \l -> pushStEp l # stGet (fieldNameFromLabel mapLabel) # someStEp l
+  , sopSetEpLambda = \l -> setStEp (fieldNameFromLabel mapLabel) l
+  , sopToEpStore = \_l -> stToField (fieldNameFromLabel fieldLabel)
+  , sopSetEpStore = \_l -> stSetField (fieldNameFromLabel fieldLabel)
   }
 
 -- | Implementation of 'StoreHasField' for a data type which has an
@@ -412,7 +520,7 @@
   :: ( HasFieldOfType storage fieldsPartName fields
      , StoreHasField fields fname ftype
      )
-  => Label fieldsPartName
+  => FieldRef fieldsPartName
   -> StoreFieldOps storage fname ftype
 storeFieldOpsDeeper fieldsLabel =
   composeStoreFieldOps fieldsLabel storeFieldOpsADT storeFieldOps
@@ -422,12 +530,13 @@
 -- For instance, it can be used for top-level storage.
 storeSubmapOpsDeeper
   :: ( HasFieldOfType storage bigMapPartName fields
-     , StoreHasSubmap fields mname key value
+     , StoreHasSubmap fields SelfRef key value
      )
-  => Label bigMapPartName
+  => FieldRef bigMapPartName
   -> StoreSubmapOps storage mname key value
 storeSubmapOpsDeeper submapLabel =
-  composeStoreSubmapOps submapLabel storeFieldOpsADT storeSubmapOps
+  storeSubmapOpsReferTo this $
+    composeStoreSubmapOps submapLabel storeFieldOpsADT storeSubmapOps
 
 -- | Implementation of 'StoreHasEntrypoint' for a data type which has an
 -- instance of 'StoreHasEntrypoint' inside.
@@ -436,7 +545,7 @@
   :: ( HasFieldOfType store nameInStore substore
      , StoreHasEntrypoint substore epName epParam epStore
      )
-  => Label nameInStore
+  => FieldRef nameInStore
   -> StoreEntrypointOps store epName epParam epStore
 storeEntrypointOpsDeeper fieldsLabel =
   composeStoreEntrypointOps fieldsLabel storeFieldOpsADT storeEpOps
@@ -455,7 +564,7 @@
 @
 -}
 storeSubmapOpsReferTo
-  :: Label name
+  :: FieldRef name
   -> StoreSubmapOps storage name key value
   -> StoreSubmapOps storage desiredName key value
 storeSubmapOpsReferTo l StoreSubmapOps{..} =
@@ -473,7 +582,7 @@
 --
 -- See also 'storeSubmapOpsReferTo'.
 storeFieldOpsReferTo
-  :: Label name
+  :: FieldRef name
   -> StoreFieldOps storage name field
   -> StoreFieldOps storage desiredName field
 storeFieldOpsReferTo l StoreFieldOps{..} =
@@ -557,7 +666,7 @@
 -- Suits for a case when your store does not contain its fields directly
 -- rather has a nested structure.
 composeStoreFieldOps
-  :: Label nameInStore
+  :: FieldRef nameInStore
   -> StoreFieldOps store nameInStore substore
   -> StoreFieldOps substore nameInSubstore field
   -> StoreFieldOps store nameInSubstore field
@@ -573,7 +682,7 @@
 
 -- | Chain implementations of field and submap operations.
 composeStoreSubmapOps
-  :: Label nameInStore
+  :: FieldRef nameInStore
   -> StoreFieldOps store nameInStore substore
   -> StoreSubmapOps substore mname key value
   -> StoreSubmapOps store mname key value
@@ -613,7 +722,7 @@
 sequenceStoreSubmapOps
   :: forall store substore value name subName key1 key2.
      (NiceConstant substore, KnownValue value)
-  => Label name
+  => FieldRef name
   -> LIso (Maybe substore) substore
   -> StoreSubmapOps store name key1 substore
   -> StoreSubmapOps substore subName key2 value
@@ -664,7 +773,7 @@
         )
 
 composeStoreEntrypointOps
-  :: Label nameInStore
+  :: FieldRef nameInStore
   -> StoreFieldOps store nameInStore substore
   -> StoreEntrypointOps substore epName epParam epStore
   -> StoreEntrypointOps store epName epParam epStore
@@ -706,7 +815,7 @@
 zoomStoreSubmapOps
   :: forall store submapName nameInSubmap key value subvalue.
      (NiceConstant value, NiceConstant subvalue)
-  => Label submapName
+  => FieldRef submapName
   -> LIso (Maybe value) value
   -> LIso (Maybe subvalue) subvalue
   -> StoreSubmapOps store submapName key value
@@ -738,7 +847,7 @@
   }
   where
     updateSubmapValue
-      :: Label nameInSubmap
+      :: FieldRef nameInSubmap
       -> key : subvalue : store : s
          :-> key : value : store : s
     updateSubmapValue l2 =
@@ -767,7 +876,7 @@
 -- Fails in case the entrypoint is already set.
 setStEp
   :: StoreHasSubmap store epmName MText (EntrypointLambda epParam epStore)
-  => Label epmName -> Label epsName
+  => FieldRef epmName -> Label epsName
   -> (EntrypointLambda epParam epStore) : store : s :-> store : s
 setStEp ml l = pushStEp l # stInsertNew ml failAlreadySetEp
   where
@@ -791,7 +900,166 @@
   -> EntrypointsField epParam epStore
 mkStoreEp l = BigMap . singleton (labelToMText l)
 
+----------------------------------------------------------------------------
+-- Complex field references
+----------------------------------------------------------------------------
 
+-- | Refer to a nested entry in storage.
+--
+-- Example: @stToField (#a :-| #b)@ fetches field @b@ in the type under field @a@.
+--
+-- If not favouring this name much, you can try an alias from
+-- "Lorentz.StoreClass.Extra".
+infixr 8 :-|
+data (:-|) (l :: k1) (r :: k2) (p :: FieldRefTag) =
+  FieldRef l :-| FieldRef r
+
+instance (KnownFieldRef l, KnownFieldRef r) => KnownFieldRef (l :-| r) where
+  type FieldRefObject (l :-| r) = l :-| r
+  mkFieldRef = mkFieldRef :-| mkFieldRef
+
+instance FieldRefHasFinalName r => FieldRefHasFinalName (l :-| r) where
+  type FieldRefFinalName (l :-| r) = FieldRefFinalName r
+  fieldRefFinalName (_ :-| r) = fieldRefFinalName r
+
+instance ( StoreHasField store field substore
+         , StoreHasField substore subfield ty
+         , KnownFieldRef field, KnownFieldRef subfield
+         ) =>
+         StoreHasField store (field :-| subfield) ty where
+  storeFieldOps =
+    storeFieldOpsReferTo (mkFieldRef @_ @subfield) $
+      composeStoreFieldOps (mkFieldRef @_ @field) storeFieldOps storeFieldOps
+
+instance ( StoreHasField store field substore
+         , StoreHasSubmap substore subfield key value
+         , KnownFieldRef field, KnownFieldRef subfield
+         ) =>
+         StoreHasSubmap store (field :-| subfield) key value where
+  storeSubmapOps =
+    storeSubmapOpsReferTo (mkFieldRef @_ @subfield) $
+      composeStoreSubmapOps (mkFieldRef @_ @field) storeFieldOps storeSubmapOps
+
+-- | Refer to no particular field, access itself.
+data SelfRef (p :: FieldRefTag) = SelfRef
+
+{- | An alias for 'SelfRef'.
+
+Examples:
+
+>>> push 5 # stMem this -$ (mempty :: Map Integer MText)
+...
+... Nothing
+...
+
+>>> stGetField this # pair -$ (5 :: Integer)
+...
+... (5, 5)
+...
+
+-}
+this :: SelfRef p
+this = SelfRef
+
+instance KnownFieldRef SelfRef where
+  type FieldRefObject SelfRef = SelfRef
+  mkFieldRef = SelfRef
+
+instance StoreHasField store SelfRef store where
+  storeFieldOps = StoreFieldOps
+    { sopToField = \SelfRef -> L.nop
+    , sopSetField = \SelfRef -> L.dip L.drop
+    }
+
+instance (NiceComparable key, KnownValue value) =>
+         StoreHasSubmap (BigMap key value) SelfRef key value where
+  storeSubmapOps = StoreSubmapOps
+    { sopMem = \SelfRef -> L.mem
+    , sopGet = \SelfRef -> L.get
+    , sopUpdate = \SelfRef -> L.update
+    , sopDelete = \SelfRef -> L.deleteMap
+    , sopInsert = \SelfRef -> L.mapInsert
+    }
+
+instance (NiceComparable key, KnownValue value) =>
+         StoreHasSubmap (Map key value) SelfRef key value where
+  storeSubmapOps = StoreSubmapOps
+    { sopMem = \SelfRef -> L.mem
+    , sopGet = \SelfRef -> L.get
+    , sopUpdate = \SelfRef -> L.update
+    , sopDelete = \SelfRef -> L.deleteMap
+    , sopInsert = \SelfRef -> L.mapInsert
+    }
+
+instance NiceComparable key => StoreHasSubmap (Set key) SelfRef key () where
+  storeSubmapOps = StoreSubmapOps
+    { sopMem = \SelfRef -> L.mem
+    , sopGet = \SelfRef -> L.mem # L.if_ (L.push $ Just ()) (L.push Nothing)
+    , sopUpdate = \SelfRef -> L.dip L.isSome # L.update
+    , sopDelete = \SelfRef -> L.setDelete
+    , sopInsert = \SelfRef -> L.dip L.drop # L.setInsert
+    }
+
+-- | Provides alternative variadic interface for deep entries access.
+--
+-- Example: @stToField (stNested #a #b #c)@
+stNested :: StNestedImpl f SelfRef => f
+stNested = stNestedImpl this
+
+class StNestedImpl f acc | f -> acc where
+  stNestedImpl :: FieldRef acc -> f
+
+instance (p ~ 'FieldRefTag, res p ~ FieldRef acc) =>
+         StNestedImpl (res p) acc where
+  stNestedImpl acc = acc
+
+instance ( label ~ FieldRef name
+         , StNestedImpl f (acc :-| name)
+         ) =>
+         StNestedImpl (label -> f) acc where
+  stNestedImpl acc l = stNestedImpl (acc :-| l)
+
+{- | Alias for a field reference.
+
+This allows creating _custom_ field references; you will have to define
+the respective 'StoreHasField' and 'StoreHasSubmap' instances manually.
+Since this type occupies a different "namespace" than string labels
+and ':-|', no overlappable instances will be necessary.
+
+Example:
+
+@
+-- Shortcut for a deeply nested field X
+data FieldX
+
+instance StoreHasField Storage (FieldAlias FieldX) Integer where
+  ...
+
+accessX = stToField (stAlias @FieldX)
+@
+
+Note that @alias@ type argument allows instantiations of any kind.
+-}
+data FieldAlias (alias :: k) (p :: FieldRefTag)
+  = FieldAlias (Proxy alias)
+
+-- | Construct an alias at term level.
+--
+-- This requires passing the alias via type annotation.
+stAlias :: forall alias. FieldRef (FieldAlias alias)
+stAlias = mkFieldRef
+
+-- | Kind-restricted version of 'FieldAlias' to work solely with string labels.
+type FieldNickname alias = FieldAlias (alias :: Symbol)
+
+-- | Version of 'stAlias' adopted to labels.
+stNickname :: Label name -> FieldRef (FieldAlias name)
+stNickname _ = mkFieldRef
+
+instance KnownFieldRef (FieldAlias alias) where
+  type FieldRefObject (FieldAlias alias) = FieldAlias alias
+  mkFieldRef = FieldAlias Proxy
+
 ----------------------------------------------------------------------------
 -- Utilities
 ----------------------------------------------------------------------------
@@ -816,6 +1084,9 @@
   , "balances" := Address ~> Int
   ]
 @
+
+Note that this won't work with complex field references, they have to be
+included using e.g. 'StoreHasField' manually.
 
 -}
 type family StorageContains store (content :: [NamedField]) :: Constraint where
diff --git a/src/Lorentz/StoreClass/Extra.hs b/src/Lorentz/StoreClass/Extra.hs
new file mode 100644
--- /dev/null
+++ b/src/Lorentz/StoreClass/Extra.hs
@@ -0,0 +1,26 @@
+-- SPDX-FileCopyrightText: 2021 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | Some conveniences for "Lorentz.StoreClass" module.
+--
+-- This is not part of the umbrella 'Lorentz' module, you have to import
+-- this specially.
+module Lorentz.StoreClass.Extra
+  ( (.)
+  ) where
+
+import Prelude ()
+
+import Lorentz.StoreClass
+
+-- | Alias for ':-|'.
+--
+-- This makes nested field access look just like in other languages.
+--
+-- Though it may collide with the dot operator from Haskell world,
+-- for instance, in tests, so we do not yet provide it directly in
+-- "Lorentz.StoreClass".
+infixr 8 .
+(.) :: FieldRef l -> FieldRef r -> FieldRef (l :-| r)
+(.) = (:-|)
diff --git a/src/Lorentz/UParam.hs b/src/Lorentz/UParam.hs
--- a/src/Lorentz/UParam.hs
+++ b/src/Lorentz/UParam.hs
@@ -48,7 +48,6 @@
   ) where
 
 import Data.Constraint ((\\))
-import qualified Data.Kind as Kind
 import qualified Fcf
 import Fmt (Buildable(..))
 import GHC.Generics ((:*:)(..), (:+:)(..))
@@ -74,7 +73,7 @@
 import Util.TypeTuple
 
 -- | An entrypoint is described by two types: its name and type of argument.
-type EntrypointKind = (Symbol, Kind.Type)
+type EntrypointKind = (Symbol, Type)
 
 -- | A convenient alias for type-level name-something pair.
 type (n :: Symbol) ?: (a :: k) = '(n, a)
@@ -114,7 +113,7 @@
 
 -- | Get type of entrypoint argument by its name.
 type family LookupEntrypoint (name :: Symbol) (entries :: [EntrypointKind])
-             :: Kind.Type where
+             :: Type where
   LookupEntrypoint name ('(name, a) ': _) = a
   LookupEntrypoint name (_ ': entries) = LookupEntrypoint name entries
   LookupEntrypoint name '[] =
@@ -158,7 +157,7 @@
 ----------------------------------------------------------------------------
 
 -- | This type can store any value that satisfies a certain constraint.
-data ConstrainedSome (c :: Kind.Type -> Constraint) where
+data ConstrainedSome (c :: Type -> Constraint) where
   ConstrainedSome :: c a => a -> ConstrainedSome c
 
 instance Show (ConstrainedSome Show) where
@@ -168,7 +167,7 @@
   build (ConstrainedSome a) = build a
 
 -- | This class is needed to implement `unpackUParam`.
-class UnpackUParam (c :: Kind.Type -> Constraint) entries where
+class UnpackUParam (c :: Type -> Constraint) entries where
   -- | Turn 'UParam' into a Haskell value.
   -- Since we don't know its type in compile time, we have to erase it using
   -- 'ConstrainedSome'. The user of this function can require arbitrary
@@ -350,8 +349,8 @@
 type UParamLinearized p = GUParamLinearized (G.Rep p)
 
 -- | Generic traversal for conversion between ADT sum and 'UParam'.
-class GUParamLinearize (x :: Kind.Type -> Kind.Type) where
-  type GUParamLinearized x :: [(Symbol, Kind.Type)]
+class GUParamLinearize (x :: Type -> Type) where
+  type GUParamLinearized x :: [(Symbol, Type)]
   adtToRec :: x p -> UParam (GUParamLinearized x)
 
 instance GUParamLinearize x => GUParamLinearize (G.D1 i x) where
diff --git a/src/Lorentz/Wrappable.hs b/src/Lorentz/Wrappable.hs
--- a/src/Lorentz/Wrappable.hs
+++ b/src/Lorentz/Wrappable.hs
@@ -7,7 +7,6 @@
   , Unwrappable
   ) where
 
-import Data.Kind (Type)
 import GHC.Generics
 import GHC.TypeLits
 import Named (NamedF(..))
diff --git a/src/Lorentz/Zip.hs b/src/Lorentz/Zip.hs
--- a/src/Lorentz/Zip.hs
+++ b/src/Lorentz/Zip.hs
@@ -21,8 +21,6 @@
 
 import Prelude hiding (drop)
 
-import qualified Data.Kind as Kind
-
 import Lorentz.Annotation
 import Lorentz.Base
 import Michelson.Typed
@@ -52,9 +50,9 @@
 -}
 
 -- | Zipping stack into tuple and back.
-class (KnownIsoT (ZippedStack s)) => ZipInstr (s :: [Kind.Type]) where
+class (KnownIsoT (ZippedStack s)) => ZipInstr (s :: [Type]) where
   -- | A type which contains the whole stack zipped.
-  type ZippedStack s :: Kind.Type
+  type ZippedStack s :: Type
 
   -- | Fold given stack into single value in typed Michelson.
   zipInstrTyped :: Instr (ToTs s) '[ToT (ZippedStack s)]