diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,21 @@
+Unreleased
+==========
+<!-- Append new entries here -->
+
+0.3.0
+==========
+* [!583](https://gitlab.com/morley-framework/morley/-/merge_requests/583)
+  Add an intermediate compilation representation for optimization.
+  + `fail`-like statements return `RetVars r` instead of `r`.
+* [!534](https://gitlab.com/morley-framework/morley/-/merge_requests/534)
+  Add a tutorial on how to setup an Indigo project using Indigo CLI.
+  + Bump the dependencies version of the boilerplate generated by `indigo new`
+  to the latest.
+
+* [!566](https://gitlab.com/morley-framework/morley/-/merge_requests/566)
+  Add Indigo CLI installation script.
+  + Mention how Indigo CLI can be installed in the Indigo documentation.
+
 0.2.2
 =====
 * [!544](https://gitlab.com/morley-framework/morley/-/merge_requests/544)
diff --git a/app/FileGen/Files.hs b/app/FileGen/Files.hs
--- a/app/FileGen/Files.hs
+++ b/app/FileGen/Files.hs
@@ -287,13 +287,13 @@
 extra-deps:
   - tasty-hunit-compat-0.2
   - morley-prelude-0.3.0
-  - morley-1.6.0
-  - lorentz-0.6.0
-  - indigo-0.2.0
+  - morley-1.7.0
+  - lorentz-0.6.1
+  - indigo-0.2.2
   - git:
       https://gitlab.com/morley-framework/morley.git
     commit:
-      3bc23ad17a0719ee96d83a94b0194ca5bfe3b8c7 # morley-1.6.0
+      2d0506578493fec3851d711a5cc26c9dc5885001 # morley-1.7.0
     subdirs:
       - code/cleveland
       - code/morley-client
diff --git a/indigo.cabal b/indigo.cabal
--- a/indigo.cabal
+++ b/indigo.cabal
@@ -1,13 +1,11 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.33.0.
+-- This file has been generated from package.yaml by hpack version 0.34.2.
 --
 -- see: https://github.com/sol/hpack
---
--- hash: d2d0380bd7fe31c9c13bc66fa1ba8f5589bfb4518b14975a4e15bb0d833ce0d6
 
 name:           indigo
-version:        0.2.2
+version:        0.3.0
 synopsis:       Convenient imperative eDSL over Lorentz.
 description:    Syntax and implementation of Indigo eDSL.
 category:       Language
@@ -39,8 +37,10 @@
       Indigo.Backend.Scope
       Indigo.Backend.Var
       Indigo.Compilation
+      Indigo.Compilation.Field
       Indigo.Compilation.Lambda
       Indigo.Compilation.Params
+      Indigo.Compilation.Sequential
       Indigo.Frontend
       Indigo.Frontend.Language
       Indigo.Frontend.Program
@@ -56,6 +56,7 @@
       Indigo.Internal.Object
       Indigo.Internal.SIS
       Indigo.Internal.State
+      Indigo.Internal.Var
       Indigo.Lib
       Indigo.Lorentz
       Indigo.Prelude
diff --git a/src/Indigo.hs b/src/Indigo.hs
--- a/src/Indigo.hs
+++ b/src/Indigo.hs
@@ -8,7 +8,7 @@
 
 import Indigo.Compilation as Exports
 import Indigo.Frontend as Exports
-import Indigo.Internal as Exports hiding (return, (=<<), (>>), (>>=))
+import Indigo.Internal as Exports hiding ((>>))
 import Indigo.Lib as Exports
 import Indigo.Lorentz as Exports hiding (forcedCoerce)
 import Indigo.Prelude as Exports
diff --git a/src/Indigo/Backend.hs b/src/Indigo/Backend.hs
--- a/src/Indigo/Backend.hs
+++ b/src/Indigo/Backend.hs
@@ -30,6 +30,7 @@
   -- * Side-effects
   , transferTokens
   , setDelegate
+  , createContract
 
   -- * Functions, Procedures and Scopes
   , scope
@@ -52,6 +53,7 @@
 import qualified Lorentz.Entrypoints.Doc as L (finalizeParamCallingDoc)
 import Lorentz.Entrypoints.Helpers (RequireSumType)
 import qualified Lorentz.Instr as L
+import qualified Lorentz.Run as L
 import qualified Michelson.Typed as MT
 import Util.Type (type (++))
 
@@ -59,84 +61,100 @@
 -- Loop
 ----------------------------------------------------------------------------
 
--- | While statement. The same rule about releasing.
-while :: Expr Bool -> IndigoState inp xs () -> IndigoState inp inp ()
+-- | While statement.
+while
+  :: Expr Bool
+  -- ^ Expression for the control flow
+  -> SomeIndigoState inp
+  -- ^ Block of code to execute, as long as the expression holds 'True'
+  -> IndigoState inp inp
 while e body = IndigoState $ \md ->
-  let expCd = gcCode $ runIndigoState (compileExpr e) md in
-  let bodyIndigoState = cleanGenCode $ runIndigoState body md in
-  GenCode () md (expCd # L.loop (bodyIndigoState # expCd)) L.nop
+  let expCd = gcCode $ usingIndigoState md (compileExpr e)
+      bodyIndigoState = runSIS body md cleanGenCode
+  in GenCode (mdStack md) (expCd # L.loop (bodyIndigoState # expCd)) L.nop
 
+-- | While-left statement. Repeats a block of code as long as the control
+-- 'Either' is 'Left', returns when it is 'Right'.
 whileLeft
   :: (KnownValue l, KnownValue r)
   => Expr (Either l r)
-  -> (Var l -> IndigoState (l & inp) xs ())
-  -> IndigoState inp (r & inp) (Var r)
-whileLeft e body = IndigoState $ \md ->
+  -- ^ Expression for the control flow value
+  -> Var l
+  -- ^ Variable for the 'Left' value (available to the code block)
+  -> SomeIndigoState (l & inp)
+  -- ^ Code block to execute while the value is 'Left'
+  -> Var r
+  -- ^ Variable that will be assigned to the resulting value
+  -> IndigoState inp (r & inp)
+whileLeft e varL body varR = IndigoState $ \md ->
   let
-    cde = gcCode $ runIndigoState (compileExpr e) md
-    (l, newMd) = pushRefMd md
-    gc = cleanGenCode $ runIndigoState (body l) newMd
-    (r, resMd) = pushRefMd md
-  in GenCode r resMd (cde # L.loopLeft (gc # L.drop # cde)) L.drop
+    cde = gcCode $ usingIndigoState md (compileExpr e)
+    newMd = pushRefMd varL md
+    gc = runSIS body newMd cleanGenCode
+    resSt = pushRef varR $ mdStack md
+  in GenCode resSt (cde # L.loopLeft (gc # L.drop # cde)) L.drop
 
--- | For statements to iterate over container.
+-- | For statements to iterate over a container.
 forEach
   :: (IterOpHs a, KnownValue (IterOpElHs a))
-  => Expr a -> (Var (IterOpElHs a) -> IndigoState ((IterOpElHs a) & inp) xs ())
-  -> IndigoState inp inp ()
-forEach container body = IndigoState $ \md ->
-  let cde = gcCode $ runIndigoState (compileExpr container) md in
-  let (var, newMd) = pushRefMd md in
-  let bodyIndigoState = cleanGenCode $ runIndigoState (body var) newMd in
-  GenCode () md (cde # L.iter (bodyIndigoState # L.drop)) L.nop
+  => Expr a
+  -- ^ Expression for the container to traverse
+  -> Var (IterOpElHs a)
+  -- ^ Variable for the current item (available to the code block)
+  -> SomeIndigoState ((IterOpElHs a) & inp)
+  -- ^ Code block to execute over each element of the container
+  -> IndigoState inp inp
+forEach container var body = IndigoState $ \md ->
+  let cde = gcCode $ usingIndigoState md (compileExpr container)
+      newMd = pushRefMd var md
+      bodyIndigoState = runSIS body newMd cleanGenCode
+  in GenCode (mdStack md) (cde # L.iter (bodyIndigoState # L.drop)) L.nop
 
 ----------------------------------------------------------------------------
 -- Documentation
 ----------------------------------------------------------------------------
 
 -- | Put a document item.
-doc :: DocItem di => di -> IndigoState s s ()
-doc di = IndigoState \md -> GenCode () md (L.doc di) L.nop
+doc :: DocItem di => di -> IndigoState s s
+doc di = IndigoState \md -> GenCode (mdStack md) (L.doc di) L.nop
 
 -- | Group documentation built in the given piece of code
--- into block dedicated to one thing, e.g. to one entrypoint.
-docGroup :: DocGrouping -> IndigoState i o () -> IndigoState i o ()
-docGroup gr ii = IndigoState $ \md ->
-  let GenCode _ mdii cd clr = runIndigoState ii md in
-  GenCode () mdii (L.docGroup gr cd) clr
+-- into a block dedicated to one thing, e.g. to one entrypoint.
+docGroup :: DocGrouping -> SomeIndigoState i -> SomeIndigoState i
+docGroup gr = overSIS $ \(GenCode md cd clr) -> SomeGenCode $
+  GenCode md (L.docGroup gr cd) clr
 
 -- | Insert documentation of the contract storage type. The type
 -- should be passed using type applications.
-docStorage :: forall storage s. TypeHasDoc storage => IndigoState s s ()
-docStorage = IndigoState \md -> GenCode () md (L.docStorage @storage) L.nop
+docStorage :: forall storage s. TypeHasDoc storage => IndigoState s s
+docStorage = IndigoState \md -> GenCode (mdStack md) (L.docStorage @storage) L.nop
 
--- | Give a name to given contract. Apply it to the whole contract code.
-contractName :: Text -> IndigoState i o () -> IndigoState i o ()
-contractName cName b = IndigoState $ \md ->
-  let GenCode _ mdb gc clr = runIndigoState b md in
-  GenCode () mdb (L.contractName cName gc) clr
+-- | Give a name to the given contract. Apply it to the whole contract code.
+contractName :: Text -> SomeIndigoState i -> SomeIndigoState i
+contractName cName = overSIS $ \(GenCode mdb gc clr) ->
+  SomeGenCode $ GenCode mdb (L.contractName cName gc) clr
 
--- | Attach general info to given contract.
-contractGeneral :: IndigoState i o () -> IndigoState i o ()
-contractGeneral b = IndigoState $ \md ->
-  let GenCode _ mdb gc clr = runIndigoState b md in
-  GenCode () mdb (L.contractGeneral gc) clr
+-- | Attach general info to the given contract.
+contractGeneral :: SomeIndigoState i -> SomeIndigoState i
+contractGeneral = overSIS $ \(GenCode mdb gc clr) ->
+  SomeGenCode $ GenCode mdb (L.contractGeneral gc) clr
 
 -- | Attach default general info to the contract documentation.
-contractGeneralDefault :: IndigoState s s ()
-contractGeneralDefault =
-  IndigoState \md -> GenCode () md L.contractGeneralDefault L.nop
+contractGeneralDefault :: IndigoState s s
+contractGeneralDefault = IndigoState \md -> GenCode (mdStack md) L.contractGeneralDefault L.nop
 
 -- | Indigo version for the function of the same name from Lorentz.
 finalizeParamCallingDoc
   :: (NiceParameterFull cp, RequireSumType cp, HasCallStack)
-  => (Var cp -> IndigoState (cp & inp) out x)
-  -> (Expr cp -> IndigoState inp out x)
-finalizeParamCallingDoc act param = IndigoState $ \md ->
-  let cde = gcCode $ runIndigoState (compileExpr param) md in
-  let (var, newMd) = pushRefMd md in
-  let GenCode x md1 cd clr = runIndigoState (act var) newMd in
-  GenCode x md1 (cde # L.finalizeParamCallingDoc cd) (clr # L.drop)
+  => Var cp
+  -> SomeIndigoState (cp & inp)
+  -> Expr cp
+  -> SomeIndigoState inp
+finalizeParamCallingDoc vc act param = SomeIndigoState $ \md ->
+  let cde = gcCode $ usingIndigoState md (compileExpr param)
+      newMd = pushRefMd vc md
+  in runSIS act newMd $ \(GenCode st1 cd clr) ->
+    SomeGenCode $ GenCode st1 (cde # L.finalizeParamCallingDoc cd) (clr # L.drop)
 
 ----------------------------------------------------------------------------
 -- Contract call
@@ -148,11 +166,12 @@
      , KnownValue (GetEntrypointArgCustom p mname)
      )
   => EntrypointRef mname
+  -> Var (ContractRef (GetEntrypointArgCustom p mname))
+  -- ^ Variable that will be assigned to the resulting 'ContractRef'
   -> IndigoState inp (ContractRef (GetEntrypointArgCustom p mname) & inp)
-                     (Var (ContractRef (GetEntrypointArgCustom p mname)))
-selfCalling epRef = do
+selfCalling epRef var = do
   nullaryOp (L.selfCalling @p epRef)
-  makeTopVar
+  assignTopVar var
 
 contractCalling
   :: forall cp inp epRef epArg addr.
@@ -161,11 +180,14 @@
      , ToT addr ~ ToT Address
      , KnownValue epArg
      )
-  => epRef -> Expr addr
-  -> IndigoState inp (Maybe (ContractRef epArg) & inp) (Var (Maybe (ContractRef epArg)))
-contractCalling epRef addr = do
+  => epRef
+  -> Expr addr
+  -> Var (Maybe (ContractRef epArg))
+  -- ^ Variable that will be assigned to the resulting 'ContractRef'
+  -> IndigoState inp (Maybe (ContractRef epArg) & inp)
+contractCalling epRef addr var = do
   unaryOp addr (L.contractCalling @cp epRef)
-  makeTopVar
+  assignTopVar var
 
 ----------------------------------------------------------------------------
 -- Side-effects
@@ -174,16 +196,28 @@
 transferTokens
   :: (NiceParameter p, HasSideEffects)
   => Expr p -> Expr Mutez -> Expr (ContractRef p)
-  -> IndigoState inp inp ()
-transferTokens ep em ec = do
-  MetaData s _ <- iget
+  -> IndigoState inp inp
+transferTokens ep em ec = withStackVars $ \s ->
   ternaryOpFlat ep em ec (L.transferTokens # varActionOperation s)
 
-setDelegate :: HasSideEffects => Expr (Maybe KeyHash) -> IndigoState inp inp ()
-setDelegate e =  do
-  MetaData s _ <- iget
+setDelegate :: HasSideEffects => Expr (Maybe KeyHash) -> IndigoState inp inp
+setDelegate e = withStackVars $ \s ->
   unaryOpFlat e (L.setDelegate # varActionOperation s)
 
+createContract
+  :: (HasSideEffects, NiceStorage s, NiceParameterFull p)
+  => L.Contract p s
+  -> Expr (Maybe KeyHash)
+  -> Expr Mutez
+  -> Expr s
+  -> Var Address
+  -- ^ Variable that will be assigned to the resulting 'Address'
+  -> IndigoState inp (Address & inp)
+createContract lCtr ek em es var = do
+  withStackVars $ \s ->
+    ternaryOp ek em es $ L.createContract lCtr # varActionOperation (NoRef :& s)
+  assignTopVar var
+
 ----------------------------------------------------------------------------
 -- Functions, Procedures and Scopes
 ----------------------------------------------------------------------------
@@ -214,13 +248,17 @@
 --   *[s]*
 -- @
 scope
-  :: forall a inp out . ScopeCodeGen a
-  => IndigoState inp out a
-  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
-scope f = IndigoState $ \md ->
-  let gc = runIndigoState f md in
-  finalizeStatement @a md (compileScope gc)
+  :: forall ret inp . ScopeCodeGen ret
+  => SomeIndigoState inp
+  -- ^ Code block to execute inside the scope
+  -> ret
+  -- ^ Return value(s) of the scoped code block
+  -> RetVars ret
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack ret ++ inp)
+scope f ret retVars = IndigoState $ \md@MetaData{..} ->
+  runSIS f md $ \fs -> finalizeStatement @ret mdStack retVars $ compileScope @ret mdObjects fs ret
 
 -- | Add a comment
-comment :: MT.CommentType -> IndigoState i i ()
-comment t = IndigoState $ \md -> GenCode () md (L.comment t) L.nop
+comment :: MT.CommentType -> IndigoState i i
+comment t = IndigoState $ \md -> GenCode (mdStack md) (L.comment t) L.nop
diff --git a/src/Indigo/Backend/Case.hs b/src/Indigo/Backend/Case.hs
--- a/src/Indigo/Backend/Case.hs
+++ b/src/Indigo/Backend/Case.hs
@@ -4,7 +4,7 @@
 
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
--- | High level statements of Indigo language.
+-- | Backend machinery for cases.
 
 module Indigo.Backend.Case
   ( caseRec
@@ -12,9 +12,8 @@
   , entryCaseSimpleRec
 
   , IndigoCaseClauseL
+  , IndigoClause (..)
   , CaseCommonF
-  , CaseCommon
-  , IndigoAnyOut (..)
   ) where
 
 import Data.Vinyl.Core (RMap(..))
@@ -35,49 +34,56 @@
 -- instruction, this wraps an Indigo value with the same input/output types.
 data IndigoCaseClauseL ret (param :: CaseClauseParam) where
   OneFieldIndigoCaseClauseL
-    :: (forall inp . MetaData inp -> CaseClauseL inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x)))
+    :: (forall inp .
+         MetaData inp
+      -> CaseClauseL inp (RetOutStack ret ++ inp) ('CaseClauseParam ctor ('OneField x)))
     -> IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x))
 
-data IndigoAnyOut x ret = forall retBranch .
-  ( ScopeCodeGen retBranch
-  , RetOutStack ret ~ RetOutStack retBranch
-  ) =>
-  IndigoAnyOut (forall inp . SomeIndigoState (x : inp) retBranch)
+data IndigoClause x ret where
+  IndigoClause
+    :: ( KnownValue x
+       , ScopeCodeGen retBr
+       , ret ~ RetExprs retBr
+       , RetOutStack ret ~ RetOutStack retBr
+       )
+    => Var x
+    -- ^ Variable for the clause input value (available to its code block)
+    -> (forall inp. SomeIndigoState (x : inp))
+    -- ^ Clause code block
+    -> retBr
+    -- ^ Clause return value(s)
+    -> IndigoClause x ret
 
 instance
-  ( name ~ AppendSymbol "c" ctor
-  , KnownValue x
-  )
+  (name ~ AppendSymbol "c" ctor, KnownValue x)
   =>
     CaseArrow
       name
-      (Var x -> IndigoAnyOut x ret)
+      (IndigoClause x ret)
       (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
   where
-    (/->) _ ind =
-      OneFieldIndigoCaseClauseL (\(md :: MetaData inp) ->
-        -- Create a reference to the top of stack
-        let (varCase, mdCaseBody) = pushRefMd md in
-        -- Pass the reference to the case body
-        case ind varCase of
-          IndigoAnyOut (SomeIndigoState body :: SomeIndigoState (x : inp) retBr) ->
-            case body mdCaseBody of
-              SomeGenCode gc ->
-                CaseClauseL $
-                  -- Compute returning expressions and clean up everything
-                  compileScope gc #
-                  -- Remove @x@ from the stack too
-                  liftClear' @(ClassifyReturnValue retBr) @retBr @(x & inp) @inp L.drop
-      )
+    (/->) _ (IndigoClause varCase sIndSt (ret :: retBr)) =
+      OneFieldIndigoCaseClauseL $ \md@MetaData{..} -> case sIndSt of
+        (SomeIndigoState body :: SomeIndigoState (x : inp)) ->
+          -- Create a reference to the top of stack
+          case body (pushRefMd varCase md) of
+            SomeGenCode gc ->
+              CaseClauseL $
+                -- Compute returning expressions and clean up everything
+                compileScope @retBr mdObjects gc ret #
+                -- Remove @x@ from the stack too
+                liftClear @retBr @inp @(x : inp) L.drop
 
--- This constraint is shared by all @case*@ functions.
+-- | This constraint is shared by all @case*@ functions.
+-- Including some outside this module.
 type CaseCommonF f dt ret clauses =
-     ( InstrCaseC dt
-     , RMap (CaseClauses dt)
-     , clauses ~ Rec (f ret) (CaseClauses dt)
-     , ScopeCodeGen ret
-     )
+  ( InstrCaseC dt
+  , RMap (CaseClauses dt)
+  , clauses ~ Rec (f ret) (CaseClauses dt)
+  , ScopeCodeGen ret
+  )
 
+-- | This constraint is shared by all backend @case*@ functions.
 type CaseCommon dt ret clauses = CaseCommonF IndigoCaseClauseL dt ret clauses
 
 -- | A case statement for indigo. See examples for a sample usage.
@@ -85,10 +91,12 @@
   :: forall dt inp ret clauses . CaseCommon dt ret clauses
   => Expr dt
   -> clauses
-  -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
-caseRec g cls = IndigoState $ \md ->
-  let cdG = gcCode $ runIndigoState (compileExpr g) md in
-  finalizeStatement @ret md (cdG # L.case_ (toCaseClauseL md cls))
+  -> RetVars ret
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack ret ++ inp)
+caseRec g cls vars = IndigoState $ \md ->
+  let cdG = gcCode $ usingIndigoState md (compileExpr g) in
+  finalizeStatement @ret (mdStack md) vars (cdG # L.case_ (toCaseClauseL md cls))
 
 -- | 'case_' for pattern-matching on parameter.
 entryCaseRec
@@ -99,25 +107,29 @@
   => Proxy entrypointKind
   -> Expr dt
   -> clauses
-  -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
-entryCaseRec proxy g cls = IndigoState $ \md ->
-  let cdG = gcCode $ runIndigoState (compileExpr g) md in
-  finalizeStatement @ret md (cdG # L.entryCase_ proxy (toCaseClauseL md cls))
+  -> RetVars ret
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack ret ++ inp)
+entryCaseRec proxy g cls vars = IndigoState $ \md ->
+  let cdG = gcCode $ usingIndigoState md (compileExpr g) in
+  finalizeStatement @ret (mdStack md) vars(cdG # L.entryCase_ proxy (toCaseClauseL md cls))
 
 -- | 'entryCase_' for contracts with flat parameter.
 entryCaseSimpleRec
-  :: forall cp inp ret clauses .
-     ( CaseCommon cp ret clauses
-     , DocumentEntrypoints PlainEntrypointsKind cp
-     , NiceParameterFull cp
-     , RequireFlatParamEps cp
+  :: forall dt inp ret clauses .
+     ( CaseCommon dt ret clauses
+     , DocumentEntrypoints PlainEntrypointsKind dt
+     , NiceParameterFull dt
+     , RequireFlatParamEps dt
      )
-  => Expr cp
+  => Expr dt
   -> clauses
-  -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
-entryCaseSimpleRec g cls = IndigoState $ \md ->
-  let cdG = gcCode $ runIndigoState (compileExpr g) md in
-  finalizeStatement @ret md (cdG # L.entryCaseSimple_ (toCaseClauseL md cls))
+  -> RetVars ret
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack ret ++ inp)
+entryCaseSimpleRec g cls vars = IndigoState $ \md ->
+  let cdG = gcCode $ usingIndigoState md (compileExpr g) in
+  finalizeStatement @ret (mdStack md) vars (cdG # L.entryCaseSimple_ (toCaseClauseL md cls))
 
 toCaseClauseL
   :: forall inp ret cs .
diff --git a/src/Indigo/Backend/Conditional.hs b/src/Indigo/Backend/Conditional.hs
--- a/src/Indigo/Backend/Conditional.hs
+++ b/src/Indigo/Backend/Conditional.hs
@@ -4,7 +4,7 @@
 
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
--- | Conditional statements of Indigo language.
+-- | Backend conditional statements of Indigo
 
 module Indigo.Backend.Conditional
   ( if_
@@ -44,87 +44,134 @@
 -- | If statement. All variables created inside its branches will be released
 -- after the execution leaves the scope in which they were created.
 if_
-  :: forall inp xs ys a b . IfConstraint a b
+  :: forall inp a b . IfConstraint a b
   => Expr Bool
-  -> IndigoState inp xs a
-  -> IndigoState inp ys b
-  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
-if_ e t f = IndigoState $ \md ->
-  let cde = gcCode $ runIndigoState (compileExpr e) md in
-  let gc1 = runIndigoState t md in
-  let gc2 = runIndigoState f md in
-  finalizeStatement @a md (cde # L.if_ (compileScope gc1) (compileScope gc2))
+  -- ^ Expression for the control flow
+  -> SomeIndigoState inp
+  -- ^ Code block for the positive branch
+  -> a
+  -- ^ Return value(s) of the positive branch
+  -> SomeIndigoState inp
+  -- ^ Code block for the negative branch
+  -> b
+  -- ^ Return value(s) of the negative branch
+  -> RetVars a
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack a ++ inp)
+if_ e t retA f retB retVars = IndigoState $ \md@MetaData{..} ->
+  let cde = gcCode $ usingIndigoState md (compileExpr e) in
+  runSIS t md $ \gc1 ->
+    runSIS f md $ \gc2 ->
+      finalizeStatement @a mdStack retVars $
+        cde # L.if_ (compileScope @a mdObjects gc1 retA) (compileScope @b mdObjects gc2 retB)
 
 -- | If which works like case for Maybe.
 ifSome
-  :: forall inp xs ys x a b . (IfConstraint a b, KnownValue x)
+  :: forall inp x a b . (IfConstraint a b, KnownValue x)
   => Expr (Maybe x)
-  -> (Var x -> IndigoState (x & inp) xs a)
-  -> IndigoState inp ys b
-  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
-ifSome e t f = IndigoState $ \md ->
-  let cde = gcCode $ runIndigoState (compileExpr e) md in
-  let (v, mdJust) = pushRefMd md in
-  let gc1 = runIndigoState (t v) mdJust in
-  let gc2 = runIndigoState f md in
-  finalizeStatement @a md $
-    cde #
-    L.ifSome
-      ( compileScope gc1 #
-       -- after this we have stack (e1 & e2 .. & ek & x & inp)
-       liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop
-       -- this can be lifted together with glClear code, but let's leave it like this for now
-      )
-      (compileScope gc2)
+  -- ^ Expression for the control flow
+  -> Var x
+  -- ^ Variable for the 'Just' value (available to the next code block)
+  -> SomeIndigoState (x & inp)
+  -- ^ Code block for the 'Just' branch
+  -> a
+  -- ^ Return value(s) of the 'Just' branch
+  -> SomeIndigoState inp
+  -- ^ Code block for the 'Nothing' branch
+  -> b
+  -- ^ Return value(s) of the 'Nothing' branch
+  -> RetVars a
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack a ++ inp)
+ifSome e varX t retA f retB retVars = IndigoState $ \md@MetaData{..} ->
+  let cde = gcCode $ usingIndigoState md (compileExpr e) in
+  let mdJust = pushRefMd varX md in
+  runSIS t mdJust $ \gc1 ->
+    runSIS f md $ \gc2 ->
+      finalizeStatement @a mdStack retVars $
+        cde #
+        L.ifSome
+          ( compileScope @a mdObjects gc1 retA #
+            -- after this we have stack (e1 & e2 .. & ek & x & inp)
+            liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop
+            -- this can be lifted together with glClear code, but let's leave it like this for now
+          )
+          (compileScope @b mdObjects gc2 retB)
 
 -- | If which works like case for Either.
 ifRight
-  :: forall inp xs ys x y a b . (IfConstraint a b, KnownValue x, KnownValue y)
-  => Expr (Either y x)
-  -> (Var x -> IndigoState (x & inp) xs a)
-  -> (Var y -> IndigoState (y & inp) ys b)
-  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
-ifRight e r l = IndigoState $ \md ->
+  :: forall inp r l a b . (IfConstraint a b, KnownValue r, KnownValue l)
+  => Expr (Either l r)
+  -- ^ Expression for the control flow
+  -> Var r
+  -- ^ Variable for the 'Right' value (available to the next code block)
+  -> SomeIndigoState (r & inp)
+  -- ^ Code block for the 'Right' branch
+  -> a
+  -- ^ Return value(s) of the 'Right' branch
+  -> Var l
+  -- ^ Variable for the 'Left' value (available to the next code block)
+  -> SomeIndigoState (l & inp)
+  -- ^ Code block for the 'Left' branch
+  -> b
+  -- ^ Return value(s) of the 'Left' branch
+  -> RetVars a
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack a ++ inp)
+ifRight e varR r retA varL l retB retVars = IndigoState $ \md@MetaData{..} ->
   let
-    cde = gcCode $ runIndigoState (compileExpr e) md
-    (v, mdRight) = pushRefMd md
-    (w, mdLeft) = pushRefMd md
-    gc1 = runIndigoState (r v) mdRight
-    gc2 = runIndigoState (l w) mdLeft
+    cde = gcCode $ usingIndigoState md (compileExpr e)
+    mdRight = pushRefMd varR md
+    mdLeft = pushRefMd varL md
   in
-    finalizeStatement @a md $
-      cde #
-      L.ifRight
-        ( compileScope gc1 #
-        -- after this we have stack (e1 & e2 .. & ek & x & inp)
-        liftClear' @(ClassifyReturnValue a) @a @(x & inp) @inp L.drop
-        -- this can be lifted together with glClear code, but let's leave it like this for now
-        )
-        ( compileScope gc2 #
-        -- after this we have stack (e1 & e2 .. & ek & x & inp)
-        liftClear' @(ClassifyReturnValue b) @b @(y & inp) @inp L.drop
-        -- this can be lifted together with glClear code, but let's leave it like this for now
-        )
+    runSIS r mdRight $ \gc1 ->
+      runSIS l mdLeft $ \gc2 ->
+        finalizeStatement @a mdStack retVars $
+          cde #
+          L.ifRight
+            ( compileScope @a mdObjects gc1 retA #
+            -- after this we have stack (e1 & e2 .. & ek & x & inp)
+            liftClear' @(ClassifyReturnValue a) @a @(r & inp) @inp L.drop
+            -- this can be lifted together with glClear code, but let's leave it like this for now
+            )
+            ( compileScope @b mdObjects gc2 retB #
+            -- after this we have stack (e1 & e2 .. & ek & x & inp)
+            liftClear' @(ClassifyReturnValue b) @b @(l & inp) @inp L.drop
+            -- this can be lifted together with glClear code, but let's leave it like this for now
+            )
 
+-- | If which works like uncons for lists.
 ifCons
-  :: forall inp xs ys x a b . (IfConstraint a b, KnownValue x)
+  :: forall inp x a b . (IfConstraint a b, KnownValue x)
   => Expr (List x)
-  -> (Var x -> Var (List x) -> IndigoState (x & List x & inp) xs a)
-  -> IndigoState inp ys b
-  -> IndigoState inp (RetOutStack a ++ inp) (RetVars a)
-ifCons e t f = IndigoState $ \md ->
+  -- ^ Expression for the control flow
+  -> Var x
+  -- ^ Variable for the "head" value (available to the next code block)
+  -> Var (List x)
+  -- ^ Variable for the "tail" value (available to the next code block)
+  -> SomeIndigoState (x & List x & inp)
+  -- ^ Code block for the non-empty list branch
+  -> a
+  -- ^ Return value(s) of the non-empty list branch
+  -> SomeIndigoState inp
+  -- ^ Code block for the empty list branch
+  -> b
+  -- ^ Return value(s) of the empty list branch
+  -> RetVars a
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> IndigoState inp (RetOutStack a ++ inp)
+ifCons e vx vlx t retA f retB retVars = IndigoState $ \md@MetaData{..} ->
   let
-    cde = gcCode $ runIndigoState (compileExpr e) md
-    (l, mdList) = pushRefMd md
-    (v, mdVal) = pushRefMd mdList
-    gc1 = runIndigoState (t v l) mdVal
-    gc2 = runIndigoState f md
+    cde = gcCode $ usingIndigoState md (compileExpr e)
+    mdList = pushRefMd vlx md
+    mdVal = pushRefMd vx mdList
   in
-    finalizeStatement @a md $
-      cde #
-      L.ifCons
-        ( compileScope gc1 #
-          liftClear' @(ClassifyReturnValue a) @a @(x & List x & inp) @inp (L.drop # L.drop)
-        )
-        (compileScope gc2)
-
+    runSIS t mdVal $ \gc1 ->
+      runSIS f md $ \gc2 ->
+        finalizeStatement @a mdStack retVars $
+          cde #
+          L.ifCons
+            ( compileScope @a mdObjects gc1 retA #
+              liftClear' @(ClassifyReturnValue a) @a @(x & List x & inp) @inp (L.drop # L.drop)
+            )
+            (compileScope @b mdObjects gc2 retB)
diff --git a/src/Indigo/Backend/Error.hs b/src/Indigo/Backend/Error.hs
--- a/src/Indigo/Backend/Error.hs
+++ b/src/Indigo/Backend/Error.hs
@@ -4,7 +4,7 @@
 
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
--- | Error related statements of Indigo language.
+-- | Backend failing statements of Indigo.
 
 module Indigo.Backend.Error
   ( failWith
@@ -12,16 +12,8 @@
   , failCustom
   , failCustom_
   , failUnexpected_
-  , assert
-  , assertSome
-  , assertNone
-  , assertRight
-  , assertLeft
-  , assertCustom
-  , assertCustom_
   ) where
 
-import Indigo.Backend.Conditional
 import Indigo.Backend.Prelude
 import Indigo.Internal.Expr.Compilation
 import Indigo.Internal.Expr.Types
@@ -30,97 +22,42 @@
 import qualified Lorentz.Errors as L
 import qualified Lorentz.Instr as L
 
-failIndigoState :: inp :-> out -> IndigoState inp out r
-failIndigoState code = iput $ GenCode errOut errMd code failCl
+-- | Generic generator of failing 'IndigoState' from failing Lorentz instructions.
+failIndigoState :: inp :-> out -> IndigoState inp out
+failIndigoState gcCode = iput $ GenCode {..}
   where
     -- note: here we can use errors for the output and MetaData, because they
     -- are lazy field of GenCode and, due to the way # combines the generated
     -- code (ignores everything following a failWith) they won't actually ever
     -- be accessed again. The same goes for the "cleaning" code, except it is
     -- not lazy and needs to typecheck, so we have to use `failWith` again.
-    msg = " is undefined after a failing instruction"
-    errOut = error $ "Output" <> msg
-    errMd = error $ "MetaData" <> msg
-    failCl = L.unit # L.failWith
+    gcStack = error $ "StackVars is undefined after a failing instruction"
+    gcClear = L.unit # L.failWith
 
-failWith :: KnownValue a => Expr a -> IndigoState s t r
+failWith :: KnownValue a => Expr a -> IndigoState s t
 failWith exa = compileExpr exa >> failIndigoState L.failWith
 
-failUsing_ :: (IsError x) => x -> IndigoState s t r
+failUsing_ :: (IsError x) => x -> IndigoState s t
 failUsing_ x = failIndigoState (failUsing x)
 
 failCustom
-  :: forall tag err s t r.
+  :: forall tag err s t.
      ( err ~ ErrorArg tag
      , CustomErrorHasDoc tag
      , NiceConstant err
      )
-  => Label tag -> Expr err -> IndigoState s t r
+  => Label tag -> Expr err -> IndigoState s t
 failCustom l errEx = withDict (niceConstantEvi @err) $ do
   compileExpr errEx
   failIndigoState $ L.failCustom l
 
 failCustom_
-  :: forall tag s t r notVoidErrorMsg.
+  :: forall tag s t notVoidErrorMsg.
      ( RequireNoArgError tag notVoidErrorMsg
      , CustomErrorHasDoc tag
      )
-  => Label tag -> IndigoState s t r
+  => Label tag -> IndigoState s t
 failCustom_ = failIndigoState . L.failCustom_
 
-failUnexpected_ :: MText -> IndigoState s t r
+failUnexpected_ :: MText -> IndigoState s t
 failUnexpected_ msg = failUsing_ $ [mt|Unexpected: |] <> msg
-
-assert
-  :: forall s x. IsError x
-  => x -> Expr Bool -> IndigoState s s ()
-assert err e = if_ (toExpr e) (return ()) (failUsing_ err :: IndigoState s s ())
-
-assertSome
-  :: forall x s err. (IsError err, KnownValue x)
-  => err -> Expr (Maybe x) -> IndigoState s s ()
-assertSome err ex =
-  ifSome ex
-    (\_ -> failUsing_ err :: IndigoState (x & s) s ())
-    (return ())
-
-assertNone
-  :: forall x s err. (IsError err, KnownValue x)
-  => err -> Expr (Maybe x) -> IndigoState s s ()
-assertNone err ex =
-  ifSome ex
-    (\_ -> return ())
-    (failUsing_ err :: IndigoState s s ())
-
-assertRight
-  :: forall x y s err. (IsError err, KnownValue x, KnownValue y)
-  => err -> Expr (Either y x) -> IndigoState s s ()
-assertRight err ex =
-  ifRight ex
-    (\_ -> failUsing_ err :: IndigoState (x & s) s ())
-    (\_ -> return ())
-
-assertLeft
-  :: forall x y s err. (IsError err, KnownValue x, KnownValue y)
-  => err -> Expr (Either y x) -> IndigoState s s ()
-assertLeft err ex =
-  ifRight ex
-    (\_ -> return ())
-    (\_ -> failUsing_ err :: IndigoState (y & s) s ())
-
-assertCustom
-  :: forall tag err s.
-     ( err ~ ErrorArg tag
-     , CustomErrorHasDoc tag
-     , NiceConstant err
-     )
-  => Label tag -> Expr err -> Expr Bool -> IndigoState s s ()
-assertCustom tag errEx e = if_ (toExpr e) (return ()) (failCustom tag errEx :: IndigoState s s ())
-
-assertCustom_
-  :: forall tag s notVoidErrorMsg.
-     ( RequireNoArgError tag notVoidErrorMsg
-     , CustomErrorHasDoc tag
-     )
-  => Label tag -> Expr Bool -> IndigoState s s ()
-assertCustom_ tag e = if_ (toExpr e) (return ()) (failCustom_ tag :: IndigoState s s ())
diff --git a/src/Indigo/Backend/Lambda.hs b/src/Indigo/Backend/Lambda.hs
--- a/src/Indigo/Backend/Lambda.hs
+++ b/src/Indigo/Backend/Lambda.hs
@@ -5,30 +5,23 @@
 -- | This module implements the ability to put
 -- Indigo computations on the stack as a lambda and execute them.
 module Indigo.Backend.Lambda
-  ( LambdaPure1
-  , createLambdaPure1
+  ( LambdaKind (..)
+  , withLambdaKind
+  , executeLambda1
+  , initLambdaStackVars
+
+  -- * Functionality for Frontend
   , CreateLambdaPure1C
-  , executeLambdaPure1
   , ExecuteLambdaPure1C
-  , initMetaDataPure
-
-  , Lambda1
-  , createLambda1
   , CreateLambda1C
-  , executeLambda1
   , ExecuteLambda1C
-  , initMetaData
-
-  , LambdaEff1
-  , createLambdaEff1
   , CreateLambdaEff1C
-  , executeLambdaEff1
   , ExecuteLambdaEff1C
-  , initMetaDataEff
 
+  -- * Functionality for Sequential
+  , CreateLambda1CGeneric
+  , createLambda1Generic
   , Lambda1Generic
-  , LambdaExecutor
-  , LambdaCreator
   ) where
 
 import Data.Constraint (Dict(..))
@@ -36,53 +29,108 @@
 import Indigo.Backend.Prelude
 import Indigo.Backend.Scope
 import Indigo.Backend.Var
-import Indigo.Internal
+import Indigo.Internal hiding ((+), (<>))
 import Indigo.Lorentz
 import qualified Lorentz.Instr as L
 import Lorentz.Zip (ZipInstr, ZippedStack)
 import Util.Type (type (++), KnownList, listOfTypesConcatAssociativityAxiom)
 
 ----------------------------------------------------------------------------
--- Pure lambdas
+-- External interface
 ----------------------------------------------------------------------------
 
-type LambdaPure1 arg res = Lambda1Generic '[] arg res
+-- | Describes kind of lambda: pure, modifying storage, effectfull
+data LambdaKind st arg res extra where
+  PureLambda ::
+    (ExecuteLambdaPure1C arg res, CreateLambda1CGeneric '[] arg res, Typeable res)
+    => LambdaKind st arg res '[]
+  StorageLambda ::
+    (ExecuteLambda1C st arg res, CreateLambda1CGeneric '[st] arg res, Typeable res)
+    => Proxy st
+    -> LambdaKind st arg res '[st]
+  EffLambda
+    :: (ExecuteLambdaEff1C st arg res, CreateLambda1CGeneric '[st, Ops] arg res, Typeable res)
+    => Proxy st
+    -> LambdaKind st arg res '[st, Ops]
 
-type CreateLambdaPure1C arg res = CreateLambda1CGeneric '[] arg res
+-- | Provide common constraints that are presented in all constructors of 'LambdaKind'
+withLambdaKind
+  :: LambdaKind st arg res extra
+  -> ((ScopeCodeGen res, KnownValue arg, Typeable res, CreateLambda1CGeneric extra arg res) => r)
+  -> r
+withLambdaKind PureLambda r = r
+withLambdaKind (StorageLambda _) r = r
+withLambdaKind (EffLambda _) r = r
 
--- | Create a lambda, that takes only one argument, from the given computation.
--- The lambda is not allowed to modify storage and emit operations.
-createLambdaPure1
-  :: forall res arg inp out . CreateLambdaPure1C arg res
-  => LambdaCreator '[] arg res inp out
-createLambdaPure1 = createLambda1Generic initMetaDataPure
+-- | Execute lambda depending on its 'LambdaKind'
+executeLambda1
+  :: forall res st arg extra inp .
+  LambdaKind st arg res extra -> RefId -> RetVars res -> LambdaExecutor extra arg res inp
+executeLambda1 PureLambda _ retVars = executeLambdaPure1 @res retVars
+executeLambda1 (StorageLambda _) refId retVars = executeLambdaSt1 @res refId retVars
+executeLambda1 (EffLambda _) refId retVars = executeLambdaEff1 @res refId retVars
 
+-- | Create initial stack vars depending on 'LambdaKind'
+initLambdaStackVars :: LambdaKind st arg res extra -> Var arg -> StackVars (arg & extra)
+initLambdaStackVars PureLambda = initStackVarsPure
+initLambdaStackVars (StorageLambda _) = initStackVars
+initLambdaStackVars (EffLambda _) = initStackVarsEff
+
+type Lambda1Generic extra arg res = (arg & extra) :-> (RetOutStack res ++ extra)
+
+type CreateLambda1CGeneric extra arg res =
+  ( ScopeCodeGen res, KnownValue arg, Typeable extra
+  , ZipInstr (arg & extra)
+  , KnownValue (ZippedStack (arg ': extra))
+  , KnownValue (ZippedStack (RetOutStack res ++ extra))
+  , ZipInstr (RetOutStack res ++ extra)
+  , Typeable (RetOutStack res ++ extra)
+  )
+
+-- | Create a lambda, that takes only one argument, from the given computation,
+-- and return a variable referring to this lambda.
+createLambda1Generic
+  :: forall arg res extra inp . CreateLambda1CGeneric extra arg res
+  => Var (Lambda1Generic extra arg res)
+  -> res
+  -> StackVars (arg & extra)
+  -> SomeIndigoState (arg & extra)
+  -> IndigoState inp (Lambda1Generic extra arg res & inp)
+createLambda1Generic var ret initMd act = IndigoState $ \MetaData{..} ->
+  -- Decomposed objects are passed as mempty here because in the lambda
+  -- we don't decompose storage value (but we might be doing it as an optimisation)
+  -- so we just have it as an stack cell
+  runSIS act (MetaData initMd mempty) $ \gc ->
+    let gcStack = pushRef var mdStack
+        gcCode = L.lambda (compileScope mdObjects gc ret # liftClear @res @extra @(arg & extra) L.drop)
+        gcClear = L.drop
+    in GenCode {..}
+
+----------------------------------------------------------------------------
+-- Pure lambdas
+----------------------------------------------------------------------------
+
+type CreateLambdaPure1C arg res = CreateLambda1CGeneric '[] arg res
+
 type ExecuteLambdaPure1C arg res = ExecuteLambda1CGeneric '[] arg res
 
 -- | Execute a lambda, which accepts only one argument, on passed expression.
 executeLambdaPure1
-  :: forall res arg inp . ExecuteLambdaPure1C arg res
-  => LambdaExecutor '[] arg res inp
-executeLambdaPure1 = executeLambda1Generic @res (return ())
+  :: forall res arg inp. ExecuteLambdaPure1C arg res
+  => RetVars res
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> LambdaExecutor '[] arg res inp
+executeLambdaPure1 retVars = executeLambda1Generic @res retVars nopState
 
-initMetaDataPure :: KnownValue arg => (Var arg, MetaData '[arg])
-initMetaDataPure = let v = Cell 0 in (v, MetaData (Ref 0 :& RNil) 1)
+initStackVarsPure :: KnownValue arg => Var arg -> StackVars '[arg]
+initStackVarsPure var = pushRef var emptyStack
 
 ----------------------------------------------------------------------------
 -- Impure lambda (modifying storage only)
 ----------------------------------------------------------------------------
 
-type Lambda1 st arg res = Lambda1Generic '[st] arg res
-
 type CreateLambda1C st arg res = (KnownValue st, CreateLambda1CGeneric '[st] arg res)
 
--- | Create a lambda, that takes only one argument, from the given computation.
--- The lambda is not allowed to emit operations.
-createLambda1
-  :: forall st res arg inp out . CreateLambda1C st arg res
-  => LambdaCreator '[st] arg res inp out
-createLambda1 = createLambda1Generic initMetaData
-
 type ExecuteLambda1C st arg res =
   ( IsObject st
   , HasStorage st
@@ -90,45 +138,40 @@
   )
 
 -- | Execute a lambda that accepts only one argument on the given expression.
-executeLambda1
-  :: forall st res arg inp . ExecuteLambda1C st arg res
-  => LambdaExecutor '[st] arg res inp
-executeLambda1 =
-  executeLambda1Generic @res
-    -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage.
-    -- This is pretty expensive operation and it has to be fixed:
-    -- we have to materialise only fields used in the lambda
-    (IndigoState $ \md ->
-      let GenCode _ newMd alloc _ = usingIndigoState md $ compileExpr (V (storageVar @st)) in
-      let GenCode _ _ cleanup _   = usingIndigoState newMd (makeTopVar >>= (setVar (storageVar @st) . V)) in
-      GenCode () newMd alloc (cleanup # L.drop)
-    )
+executeLambdaSt1
+  :: forall res st arg inp. ExecuteLambda1C st arg res
+  => RefId
+  -> RetVars res
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> LambdaExecutor '[st] arg res inp
+executeLambdaSt1 nextRef retVars = executeLambda1Generic @res retVars $
+    IndigoState $ \md ->
+      let storage = storageVar @st
+          -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage.
+          -- This is pretty expensive operation and it has to be fixed:
+          -- we have to materialise only fields used in the lambda
+          GenCode gcStack fetchCode _ = usingIndigoState md $ compileExpr (V storage)
+          tmpVar = Var nextRef
+          gcClear = gcCode (usingIndigoState (pushRefMd tmpVar md) $
+                              setVar (nextRef + 1) storage (V tmpVar))
+                    # L.drop
+      in GenCode {gcCode=fetchCode,..}
 
-initMetaData :: (KnownValue arg, KnownValue st) => (Var arg, MetaData '[arg, st])
-initMetaData =
-  -- This numeration is intentional.
-  -- We have to provide HasStorage for a lambda.
+
+initStackVars :: (HasStorage st, KnownValue arg) => Var arg -> StackVars '[arg, st]
+initStackVars var = emptyStack
+  & pushRef storageVar
+  & pushRef var
+  -- This 'storageVar' usage is intentional.
+  -- We have to provide 'HasStorage' for a lambda.
   -- To avoid excessive 'given' calls with new indexes,
-  -- we just refer to storage variable with the same index.
-  let argm = Cell 2 in
-  (argm, MetaData (Ref 2 :& Ref 1 :& RNil) 3)
 
 ----------------------------------------------------------------------------
 -- Lambda with side effects (might emit operations)
 ----------------------------------------------------------------------------
 
-type LambdaEff1 st arg res = Lambda1Generic '[st, Ops] arg res
-
 type CreateLambdaEff1C st arg res = (KnownValue st, CreateLambda1CGeneric '[st, Ops] arg res)
 
--- | Create a lambda, that takes only one argument, from the given computation,
--- and return a variable referring to this lambda.
--- The lambda is allowed to modify storage and emit operations.
-createLambdaEff1
-  :: forall st res arg inp out . CreateLambdaEff1C st arg res
-  => LambdaCreator '[st, Ops] arg res inp out
-createLambdaEff1 = createLambda1Generic initMetaDataEff
-
 type ExecuteLambdaEff1C st arg res =
   ( HasStorage st
   , HasSideEffects
@@ -139,65 +182,43 @@
 -- | Execute a lambda that accepts only one argument on the given expression.
 -- Also updates the storage and operations with the values returned from the lambda.
 executeLambdaEff1
-  :: forall st res arg inp . ExecuteLambdaEff1C st arg res
-  => LambdaExecutor '[st, Ops] arg res inp
-executeLambdaEff1 =
-  executeLambda1Generic @res
+  :: forall res st arg inp. ExecuteLambdaEff1C st arg res
+  => RefId
+  -> RetVars res
+  -- ^ Variable(s) that will be assigned to the resulting value(s)
+  -> LambdaExecutor '[st, Ops] arg res inp
+executeLambdaEff1 nextRef retVars =
+  executeLambda1Generic @res retVars $
     -- TODO this @compileExpr (V (storageVar @st))@ call materialises the whole decomposed storage.
     -- This is pretty expensive operation and it has to be fixed:
     -- we have to materialise only fields used in the lambda
-    (IndigoState $ \md ->
-      let GenCode _ newMd alloc _ =
-              usingIndigoState md (do
-                  compileExpr (V operationsVar)
-                  compileExpr (V (storageVar @st))) in
-      let (newStoreVar, newMdStore) = pushRefMd (pushNoRefMd md) in
-      let (newOpsVar, newMdOps) = pushRefMd md in
-      let cleanup =
-            gcCode (usingIndigoState newMdStore $ setVar (storageVar @st) (V newStoreVar)) #
-            L.drop #
-            gcCode (usingIndigoState newMdOps $ setVar operationsVar (V newOpsVar)) #
-            L.drop
-      in GenCode () newMd alloc cleanup
-    )
+    IndigoState $ \MetaData{..} ->
+      let storage = storageVar @st
+          ops@(Var opsRefId) = operationsVar
+          gcStack = pushRef storage $ pushRef ops mdStack
+          fetchCode =
+            varActionGet opsRefId mdStack #
+            (gcCode $ usingIndigoState (MetaData sPlus mdObjects) $ compileExpr (V storage))
+          sPlus = NoRef :& mdStack
+          tmpVar = Var nextRef
+          setStorage = gcCode (usingIndigoState (MetaData (pushRef tmpVar sPlus) mdObjects) $
+                                 setVar (nextRef + 1) storage (V tmpVar))
+                       # L.drop
+          gcClear = setStorage # varActionSet opsRefId mdStack
+      in GenCode {gcCode=fetchCode,..}
 
-initMetaDataEff :: (KnownValue arg, KnownValue st) => (Var arg, MetaData '[arg, st, Ops])
-initMetaDataEff =
-  let argm = Cell 2 in
-  (argm, MetaData (Ref 2 :& Ref 1 :& Ref 0 :& RNil) 3)
+initStackVarsEff
+  :: (HasSideEffects, HasStorage st, KnownValue arg)
+  => Var arg -> StackVars '[arg, st, Ops]
+initStackVarsEff var = emptyStack
+  & pushRef operationsVar
+  & pushRef storageVar
+  & pushRef var
 
 ----------------------------------------------------------------------------
--- Common lambda functionality
+-- Generic functionality of lambda execution
 ----------------------------------------------------------------------------
 
-type Lambda1Generic extra arg res = (arg & extra) :-> (RetOutStack res ++ extra)
-
-type CreateLambda1CGeneric extra arg res =
-  ( ScopeCodeGen res, KnownValue arg, Typeable extra
-  , ZipInstr (arg & extra)
-  , KnownValue (ZippedStack (arg ': extra))
-  , KnownValue (ZippedStack (RetOutStack res ++ extra))
-  , ZipInstr (RetOutStack res ++ extra)
-  , Typeable (RetOutStack res ++ extra)
-  )
-
-type LambdaCreator extra arg res inp out
-  = (Var arg -> IndigoState (arg & extra) out res)
-  -> IndigoState inp (Lambda1Generic extra arg res & inp) (Var (Lambda1Generic extra arg res))
-
--- | Create a lambda, that takes only one argument, from the given computation,
--- and return a variable referring to this lambda.
-createLambda1Generic
-  :: forall arg res extra inp out . CreateLambda1CGeneric extra arg res
-  => (Var arg, MetaData (arg & extra))
-  -> (Var arg -> IndigoState (arg & extra) out res)
-  -> IndigoState inp (Lambda1Generic extra arg res & inp) (Var (Lambda1Generic extra arg res))
-createLambda1Generic (varArg, initMd) act = IndigoState $ \md ->
-  let gc = runIndigoState (act varArg) initMd in
-  let (var, md1) = pushRefMd md in
-  GenCode var md1 (L.lambda (compileScope gc # liftClear @res @extra @(arg & extra) L.drop)) L.drop
-
-
 type ExecuteLambda1CGeneric extra arg res =
   ( ScopeCodeGen res, KnownValue arg
   , KnownValue ((arg & extra) :-> (RetOutStack res ++ extra))
@@ -210,24 +231,25 @@
   )
 
 type LambdaExecutor extra arg res inp
-  = Var (Lambda1Generic extra arg res)
+   = Var (Lambda1Generic extra arg res)
   -> Expr arg
-  -> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
+  -> IndigoState inp (RetOutStack res ++ inp)
 
 -- | Execute a lambda that accepts only one argument on the given expression.
 -- Also updates the storage and operations with the values returned from the lambda.
 executeLambda1Generic
   :: forall res arg extra inp . ExecuteLambda1CGeneric extra arg res
-  => IndigoState inp (extra ++ inp) ()
+  => RetVars res
+  -> IndigoState inp (extra ++ inp)
   -> Var (Lambda1Generic extra arg res)
   -> Expr arg
-  -> IndigoState inp (RetOutStack res ++ inp) (RetVars res)
-executeLambda1Generic allocateCleanup varF argm = IndigoState $ \md ->
-  let GenCode _ allocMd allocate cleanup = runIndigoState allocateCleanup md in
+  -> IndigoState inp (RetOutStack res ++ inp)
+executeLambda1Generic vars allocateCleanup varF argm = IndigoState $ \md@MetaData{..} ->
+  let GenCode allocStk allocate cleanup = usingIndigoState md allocateCleanup in
   let getArgs =
         allocate #
         (gcCode $
-          usingIndigoState allocMd $ do
+          usingIndigoState (MetaData allocStk mdObjects) $ do
               compileExpr argm
               compileExpr (V varF)) in
   case listOfTypesConcatAssociativityAxiom @(RetOutStack res) @extra @inp of
@@ -235,4 +257,4 @@
       let code = getArgs #
                  L.execute @_ @_ @inp #
                  liftClear @res cleanup
-      in finalizeStatement @res md code
+      in finalizeStatement @res mdStack vars code
diff --git a/src/Indigo/Backend/Prelude.hs b/src/Indigo/Backend/Prelude.hs
--- a/src/Indigo/Backend/Prelude.hs
+++ b/src/Indigo/Backend/Prelude.hs
@@ -11,4 +11,4 @@
   ( module Prelude
   ) where
 
-import Prelude hiding ((>>), (>>=), (=<<), return)
+import Prelude hiding ((>>))
diff --git a/src/Indigo/Backend/Scope.hs b/src/Indigo/Backend/Scope.hs
--- a/src/Indigo/Backend/Scope.hs
+++ b/src/Indigo/Backend/Scope.hs
@@ -46,8 +46,8 @@
 
 import Indigo.Backend.Prelude
 import Indigo.Internal.Expr
-import Indigo.Internal.Object
 import Indigo.Internal.State
+import Indigo.Internal.Var
 import Indigo.Lorentz
 import qualified Lorentz.Instr as L
 
@@ -102,11 +102,19 @@
   type family RetExprs' retKind ret :: Kind.Type
 
   -- | Allocate variables referring to result of the statement.
+  -- Requires an allocator operating in a Monad.
   allocateVars'
-    :: (forall inpt x . KnownValue x => MetaData inpt -> (Var x, MetaData (x & inpt))) -- ^ Single variable allocator
-    -> MetaData inp
-    -> (RetVars' retKind ret, MetaData (RetOutStack' retKind ret ++ inp))
+    :: Monad m
+    => (forall (x :: Kind.Type) . m (Var x))
+    -> m (RetVars' retKind ret)
 
+  -- | Push the variables referring to the result of the statement on top of
+  -- the stack of the given 'StackVars'.
+  assignVars'
+    :: RetVars' retKind ret
+    -> StackVars inp
+    -> StackVars (RetOutStack' retKind ret ++ inp)
+
 -- | Type class which unions all related management of computations in a scope,
 -- like in @if@ branch, in @case@ body, etc.
 --
@@ -125,7 +133,7 @@
 class ReturnableValue' retKind ret => ScopeCodeGen' (retKind :: BranchRetKind) (ret :: Kind.Type) where
   -- | Produces an Indigo computation that puts on the stack
   -- the evaluated returned expressions from the leaving scope.
-  compileScopeReturn' :: ret -> IndigoState xs (RetOutStack' retKind ret ++ xs) ()
+  compileScopeReturn' :: ret -> IndigoState xs (RetOutStack' retKind ret ++ xs)
 
   -- | Drop the stack cells that were produced in the leaving scope,
   -- apart from ones corresponding to the returning expressions.
@@ -142,10 +150,9 @@
 
 -- | Specific version of 'allocateVars\''
 allocateVars
-  :: forall ret inp . ReturnableValue ret
-  => (forall inpt x . KnownValue x => MetaData inpt -> (Var x, MetaData (x & inpt))) -- Single variable allocator
-  -> MetaData inp
-  -> (RetVars ret, MetaData (RetOutStack ret ++ inp))
+  :: forall ret m . (ReturnableValue ret, Monad m)
+  => (forall (x :: Kind.Type) . m (Var x))
+  -> m (RetVars ret)
 allocateVars = allocateVars' @(ClassifyReturnValue ret) @ret
 
 -- | Specific version of 'liftClear\''
@@ -159,23 +166,26 @@
 -- and clean up of redundant cells from the stack.
 compileScope
   :: forall ret inp xs . ScopeCodeGen ret
-  => GenCode inp xs ret
+  => DecomposedObjects
+  -> GenCode inp xs
+  -> ret
   -> (inp :-> RetOutStack ret ++ inp)
-compileScope gc =
+compileScope objs gc gcRet =
   gcCode gc #
-  gcCode (runIndigoState (compileScopeReturn' @(ClassifyReturnValue ret) (gcOut gc)) (gcMeta gc)) #
+  gcCode (usingIndigoState (MetaData (gcStack gc) objs) (compileScopeReturn' @(ClassifyReturnValue ret) gcRet)) #
   liftClear' @(ClassifyReturnValue ret) @ret (gcClear gc)
 
--- | Push a variables in 'MetaData', referring to the generated expressions,
+-- | Push variables in the 'StackVars', referring to the generated expressions,
 -- and generate 'gcClear' for the whole statement.
 finalizeStatement
   :: forall ret inp . ScopeCodeGen ret
-  => MetaData inp
+  => StackVars inp
+  -> RetVars ret
   -> (inp :-> RetOutStack ret ++ inp)
-  -> GenCode inp (RetOutStack ret ++ inp) (RetVars ret)
-finalizeStatement md code =
-  let (vars, newMd) = allocateVars' @(ClassifyReturnValue ret) @ret pushRefMd md in
-  GenCode vars newMd code (genGcClear' @(ClassifyReturnValue ret) @ret)
+  -> GenCode inp (RetOutStack ret ++ inp)
+finalizeStatement md vars code =
+  let newMd = assignVars' @(ClassifyReturnValue ret) @ret vars md in
+  GenCode newMd code (genGcClear' @(ClassifyReturnValue ret) @ret)
 
 -- Type instances for ScopeCodeGen'.
 -- Perhaps, they could be implemented more succinctly
@@ -188,10 +198,11 @@
   type RetOutStack' 'Unit () = '[]
   type RetVars' 'Unit () = ()
   type RetExprs' 'Unit () = ()
-  allocateVars' _ md = ((), md)
+  allocateVars' _ = pure ()
+  assignVars' _ md = md
 
 instance ScopeCodeGen' 'Unit () where
-  compileScopeReturn' _ = return ()
+  compileScopeReturn' _ = nopState
   liftClear' = id
   genGcClear' = L.nop
 
@@ -199,7 +210,8 @@
   type RetOutStack' 'SingleVal single = '[ExprType single]
   type RetVars' 'SingleVal single = Var (ExprType single)
   type RetExprs' 'SingleVal single = ExprType single
-  allocateVars' allocator = allocator
+  allocateVars' allocator = allocator @(ExprType single)
+  assignVars' = pushRef
 
 instance KnownValueExpr single  => ScopeCodeGen' 'SingleVal single where
   compileScopeReturn' = compileToExpr
@@ -210,10 +222,8 @@
   type RetOutStack' 'Tuple (x, y) = ExprType x ': '[ExprType y]
   type RetVars' 'Tuple (x, y) = (Var (ExprType x), Var (ExprType y))
   type RetExprs' 'Tuple (x, y) = (ExprType x, ExprType y)
-  allocateVars' allocator md =
-    let (var2, newMd1) = allocator md in
-    let (var1, newMd2) = allocator newMd1 in
-    ((var1, var2), newMd2)
+  allocateVars' allocator = (,) <$> allocator <*> allocator
+  assignVars' (var1, var2) md = pushRef var1 $ pushRef var2 md
 
 instance (KnownValueExpr x, KnownValueExpr y) => ScopeCodeGen' 'Tuple (x, y) where
   compileScopeReturn' (e1, e2) = compileToExpr e2 >> compileToExpr e1
@@ -225,16 +235,15 @@
   type RetOutStack' 'Tuple (x, y, z) = ExprType x ': ExprType y ': '[ExprType z]
   type RetVars' 'Tuple (x, y, z) = (Var (ExprType x), Var (ExprType y), Var (ExprType z))
   type RetExprs' 'Tuple (x, y, z) = (ExprType x, ExprType y, ExprType z)
-  allocateVars' allocator md =
-    let (var3, newMd1) = allocator md in
-    let (var2, newMd2) = allocator newMd1 in
-    let (var1, newMd3) = allocator newMd2 in
-    ((var1, var2, var3), newMd3)
+  allocateVars' allocator = (,,) <$> allocator <*> allocator <*> allocator
+  assignVars' (var1, var2, var3) md =
+    pushRef var1 . pushRef var2 $ pushRef var3 md
 
 instance (KnownValueExpr x, KnownValueExpr y, KnownValueExpr z) => ScopeCodeGen' 'Tuple (x, y, z) where
   compileScopeReturn' (e1, e2, e3) = compileToExpr e3 >> compileToExpr e2 >> compileToExpr e1
   liftClear' = L.dipN @3
   genGcClear' = L.drop # L.drop # L.drop
 
-compileToExpr :: ToExpr a => a -> IndigoState inp ((ExprType a) & inp) ()
+-- | Utility function to compile from an 'IsExpr'
+compileToExpr :: ToExpr a => a -> IndigoState inp ((ExprType a) & inp)
 compileToExpr = compileExpr . toExpr
diff --git a/src/Indigo/Backend/Var.hs b/src/Indigo/Backend/Var.hs
--- a/src/Indigo/Backend/Var.hs
+++ b/src/Indigo/Backend/Var.hs
@@ -2,24 +2,25 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
--- | Backend of the statements to create and modify variables
+-- | Backend statements for variable manipulation: assignment, replacement, update.
+
 module Indigo.Backend.Var
-  ( newVar
+  ( assignVar
   , setVar
   , setField
   , updateVar
   ) where
 
 import Indigo.Backend.Prelude
-import Indigo.Internal
+import Indigo.Internal hiding ((+))
 import Indigo.Lorentz
 import qualified Lorentz.Instr as L
 import Michelson.Typed.Haskell.Instr.Product (GetFieldType)
 import Util.Type (type (++))
 
--- | Create a new variable with passed expression as an initial value.
-newVar :: KnownValue x => Expr x -> IndigoState inp (x & inp) (Var x)
-newVar e = compileExpr e >> makeTopVar
+-- | Assign the given variable to the value resulting from the given expression.
+assignVar :: KnownValue x => Var x -> Expr x -> IndigoState inp (x & inp)
+assignVar var e = compileExpr e >> assignTopVar var
 
 -- | Set the variable to a new value.
 --
@@ -27,34 +28,48 @@
 -- we just compile passed expression and replace variable cell on stack.
 -- If a variable is decomposed, we decompose passed expression
 -- and call 'setVar' recursively from its fields.
-setVar :: forall a inp. Var a -> Expr a -> IndigoState inp inp ()
-setVar (Cell refId) e = do
-  MetaData s _ <- iget
-  unaryOpFlat e $ varActionSet refId s
-setVar (Decomposed fields) ex = case decomposeExpr (toExpr ex) of
+--
+-- Pay attention that this function takes a next RefId but it doesn't return RefId
+-- because all allocated variables will be destroyed during execution of the function,
+-- so allocated ones won't affect next allocated ones.
+setVar :: forall a inp. KnownValue a => RefId -> Var a -> Expr a -> IndigoState inp inp
+setVar nextRef v ex = withObjectState v $ flip (setVarImpl nextRef) ex
+
+setVarImpl :: forall a inp . RefId -> Object a -> Expr a -> IndigoState inp inp
+setVarImpl _ (Cell refId) ex = IndigoState $ \md ->
+  usingIndigoState md $ unaryOpFlat ex $ varActionSet refId (mdStack md)
+setVarImpl nextRef (Decomposed fields) ex = IndigoState $ \md -> case decomposeExpr (mdObjects md) ex of
   ExprFields fieldsExpr ->
-    rmapZipM (namedToTypedRec @a namedToTypedFieldVar fields) fieldsExpr
+    usingIndigoState md $ rmapZipM (namedToTypedRec @a namedToTypedFieldObj fields) fieldsExpr
   Deconstructed comp ->
-    IndigoState $ \md ->
-      let GenCode _ decomposeMd decomposeExCd _ = usingIndigoState md comp in
-      let setAllFieldsCd = setFieldsOnStack (namedToTypedRec @a namedToTypedFieldVar fields) decomposeMd in
-      GenCode () md (decomposeExCd # setAllFieldsCd) L.nop
+    let GenCode decomposeSt decomposeExCd _ = usingIndigoState md comp in
+    let setAllFieldsCd =
+          setFieldsOnStack
+            (MetaData decomposeSt $ mdObjects md)
+            (namedToTypedRec @a namedToTypedFieldObj fields) in
+    GenCode (mdStack md) (decomposeExCd # setAllFieldsCd) L.nop
   where
     -- Set fields, if they are decomposed on stack.
-    setFieldsOnStack :: forall rs . Rec TypedFieldVar rs -> MetaData (rs ++ inp) -> (rs ++ inp) :-> inp
-    setFieldsOnStack RNil _ = L.nop
-    setFieldsOnStack (TypedFieldVar f :& vs) md =
-      let (val, setVarMd) = pushRefMd (popNoRefMd md) in
-      let setVarCd = gcCode $ usingIndigoState setVarMd $ setVar f (V val) in
-      setVarCd #
+    setFieldsOnStack
+      :: forall rs .
+         MetaData (rs ++ inp)
+      -> Rec TypedFieldObj rs
+      -> (rs ++ inp) :-> inp
+    setFieldsOnStack _ RNil = L.nop
+    setFieldsOnStack md (TypedFieldObj f :& vs) =
+      let tmpFieldVar = Var nextRef
+          setVarMd = pushRefMd tmpFieldVar (popNoRefMd md) in
+      (gcCode $ usingIndigoState setVarMd $ setVarImpl (nextRef + 1) f (V tmpFieldVar)) #
       L.drop #
-      setFieldsOnStack vs (popNoRefMd md)
+      setFieldsOnStack (popNoRefMd md) vs
 
     -- Take list of fields (variables, referring to them)
-    -- and list of corresponding expressions and call 'setVar' recursively.
-    rmapZipM :: Rec TypedFieldVar rs -> Rec Expr rs -> IndigoState inp inp ()
-    rmapZipM RNil RNil = return ()
-    rmapZipM (TypedFieldVar f :& flds) (e :& exprs) = setVar f e >> rmapZipM flds exprs
+    -- and list of corresponding expressions and call 'setVarImpl' recursively.
+    rmapZipM :: Rec TypedFieldObj rs -> Rec Expr rs -> IndigoState inp inp
+    rmapZipM RNil RNil = nopState
+    rmapZipM (TypedFieldObj f :& flds) (e :& exprs) =
+      setVarImpl nextRef f e >>
+      rmapZipM flds exprs
 
 -- | Set the field (direct or indirect) of a complex object.
 setField
@@ -63,35 +78,40 @@
      , IsObject ftype
      , HasField dt fname ftype
      )
-  => Var dt -> Label fname -> Expr ftype -> IndigoState inp inp ()
-setField v@(Cell _) lb ex = updateVar (sopSetField (flSFO fieldLens) lb) v ex
-setField (Decomposed fields) targetLb ex = case fieldLens @dt @fname @ftype of
-  TargetField lb _ ->
-    case fetchField @dt lb fields of
-      NamedFieldVar v ->
-        setVar v ex
-  DeeperField (lb :: Label fnameInterm) _ ->
-    case fetchField @dt lb fields of
-      NamedFieldVar vf ->
-        setField @(GetFieldType dt fnameInterm) @fname @ftype vf targetLb ex
+  => RefId -> Var dt -> Label fname -> Expr ftype -> IndigoState inp inp
+setField nextRef v targetLb e = withObjectState v setFieldImpl
+  where
+    setFieldImpl :: forall x . (IsObject x, HasField x fname ftype) => Object x -> IndigoState inp inp
+    setFieldImpl (Cell refId) = updateVar @x nextRef (sopSetField (flSFO fieldLens) targetLb) (Var refId) e
+    setFieldImpl (Decomposed fields) = case fieldLens @x @fname @ftype of
+      TargetField lb _ ->
+        case fetchField @x lb fields of
+          NamedFieldObj field ->
+            setVarImpl nextRef field e
+      DeeperField (lb :: Label fnameInterm) _ ->
+        case fetchField @x lb fields of
+          NamedFieldObj vf ->
+            setFieldImpl @(GetFieldType x fnameInterm) vf
 
--- | Call binary operator with constant argument to update variable in-place.
+-- | Call binary operator with constant argument to update a variable in-place.
 updateVar
-  :: (IsObject x, KnownValue y)
-  => [y, x] :-> '[x]
+  :: forall x y inp . (IsObject x, KnownValue y)
+  => RefId
+  -> [y, x] :-> '[x]
   -> Var x
   -> Expr y
-  -> IndigoState inp inp ()
-updateVar action (Cell refId) e = do
-  MetaData s _ <- iget
-  unaryOpFlat e $ varActionUpdate refId s action
--- This function doesn't have to be called for complex data types,
--- it's only supposed to be used for assign-like statements
--- (+=), (-=), etc.
--- But it's implemented just in case.
-updateVar action v@(Decomposed _) e = IndigoState $ \md ->
-  let (var, newMd) = pushRefMd md in
-  usingIndigoState md $ binaryOpFlat e (V v) $
-    L.framed action #
-    gcCode (usingIndigoState newMd (setVar v (V var))) #
-    L.drop
+  -> IndigoState inp inp
+updateVar nextRef action vr e = withObjectState vr updateVarImpl
+  where
+    updateVarImpl (Cell refId) = IndigoState $ \md ->
+      usingIndigoState md $ unaryOpFlat e $ varActionUpdate refId (mdStack md) action
+    -- This function doesn't have to be called for complex data types,
+    -- it's only supposed to be used for assign-like statements
+    -- (+=), (-=), etc but implemented just in case.
+    updateVarImpl obj@(Decomposed _) = IndigoState $ \md ->
+      let tmpVar = Var nextRef in
+      let newMd = pushRefMd tmpVar md in
+      usingIndigoState md $ binaryOpFlat e (V vr) $
+        L.framed action #
+        gcCode (usingIndigoState newMd (setVarImpl (nextRef + 1) obj (V tmpVar))) #
+        L.drop
diff --git a/src/Indigo/Compilation.hs b/src/Indigo/Compilation.hs
--- a/src/Indigo/Compilation.hs
+++ b/src/Indigo/Compilation.hs
@@ -2,242 +2,52 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
--- | This module contains everything related to compilation from Indigo to Lorentz,
+-- | This module contains the high-level compilation of Indigo to Lorentz,
 -- including plain Indigo code, as well as Indigo contracts.
 
 module Indigo.Compilation
   ( compileIndigo
-  , IndigoWithParams
-  , IndigoContract
   , compileIndigoContract
-
-  , Ops
-  , HasSideEffects
-  , operationsVar
-  , HasStorage
-  , storageVar
   ) where
 
 import qualified Data.Map as M
-import Data.Reflection (give)
-import qualified Data.Set as S
-import Data.Singletons (SingI(..))
-import Data.Typeable ((:~:)(..), eqT)
-import Data.Vinyl.Core (RMap(..))
 
-import qualified Indigo.Backend as B
+import Indigo.Compilation.Field
 import Indigo.Compilation.Lambda
 import Indigo.Compilation.Params
-import Indigo.Frontend.Program (IndigoM(..), Program(..))
-import Indigo.Frontend.Statement
-import Indigo.Internal hiding (SetField, return, (>>), (>>=))
-import qualified Indigo.Internal as I
+import Indigo.Compilation.Sequential
+import Indigo.Frontend.Program (IndigoContract)
+import Indigo.Internal hiding (SetField, (>>))
 import Indigo.Lorentz
 import Indigo.Prelude
 import qualified Lorentz.Instr as L
 import qualified Lorentz.Macro as L
-import Util.Peano
 
--- | Iteration over Indigo freer monad
-compileIndigoM
-  :: forall inp a .
-    (forall x anyInp . StatementF IndigoM x -> SomeIndigoState anyInp x)
-  -> IndigoM a
-  -> SomeIndigoState inp a
-compileIndigoM _ (IndigoM (Done a)) = returnSIS a
-compileIndigoM interp (IndigoM (Instr i)) = interp i
-compileIndigoM interp (IndigoM (Bind instr cont)) =
-  compileIndigoM interp (IndigoM instr) `bindSIS` (compileIndigoM interp . IndigoM . cont)
-
--- | Convert frontend Freer to 'IndigoState'.
---
--- First of all, this function generates the definitions of
--- lambdas, creates the variables that refer to them
--- and calls them in the places where they are used.
--- This happens only for those lambdas that are called
--- at least twice, those that are used only once will be
--- inlined instead.
---
--- After that the generation of the body code starts.
-simpleCompileIndigoM :: forall inp a . IndigoM a -> SomeIndigoState inp a
-simpleCompileIndigoM indigoM =
-  let lambdas = S.toList (collectLambdas indigoM) in
-  forMSIS lambdas defineLambda
-  `bindSIS`
-    (\defined ->
-      let definedLambdas = M.fromList $ map (\l -> (_clName l, l)) defined
-      in compileBody definedLambdas indigoM
-    )
-  where
-    compileBody definedLambdas = compileIndigoM (usingReader definedLambdas . compileSt)
-
-    compileSt :: StatementF IndigoM x -> Reader (Map String CompiledLambda) (SomeIndigoState anyInp x)
-    compileSt (LiftIndigoState cd) = pure cd
-    compileSt (NewVar ex) = pure $ toSIS (B.newVar ex)
-    compileSt (SetVar v ex) = pure $ toSIS (B.setVar v ex)
-    compileSt (SetField v fName ex) = pure $ toSIS (B.setField v fName ex)
-    compileSt (VarModification act var ex) = pure $ toSIS (B.updateVar act var ex)
-
-    compileSt (LambdaPure1Call lName (body :: (Var arg -> IndigoM res)) argm) =
-      execGenericLambda @'[] @res (B.executeLambdaPure1 @res) lName body argm
-
-    compileSt (Lambda1Call (_ :: Proxy st) lName (body :: (Var arg -> IndigoM res)) argm) =
-      execGenericLambda @'[st] @res (B.executeLambda1 @st @res) lName body argm
-
-    compileSt (LambdaEff1Call (_ :: Proxy st) lName (body :: (Var arg -> IndigoM res)) argm) =
-      execGenericLambda @'[st, Ops] @res (B.executeLambdaEff1 @st @res) lName body argm
-
-    compileSt (Scope cd) = do
-      definedLambdas <- ask
-      pure $ withSIS (compileBody definedLambdas cd) (toSIS . B.scope)
-    compileSt (If ex tb fb) = do
-      definedLambdas <- ask
-      pure $ withSIS (compileBody definedLambdas tb) $ \tb' ->
-        withSIS (compileBody definedLambdas fb) $ \fb' ->
-         toSIS (B.if_ ex tb' fb')
-    compileSt (IfSome ex tb fb) = do
-      definedLambdas <- ask
-      pure $ withSIS1 (compileBody definedLambdas . tb) $ \tb' ->
-        withSIS (compileBody definedLambdas fb) $ \fb' ->
-          toSIS (B.ifSome ex tb' fb')
-    compileSt (IfRight ex rb lb) = do
-      definedLambdas <- ask
-      pure $ withSIS1 (compileBody definedLambdas . rb) $ \rb' ->
-        withSIS1 (compileBody definedLambdas . lb) $ \lb' ->
-          toSIS (B.ifRight ex rb' lb')
-    compileSt (IfCons ex tb fb) = do
-      definedLambdas <- ask
-      pure $ withSIS2 (\x y -> compileBody definedLambdas $ tb x y) $ \tb' ->
-        withSIS (compileBody definedLambdas fb) $ \fb' ->
-          toSIS (B.ifCons ex tb' fb')
-    compileSt (Case grd clauses) = do
-      definedLambdas <- ask
-      pure $ toSIS $ B.caseRec grd (rmapClauses definedLambdas clauses)
-    compileSt (EntryCase proxy grd clauses) = do
-      definedLambdas <- ask
-      pure $ toSIS $ B.entryCaseRec proxy grd (rmapClauses definedLambdas clauses)
-    compileSt (EntryCaseSimple grd clauses) = do
-      definedLambdas <- ask
-      pure $ toSIS $ B.entryCaseSimpleRec grd (rmapClauses definedLambdas clauses)
-
-    compileSt (While ex body) = do
-      definedLambdas <- ask
-      pure $ withSIS (compileBody definedLambdas body) $ \bd -> toSIS (B.while ex bd)
-    compileSt (WhileLeft ex lb) = do
-      definedLambdas <- ask
-      pure $
-        withSIS1 (compileBody definedLambdas . lb) $ \lb' -> do
-          toSIS (B.whileLeft ex lb')
-    compileSt (ForEach e body) = do
-      definedLambdas <- ask
-      pure $ withSIS1 (compileBody definedLambdas . body) $ \bd -> toSIS (B.forEach e bd)
-
-    compileSt (ContractName cName contr) = do
-      definedLambdas <- ask
-      pure $ withSIS (compileBody definedLambdas contr) $ toSIS . B.contractName cName
-    compileSt (DocGroup gr ii) = do
-      definedLambdas <- ask
-      pure $ withSIS (compileBody definedLambdas ii) $ toSIS . B.docGroup gr
-    compileSt (ContractGeneral contr) = do
-      definedLambdas <- ask
-      pure $ withSIS (compileBody definedLambdas contr) (toSIS . B.contractGeneral)
-    compileSt (FinalizeParamCallingDoc entrypoint param) = do
-      definedLambdas <- ask
-      pure $ withSIS1 (compileBody definedLambdas . entrypoint)
-        (\bd -> toSIS $ B.finalizeParamCallingDoc bd param)
-
-    compileSt (TransferTokens expar exm exc) = pure $ toSIS (B.transferTokens expar exm exc)
-    compileSt (SetDelegate kh) = pure $ toSIS (B.setDelegate kh)
-    compileSt (CreateContract lCtr ek em es) = pure $ toSIS $
-      I.iget I.>>= \(MetaData s _) ->
-        ternaryOp ek em es (L.createContract lCtr
-                                              # varActionOperation (NoRef :& s))
-        I.>> makeTopVar
-    compileSt (ContractCalling (_ :: Proxy cp) ref addr) = pure $ toSIS $ B.contractCalling @cp ref addr
-
-    compileSt (FailWith ex) = pure $ toSIS $ B.failWith ex
-    compileSt (Assert err expr) = pure $ toSIS $ B.assert err expr
-    compileSt (FailCustom l expr) = pure $ toSIS $ B.failCustom l expr
-
-    rmapClauses:: forall ret cs . RMap cs
-       => Map String CompiledLambda
-       -> Rec (IndigoMCaseClauseL IndigoM ret) cs
-       -> Rec (B.IndigoCaseClauseL ret) cs
-    rmapClauses definedLambdas = rmap (\(OneFieldIndigoMCaseClauseL cName clause) ->
-      cName /-> (\v -> B.IndigoAnyOut $ compileBody definedLambdas $ clause v))
-
-    forMSIS :: [r] -> (forall someInp . r -> SomeIndigoState someInp v) -> SomeIndigoState someInp1 [v]
-    forMSIS [] _ = returnSIS []
-    forMSIS (x : xs) f = f x `bindSIS` (\what -> (what :) <$> forMSIS xs f)
-
-    defineLambda :: Lambda1Def -> SomeIndigoState someOut CompiledLambda
-    defineLambda (LambdaPure1Def (_ :: Proxy (_s, arg, res)) lName fun) =
-      defineGenericLambda @'[] B.initMetaDataPure B.createLambdaPure1 lName fun
-    defineLambda (Lambda1Def (_ :: Proxy (st, arg, res)) lName fun) =
-      defineGenericLambda @'[st] B.initMetaData B.createLambda1 lName fun
-    defineLambda (LambdaEff1Def (_ :: Proxy (st, arg, res)) lName fun) =
-      defineGenericLambda @'[st, Ops] B.initMetaDataEff B.createLambdaEff1 lName fun
-
-    defineGenericLambda
-      :: forall extra res arg someOut .
-      (Typeable arg, Typeable res, Typeable extra)
-      => (Var arg, MetaData (arg & extra))
-      -> (forall inpt out . B.LambdaCreator extra arg res inpt out)
-      -> String
-      -> (Var arg -> IndigoM res)
-      -> SomeIndigoState someOut CompiledLambda
-    defineGenericLambda (varArg, initMd) lambdaCreator lName fun = do
-      runSIS
-        (simpleCompileIndigoM $ fun varArg) initMd
-        (\gc -> toSIS $ lambdaCreator (\_v -> IndigoState $ \_md -> gc))
-      `bindSIS`
-      (returnSIS . CompiledLambda (Proxy @res) lName)
-
-    execGenericLambda
-      :: forall extra res arg someOut .
-         (Typeable extra, KnownValue arg, Typeable res, B.ScopeCodeGen res)
-      => (forall inpt . B.LambdaExecutor extra arg res inpt)
-      -> String
-      -> (Var arg -> IndigoM res)
-      -> Expr arg
-      -> Reader (Map String CompiledLambda) (SomeIndigoState someOut (B.RetVars res))
-    execGenericLambda executor lName (body :: (Var arg -> IndigoM res)) (argm :: Expr arg) = do
-      compiled <- ask
-      let maybeToRight' = flip maybeToRight
-      -- This code seems to be pretty unsafe, but it works almost inevitably
-      pure $ either (error . fromString) id $ do
-        case M.lookup lName compiled of
-          Nothing -> Right $
-            -- Just inline lambda without calling Lorentz lambda
-            withSIS1 (compileBody compiled . body)
-              (\bd -> toSIS $ B.newVar argm I.>>= (B.scope @res . bd))
-          Just compLam -> case compLam of
-            CompiledLambda (_ :: Proxy res1) _ (varF :: Var (B.Lambda1Generic extra1 arg1 res1)) -> do
-              Refl <- maybeToRight' (eqT @res @res1) ("unexpected result type of " ++ lName ++ " lambda didn't match")
-              Refl <- maybeToRight' (eqT @arg @arg1) ("unexpected argument type of " ++ lName ++ " lambda didn't match")
-              Refl <- maybeToRight' (eqT @extra @extra1) ("unexpected storage type of " ++ lName ++ " lambda didn't match")
-              pure $ toSIS (executor varF argm)
-
 -- | Compile Indigo code to Lorentz.
 --
 -- Note: it is necessary to specify the number of parameters (using the first
 -- type variable) of the Indigo function. Also, these should be on the top of
 -- the input stack in inverse order (see 'IndigoWithParams').
-compileIndigo
-  :: forall n inp a.
-     ( SingI (ToPeano n), Default (MetaData inp)
-     , AreIndigoParams (ToPeano n) inp, KnownValue a
-     )
-  => IndigoWithParams (ToPeano n) inp a
+compileIndigoImpl
+  :: forall n inp a. (AreIndigoParams n inp, KnownValue a, Default (StackVars inp))
+  => IndigoWithParams n inp a
+  -> (StackVars inp -> (Block, RefId) -> (inp :-> inp))
   -> inp :-> inp
-compileIndigo paramCode =
-  runSIS (simpleCompileIndigoM code) md cleanGenCode
+compileIndigoImpl paramCode runner =
+    runner initMd optimized
   where
-    (code, md) = fromIndigoWithParams @inp @_ @a paramCode def (sing @(ToPeano n))
+    (code, initMd, nextRef) = fromIndigoWithParams @n @a paramCode
+    optimized = indigoMtoSequential nextRef code
+      & compileLambdas
+      & optimizeFields
 
--- | Type of a contract that can be compiled to Lorentz with 'compileIndigoContract'.
-type IndigoContract param st =
-  (HasStorage st, HasSideEffects) => Var param -> IndigoM ()
+-- | Specialiasation of 'compileIndigoImpl' without var decompositions.
+compileIndigo
+  :: forall n inp a. (AreIndigoParams n inp, KnownValue a, Default (StackVars inp))
+  => IndigoWithParams n inp a
+  -> inp :-> inp
+compileIndigo paramCode =
+  compileIndigoImpl @n @inp @a paramCode (\stk block -> sequentialToLorentz (MetaData stk mempty) block)
 
 -- | Compile Indigo code to Lorentz contract.
 -- Drop elements from the stack to return only @[Operation]@ and @storage@.
@@ -249,16 +59,26 @@
   => IndigoContract param st
   -> ContractCode param st
 compileIndigoContract code =
-  let  (varOps, opsMd) = pushRefMd emptyMetadata
-       mdSt = pushNoRefMd opsMd in
-  -- Decompose storage value first, run contract and then compose it back.
-  runSIS (deepDecomposeCompose @st) mdSt $ \(GenCode varSt decomposedMd decomposeSt composeSt) ->
-    let (varParam, initMd) = pushRefMd decomposedMd
-        everythingGiven = (give @(Var Ops) varOps $ give @(Var st) varSt code) varParam
-        indigoCode = runSIS (simpleCompileIndigoM everythingGiven) initMd cleanGenCode in
-    L.nil # L.swap # L.unpair #
-    L.dip decomposeSt # -- decompose storage
-    indigoCode # -- run indigo code
-    L.drop # -- drop param
-    composeSt # -- compose storage back
-    L.swap # L.pair
+  prepare $ compileIndigoImpl @3 @'[param, st, Ops] (contractToIndigoWithParams code) $
+    \(parRef :& storageRef :& opsStack) (block, nextRef) ->
+      let stRef = case storageRef of
+                    NoRef -> error "Storage variable hasn't been assigned"
+                    Ref r -> r in
+      -- during code Indigo code compilation the stack will look like:
+      -- [var_10, var_9, ... , var_3, param_var_2, storage_field_11, storage_field_12, ..., storage_field_20, ops_var_0]
+      -- var_1 will represent storage and passed to DecomposedObjects
+      let (storageObj, nextRef', someGen) = deepDecomposeCompose nextRef (NoRef :& opsStack) in
+      case someGen of
+        SomeGenCode (GenCode decompStk decompose composeBack) ->
+          let md = MetaData (parRef :& decompStk) $ M.singleton stRef (SomeObject storageObj)
+              indigoCode = sequentialToLorentz md (block, nextRef') in
+          L.dip decompose # -- decompose storage
+          indigoCode # -- run indigo code
+          L.dip composeBack
+  where
+    prepare :: ('[param, st, Ops] :-> '[param, st, Ops]) -> ('[(param, st)] :-> '[(Ops, st)])
+    prepare cd =
+      L.nil # L.swap # L.unpair #
+      cd #
+      L.drop # -- drop param
+      L.swap # L.pair
diff --git a/src/Indigo/Compilation/Field.hs b/src/Indigo/Compilation/Field.hs
new file mode 100644
--- /dev/null
+++ b/src/Indigo/Compilation/Field.hs
@@ -0,0 +1,15 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+module Indigo.Compilation.Field
+  ( optimizeFields
+  ) where
+
+import Indigo.Backend.Prelude
+
+import Indigo.Compilation.Sequential
+import Indigo.Internal.Var (RefId)
+
+optimizeFields :: (Block, RefId) -> (Block, RefId)
+optimizeFields = id -- TODO #279
diff --git a/src/Indigo/Compilation/Lambda.hs b/src/Indigo/Compilation/Lambda.hs
--- a/src/Indigo/Compilation/Lambda.hs
+++ b/src/Indigo/Compilation/Lambda.hs
@@ -3,152 +3,197 @@
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
 module Indigo.Compilation.Lambda
-       ( CompiledLambda (..)
-       , Lambda1Def (..)
-       , collectLambdas
-       ) where
+  ( compileLambdas
+  ) where
 
 import Prelude
 import qualified Data.Map as M
 
 import Indigo.Backend as B
-import Indigo.Frontend.Program (IndigoM(..), interpretProgram)
-import Indigo.Frontend.Statement
-import Indigo.Internal.Object
-import Indigo.Internal.SIS
-import Indigo.Internal.State hiding ((>>))
+import Indigo.Compilation.Sequential
+import Indigo.Internal.Var
 import Indigo.Lorentz
 
-data CompiledLambda where
-  CompiledLambda
-    :: (Typeable arg, Typeable res, Typeable extra)
-    => { _clProxyRes :: Proxy res
-       , _clName :: String
-       , _clVarLam :: Var (B.Lambda1Generic extra arg res)
-       } -> CompiledLambda
+-- | Collects named lambdas that are used more than once and separates them into
+-- a lambda creation and multiple lambda executions.
+-- Leaves the remaining lambdas untouched, to be compiled inline.
+compileLambdas :: (Block, RefId) -> (Block, RefId)
+compileLambdas (block, nextRef) = (mkLambdas <> updatedBlock, newNextRef)
+  where
+    lambdaSet = collectNotInlinableLambdas block
+    (lambdaRefDefs, newNextRef) = createLambdaRefs nextRef lambdaSet
+    mkLambdas = createAllLambdas lambdaRefDefs
+    updatedBlock = updateBlock block . M.fromList $ map (first ldName) lambdaRefDefs
 
-data Lambda1Def where
-  LambdaPure1Def
-    :: (Typeable res, CreateLambdaPure1C arg res)
-    => { _ldProxy :: Proxy (_stUnit, arg, res)
-       , _ldName :: String
-       , _ldBody :: Var arg -> IndigoM res
-       } -> Lambda1Def
+-- | Collect all used lambdas in a computation that are called at least twice.
+-- Only the outer lambdas will be gathered, for example, if we call lambda "func1"
+-- from "func0", only "func0" will be considered.
+collectNotInlinableLambdas :: Block -> Set Lambda1Def
+collectNotInlinableLambdas = M.keysSet . M.filter (> 1) . executingState mempty . lookForLambdas
 
-  Lambda1Def
-    :: (Typeable res, CreateLambda1C st arg res)
-    => { _ldProxy :: Proxy (st, arg, res)
-       , _ldName :: String
-       , _ldBody :: Var arg -> IndigoM res
-       } -> Lambda1Def
+-- | Associates each given 'Lambda1Def' to a new 'RefId', starting from the given
+-- one. Also returns the first unused 'RefId'
+createLambdaRefs :: RefId -> Set Lambda1Def -> ([(Lambda1Def, RefId)], RefId)
+createLambdaRefs nextRef =
+  foldr (\lm (lst, ref) -> ((lm, ref) : lst, ref + 1)) ([], nextRef)
 
-  LambdaEff1Def
-    :: (Typeable res, CreateLambdaEff1C st arg res)
-    => { _ldProxy :: Proxy (st, arg, res)
-       , _ldName :: String
-       , _ldBody :: Var arg -> IndigoM res
-       } -> Lambda1Def
+-- | Generates an 'Instruction' for each given tuple, to generate a lambda
+-- (assigned to the respective variable) and leave it on the stack.
+createAllLambdas :: [(Lambda1Def, RefId)] -> Block
+createAllLambdas = map $ \(Lambda1Def {..}, lamRef) ->
+  CreateLambda1 ldStack ldArgVar ldBody ldRet (Var lamRef)
 
-instance Eq Lambda1Def where
-  (==) l1 l2 = _ldName l1 == _ldName l2
+-- | Updates a 'Block', it looks for lambda "Calls" (defined and used in place)
+-- to replace them with lambda "Exec", provided there is a known variable for an
+-- already created lambda.
+updateBlock :: Block -> Map String RefId -> Block
+updateBlock blk lambdaMap = updateBlock' blk
+  where
+    updateBlock' :: Block -> Block
+    updateBlock' = map $ \case
+      -- Instructions not concerned, will be kept the same
+      LiftIndigoState sis -> LiftIndigoState sis
+      AssignVar vx ex -> AssignVar vx ex
+      SetVar vx ex -> SetVar vx ex
+      VarModification upd vx ey -> VarModification upd vx ey
+      SetField vSt lName ex -> SetField vSt lName ex
 
-instance Ord Lambda1Def where
-  (<=) l1 l2 = _ldName l1 <= _ldName l2
+      -- Lambda instructions to check for possible replacement
+      lc@(LambdaCall1 lKind lName ex _var _block _ret retVars) ->
+        case M.lookup lName lambdaMap of
+          Nothing -> lc
+          Just ref -> ExecLambda1 lKind Proxy ex (Var ref) retVars
 
--- | This is a hack, which prevents using
--- a variable from an outer scope in a body of the lambda.
--- This is not needed when a lambda is defined as top level function,
--- but made just in case, if one wanted to define something like this:
---
--- @
--- f :: Var Storage -> IndigoM ()
--- f storage = do
---     field <- getStorageField
---     let lambda = defNamedLambda1 $ \arg -> ... using field here ...
--- @
--- The idea is that when we pass this variable in
--- a bind it will be propagated in all expressions,
--- including the ones that are in the lambdas.
--- An error will be raised during a variable lookup.
--- This hack will be rewritten later.
-leakedVar :: KnownValue a => Var a
-leakedVar = Cell $
-  error "In a scope of function you are using a variable from an outer scope. Closures are not supported yet."
+      -- Lambda instructions not concerned, nothing to replace here
+      c@(CreateLambda1{}) -> c
+      e@(ExecLambda1{}) -> e
 
-leakedScopeVariableAllocator :: KnownValue a => MetaData _inp -> (Var a, MetaData (a & _inp))
-leakedScopeVariableAllocator (MetaData stk cnt) =
-  let v = leakedVar
-  in (v, MetaData (Ref cnt :& stk) (cnt + 1))
+      -- Instructions with deeper code blocks to replace as well
+      Scope block ret retVars ->
+        Scope (updateBlock' block) ret retVars
+      If ex blockA retA blockB retB retVars ->
+        If ex (updateBlock' blockA) retA (updateBlock' blockB) retB retVars
+      IfSome ex varX blockA retA blockB retB retVars ->
+        IfSome ex varX (updateBlock' blockA) retA (updateBlock' blockB) retB retVars
+      IfRight ex varR blockA retA varL blockB retB retVars ->
+        IfRight ex varR (updateBlock' blockA) retA varL (updateBlock' blockB) retB retVars
+      IfCons ex varX varLX blockA retA blockB retB retVars ->
+        IfCons ex varX varLX (updateBlock' blockA) retA (updateBlock' blockB) retB retVars
 
-allocateVarsLeaked :: forall a . ReturnableValue a => RetVars a
-allocateVarsLeaked = fst (allocateVars @a leakedScopeVariableAllocator emptyMetadata)
+      Case grd blockClauses retVars ->
+        Case grd (updateClauses updateBlock' blockClauses) retVars
+      EntryCase proxy grd blockClauses retVars ->
+        EntryCase proxy grd (updateClauses updateBlock' blockClauses) retVars
+      EntryCaseSimple grd blockClauses retVars ->
+        EntryCaseSimple grd (updateClauses updateBlock' blockClauses) retVars
 
-allocateVarsLeakedM :: forall a m . (Monad m, ReturnableValue a) => m a -> m (RetVars a)
-allocateVarsLeakedM ma = allocateVarsLeaked @a <$ ma
+      While ex block ->
+        While ex (updateBlock' block)
+      WhileLeft ex varL block varR ->
+        WhileLeft ex varL (updateBlock' block) varR
+      ForEach varIop ex block ->
+        ForEach varIop ex (updateBlock' block)
 
--- | Collect all used lambdas in a computation
--- (which might be either a contract body or another function body),
--- which are called at least twice.
--- Only outer functions will be gathered, for instance,
--- if we call lambda func1 from func0, only func0 will be taken.
-collectLambdas :: forall a . IndigoM a -> Set Lambda1Def
-collectLambdas indigoM =
-  M.keysSet $ M.filter (> 1) $ executingState mempty (lookForLambdas indigoM)
+      ContractName tx block ->
+        ContractName tx (updateBlock' block)
+      DocGroup dg block ->
+        DocGroup dg (updateBlock' block)
+      ContractGeneral block ->
+        ContractGeneral (updateBlock' block)
+      FinalizeParamCallingDoc varCp block param ->
+        FinalizeParamCallingDoc varCp (updateBlock' block) param
+
+      -- Instructions not concerned, will be kept the same
+      TransferTokens ex exm exc -> TransferTokens ex exm exc
+      SetDelegate ex -> SetDelegate ex
+      CreateContract varAddr ctrc exk exm exs -> CreateContract varAddr ctrc exk exm exs
+      SelfCalling proxy varCR ep -> SelfCalling proxy varCR ep
+      ContractCalling varMcr pCp epRef exAddr -> ContractCalling varMcr pCp epRef exAddr
+
+      Fail failure -> Fail failure
+      FailOver failure ex -> FailOver failure ex
+
+-- Like 'collectLambdas', but uses 'State' to collect the 'Map' of all outer
+-- lambdas encountered, including those used once.
+lookForLambdas :: Block -> State (Map Lambda1Def Word) ()
+lookForLambdas blk = forM_ blk match
   where
-    lookForLambdas :: IndigoM x -> State (Map Lambda1Def Word) x
-    lookForLambdas (IndigoM program) = interpretProgram inspectLambda program
+    -- pva701: it's crucial to have this function 'match' instead of code like
+    -- @forM_ blk match $ \case@
+    --        ... cases here ...
+    -- because in the case of code above compilation of this function takes about 5-6 minutes
+    -- it would be nice to figure out why (inspecting generated by GHC code)
+    match :: Instruction -> State (Map Lambda1Def Word) ()
+    match = \case
+      -- Lambda instruction to collect
+      LambdaCall1 lKind ldName _ex ldArgVar ldBody ldRet _retVars -> do
+        let ldStack = initLambdaStackVars lKind ldArgVar
+        withLambdaKind lKind $ addLambda $ Lambda1Def {..}
 
-    inspectLambda :: StatementF IndigoM x -> State (Map Lambda1Def Word) x
-    inspectLambda (LambdaPure1Call name (body :: (Var arg -> IndigoM res)) _) =
-      allocateVarsLeaked @res <$ modify (addLambda (LambdaPure1Def (Proxy @((), arg, res)) name body))
+      -- Instructions with deeper code block to look into
+      Scope block _ _ -> lookForLambdas block
+      If _ blockA _ blockB _ _ ->
+        lookForLambdas blockA >> lookForLambdas blockB
+      IfSome _ _ blockA _ blockB _ _ ->
+        lookForLambdas blockA >> lookForLambdas blockB
+      IfRight _ _ blockA _ _ blockB _ _ ->
+        lookForLambdas blockA >> lookForLambdas blockB
+      IfCons _ _ _ blockA _ blockB _ _ ->
+        lookForLambdas blockA >> lookForLambdas blockB
+      Case _ blockClauses _ ->
+        mapMClauses lookForLambdas blockClauses
+      EntryCase _ _ blockClauses _ ->
+        mapMClauses lookForLambdas blockClauses
+      EntryCaseSimple _ blockClauses _ ->
+        mapMClauses lookForLambdas blockClauses
+      While _ block -> lookForLambdas block
+      WhileLeft _ _ block _ -> lookForLambdas block
+      ForEach _ _ block -> lookForLambdas block
+      ContractName _ block -> lookForLambdas block
+      DocGroup _ block -> lookForLambdas block
+      ContractGeneral block -> lookForLambdas block
+      FinalizeParamCallingDoc _ block _ -> lookForLambdas block
 
-    inspectLambda (Lambda1Call (_ :: Proxy st) name (body :: (Var arg -> IndigoM res)) _) =
-      allocateVarsLeaked @res <$ modify (addLambda (Lambda1Def (Proxy @(st, arg, res)) name body))
+      -- We skip two types of instructions:
+      -- * Instructions without deeper code block
+      -- * Unnamed lambdas creation/usage (like CreateLambda1, ExecLambda1, etc)
 
-    inspectLambda (LambdaEff1Call (_ :: Proxy st) name (body :: (Var arg -> IndigoM res)) _) =
-      allocateVarsLeaked @res <$ modify (addLambda (LambdaEff1Def (Proxy @(st, arg, res)) name body))
+      -- Instructions without deeper code block
+      LiftIndigoState {} -> return ()
+      AssignVar {}       -> return ()
+      SetVar {}          -> return ()
+      VarModification {} -> return ()
+      SetField {}        -> return ()
 
-    inspectLambda (Scope cd) = allocateVarsLeakedM $ lookForLambdas cd
-    inspectLambda (If _ tb fb) = allocateVarsLeakedM $ lookForLambdas tb >> lookForLambdas fb
-    inspectLambda (IfSome _ tb fb) = allocateVarsLeakedM $ lookForLambdas (tb leakedVar) >> lookForLambdas fb
-    inspectLambda (IfRight _ rb lb) = allocateVarsLeakedM $ lookForLambdas (rb leakedVar) >> lookForLambdas (lb leakedVar)
-    inspectLambda (IfCons _ tb fb) = allocateVarsLeakedM $ lookForLambdas (tb leakedVar leakedVar) >> lookForLambdas fb
-    inspectLambda (Case _ clauses) = rmapClauses clauses
-    inspectLambda (EntryCase _ _ clauses) = rmapClauses clauses
-    inspectLambda (EntryCaseSimple _ clauses) = rmapClauses clauses
-    inspectLambda (While _ body) = lookForLambdas body
-    inspectLambda (WhileLeft _ body) = lookForLambdas (body leakedVar) >> pure leakedVar
-    inspectLambda (ForEach _ body) = lookForLambdas $ body leakedVar
-    inspectLambda (ContractName _ contr) = lookForLambdas contr
-    inspectLambda (DocGroup _ ii) = lookForLambdas ii
-    inspectLambda (ContractGeneral contr) = lookForLambdas contr
-    inspectLambda (FinalizeParamCallingDoc entrypoint _) = lookForLambdas (entrypoint leakedVar)
+      TransferTokens {}  -> return ()
+      SetDelegate {}     -> return ()
+      CreateContract {}  -> return ()
+      SelfCalling {}     -> return ()
+      ContractCalling {} -> return ()
+      Fail {}            -> return ()
+      FailOver {}        -> return ()
 
-    -- Not recursive simple statements. They are terminal ones
-    inspectLambda (LiftIndigoState cd) = pure $ runSIS cd emptyMetadata gcOut
-    inspectLambda (NewVar _) = pure leakedVar
-    inspectLambda (SetVar _ _) = pure ()
-    inspectLambda (SetField {}) = pure ()
-    inspectLambda (VarModification {}) = pure ()
-    inspectLambda (TransferTokens {}) = pure ()
-    inspectLambda (SetDelegate _) = pure ()
-    inspectLambda (CreateContract{}) = pure leakedVar
-    inspectLambda (ContractCalling{}) = pure leakedVar
+      -- Nothing to collect in the case of already unnamed lambdas creation/usage
+      CreateLambda1 {}   -> return ()
+      ExecLambda1 {}     -> return ()
 
-    inspectLambda (FailWith ex) = pure $ gcOut $ runIndigoState (B.failWith ex) emptyMetadata
-    inspectLambda (Assert _ _) = pure ()
-    inspectLambda (FailCustom tag ex) = pure $ gcOut $ runIndigoState (B.failCustom tag ex) emptyMetadata
+    addLambda :: Lambda1Def -> State (Map Lambda1Def Word) ()
+    addLambda lDef = modify $ M.insertWith (+) lDef 1
 
-    rmapClauses:: forall ret cs . ReturnableValue ret
-       => Rec (IndigoMCaseClauseL IndigoM ret) cs
-       -> State (Map Lambda1Def Word) (RetVars ret)
-    rmapClauses RNil = pure (allocateVarsLeaked @ret)
-    rmapClauses ((OneFieldIndigoMCaseClauseL _ clause) :& rs) =
-      lookForLambdas (clause leakedVar) >> rmapClauses rs
+-- | Contains all the data necessary for the generation of a single-argument
+-- lambda. Is compared only on the base of it's 'ldName'.
+data Lambda1Def where
+  Lambda1Def
+    :: (Typeable ret, CreateLambda1CGeneric extra arg ret)
+    => { ldRet     :: ret
+       , ldName    :: String
+       , ldBody    :: Block
+       , ldArgVar  :: Var arg
+       , ldStack   :: StackVars (arg & extra)
+       } -> Lambda1Def
 
-    addLambda :: Lambda1Def -> Map Lambda1Def Word -> Map Lambda1Def Word
-    addLambda  =
-      M.alter (\case
-        Nothing -> Just 1
-        Just x -> Just (x + 1)
-      )
+instance Eq Lambda1Def where
+  (==) l1 l2 = ldName l1 == ldName l2
+
+instance Ord Lambda1Def where
+  (<=) l1 l2 = ldName l1 <= ldName l2
diff --git a/src/Indigo/Compilation/Params.hs b/src/Indigo/Compilation/Params.hs
--- a/src/Indigo/Compilation/Params.hs
+++ b/src/Indigo/Compilation/Params.hs
@@ -6,62 +6,71 @@
   ( IndigoWithParams
   , AreIndigoParams
   , fromIndigoWithParams
+  , contractToIndigoWithParams
   ) where
 
-import Data.Singletons (Sing)
-import Data.Typeable ((:~:)(..), eqT)
+import Data.Reflection (give)
+import Data.Singletons (Sing, SingI(..))
 
 import Indigo.Backend.Prelude
-import Indigo.Frontend.Program (IndigoM)
-import Indigo.Internal.Object
-import Indigo.Internal.State
+import Indigo.Frontend.Program (IndigoM, IndigoContract)
+import Indigo.Internal.Var
 import Indigo.Lorentz
 import Util.Peano
 
-----------------------------------------------------------------------------
--- Utility for compatibility with Lorentz
-----------------------------------------------------------------------------
-
 -- | Type of a function with @n@ 'Var' arguments and @IndigoM a@ result.
 --
 -- Note that the arguments are the first @n@ elements of the @inp@ stack in
 -- inverse order, for example:
--- @IndigoWithParams (\'S (\'S \'Z)) \'[a, b, c] x@ is the same as:
+-- @IndigoWithParams 2 [a, b, c] x@ is the same as:
 -- @Var b -> Var a -> IndigoM x@
-type family IndigoWithParams n inp a where
-  IndigoWithParams 'Z _ a = IndigoM a
-  IndigoWithParams ('S n) inp a = Var (At n inp) -> IndigoWithParams n inp a
+type IndigoWithParams n inp a = IndigoWithPeanoParams (ToPeano n) inp a
 
--- | Typeable and stack size constraint for the parameters of an 'IndigoWithParams'.
-type family AreIndigoParams n stk :: Constraint where
-  AreIndigoParams 'Z _ = (() :: Constraint)
-  AreIndigoParams ('S n) stk = (KnownValue (At n stk), RequireLongerThan stk n, AreIndigoParams n stk)
+-- | Typeable and stack size constraints for the parameters of an 'IndigoWithParams'
+-- and for converting to a 'Peano'
+type AreIndigoParams n stk =
+  ( AreIndigoPeanoParams (ToPeano n) stk
+  , SingI (ToPeano n)
+  )
 
+-- | 'Peano' equivalent of 'IndigoWithParams'
+type family IndigoWithPeanoParams n inp a where
+  IndigoWithPeanoParams 'Z _ a = IndigoM a
+  IndigoWithPeanoParams ('S n) inp a = Var (At n inp) -> IndigoWithPeanoParams n inp a
+
+-- | Typeable and stack size constraints for the parameters of an 'IndigoWithPeanoParams'.
+type family AreIndigoPeanoParams n stk :: Constraint where
+  AreIndigoPeanoParams 'Z _ = (() :: Constraint)
+  AreIndigoPeanoParams ('S n) stk =
+    (KnownValue (At n stk), RequireLongerThan stk n, AreIndigoPeanoParams n stk)
+
 -- | Converts an 'IndigoWithParams' to its form without input 'Var's, alongside
--- the 'MetaData' to use it with.
--- If there is an 'Ops' to the bottom of the stack it also assigns a 'Var' to it.
+-- the 'StackVars' to use it with and the first available (unassingned) 'RefId'.
 fromIndigoWithParams
-  :: forall inp n a . (AreIndigoParams n inp, KnownValue a)
+  :: forall n a inp.
+     (AreIndigoParams n inp, KnownValue a, Default (StackVars inp))
   => IndigoWithParams n inp a
-  -> MetaData inp
-  -> Sing n
-  -> (IndigoM a, MetaData inp)
-fromIndigoWithParams code md = \case
-  SZ -> (code, assignVarToOps md)
-  SS n -> let (md2, var) = withVarAt md n in fromIndigoWithParams @inp (code var) md2 n
+  -> (IndigoM a, StackVars inp, RefId)
+fromIndigoWithParams code = fromIndigoWithPeanoParams minBound def code (sing @(ToPeano n))
 
--- | Assigns a variable to the 'Ops' list at the bottom of the stack iff there is
--- one and it does not have one already. Otherwise returns the same 'MetaData'.
-assignVarToOps :: MetaData inp -> MetaData inp
-assignVarToOps md@(MetaData stk vRef) = case stk of
-  RNil -> md
-  (_ :& RNil) -> assingVarIfOps md
-  (x :& xs) -> case assignVarToOps $ MetaData xs vRef of
-    MetaData xs' vRef' -> MetaData (x :& xs') vRef'
+-- | 'Peano' version of 'fromIndigoWithParams'
+fromIndigoWithPeanoParams
+  :: forall inp n a. (AreIndigoPeanoParams n inp, KnownValue a)
+  => RefId
+  -> StackVars inp
+  -> IndigoWithPeanoParams n inp a
+  -> Sing n
+  -> (IndigoM a, StackVars inp, RefId)
+fromIndigoWithPeanoParams ref md code = \case
+  SZ -> (code, md, ref)
+  SS n -> let var = Var ref in
+    fromIndigoWithPeanoParams @inp (ref + 1) (assignVarAt var md n) (code var) n
 
-assingVarIfOps :: forall x. MetaData '[x] -> MetaData '[x]
-assingVarIfOps md@(MetaData stk vRef) = case stk of
-  (Ref _ :& RNil) -> md
-  ((NoRef :: StkEl x) :& RNil) -> case eqT @x @Ops of
-    Nothing -> md
-    Just Refl -> MetaData (Ref vRef :& RNil) (vRef + 1)
+-- | Converts an 'IndigoContract' to the equivalent 'IndigoM' with the storage,
+-- parameter and ops list as arguments.
+contractToIndigoWithParams
+  :: forall param st . KnownValue st
+  => IndigoContract param st
+  -> IndigoWithParams 3 '[param, st, Ops] ()
+contractToIndigoWithParams code = \varOps varSt varParam ->
+  (give varOps $ give varSt code) varParam
diff --git a/src/Indigo/Compilation/Sequential.hs b/src/Indigo/Compilation/Sequential.hs
new file mode 100644
--- /dev/null
+++ b/src/Indigo/Compilation/Sequential.hs
@@ -0,0 +1,669 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | 'Instruction' datatype and its compilations.
+--
+-- The idea behind this module is to provide an intermediate representation that
+-- can:
+--
+-- - be generated from the frontend freer monad
+-- - be compiled to the backend 'IndigoState'
+-- - be easy to analyze, manipulate and modify
+--
+-- This is meant to be the common ground for modular optimizations on the code
+-- before this is handed off to the backend and eventually translated to
+-- Michelson.
+
+module Indigo.Compilation.Sequential
+  ( Block
+  , Instruction (..)
+
+  , IndigoSeqCaseClause (..)
+  , CaseBranch (..)
+
+  -- * Translations
+  , indigoMtoSequential
+  , sequentialToLorentz
+
+  -- * Case machinery
+  , updateClauses
+  , mapMClauses
+  ) where
+
+import Util.TypeLits (AppendSymbol)
+import Data.Vinyl.Core (RMap(..))
+
+import Lorentz.Entrypoints.Helpers (RequireSumType)
+import qualified Lorentz.Run as L (Contract)
+import Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..))
+
+import Prelude
+import Indigo.Frontend.Program
+import qualified Indigo.Frontend.Statement as S
+import Indigo.Lorentz
+import Indigo.Internal (HasField, Expr)
+import Indigo.Internal.SIS
+import Indigo.Internal.Var
+import Indigo.Internal.Object (IsObject)
+import Indigo.Internal.State hiding ((>>))
+import qualified Indigo.Internal.State as St
+import Indigo.Backend
+
+-- | Simple synonym for a list of 'Instruction'
+type Block = [Instruction]
+
+-- | Data type representing an instruction.
+--
+-- Differently from the frontend this is not used to build a Monad of some kind,
+-- it is instead based on having as argument the variable to associate with the
+-- resulting value (if any).
+--
+-- This is combined in simple lists, named 'Block', and it is intended to be
+-- easily altered, this is because these are used as the intermediate representation
+-- between the frontend and the backend, where optimizations can occur.
+data Instruction where
+  LiftIndigoState :: (forall inp. SomeIndigoState inp) -> Instruction
+
+  AssignVar :: KnownValue x => Var x -> Expr x -> Instruction
+  SetVar :: KnownValue x => Var x -> Expr x -> Instruction
+  VarModification
+    :: (IsObject x, KnownValue y)
+    => [y, x] :-> '[x]
+    -> Var x
+    -> Expr y
+    -> Instruction
+  SetField
+    :: ( HasField store fname ftype
+       , IsObject store
+       , IsObject ftype
+       )
+    => Var store -> Label fname -> Expr ftype -> Instruction
+
+  LambdaCall1
+    :: LambdaKind st arg ret extra
+    -- ^ Kind of lambda (pure, storage modification, fully functional lambda with effects)
+    -> String
+    -- ^ Name of the lambda
+    -> Expr arg
+    -- ^ Expression for the lambda argument
+    -> Var arg
+    -- ^ Variable for the argument value (available to the lambda code block)
+    -> Block
+    -- ^ Code block for the lambda
+    -> ret
+    -- ^ Return value(s) of the lambda
+    -> RetVars ret
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+
+  CreateLambda1
+    :: CreateLambda1CGeneric extra arg ret
+    => StackVars (arg & extra)
+    -- ^ Initial 'StackVars' to be used in the lambda code
+    -> Var arg
+    -- ^ Variable for the argument value (available to the lambda code block)
+    -> Block
+    -- ^ Code block for the lambda
+    -> ret
+    -- ^ Return value(s) of the lambda
+    -> Var (Lambda1Generic extra arg ret)
+    -- ^ Variable that will be assigned to the resulting lambda
+    -> Instruction
+
+  ExecLambda1
+    :: LambdaKind st arg ret extra
+    -> Proxy ret
+    -> Expr arg
+    -- ^ Expression for the lambda argument
+    -> Var (Lambda1Generic extra arg ret)
+    -- ^ Variable of the lambda to be executed
+    -> RetVars ret
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+
+  Scope
+    :: ScopeCodeGen ret
+    => Block
+    -- ^ Code block to execute inside the scope
+    -> ret
+    -- ^ Return value(s) of the scoped code block
+    -> RetVars ret
+    -- ^ Variable that will be assigned to the resulting value(s)
+    -> Instruction
+  If
+    :: IfConstraint a b
+    => Expr Bool
+    -- ^ Expression for the control flow
+    -> Block
+    -- ^ Code block for the positive branch
+    -> a
+    -- ^ Return value(s) of the positive branch
+    -> Block
+    -- ^ Code block for the negative branch
+    -> b
+    -- ^ Return value(s) of the negative branch
+    -> RetVars a
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+  IfSome
+    :: (IfConstraint a b, KnownValue x)
+    => Expr (Maybe x)
+    -- ^ Expression for the control flow
+    -> Var x
+    -- ^ Variable for the 'Just' value (available to the next code block)
+    -> Block
+    -- ^ Code block for the 'Just' branch
+    -> a
+    -- ^ Return value(s) of the 'Just' branch
+    -> Block
+    -- ^ Code block for the 'Nothing' branch
+    -> b
+    -- ^ Return value(s) of the 'Nothing' branch
+    -> RetVars a
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+  IfRight
+    :: (IfConstraint a b, KnownValue r, KnownValue l)
+    => Expr (Either l r)
+    -- ^ Expression for the control flow
+    -> Var r
+    -- ^ Variable for the 'Right' value (available to the next code block)
+    -> Block
+    -- ^ Code block for the 'Right' branch
+    -> a
+    -- ^ Return value(s) of the 'Right' branch
+    -> Var l
+    -- ^ Variable for the 'Left' value (available to the next code block)
+    -> Block
+    -- ^ Code block for the 'Left' branch
+    -> b
+    -- ^ Return value(s) of the 'Left' branch
+    -> RetVars a
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+  IfCons
+    :: (IfConstraint a b, KnownValue x)
+    => Expr (List x)
+    -- ^ Expression for the control flow
+    -> Var x
+    -- ^ Variable for the "head" value (available to the next code block)
+    -> Var (List x)
+    -- ^ Variable for the "tail" value (available to the next code block)
+    -> Block
+    -- ^ Code block for the non-empty list branch
+    -> a
+    -- ^ Return value(s) of the non-empty list branch
+    -> Block
+    -- ^ Code block for the empty list branch
+    -> b
+    -- ^ Return value(s) of the empty list branch
+    -> RetVars a
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+
+  Case
+    :: CaseCommon dt ret clauses
+    => Expr dt
+    -> clauses
+    -> RetVars ret
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+  EntryCase
+    :: ( CaseCommon dt ret clauses
+       , DocumentEntrypoints entryPointKind dt
+       )
+    => Proxy entryPointKind
+    -> Expr dt
+    -> clauses
+    -> RetVars ret
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+  EntryCaseSimple
+    :: ( CaseCommon dt ret clauses
+       , DocumentEntrypoints PlainEntrypointsKind dt
+       , NiceParameterFull dt
+       , RequireFlatParamEps dt
+       )
+    => Expr dt
+    -> clauses
+    -> RetVars ret
+    -- ^ Variable(s) that will be assigned to the resulting value(s)
+    -> Instruction
+
+  While
+    :: Expr Bool
+    -- ^ Expression for the control flow
+    -> Block
+    -- ^ Block of code to execute, as long as the expression holds 'True'
+    -> Instruction
+  WhileLeft
+    :: (KnownValue l, KnownValue r)
+    => Expr (Either l r)
+    -- ^ Expression for the control flow value
+    -> Var l
+    -- ^ Variable for the 'Left' value (available to the code block)
+    -> Block
+    -- ^ Code block to execute while the value is 'Left'
+    -> Var r
+    -- ^ Variable that will be assigned to the resulting value
+    -> Instruction
+  ForEach
+    :: (IterOpHs a, KnownValue (IterOpElHs a))
+    => Expr a
+    -- ^ Expression for the container to traverse
+    -> Var (IterOpElHs a)
+    -- ^ Variable for the current item (available to the code block)
+    -> Block
+    -- ^ Code block to execute over each element of the container
+    -> Instruction
+
+  ContractName
+    :: Text
+    -> Block
+    -> Instruction
+  DocGroup
+    :: DocGrouping
+    -> Block
+    -> Instruction
+  ContractGeneral
+    :: Block
+    -> Instruction
+  FinalizeParamCallingDoc
+    :: (NiceParameterFull cp, RequireSumType cp)
+    => Var cp
+    -> Block
+    -> Expr cp
+    -> Instruction
+
+  TransferTokens
+    :: (NiceParameter p, HasSideEffects)
+    => Expr p
+    -> Expr Mutez
+    -> Expr (ContractRef p)
+    -> Instruction
+  SetDelegate
+    :: HasSideEffects
+    => Expr (Maybe KeyHash)
+    -> Instruction
+
+  CreateContract
+    :: (HasSideEffects, NiceStorage s, NiceParameterFull p)
+    => L.Contract p s
+    -> Expr (Maybe KeyHash)
+    -> Expr Mutez
+    -> Expr s
+    -> Var Address
+    -- ^ Variable that will be assigned to the resulting 'Address'
+    -> Instruction
+  SelfCalling
+    :: ( NiceParameterFull p
+       , KnownValue (GetEntrypointArgCustom p mname)
+       )
+    => Proxy p
+    -> EntrypointRef mname
+    -> Var (ContractRef (GetEntrypointArgCustom p mname))
+    -- ^ Variable that will be assigned to the resulting 'ContractRef'
+    -> Instruction
+  ContractCalling
+    :: ( HasEntrypointArg cp epRef epArg
+       , ToTAddress cp addr
+       , ToT addr ~ ToT Address
+       , KnownValue epArg
+       )
+    => Proxy cp
+    -> epRef
+    -> Expr addr
+    -> Var (Maybe (ContractRef epArg))
+    -- ^ Variable that will be assigned to the resulting 'ContractRef'
+    -> Instruction
+
+  Fail
+    :: (forall inp. SomeIndigoState inp)
+    -> Instruction
+  FailOver
+    :: (forall inp. Expr a -> SomeIndigoState inp)
+    -> Expr a
+    -> Instruction
+
+----------------------------------------------------------------------------
+-- Translations
+----------------------------------------------------------------------------
+
+-- | Data type internally used to collect 'Instruction's from 'IndigoM'
+data InstrCollector = InstrCollector
+  { nextRef :: RefId
+  , instrList :: Block
+  }
+
+-- | Transformation from 'IndigoM' to a 'Block' of 'Instruction's.
+--
+-- Requires the first non-used 'RefId' and returns the next one.
+indigoMtoSequential
+  :: RefId
+  -> IndigoM a
+  -> (Block, RefId)
+indigoMtoSequential refId code =
+  let InstrCollector {..} = snd $ instrCollect refId code
+  in (instrList, nextRef)
+
+-- | Collects instructions starting from an 'IndigoM'.
+-- Returns an 'InstrCollector' as well as the return value for that 'IndigoM'.
+instrCollect :: RefId -> IndigoM a -> (a, InstrCollector)
+instrCollect ref (IndigoM imCode) =
+  let instrColl = InstrCollector ref []
+      (res, resColl) = runState (interpretProgram collectStatement imCode) instrColl
+  in (res, InstrCollector (nextRef resColl) (reverse $ instrList resColl))
+
+-- | Collects instructions starting from 'S.StatementF'.
+-- IMPORTANT: the instructions are collected in the opposite order (as a stack).
+collectStatement :: S.StatementF IndigoM a -> State InstrCollector a
+collectStatement = \case
+  S.LiftIndigoState is -> appendNewInstr $ LiftIndigoState is
+  S.NewVar ex -> do
+    var <- mkNextVar
+    appendNewInstr $ AssignVar var ex
+    return var
+  S.SetVar vx ex -> appendNewInstr $ SetVar vx ex
+  S.VarModification upd vx ey -> appendNewInstr $ VarModification upd vx ey
+  S.SetField vStore fname exF -> appendNewInstr $ SetField vStore fname exF
+
+  S.LambdaCall1 lKind lName vIm ex -> withLambdaKind lKind $ do
+    (var, block, ret, retVars) <- collectInLambda vIm
+    appendNewInstr $ LambdaCall1 lKind lName ex var block ret retVars
+    return retVars
+
+  S.Scope (iM :: IndigoM ret) -> do
+    retVars <- allocateVars @ret mkNextVar
+    (ret, block) <- collectInner iM
+    appendNewInstr $ Scope block ret retVars
+    return retVars
+  S.If ex (iMa :: IndigoM ret) iMb -> do
+    retVars <- allocateVars @ret mkNextVar
+    (retA, blockA) <- collectInner iMa
+    (retB, blockB) <- collectInner iMb
+    appendNewInstr $ If ex blockA retA blockB retB retVars
+    return retVars
+  S.IfSome ex (vIMa :: Var x -> IndigoM ret) iMb -> do
+    retVars <- allocateVars @ret mkNextVar
+    varX <- mkNextVar
+    (retA, blockA) <- collectInner $ vIMa varX
+    (retB, blockB) <- collectInner iMb
+    appendNewInstr $ IfSome ex varX blockA retA blockB retB retVars
+    return retVars
+  S.IfRight ex (vIMa :: Var x -> IndigoM ret) vIMb -> do
+    retVars <- allocateVars @ret mkNextVar
+    varR <- mkNextVar
+    (retA, blockA) <- collectInner $ vIMa varR
+    varL <- mkNextVar
+    (retB, blockB) <- collectInner $ vIMb varL
+    appendNewInstr $ IfRight ex varR blockA retA varL blockB retB retVars
+    return retVars
+  S.IfCons ex (vvIMa :: Var x -> Var (List x) -> IndigoM ret) iMb -> do
+    retVars <- allocateVars @ret mkNextVar
+    varX <- mkNextVar
+    varLX <- mkNextVar
+    (retA, blockA) <- collectInner $ vvIMa varX varLX
+    (retB, blockB) <- collectInner iMb
+    appendNewInstr $ IfCons ex varX varLX blockA retA blockB retB retVars
+    return retVars
+
+  S.Case grd clauses -> do
+    retVars <- allocateClausesVars clauses
+    blockClauses <- collectClauses clauses
+    appendNewInstr $ Case grd blockClauses retVars
+    return retVars
+  S.EntryCase proxy grd clauses -> do
+    retVars <- allocateClausesVars clauses
+    blockClauses <- collectClauses clauses
+    appendNewInstr $ EntryCase proxy grd blockClauses retVars
+    return retVars
+  S.EntryCaseSimple grd clauses -> do
+    retVars <- allocateClausesVars clauses
+    blockClauses <- collectClauses clauses
+    appendNewInstr $ EntryCaseSimple grd blockClauses retVars
+    return retVars
+
+  S.While ex iM -> do
+    ((), block) <- collectInner iM
+    appendNewInstr $ While ex block
+  S.WhileLeft ex vIm -> do
+    varL <- mkNextVar
+    varR <- mkNextVar
+    ((), block) <- collectInner $ vIm varL
+    appendNewInstr $ WhileLeft ex varL block varR
+    return varR
+  S.ForEach ex vIm -> do
+    varIop <- mkNextVar
+    ((), block) <- collectInner $ vIm varIop
+    appendNewInstr $ ForEach ex varIop block
+
+  S.ContractName tx iM -> do
+    ((), block) <- collectInner iM
+    appendNewInstr $ ContractName tx block
+  S.DocGroup dg iM -> do
+    ((), block) <- collectInner iM
+    appendNewInstr $ DocGroup dg block
+  S.ContractGeneral iM -> do
+    ((), block) <- collectInner iM
+    appendNewInstr $ ContractGeneral block
+  S.FinalizeParamCallingDoc vIm param -> do
+    varCp <- mkNextVar
+    ((), block) <- collectInner $ vIm varCp
+    appendNewInstr $ FinalizeParamCallingDoc varCp block param
+
+  S.TransferTokens ex exm exc ->
+    appendNewInstr $ TransferTokens ex exm exc
+  S.SetDelegate ex ->
+    appendNewInstr $ SetDelegate ex
+  S.CreateContract ctrc exk exm exs -> do
+    varAddr <- mkNextVar
+    appendNewInstr $ CreateContract ctrc exk exm exs varAddr
+    return varAddr
+  S.SelfCalling proxy ep -> do
+    varCR <- mkNextVar
+    appendNewInstr $ SelfCalling proxy ep varCR
+    return varCR
+  S.ContractCalling proxy epRef exAddr -> do
+    varMcr <- mkNextVar
+    appendNewInstr $ ContractCalling proxy epRef exAddr varMcr
+    return varMcr
+
+  S.Fail (_ :: Proxy ret) failure -> do
+    appendNewInstr $ Fail failure
+    -- Note: because this is a failing instr, this vars are effectively never used
+    allocateVars @ret mkNextVar
+  S.FailOver (_ :: Proxy ret) failure ex -> do
+    appendNewInstr $ FailOver failure ex
+    -- Note: because this is a failing instr, this vars are effectively never used
+    allocateVars @ret mkNextVar
+
+-- | Continues collecting 'Instruction's from an inner 'IndigoM' (e.g. scoped).
+-- This keeps advancing the ref counter as well.
+collectInner :: IndigoM ret -> State InstrCollector (ret, Block)
+collectInner iM = do
+  iColl <- get
+  let (ret, InstrCollector newRef block) = instrCollect (nextRef iColl) iM
+  put $ iColl {nextRef = newRef}
+  return (ret, block)
+
+-- | Just a common set of steps used by collection of single-arg lambda's values.
+collectInLambda
+  :: ScopeCodeGen ret
+  => (Var arg -> IndigoM ret)
+  -> State InstrCollector (Var arg, Block, ret, RetVars ret)
+collectInLambda vIm = do
+  var <- mkNextVar
+  (ret :: ret, block) <- collectInner $ vIm var
+  retVars <- allocateVars @ret mkNextVar
+  return (var, block, ret, retVars)
+
+-- | Append a new 'Instruction' to the head of the list in the state.
+appendNewInstr :: Instruction -> State InstrCollector ()
+appendNewInstr is = modify $ \iColl -> iColl {instrList = is : instrList iColl}
+
+-- | Creates a new var. This simply advances the ref counter and updates it.
+mkNextVar :: State InstrCollector (Var a)
+mkNextVar = do
+  iColl <- get
+  let ref = nextRef iColl
+  put $ iColl {nextRef = ref + 1}
+  return $ Var ref
+
+-- | Translation from a 'Block' and an initial 'MetaData' to Lorentz.
+sequentialToLorentz
+  :: MetaData inp
+  -> (Block, RefId)
+  -> inp :-> inp
+sequentialToLorentz md block =
+  runSIS (sequentialToSIS block) md St.cleanGenCode
+
+-- | Translation from a 'Block' to a 'SomeIndigoState'.
+sequentialToSIS :: (Block, RefId) -> SomeIndigoState inp
+sequentialToSIS ([], _) = toSIS St.nopState
+sequentialToSIS (x : xs, refId) = instrToSIS refId x `thenSIS` sequentialToSIS (xs, refId)
+
+-- | Translation from a single 'Instruction' to a 'SomeIndigoState'.
+instrToSIS :: RefId -> Instruction -> SomeIndigoState inp
+instrToSIS nextRef = \case
+  LiftIndigoState sis -> sis
+  AssignVar vx ex -> toSIS $ assignVar vx ex
+  SetVar vx ex -> toSIS $ setVar nextRef vx ex
+  VarModification upd vx ey -> toSIS $ updateVar nextRef upd vx ey
+  SetField vSt lName ex -> toSIS $ setField nextRef vSt lName ex
+
+  LambdaCall1 lKind _lName ex var block ret retVars ->
+    withLambdaKind lKind $
+      toSIS $ scope (sequentialToSIS (AssignVar var ex : block, nextRef)) ret retVars
+  CreateLambda1 lamMd _var body ret varLam ->
+    toSIS $ createLambda1Generic varLam ret lamMd (sequentialToSIS (body, nextRef))
+  ExecLambda1 lKind (Proxy :: Proxy ret) ex varLam retVars ->
+    toSIS $ executeLambda1 @ret lKind nextRef retVars varLam ex
+
+  Scope block ret retVars ->
+    toSIS $ scope (sequentialToSIS (block, nextRef)) ret retVars
+  If ex blockA retA blockB retB retVars ->
+    toSIS $ if_ ex (sequentialToSIS (blockA, nextRef)) retA (sequentialToSIS (blockB, nextRef)) retB retVars
+  IfSome ex varX blockA retA blockB retB retVars ->
+    toSIS $ ifSome ex varX (sequentialToSIS (blockA, nextRef)) retA (sequentialToSIS (blockB, nextRef)) retB retVars
+  IfRight ex varR blockA retA varL blockB retB retVars ->
+    toSIS $ ifRight ex varR (sequentialToSIS (blockA, nextRef)) retA varL (sequentialToSIS (blockB, nextRef)) retB retVars
+  IfCons ex varX varLX blockA retA blockB retB retVars ->
+    toSIS $ ifCons ex varX varLX (sequentialToSIS (blockA, nextRef)) retA (sequentialToSIS (blockB, nextRef)) retB retVars
+
+  Case grd blockClauses retVars ->
+    toSIS $ caseRec grd (clausesToBackend nextRef blockClauses) retVars
+  EntryCase proxy grd blockClauses retVars ->
+    toSIS $ entryCaseRec proxy grd (clausesToBackend nextRef blockClauses) retVars
+  EntryCaseSimple grd blockClauses retVars ->
+    toSIS $ entryCaseSimpleRec grd (clausesToBackend nextRef blockClauses) retVars
+
+  While ex block ->
+    toSIS $ while ex (sequentialToSIS (block, nextRef))
+  WhileLeft ex varL block varR ->
+    toSIS $ whileLeft ex varL (sequentialToSIS (block, nextRef)) varR
+  ForEach ex varIop block ->
+    toSIS $ forEach ex varIop (sequentialToSIS (block, nextRef))
+
+  ContractName tx block ->
+    contractName tx (sequentialToSIS (block, nextRef))
+  DocGroup dg block ->
+    docGroup dg (sequentialToSIS (block, nextRef))
+  ContractGeneral block ->
+    contractGeneral (sequentialToSIS (block, nextRef))
+  FinalizeParamCallingDoc varCp block param ->
+    finalizeParamCallingDoc varCp (sequentialToSIS (block, nextRef)) param
+
+  TransferTokens ex exm exc ->
+    toSIS $ transferTokens ex exm exc
+  SetDelegate ex ->
+    toSIS $ setDelegate ex
+  CreateContract ctrc exk exm exs varAddr ->
+    toSIS $ createContract ctrc exk exm exs varAddr
+  SelfCalling (Proxy :: Proxy p) ep varCR ->
+    toSIS $ selfCalling @p ep varCR
+  ContractCalling (Proxy :: Proxy cp) epRef exAddr varMcr ->
+    toSIS $ contractCalling @cp epRef exAddr varMcr
+
+  Fail failure -> failure
+  FailOver failure ex -> failure ex
+
+----------------------------------------------------------------------------
+-- Case machinery
+----------------------------------------------------------------------------
+
+-- | Common constraint for case-like 'Instruction's.
+type CaseCommon dt ret clauses = CaseCommonF IndigoSeqCaseClause dt ret clauses
+
+-- | Analogous datatype as 'IndigoCaseClauseL' and 'IndigoMCaseClauseL'.
+data IndigoSeqCaseClause ret (param :: CaseClauseParam) where
+  OneFieldIndigoSeqCaseClause
+    :: (AppendSymbol "c" ctor ~ name)
+    => Label name
+    -> CaseBranch x ret
+    -> IndigoSeqCaseClause ret ('CaseClauseParam ctor ('OneField x))
+
+-- | Representation of a branch of a generic case-like 'Instruction'.
+data CaseBranch x ret where
+  CaseBranch
+    :: ( KnownValue x
+       , ScopeCodeGen retBr
+       , ret ~ RetExprs retBr
+       , RetOutStack ret ~ RetOutStack retBr
+       )
+    => Var x
+    -- ^ Input variable (accessible to the branch's code block)
+    -> Block
+    -- ^ Code block for this branch
+    -> retBr
+    -- ^ Return value of this branch
+    -> CaseBranch x ret
+
+-- | Convert clauses from their "sequential" representation to the "backend" one.
+clausesToBackend
+  :: forall ret dt . RMap dt
+  => RefId
+  -> Rec (IndigoSeqCaseClause ret) dt
+  -> Rec (IndigoCaseClauseL ret) dt
+clausesToBackend nextRef = rmap $
+  \(OneFieldIndigoSeqCaseClause cName (CaseBranch vx block ret)) ->
+    cName /-> (IndigoClause vx (sequentialToSIS (block, nextRef)) ret)
+
+-- | Allocate vars for the return value(s) of a clause-like 'Instruction'.
+allocateClausesVars
+  :: forall ret dt. ReturnableValue ret
+  => Rec (S.IndigoMCaseClauseL IndigoM ret) dt
+  -> State InstrCollector (RetVars ret)
+allocateClausesVars _ = allocateVars @ret mkNextVar
+
+-- | Collects clauses of a case-like statement.
+collectClauses
+  :: Rec (S.IndigoMCaseClauseL IndigoM ret) dt
+  -> State InstrCollector (Rec (IndigoSeqCaseClause ret) dt)
+collectClauses RNil = return RNil
+collectClauses ((S.OneFieldIndigoMCaseClauseL cName clause) :& xs) = do
+  varX <- mkNextVar
+  (ret, block) <- collectInner $ clause varX
+  let clauseX = OneFieldIndigoSeqCaseClause cName (CaseBranch varX block ret)
+  clauseXs <- collectClauses xs
+  return $ clauseX :& clauseXs
+
+-- | Applies the given 'Block' to 'Block' transformation to the inner code block
+-- of every case clause.
+updateClauses
+  :: (Block -> Block)
+  -> Rec (IndigoSeqCaseClause ret) dt
+  -> Rec (IndigoSeqCaseClause ret) dt
+updateClauses _ RNil = RNil
+updateClauses f (x :& xs) = case x of
+  OneFieldIndigoSeqCaseClause cName (CaseBranch vx block ret) ->
+    OneFieldIndigoSeqCaseClause cName (CaseBranch vx (f block) ret)
+      :& updateClauses f xs
+
+-- | Applies the given monadic function giving it the inner code block of each
+-- case clause, in order.
+mapMClauses :: Monad m => (Block -> m ()) -> Rec (IndigoSeqCaseClause ret) dt -> m ()
+mapMClauses _ RNil = return ()
+mapMClauses f (x :& xs) = case x of
+  OneFieldIndigoSeqCaseClause _cName (CaseBranch _ block _) ->
+    f block >> mapMClauses f xs
diff --git a/src/Indigo/Frontend/Language.hs b/src/Indigo/Frontend/Language.hs
--- a/src/Indigo/Frontend/Language.hs
+++ b/src/Indigo/Frontend/Language.hs
@@ -2,7 +2,7 @@
 --
 -- SPDX-License-Identifier: LicenseRef-MIT-TQ
 
--- | Duplication of Backend functions, but without input and output stack.
+-- | Frontend statements's functions of the Indigo Language.
 
 module Indigo.Frontend.Language
   ( -- * Assignment and modifications
@@ -93,6 +93,13 @@
   , failUnexpected_
   , assertCustom
   , assertCustom_
+  , assertSome
+  , assertNone
+  , assertRight
+  , assertLeft
+  -- * Re-exports
+  , ReturnableValue
+  , RetVars
 
   -- * Comments
   , comment
@@ -116,7 +123,7 @@
 import Indigo.Compilation (compileIndigoContract)
 import Indigo.Frontend.Program
 import Indigo.Frontend.Statement
-import Indigo.Internal hiding (SetField, return, (>>), (>>=))
+import Indigo.Internal hiding (SetField, (>>))
 import Indigo.Lorentz
 import Indigo.Prelude
 import Lorentz.Entrypoints.Helpers (RequireSumType)
@@ -132,7 +139,7 @@
 oneIndigoM :: StatementF IndigoM a -> IndigoM a
 oneIndigoM st = IndigoM (Instr st)
 
-liftIndigoState :: (forall inp. SomeIndigoState inp a) -> IndigoM a
+liftIndigoState :: (forall inp. SomeIndigoState inp) -> IndigoM ()
 liftIndigoState code = IndigoM (Instr $ LiftIndigoState code)
 
 varModification
@@ -149,7 +156,7 @@
 new = oneIndigoM . NewVar . toExpr
 
 -- | Set the given variable to the result of the given expression.
-setVar :: (IsExpr ex x) => Var x -> ex -> IndigoM ()
+setVar :: IsExpr ex x => Var x -> ex -> IndigoM ()
 setVar v = oneIndigoM . SetVar v . toExpr
 
 infixr 0 =:
@@ -446,13 +453,11 @@
 {-# DEPRECATED (//->) "use '#=' instead" #-}
 -- | An alias for '#=' kept only for backward compatibility.
 (//->)
-  :: ( CaseArrow name (Var x -> IndigoAnyOut x ret)
-                      (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
+  :: ( name ~ (AppendSymbol "c" ctor)
+     , KnownValue x
      , ScopeCodeGen retBr
      , ret ~ RetExprs retBr
      , RetOutStack ret ~ RetOutStack retBr
-     , KnownValue x
-     , name ~ (AppendSymbol "c" ctor)
      )
   => Label name
   -> (Var x -> IndigoM retBr)
@@ -469,13 +474,11 @@
 -- It has the added benefit of not being an arrow, so in case the body of the
 -- clause is a lambda there won't be several.
 (#=)
-  :: ( CaseArrow name (Var x -> IndigoAnyOut x ret)
-                      (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
+  :: ( name ~ (AppendSymbol "c" ctor)
+     , KnownValue x
      , ScopeCodeGen retBr
      , ret ~ RetExprs retBr
      , RetOutStack ret ~ RetOutStack retBr
-     , KnownValue x
-     , name ~ (AppendSymbol "c" ctor)
      )
   => Label name
   -> (Var x -> IndigoM retBr)
@@ -547,12 +550,13 @@
   ( ToExpr argExpr
   , Typeable res
   , ExecuteLambdaEff1C st (ExprType argExpr) res
-  , CreateLambdaEff1C st (ExprType argExpr) res)
+  , CreateLambdaEff1C st (ExprType argExpr) res
+  )
   => String
   -> (Var (ExprType argExpr) -> IndigoM res)
   -> (argExpr -> IndigoM (RetVars res))
 defNamedEffLambda1 lName body = \ex ->
-  oneIndigoM $ LambdaEff1Call (Proxy @st) lName body (toExpr ex)
+  oneIndigoM $ LambdaCall1 (EffLambda (Proxy @st)) lName body (toExpr ex)
 
 -- | Like defNamedEffLambda1 but doesn't make side effects.
 defNamedLambda1
@@ -565,7 +569,7 @@
   -> (Var (ExprType argExpr) -> IndigoM res)
   -> (argExpr -> IndigoM (RetVars res))
 defNamedLambda1 lName body = \ex ->
-  oneIndigoM $ Lambda1Call (Proxy @st) lName body (toExpr ex)
+  oneIndigoM $ LambdaCall1 (StorageLambda (Proxy @st)) lName body (toExpr ex)
 
 -- | Like defNamedLambda1 but doesn't take an argument.
 defNamedLambda0
@@ -576,7 +580,8 @@
   => String
   -> IndigoM res
   -> IndigoM (RetVars res)
-defNamedLambda0 lName body = oneIndigoM $ Lambda1Call (Proxy @st) lName (\(_ :: Var ()) -> body) (C ())
+defNamedLambda0 lName body =
+  oneIndigoM $ LambdaCall1 (StorageLambda (Proxy @st)) lName (\(_ :: Var ()) -> body) (C ())
 
 -- | Like defNamedEffLambda1 but doesn't modify storage and doesn't make side effects.
 defNamedPureLambda1
@@ -589,7 +594,7 @@
   -> (Var (ExprType argExpr) -> IndigoM res)
   -> (argExpr -> IndigoM (RetVars res))
 defNamedPureLambda1 lName body = \ex ->
-  oneIndigoM $ LambdaPure1Call lName body (toExpr ex)
+  oneIndigoM $ LambdaCall1 PureLambda lName body (toExpr ex)
 
 ----------------------------------------------------------------------------
 -- Loop
@@ -649,13 +654,13 @@
 
 -- | Indigo version for the homonym Lorentz function.
 finalizeParamCallingDoc
-  :: forall param x.
+  :: forall param.
      ( ToExpr param
      , NiceParameterFull (ExprType param)
      , RequireSumType (ExprType param)
      , HasCallStack
      )
-  => (Var (ExprType param) -> IndigoM x) -> param -> IndigoM x
+  => (Var (ExprType param) -> IndigoM ()) -> param -> IndigoM ()
 finalizeParamCallingDoc i = oneIndigoM . FinalizeParamCallingDoc i . toExpr
 
 -- | Put a 'DDescription' doc item.
@@ -681,7 +686,7 @@
      )
   => EntrypointRef mname
   -> IndigoM (Var (ContractRef (GetEntrypointArgCustom p mname)))
-selfCalling ep = liftIndigoState $ toSIS $ B.selfCalling @p ep
+selfCalling = oneIndigoM ... SelfCalling (Proxy @p)
 
 contractCalling
   :: forall cp epRef epArg addr exAddr.
@@ -743,40 +748,49 @@
 -- Error
 ----------------------------------------------------------------------------
 
-assert
-  :: forall x ex.
-     ( IsError x
-     , IsExpr ex Bool
-     )
-  => x -> ex -> IndigoM ()
-assert x = oneIndigoM . Assert x . toExpr
-
 failWith
-  :: forall r a ex . IsExpr ex a
-  => ex -> IndigoM r
-failWith = oneIndigoM . FailWith . toExpr
+  :: forall ret a ex . (IsExpr ex a, ReturnableValue ret)
+  => ex -> IndigoM (RetVars ret)
+failWith = oneIndigoM . FailOver (Proxy @ret) (toSIS . B.failWith) . toExpr
 
+failUsing_
+  :: forall ret x. (IsError x, ReturnableValue ret)
+  => x -> IndigoM (RetVars ret)
+failUsing_ x = oneIndigoM $ Fail (Proxy @ret) (toSIS $ B.failUsing_ x)
+
 failCustom
-  :: forall r tag err ex.
-     ( err ~ ErrorArg tag
+  :: forall ret tag err ex.
+     ( ReturnableValue ret
+     , err ~ ErrorArg tag
      , CustomErrorHasDoc tag
      , NiceConstant err
      , ex :~> err
      )
-  => Label tag -> ex -> IndigoM r
-failCustom l = oneIndigoM . FailCustom l . toExpr
+  => Label tag -> ex -> IndigoM (RetVars ret)
+failCustom l = oneIndigoM . FailOver (Proxy @ret) (toSIS . B.failCustom l) . toExpr
 
 failCustom_
-  :: forall r tag notVoidErrorMsg.
-     ( RequireNoArgError tag notVoidErrorMsg
+  :: forall ret tag notVoidErrorMsg.
+     ( ReturnableValue ret
+     , RequireNoArgError tag notVoidErrorMsg
      , CustomErrorHasDoc tag
      )
-  => Label tag -> IndigoM r
-failCustom_ lab = liftIndigoState $ toSIS $ B.failCustom_ lab
+  => Label tag -> IndigoM (RetVars ret)
+failCustom_ tag = oneIndigoM $ Fail (Proxy @ret) (toSIS $ B.failCustom_ tag)
 
-failUnexpected_ :: MText -> IndigoM r
-failUnexpected_ tx = liftIndigoState $ toSIS $ B.failUnexpected_ tx
+failUnexpected_
+  :: forall ret. ReturnableValue ret
+  => MText -> IndigoM (RetVars ret)
+failUnexpected_ tx = oneIndigoM $ Fail (Proxy @ret) (toSIS $ B.failUnexpected_ tx)
 
+assert
+  :: forall x ex.
+     ( IsError x
+     , IsExpr ex Bool
+     )
+  => x -> ex -> IndigoM ()
+assert err ex = if_ ex (return ()) (failUsing_ @() err)
+
 assertCustom
   :: forall tag err errEx ex .
      ( err ~ ErrorArg tag
@@ -786,7 +800,7 @@
      , IsExpr ex Bool
      )
   => Label tag -> errEx -> ex -> IndigoM ()
-assertCustom tag errEx e = if_ (toExpr e) (return ()) (failCustom tag errEx :: IndigoM ())
+assertCustom tag errEx ex = if_ ex (return ()) (failCustom @() tag errEx)
 
 assertCustom_
   :: forall tag notVoidErrorMsg ex.
@@ -795,7 +809,45 @@
      , IsExpr ex Bool
      )
   => Label tag -> ex -> IndigoM ()
-assertCustom_ tag e = if_ (toExpr e) (return ()) (failCustom_ tag :: IndigoM ())
+assertCustom_ tag ex = if_ ex (return ()) (failCustom_ @() tag)
+
+assertSome
+  :: forall x err ex.
+  ( IsError err
+  , KnownValue x
+  , ex :~> Maybe x
+  )
+  => err -> ex -> IndigoM ()
+assertSome err ex = ifSome ex (\_ -> failUsing_ @() err) (return ())
+
+assertNone
+  :: forall x err ex.
+  ( IsError err
+  , KnownValue x
+  , ex :~> Maybe x
+  )
+  => err -> ex -> IndigoM ()
+assertNone err ex = ifSome ex (\_ -> return ()) (failUsing_ @() err)
+
+assertRight
+  :: forall x y err ex.
+  ( IsError err
+  , KnownValue x
+  , KnownValue y
+  , ex :~> Either y x
+  )
+  => err -> ex -> IndigoM ()
+assertRight err ex = ifRight ex (\_ -> failUsing_ @() err) (\_ -> return ())
+
+assertLeft
+  :: forall x y err ex.
+  ( IsError err
+  , KnownValue x
+  , KnownValue y
+  , ex :~> Either y x
+  )
+  => err -> ex -> IndigoM ()
+assertLeft err ex = ifRight ex (\_ -> return ()) (\_ -> failUsing_ @() err)
 
 ----------------------------------------------------------------------------
 -- Comments
diff --git a/src/Indigo/Frontend/Program.hs b/src/Indigo/Frontend/Program.hs
--- a/src/Indigo/Frontend/Program.hs
+++ b/src/Indigo/Frontend/Program.hs
@@ -7,12 +7,15 @@
 
   , Program (..)
   , interpretProgram
+
+  , IndigoContract
   ) where
 
 import Control.Monad (liftM)
-import Prelude
 
 import Indigo.Frontend.Statement
+import Indigo.Internal.Var (HasSideEffects, HasStorage, Var)
+import Indigo.Prelude
 
 -- | This is freer monad (in other words operational monad).
 --
@@ -55,3 +58,7 @@
 newtype IndigoM a = IndigoM {unIndigoM :: Program (StatementF IndigoM) a}
   deriving stock (Functor)
   deriving newtype (Applicative, Monad)
+
+-- | Type of a contract that can be compiled to Lorentz with 'compileIndigoContract'.
+type IndigoContract param st =
+  (HasStorage st, HasSideEffects) => Var param -> IndigoM ()
diff --git a/src/Indigo/Frontend/Statement.hs b/src/Indigo/Frontend/Statement.hs
--- a/src/Indigo/Frontend/Statement.hs
+++ b/src/Indigo/Frontend/Statement.hs
@@ -9,7 +9,8 @@
 
   , IfConstraint
   , IndigoMCaseClauseL (..)
-  , CaseCommonF
+  , LambdaKind (..)
+  , withLambdaKind
   ) where
 
 import qualified Data.Kind as Kind
@@ -19,18 +20,15 @@
 import qualified Lorentz.Run as L (Contract)
 import Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..))
 
-import Indigo.Prelude
-import Indigo.Lorentz
-import Indigo.Internal
 import Indigo.Backend
+import Indigo.Internal
+import Indigo.Lorentz
+import Indigo.Prelude
 
 -- | Analogous datatype as IndigoCaseClauseL from Indigo.Backend.Case
 data IndigoMCaseClauseL freer ret (param :: CaseClauseParam) where
     OneFieldIndigoMCaseClauseL
-      :: ( CaseArrow name
-                     (Var x -> IndigoAnyOut x ret)
-                     (IndigoCaseClauseL ret ('CaseClauseParam ctor ('OneField x)))
-         , name ~ (AppendSymbol "c" ctor)
+      :: ( name ~ (AppendSymbol "c" ctor)
          , KnownValue x
          , ScopeCodeGen retBr
          , ret ~ RetExprs retBr
@@ -56,10 +54,10 @@
 data StatementF (freer :: Kind.Type -> Kind.Type) a where
   -- | Direct injection of IndigoState of statements
   -- which are not going to be analyzed by optimizer.
-  LiftIndigoState :: (forall inp . SomeIndigoState inp a) -> StatementF freer a
+  LiftIndigoState :: (forall inp. SomeIndigoState inp) -> StatementF freer ()
 
   NewVar :: KnownValue x => Expr x -> StatementF freer (Var x)
-  SetVar :: Var x -> Expr x -> StatementF freer ()
+  SetVar :: KnownValue x => Var x -> Expr x -> StatementF freer ()
   VarModification
     :: (IsObject x, KnownValue y)
     => [y, x] :-> '[x]
@@ -73,27 +71,8 @@
     )
     => Var dt -> Label fname -> Expr ftype -> StatementF cont ()
 
-  -- | Pure lambda
-  LambdaPure1Call
-    :: (ExecuteLambdaPure1C arg res, CreateLambdaPure1C arg res, Typeable res)
-    => String
-    -> (Var arg -> freer res)
-    -> Expr arg
-    -> StatementF freer (RetVars res)
-
-  -- | "Default" lambda which can modify storage
-  Lambda1Call
-    :: (ExecuteLambda1C st arg res, CreateLambda1C st arg res, Typeable res)
-    => Proxy st
-    -> String
-    -> (Var arg -> freer res)
-    -> Expr arg
-    -> StatementF freer (RetVars res)
-
-  -- | Lambda which can modify storage and emit operations
-  LambdaEff1Call
-    :: (ExecuteLambdaEff1C st arg res, CreateLambdaEff1C st arg res, Typeable res)
-    => Proxy st
+  LambdaCall1
+    :: LambdaKind st arg res extra
     -> String
     -> (Var arg -> freer res)
     -> Expr arg
@@ -163,7 +142,7 @@
   ContractGeneral :: freer () -> StatementF freer ()
   FinalizeParamCallingDoc
     :: (NiceParameterFull cp, RequireSumType cp, HasCallStack)
-    => (Var cp -> freer x) -> Expr cp -> StatementF freer x
+    => (Var cp -> freer ()) -> Expr cp -> StatementF freer ()
 
   TransferTokens
     :: (NiceParameter p, HasSideEffects)
@@ -180,6 +159,13 @@
     -> Expr Mutez
     -> Expr st
     -> StatementF freer (Var Address)
+  SelfCalling
+    :: ( NiceParameterFull p
+       , KnownValue (GetEntrypointArgCustom p mname)
+       )
+    => Proxy p
+    -> EntrypointRef mname
+    -> StatementF freer (Var (ContractRef (GetEntrypointArgCustom p mname)))
   ContractCalling
     :: ( HasEntrypointArg cp epRef epArg
        , ToTAddress cp addr
@@ -188,11 +174,16 @@
        )
     => Proxy cp -> epRef -> Expr addr -> StatementF freer (Var (Maybe (ContractRef epArg)))
 
-  FailWith :: KnownValue a => Expr a -> StatementF freer r
-  Assert :: IsError x => x -> Expr Bool -> StatementF freer ()
-  FailCustom
-    :: ( err ~ ErrorArg tag
-       , CustomErrorHasDoc tag
-       , NiceConstant err
-       )
-    => Label tag -> Expr err -> StatementF freer r
+  -- Generic failing statements, hardly more than 'LiftIndigoState', but with the
+  -- knowledge that they end in a failure.
+  Fail
+    :: ReturnableValue ret
+    => Proxy ret
+    -> (forall inp. SomeIndigoState inp)
+    -> StatementF freer (RetVars ret)
+  FailOver
+    :: ReturnableValue ret
+    => Proxy ret
+    -> (forall inp. Expr a -> SomeIndigoState inp)
+    -> Expr a
+    -> StatementF freer (RetVars ret)
diff --git a/src/Indigo/Internal.hs b/src/Indigo/Internal.hs
--- a/src/Indigo/Internal.hs
+++ b/src/Indigo/Internal.hs
@@ -12,3 +12,4 @@
 import Indigo.Internal.SIS as ReExports
 import Indigo.Internal.State as ReExports
 import Indigo.Internal.Object as ReExports
+import Indigo.Internal.Var as ReExports
diff --git a/src/Indigo/Internal/Expr.hs b/src/Indigo/Internal/Expr.hs
--- a/src/Indigo/Internal/Expr.hs
+++ b/src/Indigo/Internal/Expr.hs
@@ -4,10 +4,6 @@
 
 -- | 'Expr'essions supported in Indigo language and their compilation to
 -- Lorentz code.
---
--- This module contains only basic building blocks that can be used to
--- implement anything else. Other modules provide high level language
--- constructions and standard functions.
 
 module Indigo.Internal.Expr
   ( module Exported
diff --git a/src/Indigo/Internal/Expr/Compilation.hs b/src/Indigo/Internal/Expr/Compilation.hs
--- a/src/Indigo/Internal/Expr/Compilation.hs
+++ b/src/Indigo/Internal/Expr/Compilation.hs
@@ -9,6 +9,7 @@
 
   , ObjManipulationRes (..)
   , runObjectManipulation
+  , namedToExpr
 
   , nullaryOp
   , unaryOp
@@ -31,19 +32,19 @@
 import Indigo.Backend.Prelude
 import Indigo.Internal.Expr.Types
 import Indigo.Internal.Field
+import Indigo.Internal.State (DecomposedObjects, withObject)
 import Indigo.Internal.Lookup (varActionGet)
+import Indigo.Internal.Var (pushNoRef, Var(..))
 import Indigo.Internal.Object
-  (IndigoObjectF(..), NamedFieldVar(..), castFieldConstructors, namedToTypedRec, pushNoRefMd,
+  (IndigoObjectF(..), NamedFieldObj(..), castFieldConstructors, namedToTypedRec,
   typedToNamedRec)
 import Indigo.Internal.State
-  (GenCode(..), IndigoState(..), MetaData(..), iget, iput, usingIndigoState, (>>=))
+  (GenCode(..), IndigoState(..), usingIndigoState, withObjectState, MetaData (..), replStkMd)
 import Indigo.Lorentz
 
-compileExpr :: forall a inp . Expr a -> IndigoState inp (a & inp) ()
-compileExpr (C a) = do
-  md <- iget
-  iput $ GenCode () (pushNoRefMd md) (L.push a) L.drop
-compileExpr (V v) = compileObjectF (\(NamedFieldVar fl) -> V fl) v
+compileExpr :: forall a inp . Expr a -> IndigoState inp (a & inp)
+compileExpr (C a) = IndigoState $ \md -> GenCode (pushNoRef $ mdStack md) (L.push a) L.drop
+compileExpr (V v) = withObjectState v $ compileObjectF namedToExpr
 compileExpr (Update m key val) = ternaryOp key val m L.update
 compileExpr (Add e1 e2) = binaryOp e1 e2 L.add
 compileExpr (Sub e1 e2)  = binaryOp e1 e2 L.sub
@@ -110,12 +111,12 @@
 compileExpr (ObjMan fldAcc) = compileObjectManipulation fldAcc
 compileExpr (Construct fields) = IndigoState $ \md ->
   let cd = L.construct $ rmap (\e -> fieldCtor $ gcCode $ runIndigoState (compileExpr e) md) fields in
-  GenCode () (pushNoRefMd md) cd L.drop
+  GenCode (pushNoRef $ mdStack md) cd L.drop
 compileExpr (ConstructWithoutNamed fields) = IndigoState $ \md ->
   let fieldCtrs =
           castFieldConstructors @a $
             rmap (fieldCtor . gcCode . usingIndigoState md . compileExpr) fields
-  in GenCode () (pushNoRefMd md) (L.construct @a fieldCtrs) L.drop
+  in GenCode (pushNoRef $ mdStack md) (L.construct @a fieldCtrs) L.drop
 compileExpr (Name l e) = unaryOp e (toNamed l)
 compileExpr (UnName l e) = unaryOp e (fromNamed l)
 
@@ -145,36 +146,42 @@
 compileExpr (Exec inp lambda) = binaryOp inp lambda L.exec
 compileExpr (NonZero e) = unaryOp e L.nonZero
 
--- | Convert arbitrary 'IndigoObjectF' into 'Expr',
--- having converter for fields.
+--------------------------------------------
+-- Object manipulation: set, get fields
+--------------------------------------------
+
+-- | Compile 'ObjectManipulation' datatype to a cell on the stack.
+-- This function leverages 'ObjManipulationRes' to put off actual field compilation.
+compileObjectManipulation :: ObjectManipulation a -> IndigoState inp (a & inp)
+compileObjectManipulation fa = IndigoState $ \md -> case runObjectManipulation (mdObjects md) fa of
+  StillObject composite -> usingIndigoState md $ compileObjectF unNamedFieldExpr composite
+  OnStack computation   -> usingIndigoState md computation
+
+namedToExpr :: NamedFieldObj x name -> Expr (GetFieldType x name)
+namedToExpr (NamedFieldObj flObj) = objToExpr namedToExpr flObj
+
+-- | Convert arbitrary 'IndigoObjectF' into 'Expr'
+-- with respect to given converter for fields.
 objToExpr
   :: forall a f .
      (forall name . f name -> Expr (GetFieldType a name))
   -> IndigoObjectF f a
   -> Expr a
-objToExpr _ (Cell refId) = V (Cell @a refId)
+objToExpr _ (Cell refId) = V (Var @a refId)
 objToExpr convExpr (Decomposed fields) =
   ConstructWithoutNamed $ namedToTypedRec @a convExpr fields
 
 -- | Compile 'IndigoObjectF' to a stack cell,
--- having a function which compiles inner fields.
+-- with respect to given function that compiles inner fields.
 compileObjectF
   :: forall a inp f .
      (forall name . f name -> Expr (GetFieldType a name))
   -> IndigoObjectF f a
-  -> IndigoState inp (a & inp) ()
-compileObjectF _ (Cell ref) = do
-  md@(MetaData s _) <- iget
-  iput $ GenCode () (pushNoRefMd md) (varActionGet @a ref s) L.drop
+  -> IndigoState inp (a & inp)
+compileObjectF _ (Cell ref) = IndigoState $ \(mdStack -> s) ->
+  GenCode (pushNoRef s) (varActionGet @a ref s) L.drop
 compileObjectF conv obj = compileExpr $ objToExpr conv obj
 
--- | Compile 'ObjectManipulation' datatype to a cell on the stack.
--- This function leverages 'ObjManipulationRes' to put off actual field compilation.
-compileObjectManipulation :: forall a inp . ObjectManipulation a -> IndigoState inp (a & inp) ()
-compileObjectManipulation fa = case runObjectManipulation fa of
-  StillObject composite -> compileObjectF unNamedFieldExpr composite
-  OnStack comp -> comp
-
 -- | 'ObjManipulationRes' represents a postponed compilation of
 -- 'ObjectManipulation' datatype. When 'ObjectManipulation' is being compiled
 -- we are trying to put off the generation of code for work with an object
@@ -182,36 +189,36 @@
 -- onto stack.
 data ObjManipulationRes inp a where
   StillObject :: ObjectExpr a -> ObjManipulationRes inp a
-  OnStack :: IndigoState inp (a & inp) () -> ObjManipulationRes inp a
+  OnStack :: IndigoState inp (a & inp) -> ObjManipulationRes inp a
 
 -- | This function might look cumbersome
--- but it basically either goes deeper to an inner field or generates Lorentz code.
-runObjectManipulation :: ObjectManipulation x -> ObjManipulationRes inp x
-runObjectManipulation (Object e) = exprToManRes e
+-- but basically it either goes deeper to an inner field or generates Lorentz code.
+runObjectManipulation :: DecomposedObjects -> ObjectManipulation x -> ObjManipulationRes inp x
+runObjectManipulation objs (Object e) = exprToManRes objs e
 
-runObjectManipulation (ToField (v :: ObjectManipulation dt) (targetLb :: Label fname)) =
-  case runObjectManipulation v of
+runObjectManipulation objs (ToField (v :: ObjectManipulation dt) (targetLb :: Label fname)) =
+  case runObjectManipulation objs v of
     -- In case of decomposed fields, we just go deeper.
     StillObject (Decomposed fields) ->
       case fieldLens @dt @fname of
         -- If we access direct field, we just fetch it from fields
-        TargetField lb _ -> exprToManRes $ unNamedFieldExpr (fetchField @dt lb fields)
+        TargetField lb _ -> exprToManRes objs $ unNamedFieldExpr (fetchField @dt lb fields)
         -- If we access deeper field, we fetch direct field and goes to the deeper field
         DeeperField lb _ ->
           let fe = unNamedFieldExpr $ fetchField @dt lb fields in
-          runObjectManipulation (ToField (Object fe) targetLb)
+          runObjectManipulation objs (ToField (Object fe) targetLb)
     -- If stored object as cell on the stack, we get its field
     -- using 'sopToField', and since this moment 'ObjManipulationRes becomes
     -- a computation, not object anymore.
     StillObject (Cell refId) ->
-      OnStack $ unaryOp (V $ Cell refId) (sopToField @dt (flSFO fieldLens) targetLb)
+      OnStack $ unaryOp (V $ Var refId) (sopToField @dt (flSFO fieldLens) targetLb)
     -- If we already got into computation, we use 'sopToField' to fetch field.
-    OnStack compLHS -> OnStack $ IndigoState $ \md ->
-      let cd = gcCode $ runIndigoState compLHS md in
-      GenCode () (pushNoRefMd md) (cd # sopToField (flSFO fieldLens) targetLb) L.drop
+    OnStack compLHS -> OnStack $ IndigoState $ \mdI ->
+      let cd = gcCode $ usingIndigoState mdI compLHS in
+      GenCode (pushNoRef $ mdStack mdI) (cd # sopToField (flSFO fieldLens) targetLb) L.drop
 
-runObjectManipulation (SetField (ev :: ObjectManipulation dt) (targetLb :: Label fname) ef) =
-  case runObjectManipulation ev of
+runObjectManipulation objs (SetField (ev :: ObjectManipulation dt) (targetLb :: Label fname) ef) =
+  case runObjectManipulation objs ev of
     StillObject lhsObj@(Decomposed fields) ->
       case fieldLens @dt @fname of
         -- If we set direct field, we just reassign its value with new one.
@@ -223,8 +230,8 @@
         DeeperField (lb :: Label interm) _ ->
           let fe = unNamedFieldExpr (fetchField @dt lb fields) in
           -- Computing new value of direct field
-          case runObjectManipulation (SetField (Object fe) targetLb ef) of
-            -- If it's still object, we just reassign direct field with it.
+          case runObjectManipulation objs (SetField (Object fe) targetLb ef) of
+            -- If it's still an object, we just reassign direct field with it.
             StillObject updField -> StillObject $ Decomposed $
               assignField @dt lb (NamedFieldExpr $ objToExpr unNamedFieldExpr updField) fields
             -- Otherwise, we use power of 'L.setField' to set a new value.
@@ -234,20 +241,20 @@
     -- using 'sopSetField', and since this moment 'ObjManipulationRes' becomes
     -- a computation, not object anymore.
     StillObject (Cell refId) ->
-      OnStack $ binaryOp ef (V $ Cell refId) $ sopSetField (flSFO fieldLens) targetLb
+      OnStack $ binaryOp ef (V $ Var refId) $ sopSetField (flSFO fieldLens) targetLb
     -- If we already got into computation, we use 'sopSetField' to set a field.
     OnStack compLHS ->
       setFieldOnStack compLHS (compileExpr ef) (sopSetField (flSFO $ fieldLens @dt) targetLb)
   where
     setFieldOnStack
-      :: IndigoState inp (dt & inp) ()
-      -> IndigoState (dt & inp) (fld & dt & inp) ()
+      :: IndigoState inp (dt & inp)
+      -> IndigoState (dt & inp) (fld & dt & inp)
       -> fld & dt & inp :-> dt & inp
       -> ObjManipulationRes inp dt
-    setFieldOnStack lhs rhs setOp = OnStack $ IndigoState $ \md ->
-      let GenCode _ md1 cdObj _cl1 = runIndigoState lhs md in
-      let GenCode _ _md2 cdFld _cl2 = runIndigoState rhs md1 in
-      GenCode () (pushNoRefMd md) (cdObj # cdFld # setOp) L.drop
+    setFieldOnStack lhs rhs setOp = OnStack $ IndigoState $ \mdI ->
+      let GenCode st1 cdObj _cl1 = runIndigoState lhs mdI in
+      let GenCode _st2 cdFld _cl2 = runIndigoState rhs (replStkMd mdI st1) in
+      GenCode (pushNoRef $ mdStack mdI) (cdObj # cdFld # setOp) L.drop
 
 -- | Convert an expression to 'ObjManipulationRes'.
 -- The function pattern matches on some specific cases
@@ -256,79 +263,85 @@
 --
 -- This function can't be called for 'ObjMan' constructor, but we
 -- take care of it just in case.
-exprToManRes :: forall x inp . Expr x -> ObjManipulationRes inp x
-exprToManRes (ObjMan objMan) = runObjectManipulation objMan
-exprToManRes (ConstructWithoutNamed fields) =
+exprToManRes :: forall x inp . DecomposedObjects -> Expr x -> ObjManipulationRes inp x
+exprToManRes objs (ObjMan objMan) = runObjectManipulation objs objMan
+exprToManRes _ (ConstructWithoutNamed fields) =
   StillObject $ Decomposed $ typedToNamedRec @x NamedFieldExpr fields
-exprToManRes (V (Decomposed fields)) =
-  StillObject $ Decomposed $ rmap (\(NamedFieldVar f) -> NamedFieldExpr $ V f) fields
-exprToManRes (V (Cell refId)) = StillObject $ Cell refId
-exprToManRes ex = OnStack $ compileExpr ex
+exprToManRes objs (V var) = withObject objs var $ \case
+  Cell refId ->
+    StillObject $ Cell refId
+  Decomposed fields ->
+    StillObject $ Decomposed $ rmap (NamedFieldExpr . namedToExpr) fields
+exprToManRes _ ex = OnStack $ compileExpr ex
 
+---------------------------------------------------
+-- Convenient helpers for operators compilation
+---------------------------------------------------
+
 ternaryOp
   :: KnownValue res
   => Expr n
   -> Expr m
   -> Expr l
   -> n & m & l & inp :-> res & inp
-  -> IndigoState inp (res & inp) ()
+  -> IndigoState inp (res & inp)
 ternaryOp e1 e2 e3 opCode = IndigoState $ \md ->
-  let GenCode _ md3 cd3 _cl3  = runIndigoState (compileExpr e3) md in
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileExpr e2) md3 in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileExpr e1) md2 in
-  GenCode () (pushNoRefMd md) (cd3 # cd2 # cd1 # opCode) L.drop
+  let GenCode st3 cd3 _cl3  = runIndigoState (compileExpr e3) md in
+  let GenCode st2 cd2 _cl2  = runIndigoState (compileExpr e2) (replStkMd md st3) in
+  let GenCode _st1 cd1 _cl1 = runIndigoState (compileExpr e1) (replStkMd md st2) in
+  GenCode (pushNoRef $ mdStack md) (cd3 # cd2 # cd1 # opCode) L.drop
 
 binaryOp
   :: KnownValue res
   => Expr n -> Expr m
   -> n & m & inp :-> res & inp
-  -> IndigoState inp (res & inp) ()
+  -> IndigoState inp (res & inp)
 binaryOp e1 e2 opCode = IndigoState $ \md ->
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileExpr e2) md in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileExpr e1) md2 in
-  GenCode () (pushNoRefMd md) (cd2 # cd1 # opCode) L.drop
+  let GenCode st2 cd2 _cl2  = runIndigoState (compileExpr e2) md in
+  let GenCode _st1 cd1 _cl1 = runIndigoState (compileExpr e1) (replStkMd md st2) in
+  GenCode (pushNoRef $ mdStack md) (cd2 # cd1 # opCode) L.drop
 
 unaryOp
   :: KnownValue res
   => Expr n
   -> n & inp :-> res & inp
-  -> IndigoState inp (res & inp) ()
+  -> IndigoState inp (res & inp)
 unaryOp e opCode = IndigoState $ \md ->
   let cd = gcCode $ runIndigoState (compileExpr e) md in
-  GenCode () (pushNoRefMd md) (cd # opCode) L.drop
+  GenCode (pushNoRef $ mdStack md) (cd # opCode) L.drop
 
-nullaryOp :: KnownValue res => inp :-> res ': inp -> IndigoState inp (res ': inp) ()
+nullaryOp :: KnownValue res => inp :-> res ': inp -> IndigoState inp (res ': inp)
 nullaryOp lorentzInstr = IndigoState $ \md ->
-  GenCode () (pushNoRefMd md) lorentzInstr L.drop
+  GenCode (pushNoRef $ mdStack md) lorentzInstr L.drop
 
 ternaryOpFlat
   :: Expr n
   -> Expr m
   -> Expr l
   -> n & m & l & inp :-> inp
-  -> IndigoState inp inp ()
+  -> IndigoState inp inp
 ternaryOpFlat e1 e2 e3 opCode = IndigoState $ \md ->
-  let GenCode _ md3 cd3 _cl3  = runIndigoState (compileExpr e3) md in
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileExpr e2) md3 in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileExpr e1) md2 in
-  GenCode () md (cd3 # cd2 # cd1 # opCode) L.nop
+  let GenCode st3 cd3 _cl3  = runIndigoState (compileExpr e3) md in
+  let GenCode st2 cd2 _cl2  = runIndigoState (compileExpr e2) (replStkMd md st3) in
+  let GenCode _st1 cd1 _cl1 = runIndigoState (compileExpr e1) (replStkMd md st2) in
+  GenCode (mdStack md) (cd3 # cd2 # cd1 # opCode) L.nop
 
 binaryOpFlat
   :: Expr n -> Expr m
   -> n & m & inp :-> inp
-  -> IndigoState inp inp ()
+  -> IndigoState inp inp
 binaryOpFlat e1 e2 opCode = IndigoState $ \md ->
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileExpr e2) md in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileExpr e1) md2 in
-  GenCode () md (cd2 # cd1 # opCode) L.nop
+  let GenCode st2 cd2 _cl2  = runIndigoState (compileExpr e2) md in
+  let GenCode _st1 cd1 _cl1 = runIndigoState (compileExpr e1) (replStkMd md st2) in
+  GenCode (mdStack md) (cd2 # cd1 # opCode) L.nop
 
 unaryOpFlat
   :: Expr n
   -> n & inp :-> inp
-  -> IndigoState inp inp ()
+  -> IndigoState inp inp
 unaryOpFlat e opCode = IndigoState $ \md ->
   let cd = gcCode $ runIndigoState (compileExpr e) md in
-  GenCode () md (cd # opCode) L.nop
+  GenCode (mdStack md) (cd # opCode) L.nop
 
-nullaryOpFlat :: inp :-> inp -> IndigoState inp inp ()
-nullaryOpFlat lorentzInstr = IndigoState $ \md -> GenCode () md lorentzInstr L.nop
+nullaryOpFlat :: inp :-> inp -> IndigoState inp inp
+nullaryOpFlat lorentzInstr = IndigoState $ \md -> GenCode (mdStack md) lorentzInstr L.nop
diff --git a/src/Indigo/Internal/Expr/Decompose.hs b/src/Indigo/Internal/Expr/Decompose.hs
--- a/src/Indigo/Internal/Expr/Decompose.hs
+++ b/src/Indigo/Internal/Expr/Decompose.hs
@@ -14,71 +14,96 @@
   , IsObject
   ) where
 
+import Prelude
 import Data.Constraint (Dict(..))
 import Data.Vinyl.TypeLevel
-import Prelude (fst)
 
 import Indigo.Internal.Expr.Compilation
 import Indigo.Internal.Expr.Types
 import Indigo.Internal.Lookup
 import Indigo.Internal.Object
 import Indigo.Internal.SIS
+import Indigo.Internal.Var
 import Indigo.Internal.State
 import Indigo.Lorentz
-import Indigo.Prelude
 import qualified Lorentz.ADT as L
 import qualified Lorentz.Instr as L
 import Michelson.Typed.Haskell.Instr.Product (GetFieldType)
 import Util.Type
 
--- | Datatype representing decomposition of 'Expr'.
-data ExprDecomposition inp a where
-  ExprFields :: Rec Expr (FieldTypes a) -> ExprDecomposition inp a
-  Deconstructed :: IndigoState inp (FieldTypes a ++ inp) () -> ExprDecomposition inp a
+-----------------------------------------
+-- Object decomposition
+-----------------------------------------
 
--- | Decompose an expression to list of its direct fields.
-decomposeExpr :: ComplexObjectC a => Expr a -> ExprDecomposition inp a
-decomposeExpr (ConstructWithoutNamed fields) = ExprFields fields
-decomposeExpr (V v) = decomposeObjectF (\(NamedFieldVar vr) -> V vr) v
-decomposeExpr (ObjMan objMan) = case runObjectManipulation objMan of
-  StillObject obj -> decomposeObjectF unNamedFieldExpr obj
-  OnStack comp -> deconstructOnStack comp
-decomposeExpr ex = deconstructOnStack $ compileExpr ex
+-- | Alike 'SomeIndigoState' datatype but without objects argument
+type SIS' stk a = RefId -> StackVars stk -> (a, RefId, SomeGenCode stk)
 
 -- | For given element on stack, generate code which
 -- decomposes it to list of its deep non-decomposable fields.
 -- Clean up code of 'SomeIndigoState' composes the value back.
 deepDecomposeCompose
   :: forall a inp . IsObject a
-  => SomeIndigoState (a & inp) (Var a)
+  => SIS' (a & inp) (Object a)
 deepDecomposeCompose
-  | Just Dict <- complexObjectDict @a = SomeIndigoState $ \md ->
-      let decomposedMd = fst (noRefGenCode @(FieldTypes a) $ popNoRefMd md) in
-      runSIS (decomposeComposeFields @(FieldTypes a)) decomposedMd $ \gc ->
-        SomeGenCode $ GenCode
-          { gcOut = Decomposed (typedToNamedRec @a typedToNamedFieldVar (gcOut gc))
-          , gcMeta = gcMeta gc
+  | Just Dict <- complexObjectDict @a = \refId st ->
+      let decomposedSt = fst (noRefGenCode @(FieldTypes a) $ popNoRef st) in
+      withStack refId decomposedSt (decomposeComposeFields @(FieldTypes a)) $ \(result, newRefId, gc) ->
+        ( Decomposed (typedToNamedRec @a typedToNamedFieldObj result)
+        , newRefId
+        , SomeGenCode $ GenCode
+          { gcStack = gcStack gc
           , gcCode = L.deconstruct @a @(FieldTypes a) # gcCode gc
           , gcClear = gcClear gc # L.constructStack @a  @(FieldTypes a)
           }
-  | otherwise = SomeIndigoState $ SomeGenCode . runIndigoState makeTopVar
+        )
+  | otherwise =
+      \refId stk -> (Cell refId, refId + 1, SomeGenCode $ runIndigoState (assignTopVar $ Var refId) (MetaData stk mempty))
   where
     decomposeComposeFields
       :: forall flds . (KnownList flds, AllConstrained IsObject flds)
-      => SomeIndigoState (flds ++ inp) (Rec TypedFieldVar flds)
+      => SIS' (flds ++ inp) (Rec TypedFieldObj flds)
     decomposeComposeFields = case klist @flds of
-      KNil -> returnSIS RNil
-      KCons (_ :: Proxy r) (_ :: Proxy rest) -> SomeIndigoState $ \md ->
-        runSIS (decomposeComposeFields @rest) (popNoRefMd md) $ \restGc ->
-          runSIS (deepDecomposeCompose @r) (pushNoRefMd $ gcMeta restGc) $ \curGc ->
-            SomeGenCode $ GenCode
-              { gcOut = TypedFieldVar (gcOut curGc) :& gcOut restGc
-              , gcMeta = gcMeta curGc
+      KNil -> \refId stk -> (RNil, refId, SomeGenCode $ GenCode stk L.nop L.nop)
+      KCons (_ :: Proxy r) (_ :: Proxy rest) -> \refId st ->
+        withStack refId (popNoRef st) (decomposeComposeFields @rest) $ \(resultRest, refId', restGc) ->
+          withStack refId' (pushNoRef $ gcStack restGc) (deepDecomposeCompose @r) $ \(resultCur, newRefId, curGc) ->
+            ( TypedFieldObj resultCur :& resultRest
+            , newRefId
+            , SomeGenCode $ GenCode
+              { gcStack = gcStack curGc
               , gcCode = L.dip (gcCode restGc) # gcCode curGc
               , gcClear = gcClear curGc # L.dip (gcClear restGc)
               }
+            )
 
--- | Decompose any 'IndigoObjectF' having decomposer for field.
+withStack
+  :: RefId
+  -> StackVars inp
+  -> SIS' inp a
+  -> (forall out . (a, RefId, GenCode inp out) -> r)
+  -> r
+withStack refId stk sis f = case sis refId stk of
+  (res, newRefId, SomeGenCode genCode) -> f (res, newRefId, genCode)
+
+-----------------------------------------
+-- Expr decomposition
+-----------------------------------------
+
+-- | Datatype representing decomposition of 'Expr'.
+data ExprDecomposition inp a where
+  ExprFields :: Rec Expr (FieldTypes a) -> ExprDecomposition inp a
+  Deconstructed :: IndigoState inp (FieldTypes a ++ inp) -> ExprDecomposition inp a
+
+-- | Decompose (shallowly) an expression to list of its direct fields.
+decomposeExpr :: ComplexObjectC a => DecomposedObjects -> Expr a -> ExprDecomposition inp a
+decomposeExpr _ (ConstructWithoutNamed fields) = ExprFields fields
+decomposeExpr objs (V v) = withObject objs v $ decomposeObjectF namedToExpr
+decomposeExpr objs (ObjMan objMan) = case runObjectManipulation objs objMan of
+  StillObject obj -> decomposeObjectF unNamedFieldExpr obj
+  OnStack comp -> deconstructOnStack comp
+decomposeExpr _ ex = deconstructOnStack $ compileExpr ex
+
+-- | Decompose any 'IndigoObjectF' with regards to decomposer for field.
 decomposeObjectF
   :: forall a inp f . ComplexObjectC a
   => (forall name . f name -> Expr (GetFieldType a name))
@@ -86,7 +111,7 @@
   -> ExprDecomposition inp a
 decomposeObjectF _ (Cell refId) =
   deconstructOnStack $
-    IndigoState $ \md -> GenCode () (pushNoRefMd md) (varActionGet @a refId (mdStack md)) L.drop
+    IndigoState $ \md -> GenCode (pushNoRef $ mdStack md) (varActionGet @a refId $ mdStack md) L.drop
 decomposeObjectF unF (Decomposed fields) =
   ExprFields $ namedToTypedRec @a unF fields
 
@@ -94,17 +119,21 @@
 -- wrapped into 'Deconstructed' constructor.
 deconstructOnStack
   :: forall a inp . ComplexObjectC a
-  => IndigoState inp (a & inp) ()
+  => IndigoState inp (a & inp)
   -> ExprDecomposition inp a
 deconstructOnStack fetchFld =
   Deconstructed $ IndigoState $ \md ->
-    let (newMd, clean) = noRefGenCode @(FieldTypes a) md in
-    GenCode () newMd (gcCode (runIndigoState fetchFld md) # L.deconstruct @a @(FieldTypes a)) clean
+    let (newSt, clean) = noRefGenCode @(FieldTypes a) (mdStack md) in
+    GenCode newSt (gcCode (runIndigoState fetchFld md) # L.deconstruct @a @(FieldTypes a)) clean
 
+-----------------------------------------
+-- Helpers
+-----------------------------------------
+
 -- | Push the passed stack cells without references to them.
 noRefGenCode
   :: forall rs inp . (KnownList rs, AllConstrained KnownValue rs)
-  => MetaData inp -> (MetaData (rs ++ inp), (rs ++ inp) :-> inp)
+  => StackVars inp -> (StackVars (rs ++ inp), (rs ++ inp) :-> inp)
 noRefGenCode md = case klist @rs of
   KNil -> (md, L.nop)
-  KCons Proxy (_ :: Proxy rest) -> bimap pushNoRefMd (L.drop #) (noRefGenCode @rest md)
+  KCons Proxy (_ :: Proxy rest) -> bimap pushNoRef (L.drop #) (noRefGenCode @rest md)
diff --git a/src/Indigo/Internal/Expr/Symbolic.hs b/src/Indigo/Internal/Expr/Symbolic.hs
--- a/src/Indigo/Internal/Expr/Symbolic.hs
+++ b/src/Indigo/Internal/Expr/Symbolic.hs
@@ -109,7 +109,7 @@
 
 import Indigo.Internal.Expr.Types
 import Indigo.Internal.Field
-import Indigo.Internal.Object (Var)
+import Indigo.Internal.Var (Var)
 import Indigo.Lorentz hiding (forcedCoerce)
 import Indigo.Prelude
 import qualified Michelson.Typed.Arith as M
diff --git a/src/Indigo/Internal/Expr/Types.hs b/src/Indigo/Internal/Expr/Types.hs
--- a/src/Indigo/Internal/Expr/Types.hs
+++ b/src/Indigo/Internal/Expr/Types.hs
@@ -41,7 +41,8 @@
 import Indigo.Prelude (Either (..), id)
 import Indigo.Lorentz
 import Indigo.Internal.Field
-import Indigo.Internal.Object (Var, IndigoObjectF (..), FieldTypes, ComplexObjectC)
+import Indigo.Internal.Object (IndigoObjectF (..), FieldTypes, ComplexObjectC)
+import Indigo.Internal.Var (Var (..))
 import qualified Michelson.Typed.Arith as M
 import Michelson.Typed.Haskell.Instr.Product (GetFieldType)
 import Michelson.Typed.Haskell.Instr.Sum (CtorOnlyField, InstrUnwrapC, InstrWrapOneC)
diff --git a/src/Indigo/Internal/Lookup.hs b/src/Indigo/Internal/Lookup.hs
--- a/src/Indigo/Internal/Lookup.hs
+++ b/src/Indigo/Internal/Lookup.hs
@@ -25,13 +25,13 @@
 import Data.Constraint (Dict(..), HasDict)
 import Data.Singletons (Sing, SingI(..))
 import Data.Type.Equality (TestEquality(..))
-import Data.Typeable ((:~:)(..), eqT)
+import Data.Typeable ((:~:)(..), eqT, typeRep)
 import Data.Vinyl ((<+>))
 import Data.Vinyl.TypeLevel (type (++))
 import Prelude hiding (tail)
 
-import Indigo.Internal.Object (HasSideEffects, IndigoObjectF(..), Ops, operationsVar)
-import Indigo.Internal.State (RefId, StackVars, StkEl(..))
+import Indigo.Internal.Var
+  (HasSideEffects, Ops, RefId, StackVars, StkEl(..), Var(..), operationsVar)
 import Indigo.Lorentz
 import qualified Lorentz.Instr as L
 import qualified Lorentz.Macro as L
@@ -73,7 +73,7 @@
   -> (Operation ': stk) :-> stk
 varActionOperation s =
   case operationsVar of
-    Cell refId -> varActionUpdate @Ops refId s L.cons
+    Var refId -> varActionUpdate @Ops refId s L.cons
 
 ----------------------------------------------------------------------------
 -- Variable-based Macros
@@ -157,7 +157,9 @@
   -> StackVars s
   -> VarDepth
 varDepth refId = \case
-  RNil -> error $ "Manually created or leaked variable. Ref #" <> show refId
+  RNil -> error $
+    "You are looking for manually created or leaked variable. " <>
+    "Ref #" <> show refId <> " of type " <> show (typeRep (Proxy @a))
   stk@(_ :& _) -> varDepthNonEmpty @a refId stk
 
 varDepthNonEmpty
@@ -166,7 +168,10 @@
 varDepthNonEmpty ref (x :& xs) = case x of
   Ref topRef | ref == topRef -> case eqT @a @x of
     Just Refl -> VarDepth SZ
-    Nothing   -> error $ "Invalid variable type. Ref #" <> show ref
+    Nothing   -> error $
+      "Invalid variable type. Ref #" <> show ref <>
+      ".\nWas looking for a " <> show (typeRep $ Proxy @a) <>
+      ", but found a: " <> show (typeRep $ Proxy @x)
   _ -> case varDepth @a ref xs of
     VarDepth idx -> VarDepth (SS idx)
 
diff --git a/src/Indigo/Internal/Object.hs b/src/Indigo/Internal/Object.hs
--- a/src/Indigo/Internal/Object.hs
+++ b/src/Indigo/Internal/Object.hs
@@ -4,55 +4,38 @@
 
 module Indigo.Internal.Object
   ( IndigoObjectF (..)
-  , NamedFieldVar (..)
-  , TypedFieldVar (..)
+  , NamedFieldObj (..)
+  , TypedFieldObj (..)
   , FieldTypes
-  , Var
+  , Object
+  , SomeObject (..)
   , namedToTypedRec
   , typedToNamedRec
-  , namedToTypedFieldVar
-  , typedToNamedFieldVar
+  , namedToTypedFieldObj
+  , typedToNamedFieldObj
 
   , IsObject
   , complexObjectDict
   , ComplexObjectC
   , castFieldConstructors
-
-  -- * Stack operations
-  , withVarAt
-  , makeTopVar
-  , pushRefMd
-  , pushNoRefMd
-  , popNoRefMd
-
-  -- * Operations/Storage variables
-  , Ops
-  , HasSideEffects
-  , operationsVar
-  , HasStorage
-  , storageVar
   ) where
 
 import Data.Vinyl (RMap)
 import Data.Vinyl.TypeLevel (AllConstrained)
-import Data.Reflection (Given (..))
 import Data.Constraint (Dict(..))
-import Data.Singletons (Sing)
 import qualified GHC.Generics as G
 
+import Indigo.Internal.Var (RefId)
 import Indigo.Backend.Prelude
 import Indigo.Lorentz
-import Indigo.Internal.State
 import Michelson.Typed.Haskell.Instr.Product
   ( GetFieldType, ConstructorFieldNames, GetFieldType
   , InstrDeconstructC, FieldConstructor (..), CastFieldConstructors (..))
 import Michelson.Typed (IsPrimitiveValue)
-import qualified Lorentz.Instr as L
-import Util.Peano
 import Util.Type (KnownList (..), KList (..))
 
 ----------------------------------------------------------------------------
--- IndigoObjectF and Variable
+-- IndigoObjectF
 ----------------------------------------------------------------------------
 
 -- | A object that can be either
@@ -64,11 +47,7 @@
   -- | Value stored on the stack, it might be
   -- either complex product type, like @(a, b)@, Storage, etc,
   -- or sum type like 'Either', or primitive like 'Int', 'Operation', etc.
-  --
-  -- Laziness of 'RefId' is needed here to make possible to put
-  -- 'error' in a variable.
-  -- This is used as a workaround in "Indigo.Compilation.Lambda".
-  Cell :: KnownValue a => ~RefId -> IndigoObjectF f a
+  Cell :: KnownValue a => RefId -> IndigoObjectF f a
   -- | Decomposed product type, which is NOT stored
   -- as one cell on the stack.
   Decomposed :: ComplexObjectC a => Rec f (ConstructorFieldNames a) -> IndigoObjectF f a
@@ -108,32 +87,30 @@
   => Rec (FieldConstructor st) (FieldTypes a) -> Rec (FieldConstructor st) (ConstructorFieldTypes a)
 castFieldConstructors = castFieldConstructorsImpl
 
--- | Auxiliary datatype to define a variable.
+-- | Auxiliary datatype to define a Objiable.
 -- Keeps field name as type param
-data NamedFieldVar a name where
-  NamedFieldVar
+data NamedFieldObj a name where
+  NamedFieldObj
     :: IsObject (GetFieldType a name)
-    => { unFieldVar :: Var (GetFieldType a name)
+    => { unFieldObj :: Object (GetFieldType a name)
        }
-    -> NamedFieldVar a name
+    -> NamedFieldObj a name
 
--- | Variable exposed to a user.
---
--- 'Var' represents the tree of fields.
--- Each field is 'Var' itself:
--- either a value on the stack or 'Rec' of its direct fields.
-type Var a = IndigoObjectF (NamedFieldVar a) a
+type Object a = IndigoObjectF (NamedFieldObj a) a
 
--- | Like 'NamedFieldVar', but this one doesn't keep name of a field
-data TypedFieldVar a where
-  TypedFieldVar :: IsObject a => Var a -> TypedFieldVar a
+data SomeObject where
+  SomeObject :: IsObject a => Object a -> SomeObject
 
-namedToTypedFieldVar :: forall a name . NamedFieldVar a name -> TypedFieldVar (GetFieldType a name)
-namedToTypedFieldVar (NamedFieldVar f) = TypedFieldVar f
+-- | Like 'NamedFieldObj', but this one doesn't keep name of a field
+data TypedFieldObj a where
+  TypedFieldObj :: IsObject a => Object a -> TypedFieldObj a
 
-typedToNamedFieldVar :: forall a name . TypedFieldVar (GetFieldType a name) -> NamedFieldVar a name
-typedToNamedFieldVar (TypedFieldVar f) = NamedFieldVar f
+namedToTypedFieldObj :: forall a name . NamedFieldObj a name -> TypedFieldObj (GetFieldType a name)
+namedToTypedFieldObj (NamedFieldObj f) = TypedFieldObj f
 
+typedToNamedFieldObj :: forall a name . TypedFieldObj (GetFieldType a name) -> NamedFieldObj a name
+typedToNamedFieldObj (TypedFieldObj f) = NamedFieldObj f
+
 ----------------------------------------------------------------------------
 -- IsObject type class
 ----------------------------------------------------------------------------
@@ -203,69 +180,3 @@
   IsSumType G.V1 = 'False
   IsSumType G.U1 = 'False
   IsSumType (_ G.:+: _) = 'True
-
-----------------------------------------------------------------------------
--- Stack operations
-----------------------------------------------------------------------------
-
--- | Given a 'MetaData' and a @Peano@ singleton for a depth, it puts a new 'Var'
--- at that depth (0-indexed) and returns it with the updated 'MetaData'.
---
--- If there is a 'Var' there already it is used and the 'MetaData' not changed.
-withVarAt
-  :: (KnownValue a, a ~ At n inp, RequireLongerThan inp n)
-  => MetaData inp
-  -> Sing n
-  -> (MetaData inp, Var a)
-withVarAt md@(MetaData (top :& xs) ref) = \case
-  SS n -> first (appendToStack top) $ withVarAt (MetaData xs ref) n
-  SZ -> case top of
-    Ref matRef -> (md, Cell matRef)
-    NoRef -> (MetaData (Ref ref :& xs) (ref + 1), Cell ref)
-  where
-    appendToStack :: StkEl x -> MetaData inp -> MetaData (x ': inp)
-    appendToStack v (MetaData st r) = MetaData (v :& st) r
-
--- | Create a variable referencing the element on top of the stack.
-makeTopVar :: KnownValue x => IndigoState (x & inp) (x & inp) (Var x)
-makeTopVar = iget >>= \md ->
-  let (newMd, var) = withVarAt md SZ
-  in iput $ GenCode var newMd L.nop L.nop
-
--- | Push a new stack element with a reference to it.
--- Return the variable referencing this element.
-pushRefMd :: KnownValue x => MetaData stk -> (Var x, MetaData (x & stk))
-pushRefMd (MetaData stk cnt) = (Cell cnt, MetaData (Ref cnt :& stk) (cnt + 1))
-
--- | Push a new stack element without a reference to it.
-pushNoRefMd :: KnownValue a => MetaData inp -> MetaData (a & inp)
-pushNoRefMd (MetaData xs ref) = MetaData (NoRef :& xs) ref
-
--- | Remove the top element of the stack.
--- It's supposed that no variable refers to this element.
-popNoRefMd :: MetaData (a & inp) -> MetaData inp
-popNoRefMd (MetaData (NoRef :& xs) ref) = MetaData xs ref
-popNoRefMd (MetaData (Ref refId :& _) _) =
-  error $ "You try to pop stack element, which is referenced by some variable #" <> show refId
-
-----------------------------------------------------------------------------
--- Operations/Storage variables
-----------------------------------------------------------------------------
-
-type Ops = [Operation]
-
--- | Allows to get a variable with operations
-type HasSideEffects = Given (Var Ops)
-
--- | Return a variable which refers to a stack cell with operations
-operationsVar :: HasSideEffects => Var Ops
-operationsVar = given
-
--- This storage machinery is here to avoid cyclic deps
-
--- | Allows to get a variable with storage
-type HasStorage st = Given (Var st)
-
--- | Return a variable which refers to a stack cell with storage
-storageVar :: HasStorage st => Var st
-storageVar = given
diff --git a/src/Indigo/Internal/SIS.hs b/src/Indigo/Internal/SIS.hs
--- a/src/Indigo/Internal/SIS.hs
+++ b/src/Indigo/Internal/SIS.hs
@@ -5,97 +5,51 @@
 module Indigo.Internal.SIS
   ( SomeIndigoState (..)
   , SomeGenCode (..)
-  , returnSIS
-  , bindSIS
   , toSIS
   , runSIS
-  , withSIS
-  , withSIS1
-  , withSIS2
+  , thenSIS
+  , overSIS
   ) where
 
-
-import Indigo.Lorentz
 import Indigo.Prelude
 
 import Indigo.Internal.State
-import Indigo.Internal.Object
-import qualified Lorentz.Instr as L
-
--- | Gen code with hidden output stack
-data SomeGenCode inp a where
-  SomeGenCode :: GenCode inp out a -> SomeGenCode inp a
+import Indigo.Lorentz
 
-deriving stock instance Functor (SomeGenCode inp)
+-- | 'GenCode' with hidden output stack
+data SomeGenCode inp where
+  SomeGenCode :: GenCode inp out -> SomeGenCode inp
 
 -- | 'IndigoState' with hidden output stack,
 -- necessary to generate typed Lorentz code from untyped Indigo frontend.
-newtype SomeIndigoState inp a = SomeIndigoState {unSIS :: MetaData inp -> SomeGenCode inp a}
-  deriving stock Functor
-
--- | 'return' for 'SomeIndigoState'
-returnSIS :: a -> SomeIndigoState inp a
-returnSIS a = SomeIndigoState $ \md -> SomeGenCode $ GenCode a md L.nop L.nop
-
--- | Like bind, but the input type of the second parameter is determined by the
--- output of the first one.
-bindSIS :: SomeIndigoState inp a -> (forall someOut . a -> SomeIndigoState someOut b) -> SomeIndigoState inp b
-bindSIS m f = SomeIndigoState $ \md ->
-  case unSIS m md of
-    (SomeGenCode (GenCode a md1 cd1 cl1 :: GenCode inp out a)) ->
-      case unSIS (f @out a) md1 of
-        SomeGenCode (GenCode b md2 cd2 cl2) -> SomeGenCode (GenCode b md2 (cd1 ## cd2) (cl2 ## cl1))
+newtype SomeIndigoState inp = SomeIndigoState
+  { unSIS :: MetaData inp -> SomeGenCode inp
+  }
 
--- | To run 'SomeIndigoState' you need to pass an handler of 'GenCode' with any output stack.
-runSIS :: SomeIndigoState inp a -> MetaData inp -> (forall out . GenCode inp out a -> r) -> r
-runSIS (SomeIndigoState act) md f =
-  case act md of
-    SomeGenCode gc -> f gc
+-- | To run 'SomeIndigoState' you need to pass an handler of 'GenCode' with any
+-- output stack and initial 'MetaData'.
+runSIS :: SomeIndigoState inp -> MetaData inp -> (forall out . GenCode inp out -> r) -> r
+runSIS (SomeIndigoState act) md f = case act md of
+  SomeGenCode gc -> f gc
 
 -- | Convert 'IndigoState' to 'SomeIndigoState'
-toSIS :: IndigoState inp out a -> SomeIndigoState inp a
-toSIS is = SomeIndigoState $ SomeGenCode <$> runIndigoState is
-
--- | Call an action with 'IndigoState' stored in 'SomeIndigoState'.
---
--- This function is kinda dummy because it passes
--- IndigoState to the function which produces a GenCode independently
--- on passed MetaData to it. It has to be used with only functions
--- which pass MetaData in the same way.
--- This function is needed to pass SomeIndigoState in contravariant positions
--- of statements like @if@, @case@, @while@, @forEach@, etc.
--- Alternative solution would be abstracting out IndigoState and SomeIndigoState
--- with typeclass
--- class CodeGenerator m where
---   runCodeGen :: m inp a -> MetaData inp -> (forall out . GenCode inp out a -> r) -> r
--- and passing CodeGenerator m in contravariant positions instead of IndigoState.
-withSIS
-  :: SomeIndigoState inp a
-  -> (forall out . IndigoState inp out a -> SomeIndigoState inp b)
-  -> SomeIndigoState inp b
-withSIS (SomeIndigoState act) f = SomeIndigoState $ \md ->
-  case act md of
-    SomeGenCode gc -> unSIS (f (IndigoState $ \_ -> gc)) md
+toSIS :: IndigoState inp out -> SomeIndigoState inp
+toSIS is = SomeIndigoState $ \md -> SomeGenCode $ runIndigoState is md
 
--- | The same as 'withSIS' but converting a function with one argument, also dummy.
-withSIS1
-  :: KnownValue x
-  => (Var x -> SomeIndigoState (x & inp) a)
-  -> (forall out . (Var x -> IndigoState (x & inp) out a) -> SomeIndigoState inp b)
-  -> SomeIndigoState inp b
-withSIS1 act f = SomeIndigoState $ \md ->
-  let (var, newMd) = pushRefMd md in
-  case unSIS (act var) newMd of
-    SomeGenCode gc -> unSIS (f (\_v -> IndigoState $ \_md -> gc)) md
+-- | Similar to a @>>@ for 'SomeIndigoState'.
+thenSIS :: SomeIndigoState inp -> (forall out . SomeIndigoState out) -> SomeIndigoState inp
+thenSIS m f = SomeIndigoState $ \md ->
+  case unSIS m md of
+    (SomeGenCode (GenCode st1 cd1 cl1 :: GenCode inp out)) ->
+      case unSIS (f @out) (replStkMd md st1) of
+        SomeGenCode (GenCode st2 cd2 cl2) ->
+          SomeGenCode (GenCode st2 (cd1 ## cd2) (cl2 ## cl1))
 
--- | The same as 'withSIS1' but converting a function with 2 arguments, also dummy.
-withSIS2
-  :: (KnownValue x, KnownValue y)
-  => (Var x -> Var y -> SomeIndigoState (x & y & inp) a)
-  -> (forall out . (Var x -> Var y -> IndigoState (x & y & inp) out a) -> SomeIndigoState inp b)
-  -> SomeIndigoState inp b
-withSIS2 act f = SomeIndigoState $ \md ->
-   let (var1, newMd1) = pushRefMd md in
-   let (var2, newMd2) = pushRefMd newMd1 in
-  case unSIS (act var2 var1) newMd2 of
-    SomeGenCode gc -> unSIS (f (\_v _w -> IndigoState $ \_md -> gc)) md
+-- | Modify the 'GenCode' inside a 'SomeIndigoState' by passing an handler of
+-- 'GenCode' that returns a 'SomeGenCode'.
+-- Useful in some cases to "wrap" or update and exising 'SomeGenCode'.
+overSIS
+  :: (forall out. GenCode inp out -> SomeGenCode inp)
+  -> SomeIndigoState inp
+  -> SomeIndigoState inp
+overSIS f si = SomeIndigoState $ \md -> runSIS si md f
diff --git a/src/Indigo/Internal/State.hs b/src/Indigo/Internal/State.hs
--- a/src/Indigo/Internal/State.hs
+++ b/src/Indigo/Internal/State.hs
@@ -6,154 +6,164 @@
 
 {- |
 This module contains the core of Indigo language:
-the 'IndigoState' monad, a datatype that represents its state.
-It also includes some convenient functions to work with the state in IndigoM,
+'IndigoState', a datatype that represents its state.
+It also includes some convenient functions to work with it,
 to provide rebindable syntax.
 
-The 'IndigoState' monad implements the functionality of a symbolic interpreter.
+'IndigoState' implements the functionality of a symbolic interpreter.
 During its execution Lorentz code is being generated.
+
+Functionally, it's the same as having Lorentz instruction that can access and
+modify a 'StackVars', referring to values on the stack with a 'RefId'.
 -}
 
 module Indigo.Internal.State
   ( -- * Indigo State
     IndigoState (..)
   , usingIndigoState
-  , (>>=)
-  , (=<<)
   , (>>)
   , (<$>)
-  , return
-  , iget
   , iput
+  , nopState
+  , assignTopVar
+  , withObject
+  , withObjectState
+  , withStackVars
 
-  , RefId
-  , StkEl (..)
-  , StackVars
-  , GenCode (..)
+  , DecomposedObjects
   , MetaData (..)
-  , emptyMetadata
+  , replStkMd
+  , alterStkMd
+  , pushRefMd
+  , pushNoRefMd
+  , popNoRefMd
+
+  , GenCode (..)
   , cleanGenCode
-  , DefaultStack
   ) where
 
-import qualified Data.Kind as Kind
-import Data.Type.Equality (TestEquality(..))
-import Data.Typeable (eqT)
+import qualified Data.Map as M
+import Data.Typeable ((:~:)(..), eqT)
 
+import Indigo.Internal.Object
+import Indigo.Internal.Var
 import Indigo.Backend.Prelude
 import Indigo.Lorentz
 import qualified Lorentz.Instr as L
-
-{-# ANN module ("HLint: ignore Reduce duplication" :: Text) #-}
+import Util.Peano
 
 ----------------------------------------------------------------------------
 -- Indigo State
 ----------------------------------------------------------------------------
 
--- | IndigoState monad. It's basically
--- [Control.Monad.Indexed.State](https://hackage.haskell.org/package/category-extras-0.53.5/docs/Control-Monad-Indexed-State.html)
--- , however this package is not in the used lts and it doesn't compile.
+-- | IndigoState data type.
 --
--- It takes as input a 'MetaData' (for the initial state) and returns a
+-- It takes as input a 'StackVars' (for the initial state) and returns a
 -- 'GenCode' (for the resulting state and the generated Lorentz code).
 --
 -- IndigoState has to be used to write backend typed Lorentz code
 -- from the corresponding frontend constructions.
-newtype IndigoState inp out a =
-  IndigoState {runIndigoState :: MetaData inp -> GenCode inp out a}
-  deriving stock Functor
-
-usingIndigoState :: MetaData inp -> IndigoState inp out a -> GenCode inp out a
-usingIndigoState = flip runIndigoState
-
--- | Return for rebindable syntax.
-return :: a -> IndigoState inp inp a
-return a = IndigoState $ \md -> GenCode a md L.nop L.nop
-
--- | Bind for rebindable syntax.
 --
--- It's basically like the bind for the 'State' monad, but it also composes the
--- generated code from @m a@ and @a -> m b@.
-(>>=) :: forall inp out out1 a b . IndigoState inp out a -> (a -> IndigoState out out1 b) -> IndigoState inp out1 b
-(>>=) m f = IndigoState $ \md ->
-  let GenCode a md1 cd1 cl1 = runIndigoState m md in
-  let GenCode b md2 cd2 cl2 = runIndigoState (f a) md1 in
-  GenCode b md2 (cd1 ## cd2) (cl2 ## cl1)
+-- It has no return type, IndigoState instruction may take one or more
+-- "return variables", that they assign to values produced during their execution.
+newtype IndigoState inp out = IndigoState {
+    runIndigoState :: MetaData inp -> GenCode inp out
+  }
 
-(=<<) :: (a -> IndigoState out out1 b) -> IndigoState inp out a -> IndigoState inp out1 b
-(=<<) = flip (>>=)
+-- | Inverse of 'runIndigoState' for utility.
+usingIndigoState :: MetaData inp -> IndigoState inp out -> GenCode inp out
+usingIndigoState md act = runIndigoState act md
 
 -- | Then for rebindable syntax.
-(>>) :: IndigoState inp out a -> IndigoState out out1 b -> IndigoState inp out1 b
-(>>) a b = a >>= const b
-
--- | Get current 'MetaData'.
-iget :: IndigoState inp inp (MetaData inp)
-iget = IndigoState $ \md -> GenCode md md L.nop L.nop
+(>>) :: IndigoState inp out -> IndigoState out out1 -> IndigoState inp out1
+(>>) a b = IndigoState $ \md ->
+  let GenCode st1 cd1 cl1 = runIndigoState a md in
+  let GenCode st2 cd2 cl2 = runIndigoState b (replStkMd md st1) in
+  GenCode st2 (cd1 ## cd2) (cl2 ## cl1)
 
 -- | Put new 'GenCode'.
-iput :: GenCode inp out a -> IndigoState inp out a
+iput :: GenCode inp out -> IndigoState inp out
 iput gc = IndigoState $ \_ -> gc
 
-----------------------------------------------------------------------------
--- Indigo stack and code gen primitives
-----------------------------------------------------------------------------
+-- | The simplest 'IndigoState', it does not modify the stack, nor the produced
+-- code.
+nopState :: IndigoState inp inp
+nopState = IndigoState $ \md -> GenCode (mdStack md) L.nop L.nop
 
--- | Reference id to a stack cell
-newtype RefId = RefId Word
-  deriving stock (Show, Generic)
-  deriving newtype (Eq, Ord, Real, Num)
+-- | Assigns a variable to reference the element on top of the stack.
+assignTopVar :: KnownValue x => Var x -> IndigoState (x & inp) (x & inp)
+assignTopVar var = IndigoState $ \md ->
+  GenCode (assignVarAt var (mdStack md) SZ) L.nop L.nop
 
--- | Stack element of the symbolic interpreter.
---
--- It holds either a reference index that refers to this element
--- or just 'NoRef', indicating that there are no references
--- to this element.
-data StkEl a where
-  NoRef :: KnownValue a => StkEl a
-  Ref :: KnownValue a => RefId -> StkEl a
+withObject
+  :: forall a r .  KnownValue a
+  => DecomposedObjects
+  -> Var a
+  -> (Object a -> r)
+  -> r
+withObject objs (Var refId) f = case M.lookup refId objs of
+  Nothing -> f (Cell refId)
+  Just so -> case so of
+    SomeObject (obj :: Object a1) -> case eqT @a @a1 of
+      Just Refl -> f obj
+      Nothing ->
+        error $ "unexpectedly SomeObject with by reference #" <> show refId <> " has different type"
 
-instance TestEquality StkEl where
-  testEquality NoRef NoRef = eqT
-  testEquality (Ref _) (Ref _) = eqT
-  testEquality (Ref _) NoRef = eqT
-  testEquality NoRef (Ref _) = eqT
+withObjectState
+  :: forall a inp out . KnownValue a
+  => Var a
+  -> (Object a -> IndigoState inp out)
+  -> IndigoState inp out
+withObjectState v f = IndigoState $ \md -> usingIndigoState md (withObject (mdObjects md) v f)
 
--- | Stack of the symbolic interpreter.
-type StackVars (stk :: [Kind.Type]) = Rec StkEl stk
+-- | Utility function to create 'IndigoState' that need access to the current 'StackVars'.
+withStackVars :: (StackVars inp -> IndigoState inp out) -> IndigoState inp out
+withStackVars fIs = IndigoState $ \md -> usingIndigoState md (fIs $ mdStack md)
 
--- | Initial state of 'IndigoState'.
-data MetaData stk = MetaData
-  { mdStack :: StackVars stk
-  -- ^ Stack of the symbolic interpreter.
-  , mdRefCount :: RefId
-  -- ^ Number of allocated variables.
+----------------------------------------------------------------------------
+-- MetaData primitives
+----------------------------------------------------------------------------
+
+type DecomposedObjects = Map RefId SomeObject
+
+data MetaData inp = MetaData
+  { mdStack   :: StackVars inp
+  , mdObjects :: DecomposedObjects
   }
 
-emptyMetadata :: MetaData '[]
-emptyMetadata = MetaData RNil 0
+replStkMd :: MetaData inp -> StackVars inp1 -> MetaData inp1
+replStkMd md = alterStkMd md . const
 
-type DefaultStack stk = Default (MetaData stk)
+alterStkMd :: MetaData inp -> (StackVars inp -> StackVars inp1) -> MetaData inp1
+alterStkMd (MetaData stk objs) f = MetaData (f stk) objs
 
-instance Default (MetaData '[]) where
-  def = emptyMetadata
+-- | 'pushRef' version for 'MetaData'
+pushRefMd :: KnownValue a => Var a -> MetaData inp -> MetaData (a & inp)
+pushRefMd var md = alterStkMd md (pushRef var)
 
-instance (KnownValue x, Default (MetaData xs)) => Default (MetaData (x ': xs)) where
-  def = MetaData (NoRef :& mdStack def) 0
+-- | 'pushNoRef' version for 'MetaData'
+pushNoRefMd :: KnownValue a => MetaData inp -> MetaData (a & inp)
+pushNoRefMd md = alterStkMd md pushNoRef
 
+-- | 'popNoRef' version for 'MetaData'
+popNoRefMd :: MetaData (a & inp) -> MetaData inp
+popNoRefMd md = alterStkMd md popNoRef
+
+----------------------------------------------------------------------------
+-- Code generation primitives
+----------------------------------------------------------------------------
+
 -- | Resulting state of IndigoM.
-data GenCode inp out a = GenCode
-  { gcOut :: ~a
-  -- ^ Interpreter output value
-  , gcMeta :: ~(MetaData out)
-  -- ^ Interpreter meta data.
+data GenCode inp out = GenCode
+  { gcStack :: ~(StackVars out)
+  -- ^ Stack of the symbolic interpreter.
   , gcCode  :: inp :-> out
   -- ^ Generated Lorentz code.
   , gcClear :: out :-> inp
   -- ^ Clearing Lorentz code.
-  } deriving stock Functor
+  }
 
 -- | Produces the generated Lorentz code that cleans after itself, leaving the
 -- same stack as the input one
-cleanGenCode :: GenCode inp out a -> inp :-> inp
+cleanGenCode :: GenCode inp out -> inp :-> inp
 cleanGenCode GenCode {..} = gcCode ## gcClear
diff --git a/src/Indigo/Internal/Var.hs b/src/Indigo/Internal/Var.hs
new file mode 100644
--- /dev/null
+++ b/src/Indigo/Internal/Var.hs
@@ -0,0 +1,136 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+module Indigo.Internal.Var
+  ( -- * Variables
+    Var (..)
+  , RefId
+  , StackVars
+  , StkEl (..)
+
+  -- * Stack operations
+  , emptyStack
+  , assignVarAt
+  , pushRef
+  , pushNoRef
+  , popNoRef
+
+  -- * Operations/Storage variables
+  , Ops
+  , HasSideEffects
+  , operationsVar
+  , HasStorage
+  , storageVar
+  ) where
+
+import qualified Data.Kind as Kind
+import Data.Reflection (Given(..))
+import Data.Singletons (Sing)
+import Data.Type.Equality (TestEquality(..))
+import Data.Typeable (eqT)
+
+import Indigo.Backend.Prelude
+import Indigo.Lorentz
+import Util.Peano
+
+----------------------------------------------------------------------------
+-- Stack and variable definition
+----------------------------------------------------------------------------
+
+-- | Reference id to a stack cell
+newtype RefId = RefId Word
+  deriving stock (Show, Generic)
+  deriving newtype (Eq, Ord, Real, Num, Bounded)
+
+-- | Stack element of the symbolic interpreter.
+--
+-- It holds either a reference index that refers to this element
+-- or just 'NoRef', indicating that there are no references
+-- to this element.
+data StkEl a where
+  NoRef :: KnownValue a => StkEl a
+  Ref :: KnownValue a => RefId -> StkEl a
+
+instance TestEquality StkEl where
+  testEquality NoRef NoRef = eqT
+  testEquality (Ref _) (Ref _) = eqT
+  testEquality (Ref _) NoRef = eqT
+  testEquality NoRef (Ref _) = eqT
+
+-- | Stack of the symbolic interpreter.
+type StackVars (stk :: [Kind.Type]) = Rec StkEl stk
+
+-- | A variable referring to an element in the stack.
+data Var a = Var RefId
+  deriving stock (Generic, Show)
+
+----------------------------------------------------------------------------
+-- Stack operations
+----------------------------------------------------------------------------
+
+emptyStack :: StackVars '[]
+emptyStack = RNil
+
+instance Default (StackVars '[]) where
+  def = emptyStack
+
+instance (KnownValue x, Default (StackVars xs)) => Default (StackVars (x ': xs)) where
+  def = NoRef :& def
+
+-- | Given a 'StackVars' and a @Peano@ singleton for a depth, it puts a new 'Var'
+-- at that depth (0-indexed) and returns it with the updated 'StackVars'.
+--
+-- If there is a 'Var' there already it is used and the 'StackVars' not changed.
+assignVarAt
+  :: (KnownValue a, a ~ At n inp, RequireLongerThan inp n)
+  => Var a
+  -> StackVars inp
+  -> Sing n
+  -> StackVars inp
+assignVarAt var@(Var varRef) md@(top :& xs) = \case
+  SS n -> appendToStack top $ assignVarAt var xs n
+  SZ -> case top of
+    Ref mdRef | mdRef == varRef -> md
+    Ref _ -> error "Tried to assign a Var to an already referenced value"
+    NoRef -> Ref varRef :& xs
+  where
+    appendToStack :: StkEl x -> StackVars inp -> StackVars (x ': inp)
+    appendToStack v st = v :& st
+
+-- | Push a new stack element with a reference to it, given the variable.
+pushRef :: KnownValue a => Var a -> StackVars inp -> StackVars (a & inp)
+pushRef (Var ref) xs = Ref ref :& xs
+
+-- | Push a new stack element without a reference to it.
+pushNoRef :: KnownValue a => StackVars inp -> StackVars (a & inp)
+pushNoRef xs = NoRef :& xs
+
+-- | Remove the top element of the stack.
+-- It's supposed that no variable refers to this element.
+popNoRef :: StackVars (a & inp) -> StackVars inp
+popNoRef (NoRef :& xs) = xs
+popNoRef (Ref refId :& _) =
+  error $ "You try to pop stack element, which is referenced by some variable #" <> show refId
+
+----------------------------------------------------------------------------
+-- Operations/Storage variables
+----------------------------------------------------------------------------
+
+type Ops = [Operation]
+
+-- | Allows to get a variable with operations
+type HasSideEffects = Given (Var Ops)
+
+-- | Return a variable which refers to a stack cell with operations
+operationsVar :: HasSideEffects => Var Ops
+operationsVar = given
+
+-- This storage machinery is here to avoid cyclic deps
+
+-- | Allows to get a variable with storage
+type HasStorage st = (Given (Var st), KnownValue st)
+
+-- | Return a variable which refers to a stack cell with storage
+storageVar :: HasStorage st => Var st
+storageVar = given
diff --git a/src/Indigo/Lib.hs b/src/Indigo/Lib.hs
--- a/src/Indigo/Lib.hs
+++ b/src/Indigo/Lib.hs
@@ -19,9 +19,9 @@
   , subGt0
   ) where
 
-import Indigo.Compilation
 import Indigo.Frontend
 import Indigo.Internal.Expr
+import Indigo.Internal.Var (HasSideEffects)
 import Indigo.Lorentz
 import Indigo.Prelude
 import Indigo.Rebinded
@@ -81,7 +81,7 @@
 void_ f v = do
   doc (DThrows (Proxy @(VoidResult b)))
   r <- f (v #! #voidParam)
-  failWith $ pair voidResultTag (Exec (toExpr r) (v #! #voidResProxy))
+  failWith @() $ pair voidResultTag (Exec (toExpr r) (v #! #voidResProxy))
 
 -- | Flipped version of 'void_' that is present due to the common
 -- appearance of @flip void_ parameter $ instr@ construction.
diff --git a/src/Indigo/Print.hs b/src/Indigo/Print.hs
--- a/src/Indigo/Print.hs
+++ b/src/Indigo/Print.hs
@@ -18,6 +18,7 @@
 
 import Indigo.Compilation
 import Indigo.Internal.Object
+import Indigo.Frontend.Program (IndigoContract)
 import Indigo.Lorentz
 import Indigo.Prelude
 
diff --git a/src/Indigo/Rebinded.hs b/src/Indigo/Rebinded.hs
--- a/src/Indigo/Rebinded.hs
+++ b/src/Indigo/Rebinded.hs
@@ -28,10 +28,9 @@
 import qualified Prelude as P
 import qualified Data.Kind as Kind
 
-import Indigo.Internal
-import Indigo.Frontend
-import Indigo.Backend.Scope
 import Indigo.Backend.Conditional (IfConstraint)
+import Indigo.Frontend
+import Indigo.Internal
 import Indigo.Lorentz
 import Util.Label (IsLabel(..))
 
diff --git a/test/Test/Code/Lambda.hs b/test/Test/Code/Lambda.hs
--- a/test/Test/Code/Lambda.hs
+++ b/test/Test/Code/Lambda.hs
@@ -101,8 +101,7 @@
 
 -- | Use a variable from outer scope to check
 -- that an error is raised.
--- TODO attach scopes to variables and prevent
--- variables from leaking more severely.
+-- TODO attach scopes to variables and prevent variables from leaking more severely.
 -- Current approach doesn't throw a proper error in the following cases:
 -- * a contract param is in closure of lambda
 -- * a pure lambda uses @storageVar@ or @opsVar@
diff --git a/test/Test/Lambda.hs b/test/Test/Lambda.hs
--- a/test/Test/Lambda.hs
+++ b/test/Test/Lambda.hs
@@ -58,7 +58,7 @@
   , testCase "Outer scope error" $
       (pure $! lambdaOuterVarClosure)
       `shouldThrow`
-      (errorCall "In a scope of function you are using a variable from an outer scope. Closures are not supported yet.")
+      (errorCall "You are looking for manually created or leaked variable. Ref #RefId 3 of type Integer")
   ]
   where
     genInteger = Gen.integral (Range.linearFrom 0 -1000 1000)