diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,21 @@
+0.2.1
+=====
+* [!570](https://gitlab.com/morley-framework/morley/-/merge_requests/570)
+  Added `coerce` and `forcedCoerce` to convert between expressions of types that
+  have the same Michelson representation.
+* [!558](https://gitlab.com/morley-framework/morley/-/merge_requests/558)
+  Added `wrap` and `unwrap`, to generate from and extract to, values given a
+  constructor with a single fields for a sum type.
+* [!538](https://gitlab.com/morley-framework/morley/-/merge_requests/538)
+  Add the `showcase` section presenting a list of public smart contracts written
+  in Indigo.
+* [!533](https://gitlab.com/morley-framework/morley/-/merge_requests/533)
+  Add a tutorial on how to add documentation to a contract.
+  + Create helper functions: `saveDocumentation` and `printDocumentation`
+    which can generate the documentation via the REPL.
+  + Add short-handed doc item statements such as: `anchor`, `description`,
+    and `example`.
+
 0.2.0
 =====
 * [!542](https://gitlab.com/morley-framework/morley/-/merge_requests/542)
diff --git a/indigo.cabal b/indigo.cabal
--- a/indigo.cabal
+++ b/indigo.cabal
@@ -4,10 +4,10 @@
 --
 -- see: https://github.com/sol/hpack
 --
--- hash: 4ddca34d74587bae4cd69ff4a36aa20d8c7ae38da4031d1669a7d7a9d5b53a53
+-- hash: cffb0e9fcbd7e171ecdaea6999a9b146bc06fdac4a338f7db72867769b51c9f8
 
 name:           indigo
-version:        0.2.0
+version:        0.2.1
 synopsis:       Convenient imperative eDSL over Lorentz.
 description:    Syntax and implementation of Indigo eDSL.
 category:       Language
@@ -41,7 +41,6 @@
       Indigo.Compilation
       Indigo.Compilation.Lambda
       Indigo.Compilation.Params
-      Indigo.FromLorentz
       Indigo.Frontend
       Indigo.Frontend.Language
       Indigo.Frontend.Program
@@ -79,8 +78,8 @@
     , morley-prelude
     , reflection
     , singletons
-    , template-haskell
     , vinyl
+    , with-utf8
   mixins:
       base hiding (Prelude)
   default-language: Haskell2010
@@ -124,6 +123,7 @@
     , tasty
     , tasty-hedgehog
     , tasty-hunit-compat
+    , with-utf8
   mixins:
       base hiding (Prelude)
   default-language: Haskell2010
diff --git a/src/Indigo.hs b/src/Indigo.hs
--- a/src/Indigo.hs
+++ b/src/Indigo.hs
@@ -7,11 +7,10 @@
   ) where
 
 import Indigo.Compilation as Exports
-import Indigo.FromLorentz as Exports
 import Indigo.Frontend as Exports
 import Indigo.Internal as Exports hiding (return, (=<<), (>>), (>>=))
 import Indigo.Lib as Exports
-import Indigo.Lorentz as Exports
+import Indigo.Lorentz as Exports hiding (forcedCoerce)
 import Indigo.Prelude as Exports
 import Indigo.Print as Exports
 import Indigo.Rebinded as Exports
diff --git a/src/Indigo/Backend.hs b/src/Indigo/Backend.hs
--- a/src/Indigo/Backend.hs
+++ b/src/Indigo/Backend.hs
@@ -36,14 +36,6 @@
 
   -- * Comments
   , comment
-
-  -- * Conversion from Lorentz
-  , fromLorentzFun1
-  , fromLorentzFun2
-  , fromLorentzFun3
-  , fromLorentzFun1Void
-  , fromLorentzFun2Void
-  , fromLorentzFun3Void
   ) where
 
 import Indigo.Backend.Case as ReExports
@@ -54,7 +46,6 @@
 import Indigo.Backend.Var as ReExports
 
 import Indigo.Backend.Prelude
-import Indigo.FromLorentz
 import Indigo.Internal
 import Indigo.Lorentz
 import qualified Lorentz.Doc as L
@@ -69,24 +60,20 @@
 ----------------------------------------------------------------------------
 
 -- | While statement. The same rule about releasing.
-while :: forall inp xs ex . ex :~> Bool => ex -> IndigoState inp xs () -> IndigoState inp inp ()
+while :: Expr Bool -> IndigoState inp xs () -> IndigoState inp inp ()
 while e body = IndigoState $ \md ->
-  let expCd = gcCode $ runIndigoState (compileToExpr e) md in
+  let expCd = gcCode $ runIndigoState (compileExpr e) md in
   let bodyIndigoState = cleanGenCode $ runIndigoState body md in
   GenCode () md (expCd # L.loop (bodyIndigoState # expCd)) L.nop
 
 whileLeft
-  :: forall inp xs ex l r .
-     ( ex :~> Either l r
-     , KnownValue l
-     , KnownValue r
-     )
-  => ex
+  :: (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 ->
   let
-    cde = gcCode $ runIndigoState (compileToExpr e) md
+    cde = gcCode $ runIndigoState (compileExpr e) md
     (l, newMd) = pushRefMd md
     gc = cleanGenCode $ runIndigoState (body l) newMd
     (r, resMd) = pushRefMd md
@@ -94,11 +81,11 @@
 
 -- | For statements to iterate over container.
 forEach
-  :: forall a e inp xs. (IterOpHs a, KnownValue (IterOpElHs a), e :~> a)
-  => e -> (Var (IterOpElHs a) -> IndigoState ((IterOpElHs a) & inp) xs ())
+  :: (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 (compileToExpr container) md in
+  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
@@ -142,11 +129,11 @@
 
 -- | Indigo version for the function of the same name from Lorentz.
 finalizeParamCallingDoc
-  :: forall cp param inp out x. (param :~> cp, NiceParameterFull cp, RequireSumType cp, HasCallStack)
+  :: (NiceParameterFull cp, RequireSumType cp, HasCallStack)
   => (Var cp -> IndigoState (cp & inp) out x)
-  -> (param -> IndigoState inp out x)
+  -> (Expr cp -> IndigoState inp out x)
 finalizeParamCallingDoc act param = IndigoState $ \md ->
-  let cde = gcCode $ runIndigoState (compileToExpr param) md in
+  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)
@@ -168,14 +155,13 @@
   makeTopVar
 
 contractCalling
-  :: forall cp inp epRef epArg addr exAddr.
+  :: forall cp inp epRef epArg addr.
      ( HasEntrypointArg cp epRef epArg
      , ToTAddress cp addr
      , ToT addr ~ ToT Address
-     , IsExpr exAddr addr
      , KnownValue epArg
      )
-  => epRef -> exAddr
+  => epRef -> Expr addr
   -> IndigoState inp (Maybe (ContractRef epArg) & inp) (Var (Maybe (ContractRef epArg)))
 contractCalling epRef addr = do
   unaryOp addr (L.contractCalling @cp epRef)
@@ -186,13 +172,14 @@
 ----------------------------------------------------------------------------
 
 transferTokens
-  :: (IsExpr exp p, IsExpr exm Mutez, IsExpr exc (ContractRef p), NiceParameter p, HasSideEffects)
-  => exp -> exm -> exc -> IndigoState inp inp ()
+  :: (NiceParameter p, HasSideEffects)
+  => Expr p -> Expr Mutez -> Expr (ContractRef p)
+  -> IndigoState inp inp ()
 transferTokens ep em ec = do
   MetaData s _ <- iget
   ternaryOpFlat ep em ec (L.transferTokens # varActionOperation s)
 
-setDelegate :: (HasSideEffects, IsExpr ex (Maybe KeyHash)) => ex -> IndigoState inp inp ()
+setDelegate :: HasSideEffects => Expr (Maybe KeyHash) -> IndigoState inp inp ()
 setDelegate e =  do
   MetaData s _ <- iget
   unaryOpFlat e (L.setDelegate # varActionOperation s)
@@ -237,12 +224,3 @@
 -- | Add a comment
 comment :: MT.CommentType -> IndigoState i i ()
 comment t = IndigoState $ \md -> GenCode () md (L.comment t) L.nop
-
-----------------------------------------------------------------------------
--- Conversion from Lorentz
-----------------------------------------------------------------------------
-
--- Functions that convert Lorentz code to Indigo.
--- Will be removed when all Lorentz code is translated in Indigo.
-
-$(genFromLorentzFunN 3)
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
@@ -71,53 +71,52 @@
       )
 
 -- This constraint is shared by all @case*@ functions.
-type CaseCommonF f dt guard ret clauses =
-     ( guard :~> dt
-     , InstrCaseC dt
+type CaseCommonF f dt ret clauses =
+     ( InstrCaseC dt
      , RMap (CaseClauses dt)
      , clauses ~ Rec (f ret) (CaseClauses dt)
      , ScopeCodeGen ret
      )
 
-type CaseCommon dt guard ret clauses = CaseCommonF IndigoCaseClauseL dt guard ret clauses
+type CaseCommon dt ret clauses = CaseCommonF IndigoCaseClauseL dt ret clauses
 
 -- | A case statement for indigo. See examples for a sample usage.
 caseRec
-  :: forall dt guard inp ret clauses . ( CaseCommon dt guard ret clauses)
-  => guard
+  :: 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 (compileToExpr g) md in
+  let cdG = gcCode $ runIndigoState (compileExpr g) md in
   finalizeStatement @ret md (cdG # L.case_ (toCaseClauseL md cls))
 
 -- | 'case_' for pattern-matching on parameter.
 entryCaseRec
-  :: forall dt entrypointKind guard inp ret clauses .
-  ( CaseCommon dt guard ret clauses
+  :: forall dt entrypointKind inp ret clauses .
+  ( CaseCommon dt ret clauses
   , DocumentEntrypoints entrypointKind dt
   )
   => Proxy entrypointKind
-  -> guard
+  -> Expr dt
   -> clauses
   -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
 entryCaseRec proxy g cls = IndigoState $ \md ->
-  let cdG = gcCode $ runIndigoState (compileToExpr g) md in
+  let cdG = gcCode $ runIndigoState (compileExpr g) md in
   finalizeStatement @ret md (cdG # L.entryCase_ proxy (toCaseClauseL md cls))
 
 -- | 'entryCase_' for contracts with flat parameter.
 entryCaseSimpleRec
-  :: forall cp guard inp ret clauses .
-     ( CaseCommon cp guard ret clauses
+  :: forall cp inp ret clauses .
+     ( CaseCommon cp ret clauses
      , DocumentEntrypoints PlainEntrypointsKind cp
      , NiceParameterFull cp
      , RequireFlatParamEps cp
      )
-  => guard
+  => Expr cp
   -> clauses
   -> IndigoState inp (RetOutStack ret ++ inp) (RetVars ret)
 entryCaseSimpleRec g cls = IndigoState $ \md ->
-  let cdG = gcCode $ runIndigoState (compileToExpr g) md in
+  let cdG = gcCode $ runIndigoState (compileExpr g) md in
   finalizeStatement @ret md (cdG # L.entryCaseSimple_ (toCaseClauseL md cls))
 
 toCaseClauseL
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
@@ -44,32 +44,26 @@
 -- | 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 exc .
-     ( IfConstraint a b
-     , exc :~> Bool
-     )
-  => exc
+  :: forall inp xs ys 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 (compileToExpr e) md in
+  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))
 
 -- | If which works like case for Maybe.
 ifSome
-  :: forall inp xs ys x a b exa .
-     ( IfConstraint a b, KnownValue x
-     , exa :~> Maybe x
-     )
-  => exa
+  :: forall inp xs ys 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 (compileToExpr e) md in
+  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
@@ -85,17 +79,14 @@
 
 -- | If which works like case for Either.
 ifRight
-  :: forall inp xs ys x y a b exa .
-     ( IfConstraint a b, KnownValue x, KnownValue y
-     , exa :~> Either y x
-     )
-  => exa
+  :: 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 ->
   let
-    cde = gcCode $ runIndigoState (compileToExpr e) md
+    cde = gcCode $ runIndigoState (compileExpr e) md
     (v, mdRight) = pushRefMd md
     (w, mdLeft) = pushRefMd md
     gc1 = runIndigoState (r v) mdRight
@@ -116,18 +107,14 @@
         )
 
 ifCons
-  :: forall inp xs ys x a b exa .
-     ( IfConstraint a b
-     , KnownValue x
-     , exa :~> List x
-     )
-  => exa
+  :: forall inp xs ys 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 ->
   let
-    cde = gcCode $ runIndigoState (compileToExpr e) md
+    cde = gcCode $ runIndigoState (compileExpr e) md
     (l, mdList) = pushRefMd md
     (v, mdVal) = pushRefMd mdList
     gc1 = runIndigoState (t v l) mdVal
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
@@ -43,24 +43,21 @@
     errMd = error $ "MetaData" <> msg
     failCl = L.unit # L.failWith
 
-failWith
-  :: IsExpr ex a
-  => ex -> IndigoState s t r
-failWith exa = compileToExpr exa >> failIndigoState L.failWith
+failWith :: KnownValue a => Expr a -> IndigoState s t r
+failWith exa = compileExpr exa >> failIndigoState L.failWith
 
 failUsing_ :: (IsError x) => x -> IndigoState s t r
 failUsing_ x = failIndigoState (failUsing x)
 
 failCustom
-  :: forall tag err ex s t r.
+  :: forall tag err s t r.
      ( err ~ ErrorArg tag
      , CustomErrorHasDoc tag
      , NiceConstant err
-     , IsExpr ex err
      )
-  => Label tag -> ex -> IndigoState s t r
+  => Label tag -> Expr err -> IndigoState s t r
 failCustom l errEx = withDict (niceConstantEvi @err) $ do
-  compileToExpr errEx
+  compileExpr errEx
   failIndigoState $ L.failCustom l
 
 failCustom_
@@ -75,79 +72,55 @@
 failUnexpected_ msg = failUsing_ $ [mt|Unexpected: |] <> msg
 
 assert
-  :: forall s x ex.
-  ( IsError x
-  , IsExpr ex Bool
-  )
-  => x -> ex -> IndigoState s s ()
+  :: 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 ex.
-  ( IsError err
-  , KnownValue x
-  , ex :~> Maybe x
-  )
-  => err -> ex -> IndigoState s s ()
+  :: 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 ex.
-  ( IsError err
-  , KnownValue x
-  , ex :~> Maybe x
-  )
-  => err -> ex -> IndigoState s s ()
+  :: 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 ex.
-  ( IsError err
-  , KnownValue x
-  , KnownValue y
-  , ex :~> Either y x
-  )
-  => err -> ex -> IndigoState s s ()
+  :: 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 ex.
-  ( IsError err
-  , KnownValue x
-  , KnownValue y
-  , ex :~> Either y x
-  )
-  => err -> ex -> IndigoState s s ()
+  :: 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 errEx ex s.
+  :: forall tag err s.
      ( err ~ ErrorArg tag
      , CustomErrorHasDoc tag
      , NiceConstant err
-     , IsExpr errEx err
-     , IsExpr ex Bool
      )
-  => Label tag -> errEx -> ex -> IndigoState s s ()
+  => 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 ex.
+  :: forall tag s notVoidErrorMsg.
      ( RequireNoArgError tag notVoidErrorMsg
      , CustomErrorHasDoc tag
-     , IsExpr ex Bool
      )
-  => Label tag -> ex -> IndigoState s s ()
+  => 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
@@ -229,7 +229,7 @@
         (gcCode $
           usingIndigoState allocMd $ do
               compileExpr argm
-              compileToExpr (V varF)) in
+              compileExpr (V varF)) in
   case listOfTypesConcatAssociativityAxiom @(RetOutStack res) @extra @inp of
     Dict ->
       let code = getArgs #
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
@@ -235,3 +235,6 @@
   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) ()
+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
@@ -18,8 +18,8 @@
 import Util.Type (type (++))
 
 -- | Create a new variable with passed expression as an initial value.
-newVar :: IsExpr ex x => ex -> IndigoState inp (x & inp) (Var x)
-newVar e = compileToExpr e >> makeTopVar
+newVar :: KnownValue x => Expr x -> IndigoState inp (x & inp) (Var x)
+newVar e = compileExpr e >> makeTopVar
 
 -- | Set the variable to a new value.
 --
@@ -27,9 +27,7 @@
 -- 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 ex inp . ex :~> a
-  => Var a -> ex -> IndigoState inp inp ()
+setVar :: forall a inp. Var a -> Expr a -> IndigoState inp inp ()
 setVar (Cell refId) e = do
   MetaData s _ <- iget
   unaryOpFlat e $ varActionSet refId s
@@ -59,14 +57,13 @@
     rmapZipM (TypedFieldVar f :& flds) (e :& exprs) = setVar f e >> rmapZipM flds exprs
 
 -- | Set the field (direct or indirect) of a complex object.
-setField ::
-  forall dt fname ftype ex inp .
-  ( ex :~> ftype
-  , IsObject dt
-  , IsObject ftype
-  , HasField dt fname ftype
-  )
-  => Var dt -> Label fname -> ex -> IndigoState inp inp ()
+setField
+  :: forall dt fname ftype inp .
+     ( IsObject dt
+     , 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 _ ->
@@ -80,10 +77,10 @@
 
 -- | Call binary operator with constant argument to update variable in-place.
 updateVar
-  :: (IsExpr ey y, IsObject x)
+  :: (IsObject x, KnownValue y)
   => [y, x] :-> '[x]
   -> Var x
-  -> ey
+  -> Expr y
   -> IndigoState inp inp ()
 updateVar action (Cell refId) e = do
   MetaData s _ <- iget
diff --git a/src/Indigo/FromLorentz.hs b/src/Indigo/FromLorentz.hs
deleted file mode 100644
--- a/src/Indigo/FromLorentz.hs
+++ /dev/null
@@ -1,101 +0,0 @@
--- SPDX-FileCopyrightText: 2020 Tocqueville Group
---
--- SPDX-License-Identifier: LicenseRef-MIT-TQ
-
-{-# LANGUAGE NoRebindableSyntax #-}
-
--- | Generation of functions that convert Lorentz code to Indigo
-
-module Indigo.FromLorentz
-  ( genFromLorentzFunN
-  , fromLorentzFunN
-  ) where
-
-import Control.Monad hiding (replicateM)
-import Language.Haskell.TH
-
-import Indigo.Backend.Prelude
-import Indigo.Internal.Expr (IsExpr)
-import qualified Indigo.Internal.Object as O
-import qualified Indigo.Internal.State as S
-import Indigo.Lorentz (type (&), (:->), KnownValue)
-import qualified Lorentz.Instr as L
-
--- | Generates all of the 'fromLorentzFunN' (both with and without return value)
--- from 1 to the given @n@
-genFromLorentzFunN :: Int -> Q [Dec]
-genFromLorentzFunN n = do
-  fsArgs <- mapM (`fromLorentzFunN` True ) [1..n]
-  fsVoid <- mapM (`fromLorentzFunN` False) [1..n]
-  return $ concat (fsArgs ++ fsVoid)
-
--- | Generates a function that converts a Lorentz expression to an Indigo one.
---
--- The first parameter is the number of elements that the Lorentz code consumes
--- from the stack, as well as the number of Indigo 'IsExpr' values.
---
--- The second parameter is to establish if there is a return value or not,
--- as well as the name of the function.
---
--- Examples:
---
--- * @fromLorentzFunN 1 False@ produces:
---
--- @
--- fromLorentzFun1Void :: IsExpr ex a => a & s :-> s -> ex -> IndigoM s s ()
--- @
--- * @fromLorentzFunN 2 True@ produces:
---
--- @
--- fromLorentzFun2
---   :: (KnownValue ret, IsExpr ex1 a, IsExpr ex2 b)
---   => a & b & s :-> ret & s
---   -> ex1 -> ex2 -> IndigoM s (ret & s) (Var ret)
--- @
-fromLorentzFunN :: Int -> Bool -> Q [Dec]
-fromLorentzFunN n hasRet
-  | n <= 0 = fail "fromLorentzFunN requires a positive number of arguments"
-  | otherwise = do
-    -- Names
-    lz  <- newName "lz"
-    exs <- replicateM n $ newName "ex"
-    as  <- replicateM n $ newName "a"
-    st  <- newName "s"
-    ret <- newName "ret"
-    let
-      -- Parameters
-      args = map varP (lz : exs)
-      -- Expressions
-      exCompile = map (\x -> [| compileToExpr $(varE x) |]) exs
-      compile = foldl1 (\l r -> [| $r S.>> $l |]) exCompile
-      updateMd = if hasRet then [| pushNoRefMd |] else [| id |]
-      clear = if hasRet then [| L.drop |] else [| L.nop |]
-      fun = varE lz
-      execute = [| S.IndigoState $ \md ->
-        let cdc = gcCode $ runIndigoState $compile md in
-        S.GenCode () ($updateMd md) (cdc # $fun) $clear |]
-      body = if hasRet
-        then [| $execute S.>> O.makeTopVar |]
-        else [| $execute |]
-      -- Types
-      asType = map varT as
-      exTypes = map varT exs
-      stType = varT st
-      retType = varT ret
-
-      inpType = foldr1 (\a c -> [t| ($a & $c) |] ) (asType ++ [stType])
-      outType = if hasRet then [t| $retType & $stType |] else stType
-      lzType = [t| $inpType :-> $outType |]
-
-      indigoRetType = if hasRet then [t| O.Var $retType |] else [t| () |]
-      indigoType = [t| S.IndigoState $stType $outType $indigoRetType |]
-
-      fullType = foldr (appT . appT arrowT) indigoType (lzType : exTypes)
-      constraints = cxt . (if hasRet then ([t| KnownValue $retType |] :) else id) $
-        zipWith (\ex a -> [t| IsExpr $ex $a |]) exTypes asType
-    -- Definitions
-    signature <- sigD name $ forallT [] constraints fullType
-    definition <- funD name [clause args (normalB body) []]
-    return [signature, definition]
-  where
-    name = mkName $ "fromLorentzFun" ++ show n ++ (if hasRet then "" else "Void")
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
@@ -74,6 +74,11 @@
   , contractGeneralDefault
   , finalizeParamCallingDoc
 
+  -- * Short-handed doc item
+  , anchor
+  , description
+  , example
+
   -- * Side-effects operations
   , transferTokens
   , setDelegate
@@ -120,6 +125,7 @@
 import qualified Michelson.Typed as MT
 import qualified Michelson.Typed.Arith as M
 import Michelson.Typed.Haskell.Instr.Sum (CaseClauseParam(..), CtorField(..))
+import Util.Markdown (toAnchor)
 import Util.TypeLits (AppendSymbol)
 import Util.TypeTuple.Class
 
@@ -132,7 +138,7 @@
 varModification
   :: (IsExpr ey y, IsObject x)
   => ([y, x] :-> '[x]) -> Var x -> ey -> IndigoM ()
-varModification act v ex = oneIndigoM $ VarModification act v ex
+varModification act v = oneIndigoM . VarModification act v . toExpr
 
 ----------------------------------------------------------------------------
 -- Var creation and assignment
@@ -140,14 +146,14 @@
 
 -- | Create a new variable with the result of the given expression as its initial value.
 new :: IsExpr ex x => ex -> IndigoM (Var x)
-new e = oneIndigoM $ NewVar e
+new = oneIndigoM . NewVar . toExpr
 
 -- | Set the given variable to the result of the given expression.
-setVar :: (IsExpr ex x, IsObject x) => Var x -> ex -> IndigoM ()
-setVar v e = oneIndigoM $ SetVar v e
+setVar :: (IsExpr ex x) => Var x -> ex -> IndigoM ()
+setVar v = oneIndigoM . SetVar v . toExpr
 
 infixr 0 =:
-(=:) :: (IsExpr ex x, IsObject x) => Var x -> ex -> IndigoM ()
+(=:) :: IsExpr ex x => Var x -> ex -> IndigoM ()
 v =: e = setVar v e
 
 setField
@@ -157,7 +163,7 @@
      , HasField dt fname ftype
      )
   => Var dt -> Label fname -> ex -> IndigoM ()
-setField v fName e = oneIndigoM $ SetField v fName e
+setField v fName = oneIndigoM . SetField v fName . toExpr
 
 (+=)
   :: ( IsExpr ex1 n, IsObject m
@@ -262,7 +268,7 @@
   -> IndigoM a
   -> IndigoM b
   -> IndigoM (RetVars a)
-if_ ex tb fb = oneIndigoM $ If ex tb fb
+if_ ex tb fb = oneIndigoM $ If (toExpr ex) tb fb
 
 -- | Run the instruction when the condition is met, do nothing otherwise.
 when :: (exc :~> Bool) => exc -> IndigoM () -> IndigoM ()
@@ -278,7 +284,7 @@
   -> (Var x -> IndigoM a)
   -> IndigoM b
   -> IndigoM (RetVars a)
-ifSome ex tb fb = oneIndigoM $ IfSome ex tb fb
+ifSome ex tb fb = oneIndigoM $ IfSome (toExpr ex) tb fb
 
 ifNone
   :: forall x a b ex . (KnownValue x, ex :~> Maybe x, IfConstraint a b)
@@ -286,7 +292,7 @@
   -> IndigoM b
   -> (Var x -> IndigoM a)
   -> IndigoM (RetVars a)
-ifNone ex fb tb = ifSome ex tb fb
+ifNone ex fb tb = ifSome (toExpr ex) tb fb
 
 -- | Run the instruction when the given expression returns 'Just' a value,
 -- do nothing otherwise.
@@ -323,7 +329,7 @@
   -> (Var x -> IndigoM a)
   -> (Var y -> IndigoM b)
   -> IndigoM (RetVars a)
-ifRight ex rb lb = oneIndigoM $ IfRight ex rb lb
+ifRight ex rb lb = oneIndigoM $ IfRight (toExpr ex) rb lb
 
 ifLeft
   :: forall x y a b ex .
@@ -366,7 +372,7 @@
   -> (Var x -> Var (List x) -> IndigoM a)
   -> IndigoM b
   -> IndigoM (RetVars a)
-ifCons ex tb fb = oneIndigoM $ IfCons ex tb fb
+ifCons ex tb fb = oneIndigoM $ IfCons (toExpr ex) tb fb
 
 ----------------------------------------------------------------------------
 -- Case
@@ -375,42 +381,47 @@
 -- | A case statement for indigo. See examples for a sample usage.
 caseRec
   :: forall dt guard ret clauses .
-     CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses
+     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt ret clauses
+     , guard :~> dt
+     )
   => guard
   -> clauses
   -> IndigoM (RetVars ret)
-caseRec = oneIndigoM ... Case
+caseRec g = oneIndigoM . Case (toExpr g)
 
 -- | 'caseRec' for tuples.
 case_
   :: forall dt guard ret clauses.
-     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses
+     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt ret clauses
      , RecFromTuple clauses
+     , guard :~> dt
      )
   => guard
   -> IsoRecTuple clauses
   -> IndigoM (RetVars ret)
-case_ g = caseRec g . recFromTuple @clauses
+case_ g = caseRec (toExpr g) . recFromTuple @clauses
 
 
 -- | 'caseRec' for pattern-matching on parameter.
 entryCaseRec
   :: forall dt entrypointKind guard ret clauses .
-     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses
+     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt ret clauses
      , DocumentEntrypoints entrypointKind dt
+     , guard :~> dt
      )
   => Proxy entrypointKind
   -> guard
   -> clauses
   -> IndigoM (RetVars ret)
-entryCaseRec proxy g cls = oneIndigoM $ EntryCase proxy g cls
+entryCaseRec proxy g cls = oneIndigoM $ EntryCase proxy (toExpr g) cls
 
 -- | 'entryCaseRec' for tuples.
 entryCase
   :: forall dt entrypointKind guard ret clauses .
-     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt guard ret clauses
+     ( CaseCommonF (IndigoMCaseClauseL IndigoM) dt ret clauses
      , RecFromTuple clauses
      , DocumentEntrypoints entrypointKind dt
+     , guard :~> dt
      )
   => Proxy entrypointKind
   -> guard
@@ -420,16 +431,17 @@
 
 entryCaseSimple
   :: forall cp guard ret clauses .
-     ( CaseCommonF (IndigoMCaseClauseL IndigoM) cp guard ret clauses
+     ( CaseCommonF (IndigoMCaseClauseL IndigoM) cp ret clauses
      , RecFromTuple clauses
      , DocumentEntrypoints PlainEntrypointsKind cp
      , NiceParameterFull cp
      , RequireFlatParamEps cp
+     , guard :~> cp
      )
   => guard
   -> IsoRecTuple clauses
   -> IndigoM (RetVars ret)
-entryCaseSimple g = oneIndigoM . EntryCaseSimple g . recFromTuple @clauses
+entryCaseSimple g = oneIndigoM . EntryCaseSimple (toExpr g) . recFromTuple @clauses
 
 {-# DEPRECATED (//->) "use '#=' instead" #-}
 -- | An alias for '#=' kept only for backward compatibility.
@@ -585,7 +597,7 @@
 
 -- | While statement.
 while :: forall ex . ex :~> Bool => ex -> IndigoM () -> IndigoM ()
-while e body = oneIndigoM $ While e body
+while e body = oneIndigoM $ While (toExpr e) body
 
 whileLeft
   :: forall x y ex .
@@ -596,14 +608,14 @@
   => ex
   -> (Var y -> IndigoM ())
   -> IndigoM (Var x)
-whileLeft e body = oneIndigoM $ WhileLeft e body
+whileLeft e body = oneIndigoM $ WhileLeft (toExpr e) body
 
 -- | For statements to iterate over a container.
 forEach
   :: forall a e . (IterOpHs a, KnownValue (IterOpElHs a), e :~> a)
   => e -> (Var (IterOpElHs a) -> IndigoM ())
   -> IndigoM ()
-forEach container body = oneIndigoM $ ForEach container body
+forEach container body = oneIndigoM $ ForEach (toExpr container) body
 
 ----------------------------------------------------------------------------
 -- Documentation
@@ -643,9 +655,21 @@
      , RequireSumType (ExprType param)
      , HasCallStack
      )
-  => (Var (ExprType param) -> IndigoM x) -> (param -> IndigoM x)
-finalizeParamCallingDoc = oneIndigoM ... FinalizeParamCallingDoc
+  => (Var (ExprType param) -> IndigoM x) -> param -> IndigoM x
+finalizeParamCallingDoc i = oneIndigoM . FinalizeParamCallingDoc i . toExpr
 
+-- | Put a 'DDescription' doc item.
+description :: Markdown -> IndigoM ()
+description = doc . DDescription
+
+-- | Put a 'DAnchor' doc item.
+anchor :: Text -> IndigoM ()
+anchor = doc . DAnchor . toAnchor
+
+-- | Put a 'DEntrypointExample' doc item.
+example :: forall a. NiceParameter a => a -> IndigoM ()
+example = doc . mkDEntrypointExample
+
 ----------------------------------------------------------------------------
 -- Contract call
 ----------------------------------------------------------------------------
@@ -668,7 +692,7 @@
      , KnownValue epArg
      )
   => epRef -> exAddr -> IndigoM (Var (Maybe (ContractRef epArg)))
-contractCalling = oneIndigoM ... ContractCalling (Proxy @cp)
+contractCalling epRef = oneIndigoM . ContractCalling (Proxy @cp) epRef . toExpr
 
 ----------------------------------------------------------------------------
 -- Side-effects operations
@@ -677,10 +701,11 @@
 transferTokens
   :: (IsExpr exp p, IsExpr exm Mutez, IsExpr exc (ContractRef p), NiceParameter p, HasSideEffects)
   => exp -> exm -> exc -> IndigoM ()
-transferTokens = oneIndigoM ... TransferTokens
+transferTokens ep em ec = oneIndigoM $
+  TransferTokens (toExpr ep) (toExpr em) (toExpr ec)
 
 setDelegate :: (HasSideEffects, IsExpr ex (Maybe KeyHash)) => ex -> IndigoM ()
-setDelegate =  oneIndigoM ... SetDelegate
+setDelegate =  oneIndigoM . SetDelegate . toExpr
 
 -- | Create contract using default compilation options for Lorentz compiler.
 --
@@ -696,7 +721,8 @@
   -> exm
   -> exs
   -> IndigoM (Var Address)
-createContract iCtr ek em es = oneIndigoM $ CreateContract (defaultContract $ compileIndigoContract iCtr) ek em es
+createContract iCtr ek em es = oneIndigoM $
+  CreateContract (defaultContract $ compileIndigoContract iCtr) (toExpr ek) (toExpr em) (toExpr es)
 
 -- | Create contract from raw Lorentz 'L.Contract'.
 createLorentzContract
@@ -710,7 +736,8 @@
   -> exm
   -> exs
   -> IndigoM (Var Address)
-createLorentzContract lCtr ek em es = oneIndigoM $ CreateContract lCtr ek em es
+createLorentzContract lCtr ek em es = oneIndigoM $
+  CreateContract lCtr (toExpr ek) (toExpr em) (toExpr es)
 
 ----------------------------------------------------------------------------
 -- Error
@@ -722,12 +749,12 @@
      , IsExpr ex Bool
      )
   => x -> ex -> IndigoM ()
-assert = oneIndigoM ... Assert
+assert x = oneIndigoM . Assert x . toExpr
 
 failWith
   :: forall r a ex . IsExpr ex a
   => ex -> IndigoM r
-failWith = oneIndigoM . FailWith
+failWith = oneIndigoM . FailWith . toExpr
 
 failCustom
   :: forall r tag err ex.
@@ -737,7 +764,7 @@
      , ex :~> err
      )
   => Label tag -> ex -> IndigoM r
-failCustom l errEx = oneIndigoM $ FailCustom l errEx
+failCustom l = oneIndigoM . FailCustom l . toExpr
 
 failCustom_
   :: forall r tag notVoidErrorMsg.
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,6 +9,7 @@
 
   , IfConstraint
   , IndigoMCaseClauseL (..)
+  , CaseCommonF
   ) where
 
 import qualified Data.Kind as Kind
@@ -57,21 +58,20 @@
   -- which are not going to be analyzed by optimizer.
   LiftIndigoState :: (forall inp . SomeIndigoState inp a) -> StatementF freer a
 
-  NewVar :: (ex :~> x) => ex -> StatementF freer (Var x)
-  SetVar :: (ex :~> x, IsObject x) => Var x -> ex -> StatementF freer ()
+  NewVar :: KnownValue x => Expr x -> StatementF freer (Var x)
+  SetVar :: Var x -> Expr x -> StatementF freer ()
   VarModification
-    :: (ey :~> y, IsObject x)
+    :: (IsObject x, KnownValue y)
     => [y, x] :-> '[x]
     -> Var x
-    -> ey
+    -> Expr y
     -> StatementF freer ()
   SetField ::
-    ( ex :~> ftype
-    , IsObject dt
+    ( IsObject dt
     , IsObject ftype
     , HasField dt fname ftype
     )
-    => Var dt -> Label fname -> ex -> StatementF cont ()
+    => Var dt -> Label fname -> Expr ftype -> StatementF cont ()
 
   -- | Pure lambda
   LambdaPure1Call
@@ -100,105 +100,99 @@
     -> StatementF freer (RetVars res)
 
   Scope :: ScopeCodeGen a => freer a -> StatementF freer (RetVars a)
-  If :: (IfConstraint a b, ex :~> Bool)
-     => ex
-     -> freer a
-     -> freer b
-     -> StatementF freer (RetVars a)
-  IfSome :: (IfConstraint a b, KnownValue x, ex :~> Maybe x)
-     => ex
-     -> (Var x -> freer a)
-     -> freer b
-     -> StatementF freer (RetVars a)
+  If
+    :: IfConstraint a b
+    => Expr Bool
+    -> freer a
+    -> freer b
+    -> StatementF freer (RetVars a)
+  IfSome
+    :: (IfConstraint a b, KnownValue x)
+    => Expr (Maybe x)
+    -> (Var x -> freer a)
+    -> freer b
+    -> StatementF freer (RetVars a)
   IfRight
-     :: (IfConstraint a b, KnownValue x, KnownValue y, ex :~> Either y x)
-     => ex
-     -> (Var x -> freer a)
-     -> (Var y -> freer b)
-     -> StatementF freer (RetVars a)
+    :: (IfConstraint a b, KnownValue x, KnownValue y)
+    => Expr (Either y x)
+    -> (Var x -> freer a)
+    -> (Var y -> freer b)
+    -> StatementF freer (RetVars a)
   IfCons
-     :: (IfConstraint a b, KnownValue x, ex :~> (List x) )
-     => ex
-     -> (Var x -> Var (List x) -> freer a)
-     -> freer b
-     -> StatementF freer (RetVars a)
-  Case :: CaseCommonF (IndigoMCaseClauseL freer) dt guard ret clauses
-       => guard -> clauses
-       -> StatementF freer (RetVars ret)
-  EntryCase ::
-    ( CaseCommonF (IndigoMCaseClauseL freer) dt guard ret clauses
-    , DocumentEntrypoints entrypointKind dt
-    )
+    :: (IfConstraint a b, KnownValue x)
+    => Expr (List x)
+    -> (Var x -> Var (List x) -> freer a)
+    -> freer b
+    -> StatementF freer (RetVars a)
+  Case
+    :: CaseCommonF (IndigoMCaseClauseL freer) dt ret clauses
+    => Expr dt -> clauses
+    -> StatementF freer (RetVars ret)
+  EntryCase
+    :: ( CaseCommonF (IndigoMCaseClauseL freer) dt ret clauses
+       , DocumentEntrypoints entrypointKind dt
+       )
     => Proxy entrypointKind
-    -> guard
+    -> Expr dt
     -> clauses
     -> StatementF freer (RetVars ret)
-  EntryCaseSimple ::
-         ( CaseCommonF (IndigoMCaseClauseL freer) cp guard ret clauses
-         , DocumentEntrypoints PlainEntrypointsKind cp
-         , NiceParameterFull cp
-         , RequireFlatParamEps cp
-         )
-      => guard
-      -> clauses
-      -> StatementF freer (RetVars ret)
+  EntryCaseSimple
+    :: ( CaseCommonF (IndigoMCaseClauseL freer) cp ret clauses
+       , DocumentEntrypoints PlainEntrypointsKind cp
+       , NiceParameterFull cp
+       , RequireFlatParamEps cp
+       )
+    => Expr cp
+    -> clauses
+    -> StatementF freer (RetVars ret)
 
-  While :: ex :~> Bool => ex -> freer () -> StatementF freer ()
+  While :: Expr Bool -> freer () -> StatementF freer ()
   WhileLeft
-    :: (KnownValue x, KnownValue y, ex :~> Either y x)
-    => ex
+    :: (KnownValue x, KnownValue y)
+    => Expr (Either y x)
     -> (Var y -> freer ())
     -> StatementF freer (Var x)
-  ForEach :: (IterOpHs a, KnownValue (IterOpElHs a), e :~> a)
-          => e
-          -> (Var (IterOpElHs a) -> freer ())
-          -> StatementF freer ()
+  ForEach
+    :: (IterOpHs a, KnownValue (IterOpElHs a))
+    => Expr a
+    -> (Var (IterOpElHs a) -> freer ())
+    -> StatementF freer ()
 
   ContractName :: Text        -> freer () -> StatementF freer ()
   DocGroup     :: DocGrouping -> freer () -> StatementF freer ()
   ContractGeneral :: freer () -> StatementF freer ()
   FinalizeParamCallingDoc
-    :: (ToExpr param, NiceParameterFull (ExprType param), RequireSumType (ExprType param), HasCallStack)
-    => (Var (ExprType param) -> freer x) -> param -> StatementF freer x
+    :: (NiceParameterFull cp, RequireSumType cp, HasCallStack)
+    => (Var cp -> freer x) -> Expr cp -> StatementF freer x
 
   TransferTokens
-    :: (exp :~> p, exm :~> Mutez, exc :~> ContractRef p, NiceParameter p, HasSideEffects)
-    => exp -> exm -> exc -> StatementF freer ()
-  SetDelegate :: (HasSideEffects, ex :~> Maybe KeyHash) => ex -> StatementF freer ()
+    :: (NiceParameter p, HasSideEffects)
+    => Expr p -> Expr Mutez -> Expr (ContractRef p) -> StatementF freer ()
+  SetDelegate :: HasSideEffects => Expr (Maybe KeyHash) -> StatementF freer ()
 
-  CreateContract ::
-    ( IsObject st
-    , exk :~> Maybe KeyHash, exm :~> Mutez, exs :~> st
-    , NiceStorage st, NiceParameterFull param
-    , HasSideEffects
-    )
+  CreateContract
+    :: ( IsObject st
+       , NiceStorage st, NiceParameterFull param
+       , HasSideEffects
+       )
     => L.Contract param st
-    -> exk
-    -> exm
-    -> exs
+    -> Expr (Maybe KeyHash)
+    -> Expr Mutez
+    -> Expr st
     -> StatementF freer (Var Address)
-  ContractCalling ::
-     ( HasEntrypointArg cp epRef epArg
-     , ToTAddress cp addr
-     , ToT addr ~ ToT Address
-     , exAddr :~> addr
-     , KnownValue epArg
-     )
-     => Proxy cp -> epRef -> exAddr -> StatementF freer (Var (Maybe (ContractRef epArg)))
+  ContractCalling
+    :: ( HasEntrypointArg cp epRef epArg
+       , ToTAddress cp addr
+       , ToT addr ~ ToT Address
+       , KnownValue epArg
+       )
+    => Proxy cp -> epRef -> Expr addr -> StatementF freer (Var (Maybe (ContractRef epArg)))
 
-  FailWith ::
-    ( ex :~> a
-    )
-    => ex -> StatementF freer r
-  Assert ::
-    ( IsError x
-    , ex :~> Bool
-    )
-    => x -> ex -> StatementF freer ()
-  FailCustom ::
-     ( err ~ ErrorArg tag
-     , CustomErrorHasDoc tag
-     , NiceConstant err
-     , ex :~> err
-     )
-     => Label tag -> ex -> StatementF freer r
+  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
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
@@ -6,7 +6,6 @@
 
 module Indigo.Internal.Expr.Compilation
   ( compileExpr
-  , compileToExpr
 
   , ObjManipulationRes (..)
   , runObjectManipulation
@@ -65,6 +64,8 @@
 compileExpr (Ge e1 e2) = binaryOp e1 e2 L.ge
 compileExpr (IsNat e) = unaryOp e L.isNat
 compileExpr (Int' e) = unaryOp e L.int
+compileExpr (Coerce e) = unaryOp e checkedCoerce_
+compileExpr (ForcedCoerce e) = unaryOp e forcedCoerce_
 compileExpr (And e1 e2) = binaryOp e1 e2 L.and
 compileExpr (Or e1 e2) = binaryOp e1 e2 L.or
 compileExpr (Xor e1 e2) = binaryOp e1 e2 L.xor
@@ -103,6 +104,9 @@
 compileExpr (UUpdate l ekey evalue estore) = ternaryOp ekey evalue estore (ustoreUpdate l)
 compileExpr (UDelete l ekey estore) = binaryOp ekey estore (ustoreDelete l)
 
+compileExpr (Wrap l exFld) = unaryOp exFld $ L.wrapOne l
+compileExpr (Unwrap l exDt) = unaryOp exDt $ L.unwrapUnsafe_ l
+
 compileExpr (ObjMan fldAcc) = compileObjectManipulation fldAcc
 compileExpr (Construct fields) = IndigoState $ \md ->
   let cd = L.construct $ rmap (\e -> fieldCtor $ gcCode $ runIndigoState (compileExpr e) md) fields in
@@ -112,8 +116,8 @@
           castFieldConstructors @a $
             rmap (fieldCtor . gcCode . usingIndigoState md . compileExpr) fields
   in GenCode () (pushNoRefMd md) (L.construct @a fieldCtrs) L.drop
-compileExpr (Name _ e) = unaryOp e forcedCoerce_
-compileExpr (UnName _ e) = unaryOp e forcedCoerce_
+compileExpr (Name l e) = unaryOp e (toNamed l)
+compileExpr (UnName l e) = unaryOp e (fromNamed l)
 
 compileExpr (Slice ex1 ex2 ex3) = ternaryOp ex1 ex2 ex3 L.slice
 compileExpr (Cast ex) = unaryOp ex L.cast
@@ -262,30 +266,35 @@
 exprToManRes ex = OnStack $ compileExpr ex
 
 ternaryOp
-  :: forall n m l ex1 ex2 ex3 res inp. (AreExprs ex1 ex2 n m, IsExpr ex3 l, KnownValue res)
-  => ex1
-  -> ex2
-  -> ex3
-  -> n & m & l & inp :-> res & inp -> IndigoState inp (res & inp) ()
+  :: KnownValue res
+  => Expr n
+  -> Expr m
+  -> Expr l
+  -> n & m & l & inp :-> res & inp
+  -> IndigoState inp (res & inp) ()
 ternaryOp e1 e2 e3 opCode = IndigoState $ \md ->
-  let GenCode _ md3 cd3 _cl3  = runIndigoState (compileToExpr e3) md in
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileToExpr e2) md3 in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in
+  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
 
 binaryOp
-  :: forall n m ex1 ex2 res inp . (AreExprs ex1 ex2 n m, KnownValue res)
-  => ex1 -> ex2 -> n & m & inp :-> res & inp -> IndigoState inp (res & inp) ()
+  :: KnownValue res
+  => Expr n -> Expr m
+  -> n & m & inp :-> res & inp
+  -> IndigoState inp (res & inp) ()
 binaryOp e1 e2 opCode = IndigoState $ \md ->
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileToExpr e2) md in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in
+  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
 
 unaryOp
-  :: forall n ex res inp . (IsExpr ex n, KnownValue res)
-  => ex -> n & inp :-> res & inp -> IndigoState inp (res & inp) ()
+  :: KnownValue res
+  => Expr n
+  -> n & inp :-> res & inp
+  -> IndigoState inp (res & inp) ()
 unaryOp e opCode = IndigoState $ \md ->
-  let cd = gcCode $ runIndigoState (compileToExpr e) md in
+  let cd = gcCode $ runIndigoState (compileExpr e) md in
   GenCode () (pushNoRefMd md) (cd # opCode) L.drop
 
 nullaryOp :: KnownValue res => inp :-> res ': inp -> IndigoState inp (res ': inp) ()
@@ -293,34 +302,33 @@
   GenCode () (pushNoRefMd md) lorentzInstr L.drop
 
 ternaryOpFlat
-  :: forall n m l ex1 ex2 ex3 inp. (AreExprs ex1 ex2 n m, IsExpr ex3 l)
-  => ex1
-  -> ex2
-  -> ex3
-  -> n & m & l & inp :-> inp -> IndigoState inp inp ()
+  :: Expr n
+  -> Expr m
+  -> Expr l
+  -> n & m & l & inp :-> inp
+  -> IndigoState inp inp ()
 ternaryOpFlat e1 e2 e3 opCode = IndigoState $ \md ->
-  let GenCode _ md3 cd3 _cl3  = runIndigoState (compileToExpr e3) md in
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileToExpr e2) md3 in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in
+  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
 
 binaryOpFlat
-  :: forall n m ex1 ex2 inp . (AreExprs ex1 ex2 n m)
-  => ex1 -> ex2 -> n & m & inp :-> inp -> IndigoState inp inp ()
+  :: Expr n -> Expr m
+  -> n & m & inp :-> inp
+  -> IndigoState inp inp ()
 binaryOpFlat e1 e2 opCode = IndigoState $ \md ->
-  let GenCode _ md2 cd2 _cl2  = runIndigoState (compileToExpr e2) md in
-  let GenCode _ _md1 cd1 _cl1 = runIndigoState (compileToExpr e1) md2 in
+  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
 
 unaryOpFlat
-  :: forall n ex inp . (IsExpr ex n)
-  => ex -> n & inp :-> inp -> IndigoState inp inp ()
+  :: Expr n
+  -> n & inp :-> inp
+  -> IndigoState inp inp ()
 unaryOpFlat e opCode = IndigoState $ \md ->
-  let cd = gcCode $ runIndigoState (compileToExpr e) md in
+  let cd = gcCode $ runIndigoState (compileExpr e) md in
   GenCode () md (cd # opCode) L.nop
 
 nullaryOpFlat :: inp :-> inp -> IndigoState inp inp ()
 nullaryOpFlat lorentzInstr = IndigoState $ \md -> GenCode () md lorentzInstr L.nop
-
-compileToExpr :: ToExpr a => a -> IndigoState inp ((ExprType a) & inp) ()
-compileToExpr = compileExpr . toExpr
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
@@ -37,7 +37,7 @@
   , (==), (/=), (<), (>), (<=), (>=)
 
   -- * Conversion
-  , isNat, toInt, nonZero
+  , isNat, toInt, nonZero, coerce, forcedCoerce
 
   -- * Bits and boolean
   , lsl, lsr, and, or, xor, not
@@ -70,6 +70,9 @@
   , uGet, uUpdate, uInsert, uInsertNew, uDelete, uMem
   , (#@), (!@), (+@), (++@), (-@), (?@)
 
+  -- * Sum types
+  , wrap, unwrap
+
   -- * HasField
   , (!!), (#!)
 
@@ -107,11 +110,12 @@
 import Indigo.Internal.Expr.Types
 import Indigo.Internal.Field
 import Indigo.Internal.Object (Var)
-import Indigo.Lorentz
+import Indigo.Lorentz hiding (forcedCoerce)
 import Indigo.Prelude
 import qualified Michelson.Typed.Arith as M
 import Util.TypeTuple
 import Michelson.Text (unMText)
+import Michelson.Typed.Haskell.Instr.Sum (CtorOnlyField, InstrUnwrapC, InstrWrapOneC)
 import Michelson.Untyped.Entrypoints (unsafeBuildEpName)
 
 ----------------------------------------------------------------------------
@@ -126,7 +130,7 @@
 varExpr = V
 
 cast :: (ex :~> a) => ex -> Expr a
-cast = Cast
+cast = Cast . toExpr
 
 ----------------------------------------------------------------------------
 -- Math
@@ -137,52 +141,52 @@
   :: IsArithExpr exN exM M.Add n m
   => exN -> exM
   -> Expr (ArithResHs M.Add n m)
-add = Add
-(+) = Add
+add n m = Add (toExpr n) (toExpr m)
+(+) = add
 
 infixl 6 -
 sub, (-)
   :: IsArithExpr exN exM M.Sub n m
   => exN -> exM
   -> Expr (ArithResHs M.Sub n m)
-sub = Sub
-(-) = Sub
+sub n m = Sub (toExpr n) (toExpr m)
+(-) = sub
 
 infixl 7 *
 mul, (*)
   :: IsArithExpr exN exM M.Mul n m
   => exN -> exM
   -> Expr (ArithResHs M.Mul n m)
-mul = Mul
-(*) = Mul
+mul n m = Mul (toExpr n) (toExpr m)
+(*) = mul
 
 infixl 7 /
 div, (/)
   :: IsDivExpr exN exM n m
   => exN -> exM
   -> Expr (EDivOpResHs n m)
-div = Div
-(/) = Div
+div n m = Div (toExpr n) (toExpr m)
+(/) = div
 
 infixl 7 %
 mod, (%)
   :: IsModExpr exN exM n m
   => exN -> exM
   -> Expr (EModOpResHs n m)
-mod = Mod
-(%) = Mod
+mod n m = Mod (toExpr n) (toExpr m)
+(%) = mod
 
 abs
   :: IsUnaryArithExpr exN M.Abs n
   => exN
   -> Expr (UnaryArithResHs M.Abs n)
-abs = Abs
+abs = Abs . toExpr
 
 neg
   :: IsUnaryArithExpr exN M.Neg n
   => exN
   -> Expr (UnaryArithResHs M.Neg n)
-neg = Neg
+neg = Neg . toExpr
 
 ----------------------------------------------------------------------------
 -- Comparison
@@ -190,65 +194,77 @@
 
 infix 4 ==
 eq, (==)
-  :: (NiceComparable n, AreExprs c c1 n n)
+  :: (NiceComparable n, c :~> n, c1 :~> n)
   => c -> c1
   -> Expr Bool
-eq = Eq'
-(==) = Eq'
+eq a b = Eq' (toExpr a) (toExpr b)
+(==) = eq
 
 infix 4 /=
 neq, (/=)
-  :: (NiceComparable n, AreExprs c c1 n n)
+  :: (NiceComparable n, c :~> n, c1 :~> n)
   => c -> c1
   -> Expr Bool
-neq = Neq
-(/=) = Neq
+neq a b = Neq (toExpr a) (toExpr b)
+(/=) = neq
 
 infix 4 <
 lt, (<)
-  :: (NiceComparable n, AreExprs c c1 n n)
+  :: (NiceComparable n, c :~> n, c1 :~> n)
   => c -> c1
   -> Expr Bool
-lt = Lt
-(<) = Lt
+lt a b = Lt (toExpr a) (toExpr b)
+(<) = lt
 
 infix 4 >
 gt, (>)
-  :: (NiceComparable n, AreExprs c c1 n n)
+  :: (NiceComparable n, c :~> n, c1 :~> n)
   => c -> c1
   -> Expr Bool
-gt = Gt
-(>) = Gt
+gt a b = Gt (toExpr a) (toExpr b)
+(>) = gt
 
 infix 4 <=
 le, (<=)
-  :: (NiceComparable n, AreExprs c c1 n n)
+  :: (NiceComparable n, c :~> n, c1 :~> n)
   => c -> c1
   -> Expr Bool
-le = Le
-(<=) = Le
+le a b = Le (toExpr a) (toExpr b)
+(<=) = le
 
 infix 4 >=
 ge, (>=)
-  :: (NiceComparable n, AreExprs c c1 n n)
+  :: (NiceComparable n, c :~> n, c1 :~> n)
   => c -> c1
   -> Expr Bool
-ge = Ge
-(>=) = Ge
+ge a b = Ge (toExpr a) (toExpr b)
+(>=) = ge
 
 ----------------------------------------------------------------------------
 -- Conversion
 ----------------------------------------------------------------------------
 
 isNat :: (ex :~> Integer) => ex -> Expr (Maybe Natural)
-isNat = IsNat
+isNat = IsNat . toExpr
 
 toInt :: (ex :~> Natural) => ex -> Expr Integer
-toInt = Int'
+toInt = Int' . toExpr
 
 nonZero :: (ex :~> n, NonZero n, KnownValue (Maybe n)) => ex -> Expr (Maybe n)
-nonZero = NonZero
+nonZero = NonZero . toExpr
 
+-- | Convert between types that have the same Michelson representation and an
+-- explicit permission for that in the face of 'CanCastTo' constraint.
+coerce :: forall b a ex. (Castable_ a b, KnownValue b, ex :~> a) => ex -> Expr b
+coerce = Coerce . toExpr
+
+-- | Convert between expressions of types that have the same Michelson
+-- representation.
+forcedCoerce
+  :: forall b a ex. (MichelsonCoercible a b, KnownValue b, ex :~> a)
+  => ex -> Expr b
+forcedCoerce = ForcedCoerce . toExpr
+
 ----------------------------------------------------------------------------
 -- Bits and boolean
 ----------------------------------------------------------------------------
@@ -258,78 +274,78 @@
   :: IsArithExpr exN exM M.Lsl n m
   => exN -> exM
   -> Expr (ArithResHs M.Lsl n m)
-lsl = Lsl
-(<<<) = Lsl
+lsl a b = Lsl (toExpr a) (toExpr b)
+(<<<) = lsl
 
 infixl 8 >>>
 lsr, (>>>)
   :: IsArithExpr exN exM M.Lsr n m
   => exN -> exM
   -> Expr (ArithResHs M.Lsr n m)
-lsr = Lsr
-(>>>) = Lsr
+lsr a b = Lsr (toExpr a) (toExpr b)
+(>>>) = lsr
 
 infixr 2 ||
 or, (||)
   :: IsArithExpr exN exM M.Or n m
   => exN -> exM
   -> Expr (ArithResHs M.Or n m)
-or = Or
-(||) = Or
+or a b = Or (toExpr a) (toExpr b)
+(||) = or
 
 infixr 3 &&
 and, (&&)
   :: IsArithExpr exN exM M.And n m
   => exN -> exM
   -> Expr (ArithResHs M.And n m)
-and = And
-(&&) = And
+and a b = And (toExpr a) (toExpr b)
+(&&) = and
 
 infixr 2 ^
 xor, (^)
   :: IsArithExpr exN exM M.Xor n m
   => exN -> exM
   -> Expr (ArithResHs M.Xor n m)
-xor = Xor
-(^) = Xor
+xor a b = Xor (toExpr a) (toExpr b)
+(^) = xor
 
 not
   :: IsUnaryArithExpr exN M.Not n
   => exN
   -> Expr (UnaryArithResHs M.Not n)
-not = Not
+not = Not . toExpr
 
 ----------------------------------------------------------------------------
 -- Serialization
 ----------------------------------------------------------------------------
 
-pack :: (IsExpr ex a, NicePackedValue a) => ex -> Expr ByteString
-pack = Pack
+pack :: (ex :~> a, NicePackedValue a) => ex -> Expr ByteString
+pack = Pack . toExpr
 
 unpack :: (NiceUnpackedValue a, exb :~> ByteString) => exb -> Expr (Maybe a)
-unpack = Unpack
+unpack = Unpack . toExpr
 
 ----------------------------------------------------------------------------
 -- Pairs
 ----------------------------------------------------------------------------
 
-pair :: (AreExprs ex1 ex2 n m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m)
-pair = Pair
+pair :: (ex1 :~> n, ex2 :~> m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m)
+pair a b = Pair (toExpr a) (toExpr b)
 
 car, fst :: (op :~> (n, m), KnownValue n) => op -> Expr n
-car = Fst
-fst = Fst
+car = fst
+fst = Fst . toExpr
 
 cdr, snd :: (op :~> (n, m), KnownValue m) => op -> Expr m
-cdr = Snd
-snd = Snd
+cdr = snd
+snd = Snd . toExpr
 
 ----------------------------------------------------------------------------
 -- Maybe
 ----------------------------------------------------------------------------
 
 some :: (ex :~> t, KnownValue (Maybe t)) => ex -> Expr (Maybe t)
-some = Some
+some = Some . toExpr
 
 none :: KnownValue t => Expr (Maybe t)
 none = None
@@ -339,10 +355,10 @@
 ----------------------------------------------------------------------------
 
 right :: (ex :~> x, KnownValue y, KnownValue (Either y x)) => ex -> Expr (Either y x)
-right = Right'
+right = Right' . toExpr
 
 left :: (ex :~> y, KnownValue x, KnownValue (Either y x)) => ex -> Expr (Either y x)
-left = Left'
+left = Left' . toExpr
 
 ----------------------------------------------------------------------------
 -- Bytes and string
@@ -355,15 +371,15 @@
      )
   => (an, bn) -> ex
   -> Expr (Maybe c)
-slice (a, b) = Slice a b
+slice (a, b) ex = Slice (toExpr a) (toExpr b) (toExpr ex)
 
 infixr 6 <>
 concat, (<>)
   :: IsConcatExpr exN1 exN2 n
   => exN1 -> exN2
   -> Expr n
-concat = Concat
-(<>) = Concat
+concat a b = Concat (toExpr a) (toExpr b)
+(<>) = concat
 
 ----------------------------------------------------------------------------
 -- List
@@ -371,11 +387,11 @@
 
 infixr 5 .:
 cons, (.:) :: (ex1 :~> a, ex2 :~> List a) => ex1 -> ex2 -> Expr (List a)
-cons = Cons
-(.:) = Cons
+cons el lst = Cons (toExpr el) (toExpr lst)
+(.:) = cons
 
 concatAll :: IsConcatListExpr exN n => exN -> Expr n
-concatAll = Concat'
+concatAll = Concat' . toExpr
 
 nil :: KnownValue a => Expr (List a)
 nil = Nil
@@ -409,14 +425,14 @@
 
 instance (NiceComparable k, exKey :~> k, exValue :~> v)
     => ExprInsertable (BigMap k v) (exKey, exValue) where
-  insert (k, v) c = Update c k (some v)
+  insert (k, v) c = update (k, some v) c
 
 instance (NiceComparable k, exKey :~> k, exValue :~> v)
     => ExprInsertable (Map k v) (exKey, exValue) where
-  insert (k, v) c = Update c k (some v)
+  insert (k, v) c = update (k, some v) c
 
 instance (NiceComparable a, exKey :~> a) => ExprInsertable (Set a) exKey where
-  insert k c = Update c k True
+  insert k c = update (k, True) c
 
 -- | Expression class to remove an element from a data structure.
 --
@@ -429,36 +445,36 @@
     => exKey -> exStruct -> Expr c
 
 instance (NiceComparable k, KnownValue v) => ExprRemovable (BigMap k v) where
-  remove k c = Update c k none
+  remove k c = update (k, none) c
 
 instance (NiceComparable k, KnownValue v) => ExprRemovable (Map k v) where
-  remove k c = Update c k none
+  remove k c = update (k, none) c
 
 instance NiceComparable a => ExprRemovable (Set a) where
-  remove k c = Update c k False
+  remove k c = update (k, False) c
 
 get
   :: IsGetExpr exKey exMap map
   => exKey -> exMap
   -> Expr (Maybe (GetOpValHs map))
-get = Get
+get k m = Get (toExpr k) (toExpr m)
 
 update
   :: IsUpdExpr exKey exVal exMap map
   => (exKey, exVal) -> exMap
   -> Expr map
-update (k, v) s = Update s k v
+update (k, v) s = Update (toExpr s) (toExpr k) (toExpr v)
 
 mem
   :: IsMemExpr exKey exN n
   => exKey -> exN
   -> Expr Bool
-mem = Mem
+mem key n = Mem (toExpr key) (toExpr n)
 
 size
   :: IsSizeExpr exN n
   => exN -> Expr Natural
-size = Size
+size = Size . toExpr
 
 infixl 8 #:
 (#:)
@@ -527,7 +543,7 @@
      )
   => exStore -> (Label name, exKey)
   -> Expr (Maybe value)
-uGet store (uName, key) = UGet uName key store
+uGet store (uName, key) = UGet uName (toExpr key) (toExpr store)
 (#@) = uGet
 
 infixl 8 !@
@@ -539,7 +555,8 @@
      )
   => exStore -> (Label name, exKey, exVal)
   -> Expr (UStore store)
-uUpdate store (uName, key, val) = UUpdate uName key val store
+uUpdate store (uName, key, val) =
+  UUpdate uName (toExpr key) (toExpr val) (toExpr store)
 (!@) = uUpdate
 
 infixr 8 +@
@@ -551,7 +568,8 @@
      )
   => exStore -> (Label name, exKey, exVal)
   -> Expr (UStore store)
-uInsert store (uName, key, val) = UInsert uName key val store
+uInsert store (uName, key, val) =
+  UInsert uName (toExpr key) (toExpr val) (toExpr store)
 (+@) = uInsert
 
 infixr 8 ++@
@@ -565,7 +583,8 @@
   => exStore
   -> (Label name, err, exKey, exVal)
   -> Expr (UStore store)
-uInsertNew store (uName, err, key, val) = UInsertNew uName err key val store
+uInsertNew store (uName, err, key, val) =
+  UInsertNew uName err (toExpr key) (toExpr val) (toExpr store)
 (++@) = uInsertNew
 
 infixl 8 -@
@@ -576,7 +595,7 @@
      )
   => exStore -> (Label name, exKey)
   -> Expr (UStore store)
-uDelete store (uName, key) = UDelete uName key store
+uDelete store (uName, key) = UDelete uName (toExpr key) (toExpr store)
 (-@) = uDelete
 
 infixl 8 ?@
@@ -587,10 +606,34 @@
      )
   => exStore -> (Label name, exKey)
   -> Expr Bool
-uMem store (uName, key) = UMem uName key store
+uMem store (uName, key) = UMem uName (toExpr key) (toExpr store)
 (?@) = uMem
 
 ----------------------------------------------------------------------------
+-- Sum types
+----------------------------------------------------------------------------
+
+wrap
+  :: ( InstrWrapOneC dt name
+     , exField :~> CtorOnlyField name dt
+     , KnownValue dt
+     )
+  => Label name
+  -> exField
+  -> Expr dt
+wrap l = Wrap l . toExpr
+
+unwrap
+  :: ( InstrUnwrapC dt name
+     , exDt :~> dt
+     , KnownValue (CtorOnlyField name dt)
+     )
+  => Label name
+  -> exDt
+  -> Expr (CtorOnlyField name dt)
+unwrap l = Unwrap l . toExpr
+
+----------------------------------------------------------------------------
 -- HasField
 ----------------------------------------------------------------------------
 
@@ -620,10 +663,10 @@
 ----------------------------------------------------------------------------
 
 name :: (ex :~> t, KnownValue (name :! t)) => Label name -> ex -> Expr (name :! t)
-name = Name
+name lName = Name lName . toExpr
 
 unName :: (ex :~> (name :! t), KnownValue t) => Label name -> ex -> Expr t
-unName = UnName
+unName lName = UnName lName . toExpr
 
 infixl 8 !~
 (!~)
@@ -639,6 +682,7 @@
   -> Expr t
 (#~) = flip unName
 
+-- TODO: we should try to make this have a set of 'IsExpr' as input instead of 'Expr'
 construct
   :: ( InstrConstructC dt, KnownValue dt
      , RMap (ConstructorFieldTypes dt)
@@ -669,7 +713,7 @@
      , exAddr :~> addr
      )
   => exAddr -> Expr (Maybe (ContractRef p))
-contract = Contract
+contract = Contract . toExpr
 
 self
   :: ( NiceParameterFull p
@@ -679,14 +723,14 @@
 self = Self
 
 contractAddress :: (exc :~> ContractRef p) => exc -> Expr Address
-contractAddress = ContractAddress
+contractAddress = ContractAddress . toExpr
 
 contractCallingUnsafe
   :: ( NiceParameter arg
      , exAddr :~> Address
      )
   => EpName -> exAddr -> Expr (Maybe (ContractRef arg))
-contractCallingUnsafe = ContractCallingUnsafe
+contractCallingUnsafe epName = ContractCallingUnsafe epName . toExpr
 
 contractCallingString
   :: ( NiceParameter arg
@@ -703,20 +747,20 @@
      , conExpr :~> FutureContract p
      )
   => conExpr -> Expr (Maybe (ContractRef p))
-runFutureContract = RunFutureContract
+runFutureContract = RunFutureContract . toExpr
 
 implicitAccount
   :: (exkh :~> KeyHash)
   => exkh
   -> Expr (ContractRef ())
-implicitAccount = ImplicitAccount
+implicitAccount = ImplicitAccount . toExpr
 
 convertEpAddressToContract
   :: ( NiceParameter p
      , epExpr :~> EpAddress
      )
   => epExpr -> Expr (Maybe (ContractRef p))
-convertEpAddressToContract = ConvertEpAddressToContract
+convertEpAddressToContract = ConvertEpAddressToContract . toExpr
 
 makeView
   :: ( KnownValue (View a r)
@@ -724,7 +768,7 @@
      , exCRef :~> ContractRef r
      )
   => exa -> exCRef -> Expr (View a r)
-makeView = MakeView
+makeView a cRef = MakeView (toExpr a) (toExpr cRef)
 
 makeVoid
   :: ( KnownValue (Void_ a b)
@@ -732,7 +776,7 @@
      , exCRef :~> Lambda b b
      )
   => exa -> exCRef -> Expr (Void_ a b)
-makeVoid = MakeVoid
+makeVoid a cRef = MakeVoid (toExpr a) (toExpr cRef)
 
 ----------------------------------------------------------------------------
 -- Auxiliary
@@ -754,19 +798,19 @@
      )
   => pkExpr -> sigExpr -> hashExpr
   -> Expr Bool
-checkSignature = CheckSignature
+checkSignature pk sig hash = CheckSignature (toExpr pk) (toExpr sig) (toExpr hash)
 
 sha256 :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString
-sha256 = Sha256
+sha256 = Sha256 . toExpr
 
 sha512 :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString
-sha512 = Sha512
+sha512 = Sha512 . toExpr
 
 blake2b :: (hashExpr :~> ByteString) => hashExpr -> Expr ByteString
-blake2b = Blake2b
+blake2b = Blake2b . toExpr
 
 hashKey :: (keyExpr :~> PublicKey) => keyExpr -> Expr KeyHash
-hashKey = HashKey
+hashKey = HashKey . toExpr
 
 chainId :: Expr ChainId
 chainId = ChainId
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
@@ -10,7 +10,6 @@
 
   -- * Generalizations of Expr
   , IsExpr
-  , AreExprs
   , ToExpr
   , ExprType
   , (:~>)
@@ -45,6 +44,7 @@
 import Indigo.Internal.Object (Var, IndigoObjectF (..), FieldTypes, ComplexObjectC)
 import qualified Michelson.Typed.Arith as M
 import Michelson.Typed.Haskell.Instr.Product (GetFieldType)
+import Michelson.Typed.Haskell.Instr.Sum (CtorOnlyField, InstrUnwrapC, InstrWrapOneC)
 
 ----------------------------------------------------------------------------
 -- The Expr data type
@@ -57,168 +57,152 @@
 
   ObjMan :: ObjectManipulation a -> Expr a
 
-  Cast
-    :: (ex :~> a)
-    => ex -> Expr a
+  Cast :: KnownValue a => Expr a -> Expr a
 
-  Size :: (IsExpr exc c, SizeOpHs c)
-       => exc -> Expr Natural
+  Size :: SizeOpHs c => Expr c -> Expr Natural
 
   Update
-    :: ( UpdOpHs c
-       , IsExpr exKey (UpdOpKeyHs c)
-       , IsExpr exVal (UpdOpParamsHs c)
-       , IsExpr exStructure c
-       )
-    => exStructure -> exKey -> exVal -> Expr c
+    :: (UpdOpHs c, KnownValue c)
+    => Expr c -> Expr (UpdOpKeyHs c) -> Expr (UpdOpParamsHs c) -> Expr c
 
-  Add :: (AreExprs ex1 ex2 n m, ArithOpHs M.Add n m, KnownValue (ArithResHs M.Add n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.Add n m)
+  Add
+    :: (ArithOpHs M.Add n m, KnownValue (ArithResHs M.Add n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Add n m)
 
-  Sub :: (AreExprs ex1 ex2 n m, ArithOpHs M.Sub n m, KnownValue (ArithResHs M.Sub n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.Sub n m)
+  Sub
+    :: (ArithOpHs M.Sub n m, KnownValue (ArithResHs M.Sub n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Sub n m)
 
-  Mul :: (AreExprs ex1 ex2 n m, ArithOpHs M.Mul n m, KnownValue (ArithResHs M.Mul n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.Mul n m)
+  Mul
+    :: (ArithOpHs M.Mul n m, KnownValue (ArithResHs M.Mul n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Mul n m)
 
-  Div :: (AreExprs ex1 ex2 n m, EDivOpHs n m, KnownValue (EDivOpResHs n m))
-      => ex1 -> ex2 -> Expr (EDivOpResHs n m)
+  Div
+    :: (EDivOpHs n m, KnownValue (EDivOpResHs n m))
+    => Expr n -> Expr m -> Expr (EDivOpResHs n m)
 
-  Mod :: (AreExprs ex1 ex2 n m, EDivOpHs n m, KnownValue (EModOpResHs n m))
-      => ex1 -> ex2 -> Expr (EModOpResHs n m)
+  Mod
+    :: (EDivOpHs n m, KnownValue (EModOpResHs n m))
+    => Expr n -> Expr m -> Expr (EModOpResHs n m)
 
-  Abs :: (IsExpr ex n, UnaryArithOpHs M.Abs n, KnownValue (UnaryArithResHs M.Abs n))
-      => ex -> Expr (UnaryArithResHs M.Abs n)
+  Abs
+    :: (UnaryArithOpHs M.Abs n, KnownValue (UnaryArithResHs M.Abs n))
+    => Expr n -> Expr (UnaryArithResHs M.Abs n)
 
-  Neg :: (IsExpr ex n, UnaryArithOpHs M.Neg n, KnownValue (UnaryArithResHs M.Neg n))
-      => ex -> Expr (UnaryArithResHs M.Neg n)
+  Neg
+    :: (UnaryArithOpHs M.Neg n, KnownValue (UnaryArithResHs M.Neg n))
+    => Expr n -> Expr (UnaryArithResHs M.Neg n)
 
 
-  Lsl :: (AreExprs ex1 ex2 n m, ArithOpHs M.Lsl n m, KnownValue (ArithResHs M.Lsl n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.Lsl n m)
+  Lsl
+    :: (ArithOpHs M.Lsl n m, KnownValue (ArithResHs M.Lsl n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Lsl n m)
 
-  Lsr :: (AreExprs ex1 ex2 n m, ArithOpHs M.Lsr n m, KnownValue (ArithResHs M.Lsr n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.Lsr n m)
+  Lsr
+    :: (ArithOpHs M.Lsr n m, KnownValue (ArithResHs M.Lsr n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Lsr n m)
 
 
-  Eq' :: ( AreExprs ex1 ex2 n n
-         , NiceComparable n
-         )
-      => ex1 -> ex2 -> Expr Bool
+  Eq' :: NiceComparable n => Expr n -> Expr n -> Expr Bool
 
-  Neq :: ( AreExprs ex1 ex2 n n
-         , NiceComparable n
-         )
-      => ex1 -> ex2 -> Expr Bool
+  Neq :: NiceComparable n => Expr n -> Expr n -> Expr Bool
 
-  Le :: ( AreExprs ex1 ex2 n n
-        , NiceComparable n
-        )
-     => ex1 -> ex2 -> Expr Bool
+  Le :: NiceComparable n => Expr n -> Expr n -> Expr Bool
 
-  Lt :: ( AreExprs ex1 ex2 n n
-        , NiceComparable n
-        )
-     => ex1 -> ex2 -> Expr Bool
+  Lt :: NiceComparable n => Expr n -> Expr n -> Expr Bool
 
-  Ge :: ( AreExprs ex1 ex2 n n
-        , NiceComparable n
-        )
-     => ex1 -> ex2 -> Expr Bool
+  Ge :: NiceComparable n => Expr n -> Expr n -> Expr Bool
 
-  Gt :: ( AreExprs ex1 ex2 n n
-        , NiceComparable n
-        )
-     => ex1 -> ex2 -> Expr Bool
+  Gt :: NiceComparable n => Expr n -> Expr n -> Expr Bool
 
-  Or :: (AreExprs ex1 ex2 n m, ArithOpHs M.Or n m, KnownValue (ArithResHs M.Or n m))
-     => ex1 -> ex2 -> Expr (ArithResHs M.Or n m)
+  Or
+    :: (ArithOpHs M.Or n m, KnownValue (ArithResHs M.Or n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Or n m)
 
-  Xor :: (AreExprs ex1 ex2 n m, ArithOpHs M.Xor n m, KnownValue (ArithResHs M.Xor n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.Xor n m)
+  Xor
+    :: (ArithOpHs M.Xor n m, KnownValue (ArithResHs M.Xor n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.Xor n m)
 
-  And :: (AreExprs ex1 ex2 n m, ArithOpHs M.And n m, KnownValue (ArithResHs M.And n m))
-      => ex1 -> ex2 -> Expr (ArithResHs M.And n m)
+  And
+    :: (ArithOpHs M.And n m, KnownValue (ArithResHs M.And n m))
+    => Expr n -> Expr m -> Expr (ArithResHs M.And n m)
 
-  Not :: (IsExpr op n, UnaryArithOpHs M.Not n, KnownValue (UnaryArithResHs M.Not n))
-      => op -> Expr (UnaryArithResHs M.Not n)
+  Not
+    :: (UnaryArithOpHs M.Not n, KnownValue (UnaryArithResHs M.Not n))
+    => Expr n -> Expr (UnaryArithResHs M.Not n)
 
-  Int'
-    :: IsExpr ex Natural
-    => ex -> Expr Integer
+  Int' :: Expr Natural -> Expr Integer
 
-  IsNat
-    :: IsExpr ex Integer
-    => ex -> Expr (Maybe Natural)
+  IsNat :: Expr Integer -> Expr (Maybe Natural)
 
+  Coerce
+    :: (Castable_ a b, KnownValue b)
+    => Expr a -> Expr b
 
-  Fst :: (IsExpr op (n, m), KnownValue n) => op -> Expr n
-  Snd :: (IsExpr op (n, m), KnownValue m) => op -> Expr m
+  ForcedCoerce
+    :: (MichelsonCoercible a b, KnownValue b)
+    => Expr a -> Expr b
 
-  Pair :: (AreExprs ex1 ex2 n m, KnownValue (n, m)) => ex1 -> ex2 -> Expr (n, m)
+  Fst :: KnownValue n => Expr (n, m) -> Expr n
+  Snd :: KnownValue m => Expr (n, m) -> Expr m
 
-  Some :: (IsExpr ex t, KnownValue (Maybe t)) => ex -> Expr (Maybe t)
+  Pair :: KnownValue (n, m) => Expr n -> Expr m -> Expr (n, m)
+
+  Some :: KnownValue (Maybe t) => Expr t -> Expr (Maybe t)
   None :: KnownValue t => Expr (Maybe t)
 
-  Right' :: (IsExpr ex x, KnownValue y, KnownValue (Either y x)) => ex -> Expr (Either y x)
-  Left' :: (IsExpr ex y, KnownValue x, KnownValue (Either y x)) => ex -> Expr (Either y x)
+  Right' :: (KnownValue y, KnownValue (Either y x)) => Expr x -> Expr (Either y x)
+  Left' :: (KnownValue x, KnownValue (Either y x)) => Expr y -> Expr (Either y x)
 
-  Mem
-    :: ( MemOpHs c
-       , IsExpr exc c
-       , IsExpr exck (MemOpKeyHs c)
-       )
-    => exck -> exc -> Expr Bool
+  Mem :: MemOpHs c => Expr (MemOpKeyHs c) -> Expr c -> Expr Bool
 
   UGet
     :: ( HasUStore name key value store
-       , IsExpr exKey key
-       , IsExpr exStore (UStore store)
        , KnownValue value
        )
-    => Label name -> exKey -> exStore -> Expr (Maybe value)
+    => Label name -> Expr key -> Expr (UStore store) -> Expr (Maybe value)
 
   UInsertNew
     :: ( HasUStore name key value store
        , IsError err
-       , IsExpr exKey key
-       , IsExpr exVal value
-       , IsExpr exStore (UStore store)
+       , KnownValue (UStore store)
        )
     => Label name -> err
-    -> exKey -> exVal -> exStore -> Expr (UStore store)
+    -> Expr key -> Expr value -> Expr (UStore store) -> Expr (UStore store)
 
   UInsert
-    :: ( HasUStore name key value store
-       , IsExpr exKey key
-       , IsExpr exVal value
-       , IsExpr exStore (UStore store)
-       )
+    :: (HasUStore name key value store, KnownValue (UStore store))
     => Label name
-    -> exKey -> exVal -> exStore -> Expr (UStore store)
+    -> Expr key -> Expr value -> Expr (UStore store) -> Expr (UStore store)
 
   UMem
     :: ( HasUStore name key val store
-       , exKey :~> key
-       , exStore :~> UStore store
        , KnownValue val
        )
-    => Label name -> exKey -> exStore -> Expr Bool
+    => Label name -> Expr key -> Expr (UStore store) -> Expr Bool
 
   UUpdate
-    :: ( HasUStore name key val store
-       , exKey :~> key
-       , exVal :~> Maybe val
-       , exStore :~> UStore store
-       )
-    => Label name -> exKey -> exVal -> exStore -> Expr (UStore store)
+    :: (HasUStore name key val store, KnownValue (UStore store))
+    => Label name -> Expr key -> Expr (Maybe val) -> Expr (UStore store) -> Expr (UStore store)
 
   UDelete
-    :: ( HasUStore name key val store
-       , exKey :~> key
-       , exStore :~> UStore store
+    :: (HasUStore name key val store, KnownValue (UStore store))
+    => Label name -> Expr key -> Expr (UStore store) -> Expr (UStore store)
+
+  Wrap
+    :: ( InstrWrapOneC dt name
+       , KnownValue dt
        )
-    => Label name -> exKey -> exStore -> Expr (UStore store)
+    => Label name
+    -> Expr (CtorOnlyField name dt)
+    -> Expr dt
+  Unwrap
+    :: ( InstrUnwrapC dt name
+       , KnownValue (CtorOnlyField name dt)
+       )
+    => Label name
+    -> Expr dt
+    -> Expr (CtorOnlyField name dt)
 
   Construct
     :: ( InstrConstructC dt
@@ -233,11 +217,11 @@
     => Rec Expr (FieldTypes dt) -> Expr dt
 
   Name
-    :: (IsExpr ex t, KnownValue (name :! t))
-    => Label name -> ex -> Expr (name :! t)
+    :: KnownValue (name :! t)
+    => Label name -> Expr t -> Expr (name :! t)
   UnName
-    :: (IsExpr ex (name :! t), KnownValue t)
-    => Label name -> ex -> Expr t
+    :: KnownValue t
+    => Label name -> Expr (name :! t) -> Expr t
 
   EmptySet
     :: (NiceComparable key, KnownValue (Set key))
@@ -246,11 +230,9 @@
   Get
     :: ( GetOpHs c
        , KnownValue (Maybe (GetOpValHs c))
-       , IsExpr exKey (GetOpKeyHs c)
-       , IsExpr exMap c
        , KnownValue (GetOpValHs c)
        )
-    => exKey -> exMap -> Expr (Maybe (GetOpValHs c))
+    => Expr (GetOpKeyHs c) -> Expr c -> Expr (Maybe (GetOpValHs c))
 
   EmptyMap
     :: (KnownValue value, NiceComparable key, KnownValue (Map key value))
@@ -261,53 +243,36 @@
     => Expr (BigMap key value)
 
   Pack
-    :: (IsExpr ex a, NicePackedValue a)
-    => ex -> Expr ByteString
+    :: NicePackedValue a
+    => Expr a -> Expr ByteString
 
   Unpack
-    :: ( NiceUnpackedValue a
-       , IsExpr bsExpr ByteString
-       )
-    => bsExpr -> Expr (Maybe a)
+    :: NiceUnpackedValue a
+    => Expr ByteString -> Expr (Maybe a)
 
-  Cons
-    :: ( IsExpr ex1 a
-       , IsExpr ex2 (List a)
-       )
-    => ex1 -> ex2 -> Expr (List a)
+  Cons :: KnownValue (List a) => Expr a -> Expr (List a) -> Expr (List a)
 
   Nil :: KnownValue a => Expr (List a)
 
   Concat
-    :: ( IsExpr ex1 c
-       , IsExpr ex2 c
-       , ConcatOpHs c
-       )
-    => ex1 -> ex2 -> Expr c
+    :: (ConcatOpHs c, KnownValue c)
+    => Expr c -> Expr c -> Expr c
 
   Concat'
-    :: ( IsExpr ex (List c)
-       , ConcatOpHs c
-       , KnownValue c
-       )
-    => ex -> Expr c
+    :: (ConcatOpHs c, KnownValue c)
+    => Expr (List c) -> Expr c
 
   Slice
-    :: ( IsExpr ex c
-       , SliceOpHs c
-       , IsExpr an Natural
-       , IsExpr bn Natural
-       )
-    => an -> bn -> ex -> Expr (Maybe c)
+    :: (SliceOpHs c, KnownValue c)
+    => Expr Natural -> Expr Natural -> Expr c -> Expr (Maybe c)
 
   Contract
     :: ( NiceParameterFull p
        , NoExplicitDefaultEntrypoint p
        , ToTAddress p addr
        , ToT addr ~ ToT Address
-       , IsExpr exAddr addr
        )
-    => exAddr -> Expr (Maybe (ContractRef p))
+    => Expr addr -> Expr (Maybe (ContractRef p))
 
   Self
     :: ( NiceParameterFull p
@@ -316,56 +281,35 @@
     => Expr (ContractRef p)
 
   ContractAddress
-    :: IsExpr exc (ContractRef p)
-    => exc -> Expr Address
+    :: Expr (ContractRef p) -> Expr Address
 
   ContractCallingUnsafe
-    :: ( NiceParameter arg
-       , IsExpr exAddr Address
-       )
-    => EpName -> exAddr -> Expr (Maybe (ContractRef arg))
+    :: NiceParameter arg
+    => EpName -> Expr Address -> Expr (Maybe (ContractRef arg))
 
   RunFutureContract
-    :: ( NiceParameter p
-       , IsExpr conExpr (FutureContract p)
-       )
-    => conExpr -> Expr (Maybe (ContractRef p))
+    :: NiceParameter p
+    => Expr (FutureContract p) -> Expr (Maybe (ContractRef p))
 
-  ImplicitAccount
-    :: (IsExpr exkh KeyHash)
-    => exkh -> Expr (ContractRef ())
+  ImplicitAccount :: Expr KeyHash -> Expr (ContractRef ())
 
   ConvertEpAddressToContract
-    :: ( NiceParameter p
-       , IsExpr epExpr EpAddress
-       )
-    => epExpr -> Expr (Maybe (ContractRef p))
+    :: NiceParameter p => Expr EpAddress -> Expr (Maybe (ContractRef p))
 
   MakeView
-    :: ( KnownValue (View a r)
-       , exa :~> a
-       , exCRef :~> ContractRef r
-       )
-    => exa -> exCRef -> Expr (View a r)
+    :: KnownValue (View a r)
+    => Expr a -> Expr (ContractRef r) -> Expr (View a r)
 
   MakeVoid
-    :: ( KnownValue (Void_ a b)
-       , exa :~> a
-       , exCRef :~> Lambda b b
-       )
-    => exa -> exCRef -> Expr (Void_ a b)
+    :: KnownValue (Void_ a b)
+    => Expr a -> Expr (Lambda b b) -> Expr (Void_ a b)
 
-  CheckSignature
-    :: ( IsExpr pkExpr PublicKey
-       , IsExpr sigExpr Signature
-       , IsExpr hashExpr ByteString
-       )
-    => pkExpr -> sigExpr -> hashExpr -> Expr Bool
+  CheckSignature :: Expr PublicKey -> Expr Signature -> Expr ByteString -> Expr Bool
 
-  Sha256 :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString
-  Sha512 :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString
-  Blake2b :: (IsExpr hashExpr ByteString) => hashExpr -> Expr ByteString
-  HashKey :: (IsExpr keyExpr PublicKey) => keyExpr -> Expr KeyHash
+  Sha256 :: Expr ByteString -> Expr ByteString
+  Sha512 :: Expr ByteString -> Expr ByteString
+  Blake2b :: Expr ByteString -> Expr ByteString
+  HashKey :: Expr PublicKey -> Expr KeyHash
 
   ChainId :: Expr ChainId
 
@@ -375,14 +319,12 @@
   Sender :: Expr Address
 
   Exec
-    :: ( IsExpr exA a, IsExpr exLambda (Lambda a b)
-       , KnownValue b
-       )
-    => exA -> exLambda -> Expr b
+    :: KnownValue b
+    => Expr a -> Expr (Lambda a b) -> Expr b
 
   NonZero
-    :: (IsExpr ex n, NonZero n, KnownValue (Maybe n))
-    => ex -> Expr (Maybe n)
+    :: (NonZero n, KnownValue (Maybe n))
+    => Expr n -> Expr (Maybe n)
 
 ----------------------------------------------------------------------------
 -- Object manipulation
@@ -428,8 +370,6 @@
 type IsExpr op n = (ToExpr op, ExprType op ~ n, KnownValue n)
 type (:~>) op n = IsExpr op n
 
-type AreExprs ex1 ex2 n m = (IsExpr ex1 n, IsExpr ex2 m)
-
 type ExprType a = ExprType' (Decide a) a
 
 toExpr :: forall a . ToExpr a => a -> Expr (ExprType a)
@@ -478,19 +418,19 @@
   )
 
 type IsArithExpr exN exM a n m =
-  ( AreExprs exN exM n m
+  ( exN :~> n, exM :~> m
   , ArithOpHs a n m
   , KnownValue (ArithResHs a n m)
   )
 
 type IsDivExpr exN exM n m =
-  ( AreExprs exN exM n m
+  ( exN :~> n, exM :~> m
   , EDivOpHs n m
   , KnownValue (EDivOpResHs n m)
   )
 
 type IsModExpr exN exM n m =
-  ( AreExprs exN exM n m
+  ( exN :~> n, exM :~> m
   , EDivOpHs n m
   , KnownValue (EModOpResHs n m)
   )
diff --git a/src/Indigo/Lib.hs b/src/Indigo/Lib.hs
--- a/src/Indigo/Lib.hs
+++ b/src/Indigo/Lib.hs
@@ -81,7 +81,7 @@
 void_ f v = do
   doc (DThrows (Proxy @(VoidResult b)))
   r <- f (v #! #voidParam)
-  failWith $ pair voidResultTag (Exec 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/Lorentz.hs b/src/Indigo/Lorentz.hs
--- a/src/Indigo/Lorentz.hs
+++ b/src/Indigo/Lorentz.hs
@@ -38,5 +38,6 @@
 import Lorentz.StoreClass as L
 import Lorentz.UParam as L
 import Lorentz.UStore as L
+import Lorentz.Util.TH as L
 import Lorentz.Value as L
 import Lorentz.Zip as L ()
diff --git a/src/Indigo/Print.hs b/src/Indigo/Print.hs
--- a/src/Indigo/Print.hs
+++ b/src/Indigo/Print.hs
@@ -6,11 +6,16 @@
 
 module Indigo.Print
   ( printIndigoContract
+  , renderIndigoDoc
 
   , printAsMichelson
   , saveAsMichelson
+  , printDocumentation
+  , saveDocumentation
   ) where
 
+import Data.Text.Lazy.IO.Utf8 (writeFile)
+
 import Indigo.Compilation
 import Indigo.Internal.Object
 import Indigo.Lorentz
@@ -30,6 +35,17 @@
   defaultContract $
   compileIndigoContract @param @st ctr
 
+-- | Generate an Indigo contract documentation.
+renderIndigoDoc
+  :: forall param st .
+     ( IsObject st
+     , NiceParameterFull param
+     )
+  => IndigoContract param st
+  -> LText
+renderIndigoDoc ctr =
+  renderLorentzDocWithGitRev DGitRevisionUnknown $ compileIndigoContract @param @st ctr
+
 -- | Prints the pretty-printed Michelson code of an Indigo contract to
 -- the standard output.
 --
@@ -56,4 +72,27 @@
   -> FilePath
   -> m ()
 saveAsMichelson cntr filePath =
-  withFile filePath WriteMode (`hPutStrLn` (printIndigoContract @param @st False cntr))
+  writeFile filePath (printIndigoContract @param @st False cntr)
+
+-- | Print the generated documentation to the standard output.
+printDocumentation
+  :: forall param st m . ( IsObject st
+     , NiceParameterFull param
+     , MonadIO m
+     )
+  => IndigoContract param st
+  -> m ()
+printDocumentation ctr =
+  putStrLn $ renderIndigoDoc @param @st ctr
+
+-- | Save the generated documentation to the given file.
+saveDocumentation
+  :: forall param st m . ( IsObject st
+     , NiceParameterFull param
+     , MonadIO m, MonadMask m
+     )
+  => IndigoContract param st
+  -> FilePath
+  -> m ()
+saveDocumentation ctr filePath = do
+  writeFile filePath (renderIndigoDoc @param @st ctr)
diff --git a/test/Test/Code/Examples.hs b/test/Test/Code/Examples.hs
--- a/test/Test/Code/Examples.hs
+++ b/test/Test/Code/Examples.hs
@@ -98,12 +98,12 @@
   -- Create a variable to demostrate that branches of case
   -- are cleaned automatically
   testVar <- new$ True
-  storage =: Fst p - Snd p
+  storage =: fst p - snd p
   return testVar
 
 doAdd :: Var Integer -> Var (Integer, Integer) -> IndigoM Bool
 doAdd storage p = do
-  storage =: Fst p + Snd p
+  storage =: fst p + snd p
   return False
 
 contractDocLorentz :: ContractCode Integer Integer
diff --git a/test/Test/Code/Expr.hs b/test/Test/Code/Expr.hs
--- a/test/Test/Code/Expr.hs
+++ b/test/Test/Code/Expr.hs
@@ -7,6 +7,7 @@
 module Test.Code.Expr
   ( MyUStore
   , MyTemplate (..)
+  , MySum (..)
   , SignatureData (..)
   , sampleSignature
   , partialParse
@@ -43,6 +44,7 @@
   , exprCrypto
   , exprHashKey
   , exprNonZero
+  , exprWrap
   ) where
 
 import Fmt (Buildable, pretty)
@@ -61,6 +63,10 @@
 
 type MyUStore = UStore MyTemplate
 
+data MySum = MySumA Bool | MySumB Natural
+  deriving stock (Eq, Show, Generic)
+  deriving anyclass IsoValue
+
 ----------------------------------------------------------------------------
 -- Sample data
 ----------------------------------------------------------------------------
@@ -233,3 +239,7 @@
 exprNonZero = compileIndigo @2 $ \st param ->
   st =: nonZero param
 
+exprWrap :: '[Bool, MySum] :-> '[Bool, MySum]
+exprWrap = compileIndigo @2 $ \st param -> do
+  st =: wrap #cMySumA param
+  param =: unwrap #cMySumA st
diff --git a/test/Test/Expr.hs b/test/Test/Expr.hs
--- a/test/Test/Expr.hs
+++ b/test/Test/Expr.hs
@@ -46,6 +46,9 @@
 genMyUStore :: Gen MyUStore
 genMyUStore = mkUStore <$> genMyTemplate
 
+genMySum :: Gen MySum
+genMySum = Gen.choice [MySumA <$> Gen.bool, MySumB <$> Gen.integral (Range.linear 0 1000)]
+
 -- | Tests on single Indigo `Expr`s or simple combinations of them.
 -- Param and storage for these are generated randomly and their resulting stack
 -- is validated against an Haskell function.
@@ -118,6 +121,8 @@
   -- , Now
 
   , testIndigo "NonZero" genInteger genIntegerMaybe (validateStSuccess nonZeroCheck) exprNonZero
+
+  , testIndigo "Wrap" Gen.bool genMySum (validateStSuccess wrapCheck) exprWrap
   ]
 
   where
@@ -209,3 +214,6 @@
 nonZeroCheck param _st
   | param == 0 = Nothing
   | otherwise = Just param
+
+wrapCheck :: Bool -> MySum -> MySum
+wrapCheck param _st = MySumA param
diff --git a/test/Test/Util.hs b/test/Test/Util.hs
--- a/test/Test/Util.hs
+++ b/test/Test/Util.hs
@@ -27,6 +27,7 @@
   , noOptimizationContract
   ) where
 
+import qualified Data.Text.IO.Utf8 as Utf8 (readFile)
 import Fmt (pretty)
 import Hedgehog (Gen, MonadTest, PropertyT, annotate, forAll, property, (===))
 import Prelude
@@ -40,7 +41,6 @@
 import Lorentz.Test (ContractPropValidator, contractProp, dummyContractEnv, failedTest)
 import Michelson.Interpret (MichelsonFailed(..))
 import Michelson.Typed.Haskell.Value (IsoValuesStack)
-import Util.IO (readFileUtf8)
 
 type IndigoInstrValidator m pm st out =
   pm -> st -> Either MichelsonFailed (Rec Identity out) -> m ()
@@ -67,7 +67,7 @@
 testIndigoContract name genPm genSt propValidator iContract michelsonFile =
   testGroup ("Indigo contract: " <> name)
     [ testCase "matches Michelson reference contract" $ do
-        expectedContract <- readFileUtf8 michelsonFile
+        expectedContract <- Utf8.readFile michelsonFile
         printLorentzContract False iContractWithoutOptimization @?= fromStrict expectedContract
     , testProperty "has the correct resulting state and operations" $ property $ do
         pm <- forAll genPm