-- 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
    , typeCheckValue
    , typeCheckList
    , typeVerifyTopLevelType
    , typeCheckTopLevelType
    ) where

import Prelude hiding (EQ, GT, LT)

import Control.Monad.Except (MonadError, liftEither, throwError)
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.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)

typeCheckContract
  :: TcOriginatedContracts
  -> U.Contract
  -> Either TCError SomeContract
typeCheckContract cs c =
  runTypeCheck (U.contractParameter c) cs $ typeCheckContractImpl c

withWTP :: forall t a. SingI t => (WellTyped t => TypeCheck a) -> TypeCheck a
withWTP fn = case getWTP @t of
  Just Dict -> fn
  Nothing -> throwError $ TCContractError "Not a well typed value" Nothing

withWTPInstr_ :: forall t a. SingI t => U.ExpandedInstr -> SomeHST -> (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
withWTPInstr_ v t fn = case getWTP @t of
  Just Dict -> fn
  Nothing -> do
    loc <- ask
    throwError $ TCFailedOnInstr v t loc Nothing (Just $ UnsupportedTypeForScope (demote @t) BtNotComparable)

typeCheckContractImpl
  :: U.Contract
  -> TypeCheck SomeContract
typeCheckContractImpl (U.Contract (U.ParameterType mParam rootAnn) mStorage pCode) = 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
          inp' :/ instrOut <- usingReaderT def $ typeCheckImpl typeCheckInstr pCode inp
          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 (NTPair def def def starNotes storageNote)
                          `onLeft`
                      ((TCContractError "contract output type violates convention:") . Just . AnnError)
                  pure $ SomeContract Contract
                    { cCode = instr
                    , cParamNotes
                    , cStoreNotes
                    }
                Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err
            AnyOutInstr instr ->
              pure $ SomeContract Contract
                { cCode = instr
                , cParamNotes
                , cStoreNotes
                }
  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

-- | 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 = 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 @Val 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 typeCheckInstr

typeVerifyTopLevelType
  :: (SingI t, HasCallStack)
  => TcOriginatedContracts -> U.Value -> Either TCError (Value t)
typeVerifyTopLevelType originatedContracts valueU =
  runTypeCheck param originatedContracts $ usingReaderT (def :: InstrCallStack) $
    typeCheckValue valueU
  where
    param = error "parameter type touched during top-level type typecheck"

typeCheckTopLevelType
  :: HasCallStack
  => TcOriginatedContracts -> U.Type -> U.Value -> Either TCError SomeValue
typeCheckTopLevelType originatedContracts typeU valueU =
  withSomeSingT (fromUType typeU) $ \(_ :: Sing t) ->
    SomeValue <$> typeVerifyTopLevelType @t originatedContracts 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

-- | 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 typeCheckList ext si

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

  (U.DROP, SNil) -> notEnoughItemsOnStack

  (U.DROPN nTotal, inputHST) ->
    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) ->
    pure (inp :/ DUP ::: (a ::& a::& rs))

  (U.DUP _vn, SNil) -> notEnoughItemsOnStack

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

  (U.SWAP, _) -> notEnoughItemsOnStack

  (U.DIG nTotal, inputHST) ->
    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) ->
    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) ->
    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) -> do
    pure (inp :/ SOME ::: ((NTOption tn an, Dict, vn) ::& rs))

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

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

  (U.UNIT tn vn, _) ->
    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) -> 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 :/ PAIR ::: ((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) -> 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) -> 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) -> 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) -> 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) ->
    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) ->
    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) -> do
        ait <- withWTPInstr @t1 $ pure $ (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{}, _, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTSet{}, _, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTMap{}, _, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTString{}, _, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTBytes{}, _, _) ::& _) -> 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) ->
    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) -> 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) ->
    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 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 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, _, _) ::&+ _) ->
    memImpl notesK inp varNotes
  (U.MEM varNotes,
   _ ::& (STMap{}, NTMap _ notesK _, _, _) ::&+ _) ->
    memImpl notesK inp varNotes
  (U.MEM varNotes,
   _ ::& (STBigMap{}, NTBigMap _ notesK _, _, _) ::&+ _) ->
    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), _, _) ::&+ _) ->
    withWTPInstr @v $ getImpl notesK inp notesV varNotes
  (U.GET varNotes,
   _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
    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)), _, _) ::&+ _) ->
    updImpl notesK inp (NTOption U.noAnn notesV) varNotes
  (U.UPDATE varNotes,
   _ ::& _ ::& (STBigMap{}, NTBigMap _ notesK (notesV :: Notes v), _, _) ::&+ _) ->
    updImpl notesK inp (NTOption U.noAnn notesV) varNotes
  (U.UPDATE varNotes,
   _ ::& _ ::& (STSet{}, NTSet _ (notesK :: Notes k), _, _) ::&+ _) ->
    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
    _ :/ tp <- lift $ typeCheckList is rs
    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
          _ :/ tp <- lift $ typeCheckList is ait
          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 (AsUType (ins :: Notes t)) (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 uInstr is vn ins ons i

  (U.EXEC vn, ((_ :: Notes t1), _, _)
                              ::& ( STLambda _ _
                                  , NTLambda _ (_ :: Notes t1') (t2n :: Notes t2')
                                  , _
                                  , _
                                  )
                              ::&+ rs) -> 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) -> 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 uInstr is s $
      \subI t -> pure $ inp :/ DIP subI ::: (a ::& t)

  (U.DIP _is, SNil) -> notEnoughItemsOnStack

  (U.DIPN nTotal instructions, inputHST) ->
    go nTotal inputHST <&> \case
    TCDipHelper s subI out -> inputHST :/ DIPN s subI ::: out
    where
      go :: forall inp. Typeable inp
        => Word
        -> HST inp
        -> TypeCheckInstr (TCDipHelper inp)
      go n curHST = case (n, curHST) of
        (0, _) -> typeCheckDipBody uInstr instructions curHST $ \subI t ->
          pure (TCDipHelper SZ subI t)
        (_, SNil) -> notEnoughItemsOnStack
        (_, hstHead ::& hstTail) ->
          go (n - 1) hstTail <&> \case
          TCDipHelper s subI out -> TCDipHelper (SS s) subI (hstHead ::& out)
  (u, v) -> case (u, v) of -- Workaround for not exceeding -fmax-pmcheck-iterations limit
    (U.FAILWITH, (_ ::& _)) ->
      pure $ inp :/ AnyOutInstr FAILWITH

    (U.FAILWITH, _) -> notEnoughItemsOnStack

    (U.CAST vn (AsUType (castToNotes :: Notes t)), (en, _, evn) ::& rs) -> 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) ->
      pure $ inp :/ RENAME ::: ((an, Dict, vn) ::& rs)

    (U.RENAME _, SNil) -> notEnoughItemsOnStack

    (U.UNPACK tn vn mt, (NTBytes{}, _, _) ::& rs) ->
      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) -> 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{}, _, _) ::& _) ->
      concatImpl inp vn
    (U.CONCAT vn, (NTString{}, _, _) ::& (NTString{}, _, _) ::& _) ->
      concatImpl inp vn
    (U.CONCAT vn, (STList STBytes, _, _, _) ::&+ _) ->
      concatImpl' inp vn
    (U.CONCAT vn, (STList STString, _, _, _) ::&+ _) ->
      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{}, _, _) ::& _) -> sliceImpl inp vn
    (U.SLICE vn, (NTNat{}, _, _) ::&
                 (NTNat{}, _, _) ::&
                 (NTBytes{}, _, _) ::& _) -> sliceImpl inp vn

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

    (U.ISNAT vn', (NTInt{}, _, oldVn) ::& rs) -> 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, _, _, _) ::&+ _) -> addImpl a b inp vn

    (U.ADD _, _) -> notEnoughItemsOnStack

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

    (U.SUB _, _) -> notEnoughItemsOnStack

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

    (U.MUL _, _) -> notEnoughItemsOnStack

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

    (U.EDIV _, _) -> notEnoughItemsOnStack

    (U.ABS vn, (STInt, _, _, _) ::&+ _) -> unaryArithImpl @Abs ABS inp vn
    (U.ABS _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []

    (U.ABS _, SNil) -> notEnoughItemsOnStack

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

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

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

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

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

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

    (U.NOT vn, (STNat, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
    (U.NOT vn, (STBool, _, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
    (U.NOT vn, (STInt, _, _, _) ::&+ _) -> 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
      )
      -> 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{}, _, _) ::& _) -> unaryArithImpl @Eq' EQ inp vn
    (U.EQ _, _ ::& _) ->
      failWithErr $ UnexpectedType $ (ExpectInt :| []) :| []
    (U.EQ _, SNil) -> notEnoughItemsOnStack

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

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

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

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

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

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

    (U.SELF vn fn, _) -> do
      (U.ParameterType cpType rootAnn) <- gets tcContractParam
      -- Wrapping into 'ParamNotesUnsafe' is safe because originated contract has
      -- valid parameter type
      withUType cpType $ \((`ParamNotesUnsafe` rootAnn) -> notescp :: ParamNotes t) -> do
        proofScope <- onScopeCheckInstrErr @t uInstr (SomeHST inp) (Just ContractParameter)
          $ checkScope @(ParameterScope t)
        case proofScope of
          Dict -> do
            epName <- onTypeCheckInstrErr uInstr (SomeHST inp) Nothing $
                        epNameFromRefAnn fn `onLeft` IllegalEntryPoint
            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)

    (U.CONTRACT vn fn mt, (NTAddress{}, _, _) ::& rs) ->
      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) -> 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) -> 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) -> do
        (SomeContract
          (Contract
            (contr :: ContractCode p' g')
            paramNotes
            storeNotes))
          <- 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)
          ::: ((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) ->
      pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, Dict, vn) ::& rs)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    (U.CHAIN_ID vn, _) ->
      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 a. SingI t => (WellTyped t => TypeCheckInstr a) -> TypeCheckInstr a
    withWTPInstr fn = withWTPInstr_ @t uInstr (SomeHST inp) fn

    failWithErr :: (MonadReader InstrCallStack m, MonadError TCError m) => TCTypeError -> m a
    failWithErr = typeCheckInstrErr' uInstr (SomeHST inp) Nothing

    notEnoughItemsOnStack :: (MonadReader InstrCallStack m, MonadError TCError m) => m a
    notEnoughItemsOnStack = failWithErr 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'
     )
  -> ([U.ExpandedOp] -> [U.ExpandedOp] -> U.ExpandedInstr)
  -> [U.ExpandedOp]
  -> [U.ExpandedOp]
  -> HST bti
  -> HST bfi
  -> HST (cond ': rs)
  -> TypeCheckInstr (SomeInstr (cond ': rs))
genericIf cons mCons mbt mbf bti bfi i@(_ ::& _) = do
  _ :/ pinstr <- lift $ typeCheckList mbt bti
  _ :/ qinstr <- lift $ typeCheckList mbf bfi
  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)
    )
  => Notes (MapOpInp c)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST (c ': rs)
  -> (forall v' . (KnownT v') =>
        Notes v' -> HST rs -> TypeCheckInstr (HST (MapOpRes c v' ': rs)))
  -> TypeCheckInstr (SomeInstr (c ': rs))
mapImpl vn instr mp i@(_ ::& rs) mkRes = do
  _ :/ subp <- lift $ typeCheckList mp ((vn, Dict, def) ::& rs)
  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)
  -> TypeCheckInstr (SomeInstr (c ': rs))
iterImpl en instr mp i@((_, _, lvn) ::& rs) = do
  let evn = deriveVN "elt" lvn
  _ :/ subp <-
    case mp of
      [] -> typeCheckInstrErr' instr (SomeHST i) (Just Iteration) EmptyCode
      _ -> typeCheckImpl typeCheckInstr mp ((en, Dict, evn) ::& rs)
  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
    )
  => U.ExpandedInstr
  -> [U.ExpandedOp]
  -> VarAnn
  -> Notes it
  -> Notes ot
  -> HST ts
  -> TypeCheckInstr (SomeInstr ts)
lamImpl instr is vn ins ons i = do
  whenJust (getFirst $ foldMap hasSelf is) $ \selfInstr ->
    typeCheckInstrErr' instr (SomeHST i) (Just LambdaCode) $ InvalidInstruction selfInstr
  _ :/ lamI <- lift $ typeCheckList is ((ins, Dict, def) ::& SNil)
  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
  TCDipHelper ::
    forall (n :: Peano) inp out s s'.
    (Typeable out, ConstraintDIPN n inp out s s') =>
    Sing n -> Instr s s' -> HST out -> TCDipHelper inp

typeCheckDipBody ::
     forall inp r. Typeable inp
  => U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST inp
  -> (forall out. Typeable out =>
                    Instr inp out -> HST out -> TypeCheckInstr r)
  -> TypeCheckInstr r
typeCheckDipBody mainInstr instructions inputHST callback = do
  _ :/ tp <- lift (typeCheckList instructions inputHST)
  case tp 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`.
      typeCheckInstrErr' mainInstr (SomeHST inputHST) (Just DipCode) CodeAlwaysFails
    subI ::: t -> callback subI t