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

-- | Module that provides type classes for converting to and from low-level
-- Micheline representation.
module Morley.Micheline.Class
  ( ToExpression (..)
  , FromExpError (..)
  , FromExpressionError
  , FromExp (..)
  , FromExpression
  , fromExpression
  ) where

import Control.Lens ((<>~))
import Data.Bits (Bits)
import Data.Singletons (SingI(..), demote, fromSing)
import Fmt (Buildable(..), fillSepF, indentF, nameF, pretty, punctuateF, unlinesF, (++|), (|++))

import Morley.Micheline.Expression
import Morley.Michelson.Text (mkMText, unMText)
import Morley.Michelson.TypeCheck (TcError, TypeCheckOptions(..), typeCheckingWith)
import Morley.Michelson.TypeCheck.Instr (typeCheckValue)
import Morley.Michelson.Typed
  (Contract, ForbidOp, Instr, LambdaCode'(..), Notes(..), T(..), Value, Value'(..), fromUType,
  mkUType, rfAnyInstr, toUType)
import Morley.Michelson.Typed.Convert
  (convertContractOptimized, instrToOpsOptimized, untypeValueOptimized)
import Morley.Michelson.Untyped qualified as Untyped
import Morley.Michelson.Untyped.Annotation
  (AnnotationSet(..), FieldAnn, FieldTag, RootAnn, TypeAnn, TypeTag, VarAnn, VarTag, annsCount,
  firstAnn, noAnn, secondAnn)
import Morley.Michelson.Untyped.Contract (ContractBlock(..), ContractBlockError, orderContractBlock)
import Morley.Michelson.Untyped.Instr (ExpandedInstr, ExpandedOp(..), InstrAbstract(..))
import Morley.Michelson.Untyped.Type (Ty(..))
import Morley.Michelson.Untyped.View
import Morley.Util.MismatchError

-- ToExpression
----------------------------------------------------------------------------

-- | Type class that provides an ability to convert
-- something to Micheline Expression.
class ToExpression a where
  toExpression :: a -> Expression

instance ForbidOp t => ToExpression (Value t) where
  toExpression = toExpression . untypeValueOptimized

instance ToExpression Untyped.Value where
  toExpression = \case
    Untyped.ValueInt v -> expressionInt v
    Untyped.ValueString s -> expressionString $ unMText s
    Untyped.ValueBytes (Untyped.InternalByteString bs) -> expressionBytes bs
    Untyped.ValueUnit -> expressionPrim' Prim_Unit [] []
    Untyped.ValueTrue -> expressionPrim' Prim_True [] []
    Untyped.ValueFalse -> expressionPrim' Prim_False [] []
    Untyped.ValuePair l r ->
      expressionPrim' Prim_Pair [toExpression l, toExpression r] []
    Untyped.ValueLeft v -> expressionPrim' Prim_Left [toExpression v] []
    Untyped.ValueRight v -> expressionPrim' Prim_Right [toExpression v] []
    Untyped.ValueSome v -> expressionPrim' Prim_Some [toExpression v] []
    Untyped.ValueNone -> expressionPrim' Prim_None [] []
    Untyped.ValueNil -> expressionSeq []
    Untyped.ValueSeq vs -> toExpression vs
    Untyped.ValueMap elts -> toExpression $ eltToExpr <$> elts
    Untyped.ValueLambda ops -> toExpression ops
    Untyped.ValueLamRec ops -> expressionPrim' Prim_Lambda_rec [toExpression ops] []
    where
      eltToExpr :: Untyped.Elt [] ExpandedOp -> Expression
      eltToExpr (Untyped.Elt l r) = expressionPrim' Prim_Elt
        [toExpression l, toExpression r] []


instance ToExpression (Instr inp out) where
  toExpression = toExpression . instrToOpsOptimized

instance ToExpression T where
  toExpression = toExpression . toUType

instance ToExpression (Notes t) where
  toExpression = toExpression . mkUType

instance ToExpression Untyped.T where
  toExpression = \case
    Untyped.TKey -> expressionPrim' Prim_key [] []
    Untyped.TUnit -> expressionPrim' Prim_unit [] []
    Untyped.TSignature -> expressionPrim' Prim_signature [] []
    Untyped.TChainId -> expressionPrim' Prim_chain_id [] []
    Untyped.TOption arg -> expressionPrim' Prim_option [toExpression arg] []
    Untyped.TList arg -> expressionPrim' Prim_list [toExpression arg] []
    Untyped.TSet arg -> expressionPrim' Prim_set [toExpression arg] []
    Untyped.TOperation -> expressionPrim' Prim_operation [] []
    Untyped.TContract arg -> expressionPrim' Prim_contract [toExpression arg] []
    Untyped.TTicket arg -> expressionPrim' Prim_ticket [toExpression arg] []
    t@Untyped.TPair{} -> expressionPrim' Prim_pair (rightCombedPairToList t) []
    Untyped.TOr fa1 fa2 l r ->
      let exprL = addTrimmedAnns (toExpression l) [] [fa1] []
          exprR = addTrimmedAnns (toExpression r) [] [fa2] []
      in expressionPrim' Prim_or [exprL, exprR] []
    Untyped.TLambda inp out ->
      expressionPrim' Prim_lambda [toExpression inp, toExpression out] []
    Untyped.TMap k v ->
      expressionPrim' Prim_map [toExpression k, toExpression v] []
    Untyped.TBigMap k v ->
      expressionPrim' Prim_big_map [toExpression k, toExpression v] []
    Untyped.TInt -> expressionPrim' Prim_int [] []
    Untyped.TNat -> expressionPrim' Prim_nat [] []
    Untyped.TString -> expressionPrim' Prim_string [] []
    Untyped.TBytes -> expressionPrim' Prim_bytes [] []
    Untyped.TMutez -> expressionPrim' Prim_mutez [] []
    Untyped.TBool -> expressionPrim' Prim_bool [] []
    Untyped.TKeyHash -> expressionPrim' Prim_key_hash [] []
    Untyped.TBls12381Fr -> expressionPrim' Prim_bls12_381_fr [] []
    Untyped.TBls12381G1 -> expressionPrim' Prim_bls12_381_g1 [] []
    Untyped.TBls12381G2 -> expressionPrim' Prim_bls12_381_g2 [] []
    Untyped.TTimestamp -> expressionPrim' Prim_timestamp [] []
    Untyped.TAddress -> expressionPrim' Prim_address [] []
    Untyped.TChest -> expressionPrim' Prim_chest [] []
    Untyped.TChestKey -> expressionPrim' Prim_chest_key [] []
    Untyped.TNever -> expressionPrim' Prim_never [] []
    Untyped.TSaplingState n -> expressionPrim' Prim_sapling_state [integralToExpr n] []
    Untyped.TSaplingTransaction n -> expressionPrim' Prim_sapling_transaction [integralToExpr n] []

    where
      addAnns :: Expression -> [Annotation] -> Expression
      addAnns e anns =
        e & _ExpressionPrim . mpaAnnotsL <>~ anns

      rightCombedPairToList :: Untyped.T -> [Expression]
      rightCombedPairToList t =
        let go ty (fa, va)
              | Ty (Untyped.TPair faL faR vaL vaR l r) ta <- ty
              , ta == noAnn, fa == noAnn, va == noAnn
              = toExpression l `addAnns` mkAnns [] [faL] [vaL] : go r (faR, vaR)
              | otherwise
              = one $ toExpression ty `addAnns` mkAnns [] [fa] [va]
        in go (Ty t noAnn) (noAnn, noAnn)

