-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- | Module, carrying logic of @PACK@ instruction.
--
-- This is nearly symmetric to adjacent Unpack.hs module.
module Michelson.Interpret.Pack
  ( packCode'
  , packT'
  , packValue
  , packValue'
  , packValuePrefix
    -- * Serializers used in morley-client
  , encodeValue'
  , encodeValue
  , packNotedT'
    -- * Internals
  , encodeIntPayload
  , encodeKeyHashRaw
  , encodeEpAddress
  ) where

import Prelude hiding (EQ, GT, LT)

import qualified Data.Binary.Put as Bi
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 Data.Vinyl (Rec(..))
import Util.Type (type (++))

import Michelson.Interpret.Utils
import Michelson.Text
import Michelson.Typed
import Michelson.Untyped.Annotation
  (Annotation(..), FieldAnn, TypeAnn, VarAnn, fullAnnSet, isNoAnnSet, noAnn)
import Tezos.Address (Address(..), ContractHash(..))
import Tezos.Core (ChainId(..), Mutez(..), timestampToSeconds)
import Tezos.Crypto (KeyHash(..), KeyHashTag(..), PublicKey(..), signatureToBytes)
import qualified Tezos.Crypto.BLS12381 as BLS
import qualified Tezos.Crypto.Ed25519 as Ed25519
import qualified Tezos.Crypto.P256 as P256
import qualified Tezos.Crypto.Secp256k1 as Secp256k1
import Util.Peano (peanoValSing)

-- | Prefix prepended to the binary representation of a value.
packValuePrefix :: IsString s => s
packValuePrefix = "\x05"

-- | Serialize a value given to @PACK@ instruction.
packValue :: PackedValScope t => Value t -> LByteString
packValue x = packValuePrefix <> encodeValue x

-- | Same as 'packValue', for strict bytestring.
packValue' :: PackedValScope t => Value t -> ByteString
packValue' = LBS.toStrict . packValue

encodeValue' :: (SingI t, HasNoOp t) => Value t -> ByteString
encodeValue' = LBS.toStrict . encodeValue

packT' :: forall (t :: T). SingI t => ByteString
packT' = LBS.toStrict $ encodeT' @t

packCode' :: Instr inp out -> ByteString
packCode' = LBS.toStrict . encodeInstrs

