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

-- | Module, providing functions for conversion from
-- instruction and value representation from @Michelson.Type@ module
-- to strictly-typed GADT-based representation from @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 satsify 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 Michelson.TypeCheck.Instr
    ( typeCheckContract
    , typeCheckContractAndStorage
    , typeCheckInstr
    , typeCheckList
    , typeCheckListNoExcept
    , typeCheckParameter
    , typeCheckStorage
    , typeCheckValue
    , typeVerifyParameter
    , typeVerifyStorage
    ) where

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, liftEither, throwError, catchError)
import Data.Default (def)
import Data.Generics (everything, mkQ)
import Data.Singletons (Sing, demote)
import Data.Typeable ((:~:)(..))

import Michelson.ErrorPos
import Michelson.TypeCheck.Error
import Michelson.TypeCheck.Ext
import Michelson.TypeCheck.Helpers
import Michelson.TypeCheck.TypeCheck
import Michelson.TypeCheck.TypeCheckedSeq
  (IllTypedInstr(..), TypeCheckedInstr, TypeCheckedOp(..), TypeCheckedSeq(..), tcsEither, someInstrToOp)
import Michelson.TypeCheck.Types
import Michelson.TypeCheck.Value
import Michelson.Typed.Value

import Michelson.Typed
import Util.Peano

import qualified Michelson.Untyped as U
import Michelson.Untyped.Annotation (VarAnn)

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

typeCheckContract
  :: U.Contract
  -> TypeCheckOptions
  -> Either TCError SomeContract
typeCheckContract c options = do
  paramType <- mkSomeParamType (U.contractParameter c)
  runTypeCheck (TypeCheckContract paramType) options $ typeCheckContractImpl c

withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a
withWTP fn = case getWTP @t of
  Right Dict -> fn
  Left (NotWellTyped t) -> throwError $ TCContractError ("Not a well typed value: " <> show t) 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) -> do
    loc <- ask
    throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope badType BtNotComparable)

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) -> do
    loc <- ask
    let err = TCFailedOnInstr v t loc Nothing
              (Just $ UnsupportedTypeForScope badType BtNotComparable)
    pure $ IllTypedSeq err [NonTypedInstr $ U.PrimEx v]

typeCheckContractImpl
  :: U.Contract
  -> TypeCheck SomeContract