instance ToExpression Ty where
  toExpression (Ty t ta) = addTrimmedAnns (toExpression t) [ta] [] []

instance (ToExpression a) => ToExpression [a] where
  toExpression xs = expressionSeq $ toExpression <$> xs

instance (ToExpression a) => ToExpression (NonEmpty a) where
  toExpression = toExpression . toList

instance ToExpression Expression where
  toExpression = id

instance ToExpression ExpandedOp where
  toExpression = \case
    PrimEx instr   -> toExpression instr
    SeqEx s        -> expressionSeq $ toExpression <$> s
    WithSrcEx _ op -> toExpression op

instance ToExpression ViewName where
  toExpression (ViewName s) = expressionString s

-- Note: On adding new expressions here, you must also add the symmetric (reading) case
-- to FromExp x (InstrAbstract [] op) as well.
instance ToExpression ExpandedInstr where
  toExpression = \case
    PUSH va ty v -> expressionPrim' Prim_PUSH [toExpression ty, toExpression v] $
      mkAnns [] [] [va]
    DROP -> expressionPrim' Prim_DROP [] []
    DROPN n -> expressionPrim' Prim_DROP [integralToExpr n] []
    DUP va -> expressionPrim' Prim_DUP [] $ mkAnns [] [] [va]
    DUPN va n -> expressionPrim' Prim_DUP [integralToExpr n] $ mkAnns [] [] [va]
    SWAP -> expressionPrim' Prim_SWAP [] []
    DIG n -> expressionPrim' Prim_DIG [integralToExpr n] []
    DUG n -> expressionPrim' Prim_DUG [integralToExpr n] []
    SOME ta va ->
      expressionPrim' Prim_SOME [] $ mkAnns [ta] [] [va]
    NONE ta va ty -> expressionPrim' Prim_NONE [toExpression ty] $ mkAnns [ta] [] [va]
    UNIT ta va -> expressionPrim' Prim_UNIT [] $ mkAnns [ta] [] [va]
    IF_NONE ops1 ops2 ->
      expressionPrim' Prim_IF_NONE [toExpression ops1, toExpression ops2] []
    PAIR ta va fa1 fa2 -> expressionPrim' Prim_PAIR [] $ mkAnns [ta] [fa1, fa2] [va]
    UNPAIR va1 va2 fa1 fa2 -> expressionPrim' Prim_UNPAIR [] $
      mkAnns [] [fa1, fa2] [va1, va2]
    PAIRN va n -> expressionPrim' Prim_PAIR [integralToExpr n] $ mkAnns [] [] [va]
    UNPAIRN n -> expressionPrim' Prim_UNPAIR [integralToExpr n] []
    CAR va fa -> expressionPrim' Prim_CAR [] $ mkAnns [] [fa] [va]
    CDR va fa -> expressionPrim' Prim_CDR [] $ mkAnns [] [fa] [va]
    LEFT ta va fa1 fa2 ty -> expressionPrim' Prim_LEFT [toExpression ty] $
      mkAnns [ta] [fa1, fa2] [va]
    RIGHT ta va fa1 fa2 ty -> expressionPrim' Prim_RIGHT [toExpression ty] $
      mkAnns [ta] [fa1, fa2] [va]
    IF_LEFT ops1 ops2 ->
      expressionPrim' Prim_IF_LEFT [toExpression ops1, toExpression ops2] []
    NIL ta va ty -> expressionPrim' Prim_NIL [toExpression ty] $
      mkAnns [ta] [] [va]
    CONS va -> expressionPrim' Prim_CONS [] $ mkAnns [] [] [va]
    IF_CONS ops1 ops2 ->
      expressionPrim' Prim_IF_CONS [toExpression ops1, toExpression ops2] []
    SIZE va -> expressionPrim' Prim_SIZE [] $ mkAnns [] [] [va]
    EMPTY_SET ta va ty -> expressionPrim' Prim_EMPTY_SET [toExpression ty] $
      mkAnns [ta] [] [va]
    EMPTY_MAP ta va kty vty ->
      expressionPrim' Prim_EMPTY_MAP [toExpression kty, toExpression vty] $
      mkAnns [ta] [] [va]
    EMPTY_BIG_MAP ta va kty vty ->
      expressionPrim' Prim_EMPTY_BIG_MAP [toExpression kty, toExpression vty] $
      mkAnns [ta] [] [va]
    MAP va ops -> expressionPrim' Prim_MAP [toExpression ops] $ mkAnns [] [] [va]
    ITER ops -> expressionPrim' Prim_ITER [toExpression ops] []
    MEM va -> expressionPrim' Prim_MEM [] $ mkAnns [] [] [va]
    GET va -> expressionPrim' Prim_GET [] $ mkAnns [] [] [va]
    GETN va n -> expressionPrim' Prim_GET [integralToExpr n] $ mkAnns [] [] [va]
    UPDATE va -> expressionPrim' Prim_UPDATE [] $ mkAnns [] [] [va]
    UPDATEN va n -> expressionPrim' Prim_UPDATE [integralToExpr n] $ mkAnns [] [] [va]
    GET_AND_UPDATE va -> expressionPrim' Prim_GET_AND_UPDATE [] $ mkAnns [] [] [va]
    IF ops1 ops2 ->
      expressionPrim' Prim_IF [toExpression ops1, toExpression ops2] []
    LOOP ops -> expressionPrim' Prim_LOOP [toExpression ops] []
    LOOP_LEFT ops -> expressionPrim' Prim_LOOP_LEFT [toExpression ops] []
    LAMBDA va tyin tyout ops ->
      expressionPrim' Prim_LAMBDA [ toExpression tyin
                            , toExpression tyout
                            , toExpression ops
                            ] $ mkAnns [] [] [va]
    LAMBDA_REC va tyin tyout ops ->
      expressionPrim' Prim_LAMBDA_REC [ toExpression tyin
                            , toExpression tyout
                            , toExpression ops
                            ] $ mkAnns [] [] [va]
    EXEC va -> expressionPrim' Prim_EXEC [] $ mkAnns [] [] [va]
    APPLY va -> expressionPrim' Prim_APPLY [] $ mkAnns [] [] [va]
    DIP ops -> expressionPrim' Prim_DIP [toExpression ops] []
    DIPN n ops -> expressionPrim' Prim_DIP [integralToExpr n, toExpression ops] []
    FAILWITH -> expressionPrim' Prim_FAILWITH [] []
    CAST va ty -> expressionPrim' Prim_CAST [toExpression ty] $ mkAnns [] [] [va]
    RENAME va -> expressionPrim' Prim_RENAME [] $ mkAnns [] [] [va]
    PACK va -> expressionPrim' Prim_PACK [] $ mkAnns [] [] [va]
    UNPACK ta va ty -> expressionPrim' Prim_UNPACK [toExpression ty] $
      mkAnns [ta] [] [va]
    CONCAT va -> expressionPrim' Prim_CONCAT [] $ mkAnns [] [] [va]
    SLICE va -> expressionPrim' Prim_SLICE [] $ mkAnns [] [] [va]
    ISNAT va -> expressionPrim' Prim_ISNAT [] $ mkAnns [] [] [va]
    ADD va -> expressionPrim' Prim_ADD [] $ mkAnns [] [] [va]
    SUB va -> expressionPrim' Prim_SUB [] $ mkAnns [] [] [va]
    SUB_MUTEZ va -> expressionPrim' Prim_SUB_MUTEZ [] $ mkAnns [] [] [va]
    MUL va -> expressionPrim' Prim_MUL [] $ mkAnns [] [] [va]
    EDIV va -> expressionPrim' Prim_EDIV [] $ mkAnns [] [] [va]
    ABS va -> expressionPrim' Prim_ABS [] $ mkAnns [] [] [va]
    NEG va -> expressionPrim' Prim_NEG [] $ mkAnns [] [] [va]
    LSL va -> expressionPrim' Prim_LSL [] $ mkAnns [] [] [va]
    LSR va -> expressionPrim' Prim_LSR [] $ mkAnns [] [] [va]
    OR va -> expressionPrim' Prim_OR [] $ mkAnns [] [] [va]
    AND va -> expressionPrim' Prim_AND [] $ mkAnns [] [] [va]
    XOR va -> expressionPrim' Prim_XOR [] $ mkAnns [] [] [va]
    NOT va -> expressionPrim' Prim_NOT [] $ mkAnns [] [] [va]
    COMPARE va -> expressionPrim' Prim_COMPARE [] $ mkAnns [] [] [va]
    Untyped.EQ va -> expressionPrim' Prim_EQ [] $ mkAnns [] [] [va]
    NEQ va -> expressionPrim' Prim_NEQ [] $ mkAnns [] [] [va]
    Untyped.LT va -> expressionPrim' Prim_LT [] $ mkAnns [] [] [va]
    Untyped.GT va -> expressionPrim' Prim_GT [] $ mkAnns [] [] [va]
    LE va -> expressionPrim' Prim_LE [] $ mkAnns [] [] [va]
    GE va -> expressionPrim' Prim_GE [] $ mkAnns [] [] [va]
    INT va -> expressionPrim' Prim_INT [] $ mkAnns [] [] [va]
    NAT va -> expressionPrim' Prim_NAT [] $ mkAnns [] [] [va]
    BYTES va -> expressionPrim' Prim_BYTES [] $ mkAnns [] [] [va]
    VIEW va n t -> expressionPrim' Prim_VIEW [toExpression n, toExpression t] $
      mkAnns [] [] [va]
    SELF va fa -> expressionPrim' Prim_SELF [] $ mkAnns [] [fa] [va]
    CONTRACT va fa ty -> expressionPrim' Prim_CONTRACT [toExpression ty] $
      mkAnns [] [fa] [va]
    TRANSFER_TOKENS va -> expressionPrim' Prim_TRANSFER_TOKENS [] $ mkAnns [] [] [va]
    SET_DELEGATE va -> expressionPrim' Prim_SET_DELEGATE [] $ mkAnns [] [] [va]
    CREATE_CONTRACT va1 va2 c ->
      expressionPrim' Prim_CREATE_CONTRACT [toExpression c] $
      mkAnns [] [] [va1, va2]
    IMPLICIT_ACCOUNT va -> expressionPrim' Prim_IMPLICIT_ACCOUNT [] $
      mkAnns [] [] [va]
    NOW va -> expressionPrim' Prim_NOW [] $ mkAnns [] [] [va]
    AMOUNT va -> expressionPrim' Prim_AMOUNT [] $ mkAnns [] [] [va]
    BALANCE va -> expressionPrim' Prim_BALANCE [] $ mkAnns [] [] [va]
    VOTING_POWER va -> expressionPrim' Prim_VOTING_POWER [] $ mkAnns [] [] [va]
    TOTAL_VOTING_POWER va -> expressionPrim' Prim_TOTAL_VOTING_POWER [] $
      mkAnns [] [] [va]
    CHECK_SIGNATURE va -> expressionPrim' Prim_CHECK_SIGNATURE [] $ mkAnns [] [] [va]
    SHA256 va -> expressionPrim' Prim_SHA256 [] $ mkAnns [] [] [va]
    SHA512 va -> expressionPrim' Prim_SHA512 [] $ mkAnns [] [] [va]
    BLAKE2B va -> expressionPrim' Prim_BLAKE2B [] $ mkAnns [] [] [va]
    SHA3 va -> expressionPrim' Prim_SHA3 [] $ mkAnns [] [] [va]
    KECCAK va -> expressionPrim' Prim_KECCAK [] $ mkAnns [] [] [va]
    HASH_KEY va -> expressionPrim' Prim_HASH_KEY [] $ mkAnns [] [] [va]
    PAIRING_CHECK va -> expressionPrim' Prim_PAIRING_CHECK [] $ mkAnns [] [] [va]
    SOURCE va -> expressionPrim' Prim_SOURCE [] $ mkAnns [] [] [va]
    SENDER va -> expressionPrim' Prim_SENDER [] $ mkAnns [] [] [va]
    ADDRESS va -> expressionPrim' Prim_ADDRESS [] $ mkAnns [] [] [va]
    CHAIN_ID va -> expressionPrim' Prim_CHAIN_ID [] $ mkAnns [] [] [va]
    LEVEL va -> expressionPrim' Prim_LEVEL [] $ mkAnns [] [] [va]
    SELF_ADDRESS va -> expressionPrim' Prim_SELF_ADDRESS [] $ mkAnns [] [] [va]
    TICKET va -> expressionPrim' Prim_TICKET [] $ mkAnns [] [] [va]
    TICKET_DEPRECATED va -> expressionPrim' Prim_TICKET_DEPRECATED [] $ mkAnns [] [] [va]
    READ_TICKET va -> expressionPrim' Prim_READ_TICKET [] $ mkAnns [] [] [va]
    SPLIT_TICKET va -> expressionPrim' Prim_SPLIT_TICKET [] $ mkAnns [] [] [va]
    JOIN_TICKETS va -> expressionPrim' Prim_JOIN_TICKETS [] $ mkAnns [] [] [va]
    OPEN_CHEST va -> expressionPrim' Prim_OPEN_CHEST [] $ mkAnns [] [] [va]
    NEVER -> expressionPrim' Prim_NEVER [] []
    EXT _ -> expressionSeq []
    SAPLING_EMPTY_STATE va n -> expressionPrim' Prim_SAPLING_EMPTY_STATE [integralToExpr n] $ mkAnns [] [] [va]
    SAPLING_VERIFY_UPDATE va -> expressionPrim' Prim_SAPLING_VERIFY_UPDATE [] $ mkAnns [] [] [va]
    MIN_BLOCK_TIME va -> expressionPrim' Prim_MIN_BLOCK_TIME [] $ mkAnnsFromAny va
    EMIT va tag ty -> expressionPrim' Prim_EMIT (toExpression <$> maybeToList ty) $ mkAnns [] [tag] [va]