-- | Generic serializer.
--
-- We don't require @HasNoBigMap@ constraint here since the big_map serialization
-- is only prohibited in @PACK@ instructions, however, we still want to be able to
-- serialize big_map e.g. in order to transform typed value to low-level Micheline
-- representation.
-- TODO: Serialize chain operations properly as well since they actually also have
-- byte representation.
encodeValue :: forall t. (SingI t, HasNoOp t) => Value t -> LByteString
encodeValue val = case (val, sing @t) of
  (VKey s, _) -> encodeBytes' $ case s of
    PublicKeyEd25519 pk -> "\x00" <> Ed25519.publicKeyToBytes pk
    PublicKeySecp256k1 pk -> "\x01" <> Secp256k1.publicKeyToBytes pk
    PublicKeyP256 pk -> "\x02" <> P256.publicKeyToBytes pk
  (VUnit, _) -> "\x03\x0b"
  (VSignature x, _) -> encodeBytes' $ signatureToBytes x
  (VChainId x, _) ->
    encodeBytes' $ ByteArray.convert (unChainId x)
  (VOption (Just x), STOption _) -> "\x05\x09" <> encodeValue x
  (VOption Nothing, _) -> "\x03\x06"
  (VList xs, STList _) -> encodeList encodeValue xs
  (VSet xs, (STSet (st :: Sing st))) -> case checkOpPresence st of
    OpAbsent -> encodeList encodeValue (toList xs)
  (VContract addr sepc, _) -> encodeEpAddress $ EpAddress addr (sepcName sepc)
  (VPair (v1, v2), STPair l _) ->
    case checkOpPresence l of
      OpAbsent -> "\x07\x07" <> encodeValue v1 <> encodeValue v2
  (VOr (Left v), STOr l _) ->
    case checkOpPresence l of
      OpAbsent -> "\x05\x05" <> encodeValue v
  (VOr (Right v), STOr l _) ->
    case checkOpPresence l of
      OpAbsent-> "\x05\x08" <> encodeValue v
  (VLam lam, _) -> encodeInstrs $ rfAnyInstr lam
  (VMap m, STMap sk _) -> case checkOpPresence sk of
    OpAbsent -> encodeMap m
  (VBigMap m, STBigMap sk _) -> case checkOpPresence sk of
    OpAbsent -> encodeMap m
  (VInt x, STInt) -> encodeNumeric x
  (VNat x, STNat) -> encodeNumeric x
  (VString text, STString) -> encodeString text
  (VBytes bytes, STBytes) -> encodeBytes' bytes
  (VMutez x, STMutez) -> encodeNumeric (unMutez x)
  (VBool True, STBool) -> "\x03\x0a"
  (VBool False, STBool) -> "\x03\x03"
  (VKeyHash kh, STKeyHash) -> encodeBytes $ encodeKeyHashRaw kh
  (VBls12381Fr v, STBls12381Fr) -> encodeBytes' $ BLS.toMichelsonBytes v
  (VBls12381G1 v, STBls12381G1) -> encodeBytes' $ BLS.toMichelsonBytes v
  (VBls12381G2 v, STBls12381G2) -> encodeBytes' $ BLS.toMichelsonBytes v
  (VTimestamp x, STTimestamp) -> encodeNumeric (timestampToSeconds @Integer x)
  (VAddress addr, STAddress) -> encodeEpAddress addr

encodeLength :: Int -> LByteString
encodeLength = Bi.runPut . Bi.putWord32be . fromIntegral

-- | Lift encoded list content to an entire encoded list.
encodeAsList :: LByteString -> LByteString
encodeAsList bs = encodeLength (length bs) <> bs

-- | Encode a list-like structure.
encodeList :: (a -> LByteString) -> [a] -> LByteString
encodeList encodeElem l = "\x02" <> encodeAsList (LBS.concat $ map encodeElem l)

-- | Encode a text.
encodeString :: MText -> LByteString
encodeString text = "\x01" <> encodeAsList (encodeUtf8 $ unMText text)

-- | Encode some raw data.
encodeBytes :: LByteString -> LByteString
encodeBytes bs =
  "\x0a" <> encodeAsList bs

-- | Version of 'encodeBytes' that accepts a strict bytestring.
encodeBytes' :: ByteString -> LByteString
encodeBytes' = encodeBytes . LBS.fromStrict

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

-- | Encode some map.
encodeMap :: (SingI v, HasNoOp v, SingI k, HasNoOp k) => Map (Value k) (Value v) -> LByteString
encodeMap m =
  encodeList (\(k, v) -> "\x07\x04" <> encodeValue k <> encodeValue v) (Map.toList m)

encodeKeyHashRaw :: KeyHash -> LByteString
encodeKeyHashRaw kh = (<> LBS.fromStrict (khBytes kh)) $
  case khTag kh of
    KeyHashEd25519 -> "\x00"
    KeyHashSecp256k1 -> "\x01"
    KeyHashP256 -> "\x02"

encodeAddress :: Address -> LByteString
encodeAddress = \case
  KeyAddress keyHash ->
    "\x00" <> (encodeKeyHashRaw keyHash)
  ContractAddress (ContractHash address) ->
    "\x01" <> LBS.fromStrict address <> "\x00"

encodeEpAddress :: EpAddress -> LByteString
encodeEpAddress (EpAddress addr epName) =
  encodeBytes $ encodeAddress addr <> encodeEpName epName

-- | Encode contents of a given number.
encodeIntPayload :: Integer -> LByteString
encodeIntPayload = LBS.pack . toList . encodeZarithNumber

