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

-- | Module, providing functions for conversion from
-- instruction and value representation from @Morley.Michelson.Type@ module
-- to strictly-typed GADT-based representation from @Morley.Michelson.Value@ module.
--
-- This conversion is labeled as type check because that's what we are obliged
-- to do on our way.
--
-- Type check algorithm relies on the property of Michelson language that each
-- instruction on a given input stack type produces a definite output stack
-- type.
-- Michelson contract defines concrete types for storage and parameter, from
-- which input stack type is deduced. Then this type is being combined with
-- each subsequent instruction, producing next stack type after each
-- application.
--
-- Function @typeCheck@ takes list of instructions and returns value of type
-- @Instr inp out@ along with @HST inp@ and @HST out@ all wrapped into
-- @SomeInstr@ data type. This wrapping is done to satisfy Haskell type
-- system (which has no support for dependent types).
-- Functions @typeCheckInstr@, @typeCheckValue@ behave similarly.
--
-- When a recursive call is made within @typeCheck@, @typeCheckInstr@ or
-- @typeCheckValue@, result of a call is unwrapped from @SomeInstr@ and type
-- information from @HST inp@ and @HST out@ is being used to assert that
-- recursive call returned instruction of expected type
-- (error is thrown otherwise).
module Morley.Michelson.TypeCheck.Instr
    ( typeCheckContract
    , typeCheckContractAndStorage
    , typeCheckInstr
    , typeCheckList
    , tcList
    , typeCheckListNoExcept
    , typeCheckParameter
    , typeCheckStorage
    , typeCheckTopLevelType
    , typeCheckValue
    , typeCheckValueRunCodeCompat
    , typeVerifyContract
    , typeVerifyParameter
    , typeVerifyStorage
    , typeVerifyTopLevelType
    , typeVerifyView
    ) where

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, catchError, liftEither, throwError)
import Data.Constraint ((\\))
import Data.Default (def)
import Data.Generics (everything, mkQ)
import Data.Sequence ((|>))
import Data.Sequence qualified as Seq
import Data.Singletons (Sing, SomeSing(..), demote, withSingI, withSomeSing)
import Data.Type.Equality (TestEquality(..))
import Data.Typeable ((:~:)(..))
import Fmt (pretty)

import Morley.Michelson.TypeCheck.Error
import Morley.Michelson.TypeCheck.Ext
import Morley.Michelson.TypeCheck.Helpers
import Morley.Michelson.TypeCheck.TypeCheck
import Morley.Michelson.TypeCheck.TypeCheckedSeq
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), someInstrToOp,
  someViewToOp, tcsEither)
import Morley.Michelson.TypeCheck.Types
import Morley.Michelson.TypeCheck.Value
import Morley.Michelson.Typed hiding (Branch(..))
import Morley.Michelson.Typed.Contract (giveNotInView)

import Morley.Util.MismatchError
import Morley.Util.Peano
import Morley.Util.PeanoNatural
import Morley.Util.Sing (SingIOne, withSingIOne)
import Morley.Util.Type (knownListFromSingI, onFirst, type (++))

import Morley.Michelson.Untyped qualified as U
import Morley.Michelson.Untyped.Annotation (VarAnn)
import Morley.Util.Peano qualified as Peano

-- | Type check a contract and verify that the given storage
-- is of the type expected by the contract.
typeCheckContractAndStorage
  :: U.Contract -> U.Value -> TypeCheckResult SomeContractAndStorage
typeCheckContractAndStorage uContract uStorage = do
  SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract uContract
  storage <- typeVerifyStorage @st uStorage
  pure $ SomeContractAndStorage contract storage

typeCheckContract
  :: U.Contract
  -> TypeCheckResult SomeContract
typeCheckContract c = do
  paramType <- liftEither $ mkSomeParamType (U.contractParameter c)
  runTypeCheck (TypeCheckContract paramType) $ typeCheckContractImpl c

typeVerifyContract
  :: forall cp st.
     (SingI cp, SingI st)
  => U.Contract -> TypeCheckResult (Contract cp st)
typeVerifyContract uContract = do
  SomeContract tContract@(Contract{} :: Contract cp' st') <-
    typeCheckContract uContract
  Refl <- requireEq @cp' @cp (mkErr TltParameterType)
  Refl <- requireEq @st' @st (mkErr TltStorageType)
  return tContract
  where
    mkErr :: TopLevelType -> MismatchError T -> TypeCheckResult any
    mkErr tyDesc merr =
      throwError $ TCContractError "error in contract type" $ Just $
          UnexpectedTopLevelType tyDesc merr

withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a
withWTP fn = case getWTP @t of
  Right Dict -> fn
  Left err -> throwError $ TCContractError (pretty err) Nothing

withWTPInstr_ :: forall t a. SingI t => U.ExpandedInstr -> SomeHST -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTPInstr_ v t fn = case getWTP @t of
  Right Dict -> fn
  Left (NotWellTyped badType cause) -> do
    loc <- view tcieErrorPos
    throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType cause)

withWTPInstr'_
  :: forall t inp. SingI t
  => U.ExpandedInstr
  -> SomeHST
  -> (WellTyped t => TypeCheckInstrNoExcept (TypeCheckedSeq inp))
  -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
withWTPInstr'_ v t fn = case getWTP @t of
  Right Dict -> fn
  Left (NotWellTyped badType cause) -> do
    loc <- view tcieErrorPos
    let err = TCFailedOnInstr v t loc Nothing
              (Just $ UnsupportedTypeForScope badType cause)
    pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx v]

typeCheckContractImpl
  :: U.Contract
  -> TypeCheck SomeContract
