-- 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
-- @SomeTcInstr@ 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 @SomeTcInstr@ 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
    , typeCheckContract'
    , typeCheckContractAndStorage
    , typeCheckContractAndStorage'
    , typeCheckInstr
    , typeCheckList
    , tcList
    , typeCheckListNoExcept
    , typeCheckParameter
    , typeCheckStorage
    , typeCheckTopLevelType
    , typeCheckTopLevelType'
    , typeCheckViews
    , typeCheckView'
    , typeCheckViews'
    , typeCheckValue
    , typeCheckValueRunCodeCompat
    , typeCheckExpandedOp
    , typeVerifyContract
    , typeVerifyContract'
    , typeVerifyParameter
    , typeVerifyStorage
    , typeVerifyTopLevelType
    , typeVerifyView
    , typeVerifyView'
    ) where

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, catchError, liftEither, throwError)
import Data.Coerce (coerce)
import Data.Constraint ((\\))
import Data.Default (Default(def))
import Data.Generics (everything, mkQ)
import Data.Singletons (Sing, SomeSing(..), demote, withSingI)
import Data.Type.Equality (TestEquality(..))
import Data.Typeable ((:~:)(..))
import Fmt (pretty)

import Morley.Michelson.ErrorPos (ErrorSrcPos)
import Morley.Michelson.Internal.ViewsSet as VS
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.Michelson.Typed.Instr.Constraints

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 U.ExpandedOp SomeContractAndStorage
typeCheckContractAndStorage = typeCheckContractAndStorage' typeCheckExpandedOp

typeCheckContractAndStorage'
  :: IsInstrOp op
  => TcInstrBase op -> U.Contract' op -> U.Value' [] op -> TypeCheckResult op SomeContractAndStorage
typeCheckContractAndStorage' tcOp uContract uStorage = do
  SomeContract (contract@Contract{} :: Contract cp st) <- typeCheckContract' tcOp uContract
  storage <- typeVerifyStorage' @st tcOp uStorage
  pure $ SomeContractAndStorage contract storage

typeCheckContract
  :: U.Contract
  -> TypeCheckResult U.ExpandedOp SomeContract
typeCheckContract = typeCheckContract' typeCheckExpandedOp

typeCheckContract'
  :: TcInstrBase op
  -> U.Contract' op
  -> TypeCheckResult op SomeContract
typeCheckContract' tcOp c = do
  paramType <- liftEither $ first (TcContractError "illegal parameter declaration: " . Just ) $
    mkSomeParamType (U.contractParameter c)
  runTypeCheck (TypeCheckContract paramType) $ doTypeCheckContract' tcOp c

typeVerifyContract
  :: forall cp st.
     (SingI cp, SingI st)
  => U.Contract -> TypeCheckResult U.ExpandedOp (Contract cp st)
typeVerifyContract = typeVerifyContract' typeCheckExpandedOp

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

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

withWTPInstr_ :: forall t op a. SingI t => U.InstrAbstract [] op -> SomeHST -> (WellTyped t => TypeCheckInstr op a) -> TypeCheckInstr op 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 op inp. (SingI t, IsInstrOp op)
  => U.InstrAbstract [] op
  -> SomeHST
  -> (WellTyped t => TypeCheckInstrNoExcept op (TypeCheckedSeq op inp))
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op 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 $ liftInstr v]

doTypeCheckContract'
  :: forall op. TcInstrBase op
  -> U.Contract' op
  -> TypeCheck op SomeContract
doTypeCheckContract' tcOp uContract@(U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder uViews) = do
  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 $
            giveNotInView $ local (set tcieNotInView $ Just Dict) $
            tcOp pCode inp
          instr@(_ :/ instrOut) <-
            tcsEither onFailedCodeTypeCheck pure codeRes

          -- typecheck views
          cViews <- typeCheckViews' tcOp
            uContract{ U.contractCode = someInstrToOp instr, U.contractViews = def }
            storageNote uViews

          let tcViews = coerce $ someViewToOp @_ @op <$> coerce @_ @(ViewsSetF (SomeView st)) cViews
          handleError (onFailedFullTypeCheck (someInstrToOp instr) tcViews) $ 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
            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 op a
    hasTypeError name reason = throwError $
      TcContractError ("contract " <> name <> " type error") $
      Just $ UnsupportedTypeForScope (demote @t) reason

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

    onFailedFullTypeCheck :: TypeCheckedOp op -> U.ViewsSet (TypeCheckedOp op) -> TcError' op -> TypeCheck op a
    onFailedFullTypeCheck ops views err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TcIncompletelyTyped err U.Contract
             { contractParameter = wholeParam
             , contractStorage = mStorage
             , contractCode = TCOpSeq [ops]
             , entriesOrder = entriesOrder
             , contractViews = TCOpSeq . one <$> views
             }
        else err