-- | Encode an int-like value.
encodeNumeric :: Integral i => i -> LByteString
encodeNumeric i = "\x00" <> encodeIntPayload (fromIntegral i)

-- | Encode a code block.
encodeInstrs :: Instr inp out -> LByteString
encodeInstrs = encodeList id . one . encodeInstr

-- | Encode an instruction.
encodeInstr :: forall inp out. Instr inp out -> LByteString
encodeInstr = \case
  WithLoc _ i ->
    encodeInstr i
  InstrWithNotes proxy notes instr ->
    encodeNotedInstr proxy instr notes []
  InstrWithVarNotes varNotes a -> case a of
    AnnLEFT{} | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->
      encodeVarNotedInstr a varNotes (encodeT' @r)
    AnnRIGHT{} | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->
      encodeVarNotedInstr a varNotes (encodeT' @l)
    _ -> encodeVarNotedInstr a varNotes ""
  InstrWithVarAnns _ a ->
    encodeInstr a
  FrameInstr _ i ->
    encodeInstr i
  Seq a b ->
    encodeInstr a <> encodeInstr b
  Nop ->
    mempty
  Nested i ->
    encodeInstrs i
  DocGroup _ i ->
    encodeInstrs i
  Ext _ ->
    ""
  DROP ->
    "\x03\x20"
  DROPN s ->
    "\x05\x20" <> encodeNumeric (peanoValSing s)
  DUP ->
    "\x03\x21"
  DUPN s ->
    "\x05\x21" <> encodeNumeric (peanoValSing s)
  SWAP ->
    "\x03\x4c"
  DIG s ->
    "\x05\x70" <> encodeNumeric (peanoValSing s)
  DUG s ->
    "\x05\x71" <> encodeNumeric (peanoValSing s)
  PUSH (a :: Value t) ->
    "\x07\x43" <> encodeT' @t <> encodeValue a
  SOME ->
    "\x03\x46"
  NONE | _ :: Proxy ('TOption t ': s) <- Proxy @out ->
    "\x05\x3e" <> encodeT' @t
  UNIT ->
    "\x03\x4f"
  IF_NONE a b ->
    "\x07\x2f" <> encodeInstrs a <> encodeInstrs b
  AnnPAIR tn fn1 fn2 ->
    encodeWithAnns [tn] [fn1, fn2] [] "\x03\x42"
  PAIRN n ->
    "\x05\x42" <> encodeNumeric (peanoValSing n)
  UNPAIRN n ->
    "\x05\x7a" <> encodeNumeric (peanoValSing n)
  (AnnCAR fn) ->
    encodeWithAnns [] [fn] [] "\x03\x16"
  (AnnCDR fn) ->
    encodeWithAnns [] [fn] [] "\x03\x17"
  (AnnLEFT tn fn1 fn2) | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->
    encodeWithAnns [tn] [fn1, fn2] [] $ "\x05\x33" <> encodeT' @r
  (AnnRIGHT tn fn1 fn2) | _ :: Proxy ('TOr l r ': s) <- Proxy @out ->
    encodeWithAnns [tn] [fn1, fn2] [] $ "\x05\x44" <> encodeT' @l
  IF_LEFT a b ->
    "\x07\x2e" <> encodeInstrs a <> encodeInstrs b
  NIL | _ :: Proxy ('TList t ': s) <- Proxy @out ->
    "\x05\x3d" <> encodeT' @t
  CONS ->
    "\x03\x1b"
  IF_CONS a b ->
    "\x07\x2d" <> encodeInstrs a <> encodeInstrs b
  SIZE ->
    "\x03\x45"
  EMPTY_SET | _ :: Proxy ('TSet t ': s) <- Proxy @out ->
    "\x05\x24" <> encodeT' @t
  EMPTY_MAP | _ :: Proxy ('TMap k v ': s) <- Proxy @out ->
    "\x07\x23" <> encodeT' @k <> encodeT' @v
  EMPTY_BIG_MAP | _ :: Proxy ('TBigMap k v ': s) <- Proxy @out ->
    "\x07\x72" <> encodeT' @k <> encodeT' @v
  MAP a ->
    "\x05\x38" <> encodeInstrs a
  ITER a ->
    "\x05\x52" <> encodeInstrs a
  MEM ->
    "\x03\x39"
  GET ->
    "\x03\x29"
  GETN n ->
    "\x05\x29" <> encodeNumeric (peanoValSing n)
  UPDATE ->
    "\x03\x50"
  UPDATEN n ->
    "\x05\x50" <> encodeNumeric (peanoValSing n)
  GET_AND_UPDATE ->
    "\x03\x8c"
  IF a b ->
    "\x07\x2c" <> encodeInstrs a <> encodeInstrs b
  LOOP a ->
    "\x05\x34" <> encodeInstrs a
  LOOP_LEFT a ->
    "\x05\x53" <> encodeInstrs a
  LAMBDA (v :: Value ('TLambda i o)) ->
    "\x09\x31" <>
    encodeAsList (encodeT' @i <> encodeT' @o <> encodeValue v) <>
    encodeLength 0  -- encoding of a Variable Annotation (that we don't support)
  EXEC ->
    "\x03\x26"
  APPLY ->
    "\x03\x73"
  DIP a ->
    "\x05\x1f" <> encodeInstrs a
  DIPN s a ->
    "\x07\x1f" <> encodeNumeric (peanoValSing s) <> encodeInstrs a
  FAILWITH ->
    "\x03\x27"
  CAST | _ :: Proxy (t ': s) <- Proxy @out ->
    "\x05\x57" <> encodeT' @t
  RENAME ->
    "\x03\x58"
  PACK ->
    "\x03\x0c"
  UNPACK | _ :: Proxy ('TOption t ': s) <- Proxy @out ->
    "\x05\x0d" <> encodeT' @t
  CONCAT ->
    "\x03\x1a"
  CONCAT' ->
    "\x03\x1a"
  SLICE ->
    "\x03\x6f"
  ISNAT ->
    "\x03\x56"
  ADD ->
    "\x03\x12"
  SUB ->
    "\x03\x4b"
  MUL ->
    "\x03\x3a"
  EDIV ->
    "\x03\x22"
  ABS ->
    "\x03\x11"
  NEG ->
    "\x03\x3b"
  LSL ->
    "\x03\x35"
  LSR ->
    "\x03\x36"
  OR ->
    "\x03\x41"
  AND ->
    "\x03\x14"
  XOR ->
    "\x03\x51"
  NOT ->
    "\x03\x3f"
  COMPARE ->
    "\x03\x19"
  EQ ->
    "\x03\x25"
  NEQ ->
    "\x03\x3c"
  LT ->
    "\x03\x37"
  GT ->
    "\x03\x2a"
  LE ->
    "\x03\x32"
  GE ->
    "\x03\x28"
  INT ->
    "\x03\x30"
  SELF sepc ->
    case sepcName sepc of
      DefEpName ->  "\x03\x49"
      epName -> encodeWithAnns [] [epNameToRefAnn epName] [] "\x03\x49"
  CONTRACT ns ep | _ :: Proxy ('TOption ('TContract t) ': s) <- Proxy @out ->
    encodeWithAnns [] [epNameToRefAnn ep] [] $ "\x05\x55" <> encodeNotedT' @t ns
  TRANSFER_TOKENS ->
    "\x03\x4d"
  SET_DELEGATE ->
    "\x03\x4e"
  CREATE_CONTRACT contract@Contract{..}
    | _ :: Instr '[ 'TPair p g ] '[ 'TPair ('TList 'TOperation) g ] <- cCode ->
    let contents = mapEntriesOrdered contract
            (\np -> "\x05\x00" <> encodeParamNotes' @p np)
            (\ng -> "\x05\x01" <> encodeNotedT' @g ng)
            (\instr -> "\x05\x02" <> encodeInstrs instr)
    in "\x05\x1d" <> encodeList id contents
  IMPLICIT_ACCOUNT ->
   "\x03\x1e"
  NOW ->
   "\x03\x40"
  AMOUNT ->
   "\x03\x13"
  BALANCE ->
   "\x03\x15"
  VOTING_POWER ->
   "\x03\x7b"
  TOTAL_VOTING_POWER ->
   "\x03\x7c"
  CHECK_SIGNATURE ->
   "\x03\x18"
  SHA256 ->
   "\x03\x0f"
  SHA512 ->
   "\x03\x10"
  BLAKE2B ->
   "\x03\x0e"
  SHA3 ->
   "\x03\x7e"
  KECCAK ->
   "\x03\x7d"
  HASH_KEY ->
   "\x03\x2b"
  PAIRING_CHECK ->
   "\x03\x7f"
  SOURCE ->
   "\x03\x47"
  SENDER ->
   "\x03\x48"
  ADDRESS ->
   "\x03\x54"
  CHAIN_ID ->
   "\x03\x75"
  LEVEL ->
   "\x03\x76"
  SELF_ADDRESS ->
   "\x03\x77"
  NEVER ->
   "\x03\x79"


-- | Iff there are non-empty annotations it increments the value's tag and
-- appends the encoded annotations.
encodeWithAnns :: [TypeAnn] -> [FieldAnn] -> [VarAnn] -> LByteString -> LByteString
encodeWithAnns tns fns vns encodedInput
  | null encodedInput = encodedInput
  | isNoAnnSet annSet = encodedInput
  | otherwise = inputIncrem <> encodedAnns
  where
    annSet = fullAnnSet tns fns vns
    encodedAnns = encodeAsList . encodeUtf8 $ show @Text annSet
    inputIncrem = (1 + LBS.head encodedInput) `LBS.cons` LBS.tail encodedInput

-- | Encode an instruction with variable annotations
encodeVarNotedInstr :: Instr inp out -> NonEmpty VarAnn -> LByteString -> LByteString
encodeVarNotedInstr i vns'@(toList -> vns) encodedType = case i of
  InstrWithNotes proxy n a -> encodeNotedInstr proxy a n vns
  InstrWithVarAnns _ a -> encodeInstr $ InstrWithVarNotes vns' a
  -- AnnPAIR, AnnCAR, AnnCDR and AnnLEFT, AnnRIGHT are checked here because
  -- their cases on `encodeInstr` increment them to \x04 and to \x05 respectively
  -- when they have a field annotation, but they would also get increment due to
  -- variable annotations, resulting in incorrect \x05 and \x06 codes respectively.
  AnnPAIR tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns "\x03\x42"
  AnnCAR fn -> encodeWithAnns [] [fn] vns "\x03\x16"
  AnnCDR fn -> encodeWithAnns [] [fn] vns "\x03\x17"
  AnnLEFT tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x33" <> encodedType
  AnnRIGHT tn fn1 fn2 -> encodeWithAnns [tn] [fn1, fn2] vns $ "\x05\x44" <> encodedType
  _ -> encodeWithAnns [] [] vns $ encodeInstr i

-- | Encode an instruction with Annotations
encodeNotedInstr
  :: forall inp out topElems rest.
     out ~ (topElems ++ rest)
  => Proxy rest -> Instr inp out -> Rec Notes topElems -> [VarAnn] -> LByteString
encodeNotedInstr proxy instr notes vns = case (instr, Proxy @out, notes) of
  (WithLoc _ instr', _, _) ->
    encodeNotedInstr proxy instr' notes vns
  (SOME, _, NTOption tn _ns :& _) ->
    encodeWithAnns [tn] [] vns $ encodeInstr instr
  (NONE, _ :: Proxy ('TOption t ': s), NTOption tn ns :& _) ->
    encodeWithAnns [tn] [] vns $ "\x05\x3e" <> encodeNotedT' @t ns
  (UNIT, _, NTUnit tn :& _) ->
    encodeWithAnns [tn] [] vns $ encodeInstr instr
  (NIL, _ :: Proxy ('TList t ': s), NTList tn ns :& _) ->
    encodeWithAnns [tn] [] vns $ "\x05\x3d" <> encodeNotedT' @t ns
  (EMPTY_SET, _ :: Proxy ('TSet t ': s), NTSet tn ns :& _) ->
    encodeWithAnns [tn] [] vns $ "\x05\x24" <> encodeNotedT' @t ns
  (EMPTY_MAP, _ :: Proxy ('TMap k v ': s), NTMap tn1 nk ns :& _) ->
    encodeWithAnns [tn1] [] vns $
      "\x07\x23" <> encodeNotedT' @k nk <> encodeNotedT' @v ns
  (EMPTY_BIG_MAP, _ :: Proxy ('TBigMap k v ': s), NTBigMap tn1 nk ns :& _) ->
    encodeWithAnns [tn1] [] vns $
      "\x07\x72" <> encodeNotedT' @k nk <> encodeNotedT' @v ns
  (PUSH (v :: Value t), _, tn :& _) ->
    "\x07\x43" <> encodeNotedT' @t tn <> encodeValue v
  (LAMBDA (v :: Value ('TLambda i o)), _, NTLambda _tn ns1 ns2 :& _) ->
    "\x09\x31" <>
    encodeAsList (encodeNotedT' @i ns1 <> encodeNotedT' @o ns2 <> encodeValue v) <>
    encodeLength 0  -- encoding of a Variable Annotation (that we don't support)
  (CAST, _ :: Proxy (t ': s), tn :& _) ->
    "\x05\x57" <> encodeNotedT' @t tn
  (UNPACK, _ :: Proxy ('TOption t ': s), NTOption tn ns :& _) ->
    encodeWithAnns [tn] [] vns $ "\x05\x0d" <> encodeNotedT' @t ns
  -- NOTE: `CONTRACT` may be part of an `InstrWithNotes` with `NTOption`, but is
  -- taken care of in `encodeInstr` anyway (because it contains the note itself)
  _ -> encodeInstr instr

packNotedT' :: forall (t :: T). SingI t => Notes t -> ByteString
packNotedT' = LBS.toStrict . encodeNotedT'

encodeNotedT' :: forall (t :: T). SingI t => Notes t -> LByteString
encodeNotedT' = encodeNotedST (sing @t) noAnn

encodeParamNotes' ::
  forall (t :: T). SingI t => ParamNotes t -> LByteString
encodeParamNotes' ParamNotesUnsafe{..} = encodeNotedST (sing @t) pnRootAnn pnNotes

-- Note: to encode field annotations we have to accept them as an additional
-- parameter because they are stored in the parent's `Notes t`, e.g. see STPair.
encodeNotedST :: Sing t -> FieldAnn -> Notes t -> LByteString
encodeNotedST st fn n = case (st, n) of
  (STInt, NTInt tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STNat, NTNat tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STString, NTString tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STBytes, NTBytes tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STMutez, NTMutez tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STBool, NTBool tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STKeyHash, NTKeyHash tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STBls12381Fr, NTBls12381Fr tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STBls12381G1, NTBls12381G1 tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STBls12381G2, NTBls12381G2 tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STTimestamp, NTTimestamp tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)
  (STAddress, NTAddress tn) ->
    encodeWithAnns [tn] [fn] [] $ encodeT (fromSingT st)

  (STKey, NTKey tn) ->
    encodeWithAnns [tn] [fn] [] $ "\x03\x5c"
  (STUnit, NTUnit tn) ->
    encodeWithAnns [tn] [fn] [] $ "\x03\x6c"
  (STNever, NTNever tn) ->
    encodeWithAnns [tn] [fn] [] $ "\x03\x78"
  (STSignature, NTSignature tn) ->
    encodeWithAnns [tn] [fn] [] $ "\x03\x67"
  (STChainId, NTChainId tn) ->
    encodeWithAnns [tn] [fn] [] $ "\x03\x74"
  (STOption a, NTOption tn ns) ->
    encodeWithAnns [tn] [fn] [] $ "\x05\x63" <> encodeNotedST a noAnn ns
  (STList a, NTList tn ns) ->
    encodeWithAnns [tn] [fn] [] $ "\x05\x5f" <> encodeNotedST a noAnn ns
  (STSet a, NTSet tn ns) ->
    encodeWithAnns [tn] [fn] [] $ "\x05\x66" <> encodeNotedST a noAnn ns
  (STOperation, NTOperation tn) ->
    encodeWithAnns [tn] [fn] [] $ "\x03\x6d"
  (STContract a, NTContract tn ns) ->
    encodeWithAnns [tn] [fn] [] $ "\x05\x5a" <> encodeNotedST a noAnn ns
  (STPair a b, NTPair tn fn1 fn2 _vn1 _vn2 ns1 ns2) ->
    encodeWithAnns [tn] [fn] [] $
      "\x07\x65" <> encodeNotedST a fn1 ns1 <> encodeNotedST b fn2 ns2
  (STOr a b, NTOr tn fn1 fn2 ns1 ns2) ->
    encodeWithAnns [tn] [fn] [] $
      "\x07\x64" <> encodeNotedST a fn1 ns1 <> encodeNotedST b fn2 ns2
  (STLambda a r, NTLambda tn ns1 ns2) ->
    encodeWithAnns [tn] [fn] [] $
      "\x07\x5e" <> encodeNotedST a noAnn ns1 <> encodeNotedST r noAnn ns2
  (STMap k v, NTMap tn nk nv) ->
    encodeWithAnns [tn] [fn] [] $
      "\x07\x60" <> encodeNotedST k noAnn nk <> encodeNotedST v noAnn nv
  (STBigMap k v, NTBigMap tn nk nv) ->
    encodeWithAnns [tn] [fn] [] $
      "\x07\x61" <> encodeNotedST k noAnn nk <> encodeNotedST v noAnn nv

encodeT :: T -> LByteString
encodeT = \case
  TKey  -> "\x03\x5c"
  TUnit -> "\x03\x6c"
  TNever -> "\x03\x78"
  TSignature -> "\x03\x67"
  TChainId -> "\x03\x74"
  TOption t -> "\x05\x63" <> encodeT t
  TList t -> "\x05\x5f" <> encodeT t
  TSet t -> "\x05\x66" <> encodeT t
  TOperation -> "\x03\x6d"
  TContract t -> "\x05\x5a" <> encodeT t
  TPair a b -> "\x07\x65" <> encodeT a <> encodeT b
  TOr a b -> "\x07\x64" <> encodeT a <> encodeT b
  TLambda a r -> "\x07\x5e" <> encodeT a <> encodeT r
  TMap k v -> "\x07\x60" <> encodeT k <> encodeT v
  TBigMap k v -> "\x07\x61" <> encodeT k <> encodeT v
  TInt -> "\x03" <> "\x5b"
  TNat -> "\x03" <> "\x62"
  TString -> "\x03" <> "\x68"
  TBytes -> "\x03" <> "\x69"
  TMutez -> "\x03" <> "\x6a"
  TBool -> "\x03" <> "\x59"
  TKeyHash -> "\x03" <> "\x5d"
  TBls12381Fr -> "\x03" <> "\x82"
  TBls12381G1 -> "\x03" <> "\x80"
  TBls12381G2 -> "\x03" <> "\x81"
  TTimestamp -> "\x03" <> "\x6b"
  TAddress -> "\x03" <> "\x6e"

encodeT' :: forall (t :: T). SingI t => LByteString
encodeT' = encodeT (demote @t)