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

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

import Control.Lens ((<>~))
import Data.Bits (toIntegralSized)
import Data.Default
import Data.Singletons (SingI(..), demote)
import Fmt (Buildable(..), indentF, pretty, unlinesF)

import Morley.Micheline.Expression
  (Annotation(..), Expression(..), MichelinePrimAp(..), _ExpressionPrim, isAnnotationField,
  isAnnotationType, isAnnotationVariable, mkAnns, mpaAnnotsL, toAnnSet)
import Morley.Michelson.Text (mkMText, unMText)
import Morley.Michelson.TypeCheck
  (TypeCheckMode(..), TypeCheckOptions(..), runTypeCheck, typeCheckingWith)
import Morley.Michelson.TypeCheck.Instr (typeCheckValue)
import Morley.Michelson.Typed
  (Contract(..), HasNoOp, Instr, Notes(..), T(..), Value, Value'(..), fromUType, mkUType,
  rfAnyInstr, toUType)
import Morley.Michelson.Typed.Convert (convertContract, instrToOpsOptimized, untypeValueOptimized)
import qualified Morley.Michelson.Untyped as Untyped
import Morley.Michelson.Untyped.Annotation
  (AnnotationSet(..), FieldAnn, FieldTag, RootAnn, TypeAnn, TypeTag, VarAnn, VarTag, annsCount,
  emptyAnnSet, firstAnn, noAnn, secondAnn)
import Morley.Michelson.Untyped.Contract (ContractBlock(..), orderContractBlock)
import Morley.Michelson.Untyped.Instr (ExpandedInstr, ExpandedOp(..), InstrAbstract(..))
import Morley.Michelson.Untyped.Type (Ty(..))

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