typeCheckContractImpl uContract@(U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder uViews) = do
  _ <- maybe (throwError $ TCContractError "no instructions in contract code" $ Just EmptyCode)
                pure (nonEmpty pCode)
  withUType mParam $ \(paramNote :: Notes param) ->
    withUType mStorage $ \(storageNote :: Notes st) -> do
      withWTP @st $ do
        withWTP @param $ do
          Dict <- either (hasTypeError @param "parameter") pure
            $ checkScope @(ParameterScope param)
          Dict <- either (hasTypeError @st "storage") pure
            $ checkScope @(StorageScope st)
          let inp = (sing @('TPair param st), Dict) ::& SNil

          -- typecheck contract code
          codeRes <-
            usingReaderT def $
            liftNoExcept $
            typeCheckImpl
              (giveNotInView $ local (set tcieNotInView $ Just Dict) ... typeCheckInstr)
              pCode
              inp
          instr@(_ :/ instrOut) <-
            tcsEither onFailedCodeTypeCheck pure codeRes

          -- typecheck views
          views <- typeCheckViewsImpl
            uContract{ U.contractCode = [someInstrToOp instr], U.contractViews = [] }
            storageNote uViews

          handleError (onFailedFullTypeCheck [someInstrToOp instr] (zipWith someViewToOp uViews views)) $ do
            -- match contract code with contract signature, construct contract
            let cStoreNotes = storageNote
            cParamNotes <-
              liftEither $
              mkParamNotes paramNote rootAnn `onFirst`
                  (TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)
            let cEntriesOrder = entriesOrder
            cViews <- liftEither $
              mkViewsSet views `onFirst` \e -> TCContractError (pretty e) Nothing
            case instrOut of
              instr' ::: out -> liftEither $ do
                case eqHST1 @('TPair ('TList 'TOperation) st) out of
                  Right Refl ->
                    pure $ SomeContract Contract{ cCode = ContractCode instr', .. }
                  Left err ->
                    Left $ TCContractError "contract output type violates convention:" $ Just err
              AnyOutInstr instr' ->
                pure $ SomeContract Contract{ cCode = ContractCode instr', .. }

  where
    hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a
    hasTypeError name reason = throwError $
      TCContractError ("contract " <> name <> " type error") $
      Just $ UnsupportedTypeForScope (demote @t) reason

    onFailedCodeTypeCheck :: [TypeCheckedOp] -> TCError -> TypeCheck a
    onFailedCodeTypeCheck ops err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TCIncompletelyTyped err U.Contract
             { contractParameter = wholeParam
             , contractStorage = mStorage
             , contractCode = ops
             , entriesOrder = entriesOrder
             , contractViews = []
             }
        else err

    onFailedFullTypeCheck :: [TypeCheckedOp] -> [U.View' TypeCheckedOp] -> TCError -> TypeCheck a
    onFailedFullTypeCheck ops views err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TCIncompletelyTyped err U.Contract
             { contractParameter = wholeParam
             , contractStorage = mStorage
             , contractCode = ops
             , entriesOrder = entriesOrder
             , contractViews = views
             }
        else err

typeVerifyView
  :: forall arg ret st.
     (SingI arg, SingI ret, WellTyped st)
  => Notes st -> U.View -> TypeCheckResult (View arg st ret)
typeVerifyView notes v = do
  SomeView (tcView@View{} :: View arg' st' ret') <-
    runTypeCheck TypeCheckTest $ typeCheckViewImpl notes v
  Refl <- requireEq @arg' @arg (mkErr TltParameterType)
  Refl <- requireEq @st' @st (mkErr TltStorageType)
  Refl <- requireEq @ret' @ret (mkErr TltParameterType)
  return tcView
  where
    mkErr :: TopLevelType -> MismatchError T -> TypeCheckResult any
    mkErr tyDesc merr =
      throwError $ TCContractError "error in view type" $ Just $
          UnexpectedTopLevelType tyDesc merr

typeCheckViewImpl :: WellTyped st => Notes st -> U.View -> TypeCheck (SomeView st)
typeCheckViewImpl storageNote
  uView@U.View
  { U.viewArgument = AsUType (argNote :: Notes param)
  , U.viewReturn = AsUType (returnNote :: Notes ret)
  , U.viewCode = uInstr
  , U.viewName = viewName
  }
  = withWTP @param $ withWTP @ret $ do
    let inp = (STPair (notesSing argNote) (notesSing storageNote), Dict) ::& SNil
    Dict <-
      checkScope @(ViewableScope param)
      & either (hasTypeError @param "parameter") pure
    Dict <-
      checkScope @(ViewableScope ret)
      & either (hasTypeError @ret "return") pure
    codeRes <-
      usingReaderT def $
      liftNoExcept $
      typeCheckImpl typeCheckInstr uInstr inp
    _ :/ instrOut <-
      tcsEither (onFailedViewsTypeCheck uView) pure codeRes

    let vName = viewName
        vArgument = argNote
        vReturn = returnNote
    case instrOut of
      instr ::: out -> liftEither do
        Refl <- eqHST1 @ret out
          `onFirst` (TCViewError "view return type mismatch:" viewName . Just)
        return $ SomeView View{ vCode = instr, .. }
      AnyOutInstr instr ->
        return $ SomeView View{ vCode = instr, .. }

  where
    onFailedViewsTypeCheck
      :: U.View -> [TypeCheckedOp] -> TCError -> TypeCheck a
    onFailedViewsTypeCheck v viewOps err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TCIncompletelyTypedView err v{ U.viewCode = viewOps }
        else err

    hasTypeError :: forall (t :: T) a. SingI t => Text -> BadTypeForScope -> TypeCheck a
    hasTypeError desc reason = throwError $
      TCViewError (desc <> " type error in view") viewName $
      Just $ UnsupportedTypeForScope (demote @t) reason

typeCheckViewsImpl
  :: (WellTyped st)
  => U.Contract' TypeCheckedOp -> Notes st -> [U.View] -> TypeCheck [SomeView st]
typeCheckViewsImpl tcCotract storageNote cViews =
  let myfoldM l acc f = foldM f acc l in
  fmap (map snd . toList) $ myfoldM cViews (Seq.Empty :: Seq (U.View, SomeView st))
    \processedViews uView -> do
      resView <- typeCheckViewImpl storageNote uView
      pure $ processedViews |> (uView, resView)
      `catchError` \case
        TCIncompletelyTypedView err view' ->
          let tcViews = map (uncurry someViewToOp) processedViews
          in onFailedViewsTypeCheck tcViews view' err
        err -> throwError err
  where
    onFailedViewsTypeCheck
      :: Seq (U.View' TypeCheckedOp) -> U.View' TypeCheckedOp -> TCError -> TypeCheck a
    onFailedViewsTypeCheck processedViews v err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TCIncompletelyTyped err tcCotract
             { U.contractViews = toList (processedViews |> v)
             }
        else err

-- | Function @typeCheckList@ converts list of Michelson instructions
-- given in representation from @Morley.Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- Types are checked along the way which is necessary to construct a
-- strictly typed value.
--
-- As a second argument, @typeCheckList@ accepts input stack type representation.
typeCheckList
  :: (SingI inp)
  => [U.ExpandedOp]
  -> HST inp
  -> TypeCheck (SomeInstr inp)
typeCheckList = throwingTCError ... typeCheckListNoExcept

-- | Function @typeCheckListNoExcept@ converts list of Michelson instructions
-- given in representation from @Morley.Michelson.Type@ module to representation in a
-- partially typed tree. See @TypeCheckedSeq@ and @TypeCheckedOp@.
--
-- Types are checked along the way. It is necessary to embed well typed node as
-- well as type checking errors into the tree.
typeCheckListNoExcept
  :: (SingI inp)
  => [U.ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp)
typeCheckListNoExcept = usingReaderT def ... typeCheckImpl typeCheckInstr

-- | Function @typeCheckValue@ converts a single Michelson value
-- given in representation from @Morley.Michelson.Untyped@ module hierarchy to
-- representation in strictly typed GADT.
--
-- @typeCheckValue@ is polymorphic in the expected type of value.
--
-- Type checking algorithm pattern-matches on parse value representation,
-- expected type @t@ and constructs @Value t@ value.
--
-- If there was no match on a given pair of value and expected type,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
typeCheckValue
  :: forall t. SingI t
  => U.Value
  -> TypeCheckResult (Value t)
typeCheckValue value = do
  runTypeCheck (TypeCheckValue (value, demote @t) Nothing) $
    usingReaderT def $
      typeCheckValImpl Nothing typeCheckInstr value

-- | Simulates the typechecking behavior of the RPC's @/run_code@ endpoint.
--
-- If an integer is found where a big_map is expected,
-- we check if a big_map exists with that ID.
-- If it does, and if the big_map's value and key have the expected types, we replace the
-- big_map ID with the corresponding big_map value.
typeCheckValueRunCodeCompat :: forall t. SingI t => BigMapFinder -> U.Value -> TypeCheckResult (Value t)
typeCheckValueRunCodeCompat bigMapFinder val =
  runTypeCheck (TypeCheckValue (val, demote @t) (Just bigMapFinder)) $
    usingReaderT def $
      typeCheckValImpl Nothing typeCheckInstr val

typeVerifyParameter
  :: SingI t
  => TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)
typeVerifyParameter originatedContracts = typeVerifyTopLevelType (Just originatedContracts)

typeVerifyStorage
  :: SingI t
  => U.Value -> TypeCheckResult (Value t)
typeVerifyStorage = typeVerifyTopLevelType Nothing

typeVerifyTopLevelType
  :: forall t. SingI t
  => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult (Value t)
typeVerifyTopLevelType mOriginatedContracts valueU =
  runTypeCheck (TypeCheckValue (valueU, demote @t) Nothing) $ usingReaderT def $
    typeCheckValImpl mOriginatedContracts typeCheckInstr valueU

-- | Like 'typeCheckValue', but for values to be used as parameter.
--
-- Also accepts a 'TcOriginatedContracts' in order to be able to type-check
-- @contract p@ values (which can only be part of a parameter).
typeCheckParameter
  :: TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult SomeValue
typeCheckParameter originatedContracts = typeCheckTopLevelType (Just originatedContracts)

-- | Like 'typeCheckValue', but for values to be used as storage.
typeCheckStorage
  :: U.Ty -> U.Value -> TypeCheckResult SomeValue
typeCheckStorage = typeCheckTopLevelType Nothing

typeCheckTopLevelType
  :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult SomeValue
typeCheckTopLevelType mOriginatedContracts typeU valueU =
  withSomeSing (fromUType typeU) $ \(s :: Sing t) ->
    withSingI s $ SomeValue <$> typeVerifyTopLevelType @t mOriginatedContracts valueU

-- | Helper data type we use to typecheck DUPN.
data TCDupNHelper inp where
  TCDupNHelper ::
    forall (n :: Peano) inp out a.
    (SingI out, ConstraintDUPN n inp out a, DupableScope a) =>
    PeanoNatural n -> HST out -> TCDupNHelper inp

-- | Helper data type we use to typecheck DROPN.
data TCDropHelper inp where
  TCDropHelper ::
    forall (n :: Peano) inp out.
    (SingI out, LongerOrSameLength inp n, Drop n inp ~ out) =>
    PeanoNatural n -> HST out -> TCDropHelper inp

-- | Helper data type we use to typecheck DIG.
data TCDigHelper inp where
  TCDigHelper ::
    forall (n :: Peano) inp out a.
    (SingI out, ConstraintDIG n inp out a) =>
    PeanoNatural n -> HST out -> TCDigHelper inp

-- | Helper data type we use to typecheck DUG.
data TCDugHelper inp where
  TCDugHelper ::
    forall (n :: Peano) inp out a.
    (SingI out, ConstraintDUG n inp out a) =>
    PeanoNatural n -> HST out -> TCDugHelper inp

-- | Helper data type we use to typecheck PAIRN.
--
-- It holds all the necessary data to construct a typed PAIRN
-- instruction once we're done traversing the stack.
data TCPairNHelper inp where
  TCPairNHelper ::
    forall (n :: Peano) (inp :: [T]).
    (SingI (PairN n inp), ConstraintPairN n inp) =>
    PeanoNatural n -> HST (PairN n inp) -> TCPairNHelper inp

-- | Helper data type we use to typecheck UNPAIRN.
--
-- It holds all the necessary data to construct a typed UNPAIRN
-- instruction once we're done traversing the pair.
data TCUnpairNHelper (inp :: [T]) where
  TCUnpairNHelper ::
    forall (n :: Peano) (a :: T) (b :: T) (rest :: [T]).
    (SingI (UnpairN n ('TPair a b) ++ rest), ConstraintUnpairN n ('TPair a b)) =>
    PeanoNatural n -> HST (UnpairN n ('TPair a b) ++ rest) -> TCUnpairNHelper ('TPair a b : rest)

-- | Helper data type we use to typecheck GETN.
--
-- It holds all the necessary data to construct a typed GETN
-- instruction once we're done traversing the pair.
data TCGetNHelper (inp :: [T]) where
  TCGetNHelper ::
    forall (ix :: Peano) (pair :: T) (rest :: [T]).
    (SingI (GetN ix pair ': rest), ConstraintGetN ix pair) =>
    PeanoNatural ix -> HST (GetN ix pair ': rest) -> TCGetNHelper (pair : rest)

-- | Helper data type we use to typecheck UPDATEN.
--
-- It holds all the necessary data to construct a typed UPDATEN
-- instruction once we're done traversing the pair.
data TCUpdateNHelper (inp :: [T]) where
  TCUpdateNHelper ::
    forall (ix :: Peano) (val :: T) (pair :: T) (rest :: [T]).
    (SingI (UpdateN ix val pair ': rest), ConstraintUpdateN ix pair) =>
    PeanoNatural ix -> HST (UpdateN ix val pair ': rest) -> TCUpdateNHelper (val : pair : rest)

-- | Helper function to convert a simple throwing typechecking action into a
-- non-throwing one, embedding possible errors into the type checking tree.
workOnInstr
  :: U.ExpandedInstr
  -> TypeCheckInstr (SomeInstr s)
  -> TypeCheckInstrNoExcept (TypeCheckedSeq s)
workOnInstr instr = tcEither
  (\err -> pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx instr])
  (pure . WellTypedSeq)

-- | Less verbose version of `typeCheckImpl typeCheckInstr`.
tcList
  :: (SingI inp)
  => [U.ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
tcList = typeCheckImpl typeCheckInstr

-- | Function @typeCheckInstr@ converts a single Michelson instruction
-- given in representation from @Morley.Michelson.Type@ module to representation
-- in strictly typed GADT.
--
-- As a second argument, @typeCheckInstr@ accepts input stack type representation.
--
-- Type checking algorithm pattern-matches on given instruction, input stack
-- type and constructs strictly typed GADT value, checking necessary type
-- equalities when necessary.
--
-- If there was no match on a given pair of instruction and input stack,
-- that is interpreted as input of wrong type and type check finishes with
-- error.
typeCheckInstr :: TcInstrHandler
typeCheckInstr uInstr inp = case (uInstr, inp) of
  (U.EXT ext, si) ->
    typeCheckExt typeCheckInstr ext si

  (U.DROP, _ ::& rs) -> workOnInstr uInstr $ pure $ inp :/ DROP ::: rs

  (U.DROP, SNil) -> notEnoughItemsOnStack

  (U.DROPN nTotal, inputHST) -> workOnInstr uInstr $
    go nTotal inputHST <&> \case
      TCDropHelper s out -> inputHST :/ DROPN s ::: out
    where
      go :: forall inp. SingI inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDropHelper inp)
      go = curry \case
        (0, i) -> pure (TCDropHelper Zero i)

        (_, SNil) -> notEnoughItemsOnStack'

        (n, (_ ::& iTail)) -> do
          go (n - 1) iTail <&> \(TCDropHelper s out) -> TCDropHelper (Succ s) out

  (U.DUP vn1, a@(n :: SingT t, d) ::& rs) -> workOnInstr uInstr $ do
    Dict <-
      onScopeCheckInstrErr @t uInstr (SomeHST inp) Nothing $
      checkScope @(DupableScope t)
    pure (inp :/ AnnDUP (Anns1 vn1) ::: ((n, d) ::& a ::& rs))

  (U.DUP _vn, SNil) -> notEnoughItemsOnStack

  (U.DUPN vn nTotal, inputHST) -> workOnInstr uInstr $
    go nTotal inputHST <&> \(TCDupNHelper s out) -> inputHST :/ AnnDUPN (Anns1 vn) s ::: out
    where
      go :: forall inp. SingI inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDupNHelper inp)
      go = curry \case
        (_, SNil) -> notEnoughItemsOnStack'

        (0, _) ->
          typeCheckInstrErr' uInstr (SomeHST inp) Nothing (InvalidInstruction uInstr "'DUP n' expects n > 0")

        -- Don't bind whatever variable annotation is here because DUP n doesn't
        -- duplicate variable annotations. This is consistent with tezos-client.
        (1, i@((an :: SingT a, dict) ::& _)) -> do
          Dict <-
            onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing $
            checkScope @(DupableScope a)
          pure (TCDupNHelper One ((an, dict) ::& i))

        (n, (b ::& iTail)) ->
          go (n - 1) iTail <&> \(TCDupNHelper s@(Succ _) (a ::& resTail)) ->
            TCDupNHelper (Succ s) (a ::& b ::& resTail)

  (U.SWAP, a ::& b ::& rs) -> workOnInstr uInstr $
    pure (inp :/ SWAP ::: (b ::& a ::& rs))

  (U.SWAP, _) -> notEnoughItemsOnStack

  (U.DIG nTotal, inputHST) -> workOnInstr uInstr $
    go nTotal inputHST <&> \(TCDigHelper s out) -> inputHST :/ DIG s ::: out
    where
      go :: forall inp. SingI inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDigHelper inp)
      go = curry \case
        -- Even 'DIG 0' is invalid on empty stack (so it is not strictly `Nop`).
        (_, SNil) -> notEnoughItemsOnStack'

        (0, i@(_ ::& _)) -> pure (TCDigHelper Zero i \\ knownListFromSingI @inp)

        (n, (b ::& iTail)) ->
          go (n - 1) iTail <&> \(TCDigHelper s (a ::& resTail)) ->
            TCDigHelper (Succ s) (a ::& b ::& resTail)

  (U.DUG nTotal, inputHST) -> workOnInstr uInstr $
    go nTotal inputHST <&> \(TCDugHelper s out) -> inputHST :/ DUG s ::: out
    where
      go :: forall inp. SingI inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDugHelper inp)
      go = curry \case
        (0, i@(_ ::& _)) -> pure (TCDugHelper Zero i)

        (n, (a ::& b ::& iTail)) ->
          go (n - 1) (a ::& iTail) <&> \(TCDugHelper s resTail) ->
            TCDugHelper (Succ s) (b ::& resTail)

        -- Two cases:
        -- 1. Input stack is empty.
        -- 2. n > 0 and input stack has exactly 1 item.
        _ -> notEnoughItemsOnStack'

  (U.PUSH vn mt mval, i) -> workOnInstr uInstr $
    withUType mt $ \(nt :: Notes t) -> do
      -- Locally switch 'TypeCheckMode' to 'TypeCheckValue'.
      val <- local' (tcModeL .~ TypeCheckValue (mval, demote @t) Nothing) $
        typeCheckValImpl @t Nothing typeCheckInstr mval

      proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing
        $ checkScope @(ConstantScope t)
      case proofScope of
        Dict -> withWTPInstr @t $ pure $
          i :/ AnnPUSH (Anns2' vn nt) val ::: ((notesSing nt, Dict) ::& i)

  (U.SOME tn vn, (an, Dict) ::& rs) -> workOnInstr uInstr $
    pure (inp :/ AnnSOME (Anns2 tn vn) ::: ((STOption an, Dict) ::& rs))

  (U.SOME _ _, SNil) -> notEnoughItemsOnStack

  (U.NONE tn vn elMt, _) -> workOnInstr uInstr $
    withUType elMt $ \(elNotes :: Notes t) ->
      withWTPInstr @t $
        pure $ inp :/ AnnNONE (Anns3' tn vn elNotes) ::: ((STOption (notesSing elNotes), Dict) ::& inp)

  (U.UNIT tn vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnUNIT (Anns2 tn vn) ::: ((STUnit, Dict) ::& inp)

  (U.MIN_BLOCK_TIME vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnMIN_BLOCK_TIME vn ::: ((STNat, Dict) ::& inp)

  (U.IF_NONE mp mq, (STOption (asing :: SingT a), Dict) ::& rs) ->
    withWTPInstr' @a $
      genericIf IF_NONE U.IF_NONE mp mq rs ((asing, Dict) ::& rs) inp

  (U.IF_NONE _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("option 'a" :| []) :| []

  (U.IF_NONE _ _, SNil) -> notEnoughItemsOnStack

  (U.PAIR tn vn pfn qfn, (an :: SingT a, _) ::& (bn :: SingT b, _) ::& rs) -> workOnInstr uInstr $
    withWTPInstr @('TPair a b) $
      pure (inp :/ AnnPAIR (Anns4 tn vn pfn qfn) ::: ((STPair an bn, Dict) ::& rs))

  (U.PAIR {}, _) -> notEnoughItemsOnStack
  (U.UNPAIR instrVn1 instrVn2 instrFn1 instrFn2, (STPair n1 n2, Dict) ::& rs) ->
    workOnInstr uInstr $ do
      pure $
        inp :/ AnnUNPAIR (Anns4 instrVn1 instrVn2 instrFn1 instrFn2) :::
          ( (n1, Dict) ::&
            (n2, Dict) ::&
            rs
          )

  (U.UNPAIR {}, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("pair 'a 'b" :| []) :| []

  (U.UNPAIR {}, _) -> notEnoughItemsOnStack
  (U.PAIRN varAnn nTotal, _) -> workOnInstr uInstr $ do
    go nTotal inp <&> \case
      TCPairNHelper s out -> inp :/ AnnPAIRN (Anns1 varAnn) s ::: out
    where
      go :: forall inp. Word -> HST inp -> TypeCheckInstr (TCPairNHelper inp)
      go n hst
        | n < 2 =
            typeCheckInstrErr' uInstr (SomeHST inp) Nothing
              (InvalidInstruction uInstr "'PAIR n' expects n ≥ 2")
        | n == 2 =
            case hst of
              (an :: SingT a, _) ::& (bn :: SingT b, _) ::& hstTail -> do
                withWTPInstr @('TPair a b) $ do
                  pure $ TCPairNHelper Two $
                    (STPair an bn, Dict) ::& hstTail
              _ -> notEnoughItemsOnStack'
        | otherwise =
            case hst of
              (an :: SingT a, _) ::& hstTail@(_ ::& _ ::& _) -> do
                go (n - 1) hstTail >>= \case
                  TCPairNHelper nSing@(Succ (Succ _)) ((bn :: SingT b, _) ::& hstTail') -> do
                    withWTPInstr @('TPair a b) $ do
                      pure $ TCPairNHelper (Succ nSing) $
                        (STPair an bn, Dict) ::& hstTail'
              _ -> notEnoughItemsOnStack'

  (U.UNPAIRN _, SNil) -> notEnoughItemsOnStack
  (U.UNPAIRN nTotal, _ ::& _) -> workOnInstr uInstr $ do
    go nTotal inp <&> \case
      TCUnpairNHelper s out ->
        inp :/ UNPAIRN s ::: out
    where
      go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr (TCUnpairNHelper (x : xs))
      go n hst
        | n < 2 =
            typeCheckInstrErr' uInstr (SomeHST inp) Nothing
              (InvalidInstruction uInstr "UNPAIR expects an argument of at least 2.")
        | n == 2 =
            case hst of
              (STPair aT bT, Dict) ::& rest -> do
                pure $ TCUnpairNHelper Two $
                  (aT, Dict)
                  ::& (bT, Dict)
                  ::& rest
              _ -> unexpectedType
        | otherwise =
            case hst of
              (STPair aT bT, Dict) ::& rest -> do
                go (n - 1) ((bT, Dict) ::& rest) >>= \case
                  TCUnpairNHelper nSing@(Succ (Succ _)) out -> do
                    pure $ TCUnpairNHelper (Succ nSing) $
                      (aT, Dict) ::& out
              _ -> unexpectedType

      unexpectedType :: TypeCheckInstr a
      unexpectedType = failWithErr' $ UnexpectedType $ (pairWithElems nTotal :| []) :| []

  (U.CAR vn fn, (STPair lt _, Dict) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnCAR (Anns2 vn fn) ::: ((lt, Dict) ::& rs)

  (U.CAR _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("pair 'a 'b" :| []) :| []

  (U.CAR _ _, SNil) -> notEnoughItemsOnStack

  (U.CDR vn fn, (STPair _ rt, Dict) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnCDR (Anns2 vn fn) ::: ((rt, Dict) ::& rs)

  (U.CDR _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("pair 'a 'b" :| []) :| []

  (U.CDR _ _, SNil) -> notEnoughItemsOnStack

  (U.LEFT tn vn pfn qfn bMt, (an :: SingT l, Dict) ::& rs) ->
    withUType bMt $ \(bn :: Notes r) -> workOnInstr uInstr $ do
      withWTPInstr @r $ do
        let ns = STOr an (notesSing bn)
        pure (inp :/ AnnLEFT (Anns5' tn vn pfn qfn bn) ::: ((ns, Dict) ::& rs))

  (U.LEFT {}, SNil) -> notEnoughItemsOnStack

  (U.RIGHT tn vn pfn qfn aMt, (bn :: SingT r, Dict) ::& rs) ->
    withUType aMt $ \(an :: Notes l) -> workOnInstr uInstr $ do
      withWTPInstr @l $ do
        let ns = STOr (notesSing an) bn
        pure (inp :/ AnnRIGHT (Anns5' tn vn pfn qfn an) ::: ((ns, Dict) ::& rs))

  (U.RIGHT {}, SNil) -> notEnoughItemsOnStack

  (U.IF_LEFT mp mq, (STOr (lt :: SingT l) (rt :: SingT r), _) ::& rs) -> do
    withSingI lt $ withSingI rt $
      withWTPInstr' @l $
        withWTPInstr' @r $ do
          let
            ait = (lt, Dict) ::& rs
            bit = (rt, Dict) ::& rs
          genericIf IF_LEFT U.IF_LEFT mp mq ait bit inp

  (U.IF_LEFT _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("or 'a 'b" :| []) :| []

  (U.IF_LEFT _ _, SNil) -> notEnoughItemsOnStack

  (U.NIL tn vn elMt, i) -> workOnInstr uInstr $
    withUType elMt $ \(elNotes :: Notes t) ->
      withWTPInstr @('TList t) $
        pure $ i :/ AnnNIL (Anns3' tn vn elNotes) ::: ((STList (notesSing elNotes), Dict) ::& i)

  (U.CONS vn, ((_ :: SingT a), _) ::& ((ln :: SingT l), _) ::& rs) -> workOnInstr uInstr
    case eqType @('TList a) @l of
      Right Refl -> do
        withWTPInstr @('TList l) $
          pure $ inp :/ AnnCONS (Anns1 vn) ::: ((ln, Dict) ::& rs)
      Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just ConsArgument) m

  (U.CONS _, _) -> notEnoughItemsOnStack

  (U.IF_CONS mp mq, (ns@(STList (an :: SingT t1)), Dict) ::& rs) -> do
    withWTPInstr' @t1 $ do
      let ait = (an, Dict) ::& (ns, Dict) ::& rs
      genericIf IF_CONS U.IF_CONS mp mq ait rs inp

  (U.IF_CONS _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("list 'a" :| []) :| []

  (U.IF_CONS _ _, SNil)-> notEnoughItemsOnStack

  (U.SIZE vn, (STList{}, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (STSet{}, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (STMap{}, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (STString{}, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (STBytes{}, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("list 'a" :| []) :|
      [ ("set 'a" :| [])
      , ("map 'k 'v" :| [])
      , ("string" :| [])
      , ("bytes" :| [])
      ]

  (U.SIZE _, SNil) -> notEnoughItemsOnStack

  (U.EMPTY_SET tn vn mv, i) -> workOnInstr uInstr $
    withUType mv $ \(vns :: Notes v) ->
      withWTPInstr @('TSet v) $
        withCompareableCheck (notesSing vns) uInstr inp $
          i :/ AnnEMPTY_SET (Anns3' tn vn vns) ::: ((STSet (notesSing vns), Dict) ::& i)

  (U.EMPTY_MAP tn vn mk mv, i) -> workOnInstr uInstr $ do
    withUType mv $ \(vns :: Notes v)  ->
      withUType mk $ \(ktn :: Notes k) ->
        withWTPInstr @('TMap k v) $
          withCompareableCheck (notesSing ktn) uInstr inp $
            i :/ AnnEMPTY_MAP (Anns4'' tn vn ktn vns) ::: ((STMap (notesSing ktn) (notesSing vns), Dict) ::& i)

  (U.EMPTY_BIG_MAP tn vn mk mv, i) -> workOnInstr uInstr $
    withUType mv $ \(vns :: Notes v)  ->
      withUType mk $ \(ktn :: Notes k) ->
        withWTPInstr @('TBigMap k v) $
          withCompareableCheck (notesSing ktn) uInstr inp $
            i :/ AnnEMPTY_BIG_MAP (Anns4'' tn vn ktn vns) ::: ((STBigMap (notesSing ktn) (notesSing vns), Dict) ::& i)

  (U.MAP vn mp, (STList (vns :: SingT t1), Dict) ::& _) -> withSingI vns $ do
    withWTPInstr' @t1 $
      mapImpl (U.MAP vn) vns vn uInstr mp inp
        (\(rn :: SingT t) hst -> withWTPInstr @t $ pure $ (STList rn, Dict) ::& hst)

  (U.MAP vn mp, (STOption (vns :: SingT t1), Dict) ::& _) -> withSingI vns $ do
    withWTPInstr' @t1 $
      mapImpl (U.MAP vn) vns vn uInstr mp inp
        (\(rn :: SingT t) hst -> withWTPInstr @t $ pure $ (STOption rn, Dict) ::& hst)

  (U.MAP vn mp, (STMap (k :: SingT k) (v :: SingT v1), Dict) ::& _) -> withSingI k $ withSingI v $ do
    withWTPInstr' @('TPair k v1) $
      mapImpl (U.MAP vn) (STPair k v) vn uInstr mp inp
          (\(rn :: SingT v) hst -> withWTPInstr @('TMap k v) $ pure $ (STMap k rn, Dict) ::& hst)

  (U.MAP _ _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("list 'a" :| []) :|
      [ ("map 'k 'v" :| [])
      , ("option 'a" :| [])
      ]

  (U.MAP _ _, SNil) -> notEnoughItemsOnStack

  (U.ITER is, (STSet (s :: Sing t1), _) ::& _) -> withSingI s $ do
    withWTPInstr' @t1 $
      iterImpl s uInstr is inp

  (U.ITER is, (STList (l :: Sing t1), _) ::& _) -> withSingI l $ do
    withWTPInstr' @t1 $
      iterImpl l uInstr is inp

  (U.ITER is, (STMap (k :: SingT a) (v :: SingT b), _) ::& _) -> withSingI k $ withSingI v $ do
    withWTPInstr' @('TPair a b) $ iterImpl (STPair k v) uInstr is inp

  (U.ITER _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("set 'a" :| []) :|
      [ ("list 'a" :| [])
      , ("map 'k 'v" :| [])
      ]

  (U.ITER _, SNil) -> notEnoughItemsOnStack

  (U.MEM varNotes,
   _ ::& (STSet s, _) ::& _) -> withSingI s $ workOnInstr uInstr $
    memImpl inp varNotes
  (U.MEM varNotes,
   _ ::& (STMap k v, _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $
    memImpl inp varNotes
  (U.MEM varNotes,
   _ ::& (STBigMap k v, _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $
    memImpl inp varNotes
  (U.MEM _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("'a" :| ["set 'a"]) :|
      [ ("'k" :| ["map 'k 'v"])
      , ("'k" :| ["big_map 'k 'v"])
      ]

  (U.MEM _, _) -> notEnoughItemsOnStack

  (U.GET varNotes,
   _ ::& (STMap k (v :: SingT v), _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $ withWTPInstr @v $
      getImpl inp v varNotes
  (U.GET varNotes,
   _ ::& (STBigMap k (v :: SingT v), _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $ withWTPInstr @v $
      getImpl inp v varNotes

  (U.GET _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("'k" :| ["map 'k 'v"]) :|
      [ ("'k" :| ["big_map 'k 'v"])
      ]

  (U.GET _, _) -> notEnoughItemsOnStack

  (U.GETN _ _, SNil) -> notEnoughItemsOnStack
  (U.GETN getNVarAnn ix0, _ ::& _) -> workOnInstr uInstr $ do
    go ix0 inp <&> \case
      TCGetNHelper s out ->
        inp :/ AnnGETN (Anns1 getNVarAnn) s ::: out
    where
      go :: forall x xs. Word -> HST (x : xs) -> TypeCheckInstr (TCGetNHelper (x : xs))
      go 0 ((a, Dict) ::& rest) =
        pure $ TCGetNHelper Zero ((a, Dict) ::& rest)
      go 1 ((STPair leftNotes _, Dict) ::& rest) =
        pure $ TCGetNHelper One $ (leftNotes, Dict) ::& rest
      go ix ((STPair _ rightNotes, Dict) ::& rest) =
        go (ix - 2) ((rightNotes, Dict) ::& rest) <&> \(TCGetNHelper ixSing out) ->
          TCGetNHelper (Succ (Succ ixSing)) out
      go _ _ = failWithErr' $ UnexpectedType $ (pairWithNodeIndex ix0 :| []) :| []

  (U.UPDATE varAnn,
   _ ::& _ ::& (STMap k v, _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $ updImpl inp varAnn
  (U.UPDATE varAnn,
   _ ::& _ ::& (STBigMap k v, _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $ updImpl inp varAnn
  (U.UPDATE varAnn,
   _ ::& _ ::& (STSet s, _) ::& _) ->
    withSingI s $ workOnInstr uInstr $ updImpl inp varAnn

  (U.UPDATE _, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("'a" :| ["bool", "set 'a"]) :|
      [ ("'k" :| ["option 'v", "map 'k 'v"])
      , ("'k" :| ["option 'v", "big_map 'k 'v"])
      ]

  (U.UPDATE _, _) -> notEnoughItemsOnStack

  (U.UPDATEN updateNVarAnn ix0, _ ::& _ ::& _) -> workOnInstr uInstr $ do
    go ix0 inp <&> \case
      TCUpdateNHelper s out ->
        inp :/ AnnUPDATEN (Anns1 updateNVarAnn) s ::: out
    where
      go :: forall val pair rest. Word -> HST (val : pair : rest) -> TypeCheckInstr (TCUpdateNHelper (val : pair : rest))
      go 0 ((valNotes, Dict) ::& (_, _) ::& rest) =
        pure $ TCUpdateNHelper Zero $
          (valNotes, Dict) ::& rest
      go 1 ((valNotes, Dict) ::& (STPair _ rightNotes, Dict) ::& rest) =
        pure $ TCUpdateNHelper One $
          (STPair valNotes rightNotes, Dict) ::& rest
      go ix (val ::& (STPair leftNotes rightNotes, Dict) ::& rest) =
        go (ix - 2) (val ::& (rightNotes, Dict) ::& rest) <&>
          \(TCUpdateNHelper ixSing ((updatedRightNotes, Dict) ::& outRest)) ->
            TCUpdateNHelper (Succ (Succ ixSing)) $
              (STPair leftNotes updatedRightNotes, Dict) ::& outRest
      go _ _ = failWithErr' $ UnexpectedType $ ("'val" :| [pairWithNodeIndex ix0]) :| []
  (U.UPDATEN _ _, _) -> notEnoughItemsOnStack

  (U.GET_AND_UPDATE varAnn,
   _ ::& _ ::& (STMap k (v :: SingT v), _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $
      withWTPInstr @v $
        getUpdImpl inp varAnn
  (U.GET_AND_UPDATE varAnn,
   _ ::& _ ::& (STBigMap k (v :: SingT v), _) ::& _) ->
    withSingI k $ withSingI v $ workOnInstr uInstr $
      withWTPInstr @v $
        getUpdImpl inp varAnn
  (U.GET_AND_UPDATE _, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("'k" :| ["option 'v", "map 'k 'v"]) :|
      [ ("'k" :| ["option 'v", "big_map 'k 'v"])
      ]
  (U.GET_AND_UPDATE _, _) -> notEnoughItemsOnStack

  (U.IF mp mq, (STBool{}, _) ::& rs) ->
    genericIf IF U.IF mp mq rs rs inp

  (U.IF _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bool" :| []) :| []

  (U.IF _ _, SNil) -> notEnoughItemsOnStack

  (U.LOOP is, (STBool{}, _) ::& (rs :: HST rs)) -> do
    preserving (tcList is rs) U.LOOP $ \(_ :/ tp) ->
      case tp of
        subI ::: (o :: HST o) -> do
          case eqHST o (sing @'TBool -:& rs) of
            Right Refl -> pure $ inp :/ LOOP subI ::: rs
            Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m
        AnyOutInstr subI ->
          pure $ inp :/ LOOP subI ::: rs

  (U.LOOP _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("bool" :| []) :| []

  (U.LOOP _, _) -> notEnoughItemsOnStack

  (U.LOOP_LEFT is, (os@(STOr (an :: SingT t) (bn :: SingT b)), Dict) ::& rs) -> do
    withWTPInstr' @t $ withWTPInstr' @b $ do
      let ait = (an, Dict) ::& rs
      preserving (tcList is ait) U.LOOP_LEFT $ \(_ :/ tp) ->
        case tp of
          subI ::: o -> do
            case (eqHST o (os -:& rs), o) of
              (Right Refl, (_, Dict) ::& rs') ->
                  pure $ inp :/ LOOP_LEFT subI ::: ((bn, Dict) ::& rs')
              (Left m, _) -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m
          AnyOutInstr subI -> do
            let br = (bn, Dict)
            pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs)

  (U.LOOP_LEFT _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("or 'a 'b" :| []) :| []

  (U.LOOP_LEFT _, _) -> notEnoughItemsOnStack

  (U.LAMBDA vn p1@(AsUType (ins :: Notes t)) p2@(AsUType (ons :: Notes u)) is, i) -> do
    -- further processing is extracted into another function just not to
    -- litter our main typechecking logic
    withWTPInstr' @t $
      withWTPInstr' @u $
        lamImpl (U.LAMBDA vn p1 p2) (Anns3'' vn ins ons) uInstr is (notesSing ins) (notesSing ons) i

  (U.EXEC vn, ((_ :: SingT t1), _)
                              ::& ( STLambda (v :: SingT t1') (b :: SingT t2'), _)
                              ::& rs) -> withSingI v $ withSingI b $ workOnInstr uInstr $ do
    Refl <- errM $ eqType @t1 @t1'
    withWTPInstr @t2' $ pure $ inp :/ AnnEXEC (Anns1 vn) ::: ((b, Dict) ::& rs)
      where
        errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a
        errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)

  (U.EXEC _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("'a" :| ["lambda 'a 'b"]) :| []

  (U.EXEC _, _) -> notEnoughItemsOnStack

  (U.APPLY vn, ((_ :: SingT a'), _)
            ::& ( STLambda (STPair (lt :: SingT a) (rt :: SingT b) :: SingT t1) (b :: SingT t2), _)
            ::& rs) -> withSingI lt $ withSingI rt $ withSingI b $ workOnInstr uInstr $ do
    withWTPInstr @('TLambda t1 t2) $ do
      proofArgEq <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)
                    (eqType @a' @a)
      proofScope <- onScopeCheckInstrErr @a uInstr (SomeHST inp) (Just LambdaArgument)
        $ checkScope @(ConstantScope a)
      case (proofArgEq, proofScope) of
        (Refl, Dict) ->
          pure $ inp :/ AnnAPPLY @a (Anns1 vn) ::: ((STLambda rt b, Dict) ::& rs)

  (U.APPLY _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("'a" :| ["lambda (pair 'a 'b) 'c"]) :| []

  (U.APPLY _, _) -> notEnoughItemsOnStack

  (U.DIP is, a ::& s) -> do
    typeCheckDipBody U.DIP uInstr is s
      (IllTypedSeq)
      (\subI t -> WellTypedSeq $ inp :/ DIP subI ::: (a ::& t))

  (U.DIP _is, SNil) -> notEnoughItemsOnStack

  (U.DIPN nTotal instructions, inputHST) ->
    go nTotal inputHST <&> \case
      TCDipHelperErr err rest -> IllTypedSeq err rest
      TCDipHelperOk s subI out -> WellTypedSeq $ inputHST :/ DIPN s subI ::: out
    where
      go :: forall inp. SingI inp
        => Word
        -> HST inp
        -> TypeCheckInstrNoExcept (TCDipHelper inp)
      go n curHST = case (n, curHST) of
        (0, _) -> typeCheckDipBody (U.DIPN nTotal) uInstr instructions curHST
          (TCDipHelperErr)
          (TCDipHelperOk Zero)
        (_, SNil) -> do
          pos <- view tcieErrorPos
          let err = TCFailedOnInstr uInstr (SomeHST inp) pos Nothing (Just NotEnoughItemsOnStack)
          pure $ TCDipHelperErr err [NonTypedInstr $ U.PrimEx uInstr]
        (_, hstHead ::& hstTail) ->
          go (n - 1) hstTail <&> \case
          TCDipHelperOk s subI out -> TCDipHelperOk (Succ s) subI (hstHead ::& out)
          TCDipHelperErr err rest -> TCDipHelperErr err rest

  (U.FAILWITH, ((_ :: SingT a, _) ::& _)) -> workOnInstr uInstr $ do
    Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) (Just FailwithArgument)
      $ checkScope @(ConstantScope a)
    pure $ inp :/ AnyOutInstr FAILWITH

  (U.FAILWITH, _) -> notEnoughItemsOnStack

  (U.CAST vn (AsUType (castToNotes :: Notes t)), (_ :: SingT t1, _) ::& rs) ->
    workOnInstr uInstr $ do
      Refl <- errM $ eqType @t @t1
      withWTPInstr @t $
        pure $ inp :/ AnnCAST (Anns2' vn castToNotes) ::: ((notesSing castToNotes, Dict) ::& rs)
    where
      errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a
      errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just Cast)

  (U.CAST _ _, _) -> notEnoughItemsOnStack

  (U.RENAME vn, (an, Dict) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnRENAME (Anns1 vn) ::: ((an, Dict) ::& rs)

  (U.RENAME _, SNil) -> notEnoughItemsOnStack

  (U.UNPACK tn vn mt, (STBytes{}, _) ::& rs) -> workOnInstr uInstr $
    withUType mt $ \(tns :: Notes tn) -> do
      case NTOption tn tns of
        (ns :: Notes ('TOption t1)) -> withWTPInstr @('TOption t1) $ do
          Dict <- onScopeCheckInstrErr @tn uInstr (SomeHST inp) Nothing
            $ checkScope @(UnpackedValScope tn)
          pure $ inp :/ AnnUNPACK (Anns3' tn vn tns) ::: ((notesSing ns, Dict) ::& rs)

  (U.UNPACK {}, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []

  (U.UNPACK {}, SNil) -> notEnoughItemsOnStack

  (U.PACK vn, (_ :: SingT a, _) ::& rs) -> workOnInstr uInstr $ do
    Dict <- onScopeCheckInstrErr @a uInstr (SomeHST inp) Nothing
      $ checkScope @(PackedValScope a)
    pure $ inp :/ AnnPACK (Anns1 vn) ::: ((sing, Dict) ::& rs)

  (U.PACK _, SNil) -> notEnoughItemsOnStack

  (U.CONCAT vn, (STBytes{}, _) ::& (STBytes{}, _) ::& _) ->
    workOnInstr uInstr $ concatImpl inp vn
  (U.CONCAT vn, (STString{}, _) ::& (STString{}, _) ::& _) ->
    workOnInstr uInstr $ concatImpl inp vn
  (U.CONCAT vn, (STList STBytes, _) ::& _) ->
    workOnInstr uInstr $ concatImpl' inp vn
  (U.CONCAT vn, (STList STString, _) ::& _) ->
    workOnInstr uInstr $ concatImpl' inp vn
  (U.CONCAT _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("string" :| ["string"]) :|
      [ ("bytes" :| ["bytes"])
      , ("list string" :| ["list string"])
      , ("list bytes" :| ["list bytes"])
      ]
  (U.CONCAT _, SNil) -> notEnoughItemsOnStack

  (U.SLICE vn, (STNat{}, _) ::&
               (STNat{}, _) ::&
               (STString{}, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn
  (U.SLICE vn, (STNat{}, _) ::&
               (STNat{}, _) ::&
               (STBytes{}, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn

  (U.SLICE _, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("nat" :| ["nat", "string"]) :|
      [ ("nat" :| ["nat", "bytes"])
      ]
  (U.SLICE _, _) -> notEnoughItemsOnStack

  (U.ISNAT vn', (STInt{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnISNAT (Anns1 vn') ::: ((sing, Dict) ::& rs)

  (U.ISNAT _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []

  (U.ISNAT _, SNil)-> notEnoughItemsOnStack

  -- Type checking is already done inside `addImpl`.
  (U.ADD vn, (a, _) ::& (b, _) ::& _) -> workOnInstr uInstr $
    addImpl a b inp vn uInstr

  (U.ADD _, _) -> notEnoughItemsOnStack

  (U.SUB vn, (a, _) ::& (b, _) ::& _) -> workOnInstr uInstr $
    subImpl a b inp vn uInstr

  (U.SUB _, _) -> notEnoughItemsOnStack

  (U.SUB_MUTEZ vn, (STMutez, _) ::& (STMutez, _) ::& _) -> workOnInstr uInstr $
    arithImpl @SubMutez AnnSUB_MUTEZ inp vn uInstr
  (U.SUB_MUTEZ _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("mutez" :| ["mutez"]) :| []
  (U.SUB_MUTEZ _, _) -> notEnoughItemsOnStack

  (U.MUL vn, (a, _) ::& (b, _) ::& _) -> workOnInstr uInstr $
    mulImpl a b inp vn uInstr

  (U.MUL _, _) -> notEnoughItemsOnStack

  (U.EDIV vn, (a, _) ::& (b, _) ::& _) -> workOnInstr uInstr $
    edivImpl a b inp vn uInstr

  (U.EDIV _, _) -> notEnoughItemsOnStack

  (U.ABS vn, (STInt, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Abs (AnnABS (Anns1 vn)) inp vn
  (U.ABS _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []

  (U.ABS _, SNil) -> notEnoughItemsOnStack

  (U.NEG vn, (STInt, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Neg (AnnNEG (Anns1 vn)) inp vn
  (U.NEG vn, (STNat, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Neg (AnnNEG (Anns1 vn)) inp vn
  (U.NEG vn, (STBls12381Fr, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Neg (AnnNEG (Anns1 vn)) inp vn
  (U.NEG vn, (STBls12381G1, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Neg (AnnNEG (Anns1 vn)) inp vn
  (U.NEG vn, (STBls12381G2, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Neg (AnnNEG (Anns1 vn)) inp vn
  (U.NEG _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("int" :| []) :|
      [ ("nat" :| [])
      , ("bls12_381_fr" :| [])
      , ("bls12_381_g1" :| [])
      , ("bls12_381_g2" :| [])
      ]
  (U.NEG _, SNil) -> notEnoughItemsOnStack

  (U.LSL vn, (STNat, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Lsl AnnLSL inp vn uInstr
  (U.LSL _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| []
  (U.LSL _, _) -> notEnoughItemsOnStack

  (U.LSR vn, (STNat, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Lsr AnnLSR inp vn uInstr
  (U.LSR _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| []
  (U.LSR _, _) -> notEnoughItemsOnStack

  (U.OR vn, (STBool, _) ::&
            (STBool, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Or AnnOR inp vn uInstr
  (U.OR vn, (STNat, _) ::&
            (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Or AnnOR inp vn uInstr
  (U.OR _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("bool" :| ["bool"]) :|
      [ ("nat" :| ["nat"])
      ]
  (U.OR _, _) -> notEnoughItemsOnStack

  (U.AND vn, (STInt, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @And AnnAND inp vn uInstr
  (U.AND vn, (STNat, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @And AnnAND inp vn uInstr
  (U.AND vn, (STBool, _) ::&
             (STBool, _) ::& _) -> workOnInstr uInstr $
    arithImpl @And AnnAND inp vn uInstr
  (U.AND _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("int" :| ["nat"]) :|
      [ ("nat" :| ["nat"])
      , ("bool" :| ["bool"])
      ]
  (U.AND _, _) -> notEnoughItemsOnStack

  (U.XOR vn, (STBool, _) ::&
             (STBool, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Xor AnnXOR inp vn uInstr
  (U.XOR vn, (STNat, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Xor AnnXOR inp vn uInstr
  (U.XOR _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("bool" :| ["bool"]) :|
      [ ("nat" :| ["nat"])
      ]
  (U.XOR _, _) -> notEnoughItemsOnStack

  (U.NOT vn, (STNat, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Not (AnnNOT (Anns1 vn)) inp vn
  (U.NOT vn, (STBool, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Not (AnnNOT (Anns1 vn)) inp vn
  (U.NOT vn, (STInt, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Not (AnnNOT (Anns1 vn)) inp vn
  (U.NOT _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("nat" :| []) :|
      [ ("bool" :| [])
      , ("int" :| [])
      ]
  (U.NOT _, SNil) -> notEnoughItemsOnStack

  (U.COMPARE vn,
        (_ :: SingT aT, _)
    ::& (_ :: SingT bT, _)
    ::& rs
    )
    -> workOnInstr uInstr $ do
    case eqType @aT @bT of
      Right Refl -> do
        proofScope <- onScopeCheckInstrErr @aT (U.COMPARE vn) (SomeHST inp) (Just ComparisonArguments)
          $ checkScope @(ComparabilityScope aT)
        case proofScope of
          Dict ->
            pure $ inp :/ AnnCOMPARE (Anns1 vn) ::: ((sing, Dict) ::& rs)

      Left err -> do
        typeCheckInstrErr' uInstr (SomeHST inp) (Just ComparisonArguments) err

  (U.COMPARE _, _) -> notEnoughItemsOnStack

  (U.EQ vn, (STInt{}, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Eq' (AnnEQ (Anns1 vn)) inp vn
  (U.EQ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []
  (U.EQ _, SNil) -> notEnoughItemsOnStack

  (U.NEQ vn, (STInt{}, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Neq (AnnNEQ (Anns1 vn)) inp vn
  (U.NEQ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []
  (U.NEQ _, SNil) -> notEnoughItemsOnStack

  (U.LT vn, (STInt{}, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Lt (AnnLT (Anns1 vn)) inp vn
  (U.LT _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []
  (U.LT _, SNil) -> notEnoughItemsOnStack

  (U.GT vn, (STInt{}, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Gt (AnnGT (Anns1 vn)) inp vn
  (U.GT _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []
  (U.GT _, SNil) -> notEnoughItemsOnStack

  (U.LE vn, (STInt{}, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Le (AnnLE (Anns1 vn)) inp vn
  (U.LE _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []
  (U.LE _, SNil) -> notEnoughItemsOnStack

  (U.GE vn, (STInt{}, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImpl @Ge (AnnGE (Anns1 vn)) inp vn
  (U.GE _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| []
  (U.GE _, SNil) -> notEnoughItemsOnStack

  (U.INT vn, (STNat{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnINT (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.INT vn, (STBls12381Fr{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnINT (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.INT _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("nat" :| []) :| ["bls12_381_fr" :| []]
  (U.INT _, SNil) -> notEnoughItemsOnStack

  (U.VIEW vn name (AsUType (retNotes :: Notes ret)), _ ::& (STAddress{}, _) ::& rs) ->
    workOnInstr uInstr $
      withWTPInstr @ret $ do
        Dict <- onScopeCheckInstrErr @ret uInstr (SomeHST inp) Nothing
              $ checkScope @(ViewableScope ret)
        pure $ inp :/ AnnVIEW (Anns2' vn retNotes) name ::: ((STOption (notesSing retNotes), Dict) ::& rs)
  (U.VIEW{}, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("'arg" :| ["address"]) :| []
  (U.VIEW{}, _) -> notEnoughItemsOnStack

  (U.SELF vn fn, _) -> workOnInstr uInstr $ withNotInView uInstr do
    mode <- asks' tcMode
    case mode of
      TypeCheckValue (value, ty) _ ->
        tcFailedOnValue value ty "The SELF instruction cannot appear in a lambda" Nothing
      TypeCheckContract (SomeParamType notescp) -> do
        let epName = U.epNameFromSelfAnn fn
        MkEntrypointCallRes (argNotes :: Notes arg) epc <-
          mkEntrypointCall epName notescp
            & maybeToRight (EntrypointNotFound epName)
            & onTypeCheckInstrErr uInstr (SomeHST inp) Nothing

        case NTContract U.noAnn argNotes of
                (ntRes :: Notes ('TContract t1)) ->
                  withWTPInstr @('TContract t1) $
                    pure $ inp :/ AnnSELF @arg (Anns1 vn) (SomeEpc epc) ::: ((notesSing ntRes, Dict) ::& inp)
      TypeCheckTest ->
        failWithErr' $ InvalidInstruction uInstr "'SELF' appears in test typechecking"
  (U.CONTRACT vn fn mt, (STAddress{}, _) ::& rs) -> workOnInstr uInstr $
    withUType mt $ \(tns :: Notes t) -> do
      proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)
        $ checkScope @(ParameterScope t)
      let ns = NTOption def $ NTContract def tns
      epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing
        $ epNameFromRefAnn fn `onFirst` IllegalEntrypoint
      case proofScope of
        Dict ->
          withWTPInstr @t $ pure $ inp :/ AnnCONTRACT (Anns2' vn tns) epName ::: ((notesSing ns, Dict) ::& rs)

  (U.CONTRACT {}, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("address" :| []) :| []
  (U.CONTRACT {}, SNil) -> notEnoughItemsOnStack

  (U.TRANSFER_TOKENS vn, ((_ :: SingT p'), _)
    ::& (STMutez{}, _)
    ::& (STContract (s :: Sing p), _) ::& rs) -> withSingI s $ workOnInstr uInstr $
      withNotInView uInstr do
        proofScope <- onScopeCheckInstrErr @p uInstr (SomeHST inp) (Just ContractParameter)
          $ checkScope @(ParameterScope p)
        case (eqType @p @p', proofScope) of
          (Right Refl, Dict) ->
            pure $ inp :/ AnnTRANSFER_TOKENS (Anns1 vn) ::: ((sing, Dict) ::& rs)
          (Left m, _) ->
            typeCheckInstrErr' uInstr (SomeHST inp) (Just ContractParameter) m

  (U.TRANSFER_TOKENS _, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("'p" :| ["mutez", "contract 'p"]) :| []

  (U.TRANSFER_TOKENS _, _) -> notEnoughItemsOnStack

  (U.SET_DELEGATE vn,
    (STOption STKeyHash, _)
    ::& rs) -> workOnInstr uInstr $ withNotInView uInstr do
      pure $ inp :/ AnnSET_DELEGATE (Anns1 vn) ::: ((sing, Dict) ::& rs)

  (U.SET_DELEGATE _,  _ ::& _) ->
    failWithErr $ UnexpectedType $ ("option key_hash" :| []) :| []

  (U.SET_DELEGATE _, _) -> notEnoughItemsOnStack

  (U.CREATE_CONTRACT ovn avn contract,
    (STOption STKeyHash, _)
    ::& (STMutez{}, _)
    ::& (_ :: SingT g, Dict) ::& rs) -> workOnInstr uInstr $ withNotInView uInstr do
      (SomeContract contr@(Contract _ _ (_ :: Notes st) _ _))
        <- lift $ typeCheckContractImpl contract
      Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just ContractStorage) $
        eqType @g @st
      pure
        $ inp :/ AnnCREATE_CONTRACT (Anns2 ovn avn) contr
        ::: ((sing, Dict) ::& (sing, Dict) ::& rs)

  (U.CREATE_CONTRACT {}, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("option key_hash" :| ["mutez", "'a"]) :| []

  (U.CREATE_CONTRACT {},  _) -> notEnoughItemsOnStack

  (U.IMPLICIT_ACCOUNT vn, (STKeyHash{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnIMPLICIT_ACCOUNT (Anns1 vn) ::: ((sing, Dict) ::& rs)

  (U.IMPLICIT_ACCOUNT _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("key_hash" :| []) :| []
  (U.IMPLICIT_ACCOUNT _, SNil) -> notEnoughItemsOnStack

  (U.NOW vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnNOW (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.AMOUNT vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnAMOUNT (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.BALANCE vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnBALANCE (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.VOTING_POWER vn, (STKeyHash{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnVOTING_POWER (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.VOTING_POWER _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("key_hash" :| []) :| []
  (U.VOTING_POWER _, SNil) -> notEnoughItemsOnStack

  (U.TOTAL_VOTING_POWER vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnTOTAL_VOTING_POWER (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.CHECK_SIGNATURE vn,
             (STKey{}, _)
             ::& (STSignature{}, _) ::& (STBytes{}, _) ::& rs) ->
    workOnInstr uInstr $
      pure $ inp :/ AnnCHECK_SIGNATURE (Anns1 vn) ::: ((sing, Dict) ::& rs)

  (U.CHECK_SIGNATURE _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("key" :| ["signature", "bytes"]) :| []
  (U.CHECK_SIGNATURE _, _) -> notEnoughItemsOnStack

  (U.SHA256 vn, (STBytes{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnSHA256 (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.SHA256 _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []
  (U.SHA256 _, SNil) -> notEnoughItemsOnStack

  (U.SHA512 vn, (STBytes{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnSHA512 (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.SHA512 _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []
  (U.SHA512 _, SNil) -> notEnoughItemsOnStack

  (U.BLAKE2B vn, (STBytes{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnBLAKE2B (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.BLAKE2B _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []
  (U.BLAKE2B _, SNil) -> notEnoughItemsOnStack

  (U.SHA3 vn, (STBytes{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnSHA3 (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.SHA3 _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []
  (U.SHA3 _, SNil) -> notEnoughItemsOnStack

  (U.KECCAK vn, (STBytes{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnKECCAK (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.KECCAK _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("bytes" :| []) :| []
  (U.KECCAK _, SNil) -> notEnoughItemsOnStack

  (U.HASH_KEY vn, (STKey{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnHASH_KEY (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.HASH_KEY _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("key" :| []) :| []
  (U.HASH_KEY _, SNil) -> notEnoughItemsOnStack

  (U.PAIRING_CHECK vn, (STList (STPair STBls12381G1 STBls12381G2), _) ::& rs) ->
    workOnInstr uInstr $
      pure $ inp :/ AnnPAIRING_CHECK (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.PAIRING_CHECK _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("list (pair bls12_381_g1 bls12_381_g2)" :| []) :| []
  (U.PAIRING_CHECK _, SNil) -> notEnoughItemsOnStack

  (U.SOURCE vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnSOURCE (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.SENDER vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnSENDER (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.ADDRESS vn, (STContract{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnADDRESS (Anns1 vn) ::: ((sing, Dict) ::& rs)

  (U.ADDRESS _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("contract 'p" :| []) :| []
  (U.ADDRESS _, SNil) -> notEnoughItemsOnStack

  (U.CHAIN_ID vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnCHAIN_ID (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.LEVEL vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnLEVEL (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.SELF_ADDRESS vn, _) -> workOnInstr uInstr $
    pure $ inp :/ AnnSELF_ADDRESS (Anns1 vn) ::: ((sing, Dict) ::& inp)

  (U.NEVER, (STNever{}, _) ::& _) -> workOnInstr uInstr $
    pure $ inp :/ AnyOutInstr NEVER
  (U.NEVER, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("never" :| []) :| []
  (U.NEVER, SNil) -> notEnoughItemsOnStack

  (U.TICKET vn, (stVal :: Sing v, _) ::& (STNat{}, _) ::& rs) -> workOnInstr uInstr $
    withWTPInstr @v $
    withCompareableCheck stVal uInstr inp $
      inp :/ AnnTICKET (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.TICKET _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("a'" :| ["nat"]) :| []
  (U.TICKET _, _) -> notEnoughItemsOnStack

  (U.READ_TICKET vn, ticket@(STTicket{}, Dict) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ AnnREAD_TICKET (Anns1 vn) ::: ((sing, Dict) ::& ticket ::& rs)
  (U.READ_TICKET _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("ticket 'a" :| []) :| []
  (U.READ_TICKET _, _) -> notEnoughItemsOnStack

  (U.SPLIT_TICKET vn, (STTicket{}, Dict) ::& (STPair STNat{} STNat{}, _) ::& rs) ->
    workOnInstr uInstr $
      pure $ inp :/ AnnSPLIT_TICKET (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.SPLIT_TICKET _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("pair nat nat" :| ["ticket 'a"]) :| []
  (U.SPLIT_TICKET _, _) -> notEnoughItemsOnStack

  (U.JOIN_TICKETS vn,
     (STPair (nt1@STTicket{} :: SingT t1) (STTicket{} :: SingT t2), Dict) ::& rs) ->
    workOnInstr uInstr $ do
      Refl <-
        onTypeCheckInstrErr uInstr (SomeHST inp) (Just TicketsJoin) $
          eqType @t1 @t2
      pure $ inp :/ AnnJOIN_TICKETS (Anns1 vn) ::: ((STOption nt1, Dict) ::& rs)
  (U.JOIN_TICKETS _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("pair (ticket 'a) (ticket 'a)" :| []) :| []
  (U.JOIN_TICKETS _, _) -> notEnoughItemsOnStack

  (U.OPEN_CHEST vn,
      (STChestKey, Dict)
      ::& (STChest, Dict)
      ::& (STNat, Dict)
      ::& rs) ->
      workOnInstr uInstr $ do
        pure $ inp :/ AnnOPEN_CHEST (Anns1 vn) ::: (
          (STOr STBytes STBool, Dict)
          ::& rs)
  (U.OPEN_CHEST _, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("chest_key" :| ["chest", "nat"]) :| []
  (U.OPEN_CHEST _, _) -> notEnoughItemsOnStack

  (U.SAPLING_EMPTY_STATE vn n, _) -> workOnInstr uInstr $
    (\(SomeSing (s :: Sing a)) -> withSingI s $
      pure $ inp :/ AnnSAPLING_EMPTY_STATE (Anns1 vn) s ::: ((sing, Dict) ::& inp)
    ) $ Peano.someSingNat n

  (U.SAPLING_VERIFY_UPDATE vn,
      (STSaplingTransaction s1, Dict)
      ::& (STSaplingState s2, Dict)
      ::& rs) ->
      workOnInstr uInstr $
        case testEquality s1 s2 of
          Just Refl ->
            pure $ inp :/ AnnSAPLING_VERIFY_UPDATE (Anns1 vn) ::: (
              (STOption (STPair STBytes (STPair STInt (STSaplingState s1))), Dict)
              ::& rs)
          Nothing -> failWithErr' $ InvalidInstruction uInstr
            "Memo sizes of two sapling states or transactions do not match."

  (U.SAPLING_VERIFY_UPDATE _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("sapling_transaction" :| ["sapling_state"]) :| []
  (U.SAPLING_VERIFY_UPDATE _, _) -> notEnoughItemsOnStack

  (U.EMIT{}, SNil) -> notEnoughItemsOnStack

  (U.EMIT va tag mty, ((_ :: SingT t2), Dict) ::& rs) ->
    workOnInstr uInstr do
      Dict <- onScopeCheckInstrErr @t2 uInstr (SomeHST inp) Nothing $
        checkScope @(PackedValScope t2)
      case mty of
        Just (AsUType (ty :: Notes t1)) -> do
          Refl <- errM $ eqType @t1 @t2
          pure $ inp :/ AnnEMIT (Anns1 va) tag (Just ty) ::: ((sing, Dict) ::& rs)
        Nothing ->
          pure $ inp :/ AnnEMIT (Anns1 va) tag Nothing ::: ((sing, Dict) ::& rs)
      where
        errM :: (MonadReader TypeCheckInstrEnv m, MonadError TCError m) => Either TCTypeError a -> m a
        errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just EmitArgument)

  where
    withWTPInstr'
      :: forall t inp. SingI t
      => (WellTyped t => TypeCheckInstrNoExcept (TypeCheckedSeq inp))
      -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
    withWTPInstr' = withWTPInstr'_ @t uInstr (SomeHST inp)

    withWTPInstr
      :: forall t a. SingI t => (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
    withWTPInstr = withWTPInstr_ @t uInstr (SomeHST inp)

    failWithErr :: TCTypeError -> TypeCheckInstrNoExcept (TypeCheckedSeq a)
    failWithErr = workOnInstr uInstr . failWithErr'

    failWithErr' :: TCTypeError -> TypeCheckInstr a
    failWithErr' = typeCheckInstrErr' uInstr (SomeHST inp) Nothing

    notEnoughItemsOnStack :: TypeCheckInstrNoExcept (TypeCheckedSeq a)
    notEnoughItemsOnStack = failWithErr NotEnoughItemsOnStack

    notEnoughItemsOnStack' :: TypeCheckInstr a
    notEnoughItemsOnStack' = failWithErr' NotEnoughItemsOnStack

    withNotInView :: U.ExpandedInstr -> (IsNotInView => TypeCheckInstr r) -> TypeCheckInstr r
    withNotInView instr act = asks' tcMode >>= \case
      -- we provide the not-in-view constraint in the isolated mode
      TypeCheckTest -> giveNotInView act
      _ -> view tcieNotInView >>= \case
        Just Dict -> act
        Nothing -> failWithErr' $
          InvalidInstruction instr "This instruction cannot be used on the top level of a view"

-- | Helper function for two-branch if where each branch is given a single
-- value.
genericIf
  :: forall bti bfi cond rs .
    (SingI bti, SingI bfi)
  => (forall s'.
        Instr bti s' ->
        Instr bfi s' ->
        Instr (cond ': rs) s'
     )
  -> (forall op. [op] -> [op] -> U.InstrAbstract op)
  -> [U.ExpandedOp]
  -> [U.ExpandedOp]
  -> HST bti
  -> HST bfi
  -> HST (cond ': rs)
  -> TypeCheckInstrNoExcept (TypeCheckedSeq (cond ': rs))
genericIf cons mCons mbt mbf bti bfi i@(_ ::& _) = do
  let cons1 opsT = mCons opsT (map (IllTypedOp . NonTypedInstr) mbf)
  preserving' (tcList mbt bti) cons1 $ \tInstr@(_ :/ pinstr) -> do
    let cons2 opsF = mCons [someInstrToOp tInstr] opsF
    preserving (tcList mbf bfi) cons2 $ \(_ :/ qinstr) -> do
      fmap (i :/) $ case (pinstr, qinstr) of
        (p ::: po, q ::: qo) -> do
          let instr = mCons mbt mbf
          Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just If)
            $ eqHST po qo
          pure $ cons p q ::: qo
        (AnyOutInstr p, q ::: qo) -> do
          pure $ cons p q ::: qo
        (p ::: po, AnyOutInstr q) -> do
          pure $ cons p q ::: po
        (AnyOutInstr p, AnyOutInstr q) ->
          pure $ AnyOutInstr (cons p q)

mapImpl
  :: forall c rs.
    ( MapOp c
    , WellTyped (MapOpInp c)
    , SingIOne (MapOpRes c)
    )
  => ([TypeCheckedOp] -> TypeCheckedInstr)
  -> SingT (MapOpInp c)
  -> VarAnn
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST (c ': rs)
  -> (forall v'. (SingI v') =>
        SingT v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs)))
  -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs))
mapImpl cons vn anns instr mp i@(_ ::& rs) mkRes = do
  preserving (tcList mp ((vn, Dict) ::& rs)) cons $ \(_ :/ subp) ->
    case subp of
      sub ::: subo ->
        case subo of
          (bn :: SingT v', _) ::& rs' -> do
            Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)
              $ eqHST rs rs'
            x <- mkRes bn rs'
            pure $ i :/ withSingIOne @(MapOpRes c) @v' (AnnMAP (Anns1 anns) sub ::: x)
          _ -> typeCheckInstrErr instr (SomeHST i) (Just Iteration)
      AnyOutInstr _ ->
        typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails

iterImpl
  :: forall c rs .
    ( IterOp c
    , WellTyped (IterOpEl c)
    )
  => SingT (IterOpEl c)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST (c ': rs)
  -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs))
iterImpl en instr mp i@((_, _) ::& rs) = do
  let tcAction = case mp of
        [] -> workOnInstr instr
          (typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode)
        _ -> typeCheckImpl typeCheckInstr mp ((en, Dict) ::& rs)
  preserving tcAction U.ITER $ \(_ :/ subp) -> case subp of
    subI ::: o -> do
      Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration) $ eqHST o rs
      pure $ i :/ ITER subI ::: o
    AnyOutInstr subI ->
      pure $ i :/ ITER subI ::: rs

lamImpl
  :: forall it ot ts .
    ( WellTyped it, WellTyped ot
    , SingI ts
    )
  => ([TypeCheckedOp] -> TypeCheckedInstr)
  -> Anns '[VarAnn, Notes it, Notes ot]
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> SingT it
  -> SingT ot
  -> HST ts
  -> TypeCheckInstrNoExcept (TypeCheckedSeq ts)
lamImpl cons anns instr is ins ons i =
  guarding_ instr
    (whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr -> do
      let err = InvalidInstruction selfInstr "SELF instruction cannot be used in a LAMBDA"
      typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) err) $
    preserving tcInstr cons $ \(_ :/ lamI) -> do
      let lamNotes onsr = STLambda ins onsr
      let lamSt onsr = (lamNotes onsr, Dict) ::& i
      fmap (i :/) $ case lamI of
        lam ::: lo -> do
          case eqHST1 @ot lo of
            Right Refl -> do
                pure (AnnLAMBDA anns (VLam $ RfNormal lam) ::: lamSt ons)
            Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) m
        AnyOutInstr lam ->
          pure (AnnLAMBDA anns (VLam $ RfAlwaysFails lam) ::: lamSt ons)
  where
    tcInstr = giveNotInView $ local (set tcieNotInView $ Just Dict) $ tcList is ((ins, Dict) ::& SNil)
    hasSelf :: U.ExpandedOp -> First U.ExpandedInstr
    hasSelf = everything (<>)
      (mkQ (First Nothing)
       (\case
           selfInstr@(U.SELF{} :: U.InstrAbstract U.ExpandedOp) -> First $ Just selfInstr
           _ -> First Nothing
       )
      )

----------------------------------------------------------------------------
-- Helpers for DIP (n) typechecking
----------------------------------------------------------------------------

-- Helper data type we use to typecheck DIPN.
data TCDipHelper inp where
  TCDipHelperOk ::
    forall (n :: Peano) inp out s s'.
    (SingI out, ConstraintDIPN n inp out s s') =>
    PeanoNatural n -> Instr s s' -> HST out -> TCDipHelper inp
  TCDipHelperErr :: TCError -> [IllTypedInstr] -> TCDipHelper inp

typeCheckDipBody
  :: SingI inp
  => ([TypeCheckedOp] -> TypeCheckedInstr)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST inp
  -> (TCError -> [IllTypedInstr] -> r)
  -> (forall out. SingI out => Instr inp out -> HST out -> r)
  -> TypeCheckInstrNoExcept r
typeCheckDipBody cons mainInstr instructions inputHST onErr onOk = do
  listRes <- tcList instructions inputHST
  pos <- view tcieErrorPos
  pure $ listRes & tcsEither
    (\tcOps err -> onErr err [SemiTypedInstr $ cons tcOps])
    (\someInstr@(_ :/ iAndOut) -> case iAndOut of
        AnyOutInstr _ ->
        -- This may seem like we throw error because of despair, but in fact,
        -- the reference implementation seems to behave exactly in this way -
        -- if output stack of code block within @DIP@ occurs to be any, an
        -- error "FAILWITH must be at tail position" is raised.
        -- It is not allowed even in `DIP 0`.
          let err = TCFailedOnInstr mainInstr
                                    (SomeHST inputHST)
                                    pos
                                    (Just DipCode)
                                    (Just CodeAlwaysFails)
          in onErr err [SemiTypedInstr $ cons [someInstrToOp someInstr]]
        subI ::: t -> onOk subI t)