-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- TODO [#712]: Remove this next major release
{-# OPTIONS_GHC -Wno-deprecations #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module Morley.Michelson.Typed.Convert
  ( convertParamNotes
  , convertView
  , convertSomeView
  , convertContractCode
  , convertContract
  , instrToOps
  , instrToOpsOptimized
  , untypeDemoteT
  , untypeValue
  , untypeValueHashable
  , untypeValueOptimized

  -- Helper for generating documentation
  , sampleTypedValue

  -- * Misc
  , flattenEntrypoints
  ) where

import Data.ByteArray qualified as ByteArray
import Data.Constraint (Dict(..), (\\))
import Data.List.NonEmpty ((<|))
import Data.Map qualified as Map
import Data.Singletons (Sing, demote, withSingI)
import Data.Vinyl (Rec(..))
import Fmt (Buildable(..), Builder, blockListF, fmt, indentF, listF, pretty, unlinesF)
import Text.PrettyPrint.Leijen.Text (Doc)
import Unsafe qualified (fromIntegral)

import Morley.Michelson.Printer.Util
import Morley.Michelson.Text
import Morley.Michelson.Typed.Aliases
import Morley.Michelson.Typed.Annotation (Notes(..), mkUType)
import Morley.Michelson.Typed.Contract
import Morley.Michelson.Typed.Entrypoints
import Morley.Michelson.Typed.Extract (toUType)
import Morley.Michelson.Typed.Instr as Instr
import Morley.Michelson.Typed.Scope
import Morley.Michelson.Typed.Sing (SingT(..))
import Morley.Michelson.Typed.T (T(..))
import Morley.Michelson.Typed.Value
import Morley.Michelson.Typed.View
import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Annotation (Annotation(unAnnotation))
import Morley.Tezos.Address (Address(..), ContractHash(..))
import Morley.Tezos.Core
  (ChainId(unChainId), mformatChainId, parseChainId, timestampFromSeconds, timestampToSeconds, tz,
  unMutez)
import Morley.Tezos.Crypto
import Morley.Tezos.Crypto.BLS12381 qualified as BLS
import Morley.Tezos.Crypto.Ed25519 qualified as Ed25519
import Morley.Tezos.Crypto.P256 qualified as P256
import Morley.Tezos.Crypto.Secp256k1 qualified as Secp256k1
import Morley.Tezos.Crypto.Timelock (chestBytes, chestKeyBytes)
import Morley.Util.PeanoNatural (fromPeanoNatural, singPeanoVal)
import Morley.Util.Sing (eqParamSing)

-- | Convert typed parameter annotations to an untyped 'U.ParameterType'.
convertParamNotes :: ParamNotes cp -> U.ParameterType
convertParamNotes (ParamNotes notes rootAnn) =
  U.ParameterType (mkUType notes) rootAnn

-- | Convert typed 'ContractCode' to an untyped t'U.Contract'.
convertContractCode
  :: forall param store . (SingI param, SingI store)
  => ContractCode param store -> U.Contract
convertContractCode contract =
  U.Contract
    { contractParameter = U.ParameterType (untypeDemoteT @param) U.noAnn
    , contractStorage = untypeDemoteT @store
    , contractCode = instrToOps contract
    , entriesOrder = U.canonicalEntriesOrder
    , contractViews = []
    }

convertView :: forall arg store ret. View arg store ret -> U.View
convertView View{..} =
  U.View
    { viewName = vName
    , viewArgument = untypeDemoteT @arg
    , viewReturn = untypeDemoteT @ret
    , viewCode = instrToOps vCode
    }

convertSomeView :: SomeView st -> U.View
convertSomeView (SomeView v) = convertView v

-- | Convert typed t'Contract' to an untyped t'U.Contract'.
convertContract :: Contract param store -> U.Contract
convertContract fc@Contract{} =
  let c = convertContractCode (cCode fc)
  in c { U.contractParameter = convertParamNotes (cParamNotes fc)
       , U.contractStorage = mkUType (cStoreNotes fc)
       , U.entriesOrder = cEntriesOrder fc
       , U.contractViews = convertSomeView <$> toList (cViews fc)
       }

-- Note: if you change this type, check 'untypeValueImpl' wildcard patterns.
data UntypingOptions
  = Readable
  -- ^ Convert value to human-readable representation
  | Optimized
  -- ^ Convert value to optimized representation
  | Hashable
  -- ^ Like 'Optimized', but without list notation for pairs.
  -- Created to match 'tezos-client hash data' behavior for typed values.
  -- See https://gitlab.com/morley-framework/morley/-/issues/611
  deriving stock (Eq, Show)

-- | Convert a typed value to an untyped human-readable representation
untypeValue :: HasNoOp t => Value' Instr t -> U.Value
untypeValue = untypeValueImpl' Readable

-- | Like 'untypeValueOptimized', but without list notation for pairs.
--
-- Created to match @tezos-client hash data@ behaviour for typed values.
untypeValueHashable :: HasNoOp t => Value' Instr t -> U.Value
untypeValueHashable = untypeValueImpl' Hashable

-- | Convert a typed value to an untyped optimized representation
untypeValueOptimized :: HasNoOp t => Value' Instr t -> U.Value
untypeValueOptimized = untypeValueImpl' Optimized

untypeValueImpl'
  :: HasNoOp t
  => UntypingOptions
  -> Value' Instr t
  -> U.Value
untypeValueImpl' opts val = untypeValueImpl opts (sing \\ valueTypeSanity val) val

-- | Convert a typed t'Morley.Michelson.Typed.Aliases.Value' to an untyped 'Value'.
--
-- For full isomorphism type of the given t'Morley.Michelson.Typed.Aliases.Value' should not contain
-- 'TOperation' - a compile error will be raised otherwise.
-- You can analyse its presence with 'checkOpPresence' function.
untypeValueImpl
  :: HasNoOp t
  => UntypingOptions
  -> Sing t
  -> Value' Instr t
  -> U.Value
untypeValueImpl opts sng val = case (val, sng) of
  (VInt i, _) -> U.ValueInt i
  (VNat i, _) -> U.ValueInt $ toInteger i
  (VString s, _) -> U.ValueString s
  (VBytes b, _) -> U.ValueBytes $ U.InternalByteString b
  (VMutez m, _) -> U.ValueInt $ toInteger $ unMutez m
  (VBool True, _) -> U.ValueTrue
  (VBool False, _) -> U.ValueFalse
  (VKeyHash h, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatKeyHash h
      _         -> U.ValueBytes $ U.InternalByteString $ keyHashToBytes h
  (VBls12381Fr v, _) ->
    case opts of
      Readable  -> U.ValueInt $ toInteger v
      _         -> U.ValueBytes . U.InternalByteString $ BLS.toMichelsonBytes v
  (VBls12381G1 v, _) ->
    U.ValueBytes . U.InternalByteString $ BLS.toMichelsonBytes v
  (VBls12381G2 v, _) ->
    U.ValueBytes . U.InternalByteString $ BLS.toMichelsonBytes v
  (VTimestamp t, _) ->
    case opts of
      Readable   -> U.ValueString . unsafe . mkMText $ pretty t
      _          -> U.ValueInt $ timestampToSeconds t
  (VAddress a, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatEpAddress a
      _         -> U.ValueBytes . U.InternalByteString  $ encodeEpAddress a
  (VKey b, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatPublicKey b
      _         -> U.ValueBytes . U.InternalByteString $ keyToBytes b
  (VUnit, _) ->
    U.ValueUnit
  (VSignature b, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatSignature b
      _         -> U.ValueBytes . U.InternalByteString $ signatureToBytes b
  (VChainId b, _) ->
    case opts of
      Readable  -> U.ValueString $ mformatChainId b
      _         ->
        U.ValueBytes . U.InternalByteString $ ByteArray.convert (unChainId b)
  (VOption (Just x), STOption op) ->
    U.ValueSome (untypeValueImpl opts op x)
  (VOption Nothing, STOption _) ->
    U.ValueNone
  (VList l, STList lt) ->
    vList U.ValueSeq $ map (untypeValueImpl opts lt) l
  (VSet s, STSet st) ->
    case checkOpPresence st of
      OpAbsent -> vList U.ValueSeq $ map (untypeValueImpl opts st) $ toList s
  (VContract addr sepc, _) ->
    case opts of
      Readable  ->
        U.ValueString . mformatEpAddress $ EpAddress addr (sepcName sepc)
      _         -> U.ValueBytes . U.InternalByteString . encodeEpAddress $
        EpAddress addr (sepcName sepc)
  (VChest c, _) -> U.ValueBytes . U.InternalByteString $ chestBytes c
  (VChestKey c, _) -> U.ValueBytes . U.InternalByteString $ chestKeyBytes c
  (VTicket s v a, STTicket vt) ->
    case valueTypeSanity v of
      Dict ->
        let us = untypeValueImpl opts STAddress $ VAddress (EpAddress s DefEpName)
            uv = untypeValueImpl opts vt v
            ua = untypeValueImpl opts STNat $ VNat a
        in case opts of
          Optimized -> U.ValueSeq $ us :| [uv, ua]
          _         -> U.ValuePair us (U.ValuePair uv ua)
  p@(VPair (l, r), STPair lt rt) ->
    case checkOpPresence lt of
      OpAbsent -> case opts of
        Optimized -> U.ValueSeq $ pairToSeq p
        _         -> U.ValuePair (untypeValueImpl opts lt l) (untypeValueImpl opts rt r)

  (VOr (Left x), STOr lt _) ->
    case checkOpPresence lt of
      OpAbsent -> U.ValueLeft (untypeValueImpl opts lt x)

  (VOr (Right x), STOr lt rt) ->
    case checkOpPresence lt of
      OpAbsent -> U.ValueRight (untypeValueImpl opts rt x)

  (VLam (rfAnyInstr -> ops), _) ->
    vList U.ValueLambda $ instrToOpsImpl opts ops

  (VMap m, STMap kt vt) ->
    case (checkOpPresence kt, checkOpPresence vt) of
      (OpAbsent, OpAbsent) ->
        vList U.ValueMap $ Map.toList m <&> \(k, v) ->
        U.Elt (untypeValueImpl opts kt k) (untypeValueImpl opts vt v)

  (VBigMap _ m, STBigMap kt vt) ->
    case (checkOpPresence kt, checkOpPresence vt) of
      (OpAbsent, OpAbsent) ->
        vList U.ValueMap $ Map.toList m <&> \(k, v) ->
        U.Elt (untypeValueImpl opts kt k) (untypeValueImpl opts vt v)
  where
    vList ctor = maybe U.ValueNil ctor . nonEmpty

    pairToSeq :: HasNoOp ty
              => (Value ty, Sing ty)
              -> NonEmpty U.Value
    pairToSeq = \case
      (VPair (a, b), STPair l r) -> case checkOpPresence l of
        OpAbsent -> untypeValueImpl opts l a <| pairToSeq (b, r)
      (v, vt) -> untypeValueImpl opts vt v :| []

    keyHashToBytes :: KeyHash -> ByteString
    keyHashToBytes kh = (<> (khBytes kh)) $
      case khTag kh of
        KeyHashEd25519 -> "\x00"
        KeyHashSecp256k1 -> "\x01"
        KeyHashP256 -> "\x02"

    keyToBytes :: PublicKey -> ByteString
    keyToBytes = \case
      PublicKeyEd25519 pk -> "\x00" <> Ed25519.publicKeyToBytes pk
      PublicKeySecp256k1 pk -> "\x01" <> Secp256k1.publicKeyToBytes pk
      PublicKeyP256 pk -> "\x02" <> P256.publicKeyToBytes pk

    encodeEpAddress :: EpAddress -> ByteString
    encodeEpAddress (EpAddress addr epName) =
      encodeAddress addr <> encodeEpName epName

    encodeAddress :: Address -> ByteString
    encodeAddress = \case
      KeyAddress keyHash ->
        "\x00" <> keyHashToBytes keyHash
      ContractAddress (ContractHash address) ->
        "\x01" <> address <> "\x00"

    encodeEpName :: EpName -> ByteString
    encodeEpName = encodeUtf8 . unAnnotation . epNameToRefAnn . canonicalize
      where
        canonicalize :: EpName -> EpName
        canonicalize (UnsafeEpName "default") = DefEpName
        canonicalize epName                   = epName

-- | Convert a Haskell type-level type tag into an
-- untyped value representation.
--
-- This function is intended to be used with @TypeApplications@.
untypeDemoteT :: forall (t :: T). SingI t => U.Ty
untypeDemoteT = toUType $ demote @t

-- | Convert Haskell-typed 'Instr' to a list of optimized untyped operations
instrToOpsOptimized :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOpsOptimized = instrToOpsImpl Optimized

-- | Convert Haskell-typed 'Instr' to a list of human-readable untyped operations
instrToOps :: HasCallStack => Instr inp out -> [U.ExpandedOp]
instrToOps = instrToOpsImpl Readable

instrToOpsImpl :: HasCallStack
               => UntypingOptions
               -> Instr inp out
               -> [U.ExpandedOp]
instrToOpsImpl opts = \case
  Nop -> []
  Seq i1 i2 -> instrToOpsImpl opts i1 <> instrToOpsImpl opts i2
  Nested sq -> one $ U.SeqEx $ instrToOps sq
  DocGroup _ sq -> instrToOpsImpl opts sq
  Fn t sfn i -> [U.PrimEx . U.EXT . U.FN t sfn $ instrToOps i]
  Ext (ext :: ExtInstr inp) -> (U.PrimEx . U.EXT) <$> extInstrToOps ext
  FrameInstr _ i -> instrToOpsImpl opts i
  -- TODO [#283] After representation of locations is polished,
  -- this place should be updated to pass it from typed to untyped ASTs.
  WithLoc _ i -> instrToOpsImpl opts i
  Meta _ i -> instrToOpsImpl opts i
  InstrWithVarAnns _ i -> instrToOpsImpl opts i
  InstrWithNotes proxy n i -> case i of
    Nop -> instrToOpsImpl opts i
    Seq _ _ -> instrToOpsImpl opts i
    Nested _ -> instrToOpsImpl opts i
    DocGroup _ _ -> instrToOpsImpl opts i
    Ext _ -> instrToOpsImpl opts i
    WithLoc _ i0 -> instrToOpsImpl opts (InstrWithNotes proxy n i0)
    Meta _ i0 -> instrToOpsImpl opts (InstrWithNotes proxy n i0)
    InstrWithNotes {} -> instrToOpsImpl opts i
    -- For inner instruction, filter out values that we don't want to apply
    -- annotations to and delegate it's conversion to this function itself.
    -- If none of the above, convert a single instruction and copy annotations
    -- to it.
    InstrWithVarNotes n0 (InstrWithVarAnns _ i0) ->
      instrToOpsImpl opts $ InstrWithNotes proxy n $ InstrWithVarNotes n0 i0
    InstrWithVarNotes n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n n0]
    InstrWithVarAnns _ _ -> instrToOpsImpl opts i
    _ -> [U.PrimEx $ handleInstrAnnotate i n]
  InstrWithVarNotes n i -> case i of
    Nop -> instrToOpsImpl opts i
    Seq _ _ -> instrToOpsImpl opts i
    Nested _ -> instrToOpsImpl opts i
    DocGroup _ _ -> instrToOpsImpl opts i
    Ext _ -> instrToOpsImpl opts i
    WithLoc _ i0 -> instrToOpsImpl opts (InstrWithVarNotes n i0)
    Meta _ i0 -> instrToOpsImpl opts (InstrWithVarNotes n i0)
    InstrWithNotes p0 n0 (InstrWithVarAnns _ i0) ->
      instrToOpsImpl opts $ InstrWithNotes p0 n0 $ InstrWithVarNotes n i0
    InstrWithNotes _ n0 i0 -> [U.PrimEx $ handleInstrAnnotateWithVarNotes i0 n0 n]
    InstrWithVarNotes _ _ -> instrToOpsImpl opts i
    InstrWithVarAnns _ i0 -> instrToOpsImpl opts $ InstrWithVarNotes n i0
    _ -> [U.PrimEx $ handleInstrVarNotes i n]
  i -> [U.PrimEx $ handleInstr i]
  where
    handleInstrAnnotateWithVarNotes
      :: forall inp' out' topElems . HasCallStack
      => Instr inp' out'
      -> Rec Notes topElems
      -> NonEmpty U.VarAnn
      -> U.ExpandedInstr
    handleInstrAnnotateWithVarNotes instr notes varAnns =
      addVarNotes (addInstrNote (handleInstr instr) notes) varAnns

    handleInstrAnnotate
      :: forall inp' out' topElems. HasCallStack
      => Instr inp' out' -> Rec Notes topElems -> U.ExpandedInstr
    handleInstrAnnotate ins' notes =
      addInstrNote (handleInstr ins') notes

    addInstrNote
      :: forall topElems. HasCallStack
      => U.ExpandedInstr -> Rec Notes topElems -> U.ExpandedInstr
    addInstrNote instr notes =
      case (instr, notes) of
        (U.PUSH va _ v, notes' :& _) -> U.PUSH va (mkUType notes') v
        (U.SOME _ va, NTOption ta _ :& _) -> U.SOME ta va
        (U.NONE _ va _, (NTOption ta nt :: Notes t) :& _) ->
          U.NONE ta va $ mkUType nt
        (U.UNIT _ va, NTUnit ta :& _) -> U.UNIT ta va
        (U.PAIRN va n, _) -> U.PAIRN va n
        (U.LEFT ta va fa1 fa2 _, (NTOr _ _ _ _ n2 :: Notes t) :& _) ->
          U.LEFT ta va fa1 fa2 $ mkUType n2
        (U.RIGHT ta va fa1 fa2 _, (NTOr _ _ _ n1 _ :: Notes t) :& _) ->
          U.RIGHT ta va fa1 fa2 $ mkUType n1
        (U.NIL _ va _, (NTList ta n :: Notes t) :& _) ->
          U.NIL ta va $ mkUType n
        (U.EMPTY_SET _ va _, (NTSet ta1 n :: Notes t) :& _) ->
          U.EMPTY_SET ta1 va $ mkUType n
        (U.EMPTY_MAP _ va _ _, (NTMap ta1 k n :: Notes t) :& _) ->
          U.EMPTY_MAP ta1 va (mkUType k) (mkUType n)
        (U.EMPTY_BIG_MAP _ va _ _, (NTBigMap ta1 k n :: Notes t) :& _) ->
          U.EMPTY_BIG_MAP ta1 va (mkUType k) (mkUType n)
        (U.LAMBDA va _ _ ops, (NTLambda _ n1 n2 :: Notes t) :& _) ->
          U.LAMBDA va (mkUType n1) (mkUType n2) ops
        (U.CAST va _, n :& _) -> U.CAST va (mkUType n)
        (U.UNPACK _ va _, (NTOption ta nt :: Notes t) :& _) ->
          U.UNPACK ta va (mkUType nt)
        (U.CONTRACT va fa _, (NTOption _ (NTContract _ nt :: Notes t) :: Notes t2) :& _) ->
          U.CONTRACT va fa (mkUType nt)
        (U.CONTRACT va fa t, NTOption _ _ :& _) -> U.CONTRACT va fa t
        (U.CAR {}, _) -> instr
        (U.CDR {}, _) -> instr
        (U.PAIR {}, _) -> instr
        (U.UNPAIR {}, _) -> instr
        (U.APPLY {}, _) -> instr
        (U.CHAIN_ID {}, _) -> instr
        (U.EXT _, _) -> instr
        (U.DROP, _) -> instr
        (U.DROPN _, _) -> instr
        (U.DUP _, _) -> instr
        (U.DUPN _ _, _) -> instr
        (U.SWAP, _) -> instr
        (U.DIG {}, _) -> instr
        (U.DUG {}, _) -> instr
        (U.IF_NONE _ _, _) -> instr
        (U.CONS _, _) -> instr
        (U.IF_LEFT _ _, _) -> instr
        (U.IF_CONS _ _, _) -> instr
        (U.SIZE _, _) -> instr
        (U.MAP _ _, _) -> instr
        (U.ITER _, _) -> instr
        (U.MEM _, _) -> instr
        (U.GET _, _) -> instr
        (U.GETN _ _, _) -> instr
        (U.UPDATE _, _) -> instr
        (U.UPDATEN _ _, _) -> instr
        (U.GET_AND_UPDATE _, _) -> instr
        (U.IF _ _, _) -> instr
        (U.LOOP _, _) -> instr
        (U.LOOP_LEFT _, _) -> instr
        (U.EXEC _, _) -> instr
        (U.DIP _, _) -> instr
        (U.DIPN {}, _) -> instr
        (U.FAILWITH, _) -> instr
        (U.RENAME _, _) -> instr
        (U.PACK _, _) -> instr
        (U.CONCAT _, _) -> instr
        (U.SLICE _, _) -> instr
        (U.ISNAT _, _) -> instr
        (U.ADD _, _) -> instr
        (U.SUB _, _) -> instr
        (U.SUB_MUTEZ _, _) -> instr
        (U.MUL _, _) -> instr
        (U.EDIV _, _) -> instr
        (U.ABS _, _) -> instr
        (U.NEG _, _) -> instr
        (U.LSL _, _) -> instr
        (U.LSR _, _) -> instr
        (U.OR _, _) -> instr
        (U.AND _, _) -> instr
        (U.XOR _, _) -> instr
        (U.NOT _, _) -> instr
        (U.COMPARE _, _) -> instr
        (U.EQ _, _) -> instr
        (U.NEQ _, _) -> instr
        (U.LT _, _) -> instr
        (U.GT _, _) -> instr
        (U.LE _, _) -> instr
        (U.GE _, _) -> instr
        (U.INT _, _) -> instr
        (U.VIEW{}, _) -> instr
        (U.SELF _ _, _) -> instr
        (U.TRANSFER_TOKENS _, _) -> instr
        (U.SET_DELEGATE _, _) -> instr
        (U.CREATE_CONTRACT {}, _) -> instr
        (U.IMPLICIT_ACCOUNT _, _) -> instr
        (U.NOW _, _) -> instr
        (U.LEVEL _, _) -> instr
        (U.AMOUNT _, _) -> instr
        (U.BALANCE _, _) -> instr
        (U.VOTING_POWER _, _) -> instr
        (U.TOTAL_VOTING_POWER _, _) -> instr
        (U.CHECK_SIGNATURE _, _) -> instr
        (U.SHA256 _, _) -> instr
        (U.SHA512 _, _) -> instr
        (U.BLAKE2B _, _) -> instr
        (U.SHA3 _, _) -> instr
        (U.KECCAK _, _) -> instr
        (U.HASH_KEY _, _) -> instr
        (U.SOURCE _, _) -> instr
        (U.SENDER _, _) -> instr
        (U.ADDRESS _, _) -> instr
        (U.SELF_ADDRESS _, _) -> instr
        (U.NEVER, _) -> instr
        (U.TICKET _, _) -> instr
        (U.READ_TICKET _, _) -> instr
        (U.SPLIT_TICKET _, _) -> instr
        (U.JOIN_TICKETS _, _) -> instr
        _ -> error $ pretty $ unlinesF
          [ "addInstrNote: Unexpected instruction/annotation combination"
          , "Instruction:"
          , indentF 2 $ build instr
          , "Annotations:"
          , indentF 2 $ blockListF $ buildNotes notes
          ]
          where
            buildNotes :: Rec Notes ts -> [Builder]
            buildNotes = \case
              RNil -> []
              n :& ns -> build n : buildNotes ns

    handleInstrVarNotes :: forall inp' out' . HasCallStack
      => Instr inp' out' -> NonEmpty U.VarAnn -> U.ExpandedInstr
    handleInstrVarNotes ins' varAnns =
      let x = handleInstr ins' in addVarNotes x varAnns

    addVarNotes
      :: HasCallStack
      => U.ExpandedInstr -> NonEmpty U.VarAnn -> U.ExpandedInstr
    addVarNotes ins varNotes = case varNotes of
      va1 :| [va2] -> case ins of
        U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va1 va2 c
        _ -> error $
          "addVarNotes: Cannot add two var annotations to instr: " <> pretty ins
      va :| [] -> case ins of
        U.DUP _ -> U.DUP va
        U.DUPN _ s -> U.DUPN va s
        U.PUSH _ t v -> U.PUSH va t v
        U.SOME ta _ -> U.SOME ta va
        U.NONE ta _ t -> U.NONE ta va t
        U.UNIT ta _ -> U.UNIT ta va
        U.PAIR ta _ fa1 fa2 -> U.PAIR ta va fa1 fa2
        U.PAIRN _ n -> U.PAIRN va n
        U.LEFT ta _ fa1 fa2 t -> U.LEFT ta va fa1 fa2 t
        U.RIGHT ta _ fa1 fa2 t -> U.RIGHT ta va fa1 fa2 t
        U.NIL ta _ t -> U.NIL ta va t
        U.CONS _ -> U.CONS va
        U.SIZE _ -> U.SIZE va
        U.EMPTY_SET ta _ c -> U.EMPTY_SET ta va c
        U.EMPTY_MAP ta _ c t -> U.EMPTY_MAP ta va c t
        U.EMPTY_BIG_MAP ta _ c t -> U.EMPTY_BIG_MAP ta va c t
        U.MAP _ ops -> U.MAP va ops
        U.MEM _ -> U.MEM va
        U.GET _ -> U.GET va
        U.GETN _ n -> U.GETN va n
        U.UPDATE _ -> U.UPDATE va
        U.UPDATEN _ n -> U.UPDATEN va n
        U.GET_AND_UPDATE _ -> U.GET_AND_UPDATE va
        U.LAMBDA _ t1 t2 ops -> U.LAMBDA va t1 t2 ops
        U.EXEC _ -> U.EXEC va
        U.APPLY _ -> U.APPLY va
        U.CAST _ t -> U.CAST va t
        U.RENAME _ -> U.RENAME va
        U.PACK _ -> U.PACK va
        U.UNPACK ta _ t -> U.UNPACK ta va t
        U.CONCAT _ -> U.CONCAT va
        U.SLICE _ -> U.SLICE va
        U.ISNAT _ -> U.ISNAT va
        U.ADD _ -> U.ADD va
        U.SUB _ -> U.SUB va
        U.SUB_MUTEZ _ -> U.SUB_MUTEZ va
        U.MUL _ -> U.MUL va
        U.EDIV _ -> U.EDIV va
        U.ABS _ -> U.ABS va
        U.NEG _ -> U.NEG va
        U.LSL _ -> U.LSL va
        U.LSR _ -> U.LSR va
        U.OR _ -> U.OR va
        U.AND _ -> U.AND va
        U.XOR _ -> U.XOR va
        U.NOT _ -> U.NOT va
        U.COMPARE _ -> U.COMPARE va
        U.EQ _ -> U.EQ va
        U.NEQ _ -> U.NEQ va
        U.LT _ -> U.LT va
        U.GT _ -> U.GT va
        U.LE _ -> U.LE va
        U.GE _ -> U.GE va
        U.INT _ -> U.INT va
        U.VIEW _ n t -> U.VIEW va n t
        U.SELF _ fa -> U.SELF va fa
        U.CONTRACT _ fa t -> U.CONTRACT va fa t
        U.TRANSFER_TOKENS _ -> U.TRANSFER_TOKENS va
        U.SET_DELEGATE _ -> U.SET_DELEGATE va
        U.CREATE_CONTRACT _ _ c -> U.CREATE_CONTRACT va U.noAnn c
        U.IMPLICIT_ACCOUNT _ -> U.IMPLICIT_ACCOUNT va
        U.NOW _ -> U.NOW va
        U.AMOUNT _ -> U.AMOUNT va
        U.BALANCE _ -> U.BALANCE va
        U.VOTING_POWER _ -> U.VOTING_POWER va
        U.TOTAL_VOTING_POWER _ -> U.TOTAL_VOTING_POWER va
        U.CHECK_SIGNATURE _ -> U.CHECK_SIGNATURE va
        U.SHA256 _ -> U.SHA256 va
        U.SHA512 _ -> U.SHA512 va
        U.BLAKE2B _ -> U.BLAKE2B va
        U.SHA3 _ -> U.SHA3 va
        U.KECCAK _ -> U.KECCAK va
        U.HASH_KEY _ -> U.HASH_KEY va
        U.SOURCE _ -> U.SOURCE va
        U.SENDER _ -> U.SENDER va
        U.ADDRESS _ -> U.ADDRESS va
        U.CHAIN_ID _ -> U.CHAIN_ID va
        U.LEVEL _ -> U.LEVEL va
        U.SELF_ADDRESS _ -> U.SELF_ADDRESS va
        U.TICKET _ -> U.TICKET va
        U.READ_TICKET _ -> U.READ_TICKET va
        U.SPLIT_TICKET _ -> U.SPLIT_TICKET va
        U.JOIN_TICKETS _ -> U.JOIN_TICKETS va
        _ -> error $
          "addVarNotes: Cannot add single var annotation to instr: " <> (pretty ins) <> " with " <> pretty va
      _ -> error $
        "addVarNotes: Trying to add more than two var annotations to instr: " <> (pretty ins)

    handleInstr :: HasCallStack => Instr inp out -> U.ExpandedInstr
    handleInstr = \case
      (WithLoc _ _) -> error "impossible"
      InstrWithNotes {} -> error "impossible"
      (InstrWithVarNotes _ _) -> error "impossible"
      (InstrWithVarAnns _ _) -> error "impossible"
      (FrameInstr _ _) -> error "impossible"
      (Seq _ _) -> error "impossible"
      Nop -> error "impossible"
      (Ext _) -> error "impossible"
      (Nested _) -> error "impossible"
      DocGroup{} -> error "impossible"
      Meta _ i -> handleInstr i
      Fn t sfn i -> U.EXT . U.FN t sfn $ instrToOpsImpl opts i
      DROP -> U.DROP
      (DROPN s) -> U.DROPN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
      DUP -> U.DUP U.noAnn
      (DUPN s) -> U.DUPN U.noAnn (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
      SWAP -> U.SWAP
      (DIG s) -> U.DIG (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
      (DUG s) -> U.DUG (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s)
      i@(PUSH val) | _ :: Instr inp1 (t ': s) <- i ->
        let value = untypeValueImpl opts (sing @t) val
        in U.PUSH U.noAnn (untypeDemoteT @t) value
      i@NONE | _ :: Instr inp1 ('TOption a ': inp1) <- i ->
        U.NONE U.noAnn U.noAnn (untypeDemoteT @a)
      SOME -> U.SOME U.noAnn U.noAnn
      UNIT -> U.UNIT U.noAnn U.noAnn
      (IF_NONE i1 i2) -> U.IF_NONE (instrToOpsImpl opts i1) (instrToOpsImpl opts i2)

      -- `AnnUNPAIR` accepts special var anns, so it carries them inside its constructor,
      -- so we can use them here to re-construct an untyped `U.UNPAIR`.
      -- `AnnPAIR`, on the other hand, doesn't accept special var anns, so the var anns
      -- are carried in the `InstrWithVarNotes` meta-instruction instead.
      --
      -- See: Note [Annotations - Exceptional scenarios] in `Morley.Michelson.Typed.Instr`
      --
      -- TODO [#580]
      AnnPAIR tn fn1 fn2 -> U.PAIR tn U.noAnn fn1 fn2
      AnnUNPAIR vn1 vn2 fn1 fn2 -> U.UNPAIR vn1 vn2 fn1 fn2

      PAIRN n -> U.PAIRN U.noAnn (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
      UNPAIRN n -> U.UNPAIRN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
      (AnnCAR vn fn) -> U.CAR vn fn
      (AnnCDR vn fn) -> U.CDR vn fn
      i@(AnnLEFT tn fn1 fn2) | _ :: Instr (a ': s) ('TOr a b ': s) <- i ->
        U.LEFT tn U.noAnn fn1 fn2 (untypeDemoteT @b)
      i@(AnnRIGHT tn fn1 fn2) | _ :: Instr (b ': s) ('TOr a b ': s) <- i ->
        U.RIGHT tn U.noAnn fn1 fn2 (untypeDemoteT @a)
      (IF_LEFT i1 i2) -> U.IF_LEFT (instrToOpsImpl opts i1) (instrToOpsImpl opts i2)
      i@NIL | _ :: Instr s ('TList p ': s) <- i ->
        U.NIL U.noAnn U.noAnn (untypeDemoteT @p)
      CONS -> U.CONS U.noAnn
      (IF_CONS i1 i2) -> U.IF_CONS (instrToOpsImpl opts i1) (instrToOpsImpl opts i2)
      SIZE -> U.SIZE U.noAnn
      i@EMPTY_SET | _ :: Instr s ('TSet e ': s) <- i ->
        U.EMPTY_SET U.noAnn U.noAnn (U.Ty (U.unwrapT $ untypeDemoteT @e) U.noAnn)
      i@EMPTY_MAP | _ :: Instr s ('TMap a b ': s) <- i ->
        U.EMPTY_MAP U.noAnn U.noAnn (U.Ty (U.unwrapT $ untypeDemoteT @a) U.noAnn)
          (untypeDemoteT @b)
      i@EMPTY_BIG_MAP | _ :: Instr s ('TBigMap a b ': s) <- i ->
        U.EMPTY_BIG_MAP U.noAnn U.noAnn (U.Ty (U.unwrapT $ untypeDemoteT @a) U.noAnn)
          (untypeDemoteT @b)
      (MAP op) -> U.MAP U.noAnn $ instrToOpsImpl opts op
      (ITER op) -> U.ITER $ instrToOpsImpl opts op
      MEM -> U.MEM U.noAnn
      GET -> U.GET U.noAnn
      GETN n -> U.GETN U.noAnn (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
      UPDATE -> U.UPDATE U.noAnn
      UPDATEN n -> U.UPDATEN U.noAnn (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural n)
      GET_AND_UPDATE -> U.GET_AND_UPDATE U.noAnn
      (IF op1 op2) -> U.IF (instrToOpsImpl opts op1) (instrToOpsImpl opts op2)
      (LOOP op) -> U.LOOP (instrToOpsImpl opts op)
      (LOOP_LEFT op) -> U.LOOP_LEFT (instrToOpsImpl opts op)
      i@(LAMBDA {}) | LAMBDA (VLam l) :: Instr s ('TLambda i o ': s) <- i ->
        U.LAMBDA U.noAnn (untypeDemoteT @i) (untypeDemoteT @o) (instrToOpsImpl opts $ rfAnyInstr l)
      EXEC -> U.EXEC U.noAnn
      APPLY -> U.APPLY U.noAnn
      (DIP op) -> U.DIP (instrToOpsImpl opts op)
      (DIPN s op) ->
        U.DIPN (Unsafe.fromIntegral @Natural @Word $ fromPeanoNatural s) (instrToOpsImpl opts op)
      FAILWITH -> U.FAILWITH
      i@CAST | _ :: Instr (a ': s) (a ': s) <- i ->
        U.CAST U.noAnn (untypeDemoteT @a)
      RENAME -> U.RENAME U.noAnn
      PACK -> U.PACK U.noAnn
      i@UNPACK
        | _ :: Instr ('TBytes ': s) ('TOption a ': s) <- i ->
            U.UNPACK U.noAnn U.noAnn (untypeDemoteT @a)
      CONCAT -> U.CONCAT U.noAnn
      CONCAT' -> U.CONCAT U.noAnn
      SLICE -> U.SLICE U.noAnn
      ISNAT -> U.ISNAT U.noAnn
      ADD -> U.ADD U.noAnn
      SUB -> U.SUB U.noAnn
      SUB_MUTEZ -> U.SUB_MUTEZ U.noAnn
      MUL -> U.MUL U.noAnn
      EDIV -> U.EDIV U.noAnn
      ABS -> U.ABS U.noAnn
      NEG -> U.NEG U.noAnn
      LSL -> U.LSL U.noAnn
      LSR -> U.LSR U.noAnn
      OR -> U.OR U.noAnn
      AND -> U.AND U.noAnn
      XOR -> U.XOR U.noAnn
      NOT -> U.NOT U.noAnn
      COMPARE -> U.COMPARE U.noAnn
      Instr.EQ -> U.EQ U.noAnn
      NEQ -> U.NEQ U.noAnn
      Instr.LT -> U.LT U.noAnn
      Instr.GT -> U.GT U.noAnn
      LE -> U.LE U.noAnn
      GE -> U.GE U.noAnn
      INT -> U.INT U.noAnn
      VIEW viewName nt -> U.VIEW U.noAnn viewName (mkUType nt)
      SELF sepc ->
        U.SELF U.noAnn (epNameToRefAnn $ sepcName sepc)
      i@(CONTRACT nt epName)
        | _ :: Instr ('TAddress ': s) ('TOption ('TContract p) ': s) <- i ->
            let fa = epNameToRefAnn epName
            in U.CONTRACT U.noAnn fa (mkUType nt)
      TRANSFER_TOKENS -> U.TRANSFER_TOKENS U.noAnn
      SET_DELEGATE -> U.SET_DELEGATE U.noAnn
      i@(CREATE_CONTRACT contract)
        | _ :: Instr
            (  'TOption ('TKeyHash)
            ': 'TMutez
            ': g
            ': s)
            ('TOperation ': 'TAddress ': s) <- i ->
          U.CREATE_CONTRACT U.noAnn U.noAnn (convertContract contract)
      IMPLICIT_ACCOUNT -> U.IMPLICIT_ACCOUNT U.noAnn
      NOW -> U.NOW U.noAnn
      AMOUNT -> U.AMOUNT U.noAnn
      BALANCE -> U.BALANCE U.noAnn
      VOTING_POWER -> U.VOTING_POWER U.noAnn
      TOTAL_VOTING_POWER -> U.TOTAL_VOTING_POWER U.noAnn
      CHECK_SIGNATURE -> U.CHECK_SIGNATURE U.noAnn
      SHA256 -> U.SHA256 U.noAnn
      SHA512 -> U.SHA512 U.noAnn
      BLAKE2B -> U.BLAKE2B U.noAnn
      SHA3 -> U.SHA3 U.noAnn
      KECCAK -> U.KECCAK U.noAnn
      HASH_KEY -> U.HASH_KEY U.noAnn
      PAIRING_CHECK -> U.PAIRING_CHECK U.noAnn
      SOURCE -> U.SOURCE U.noAnn
      SENDER -> U.SENDER U.noAnn
      ADDRESS -> U.ADDRESS U.noAnn
      CHAIN_ID -> U.CHAIN_ID U.noAnn
      LEVEL -> U.LEVEL U.noAnn
      SELF_ADDRESS -> U.SELF_ADDRESS U.noAnn
      NEVER -> U.NEVER
      TICKET -> U.TICKET U.noAnn
      READ_TICKET -> U.READ_TICKET U.noAnn
      SPLIT_TICKET -> U.SPLIT_TICKET U.noAnn
      JOIN_TICKETS -> U.JOIN_TICKETS U.noAnn
      OPEN_CHEST -> U.OPEN_CHEST U.noAnn
      SAPLING_EMPTY_STATE s ->
        U.SAPLING_EMPTY_STATE U.noAnn (singPeanoVal s)
      SAPLING_VERIFY_UPDATE -> U.SAPLING_VERIFY_UPDATE U.noAnn

untypeStackRef :: StackRef s -> U.StackRef
untypeStackRef (StackRef n) = U.StackRef (fromPeanoNatural n)

untypePrintComment :: PrintComment s -> U.PrintComment
untypePrintComment (PrintComment pc) = U.PrintComment $ map (second untypeStackRef) pc

extInstrToOps :: ExtInstr s -> [U.ExtInstrAbstract U.ExpandedOp]
extInstrToOps = \case
  PRINT pc -> one $ U.UPRINT (untypePrintComment pc)
  TEST_ASSERT (TestAssert nm pc i) ->
    one $ U.UTEST_ASSERT $
    U.TestAssert nm (untypePrintComment pc) (instrToOps i)
  DOC_ITEM{} -> []
  COMMENT_ITEM tp ->
    case tp of
      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"
  STACKTYPE s -> one $ U.STACKTYPE s

eqInstrExt :: Instr i1 o1 -> Instr i2 o2 -> Bool
eqInstrExt i1 i2 = instrToOps i1 == instrToOps i2

-- It's an orphan instance, but it's better than checking all cases manually.
-- We can also move this convertion to the place where `Instr` is defined,
-- but then there will be a very large module (as we'll have to move a lot of
-- stuff as well).
instance Eq (Instr inp out) where
  (==) = eqInstrExt

instance SingI s => Eq (TestAssert s) where
  TestAssert   name1 pattern1 instr1
    ==
    TestAssert name2 pattern2 instr2
    = and
    [ name1 == name2
    , pattern1 `eqParamSing` pattern2
    , instr1 `eqInstrExt` instr2
    ]

instance HasNoOp t => RenderDoc (Value' Instr t) where
  renderDoc pn = renderDoc pn . untypeValue

instance Buildable (Value' Instr t) where
  build val = printDocB True $ let tv = withValueTypeSanity val sing
    in renderDocSing doesntNeedParens (checkOpPresence tv) (val, tv)

instance Buildable (Instr inp out) where
  build = buildRenderDocExtended

instance RenderDoc (Instr inp out) where
  renderDoc context = renderDocList context . instrToOps

-- | Generate a value used for generating examples in documentation.
--
-- Since not for all types it is possible to produce a sensible example,
-- the result is optional. E.g. for operations, @never@, not proper
-- types like @contract operation@ we return 'Nothing'.
sampleTypedValue :: forall t. Sing t -> Maybe (Value t)
sampleTypedValue = \case
    STInt              -> Just $ VInt -1
    STNat              -> Just $ VNat 0
    STString           -> Just $ VString [mt|hello|]
    STMutez            -> Just $ VMutez [tz|100u|]
    STBool             -> Just $ VBool True
    STKey              -> Just $ VKey samplePublicKey
    STKeyHash          -> Just $ VKeyHash $ hashKey samplePublicKey
    STBls12381Fr       -> Just $ VBls12381Fr 1
    STBls12381G1       -> Just $ VBls12381G1 BLS.g1One
    STBls12381G2       -> Just $ VBls12381G2 BLS.g2One
    STTimestamp        -> Just $ VTimestamp $ timestampFromSeconds 1564142952
    STBytes            -> Just $ VBytes "\10"
    STAddress          -> Just $ VAddress $ sampleAddress
    STUnit             -> Just $ VUnit
    STSignature        -> Just $ VSignature $ sampleSignature
    STChainId          -> Just $ VChainId sampleChainId
    STOperation        -> Nothing
    -- It's not hard to generate a chest with a matching key, but
    -- representing those in source is extremely unwieldy due to large
    -- primes involved.
    STChest            -> Nothing
    STChestKey         -> Nothing
    STNever            -> Nothing
    STSaplingState _   -> Nothing
    STSaplingTransaction _ -> Nothing
    STOption t ->
      withSingI t $ VOption . Just <$> sampleTypedValue t
    STList t ->
      withSingI t $ VList . one <$> sampleTypedValue t
    STSet t -> withSingI t $ do
      Dict <- comparabilityPresence t
      VSet . one <$> sampleTypedValue t
    STContract t -> withSingI t $ do
      Dict <- rightToMaybe $ getWTP @t
      Dict <- opAbsense t
      Dict <- nestedBigMapsAbsense t
      pure . VContract (eaAddress sampleAddress) $ SomeEpc unsafeEpcCallRoot
    STTicket t -> withSingI t $ do
      cmpProof <- comparabilityPresence t
      dat <- sampleTypedValue t
      VNat amount <- sampleTypedValue STNat
      case cmpProof of
        Dict -> return $ VTicket (eaAddress sampleAddress) dat amount
    STPair t1 t2 -> withSingI t1 $ withSingI t2 $ do
      val1 <- sampleTypedValue t1
      val2 <- sampleTypedValue t2
      pure $ VPair (val1, val2)
    STOr tl tr -> withSingI tl $ withSingI tr $ asum
      [ VOr . Left <$> sampleTypedValue tl
      , VOr . Right <$> sampleTypedValue tr
      ]
    STMap t1 t2 -> withSingI t1 $ withSingI t2 $ do
      val1 <- sampleTypedValue t1
      val2 <- sampleTypedValue t2
      case checkComparability t1 of
        CanBeCompared -> pure $ VMap $ Map.fromList [(val1, val2)]
        CannotBeCompared -> Nothing
    STBigMap t1 t2 -> withSingI t1 $ withSingI t2 $ do
      val1 <- sampleTypedValue t1
      val2 <- sampleTypedValue t2
      case (checkComparability t1, bigMapAbsense t2) of
        (CanBeCompared, Just Dict) -> pure $ VBigMap Nothing $ Map.fromList [(val1, val2)]
        _                          -> Nothing
    STLambda v (t2 :: Sing t2) -> withSingI v $ withSingI t2 $
      case checkScope @(ConstantScope t2) of
        Right Dict -> do
          val <- sampleTypedValue t2
          pure $ VLam $ RfNormal (DROP `Seq` PUSH val)
        _ -> pure $ VLam $ RfAlwaysFails (PUSH (VString [mt|lambda sample|]) `Seq` FAILWITH)
    where
      sampleAddress = (unsafe . parseEpAddress) "KT1AEseqMV6fk2vtvQCVyA7ZCaxv7cpxtXdB"
      samplePublicKey = fromRight (error "impossible") $ parsePublicKey
        "edpkuwTWKgQNnhR5v17H2DYHbfcxYepARyrPGbf1tbMoGQAj8Ljr3V"
      sampleSignature = fromRight (error "impossible") $ parseSignature
        "edsigtrs8bK7vNfiR4Kd9dWasVa1bAWaQSu2ipnmLGZuwQa8ktCEMYVKqbWsbJ7zTS8dgYT9tiSUKorWCPFHosL5zPsiDwBQ6vb"
      sampleChainId = fromRight (error "impossible") $ parseChainId "NetXUdfLh6Gm88t"

-- Misc
----------------------------------------------------------------------------

-- | Flatten a provided list of notes to a map of its entrypoints and its
-- corresponding utype. Please refer to 'U.mkEntrypointsMap' in regards to how
-- duplicate entrypoints are handled.
flattenEntrypoints :: ParamNotes t -> Map EpName U.Ty
flattenEntrypoints = U.mkEntrypointsMap . convertParamNotes

-------------------------------------------------------------------------------
-- Rendering helpers
-------------------------------------------------------------------------------

-- | An extended version of renderDoc for typed values that handles VOp
-- accepts explicit singleton
renderDocSing :: RenderContext -> OpPresence t -> (Value' Instr t, Sing t) -> Doc
renderDocSing pn = \case
  OpAbsent -> renderDoc pn . untypeValue . fst
  OpPresent -> \case
    (VOp op, _) -> renderAnyBuildable op
    -- other cases try to mimic instance RenderDoc U.Value, see "Michelson.Untyped.Value"
    (VOption Nothing, _) -> U.renderNone
    (VOption (Just x), STOption tx) -> U.renderSome pn $ \ctx -> renderDocSing ctx OpPresent (x, tx)
    (VList xs, STList txs) -> renderList OpPresent txs xs
    (VSet ss, STSet tss) -> renderList OpPresent tss $ toList ss
    (VTicket s v a, STTicket tv) -> renderDocSing
      needsParens
      OpPresent
      (VPair (VAddress (EpAddress s DefEpName), VPair (v, VNat a))
        , STPair STAddress (STPair tv STNat))
    val@(VPair (_, (VPair (_, _))), _) ->
      U.renderValuesList id $ renderLinearizedRightCombValuePair val
    (VPair (l, r), STPair tl tr) -> U.renderPair pn (render tl l) (render tr r)
    (VOr (Left l), STOr tl _) -> U.renderLeft pn $ render tl l
    (VOr (Right r), STOr _ tr) -> U.renderRight pn $ render tr r
    (VMap m, STMap tk tv) -> renderMap (tk, tv, checkOpPresence tk, checkOpPresence tv) m
    (VBigMap _ m, STBigMap tk tv) -> renderMap (tk, tv, checkOpPresence tk, checkOpPresence tv) m
  where render sg v ctx = renderDocSing ctx (checkOpPresence sg) (v, sg)

renderList :: OpPresence t -> Sing t -> [Value' Instr t] -> Doc
renderList osg sg = renderList' $ renderDocSing doesntNeedParens osg . (, sg)

renderMap :: (Sing tk, Sing tv, OpPresence tk, OpPresence tv)
          -> Map (Value' Instr tk) (Value' Instr tv) -> Doc
renderMap ctx = renderList' (renderElt ctx) . Map.toList

renderList' :: (a -> Doc) -> [a] -> Doc
renderList' f = maybe "{ }" (U.renderValuesList f) . nonEmpty

renderElt :: (Sing tk, Sing tv, OpPresence tk, OpPresence tv)
          -> (Value' Instr tk, Value' Instr tv) -> Doc
renderElt (tk, tv, otk, otv) (k, v) =
  U.renderElt' (render otk k tk) (render otv v tv)
  where render o x tx ctx = renderDocSing ctx o (x, tx)

-- | Mimics U.linearizeRightCombValuePair, but for typed values;
-- however, unlike U.linearizeRightCombValuePair renders values on-the-fly.
renderLinearizedRightCombValuePair :: (Value' Instr t, Sing t) -> NonEmpty Doc
renderLinearizedRightCombValuePair = \case
  (VPair (l, r), STPair tl tr) -> renderDocSing doesntNeedParens (checkOpPresence tl) (l, tl)
                               <| renderLinearizedRightCombValuePair (r, tr)
  val@(_, tv)                  -> renderDocSing doesntNeedParens (checkOpPresence tv) val :| []