typeVerifyView
  :: forall arg ret st.
     (SingI arg, SingI ret, WellTyped st)
  => Notes st -> U.View -> TypeCheckResult U.ExpandedOp (View arg st ret)
typeVerifyView = typeVerifyView' typeCheckExpandedOp

typeVerifyView'
  :: forall arg ret st op.
     (SingI arg, SingI ret, WellTyped st)
  => TcInstrBase op -> Notes st -> U.View' op -> TypeCheckResult op (View arg st ret)
typeVerifyView' tcOp notes v = do
  SomeView (tcView@View{} :: View arg' st' ret') <-
    runTypeCheck TypeCheckTest $ typeCheckView' tcOp 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 op any
    mkErr tyDesc merr =
      throwError $ TcContractError "error in view type" $ Just $
          UnexpectedTopLevelType tyDesc merr

typeCheckView'
  :: WellTyped st
  => TcInstrBase op
  -> Notes st
  -> U.View' op
  -> TypeCheck op (SomeView st)
typeCheckView' tcOp 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 $
      tcOp 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' op -> [TypeCheckedOp op] -> TcError' op -> TypeCheck op a
    onFailedViewsTypeCheck v viewOps err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TcIncompletelyTypedView err v{ U.viewCode = TCOpSeq viewOps }
        else err

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

typeCheckViews'
  :: forall st op.
     WellTyped st
  => TcInstrBase op
  -> U.Contract' (TypeCheckedOp op)
  -> Notes st
  -> U.ViewsSet op
  -> TypeCheck op (ViewsSet st)
typeCheckViews' doTypeCheckOp tcContract storageNote cViews = coerce $
  coerce cViews & runningTotalMapM \processedViews name uView -> do
    typeCheckView' doTypeCheckOp storageNote uView
    `catchError` \case
      TcIncompletelyTypedView err view' ->
        let tcViews = fmap (TCOpSeq . one) . someViewToOp <$> processedViews
        in onFailedViewsTypeCheck (coerce $ unsafeInsert name view' tcViews) err
      err -> throwError err
  where
    -- NB: since we only walk one map and build another one using the same keys,
    -- this is actually safe, but be mindful of this when changing this code.
    unsafeInsert :: ViewName -> a -> ViewsSetF a -> ViewsSetF a
    unsafeInsert = unsafe ... VS.addViewToSet . const

    onFailedViewsTypeCheck :: U.ViewsSet (TCOpSeq op) -> TcError' op -> TypeCheck op a
    onFailedViewsTypeCheck processedViews err = do
      verbose <- asks' tcVerbose
      throwError if verbose
        then TcIncompletelyTyped err (TCOpSeq . one <$> tcContract)
             { U.contractViews = processedViews
             }
        else err

    runningTotalMapM :: Monad m => (ViewsSetF b -> ViewName -> a -> m b) -> ViewsSetF a -> m (ViewsSetF b)
    runningTotalMapM f views = toPairs views & flip foldM def \acc (k, el) -> do
      newEl <- f acc k el
      pure $ unsafeInsert k newEl acc

typeCheckViews
  :: WellTyped st
  => U.Contract' (TypeCheckedOp U.ExpandedOp)
  -> Notes st
  -> U.ViewsSet U.ExpandedOp
  -> TypeCheck U.ExpandedOp (ViewsSet st)
typeCheckViews = coerce $ typeCheckViews' typeCheckExpandedOp

-- | 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 U.ExpandedOp (SomeTcInstr inp)
typeCheckList = throwingTcError ... typeCheckListNoExcept typeCheckExpandedOp

-- | 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, IsInstrOp op)
  => TcInstrBase op -> [op] -> HST inp -> TypeCheckNoExcept op (TypeCheckedSeq op inp)
typeCheckListNoExcept tcOp = usingReaderT def ... typeCheckImpl tcOp

-- | 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 U.ExpandedOp (Value t)
typeCheckValue value = do
  runTypeCheck (TypeCheckValue (value, demote @t) Nothing) $
    usingReaderT def $
      typeCheckValImpl Nothing typeCheckExpandedOp 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 U.ExpandedOp (Value t)
typeCheckValueRunCodeCompat bigMapFinder val =
  runTypeCheck (TypeCheckValue (val, demote @t) (Just bigMapFinder)) $
    usingReaderT def $
      typeCheckValImpl Nothing typeCheckExpandedOp val

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

typeVerifyStorage
  :: SingI t
  => U.Value -> TypeCheckResult U.ExpandedOp (Value t)
typeVerifyStorage = typeVerifyStorage' typeCheckExpandedOp

typeVerifyStorage'
  :: (SingI t, IsInstrOp op)
  => TcInstrBase op -> U.Value' [] op -> TypeCheckResult op (Value t)
typeVerifyStorage' tcOp = typeVerifyTopLevelType' tcOp Nothing

typeVerifyTopLevelType
  :: forall t. SingI t
  => Maybe TcOriginatedContracts -> U.Value -> TypeCheckResult U.ExpandedOp (Value t)
typeVerifyTopLevelType = typeVerifyTopLevelType' typeCheckExpandedOp

typeVerifyTopLevelType'
  :: forall t op. (SingI t, IsInstrOp op)
  => TcInstrBase op -> Maybe TcOriginatedContracts -> U.Value' [] op -> TypeCheckResult op (Value t)
typeVerifyTopLevelType' tcOp mOriginatedContracts valueU =
  runTypeCheck (TypeCheckValue (valueU, demote @t) Nothing) $ usingReaderT def $
    typeCheckValImpl mOriginatedContracts tcOp 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 U.ExpandedOp SomeValue
typeCheckParameter originatedContracts = typeCheckTopLevelType (Just originatedContracts)

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

typeCheckTopLevelType
  :: Maybe TcOriginatedContracts -> U.Ty -> U.Value -> TypeCheckResult U.ExpandedOp SomeValue
typeCheckTopLevelType = typeCheckTopLevelType' typeCheckExpandedOp

typeCheckTopLevelType'
  :: IsInstrOp op
  => TcInstrBase op -> Maybe TcOriginatedContracts -> U.Ty -> U.Value' [] op -> TypeCheckResult op SomeValue
typeCheckTopLevelType' tcOp mOriginatedContracts (AsUType (_ :: Notes t)) valueU =
  SomeValue <$> typeVerifyTopLevelType' @t tcOp 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
  :: IsInstrOp op
  => U.InstrAbstract [] op
  -> TypeCheckInstr op (SomeTcInstr s)
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op s)
workOnInstr instr = tcEither
  (\err -> pure $ IllTypedSeq err [NonTypedInstr $ liftInstr instr])
  (pure . WellTypedSeq)