instance (HasNoOp 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 -> PrimExpr "Unit" [] []
    Untyped.ValueTrue -> PrimExpr "True" [] []
    Untyped.ValueFalse -> PrimExpr "False" [] []
    Untyped.ValuePair l r ->
      PrimExpr "Pair" [toExpression l, toExpression r] []
    Untyped.ValueLeft v -> PrimExpr "Left" [toExpression v] []
    Untyped.ValueRight v -> PrimExpr "Right" [toExpression v] []
    Untyped.ValueSome v -> PrimExpr "Some" [toExpression v] []
    Untyped.ValueNone -> PrimExpr "None" [] []
    Untyped.ValueNil -> ExpressionSeq []
    Untyped.ValueSeq vs -> toExpression vs
    Untyped.ValueMap elts -> toExpression $ eltToExpr <$> elts
    Untyped.ValueLambda ops -> toExpression ops
    where
      eltToExpr :: Untyped.Elt ExpandedOp -> Expression
      eltToExpr (Untyped.Elt l r) = PrimExpr "Elt"
        [toExpression l, toExpression r] []


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

instance ToExpression T where
  toExpression = toExpression . toUType

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

instance ToExpression Untyped.T where
  toExpression = \case
    Untyped.TKey -> PrimExpr "key" [] []
    Untyped.TUnit -> PrimExpr "unit" [] []
    Untyped.TSignature -> PrimExpr "signature" [] []
    Untyped.TChainId -> PrimExpr "chain_id" [] []
    Untyped.TOption arg -> PrimExpr "option" [toExpression arg] []
    Untyped.TList arg -> PrimExpr "list" [toExpression arg] []
    Untyped.TSet arg -> PrimExpr "set" [toExpression arg] []
    Untyped.TOperation -> PrimExpr "operation" [] []
    Untyped.TContract arg -> PrimExpr "contract" [toExpression arg] []
    Untyped.TTicket arg -> PrimExpr "ticket" [toExpression arg] []
    t@Untyped.TPair{} -> PrimExpr "pair"
      (rightCombedPairToList (Ty t noAnn) (noAnn, noAnn)) []
    Untyped.TOr fa1 fa2 l r ->
      let exprL = addTrimmedAnns (toExpression l) [] [fa1] []
          exprR = addTrimmedAnns (toExpression r) [] [fa2] []
      in PrimExpr "or" [exprL, exprR] []
    Untyped.TLambda inp out ->
      PrimExpr "lambda" [toExpression inp, toExpression out] []
    Untyped.TMap k v ->
      PrimExpr "map" [toExpression k, toExpression v] []
    Untyped.TBigMap k v ->
      PrimExpr "big_map" [toExpression k, toExpression v] []
    Untyped.TInt -> PrimExpr "int" [] []
    Untyped.TNat -> PrimExpr "nat" [] []
    Untyped.TString -> PrimExpr "string" [] []
    Untyped.TBytes -> PrimExpr "bytes" [] []
    Untyped.TMutez -> PrimExpr "mutez" [] []
    Untyped.TBool -> PrimExpr "bool" [] []
    Untyped.TKeyHash -> PrimExpr "key_hash" [] []
    Untyped.TBls12381Fr -> PrimExpr "bls12_381_fr" [] []
    Untyped.TBls12381G1 -> PrimExpr "bls12_381_g1" [] []
    Untyped.TBls12381G2 -> PrimExpr "bls12_381_g2" [] []
    Untyped.TTimestamp -> PrimExpr "timestamp" [] []
    Untyped.TAddress -> PrimExpr "address" [] []
    Untyped.TNever -> PrimExpr "never" [] []

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

      rightCombedPairToList :: Ty -> (FieldAnn, VarAnn) -> [Expression]
      rightCombedPairToList ty (fa, va) = case (ty, fa) of
        (Ty (Untyped.TPair fa1 fa2 va1 va2 l r) (Untyped.Annotation ""), Untyped.Annotation "") ->
          let annsL = mkAnns [] [fa1] [va1]
              exprL = toExpression l `addAnns` annsL
          in exprL : (rightCombedPairToList r (fa2, va2))
        _ ->
          let anns = mkAnns [] [fa] [va]
          in one $ toExpression ty `addAnns` anns

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 ExpandedInstr where
  toExpression = \case
    PUSH va ty v -> PrimExpr "PUSH" [toExpression ty, toExpression v] $
      mkAnns [] [] [va]
    DROP -> PrimExpr "DROP" [] []
    DROPN n -> PrimExpr "DROP" [wordToExpr n] []
    DUP va -> PrimExpr "DUP" [] $ mkAnns [] [] [va]
    DUPN va n -> PrimExpr "DUP" [wordToExpr n] $ mkAnns [] [] [va]
    SWAP -> PrimExpr "SWAP" [] []
    DIG n -> PrimExpr "DIG" [wordToExpr n] []
    DUG n -> PrimExpr "DUG" [wordToExpr n] []
    SOME ta va ->
      PrimExpr "SOME" [] $ mkAnns [ta] [] [va]
    NONE ta va ty -> PrimExpr "NONE" [toExpression ty] $ mkAnns [ta] [] [va]
    UNIT ta va -> PrimExpr "UNIT" [] $ mkAnns [ta] [] [va]
    IF_NONE ops1 ops2 ->
      PrimExpr "IF_NONE" [toExpression ops1, toExpression ops2] []
    PAIR ta va fa1 fa2 -> PrimExpr "PAIR" [] $ mkAnns [ta] [fa1, fa2] [va]
    UNPAIR va1 va2 fa1 fa2 -> PrimExpr "UNPAIR" [] $
      mkAnns [] [fa1, fa2] [va1, va2]
    PAIRN va n -> PrimExpr "PAIR" [wordToExpr n] $ mkAnns [] [] [va]
    UNPAIRN n -> PrimExpr "UNPAIR" [wordToExpr n] []
    CAR va fa -> PrimExpr "CAR" [] $ mkAnns [] [fa] [va]
    CDR va fa -> PrimExpr "CDR" [] $ mkAnns [] [fa] [va]
    LEFT ta va fa1 fa2 ty -> PrimExpr "LEFT" [toExpression ty] $
      mkAnns [ta] [fa1, fa2] [va]
    RIGHT ta va fa1 fa2 ty -> PrimExpr "RIGHT" [toExpression ty] $
      mkAnns [ta] [fa1, fa2] [va]
    IF_LEFT ops1 ops2 ->
      PrimExpr "IF_LEFT" [toExpression ops1, toExpression ops2] []
    NIL ta va ty -> PrimExpr "NIL" [toExpression ty] $
      mkAnns [ta] [] [va]
    CONS va -> PrimExpr "CONS" [] $ mkAnns [] [] [va]
    IF_CONS ops1 ops2 ->
      PrimExpr "IF_CONS" [toExpression ops1, toExpression ops2] []
    SIZE va -> PrimExpr "SIZE" [] $ mkAnns [] [] [va]
    EMPTY_SET ta va ty -> PrimExpr "EMPTY_SET" [toExpression ty] $
      mkAnns [ta] [] [va]
    EMPTY_MAP ta va kty vty ->
      PrimExpr "EMPTY_MAP" [toExpression kty, toExpression vty] $
      mkAnns [ta] [] [va]
    EMPTY_BIG_MAP ta va kty vty ->
      PrimExpr "EMPTY_BIG_MAP" [toExpression kty, toExpression vty] $
      mkAnns [ta] [] [va]
    MAP va ops -> PrimExpr "MAP" [toExpression ops] $ mkAnns [] [] [va]
    ITER ops -> PrimExpr "ITER" [toExpression ops] []
    MEM va -> PrimExpr "MEM" [] $ mkAnns [] [] [va]
    GET va -> PrimExpr "GET" [] $ mkAnns [] [] [va]
    GETN va n -> PrimExpr "GET" [wordToExpr n] $ mkAnns [] [] [va]
    UPDATE va -> PrimExpr "UPDATE" [] $ mkAnns [] [] [va]
    UPDATEN va n -> PrimExpr "UPDATE" [wordToExpr n] $ mkAnns [] [] [va]
    GET_AND_UPDATE va -> PrimExpr "GET_AND_UPDATE" [] $ mkAnns [] [] [va]
    IF ops1 ops2 ->
      PrimExpr "IF" [toExpression ops1, toExpression ops2] []
    LOOP ops -> PrimExpr "LOOP" [toExpression ops] []
    LOOP_LEFT ops -> PrimExpr "LOOP_LEFT" [toExpression ops] []
    LAMBDA va tyin tyout ops ->
      PrimExpr "LAMBDA" [ toExpression tyin
                            , toExpression tyout
                            , toExpression ops
                            ] $ mkAnns [] [] [va]
    EXEC va -> PrimExpr "EXEC" [] $ mkAnns [] [] [va]
    APPLY va -> PrimExpr "APPLY" [] $ mkAnns [] [] [va]
    DIP ops -> PrimExpr "DIP" [toExpression ops] []
    DIPN n ops -> PrimExpr "DIP" [wordToExpr n, toExpression ops] []
    FAILWITH -> PrimExpr "FAILWITH" [] []
    CAST va ty -> PrimExpr "CAST" [toExpression ty] $ mkAnns [] [] [va]
    RENAME va -> PrimExpr "RENAME" [] $ mkAnns [] [] [va]
    PACK va -> PrimExpr "PACK" [] $ mkAnns [] [] [va]
    UNPACK ta va ty -> PrimExpr "UNPACK" [toExpression ty] $
      mkAnns [ta] [] [va]
    CONCAT va -> PrimExpr "CONCAT" [] $ mkAnns [] [] [va]
    SLICE va -> PrimExpr "SLICE" [] $ mkAnns [] [] [va]
    ISNAT va -> PrimExpr "ISNAT" [] $ mkAnns [] [] [va]
    ADD va -> PrimExpr "ADD" [] $ mkAnns [] [] [va]
    SUB va -> PrimExpr "SUB" [] $ mkAnns [] [] [va]
    MUL va -> PrimExpr "MUL" [] $ mkAnns [] [] [va]
    EDIV va -> PrimExpr "EDIV" [] $ mkAnns [] [] [va]
    ABS va -> PrimExpr "ABS" [] $ mkAnns [] [] [va]
    NEG va -> PrimExpr "NEG" [] $ mkAnns [] [] [va]
    LSL va -> PrimExpr "LSL" [] $ mkAnns [] [] [va]
    LSR va -> PrimExpr "LSR" [] $ mkAnns [] [] [va]
    OR va -> PrimExpr "OR" [] $ mkAnns [] [] [va]
    AND va -> PrimExpr "AND" [] $ mkAnns [] [] [va]
    XOR va -> PrimExpr "XOR" [] $ mkAnns [] [] [va]
    NOT va -> PrimExpr "NOT" [] $ mkAnns [] [] [va]
    COMPARE va -> PrimExpr "COMPARE" [] $ mkAnns [] [] [va]
    Untyped.EQ va -> PrimExpr "EQ" [] $ mkAnns [] [] [va]
    NEQ va -> PrimExpr "NEQ" [] $ mkAnns [] [] [va]
    Untyped.LT va -> PrimExpr "LT" [] $ mkAnns [] [] [va]
    Untyped.GT va -> PrimExpr "GT" [] $ mkAnns [] [] [va]
    LE va -> PrimExpr "LE" [] $ mkAnns [] [] [va]
    GE va -> PrimExpr "GE" [] $ mkAnns [] [] [va]
    INT va -> PrimExpr "INT" [] $ mkAnns [] [] [va]
    SELF va fa -> PrimExpr "SELF" [] $ mkAnns [] [fa] [va]
    CONTRACT va fa ty -> PrimExpr "CONTRACT" [toExpression ty] $
      mkAnns [] [fa] [va]
    TRANSFER_TOKENS va -> PrimExpr "TRANSFER_TOKENS" [] $ mkAnns [] [] [va]
    SET_DELEGATE va -> PrimExpr "SET_DELEGATE" [] $ mkAnns [] [] [va]
    CREATE_CONTRACT va1 va2 c ->
      PrimExpr "CREATE_CONTRACT" [toExpression c] $
      mkAnns [] [] [va1, va2]
    IMPLICIT_ACCOUNT va -> PrimExpr "IMPLICIT_ACCOUNT" [] $
      mkAnns [] [] [va]
    NOW va -> PrimExpr "NOW" [] $ mkAnns [] [] [va]
    AMOUNT va -> PrimExpr "AMOUNT" [] $ mkAnns [] [] [va]
    BALANCE va -> PrimExpr "BALANCE" [] $ mkAnns [] [] [va]
    VOTING_POWER va -> PrimExpr "VOTING_POWER" [] $ mkAnns [] [] [va]
    TOTAL_VOTING_POWER va -> PrimExpr "TOTAL_VOTING_POWER" [] $
      mkAnns [] [] [va]
    CHECK_SIGNATURE va -> PrimExpr "CHECK_SIGNATURE" [] $ mkAnns [] [] [va]
    SHA256 va -> PrimExpr "SHA256" [] $ mkAnns [] [] [va]
    SHA512 va -> PrimExpr "SHA512" [] $ mkAnns [] [] [va]
    BLAKE2B va -> PrimExpr "BLAKE2B" [] $ mkAnns [] [] [va]
    SHA3 va -> PrimExpr "SHA3" [] $ mkAnns [] [] [va]
    KECCAK va -> PrimExpr "KECCAK" [] $ mkAnns [] [] [va]
    HASH_KEY va -> PrimExpr "HASH_KEY" [] $ mkAnns [] [] [va]
    PAIRING_CHECK va -> PrimExpr "PAIRING_CHECK" [] $ mkAnns [] [] [va]
    SOURCE va -> PrimExpr "SOURCE" [] $ mkAnns [] [] [va]
    SENDER va -> PrimExpr "SENDER" [] $ mkAnns [] [] [va]
    ADDRESS va -> PrimExpr "ADDRESS" [] $ mkAnns [] [] [va]
    CHAIN_ID va -> PrimExpr "CHAIN_ID" [] $ mkAnns [] [] [va]
    LEVEL va -> PrimExpr "LEVEL" [] $ mkAnns [] [] [va]
    SELF_ADDRESS va -> PrimExpr "SELF_ADDRESS" [] $ mkAnns [] [] [va]
    TICKET va -> PrimExpr "TICKET" [] $ mkAnns [] [] [va]
    READ_TICKET va -> PrimExpr "READ_TICKET" [] $ mkAnns [] [] [va]
    SPLIT_TICKET va -> PrimExpr "SPLIT_TICKET" [] $ mkAnns [] [] [va]
    JOIN_TICKETS va -> PrimExpr "JOIN_TICKETS" [] $ mkAnns [] [] [va]
    NEVER -> PrimExpr "NEVER" [] []
    EXT _ -> ExpressionSeq []
    where
      wordToExpr :: Word -> Expression
      wordToExpr = toExpression @(Value 'TInt) . VInt . fromIntegral @Word @Integer

instance ToExpression Untyped.Contract where
  toExpression contract
    = ExpressionSeq $ Untyped.mapEntriesOrdered contract
          (\(Untyped.ParameterType ty rootAnn) -> PrimExpr "parameter"
            [insertRootAnn (toExpression ty) rootAnn] [])
          (\storage -> PrimExpr "storage" [toExpression storage] [])
          (\code -> PrimExpr "code" [toExpression code] [])

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

-- | Errors that can happen when we convert an 'Expression' to our
-- data type.
data FromExpressionError = FromExpressionError Expression Text
  deriving stock (Show, Eq)

instance Buildable FromExpressionError where
  build (FromExpressionError 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 FromExpression a where
  fromExpression :: Expression -> Either FromExpressionError a

instance (SingI t) => FromExpression (Value t) where
  fromExpression expr =
    case fromExpression @Untyped.Value expr of
    Right uv -> case typeCheck uv of
      Left tcErr -> Left $ FromExpressionError expr $
        pretty $ unlinesF
          [ "Failed to typecheck expression as a value of type:"
          , indentF 2 $ build $ demote @t
          , ""
          , "Typechecker error:"
          , indentF 2 $ build tcErr
          ]
      Right tv -> Right tv
    Left e -> Left e
    where
      typeCheck uv = typeCheckingWith (TypeCheckOptions False False) $
        (runTypeCheck $ TypeCheckValue (uv, demote @t)) $
        usingReaderT def $
        typeCheckValue uv

instance FromExpression Untyped.Value where
  fromExpression e = case e of
    ExpressionInt v -> pure $ Untyped.ValueInt v
    ExpressionString s -> first (FromExpressionError e)
      (Untyped.ValueString <$> mkMText s)
    ExpressionBytes bs -> pure $ Untyped.ValueBytes $ Untyped.InternalByteString bs
    PrimExpr "Unit" [] [] -> pure Untyped.ValueUnit
    PrimExpr "True" [] [] -> pure Untyped.ValueTrue
    PrimExpr "False" [] [] -> pure Untyped.ValueFalse
    PrimExpr "Pair" [l, r] [] -> do
      l' <- fromExpression l
      r' <- fromExpression r
      pure $ Untyped.ValuePair l' r'
    PrimExpr "Pair" args [] ->
      case (nonEmpty args) >>= forbidSingletonList of
        Nothing -> Left $ FromExpressionError e
          "Expected a pair with at least 2 arguments"
        Just args' -> fromExpression $ seqToPairExpr args' "Pair"
    PrimExpr "Left" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.ValueLeft arg'
    PrimExpr "Right" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.ValueRight arg'
    PrimExpr "Some" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.ValueSome arg'
    PrimExpr "None" [] [] -> pure Untyped.ValueNone
    ExpressionSeq [] -> pure Untyped.ValueNil
    ExpressionSeq (h : t) ->
      case fromExpression @Untyped.ExpandedOp h of
      Right op -> do
        ops <- traverse (fromExpression @Untyped.ExpandedOp) 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 fromExpression h of
          Left (FromExpressionError err _) -> Left $ FromExpressionError err
            "Value, instruction or 'Elt' expression expected"
          Right h' -> do
            t' <- traverse fromExpression t
            pure . Untyped.ValueSeq $ h' :| t'
    _ -> Left $ FromExpressionError e "Expected a value"
    where
      exprToElt :: Expression -> Either FromExpressionError (Untyped.Elt ExpandedOp)
      exprToElt ex = case ex of
        PrimExpr "Elt" [l, r] [] -> do
          l' <- fromExpression l
          r' <- fromExpression r
          pure $ Untyped.Elt l' r'
        PrimExpr "Elt" _ [] -> Left $ FromExpressionError ex
          "Expected 'Elt' expression with exactly 2 elements"
        PrimExpr "Elt" _ _ -> Left $ FromExpressionError ex
          "Expected 'Elt' expression without annotations"
        _ -> Left $ FromExpressionError ex "Expected 'Elt' expression"

instance (FromExpression a) => FromExpression [a] where
  fromExpression = \case
    ExpressionSeq exprs -> traverse fromExpression exprs
    e -> Left $ FromExpressionError e "'ExpressionSeq' expected"

instance FromExpression ExpandedOp where
  fromExpression = \case
    ExpressionSeq s -> SeqEx <$> traverse fromExpression s
    e               -> PrimEx <$> fromExpression e

instance FromExpression ExpandedInstr where
  fromExpression e = let annSet = getAnnSet e in case e of
    PrimExpr "DROP" [n] [] -> do
      n' <- intExprToWord n
      pure $ DROPN n'
    PrimExpr "DROP" [] _ -> pure $ DROP
    PrimExpr "DUP" [n] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      let va = firstAnn @VarTag annSet
      n' <- intExprToWord n
      pure $ DUPN va n'
    PrimExpr "DUP" [] _ ->
      let va = firstAnn @VarTag annSet
      in checkAnnsCount e annSet (0, 0, 1) $> DUP va
    PrimExpr "SWAP" [] [] -> pure $ SWAP
    PrimExpr "DIG" [n] [] -> do
      n' <- intExprToWord n
      pure $ DIG $ n'
    PrimExpr "DUG" [n] [] -> do
      n' <- intExprToWord n
      pure $ DUG n'
    PrimExpr "PUSH" [t, v] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      let va = firstAnn @VarTag annSet
      t' <- fromExpression @Ty t
      v' <- fromExpression @Untyped.Value v
      pure $ PUSH va t' v'
    PrimExpr "SOME" [] _ ->
      let ta = firstAnn @TypeTag annSet
          va = firstAnn @VarTag annSet
      in checkAnnsCount e annSet (1, 0, 1) $> SOME ta va
    PrimExpr "NONE" [t] _ -> do
      checkAnnsCount e annSet (1, 0, 1)
      let ta = firstAnn @TypeTag annSet
      let va = firstAnn @VarTag annSet
      t' <- fromExpression @Ty t
      pure $ NONE ta va t'
    PrimExpr "UNIT" [] _ ->
      let ta = firstAnn @TypeTag annSet
          va = firstAnn @VarTag annSet
      in checkAnnsCount e annSet (1, 0, 1) $> UNIT ta va
    PrimExpr "IF_NONE" [ops1, ops2] [] -> do
      ops1' <- fromExpression @([ExpandedOp]) ops1
      ops2' <- fromExpression @([ExpandedOp]) ops2
      pure $ IF_NONE ops1' ops2'
    PrimExpr "PAIR" [] _ ->
      let ta = firstAnn @TypeTag annSet
          va = firstAnn @VarTag annSet
          fa1 = firstAnn @FieldTag annSet
          fa2 = secondAnn @FieldTag annSet
      in (checkAnnsCount e annSet (1, 2, 1)) $> PAIR ta va fa1 fa2
    PrimExpr "UNPAIR" [] _ ->
      let va1 = firstAnn @VarTag annSet
          va2 = secondAnn @VarTag annSet
          fa1 = firstAnn @FieldTag annSet
          fa2 = secondAnn @FieldTag annSet
      in checkAnnsCount e annSet (0, 2, 2) $> UNPAIR va1 va2 fa1 fa2
    PrimExpr "PAIR" [n] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      n' <- intExprToWord n
      let va = firstAnn @VarTag annSet
      pure $ PAIRN va n'
    PrimExpr "UNPAIR" [n] [] -> do
      n' <- intExprToWord n
      pure $ UNPAIRN n'
    PrimExpr "CAR" [] _ ->
      let va = firstAnn @VarTag annSet
          fa = firstAnn @FieldTag annSet
      in checkAnnsCount e annSet (0, 1, 1) $> CAR va fa
    PrimExpr "CDR" [] _ ->
      let va = firstAnn @VarTag annSet
          fa = firstAnn @FieldTag annSet
      in checkAnnsCount e annSet (0, 1, 1) $> CDR va fa
    PrimExpr "LEFT" [t] _ -> do
      checkAnnsCount e annSet (1, 2, 1)
      t' <- fromExpression @Ty t
      let ta = firstAnn @TypeTag annSet
      let va = firstAnn @VarTag annSet
      let fa1 = firstAnn @FieldTag annSet
      let fa2 = secondAnn @FieldTag annSet
      pure $ LEFT ta va fa1 fa2 t'
    PrimExpr "RIGHT" [t] _ -> do
      checkAnnsCount e annSet (1, 2, 1)
      t' <- fromExpression @Ty t
      let ta = firstAnn @TypeTag annSet
      let va = firstAnn @VarTag annSet
      let fa1 = firstAnn @FieldTag annSet
      let fa2 = secondAnn @FieldTag annSet
      pure $ RIGHT ta va fa1 fa2 t'
    PrimExpr "IF_LEFT" [ops1, ops2] [] -> do
      ops1' <- fromExpression @([ExpandedOp]) ops1
      ops2' <- fromExpression @([ExpandedOp]) ops2
      pure $ IF_LEFT ops1' ops2'
    PrimExpr "NIL" [t] _ -> do
      checkAnnsCount e annSet (1, 0, 1)
      t' <- fromExpression @Ty t
      let va = firstAnn @VarTag annSet
      let ta = firstAnn @TypeTag annSet
      pure $ NIL ta va t'
    PrimExpr "CONS" [] anns -> mkInstrWithVarAnn CONS anns
    PrimExpr "IF_CONS" [ops1, ops2] [] -> do
      ops1' <- fromExpression @([ExpandedOp]) ops1
      ops2' <- fromExpression @([ExpandedOp]) ops2
      pure $ IF_CONS ops1' ops2'
    PrimExpr "SIZE" [] anns -> mkInstrWithVarAnn SIZE anns
    PrimExpr "EMPTY_SET" [t] _ -> do
      checkAnnsCount e annSet (1, 0, 1)
      t' <- fromExpression @Ty t
      let va = firstAnn @VarTag annSet
      let ta = firstAnn @TypeTag annSet
      pure $ EMPTY_SET ta va t'
    PrimExpr "EMPTY_MAP" [kt, vt] _ -> do
      checkAnnsCount e annSet (1, 0, 1)
      kt' <- fromExpression @Ty kt
      vt' <- fromExpression @Ty vt
      let va = firstAnn @VarTag annSet
      let ta = firstAnn @TypeTag annSet
      pure $ EMPTY_MAP ta va kt' vt'
    PrimExpr "EMPTY_BIG_MAP" [kt, vt] _ -> do
      checkAnnsCount e annSet (1, 0, 1)
      kt' <- fromExpression @Ty kt
      vt' <- fromExpression @Ty vt
      let va = firstAnn @VarTag annSet
      let ta = firstAnn @TypeTag annSet
      pure $ EMPTY_BIG_MAP ta va kt' vt'
    PrimExpr "MAP" [ops] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      ops' <- fromExpression @([ExpandedOp]) ops
      let va = firstAnn @VarTag annSet
      pure $ MAP va ops'
    PrimExpr "ITER" [ops] [] -> do
      ops' <- fromExpression @([ExpandedOp]) ops
      pure $ ITER ops'
    PrimExpr "MEM" [] anns -> mkInstrWithVarAnn MEM anns
    PrimExpr "GET" [] anns -> mkInstrWithVarAnn GET anns
    PrimExpr "GET" [n] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      n' <- intExprToWord n
      let va = firstAnn @VarTag annSet
      pure $ GETN va n'
    PrimExpr "UPDATE" [] anns -> mkInstrWithVarAnn UPDATE anns
    PrimExpr "UPDATE" [n] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      n' <- intExprToWord n
      let va = firstAnn @VarTag annSet
      pure $ UPDATEN va n'
    PrimExpr "GET_AND_UPDATE" [] anns ->
      mkInstrWithVarAnn GET_AND_UPDATE anns
    PrimExpr "IF" [ops1, ops2] [] -> do
      ops1' <- fromExpression @([ExpandedOp]) ops1
      ops2' <- fromExpression @([ExpandedOp]) ops2
      pure $ IF ops1' ops2'
    PrimExpr "LOOP" [ops] [] -> do
      ops' <- fromExpression @([ExpandedOp]) ops
      pure $ LOOP ops'
    PrimExpr "LOOP_LEFT" [ops] [] -> do
      ops' <- fromExpression @([ExpandedOp]) ops
      pure $ LOOP_LEFT ops'
    PrimExpr "LAMBDA" [inp, out, ops] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      inp' <- fromExpression @Ty inp
      out' <- fromExpression @Ty out
      ops' <- fromExpression @([ExpandedOp]) ops
      let va = firstAnn @VarTag annSet
      pure $ LAMBDA va inp' out' ops'
    PrimExpr "EXEC" [] anns -> mkInstrWithVarAnn EXEC anns
    PrimExpr "APPLY" [] anns -> mkInstrWithVarAnn APPLY anns
    PrimExpr "DIP" [ops] [] -> do
      ops' <- fromExpression @([ExpandedOp]) ops
      pure $ DIP ops'
    PrimExpr "DIP" [n, ops] [] -> do
      n' <- intExprToWord n
      ops' <- fromExpression @([ExpandedOp]) ops
      pure $ DIPN n' ops'
    PrimExpr "FAILWITH" [] [] -> pure FAILWITH
    PrimExpr "CAST" [t] _ -> do
      checkAnnsCount e annSet (0, 0, 1)
      t' <- fromExpression @Ty t
      let va = firstAnn @VarTag annSet
      pure $ CAST va t'
    PrimExpr "RENAME" [] anns -> mkInstrWithVarAnn RENAME anns
    PrimExpr "PACK" [] anns -> mkInstrWithVarAnn PACK anns
    PrimExpr "UNPACK" [t] _ -> do
      checkAnnsCount e annSet (1, 0, 1)
      t' <- fromExpression @Ty t
      let ta = firstAnn @TypeTag annSet
      let va = firstAnn @VarTag annSet
      pure $ UNPACK ta va t'
    PrimExpr "CONCAT" [] anns -> mkInstrWithVarAnn CONCAT anns
    PrimExpr "SLICE" [] anns -> mkInstrWithVarAnn SLICE anns
    PrimExpr "ISNAT" [] anns -> mkInstrWithVarAnn ISNAT anns
    PrimExpr "ADD" [] anns -> mkInstrWithVarAnn ADD anns
    PrimExpr "SUB" [] anns -> mkInstrWithVarAnn SUB anns
    PrimExpr "MUL" [] anns -> mkInstrWithVarAnn MUL anns
    PrimExpr "EDIV" [] anns -> mkInstrWithVarAnn EDIV anns
    PrimExpr "ABS" [] anns -> mkInstrWithVarAnn ABS anns
    PrimExpr "NEG" [] anns -> mkInstrWithVarAnn NEG anns
    PrimExpr "LSL" [] anns -> mkInstrWithVarAnn LSL anns
    PrimExpr "LSR" [] anns -> mkInstrWithVarAnn LSR anns
    PrimExpr "OR" [] anns -> mkInstrWithVarAnn OR anns
    PrimExpr "AND" [] anns -> mkInstrWithVarAnn AND anns
    PrimExpr "XOR" [] anns -> mkInstrWithVarAnn XOR anns
    PrimExpr "NOT" [] anns -> mkInstrWithVarAnn NOT anns
    PrimExpr "COMPARE" [] anns -> mkInstrWithVarAnn COMPARE anns
    PrimExpr "EQ" [] anns -> mkInstrWithVarAnn Untyped.EQ anns
    PrimExpr "NEQ" [] anns -> mkInstrWithVarAnn NEQ anns
    PrimExpr "LT" [] anns -> mkInstrWithVarAnn Untyped.LT anns
    PrimExpr "GT" [] anns -> mkInstrWithVarAnn Untyped.GT anns
    PrimExpr "LE" [] anns -> mkInstrWithVarAnn LE anns
    PrimExpr "GE" [] anns -> mkInstrWithVarAnn GE anns
    PrimExpr "INT" [] anns -> mkInstrWithVarAnn INT anns
    PrimExpr "SELF" [] _ ->
      let fa = firstAnn @FieldTag annSet
          va = firstAnn @VarTag annSet
      in checkAnnsCount e annSet (0, 1, 1) $> SELF va fa
    PrimExpr "CONTRACT" [t] _ -> do
      checkAnnsCount e annSet (0, 1, 1)
      t' <- fromExpression @Ty t
      let va = firstAnn @VarTag annSet
      let fa = firstAnn @FieldTag annSet
      pure $ CONTRACT va fa t'
    PrimExpr "TRANSFER_TOKENS" [] anns ->
      mkInstrWithVarAnn TRANSFER_TOKENS anns
    PrimExpr "SET_DELEGATE" [] anns ->
      mkInstrWithVarAnn SET_DELEGATE anns
    PrimExpr "CREATE_CONTRACT" [c] _ -> do
      checkAnnsCount e annSet (0, 0, 2)
      c' <- fromExpression @Untyped.Contract c
      let va1 = firstAnn @VarTag annSet
      let va2 = secondAnn @VarTag annSet
      pure $ CREATE_CONTRACT va1 va2 c'
    PrimExpr "IMPLICIT_ACCOUNT" [] anns ->
      mkInstrWithVarAnn IMPLICIT_ACCOUNT anns
    PrimExpr "NOW" [] anns -> mkInstrWithVarAnn NOW anns
    PrimExpr "AMOUNT" [] anns -> mkInstrWithVarAnn AMOUNT anns
    PrimExpr "BALANCE" [] anns -> mkInstrWithVarAnn BALANCE anns
    PrimExpr "VOTING_POWER" [] anns ->
      mkInstrWithVarAnn VOTING_POWER anns
    PrimExpr "TOTAL_VOTING_POWER" [] anns ->
      mkInstrWithVarAnn TOTAL_VOTING_POWER anns
    PrimExpr "CHECK_SIGNATURE" [] anns ->
      mkInstrWithVarAnn CHECK_SIGNATURE anns
    PrimExpr "SHA256" [] anns -> mkInstrWithVarAnn SHA256 anns
    PrimExpr "SHA512" [] anns -> mkInstrWithVarAnn SHA512 anns
    PrimExpr "BLAKE2B" [] anns -> mkInstrWithVarAnn BLAKE2B anns
    PrimExpr "SHA3" [] anns -> mkInstrWithVarAnn SHA3 anns
    PrimExpr "KECCAK" [] anns -> mkInstrWithVarAnn KECCAK anns
    PrimExpr "HASH_KEY" [] anns -> mkInstrWithVarAnn HASH_KEY anns
    PrimExpr "PAIRING_CHECK" [] anns ->
      mkInstrWithVarAnn PAIRING_CHECK anns
    PrimExpr "SOURCE" [] anns -> mkInstrWithVarAnn SOURCE anns
    PrimExpr "SENDER" [] anns -> mkInstrWithVarAnn SENDER anns
    PrimExpr "ADDRESS" [] anns -> mkInstrWithVarAnn ADDRESS anns
    PrimExpr "CHAIN_ID" [] anns -> mkInstrWithVarAnn CHAIN_ID anns
    PrimExpr "LEVEL" [] anns -> mkInstrWithVarAnn LEVEL anns
    PrimExpr "SELF_ADDRESS" [] anns ->
      mkInstrWithVarAnn SELF_ADDRESS anns
    PrimExpr "NEVER" [] [] -> pure NEVER
    PrimExpr "TICKET" [] anns -> mkInstrWithVarAnn TICKET anns
    PrimExpr "READ_TICKET" [] anns ->
      mkInstrWithVarAnn READ_TICKET anns
    PrimExpr "SPLIT_TICKET" [] anns ->
      mkInstrWithVarAnn SPLIT_TICKET anns
    PrimExpr "JOIN_TICKETS" [] anns ->
      mkInstrWithVarAnn JOIN_TICKETS anns
    _ -> Left $ FromExpressionError e "Expected an instruction"

    where
      intExprToWord :: Expression -> Either FromExpressionError Word
      intExprToWord n = do
        v <- fromExpression @(Value 'TInt) n
        case v of
          VInt n' -> maybeToRight (FromExpressionError n "Value is out of bounds")
            (toIntegralSized @Integer @Word n')

      mkInstrWithVarAnn
        :: (VarAnn -> ExpandedInstr)
        -> [Annotation]
        -> Either FromExpressionError ExpandedInstr
      mkInstrWithVarAnn ctor anns =
        let annSet = toAnnSet anns
            va = firstAnn @VarTag annSet
        in checkAnnsCount e annSet (0, 0, 1) $> ctor va

      getAnnSet :: Expression -> AnnotationSet
      getAnnSet = \case
        PrimExpr _ _ anns -> toAnnSet anns
        _                 -> emptyAnnSet

instance FromExpression Untyped.Contract where
  fromExpression blocks = case blocks of
    ExpressionSeq [b1, b2, b3] -> do
      b1' <- exprToCB b1
      b2' <- exprToCB b2
      b3' <- exprToCB b3
      maybeToRight (FromExpressionError blocks fullErrorMsg)
        (orderContractBlock (b1', b2', b3'))
    expr -> Left $ FromExpressionError expr fullErrorMsg
    where
      exprToCB
        :: Expression
        -> Either FromExpressionError (ContractBlock ExpandedOp)
      exprToCB e = case e of
        PrimExpr "parameter" args anns -> mkCbParam e args anns
        PrimExpr "storage"   args anns -> mkCBStorage e args anns
        PrimExpr "code"      args anns -> mkCBCode e args anns
        _                              -> Left $ FromExpressionError e fullErrorMsg

      mkCbParam
        :: Expression
        -> [Expression]
        -> [Annotation]
        -> Either FromExpressionError (ContractBlock ExpandedOp)
      mkCbParam e args anns = case (args, anns) of
        ([p], []) -> do
          let annSet = toAnnSet (p ^. _ExpressionPrim . mpaAnnotsL)
          let rootAnn = firstAnn @FieldTag annSet
          unless (secondAnn @FieldTag annSet == noAnn) $
            Left $ FromExpressionError p
              "Expected parameter with at most 1 root annotation"
          p' <- fromExpression @Ty
            (p & _ExpressionPrim . mpaAnnotsL %~ filter (not . isAnnotationField))
          pure $ CBParam $ Untyped.ParameterType p' rootAnn
        _ -> Left $ FromExpressionError e
          "Expected 'parameter' block without annotations and exactly 1 argument"

      mkCBStorage
        :: Expression
        -> [Expression]
        -> [Annotation]
        -> Either FromExpressionError (ContractBlock ExpandedOp)
      mkCBStorage e args anns = case (args, anns) of
        ([s], []) -> do
          s' <- fromExpression @Ty s
          pure $ CBStorage s'
        _ -> Left $ FromExpressionError e
               "Expected 'storage' block without annotations and exactly 1 argument"

      mkCBCode
        :: Expression
        -> [Expression]
        -> [Annotation]
        -> Either FromExpressionError (ContractBlock ExpandedOp)
      mkCBCode e args anns = case (args, anns) of
        ([ops], []) -> do
          ops' <- fromExpression @([ExpandedOp]) ops
          pure $ CBCode ops'
        _ -> Left $ FromExpressionError e
               "Expected 'code' block without annotations"

      fullErrorMsg = "Expected contract expression to have exactly 3 " <>
        "sub-expressions ('parameter', 'storage' and 'code')"


instance FromExpression Untyped.T where
  fromExpression e = case e of
    PrimExpr "key" [] [] -> pure Untyped.TKey
    PrimExpr "unit" [] [] -> pure Untyped.TUnit
    PrimExpr "signature" [] [] -> pure Untyped.TSignature
    PrimExpr "chain_id" [] [] -> pure Untyped.TChainId
    PrimExpr "option" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.TOption arg'
    PrimExpr "list" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.TList arg'
    PrimExpr "set" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.TSet arg'
    PrimExpr "operation" [] [] -> pure Untyped.TOperation
    PrimExpr "contract" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.TContract arg'
    PrimExpr "ticket" [arg] [] -> do
      arg' <- fromExpression arg
      pure $ Untyped.TTicket arg'
    PrimExpr "or" [arg1, arg2] [] -> do
      let as1 = toAnnSet $ arg1 ^. _ExpressionPrim . mpaAnnotsL
      let as2 = toAnnSet $ arg2 ^. _ExpressionPrim . mpaAnnotsL
      checkAnnsCount e as1 (1, 1, 0)
      checkAnnsCount e as2 (1, 1, 0)
      let fa1 = firstAnn @FieldTag as1
      let fa2 = firstAnn @FieldTag as2
      l <- fromExpression $ removeAnns arg1 isAnnotationField
      r <- fromExpression $ removeAnns arg2 isAnnotationField
      pure $ Untyped.TOr fa1 fa2 l r
    PrimExpr "pair" [arg1, arg2] [] -> do
      let as1 = toAnnSet $ arg1 ^. _ExpressionPrim . mpaAnnotsL
      let as2 = toAnnSet $ arg2 ^. _ExpressionPrim . mpaAnnotsL
      checkAnnsCount e as1 (1, 1, 1)
      checkAnnsCount e as2 (1, 1, 1)
      let fa1 = firstAnn @FieldTag as1
      let fa2 = firstAnn @FieldTag as2
      let va1 = firstAnn @VarTag as1
      let va2 = firstAnn @VarTag as2
      l <- fromExpression $ removeAnns arg1
        (isAnnotationField || isAnnotationVariable)
      r <- fromExpression $ removeAnns arg2
        (isAnnotationField || isAnnotationVariable)
      pure $ Untyped.TPair fa1 fa2 va1 va2 l r
    PrimExpr "pair" args [] ->
      case (nonEmpty args) >>= forbidSingletonList of
        Nothing -> Left $ FromExpressionError e
          "Expected a pair with at least 2 arguments"
        Just args' -> fromExpression $ seqToPairExpr args' "pair"
    PrimExpr "lambda" args [] -> mkDoubleParamType Untyped.TLambda args e
      "Expected a lambda with input and output types"
    PrimExpr "map" args [] -> mkDoubleParamType Untyped.TMap args e
      "Expected a map with key and value types"
    PrimExpr "big_map" args [] -> mkDoubleParamType Untyped.TBigMap args e
      "Expected a big_map with key and value types"
    PrimExpr "int" [] [] -> pure Untyped.TInt
    PrimExpr "nat" [] [] -> pure Untyped.TNat
    PrimExpr "string" [] [] -> pure Untyped.TString
    PrimExpr "bytes" [] [] -> pure Untyped.TBytes
    PrimExpr "mutez" [] [] -> pure Untyped.TMutez
    PrimExpr "bool" [] [] -> pure Untyped.TBool
    PrimExpr "key_hash" [] [] -> pure Untyped.TKeyHash
    PrimExpr "bls12_381_fr" [] [] -> pure Untyped.TBls12381Fr
    PrimExpr "bls12_381_g1" [] [] -> pure Untyped.TBls12381G1
    PrimExpr "bls12_381_g2" [] [] -> pure Untyped.TBls12381G2
    PrimExpr "timestamp" [] [] -> pure Untyped.TTimestamp
    PrimExpr "address" [] [] -> pure Untyped.TAddress
    PrimExpr "never" [] [] -> pure Untyped.TNever
    _ -> Left $ FromExpressionError e "Expected a type"
    where
      mkDoubleParamType
        :: (Ty -> Ty -> Untyped.T)
        -> [Expression]
        -> Expression
        -> Text
        -> Either FromExpressionError Untyped.T
      mkDoubleParamType ctor args expr msg = do
        case args of
          [arg1, arg2] -> do
            arg1' <- fromExpression arg1
            arg2' <- fromExpression arg2
            pure $ ctor arg1' arg2'
          _ -> Left $ FromExpressionError expr msg

      removeAnns :: Expression -> (Annotation -> Bool) -> Expression
      removeAnns expr p =
        expr & _ExpressionPrim . mpaAnnotsL %~ filter (not . p)

instance FromExpression Ty where
  fromExpression e = case e of
    PrimExpr primName args anns -> do
      let annSet = toAnnSet anns
      let ta = firstAnn @TypeTag annSet
      when (secondAnn @TypeTag annSet /= noAnn) $
        Left $ FromExpressionError e
          "Expected expression with at most 1 type annotation"
      t <- fromExpression @Untyped.T $ PrimExpr primName args $ filter
        (not . isAnnotationType) anns
      pure $ Ty t ta
    _ -> Left $ FromExpressionError e "Expected a type"

instance FromExpression T where
  fromExpression =
    second fromUType . fromExpression @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) => FromExpression (Instr '[inp] '[out]) where
  fromExpression expr =
    fromExpression @(Value ('TLambda inp out)) expr <&> \case
      VLam instr -> rfAnyInstr instr

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

-- | Converts a sequence of expression to the right combed pair.
seqToPairExpr :: NonEmpty Expression -> Text -> Expression
seqToPairExpr e name = foldr1 (\x xs -> PrimExpr name [x, xs] []) e

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

-- | Inserts the root annotation into the contract parameter.
insertRootAnn :: HasCallStack => Expression -> RootAnn -> Expression
insertRootAnn expr rootAnn = case expr of
  ExpressionPrim 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: " <> show expr

-- | Checks for a given expression that the number of annotations
-- of each type in it doesn't exceed the specified threshold.
checkAnnsCount
  :: Expression
  -> AnnotationSet
  -> (Int, Int, Int)
  -> Either FromExpressionError ()
checkAnnsCount e annSet maxCount@(maxTas, maxFas, maxVas) =
  let actualCount@(tasCnt, fasCnt, vasCnt) = annsCount annSet
  in unless (actualCount <= maxCount) $
    Left $ FromExpressionError e $ pretty $ unlinesF
      [ "Expected at most"
      , indentF 2 $ build maxTas <> " type annotations,"
      , indentF 2 $ build maxFas <> " field annotations,"
      , indentF 2 $ build maxVas <> " variable annotations"
      , "but found:"
      , indentF 2 $ build tasCnt <> " type annotations,"
      , indentF 2 $ build fasCnt <> " field annotations,"
      , indentF 2 $ build vasCnt <> " variable annotations."
      ]

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