Instr.hs

-- | 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.Constraint (Dict(..))
import Data.Default (def)
import Data.Generics (everything, mkQ)
import Data.Singletons (SingI(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
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.para c) cs $ typeCheckContractImpl c

typeCheckContractImpl
  :: U.Contract
  -> TypeCheck SomeContract
typeCheckContractImpl (U.Contract mParam mStorage pCode) = do
  code <- maybe (throwError $ TCContractError "no instructions in contract code" Nothing)
                pure (nonEmpty pCode)
  withUType mParam $ \(paramNote :: Notes param) ->
    withUType mStorage $ \(storageNote :: Notes st) -> do
      (Dict, Dict) <-
        note (hasTypeError "parameter" paramNote) $
          (,) <$> opAbsense (notesSing paramNote)
              <*> nestedBigMapsAbsense (notesSing paramNote)
      (Dict, Dict, Dict) <-
        note (hasTypeError "storage" storageNote) $
          (,,) <$> opAbsense (notesSing storageNote)
               <*> nestedBigMapsAbsense (notesSing storageNote)
               <*> contractTypeAbsense (notesSing storageNote)
      let inpNote = NTPair def def def paramNote storageNote
      let inp = (inpNote, def) ::& SNil
      inp' :/ instrOut <- typeCheckNE code inp
      let (paramNotesRaw, fcStoreNotes) = case inp' of
            (NTPair _ _ _ cpNotes stNotes, _) ::& SNil -> (cpNotes, stNotes)
      fcParamNotesSafe <-
        liftEither $
        mkParamNotes paramNotesRaw `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 FullContract
                { fcCode = instr
                , fcParamNotesSafe, fcStoreNotes
                }
            Left err -> Left $ TCContractError "contract output type violates convention:" $ Just err
        AnyOutInstr instr ->
          pure $ SomeContract FullContract
            { fcCode = instr
            , fcParamNotesSafe, fcStoreNotes
            }
  where
    hasTypeError name (_ :: proxy t) =
      TCContractError ("contract " <> name <> " type error") $
      Just $ UnsupportedTypes [demote @t]

-- | Like 'typeCheck', but for non-empty lists.
typeCheckNE
  :: (Typeable inp)
  => NonEmpty U.ExpandedOp
  -> HST inp
  -> TypeCheck (SomeInstr inp)
typeCheckNE (x :| xs) = usingReaderT def . typeCheckImpl typeCheckInstr (x : xs)

-- | 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.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) -> onTypeCheckInstrErr uInstr
          (SomeHST SNil) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDrop))

        (_, (_ ::& 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.SWAP, a ::& b ::& rs) ->
    pure (inp :/ SWAP ::: (b ::& a ::& rs))

  (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) -> onTypeCheckInstrErr uInstr
          (SomeHST SNil) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDig))

        (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.
        _ -> onTypeCheckInstrErr uInstr
          (SomeHST i) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDug))

  (U.PUSH vn mt mval, i) ->
    withUType mt $ \(nt :: Notes t) -> do
      val <- typeCheckValue @t mval
      proofOp <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST i)
              "Operations in constant are not allowed"
              $ Left $ UnsupportedTypes [demote @t])
        pure (opAbsense $ notesSing nt)
      proofBigMap <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST i)
              "BigMaps in constant are not allowed"
              $ Left $ UnsupportedTypes [demote @t])
        pure (bigMapAbsense $ notesSing nt)
      proofContract <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST i)
              "Contract type in constant is not allowed"
              $ Left $ UnsupportedTypes [demote @t])
        pure (contractTypeAbsense $ notesSing nt)
      case (proofOp, proofBigMap, proofContract) of
        (Dict, Dict, Dict) -> pure $ i :/ PUSH val ::: ((nt, vn) ::& i)

  (U.SOME tn vn, (an, _) ::& rs) -> do
    pure (inp :/ SOME ::: ((NTOption tn an, vn) ::& rs))

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

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

  (U.IF_NONE mp mq, (STOption{}, ons, ovn) ::&+ rs) -> do
    let (an, avn) = deriveNsOption ons ovn
    genericIf IF_NONE U.IF_NONE mp mq rs ((an, avn) ::& rs) inp

  (U.PAIR tn vn pfn qfn, (an, avn) ::& (bn, bvn) ::& rs) -> do
    let (vn', pfn', qfn') = deriveSpecialFNs pfn qfn avn bvn
        ns = NTPair tn pfn' qfn' an bn
    pure (inp :/ PAIR ::: ((ns, vn `orAnn` vn') ::& rs))

  (U.CAR vn fn, (STPair{}, NTPair pairTN pfn qfn pns qns, pairVN) ::&+ rs) -> do
    pfn' <- onTypeCheckInstrAnnErr uInstr inp "wrong car type:" (convergeAnns fn pfn)
    let vn' = deriveSpecialVN vn pfn' pairVN
        i' = (NTPair pairTN pfn' qfn pns qns, pairVN) ::& rs
    pure $ i' :/ AnnCAR fn ::: ((pns, vn') ::& rs)

  (U.CDR vn fn, (STPair{}, NTPair pairTN pfn qfn pns qns, pairVN) ::&+ rs) -> do
    qfn' <- onTypeCheckInstrAnnErr uInstr inp "wrong cdr type:" (convergeAnns fn qfn)

    let vn' = deriveSpecialVN vn qfn' pairVN
        i' = (NTPair pairTN pfn qfn' pns qns, pairVN) ::& rs
    pure $ i' :/ AnnCDR fn ::: ((qns, vn') ::& rs)

  (U.LEFT tn vn pfn qfn bMt, (an, _) ::& rs) ->
    withUType bMt $ \bn -> do
      let ns = NTOr tn pfn qfn an bn
      pure (inp :/ LEFT ::: ((ns, vn) ::& rs))

  (U.RIGHT tn vn pfn qfn aMt, (bn, _) ::& rs) ->
    withUType aMt $ \an -> do
      let ns = NTOr tn pfn qfn an bn
      pure (inp :/ RIGHT ::: ((ns, vn) ::& rs))

  (U.IF_LEFT mp mq, (STOr{}, ons, ovn) ::&+ rs) -> do
    let (an, bn, avn, bvn) = deriveNsOr ons ovn
        ait = (an, avn) ::& rs
        bit = (bn, bvn) ::& rs
    genericIf IF_LEFT U.IF_LEFT mp mq ait bit inp

  (U.NIL tn vn elMt, i) ->
    withUType elMt $ \elNotes ->
      pure $ i :/ NIL ::: ((NTList tn elNotes, vn) ::& i)

  (U.CONS vn, ((an :: Notes a), _)
                ::& ((ln :: Notes l), _) ::& rs) ->
    case eqType @('TList a) @l of
      Right Refl -> do
        n <- onTypeCheckInstrAnnErr uInstr inp "wrong cons type:" (converge ln (NTList def an))
        pure $ inp :/ CONS ::: ((n, vn) ::& rs)
      Left m -> onTypeCheckInstrErr uInstr (SomeHST inp)
                  ("list element type is different from one "
                  <> "that is being CONSed:") (Left m)

  (U.IF_CONS mp mq, (STList{}, ns, vn) ::&+ rs) -> do
    let NTList _ an = ns
        ait = (an, vn <> "hd") ::& (ns, vn <> "tl") ::& rs
    genericIf IF_CONS U.IF_CONS mp mq ait rs inp

  (U.SIZE vn, (NTList{}, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTSet{}, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTMap{}, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTcs SCString, _) ::& _) -> sizeImpl inp vn
  (U.SIZE vn, (NTcs SCBytes, _) ::& _) -> sizeImpl inp vn

  (U.EMPTY_SET tn vn (U.Comparable mk ktn), i) ->
    withSomeSingCT mk $ \k ->
      pure $ i :/ EMPTY_SET ::: ((STSet k, NTSet tn ktn, vn) ::&+ inp)

  (U.EMPTY_MAP tn vn (U.Comparable mk ktn) mv, i) ->
    withUType mv $ \vns ->
    withSomeSingCT mk $ \k -> do
      let ns = NTMap tn ktn vns
      pure $ i :/ EMPTY_MAP ::: ((STMap k sing, ns, vn) ::&+ i)

  (U.EMPTY_BIG_MAP tn vn (U.Comparable mk ktn) mv, i) ->
    withUType mv $ \vns ->
    withSomeSingCT mk $ \k -> do
      let ns = NTBigMap tn ktn vns
      pure $ i :/ EMPTY_BIG_MAP ::: ((STBigMap k sing, ns, vn) ::&+ i)

  (U.MAP vn mp, (STList _, NTList _ vns, _vn) ::&+ _) -> do
    mapImpl vns uInstr mp inp
      (\rn -> (::&) (NTList def rn, vn))


  (U.MAP vn mp, (STMap{}, NTMap _ kns vns, _vn) ::&+ _) -> do
    let pns = NTPair def def def (NTc kns) vns
    mapImpl pns uInstr mp inp
      (\rn -> (::&) (NTMap def kns rn, vn))

-- case `U.HSTER []` is wrongly typed by definition
-- (as it is required to at least drop an element), so we don't consider it

  (U.ITER (i1 : ir), (STSet _, NTSet _ en, _) ::&+ _) -> do
    iterImpl (NTc en) uInstr (i1 :| ir) inp

  (U.ITER (i1 : ir), (STList _, NTList _ en, _) ::&+ _) -> do
    iterImpl en uInstr (i1 :| ir) inp

  (U.ITER (i1 : ir), (STMap _ _, NTMap _ kns vns, _) ::&+ _) -> do
    let en = NTPair def def def (NTc kns) vns
    iterImpl en uInstr (i1 :| ir) inp

  (U.MEM vn, (NTc _, _) ::& (STSet{}, NTSet{}, _) ::&+ _) ->
    memImpl uInstr inp vn
  (U.MEM vn, (NTc _, _) ::& (STMap{}, NTMap{}, _) ::&+ _) ->
    memImpl uInstr inp vn
  (U.MEM vn, (NTc _, _) ::& (STBigMap{}, NTBigMap{}, _) ::&+ _) ->
    memImpl uInstr inp vn

  (U.GET vn, _ ::& (STMap{}, NTMap _ _ v, _) ::&+ _) ->
    getImpl uInstr inp v vn
  (U.GET vn, _ ::& (STBigMap{}, NTBigMap _ _ v, _) ::&+ _) ->
    getImpl uInstr inp v vn

  (U.UPDATE vn, _ ::& _ ::& (STMap _ _, _, _) ::&+ _) ->
    updImpl uInstr inp vn
  (U.UPDATE vn, _ ::& _ ::& (STBigMap _ _, _, _) ::&+ _) ->
    updImpl uInstr inp vn
  (U.UPDATE vn, _ ::& _ ::& (STSet _, _, _) ::&+ _) ->
    updImpl uInstr inp vn

  (U.IF mp mq, (NTcs SCBool, _) ::& rs) ->
    genericIf IF U.IF mp mq rs rs inp

  (U.LOOP is, (NTcs SCBool, _) ::& (rs :: HST rs)) -> do
    _ :/ tp <- lift $ typeCheckList is rs
    case tp of
      subI ::: (o :: HST o) -> do
        case eqHST o (sing @('Tc 'CBool) -:& rs) of
          Right Refl -> do
            let _ ::& rs' = o
            pure $ inp :/ LOOP subI ::: rs'
          Left m -> onTypeCheckInstrErr uInstr (SomeHST inp)
                      "iteration expression has wrong output stack type:" (Left m)
      AnyOutInstr subI ->
        pure $ inp :/ LOOP subI ::: rs

  (U.LOOP_LEFT is, (os@STOr{}, ons, ovn) ::&+ rs) -> do
    let (an, bn, avn, bvn) = deriveNsOr ons ovn
        ait = (an, avn) ::& rs
    _ :/ tp <- lift $ typeCheckList is ait
    case tp of
      subI ::: o -> do
        case (eqHST o (os -:& rs), o) of
          (Right Refl, ((ons', ovn') ::& rs')) -> do
              let (_, bn', _, bvn') = deriveNsOr ons' ovn'
              br <- onTypeCheckInstrAnnErr uInstr inp "wrong LOOP_LEFT input type:" $
                      convergeHSTEl (bn, bvn) (bn', bvn')
              pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs')
          (Left m, _) -> onTypeCheckInstrErr uInstr (SomeHST inp)
                          "iteration expression has wrong output stack type:" (Left m)
      AnyOutInstr subI -> do
        let br = (bn, bvn)
        pure $ inp :/ LOOP_LEFT subI ::: (br ::& rs)

  (U.LAMBDA vn (AsUType ins) (AsUType ons) is, i) -> do
    -- further processing is extracted into another function just not to
    -- litter our main typechecking logic
    lamImpl uInstr is vn ins ons i

  (U.EXEC vn, ((_ :: Notes t1), _)
                              ::& ( STLambda _ _
                                  , NTLambda _ (_ :: Notes t1') t2n
                                  , _
                                  )
                              ::&+ rs) -> do
    Refl <- onTypeCheckInstrErr uInstr (SomeHST inp)
                  "lambda is given argument with wrong type:" (eqType @t1 @t1')
    pure $ inp :/ EXEC ::: ((t2n, vn) ::& rs)

  (U.APPLY vn, ((_ :: Notes a'), _)
                  ::& ( STLambda (STPair sa _) _
                      , NTLambda vann (NTPair _ _ _ (_ :: Notes a) (nb :: Notes b)) sc
                      , _)
                  ::&+ rs) -> do
    let
      l2n = NTLambda vann nb sc

    proofArgEq <- onTypeCheckInstrErr uInstr (SomeHST inp)
                  "lambda is given argument with wrong type:" (eqType @a' @a)
    proofOp <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
              "Operations in argument of partially applied lambda are not allowed"
              $ Left $ UnsupportedTypes [demote @a])
      pure (opAbsense sa)
    proofBigMap <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
              "BigMaps in argument of partially applied lambda are not allowed"
              $ Left $ UnsupportedTypes [demote @a])
      pure (bigMapAbsense sa)
    proofContract <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
              "Contract type in constant is not allowed"
              $ Left $ UnsupportedTypes [demote @a])
      pure (contractTypeAbsense sa)
    case (proofArgEq, proofOp, proofBigMap, proofContract) of
      (Refl, Dict, Dict, Dict) ->
        pure $ inp :/ (APPLY @a) ::: ((l2n, vn) ::& rs)

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

  (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) -> onTypeCheckInstrErr uInstr
          (SomeHST SNil) "" (Left (NotEnoughItemsOnStack nTotal NotEnoughDip))
        (_, hstHead ::& hstTail) ->
          go (n - 1) hstTail <&> \case
          TCDipHelper s subI out -> TCDipHelper (SS s) subI (hstHead ::& out)

  (U.FAILWITH, (_ ::& _)) ->
    pure $ inp :/ AnyOutInstr FAILWITH

  (U.CAST vn (AsUType castToNotes), (en, evn) ::& rs) -> do
    (Refl, _) <- errM $ matchTypes en castToNotes
    pure $ inp :/ CAST ::: ((castToNotes, vn `orAnn` evn) ::& rs)
    where
      errM :: (MonadReader InstrCallStack m, MonadError TCError m) => Either TCTypeError a -> m a
      errM = onTypeCheckInstrErr uInstr (SomeHST inp) "cast to incompatible type:"

  (U.RENAME vn, (an, _) ::& rs) ->
    pure $ inp :/ RENAME ::: ((an, vn) ::& rs)

  (U.UNPACK tn vn mt, (NTcs SCBytes, _) ::& rs) ->
    withUType mt $ \tns -> do
      let ns = NTOption tn tns
      proofOp <-
        maybe (typeCheckInstrErr uInstr (SomeHST inp)
              "Operation cannot appear in serialized data")
        pure (opAbsense $ notesSing tns)
      proofBigMap <-
        maybe (typeCheckInstrErr uInstr (SomeHST inp)
              "BigMap cannot appear in serialized data")
        pure (bigMapAbsense $ notesSing tns)
      proofContract <-
        maybe (typeCheckInstrErr uInstr (SomeHST inp)
              "UNPACK should not contain 'contract' type")
        pure (contractTypeAbsense $ notesSing tns)
      case (proofOp, proofBigMap, proofContract) of
        (Dict, Dict, Dict) ->
          pure $ inp :/ UNPACK ::: ((ns, vn) ::& rs)

  (U.PACK vn, (a, _) ::& rs) -> do
    proofOp <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
            "Operations cannot appear in serialized data"
            $ Left $ UnsupportedTypes [notesT a])
      pure (opAbsense $ notesSing a)
    proofBigMap <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
            "BigMap cannot appear in serialized data"
            $ Left $ UnsupportedTypes [notesT a])
      pure (bigMapAbsense $ notesSing a)
    case (proofOp, proofBigMap) of
      (Dict, Dict) ->
        pure $ inp :/ PACK ::: ((starNotes, vn) ::& rs)

  (U.CONCAT vn, (NTcs SCBytes, _) ::& (NTcs SCBytes, _) ::& _) ->
    concatImpl inp vn
  (U.CONCAT vn, (NTcs SCString, _) ::& (NTcs SCString, _) ::& _) ->
    concatImpl inp vn
  (U.CONCAT vn, (STList (STc SCBytes), _, _) ::&+ _) ->
    concatImpl' inp vn
  (U.CONCAT vn, (STList (STc SCString), _, _) ::&+ _) ->
    concatImpl' inp vn
  (U.SLICE vn, (NTcs SCNat, _) ::&
               (NTcs SCNat, _) ::&
               (NTcs SCString, _) ::& _) -> sliceImpl inp vn
  (U.SLICE vn, (NTcs SCNat, _) ::&
               (NTcs SCNat, _) ::&
               (NTcs SCBytes, _) ::& _) -> sliceImpl inp vn

  (U.ISNAT vn', (NTcs SCInt, oldVn) ::& rs) -> do
    let vn = vn' `orAnn` oldVn
    pure $ inp :/ ISNAT ::: ((starNotes, vn) ::& rs)

  (U.ADD vn, (STc a, _, _) ::&+ (STc b, _, _) ::&+ _) -> addImpl a b inp vn
  (U.SUB vn, (STc a, _, _) ::&+ (STc b, _, _) ::&+ _) -> subImpl a b inp vn
  (U.MUL vn, (STc a, _, _) ::&+ (STc b, _, _) ::&+ _) -> mulImpl a b inp vn
  (U.EDIV vn, (STc a, _, _) ::&+ (STc b, _, _) ::&+ _) -> edivImpl a b inp vn

  (U.ABS vn, (STc SCInt, _, _) ::&+ _) -> unaryArithImpl @Abs ABS inp vn

  (U.NEG vn, (STc SCInt, _, _) ::&+ _) -> unaryArithImpl @Neg NEG inp vn
  (U.NEG vn, (STc SCNat, _, _) ::&+ _) -> unaryArithImpl @Neg NEG inp vn

  (U.LSL vn, (STc SCNat, _, _) ::&+
             (STc SCNat, _, _) ::&+ _) -> arithImpl @Lsl LSL inp vn

  (U.LSR vn, (STc SCNat, _, _) ::&+
             (STc SCNat, _, _) ::&+ _) -> arithImpl @Lsr LSR inp vn

  (U.OR vn, (STc SCBool, _, _) ::&+
            (STc SCBool, _, _) ::&+ _) -> arithImpl @Or OR inp vn
  (U.OR vn, (STc SCNat, _, _) ::&+
            (STc SCNat, _, _) ::&+ _) -> arithImpl @Or OR inp vn

  (U.AND vn, (STc SCInt, _, _) ::&+
             (STc SCNat, _, _) ::&+ _) -> arithImpl @And AND inp vn
  (U.AND vn, (STc SCNat, _, _) ::&+
             (STc SCNat, _, _) ::&+ _) -> arithImpl @And AND inp vn
  (U.AND vn, (STc SCBool, _, _) ::&+
             (STc SCBool, _, _) ::&+ _) -> arithImpl @And AND inp vn

  (U.XOR vn, (STc SCBool, _, _) ::&+
             (STc SCBool, _, _) ::&+ _) -> arithImpl @Xor XOR inp vn
  (U.XOR vn, (STc SCNat, _, _) ::&+
             (STc SCNat, _, _) ::&+ _) -> arithImpl @Xor XOR inp vn

  (U.NOT vn, (STc SCNat, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
  (U.NOT vn, (STc SCBool, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn
  (U.NOT vn, (STc SCInt, _, _) ::&+ _) -> unaryArithImpl @Not NOT inp vn

  (U.COMPARE vn,
        (an :: Notes aT, _)
    ::& (bn :: Notes bT, _)
    ::& rs
    )
    -> do
    case eqType @aT @bT of
      Right Refl -> do
        void . errConv $ converge an bn
        proof <-
          maybe (onTypeCheckInstrErr (U.COMPARE vn) (SomeHST inp)
                  "comparison is given incomparable arguments"
                  $ Left $ UnsupportedTypes [demote @aT, demote @bT])
            pure (comparabilityPresence $ notesSing an)

        case proof of
          Dict -> do
            pure $ inp :/ COMPARE ::: ((starNotes, vn) ::& rs)

      Left err -> do
        typeCheckInstrErr' uInstr (SomeHST inp) "comparing different types:" err
    where
      errConv :: (MonadReader InstrCallStack m, MonadError TCError m) => Either AnnConvergeError a -> m a
      errConv = onTypeCheckInstrAnnErr uInstr inp "comparing types with different annotations:"

  (U.EQ vn, (NTcs SCInt, _) ::& _) -> unaryArithImpl @Eq' EQ inp vn

  (U.NEQ vn, (NTcs SCInt, _) ::& _) -> unaryArithImpl @Neq NEQ inp vn

  (U.LT vn, (NTcs SCInt, _) ::& _) -> unaryArithImpl @Lt LT inp vn

  (U.GT vn, (NTcs SCInt, _) ::& _) -> unaryArithImpl @Gt GT inp vn

  (U.LE vn, (NTcs SCInt, _) ::& _) -> unaryArithImpl @Le LE inp vn

  (U.GE vn, (NTcs SCInt, _) ::& _) -> unaryArithImpl @Ge GE inp vn

  (U.INT vn, (NTcs SCNat, _) ::& rs) ->
    pure $ inp :/ INT ::: ((starNotes, vn) ::& rs)

  (U.SELF vn fn, _) -> do
    cpType <- gets tcContractParam
    let t = fromUType cpType
    -- Wrapping into 'ParamNotesUnsafe' is safe because originated contract has
    -- valid parameter type
    withUType cpType $ \(ParamNotesUnsafe -> notescp :: ParamNotes t) -> do
      proofOp <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
                "contract param type cannot contain operation"
                $ Left $ UnsupportedTypes [t])
        pure (opAbsense $ sing @t)
      proofBigMap <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
                "contract param type cannot contain nested big_map"
                $ Left $ UnsupportedTypes [t])
        pure (nestedBigMapsAbsense $ sing @t)
      case (proofOp, proofBigMap) of
        (Dict, Dict) -> do
          epName <- onTypeCheckInstrErr uInstr (SomeHST inp) "Bad annotation:" $
                      epNameFromRefAnn fn `onLeft` IllegalEntryPoint
          MkEntryPointCallRes (argNotes :: Notes arg) epc <-
            mkEntryPointCall epName notescp
              & maybeToRight (EntryPointNotFound epName)
              & onTypeCheckInstrErr uInstr (SomeHST inp) "entrypoint not found"
          let ntRes = NTContract U.noAnn argNotes
          pure $ inp :/ SELF @arg (SomeEpc epc)
                  ::: ((ntRes, vn) ::& inp)

  (U.CONTRACT vn fn mt, (NTcs SCAddress, _) ::& rs) ->
    withUType mt $ \(tns :: Notes t) -> do
      proofOp <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
                "contract param type cannot contain operation"
                $ Left $ UnsupportedTypes [fromUType mt])
        pure (opAbsense $ sing @t)
      proofBigMap <-
        maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
                "contract param type cannot contain nested big_map"
                $ Left $ UnsupportedTypes [fromUType mt])
        pure (nestedBigMapsAbsense $ sing @t)
      let ns = NTOption def $ NTContract def tns
      epName <- onTypeCheckInstrErr uInstr (SomeHST inp) "Bad annotation:" $
                  epNameFromRefAnn fn `onLeft` IllegalEntryPoint
      case (proofOp, proofBigMap) of
        (Dict, Dict) ->
          pure $ inp :/ CONTRACT tns epName ::: ((ns, vn) ::& rs)

  (U.TRANSFER_TOKENS vn, ((_ :: Notes p'), _)
    ::& (NTcs SCMutez, _)
    ::& (STContract (p :: Sing p), _, _) ::&+ rs) -> do
    proofOp <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
              "contract param type cannot contain operation"
              $ Left $ UnsupportedTypes [fromSingT p])
      pure (opAbsense p)
    proofBigMap <-
      maybe (onTypeCheckInstrErr uInstr (SomeHST inp)
              "contract param type cannot contain big_map"
              $ Left $ UnsupportedTypes [fromSingT p])
      pure (nestedBigMapsAbsense p)
    case (eqType @p @p', proofOp, proofBigMap) of
      (Right Refl, Dict, Dict) ->
        pure $ inp :/ TRANSFER_TOKENS ::: ((starNotes, vn) ::& rs)
      (Left m, _, _) ->
        onTypeCheckInstrErr uInstr (SomeHST inp)
          "mismatch of contract param type:" (Left m)

  (U.SET_DELEGATE vn, (STOption (STc SCKeyHash), _, _) ::&+ rs) -> do
    pure $ inp :/ SET_DELEGATE ::: ((starNotes, vn) ::& rs)

  (U.CREATE_CONTRACT ovn avn contract,
                 (STOption (STc SCKeyHash), _, _)
            ::&+ (NTcs SCMutez, _)
             ::& (gn :: Notes g, _) ::& rs) -> do
    (SomeContract (FullContract (contr :: ContractCode p' g') paramNotes storeNotes))
      <- lift $ typeCheckContractImpl contract
    Refl <- checkEqT @g @g' uInstr inp "contract storage type mismatch"
    void $ onTypeCheckInstrAnnErr uInstr inp "contract storage type mismatch" (converge gn storeNotes)
    pure $ inp :/ CREATE_CONTRACT (FullContract contr paramNotes storeNotes) :::
          ((starNotes, ovn) ::& (starNotes, avn) ::& rs)

  (U.IMPLICIT_ACCOUNT vn, (NTcs SCKeyHash, _) ::& rs) ->
    pure $ inp :/ IMPLICIT_ACCOUNT ::: ((starNotes, vn) ::& rs)

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

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

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

  (U.CHECK_SIGNATURE vn,
             (NTKey _, _)
             ::& (NTSignature _, _) ::& (NTcs SCBytes, _) ::& rs) ->
    pure $ inp :/ CHECK_SIGNATURE ::: ((starNotes, vn) ::& rs)

  (U.SHA256 vn, (NTcs SCBytes, _) ::& rs) ->
    pure $ inp :/ SHA256 ::: ((starNotes, vn) ::& rs)

  (U.SHA512 vn, (NTcs SCBytes, _) ::& rs) ->
    pure $ inp :/ SHA512 ::: ((starNotes, vn) ::& rs)

  (U.BLAKE2B vn, (NTcs SCBytes, _) ::& rs) ->
    pure $ inp :/ BLAKE2B ::: ((starNotes, vn) ::& rs)

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

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

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

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

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

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

  _ ->
    typeCheckInstrErr uInstr (SomeHST inp) "unknown expression"

-- | 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 <- checkEqHST qo po instr i
                    "branches have different output stack types:"
      o <- onTypeCheckInstrAnnErr instr i "branches have different output stack types:" (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
    , SingI (MapOpInp c)
    , Typeable (MapOpInp c)
    , Typeable (MapOpRes c)
    )
  => Notes (MapOpInp c)
  -> U.ExpandedInstr
  -> [U.ExpandedOp]
  -> HST (c ': rs)
  -> (forall v' . (Typeable v', SingI v') =>
        Notes v' -> HST rs -> HST (MapOpRes c v' ': rs))
  -> TypeCheckInstr (SomeInstr (c ': rs))
mapImpl vn instr mp i@(_ ::& rs) mkRes = do
  _ :/ subp <- lift $ typeCheckList mp ((vn, def) ::& rs)
  case subp of
    sub ::: subo ->
      case subo of
        (bn, _bvn) ::& rs' -> do
          Refl <- checkEqHST rs rs' instr i $
                      "map expression has changed not only top of the stack"
          pure $ i :/ MAP sub ::: mkRes bn rs'
        _ -> typeCheckInstrErr instr (SomeHST i) "map expression has wrong output stack type (empty stack)"
    AnyOutInstr _ ->
      typeCheckInstrErr instr (SomeHST i) "MAP code block always fails, which is not allowed"

iterImpl
  :: forall c rs .
    ( IterOp c
    , SingI (IterOpEl c)
    , Typeable (IterOpEl c)
    )
  => Notes (IterOpEl c)
  -> U.ExpandedInstr
  -> NonEmpty U.ExpandedOp
  -> HST (c ': rs)
  -> TypeCheckInstr (SomeInstr (c ': rs))
iterImpl en instr mp i@((_, lvn) ::& rs) = do
  let evn = deriveVN "elt" lvn
  _ :/ subp <- lift $ typeCheckNE mp ((en, evn) ::& rs)
  case subp of
    subI ::: o -> do
      Refl <- checkEqHST o rs instr i
                "iteration expression has wrong output stack type"
      pure $ i :/ ITER subI ::: o
    AnyOutInstr _ ->
      typeCheckInstrErr instr (SomeHST i) "ITER code block always fails, which is not allowed"

lamImpl
  :: forall it ot ts .
    ( Typeable it, Typeable ts, Typeable ot
    , SingI it, SingI ot
    )
  => U.ExpandedInstr
  -> [U.ExpandedOp]
  -> VarAnn
  -> Notes it
  -> Notes ot
  -> HST ts
  -> TypeCheckInstr (SomeInstr ts)
lamImpl instr is vn ins ons i = do
  when (any hasSelf is) $
    typeCheckInstrErr instr (SomeHST i) "The SELF instruction cannot appear in a lambda"
  _ :/ lamI <- lift $ typeCheckList is ((ins, def) ::& SNil)
  let lamNotes onsr = NTLambda def ins onsr
  let lamSt onsr = (lamNotes onsr, 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 "wrong output type of lambda's expression:" (converge ons ons')
            pure (LAMBDA (VLam $ RfNormal lam) ::: lamSt onsr)
        Left m -> onTypeCheckInstrErr instr (SomeHST i)
                    "wrong output type of lambda's expression:" (Left m)
    AnyOutInstr lam ->
      pure (LAMBDA (VLam $ RfAlwaysFails lam) ::: lamSt ons)
  where
    hasSelf :: U.ExpandedOp -> Bool
    hasSelf = everything (||)
      (mkQ False
       (\case
           (U.SELF{} :: U.InstrAbstract U.ExpandedOp) -> True
           _ -> False
       )
      )

----------------------------------------------------------------------------
-- 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)
          "Code within DIP instruction always fails, which is not allowed"
    subI ::: t -> callback subI t