typeCheckContractImpl (U.Contract wholeParam@(U.ParameterType mParam rootAnn) mStorage pCode entriesOrder) = 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 inpNote = NTPair def def def paramNote storageNote
          let inp = (inpNote, Dict, def) ::& SNil

          codeRes <- usingReaderT def $
                     liftNoExcept $
                     typeCheckImpl typeCheckInstr pCode inp
          codeRes & tcsEither
            (onFailedTypeCheck)
            (onSuccessfulTypeCheck (NTPair def def def starNotes storageNote))
  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

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

    onSuccessfulTypeCheck
      :: forall st param
      . (ParameterScope param, StorageScope st, WellTyped st)
      => Notes (ContractOut1 st)
      -> SomeInstr (ContractInp param st)
      -> TypeCheck SomeContract
    onSuccessfulTypeCheck outNote i@(inp' :/ instrOut) = wrapErrorsIfVerbose i $ do
      let (paramNotesRaw, cStoreNotes) = case inp' of
            (NTPair _ _ _ cpNotes stNotes, _, _) ::& SNil -> (cpNotes, stNotes)
      cParamNotes <-
        liftEither $
        mkParamNotes paramNotesRaw rootAnn `onLeft`
            (TCContractError "invalid parameter declaration: " . Just . IllegalParamDecl)
      case instrOut of
        instr ::: out -> liftEither $ do
          case eqHST1 @(ContractOut1 st) out of
            Right Refl -> do
              let (outN, _, _) ::& SNil = out
              _ <- converge outN outNote
                      `onLeft`
                  ((TCContractError "contract output type violates convention:") . Just . AnnError)
              pure $ SomeContract Contract
                { cCode = instr
                , cParamNotes
                , cStoreNotes
                , cEntriesOrder = entriesOrder
                }
            Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err
        AnyOutInstr instr ->
          pure $ SomeContract Contract
            { cCode = instr
            , cParamNotes
            , cStoreNotes
            , cEntriesOrder = entriesOrder
            }

    wrapErrorsIfVerbose :: SomeInstr inp -> TypeCheck SomeContract -> TypeCheck SomeContract
    wrapErrorsIfVerbose instr action =
      action `catchError` (onFailedTypeCheck [someInstrToOp instr])

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

-- | Function @typeCheckListNoExcept@ converts list of Michelson instructions
-- given in representation from @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
  :: (Typeable inp)
  => [U.ExpandedOp] -> HST inp -> TypeCheckNoExcept (TypeCheckedSeq inp)
typeCheckListNoExcept = usingReaderT def ... typeCheckImpl typeCheckInstr

-- | Function @typeCheckValue@ converts a single Michelson value
-- given in representation from @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
  -> TypeCheckInstr (Value t)
typeCheckValue = typeCheckValImpl @t Nothing typeCheckInstr

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

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

typeVerifyTopLevelType
  :: forall t. SingI t
  => Maybe TcOriginatedContracts -> U.Value -> Either TCError (Value t)
typeVerifyTopLevelType mOriginatedContracts valueU =
  runTypeCheck (TypeCheckValue (valueU, demote @t)) def $ 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.Type -> U.Value -> Either TCError SomeValue
typeCheckParameter originatedContracts = typeCheckTopLevelType (Just originatedContracts)

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

typeCheckTopLevelType
  :: Maybe TcOriginatedContracts -> U.Type -> U.Value -> Either TCError SomeValue
typeCheckTopLevelType mOriginatedContracts typeU valueU =
  withSomeSingT (fromUType typeU) $ \(_ :: Sing t) ->
    SomeValue <$> typeVerifyTopLevelType @t mOriginatedContracts valueU

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

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

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

-- 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 `lift ... typeCheckListNoExcept`.
tcList
  :: (Typeable inp)
  => [U.ExpandedOp] -> HST inp -> TypeCheckInstrNoExcept (TypeCheckedSeq inp)
tcList ops stack = lift $ typeCheckListNoExcept ops stack

-- | Function @typeCheckInstr@ converts a single Michelson instruction
-- given in representation from @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 neccessary.
--
-- 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. Typeable inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDropHelper inp)
      go n i = case (n, i) of
        (0, _) -> pure (TCDropHelper SZ i)

        (_, SNil) -> notEnoughItemsOnStack'

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

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

  (U.DUP _vn, SNil) -> notEnoughItemsOnStack

  (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 <&> \case
      TCDigHelper s out -> inputHST :/ DIG s ::: out
    where
      go :: forall inp. Typeable inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDigHelper inp)
      go n i = case (n, i) of
        -- Even 'DIG 0' is invalid on empty stack (so it is not strictly `Nop`).
        (_, SNil) -> notEnoughItemsOnStack'

        (0, (_ ::& _)) -> pure (TCDigHelper SZ i)

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

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

        (_, (a ::& b ::& iTail)) ->
          go (n - 1) (a ::& iTail) <&> \case
          TCDugHelper s resTail -> TCDugHelper (SS 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
      val <- typeCheckValue @t mval
      proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST i) Nothing
        $ checkScope @(ConstantScope t)
      case proofScope of
        Dict -> withWTPInstr @t $ pure $ i :/ PUSH val ::: ((nt, Dict, vn) ::& i)

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

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

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

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

  (U.IF_NONE mp mq, (STOption{}, (ons :: Notes ('TOption a)), Dict, ovn) ::&+ rs) -> do
    let (an, avn) = deriveNsOption ons ovn
    withWTPInstr' @a $
      genericIf IF_NONE U.IF_NONE mp mq rs ((an, Dict, avn) ::& rs) inp

  (U.IF_NONE _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ (ExpectOption Nothing :| []) :| []

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

  (U.PAIR tn vn pfn qfn, (an, _, avn) ::& (bn, _, bvn) ::& rs) -> workOnInstr uInstr $ do
    let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn
    case NTPair tn pfn' qfn' an bn of
      (ns :: Notes ('TPair a b)) -> withWTPInstr @('TPair a b) $
        pure (inp :/ AnnPAIR tn pfn qfn ::: ((ns, Dict, vn `orAnn` vn') ::& rs))

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

  (U.CAR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> workOnInstr uInstr $ do
    pfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CarArgument) (convergeAnns fn pfn)
    withWTPInstr @p $
      withWTPInstr @('TPair p q) $ do
        let vn' = deriveSpecialVN vn pfn' pairVN
            i' = (NTPair pairTN pfn' qfn pns qns, Dict, pairVN) ::& rs
        pure $ i' :/ AnnCAR fn ::: ((pns, Dict, vn') ::& rs)

  (U.CAR _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ (ExpectPair Nothing Nothing :| []) :| []

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

  (U.CDR vn fn, (STPair{}, NTPair pairTN pfn qfn (pns :: Notes p) (qns :: Notes q), _, pairVN) ::&+ rs) -> workOnInstr uInstr $ do
    qfn' <- onTypeCheckInstrAnnErr uInstr inp (Just CdrArgument) (convergeAnns fn qfn)

    withWTPInstr @q $
      withWTPInstr @('TPair p q) $ do
        let vn' = deriveSpecialVN vn qfn' pairVN
            i' = (NTPair pairTN pfn qfn' pns qns, Dict, pairVN) ::& rs
        pure $ i' :/ AnnCDR fn ::: ((qns, Dict, vn') ::& rs)

  (U.CDR _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ (ExpectPair Nothing Nothing :| []) :| []

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

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

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

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

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

  (U.IF_LEFT mp mq, (STOr{}, ons, _, ovn) ::&+ rs) -> do
    case deriveNsOr ons ovn of
      (an :: Notes a, bn :: Notes b, avn, bvn) ->
        withWTPInstr' @a $
          withWTPInstr' @b $ do
            let
              ait = (an, Dict, avn) ::& rs
              bit = (bn, Dict, bvn) ::& rs
            genericIf IF_LEFT U.IF_LEFT mp mq ait bit inp

  (U.IF_LEFT _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ (ExpectOr Nothing Nothing :| []) :| []

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

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

  (U.CONS vn, ((an :: Notes a), _, _)
                ::& ((ln :: Notes l), _, _) ::& rs) -> workOnInstr uInstr
    case eqType @('TList a) @l of
      Right Refl -> do
        (n :: Notes t) <- onTypeCheckInstrAnnErr uInstr inp (Just ConsArgument) (converge ln (NTList def an))
        withWTPInstr @t $
          pure $ inp :/ CONS ::: ((n, Dict, vn) ::& rs)
      Left m -> typeCheckInstrErr' uInstr (SomeHST inp) (Just ConsArgument) m

  (U.CONS _, _) -> notEnoughItemsOnStack

  (U.IF_CONS mp mq, (STList{}, ns, Dict, vn) ::&+ rs) -> do
    case ns of
      NTList _ (an :: Notes t1) -> withWTPInstr' @t1 $ do
        let ait = (an, Dict, vn <> "hd") ::& (ns, Dict, vn <> "tl") ::& rs
        genericIf IF_CONS U.IF_CONS mp mq ait rs inp

  (U.IF_CONS _ _, _ ::& _) ->
    failWithErr $ UnexpectedType $ (ExpectList Nothing :| []) :| []

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

  (U.SIZE vn, (NTList{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (NTSet{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (NTMap{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (NTString{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE vn, (NTBytes{}, _, _) ::& _) -> workOnInstr uInstr $ sizeImpl inp vn
  (U.SIZE _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectList Nothing :| []) :|
      [ (ExpectSet Nothing :| [])
      , (ExpectMap :| [])
      , (ExpectString :| [])
      , (ExpectByte :| [])
      ]

  (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 :/ EMPTY_SET ::: ((STSet sing, NTSet tn vns, Dict, vn) ::&+ 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 :/ EMPTY_MAP ::: ((STMap sing sing, NTMap tn ktn vns, Dict, vn) ::&+ 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 :/ EMPTY_BIG_MAP ::: ((STBigMap sing sing, NTBigMap tn ktn vns, Dict, vn) ::&+ i)

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

  (U.MAP vn mp, (STMap{}, NTMap _ kns vns, Dict, _vn) ::&+ _) -> do
    case NTPair def def def kns vns of
      (pns :: Notes ('TPair k v1)) ->
        withWTPInstr' @('TPair k v1) $
          mapImpl (U.MAP vn) pns uInstr mp inp
             (\(rn :: Notes v) hst -> withWTPInstr @('TMap k v) $ pure $ (NTMap def kns rn, Dict, vn) ::& hst)

  (U.MAP _ _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectList Nothing :| []) :|
      [ (ExpectMap :| [])
      ]

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

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

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

  (U.ITER is, (STMap _ _, NTMap _ kns vns, _, _) ::&+ _) -> do
    case NTPair def def def kns vns of
      (en :: Notes ('TPair a b)) ->
        withWTPInstr' @('TPair a b) $ iterImpl en uInstr is inp

  (U.ITER _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectSet Nothing :| []) :|
      [ (ExpectList Nothing :| [])
      , (ExpectMap :| [])
      ]

  (U.ITER _, SNil) -> notEnoughItemsOnStack

  (U.MEM varNotes,
   _ ::& (STSet{}, NTSet _ notesK, _, _) ::&+ _) -> workOnInstr uInstr $
    memImpl notesK inp varNotes
  (U.MEM varNotes,
   _ ::& (STMap{}, NTMap _ notesK _, _, _) ::&+ _) -> workOnInstr uInstr $
    memImpl notesK inp varNotes
  (U.MEM varNotes,
   _ ::& (STBigMap{}, NTBigMap _ notesK _, _, _) ::&+ _) -> workOnInstr uInstr $
    memImpl notesK inp varNotes
  (U.MEM _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectTypeVar :| [ExpectSet Nothing]) :|
      [ (ExpectTypeVar :| [ExpectMap])
      , (ExpectTypeVar :| [ExpectBigMap])
      ]

  (U.MEM _, _) -> notEnoughItemsOnStack


  (U.GET varNotes,
   _ ::& (STMap{}, NTMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
    workOnInstr uInstr $ withWTPInstr @v $
      getImpl notesK inp notesV varNotes
  (U.GET varNotes,
   _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
    workOnInstr uInstr $ withWTPInstr @v $
      getImpl notesK inp notesV varNotes

  (U.GET _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectTypeVar :| [ExpectMap]) :|
      [ (ExpectTypeVar :| [ExpectBigMap])
      ]

  (U.GET _, _) -> notEnoughItemsOnStack

  (U.UPDATE varNotes,
   _ ::& _ ::& (STMap{}, (NTMap _ notesK (notesV :: Notes v)), _, _) ::&+ _) ->
    workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varNotes
  (U.UPDATE varNotes,
   _ ::& _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
    workOnInstr uInstr $ updImpl notesK inp (NTOption U.noAnn notesV) varNotes
  (U.UPDATE varNotes,
   _ ::& _ ::& (STSet{}, NTSet _ (notesK :: Notes k), _, _) ::&+ _) ->
    workOnInstr uInstr $ updImpl notesK inp (NTBool U.noAnn) varNotes

  (U.UPDATE _, _ ::& _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectTypeVar :| [ExpectTypeVar, ExpectMap]) :|
      [ (ExpectTypeVar :| [ExpectTypeVar, ExpectBigMap])
      , (ExpectTypeVar :| [ExpectTypeVar, ExpectSet Nothing])
      ]

  (U.UPDATE _, _) -> notEnoughItemsOnStack

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

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

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

  (U.LOOP is, (NTBool{}, _, _) ::& (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 -> do
              let _ ::& rs' = o
              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
      $ (ExpectBool :| [ExpectStackVar]) :| []

  (U.LOOP _, _) -> notEnoughItemsOnStack

  (U.LOOP_LEFT is, (os@STOr{}, ons, Dict, ovn) ::&+ rs) -> do
    case deriveNsOr ons ovn of
      (an :: Notes t, bn :: Notes b, avn, bvn) -> do
        withWTPInstr' @t $ withWTPInstr' @b $ do
          let ait = (an, Dict, avn) ::& rs
          preserving (tcList is ait) U.LOOP_LEFT $ \(_ :/ tp) ->
            case tp of
              subI ::: o -> do
                case (eqHST o (os -:& rs), o) of
                  (Right Refl, ((ons', Dict, ovn') ::& rs')) -> do
                      let (_, bn', _, bvn') = deriveNsOr ons' ovn'
                      br <- onTypeCheckInstrAnnErr uInstr inp
                              (Just Iteration)
                              (convergeHSTEl (bn, Dict, bvn) (bn', Dict, bvn'))
                      pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs')
                  (Left m, _) -> typeCheckInstrErr' uInstr (SomeHST inp) (Just Iteration) m
              AnyOutInstr subI -> do
                let br = (bn, Dict, bvn)
                pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs)

  (U.LOOP_LEFT _, _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectOr Nothing Nothing :| [ExpectStackVar]) :| []

  (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) uInstr is vn ins ons i

  (U.EXEC vn, ((_ :: Notes t1), _, _)
                              ::& ( STLambda _ _
                                  , NTLambda _ (_ :: Notes t1') (t2n :: Notes t2')
                                  , _
                                  , _
                                  )
                              ::&+ rs) -> workOnInstr uInstr $ do
    Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just LambdaArgument)
                  (eqType @t1 @t1')
    withWTPInstr @t2' $ pure $ inp :/ EXEC ::: ((t2n, Dict, vn) ::& rs)

  (U.EXEC _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectTypeVar :| [ExpectLambda Nothing Nothing]) :| []

  (U.EXEC _, _) -> notEnoughItemsOnStack

  (U.APPLY vn, ((_ :: Notes a'), _, _)
                  ::& ( STLambda (STPair _ _) _
                      , NTLambda vann (NTPair _ _ _ (_ :: Notes a) (nb :: Notes b)) sc
                      , _
                      , _)
                  ::&+ rs) -> workOnInstr uInstr $ do
    case NTLambda vann nb sc of
      (l2n :: Notes ('TLambda t1 t2)) -> 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 :/ (APPLY @a) ::: ((l2n, Dict, vn) ::& rs)

  (U.APPLY _, _ ::& _ ::& _) ->
    failWithErr $ UnexpectedType
      $ (ExpectTypeVar :| [ExpectLambda (Just $ ExpectPair Nothing Nothing) Nothing]) :| []

  (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. Typeable inp
        => Word
        -> HST inp
        -> TypeCheckInstrNoExcept (TCDipHelper inp)
      go n curHST = case (n, curHST) of
        (0, _) -> typeCheckDipBody (U.DIPN nTotal) uInstr instructions curHST
          (TCDipHelperErr)
          (TCDipHelperOk SZ)
        (_, SNil) -> do
          pos <- ask
          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 (SS s) subI (hstHead ::& out)
          TCDipHelperErr err rest -> TCDipHelperErr err rest

  (u, v) -> case (u, v) of -- Workaround for not exceeding -fmax-pmcheck-iterations limit
    (U.FAILWITH, (_ ::& _)) -> workOnInstr uInstr $
      pure $ inp :/ AnyOutInstr FAILWITH

    (U.FAILWITH, _) -> notEnoughItemsOnStack

    (U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) ->
      workOnInstr uInstr $ do
        (Refl, _) <- errM $ matchTypes en castToNotes
        withWTPInstr @t $
          pure $ inp :/ CAST ::: ((castToNotes, Dict, vn `orAnn` evn) ::& rs)
      where
        errM :: (MonadReader InstrCallStack 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 :/ RENAME ::: ((an, Dict, vn) ::& rs)

    (U.RENAME _, SNil) -> notEnoughItemsOnStack

    (U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& 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 :/ UNPACK ::: ((ns, Dict, vn) ::& rs)

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

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

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

    (U.PACK _, SNil) -> notEnoughItemsOnStack

    (U.CONCAT vn, (NTBytes{}, _, _) ::& (NTBytes{}, _, _) ::& _) ->
      workOnInstr uInstr $ concatImpl inp vn
    (U.CONCAT vn, (NTString{}, _, _) ::& (NTString{}, _, _) ::& _) ->
      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
        $ (ExpectByte :| [ExpectByte]) :|
        [ (ExpectString :| [ExpectString])
        ]
    (U.CONCAT _, _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectList (Just ExpectByte) :| [ExpectList (Just ExpectByte)]) :|
        [ (ExpectList (Just ExpectString) :| [ExpectList (Just ExpectString)])
        ]
    (U.CONCAT _, SNil) -> notEnoughItemsOnStack

    (U.SLICE vn, (NTNat{}, _, _) ::&
                 (NTNat{}, _, _) ::&
                 (NTString{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn
    (U.SLICE vn, (NTNat{}, _, _) ::&
                 (NTNat{}, _, _) ::&
                 (NTBytes{}, _, _) ::& _) -> workOnInstr uInstr $ sliceImpl inp vn

    (U.SLICE _, _ ::& _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectNat :| [ExpectNat, ExpectString]) :|
        [ (ExpectNat :| [ExpectNat, ExpectByte])
        ]
    (U.SLICE _, _) -> notEnoughItemsOnStack

    (U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> workOnInstr uInstr $ do
      let vn = vn' `orAnn` oldVn
      pure $ inp :/ ISNAT ::: ((starNotes, Dict, vn) ::& rs)

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

    (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.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 $
      unaryArithImpl @Abs ABS inp vn
    (U.ABS _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []

    (U.ABS _, SNil) -> notEnoughItemsOnStack

    (U.NEG vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $
      unaryArithImpl @Neg NEG inp vn
    (U.NEG vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $
      unaryArithImpl @Neg NEG inp vn
    (U.NEG _, _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectInt :| []) :|
        [ (ExpectNat :| [])
        ]
    (U.NEG _, SNil) -> notEnoughItemsOnStack

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

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

    (U.OR vn, (STBool, _, _, _) ::&+
              (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @Or OR inp vn uInstr
    (U.OR vn, (STNat, _, _, _) ::&+
              (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @Or OR inp vn uInstr
    (U.OR _, _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectBool :| [ExpectBool]) :|
        [ (ExpectNat :| [ExpectNat])
        ]
    (U.OR _, _) -> notEnoughItemsOnStack

    (U.AND vn, (STInt, _, _, _) ::&+
               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @And AND inp vn uInstr
    (U.AND vn, (STNat, _, _, _) ::&+
               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @And AND inp vn uInstr
    (U.AND vn, (STBool, _, _, _) ::&+
               (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @And AND inp vn uInstr
    (U.AND _, _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectInt :| [ExpectNat]) :|
        [ (ExpectNat :| [ExpectNat])
        , (ExpectBool :| [ExpectBool])
        ]
    (U.AND _, _) -> notEnoughItemsOnStack

    (U.XOR vn, (STBool, _, _, _) ::&+
               (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @Xor XOR inp vn uInstr
    (U.XOR vn, (STNat, _, _, _) ::&+
               (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $
      arithImpl @Xor XOR inp vn uInstr
    (U.XOR _, _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectBool :| [ExpectBool]) :|
        [ (ExpectNat :| [ExpectNat])
        ]
    (U.XOR _, _) -> notEnoughItemsOnStack

    (U.NOT vn, (STNat, _, _, _) ::&+ _) -> workOnInstr uInstr $
      unaryArithImpl @Not NOT inp vn
    (U.NOT vn, (STBool, _, _, _) ::&+ _) -> workOnInstr uInstr $
      unaryArithImpl @Not NOT inp vn
    (U.NOT vn, (STInt, _, _, _) ::&+ _) -> workOnInstr uInstr $
      unaryArithImpl @Not NOT inp vn
    (U.NOT _, _ ::& _) ->
      failWithErr $ UnexpectedType
        $ (ExpectNat :| []) :|
        [ (ExpectBool :| [])
        , (ExpectInt :| [])
        ]
    (U.NOT _, SNil) -> notEnoughItemsOnStack

    (U.COMPARE vn,
          (an :: Notes aT, _, _)
      ::& (bn :: Notes bT, _, _)
      ::& rs
      )
      -> workOnInstr uInstr $ do
      case eqType @aT @bT of
        Right Refl -> do
          void . errConv $ converge an bn
          proofScope <- onScopeCheckInstrErr @aT (U.COMPARE vn) (SomeHST inp) (Just ComparisonArguments)
            $ checkScope @(ComparabilityScope aT)
          case proofScope of
            Dict ->
              pure $ inp :/ COMPARE ::: ((starNotes, Dict, vn) ::& rs)

        Left err -> do
          typeCheckInstrErr' uInstr (SomeHST inp) (Just ComparisonArguments) err
      where
        errConv :: (MonadReader InstrCallStack m, MonadError TCError m) => Either AnnConvergeError a -> m a
        errConv = onTypeCheckInstrAnnErr uInstr inp (Just ComparisonArguments)

    (U.COMPARE _, _) -> notEnoughItemsOnStack

    (U.EQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $
      unaryArithImpl @Eq' EQ inp vn
    (U.EQ _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.EQ _, SNil) -> notEnoughItemsOnStack

    (U.NEQ vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $
      unaryArithImpl @Neq NEQ inp vn
    (U.NEQ _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.NEQ _, SNil) -> notEnoughItemsOnStack

    (U.LT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $
      unaryArithImpl @Lt LT inp vn
    (U.LT _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.LT _, SNil) -> notEnoughItemsOnStack

    (U.GT vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $
      unaryArithImpl @Gt GT inp vn
    (U.GT _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.GT _, SNil) -> notEnoughItemsOnStack

    (U.LE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $
      unaryArithImpl @Le LE inp vn
    (U.LE _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.LE _, SNil) -> notEnoughItemsOnStack

    (U.GE vn, (NTInt{}, _, _) ::& _) -> workOnInstr uInstr $
      unaryArithImpl @Ge GE inp vn
    (U.GE _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.GE _, SNil) -> notEnoughItemsOnStack

    (U.INT vn, (NTNat{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ INT ::: ((starNotes, Dict, vn) ::& rs)
    (U.INT _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectNat :| []) :| []
    (U.INT _, SNil) -> notEnoughItemsOnStack

    (U.SELF vn fn, _) -> workOnInstr uInstr $ do
      mode <- gets 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 :/ SELF @arg (SomeEpc epc) ::: ((ntRes, Dict, vn) ::& inp)
        TypeCheckTest ->
          error "'SELF' appears in test typechecking."
        TypeCheckPack ->
          error "'SELF' appears in packed data."
    (U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& 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 `onLeft` IllegalEntrypoint
        case proofScope of
          Dict ->
            withWTPInstr @t $ pure $ inp :/ CONTRACT tns epName ::: ((ns, Dict, vn) ::& rs)

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

    (U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _, _)
      ::& (NTMutez{}, _, _)
      ::& (STContract (_ :: Sing p), _, _, _) ::&+ rs) -> workOnInstr uInstr $ do
      proofScope <- onScopeCheckInstrErr @p uInstr (SomeHST inp) (Just ContractParameter)
        $ checkScope @(ParameterScope p)
      case (eqType @p @p', proofScope) of
        (Right Refl, Dict) ->
          pure $ inp :/ TRANSFER_TOKENS ::: ((starNotes, Dict, vn) ::& rs)
        (Left m, _) ->
          typeCheckInstrErr' uInstr (SomeHST inp) (Just ContractParameter) m

    (U.TRANSFER_TOKENS _, _ ::& _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectTypeVar :| [ExpectMutez, ExpectContract]) :| []

    (U.TRANSFER_TOKENS _, _) -> notEnoughItemsOnStack

    (U.SET_DELEGATE vn,
      (STOption STKeyHash, NTOption _ NTKeyHash{}, _, _)
      ::&+ rs) -> workOnInstr uInstr $ do
        pure $ inp :/ SET_DELEGATE ::: ((starNotes, Dict, vn) ::& rs)

    (U.SET_DELEGATE _,  _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectOption (Just ExpectKeyHash) :| []) :| []

    (U.SET_DELEGATE _, _) -> notEnoughItemsOnStack

    (U.CREATE_CONTRACT ovn avn contract,
      (STOption STKeyHash, NTOption _ (_ :: Notes ('TKeyHash)), _, _)
      ::&+ (NTMutez{}, _, _)
      ::& (gn :: Notes g, Dict, _) ::& rs) -> workOnInstr uInstr $ do
        (SomeContract
          (Contract
            (contr :: ContractCode p' g')
            paramNotes
            storeNotes
            entriesOrder))
          <- lift $ typeCheckContractImpl contract
        Refl <- onTypeCheckInstrErr uInstr (SomeHST inp) (Just ContractStorage)
          $ eqType @g @g'
        void $ onTypeCheckInstrAnnErr uInstr inp (Just ContractStorage) (converge gn storeNotes)
        pure
          $ inp :/ CREATE_CONTRACT (Contract contr paramNotes storeNotes entriesOrder)
          ::: ((starNotes, Dict, ovn) ::& (starNotes, Dict, avn) ::& rs)

    (U.CREATE_CONTRACT {}, _ ::& _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectOption Nothing :| [ExpectMutez, ExpectTypeVar]) :| []

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

    (U.IMPLICIT_ACCOUNT vn, (NTKeyHash{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, Dict, vn) ::& rs)

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

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

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

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

    (U.CHECK_SIGNATURE vn,
               (NTKey _, _, _)
               ::& (NTSignature _, _, _) ::& (NTBytes{}, _, _) ::& rs) ->
      workOnInstr uInstr $
        pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, Dict, vn) ::& rs)

    (U.CHECK_SIGNATURE _, _ ::& _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectKey :| [ExpectSignature]) :| []
    (U.CHECK_SIGNATURE _, _) -> notEnoughItemsOnStack

    (U.SHA256 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ SHA256 ::: ((starNotes, Dict, vn) ::& rs)
    (U.SHA256 _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
    (U.SHA256 _, SNil) -> notEnoughItemsOnStack

    (U.SHA512 vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ SHA512 ::: ((starNotes, Dict, vn) ::& rs)
    (U.SHA512 _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
    (U.SHA512 _, SNil) -> notEnoughItemsOnStack

    (U.BLAKE2B vn, (NTBytes{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ BLAKE2B ::: ((starNotes, Dict, vn) ::& rs)
    (U.BLAKE2B _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectByte :| []) :| []
    (U.BLAKE2B _, SNil) -> notEnoughItemsOnStack

    (U.HASH_KEY vn, (NTKey{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ HASH_KEY ::: ((starNotes, Dict, vn) ::& rs)
    (U.HASH_KEY _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectKey :| []) :| []
    (U.HASH_KEY _, SNil) -> notEnoughItemsOnStack

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

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

    (U.ADDRESS vn, (NTContract{}, _, _) ::& rs) -> workOnInstr uInstr $
      pure $ inp :/ ADDRESS ::: ((starNotes, Dict, vn) ::& rs)

    (U.ADDRESS _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectContract :| []) :| []
    (U.ADDRESS _, SNil) -> notEnoughItemsOnStack

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

    -- Could not get rid of the catch all clause due to this warning:
    -- @
    -- Pattern match checker exceeded (2000000) iterations in
    -- a case alternative. (Use -fmax-pmcheck-iterations=n
    -- to set the maximum number of iterations to n)
    -- @
    i ->
      error $ "Pattern matches should be exhuastive, but instead got: " <> show i
  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 . typeCheckInstrErr' uInstr (SomeHST inp) Nothing

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

    notEnoughItemsOnStack' :: TypeCheckInstr a
    notEnoughItemsOnStack' = typeCheckInstrErr' uInstr (SomeHST inp) Nothing NotEnoughItemsOnStack

-- | Helper function for two-branch if where each branch is given a single
-- value.
genericIf
  :: forall bti bfi cond rs .
    (Typeable bti, Typeable 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
          o <- onTypeCheckInstrAnnErr instr i (Just If) (convergeHST po qo)
          pure $ cons p q ::: o
        (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)
    , Typeable (MapOpRes c)
    )
  => ([TypeCheckedOp] -> TypeCheckedInstr)
  -> Notes (MapOpInp c)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST (c ': rs)
  -> (forall v' . (KnownT v') =>
        Notes v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs)))
  -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs))
mapImpl cons vn instr mp i@(_ ::& rs) mkRes = do
  preserving (tcList mp ((vn, Dict, def) ::& rs)) cons $ \(_ :/ subp) ->
    case subp of
      sub ::: subo ->
        case subo of
          (bn, _, _bvn) ::& rs' -> do
            Refl <- onTypeCheckInstrErr instr (SomeHST i) (Just Iteration)
              $ eqHST rs rs'
            x <- mkRes bn rs'
            pure $ i :/ MAP 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)
    )
  => Notes (IterOpEl c)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST (c ': rs)
  -> TypeCheckInstrNoExcept (TypeCheckedSeq (c ': rs))
iterImpl en instr mp i@((_, _, lvn) ::& rs) = do
  let evn = deriveVN "elt" lvn
  let tcAction = case mp of
        [] -> workOnInstr instr
          (typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode)
        _ -> typeCheckImpl typeCheckInstr mp ((en, Dict, evn) ::& 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 _ ->
      typeCheckInstrErr' instr (SomeHST i) (Just Iteration) CodeAlwaysFails

lamImpl
  :: forall it ot ts .
    ( WellTyped it, WellTyped ot
    , Typeable ts
    )
  => ([TypeCheckedOp] -> TypeCheckedInstr)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> VarAnn
  -> Notes it
  -> Notes ot
  -> HST ts
  -> TypeCheckInstrNoExcept (TypeCheckedSeq ts)
lamImpl cons instr is vn ins ons i =
  guarding_ instr
    (whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr ->
      typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) $ InvalidInstruction selfInstr) $
    preserving (tcList is ((ins, Dict, def) ::& SNil)) cons $ \(_ :/ lamI) -> do
      let lamNotes onsr = NTLambda def ins onsr
      let lamSt onsr = (lamNotes onsr, Dict, vn) ::& i
      fmap (i :/) $ case lamI of
        lam ::: lo -> do
          case eqHST1 @ot lo of
            Right Refl -> do
                let (ons', _, _) ::& SNil = lo
                onsr <- onTypeCheckInstrAnnErr instr i (Just LambdaCode) (converge ons ons')
                pure (LAMBDA (VLam $ RfNormal lam) ::: lamSt onsr)
            Left m -> typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) m
        AnyOutInstr lam ->
          pure (LAMBDA (VLam $ RfAlwaysFails lam) ::: lamSt ons)
  where
    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'.
    (Typeable out, ConstraintDIPN n inp out s s') =>
    Sing n -> Instr s s' -> HST out -> TCDipHelper inp
  TCDipHelperErr :: TCError -> [IllTypedInstr] -> TCDipHelper inp

typeCheckDipBody
  :: Typeable inp
  => ([TypeCheckedOp] -> TypeCheckedInstr)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST inp
  -> (TCError -> [IllTypedInstr] -> r)
  -> (forall out. Typeable out => Instr inp out -> HST out -> r)
  -> TypeCheckInstrNoExcept r
typeCheckDipBody cons mainInstr instructions inputHST onErr onOk = do
  listRes <- lift $ typeCheckListNoExcept instructions inputHST
  pos <- ask
  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)