diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,6 +1,30 @@
 <!-- Unreleased: append new entries here -->
 
 
+0.15.2
+======
+* [!1362](https://gitlab.com/morley-framework/morley/-/merge_requests/1362)
+  Add division operators over integral operands returning fractional results
+  + Fix division for fixed-point arithmetic;
+  + Add more instances for fixed and rational arithmetic, for better interpop
+    with integrals;
+  + Optimize fixed-point division;
+  + Add `Real NFixed` instance for convenience;
+  + Fix bitshift operations for fixed-point arithmetic;
+  + Fix division between `Rational` (or `NRational`) and `Natural`;
+* [!1342](https://gitlab.com/morley-framework/morley/-/merge_requests/1342)
+  Replace fmt with prettyprinter
+  + Removed trivial `Buildable` instance for `:->` in favor of the default one
+* [!1341](https://gitlab.com/morley-framework/morley/-/merge_requests/1341)
+  Refactor scope constraints
+  + Avoid redundant `check*Presence` uses
+  + Improve error messages with `Nice*` constraints
+* [!1340](https://gitlab.com/morley-framework/morley/-/merge_requests/1340)
+  Remove deprecated types and functions
+  + `defaultAnnOptions`
+  + `dropPrefixThen`
+  + `haskellRepStripFieldPrefix`
+
 0.15.1
 ======
 * [!1325](https://gitlab.com/morley-framework/morley/-/merge_requests/1325)
diff --git a/lorentz.cabal b/lorentz.cabal
--- a/lorentz.cabal
+++ b/lorentz.cabal
@@ -5,7 +5,7 @@
 -- see: https://github.com/sol/hpack
 
 name:           lorentz
-version:        0.15.1
+version:        0.15.2
 synopsis:       EDSL for the Michelson Language
 description:    Lorentz is a powerful meta-programming tool which allows one to write Michelson contracts directly in Haskell. It has the same instructions as Michelson, but operates on Haskell values and allows one to use Haskell features.
 category:       Language
@@ -153,7 +153,6 @@
     , cryptonite
     , data-default
     , first-class-families >=0.5.0.0
-    , fmt
     , lens
     , morley
     , morley-prelude >=0.3.0
diff --git a/src/Lorentz/ADT.hs b/src/Lorentz/ADT.hs
--- a/src/Lorentz/ADT.hs
+++ b/src/Lorentz/ADT.hs
@@ -273,7 +273,7 @@
 -- >>> :{
 --  let ctor =
 --        (fieldCtor (push True)) :&
---        (fieldCtor (push 42)) :&
+--        (fieldCtor (push (42 :: Integer))) :&
 --        (fieldCtor (push ())) :&
 --        RNil
 -- :}
@@ -293,7 +293,7 @@
 
 -- | Version of 'construct' which accepts tuple of field constructors.
 --
--- >>> let ctor = (fieldCtor (push True), fieldCtor (push 42), fieldCtor (push ()))
+-- >>> let ctor = (fieldCtor (push True), fieldCtor (push @Integer 42), fieldCtor (push ()))
 -- >>> constructT @TestProduct ctor -$ ZSNil
 -- TestProduct {fieldA = True, fieldB = 42, fieldC = ()}
 constructT
@@ -454,8 +454,8 @@
 --
 -- >>> unsafeUnwrap_ @TestSum #cTestSumA -$? TestSumA 42
 -- Right 42
--- >>> first pretty $ unsafeUnwrap_ @TestSum #cTestSumA -$? TestSumB (False, ())
--- Left "Reached FAILWITH instruction with \"BadCtor\" at Error occurred on line 1 char 1."
+-- >>> pretty $ unsafeUnwrap_ @TestSum #cTestSumA -$? TestSumB (False, ())
+-- <Left: Reached FAILWITH instruction with '"BadCtor"' at line 1 char 1.>
 unsafeUnwrap_
   :: forall dt name st.
      InstrUnwrapC dt name
diff --git a/src/Lorentz/Annotation.hs b/src/Lorentz/Annotation.hs
--- a/src/Lorentz/Annotation.hs
+++ b/src/Lorentz/Annotation.hs
@@ -6,9 +6,7 @@
 -- | Type and field annotations for Lorentz types.
 module Lorentz.Annotation
   ( AnnOptions (..)
-  , defaultAnnOptions
   , dropPrefix
-  , dropPrefixThen
   , appendTo
   , toCamel
   , toPascal
@@ -54,21 +52,6 @@
 
 instance Default AnnOptions where
   def = AnnOptions id
-
-defaultAnnOptions :: AnnOptions
-defaultAnnOptions = def
-{-# DEPRECATED defaultAnnOptions "Use 'Data.Default.def' instead." #-}
-
--- | Drops the field name prefix from a field.
--- We assume a convention of the prefix always being lower case,
--- and the first letter of the actual field name being uppercase.
--- It also accepts another function which will be applied directly
--- after dropping the prefix.
---
--- Left for compatibility.
-dropPrefixThen :: (Text -> Text) -> Text -> Text
-dropPrefixThen = (. dropPrefix)
-{-# DEPRECATED dropPrefixThen " Use 'dropPrefix' and function composition instead." #-}
 
 -- | @appendTo suffix fields field@ appends the given suffix to @field@
 -- if the field exists in the @fields@ list.
diff --git a/src/Lorentz/Base.hs b/src/Lorentz/Base.hs
--- a/src/Lorentz/Base.hs
+++ b/src/Lorentz/Base.hs
@@ -46,7 +46,7 @@
 import Morley.Michelson.Optimizer (OptimizerConf, optimize, optimizeWithConf)
 import Morley.Michelson.Parser (MichelsonSource, ParserException, parseExpandValue)
 import Morley.Michelson.Preprocess (transformBytes, transformStrings)
-import Morley.Michelson.Printer.Util (RenderDoc(..), buildRenderDocExtended)
+import Morley.Michelson.Printer.Util (RenderDoc(..))
 import Morley.Michelson.Text (MText)
 import Morley.Michelson.TypeCheck (TcError, typeCheckValue, typeCheckingWith)
 import Morley.Michelson.Typed
@@ -62,9 +62,6 @@
   { unLorentzInstr :: RemFail Instr (ToTs inp) (ToTs out)
   } deriving newtype (Show, Eq)
 infixr 1 :->
-
-instance Buildable (inp :-> out) where
-  build = buildRenderDocExtended
 
 instance RenderDoc (inp :-> out) where
   renderDoc context = renderDoc context . iAnyCode
diff --git a/src/Lorentz/Constraints/Scopes.hs b/src/Lorentz/Constraints/Scopes.hs
--- a/src/Lorentz/Constraints/Scopes.hs
+++ b/src/Lorentz/Constraints/Scopes.hs
@@ -35,7 +35,15 @@
 
 import Lorentz.Annotation (HasAnnotation)
 import Morley.Michelson.Typed
+import Morley.Michelson.Typed.Scope.Internal.ForbidT
+import Morley.Michelson.Typed.Scope.Internal.Scopes
 
+{- $setup
+>>> import Lorentz
+>>> import Morley.Michelson.Typed
+>>> import Fmt (pretty)
+-}
+
 -- We write these constraints as class + instance, rather than
 -- type aliases, in order to allow their partial application.
 
@@ -53,35 +61,216 @@
 class (ForbidBigMap (ToT a), IsoValue a) => NoBigMap a
 instance (ForbidBigMap (ToT a), IsoValue a) => NoBigMap a
 
-class (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a
-instance (HasNoNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a
+class (ForbidNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a
+instance (ForbidNestedBigMaps (ToT a), IsoValue a) => CanHaveBigMap a
 
--- | Constraint applied to any part of a parameter type.
---
--- Use t'Lorentz.Constraints.Derivative.NiceParameterFull' instead
--- when you need to know the contract's entrypoints at compile-time.
-type NiceParameter a = (ProperParameterBetterErrors (ToT a), KnownValue a)
+-- For NiceSomething we use type classes to display user-friendly error messages
+-- on ambiguous and polymorphic types. We use SomethingScopeC instead of
+-- SomethingScope for the same reason.
 
-type NiceStorage a = (ProperStorageBetterErrors (ToT a), KnownValue a)
+{- | Constraint applied to any part of a parameter type.
 
+Use t'Lorentz.Constraints.Derivative.NiceParameterFull' instead
+when you need to know the contract's entrypoints at compile-time.
+
+Shows human-readable errors:
+
+>>> epAddressToContract @Operation
+...
+... Type `operation` found in
+... 'TOperation
+... is not allowed in this scope
+...
+
+Also on ambiguity:
+
+>>> epAddressToContract
+...
+... Can't check if type
+... ToT p
+... contains `operation` or nested `big_map`s. Perhaps you need to add
+... NiceParameter p
+... constraint? You can also try adding a type annotation.
+...
+-}
+class (ParameterScopeC (NiceParameter a) (ToT a), KnownValue a) => NiceParameter a
+instance (ParameterScopeC (NiceParameter a) (ToT a), KnownValue a) => NiceParameter a
+
+class (StorageScopeC (NiceStorage a) (ToT a), KnownValue a) => NiceStorage a
+instance (StorageScopeC (NiceStorage a) (ToT a), KnownValue a) => NiceStorage a
+
 type NiceStorageFull a = (NiceStorage a, HasAnnotation a)
 
-type NiceConstant a = (ProperConstantBetterErrors (ToT a), KnownValue a)
+{- | Constraint applied to constants.
 
-type Dupable a = (ProperDupableBetterErrors (ToT a), KnownValue a)
+Shows human-readable errors on ambiguity:
 
-type NicePackedValue a = (ProperPackedValBetterErrors (ToT a), KnownValue a)
+>>> push 1
+...
+... Can't check if type
+... ToT t
+... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
+... NiceConstant t
+... constraint? You can also try adding a type annotation.
+...
 
-type NiceUnpackedValue a = (ProperUnpackedValBetterErrors (ToT a), KnownValue a)
+>>> pretty $ push (1 :: Integer)
+[PUSH int 1]
+-}
+class (ConstantScopeC (NiceConstant a) (ToT a), KnownValue a) => NiceConstant a
+instance (ConstantScopeC (NiceConstant a) (ToT a), KnownValue a) => NiceConstant a
 
+{- | Constraint applied to constants.
+
+Shows human-readable errors:
+
+>>> ticket # dup
+...
+... Type `ticket` found in
+... 'TOption ('TTicket (ToT a))
+... is not allowed in this scope
+...
+
+Also on ambiguity:
+
+>>> dup
+...
+... Can't check if type
+... ToT a
+... contains `ticket`. Perhaps you need to add
+... Dupable a
+... constraint? You can also try adding a type annotation.
+...
+
+>>> pretty $ dup @Integer
+[DUP]
+-}
+class (DupableScopeC (Dupable a) (ToT a), KnownValue a) => Dupable a
+instance (DupableScopeC (Dupable a) (ToT a), KnownValue a) => Dupable a
+
+{- | Constraint applied to a value being packed.
+
+Shows human-readable errors:
+
+>>> pack @Operation
+...
+... Type `operation` found in
+... 'TOperation
+... is not allowed in this scope
+...
+
+Also on ambiguity:
+
+>>> pack
+...
+... Can't check if type
+... ToT a
+... contains `operation`, `big_map`, `ticket` or `sapling_state`. Perhaps you need to add
+... NicePackedValue a
+... constraint? You can also try adding a type annotation.
+...
+-}
+class (PackedValScopeC (NicePackedValue a) (ToT a), KnownValue a) => NicePackedValue a
+instance (PackedValScopeC (NicePackedValue a) (ToT a), KnownValue a) => NicePackedValue a
+
+{- | Constraint applied to a value being unpacked.
+
+Shows human-readable errors:
+
+>>> unpack @Operation
+...
+... Type `operation` found in
+... 'TOperation
+... is not allowed in this scope
+...
+
+Also on ambiguity:
+
+>>> unpack
+...
+... Can't check if type
+... ToT a
+... contains `operation`, `big_map`, `contract`, `ticket` or `sapling_state`. Perhaps you need to add
+... NiceUnpackedValue a
+... constraint? You can also try adding a type annotation.
+...
+-}
+class (UnpackedValScopeC (NiceUnpackedValue a) (ToT a), KnownValue a) => NiceUnpackedValue a
+instance (UnpackedValScopeC (NiceUnpackedValue a) (ToT a), KnownValue a) => NiceUnpackedValue a
+
 type NiceFullPackedValue a = (NicePackedValue a, NiceUnpackedValue a)
 
-type NiceUntypedValue a = (ProperUntypedValBetterErrors (ToT a), KnownValue a)
+class (UntypedValScopeC (NiceUntypedValue a) (ToT a), KnownValue a) => NiceUntypedValue a
+instance (UntypedValScopeC (NiceUntypedValue a) (ToT a), KnownValue a) => NiceUntypedValue a
 
-type NiceViewable a = (ProperViewableBetterErrors (ToT a), KnownValue a)
+{- | Constraint applied to a value returned from a view.
 
--- | Constraint applied to any type, to check if Michelson representation (if exists) of this
--- type is Comparable. In case it is not prints human-readable error message
-type NiceComparable n = (ProperNonComparableValBetterErrors (ToT n), KnownValue n, Comparable (ToT n))
+Shows human-readable errors:
 
-type NiceNoBigMap n = (KnownValue n, HasNoBigMap (ToT n))
+>>> view' @"SomeView" @Operation
+...
+... Type `operation` found in
+... 'TOperation
+... is not allowed in this scope
+...
+
+Also on ambiguity:
+
+>>> view' @"SomeView"
+...
+... Can't check if type
+... ToT ret
+... contains `operation`, `big_map` or `ticket`. Perhaps you need to add
+... NiceViewable ret
+... constraint? You can also try adding a type annotation.
+...
+-}
+class (ViewableScopeC (NiceViewable a) (ToT a), KnownValue a) => NiceViewable a
+instance (ViewableScopeC (NiceViewable a) (ToT a), KnownValue a) => NiceViewable a
+
+{- | Constraint applied to any type, to check if Michelson representation (if exists) of this
+type is Comparable. In case it is not prints human-readable error message
+
+>>> emptySet @[Integer]
+...
+... Non-comparable type
+... 'TList 'TInt
+... is not allowed in this scope
+...
+
+>>> emptySet
+...
+... Can't check if type
+... ToT e
+... contains non-comparable types. Perhaps you need to add
+... NiceComparable e
+... constraint? You can also try adding a type annotation.
+...
+-}
+class (ComparabilityScopeC (NiceComparable n) (ToT n), KnownValue n) => NiceComparable n
+instance (ComparabilityScopeC (NiceComparable n) (ToT n), KnownValue n) => NiceComparable n
+
+{- | Constraint applied to a @big_map@ value type.
+
+Shows human-readable errors:
+
+>>> emptyBigMap @Integer @(BigMap Integer Integer)
+...
+... Type `big_map` found in
+... 'TBigMap 'TInt 'TInt
+... is not allowed in this scope
+...
+
+Also on ambiguity:
+
+>>> emptyBigMap @Integer
+...
+... Can't check if type
+... ToT v
+... contains `big_map`. Perhaps you need to add
+... NiceNoBigMap v
+... constraint? You can also try adding a type annotation.
+...
+-}
+class (KnownValue n, ForbidManyT (NiceNoBigMap n) '[ 'PSBigMap] (ToT n)) => NiceNoBigMap n
+instance (KnownValue n, ForbidManyT (NiceNoBigMap n) '[ 'PSBigMap] (ToT n)) => NiceNoBigMap n
diff --git a/src/Lorentz/ContractRegistry.hs b/src/Lorentz/ContractRegistry.hs
--- a/src/Lorentz/ContractRegistry.hs
+++ b/src/Lorentz/ContractRegistry.hs
@@ -188,7 +188,7 @@
 -- | Run an action operating with 'ContractRegistry'.
 runContractRegistry :: ContractRegistry -> CmdLnArgs -> IO ()
 runContractRegistry registry = \case
-  List -> pretty registry
+  List -> putTextLn $ pretty registry
   Print mName mOutput forceOneLine useMicheline -> do
     (ContractInfo{..}, name) <- getContract mName registry
     let
diff --git a/src/Lorentz/CustomArith/FixedArith.hs b/src/Lorentz/CustomArith/FixedArith.hs
--- a/src/Lorentz/CustomArith/FixedArith.hs
+++ b/src/Lorentz/CustomArith/FixedArith.hs
@@ -10,18 +10,25 @@
   , castFixedToNFixed
   , unsafeCastFixedToNFixed
     -- * Typeclasses
-  , LorentzFixedCast (..)
   , Fixed (..)
   , NFixed (..)
 
   -- * Support types and functions
-  , DecBase (..)
-  , BinBase (..)
+  , LorentzFixedBaseKind
+  , DecBase
+  , BinBase
   , resolution_
+  , toFixed
+  , fromFixed
+  , LorentzFixedBase
 
+  -- * Internals
+  , getBase
+
   ) where
 
 import Data.Fixed (Fixed(..), HasResolution(..))
+import Data.Ratio ((%))
 import GHC.Num qualified (fromInteger)
 import GHC.TypeLits qualified as Lit
 import Prelude hiding (and, compare, drop, natVal, some, swap)
@@ -43,17 +50,31 @@
 
 {-# ANN module ("HLint: ignore Use 'natVal' from Universum" :: Text) #-}
 
--- | Datatypes, representing base of the fixed-point values
-data DecBase p where
-  DecBase :: KnownNat p => DecBase p
-data BinBase p where
-  BinBase :: KnownNat p => BinBase p
+data LorentzFixedBaseKindTag
 
+-- | Open kind for fixed value bases.
+type LorentzFixedBaseKind = LorentzFixedBaseKindTag -> Type
+
+-- | Represents binary base of the Lorentz fixed-point values
+data BinBase :: Lit.Nat -> LorentzFixedBaseKind
+
+-- | Represents decimal base of the Lorentz fixed-point values
+data DecBase :: Lit.Nat -> LorentzFixedBaseKind
+
+type LorentzFixedBase :: (Lit.Nat -> LorentzFixedBaseKind) -> Constraint
+class Typeable a => LorentzFixedBase a where
+  getBase :: Num b => b
+
+instance LorentzFixedBase DecBase where
+  getBase = 10
+instance LorentzFixedBase BinBase where
+  getBase = 2
+
 instance KnownNat p => HasResolution (DecBase p) where
-  resolution _ = 10 ^ (Lit.natVal (Proxy @p))
+  resolution _ = getBase @DecBase ^ (Lit.natVal (Proxy @p))
 
 instance KnownNat p => HasResolution (BinBase p) where
-  resolution _ = 2 ^ (Lit.natVal (Proxy @p))
+  resolution _ = getBase @BinBase ^ (Lit.natVal (Proxy @p))
 
 -- | Special function to get resolution without argument
 resolution_ :: forall a. HasResolution a => Natural
@@ -63,12 +84,11 @@
        then error "Lorentz Rationals support only positive resolutions"
        else Unsafe.fromIntegral @Integer @Natural r
 
-
 -- | Like @Fixed@ but with a @Natural@ value inside constructor
 newtype NFixed p = MkNFixed Natural deriving stock (Eq, Ord)
 
 convertNFixedToFixed :: NFixed a -> Fixed a
-convertNFixedToFixed (MkNFixed a) = MkFixed (Unsafe.fromIntegral @Natural @Integer a)
+convertNFixedToFixed (MkNFixed a) = MkFixed (fromIntegral @Natural @Integer a)
 
 instance (HasResolution a) => Show (NFixed a) where
   show = show . convertNFixedToFixed
@@ -89,6 +109,9 @@
       res = fromInteger $ resolution fa
   fromRational r = withResolution (\res -> MkNFixed (floor (r * (toRational res))))
 
+instance (HasResolution a) => Real (NFixed a) where
+  toRational (MkNFixed x) = fromIntegral x % resolution (Proxy @a)
+
 instance IsoValue (NFixed p) where
   type ToT (NFixed p) = 'TNat
   toVal (MkNFixed x) = VNat x
@@ -102,7 +125,7 @@
 withResolution foo = foo . fromInteger . resolution $ Proxy @a
 
 ------------------------------------------------------------------------------
--- Arithmetic operations' Insances
+-- Arithmetic operations' Instances
 ------------------------------------------------------------------------------
 
 instance (r ~ (Fixed p)) => ArithOpHs Add (Fixed p) (Fixed p) r
@@ -136,27 +159,23 @@
 instance (r ~ (Fixed p)) => ArithOpHs Sub (NFixed p) (Fixed p) r
 
 
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))
+instance (r ~ Fixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (Fixed (b1 a)) (Fixed (b2 b)) r
 instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Integer r
 instance (r ~ (Fixed p)) => ArithOpHs Mul (Fixed p) Natural r
 instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (Fixed p) r
 instance (r ~ (Fixed p)) => ArithOpHs Mul Natural (Fixed p) r
 
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (DecBase a)) (NFixed (DecBase b)) (NFixed (DecBase r))
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (BinBase a)) (NFixed (BinBase b)) (NFixed (BinBase r))
+instance (r ~ NFixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (NFixed (b1 a)) (NFixed (b2 b)) r
 instance (r ~ (Fixed p)) => ArithOpHs Mul (NFixed p) Integer r
 instance (r ~ (NFixed p)) => ArithOpHs Mul (NFixed p) Natural r
 instance (r ~ (Fixed p)) => ArithOpHs Mul Integer (NFixed p) r
 instance (r ~ (NFixed p)) => ArithOpHs Mul Natural (NFixed p) r
 
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (DecBase a)) (Fixed (DecBase b)) (Fixed (DecBase r))
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (DecBase a)) (NFixed (DecBase b)) (Fixed (DecBase r))
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (NFixed (BinBase a)) (Fixed (BinBase b)) (Fixed (BinBase r))
-instance (r ~ (a Lit.+ b)) => ArithOpHs Mul (Fixed (BinBase a)) (NFixed (BinBase b)) (Fixed (BinBase r))
+instance (r ~ Fixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (Fixed (b1 a)) (NFixed (b2 b)) r
+instance (r ~ Fixed (b1 (a Lit.+ b)), b1 ~ b2) => ArithOpHs Mul (NFixed (b1 a)) (Fixed (b2 b)) r
 
-instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r
-instance (r ~ (NFixed (BinBase b))) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r
+instance (r ~ (NFixed (BinBase a))) => ArithOpHs Lsl (NFixed (BinBase a)) Natural r
+instance (r ~ (NFixed (BinBase a))) => ArithOpHs Lsr (NFixed (BinBase a)) Natural r
 
 instance UnaryArithOpHs Neg (Fixed p) where
   type UnaryArithResHs Neg (Fixed p) = (Fixed p)
@@ -167,72 +186,92 @@
 
 -- | Round is implemented using "banker's rounding" strategy, rounding half-way values
 -- towards nearest even value
-instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)) where
-  round_ = roundingHelper @a @b Round 10
-  ceil_ = roundingHelper @a @b Ceil 10
-  floor_ = roundingHelper @a @b Floor 10
+instance (KnownNat a, KnownNat b, b1 ~ b2, LorentzFixedBase b1)
+  => LorentzRounding (Fixed (b1 a)) (Fixed (b2 b)) where
+  round_ = roundingHelper Round
+  ceil_ = roundingHelper Ceil
+  floor_ = roundingHelper Floor
 
-instance (KnownNat a, KnownNat b) => LorentzRounding (Fixed (BinBase a)) (Fixed (BinBase b)) where
-  round_ = roundingHelper @a @b Round 2
-  ceil_ = roundingHelper @a @b Ceil 2
-  floor_ = roundingHelper @a @b Floor 2
+instance (KnownNat a, KnownNat b, b1 ~ b2, LorentzFixedBase b1)
+  => LorentzRounding (NFixed (b1 a)) (NFixed (b2 b)) where
+  round_ = roundingHelper Round
+  ceil_ = roundingHelper Ceil
+  floor_ = roundingHelper Floor
 
-instance (LorentzRounding (Fixed (DecBase a)) (Fixed (DecBase b)))
-  => LorentzRounding (NFixed (DecBase a)) (NFixed (DecBase b)) where
-  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed
-  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed
-  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed
+-- | Convert to the corresponding integral type by banker's rounding.
+fromFixed
+  :: forall a f base t s.
+    ( a ~ f (base t)
+    , ToT (f (base 0)) ~ ToT (Unwrappabled a)
+    , LorentzRounding a (f (base 0))
+    )
+  => a : s :-> Unwrappabled a : s
+fromFixed = round_ @_ @(f (base 0)) # forcedCoerce_
 
-instance (KnownNat a, KnownNat b)
-  => LorentzRounding (NFixed (BinBase a)) (NFixed (BinBase b)) where
-  round_ = castNFixedToFixed # round_ # unsafeCastFixedToNFixed
-  ceil_ = castNFixedToFixed # ceil_ # unsafeCastFixedToNFixed
-  floor_ = castNFixedToFixed # floor_ # unsafeCastFixedToNFixed
+-- | Convert from the corresponding integral type.
+toFixed
+  :: forall a f base t s.
+    ( a ~ f (base t), LorentzFixedBase base
+    , Unwrappable a
+    , KnownNat t
+    , ArithOpHs Mul Natural (Unwrappabled a) (Unwrappabled a)
+    )
+  => Unwrappabled a : s :-> a : s
+toFixed = rebase @base @t # forcedCoerce_ @(Unwrappabled a) @(f (base t))
 
--- | Class that allows casting @Fixed@ values to Integer in vice versa
-class LorentzFixedCast a where
-  fromFixed :: a : s :-> Integer : s
-  toFixed :: Integer : s :-> a : s
+type DivConstraint a b t r f b1 b2 =
+  ( KnownNat b
+  , b1 ~ b2
+  , DivConstraint1 a t r f b1
+  )
 
-instance (KnownNat a) => LorentzFixedCast (Fixed (DecBase a)) where
-  fromFixed :: (Fixed (DecBase a)) : s :-> Integer : s
-  fromFixed = (round_ @(Fixed (DecBase a)) @(Fixed (DecBase 0))) # forcedCoerce_
-  toFixed = let pow :: Integer = 10 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (DecBase a))
+type DivConstraint1 a t r f base =
+  ( KnownNat a
+  , KnownNat t
+  , LorentzFixedBase base
+  , r ~ Maybe (f (base t))
+  )
 
-instance (KnownNat a) => LorentzFixedCast (Fixed (BinBase a)) where
-  fromFixed :: (Fixed (BinBase a)) : s :-> Integer : s
-  fromFixed = (round_ @(Fixed (BinBase a)) @(Fixed (BinBase 0))) # forcedCoerce_
-  toFixed = let pow :: Integer = 2 ^ Lit.natVal (Proxy @a) in push pow # mul # forcedCoerce_ @Integer @(Fixed (BinBase a))
+instance DivConstraint a b t r Fixed b1 b2 => ArithOpHs Div (Fixed (b1 a)) (Fixed (b2 b)) r where
+  evalArithOpHs = fixedDivHelper
 
-instance (LorentzFixedCast (Fixed a)) => LorentzFixedCast (NFixed a) where
-  fromFixed = castNFixedToFixed # fromFixed
-  toFixed = toFixed # castFixedToNFixed # assertSome [mt|casting negative value to NFixed|]
+instance DivConstraint1 a t r Fixed b1 => ArithOpHs Div Integer (Fixed (b1 a)) r where
+  evalArithOpHs = toFixed @_ @_ @_ @0 # fixedDivHelper
 
-instance ( KnownNat a
-         , KnownNat b
-         , KnownNat r
-         ) => ArithOpHs Div (Fixed (DecBase a)) (Fixed (DecBase b)) (Maybe (Fixed (DecBase r))) where
-  evalArithOpHs = fixedDivHelper @a @b @r 10
+instance DivConstraint1 a t r Fixed b1 => ArithOpHs Div Natural (Fixed (b1 a)) r where
+  evalArithOpHs = int # toFixed @_ @_ @_ @0 # fixedDivHelper
 
-instance ( KnownNat a
-         , KnownNat b
-         , KnownNat r
-         ) => ArithOpHs Div (Fixed (BinBase a)) (Fixed (BinBase b)) (Maybe (Fixed (BinBase r))) where
-  evalArithOpHs = fixedDivHelper @a @b @r 2
+-- NFixed
 
-instance ( KnownNat a
-         , KnownNat b
-         , KnownNat r
-         ) => ArithOpHs Div (NFixed (DecBase a)) (NFixed (DecBase b)) (Maybe (NFixed (DecBase r))) where
-  evalArithOpHs = fixedDivHelper @a @b @r 10
+instance DivConstraint a b t r NFixed b1 b2 => ArithOpHs Div (NFixed (b1 a)) (NFixed (b2 b)) r where
+  evalArithOpHs = fixedDivHelper
 
-instance ( KnownNat a
-         , KnownNat b
-         , KnownNat r
-         ) => ArithOpHs Div (NFixed (BinBase a)) (NFixed (BinBase b)) (Maybe (NFixed (BinBase r))) where
-  evalArithOpHs = fixedDivHelper @a @b @r 2
+instance DivConstraint1 a t r NFixed b1 => ArithOpHs Div Natural (NFixed (b1 a)) r where
+  evalArithOpHs = toFixed @_ @_ @_ @0 # fixedDivHelper
 
+instance DivConstraint1 a t r Fixed b1 => ArithOpHs Div Integer (NFixed (b1 a)) r where
+  evalArithOpHs = toFixed @_ @_ @_ @0 # dip castNFixedToFixed # fixedDivHelper
 
+type DivIntegralConstraint r b =
+  ( KnownNat r
+  , LorentzFixedBase b
+  )
+
+-- NB: Instances are parametrized by the result type by design since we also
+-- have rational arithmetic.
+
+instance DivIntegralConstraint r b => ArithOpHs Div Integer Integer (Maybe (Fixed (b r))) where
+  evalArithOpHs = toFixed @(Fixed (b r)) # dip (toFixed @(Fixed (b 0))) # fixedDivHelper
+instance DivIntegralConstraint r b => ArithOpHs Div Natural Natural (Maybe (Fixed (b r))) where
+  evalArithOpHs = int # toFixed @(Fixed (b r)) # dip (int # toFixed @(Fixed (b 0))) # fixedDivHelper
+instance DivIntegralConstraint r b => ArithOpHs Div Integer Natural (Maybe (Fixed (b r))) where
+  evalArithOpHs = toFixed @(Fixed (b r)) # dip (int # toFixed @(Fixed (b 0))) # fixedDivHelper
+instance DivIntegralConstraint r b => ArithOpHs Div Natural Integer (Maybe (Fixed (b r))) where
+  evalArithOpHs = int # toFixed @(Fixed (b r)) # dip (toFixed @(Fixed (b 0))) # fixedDivHelper
+
+instance DivIntegralConstraint r b => ArithOpHs Div Natural Natural (Maybe (NFixed (b r))) where
+  evalArithOpHs = toFixed @(NFixed (b r)) # dip (toFixed @(NFixed (b r))) # fixedDivHelper
+
 castNFixedToFixed :: NFixed p : s :-> Fixed p : s
 castNFixedToFixed = int # forcedCoerce_
 
@@ -242,29 +281,21 @@
 unsafeCastFixedToNFixed ::  Fixed p : s :-> NFixed p : s
 unsafeCastFixedToNFixed = coerceUnwrap # Lorentz.Instr.abs # forcedCoerce_
 
-instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Integer r where
-  evalArithOpHs = edivHelper @a @Integer 10
-
-instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (DecBase a)) Natural r where
-  evalArithOpHs = edivHelper @a @Integer 10
-
-instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Integer r where
-  evalArithOpHs = edivHelper @a @Natural 2
-
-instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (Fixed (BinBase a)) Natural r where
-  evalArithOpHs = edivHelper @a @Natural 2
-
-instance (r ~ Maybe (Integer, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Integer r where
-  evalArithOpHs = edivHelper @a @Integer 10
+instance (r ~ Maybe (Integer, NFixed (base a)), KnownNat a, LorentzFixedBase base)
+  => ArithOpHs EDiv (Fixed (base a)) Integer r where
+  evalArithOpHs = edivHelper
 
-instance (r ~ Maybe (Natural, NFixed (DecBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (DecBase a)) Natural r where
-  evalArithOpHs = edivHelper @a @Natural 10
+instance (r ~ Maybe (Integer, NFixed (base a)), KnownNat a, LorentzFixedBase base)
+  => ArithOpHs EDiv (Fixed (base a)) Natural r where
+  evalArithOpHs = edivHelper
 
-instance (r ~ Maybe (Integer, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Integer r where
-  evalArithOpHs = edivHelper @a @Natural 2
+instance (r ~ Maybe (Integer, NFixed (base a)), KnownNat a, LorentzFixedBase base)
+  => ArithOpHs EDiv (NFixed (base a)) Integer r where
+  evalArithOpHs = edivHelper
 
-instance (r ~ Maybe (Natural, NFixed (BinBase a)), KnownNat a) => ArithOpHs EDiv (NFixed (BinBase a)) Natural r where
-  evalArithOpHs = edivHelper @a @Natural 2
+instance (r ~ Maybe (Natural, NFixed (base a)), KnownNat a, LorentzFixedBase base)
+  => ArithOpHs EDiv (NFixed (base a)) Natural r where
+  evalArithOpHs = edivHelper
 
 ----------------------------------------------------------------------------
 -- Helpers
@@ -275,27 +306,31 @@
 -- Note: Round is implemented using "banker's rounding" strategy, rounding half-way values
 -- towards the nearest even value.
 roundingHelper
-  :: forall a b r1 r2 s.
+  :: forall a b r1 r2 s base f.
     ( KnownNat a, KnownNat b
     , ForbidTicket (ToT (Unwrappabled r1))
     , MichelsonCoercible r1 r2
-    , Typeable (Unwrappabled r2)
-    , IsoValue (Unwrappabled r2)
     , SingI (ToT (Unwrappabled r1))
     , Unwrappable r2
     , Unwrappable r1
-    , ArithOpHs Add Integer (Unwrappabled r2) (Unwrappabled r2)
     , ArithOpHs Add Natural (Unwrappabled r2) (Unwrappabled r2)
+    , ArithOpHs Add (Unwrappabled r2) (Unwrappabled r2) (Unwrappabled r2)
     , ArithOpHs And (Unwrappabled r2) Natural Natural
-    , ArithOpHs EDiv (Unwrappabled r1) Integer (Maybe (Unwrappabled r2, Natural))
-    , ArithOpHs Mul Integer r1 r1
+    , ArithOpHs EDiv (Unwrappabled r1) Natural (Maybe (Unwrappabled r2, Natural))
+    , ArithOpHs Mul Natural r1 r1
+    , LorentzFixedBase base
+    , r1 ~ f (base a)
+    , r2 ~ f (base b)
+    , NiceConstant (Unwrappabled r2)
+    , Num (Unwrappabled r2)
     )
-  => RoundingPattern -> Natural -> (r1 : s :-> r2 : s)
-roundingHelper rp base =
+  => RoundingPattern -> (r1 : s :-> r2 : s)
+roundingHelper rp =
   let halfBase :: Natural = base `P.div` 2
-      powDifference :: Integer = (Lit.natVal (Proxy @b)) - (Lit.natVal (Proxy @a))
-      newPow :: Integer = fromIntegral $ 2 * halfNewPow
+      powDifference :: Integer = Lit.natVal (Proxy @b) - Lit.natVal (Proxy @a)
+      newPow = 2 * halfNewPow
       halfNewPow :: Natural = halfBase * (base ^ (Prelude.abs powDifference - 1))
+      base = getBase @base
    in case () of
         _ | powDifference == 0 -> (forcedCoerce_ :: (r1 : s :-> r2 : s))
           | powDifference > 0 ->
@@ -319,61 +354,96 @@
                     ifEq0 (dupN @2 # and) nop #
                     -- if quot is odd or rem > halfNewPow, add 1 to quot.
                     add
-                   )
+                    )
                 Ceil ->
                   unpair #
                   swap #
-                  ifNeq0 (push (1 :: Integer) # add) nop
+                  ifNeq0 (push (1 :: Unwrappabled r2) # add) nop
                 Floor -> car
               # unsafeCoerceWrap
 
 fixedDivHelper
-  :: forall t1 t2 t3 base b1 b2 a r s.
-     ( KnownNat t1, KnownNat t2, KnownNat t3
-     , Num base, NiceConstant base
-     , Unwrappable r, Unwrappable b1, Unwrappable a
-     , Unwrappabled a ~ base
-     , ArithOpHs Mul base r r
-     , ArithOpHs EDiv (Unwrappabled r) (Unwrappabled b1) (Maybe (base, b2))
-     , IsoValue a, Typeable a
+  :: forall t1 t2 t3 base any s f x y r.
+     ( x ~ f (base t1), y ~ f (base t2), r ~ f (base t3)
+     , LorentzFixedBase base
+     , Each '[Unwrappable] '[x, y, r]
+     , Each '[KnownNat] '[t1, t2, t3]
+     , ArithOpHs
+          EDiv
+          (Unwrappabled x)
+          (Unwrappabled y)
+          (Maybe (Unwrappabled r, any))
+     , IsoValue r, Typeable f
+     , ArithOpHs Mul Natural x x
+     , ArithOpHs Mul Natural y y
      )
-  => base -> (r : b1 : s) :-> (Maybe a : s)
-fixedDivHelper base =
-  let powA = Lit.natVal (Proxy @t1)
-      powB = Lit.natVal (Proxy @t2)
-      powR = base ^ (Lit.natVal (Proxy @t3) - 1)
-   in
-     push powB #
-     push powA #
-     ifGt (push powR # mul) nop #
-     dip coerceUnwrap #
-     coerceUnwrap #
-     ediv @_ @_ @(Maybe (base, b2)) #
-     ifNone (none) (car # unsafeCoerceWrap # some)
+  => x : y : s :-> Maybe r : s
+fixedDivHelper =
+  adjust #
+  dip coerceUnwrap #
+  coerceUnwrap #
+  ediv #
+  Lorentz.Instr.map @(Maybe (Unwrappabled r, any)) (car # unsafeCoerceWrap)
+  where
+    powDifference :: Integer
+    powDifference = Lit.natVal (Proxy @t2) + Lit.natVal (Proxy @t3) - Lit.natVal (Proxy @t1)
+    -- see Note [fixedDivHelper] below for an explanation.
+    multiplier :: Natural
+    multiplier = getBase @base ^ P.abs powDifference
+    adjust = case P.compare powDifference 0 of
+      P.EQ -> nop
+      P.GT -> push multiplier # mul
+      P.LT -> dip $ push multiplier # mul
 
+{-
+Note [fixedDivHelper]
+~~~~~~~~~~~~~~~~~~~~~
+
+This code may look a little bit mysterious without an explanation, so here goes:
+
+We want to compute r = x / y, where x = a β⁻ⁿ¹, y = b β⁻ⁿ², and r has to be
+represented as some r = c β⁻ⁿ³. Ultimately we need to compute c. Thus:
+
+c β⁻ⁿ³ = (a β⁻ⁿ¹) / (b β⁻ⁿ²)
+c β⁻ⁿ³ = (a / b) β⁻ⁿ¹⁺ⁿ²
+c = (a / b) β⁻ⁿ¹⁺ⁿ²⁺ⁿ³
+
+Let ε = | -n₁ + n₂ + n₃ |
+Let μ = βᵋ
+
+(-n₁ + n₂ + n₃) can be either positive, negative, or zero. If it's zero, μ = 1,
+and no futher action is necessary.
+If it's positive, we need to multiply a by μ before division.
+If it's negative, technically we could divide a by μ, but division is more
+costly than multiplication, so instead we can multiply b by μ to obtain the same
+result.
+
+In the code above, β = getBase @base, μ = multiplier, and
+(-n₁ + n₂ + n₃) = powDifference.
+
+-- @lierdakil
+-}
+
 edivHelper
-  :: forall a base x y r1 r2 m s.
-     ( KnownNat a, Num base, NiceConstant base, KnownValue r1, KnownValue r2, Dupable m
-     , UnaryArithOpHs Eq' m, ArithOpHs Mul base y m
-     , ArithOpHs EDiv (Unwrappabled x) m (Maybe (r1, Unwrappabled r2))
-     , Unwrappable x, Unwrappable r2, UnaryArithResHs Eq' m ~ Bool
-     )
-  => base -> (x : y : s) :-> (Maybe (r1, r2) : s)
-edivHelper base =
-  let powA = base ^ (Lit.natVal (Proxy @a))
-   in
-     swap  #
-     push powA #
-     mul #
-     dup #
-     ifEq0 @m (dropN @2 # none)
-     (
-       swap #
-       coerceUnwrap #
-       ediv #
-       assertSome (Impossible @"Division by zero impossible here") #
-       unpair #
-       dip unsafeCoerceWrap #
-       pair #
-       some
+  :: forall a base x y r1 r2 s f.
+     ( KnownNat a
+     , ArithOpHs Mul Natural y y
+     , ArithOpHs EDiv (Unwrappabled x) y (Maybe (r1, Unwrappabled r2))
+     , Unwrappable x, Unwrappable r2
+     , LorentzFixedBase base
+     , x ~ f (base a)
      )
+  => (x : y : s) :-> (Maybe (r1, r2) : s)
+edivHelper =
+  dip (rebase @base @a) #
+  coerceUnwrap #
+  ediv #
+  forcedCoerce_ @(Maybe (r1, Unwrappabled r2)) @(Maybe (r1, r2))
+
+rebase
+  :: forall base (exp :: Lit.Nat) b s.
+    (KnownNat exp, ArithOpHs Mul Natural b b, LorentzFixedBase base)
+  => b : s :-> b : s
+rebase = case getBase @base ^ Lit.natVal (Proxy @exp) :: Natural of
+  1 -> nop
+  pow -> push pow # mul
diff --git a/src/Lorentz/CustomArith/RationalArith.hs b/src/Lorentz/CustomArith/RationalArith.hs
--- a/src/Lorentz/CustomArith/RationalArith.hs
+++ b/src/Lorentz/CustomArith/RationalArith.hs
@@ -56,7 +56,6 @@
 import Morley.Michelson.Text
 import Morley.Michelson.Typed
 import Morley.Util.Named
-import Morley.Util.Type
 
 newtype Rational =
   UnsafeRational (Integer, Natural)
@@ -147,7 +146,7 @@
 
   oppositeRational :: r : s :-> r : s
 
-  reduce :: (KnownList s, KnownList (ToTs s)) => r : s :-> r : s
+  reduce :: r : s :-> r : s
 
 instance LorentzRational Rational where
   oppositeRational = do
@@ -198,7 +197,7 @@
   evalArithOpHs = dip deconstructRational # mul # constructRational
 
 instance (r ~ Rational) => ArithOpHs Mul Rational Rational r where
-  evalArithOpHs = mulRationalHelper @Rational @Rational @Rational
+  evalArithOpHs = mulRationalHelper
 
 instance (r ~ Rational) => ArithOpHs Div Integer Rational r where
   evalArithOpHs = dip oppositeRational # mul
@@ -207,7 +206,7 @@
 instance (r ~ Rational) => ArithOpHs Div Rational Integer r where
   evalArithOpHs = oppositeRational # mul # oppositeRational
 instance (r ~ Rational) => ArithOpHs Div Rational Natural r where
-  evalArithOpHs = oppositeRational # mul
+  evalArithOpHs = oppositeRational # mul # oppositeRational
 instance (r ~ Rational) => ArithOpHs Div Rational Rational r where
   evalArithOpHs = dip oppositeRational # mul
 
@@ -243,7 +242,7 @@
   evalArithOpHs = dip deconstructRational # mul # constructRational
 
 instance (r ~ NRational) => ArithOpHs Mul NRational NRational r where
-  evalArithOpHs = mulRationalHelper @NRational @NRational @NRational
+  evalArithOpHs = mulRationalHelper
 
 instance (r ~ Rational) => ArithOpHs Div Integer NRational r where
   evalArithOpHs = dip oppositeRational # mul
@@ -252,7 +251,7 @@
 instance (r ~ Rational) => ArithOpHs Div NRational Integer r where
   evalArithOpHs = oppositeRational # mul # oppositeRational
 instance (r ~ NRational) => ArithOpHs Div NRational Natural r where
-  evalArithOpHs = oppositeRational # mul
+  evalArithOpHs = oppositeRational # mul # oppositeRational
 instance (r ~ NRational) => ArithOpHs Div NRational NRational r where
   evalArithOpHs = dip oppositeRational # mul
 
@@ -265,14 +264,34 @@
 instance (r ~ Rational) => ArithOpHs Sub NRational Rational r where
   evalArithOpHs = addSubRationalHelper sub
 instance (r ~ Rational) => ArithOpHs Mul Rational NRational r where
-  evalArithOpHs = mulRationalHelper @Rational @NRational @Rational
+  evalArithOpHs = mulRationalHelper
 instance (r ~ Rational) => ArithOpHs Mul NRational Rational r where
-  evalArithOpHs = mulRationalHelper @NRational @Rational @Rational
+  evalArithOpHs = mulRationalHelper
 instance (r ~ Rational) => ArithOpHs Div Rational NRational r where
   evalArithOpHs = dip oppositeRational # mul
 instance (r ~ Rational) => ArithOpHs Div NRational Rational r where
   evalArithOpHs = dip oppositeRational # mul
 
+-- NB: Instances are parametrized by the result type by design since we also
+-- have fixed arithmetic.
+
+instance ArithOpHs Div Integer Integer (Maybe Rational) where
+  evalArithOpHs = do
+    dupN @2; ifLt0 neg nop; dip abs
+    mkRatReduce
+instance ArithOpHs Div Natural Natural (Maybe NRational) where
+  evalArithOpHs = mkRatReduce
+instance ArithOpHs Div Integer Natural (Maybe Rational) where
+  evalArithOpHs = mkRatReduce
+instance ArithOpHs Div Natural Integer (Maybe Rational) where
+  evalArithOpHs = do
+    dupN @2; ifLt0 neg int; dip abs
+    mkRatReduce
+
+mkRatReduce
+  :: (LorentzRational r, Unwrappabled r ~ (a, Natural), KnownValue r)
+  => a : Natural : s :-> Maybe r : s
+mkRatReduce = do pair; pairToRational; map reduce
 
 instance {-# OVERLAPPABLE #-} ( LorentzRational r
          , Unwrappabled r ~ (a, Natural)
diff --git a/src/Lorentz/Doc.hs b/src/Lorentz/Doc.hs
--- a/src/Lorentz/Doc.hs
+++ b/src/Lorentz/Doc.hs
@@ -76,7 +76,6 @@
   , unsafeConcreteTypeDocHaskellRep
   , haskellAddNewtypeField
   , haskellRepNoFields
-  , haskellRepStripFieldPrefix
   , homomorphicTypeDocMichelsonRep
   , concreteTypeDocMichelsonRep
   , unsafeConcreteTypeDocMichelsonRep
@@ -84,7 +83,7 @@
   ) where
 
 import Data.Typeable (typeRep)
-import Fmt (Buildable(..), Builder, pretty)
+import Fmt (Buildable(..), Doc, pretty)
 
 import Lorentz.Base
 import Lorentz.Constraints
@@ -255,7 +254,7 @@
 
 -- | Helper typeclass to renders information about view interface.
 class RenderViewsImpl (vs :: [ViewTyInfo]) where
-  renderViewsDocImpl :: Proxy vs -> Builder
+  renderViewsDocImpl :: Proxy vs -> Doc
 
 instance RenderViewsImpl '[] where
   renderViewsDocImpl _ = mempty
@@ -293,7 +292,7 @@
   viewsDescriptorName _ = toText $ symbolVal (Proxy @(GenericTypeName vd))
     where _reallyNeedGenerics = Dict @(Generic vd)
 
-  renderViewsDescriptorDoc :: Proxy vd -> Builder
+  renderViewsDescriptorDoc :: Proxy vd -> Doc
   renderViewsDescriptorDoc _ =
     "Contract having this type must contain the following views:\n"
     <> renderViewsDocImpl (Proxy @(RevealViews vd))
diff --git a/src/Lorentz/Entrypoints/Core.hs b/src/Lorentz/Entrypoints/Core.hs
--- a/src/Lorentz/Entrypoints/Core.hs
+++ b/src/Lorentz/Entrypoints/Core.hs
@@ -193,7 +193,7 @@
 -- like 'GetParameterEpDerivation' does.
 pepCall
   :: forall cp name.
-     (ParameterDeclaresEntrypoints cp, ParameterScope (ToT cp))
+     (ParameterDeclaresEntrypoints cp)
   => Label name
   -> EpConstructionRes (ToT cp) (Eval (LookupParameterEntrypoint cp name))
 pepCall = epdCall @(GetParameterEpDerivation cp) @cp
diff --git a/src/Lorentz/Entrypoints/Doc.hs b/src/Lorentz/Entrypoints/Doc.hs
--- a/src/Lorentz/Entrypoints/Doc.hs
+++ b/src/Lorentz/Entrypoints/Doc.hs
@@ -55,7 +55,7 @@
 import Data.Text qualified as T
 import Data.Vinyl.Core (RMap)
 import Fcf (IsJust, type (@@))
-import Fmt (Buildable(..), build, fmt, listF)
+import Fmt (Buildable(..), build, fmt, listF, singleLineF)
 import GHC.Generics ((:+:))
 import GHC.Generics qualified as G
 
@@ -68,7 +68,6 @@
 import Lorentz.Entrypoints.Helpers
 import Lorentz.Entrypoints.Impl
 import Morley.Michelson.Printer (printTypedValue)
-import Morley.Michelson.Printer.Util (RenderDoc(..), needsParens, printDocB)
 import Morley.Michelson.Typed (EpName, ToT, mkUType, pattern DefEpName, sampleTypedValue, sing)
 import Morley.Michelson.Typed qualified as T
 import Morley.Michelson.Typed.Haskell.Doc
@@ -77,9 +76,9 @@
 import Morley.Util.Label (Label)
 import Morley.Util.Markdown
 import Morley.Util.Type
+import Morley.Util.Typeable
 import Morley.Util.TypeLits
 import Morley.Util.TypeTuple
-import Morley.Util.Typeable
 
 -- | Gathers information about single entrypoint.
 --
@@ -294,9 +293,6 @@
 instance Buildable ParamBuilder where
   build = pbSample
 
-instance Eq ParamBuilder where
-  (==) = (==) `on` pbSample
-
 data ParamBuildingDesc = ParamBuildingDesc
   { pbdEnglish :: Markdown
     -- ^ Plain english description of this step.
@@ -304,7 +300,7 @@
     -- ^ How to construct parameter in Haskell code.
   , pbdMichelson :: ParamBuilder
     -- ^ How to construct parameter working on raw Michelson.
-  } deriving stock (Eq)
+  }
 
 -- | Describes a parameter building step.
 --
@@ -327,7 +323,6 @@
     -- It contains dummy 'ParamBuildingStep's which were assigned before
     -- entrypoints were taken into account.
   | PbsUncallable [ParamBuildingStep]
-  deriving stock (Eq)
 
 instance Buildable ParamBuildingStep where
   build = \case
@@ -417,8 +412,7 @@
                   (typeDocMdReference dty (WithinParens False))
               , "  + " <>
                 mdSubsection "In Michelson"
-                  (mdTicked $ printDocB False . renderDoc needsParens $
-                     T.untypeDemoteT @(T.ToT ep))
+                  (mdTicked $ singleLineF $ T.untypeDemoteT @(T.ToT ep))
               , fromMaybe "" $ sampleTypedValue (sing @(ToT ep)) <&> \sampleVal ->
                 "    + " <>
                 mdSubsection "Example"
diff --git a/src/Lorentz/Entrypoints/Impl.hs b/src/Lorentz/Entrypoints/Impl.hs
--- a/src/Lorentz/Entrypoints/Impl.hs
+++ b/src/Lorentz/Entrypoints/Impl.hs
@@ -15,7 +15,6 @@
   , BuildEPTree
   ) where
 
-import Data.Singletons (withSingI)
 import Data.Vinyl.Core (Rec(..), (<+>))
 import Data.Vinyl.Recursive (rmap)
 import Fcf (Eval, Exp)
@@ -261,15 +260,14 @@
         (ynotes, yann) = gMkEntrypointsNotes @mode @epy @y
     in (NTOr noAnn xann yann xnotes ynotes, noAnn)
   gMkEpLiftSequence label =
-    case sing @(GValueType (x G.:+: y)) of
-      STOr sl sr -> withSingI sl $ withSingI sr $ case (checkOpPresence sl, checkNestedBigMapsPresence sl) of
-        (OpAbsent, NestedBigMapsAbsent) ->
-          case gMkEpLiftSequence @mode @epx @x label of
-            EpConstructed liftSeq -> EpConstructed (EplWrapLeft liftSeq)
-            EpConstructionFailed ->
-              case gMkEpLiftSequence @mode @epy @y label of
-                EpConstructed liftSeq -> EpConstructed (EplWrapRight liftSeq)
-                EpConstructionFailed -> EpConstructionFailed
+    withDeMorganScope @ForbidOp @'TOr @(GValueType x) @(GValueType y) $
+    withDeMorganScope @ForbidNestedBigMaps @'TOr @(GValueType x) @(GValueType y) $
+      case gMkEpLiftSequence @mode @epx @x label of
+        EpConstructed liftSeq -> EpConstructed (EplWrapLeft liftSeq)
+        EpConstructionFailed ->
+          case gMkEpLiftSequence @mode @epy @y label of
+            EpConstructed liftSeq -> EpConstructed (EplWrapRight liftSeq)
+            EpConstructionFailed -> EpConstructionFailed
   gMkDescs =
     gMkDescs @mode @epx @x <+> gMkDescs @mode @epy @y
 
diff --git a/src/Lorentz/Errors.hs b/src/Lorentz/Errors.hs
--- a/src/Lorentz/Errors.hs
+++ b/src/Lorentz/Errors.hs
@@ -69,8 +69,8 @@
 import Morley.Util.Markdown
 import Morley.Util.MismatchError
 import Morley.Util.Type
-import Morley.Util.TypeLits
 import Morley.Util.Typeable
+import Morley.Util.TypeLits
 
 ----------------------------------------------------------------------------
 -- IsError
@@ -319,7 +319,7 @@
 deriving stock instance Eq (CustomErrorRep tag) => Eq (CustomError tag)
 deriving stock instance Show (CustomErrorRep tag) => Show (CustomError tag)
 
-instance Buildable (CustomError tag) where
+instance {-# overlappable #-} Buildable (CustomError tag) where
   build (CustomError tg _err) = "CustomError #" +| build tg
 
 -- | To be used as @ErrorArg@ instance when failing with just
diff --git a/src/Lorentz/Instr.hs b/src/Lorentz/Instr.hs
--- a/src/Lorentz/Instr.hs
+++ b/src/Lorentz/Instr.hs
@@ -917,8 +917,8 @@
 -- | Like 'update', but throw an error on attempt to overwrite existing entry.
 updateNew
   :: forall c k s e.
-     ( UpdOpHs c, MemOpHs c, GetOpHs c
-     , k ~ UpdOpKeyHs c, k ~ MemOpKeyHs c, k ~ GetOpKeyHs c
+     ( UpdOpHs c, GetOpHs c
+     , k ~ UpdOpKeyHs c, k ~ GetOpKeyHs c
      , KnownValue (GetOpValHs c), NiceConstant e, Dupable k
      )
   => (forall s0. k : s0 :-> e : s0)
diff --git a/src/Lorentz/Macro.hs b/src/Lorentz/Macro.hs
--- a/src/Lorentz/Macro.hs
+++ b/src/Lorentz/Macro.hs
@@ -138,8 +138,7 @@
 import Prelude hiding (and, compare, drop, some, swap, view)
 
 import Data.Constraint (Bottom(..))
-import Fmt (Buildable(..), Builder, pretty, tupleF, (+|), (|+))
-import Fmt.Internal.Tuple (TupleF)
+import Fmt (Buildable(..), Doc, TupleF(..), pretty, (+|), (|+))
 import GHC.TypeLits qualified as Lit
 import GHC.TypeNats (Nat, type (*), type (+), type (-))
 
@@ -796,7 +795,7 @@
   } deriving stock (Eq, Show, Generic)
     deriving anyclass (HasAnnotation)
 
-deriving anyclass instance (HasNoOpToT r, HasNoNestedBigMaps (ToT r), WellTypedToT a)
+deriving anyclass instance (HasNoOpToT r, ForbidNestedBigMaps (ToT r), WellTypedToT a)
   => IsoValue (View_ a r)
 
 instance (CanCastTo a1 a2, CanCastTo r1 r2) => CanCastTo (View_ a1 r1) (View_ a2 r2)
@@ -819,17 +818,17 @@
   typeDocMichelsonRep =
     concreteTypeDocMichelsonRep @(View_ MText Integer)
 
-instance {-# OVERLAPPABLE #-} (Buildable a, HasNoOpToT r, HasNoNestedBigMaps (ToT r))
+instance {-# OVERLAPPABLE #-} (Buildable a, HasNoOpToT r, ForbidNestedBigMaps (ToT r))
   => Buildable (View_ a r) where
   build = buildView_ build
 
-instance {-# OVERLAPPING  #-} (HasNoOpToT r, HasNoNestedBigMaps (ToT r)) => Buildable (View_ () r) where
+instance {-# OVERLAPPING  #-} (HasNoOpToT r, ForbidNestedBigMaps (ToT r)) => Buildable (View_ () r) where
   build = buildView_ $ const "()"
 
-buildViewTuple_ :: (HasNoOpToT r, HasNoNestedBigMaps (ToT r), TupleF a) => View_ a r -> Builder
+buildViewTuple_ :: (HasNoOpToT r, ForbidNestedBigMaps (ToT r), TupleF a) => View_ a r -> Doc
 buildViewTuple_ = buildView_ tupleF
 
-buildView_ :: (HasNoOpToT r, HasNoNestedBigMaps (ToT r)) => (a -> Builder) -> View_ a r -> Builder
+buildView_ :: (HasNoOpToT r, ForbidNestedBigMaps (ToT r)) => (a -> Doc) -> View_ a r -> Doc
 buildView_ bfp (View_ {..}) =
   "(View param: " +| bfp viewParam |+ " callbackTo: " +| viewCallbackTo |+ ")"
 
@@ -1023,9 +1022,9 @@
 
 -- | Retain the value if it is not equal to the given one.
 --
--- >>> non 0 -$ 5
+-- >>> non (0 :: Integer) -$ 5
 -- Just 5
--- >>> non 0 -$ 0
+-- >>> non (0 :: Integer) -$ 0
 -- Nothing
 non
   :: (NiceConstant a, NiceComparable a)
@@ -1034,9 +1033,9 @@
 
 -- | Version of 'non' with a custom predicate.
 --
--- >>> non' eq0 -$ 5
+-- >>> non' @Integer eq0 -$ 5
 -- Just 5
--- >>> non' eq0 -$ 0
+-- >>> non' @Integer eq0 -$ 0
 -- Nothing
 non'
   :: (NiceConstant a)
diff --git a/src/Lorentz/Referenced.hs b/src/Lorentz/Referenced.hs
--- a/src/Lorentz/Referenced.hs
+++ b/src/Lorentz/Referenced.hs
@@ -42,7 +42,6 @@
 -- >>> import Lorentz
 -- >>> import Lorentz.Zip (zipInstr)
 -- >>> import Fmt (pretty, Buildable(..))
--- >>> instance Buildable () where build () = "()"
 
 -- Errors
 ----------------------------------------------------------------------------
diff --git a/src/Lorentz/Run/Simple.hs b/src/Lorentz/Run/Simple.hs
--- a/src/Lorentz/Run/Simple.hs
+++ b/src/Lorentz/Run/Simple.hs
@@ -57,7 +57,7 @@
 -- 5
 -- >>> sub -$ 3 ::: 2 :: Integer
 -- 1
--- >>> push 9 -$ ZSNil
+-- >>> push (9 :: Integer) -$ ZSNil
 -- 9
 -- >>> add # add -$ 1 ::: 2 ::: 3 :: Integer
 -- 6