-- | Alias for 'typeCheckImpl'.
tcList :: IsInstrOp op => TcInstrBase op -> TcInstr op [op]
tcList = typeCheckImpl

-- | 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 :: forall op. IsInstrOp op => TcInstrBase op -> TcInstr op (U.InstrAbstract [] op)
typeCheckInstr tcOp uInstr inp = case (uInstr, inp) of
  (U.EXT ext, si) ->
    typeCheckExt tcOp 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 op (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 op (TCDupNHelper inp)
      go = curry \case
        (_, SNil) -> notEnoughItemsOnStack'

        (0, _) ->
          typeCheckInstrErr' uInstr (SomeHST inp) Nothing (InvalidInstruction (void 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 @octez-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 op (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 op (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 tcOp 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 tcOp 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 op (TCPairNHelper inp)
      go n hst
        | n < 2 =
            typeCheckInstrErr' uInstr (SomeHST inp) Nothing
              (InvalidInstruction (void 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 op (TCUnpairNHelper (x : xs))
      go n hst
        | n < 2 =
            typeCheckInstrErr' uInstr (SomeHST inp) Nothing
              (InvalidInstruction (void 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 op 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 tcOp 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 tcOp 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 tcOp (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 tcOp (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 tcOp (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 tcOp s uInstr is inp

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

  (U.ITER is, (STMap (k :: SingT a) (v :: SingT b), _) ::& _) -> withSingI k $ withSingI v $ do
    withWTPInstr' @('TPair a b) $ iterImpl tcOp (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 op (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 op (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 tcOp 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 tcOp 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 tcOp 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 tcOp is (notesSing ins) (notesSing ons)
          (U.LAMBDA vn p1 p2) (Anns3'' vn ins ons) uInstr i

  (U.LAMBDA_REC 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 $
        lamRecImpl tcOp is (notesSing ins) (notesSing ons)
          (U.LAMBDA_REC vn p1 p2) (Anns3'' vn ins ons) uInstr 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' op) 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 tcOp 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 op (TCDipHelper op inp)
      go n curHST = case (n, curHST) of
        (0, _) -> typeCheckDipBody tcOp (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 $ liftInstr 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' op) 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 vn, (STBytes, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Lsl AnnLSL inp vn uInstr
  (U.LSL _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| [("bytes" :| ["nat"])]
  (U.LSL _, _) -> notEnoughItemsOnStack

  (U.LSR vn, (STNat, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Lsr AnnLSR inp vn uInstr
  (U.LSR vn, (STBytes, _) ::&
             (STNat, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Lsr AnnLSR inp vn uInstr
  (U.LSR _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("nat" :| ["nat"]) :| [("bytes" :| ["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 vn, (STBytes, _) ::&
            (STBytes, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Or AnnOR inp vn uInstr
  (U.OR _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("bool" :| ["bool"]) :|
      [ ("nat" :| ["nat"])
      , ("bytes" :| ["bytes"])
      ]
  (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 vn, (STBytes, _) ::&
             (STBytes, _) ::& _) -> workOnInstr uInstr $
    arithImpl @And AnnAND inp vn uInstr
  (U.AND _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("int" :| ["nat"]) :|
      [ ("nat" :| ["nat"])
      , ("bool" :| ["bool"])
      , ("bytes" :| ["bytes"])
      ]
  (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 vn, (STBytes, _) ::&
             (STBytes, _) ::& _) -> workOnInstr uInstr $
    arithImpl @Xor AnnXOR inp vn uInstr
  (U.XOR _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("bool" :| ["bool"]) :|
      [ ("nat" :| ["nat"])
      , ("bytes" :| ["bytes"])
      ]
  (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 vn, (STBytes, _) ::& _) -> workOnInstr uInstr $
    pure $ unaryArithImplAnnotated @Not (AnnNOT (Anns1 vn)) inp vn
  (U.NOT _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ ("nat" :| []) :|
      [ ("bool" :| [])
      , ("int" :| [])
      , ("bytes" :| [])
      ]
  (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, (STBytes{}, _) ::& 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 $ one "nat" :| [one "bytes", one "bls12_381_fr"]
  (U.INT _, SNil) -> notEnoughItemsOnStack

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

  (U.BYTES vn, (STInt{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnBYTES (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.BYTES vn, (STNat{}, _) ::& rs) -> workOnInstr uInstr $
    pure $ inp :/ AnnBYTES (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.BYTES _, _ ::& _) ->
    failWithErr $ UnexpectedType $ ("int" :| []) :| [ "nat" :| [] ]
  (U.BYTES _, 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 (void 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
      paramType <- liftEither $ first (TcContractError "illegal parameter declaration: " . Just ) $
        mkSomeParamType $ U.contractParameter contract
      SomeContract contr@(Contract _ _ (_ :: Notes st) _ _) <- lift $
          local (tcModeL .~ TypeCheckContract paramType) $
          doTypeCheckContract' tcOp 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.TICKET_DEPRECATED vn, (stVal :: Sing v, _) ::& (STNat{}, _) ::& rs) -> workOnInstr uInstr $
    withWTPInstr @v $
    withCompareableCheck stVal uInstr inp $
      inp :/ AnnTICKET_DEPRECATED (Anns1 vn) ::: ((sing, Dict) ::& rs)
  (U.TICKET_DEPRECATED _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType $ ("a'" :| ["nat"]) :| []
  (U.TICKET_DEPRECATED _, _) -> 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
        isStrict <- asks' tcStrict
        when isStrict $
          typeCheckInstrErr' uInstr (SomeHST inp) Nothing $
            InvalidInstruction (void uInstr) "OPEN_CHEST temporarily deprecated"
        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 (void 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' op) m) => Either TcTypeError a -> m a
        errM = onTypeCheckInstrErr uInstr (SomeHST inp) (Just EmitArgument)

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

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

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

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

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

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

    withNotInView :: U.InstrAbstract [] op -> (IsNotInView => TypeCheckInstr op r) -> TypeCheckInstr op r
    withNotInView instr act = asks' (tcMode @op) >>= \case
      -- we provide the not-in-view constraint in the isolated mode
      TypeCheckTest -> giveNotInView act
      _ -> view tcieNotInView >>= \case
        Just Dict -> act
        Nothing -> failWithErr' $
          InvalidInstruction (void 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 op .
    (SingI bti, SingI bfi, IsInstrOp op)
  => TcInstrBase op
  -> (forall s'.
        Instr bti s' ->
        Instr bfi s' ->
        Instr (cond ': rs) s'
     )
  -> (forall op1. [op1] -> [op1] -> U.InstrAbstract [] op1)
  -> [op]
  -> [op]
  -> HST bti
  -> HST bfi
  -> HST (cond ': rs)
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op (cond ': rs))
genericIf tcOp cons mCons mbt mbf bti bfi i@(_ ::& _) = do
  let cons1 opsT = mCons opsT (one $ IllTypedOp $ map NonTypedInstr mbf)
  preserving' (tcList tcOp mbt bti) cons1 $ \tInstr@(_ :/ pinstr) -> do
    let cons2 opsF = mCons [someInstrToOp tInstr] opsF
    preserving (tcList tcOp 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 op.
    ( MapOp c
    , WellTyped (MapOpInp c)
    , SingIOne (MapOpRes c)
    , IsInstrOp op
    )
  => TcInstrBase op
  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)
  -> SingT (MapOpInp c)
  -> VarAnn
  -> U.InstrAbstract [] op
  -> [op]
  -> HST (c ': rs)
  -> (forall v'. (SingI v') =>
        SingT v' -> HST rs -> TypeCheckInstr op (HST (MapOpRes c v' ': rs)))
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op (c ': rs))
mapImpl tcOp cons vn anns instr mp i@(_ ::& rs) mkRes = do
  preserving (tcList tcOp 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 op .
    ( IterOp c
    , WellTyped (IterOpEl c)
    , IsInstrOp op
    )
  => TcInstrBase op
  -> SingT (IterOpEl c)
  -> U.InstrAbstract [] op
  -> [op]
  -> HST (c ': rs)
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op (c ': rs))
iterImpl tcOp en instr mp i@((_, _) ::& rs) = do
  let tcAction = case mp of
        [] -> workOnInstr instr
          (typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode)
        _ -> typeCheckImpl tcOp 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

type LamTC it ot ts op
  =  [op]
  -> SingT it
  -> SingT ot
  ->  ([TypeCheckedOp op] -> TypeCheckedInstr op)
  -> Anns '[VarAnn, Notes it, Notes ot]
  -> U.InstrAbstract [] op
  -> HST ts
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op ts)

lamImpl
  :: forall it ot ts op .
    ( WellTyped it, WellTyped ot
    , SingI ts
    , IsInstrOp op
    )
  => TcInstrBase op
  -> LamTC it ot ts op
lamImpl tcOp is ins = lamCommon AnnLAMBDA
  (giveNotInView $ local (set tcieNotInView $ Just Dict) $ tcList tcOp is ((ins, Dict) ::& SNil))
  is ins

lamRecImpl
  :: forall it ot ts op .
    ( WellTyped it, WellTyped ot
    , SingI ts
    , IsInstrOp op
    )
  => TcInstrBase op
  -> LamTC it ot ts op
lamRecImpl tcOp is ins ons = lamCommon AnnLAMBDA_REC
  (giveNotInView $
      local (set tcieNotInView $ Just Dict) $
        tcList tcOp is ((ins, Dict) ::& (STLambda ins ons, Dict) ::& SNil))
  is ins ons

lamCommon
  :: forall it ot ts op inp .
    ( WellTyped it, WellTyped ot
    , SingI ts
    , IsInstrOp op
    )
  => (Anns '[VarAnn, Notes it, Notes ot] -> RemFail Instr inp '[ot] -> Instr ts ('TLambda it ot : ts))
  -> TypeCheckInstrNoExcept op (TypeCheckedSeq op inp)
  -> LamTC it ot ts op
lamCommon tyCon tcInstr is ins ons cons anns instr i =
  guarding_ instr
    (whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr -> do
      let err = InvalidInstruction (void selfInstr) "SELF instruction cannot be used in a LAMBDA"
      typeCheckInstrErr' instr (SomeHST i) (Just LambdaCodeCtx) 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 (tyCon anns (RfNormal lam) ::: lamSt ons)
            Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCodeCtx) m
        AnyOutInstr lam ->
          pure (tyCon anns (RfAlwaysFails lam) ::: lamSt ons)
  where
    hasSelf :: op -> First (U.InstrAbstract [] op)
    hasSelf = everything (<>)
      (mkQ (First Nothing)
       (\case
           selfInstr@(U.SELF{} :: U.InstrAbstract [] op) -> First $ Just selfInstr
           _ -> First Nothing
       )
      )

typeCheckExpandedOp :: TcInstrBase U.ExpandedOp
typeCheckExpandedOp = \case
  U.WithSrcEx _ op@U.WithSrcEx{} -> typeCheckExpandedOp op
  U.WithSrcEx loc (U.PrimEx op)  -> typeCheckPrimWithLoc loc op
  U.WithSrcEx loc (U.SeqEx sq)   -> typeCheckSeqWithLoc loc sq
  U.PrimEx op                    -> typeCheckPrim op
  U.SeqEx sq                     -> typeCheckSeq sq
  where
    -- If we know source location from the untyped instruction, keep it in the typed one.
    typeCheckPrimWithLoc :: ErrorSrcPos -> TcInstr U.ExpandedOp U.ExpandedInstr
    typeCheckPrimWithLoc loc op hst = local (set tcieErrorPos loc)
      (wrapWithLoc loc <$> typeCheckPrim op hst)

    typeCheckPrim :: TcInstr U.ExpandedOp U.ExpandedInstr
    typeCheckPrim = typeCheckInstr typeCheckExpandedOp

    typeCheckSeqWithLoc :: ErrorSrcPos -> TcInstr U.ExpandedOp [U.ExpandedOp]
    typeCheckSeqWithLoc loc op = fmap (wrapWithLoc loc) . local (set tcieErrorPos loc) . typeCheckSeq op

    typeCheckSeq :: TcInstr U.ExpandedOp [U.ExpandedOp]
    typeCheckSeq sq hst = typeCheckImpl typeCheckExpandedOp sq hst <&> \case
      WellTypedSeq instr -> WellTypedSeq $ mapSomeInstr Nested instr
      MixedSeq nest instr err rest -> MixedSeq (succ nest) instr err rest
      IllTypedSeq err op -> IllTypedSeq err [IllTypedNest op]

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

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

typeCheckDipBody
  :: (SingI inp, IsInstrOp op)
  => TcInstrBase op
  -> ([TypeCheckedOp op] -> TypeCheckedInstr op)
  -> U.InstrAbstract [] op
  -> [op]
  -> HST inp
  -> (TcError' op -> [IllTypedInstr op] -> r)
  -> (forall out. SingI out => Instr inp out -> HST out -> r)
  -> TypeCheckInstrNoExcept op r
typeCheckDipBody tcOp cons mainInstr instructions inputHST onErr onOk = do
  listRes <- tcList tcOp 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)