diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,63 @@
 <!-- Unreleased: append new entries here -->
 
 
+0.15.0
+======
+* [!1273](https://gitlab.com/morley-framework/morley/-/merge_requests/1273)
+  Add LAMBDA_REC and Lambda_rec support
+  + `framed` instruction moved to `Lorentz.Instr.Framed` (re-exported from
+    `Lorentz.Instr`).
+  + `IsoValue` and `HasAnnotation` instances for `(:->)` are replaced with
+    type-errored ones, as Lorentz code is no longer isomorphic to lambdas.
+  + `TypeHasDoc` instance for `(:->)` removed.
+  + `WrappedLambda` is now a sum datatype.
+  + `unWrappedLambda` removed, as recursive lambdas can't be unwrapped like
+    that.
+  + All lambda-related instances moved to `Lorentz.Lambda`.
+  + `lambdaRec` instruction introduced.
+  + `mkLambdaRec` helper for constructing recursive lambda values introduced.
+* [!1278](https://gitlab.com/morley-framework/morley/-/merge_requests/1278)
+  Deprecate timelock-related functions
+* [!1270](https://gitlab.com/morley-framework/morley/-/merge_requests/1270)
+  Add lima protocol TICKET instruction, rename old one to TICKET_DEPRECATED
+  + The `TICKET` instruction was renamed to `TICKET_DEPRECATED`
+  + A new `TICKET` instruction was added which no longer allows zero amount
+    tickets. It now returns `Some Ticket` and `None` in case of zero amount
+    supplied.
+* [!1267](https://gitlab.com/morley-framework/morley/-/merge_requests/1267)
+  Added Lorentz.ADT doctests examples / tests
+* [!1271](https://gitlab.com/morley-framework/morley/-/merge_requests/1271)
+  Miscellaneous chores
+  + Add Buildable instances for `ZippedStackRepr` and `ZSNil`.
+  + Export `DupT` and `DipT` classes from `Lorentz.Referenced`.
+* [!1252](https://gitlab.com/morley-framework/morley/-/merge_requests/1252)
+  Better errors on stuck GetEntrypointArgCustom
+* [!1233](https://gitlab.com/morley-framework/morley/-/merge_requests/1233)
+  Rename Lorentz.Rebinded to Lorentz.Rebound
+* [!1242](https://gitlab.com/morley-framework/morley/-/merge_requests/1242)
+  Use `Constrained` utility existential
+* [!1180](https://gitlab.com/morley-framework/morley/-/merge_requests/1180)
+  Implement lmap for more types, and change signature of the typeclass to
+  be more pure.
+* [!1178](https://gitlab.com/morley-framework/morley/-/merge_requests/1178)
+  Add `HasNoNestedBigMaps t` constraint where required.
+  + These constraint were missing on TZIP-16 views, but effectively it is
+    required by the network for callbacks. This is a consequence of adding this
+    constraint to `Contract t` in Morley.
+* [!1222](https://gitlab.com/morley-framework/morley/-/merge_requests/1222)
+  Change the constraints on `constructStack` and `deconstruct` in
+  `Lorentz.ADT`, and on `documentEntrypoints` in `Lorentz.Entrypoints.Doc`.
+  Code using them in surprisingly polymorphic ways may need minor adjustments.
+  Applications of these functions should now be faster to typecheck and also
+  faster to run.
+* [!1216](https://gitlab.com/morley-framework/morley/-/merge_requests/1216)
+  Remove `KnownList` constraints from `euclidExtendedNormalization` and
+  `reduceRationalHelper` in `Lorentz.CustomArith.RationalArith`.
+* [!1198](https://gitlab.com/morley-framework/morley/-/merge_requests/1198)
+  Implement `dipT` using `dipN` for performance. This change also allows
+  `dipT` to be used without an explicit type argument when enough is known
+  about the passed stack action. Do the same for `dupT`, using `dupN`.
+
 0.14.1
 ======
 * [!1214](https://gitlab.com/morley-framework/morley/-/merge_requests/1214)
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.14.1
+version:        0.15.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
@@ -61,6 +61,7 @@
       Lorentz.Ext
       Lorentz.Extensible
       Lorentz.Instr
+      Lorentz.Instr.Framed
       Lorentz.Iso
       Lorentz.Lambda
       Lorentz.Layouts
@@ -70,7 +71,7 @@
       Lorentz.Polymorphic
       Lorentz.Prelude
       Lorentz.Print
-      Lorentz.Rebinded
+      Lorentz.Rebound
       Lorentz.Referenced
       Lorentz.ReferencedByName
       Lorentz.Run
@@ -142,7 +143,7 @@
       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 -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -Wno-unused-packages
+  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
   build-depends:
       aeson-pretty
     , base-noprelude >=4.7 && <5
@@ -165,6 +166,7 @@
     , template-haskell
     , text
     , text-manipulate
+    , type-errors
     , unordered-containers
     , vinyl
     , with-utf8
diff --git a/src/Lorentz.hs b/src/Lorentz.hs
--- a/src/Lorentz.hs
+++ b/src/Lorentz.hs
@@ -24,13 +24,13 @@
 import Lorentz.Ext as Exports
 import Lorentz.Instr as Exports
 import Lorentz.Iso as Exports
-import Lorentz.Lambda as Exports (Lambda, WrappedLambda, mkLambda)
+import Lorentz.Lambda as Exports
 import Lorentz.Macro as Exports
 import Lorentz.Pack as Exports
 import Lorentz.Polymorphic as Exports
 import Lorentz.Prelude as Exports
 import Lorentz.Print as Exports
-import Lorentz.Rebinded as Exports
+import Lorentz.Rebound as Exports
 import Lorentz.Referenced as Exports
 import Lorentz.ReferencedByName as Exports
 import Lorentz.Run as Exports
diff --git a/src/Lorentz/ADT.hs b/src/Lorentz/ADT.hs
--- a/src/Lorentz/ADT.hs
+++ b/src/Lorentz/ADT.hs
@@ -41,10 +41,13 @@
     -- * Advanced methods
   , getFieldOpen
   , setFieldOpen
+
+    -- * Definitions used in examples
+    -- $setup
   ) where
 
-import Data.Constraint ((\\))
 import Data.Vinyl.Core (RMap(..), Rec(..))
+import GHC.Generics qualified as G
 import GHC.TypeLits (AppendSymbol, Symbol)
 
 import Lorentz.Base
@@ -54,9 +57,46 @@
 import Morley.Michelson.Typed.Haskell.Value
 import Morley.Util.Label (Label)
 import Morley.Util.Named
-import Morley.Util.Type (KnownList, type (++))
+import Morley.Util.Type (type (++))
 import Morley.Util.TypeTuple
 
+{- $setup
+>>> import Data.Vinyl (Rec(..))
+>>> import Fmt (pretty)
+>>> import Lorentz.Base ((#))
+>>> import Lorentz.Instr as L
+>>> import Lorentz.Zip (ZippedStackRepr(..), ZSNil(..))
+>>> import Lorentz.Run.Simple ((-$), (-$?))
+>>> import Morley.Michelson.Runtime.Dummy (dummySelf)
+>>> import Morley.Michelson.Typed (IsoValue(..))
+>>> import Morley.Michelson.Typed.Haskell.Value (Ticket(..))
+>>> import Morley.Tezos.Address (Constrained(..))
+>>> :{
+data TestProduct = TestProduct
+  { fieldA :: Bool
+  , fieldB :: Integer
+  , fieldC :: ()
+  } deriving stock (Generic, Eq, Show)
+    deriving anyclass (IsoValue)
+--
+data TestProductWithNonDup = TestProductWithNonDup
+  { fieldTP :: TestProduct
+  , fieldD  :: Ticket () -- non-dupable value
+  } deriving stock (Generic, Eq, Show)
+    deriving anyclass (IsoValue)
+--
+data TestSum
+  = TestSumA Integer
+  | TestSumB (Bool, ())
+  deriving stock (Generic, Eq, Show)
+  deriving anyclass (IsoValue)
+:}
+
+>>> let testTicket = Ticket (Constrained dummySelf) () 10
+>>> let testProduct = TestProduct True 42 ()
+>>> let testProductWithNonDup = TestProductWithNonDup testProduct testTicket
+-}
+
 -- | Allows field access and modification.
 type HasField dt fname =
   ( InstrGetFieldC dt fname
@@ -116,6 +156,12 @@
 --
 -- For this and the following functions you have to specify field name
 -- which is either record name or name attached with @(:!)@ operator.
+--
+-- >>> :{
+--  (toField @TestProductWithNonDup #fieldTP -$ testProductWithNonDup) == testProduct
+-- :}
+-- True
+--
 toField
   :: forall dt name st.
      InstrGetFieldC dt name
@@ -130,12 +176,17 @@
 toFieldNamed l = toField l # toNamed l
 
 -- | Extract a field of a datatype, leaving the original datatype on stack.
+--
+-- >>> :{
+--  (getField @TestProduct #fieldB # L.swap # toField @TestProduct #fieldB # mul) -$
+--     testProduct { fieldB = 3 }
+-- :}
+-- 9
 getField
   :: forall dt name st.
      (InstrGetFieldC dt name, Dupable (GetFieldType dt name), HasDupableGetters dt)
   => Label name -> dt : st :-> GetFieldType dt name : dt ': st
 getField = I . instrGetField @dt
-  \\ dupableEvi @(GetFieldType dt name)
   where
     _needHasDupableGetters = Dict @(HasDupableGetters dt)
 
@@ -147,6 +198,9 @@
 getFieldNamed l = getField l # coerceWrap
 
 -- | Set a field of a datatype.
+--
+-- >>> setField @TestProduct #fieldB -$ 23 ::: testProduct
+-- TestProduct {fieldA = True, fieldB = 23, fieldC = ()}
 setField
   :: forall dt name st.
      InstrSetFieldC dt name
@@ -154,6 +208,9 @@
 setField = I . instrSetField @dt
 
 -- | Apply given modifier to a datatype field.
+--
+-- >>> modifyField @TestProduct #fieldB (dup # mul) -$ testProduct { fieldB = 8 }
+-- TestProduct {fieldA = True, fieldB = 64, fieldC = ()}
 modifyField
   :: forall dt name st.
      ( InstrGetFieldC dt name
@@ -212,6 +269,17 @@
 -- Instructions have to output fields of the built datatype, one per instruction;
 -- instructions order is expected to correspond to the order of fields in the
 -- datatype.
+--
+-- >>> :{
+--  let ctor =
+--        (fieldCtor (push True)) :&
+--        (fieldCtor (push 42)) :&
+--        (fieldCtor (push ())) :&
+--        RNil
+-- :}
+--
+-- >>> construct @TestProduct ctor -$ ZSNil
+-- TestProduct {fieldA = True, fieldB = 42, fieldC = ()}
 construct
   :: forall dt st.
      ( InstrConstructC dt
@@ -224,6 +292,10 @@
   rmap (\(FieldConstructor i) -> FieldConstructor i) fctors
 
 -- | Version of 'construct' which accepts tuple of field constructors.
+--
+-- >>> let ctor = (fieldCtor (push True), fieldCtor (push 42), fieldCtor (push ()))
+-- >>> constructT @TestProduct ctor -$ ZSNil
+-- TestProduct {fieldA = True, fieldB = 42, fieldC = ()}
 constructT
   :: forall dt fctors st.
      ( InstrConstructC dt
@@ -236,30 +308,32 @@
 constructT = construct . recFromTuple
 
 -- | Construct an object from fields on the stack.
+--
+-- >>> constructStack @TestProduct -$ True ::: 42 ::: ()
+-- TestProduct {fieldA = True, fieldB = 42, fieldC = ()}
 constructStack
   :: forall dt fields st .
   ( InstrConstructC dt
   , fields ~ ConstructorFieldTypes dt
-  , KnownList fields
+  , ToTs fields ++ ToTs st ~ ToTs (fields ++ st)
   )
   => (fields ++ st) :-> dt : st
 constructStack =
   I (instrConstructStack @dt @(ToTs fields))
-      \\ totsKnownLemma @fields
-      \\ totsAppendLemma @fields @st
 
 -- | Decompose a complex object into its fields
+--
+-- >>> deconstruct @TestProduct # constructStack @TestProduct -$ testProduct
+-- TestProduct {fieldA = True, fieldB = 42, fieldC = ()}
 deconstruct
   :: forall dt fields st .
-  ( InstrDeconstructC dt
-  , KnownList fields
-  , fields ~ ConstructorFieldTypes dt
+  ( InstrDeconstructC dt (ToTs st)
+  , fields ~ GFieldTypes (G.Rep dt) '[]
+  , ToTs fields ++ ToTs st ~ ToTs (fields ++ st)
   )
   => dt : st :-> (fields ++ st)
 deconstruct =
   I (instrDeconstruct @dt @(ToTs fields))
-    \\ totsKnownLemma @fields
-    \\ totsAppendLemma @fields @st
 
 -- | Lift an instruction to field constructor.
 fieldCtor :: HasCallStack => (st :-> f : st) -> FieldConstructor st f
@@ -268,6 +342,9 @@
   FI _ -> error "Field constructor always fails"
 
 -- | Wrap entry in constructor. Useful for sum types.
+--
+-- >>> wrap_ @TestSum #cTestSumB -$ (False, ())
+-- TestSumB (False,())
 wrap_
   :: forall dt name st.
      InstrWrapC dt name
@@ -277,6 +354,9 @@
     Dict -> I . instrWrap @dt
 
 -- | Wrap entry in single-field constructor. Useful for sum types.
+--
+-- >>> wrapOne @TestSum #cTestSumA -$ 42
+-- TestSumA 42
 wrapOne
   :: forall dt name st.
      InstrWrapOneC dt name
@@ -311,6 +391,18 @@
 --
 -- You have to provide a 'Rec' containing case branches.
 -- To construct a case branch use '/->' operator.
+--
+-- >>> :{
+--  let caseTestSum = case_ @TestSum $
+--        (#cTestSumA /-> nop) :&
+--        (#cTestSumB /-> L.drop # push 23) :&
+--        RNil
+-- :}
+--
+-- >>> caseTestSum -$ TestSumA 42
+-- 42
+-- >>> caseTestSum -$ TestSumB (False, ())
+-- 23
 case_
   :: forall dt out inp.
      ( InstrCaseC dt
@@ -333,6 +425,18 @@
 -- this function, he should take look at "Morley.Util.TypeTuple.Instances" and ensure
 -- that his tuple isn't bigger than generated instances, if so, he should probably
 -- extend number of generated instances.
+--
+-- >>> :{
+--  let caseTTestSum = caseT @TestSum $
+--        ( #cTestSumA /-> nop
+--        , #cTestSumB /-> L.drop # push 23
+--        )
+-- :}
+--
+-- >>> caseTTestSum -$ TestSumA 42
+-- 42
+-- >>> caseTTestSum -$ TestSumB (False, ())
+-- 23
 caseT
   :: forall dt out inp clauses.
      CaseTC dt out inp clauses
@@ -347,6 +451,11 @@
   )
 
 -- | Unwrap a constructor with the given name. Useful for sum types.
+--
+-- >>> unsafeUnwrap_ @TestSum #cTestSumA -$? TestSumA 42
+-- Right 42
+-- >>> first pretty $ unsafeUnwrap_ @TestSum #cTestSumA -$? TestSumB (False, ())
+-- Left "Reached FAILWITH instruction with \"BadCtor\" at Error occurred on line 1 char 1."
 unsafeUnwrap_
   :: forall dt name st.
      InstrUnwrapC dt name
diff --git a/src/Lorentz/Address.hs b/src/Lorentz/Address.hs
--- a/src/Lorentz/Address.hs
+++ b/src/Lorentz/Address.hs
@@ -63,6 +63,7 @@
 import Morley.Michelson.Typed qualified as M
 import Morley.Michelson.Typed.Entrypoints (EpAddress(..))
 import Morley.Tezos.Address
+import Morley.Util.Constrained
 import Morley.Util.Type
 import Morley.Util.TypeLits
 
@@ -98,7 +99,6 @@
   -> Ep.EntrypointRef mname
   -> ContractRef (Ep.GetEntrypointArgCustom cp mname)
 callingAddress (toTAddress @cp @vd -> TAddress addr) epRef =
-  withDict (niceParameterEvi @cp) $
   case Ep.parameterEntrypointCallCustom @cp epRef of
     epc@M.EntrypointCall{} -> ContractRef addr (M.SomeEpc epc)
 
@@ -157,7 +157,7 @@
   toAddress = id
 
 instance ToAddress L1Address where
-  toAddress (MkConstrainedAddress x) = MkAddress x
+  toAddress = foldConstrained MkAddress
 
 instance ToAddress (KindedAddress kind) where
   toAddress = MkAddress
@@ -189,7 +189,7 @@
   toTAddress = TAddress . MkAddress
 
 instance ToTAddress cp vd L1Address where
-  toTAddress (MkConstrainedAddress x) = TAddress $ MkAddress x
+  toTAddress = foldConstrained $ TAddress . MkAddress
 
 instance (cp ~ cp', vd ~ vd') => ToTAddress cp vd (TAddress cp' vd') where
   toTAddress = id
diff --git a/src/Lorentz/Base.hs b/src/Lorentz/Base.hs
--- a/src/Lorentz/Base.hs
+++ b/src/Lorentz/Base.hs
@@ -35,9 +35,12 @@
   , Fn
   ) where
 
+import Data.Constraint (Bottom(..))
 import Data.Default (def)
 import Fmt (Buildable(..))
+import Type.Errors (DelayError, ErrorMessage(..))
 
+import Lorentz.Annotation (HasAnnotation(..))
 import Lorentz.Constraints
 import Morley.Micheline (ToExpression(..))
 import Morley.Michelson.Optimizer (OptimizerConf, optimizeWithConf)
@@ -45,10 +48,10 @@
 import Morley.Michelson.Preprocess (transformBytes, transformStrings)
 import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDocExtended)
 import Morley.Michelson.Text (MText)
-import Morley.Michelson.TypeCheck (TCError, typeCheckValue, typeCheckingWith)
+import Morley.Michelson.TypeCheck (TcError, typeCheckValue, typeCheckingWith)
 import Morley.Michelson.Typed
-  (Instr(..), IsNotInView, IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, rfAnyInstr,
-  rfMapAnyInstr, rfMerge)
+  (Instr(..), IsNotInView, IsoValue(..), Operation, RemFail(..), ToT, ToTs, Value, WellTyped,
+  rfAnyInstr, rfMapAnyInstr, rfMerge)
 import Morley.Michelson.Typed qualified as M (Contract)
 import Morley.Michelson.Typed.Contract (giveNotInView)
 import Morley.Michelson.Untyped qualified as U
@@ -81,6 +84,56 @@
 
 {-# COMPLETE I, FI #-}
 
+{- | Essentially, a compatibility notice. Constructing a value from code
+directly isn't possible any more.
+
+>>> :set -XQualifiedDo
+>>> import Lorentz
+>>> import Prelude ()
+>>> :{
+some_code :: KnownValue a => s :-> Lambda a () : s
+some_code = Lorentz.do
+  push Lorentz.do
+    drop
+    unit
+:}
+...
+... Since the introduction of recursive lambdas in the Lima protocol,
+... Lorentz code (:->) is no longer isomorphic to lambdas.
+... Construct a lambda value explicitly using mkLambda or mkLambdaRec.
+...
+
+>>> :{
+some_code :: KnownValue a => s :-> Lambda a () : s
+some_code = Lorentz.do
+  push $ mkLambda Lorentz.do
+    drop
+    unit
+:}
+-}
+type NoLambdaCodeIsomorphismError :: Constraint
+type NoLambdaCodeIsomorphismError =
+  ( Bottom
+  , DelayError
+      ( 'Text "Since the introduction of recursive lambdas in the Lima protocol,"
+      ':$$: 'Text "Lorentz code (:->) is no longer isomorphic to lambdas."
+      ':$$: 'Text "Construct a lambda value explicitly using mkLambda or mkLambdaRec."
+      )
+  )
+
+-- | An always-stuck type family to stub 'ToT' for lorentz code 'IsoValue'
+-- instance.
+type family LorentzCodeIsNotIsomorphicToMichelsonValues :: k where {}
+
+instance (NoLambdaCodeIsomorphismError, WellTyped LorentzCodeIsNotIsomorphicToMichelsonValues)
+  => IsoValue (inp :-> out) where
+  type ToT (inp :-> out) = LorentzCodeIsNotIsomorphicToMichelsonValues
+  toVal = no
+  fromVal = no
+
+instance NoLambdaCodeIsomorphismError => HasAnnotation (i :-> o) where
+  getAnnotation = no
+
 iGenericIf
   :: (forall s'. Instr (ToTs a) s' -> Instr (ToTs b) s' -> Instr (ToTs c) s')
   -> (a :-> s) -> (b :-> s) -> (c :-> s)
@@ -192,7 +245,7 @@
 -- | Errors that can happen during parsing into a Lorentz value.
 data ParseLorentzError
   = ParseLorentzParseError ParserException
-  | ParseLorentzTypecheckError TCError
+  | ParseLorentzTypecheckError TcError
   deriving stock (Show, Eq)
 
 instance Buildable ParseLorentzError where
diff --git a/src/Lorentz/Bytes.hs b/src/Lorentz/Bytes.hs
--- a/src/Lorentz/Bytes.hs
+++ b/src/Lorentz/Bytes.hs
@@ -1,6 +1,8 @@
 -- SPDX-FileCopyrightText: 2021 Oxhead Alpha
 -- SPDX-License-Identifier: LicenseRef-MIT-OA
 
+{-# OPTIONS_GHC -Wno-deprecations #-} -- due to temporary OPEN_CHEST deprecation
+
 {-# LANGUAGE NoPolyKinds #-}
 
 -- | Type-safe operations with @bytes@-like data.
@@ -288,3 +290,7 @@
 
 openChestT :: BytesLike a => ChestKey : ChestT a : Natural : s :-> OpenChestT a : s
 openChestT = I T.OPEN_CHEST
+
+{-# DEPRECATED openChestT
+  "Due to a vulnerability discovered in time-lock protocol, \
+  \OPEN_CHEST is temporarily deprecated since Lima" #-}
diff --git a/src/Lorentz/Coercions.hs b/src/Lorentz/Coercions.hs
--- a/src/Lorentz/Coercions.hs
+++ b/src/Lorentz/Coercions.hs
@@ -42,14 +42,12 @@
 import Lorentz.Address
 import Lorentz.Base
 import Lorentz.Bytes
-import Lorentz.Lambda
 import Lorentz.Value
 import Lorentz.Wrappable
 import Lorentz.Zip
 import Morley.Michelson.Typed
 import Morley.Util.Named
 
-
 ----------------------------------------------------------------------------
 -- Unsafe coercions
 ----------------------------------------------------------------------------
@@ -240,11 +238,6 @@
 
 instance (CanCastTo a1 a2, CanCastTo b1 b2)
   => CanCastTo (ZippedStackRepr a1 b1) (ZippedStackRepr a2 b2) where
-  castDummy = castDummyG
-
-instance ( CanCastTo (ZippedStack inp1) (ZippedStack inp2)
-         , CanCastTo (ZippedStack out1) (ZippedStack out2) )
-  => WrappedLambda inp1 out1 `CanCastTo` WrappedLambda inp2 out2 where
   castDummy = castDummyG
 
 {- Note about potential use of 'Coercible'.
diff --git a/src/Lorentz/Constraints/Scopes.hs b/src/Lorentz/Constraints/Scopes.hs
--- a/src/Lorentz/Constraints/Scopes.hs
+++ b/src/Lorentz/Constraints/Scopes.hs
@@ -42,8 +42,6 @@
     withDict
   ) where
 
-import Data.Constraint (evidence, trans, weaken1)
-
 import Lorentz.Annotation (HasAnnotation)
 import Morley.Michelson.Typed
 
@@ -97,34 +95,31 @@
 
 type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n))
 
+{-# DEPRECATED niceParameterEvi, niceStorageEvi, niceConstantEvi, dupableEvi
+  , nicePackedValueEvi, niceUnpackedValueEvi, niceUntypedValueEvi
+  , niceViewableEvi
+  "This is no longer needed; the constraint implication is now trivial."
+ #-}
 niceParameterEvi :: forall a. NiceParameter a :- ParameterScope (ToT a)
-niceParameterEvi =
-  properParameterEvi @(ToT a) `trans` weaken1
+niceParameterEvi = Sub Dict
 
 niceStorageEvi :: forall a. NiceStorage a :- StorageScope (ToT a)
-niceStorageEvi =
-  Sub (evidence $ properStorageEvi @(ToT a))
+niceStorageEvi = Sub Dict
 
 niceConstantEvi :: forall a. NiceConstant a :- ConstantScope (ToT a)
-niceConstantEvi =
-  properConstantEvi @(ToT a) `trans` weaken1
+niceConstantEvi = Sub Dict
 
 dupableEvi :: forall a. Dupable a :- DupableScope (ToT a)
-dupableEvi =
-  properDupableEvi @(ToT a) `trans` weaken1
+dupableEvi = Sub Dict
 
 nicePackedValueEvi :: forall a. NicePackedValue a :- PackedValScope (ToT a)
-nicePackedValueEvi =
-  properPackedValEvi @(ToT a) `trans` weaken1
+nicePackedValueEvi = Sub Dict
 
 niceUnpackedValueEvi :: forall a. NiceUnpackedValue a :- UnpackedValScope (ToT a)
-niceUnpackedValueEvi =
-  properUnpackedValEvi @(ToT a) `trans` weaken1
+niceUnpackedValueEvi = Sub Dict
 
 niceUntypedValueEvi :: forall a. NiceUntypedValue a :- UntypedValScope (ToT a)
-niceUntypedValueEvi =
-  properUntypedValEvi @(ToT a) `trans` weaken1
+niceUntypedValueEvi = Sub Dict
 
 niceViewableEvi :: forall a. NiceViewable a :- ViewableScope (ToT a)
-niceViewableEvi =
-  properViewableEvi @(ToT a) `trans` weaken1
+niceViewableEvi = Sub Dict
diff --git a/src/Lorentz/ContractRegistry.hs b/src/Lorentz/ContractRegistry.hs
--- a/src/Lorentz/ContractRegistry.hs
+++ b/src/Lorentz/ContractRegistry.hs
@@ -22,7 +22,6 @@
 
 import Data.Aeson.Encode.Pretty (encodePretty, encodePrettyToTextBuilder)
 import Data.ByteString.Lazy.Char8 qualified as BS (putStrLn)
-import Data.Constraint ((\\))
 import Data.Map qualified as Map
 import Data.Text.Lazy.Builder (toLazyText)
 import Data.Text.Lazy.IO.Utf8 qualified as Utf8 (writeFile)
@@ -176,7 +175,7 @@
         (PrintStorage . SomeNiceStorage <$> storageParser <*> michelineOption)
         ("Print initial storage for the contract '" <> name <> "'")
 
-    -- | This will generated `storage` command instead of `storage-<contractName>` commands
+    -- This will generated `storage` command instead of `storage-<contractName>` commands
     -- Useful when there is exactly one contract.
     storageSubCmdSingle ::
       (Text, ContractInfo) -> Maybe $ Opt.Mod Opt.CommandFields CmdLnArgs
@@ -213,7 +212,7 @@
     else putStrLn $ printLorentzValue True storage
   where
     toExpressionHelper :: forall st'. NiceStorage st' => st' -> Expression
-    toExpressionHelper = toExpression . toVal \\ niceStorageEvi @st'
+    toExpressionHelper = toExpression . toVal
 
 writeFunc :: FilePath -> Maybe FilePath -> LText -> IO ()
 writeFunc defName = \case
diff --git a/src/Lorentz/CustomArith/Conversions.hs b/src/Lorentz/CustomArith/Conversions.hs
--- a/src/Lorentz/CustomArith/Conversions.hs
+++ b/src/Lorentz/CustomArith/Conversions.hs
@@ -5,7 +5,6 @@
 {-# LANGUAGE RebindableSyntax #-}
 {-# LANGUAGE NoApplicativeDo #-}
 {-# OPTIONS_GHC -Wno-unused-do-bind #-}
-{-# OPTIONS_GHC -Wno-orphans #-}
 
 module Lorentz.CustomArith.Conversions
  ( -- * Rational to Fixed/NFixed
@@ -34,7 +33,7 @@
 import Lorentz.Errors
 import Lorentz.Instr
 import Lorentz.Macro
-import Lorentz.Rebinded
+import Lorentz.Rebound
 
 convertRationalToNRational :: Rational : s :-> Maybe (NRational) : s
 convertRationalToNRational = do
diff --git a/src/Lorentz/CustomArith/FixedArith.hs b/src/Lorentz/CustomArith/FixedArith.hs
--- a/src/Lorentz/CustomArith/FixedArith.hs
+++ b/src/Lorentz/CustomArith/FixedArith.hs
@@ -277,7 +277,7 @@
 roundingHelper
   :: forall a b r1 r2 s.
     ( KnownNat a, KnownNat b
-    , FailOnTicketFound (ContainsTicket (ToT (Unwrappabled r1)))
+    , ForbidTicket (ToT (Unwrappabled r1))
     , MichelsonCoercible r1 r2
     , Typeable (Unwrappabled r2)
     , IsoValue (Unwrappabled r2)
diff --git a/src/Lorentz/CustomArith/RationalArith.hs b/src/Lorentz/CustomArith/RationalArith.hs
--- a/src/Lorentz/CustomArith/RationalArith.hs
+++ b/src/Lorentz/CustomArith/RationalArith.hs
@@ -52,7 +52,7 @@
 import Lorentz.Errors
 import Lorentz.Instr
 import Lorentz.Macro
-import Lorentz.Rebinded
+import Lorentz.Rebound
 import Morley.Michelson.Text
 import Morley.Michelson.Typed
 import Morley.Util.Named
@@ -342,7 +342,7 @@
 -- This operation should be commonly used after several arithmetic operations, because
 -- numerator and denominator can become quite big. That in order, can lead to serious
 -- gas consumption.
-reduceRationalHelper :: (KnownList s, KnownList (ToTs s)) => Rational : s :-> Rational : s
+reduceRationalHelper :: Rational : s :-> Rational : s
 reduceRationalHelper = do
   deconstructRational
   dup; ifLt0 (push (-1 :: Integer)) (push (1 :: Integer)); dug @2; abs;
@@ -365,7 +365,7 @@
 
 -- | Reduce 'Rational' value, using extended Euclid algorithm.
 -- Consumes slightly more gas, than @reduce@, but contract with it is cheaper in terms of origination.
-euclidExtendedNormalization :: forall s. (KnownList s, KnownList (ToTs s)) => Rational : s :-> Rational : s
+euclidExtendedNormalization :: forall s. Rational : s :-> Rational : s
 euclidExtendedNormalization = do
   deconstructRational; dip int
   dipN @2 do
diff --git a/src/Lorentz/Doc.hs b/src/Lorentz/Doc.hs
--- a/src/Lorentz/Doc.hs
+++ b/src/Lorentz/Doc.hs
@@ -82,23 +82,19 @@
   , mdTocFromRef
   ) where
 
-import Data.Singletons (demote)
 import Data.Typeable (typeRep)
 import Fmt (Buildable(..), Builder, pretty)
 
 import Lorentz.Base
 import Lorentz.Constraints
-import Lorentz.Lambda
 import Lorentz.Value
 import Lorentz.ViewBase
-import Lorentz.Zip ()
 import Morley.Michelson.Doc
 import Morley.Michelson.Optimizer
 import Morley.Michelson.Printer
 import Morley.Michelson.Typed hiding (Contract, ContractCode, ContractCode'(..))
 import Morley.Util.Generic
 import Morley.Util.Markdown
-import Morley.Util.Type
 import Morley.Util.TypeLits
 
 -- | Put a document item.
@@ -152,46 +148,6 @@
 cutLorentzNonDoc :: (inp :-> out) -> (s :-> s)
 cutLorentzNonDoc (iAnyCode -> code) = I $ cutInstrNonDoc optimize code
 
-instance Each [Typeable, ReifyList TypeHasDoc] [i, o] => TypeHasDoc (WrappedLambda i o) where
-  typeDocName _ = "WrappedLambda (extended lambda)"
-  typeDocMdReference tp wp =
-    let DocItemRef ctorDocItemId = docItemRef (DType tp)
-        refToThis = mdLocalRef (mdTicked "WrappedLambda") ctorDocItemId
-    in applyWithinParens wp $
-      mconcat $ intersperse " " [refToThis, refToStack @i, refToStack @o]
-    where
-    refToStack :: forall s. ReifyList TypeHasDoc s => Markdown
-    refToStack =
-      let stack = reifyList @_ @TypeHasDoc @s (\p -> typeDocMdReference p (WithinParens False))
-      in mconcat
-          [ mdBold "["
-          , case stack of
-              [] -> " "
-              st -> mconcat $ intersperse (mdBold "," <> " ") st
-          , mdBold "]"
-          ]
-
-  typeDocMdDescription =
-    "`WrappedLambda i o` stands for a sequence of instructions which accepts stack \
-    \of type `i` and returns stack of type `o`.\n\n\
-    \When both `i` and `o` are of length 1, this primitive corresponds to \
-    \the Michelson lambda. In more complex cases code is surrounded with `pair`\
-    \and `unpair` instructions until fits into mentioned restriction.\
-    \"
-  typeDocDependencies _ = mconcat
-    [ reifyList @_ @TypeHasDoc @i dTypeDepP
-    , reifyList @_ @TypeHasDoc @o dTypeDepP
-    , [ dTypeDep @Integer
-      , dTypeDep @Natural
-      , dTypeDep @MText
-      ]
-    ]
-  typeDocHaskellRep _ _ = Nothing
-  typeDocMichelsonRep _ =
-    ( Just "Code [Integer, Natural, MText, ()] [ByteString]"
-    , demote @(ToT ([Integer, Natural, MText, ()] :-> '[ByteString]))
-    )
-
 instance (TypeHasDoc p, ViewsDescriptorHasDoc vd) => TypeHasDoc (TAddress p vd) where
   typeDocMdDescription = [md|
     A typed version of address primitive.
@@ -240,9 +196,7 @@
     build $ printUntypedValue True $ untypeValue val
 
 mkDEntrypointExample :: forall a. NiceParameter a => a -> DEntrypointExample
-mkDEntrypointExample v =
-  withDict (niceParameterEvi @a) $
-    DEntrypointExample $ toVal v
+mkDEntrypointExample v = DEntrypointExample $ toVal v
 
 ----------------------------------------------------------------------------
 -- Views documentation
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
@@ -45,13 +45,13 @@
   , RequireAllUniqueEntrypoints'
   ) where
 
-import Data.Constraint ((\\))
 import Data.Typeable (typeRep)
 import Data.Vinyl (Rec(..))
 import Fcf (Eval, Exp)
 import Fcf qualified
 import Fcf.Utils qualified as Fcf
 import Fmt (pretty)
+import Type.Errors (DelayError, DelayErrorFcf, IfStuck)
 
 import Morley.Michelson.Typed
 import Morley.Michelson.Untyped qualified as U
@@ -279,7 +279,6 @@
   => Label name
   -> EntrypointCall cp (GetEntrypointArg cp name)
 parameterEntrypointCall label@Label =
-  withDict (niceParameterEvi @cp) $
   case pepCall @cp label of
     EpConstructed liftSeq -> EntrypointCall
       { epcName = ctorNameToEp @name
@@ -307,7 +306,6 @@
      (ParameterDeclaresEntrypoints cp)
   => EntrypointCall cp (GetDefaultEntrypointArg cp)
 parameterEntrypointCallDefault =
-  withDict (niceParameterEvi @cp) $
   case pepCall @cp (fromLabel @DefaultEpName) of
     EpConstructed liftSeq -> EntrypointCall
       { epcName = DefEpName
@@ -352,7 +350,7 @@
   :: forall cp.
      (NiceParameter cp, ForbidExplicitDefaultEntrypoint cp)
   => SomeEntrypointCall cp
-sepcCallRootChecked = unsafeSepcCallRoot \\ niceParameterEvi @cp
+sepcCallRootChecked = unsafeSepcCallRoot
   where
     -- Avoiding redundant-constraints warning.
     _validUsage = Dict @(ForbidExplicitDefaultEntrypoint cp)
@@ -410,26 +408,57 @@
 -- Type class for functions that take entrypoint name as argument
 ----------------------------------------------------------------------------
 
--- | When we call a Lorentz contract we should pass entrypoint name
--- and corresponding argument. Ideally we want to statically check
--- that parameter has entrypoint with given name and
--- argument. Constraint defined by this type class holds for contract
--- with parameter @cp@ that have entrypoint matching @name@ with type
--- @arg@.
---
--- In order to check this property statically, we need to know entrypoint
--- name in compile time, 'EntrypointRef' type serves this purpose.
--- If entrypoint name is not known, one can use 'TrustEpName' wrapper
--- to take responsibility for presence of this entrypoint.
---
--- If you want to call a function which has this constraint, you have
--- two options:
--- 1. Pass contract parameter @cp@ using type application, pass 'EntrypointRef'
--- as a value and pass entrypoint argument. Type system will check that
--- @cp@ has an entrypoint with given reference and type.
--- 2. Pass 'EpName' wrapped into 'TrustEpName' and entrypoint argument.
--- In this case passing contract parameter is not necessary, you do not even
--- have to know it.
+{- | When we call a Lorentz contract we should pass entrypoint name and
+corresponding argument. Ideally we want to statically check that parameter has
+entrypoint with given name and argument. Constraint defined by this type class
+holds for contract with parameter @cp@ that have entrypoint matching @name@ with
+type @arg@.
+
+In order to check this property statically, we need to know entrypoint name in
+compile time, 'EntrypointRef' type serves this purpose. If entrypoint name is
+not known, one can use 'TrustEpName' wrapper to take responsibility for presence
+of this entrypoint.
+
+If you want to call a function which has this constraint, you have two options:
+
+1. Pass contract parameter @cp@ using type application, pass 'EntrypointRef' as
+a value and pass entrypoint argument. Type system will check that @cp@ has an
+entrypoint with given reference and type.
+
+2. Pass 'EpName' wrapped into 'TrustEpName' and entrypoint argument. In this
+case passing contract parameter is not necessary, you do not even have to know
+it.
+
+You may need to add this constraint for polymorphic arguments. GHC should tell
+you when that is the case:
+
+>>> :{
+f :: forall (cp :: Type). ParameterDeclaresEntrypoints cp => ()
+f = useHasEntrypointArg @cp @_ @(Maybe Integer) CallDefault & const ()
+:}
+...
+... Can not look up entrypoints in type
+...   cp
+... The most likely reason it is ambiguous, or you need
+...   HasEntrypointArg cp (EntrypointRef 'Nothing) (Maybe Integer)
+... constraint
+...
+
+If GHC can't deduce the type of entrypoint argument, it'll use an unbound type
+variable, usually @arg0@, in the error message:
+
+>>> :{
+f :: forall (cp :: Type). ParameterDeclaresEntrypoints cp => ()
+f = useHasEntrypointArg @cp CallDefault & const ()
+:}
+...
+... Can not look up entrypoints in type
+...   cp
+... The most likely reason it is ambiguous, or you need
+...   HasEntrypointArg cp (EntrypointRef 'Nothing) arg0
+... constraint
+...
+-}
 class HasEntrypointArg cp name arg where
   -- | Data returned by this method may look somewhat arbitrary.
   -- 'EpName' is obviously needed because @name@ can be
@@ -444,11 +473,37 @@
   , HasEntrypointArg cp defEpName defArg
   )
 
+type StuckEpErrorTemplate cp constraint =
+  'Text "Can not look up entrypoints in type" ':$$:
+  'Text "  " ':<>: 'ShowType cp ':$$:
+  'Text "The most likely reason it is ambiguous, or you need" ':$$:
+  'Text "  " ':<>: 'ShowType constraint ':$$:
+  'Text "constraint"
+
+type CheckStuckEp cp mname fixedArg freeArg =
+  -- NB: if you're wondering why we need @freeArg@ and @fixedArg@, when
+  -- @fixedArg@ is fully polymorphic, GHC will assign it to the stuck type
+  -- family, and @ShowType@ will show FCF internals, which is exactly what we
+  -- wanted to avoid. Hence if @fixedArg@ is also stuck, we show @freeArg@
+  -- instead. Finally, when there are no errors, we equate @freeArg@ and
+  -- @fixedArg@.
+  IfStuck (GetEntrypointArgCustom cp mname)
+    (IfStuck fixedArg
+      (DelayError (StuckEpErrorTemplate cp
+        (HasEntrypointArg cp (EntrypointRef mname) freeArg)
+      ))
+      (DelayErrorFcf (StuckEpErrorTemplate cp
+        (HasEntrypointArg cp (EntrypointRef mname) fixedArg)
+      ))
+    )
+    (Fcf.Pure (freeArg ~ fixedArg))
+
 instance
-  (GetEntrypointArgCustom cp mname ~ arg, ParameterDeclaresEntrypoints cp) =>
-  HasEntrypointArg cp (EntrypointRef mname) arg where
+  ( CheckStuckEp cp mname arg' arg
+  , GetEntrypointArgCustom cp mname ~ arg'
+  , ParameterDeclaresEntrypoints cp) =>
+  HasEntrypointArg cp (EntrypointRef mname) arg' where
   useHasEntrypointArg epRef =
-    withDict (niceParameterEvi @cp) $
     case parameterEntrypointCallCustom @cp epRef of
       EntrypointCall{} -> (Dict, eprName epRef)
 
@@ -458,7 +513,7 @@
 
 instance (NiceParameter arg) =>
   HasEntrypointArg cp TrustEpName arg where
-  useHasEntrypointArg (TrustEpName epName) = (Dict, epName) \\ niceParameterEvi @arg
+  useHasEntrypointArg (TrustEpName epName) = (Dict, epName)
 
 -- | Checks that the given parameter consists of some specific entrypoint. Similar as
 -- `HasEntrypointArg` but ensures that the argument matches the following datatype.
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
@@ -53,7 +53,7 @@
 import Data.Map qualified as Map
 import Data.Singletons (fromSing)
 import Data.Text qualified as T
-import Data.Vinyl.Core (RMap, rappend)
+import Data.Vinyl.Core (RMap)
 import Fcf (IsJust, type (@@))
 import Fmt (Buildable(..), build, fmt, listF)
 import GHC.Generics ((:+:))
@@ -115,7 +115,7 @@
     filterDEntrypointExample (SubDoc subdoc) =
       SubDoc $ Map.delete (docItemPosition @DEntrypointExample) subdoc
 
-    -- | Modify 'SubDoc' of an entrypoint to replace its example value with the one defined in
+    -- Modify 'SubDoc' of an entrypoint to replace its example value with the one defined in
     -- 'DEntrypointExample' in an ad-hoc way.
     modifyExample :: SubDoc -> Markdown -> Markdown
     modifyExample (SubDoc sub) subDocMd =
@@ -488,44 +488,51 @@
      DocumentEntrypoints kind a
   => Rec (CaseClauseL inp out) (CaseClauses a)
   -> Rec (CaseClauseL inp out) (CaseClauses a)
-documentEntrypoints =
-  gDocumentEntrypoints @(BuildEPTree' a) @kind @(G.Rep a) $
-    ParamBuilder id
+documentEntrypoints r =
+  gDocumentEntrypoints @(BuildEPTree' a) @kind @(G.Rep a) @'[]
+    (ParamBuilder id) r (\RNil -> RNil)
 
 -- | Constraint for 'documentEntrypoints'.
 type DocumentEntrypoints kind a =
-  (Generic a, GDocumentEntrypoints (BuildEPTree' a) kind (G.Rep a))
+  (Generic a, GDocumentEntrypoints (BuildEPTree' a) kind (G.Rep a) '[])
 
 type BuildEPTree' a = BuildEPTree (GetParameterEpDerivation a) a
 
 -- | 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 (ept :: EPTree) (kind :: Type) (x :: Type -> Type) where
+class GDocumentEntrypoints
+  (ept :: EPTree)
+  (kind :: Type)
+  (x :: Type -> Type)
+  (rest :: [CaseClauseParam]) where
   -- | Add corresponding parameter building step.
   --
-  -- First argument is accumulator for Michelson description of the building step.
+  -- The first argument is accumulator for Michelson description of the
+  -- building step.
+  --
+  -- The third argument is a function to which the remaining unprocessed
+  -- portion of the record will be passed.
   gDocumentEntrypoints
     :: ParamBuilder
-    -> Rec (CaseClauseL inp out) (GCaseClauses x)
-    -> Rec (CaseClauseL inp out) (GCaseClauses x)
+    -> Rec (CaseClauseL inp out) (GCaseClauses x rest)
+    -> (Rec (CaseClauseL inp out) rest -> Rec (CaseClauseL inp out) rest)
+    -> Rec (CaseClauseL inp out) (GCaseClauses x rest)
 
-instance GDocumentEntrypoints ept kind x => GDocumentEntrypoints ept kind (G.D1 i x) where
-  gDocumentEntrypoints = gDocumentEntrypoints @ept @kind @x
+instance GDocumentEntrypoints ept kind x rest =>
+         GDocumentEntrypoints ept kind (G.D1 i x) rest where
+  gDocumentEntrypoints = gDocumentEntrypoints @ept @kind @x @rest
 
-instance ( GDocumentEntrypoints eptl kind x, GDocumentEntrypoints eptr kind y
-         , RSplit (GCaseClauses x) (GCaseClauses y)
+instance ( GDocumentEntrypoints eptl kind x (GCaseClauses y rest)
+         , GDocumentEntrypoints eptr kind y rest
          ) =>
-         GDocumentEntrypoints ('EPNode eptl eptr) kind (x :+: y) where
-  gDocumentEntrypoints (ParamBuilder michDesc) clauses =
-    let (lclauses, rclauses) = rsplit @CaseClauseParam @(GCaseClauses x) clauses
-    in gDocumentEntrypoints @eptl @kind @x
-         (ParamBuilder $ \a -> michDesc $ "Left (" <> a <> ")")
-         lclauses
-       `rappend`
-       gDocumentEntrypoints @eptr @kind @y
-         (ParamBuilder $ \a -> michDesc $ "Right (" <> a <> ")")
-         rclauses
+         GDocumentEntrypoints ('EPNode eptl eptr) kind (x :+: y) rest where
+  gDocumentEntrypoints (ParamBuilder michDesc) clauses cont =
+    gDocumentEntrypoints @eptl @kind @x lpb clauses
+      (\clauses' -> gDocumentEntrypoints @eptr @kind @y @rest rpb clauses' cont)
+    where
+      lpb = ParamBuilder $ \a -> michDesc $ "Left (" <> a <> ")"
+      rpb = ParamBuilder $ \a -> michDesc $ "Right (" <> a <> ")"
 
 instance {-# OVERLAPPABLE #-}
          ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
@@ -533,25 +540,25 @@
          , DocItem (DEntrypoint (EntrypointKindOverride kind))
          , DeriveCtorFieldDoc ctor cf
          ) =>
-         GDocumentEntrypoints ept kind (G.C1 ('G.MetaCons ctor _1 _2) x) where
-  gDocumentEntrypoints michDesc (CaseClauseL clause :& RNil) =
+         GDocumentEntrypoints ept kind (G.C1 ('G.MetaCons ctor _1 _2) x) rest where
+  gDocumentEntrypoints michDesc (CaseClauseL clause :& rest) cont =
     let entrypointName = toText $ symbolVal (Proxy @ctor)
         psteps = mkPbsWrapIn entrypointName michDesc
         addDoc instr =
           clarifyParamBuildingSteps psteps $
           docGroup (DEntrypoint @(EntrypointKindOverride kind) entrypointName) $
           doc (deriveCtorFieldDoc @ctor @cf) # instr
-    in CaseClauseL (addDoc clause) :& RNil
+    in CaseClauseL (addDoc clause) :& cont rest
 
 instance ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
          , KnownSymbol ctor
          ) =>
          GDocumentEntrypoints ('EPNode a b) (FlattenedEntrypointsKindHiding _heps)
-            (G.C1 ('G.MetaCons ctor _1 _2) x) where
-  gDocumentEntrypoints michDesc (CaseClauseL clause :& RNil) =
+            (G.C1 ('G.MetaCons ctor _1 _2) x) rest where
+  gDocumentEntrypoints michDesc (CaseClauseL clause :& rest) cont =
     let entrypointName = toText $ symbolVal (Proxy @ctor)
         psteps = mkPbsWrapIn entrypointName michDesc
-    in CaseClauseL (clarifyParamBuildingSteps psteps clause) :& RNil
+    in CaseClauseL (clarifyParamBuildingSteps psteps clause) :& cont rest
 
 instance {-# OVERLAPPABLE #-}
          ( 'CaseClauseParam ctor cf ~ GCaseBranchInput ctor x
@@ -560,8 +567,8 @@
          , T.SingI heps
          ) =>
          GDocumentEntrypoints ept (FlattenedEntrypointsKindHiding heps)
-            (G.C1 ('G.MetaCons ctor _1 _2) x) where
-  gDocumentEntrypoints michDesc (CaseClauseL clause :& RNil) =
+            (G.C1 ('G.MetaCons ctor _1 _2) x) rest where
+  gDocumentEntrypoints michDesc (CaseClauseL clause :& rest) cont =
     let epName = toText $ symbolVal (Proxy @ctor)
         psteps = mkPbsWrapIn epName michDesc
         hiddenEps = fromSing $ T.sing @heps
@@ -574,7 +581,7 @@
         addDoc instr =
           clarifyParamBuildingSteps psteps $
             epDoc instr
-    in CaseClauseL (addDoc clause) :& RNil
+    in CaseClauseL (addDoc clause) :& cont rest
 
 -- | Like 'case_', to be used for pattern-matching on a parameter
 -- or its part.
diff --git a/src/Lorentz/Errors.hs b/src/Lorentz/Errors.hs
--- a/src/Lorentz/Errors.hs
+++ b/src/Lorentz/Errors.hs
@@ -50,6 +50,7 @@
   ) where
 
 import Data.Char qualified as C
+import Data.Constraint (Bottom(..))
 import Data.List qualified as L
 import Fmt (Buildable, build, fmt, pretty, (+|), (|+))
 import Language.Haskell.TH.Syntax (Lift)
@@ -189,15 +190,15 @@
   errorDocClass = ErrClassContractInternal
   errorDocDependencies = [SomeDocDefinitionItem (DType $ Proxy @MText)]
 
-instance TypeError ('Text "Use representative error messages") => IsError () where
-  errorToVal _ _ = error "impossible"
-  errorFromVal = error "impossible"
+instance (Bottom, TypeError ('Text "Use representative error messages")) => IsError () where
+  errorToVal _ _ = no
+  errorFromVal = no
 
-instance TypeError ('Text "Use representative error messages") => ErrorHasDoc () where
-  errorDocName = error "impossible"
-  errorDocMdCause = error "impossible"
-  errorDocHaskellRep = error "impossible"
-  errorDocDependencies = error "impossible"
+instance (Bottom, TypeError ('Text "Use representative error messages")) => ErrorHasDoc () where
+  errorDocName = no
+  errorDocMdCause = no
+  errorDocHaskellRep = no
+  errorDocDependencies = no
 
 -- | Use this type as replacement for @()@ when you __really__ want to leave
 -- error cause unspecified.
@@ -373,15 +374,15 @@
     ]
 
 -- | This instance cannot be implemented, use 'IsError' instance instead.
-instance (WellTypedToT (CustomErrorRep tag), TypeError ('Text "CustomError has no IsoValue instance")) =>
+instance (Bottom, WellTypedToT (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 (CustomErrorRep tag))
-  toVal = error "impossible"
-  fromVal = error "impossible"
+  toVal = no
+  fromVal = no
 
 instance ( CustomErrorHasDoc tag
          , KnownError (CustomErrorRep tag)
diff --git a/src/Lorentz/Expr.hs b/src/Lorentz/Expr.hs
--- a/src/Lorentz/Expr.hs
+++ b/src/Lorentz/Expr.hs
@@ -104,7 +104,7 @@
 import Lorentz.Errors
 import Lorentz.Instr
 import Lorentz.Macro
-import Lorentz.Rebinded
+import Lorentz.Rebound
 import Lorentz.Value
 import Lorentz.ViewBase
 import Morley.Michelson.Typed.Arith
diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs
--- a/src/Lorentz/Instr.hs
+++ b/src/Lorentz/Instr.hs
@@ -1,6 +1,8 @@
 -- SPDX-FileCopyrightText: 2021 Oxhead Alpha
 -- SPDX-License-Identifier: LicenseRef-MIT-OA
 
+{-# OPTIONS_GHC -Wno-deprecations #-} -- due to temporary OPEN_CHEST deprecation
+
 {-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
 
 module Lorentz.Instr
@@ -55,6 +57,7 @@
   , loop
   , loopLeft
   , lambda
+  , lambdaRec
   , exec
   , execute
   , apply
@@ -139,7 +142,6 @@
 import Prelude hiding
   (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)
 
-import Data.Constraint ((\\))
 import GHC.TypeNats (Nat)
 
 import Lorentz.Address
@@ -149,6 +151,7 @@
 import Lorentz.Bytes
 import Lorentz.Constraints
 import Lorentz.Entrypoints
+import Lorentz.Instr.Framed
 import Lorentz.Lambda
 import Lorentz.Polymorphic
 import Lorentz.Value
@@ -157,8 +160,8 @@
 import Morley.Michelson.Typed
   (ConstraintDIG, ConstraintDIG', ConstraintDIPN, ConstraintDIPN', ConstraintDUG, ConstraintDUG',
   ConstraintDUPN, ConstraintDUPN', ConstraintGetN, ConstraintUpdateN, EntrypointCallT(..), GetN,
-  Instr(..), Notes, RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, Value'(..), pattern CAR,
-  pattern CDR, pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes)
+  Instr(..), Notes, RemFail(..), SingI, SomeEntrypointCallT(..), UpdateN, pattern CAR, pattern CDR,
+  pattern LEFT, pattern PAIR, pattern RIGHT, pattern UNPAIR, sepcName, starNotes)
 import Morley.Michelson.Typed.Arith
 import Morley.Michelson.Typed.Contract (giveNotInView)
 import Morley.Michelson.Typed.Haskell.Value
@@ -208,7 +211,7 @@
 -- 3. Use 'decideOnDupable' to provide two code paths - when type is dupable
 --    and when it is not.
 dup :: forall a s. Dupable a => a : s :-> a : a : s
-dup = I DUP \\ dupableEvi @a
+dup = I DUP
 
 type ConstraintDUPNLorentz (n :: Peano) (inp :: [Type]) (out :: [Type])
   (a :: Type) =
@@ -220,7 +223,7 @@
 dupNPeano ::
   forall (n :: Peano) a inp out.
   ( ConstraintDUPNLorentz n inp out a, Dupable a ) => inp :-> out
-dupNPeano = (I $ DUPN $ toPeanoNatural @n) \\ dupableEvi @a
+dupNPeano = I $ DUPN $ toPeanoNatural @n
 
 dupN ::
   forall (n :: Nat) a inp out.
@@ -287,7 +290,7 @@
     _example = dug @3
 
 push :: forall t s . NiceConstant t => t -> (s :-> t : s)
-push a = I $ PUSH (toVal a) \\ niceConstantEvi @t
+push a = I $ PUSH (toVal a)
 
 some :: a : s :-> Maybe a : s
 some = I SOME
@@ -428,9 +431,21 @@
   :: ZipInstrs [i, o]
   => (IsNotInView => i :-> o) -> (s :-> WrappedLambda i o : s)
 lambda instr = case zippingStack $ giveNotInView instr of
-  I l -> I (LAMBDA $ VLam $ RfNormal l)
-  FI l -> I (LAMBDA $ VLam $ RfAlwaysFails l)
+  I l -> I (LAMBDA $ RfNormal l)
+  FI l -> I (LAMBDA $ RfAlwaysFails l)
 
+lambdaRec
+  :: forall i o s. (ZipInstrs [i, o], KnownList i)
+  => (IsNotInView => (i ++ '[WrappedLambda i o]) :-> o) -> (s :-> WrappedLambda i o : s)
+lambdaRec instr = case code of
+  I l -> I $ LAMBDA_REC $ RfNormal l
+  FI l -> I $ LAMBDA_REC $ RfAlwaysFails l
+  where
+    code =
+      framed @'[WrappedLambda i o] (unzipInstr @i)
+      ## giveNotInView instr
+      ## zipInstr
+
 exec :: a : Lambda a b : s :-> b : s
 exec = I EXEC
 
@@ -446,15 +461,13 @@
 execute = framed @s $
   dip (zipInstr @i) # swap # I EXEC # unzipInstr @o
   where
-    _example
-      :: (WrappedLambda [Integer, Natural] [(), ()]) : Integer : Natural : s
-      :-> () : () : s
+    _example :: (WrappedLambda [Integer, Natural] [(), ()]) : Integer : Natural : s :-> () : () : s
     _example = execute
 
 apply
   :: forall a b c s. (NiceConstant a, KnownValue b)
   => a : Lambda (a, b) c : s :-> Lambda b c : s
-apply = I $ APPLY \\ niceConstantEvi @a
+apply = I $ APPLY
 
 -- | Version of 'apply' that works for lambdas with arbitrary length
 -- input and output.
@@ -462,7 +475,7 @@
   :: forall a b c inp2nd inpTail s.
      (NiceConstant a, ZipInstr b, b ~ (inp2nd : inpTail))
   => a : WrappedLambda (a : b) c : s :-> WrappedLambda b c : s
-applicate = I APPLY \\ niceConstantEvi @a
+applicate = I APPLY
 
 dip :: forall a s s'. HasCallStack => (s :-> s') -> (a : s :-> a : s')
 dip (iNonFailingCode -> a) = I (DIP a)
@@ -504,7 +517,7 @@
 -- '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
+failWith = FI FAILWITH
 
 cast :: KnownValue a => (a : s :-> a : s)
 cast = I CAST
@@ -512,22 +525,22 @@
 pack
   :: forall a s. (NicePackedValue a)
   => a : s :-> Packed a : s
-pack = I $ PACK \\ nicePackedValueEvi @a
+pack = I $ PACK
 
 unpack
   :: forall a s. (NiceUnpackedValue a)
   => Packed a : s :-> Maybe a : s
-unpack = I $ UNPACK \\ niceUnpackedValueEvi @a
+unpack = I $ UNPACK
 
 packRaw
   :: forall a s. (NicePackedValue a)
   => a : s :-> ByteString : s
-packRaw = I $ PACK \\ nicePackedValueEvi @a
+packRaw = I $ PACK
 
 unpackRaw
   :: forall a s. (NiceUnpackedValue a)
   => ByteString : s :-> Maybe a : s
-unpackRaw = I $ UNPACK \\ niceUnpackedValueEvi @a
+unpackRaw = I $ UNPACK
 
 concat :: ConcatOpHs c => c : c : s :-> c : s
 concat = I CONCAT
@@ -642,7 +655,6 @@
     (HasCallStack, KnownSymbol name, KnownValue arg, NiceViewable ret)
   => arg : Address : s :-> Maybe ret : s
 view' = I $ VIEW (demoteViewName @name)
-  \\ niceViewableEvi @ret
 
 -- | Get a reference to the current contract.
 --
@@ -660,7 +672,7 @@
   :: forall p s.
       (NiceParameterFull p, ForbidExplicitDefaultEntrypoint p, IsNotInView)
   => s :-> ContractRef p : s
-self = I (SELF $ sepcCallRootChecked @p) \\ niceParameterEvi @p
+self = I (SELF $ sepcCallRootChecked @p)
 
 -- | Make a reference to the current contract, maybe a specific entrypoint.
 --
@@ -673,7 +685,6 @@
   => EntrypointRef mname
   -> s :-> ContractRef (GetEntrypointArgCustom p mname) : s
 selfCalling epRef = I $
-  withDict (niceParameterEvi @p) $
   case parameterEntrypointCallCustom @p epRef of
     epc@EntrypointCall{} -> SELF (SomeEpc epc)
 
@@ -690,7 +701,7 @@
       , ToTAddress_ p vd addr
       )
   => addr : s :-> Maybe (ContractRef p) : s
-contract = I (CONTRACT epName) \\ niceParameterEvi @p
+contract = I (CONTRACT epName)
   where
     epName = sepcName (sepcCallRootChecked @p)
 
@@ -737,13 +748,12 @@
 epAddressToContract
   :: forall p s. (NiceParameter p)
   => EpAddress : s :-> Maybe (ContractRef p) : s
-epAddressToContract =
-  I (CONTRACT DefEpName) \\ niceParameterEvi @p
+epAddressToContract = I (CONTRACT DefEpName)
 
 transferTokens
   :: forall p s. (NiceParameter p, IsNotInView)
   => p : Mutez : ContractRef p : s :-> Operation : s
-transferTokens = I $ TRANSFER_TOKENS \\ niceParameterEvi @p
+transferTokens = I TRANSFER_TOKENS
 
 setDelegate :: IsNotInView => Maybe KeyHash : s :-> Operation : s
 setDelegate = I SET_DELEGATE
@@ -754,9 +764,7 @@
   -> Maybe KeyHash : Mutez : g : s
   :-> Operation : TAddress p vd : s
 createContract cntrc@Contract{} =
-  I $ CREATE_CONTRACT (toMichelsonContract cntrc)
-    \\ niceParameterEvi @p
-    \\ niceStorageEvi @g
+  I (CREATE_CONTRACT (toMichelsonContract cntrc))
 
 implicitAccount :: KeyHash : s :-> ContractRef () : s
 implicitAccount = I IMPLICIT_ACCOUNT
@@ -827,7 +835,7 @@
 never :: Never : s :-> s'
 never = FI NEVER
 
-ticket :: (NiceComparable a) => a : Natural : s :-> Ticket a : s
+ticket :: (NiceComparable a) => a : Natural : s :-> Maybe (Ticket a) : s
 ticket = I TICKET
 
 -- | Note: for more advanced helpers for tickets see "Lorentz.Tickets" module.
@@ -852,6 +860,10 @@
 openChest :: ChestKey : Chest : Natural : s :-> OpenChest : s
 openChest = I OPEN_CHEST
 
+{-# DEPRECATED openChest
+  "Due to a vulnerability discovered in time-lock protocol, \
+  \OPEN_CHEST is temporarily deprecated since Lima" #-}
+
 -- | Version of 'emit' that adds the type annotation, only when @t@ has annotations.
 emit :: forall t s. (NicePackedValue t, HasAnnotation t) => FieldAnn -> t : s :-> Operation : s
 emit tag = emit' tag ann'
@@ -872,22 +884,7 @@
   => FieldAnn
   -> Maybe (Notes (ToT t))
   -> t : s :-> Operation : s
-emit' tag mNotes = I $ EMIT tag mNotes \\ nicePackedValueEvi @t
-
--- | Execute given instruction on truncated stack.
---
--- This instruction requires you to specify the piece of stack to truncate
--- as type argument.
-framed
-  :: forall s i o.
-      (KnownList i, KnownList o)
-  => (i :-> o) -> ((i ++ s) :-> (o ++ s))
-framed (iNonFailingCode -> i) =
-  I $ FrameInstr (Proxy @(ToTs s)) i
-    \\ totsKnownLemma @i
-    \\ totsKnownLemma @o
-    \\ totsAppendLemma @i @s
-    \\ totsAppendLemma @o @s
+emit' tag mNotes = I $ EMIT tag mNotes
 
 ----------------------------------------------------------------------------
 -- Non-canonical instructions
@@ -921,8 +918,26 @@
   -> k : UpdOpParamsHs c : c : s :-> c : s
 updateNew mkErr = dup # dip getAndUpdate # swap # ifNone drop (drop # mkErr # failWith)
 
-class LorentzFunctor (c :: Type -> Type) where
-  lmap :: KnownValue b => (a : s :-> b : s) -> (c a : s :-> c b : s)
+class LorentzFunctor (c :: Type -> Type) a b where
+  lmap :: KnownValue b => ('[a] :-> '[b]) -> (c a : s :-> c b : s)
 
-instance LorentzFunctor Maybe where
-  lmap = map
+instance LorentzFunctor Maybe a b where
+  lmap = framed . map
+
+instance KnownValue a => LorentzFunctor (Either a) a b where
+  lmap f = (ifLeft left (framed f # right))
+
+instance LorentzFunctor [] a b where
+  lmap = framed . map
+
+instance NiceComparable k => LorentzFunctor (Map k) a b where
+  lmap f = (map (cdr # framed f))
+
+instance (NiceComparable a, NiceComparable b) => LorentzFunctor Set a b where
+  lmap f = dip emptySet # iter body
+    where
+      body :: a : Set b : s :-> Set b : s
+      body =
+        framed f #
+        dip (push True) #
+        update
diff --git a/src/Lorentz/Instr/Framed.hs b/src/Lorentz/Instr/Framed.hs
new file mode 100644
--- /dev/null
+++ b/src/Lorentz/Instr/Framed.hs
@@ -0,0 +1,33 @@
+-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
+-- SPDX-License-Identifier: LicenseRef-MIT-OA
+
+{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
+{-# OPTIONS_HADDOCK not-home #-}
+
+-- | This module is introduced to break some cycles in "Lorentz.Lambda"
+module Lorentz.Instr.Framed
+  ( framed
+  ) where
+
+import Prelude hiding
+  (EQ, GT, LT, abs, and, compare, concat, drop, get, map, not, or, some, swap, xor)
+
+import Data.Constraint ((\\))
+
+import Lorentz.Base
+import Morley.Michelson.Typed hiding (Contract, pattern S)
+import Morley.Util.Type
+
+-- | Execute given instruction on truncated stack.
+--
+-- This instruction requires you to specify the piece of stack to truncate
+-- as type argument.
+framed
+  :: forall s i o.
+      (KnownList i, KnownList o)
+  => (i :-> o) -> ((i ++ s) :-> (o ++ s))
+framed (iNonFailingCode -> i) =
+  I $ FrameInstr (Proxy @(ToTs s)) i
+    \\ totsKnownLemma @i
+    \\ totsAppendLemma @i @s
+    \\ totsAppendLemma @o @s
diff --git a/src/Lorentz/Lambda.hs b/src/Lorentz/Lambda.hs
--- a/src/Lorentz/Lambda.hs
+++ b/src/Lorentz/Lambda.hs
@@ -5,31 +5,120 @@
   ( WrappedLambda(..)
   , Lambda
   , mkLambda
+  , mkLambdaRec
   ) where
 
+import Data.Singletons (demote)
+
 import Lorentz.Annotation
 import Lorentz.Base
-import Morley.AsRPC (HasRPCRepr(..))
-import Morley.Michelson.Typed
+import Lorentz.Coercions
+import Lorentz.Instr.Framed
+import Lorentz.Value
+import Lorentz.Zip
+import Morley.AsRPC
+import Morley.Michelson.Doc
+import Morley.Michelson.Typed hiding (Contract, pattern S)
 import Morley.Michelson.Typed.Contract (giveNotInView)
+import Morley.Michelson.Untyped (noAnn)
+import Morley.Util.Markdown
+import Morley.Util.Type
 
 -- | A helper type to construct Lorentz lambda values; Use this for lambda
 -- values outside of Lorentz contracts or with @push@.
---
--- The primary reason this is a newtype and not a type synonym is to avoid
--- accidentally splicing the output of 'mkLambda' in-line.
-newtype WrappedLambda i o = WrappedLambda {unWrappedLambda :: i :-> o}
+data WrappedLambda i o
+  = WrappedLambda (i :-> o)
+  | RecLambda (i ++ '[WrappedLambda i o] :-> o)
   deriving stock (Show, Eq, Generic)
-  deriving newtype MapLorentzInstr
 
-deriving newtype instance IsoValue (a :-> b) => IsoValue (WrappedLambda a b)
-deriving newtype instance HasAnnotation (i :-> o) => HasAnnotation (WrappedLambda i o)
-deriving newtype instance HasRPCRepr (i :-> o) => HasRPCRepr (WrappedLambda i o)
+instance (KnownList i, ZipInstr i, ZipInstr o) => IsoValue (WrappedLambda i o) where
+  type ToT (WrappedLambda i o) = 'TLambda (ToT (ZippedStack i)) (ToT (ZippedStack o))
+  toVal (WrappedLambda i) = mkVLam $ unLorentzInstr $ zippingStack i
+  toVal (RecLambda i) = mkVLamRec $ unLorentzInstr $
+    framed @'[WrappedLambda i o] (unzipInstr @i)
+    ## i
+    ## zipInstr
+  fromVal (VLam (LambdaCode i)) = WrappedLambda $ unzippingStack $ LorentzInstr i
+  fromVal (VLam (LambdaCodeRec i)) = RecLambda $
+    framed @'[WrappedLambda i o] (zipInstr @i)
+    ## LorentzInstr i
+    ## unzipInstr
 
+instance MapLorentzInstr (WrappedLambda inp out) where
+  mapLorentzInstr
+    :: (forall i o. (i :-> o) -> (i :-> o))
+    -> WrappedLambda inp out
+    -> WrappedLambda inp out
+  mapLorentzInstr f = \case
+    WrappedLambda i -> WrappedLambda $ f i
+    RecLambda i -> RecLambda $ f i
+
+instance (Each '[HasAnnotation] '[ZippedStack i, ZippedStack o])
+  => HasAnnotation (WrappedLambda i o) where
+  getAnnotation b = NTLambda noAnn
+    (getAnnotation @(ZippedStack i) b)
+    (getAnnotation @(ZippedStack o) b)
+
+instance HasRPCRepr (WrappedLambda i o) where type AsRPC (WrappedLambda i o) = WrappedLambda i o
+
 -- | A constructor providing the required constraint for 'WrappedLambda'. This is
 -- the only way to construct a lambda that uses operations forbidden in views.
 mkLambda :: (IsNotInView => i :-> o) -> WrappedLambda i o
 mkLambda i = WrappedLambda $ giveNotInView i
 
+-- | A constructor providing the required constraint for 'WrappedLambda'. This is
+-- the only way to construct a lambda that uses operations forbidden in views.
+mkLambdaRec :: (IsNotInView => i ++ '[WrappedLambda i o] :-> o) -> WrappedLambda i o
+mkLambdaRec i = RecLambda $ giveNotInView i
+
 -- | A type synonym representing Michelson lambdas.
 type Lambda i o = WrappedLambda '[i] '[o]
+
+instance (Each [Typeable, ReifyList TypeHasDoc] [i, o])
+  => TypeHasDoc (WrappedLambda i o) where
+  typeDocName _ = "WrappedLambda (extended lambda)"
+  typeDocMdReference tp wp =
+    let DocItemRef ctorDocItemId = docItemRef (DType tp)
+        refToThis = mdLocalRef (mdTicked "WrappedLambda") ctorDocItemId
+    in applyWithinParens wp $
+      mconcat $ intersperse " " [refToThis, refToStack @i, refToStack @o]
+    where
+    refToStack :: forall s. ReifyList TypeHasDoc s => Markdown
+    refToStack =
+      let stack = reifyList @_ @TypeHasDoc @s (\p -> typeDocMdReference p (WithinParens False))
+      in mconcat
+          [ mdBold "["
+          , case stack of
+              [] -> " "
+              st -> mconcat $ intersperse (mdBold "," <> " ") st
+          , mdBold "]"
+          ]
+
+  typeDocMdDescription =
+    "`WrappedLambda i o` stands for a sequence of instructions which accepts stack \
+    \of type `i` and returns stack of type `o`.\n\n\
+    \When both `i` and `o` are of length 1, this primitive corresponds to \
+    \the Michelson lambda. In more complex cases code is surrounded with `pair`\
+    \and `unpair` instructions until fits into mentioned restriction.\
+    \"
+  typeDocDependencies _ = mconcat
+    [ reifyList @_ @TypeHasDoc @i dTypeDepP
+    , reifyList @_ @TypeHasDoc @o dTypeDepP
+    , [ dTypeDep @Integer
+      , dTypeDep @Natural
+      , dTypeDep @MText
+      ]
+    ]
+  typeDocHaskellRep _ _ = Nothing
+  typeDocMichelsonRep _ =
+    ( Just "WrappedLambda [Integer, Natural, MText, ()] [ByteString]"
+    , demote @(ToT (WrappedLambda [Integer, Natural, MText, ()] '[ByteString]))
+    )
+
+instance ( CanCastTo (ZippedStack inp1) (ZippedStack inp2)
+         , CanCastTo (ZippedStack out1) (ZippedStack out2)
+         , CanCastTo (ZippedStack (inp1 ++ '[WrappedLambda inp1 out1]))
+                     (ZippedStack (inp2 ++ '[WrappedLambda inp2 out2]))
+         )
+  => WrappedLambda inp1 out1 `CanCastTo` WrappedLambda inp2 out2 where
+  castDummy = castDummyG
diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs
--- a/src/Lorentz/Macro.hs
+++ b/src/Lorentz/Macro.hs
@@ -137,7 +137,7 @@
 
 import Prelude hiding (and, compare, drop, some, swap, view)
 
-import Data.Constraint ((\\))
+import Data.Constraint (Bottom(..))
 import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+))
 import Fmt.Internal.Tuple (TupleF)
 import GHC.TypeLits qualified as Lit
@@ -418,6 +418,8 @@
 framedN
   :: forall n nNat s i i' o o'.
      ( nNat ~ ToPeano n
+     -- We use Take instead of LazyTake here because we allow @n@
+     -- to be greater than the length of @i@.
      , i' ~ Take nNat i, s ~ Drop nNat i
      , i ~ (i' ++ s), o ~ (o' ++ s)
      , KnownList i', KnownList o'
@@ -793,7 +795,8 @@
   } deriving stock (Eq, Show, Generic)
     deriving anyclass (HasAnnotation)
 
-deriving anyclass instance (HasNoOpToT r, WellTypedToT a) => IsoValue (View_ a r)
+deriving anyclass instance (HasNoOpToT r, HasNoNestedBigMaps (ToT r), WellTypedToT a)
+  => IsoValue (View_ a r)
 
 instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (View_ a1 r1) (View_ a2 r2)
 
@@ -815,16 +818,17 @@
   typeDocMichelsonRep =
     concreteTypeDocMichelsonRep @(View_ MText Integer)
 
-instance {-# OVERLAPPABLE #-} (Buildable a, HasNoOpToT r) => Buildable (View_ a r) where
+instance {-# OVERLAPPABLE #-} (Buildable a, HasNoOpToT r, HasNoNestedBigMaps (ToT r))
+  => Buildable (View_ a r) where
   build = buildView_ build
 
-instance {-# OVERLAPPING  #-} (HasNoOpToT r) => Buildable (View_ () r) where
+instance {-# OVERLAPPING  #-} (HasNoOpToT r, HasNoNestedBigMaps (ToT r)) => Buildable (View_ () r) where
   build = buildView_ $ const "()"
 
-buildViewTuple_ :: (HasNoOpToT r, TupleF a) => View_ a r -> Builder
+buildViewTuple_ :: (HasNoOpToT r, HasNoNestedBigMaps (ToT r), TupleF a) => View_ a r -> Builder
 buildViewTuple_ = buildView_ tupleF
 
-buildView_ :: (HasNoOpToT r) => (a -> Builder) -> View_ a r -> Builder
+buildView_ :: (HasNoOpToT r, HasNoNestedBigMaps (ToT r)) => (a -> Builder) -> View_ a r -> Builder
 buildView_ bfp (View_ {..}) =
   "(View param: " +| bfp viewParam |+ " callbackTo: " +| viewCallbackTo |+ ")"
 
@@ -928,7 +932,6 @@
 instance (NiceConstant r, ErrorHasDoc (VoidResult r)) =>
          IsError (VoidResult r) where
   errorToVal (VoidResult e) cont =
-    withDict (niceConstantEvi @r) $
     isoErrorToVal @(VoidResultRep r) (voidResultTag, e) cont
   errorFromVal fullErr =
     isoErrorFromVal fullErr >>= \((tag, e) :: VoidResultRep r) ->
@@ -949,13 +952,14 @@
     [dTypeDep @MText, dTypeDep @r]
 
 instance
-  ( WellTypedToT (VoidResult r)
+  ( Bottom
+  , WellTypedToT (VoidResult r)
   , Lit.TypeError ('Lit.Text "No IsoValue instance for VoidResult " 'Lit.:<>: 'Lit.ShowType r)
   ) => IsoValue (VoidResult r) where
   type ToT (VoidResult r) =
     Lit.TypeError ('Lit.Text "No IsoValue instance for VoidResult " 'Lit.:<>: 'Lit.ShowType r)
-  toVal = error "impossible"
-  fromVal = error "impossible"
+  toVal = no
+  fromVal = no
 
 mkVoid :: forall b a. a -> Void_ a b
 mkVoid a = Void_ a (mkLambda nop)
@@ -998,9 +1002,8 @@
   -> ContractRef arg
   -> (s :-> ContractRef arg : s)
 pushContractRef onContractNotFound (contractRef :: ContractRef arg) =
-  withDict (niceParameterEvi @arg) $
-    push (FutureContract contractRef) # dup #
-    runFutureContract # ifNone onContractNotFound (dip drop)
+  push (FutureContract contractRef) # dup #
+  runFutureContract # ifNone onContractNotFound (dip drop)
 
 -- | Duplicate two topmost items on top of the stack.
 dupTop2
@@ -1081,7 +1084,6 @@
 view =
   dip checkedCoerce_ # view' @name #
   ifSome nop (push (viewNameToMText viewName) # failCustom #no_view)
-  \\ niceViewableEvi @ret
   where
     viewName = demoteViewName @name
     _needHasView = Dict @(HasView vd name arg ret)
diff --git a/src/Lorentz/Pack.hs b/src/Lorentz/Pack.hs
--- a/src/Lorentz/Pack.hs
+++ b/src/Lorentz/Pack.hs
@@ -13,7 +13,6 @@
   ) where
 
 import Data.ByteString qualified as BS
-import Data.Constraint ((\\))
 
 import Lorentz.Bytes
 import Lorentz.Constraints
@@ -27,15 +26,13 @@
   :: forall a.
      (NicePackedValue a)
   => a -> ByteString
-lPackValueRaw =
-  packValue' . toVal \\ nicePackedValueEvi @a
+lPackValueRaw = packValue' . toVal
 
 lUnpackValueRaw
   :: forall a.
      (NiceUnpackedValue a)
   => ByteString -> Either UnpackError a
-lUnpackValueRaw =
-  fmap fromVal . unpackValue' \\ niceUnpackedValueEvi @a
+lUnpackValueRaw = fmap fromVal . unpackValue'
 
 lPackValue
   :: forall a.
@@ -54,7 +51,7 @@
 lEncodeValue
   :: forall a. (NiceUntypedValue a)
   => a -> ByteString
-lEncodeValue = toBinary' . toVal \\ niceUntypedValueEvi @a
+lEncodeValue = toBinary' . toVal
 
 -- | This function transforms Lorentz values into @script_expr@.
 --
diff --git a/src/Lorentz/Print.hs b/src/Lorentz/Print.hs
--- a/src/Lorentz/Print.hs
+++ b/src/Lorentz/Print.hs
@@ -20,8 +20,7 @@
     (NiceUntypedValue v)
   => Bool -> v -> LText
 printLorentzValue forceSingleLine =
-  withDict (niceUntypedValueEvi @v) $
-    printTypedValue forceSingleLine . toVal
+  printTypedValue forceSingleLine . toVal
 
 -- | Pretty-print a Lorentz contract into Michelson code.
 printLorentzContract
diff --git a/src/Lorentz/Rebinded.hs b/src/Lorentz/Rebinded.hs
deleted file mode 100644
--- a/src/Lorentz/Rebinded.hs
+++ /dev/null
@@ -1,193 +0,0 @@
--- SPDX-FileCopyrightText: 2021 Oxhead Alpha
--- SPDX-License-Identifier: LicenseRef-MIT-OA
-
-{- | Reimplementation of some syntax sugar.
-
-You need the following module pragmas to make it work smoothly:
-
-{-# LANGUAGE NoApplicativeDo, RebindableSyntax #-}
-{-# OPTIONS_GHC -Wno-unused-do-bind #-}
-
--}
-module Lorentz.Rebinded
-  ( (>>)
-  , pure
-  , return
-  , IsCondition (ifThenElse)
-  , Condition (..)
-  , (<.)
-  , (>.)
-  , (<=.)
-  , (>=.)
-  , (==.)
-  , (/=.)
-  , keepIfArgs
-
-    -- * Re-exports required for RebindableSyntax
-  , fromInteger
-  , fromString
-  , fromLabel
-  , negate
-  ) where
-
-
-import Prelude hiding (drop, not, swap, (>>), (>>=))
-
-import Lorentz.Arith
-import Lorentz.Base
-import Lorentz.Coercions
-import Lorentz.Constraints.Scopes
-import Lorentz.Instr
-import Lorentz.Macro
-import Morley.Michelson.Typed.Arith
-import Morley.Util.Label (Label)
-import Morley.Util.Named
-
--- | Aliases for '(#)' used by do-blocks.
-(>>) :: (a :-> b) -> (b :-> c) -> (a :-> c)
-(>>) = (#)
-
--- | The most basic predicate for @if ... then .. else ...@ construction,
--- defines a kind of operation applied to the top elements of the current stack.
---
--- Type arguments mean:
--- 1. Input of @if@
--- 2. Left branch input
--- 3. Right branch input
--- 4. Output of branches
--- 5. Output of @if@
-data Condition arg argl argr outb out where
-  Holds :: Condition (Bool ': s) s s o o
-  IsSome :: Condition (Maybe a ': s) (a ': s) s o o
-  IsNone :: Condition (Maybe a ': s) s (a ': s) o o
-  IsLeft :: Condition (Either l r ': s) (l ': s) (r ': s) o o
-  IsRight :: Condition (Either l r ': s) (r ': s) (l ': s) o o
-  IsCons :: Condition ([a] ': s) (a ': [a] ': s) s o o
-  IsNil :: Condition ([a] ': s) s (a ': [a] ': s) o o
-
-  Not :: Condition s s1 s2 ob o -> Condition s s2 s1 ob o
-
-  IsZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)
-         => Condition (a ': s) s s o o
-
-  IsEq :: NiceComparable a => Condition (a ': a ': s) s s o o
-  IsNeq :: NiceComparable a => Condition (a ': a ': s) s s o o
-  IsLt :: NiceComparable a => Condition (a ': a ': s) s s o o
-  IsGt :: NiceComparable a => Condition (a ': a ': s) s s o o
-  IsLe :: NiceComparable a => Condition (a ': a ': s) s s o o
-  IsGe :: NiceComparable a => Condition (a ': a ': s) s s o o
-
-  -- | Explicitly named binary condition, to ensure proper order of
-  -- stack arguments.
-  NamedBinCondition ::
-    Condition (a ': a ': s) s s o o ->
-    Label n1 -> Label n2 ->
-    Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-
-  -- | Provide the compared arguments to @if@ branches.
-  PreserveArgsBinCondition ::
-    (Dupable a, Dupable b) =>
-    (forall st o. Condition (a ': b ': st) st st o o) ->
-    Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s
-
--- | Everything that can be put after @if@ keyword.
---
--- The first type argument stands for the condition type, and all other type
--- arguments define stack types around/within the @if then else@ construction.
--- For semantics of each type argument see 'Condition'.
-class IsCondition cond arg argl argr outb out where
-  -- | Defines semantics of @if ... then ... else ...@ construction.
-  ifThenElse :: cond -> (argl :-> outb) -> (argr :-> outb) -> (arg :-> out)
-
-instance (arg ~ arg0, argl ~ argl0, argr ~ argr0, outb ~ outb0, out ~ out0) =>
-         IsCondition (Condition arg argl argr outb out) arg0 argl0 argr0 outb0 out0 where
-  ifThenElse = \case
-    Holds -> if_
-    IsSome -> flip ifNone
-    IsNone -> ifNone
-    IsLeft -> ifLeft
-    IsRight -> flip ifLeft
-    IsCons -> ifCons
-    IsNil -> flip ifCons
-
-    Not cond -> \l r -> ifThenElse cond r l
-
-    IsZero -> \l r -> eq0 # if_ l r
-
-    IsEq -> ifEq
-    IsNeq -> ifNeq
-    IsLt -> ifLt
-    IsGt -> ifGt
-    IsLe -> ifLe
-    IsGe -> ifGe
-
-    NamedBinCondition condition l1 l2 -> \l r ->
-      fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r
-
-    PreserveArgsBinCondition condition -> \l r ->
-      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
-        -- appearing to be dead code will be cut off
-        (l # drop # drop)
-        (r # drop # drop)
-
--- | Named version of 'IsLt'.
---
--- In this and similar operators you provide names of accepted stack operands as
--- a safety measure of that they go in the expected order.
-infix 4 <.
-(<.)
-  :: NiceComparable a
-  => Label n1 -> Label n2
-  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-(<.) = NamedBinCondition IsLt
-
--- | Named version of 'IsGt'.
-infix 4 >.
-(>.)
-  :: NiceComparable a
-  => Label n1 -> Label n2
-  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-(>.) = NamedBinCondition IsGt
-
--- | Named version of 'IsLe'.
-infix 4 <=.
-(<=.)
-  :: NiceComparable a
-  => Label n1 -> Label n2
-  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-(<=.) = NamedBinCondition IsLe
-
--- | Named version of 'IsGe'.
-infix 4 >=.
-(>=.)
-  :: NiceComparable a
-  => Label n1 -> Label n2
-  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-(>=.) = NamedBinCondition IsGe
-
--- | Named version of 'IsEq'.
-infix 4 ==.
-(==.)
-  :: NiceComparable a
-  => Label n1 -> Label n2
-  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-(==.) = NamedBinCondition IsEq
-
--- | Named version of 'IsNeq'.
-infix 4 /=.
-(/=.)
-  :: NiceComparable a
-  => Label n1 -> Label n2
-  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
-(/=.) = NamedBinCondition IsNeq
-
--- | Condition modifier, makes stack operands of binary comparison to be
--- available within @if@ branches.
-keepIfArgs
-  :: (Dupable a, Dupable b)
-  => (forall st o. Condition (a ': b ': st) st st o o)
-  -> Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s
-keepIfArgs = PreserveArgsBinCondition
diff --git a/src/Lorentz/Rebound.hs b/src/Lorentz/Rebound.hs
new file mode 100644
--- /dev/null
+++ b/src/Lorentz/Rebound.hs
@@ -0,0 +1,193 @@
+-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
+-- SPDX-License-Identifier: LicenseRef-MIT-OA
+
+{- | Reimplementation of some syntax sugar.
+
+You need the following module pragmas to make it work smoothly:
+
+{-# LANGUAGE NoApplicativeDo, RebindableSyntax #-}
+{-# OPTIONS_GHC -Wno-unused-do-bind #-}
+
+-}
+module Lorentz.Rebound
+  ( (>>)
+  , pure
+  , return
+  , IsCondition (ifThenElse)
+  , Condition (..)
+  , (<.)
+  , (>.)
+  , (<=.)
+  , (>=.)
+  , (==.)
+  , (/=.)
+  , keepIfArgs
+
+    -- * Re-exports required for RebindableSyntax
+  , fromInteger
+  , fromString
+  , fromLabel
+  , negate
+  ) where
+
+
+import Prelude hiding (drop, not, swap, (>>), (>>=))
+
+import Lorentz.Arith
+import Lorentz.Base
+import Lorentz.Coercions
+import Lorentz.Constraints.Scopes
+import Lorentz.Instr
+import Lorentz.Macro
+import Morley.Michelson.Typed.Arith
+import Morley.Util.Label (Label)
+import Morley.Util.Named
+
+-- | Aliases for '(#)' used by do-blocks.
+(>>) :: (a :-> b) -> (b :-> c) -> (a :-> c)
+(>>) = (#)
+
+-- | The most basic predicate for @if ... then .. else ...@ construction,
+-- defines a kind of operation applied to the top elements of the current stack.
+--
+-- Type arguments mean:
+-- 1. Input of @if@
+-- 2. Left branch input
+-- 3. Right branch input
+-- 4. Output of branches
+-- 5. Output of @if@
+data Condition arg argl argr outb out where
+  Holds :: Condition (Bool ': s) s s o o
+  IsSome :: Condition (Maybe a ': s) (a ': s) s o o
+  IsNone :: Condition (Maybe a ': s) s (a ': s) o o
+  IsLeft :: Condition (Either l r ': s) (l ': s) (r ': s) o o
+  IsRight :: Condition (Either l r ': s) (r ': s) (l ': s) o o
+  IsCons :: Condition ([a] ': s) (a ': [a] ': s) s o o
+  IsNil :: Condition ([a] ': s) s (a ': [a] ': s) o o
+
+  Not :: Condition s s1 s2 ob o -> Condition s s2 s1 ob o
+
+  IsZero :: (UnaryArithOpHs Eq' a, UnaryArithResHs Eq' a ~ Bool)
+         => Condition (a ': s) s s o o
+
+  IsEq :: NiceComparable a => Condition (a ': a ': s) s s o o
+  IsNeq :: NiceComparable a => Condition (a ': a ': s) s s o o
+  IsLt :: NiceComparable a => Condition (a ': a ': s) s s o o
+  IsGt :: NiceComparable a => Condition (a ': a ': s) s s o o
+  IsLe :: NiceComparable a => Condition (a ': a ': s) s s o o
+  IsGe :: NiceComparable a => Condition (a ': a ': s) s s o o
+
+  -- | Explicitly named binary condition, to ensure proper order of
+  -- stack arguments.
+  NamedBinCondition ::
+    Condition (a ': a ': s) s s o o ->
+    Label n1 -> Label n2 ->
+    Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+
+  -- | Provide the compared arguments to @if@ branches.
+  PreserveArgsBinCondition ::
+    (Dupable a, Dupable b) =>
+    (forall st o. Condition (a ': b ': st) st st o o) ->
+    Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s
+
+-- | Everything that can be put after @if@ keyword.
+--
+-- The first type argument stands for the condition type, and all other type
+-- arguments define stack types around/within the @if then else@ construction.
+-- For semantics of each type argument see 'Condition'.
+class IsCondition cond arg argl argr outb out where
+  -- | Defines semantics of @if ... then ... else ...@ construction.
+  ifThenElse :: cond -> (argl :-> outb) -> (argr :-> outb) -> (arg :-> out)
+
+instance (arg ~ arg0, argl ~ argl0, argr ~ argr0, outb ~ outb0, out ~ out0) =>
+         IsCondition (Condition arg argl argr outb out) arg0 argl0 argr0 outb0 out0 where
+  ifThenElse = \case
+    Holds -> if_
+    IsSome -> flip ifNone
+    IsNone -> ifNone
+    IsLeft -> ifLeft
+    IsRight -> flip ifLeft
+    IsCons -> ifCons
+    IsNil -> flip ifCons
+
+    Not cond -> \l r -> ifThenElse cond r l
+
+    IsZero -> \l r -> eq0 # if_ l r
+
+    IsEq -> ifEq
+    IsNeq -> ifNeq
+    IsLt -> ifLt
+    IsGt -> ifGt
+    IsLe -> ifLe
+    IsGe -> ifGe
+
+    NamedBinCondition condition l1 l2 -> \l r ->
+      fromNamed l1 # dip (fromNamed l2) # ifThenElse condition l r
+
+    PreserveArgsBinCondition condition -> \l r ->
+      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
+        -- appearing to be dead code will be cut off
+        (l # drop # drop)
+        (r # drop # drop)
+
+-- | Named version of 'IsLt'.
+--
+-- In this and similar operators you provide names of accepted stack operands as
+-- a safety measure of that they go in the expected order.
+infix 4 <.
+(<.)
+  :: NiceComparable a
+  => Label n1 -> Label n2
+  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+(<.) = NamedBinCondition IsLt
+
+-- | Named version of 'IsGt'.
+infix 4 >.
+(>.)
+  :: NiceComparable a
+  => Label n1 -> Label n2
+  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+(>.) = NamedBinCondition IsGt
+
+-- | Named version of 'IsLe'.
+infix 4 <=.
+(<=.)
+  :: NiceComparable a
+  => Label n1 -> Label n2
+  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+(<=.) = NamedBinCondition IsLe
+
+-- | Named version of 'IsGe'.
+infix 4 >=.
+(>=.)
+  :: NiceComparable a
+  => Label n1 -> Label n2
+  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+(>=.) = NamedBinCondition IsGe
+
+-- | Named version of 'IsEq'.
+infix 4 ==.
+(==.)
+  :: NiceComparable a
+  => Label n1 -> Label n2
+  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+(==.) = NamedBinCondition IsEq
+
+-- | Named version of 'IsNeq'.
+infix 4 /=.
+(/=.)
+  :: NiceComparable a
+  => Label n1 -> Label n2
+  -> Condition ((n1 :! a) ': (n2 :! a) ': s) s s o o
+(/=.) = NamedBinCondition IsNeq
+
+-- | Condition modifier, makes stack operands of binary comparison to be
+-- available within @if@ branches.
+keepIfArgs
+  :: (Dupable a, Dupable b)
+  => (forall st o. Condition (a ': b ': st) st st o o)
+  -> Condition (a ': b ': s) (a ': b ': s) (a ': b ': s) (a ': b ': s) s
+keepIfArgs = PreserveArgsBinCondition
diff --git a/src/Lorentz/Referenced.hs b/src/Lorentz/Referenced.hs
--- a/src/Lorentz/Referenced.hs
+++ b/src/Lorentz/Referenced.hs
@@ -17,131 +17,314 @@
 --
 -- Each instruction is followed with usage example.
 module Lorentz.Referenced
-  ( dupT
-  , dipT
+  ( DupT(..)
+  , DipT(..)
   , dropT
   ) where
 
 import Prelude hiding (drop, swap)
 
+import Data.Eq.Singletons (DefaultEq, DefaultEqSym1)
+import Data.List.Singletons qualified as LS
+import Data.Type.Bool (If)
+import Data.Vinyl.TypeLevel qualified as Peano
 import GHC.TypeLits (ErrorMessage(..), TypeError)
+import Type.Errors (ShowTypeQuoted)
 
 import Lorentz.Base
 import Lorentz.Constraints
 import Lorentz.Instr
-import Lorentz.Value
-import Morley.Util.Type
+import Morley.Util.Peano
+import Morley.Util.Type (IsElem)
 
+-- $setup
+-- >>> import Prelude ()
+-- >>> import Lorentz
+-- >>> import Lorentz.Zip (zipInstr)
+-- >>> import Fmt (pretty, Buildable(..))
+-- >>> instance Buildable () where build () = "()"
+
 -- Errors
 ----------------------------------------------------------------------------
 
-type family StackElemNotFound st a :: ErrorMessage where
-  StackElemNotFound st a =
-    'Text "Element of type `" ':<>: 'ShowType a ':<>:
-    'Text "` is not present on stack" ':$$: 'ShowType st
+type StackElemNotFound :: [Type] -> Type -> ErrorMessage
+type StackElemNotFound st a =
+  'Text "Element of type " ':<>: ShowTypeQuoted a ':<>:
+  'Text " is not present on stack" ':$$: 'ShowType st
 
-type family StackElemAmbiguous st a :: ErrorMessage where
-  StackElemAmbiguous st a =
-    'Text "Ambigous reference to element of type `" ':<>: 'ShowType a ':<>:
-    'Text "` for stack" ':$$: 'ShowType st
+type StackElemAmbiguous :: [Type] -> Type -> ErrorMessage
+type StackElemAmbiguous st a =
+  'Text "Ambiguous reference to element of type " ':<>: ShowTypeQuoted a ':<>:
+  'Text " for stack" ':$$: 'ShowType st
 
 -- Dup
 ----------------------------------------------------------------------------
 
--- | Allows duplicating stack elements referring them by type.
-class DupT (origSt :: [Type]) (a :: Type) (st :: [Type]) where
-  dupTImpl :: st :-> a : st
+{- | Allows duplicating stack elements referring them by type.
 
-instance TypeError (StackElemNotFound origSt a) =>
-         DupT origSt a '[] where
-  dupTImpl = error "impossible"
+>>> :{
+dupSample1 :: [Integer, MText, ()] :-> [MText, Integer, MText, ()]
+dupSample1 = dupT @MText
+:}
 
-instance {-# OVERLAPPING #-}
-         ( FailWhen (a `IsElem` st) (StackElemAmbiguous origSt a)
-         , Dupable a
-         ) =>
-         DupT origSt a (a : st) where
-  dupTImpl = dup
+>>> pretty $ dupSample1 # zipInstr -$ 123 ::: [mt|Hello|] ::: ()
+Hello : 123 : Hello : ()
 
-instance {-# OVERLAPPABLE #-}
-         DupT origSt a st =>
-         DupT origSt a (b : st) where
-  dupTImpl = dip (dupTImpl @origSt) # swap
+>>> :{
+dupSample2 :: [Integer, MText, ()] :-> [MText, Integer, MText, ()]
+dupSample2 = dupT
+:}
 
--- | Duplicate an element of stack referring it by type.
---
--- If stack contains multiple entries of this type, compile error is raised.
-dupT :: forall a st. DupT st a st => st :-> a : st
-dupT = dupTImpl @st @a @st
+>>> pretty $ dupSample2 # zipInstr -$ 123 ::: [mt|Hello|] ::: ()
+Hello : 123 : Hello : ()
 
-_dupSample1 :: [Integer, MText, ()] :-> [MText, Integer, MText, ()]
-_dupSample1 = dupT @MText
+>>> :{
+dupSampleErr1 :: '[] :-> a
+dupSampleErr1 = dupT @Bool
+:}
+...
+... • Element of type 'Bool' is not present on stack
+...   '[]
+...
 
+>>> :{
+-- Should fully infer both wildcards
+dupSampleErr2 :: _ :-> [Bool, Integer, _, ()]
+dupSampleErr2 = dupT
+:}
+...
+... • Found type wildcard ‘_’
+...    standing for ‘'[Integer, Bool, ()] :: [*]’
+...
+... • Found type wildcard ‘_’ standing for ‘Bool’
+...   To use the inferred type, enable PartialTypeSignatures
+...
+
+>>> :{
+-- Should fully infer both wildcards
+_dupSampleErr3 :: [Integer, _, ()] :-> (Bool ': _)
+_dupSampleErr3 = dupT
+:}
+...
+... • Found type wildcard ‘_’ standing for ‘Bool’
+...
+... • Found type wildcard ‘_’
+...     standing for ‘'[Integer, Bool, ()] :: [*]’
+...
+
+-}
+class st ~ (Head st ': Tail st) => DupT (a :: Type) (st :: [Type]) where
+  -- | Duplicate an element of stack referring it by type.
+  --
+  -- If stack contains multiple entries of this type, compile error is raised.
+  dupT :: st :-> a : st
+
+instance ( EnsureElem a st
+         , TheOnlyC (StackElemNotFound st a)
+                    (StackElemAmbiguous st a)
+                    (LS.FindIndices (DefaultEqSym1 a) st)
+                    indexGHC
+         , succ_index ~ 'Peano.S (ToPeano indexGHC)
+         , ConstraintDUPNLorentz succ_index st (a ': st) a
+         , Dupable a
+         ) =>
+  DupT a st where
+  dupT = dupNPeano @succ_index
+
 -- Dip
 ----------------------------------------------------------------------------
 
--- | Allows diving into stack referring expected new tip by type.
---
--- 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 :: [Type]) (a :: Type)
-           (inp :: [Type]) (dipInp :: [Type])
-           (dipOut :: [Type]) (out :: [Type])
-           | inp a -> dipInp, dipOut inp a -> out where
-  dipTImpl :: (dipInp :-> dipOut) -> (inp :-> out)
+{- | Allows diving into stack referring expected new tip by type.
 
-instance ( TypeError (StackElemNotFound origSt a)
-         , dipInp ~ TypeError ('Text "Undefined type (see next error)")
-         , out ~ TypeError ('Text "Undefined type (see next error)")
-         ) =>
-         DipT origSt a '[] dipInp dipOut out where
-  dipTImpl = error "impossible"
+>>> :{
+dipSample1
+  :: [Natural, ()] :-> '[()]
+  -> [Integer, MText, Natural, ()] :-> [Integer, MText, ()]
+dipSample1 = dipT @Natural
+:}
 
-instance {-# OVERLAPPING #-}
-         ( FailWhen (a `IsElem` st) (StackElemAmbiguous origSt a)
-         , dipInp ~ (a : st)
-         , dipOut ~ out
+>>> pretty $ dipSample1 drop # zipInstr -$ 123 ::: [mt|Hello|] ::: 321 ::: ()
+123 : Hello : ()
+
+>>> :{
+dipSample2
+  :: [Natural, ()] :-> '[()]
+  -> [Integer, MText, Natural, ()] :-> [Integer, MText, ()]
+dipSample2 = dipT -- No type application needed
+:}
+
+>>> pretty $ dipSample2 drop # zipInstr -$ 123 ::: [mt|Hello|] ::: 321 ::: ()
+123 : Hello : ()
+
+>>> :{
+-- An implementation of dropT that demands a bit more from inference.
+dipSample3
+  :: forall a inp dinp dout out.
+     ( DipT a inp dinp dout out
+     , dinp ~ (a ': dout)
+     )
+  => inp :-> out
+dipSample3 = dipT (drop @a)
+:}
+
+>>> :{
+pretty $ dipSample3 @Natural @'[Integer, MText, Natural, ()] # zipInstr
+  -$ 123 ::: [mt|Hello|] ::: 321 ::: ()
+:}
+123 : Hello : ()
+
+>>> :{
+_dipSampleErr1
+  :: [Natural, ()] :-> '[()]
+  -> [Integer, MText, ()] :-> [Integer, MText, ()]
+_dipSampleErr1 = dipT @Natural
+:}
+...
+... • Element of type 'Natural' is not present on stack
+...   '[Integer, MText, ()]
+...
+
+>>> :{
+_dipSampleErr2
+  :: [Natural, ()] :-> '[()]
+  -> [Integer, MText, Natural, (), Natural] :-> [Integer, MText, ()]
+_dipSampleErr2 = dipT @Natural
+:}
+...
+... • Ambiguous reference to element of type 'Natural' for stack
+...   '[Integer, MText, Natural, (), Natural]
+...
+
+>>> :{
+_dipSampleErr3
+  :: '[] :-> '[()]
+  -> [Integer, MText, Natural, ()] :-> [Integer, MText, ()]
+_dipSampleErr3 = dipT @Natural
+:}
+...
+... • dipT requires a Lorentz instruction that takes input on the stack.
+...
+
+-}
+type DipT :: Type -> [Type] -> [Type] -> [Type] -> [Type] -> Constraint
+class dipInp ~ (a ': Tail dipInp) => DipT a inp dipInp dipOut out
+  | inp a -> dipInp, dipOut inp a -> out, inp out a -> dipOut where
+  -- | Dip down until an element of the given type is on top of the stack.
+  --
+  -- If the stack does not contain an element of this type, or contains more
+  -- than one, then a compile-time error is raised.
+  dipT :: (dipInp :-> dipOut) -> (inp :-> out)
+
+
+{-
+-- We'd like to be able to write something like this. Unfortunately, due to GHC
+-- issue #22126, this causes numerous copies of the type error to be sprayed to
+-- the screen.
+
+instance ( dipInp ~ (a ': tlDI)
+         , EnsureElem a inp
+         , RequireNonEmpty
+             ('Text "dipT requires a Lorentz instruction that takes input on the stack.")
+             dipInp
+         , index ~ ToPeano (TheOnly (StackElemNotFound inp a)
+                                    (StackElemAmbiguous inp a)
+                                    (LS.FindIndices (DefaultEqSym1 a) inp))
+         , ConstraintDIPNLorentz index inp out dipInp dipOut
          ) =>
-         DipT origSt a (a : st) dipInp dipOut out where
-  dipTImpl = id
+  DipT a inp dipInp dipOut out where
+  dipT = dipNPeano @index
 
-instance {-# OVERLAPPABLE #-}
-         ( DipT origSt a st dipInp dipOut out
-         , out1 ~ (b : out)
+type family TheOnly (empty_err :: ErrorMessage) (many_err :: ErrorMessage) (xs :: [k]) :: k where
+  TheOnly e_err _ '[] = TypeError e_err
+  TheOnly _ _ '[x] = x
+  TheOnly _ m_err _ = TypeError m_err
+-}
+
+instance ( dipInp ~ (a ': tail_dipInp)
+         , EnsureElem a inp
+         , RequireNonEmpty
+             ('Text "dipT requires a Lorentz instruction that takes input on the stack.")
+             dipInp
+         , TheOnlyC (StackElemNotFound inp a)
+                   (StackElemAmbiguous inp a)
+                   (LS.FindIndices (DefaultEqSym1 a) inp)
+                   indexGHC
+         , index ~ ToPeano indexGHC
+         , ConstraintDIPNLorentz index inp out dipInp dipOut
          ) =>
-         DipT origSt a (b : st) dipInp dipOut out1 where
-  dipTImpl = dip . dipTImpl @origSt @a @st
+  DipT a inp dipInp dipOut out where
+  dipT = dipNPeano @index
 
--- | Dip repeatedly until element of the given type is on top of the stack.
---
--- If stack contains multiple entries of this type, compile error is raised.
-dipT
-  :: forall a inp dinp dout out.
-     DipT inp a inp dinp dout out
-  => (dinp :-> dout) -> (inp :-> out)
-dipT = dipTImpl @inp @a @inp @dinp
+-- | @EnsureElem x xs@ constrains @x@ to be an element of @xs@. Unlike
+-- @'IsElem' x xs ~ 'True@, @EnsureElem x xs@ can help infer @xs@. For
+-- example, given @EnsureElem Int '[Char, b, Bool]@, where @b@ is otherwise
+-- unknown, GHC will infer that @b ~ Int@. @EnsureElem@ can also increase
+-- information about the length of @xs@. For example, given
+-- @EnsureElem Int (Char ': more)@, GHC will infer that @more@ has at least
+-- one element.
+type EnsureElem :: forall k. k -> [k] -> Constraint
+type EnsureElem x xs = (xs ~ (Head xs ': Tail xs), EnsureElem' x xs)
+type family EnsureElem' x xs where
+  EnsureElem' x (y ': ys) =
+    ( If (x `DefaultEq` y) (() :: Constraint) (EnsureElem x ys)
+    , If (IsElem x ys) (() :: Constraint) (x ~ y))
 
-_dipSample1
-  :: [Natural, ()]
-      :-> '[ByteString]
-  -> [Integer, Text, Natural, ()]
-      :-> [Integer, Text, ByteString]
-_dipSample1 = dipT @Natural
+-- | @TheOnlyC empty_err many_err xs x@ constrains @x@ to be the only
+-- element of @xs@. It produces the type error @empty_err@ if @xs@ is empty,
+-- and the type error @many_err@ if @xs@ has more than one element.
+type TheOnlyC :: ErrorMessage -> ErrorMessage -> [k] -> k -> Constraint
+-- NB: This is not a type family because of GHC issue #22126, see above
+class TheOnlyC empty_err many_err xs x | xs -> x
+instance (TypeError e_err, y ~ Determined) => TheOnlyC e_err m_err '[] y
+instance x ~ y => TheOnlyC e_err m_err '[x] y
+instance (TypeError m_err, y ~ Determined) => TheOnlyC e_err m_err (x1 ': x2 ': xs) y
 
+type RequireNonEmpty :: ErrorMessage -> [k] -> Constraint
+type family RequireNonEmpty e xs where
+  RequireNonEmpty e '[] = TypeError e
+  RequireNonEmpty _ _ = ()
+
+-- We just use this to satisfy fundeps in error cases.
+type family Determined where {}
+
 -- Drop
 ----------------------------------------------------------------------------
 
--- | Remove element with the given type from the stack.
+{- | Remove element with the given type from the stack.
+
+>>> :{
+dropSample1 :: [Integer, (), Natural] :-> [Integer, Natural]
+dropSample1 = dropT @()
+:}
+
+>>> pretty $ dropSample1 # zipInstr -$ 123 ::: () ::: 321
+123 : 321
+
+>>> :{
+dropSampleErr1 :: [Integer, Natural] :-> [Integer, Natural]
+dropSampleErr1 = dropT @()
+:}
+...
+... • Element of type '()' is not present on stack
+...   '[Integer, Natural]
+...
+
+>>> :{
+dropSampleErr1 :: [Integer, Integer] :-> '[Integer]
+dropSampleErr1 = dropT @Integer
+:}
+...
+... • Ambiguous reference to element of type 'Integer' for stack
+...   '[Integer, Integer]
+...
+-}
 dropT
   :: forall a inp dinp dout out.
-     ( DipT inp a inp dinp dout out
+     ( DipT a inp dinp dout out
      , dinp ~ (a ': dout)
      )
   => inp :-> out
 dropT = dipT @a drop
-
-_dropSample1 :: [Integer, (), Natural] :-> [Integer, Natural]
-_dropSample1 = dropT @()
 
 -- Framing
 ----------------------------------------------------------------------------
diff --git a/src/Lorentz/ReferencedByName.hs b/src/Lorentz/ReferencedByName.hs
--- a/src/Lorentz/ReferencedByName.hs
+++ b/src/Lorentz/ReferencedByName.hs
@@ -21,8 +21,10 @@
   , VarIsUnnamed
   ) where
 
-import Data.Constraint ((\\))
+import Data.Constraint (Bottom(..), (\\))
 import Data.Singletons (Sing)
+import Fcf qualified
+import Type.Errors (DelayError, IfStuck)
 
 import Lorentz.ADT
 import Lorentz.Base
@@ -40,10 +42,10 @@
 -- Errors
 ----------------------------------------------------------------------------
 
-type family StackElemNotFound name :: ErrorMessage where
-  StackElemNotFound name =
-    'Text "Element with name `" ':<>: 'ShowType name ':<>:
-    'Text "` is not present on stack"
+type StackElemNotFound :: Symbol -> k
+type StackElemNotFound name = DelayError
+  ('Text "Element with name " ':<>: 'ShowType name ':<>: 'Text " is not present on stack")
+  -- NB: as @name@ is a Symbol, it'll be double-quoted in ShowType.
 
 data NamedVariableNotFound name
 
@@ -51,33 +53,25 @@
 ----------------------------------------------------------------------------
 
 -- | Name of a variable on stack.
-data VarNamed = VarNamed Symbol | VarUnnamed | VarNameDummy
+data VarNamed = VarNamed Symbol | VarUnnamed
 
 -- | Get variable name.
+type VarName :: Type -> VarNamed
 type family VarName (a :: Type) :: VarNamed where
   VarName (NamedF _ _ name) = 'VarNamed name
   VarName _ = 'VarUnnamed
 
-type family AnyVN :: VarNamed
-
--- Attach an error message to given variable.
--- If its evaluation is stuck, compiler's attempt to display this type
--- will cause the given error being displayed.
-type family Assert (vn :: VarNamed) (err :: Constraint) :: VarNamed where
-  Assert 'VarNameDummy _ = AnyVN
-  Assert vn _ = vn
-
-type family VarNamePretty' (x :: Type) (vn :: VarNamed) :: VarNamed where
-  VarNamePretty' x vn = Assert vn
-    (TypeError
+-- | 'VarName' with pretty error message.
+type VarNamePretty :: Type -> VarNamed
+type VarNamePretty x =
+  IfStuck (VarName x)
+    (DelayError
       ('Text "Not clear which name `" ':<>: 'ShowType x ':<>: 'Text "` variable has" ':$$:
        'Text "Consider adding `VarIsUnnamed " ':<>: 'ShowType x ':<>: 'Text "` constraint" ':$$:
        'Text "or carrying a named variable instead"
       )
     )
-
--- | 'VarName' with pretty error message.
-type VarNamePretty x = VarNamePretty' x (VarName x)
+    (Fcf.Pure (VarName x))
 
 -- | Requires type @x@ to be an unnamed variable.
 --
@@ -104,28 +98,27 @@
 and can easily add this constraint to his methods.
 
 -}
-class HasNamedVar (s :: [Type]) (name :: Symbol) (var :: Type)
-    | s name -> var where
-
+type HasNamedVar :: [Type] -> Symbol -> Type -> Constraint
+class HasNamedVar s name var | s name -> var where
   -- | 1-based position of the variable on stack.
   varPosition :: VarPosition s name var
 
+type ConstraintVarPosition :: [Type] -> Peano -> Constraint
 type ConstraintVarPosition s n =
   ( SingI n, n > 'Z ~ 'True
   , RequireLongerOrSameLength s n, RequireLongerOrSameLength (ToTs s) n
   )
 
-data VarPosition (s :: [Type]) (name :: Symbol) (var :: Type) where
-  VarPosition
-    :: (ConstraintVarPosition s n)
-    => Sing (n :: Peano)
-    -> VarPosition s name var
+type VarPosition :: [Type] -> Symbol -> Type -> Type
+data VarPosition s name var where
+  VarPosition :: (ConstraintVarPosition s n) => Sing (n :: Peano) -> VarPosition s name var
 
-instance ( TypeError (StackElemNotFound name)
+instance ( Bottom
+         , StackElemNotFound name
          , var ~ NamedVariableNotFound name
          ) =>
          HasNamedVar '[] name var where
-  varPosition = error "impossible"
+  varPosition = no
 
 instance ( ElemHasNamedVar (ty : s) name var
              (VarNamePretty ty == 'VarNamed name)
@@ -134,8 +127,8 @@
   varPosition = elemVarPosition @(ty : s) @name @var @(VarNamePretty ty == 'VarNamed name)
 
 -- Helper for handling each separate variable on stack
-class ElemHasNamedVar s name var (nameMatch :: Bool)
-    | s name nameMatch -> var where
+type ElemHasNamedVar :: [Type] -> Symbol -> Type -> Bool -> Constraint
+class ElemHasNamedVar s name var nameMatch | s name nameMatch -> var where
   elemVarPosition :: VarPosition s name var
 
 instance (ty ~ NamedF f var name) =>
@@ -150,7 +143,8 @@
 -- | Version of 'HasNamedVar' for multiple variables.
 --
 -- > type HasContext = HasNamedVars s ["x" := Integer, "f" := Lambda MText MText]
-type family HasNamedVars (s :: [Type]) (vs :: [NamedField]) :: Constraint where
+type HasNamedVars :: [Type] -> [NamedField] -> Constraint
+type family HasNamedVars s vs where
   HasNamedVars _ '[] = ()
   HasNamedVars s ((n := ty) ': vs) = (HasNamedVar s n ty, HasNamedVars s vs)
 
@@ -168,8 +162,8 @@
   => Sing (n :: Peano) -> s :-> var : s
 unsafeDupL _ =
   dupNPeano @n
-    \\ unsafeProvideConstraint @(Take (Decrement n) s ++ (var : Drop n s) ~ s)
-    \\ unsafeProvideConstraint @(Take (Decrement n) (ToTs s) ++ (ToT var : Drop n (ToTs s)) ~ ToTs s)
+    \\ unsafeProvideConstraint @(LazyTake (Decrement n) s ++ (var : Drop n s) ~ s)
+    \\ unsafeProvideConstraint @(LazyTake (Decrement n) (ToTs s) ++ (ToT var : Drop n (ToTs s)) ~ ToTs s)
 
 -- | Version of 'dupL' that leaves a named variable on stack.
 dupLNamed
diff --git a/src/Lorentz/Run.hs b/src/Lorentz/Run.hs
--- a/src/Lorentz/Run.hs
+++ b/src/Lorentz/Run.hs
@@ -55,7 +55,6 @@
   ) where
 
 import Control.Lens.Type as Lens (Lens, Lens')
-import Data.Constraint ((\\))
 import Data.Default (def)
 import Data.Vinyl.Core (Rec(..))
 import Data.Vinyl.Functor qualified as Rec
@@ -218,8 +217,7 @@
       , cStoreNotes = getAnnotation @st NotFollowEntrypoint
       , cEntriesOrder = U.canonicalEntriesOrder
       , cViews = compileLorentzViews cdCompilationOptions cdViews
-      } \\ niceParameterEvi @cp
-        \\ niceStorageEvi @st
+      }
 
     cDocumentedCode = case cdCode of
       ContractCode x -> ContractCode $
@@ -265,8 +263,6 @@
         , M.vReturn = getAnnotation @ret NotFollowEntrypoint
         , M.vCode = compileLorentzWithOptions co viewCode
         }
-        \\ niceViewableEvi @arg
-        \\ niceViewableEvi @ret
 
 {- | Set all the contract's views.
 
@@ -316,7 +312,7 @@
   => ContractEnv
   -> (IsNotInView => inp :-> out)
   -> Rec Identity inp
-  -> Either MichelsonFailureWithStack (Rec Identity out)
+  -> Either (MichelsonFailureWithStack Void) (Rec Identity out)
 interpretLorentzInstr env instr inp =
   fromValStack <$> interpretInstr env (compileLorentz $ giveNotInView instr) (toValStack inp)
 
@@ -327,7 +323,7 @@
   => ContractEnv
   -> (IsNotInView => Fn inp out)
   -> inp
-  -> Either MichelsonFailureWithStack out
+  -> Either (MichelsonFailureWithStack Void) out
 interpretLorentzLambda env instr inp = do
   res <- interpretLorentzInstr env instr (Identity inp :& RNil)
   let Identity out :& RNil = res
diff --git a/src/Lorentz/Run/Simple.hs b/src/Lorentz/Run/Simple.hs
--- a/src/Lorentz/Run/Simple.hs
+++ b/src/Lorentz/Run/Simple.hs
@@ -42,7 +42,7 @@
 -- For testing and demonstration purposes.
 infixr 2 -$?
 (-$?) :: (ZipInstr inps, IsoValue out)
-      => (IsNotInView => inps :-> '[out]) -> ZippedStack inps -> Either MichelsonFailureWithStack out
+      => (IsNotInView => inps :-> '[out]) -> ZippedStack inps -> Either (MichelsonFailureWithStack Void) out
 code -$? inp = interpretLorentzLambda dummyContractEnv (unzipInstr # code) inp
 
 -- | Like @'-$?'@, assumes that no failure is possible.
@@ -73,7 +73,7 @@
 -- | Version of (-$?) with arguments flipped.
 infixl 2 &?-
 (&?-) :: (ZipInstr inps, IsoValue out)
-      => ZippedStack inps -> (IsNotInView => inps :-> '[out]) -> Either MichelsonFailureWithStack out
+      => ZippedStack inps -> (IsNotInView => inps :-> '[out]) -> Either (MichelsonFailureWithStack Void) out
 (&?-) x y = (-$?) y x
 
 -- | Version of (-$) with arguments flipped.
diff --git a/src/Lorentz/Tickets.hs b/src/Lorentz/Tickets.hs
--- a/src/Lorentz/Tickets.hs
+++ b/src/Lorentz/Tickets.hs
@@ -107,7 +107,7 @@
 import Lorentz.Expr
 import Lorentz.Instr
 import Lorentz.Macro
-import Lorentz.Rebinded
+import Lorentz.Rebound
 import Lorentz.Value
 import Morley.Michelson.Typed.Haskell.Doc
 import Morley.Util.Markdown
diff --git a/src/Lorentz/UParam.hs b/src/Lorentz/UParam.hs
--- a/src/Lorentz/UParam.hs
+++ b/src/Lorentz/UParam.hs
@@ -46,7 +46,7 @@
   , unwrapUParam
   ) where
 
-import Data.Constraint ((\\))
+import Data.Constraint (Bottom(..))
 import Fcf qualified
 import Fmt (Buildable(..))
 import GHC.Generics ((:*:)(..), (:+:)(..))
@@ -141,7 +141,6 @@
   => Label name -> a -> UParam entries
 mkUParam label (a :: a) =
   UnsafeUParam (labelToMText label, lPackValueRaw a)
-    \\ nicePackedValueEvi @a
 
 -- Example
 ----------------------------------------------------------------------------
@@ -376,20 +375,22 @@
     )
 
 instance
-    TypeError ('Text "UParam linearization requires exactly one field \
-                    \in each constructor") =>
+    ( Bottom
+    , TypeError ('Text "UParam linearization requires exactly one field \
+                       \in each constructor")) =>
     GUParamLinearize (G.C1 i G.U1) where
   type GUParamLinearized (G.C1 i G.U1) =
     TypeError ('Text "Bad linearized ADT")
-  adtToRec = error "impossible"
+  adtToRec = no
 
 instance
-    TypeError ('Text "UParam linearization requires exactly one field \
-                    \in each constructor") =>
+    ( Bottom
+    , TypeError ('Text "UParam linearization requires exactly one field \
+                       \in each constructor")) =>
     GUParamLinearize (G.C1 i (x :*: y)) where
   type GUParamLinearized (G.C1 i (x :*: y)) =
     TypeError ('Text "Bad linearized ADT")
-  adtToRec = error "impossible"
+  adtToRec = no
 
 ----------------------------------------------------------------------------
 -- Documentation
diff --git a/src/Lorentz/Util/TH.hs b/src/Lorentz/Util/TH.hs
--- a/src/Lorentz/Util/TH.hs
+++ b/src/Lorentz/Util/TH.hs
@@ -4,7 +4,6 @@
 -- | Lorentz template-haskell and quasiquote utilities.
 module Lorentz.Util.TH
   ( entrypointDoc
-  , errorDoc
   , errorDocArg
   , typeDoc
   ) where
@@ -78,29 +77,6 @@
                 type ParameterEntrypointsDerivation $(conT $ mkName $ toString param) = $(paramValue)
               |]
             Left err -> failQQ qqName err
-
--- | QuasiQuote that helps generating @CustomErrorHasDoc@ instance.
---
--- Usage:
---
--- @
--- [errorDoc| \<error-name> \<error-type> \<error-description> |]
--- [errorDoc| "errorName" exception "Error description" |]
--- @
---
--- This is equivalent to 'errorDocArg' with @()@ specified as error argument type.
---
-errorDoc :: QuasiQuoter
-errorDoc = QuasiQuoter
-  { quoteExp  = const $ failQQType qqName "expression"
-  , quotePat  = const $ failQQType qqName "pattern"
-  , quoteType = const $ failQQType qqName "type"
-  , quoteDec  = quoteDec errorDocArg . (<> " ()")
-  }
-  where
-    qqName = "errorDoc"
-
-{-# DEPRECATED errorDoc "errorDoc is deprecated, use errorDocArg with () argument instead" #-}
 
 -- | QuasiQuote that helps generating @CustomErrorHasDoc@ instance.
 --
diff --git a/src/Lorentz/Value.hs b/src/Lorentz/Value.hs
--- a/src/Lorentz/Value.hs
+++ b/src/Lorentz/Value.hs
@@ -81,7 +81,6 @@
   , module ReExports
   ) where
 
-import Data.Constraint ((\\))
 import Data.Default (Default(..))
 import Prelude hiding (Rational)
 
@@ -140,7 +139,7 @@
 newtype PrintAsValue a = PrintAsValue a
 
 instance NiceUntypedValue a => Buildable (PrintAsValue a) where
-  build (PrintAsValue a) = build (M.toVal a) \\ niceUntypedValueEvi @a
+  build (PrintAsValue a) = build (M.toVal a)
 
 data OpenChest = ChestContent ByteString | ChestOpenFailed Bool
   deriving stock (Generic, Show, Eq)
diff --git a/src/Lorentz/Zip.hs b/src/Lorentz/Zip.hs
--- a/src/Lorentz/Zip.hs
+++ b/src/Lorentz/Zip.hs
@@ -1,8 +1,6 @@
 -- SPDX-FileCopyrightText: 2021 Oxhead Alpha
 -- SPDX-License-Identifier: LicenseRef-MIT-OA
 
-{-# OPTIONS_GHC -Wno-orphans #-}
-
 -- | Stack zipping.
 --
 -- This module provides functions for flattening stacks into tuples.
@@ -18,15 +16,16 @@
   , unzippingStack
   , ZippedStackRepr(..)
   , ZSNil(..)
+  , (##)
   ) where
 
 import Prelude hiding (drop)
 
+import Fmt (Buildable(..), (+|), (|+))
+
 import Lorentz.Annotation
 import Lorentz.Base
-import Morley.AsRPC (HasRPCRepr(..))
 import Morley.Michelson.Typed
-import Morley.Michelson.Untyped (noAnn)
 
 -- | Version of '#' which performs some optimizations immediately.
 --
@@ -63,6 +62,12 @@
   deriving stock (Show, Eq, Generic)
   deriving anyclass (IsoValue, HasAnnotation)
 
+instance (Buildable a, Buildable b) => Buildable (ZippedStackRepr a b) where
+  build (a ::: b) = a |+ " : " +| b |+ ""
+
+instance Buildable ZSNil where
+  build ZSNil = "[]"
+
 -- | Zipping stack into tuple and back.
 class (KnownIsoT (ZippedStack s)) => ZipInstr (s :: [Type]) where
   -- | A type which contains the whole stack zipped.
@@ -114,22 +119,3 @@
   :: ZipInstrs [inp, out]
   => Fn (ZippedStack inp) (ZippedStack out) -> inp :-> out
 unzippingStack code = zipInstr ## code ## unzipInstr
-
-instance (WellTypedToT (ZippedStack inp), WellTypedToT (ZippedStack out), ZipInstr inp, ZipInstr out) => IsoValue (inp :-> out) where
-  type ToT (inp :-> out) = 'TLambda (ToT (ZippedStack inp)) (ToT (ZippedStack out))
-  toVal i = mkVLam $ unLorentzInstr $ zippingStack i
-  fromVal (VLam i) = zipInstr ## LorentzInstr i ## unzipInstr
-
-instance
-    ( HasAnnotation (ZippedStack i)
-    , HasAnnotation (ZippedStack o)
-    )
-  =>
-    HasAnnotation (i :-> o)
-  where
-  getAnnotation b = NTLambda noAnn
-    (getAnnotation @(ZippedStack i) b)
-    (getAnnotation @(ZippedStack o) b)
-
-instance HasRPCRepr (inp :-> out) where
-  type AsRPC (inp :-> out) = inp :-> out