diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -2,9 +2,27 @@
 ==========
 <!-- Append new entries here -->
 
+0.10.0
+======
+* [!774](https://gitlab.com/morley-framework/morley/-/merge_requests/774)
+  + Added support for `BLS12-381` crypto primitives (types, instructions, arithmetics).
+  + Now it is possible to use `int` instruction for newtypes over `Natural`.
+* [!786](https://gitlab.com/morley-framework/morley/-/merge_requests/786)
+* [!791](https://gitlab.com/morley-framework/morley/-/merge_requests/791)
+  + Add new Edo instructions: `pairGet` and `pairUpdate`.
+* [!755](https://gitlab.com/morley-framework/morley/-/merge_requests/755)
+  Restricted `FAILWITH` only to packable values, except `CONTRACT`s
+* [!759](https://gitlab.com/morley-framework/morley/-/merge_requests/759)
+  + Add `UnitErrorArg` and `NoErrorArg` to be used with `ErrorArg` instance.
+    + `UnitErrorArg` is preferred to `()`
+    + `NoErrorArg` allows failing with just a string instead of a `pair string unit`.
+* [!764](https://gitlab.com/morley-framework/morley/-/merge_requests/764)
+  + Added `Never` type, deprecated `Empty` type.
 
 0.9.1
 =====
+* [!781](https://gitlab.com/morley-framework/morley/-/merge_requests/781)
+  + Replaced mixins and dependency on `base` with `base-noprelude`.
 * [!751](https://gitlab.com/morley-framework/morley/-/merge_requests/751)
   + Add new Edo instruction: `LEVEL`.
 * [!741](https://gitlab.com/morley-framework/morley/-/merge_requests/741)
diff --git a/lorentz.cabal b/lorentz.cabal
--- a/lorentz.cabal
+++ b/lorentz.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           lorentz
-version:        0.9.1
+version:        0.10.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
@@ -85,7 +85,7 @@
   ghc-options: -Weverything -Wno-missing-exported-signatures -Wno-missing-import-lists -Wno-missed-specialisations -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-implicit-prelude
   build-depends:
       aeson-pretty
-    , base >=4.7 && <5
+    , base-noprelude >=4.7 && <5
     , bimap
     , bytestring
     , constraints >=0.11
@@ -107,6 +107,4 @@
     , unordered-containers
     , vinyl
     , with-utf8
-  mixins:
-      base hiding (Prelude)
   default-language: Haskell2010
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, ann, noAnn)
+import Michelson.Untyped (FieldAnn, TypeAnn, VarAnn, ann, noAnn)
 import Tezos.Address
 import Tezos.Core
 import Tezos.Crypto
@@ -91,7 +91,7 @@
 gGetAnnotationNoField
     :: forall a. (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a)
     => FollowEntrypointFlag -> Notes (ToT a)
-gGetAnnotationNoField = \_ -> fst $ gGetAnnotation @(G.Rep a) defaultAnnOptions NotFollowEntrypoint NotGenerateFieldAnn
+gGetAnnotationNoField = \_ -> gGetAnnotation @(G.Rep a) defaultAnnOptions NotFollowEntrypoint NotGenerateFieldAnn ^. _1
 
 -- | This class defines the type and field annotations for a given type. Right now
 -- the type annotations come from names in a named field, and field annotations are
@@ -102,7 +102,7 @@
     :: (GHasAnnotation (G.Rep a), GValueType (G.Rep a) ~ ToT a)
     => FollowEntrypointFlag
     -> Notes (ToT a)
-  getAnnotation b = fst $ gGetAnnotation @(G.Rep a) (annOptions @a) b GenerateFieldAnn
+  getAnnotation b = gGetAnnotation @(G.Rep a) (annOptions @a) b GenerateFieldAnn ^. _1
 
   annOptions :: AnnOptions
   default annOptions :: AnnOptions
@@ -199,10 +199,10 @@
 
 -- | A Generic @HasAnnotation@ implementation
 class GHasAnnotation a where
-  gGetAnnotation :: AnnOptions -> FollowEntrypointFlag -> GenerateFieldAnnFlag -> (Notes (GValueType a), FieldAnn)
+  gGetAnnotation :: AnnOptions -> FollowEntrypointFlag -> GenerateFieldAnnFlag -> (Notes (GValueType a), FieldAnn, VarAnn)
 
 instance GHasAnnotation G.U1 where
-  gGetAnnotation _ _ _ = (starNotes, noAnn)
+  gGetAnnotation _ _ _ = (starNotes, noAnn, noAnn)
 
 instance (GHasAnnotation x)
   => GHasAnnotation (G.M1 G.S ('G.MetaSel 'Nothing b c d) x)
@@ -213,13 +213,14 @@
   => GHasAnnotation (G.M1 G.S ('G.MetaSel ('Just a) b c d) x)
   where
   gGetAnnotation o b b2 = case b2 of
-    GenerateFieldAnn -> (fst $ gGetAnnotation @x o b b2, ctorNameToAnnWithOptions @a o)
-    NotGenerateFieldAnn -> (fst $ gGetAnnotation @x o b b2, noAnn)
+    GenerateFieldAnn -> (gGetAnnotation @x o b b2 ^. _1, ctorNameToAnnWithOptions @a o, noAnn)
+    NotGenerateFieldAnn -> (gGetAnnotation @x o b b2 ^. _1, noAnn, noAnn)
 
 instance (GHasAnnotation x, KnownSymbol a) => GHasAnnotation (G.M1 G.C ('G.MetaCons a _p _f) x) where
   gGetAnnotation o b b2 =
-    ( fst $ gGetAnnotation @x o b b2
+    ( gGetAnnotation @x o b b2 ^. _1
     , ctorNameToAnnWithOptions @a o
+    , noAnn
     )
 
 instance (GHasAnnotation x) => GHasAnnotation (G.M1 G.D i1 x) where
@@ -234,20 +235,22 @@
   where
 
   gGetAnnotation o followEntrypointFlag generateAnnFlag =
-    let (xTypeAnn, xFieldAnn) = gGetAnnotation @x o followEntrypointFlag generateAnnFlag
-        (yTypeAnn, yFieldAnn) = gGetAnnotation @y o followEntrypointFlag generateAnnFlag
+    let (xTypeAnn, xFieldAnn, xVarAnn) = gGetAnnotation @x o followEntrypointFlag generateAnnFlag
+        (yTypeAnn, yFieldAnn, yVarAnn) = gGetAnnotation @y o followEntrypointFlag generateAnnFlag
     in case (followEntrypointFlag, generateAnnFlag) of
           (NotFollowEntrypoint, GenerateFieldAnn) ->
             ( NTOr noAnn
                 xFieldAnn yFieldAnn
                 xTypeAnn yTypeAnn
             , noAnn
+            , xVarAnn
             )
           _ ->
             ( NTOr noAnn
                 noAnn noAnn
                 xTypeAnn yTypeAnn
             , noAnn
+            , yVarAnn
             )
 
 instance
@@ -258,14 +261,16 @@
     GHasAnnotation (x G.:*: y)
   where
   gGetAnnotation o _ b2 =
-    let  (xTypeAnn, xFieldAnn) = gGetAnnotation @x o NotFollowEntrypoint b2
-         (yTypeAnn, yFieldAnn) = gGetAnnotation @y o NotFollowEntrypoint b2
+    let  (xTypeAnn, xFieldAnn, xVarAnn) = gGetAnnotation @x o NotFollowEntrypoint b2
+         (yTypeAnn, yFieldAnn, yVarAnn) = gGetAnnotation @y o NotFollowEntrypoint b2
     in
       ( NTPair noAnn
           xFieldAnn yFieldAnn
+          xVarAnn yVarAnn
           xTypeAnn yTypeAnn
       , noAnn
+      , noAnn
       )
 
 instance (HasAnnotation x) => GHasAnnotation (G.Rec0 x) where
-  gGetAnnotation _ b _ = (getAnnotation @x b, noAnn)
+  gGetAnnotation _ b _ = (getAnnotation @x b, noAnn, noAnn)
diff --git a/src/Lorentz/Arith.hs b/src/Lorentz/Arith.hs
--- a/src/Lorentz/Arith.hs
+++ b/src/Lorentz/Arith.hs
@@ -6,28 +6,30 @@
 module Lorentz.Arith
   ( ArithOpHs (..)
   , UnaryArithOpHs (..)
+  , ToIntegerArithOpHs
   ) where
 
 import qualified Data.Kind as Kind
 
 import Lorentz.Value
-import Lorentz.Constraints.Scopes (NiceComparable)
 import Michelson.Typed.Arith
 
 -- | Lifted 'ArithOp'.
 class ( ArithOp aop (ToT n) (ToT m)
-      , NiceComparable n, NiceComparable 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
 
 -- | Lifted 'UnaryArithOp'.
 class ( UnaryArithOp aop (ToT n)
-      , NiceComparable n
       , ToT (UnaryArithResHs aop n) ~ UnaryArithRes aop (ToT n)
       ) => UnaryArithOpHs (aop :: Kind.Type) (n :: Kind.Type) where
   type UnaryArithResHs aop n :: Kind.Type
 
+class ( ToIntArithOp (ToT n)
+      ) =>
+      ToIntegerArithOpHs (n :: Kind.Type)
+
 instance ArithOpHs Add Natural Integer where
   type ArithResHs Add Natural Integer = Integer
 instance ArithOpHs Add Integer Natural where
@@ -42,6 +44,12 @@
   type ArithResHs Add Integer Timestamp = Timestamp
 instance ArithOpHs Add Mutez Mutez where
   type ArithResHs Add Mutez Mutez = Mutez
+instance ArithOpHs Add Bls12381Fr Bls12381Fr where
+  type ArithResHs Add Bls12381Fr Bls12381Fr = Bls12381Fr
+instance ArithOpHs Add Bls12381G1 Bls12381G1 where
+  type ArithResHs Add Bls12381G1 Bls12381G1 = Bls12381G1
+instance ArithOpHs Add Bls12381G2 Bls12381G2 where
+  type ArithResHs Add Bls12381G2 Bls12381G2 = Bls12381G2
 
 instance ArithOpHs Sub Natural Integer where
   type ArithResHs Sub Natural Integer = Integer
@@ -70,14 +78,37 @@
   type ArithResHs Mul Natural Mutez = Mutez
 instance ArithOpHs Mul Mutez Natural where
   type ArithResHs Mul Mutez Natural = Mutez
-
-instance UnaryArithOpHs Abs Integer where
-  type UnaryArithResHs Abs Integer = Natural
+instance ArithOpHs Mul Integer Bls12381Fr where
+  type ArithResHs Mul Integer Bls12381Fr = Bls12381Fr
+instance ArithOpHs Mul Natural Bls12381Fr where
+  type ArithResHs Mul Natural Bls12381Fr = Bls12381Fr
+instance ArithOpHs Mul Bls12381Fr Integer where
+  type ArithResHs Mul Bls12381Fr Integer = Bls12381Fr
+instance ArithOpHs Mul Bls12381Fr Natural where
+  type ArithResHs Mul Bls12381Fr Natural = Bls12381Fr
+instance ArithOpHs Mul Bls12381Fr Bls12381Fr where
+  type ArithResHs Mul Bls12381Fr Bls12381Fr = Bls12381Fr
+instance ArithOpHs Mul Bls12381G1 Bls12381Fr where
+  type ArithResHs Mul Bls12381G1 Bls12381Fr = Bls12381G1
+instance ArithOpHs Mul Bls12381G2 Bls12381Fr where
+  type ArithResHs Mul Bls12381G2 Bls12381Fr = Bls12381G2
+instance Bls12381MulBadOrder Bls12381Fr Bls12381G1 =>
+         ArithOpHs Mul Bls12381Fr Bls12381G1 where
+  type ArithResHs Mul Bls12381Fr Bls12381G1 = Bls12381G1
+instance Bls12381MulBadOrder Bls12381Fr Bls12381G2 =>
+         ArithOpHs Mul Bls12381Fr Bls12381G2 where
+  type ArithResHs Mul Bls12381Fr Bls12381G2 = Bls12381G2
 
 instance UnaryArithOpHs Neg Integer where
   type UnaryArithResHs Neg Integer = Integer
 instance UnaryArithOpHs Neg Natural where
   type UnaryArithResHs Neg Natural = Integer
+instance UnaryArithOpHs Neg Bls12381Fr where
+  type UnaryArithResHs Neg Bls12381Fr = Bls12381Fr
+instance UnaryArithOpHs Neg Bls12381G1 where
+  type UnaryArithResHs Neg Bls12381G1 = Bls12381G1
+instance UnaryArithOpHs Neg Bls12381G2 where
+  type UnaryArithResHs Neg Bls12381G2 = Bls12381G2
 
 instance ArithOpHs Or Natural Natural where
   type ArithResHs Or Natural Natural = Natural
@@ -126,3 +157,6 @@
 
 instance UnaryArithOpHs Ge Integer where
   type UnaryArithResHs Ge Integer = Bool
+
+instance ToIntegerArithOpHs Natural
+instance ToIntegerArithOpHs Bls12381Fr
diff --git a/src/Lorentz/Empty.hs b/src/Lorentz/Empty.hs
--- a/src/Lorentz/Empty.hs
+++ b/src/Lorentz/Empty.hs
@@ -6,11 +6,10 @@
 
 -- | Support for uninhabited type.
 --
--- Currently they are not supported my Michelson, so we provide
--- a sort of replacement.
+-- Note: this module exists solely for historical reasons since the time when
+-- 'Never' was not yet supported by the Michelson.
 --
--- This module should be removed once the proposal is implemented:
--- https://gitlab.com/tezos/tezos/issues/662
+-- TODO [#549]: remove this module.
 module Lorentz.Empty
   ( Empty
   , absurd_
@@ -26,6 +25,7 @@
 import Michelson.Typed.Haskell.Doc
 
 -- | Replacement for uninhabited type.
+{-# DEPRECATED Empty "Use Never type instead" #-}
 newtype Empty = Empty ()
   deriving stock Generic
   deriving anyclass (IsoValue, HasAnnotation)
@@ -37,10 +37,10 @@
     \should never be called."
 
 -- | Someone constructed 'Empty' type.
-type instance ErrorArg "emptySupplied" = ()
+type instance ErrorArg "emptySupplied" = UnitErrorArg
 
 instance Buildable (CustomError "emptySupplied") where
-  build (CustomError _ ()) =
+  build (CustomError _ (_, ())) =
     "'Empty' value was passed to the contract."
 
 instance CustomErrorHasDoc "emptySupplied" where
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
@@ -16,6 +16,7 @@
   , CommonContractBehaviourKind
   , CommonEntrypointsBehaviourKind
   , diEntrypointToMarkdown
+  , SomeEntrypointArg (..)
   , DEntrypointArg (..)
   , DType (..)
   , DeriveCtorFieldDoc (..)
@@ -47,6 +48,7 @@
 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
 import Data.Vinyl.Core (RMap, rappend)
 import Fmt (Buildable(..), build, fmt, listF)
@@ -62,18 +64,19 @@
 import Lorentz.Entrypoints.Core
 import Lorentz.Entrypoints.Helpers
 import Lorentz.Entrypoints.Impl
-import Michelson.Printer (printUntypedValue)
+import Michelson.Printer (printTypedValue)
 import Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)
-import Michelson.Typed (pattern DefEpName, EpName, mkUType, sampleValueFromUntype)
+import Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue)
+import qualified Michelson.Typed as T
 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.Typeable
 import Util.TypeLits
 import Util.TypeTuple
+import Util.Typeable
 
 -- | Gathers information about single entrypoint.
 --
@@ -292,10 +295,14 @@
     , pbdMichelson = michDesc
     }
 
+-- | Entrypoint argument type in typed representation.
+data SomeEntrypointArg =
+  forall a. (NiceParameter a, TypeHasDoc a) => SomeEntrypointArg (Proxy a)
+
 -- | Describes argument of an entrypoint.
 data DEntrypointArg =
   DEntrypointArg
-  { epaArg :: Maybe DType
+  { epaArg :: Maybe SomeEntrypointArg
     -- ^ Argument of the entrypoint. Pass 'Nothing' if no argument is required.
   , epaBuilding :: [ParamBuildingStep]
     -- ^ Describes a way to lift an entrypoint argument into full parameter
@@ -307,29 +314,23 @@
     -- 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.
   }
 
 constructDEpArg
   :: forall arg.
-     ( TypeHasDoc arg
-     , HasAnnotation arg
-     , KnownValue arg
+     ( NiceParameter arg
+     , TypeHasDoc arg
      )
   => DEntrypointArg
 constructDEpArg = DEntrypointArg
-  { epaArg = Just $ DType (Proxy @arg)
+  { epaArg = Just $ SomeEntrypointArg (Proxy @arg)
   , epaBuilding = []
-  , epaType = mkDEpUType @arg
   }
 
 emptyDEpArg :: DEntrypointArg
 emptyDEpArg = DEntrypointArg
   { epaArg = Nothing
   , epaBuilding = []
-  , epaType = Untyped.Type Untyped.TUnit Untyped.noAnn
   }
 
 mkDEpUType :: forall t. (KnownValue t, HasAnnotation t) => Untyped.Type
@@ -337,15 +338,13 @@
 
 mkDEntrypointArgSimple
   :: forall t.
-     ( KnownValue t
-     , HasAnnotation t
+     ( NiceParameter t
      , TypeHasDoc t
      )
   => DEntrypointArg
 mkDEntrypointArgSimple = DEntrypointArg
-  { epaArg = Just $ DType (Proxy @t)
+  { epaArg = Just $ SomeEntrypointArg (Proxy @t)
   , epaBuilding = []
-  , epaType = mkDEpUType @t
   }
 
 -- | Go over contract code and update every occurrence of 'DEntrypointArg'
@@ -367,27 +366,29 @@
 instance DocItem DEntrypointArg where
   docItemPos = 20
   docItemSectionName = Nothing
-  docItemDependencies (DEntrypointArg mdty _ _) =
-    [SomeDocDefinitionItem dty | Just dty <- pure mdty]
-  docItemToMarkdown _ (DEntrypointArg mdty psteps et) =
+  docItemDependencies (DEntrypointArg mdty _) =
+    [ SomeDocDefinitionItem (DType $ Proxy @ty)
+    | Just (SomeEntrypointArg (_ :: Proxy ty)) <- pure mdty ]
+  docItemToMarkdown _ (DEntrypointArg mdty psteps) =
     mconcat . Prelude.map (<> "\n\n") $
       [ mdSubsection "Argument" $
           case mdty of
             Nothing -> "none (pass unit)"
-            Just (DType (dty :: Proxy ep)) -> mconcat . Prelude.intersperse "\n" $
+            Just (SomeEntrypointArg (dty :: Proxy ep)) -> mconcat . Prelude.intersperse "\n" $
               [ mempty
               , "  + " <>
                 mdSubsection "In Haskell"
                   (typeDocMdReference dty (WithinParens False))
               , "  + " <>
                 mdSubsection "In Michelson"
-                  (mdTicked $ printDocB False . renderDoc needsParens $ et)
-              , "    + " <>
+                  (mdTicked $ printDocB False . renderDoc needsParens $
+                     T.untypeDemoteT @(T.ToT ep))
+              , fromMaybe "" $ sampleTypedValue (sing @(ToT ep)) <&> \sampleVal ->
+                "    + " <>
                 mdSubsection "Example"
                   (mdAddId "example-id"
                     $ mdTicked
-                    $ build $ printUntypedValue True
-                    $ sampleValueFromUntype et
+                    $ build $ printTypedValue True sampleVal
                   )
               ],
           mdSpoiler "How to call this entrypoint" $
@@ -439,7 +440,7 @@
   deriveCtorFieldDoc = emptyDEpArg
 
 instance
-    (TypeHasDoc ty, HasAnnotation ty, KnownValue ty, KnownSymbol con)
+    (NiceParameter ty, TypeHasDoc ty, KnownValue ty, KnownSymbol con)
   =>
     DeriveCtorFieldDoc con ('OneField ty)
   where
@@ -536,9 +537,8 @@
   :: forall kind epName param s out.
      ( KnownSymbol epName
      , DocItem (DEntrypoint kind)
+     , NiceParameter param
      , TypeHasDoc param
-     , HasAnnotation param
-     , KnownValue param
      )
   => param : s :-> out -> param : s :-> out
 documentEntrypoint instr =
@@ -557,8 +557,8 @@
          , body ~ (param : s :-> out)
          , KnownSymbol epName
          , DocItem (DEntrypoint kind)
+         , NiceParameter param
          , TypeHasDoc param
-         , HasAnnotation param
          , KnownValue param
          ) => EntryArrow kind name body where
   (#->) _ = documentEntrypoint @kind @epName
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
@@ -282,7 +282,7 @@
   type GLookupEntrypoint mode 'EPLeaf (G.C1 ('G.MetaCons ctor _1 _2) x) =
     JustOnEq ctor (GExtractField x)
   gMkEntrypointsNotes =
-    (fst $ gGetAnnotation @x defaultAnnOptions FollowEntrypoint NotGenerateFieldAnn, ctorNameToAnn @ctor)
+    (gGetAnnotation @x defaultAnnOptions FollowEntrypoint NotGenerateFieldAnn ^. _1, ctorNameToAnn @ctor)
   gMkEpLiftSequence (Label :: Label name) =
     case sing @ctor %== sing @name of
       STrue -> EpConstructed EplArgHere
diff --git a/src/Lorentz/Errors.hs b/src/Lorentz/Errors.hs
--- a/src/Lorentz/Errors.hs
+++ b/src/Lorentz/Errors.hs
@@ -16,7 +16,6 @@
   , isoErrorFromVal
   , ErrorHasDoc (..)
   , typeDocMdDescriptionReferToError
-  , customErrorDocHaskellRepGeneral
   , isInternalErrorClass
 
   , UnspecifiedError (..)
@@ -27,11 +26,16 @@
   , failUnexpected
 
     -- * Custom errors
+  , NoErrorArg
+  , UnitErrorArg
   , ErrorArg
   , CustomError (..)
+  , CustomErrorRep
+  , IsCustomErrorArgRep (..)
+  , MustHaveErrorArg
   , failCustom
-  , RequireNoArgError
   , failCustom_
+  , failCustomNoArg
 
     -- * Documentation
   , ErrorClass (..)
@@ -63,7 +67,6 @@
 import Michelson.Typed.Haskell
 import Michelson.Typed.Instr
 import Michelson.Typed.Scope
-import Michelson.Typed.T
 import Util.Markdown
 import Util.Type
 import Util.Typeable
@@ -74,9 +77,10 @@
 ----------------------------------------------------------------------------
 
 type ErrorScope t =
-  -- We can require a weaker constraint (e.g. no 'HasNoOp'), but
-  -- for now it's the simplest way to make 'failUsing' work
   ( Typeable t
+  -- Since 008 it's prohibited to fail with non-packable values and with the
+  -- 'Contract t' type values, which is equivalent to our @ConstantScope@ constraint.
+  -- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.
   , ConstantScope t
   )
 
@@ -168,7 +172,7 @@
 instance ErrorHasDoc MText where
   errorDocName = "InternalError"
   errorDocMdCause =
-    "Some internal error occured."
+    "Some internal error occurred."
   errorDocHaskellRep =
     "Textual error message, see " <>
     typeDocMdReference (Proxy @MText) (WithinParens False) <> "."
@@ -197,7 +201,7 @@
 
 instance ErrorHasDoc UnspecifiedError where
   errorDocName = "Unspecified error"
-  errorDocMdCause = "Some error occured."
+  errorDocMdCause = "Some error occurred."
   errorDocHaskellRep = typeDocMdReference (Proxy @()) (WithinParens False) <> "."
   errorDocDependencies = typeDocDependencies (Proxy @())
 
@@ -282,79 +286,111 @@
 -- Use this in pattern matches against error (e.g. in tests).
 data CustomError (tag :: Symbol) = CustomError
   { ceTag :: Label tag
-  , ceArg :: ErrorArg tag
+  , ceArg :: CustomErrorRep tag
   }
 
-deriving stock instance Eq (ErrorArg tag) => Eq (CustomError tag)
-deriving stock instance Show (ErrorArg tag) => Show (CustomError tag)
+deriving stock instance Eq (CustomErrorRep tag) => Eq (CustomError tag)
+deriving stock instance Show (CustomErrorRep tag) => Show (CustomError tag)
 
 instance Buildable (CustomError tag) where
   build (CustomError tg _err) = "CustomError #" +| build tg
 
+-- | To be used as @ErrorArg@ instance when failing with just
+-- a @string@ instead of @pair string x@
+data NoErrorArg
+
+-- | To be used as @ErrorArg@ instances. This is equivalent to using
+-- @()@ but using @UnitErrorArg@ is preferred since @()@ behavior could
+-- be changed in the future.
+data UnitErrorArg
+
+
 -- | How 'CustomError' is actually represented in Michelson.
-type CustomErrorRep tag = (MText, ErrorArg tag)
+type CustomErrorRep tag = CustomErrorArgRep (ErrorArg tag)
 
+type family CustomErrorArgRep (errArg :: Kind.Type) where
+  CustomErrorArgRep NoErrorArg = MText
+  CustomErrorArgRep UnitErrorArg = (MText, ())
+  CustomErrorArgRep errArg = (MText, errArg)
+
+-- | Typeclass implements various method that work with `CustomErrorArgRep`.
+class IsCustomErrorArgRep a where
+  verifyErrorTag :: MText -> a -> Either Text a
+  customErrorRepDocDeps :: [SomeDocDefinitionItem]
+  customErrorHaskellRep
+    :: (KnownSymbol tag, CustomErrorHasDoc tag)
+    => Proxy tag -> Markdown
+
+instance IsCustomErrorArgRep MText where
+  verifyErrorTag expectedTag tag =
+    if tag == expectedTag
+    then Right tag
+    else Left $ "Bad tag, expected " +| expectedTag |+ ", got " +| tag |+ ""
+  customErrorRepDocDeps = []
+  customErrorHaskellRep (_ :: Proxy tag) =
+    mdTicked $ build (errorTagToText @tag)
+
+instance (TypeHasDoc errArg)
+  => IsCustomErrorArgRep (MText, errArg) where
+  verifyErrorTag expectedTag (tag, arg) =
+    if tag == expectedTag
+    then Right (tag, arg)
+    else Left $ "Bad tag, expected " +| expectedTag |+ ", got " +| tag |+ ""
+  customErrorRepDocDeps =
+    [ SomeDocDefinitionItem $ DType $ Proxy @errArg ]
+  customErrorHaskellRep (_ :: Proxy tag) = mconcat
+    [ mdTicked ("(" <> build (errorTagToText @tag) <> ", " <> "<error argument>" <> ")")
+    , ("\n\nProvided error argument will be of type "
+      <> typeDocMdReference (Proxy @(MText, errArg)) (WithinParens False)
+      <> (maybe "" (\txt -> " and stand for " <> txt) (customErrArgumentSemantics @tag))
+      <> "."
+      )
+    ]
+
 -- | This instance cannot be implemented, use 'IsError' instance instead.
-instance (WellTypedIsoValue (ErrorArg tag), TypeError ('Text "CustomError has no IsoValue instance")) =>
+instance (WellTypedIsoValue (CustomErrorRep tag), TypeError ('Text "CustomError has no IsoValue instance")) =>
          IsoValue (CustomError tag) where
   -- Originally we had a `TypeError` here, but that had to be changed when
   -- `WellTyped (ToT a)` was added as a superclass of `IsoValue`, because it
   -- resulted in the type error being triggerred from the evaluation of `ToT`
   -- typefamily in the super class clause.
-  type ToT (CustomError tag) = (ToT (MText, ErrorArg tag))
+  type ToT (CustomError tag) = (ToT (CustomErrorRep tag))
   toVal = error "impossible"
   fromVal = error "impossible"
 
-instance (CustomErrorHasDoc tag, KnownError (ErrorArg tag), IsoValue (ErrorArg tag)) =>
-         IsError (CustomError tag) where
-  errorToVal (CustomError l arg) cont =
-    cont $ toVal @(CustomErrorRep tag) (errorTagToMText l, arg)
+instance ( CustomErrorHasDoc tag
+         , KnownError (CustomErrorRep tag)
+         , IsoValue (CustomErrorRep tag)
+         , IsCustomErrorArgRep (CustomErrorRep tag)
+         )
+  => IsError (CustomError tag) where
+
+  errorToVal (CustomError _ arg) cont =
+    cont $ toVal @(CustomErrorRep tag) arg
+
   errorFromVal (v :: Value t) =
     let expectedTag = errorTagToMText (fromLabel @tag)
     in case cast v of
-        Just v' ->
-          let (tag, arg) = fromVal @(CustomErrorRep tag) v'
-          in if tag == expectedTag
-             then Right $ CustomError fromLabel arg
-             else Left $ "Bad tag, expected " +| expectedTag |+ ", got " +| tag |+ ""
+        Just v' -> do
+          errArg <- verifyErrorTag @(CustomErrorRep tag) expectedTag
+            $ fromVal @(CustomErrorRep tag) v'
+          pure $ CustomError fromLabel errArg
         Nothing -> Left $ "Wrong type for custom error: " <> pretty (demote @t)
 
-instance (CustomErrorHasDoc tag, SingI (ToT (ErrorArg tag))) =>
-         ErrorHasDoc (CustomError tag) where
+instance ( CustomErrorHasDoc tag
+         , IsCustomErrorArgRep (CustomErrorRep tag)
+         )
+  => ErrorHasDoc (CustomError tag) where
   errorDocName = errorTagToText @tag
-  errorDocDependencies = [SomeDocDefinitionItem $ DType $ Proxy @(ErrorArg tag)]
+  errorDocDependencies = customErrorRepDocDeps @(CustomErrorRep tag)
   errorDocMdCause = customErrDocMdCause @tag
   errorDocMdCauseInEntrypoint = customErrDocMdCauseInEntrypoint @tag
   errorDocClass = customErrClass @tag
-  errorDocHaskellRep =
-    customErrorDocHaskellRepGeneral (show $ errorTagToText @tag) (Proxy @tag)
+  errorDocHaskellRep = customErrorHaskellRep @(CustomErrorRep tag) (Proxy @tag)
 
-  type ErrorRequirements (CustomError tag) = (CustomErrorHasDoc tag, SingI (ToT (ErrorArg tag)))
+  type ErrorRequirements (CustomError tag) = (CustomErrorHasDoc tag, IsCustomErrorArgRep (CustomErrorRep 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 :: Label tag -> MText
 errorTagToMText l =
@@ -370,7 +406,7 @@
 -- | Fail with given custom error.
 failCustom
   :: forall tag err s any.
-     ( err ~ ErrorArg tag
+     ( MustHaveErrorArg tag (MText, err)
      , CustomErrorHasDoc tag
      , KnownError err
      )
@@ -378,38 +414,55 @@
 failCustom l =
   doc (DThrows (Proxy @(CustomError tag))) #
   push (errorTagToMText l) # pair @MText @err #
-  FI (FAILWITH @(ToT (CustomErrorRep tag)))
+  FI (FAILWITH @(ToT (MText, err)))
 
-type RequireNoArgError tag msg =
-  ( TypeErrorUnless (ErrorArg tag == ()) msg
-  , msg ~
-    ('Text "Expected no-arg error, but given error requires argument of type "
-      ':<>: 'ShowType (ErrorArg tag)
-    )
+-- | Fail with given custom error.
+failCustomNoArg
+  :: forall tag s any.
+     ( MustHaveErrorArg tag MText
+     , CustomErrorHasDoc tag
+     )
+  => Label tag -> s :-> any
+failCustomNoArg l =
+  doc (DThrows (Proxy @(CustomError tag))) #
+  push (errorTagToMText l) #
+  FI (FAILWITH @(ToT (MText)))
+
+
+type MustHaveErrorArg errorTag expectedArgRep =
+  ( TypeErrorUnless (CustomErrorRep errorTag == expectedArgRep)
+      ('Text "Error argument type is "
+        ':<>: 'ShowType (expectedArgRep)
+        ':<>: 'Text " but given error requires argument of type "
+        ':<>: 'ShowType (CustomErrorRep errorTag)
+      )
+  , CustomErrorRep errorTag ~ expectedArgRep
   )
 
--- | Specialization of 'failCustom' for no-arg errors.
+-- | Specialization of 'failCustom' for unit-arg errors.
 failCustom_
-  :: forall tag s any notVoidErrorMsg.
-     ( RequireNoArgError tag notVoidErrorMsg
+  :: forall tag s any.
+     ( MustHaveErrorArg tag (MText, ())
      , CustomErrorHasDoc tag
      )
   => Label tag -> s :-> any
 failCustom_ l =
-  inTypeErrorUnless @(ErrorArg tag == ()) @notVoidErrorMsg $
-  reifyTypeEquality @(ErrorArg tag) @() $
-    unit # failCustom l
+  reifyTypeEquality @(CustomErrorRep tag) @(MText, ()) $
+    doc (DThrows (Proxy @(CustomError tag))) #
+    unit #
+    push (errorTagToMText l) # pair @MText @() #
+    FI (FAILWITH @(ToT (MText, ())))
 
 -- Special treatment of no-arg errors
 ----------------------------------------------------------------------------
 
-instance Eq (ErrorArg tag) => Eq (() -> CustomError tag) where
+instance Eq (CustomErrorRep tag) => Eq (() -> CustomError tag) where
   e1 == e2 = e1 () == e2 ()
-instance Show (ErrorArg tag) => Show (() -> CustomError tag) where
+instance Show (CustomErrorRep tag) => Show (() -> CustomError tag) where
   show e = show (e ())
 
 -- | If 'CustomError' constructor is not provided its argument, we assume
--- that this is no-arg error and interpret the passed value as complete.
+-- that this is unit-arg error and interpret the passed value as complete.
 instance ( Typeable arg
          , IsError (CustomError tag)
          , TypeErrorUnless (arg == ()) notVoidError
@@ -421,13 +474,11 @@
          ) =>
          IsError (arg -> CustomError tag) where
   errorToVal mkCustomError cont =
-    inTypeErrorUnless @(arg == ()) @notVoidError $
     reifyTypeEquality @arg @() $
       errorToVal (mkCustomError ()) cont
   errorFromVal v =
-    inTypeErrorUnless @(arg == ()) @notVoidError $
     reifyTypeEquality @arg @() $
-      errorFromVal v <&> \(CustomError l ()) -> CustomError l
+      errorFromVal v <&> \(CustomError l (a, ())) -> \b -> CustomError l (a, b)
 
 instance (Typeable arg, ErrorHasDoc (CustomError tag)) =>
          ErrorHasDoc (arg -> CustomError tag) where
@@ -487,7 +538,7 @@
   ErrClassContractInternal -> True
   ErrClassUnknown -> False
 
-class (KnownSymbol tag, TypeHasDoc (ErrorArg tag), IsError (CustomError tag)) =>
+class (KnownSymbol tag, TypeHasDoc (CustomErrorRep tag), IsError (CustomError tag)) =>
       CustomErrorHasDoc tag where
   -- | What should happen for this error to be raised.
   customErrDocMdCause :: Markdown
@@ -608,9 +659,8 @@
   given entrypoint call two different errors may take place, the one which
   appears in the list first will be thrown.
 
-  Most of the errors are represented according to the same
-  `(error tag, error argument)` pattern. See the list of errors below
-  for details.
+  The errors are represented either as a string `error tag` or a pair `(error tag, error argument)`.
+  See the list of errors below for details.
 
   We distinquish several error classes:
   + #{mdBold $ build ErrClassActionException}: given action cannot be performed with
diff --git a/src/Lorentz/Errors/Common.hs b/src/Lorentz/Errors/Common.hs
--- a/src/Lorentz/Errors/Common.hs
+++ b/src/Lorentz/Errors/Common.hs
@@ -19,10 +19,10 @@
 
 -- | Contract initiator should be contract admin in order to perform this
 -- operation.
-type instance ErrorArg "senderIsNotAdmin" = ()
+type instance ErrorArg "senderIsNotAdmin" = UnitErrorArg
 
 instance Buildable (CustomError "senderIsNotAdmin") where
-  build (CustomError _ ()) =
+  build (CustomError _ (_, ())) =
     "This operation can be executed only by admin, but is invoked by \
     \someone else"
 
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
@@ -221,8 +221,7 @@
   numericErrorDocTextualTag :: ErrorRequirements err => Text
 
 instance ErrorHasNumericDoc (CustomError tag) where
-  numericErrorDocHaskellRep numTag =
-    customErrorDocHaskellRepGeneral numTag (Proxy @tag)
+  numericErrorDocHaskellRep _ = customErrorHaskellRep @(CustomErrorRep tag) (Proxy @tag)
   numericErrorDocTextualTag = errorTagToText @tag
 
 instance ErrorHasDoc (VoidResult res) =>
diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs
--- a/src/Lorentz/Instr.hs
+++ b/src/Lorentz/Instr.hs
@@ -12,7 +12,10 @@
   , commentAroundStmt
   , drop
   , dropN
+  , ConstraintDUPNLorentz
   , dup
+  , dupNPeano
+  , dupN
   , swap
   , ConstraintDIGLorentz
   , digPeano
@@ -41,7 +44,13 @@
   , iter
   , mem
   , get
+  , ConstraintPairGetLorentz
+  , PairGetHs
+  , pairGet
   , update
+  , ConstraintPairUpdateLorentz
+  , PairUpdateHs
+  , pairUpdate
   , failingWhenPresent
   , updateNew
   , if_
@@ -96,6 +105,8 @@
   , now
   , amount
   , balance
+  , votingPower
+  , totalVotingPower
   , checkSignature
   , sha256
   , sha512
@@ -103,11 +114,14 @@
   , sha3
   , keccak
   , hashKey
+  , pairingCheck
   , source
   , sender
   , address
+  , selfAddress
   , chainId
   , level
+  , never
   , framed
   , LorentzFunctor (..)
   , NonZero (..)
@@ -132,9 +146,10 @@
 import Lorentz.Value
 import Lorentz.Zip
 import Michelson.Typed
-  (pattern CAR, pattern CDR, CommentType(..), ConstraintDIG, ConstraintDIG', ConstraintDIPN,
-  ConstraintDIPN', ConstraintDUG, ConstraintDUG', EntrypointCallT(..), ExtInstr(..), Instr(..),
-  pattern PAIR, RemFail(..), SomeEntrypointCallT(..), Value'(..), sepcName, starNotes)
+  (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)
 import Michelson.Typed.Arith
 import Michelson.Typed.Haskell.Value
 import Util.Peano
@@ -143,7 +158,6 @@
 nop :: s :-> s
 nop = I Nop
 
-
 justComment :: Text -> s :-> s
 justComment = comment . JustComment
 
@@ -176,14 +190,35 @@
   -- ↓ Kinda obvious, but not to GHC.
   , Drop (ToPeano n) (ToTs s) ~ ToTs (Drop (ToPeano n) s)
   ) => s :-> Drop (ToPeano n) s
-dropN = I (DROPN $ sing @(ToPeano n))
+dropN = I (DROPN $ peanoSing @n)
   where
     _example :: '[ Integer, Integer, Integer ] :-> '[]
     _example = dropN @3
 
-dup  :: a : s :-> a : a : s
+dup :: a : s :-> a : a : s
 dup = I DUP
 
+type ConstraintDUPNLorentz (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type])
+  (a :: Kind.Type) =
+  ( ConstraintDUPN n (ToTs inp) (ToTs out) (ToT a)
+  , ConstraintDUPN' Kind.Type n inp out a
+  )
+
+dupNPeano ::
+  forall (n :: Peano) inp out a.
+  ( ConstraintDUPNLorentz n inp out a
+  ) => inp :-> out
+dupNPeano = I (DUPN (sing @n))
+
+dupN ::
+  forall (n :: GHC.Nat) inp out a.
+  ( ConstraintDUPNLorentz (ToPeano n) inp out a
+  ) => inp :-> out
+dupN = dupNPeano @(ToPeano n)
+  where
+    _example :: '[ Integer, (), Bool ] :-> '[ Bool, Integer, (), Bool ]
+    _example = dupN @3
+
 swap :: a : b : s :-> b : a : s
 swap = I SWAP
 
@@ -201,7 +236,7 @@
   )
 
 -- | Version of `dig` which uses Peano number.
--- It is inteded for internal usage in Lorentz.
+-- It is intended for internal usage in Lorentz.
 digPeano ::
   forall (n :: Peano) inp out a.
   ( ConstraintDIGLorentz n inp out a
@@ -220,7 +255,7 @@
     _example = dig @3
 
 -- | Version of `dug` which uses Peano number.
--- It is inteded for internal usage in Lorentz.
+-- It is intended for internal usage in Lorentz.
 dugPeano ::
   forall (n :: Peano) inp out a.
   ( ConstraintDUGLorentz n inp out a
@@ -315,9 +350,47 @@
   => GetOpKeyHs c : c : s :-> Maybe (GetOpValHs c) : s
 get = I GET
 
+type ConstraintPairGetLorentz (n :: GHC.Nat) (pair :: Kind.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
+  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]).
+     ConstraintPairGetLorentz n pair
+  => pair : s :-> PairGetHs (ToPeano n) pair : s
+pairGet = I (GETN (peanoSing @n))
+  where
+    _example :: '[ (Integer, Natural), () ] :-> '[ Integer, () ]
+    _example = pairGet @1
+
 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) =
+  ( 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
+  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]).
+     ConstraintPairUpdateLorentz n val pair
+  => val : pair : s :-> PairUpdateHs (ToPeano n) val pair : s
+pairUpdate = I (UPDATEN (peanoSing @n))
+  where
+    _example :: '[ MText, (Integer, Natural) ] :-> '[ (MText, Natural) ]
+    _example = pairUpdate @1
+
 if_ :: (s :-> s') -> (s :-> s') -> (Bool : s :-> s')
 if_ = iGenericIf IF
 
@@ -387,7 +460,7 @@
   )
 
 -- | Version of `dipN` which uses Peano number.
--- It is inteded for internal usage in Lorentz.
+-- It is intended for internal usage in Lorentz.
 dipNPeano ::
   forall (n :: Peano) (inp :: [Kind.Type]) (out :: [Kind.Type]) (s :: [Kind.Type]) (s' :: [Kind.Type]).
   ( ConstraintDIPNLorentz n inp out s s'
@@ -403,8 +476,11 @@
     _example :: '[ Integer, Integer, Integer ] :-> '[ Integer, Integer, Integer, () ]
     _example = dipN @3 unit
 
-failWith :: KnownValue a => a : s :-> t
-failWith = FI FAILWITH
+-- Since 008 it's prohibited to fail with non-packable values and with the
+-- 'Contract t' type values, which is equivalent to our @NiceConstant@ constraint.
+-- See https://gitlab.com/tezos/tezos/-/issues/1093#note_496066354 for more information.
+failWith :: forall a s t. NiceConstant a => a : s :-> t
+failWith = FI FAILWITH \\ niceConstantEvi @a
 
 cast :: KnownValue a => (a : s :-> a : s)
 cast = I CAST
@@ -524,7 +600,7 @@
 ge0 :: UnaryArithOpHs Ge n => n : s :-> UnaryArithResHs Ge n : s
 ge0 = I GE
 
-int :: Natural : s :-> Integer : s
+int :: (ToIntegerArithOpHs i) => i : s :-> Integer : s
 int = I INT
 
 -- | Get a reference to the current contract.
@@ -653,6 +729,12 @@
 balance :: s :-> Mutez : s
 balance = I BALANCE
 
+votingPower :: KeyHash : s :-> Natural : s
+votingPower = I VOTING_POWER
+
+totalVotingPower :: s :-> Natural : s
+totalVotingPower = I TOTAL_VOTING_POWER
+
 checkSignature :: BytesLike bs => PublicKey : TSignature bs : bs : s :-> Bool : s
 checkSignature = I CHECK_SIGNATURE
 
@@ -665,17 +747,18 @@
 blake2B :: BytesLike bs => bs : s :-> Hash Blake2b bs : s
 blake2B = I BLAKE2B
 
-{-# WARNING sha3 "Introduced by the Edo Protocol (008); This won't work on previous versions." #-}
 sha3 :: BytesLike bs => bs : s :-> Hash Sha3 bs : s
 sha3 = I SHA3
 
-{-# WARNING keccak "Introduced by the Edo Protocol (008); This won't work on previous versions." #-}
 keccak :: BytesLike bs => bs : s :-> Hash Keccak bs : s
 keccak = I KECCAK
 
 hashKey :: PublicKey : s :-> KeyHash : s
 hashKey = I HASH_KEY
 
+pairingCheck :: [(Bls12381G1, Bls12381G2)] : s :-> Bool : s
+pairingCheck = I PAIRING_CHECK
+
 {-# WARNING source
     "Using `source` is considered a bad practice.\n\
 \    Consider using `sender` instead until further investigation" #-}
@@ -691,10 +774,15 @@
 chainId :: s :-> ChainId : s
 chainId = I CHAIN_ID
 
-{-# WARNING level "Introduced by the Edo Protocol (008); This won't work on previous versions." #-}
 level :: s :-> Natural : s
 level = I LEVEL
 
+selfAddress :: s :-> Address : s
+selfAddress = I SELF_ADDRESS
+
+never :: Never : s :-> s'
+never = FI NEVER
+
 -- | Execute given instruction on truncated stack.
 --
 -- This instruction requires you to specify the piece of stack to truncate
@@ -721,20 +809,20 @@
 failingWhenPresent
   :: forall c k s v st e.
      ( MemOpHs c, k ~ MemOpKeyHs c
-     , KnownValue e
+     , NiceConstant e
      , st ~ (k : v : c : s)
      )
   => (forall s0. k : s0 :-> e : s0)
   -> st :-> st
 failingWhenPresent mkErr =
-  dip (dip dup # swap) # swap # dip dup # swap # mem #
+  dupN @3 # dupN @2 # mem #
   if_ (mkErr # failWith) nop
 
 -- | Like 'update', but throw an error on attempt to overwrite existing entry.
 updateNew
   :: forall c k s e.
      ( UpdOpHs c, MemOpHs c, k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c
-     , KnownValue e
+     , NiceConstant e
      )
   => (forall s0. k : s0 :-> e : s0)
   -> k : UpdOpParamsHs c : c : s :-> c : s
diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs
--- a/src/Lorentz/Macro.hs
+++ b/src/Lorentz/Macro.hs
@@ -58,10 +58,8 @@
   , assertUsing
 
   -- * Syntactic Conveniences
-  , ConstraintDuupXLorentz
   , ConstraintReplaceNLorentz
   , ConstraintUpdateNLorentz
-  , DuupX (..)
   , ReplaceN (..)
   , UpdateN (..)
   , dropX
@@ -145,7 +143,7 @@
 import Lorentz.Instr
 import Lorentz.Polymorphic
 import Lorentz.Value
-import Michelson.Typed (ConstraintDIG', ConstraintDIPN', ConstraintDUG', T)
+import Michelson.Typed (ConstraintDIPN', ConstraintDUG', T)
 import Michelson.Typed.Arith
 import Michelson.Typed.Haskell.Value
 import Util.Markdown
@@ -345,61 +343,17 @@
   => a : s :-> CloneXT (ToPeano n) a s
 cloneX = cloneXImpl @(ToPeano n)
 
--- | Kind-agnostic constraint for duupX
-type DuupXConstraint' kind (n :: Peano)
-  (s :: [kind]) (a :: kind) (s1 :: [kind]) (tail :: [kind]) =
-  ( tail ~ Drop ('S n) s
-  , ConstraintDIPN' kind n s s1 (a ': tail) (a ': a ': tail)
-  , ConstraintDIG' kind n s1 (a ': s) a
-  )
-
--- | Constraint for duupX that combines kind-agnostic constraint for
--- Lorentz (Haskell) types and for our typed Michelson.
-type ConstraintDuupXLorentz (n :: Peano)
-  (s :: [Kind.Type]) (a :: Kind.Type)
-  (s1 :: [Kind.Type]) (tail :: [Kind.Type]) =
-  ( DuupXConstraint' T n (ToTs s) (ToT a) (ToTs s1) (ToTs tail)
-  , DuupXConstraint' Kind.Type n s a s1 tail
-  )
-
-class DuupX (n :: Peano) (s :: [Kind.Type]) (a :: Kind.Type) s1 tail where
-  duupXImpl :: s :-> a ': s
-
-instance (s ~ (a ': xs)) => DuupX ('S 'Z) s a s1 tail where
-  duupXImpl = dup
-
-instance DuupX ('S ('S 'Z)) (b ': a ': xs) a s1 tail where
-  duupXImpl = dip dup # swap
-
-instance (ConstraintDuupXLorentz ('S ('S n)) s a s1 tail) =>
-  DuupX ('S ('S ('S n))) s a s1 tail where
-  duupXImpl =
-    -- 'stackType' helps GHC deduce types
-    dipNPeano @('S ('S n)) (dup # stackType @(a ': a ': tail)) #
-    digPeano @('S ('S n))
-
 -- | @DUU+P@ macro. For example, `duupX @3` is `DUUUP`, it puts
 -- the 3-rd (starting from 1) element to the top of the stack.
--- Note that it is implemented differently for `n ≤ 2` and for `n > 2`.
--- In the latter case it is implemented using `dipN`, `dig` and `dup`.
--- In the former case it uses specialized versions.
--- There is also a minor difference with the implementation of `DUU*P` in
--- Michelson.
--- They implement `DUUUUP` as `DIP 3 { DUP }; DIG 4`.
--- We implement it as `DIP 3 { DUP }; DIG 3`. These are equivalent.
--- Our version is supposedly cheaper, at least it should be packed
--- more efficiently due to the way numbers are packed.
-duupX :: forall (n :: GHC.Nat) a (s :: [Kind.Type]) (s1 :: [Kind.Type]) (tail :: [Kind.Type]).
-  ( ConstraintDuupXLorentz (ToPeano (n - 1)) s a s1 tail
-  , DuupX (ToPeano n) s a s1 tail
-  )
+--
+-- Note that @DUU+P@ has since been added as the @DUP n@ instruction and so this
+-- macro is defined simply as follows:
+--
+-- > duupX = dupN @n
+duupX
+  :: forall (n :: GHC.Nat) s s' a. ConstraintDUPNLorentz (ToPeano n) s s' a
   => s :-> a ': s
-duupX = duupXImpl @(ToPeano n) @s @a @s1 @tail
-  where
-    _example ::
-      '[ Integer, (), Bool ] :->
-      '[ Bool, Integer, (), Bool ]
-    _example = duupX @3
+duupX = dupN @n
 
 -- | Version of 'framed' which accepts number of elements on input stack
 -- which should be preserved.
@@ -491,7 +445,7 @@
   --
   -- As first argument accepts container name (for error message).
   mapInsertNew
-    :: (NiceComparable k, KnownValue e)
+    :: (NiceComparable k, NiceConstant e)
     => (forall s0. k : s0 :-> e : s0)
     -> k : v : map k v : s :-> map k v : s
 
@@ -520,7 +474,7 @@
 --
 -- As first argument accepts container name.
 setInsertNew
-  :: (NiceComparable e, KnownValue err)
+  :: (NiceComparable e, NiceConstant err)
   => (forall s0. e : s0 :-> err : s0)
   -> e : Set e : s :-> Set e : s
 setInsertNew desc = dip (push True) # failingWhenPresent desc # update
@@ -699,7 +653,7 @@
   -> View a r : storage : s :-> (List Operation, storage) : s
 view_ code =
   unwrapView #
-  unpair # dip (duupX @2) # code # dip amount #
+  unpair # dip (dupN @2) # code # dip amount #
   transferTokens # nil # swap # cons # pair
 
 -- | @void@ type synonym as described in A1.
@@ -808,7 +762,7 @@
 
 void_
   :: forall a b s s' anything.
-      (IsError (VoidResult b), KnownValue b)
+      (IsError (VoidResult b), NiceConstant b)
   => a : s :-> b : s' -> Void_ a b : s :-> anything
 void_ code =
   doc (DThrows (Proxy @(VoidResult b))) #
@@ -848,17 +802,11 @@
     push (FutureContract contractRef) # dup #
     runFutureContract # ifNone onContractNotFound (dip drop)
 
--- | Get address of the current contract.
---
--- TODO [#373]: reimplement this using SELF_ADDRESS
-selfAddress :: s :-> Address : s
-selfAddress = self @() # address
-
 -- | Duplicate two topmost items on top of the stack.
 dupTop2 ::
   forall (a :: Kind.Type) (b :: Kind.Type) (s :: [Kind.Type]).
   a ': b ': s :-> a ': b ': a ': b ': s
-dupTop2 = duupX @2 # duupX @2
+dupTop2 = dupN @2 # dupN @2
 
 fromOption
   :: (NiceConstant a)
diff --git a/src/Lorentz/Rebinded.hs b/src/Lorentz/Rebinded.hs
--- a/src/Lorentz/Rebinded.hs
+++ b/src/Lorentz/Rebinded.hs
@@ -117,7 +117,7 @@
     fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r
 
   PreserveArgsBinCondition condition -> \l r ->
-    dip dup # swap # dip dup # swap #
+    dupN @2 # dupN @2 #
     ifThenElse condition
       -- since this pattern is commonly used when one of the branches fails,
       -- it's essential to @drop@ within branches, not after @if@ - @drop@s
diff --git a/src/Lorentz/ReferencedByName.hs b/src/Lorentz/ReferencedByName.hs
--- a/src/Lorentz/ReferencedByName.hs
+++ b/src/Lorentz/ReferencedByName.hs
@@ -24,7 +24,7 @@
 
 import Data.Constraint ((\\))
 import qualified Data.Kind as Kind
-import Data.Singletons (Sing, SingI)
+import Data.Singletons (Sing)
 import Named (NamedF(..))
 
 import Lorentz.ADT
@@ -32,6 +32,7 @@
 import Lorentz.Coercions
 import Lorentz.Instr
 import Michelson.Text
+import Michelson.Typed
 import Util.Label
 import Util.Peano
 import Util.Type
@@ -110,9 +111,14 @@
   -- | 1-based position of the variable on stack.
   varPosition :: VarPosition s name var
 
+type ConstraintVarPosition s n =
+  ( SingI n, KnownPeano n, n > 'Z ~ 'True
+  , RequireLongerOrSameLength s n, RequireLongerOrSameLength (ToTs s) n
+  )
+
 data VarPosition (s :: [Kind.Type]) (name :: Symbol) (var :: Kind.Type) where
   VarPosition
-    :: (SingI n, KnownPeano n)
+    :: (ConstraintVarPosition s n)
     => (Sing (n :: Nat))
     -> VarPosition s name var
 
@@ -135,7 +141,7 @@
 
 instance (ty ~ NamedF f var name) =>
          ElemHasNamedVar (ty : s) name var 'True where
-  elemVarPosition = VarPosition SZ
+  elemVarPosition = VarPosition (SS SZ)
 
 instance (HasNamedVar s name var) =>
          ElemHasNamedVar (ty : s) name var 'False where
@@ -154,18 +160,17 @@
 --
 -- @martoon: I'm not ready to fight the compiler regarding numerous
 -- complex constraints, so just assuring it that those constraints will hold.
+--
+-- @heitor.toledo: GHC doesn't seem to enjoy it that we use 'ConstraintDUPNLorentz',
+-- so I replaced it with the expanded definition.
 dupLUnsafe
   :: forall n s var.
-     (SingI n, KnownPeano n)
+     (ConstraintVarPosition s n)
   => Sing (n :: Nat) -> s :-> var : s
 dupLUnsafe _ =
-  -- generate dummy type variables
-  case (Proxy, Proxy) of
-    (_ :: Proxy s', _ :: Proxy (s0 :: [Kind.Type])) ->
-      dipNPeano @n (dup :: var : s0 :-> var : var : s0) #
-      digPeano @n
-        \\ provideConstraintUnsafe @(ConstraintDIPNLorentz n s s' (var : s0) (var : var : s0))
-        \\ provideConstraintUnsafe @(ConstraintDIGLorentz n s' (var : s) var)
+  dupNPeano @n
+    \\ provideConstraintUnsafe @(Take (Decrement n) s ++ (var : Drop n s) ~ s)
+    \\ provideConstraintUnsafe @(Take (Decrement n) (ToTs s) ++ (ToT var : Drop n (ToTs s)) ~ ToTs s)
 
 -- | Version of 'dupL' that leaves a named variable on stack.
 dupLNamed
@@ -184,20 +189,6 @@
         (HasNamedVar s name var)
      => Label name -> s :-> var : s
 dupL l = dupLNamed l # fromNamed l
-
-{- Note about optimizations:
-
-In @duupX@ we have several separate instances in order to optimize
-"duupX @1" and "duupX @2" cases, but I'm not sure whether can we do the same
-here and at the same time preserve sane error messages
-(like "missing `HasNamedVar s name Integer` instance", without mentioning any internal
-details).
-
-Since we are already delving into severely deceving the type system here,
-I think we'd better optimize those cases via adding respective rules in
-our optimizer (that would be difficult to do in an honest way).
-
--}
 
 -- Samples
 ----------------------------------------------------------------------------
diff --git a/src/Lorentz/StoreClass.hs b/src/Lorentz/StoreClass.hs
--- a/src/Lorentz/StoreClass.hs
+++ b/src/Lorentz/StoreClass.hs
@@ -237,6 +237,15 @@
     , 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
 ----------------------------------------------------------------------------
diff --git a/src/Lorentz/UParam.hs b/src/Lorentz/UParam.hs
--- a/src/Lorentz/UParam.hs
+++ b/src/Lorentz/UParam.hs
@@ -222,13 +222,13 @@
       ArgumentUnpackFailed -> "UNPACK failed"
 
 type instance ErrorArg "uparamNoSuchEntrypoint" = MText
-type instance ErrorArg "uparamArgumentUnpackFailed" = ()
+type instance ErrorArg "uparamArgumentUnpackFailed" = UnitErrorArg
 
 instance Buildable (CustomError "uparamNoSuchEntrypoint") where
-  build (CustomError _ name) = "No such entrypoint: " <> build name
+  build (CustomError _ (_, name)) = "No such entrypoint: " <> build name
 
 instance Buildable (CustomError "uparamArgumentUnpackFailed") where
-  build (CustomError _ ()) = "UNPACK failed"
+  build (CustomError _ (_, ())) = "UNPACK failed"
 
 instance CustomErrorHasDoc "uparamNoSuchEntrypoint" where
   customErrClass = ErrClassBadArgument
diff --git a/src/Lorentz/Value.hs b/src/Lorentz/Value.hs
--- a/src/Lorentz/Value.hs
+++ b/src/Lorentz/Value.hs
@@ -2,6 +2,8 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
+{-# LANGUAGE EmptyDataDeriving #-}
+
 -- | Re-exports typed Value, CValue, some core types, some helpers and
 -- defines aliases for constructors of typed values.
 --
@@ -19,11 +21,15 @@
   , Address
   , EpAddress (..)
   , Mutez
+  , Never
   , Timestamp
   , ChainId
   , KeyHash
   , PublicKey
   , Signature
+  , Bls12381Fr
+  , Bls12381G1
+  , Bls12381G2
   , Set
   , Map
   , M.BigMap (..)
@@ -81,11 +87,26 @@
 import Tezos.Core
   (ChainId, Mutez, Timestamp, oneMutez, timestampFromSeconds, timestampFromUTCTime, timestampQuote,
   toMutez, zeroMutez)
-import Tezos.Crypto (KeyHash, PublicKey, Signature)
+import Tezos.Crypto (Bls12381Fr, Bls12381G1, Bls12381G2, KeyHash, PublicKey, Signature)
 import Util.CustomGeneric as ReExports
 import Util.Label (Label(..))
 
+import Lorentz.Annotation
+
 type List = []
+
+data Never
+  deriving stock (Generic, Show, Eq, Ord)
+  deriving anyclass (IsoValue, NFData)
+
+instance Buildable Never where
+  build = \case
+
+instance HasAnnotation Never where
+  getAnnotation _ = M.starNotes
+
+instance M.TypeHasDoc Never where
+  typeDocMdDescription = "An uninhabited type."
 
 -- | Provides 'Buildable' instance that prints Lorentz value via Michelson's
 -- 'Value'.