instance ToExpression Untyped.Contract where
  toExpression contract
    = expressionSeq $ Untyped.mapEntriesOrdered contract
          (\(Untyped.ParameterType ty rootAnn) -> expressionPrim' Prim_parameter
            [insertRootAnn (toExpression ty) rootAnn] [])
          (\storage -> expressionPrim' Prim_storage [toExpression storage] [])
          (\code -> expressionPrim' Prim_code [toExpression code] [])
          (\Untyped.View{..} -> expressionPrim' Prim_view
            [toExpression viewName, toExpression viewArgument, toExpression viewReturn, toExpression viewCode] []
          )

instance ToExpression (Contract cp st) where
  toExpression = toExpression . convertContractOptimized

-- FromExpression
----------------------------------------------------------------------------

-- | Errors that can happen when we convert an 'Exp' to our
-- data type.
data FromExpError x = FromExpError (Exp x) FromExpErrorReason

deriving stock instance Show (Exp x) => Show (FromExpError x)
deriving stock instance Eq (Exp x) => Eq (FromExpError x)

data FromExpErrorReason
  = FEERMTextDecodingFailure Text
  | FEERTcError T TcError
  | FEERNotEnoughArguments Word Int
  | FEERUnexpectedPrim (Maybe MichelinePrimitive) MichelinePrimitive
  | FEERUnexpectedPrimClass MichelinePrimitiveTag MichelinePrimitiveTag
  | FEERArgumentCountMismatch (NonEmpty Word) Int
  | FEERUnexpectedAnnotations
  | FEERExpectedPrim (NonEmpty MichelinePrimitiveTag)
  | FEERExpectedSeq
  | FEERUnsupported
  | FEERDeprecated
  | FEERTooManyAnns (Maybe Int, Maybe Int, Maybe Int) (Int, Int, Int)
  | FEEROutOfBounds
  | FEERExpectedNumber
  | FEERExpectedString
  | FEERViewNameError BadViewNameError
  | FEERBadContractBlocks (NonEmpty ContractBlockError)
  deriving stock (Show, Eq)

instance Buildable FromExpErrorReason where
  build = \case
    FEERMTextDecodingFailure msg -> nameF "Text decoding failure" $ build msg
    FEERTcError ty err -> unlinesF
      [ nameF "Failed to typecheck expression as a value of type" $ build ty
      , mempty
      , nameF "Typechecker error" $ build err
      ]
    FEERNotEnoughArguments minArgs numArgs ->
      "Expected at least" ++| minArgs |++ "arguments, but got" ++| numArgs |++ ""
    FEERUnexpectedPrim expected got ->
      nameF "Unexpected primitive" $ case expected of
        Nothing -> build got
        Just e -> build MkMismatchError { meExpected = e, meActual = got }
    FEERUnexpectedPrimClass expected got ->
      nameF "Unexpected primitive class" $ build $ MkMismatchError
        { meExpected = expected, meActual = got }
    FEERArgumentCountMismatch expected got ->
      fillSepF
        $ "Expected exactly"
        : punctuateF "," " or" expected <>
        [ "arguments, but got"
        , build got
        ]
    FEERUnexpectedAnnotations -> "Unexpected annotations"
    FEERExpectedPrim prims -> fillSepF
      $ "Expected primitive"
      : punctuateF "," " or" prims
    FEERExpectedSeq -> "Expected sequence"
    FEERTooManyAnns (maxTas, maxFas, maxVas) (tasCnt, fasCnt, vasCnt) -> unlinesF
      [ nameF "Expected at most" $ unlinesF $ catMaybes
          [ (<> " type annotations")    . build <$> maxTas
          , (<> " field annotations")   . build <$> maxFas
          , (<> " variable annotations") . build <$> maxVas
          ]
      , nameF "but found" $ unlinesF $ catMaybes
          [ (<> " type annotations")     . build <$> (maxTas $> tasCnt)
          , (<> " field annotations")    . build <$> (maxFas $> fasCnt)
          , (<> " variable annotations") . build <$> (maxVas $> vasCnt)
          ]
      ]
    FEEROutOfBounds -> "Value is out of bounds"
    FEERBadContractBlocks cbes -> unlinesF $ build <$> cbes
    FEERUnsupported -> "Unsupported"
    FEERDeprecated -> "Deprecated primitive"
    FEERExpectedNumber -> "Expected number"
    FEERExpectedString -> "Expected string"
    FEERViewNameError err -> nameF "View name error" $ build err

-- | Error in case of vanilla expression.
type FromExpressionError = FromExpError RegularExp

instance Buildable FromExpressionError where
  build (FromExpError expr err) =
    unlinesF
      [ "Failed to convert expression:"
      , indentF 2 $ build expr
      , ""
      , "Error:"
      , indentF 2 $ build err
      ]

instance Exception FromExpressionError where
  displayException = pretty

-- | Type class that provides the ability to convert
-- something from a Micheline Expression.
class FromExp x a where
  fromExp :: Exp x -> Either (FromExpError x) a

type FromExpression = FromExp RegularExp

-- | Parse vanilla expression to something.
fromExpression
  :: FromExp RegularExp a
  => Expression -> Either FromExpressionError a
fromExpression = fromExp

instance (FromExp x Untyped.Value, SingI t) => FromExp x (Value t) where
  fromExp expr =
    case fromExp @_ @Untyped.Value expr of
    Right uv -> case typeCheck uv of
      Left tcErr -> Left $ FromExpError expr $ FEERTcError (demote @t) tcErr
      Right tv -> Right tv
    Left e -> Left e
    where
      typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $
        typeCheckValue uv

instance FromExp x op => FromExp x (Untyped.Value' [] op) where
  fromExp e = case e of
    ExpInt _ v -> pure $ Untyped.ValueInt v
    ExpString _ s ->
      first (FromExpError e . FEERMTextDecodingFailure)
        (Untyped.ValueString <$> mkMText s)
    ExpBytes _ bs -> pure $ Untyped.ValueBytes $ Untyped.InternalByteString bs
    ExpPrim _ (MichelinePrimAp prim args _) -> withClassifiedPrim prim \case
      SMPTValue -> \case
        C_Prim_Unit -> withArgs Untyped.ValueUnit
        C_Prim_True -> withArgs Untyped.ValueTrue
        C_Prim_False -> withArgs Untyped.ValueFalse
        C_Prim_Pair ->
          case nonEmpty args >>= forbidSingletonList of
            Nothing -> Left $ FromExpError e $ FEERNotEnoughArguments 2 (length args)
            Just args' -> do
              tys <- mapM fromExp args'
              return $ foldr1 Untyped.ValuePair tys
        C_Prim_Left -> withArgs Untyped.ValueLeft
        C_Prim_Right -> withArgs Untyped.ValueRight
        C_Prim_Some -> withArgs Untyped.ValueSome
        C_Prim_None -> withArgs Untyped.ValueNone
        C_Prim_Lambda_rec -> withArgs Untyped.ValueLamRec
        C_Prim_Elt -> Left $ FromExpError e $ FEERUnexpectedPrim Nothing Prim_Elt
      s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTValue (fromSing s)
      where
        withArgs :: WithArgsRec x a r => a -> Either (FromExpError x) r
        withArgs = withArgsRec e args
    ExpSeq _ [] -> pure Untyped.ValueNil
    ExpSeq _ (h : t) ->
      case fromExp @x @op h of
      Right op -> do
        ops <- traverse (fromExp @x @op) t
        pure . Untyped.ValueLambda $ op : ops
      Left _ -> case exprToElt h of
        Right elt -> do
          elts <- traverse exprToElt t
          pure . Untyped.ValueMap $ elt :| elts
        Left _ -> case fromExp h of
          Left (FromExpError err _) -> Left $ FromExpError err $
            FEERExpectedPrim (MPTValue :| [MPTInstr])
          Right h' -> do
            t' <- traverse fromExp t
            pure . Untyped.ValueSeq $ h' :| t'
    ExpX _ -> Left $ FromExpError e $ FEERExpectedPrim (one MPTValue)
    where
      exprToElt :: Exp x -> Either (FromExpError x) (Untyped.Elt [] op)
      exprToElt ex = case ex of
        ExpPrim' _ Prim_Elt [l, r] [] -> do
          l' <- fromExp l
          r' <- fromExp r
          pure $ Untyped.Elt l' r'
        ExpPrim' _ Prim_Elt args' [] -> Left $ FromExpError ex $
          FEERArgumentCountMismatch (one 2) (length args')
        ExpPrim' _ Prim_Elt _ _ -> Left $ FromExpError ex FEERUnexpectedAnnotations
        ExpPrim' _ prim _ _ -> Left $ FromExpError ex $ FEERUnexpectedPrim (Just Prim_Elt) prim
        _ -> Left $ FromExpError ex $ FEERExpectedPrim $ one MPTValue

instance FromExp x a => FromExp x [a] where
  fromExp = \case
    ExpSeq _ exprs -> traverse fromExp exprs
    e -> Left $ FromExpError e FEERExpectedSeq

instance FromExp RegularExp ExpandedOp where
  fromExp = \case
    ExpSeq _ s -> SeqEx <$> traverse fromExp s
    e          -> PrimEx <$> fromExp e

instance FromExp x Word where
  fromExp = integralFromExpr

instance FromExp x Natural where
  fromExp = integralFromExpr

-- | Used to improve type inference with 'WithArgsRec'.
type family EndResult a where
  EndResult (_ -> b) = EndResult b
  EndResult b = b

-- | Recursive typeclass that unpacks a list of constructor arguments and
-- applies a function to them.
class (EndResult a ~ r, CountArgs a r) => WithArgsRec x a r where
  -- | Given the 'Exp' itself (used for error reporting), its arguments, and a
  -- function constructing the result form the arguments, produce the result or
  -- an error if the argument count is mismatched.
  withArgsRec' :: FromExpError x -> [Exp x] -> a -> Either (FromExpError x) r

instance (FromExp x a, WithArgsRec x b r) => WithArgsRec x (a -> b) r where
  withArgsRec' ee (e:es) f = fromExp @x e >>= withArgsRec' ee es . f
  withArgsRec' ee [] _ = Left ee

instance (EndResult r ~ r) => WithArgsRec x r r where
  withArgsRec' _ [] x = pure x
  withArgsRec' ee _ _ = Left ee

class CountArgs a r where countArgs :: Word
instance CountArgs r r where countArgs = 0
instance CountArgs b r => CountArgs (a -> b) r where countArgs = succ $ countArgs @b @r

withArgsRec
  :: forall x a r. WithArgsRec x a r
  => Exp x -> [Exp x] -> a -> Either (FromExpError x) r
withArgsRec e args = withArgsRec'
  (FromExpError e $ FEERArgumentCountMismatch (one $ countArgs @a @r) (length args))
  args

-- Note: On adding new expressions here, you must also add the symmetric (writing) case
-- to ToExpression as well.
instance FromExp x op =>
         FromExp x (InstrAbstract [] op) where
  fromExp e@(ExpPrim' _ prim args anns) = withClassifiedPrim prim \case
    SMPTInstr -> \case
      C_Prim_DROP -> nilAnns *> case args of
        [] -> pure DROP
        [n] -> DROPN <$> integralFromExpr n
        _ -> invalidNumArgs $ 0 :| [1]
      C_Prim_DUP -> annsCnt (0, 0, 1) *> case args of
        [n] -> DUPN va <$> integralFromExpr n
        [] -> pure $ DUP va
        _ -> invalidNumArgs $ 0 :| [1]
      C_Prim_SWAP -> withArgsAnns nil SWAP
      C_Prim_DIG -> withArgsAnns nil DIG
      C_Prim_DUG -> withArgsAnns nil DUG
      C_Prim_PUSH -> withArgsAnns (0, 0, 1) $ PUSH va
      C_Prim_SOME -> withArgsAnns (1, 0, 1) $ SOME ta va
      C_Prim_NONE -> withArgsAnns (1, 0, 1) $ NONE ta va
      C_Prim_UNIT -> withArgsAnns (1, 0, 1) $ UNIT ta va
      C_Prim_IF_NONE -> withArgsAnns nil IF_NONE
      C_Prim_PAIR -> case args of
        [] -> annsCnt (1, 2, 1) $> PAIR ta va fa1 fa2
        [n] -> annsCnt (0, 0, 1) $> PAIRN va <*> integralFromExpr n
        _ -> invalidNumArgs $ 0 :| [1]
      C_Prim_UNPAIR -> case args of
        [] -> annsCnt (0, 2, 2) $> UNPAIR va1 va2 fa1 fa2
        [n] -> nilAnns $> UNPAIRN <*> integralFromExpr n
        _ -> invalidNumArgs $ 0 :| [1]
      C_Prim_CAR -> withArgsAnns (0, 1, 1) $ CAR va fa
      C_Prim_CDR -> withArgsAnns (0, 1, 1) $ CDR va fa
      C_Prim_LEFT -> withArgsAnns (1, 2, 1) $ LEFT ta va fa1 fa2
      C_Prim_RIGHT -> withArgsAnns (1, 2, 1) $ RIGHT ta va fa1 fa2
      C_Prim_IF_LEFT -> withArgsAnns nil IF_LEFT
      C_Prim_NIL -> withArgsAnns (1, 0, 1) $ NIL ta va
      C_Prim_CONS -> mkInstrWithVarAnn CONS
      C_Prim_IF_CONS -> withArgsAnns nil IF_CONS
      C_Prim_SIZE -> mkInstrWithVarAnn SIZE
      C_Prim_EMPTY_SET -> withArgsAnns (1, 0, 1) $ EMPTY_SET ta va
      C_Prim_EMPTY_MAP -> withArgsAnns (1, 0, 1) $ EMPTY_MAP ta va
      C_Prim_EMPTY_BIG_MAP -> withArgsAnns (1, 0, 1) $ EMPTY_BIG_MAP ta va
      C_Prim_MAP -> withArgsAnns (0, 0, 1) $ MAP va
      C_Prim_ITER -> withArgsAnns nil ITER
      C_Prim_MEM -> mkInstrWithVarAnn MEM
      C_Prim_GET -> case args of
        [] -> mkInstrWithVarAnn GET
        [n] -> annsCnt (0, 0, 1) $> GETN va <*> integralFromExpr n
        _ -> invalidNumArgs $ 0 :| [1]
      C_Prim_UPDATE -> case args of
        [] -> mkInstrWithVarAnn UPDATE
        [n] -> annsCnt (0, 0, 1) $> UPDATEN va <*> integralFromExpr n
        _ -> invalidNumArgs $ 0 :| [1]
      C_Prim_GET_AND_UPDATE -> mkInstrWithVarAnn GET_AND_UPDATE
      C_Prim_IF -> withArgsAnns nil IF
      C_Prim_LOOP -> withArgsAnns nil LOOP
      C_Prim_LOOP_LEFT -> withArgsAnns nil LOOP_LEFT
      C_Prim_LAMBDA -> withArgsAnns (0, 0, 1) $ LAMBDA va
      C_Prim_LAMBDA_REC -> withArgsAnns (0, 0, 1) $ LAMBDA_REC va
      C_Prim_EXEC -> mkInstrWithVarAnn EXEC
      C_Prim_APPLY -> mkInstrWithVarAnn APPLY
      C_Prim_DIP -> nilAnns *> case args of
        [ops] -> DIP <$> fromExp ops
        [n, ops] -> DIPN <$> fromExp n <*> fromExp ops
        _ -> invalidNumArgs $ 1 :| [2]
      C_Prim_FAILWITH -> withArgsAnns nil FAILWITH
      C_Prim_CAST -> withArgsAnns (0, 0, 1) $ CAST va
      C_Prim_RENAME -> mkInstrWithVarAnn RENAME
      C_Prim_PACK -> mkInstrWithVarAnn PACK
      C_Prim_UNPACK -> withArgsAnns (1, 0, 1) $ UNPACK ta va
      C_Prim_CONCAT -> mkInstrWithVarAnn CONCAT
      C_Prim_SLICE -> mkInstrWithVarAnn SLICE
      C_Prim_ISNAT -> mkInstrWithVarAnn ISNAT
      C_Prim_ADD -> mkInstrWithVarAnn ADD
      C_Prim_SUB -> mkInstrWithVarAnn SUB
      C_Prim_SUB_MUTEZ -> mkInstrWithVarAnn SUB_MUTEZ
      C_Prim_MUL -> mkInstrWithVarAnn MUL
      C_Prim_EDIV -> mkInstrWithVarAnn EDIV
      C_Prim_ABS -> mkInstrWithVarAnn ABS
      C_Prim_NEG -> mkInstrWithVarAnn NEG
      C_Prim_LSL -> mkInstrWithVarAnn LSL
      C_Prim_LSR -> mkInstrWithVarAnn LSR
      C_Prim_OR -> mkInstrWithVarAnn OR
      C_Prim_AND -> mkInstrWithVarAnn AND
      C_Prim_XOR -> mkInstrWithVarAnn XOR
      C_Prim_NOT -> mkInstrWithVarAnn NOT
      C_Prim_COMPARE -> mkInstrWithVarAnn COMPARE
      C_Prim_EQ -> mkInstrWithVarAnn Untyped.EQ
      C_Prim_NEQ -> mkInstrWithVarAnn NEQ
      C_Prim_LT -> mkInstrWithVarAnn Untyped.LT
      C_Prim_GT -> mkInstrWithVarAnn Untyped.GT
      C_Prim_LE -> mkInstrWithVarAnn LE
      C_Prim_GE -> mkInstrWithVarAnn GE
      C_Prim_INT -> mkInstrWithVarAnn INT
      C_Prim_NAT -> mkInstrWithVarAnn NAT
      C_Prim_BYTES -> mkInstrWithVarAnn BYTES
      C_Prim_VIEW -> withArgsAnns (0, 0, 1) $ VIEW va
      C_Prim_SELF -> withArgsAnns (0, 1, 1) $ SELF va fa
      C_Prim_CONTRACT -> withArgsAnns (0, 1, 1) $ CONTRACT va fa
      C_Prim_TRANSFER_TOKENS -> mkInstrWithVarAnn TRANSFER_TOKENS
      C_Prim_SET_DELEGATE -> mkInstrWithVarAnn SET_DELEGATE
      C_Prim_CREATE_CONTRACT -> withArgsAnns (0, 0, 2) $ CREATE_CONTRACT va1 va2
      C_Prim_IMPLICIT_ACCOUNT -> mkInstrWithVarAnn IMPLICIT_ACCOUNT
      C_Prim_NOW -> mkInstrWithVarAnn NOW
      C_Prim_AMOUNT -> mkInstrWithVarAnn AMOUNT
      C_Prim_BALANCE -> mkInstrWithVarAnn BALANCE
      C_Prim_VOTING_POWER -> mkInstrWithVarAnn VOTING_POWER
      C_Prim_TOTAL_VOTING_POWER -> mkInstrWithVarAnn TOTAL_VOTING_POWER
      C_Prim_CHECK_SIGNATURE -> mkInstrWithVarAnn CHECK_SIGNATURE
      C_Prim_SHA256 -> mkInstrWithVarAnn SHA256
      C_Prim_SHA512 -> mkInstrWithVarAnn SHA512
      C_Prim_BLAKE2B -> mkInstrWithVarAnn BLAKE2B
      C_Prim_SHA3 -> mkInstrWithVarAnn SHA3
      C_Prim_KECCAK -> mkInstrWithVarAnn KECCAK
      C_Prim_HASH_KEY -> mkInstrWithVarAnn HASH_KEY
      C_Prim_PAIRING_CHECK -> mkInstrWithVarAnn PAIRING_CHECK
      C_Prim_SOURCE -> mkInstrWithVarAnn SOURCE
      C_Prim_SENDER -> mkInstrWithVarAnn SENDER
      C_Prim_ADDRESS -> mkInstrWithVarAnn ADDRESS
      C_Prim_CHAIN_ID -> mkInstrWithVarAnn CHAIN_ID
      C_Prim_LEVEL -> mkInstrWithVarAnn LEVEL
      C_Prim_SELF_ADDRESS -> mkInstrWithVarAnn SELF_ADDRESS
      C_Prim_NEVER -> withArgsAnns nil NEVER
      C_Prim_TICKET_DEPRECATED -> mkInstrWithVarAnn TICKET_DEPRECATED
      C_Prim_TICKET -> mkInstrWithVarAnn TICKET
      C_Prim_READ_TICKET -> mkInstrWithVarAnn READ_TICKET
      C_Prim_SPLIT_TICKET -> mkInstrWithVarAnn SPLIT_TICKET
      C_Prim_JOIN_TICKETS -> mkInstrWithVarAnn JOIN_TICKETS
      C_Prim_OPEN_CHEST -> mkInstrWithVarAnn OPEN_CHEST
      C_Prim_SAPLING_EMPTY_STATE -> withArgsAnns (0, 0, 1) $ SAPLING_EMPTY_STATE va
      C_Prim_SAPLING_VERIFY_UPDATE -> mkInstrWithVarAnn SAPLING_VERIFY_UPDATE
      C_Prim_MIN_BLOCK_TIME -> withArgsRec e args $ mkInstrWithAnyAnns MIN_BLOCK_TIME
      C_Prim_EMIT -> annsCnt (0, 1, 1) $> EMIT va fa <*> case args of
        [] -> pure Nothing
        [ty] -> Just <$> fromExp ty
        _ -> invalidNumArgs (0 :| [1])
    s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTInstr (fromSing s)

    where
      annSet = toAnnSet anns
      va = firstAnn @VarTag annSet
      ta = firstAnn @TypeTag annSet
      fa = firstAnn @FieldTag annSet
      fa1 = fa
      fa2 = secondAnn @FieldTag annSet
      va1 = va
      va2 = secondAnn @VarTag annSet

      withArgsAnns
        :: WithArgsRec x a (InstrAbstract [] op)
        => (Int, Int, Int) -> a -> Either (FromExpError x) (InstrAbstract [] op)
      withArgsAnns n f = annsCnt n *> withArgsRec e args f

      invalidNumArgs :: NonEmpty Word -> Either (FromExpError x) b
      invalidNumArgs expected = Left $ FromExpError e $
        FEERArgumentCountMismatch expected (length args)

      annsCnt = checkAnnsCount e annSet

      nil = (0, 0, 0)

      nilAnns = annsCnt nil

      mkInstrWithVarAnn
        :: WithArgsRec x a (InstrAbstract [] op)
        => (Untyped.Annotation VarTag -> a)
        -> Either (FromExpError x) (InstrAbstract [] op)
      mkInstrWithVarAnn ctor = withArgsAnns (0, 0, 1) $ ctor va

      mkInstrWithAnyAnns :: ([Untyped.AnyAnn] -> t) -> t
      mkInstrWithAnyAnns ctor = ctor $ anns <&> \case
        AnnotationType x -> Untyped.AnyAnnType x
        AnnotationField x -> Untyped.AnyAnnField x
        AnnotationVariable x -> Untyped.AnyAnnVar x

  fromExp e = Left $ FromExpError e $ FEERExpectedPrim (one MPTInstr)

instance (FromExp x op) => FromExp x (Untyped.Contract' op) where
  fromExp blocks = case blocks of
    ExpSeq _ bs -> do
      bs' <- mapM exprToCB bs
      first (FromExpError blocks . FEERBadContractBlocks) $ orderContractBlock bs'
    expr -> Left $ FromExpError expr FEERExpectedSeq
    where
      exprToCB
        :: Exp x
        -> Either (FromExpError x) (ContractBlock op)
      exprToCB e@(ExpPrim' _ prim args anns) = withClassifiedPrim prim \case
        SMPTKeyword -> \case
          C_Prim_parameter -> mkCbParam e args anns
          C_Prim_storage   -> mkCBStorage e args anns
          C_Prim_code      -> mkCBCode e args anns
          C_Prim_view      -> mkCBView e args anns
        s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTKeyword (fromSing s)
      exprToCB e = Left $ FromExpError e $ FEERExpectedPrim $ one MPTKeyword

      mkCbParam
        :: Exp x
        -> [Exp x]
        -> [Annotation]
        -> Either (FromExpError x) (ContractBlock op)
      mkCbParam e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *> case args of
        [p] -> do
          let annSet = toAnnSet (p ^. _ExpPrim . _2 . mpaAnnotsL)
              annCnt = annsCount annSet
          let rootAnn = firstAnn @FieldTag annSet
          unless (secondAnn @FieldTag annSet == noAnn) $
            Left $ FromExpError p $ FEERTooManyAnns (Nothing, Just 1, Nothing) annCnt
          p' <- fromExp @x @Ty
            (p & _ExpPrim . _2 . mpaAnnotsL %~ filter (not . isAnnotationField))
          pure $ CBParam $ Untyped.ParameterType p' rootAnn
        _ -> Left $ FromExpError e $ FEERArgumentCountMismatch (one 1) (length args)

      mkCBStorage
        :: Exp x
        -> [Exp x]
        -> [Annotation]
        -> Either (FromExpError x) (ContractBlock op)
      mkCBStorage e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *>
        withArgsRec e args CBStorage

      mkCBCode
        :: Exp x
        -> [Exp x]
        -> [Annotation]
        -> Either (FromExpError x) (ContractBlock op)
      mkCBCode e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *>
        withArgsRec e args CBCode

      mkCBView
        :: Exp x
        -> [Exp x]
        -> [Annotation]
        -> Either (FromExpError x) (ContractBlock op)
      mkCBView e args anns = checkAnnsCount e (toAnnSet anns) (0, 0, 0) *>
        withArgsRec e args (CBView ... Untyped.View)

instance FromExp x Untyped.T where
  fromExp e@(ExpPrim' _ prim args anns) = assertNoAnns *> withClassifiedPrim prim \case
    SMPTType -> \case
      C_Prim_key -> withArgs Untyped.TKey
      C_Prim_unit -> withArgs Untyped.TUnit
      C_Prim_signature -> withArgs Untyped.TSignature
      C_Prim_chain_id -> withArgs Untyped.TChainId
      C_Prim_option -> withArgs Untyped.TOption
      C_Prim_list -> withArgs Untyped.TList
      C_Prim_set -> withArgs Untyped.TSet
      C_Prim_operation -> withArgs Untyped.TOperation
      C_Prim_contract -> withArgs Untyped.TContract
      C_Prim_ticket -> withArgs Untyped.TTicket
      C_Prim_or
        | [arg1, arg2] <- args -> do
            let as1 = toAnnSet $ arg1 ^. _ExpPrim . _2 . mpaAnnotsL
            let as2 = toAnnSet $ arg2 ^. _ExpPrim . _2 . mpaAnnotsL
            checkAnnsCount e as1 (1, 1, 0)
            checkAnnsCount e as2 (1, 1, 0)
            let fa1 = firstAnn @FieldTag as1
            let fa2 = firstAnn @FieldTag as2
            l <- fromExp $ removeAnns arg1 isAnnotationField
            r <- fromExp $ removeAnns arg2 isAnnotationField
            pure $ Untyped.TOr fa1 fa2 l r
        | otherwise -> Left $ FromExpError e $
            FEERArgumentCountMismatch (one 2) (length args)
      C_Prim_pair -> do
        args2 <- case nonEmpty args >>= forbidSingletonList of
          Nothing -> Left $ FromExpError e $ FEERNotEnoughArguments 2 (length args)
          Just as -> pure as
        -- Check and extract annotations info
        tyInfos <- forM args2 \arg -> do
          let as = toAnnSet $ arg ^. _ExpPrim . _2 . mpaAnnotsL
          checkAnnsCount e as (1, 1, 1)
          let fa = firstAnn @FieldTag as
          let va = firstAnn @VarTag as
          ty <- fromExp $ removeAnns arg
            (isAnnotationField || isAnnotationVariable)
          return (ty, fa, va)
        -- Make a right-comb pairs tree
        let combiner (ty1, fa1, va1) (ty2, fa2, va2) =
              ( Ty (Untyped.TPair fa1 fa2 va1 va2 ty1 ty2) noAnn
              , noAnn
              , noAnn
              )
        let (Ty tRes _, _, _) = foldr1 combiner tyInfos
        return tRes
      C_Prim_lambda -> withArgs Untyped.TLambda
      C_Prim_map -> withArgs Untyped.TMap
      C_Prim_big_map -> withArgs Untyped.TBigMap
      C_Prim_int -> withArgs Untyped.TInt
      C_Prim_nat -> withArgs Untyped.TNat
      C_Prim_string -> withArgs Untyped.TString
      C_Prim_bytes -> withArgs Untyped.TBytes
      C_Prim_mutez -> withArgs Untyped.TMutez
      C_Prim_bool -> withArgs Untyped.TBool
      C_Prim_key_hash -> withArgs Untyped.TKeyHash
      C_Prim_bls12_381_fr -> withArgs Untyped.TBls12381Fr
      C_Prim_bls12_381_g1 -> withArgs Untyped.TBls12381G1
      C_Prim_bls12_381_g2 -> withArgs Untyped.TBls12381G2
      C_Prim_timestamp -> withArgs Untyped.TTimestamp
      C_Prim_address -> withArgs Untyped.TAddress
      C_Prim_chest -> withArgs Untyped.TChest
      C_Prim_chest_key -> withArgs Untyped.TChestKey
      C_Prim_tx_rollup_l2_address ->
        Left $ FromExpError e FEERUnsupported
      C_Prim_never -> withArgs Untyped.TNever
      C_Prim_sapling_state -> withArgs Untyped.TSaplingState
      C_Prim_sapling_transaction -> withArgs Untyped.TSaplingTransaction
      C_Prim_sapling_transaction_deprecated ->
        Left $ FromExpError e FEERDeprecated
    s -> const $ Left $ FromExpError e $ FEERUnexpectedPrimClass MPTType (fromSing s)
    where
      assertNoAnns = unless (null anns) $ Left $ FromExpError e FEERUnexpectedAnnotations
      withArgs :: WithArgsRec x a Untyped.T => a -> Either (FromExpError x) Untyped.T
      withArgs = withArgsRec e args

      removeAnns :: Exp x -> (Annotation -> Bool) -> Exp x
      removeAnns expr p =
        expr & _ExpPrim . _2 . mpaAnnotsL %~ filter (not . p)
  fromExp e = Left $ FromExpError e $ FEERExpectedPrim $ one MPTType

instance FromExp x Ty where
  fromExp e = case e of
    ExpPrim' ex primName args anns -> do
      let annSet = toAnnSet anns
          annCnt = annsCount annSet
      let ta = firstAnn @TypeTag annSet
      when (secondAnn @TypeTag annSet /= noAnn) $
        Left $ FromExpError e $ FEERTooManyAnns (Just 1, Nothing, Nothing) annCnt
      t <- fromExp @x @Untyped.T $ ExpPrim' ex primName args $ filter
        (not . isAnnotationType) anns
      pure $ Ty t ta
    _ -> Left $ FromExpError e $ FEERExpectedPrim (one MPTType)

instance FromExp x T where
  fromExp =
    second fromUType . fromExp @x @Untyped.Ty

-- Note: we should generalize this to work for any instruction,
-- not just lambdas (i.e. instructions with one input and one output).
instance (SingI inp, SingI out) => FromExp RegularExp (Instr '[inp] '[out]) where
  fromExp expr =
    fromExpression @(Value ('TLambda inp out)) expr >>= \case
      VLam (LambdaCode instr) -> pure $ rfAnyInstr instr
      VLam LambdaCodeRec{} -> Left $ FromExpError expr $
        FEERUnexpectedPrim Nothing Prim_Lambda_rec

instance FromExp x ViewName where
  fromExp e = case e of
    ExpString _ s ->
      first (FromExpError e . FEERViewNameError) $ mkViewName s
    _ -> Left $ FromExpError e FEERExpectedString

----------------------------------------------------------------------------
-- Helpers
----------------------------------------------------------------------------

-- | Adds annotations to the expression, after removing empty annotations
-- at the end of each list.
addTrimmedAnns
  :: Exp x
  -> [TypeAnn]
  -> [FieldAnn]
  -> [VarAnn]
  -> Exp x
addTrimmedAnns e tas fas vas =
  e & _ExpPrim . _2 . mpaAnnotsL <>~ mkAnns tas fas vas

-- | Inserts the root annotation into the contract parameter.
insertRootAnn :: HasCallStack => Expression -> RootAnn -> Expression
insertRootAnn expr rootAnn = case expr of
  ExpPrim () p
    -- The order of annotations is important iff there are
    -- multiple annotations of the same kind or there are
    -- other kinds of annotations in the list.
    -- Prepending root field annotation is okay because
    -- there can not be more than one root annotation.
    | rootAnn /= noAnn -> expressionPrim p
      { mpaAnnots = AnnotationField rootAnn : mpaAnnots p
      }
    | otherwise -> expr
  -- Currently this error can't happen because parameter type
  -- must be a Micheline primitive. If it ever changes, we
  -- would like to notice it ASAP and update this place.
  _ -> error $ "parameter is not a primitive: " <> pretty expr

-- | Checks for a given expression that the number of annotations
-- of each type in it doesn't exceed the specified threshold.
checkAnnsCount
  :: Exp x
  -> AnnotationSet
  -> (Int, Int, Int)
  -> Either (FromExpError x) ()
checkAnnsCount e annSet maxCount@(maxTas, maxFas, maxVas) = do
  let actualCount = annsCount annSet
  unless (actualCount <= maxCount) $
    Left $ FromExpError e $ FEERTooManyAnns (Just maxTas, Just maxFas, Just maxVas) actualCount

forbidSingletonList :: NonEmpty a -> Maybe (NonEmpty a)
forbidSingletonList = \case
  _ :| [] -> Nothing
  x       -> Just x

integralToExpr :: Integral i => i -> Expression
integralToExpr = expressionInt . toInteger

integralFromExpr :: (Integral i, Bits i) => Exp x -> Either (FromExpError x) i
integralFromExpr e = case e of
  ExpInt _ v ->
    maybeToRight (FromExpError e FEEROutOfBounds)
      (fromIntegralMaybe @Integer v)
  _ -> Left $ FromExpError e FEERExpectedNumber