diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,12 @@
+1.9
+=====
+* [!653](https://gitlab.com/morley-framework/morley/-/merge_requests/653)
+  + `Michelson.OpSize` module is moved to `Michelson.Untyped.OpSize`.
+  + Added primitives for evaluating `OpSize` in typed Michelson.
+  + Added `instance Buildable OpSize`.
+* [!633](https://gitlab.com/morley-framework/morley/-/merge_requests/633)
+  Added `Tezos.Core.timestampToUTCTime`.
+
 1.8.1
 =====
 * [!613](https://gitlab.com/morley-framework/morley/-/merge_requests/613)
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -4,9 +4,9 @@
 
 Morley aims to make writing smart contracts in Michelson pleasant and effective.
 It contains 3 major things:
-1. An [executable](#morley-executable) that lets you perform various operations on Michelson smart contracts.
-2. A [library](#morley-library) with core Tezos and Michelson data types, and functions such as Michelson typechecker and interpreter.
-3. A superset of the Michelson language that we call the [Morley language](#morley-language).
+1. An [executable](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-executable) that lets you perform various operations on Michelson smart contracts.
+2. A [library](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-library) with core Tezos and Michelson data types, and functions such as Michelson typechecker and interpreter.
+3. A superset of the Michelson language that we call the [Morley language](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-language).
 It relaxes Michelson parser rules, adds some syntax sugar and simple features.
 
 ## Morley executable
@@ -15,7 +15,7 @@
 
 There are three ways to get Morley executable:
 - [Docker](https://docs.docker.com/) based (preferable).
-  * Get [script](/scripts/morley.sh)
+  * Get [script](https://gitlab.com/morley-framework/morley/-/blob/master/scripts/morley.sh)
  (e. g. using `curl https://gitlab.com/morley-framework/morley/raw/master/scripts/morley.sh > morley.sh`)
   and run it `./morley.sh <args>`. This script will pull a docker image that contains the latest version of Morley executable from the `production` branch and run it with the given arguments.
     You'll need `coreutils` to be installed in order to use `morley.sh`.
@@ -51,7 +51,7 @@
 - `analyze` a contract and print some statistics about it.
 - `print` a contract in vanilla Michelson format.
 It can be useful in some cases:
-  + You have a smart contract that uses [Morley extensions](#morley-language) and want to convert it to vanilla Michelson format that can be handled by Tezos reference implementation.
+  + You have a smart contract that uses [Morley extensions](https://gitlab.com/morley-framework/morley/-/tree/master/code/morley#morley-language) and want to convert it to vanilla Michelson format that can be handled by Tezos reference implementation.
   + You have a contract with inconsistent/ugly formatting and want to format it in uniform style.
   + You want to print a contract on a single line.
 - `parse` a contract and return its representation in Haskell types.
@@ -64,18 +64,18 @@
 Morley-the library is available on [Hackage](https://hackage.haskell.org/package/morley).
 It consists of the following parts:
 
-- [`Tezos.*`](src/Tezos/) hierarchy is designed to implement cryptographic primitives, string and byte formats, and any other functionality specific to the Tezos protocol which is required for testing/execution of Michelson contracts but is used not only by Michelson.
-- [`Michelson.Untyped`](src/Michelson/Untyped.hs) and [`Michelson.Typed`](src/Michelson/Typed.hs) hierarchies define Haskell data types that assemble a Michelson contract. See [michelsonTypes.md](./docs/michelsonTypes.md).
-- [`Michelson.TypeCheck`](src/Michelson/TypeCheck.hs): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](./docs/morleyTypechecker.md).
-- [`Michelson.Interpret`](src/Michelson/Interpret.hs): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](./docs/morleyInterpreter.md).
-- [`Michelson.Macro`](src/Michelson/Macro.hs) Types for macros, syntactic sugar, and other extensions that are described in the next chapter.
-- [`Michelson.Parser`](src/Michelson/Parser.hs) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT.
-- [`Michelson.Runtime`](src/Michelson/Runtime.hs): A high-level interface to Morley functionality, see [morleyRuntime.md](./docs/morleyRuntime.md).
+- The `Tezos.*` hierarchy ([`Tezos.Address`](http://hackage.haskell.org/package/morley/docs/Tezos-Address.html), [`Tezos.Core`](http://hackage.haskell.org/package/morley/docs/Tezos-Core.html), [`Tezos.Crypto`](http://hackage.haskell.org/package/morley/docs/Tezos-Crypto.html)) is designed to implement cryptographic primitives, string and byte formats, and any other functionality specific to the Tezos protocol which is required for testing/execution of Michelson contracts but is used not only by Michelson.
+- [`Michelson.Untyped`](http://hackage.haskell.org/package/morley/docs/Michelson-Untyped.html) and [`Michelson.Typed`](http://hackage.haskell.org/package/morley/docs/Michelson-Typed.html) hierarchies define Haskell data types that assemble a Michelson contract. See [michelsonTypes.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/michelsonTypes.md).
+- [`Michelson.TypeCheck`](http://hackage.haskell.org/package/morley/docs/Michelson-TypeCheck.html): A typechecker that validates Michelson contracts according to the Michelson's typing rules. Essentially, it performs conversion from untyped representation to the typed one. See [morleyTypechecker.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyTypechecker.md).
+- [`Michelson.Interpret`](http://hackage.haskell.org/package/morley/docs/Michelson-Interpret.html): An interpreter for Michelson contracts which doesn't perform any side effects. See [morleyInterpreter.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyInterpreter.md).
+- [`Michelson.Macro`](http://hackage.haskell.org/package/morley/docs/Michelson-Macro.html) Types for macros, syntactic sugar, and other extensions that are described in the next chapter.
+- [`Michelson.Parser`](http://hackage.haskell.org/package/morley/docs/Michelson-Parser.html) A parser to turn a `.tz` or `.mtz` file (`.mtz` is a Michelson contract with Morley extensions) into a Haskell ADT.
+- [`Michelson.Runtime`](http://hackage.haskell.org/package/morley/docs/Michelson-Runtime.html): A high-level interface to Morley functionality, see [morleyRuntime.md](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/morleyRuntime.md).
 
 ## Morley language
 
 Morley-the-language is a superset of the Michelson language, which means that each Michelson contract is also a valid Morley contract but not vice versa.
 There are several extensions which make it more convenient to write Michelson contracts and test them.
 For example, one can write inline assertions in their contracts for testing.
-All the details can be found in [the document](./docs/language/morleyLanguage.md) about these extensions.
+All the details can be found in [the document](https://gitlab.com/morley-framework/morley/-/blob/master/code/morley/docs/language/morleyLanguage.md) about these extensions.
 A smart contract written in the Morley language can be transpiled to Michelson using the aforementioned `morley print` command.
diff --git a/morley.cabal b/morley.cabal
--- a/morley.cabal
+++ b/morley.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           morley
-version:        1.8.1
+version:        1.9
 synopsis:       Developer tools for the Michelson Language
 description:    A library to make writing smart contracts in Michelson — the smart contract language of the Tezos blockchain — pleasant and effective.
 category:       Language
@@ -44,9 +44,9 @@
       Michelson.Interpret
       Michelson.Interpret.Pack
       Michelson.Interpret.Unpack
+      Michelson.Interpret.Utils
       Michelson.Let
       Michelson.Macro
-      Michelson.OpSize
       Michelson.Optimizer
       Michelson.Parser
       Michelson.Parser.Annotations
@@ -95,6 +95,7 @@
       Michelson.Typed.Haskell.ValidateDescription
       Michelson.Typed.Haskell.Value
       Michelson.Typed.Instr
+      Michelson.Typed.OpSize
       Michelson.Typed.Origination
       Michelson.Typed.Polymorphic
       Michelson.Typed.Scope
@@ -109,6 +110,7 @@
       Michelson.Untyped.Entrypoints
       Michelson.Untyped.Ext
       Michelson.Untyped.Instr
+      Michelson.Untyped.OpSize
       Michelson.Untyped.Type
       Michelson.Untyped.Value
       Morley.CLI
diff --git a/src/Michelson/Interpret.hs b/src/Michelson/Interpret.hs
--- a/src/Michelson/Interpret.hs
+++ b/src/Michelson/Interpret.hs
@@ -87,8 +87,8 @@
   -- contracts have unique addresses.
   }
 
--- | Represents `[FAILED]` state of a Michelson program. Contains
--- value that was on top of the stack when `FAILWITH` was called.
+-- | Represents @[FAILED]@ state of a Michelson program. Contains
+-- value that was on top of the stack when @FAILWITH@ was called.
 data MichelsonFailed where
   MichelsonFailedWith :: (KnownT t) => T.Value t -> MichelsonFailed
   MichelsonArithError
diff --git a/src/Michelson/Interpret/Pack.hs b/src/Michelson/Interpret/Pack.hs
--- a/src/Michelson/Interpret/Pack.hs
+++ b/src/Michelson/Interpret/Pack.hs
@@ -23,14 +23,13 @@
 
 import Prelude hiding (EQ, GT, LT)
 
-import Control.Exception (assert)
 import qualified Data.Binary.Put as Bi
-import qualified Data.Bits as Bits
 import qualified Data.ByteArray as ByteArray
 import qualified Data.ByteString.Lazy as LBS
 import qualified Data.Map as Map
 import Data.Singletons (Sing, demote)
 
+import Michelson.Interpret.Utils
 import Michelson.Text
 import Michelson.Typed
 import Michelson.Untyped.Annotation
@@ -162,31 +161,7 @@
 
 -- | Encode contents of a given number.
 encodeIntPayload :: Integer -> LByteString
-encodeIntPayload = LBS.pack . toList . doEncode True
-  where
-    {- Numbers are represented as follows:
-
-    byte 0:         1              _         ______   ||  lowest digits
-            has continuation  is negative   payload   ||
-                                                      ||
-    byte 1:         1                       _______   ||
-    ...             1                       _______   ||
-    byte n:         0                       _______   ||
-            has continuation                payload   \/  highest digits
-    -}
-    doEncode :: Bool -> Integer -> NonEmpty Word8
-    doEncode isFirst a
-      | a >= byteWeight =
-          let (hi, lo) = a `divMod` byteWeight
-              byte = Bits.setBit (fromIntegral @_ @Word8 lo) 7
-          in byte :| toList (doEncode False hi)
-      | a >= 0 =
-          one (fromIntegral @_ @Word8 a)
-      | otherwise = assert isFirst $
-          let h :| t = doEncode True (-a)
-          in Bits.setBit h 6 :| t
-      where
-        byteWeight = if isFirst then 64 else 128
+encodeIntPayload = LBS.pack . toList . encodeZarithNumber
 
 -- | Encode an int-like value.
 encodeNumeric :: Integral i => i -> LByteString
diff --git a/src/Michelson/Interpret/Utils.hs b/src/Michelson/Interpret/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/Michelson/Interpret/Utils.hs
@@ -0,0 +1,43 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | General utilities used by interpreter.
+--
+-- This is not supposed to import any Michelson modules.
+module Michelson.Interpret.Utils
+  ( encodeZarithNumber
+  ) where
+
+import Control.Exception (assert)
+import qualified Data.Bits as Bits
+
+-- | Encode a number as tezos does this.
+--
+-- In the Tezos reference implementation this encoding is called @zarith@.
+encodeZarithNumber :: Integer -> NonEmpty Word8
+encodeZarithNumber = doEncode True
+  where
+    {- Numbers, when packed by tezos, are represented as follows:
+
+    byte 0:         1              _         ______   ||  lowest digits
+            has continuation  is negative   payload   ||
+                                                      ||
+    byte 1:         1                       _______   ||
+    ...             1                       _______   ||
+    byte n:         0                       _______   ||
+            has continuation                payload   \/  highest digits
+    -}
+    doEncode :: Bool -> Integer -> NonEmpty Word8
+    doEncode isFirst a
+      | a >= byteWeight =
+          let (hi, lo) = a `divMod` byteWeight
+              byte = Bits.setBit (fromIntegral @_ @Word8 lo) 7
+          in byte :| toList (doEncode False hi)
+      | a >= 0 =
+          one (fromIntegral @_ @Word8 a)
+      | otherwise = assert isFirst $
+          let h :| t = doEncode True (-a)
+          in Bits.setBit h 6 :| t
+      where
+        byteWeight = if isFirst then 64 else 128
diff --git a/src/Michelson/OpSize.hs b/src/Michelson/OpSize.hs
deleted file mode 100644
--- a/src/Michelson/OpSize.hs
+++ /dev/null
@@ -1,248 +0,0 @@
--- SPDX-FileCopyrightText: 2020 Tocqueville Group
---
--- SPDX-License-Identifier: LicenseRef-MIT-TQ
-
--- | Measuring operation size.
---
--- When originating a contract or making a transfer, tezos node forms operation
--- which is submitted over network. Size of this operation depends on content
--- of originated contract or transfer parameter resp., and tezos has a hard
--- limit on operation size thus it has to be accounted.
---
--- Functions declared in this module allow assessing size of origination or
--- transfer operation with up to constant precision because it yet accounts only
--- for Michelson primitives participating in the operation.
--- Other stuff which affects op size include parameters which user passes to
--- origination or transfer themselves, for instance, amount of mutez carried
--- to the contract. ATM we don't have necessary primitives in Haskell to be
--- able to handle those parameters here, probably waiting for [TM-89].
--- Currently, we can assess overall transfer size only approximatelly, like
--- in 'smallTransferOpSize'.
-module Michelson.OpSize
-  ( OpSize (..)
-  , opSizeHardLimit
-  , smallTransferOpSize
-  , instrOpSize
-  , expandedInstrsOpSize
-  , valueOpSize
-  ) where
-
-import Prelude hiding (Ordering(..))
-
-import Michelson.Interpret.Pack
-import Michelson.Untyped
-
--- | Operation size in bytes.
---
--- We use newtype wrapper because there are different units of measure
--- (another one is gas, and we don't want to confuse them).
-newtype OpSize = OpSize { unOpSize :: Word }
-  deriving stock (Show, Eq, Ord)
-
-instance Semigroup OpSize where
-  OpSize a <> OpSize b = OpSize (a + b)
-instance Monoid OpSize where
-  mempty = OpSize 0
-
--- | Maximal operation size allowed by Tezos production nodes.
-opSizeHardLimit :: OpSize
-opSizeHardLimit = OpSize 16384
-
--- | Base cost of any transfer of 0 mutez with no extra parameters.
--- (Add 'valueOpSize <param>' to it to get assessment of actual transfer op size)
-smallTransferOpSize :: OpSize
-smallTransferOpSize = OpSize 162
-
-instrOpSize :: InstrAbstract ExpandedOp -> OpSize
-instrOpSize = (OpSize 2 <>) . \case
-  EXT{} -> mempty
-  DROPN n -> stackDepthOpSize n
-  DROP -> mempty
-  DUP va -> annsOpSize va
-  SWAP -> mempty
-  DIG n -> stackDepthOpSize n
-  DUG n -> stackDepthOpSize n
-  PUSH va t v -> annsOpSize va <> typeOpSize t <> valueOpSize v
-  SOME ta va -> annsOpSize ta va
-  NONE ta va t -> annsOpSize ta va <> typeOpSize t
-  UNIT ta va -> annsOpSize ta va
-  IF_NONE l r -> ifOpSize l r
-  PAIR ta va fal far -> annsOpSize ta va fal far
-  CAR va fa -> annsOpSize va fa
-  CDR va fa -> annsOpSize va fa
-  LEFT ta va fal far t -> annsOpSize ta va fal far <> typeOpSize t
-  RIGHT ta va fal far t -> annsOpSize ta va fal far <> typeOpSize t
-  IF_LEFT l r -> ifOpSize l r
-  NIL ta va t -> annsOpSize ta va <> typeOpSize t
-  CONS va -> annsOpSize va
-  IF_CONS l r -> ifOpSize l r
-  SIZE va -> annsOpSize va
-  EMPTY_SET ta va ct -> annsOpSize ta va <> innerOpSize ct
-  EMPTY_MAP ta va ct t -> annsOpSize ta va <> innerOpSize ct <> typeOpSize t
-  EMPTY_BIG_MAP ta va ct t -> annsOpSize ta va <> innerOpSize ct <> typeOpSize t
-  MAP va is -> annsOpSize va <> subcodeOpSize is
-  ITER is -> subcodeOpSize is
-  MEM va -> annsOpSize va
-  GET va -> annsOpSize va
-  UPDATE va -> annsOpSize va
-  IF l r -> ifOpSize l r
-  LOOP is -> expandedInstrsOpSize is
-  LOOP_LEFT is -> expandedInstrsOpSize is
-  LAMBDA va ti to is ->
-    annsOpSize va <> typeOpSize ti <> typeOpSize to <> expandedInstrsOpSize is
-  EXEC va -> annsOpSize va
-  APPLY va -> annsOpSize va
-  DIP is -> subcodeOpSize is
-  DIPN n is -> stackDepthOpSize n <> subcodeOpSize is
-  FAILWITH -> mempty
-  CAST va t -> annsOpSize va <> typeOpSize t
-  RENAME va -> annsOpSize va
-  PACK va -> annsOpSize va
-  UNPACK ta va t -> annsOpSize ta va <> typeOpSize t
-  CONCAT va -> annsOpSize va
-  SLICE va -> annsOpSize va
-  ISNAT va -> annsOpSize va
-  ADD va -> annsOpSize va
-  SUB va -> annsOpSize va
-  MUL va -> annsOpSize va
-  EDIV va -> annsOpSize va
-  ABS va -> annsOpSize va
-  NEG va -> annsOpSize va
-  LSL va -> annsOpSize va
-  LSR va -> annsOpSize va
-  OR va -> annsOpSize va
-  AND va -> annsOpSize va
-  XOR va -> annsOpSize va
-  NOT va -> annsOpSize va
-  COMPARE va -> annsOpSize va
-  EQ va -> annsOpSize va
-  NEQ va -> annsOpSize va
-  LT va -> annsOpSize va
-  LE va -> annsOpSize va
-  GT va -> annsOpSize va
-  GE va -> annsOpSize va
-  INT va -> annsOpSize va
-  SELF va fa -> annsOpSize va fa
-  CONTRACT va fa t -> annsOpSize va fa <> typeOpSize t
-  TRANSFER_TOKENS va -> annsOpSize va
-  SET_DELEGATE va -> annsOpSize va
-  CREATE_CONTRACT va1 va2 c -> annsOpSize va1 va2 <> contractOpSize c
-  IMPLICIT_ACCOUNT va -> annsOpSize va
-  NOW va -> annsOpSize va
-  AMOUNT va -> annsOpSize va
-  BALANCE va -> annsOpSize va
-  CHECK_SIGNATURE va -> annsOpSize va
-  SHA256 va -> annsOpSize va
-  SHA512 va -> annsOpSize va
-  BLAKE2B va -> annsOpSize va
-  HASH_KEY va -> annsOpSize va
-  SOURCE va -> annsOpSize va
-  SENDER va -> annsOpSize va
-  ADDRESS va -> annsOpSize va
-  CHAIN_ID va -> annsOpSize va
-  where
-    subcodeOpSize is = expandedInstrOpSize (SeqEx is)
-    ifOpSize l r = expandedInstrOpSize (SeqEx l) <> expandedInstrOpSize (SeqEx r)
-    stackDepthOpSize n = OpSize 1 <> numOpSize n
-
-expandedInstrOpSize :: ExpandedOp -> OpSize
-expandedInstrOpSize = \case
-  PrimEx i -> instrOpSize i
-  SeqEx is -> OpSize 5 <> expandedInstrsOpSize is
-  WithSrcEx _ i -> expandedInstrOpSize i
-
-expandedInstrsOpSize :: [ExpandedOp] -> OpSize
-expandedInstrsOpSize = foldMap expandedInstrOpSize
-
-contractOpSize :: Contract -> OpSize
-contractOpSize (Contract (ParameterType cp rootAnn) st is _) =
-  OpSize 16 <> typeOpSize' [rootAnn] cp <> typeOpSize st <> expandedInstrsOpSize is
-
-numOpSize :: Integral i => i -> OpSize
-numOpSize = OpSize . fromIntegral . length . encodeIntPayload . fromIntegral
-
-valueOpSize :: Value -> OpSize
-valueOpSize = (OpSize 1 <>) . \case
-  ValueInt i -> numOpSize i
-  ValueString s -> (seqOpSize <>) . OpSize . fromIntegral $ length s
-  ValueBytes (InternalByteString b) -> (seqOpSize <>) . OpSize . fromIntegral $ length b
-  ValueUnit -> baseOpSize
-  ValueTrue -> baseOpSize
-  ValueFalse -> baseOpSize
-  ValuePair l r -> baseOpSize <> valueOpSize l <> valueOpSize r
-  ValueLeft x -> baseOpSize <> valueOpSize x
-  ValueRight x -> baseOpSize <> valueOpSize x
-  ValueSome x -> baseOpSize <> valueOpSize x
-  ValueNone -> baseOpSize
-  ValueNil -> seqOpSize
-  ValueSeq l -> seqOpSize <> foldMap valueOpSize l
-  ValueMap m -> seqOpSize <> foldMap eltOpSize m
-  ValueLambda m -> seqOpSize <> foldMap expandedInstrOpSize m
-  where
-    baseOpSize = OpSize 1
-    seqOpSize = OpSize 4
-    eltOpSize (Elt k v) = OpSize 2 <> valueOpSize k <> valueOpSize v
-
-typeOpSize :: Type -> OpSize
-typeOpSize = typeOpSize' []
-
-typeOpSize' :: [FieldAnn] -> Type -> OpSize
-typeOpSize' anns (Type t ta) =
-  tOpSize t <> annsOpSize ta anns
-
-tOpSize :: T -> OpSize
-tOpSize t =
-  OpSize 2 <> case t of
-    TKey -> mempty
-    TUnit -> mempty
-    TSignature -> mempty
-    TChainId -> mempty
-    TOption a -> typeOpSize a
-    TList a -> typeOpSize a
-    TSet a -> innerOpSize a
-    TOperation -> mempty
-    TContract a -> typeOpSize a
-    TPair al ar l r -> typeOpSize' [al] l <> typeOpSize' [ar] r
-    TOr al ar l r -> typeOpSize' [al] l <> typeOpSize' [ar] r
-    TLambda i o -> typeOpSize i <> typeOpSize o
-    TMap k v -> innerOpSize k <> typeOpSize v
-    TBigMap k v -> innerOpSize k <> typeOpSize v
-    TInt -> mempty
-    TNat -> mempty
-    TString -> mempty
-    TBytes -> mempty
-    TMutez -> mempty
-    TBool -> mempty
-    TKeyHash -> mempty
-    TTimestamp -> mempty
-    TAddress -> mempty
-
-innerOpSize :: Type -> OpSize
-innerOpSize (Type _ a) =
-  (OpSize 2) <> annsOpSize a
-
--- | Accepts an arbitrary number of 'TypeAnn' 'FieldAnn' and/or 'VarAnn' that
--- belong to the same entity and returns their total operation size.
---
--- Note that annotations which belong to the same entity (type or instruction)
--- __must be__ considered in aggregate using one call of this function and to be
--- specified in order. See 'AnnotationSet' for details.
-annsOpSize :: AnnsOpSizeVararg x => x
-annsOpSize = annsOpSizeVararg emptyAnnSet
-
-class AnnsOpSizeVararg x where
-  annsOpSizeVararg :: AnnotationSet -> x
-
-instance (KnownAnnTag t, AnnsOpSizeVararg x) => AnnsOpSizeVararg (Annotation t -> x) where
-  annsOpSizeVararg acc an = annsOpSizeVararg (acc <> singleAnnSet an)
-
-instance (KnownAnnTag t, AnnsOpSizeVararg x) => AnnsOpSizeVararg ([Annotation t] -> x) where
-  annsOpSizeVararg acc ans = annsOpSizeVararg (acc <> singleGroupAnnSet ans)
-
-instance AnnsOpSizeVararg OpSize where
-  annsOpSizeVararg = annsOpSizeImpl
-
-annsOpSizeImpl :: AnnotationSet -> OpSize
-annsOpSizeImpl annSet
-  | isNoAnnSet annSet = mempty
-  | otherwise = OpSize . fromIntegral $ 3 * (minAnnSetSize annSet + 1)
diff --git a/src/Michelson/Typed.hs b/src/Michelson/Typed.hs
--- a/src/Michelson/Typed.hs
+++ b/src/Michelson/Typed.hs
@@ -15,6 +15,7 @@
 import Michelson.Typed.Extract as Exports
 import Michelson.Typed.Haskell as Exports
 import Michelson.Typed.Instr as Exports
+import Michelson.Typed.OpSize as Exports
 import Michelson.Typed.Polymorphic as Exports
 import Michelson.Typed.Scope as Exports
 import Michelson.Typed.Sing as Exports
diff --git a/src/Michelson/Typed/Arith.hs b/src/Michelson/Typed/Arith.hs
--- a/src/Michelson/Typed/Arith.hs
+++ b/src/Michelson/Typed/Arith.hs
@@ -368,7 +368,7 @@
   build = \case
     AddOverflow -> "add overflow"
     MulOverflow -> "mul overflow"
-    SubUnderflow -> "sub overflow"
+    SubUnderflow -> "sub underflow"
 
 instance (Show n, Show m) => Buildable (ArithError n m) where
   build (MutezArithError errType n m) = "Mutez "
diff --git a/src/Michelson/Typed/Convert.hs b/src/Michelson/Typed/Convert.hs
--- a/src/Michelson/Typed/Convert.hs
+++ b/src/Michelson/Typed/Convert.hs
@@ -504,10 +504,10 @@
   DOC_ITEM{} -> []
   COMMENT_ITEM tp ->
     case tp of
-      FunctionStarts name -> one $ U.UCOMMENT $ "Function starts: " <> name
-      FunctionEnds name -> one $ U.UCOMMENT $ "Function ends: " <> name
-      StatementStarts name -> one $ U.UCOMMENT $ "Statement starts: " <> name
-      StatementEnds name -> one $ U.UCOMMENT $ "Statement ends: " <> name
+      FunctionStarts name -> one $ U.UCOMMENT $ name <> " [user func starts]"
+      FunctionEnds name -> one $ U.UCOMMENT $ name <> " [user func ends]"
+      StatementStarts name -> one $ U.UCOMMENT $ name <> " [user stmt starts]"
+      StatementEnds name -> one $ U.UCOMMENT $ name <> " [user stmt ends]"
       JustComment com -> one $ U.UCOMMENT com
       StackTypeComment (Just stack) -> one $ U.UCOMMENT $ pretty (listF stack)
       StackTypeComment Nothing -> one $ U.UCOMMENT $ fmt "any stack type"
diff --git a/src/Michelson/Typed/OpSize.hs b/src/Michelson/Typed/OpSize.hs
new file mode 100644
--- /dev/null
+++ b/src/Michelson/Typed/OpSize.hs
@@ -0,0 +1,34 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | Measuring operation size of typed stuff.
+module Michelson.Typed.OpSize
+  ( OpSize (..)
+  , U.opSizeHardLimit
+  , U.smallTransferOpSize
+
+  , instrOpSize
+  , contractOpSize
+  , valueOpSize
+  ) where
+
+import Michelson.Typed.Aliases
+import Michelson.Typed.Convert
+import Michelson.Typed.Instr
+import Michelson.Typed.Scope
+import Michelson.Untyped (OpSize)
+import qualified Michelson.Untyped as U
+
+-- | Estimate instruction operation size.
+instrOpSize :: Instr inp out -> OpSize
+instrOpSize = U.expandedInstrsOpSize . instrToOps
+
+-- | Estimate contract code operation size.
+contractOpSize :: Contract cp st -> OpSize
+contractOpSize = instrOpSize . cCode
+
+-- | Estimate value operation size.
+-- TODO: [#428]: do not use 'PrintedValScope' here.
+valueOpSize :: (PrintedValScope t) => Value t -> OpSize
+valueOpSize = U.valueOpSize . untypeValue
diff --git a/src/Michelson/Typed/Polymorphic.hs b/src/Michelson/Typed/Polymorphic.hs
--- a/src/Michelson/Typed/Polymorphic.hs
+++ b/src/Michelson/Typed/Polymorphic.hs
@@ -262,7 +262,8 @@
 divMich divisible divisor = divisible `div` divisor + extra
   where
     extra =
-      if divisor > 0
+      if divisor > 0 ||
+         divisible `mod` divisor == 0
       then 0
       else 1
 
diff --git a/src/Michelson/Typed/Scope.hs b/src/Michelson/Typed/Scope.hs
--- a/src/Michelson/Typed/Scope.hs
+++ b/src/Michelson/Typed/Scope.hs
@@ -8,12 +8,14 @@
 {- | Module, containing restrictions imposed by instruction or value scope.
 
 Michelson have multiple restrictions on values, examples:
+
 * @operation@ type cannot appear in parameter.
 * @big_map@ type cannot appear in @PUSH@-able constants.
 * @contract@ type cannot appear in type we @UNPACK@ to.
 
 Thus we declare multiple "scopes" - constraints applied in corresponding
 situations, for instance
+
 * 'ParameterScope';
 * 'StorageScope';
 * 'ConstantScope'.
diff --git a/src/Michelson/Untyped.hs b/src/Michelson/Untyped.hs
--- a/src/Michelson/Untyped.hs
+++ b/src/Michelson/Untyped.hs
@@ -12,5 +12,6 @@
 import Michelson.Untyped.Entrypoints as Exports
 import Michelson.Untyped.Ext as Exports
 import Michelson.Untyped.Instr as Exports
+import Michelson.Untyped.OpSize as Exports
 import Michelson.Untyped.Type as Exports
 import Michelson.Untyped.Value as Exports
diff --git a/src/Michelson/Untyped/OpSize.hs b/src/Michelson/Untyped/OpSize.hs
new file mode 100644
--- /dev/null
+++ b/src/Michelson/Untyped/OpSize.hs
@@ -0,0 +1,258 @@
+-- SPDX-FileCopyrightText: 2020 Tocqueville Group
+--
+-- SPDX-License-Identifier: LicenseRef-MIT-TQ
+
+-- | Measuring operation size.
+--
+-- When originating a contract or making a transfer, tezos node forms operation
+-- which is submitted over network. Size of this operation depends on content
+-- of originated contract or transfer parameter resp., and tezos has a hard
+-- limit on operation size thus it has to be accounted.
+--
+-- Functions declared in this module allow assessing size of origination or
+-- transfer operation with up to constant precision because it yet accounts only
+-- for Michelson primitives participating in the operation.
+-- Other stuff which affects op size include parameters which user passes to
+-- origination or transfer themselves, for instance, amount of mutez carried
+-- to the contract. ATM we don't have necessary primitives in Haskell to be
+-- able to handle those parameters here, probably waiting for [TM-89].
+-- Currently, we can assess overall transfer size only approximatelly, like
+-- in 'smallTransferOpSize'.
+module Michelson.Untyped.OpSize
+  ( OpSize (..)
+  , opSizeHardLimit
+  , smallTransferOpSize
+
+  , instrOpSize
+  , expandedInstrsOpSize
+  , valueOpSize
+  ) where
+
+import Fmt (Buildable(..))
+import Prelude hiding (Ordering(..))
+
+import Michelson.Interpret.Utils
+import Michelson.Untyped.Aliases
+import Michelson.Untyped.Annotation
+import Michelson.Untyped.Contract
+import Michelson.Untyped.Instr
+import Michelson.Untyped.Type
+import Michelson.Untyped.Value
+
+-- | Operation size in bytes.
+--
+-- We use newtype wrapper because there are different units of measure
+-- (another one is gas, and we don't want to confuse them).
+newtype OpSize = OpSize { unOpSize :: Word }
+  deriving stock (Show, Eq, Ord)
+
+instance Buildable OpSize where
+  build = build . unOpSize
+
+instance Semigroup OpSize where
+  OpSize a <> OpSize b = OpSize (a + b)
+instance Monoid OpSize where
+  mempty = OpSize 0
+
+-- | Maximal operation size allowed by Tezos production nodes.
+opSizeHardLimit :: OpSize
+opSizeHardLimit = OpSize 16384
+
+-- | Base cost of any transfer of 0 mutez with no extra parameters.
+-- (Add 'valueOpSize <param>' to it to get assessment of actual transfer op size)
+smallTransferOpSize :: OpSize
+smallTransferOpSize = OpSize 162
+
+instrOpSize :: InstrAbstract ExpandedOp -> OpSize
+instrOpSize = (OpSize 2 <>) . \case
+  EXT{} -> mempty
+  DROPN n -> stackDepthOpSize n
+  DROP -> mempty
+  DUP va -> annsOpSize va
+  SWAP -> mempty
+  DIG n -> stackDepthOpSize n
+  DUG n -> stackDepthOpSize n
+  PUSH va t v -> annsOpSize va <> typeOpSize t <> valueOpSize v
+  SOME ta va -> annsOpSize ta va
+  NONE ta va t -> annsOpSize ta va <> typeOpSize t
+  UNIT ta va -> annsOpSize ta va
+  IF_NONE l r -> ifOpSize l r
+  PAIR ta va fal far -> annsOpSize ta va fal far
+  CAR va fa -> annsOpSize va fa
+  CDR va fa -> annsOpSize va fa
+  LEFT ta va fal far t -> annsOpSize ta va fal far <> typeOpSize t
+  RIGHT ta va fal far t -> annsOpSize ta va fal far <> typeOpSize t
+  IF_LEFT l r -> ifOpSize l r
+  NIL ta va t -> annsOpSize ta va <> typeOpSize t
+  CONS va -> annsOpSize va
+  IF_CONS l r -> ifOpSize l r
+  SIZE va -> annsOpSize va
+  EMPTY_SET ta va ct -> annsOpSize ta va <> innerOpSize ct
+  EMPTY_MAP ta va ct t -> annsOpSize ta va <> innerOpSize ct <> typeOpSize t
+  EMPTY_BIG_MAP ta va ct t -> annsOpSize ta va <> innerOpSize ct <> typeOpSize t
+  MAP va is -> annsOpSize va <> subcodeOpSize is
+  ITER is -> subcodeOpSize is
+  MEM va -> annsOpSize va
+  GET va -> annsOpSize va
+  UPDATE va -> annsOpSize va
+  IF l r -> ifOpSize l r
+  LOOP is -> expandedInstrsOpSize is
+  LOOP_LEFT is -> expandedInstrsOpSize is
+  LAMBDA va ti to is ->
+    annsOpSize va <> typeOpSize ti <> typeOpSize to <> expandedInstrsOpSize is
+  EXEC va -> annsOpSize va
+  APPLY va -> annsOpSize va
+  DIP is -> subcodeOpSize is
+  DIPN n is -> stackDepthOpSize n <> subcodeOpSize is
+  FAILWITH -> mempty
+  CAST va t -> annsOpSize va <> typeOpSize t
+  RENAME va -> annsOpSize va
+  PACK va -> annsOpSize va
+  UNPACK ta va t -> annsOpSize ta va <> typeOpSize t
+  CONCAT va -> annsOpSize va
+  SLICE va -> annsOpSize va
+  ISNAT va -> annsOpSize va
+  ADD va -> annsOpSize va
+  SUB va -> annsOpSize va
+  MUL va -> annsOpSize va
+  EDIV va -> annsOpSize va
+  ABS va -> annsOpSize va
+  NEG va -> annsOpSize va
+  LSL va -> annsOpSize va
+  LSR va -> annsOpSize va
+  OR va -> annsOpSize va
+  AND va -> annsOpSize va
+  XOR va -> annsOpSize va
+  NOT va -> annsOpSize va
+  COMPARE va -> annsOpSize va
+  EQ va -> annsOpSize va
+  NEQ va -> annsOpSize va
+  LT va -> annsOpSize va
+  LE va -> annsOpSize va
+  GT va -> annsOpSize va
+  GE va -> annsOpSize va
+  INT va -> annsOpSize va
+  SELF va fa -> annsOpSize va fa
+  CONTRACT va fa t -> annsOpSize va fa <> typeOpSize t
+  TRANSFER_TOKENS va -> annsOpSize va
+  SET_DELEGATE va -> annsOpSize va
+  CREATE_CONTRACT va1 va2 c -> annsOpSize va1 va2 <> contractOpSize c
+  IMPLICIT_ACCOUNT va -> annsOpSize va
+  NOW va -> annsOpSize va
+  AMOUNT va -> annsOpSize va
+  BALANCE va -> annsOpSize va
+  CHECK_SIGNATURE va -> annsOpSize va
+  SHA256 va -> annsOpSize va
+  SHA512 va -> annsOpSize va
+  BLAKE2B va -> annsOpSize va
+  HASH_KEY va -> annsOpSize va
+  SOURCE va -> annsOpSize va
+  SENDER va -> annsOpSize va
+  ADDRESS va -> annsOpSize va
+  CHAIN_ID va -> annsOpSize va
+  where
+    subcodeOpSize is = expandedInstrOpSize (SeqEx is)
+    ifOpSize l r = expandedInstrOpSize (SeqEx l) <> expandedInstrOpSize (SeqEx r)
+    stackDepthOpSize n = OpSize 1 <> numOpSize n
+
+expandedInstrOpSize :: ExpandedOp -> OpSize
+expandedInstrOpSize = \case
+  PrimEx i -> instrOpSize i
+  SeqEx is -> OpSize 5 <> expandedInstrsOpSize is
+  WithSrcEx _ i -> expandedInstrOpSize i
+
+expandedInstrsOpSize :: [ExpandedOp] -> OpSize
+expandedInstrsOpSize = foldMap expandedInstrOpSize
+
+contractOpSize :: Contract -> OpSize
+contractOpSize (Contract (ParameterType cp rootAnn) st is _) =
+  OpSize 16 <> typeOpSize' [rootAnn] cp <> typeOpSize st <> expandedInstrsOpSize is
+
+numOpSize :: Integral i => i -> OpSize
+numOpSize = OpSize . fromIntegral . length . encodeZarithNumber . fromIntegral
+
+valueOpSize :: Value -> OpSize
+valueOpSize = (OpSize 1 <>) . \case
+  ValueInt i -> numOpSize i
+  ValueString s -> (seqOpSize <>) . OpSize . fromIntegral $ length s
+  ValueBytes (InternalByteString b) -> (seqOpSize <>) . OpSize . fromIntegral $ length b
+  ValueUnit -> baseOpSize
+  ValueTrue -> baseOpSize
+  ValueFalse -> baseOpSize
+  ValuePair l r -> baseOpSize <> valueOpSize l <> valueOpSize r
+  ValueLeft x -> baseOpSize <> valueOpSize x
+  ValueRight x -> baseOpSize <> valueOpSize x
+  ValueSome x -> baseOpSize <> valueOpSize x
+  ValueNone -> baseOpSize
+  ValueNil -> seqOpSize
+  ValueSeq l -> seqOpSize <> foldMap valueOpSize l
+  ValueMap m -> seqOpSize <> foldMap eltOpSize m
+  ValueLambda m -> seqOpSize <> foldMap expandedInstrOpSize m
+  where
+    baseOpSize = OpSize 1
+    seqOpSize = OpSize 4
+    eltOpSize (Elt k v) = OpSize 2 <> valueOpSize k <> valueOpSize v
+
+typeOpSize :: Type -> OpSize
+typeOpSize = typeOpSize' []
+
+typeOpSize' :: [FieldAnn] -> Type -> OpSize
+typeOpSize' anns (Type t ta) =
+  tOpSize t <> annsOpSize ta anns
+
+tOpSize :: T -> OpSize
+tOpSize t =
+  OpSize 2 <> case t of
+    TKey -> mempty
+    TUnit -> mempty
+    TSignature -> mempty
+    TChainId -> mempty
+    TOption a -> typeOpSize a
+    TList a -> typeOpSize a
+    TSet a -> innerOpSize a
+    TOperation -> mempty
+    TContract a -> typeOpSize a
+    TPair al ar l r -> typeOpSize' [al] l <> typeOpSize' [ar] r
+    TOr al ar l r -> typeOpSize' [al] l <> typeOpSize' [ar] r
+    TLambda i o -> typeOpSize i <> typeOpSize o
+    TMap k v -> innerOpSize k <> typeOpSize v
+    TBigMap k v -> innerOpSize k <> typeOpSize v
+    TInt -> mempty
+    TNat -> mempty
+    TString -> mempty
+    TBytes -> mempty
+    TMutez -> mempty
+    TBool -> mempty
+    TKeyHash -> mempty
+    TTimestamp -> mempty
+    TAddress -> mempty
+
+innerOpSize :: Type -> OpSize
+innerOpSize (Type _ a) =
+  (OpSize 2) <> annsOpSize a
+
+-- | Accepts an arbitrary number of 'TypeAnn' 'FieldAnn' and/or 'VarAnn' that
+-- belong to the same entity and returns their total operation size.
+--
+-- Note that annotations which belong to the same entity (type or instruction)
+-- __must be__ considered in aggregate using one call of this function and to be
+-- specified in order. See 'AnnotationSet' for details.
+annsOpSize :: AnnsOpSizeVararg x => x
+annsOpSize = annsOpSizeVararg emptyAnnSet
+
+class AnnsOpSizeVararg x where
+  annsOpSizeVararg :: AnnotationSet -> x
+
+instance (KnownAnnTag t, AnnsOpSizeVararg x) => AnnsOpSizeVararg (Annotation t -> x) where
+  annsOpSizeVararg acc an = annsOpSizeVararg (acc <> singleAnnSet an)
+
+instance (KnownAnnTag t, AnnsOpSizeVararg x) => AnnsOpSizeVararg ([Annotation t] -> x) where
+  annsOpSizeVararg acc ans = annsOpSizeVararg (acc <> singleGroupAnnSet ans)
+
+instance AnnsOpSizeVararg OpSize where
+  annsOpSizeVararg = annsOpSizeImpl
+
+annsOpSizeImpl :: AnnotationSet -> OpSize
+annsOpSizeImpl annSet
+  | isNoAnnSet annSet = mempty
+  | otherwise = OpSize . fromIntegral $ 3 * (minAnnSetSize annSet + 1)
diff --git a/src/Tezos/Core.hs b/src/Tezos/Core.hs
--- a/src/Tezos/Core.hs
+++ b/src/Tezos/Core.hs
@@ -27,6 +27,7 @@
   , timestampToSeconds
   , timestampFromSeconds
   , timestampFromUTCTime
+  , timestampToUTCTime
   , timestampPlusSeconds
   , formatTimestamp
   , parseTimestamp
@@ -202,6 +203,10 @@
 timestampFromUTCTime :: UTCTime -> Timestamp
 timestampFromUTCTime = Timestamp . utcTimeToPOSIXSeconds
 {-# INLINE timestampFromUTCTime #-}
+
+timestampToUTCTime :: Timestamp -> UTCTime
+timestampToUTCTime = posixSecondsToUTCTime . unTimestamp
+{-# INLINE timestampToUTCTime #-}
 
 -- | Add given amount of seconds to a 'Timestamp'.
 timestampPlusSeconds :: Timestamp -> Integer -> Timestamp
diff --git a/src/Util/Peano.hs b/src/Util/Peano.hs
--- a/src/Util/Peano.hs
+++ b/src/Util/Peano.hs
@@ -51,13 +51,15 @@
 
 import Data.Constraint (Dict(..))
 import Data.Singletons (Sing, SingI(..))
-import Data.Type.Bool (If)
 import Data.Vinyl (Rec(..))
 import Data.Vinyl.TypeLevel (Nat(..), RLength)
 import GHC.TypeLits (ErrorMessage(..), TypeError)
 import GHC.TypeNats (type (+), type (-))
 import qualified GHC.TypeNats as GHC (Nat)
+import Unsafe.Coerce (unsafeCoerce)
 
+import Util.Type
+
 ----------------------------------------------------------------------------
 -- General
 ----------------------------------------------------------------------------
@@ -91,6 +93,9 @@
 peanoValSing :: forall n. KnownPeano n => Sing n -> Natural
 peanoValSing _ = peanoVal' @n
 
+instance KnownPeano a => MockableConstraint (KnownPeano a) where
+  provideConstraintUnsafe = Dict
+
 data SingNat (n :: Nat) where
   SZ :: SingNat 'Z
   SS :: (SingI n, KnownPeano n) => SingNat n -> SingNat ('S n)
@@ -237,6 +242,12 @@
   RequireLongerOrSameLength (l :: [k]) (a :: Peano)
 instance (RequireLongerOrSameLength' l a, LongerOrSameLength l a) =>
   RequireLongerOrSameLength l a
+
+instance MockableConstraint (RequireLongerOrSameLength l a) where
+  provideConstraintUnsafe = unsafeCoerce $ Dict @(RequireLongerOrSameLength '[] 'Z)
+
+instance MockableConstraint (RequireLongerThan l a) where
+  provideConstraintUnsafe = unsafeCoerce $ Dict @(RequireLongerThan '[()] 'Z)
 
 ----------------------------------------------------------------------------
 -- Length constraints 'Dict'ionaries
diff --git a/src/Util/Type.hs b/src/Util/Type.hs
--- a/src/Util/Type.hs
+++ b/src/Util/Type.hs
@@ -34,9 +34,11 @@
 
   , ConcatListOfTypesAssociativity
   , listOfTypesConcatAssociativityAxiom
+
+  , MockableConstraint (..)
   ) where
 
-import Data.Constraint ((:-)(..), Dict(..))
+import Data.Constraint ((:-)(..), Dict(..), (\\))
 import qualified Data.Kind as Kind
 import Data.Type.Bool (type (&&), If, Not)
 import Data.Type.Equality (type (==))
@@ -77,10 +79,10 @@
 
 -- | A natural conclusion from the fact that error have not occured.
 failUnlessEvi :: forall cond msg. FailUnless cond msg :- (cond ~ 'True)
-failUnlessEvi = Sub $ unsafeCoerce $ Dict @('True ~ 'True)
+failUnlessEvi = Sub provideConstraintUnsafe
 
 failWhenEvi :: forall cond msg. FailWhen cond msg :- (cond ~ 'False)
-failWhenEvi = Sub $ unsafeCoerce $ Dict @('False ~ 'False)
+failWhenEvi = Sub provideConstraintUnsafe
 
 type family AllUnique (l :: [k]) :: Bool where
   AllUnique '[] = 'True
@@ -123,9 +125,7 @@
 
 -- | Reify type equality from boolean equality.
 reifyTypeEquality :: forall a b x. (a == b) ~ 'True => (a ~ b => x) -> x
-reifyTypeEquality x =
-  case unsafeCoerce @(Dict (a ~ a)) @(Dict (a ~ b)) Dict of
-    Dict -> x
+reifyTypeEquality x = x \\ provideConstraintUnsafe @(a ~ b)
 
 -- | Similar to @SingI []@, but does not require individual elements to be also
 -- instance of @SingI@.
@@ -171,5 +171,64 @@
 -- especially if you have complex types.
 -- But (++) type family is associative, so let's define this small hack.
 listOfTypesConcatAssociativityAxiom :: forall a b c . Dict (ConcatListOfTypesAssociativity a b c)
-listOfTypesConcatAssociativityAxiom =
-  unsafeCoerce $ Dict @(ConcatListOfTypesAssociativity '[] '[] '[])
+listOfTypesConcatAssociativityAxiom = provideConstraintUnsafe
+
+-- | Constaints that can be provided on demand.
+--
+-- Needless to say, this is a pretty unsafe operation. This typeclass makes
+-- using it safer in a sense that getting a segfault becomes harder, but still
+-- it deceives the type system and should be used only if providing a proper
+-- proof would be too difficult.
+class MockableConstraint (c :: Constraint) where
+  -- | Produce a constraint out of thin air.
+  provideConstraintUnsafe :: Dict c
+
+instance MockableConstraint (a ~ b) where
+  provideConstraintUnsafe = unsafeCoerce $ Dict @(Int ~ Int)
+
+-- | In majority of the cases we don't want to mock typeclass constraints
+-- since coercing instances of typeclasses with methods is utterly unsafe.
+instance {-# OVERLAPPABLE #-} c a => MockableConstraint (c a) where
+  provideConstraintUnsafe = Dict
+
+instance ( MockableConstraint c1
+         , MockableConstraint c2
+         ) => MockableConstraint (c1, c2) where
+  provideConstraintUnsafe = runIdentity $ do
+    Dict <- pure $ provideConstraintUnsafe @c1
+    Dict <- pure $ provideConstraintUnsafe @c2
+    return Dict
+  {-# INLINE provideConstraintUnsafe #-}
+
+instance ( MockableConstraint c1
+         , MockableConstraint c2
+         , MockableConstraint c3
+         ) => MockableConstraint (c1, c2, c3) where
+  provideConstraintUnsafe = runIdentity $ do
+    Dict <- pure $ provideConstraintUnsafe @(c1, c2)
+    Dict <- pure $ provideConstraintUnsafe @c3
+    return Dict
+  {-# INLINE provideConstraintUnsafe #-}
+
+instance ( MockableConstraint c1
+         , MockableConstraint c2
+         , MockableConstraint c3
+         , MockableConstraint c4
+         ) => MockableConstraint (c1, c2, c3, c4) where
+  provideConstraintUnsafe = runIdentity $ do
+    Dict <- pure $ provideConstraintUnsafe @(c1, c2, c3)
+    Dict <- pure $ provideConstraintUnsafe @c4
+    return Dict
+  {-# INLINE provideConstraintUnsafe #-}
+
+instance ( MockableConstraint c1
+         , MockableConstraint c2
+         , MockableConstraint c3
+         , MockableConstraint c4
+         , MockableConstraint c5
+         ) => MockableConstraint (c1, c2, c3, c4, c5) where
+  provideConstraintUnsafe = runIdentity $ do
+    Dict <- pure $ provideConstraintUnsafe @(c1, c2, c3, c4)
+    Dict <- pure $ provideConstraintUnsafe @c5
+    return Dict
+  {-# INLINE provideConstraintUnsafe #-}
diff --git a/src/Util/TypeLits.hs b/src/Util/TypeLits.hs
--- a/src/Util/TypeLits.hs
+++ b/src/Util/TypeLits.hs
@@ -20,10 +20,11 @@
   , inTypeErrorUnless
   ) where
 
-import Data.Constraint (Dict(..))
+import Data.Constraint ((\\))
 import GHC.TypeLits
-import Unsafe.Coerce (unsafeCoerce)
 
+import Util.Type
+
 symbolValT :: forall s. KnownSymbol s => Proxy s -> Text
 symbolValT = toText . symbolVal
 
@@ -46,6 +47,4 @@
       TypeErrorUnless cond err
   => (cond ~ 'True => a)
   -> a
-inTypeErrorUnless a =
-  case unsafeCoerce @(Dict ('True ~ 'True)) @(Dict (cond ~ 'True)) Dict of
-    Dict -> a
+inTypeErrorUnless a = a \\ provideConstraintUnsafe @(cond ~ 'True)
