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

-- TODO [#549]: remove this pragma
{-# OPTIONS_GHC -Wno-deprecations #-}

-- | This module contains a type family for converting a type to its RPC representation,
-- and TemplateHaskell functions for deriving RPC representations for custom types.
module Morley.Client.RPC.AsRPC
  ( AsRPC
  , deriveRPC
  , deriveRPCWithStrategy
  , deriveManyRPC
  , deriveManyRPCWithStrategy
  -- * Conversions
  , valueAsRPC
  , notesAsRPC
  -- * Entailments
  , rpcSingIEvi
  , rpcHasNoOpEvi
  , rpcHasNoBigMapEvi
  , rpcHasNoNestedBigMapsEvi
  , rpcHasNoContractEvi
  , rpcStorageScopeEvi
  ) where

import Prelude hiding (Type)

import Control.Lens.Plated (universe)
import Data.Constraint (Dict(..), (***), (:-)(Sub), (\\))
import qualified Data.List as List ((\\))
import Data.Singletons (Sing, withSingI)
import qualified GHC.Generics as G
import Language.Haskell.TH
  (Con(InfixC, NormalC, RecC), Cxt, Dec(DataD, NewtypeD, TySynD, TySynInstD),
  DerivStrategy(AnyclassStrategy), Info(TyConI), Kind, Loc(loc_module), Name, Q, TyLit(StrTyLit),
  TySynEqn(..), TyVarBndr, Type(..), cxt, location, mkName, nameBase, reify, reifyInstances,
  standaloneDerivWithStrategyD)
import Language.Haskell.TH.ReifyMany (reifyManyTyCons)
import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames)

import Lorentz hiding (TAddress, TSignature, drop, not)
import qualified Lorentz as L
import Lorentz.Extensible (Extensible)
import Morley.Michelson.Typed
  (ContractPresence(ContractAbsent), HasNoBigMap, HasNoContract, HasNoNestedBigMaps, HasNoOp,
  Notes(..), OpPresence(..), SingI(sing), SingT(..), StorageScope, T(..), Value'(..),
  checkContractTypePresence, checkOpPresence)
import Morley.Util.Named hiding (Name(..))
import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail)

{-# ANN module ("HLint: ignore Avoid lambda using `infix`" :: Text) #-}

----------------------------------------------------------------------------
-- AsRPC
----------------------------------------------------------------------------

-- | A type-level function that maps a type to its Tezos RPC representation.
--
-- For example, when we retrieve a contract's storage using the Tezos RPC, all its 'BigMap's will be replaced
-- by 'BigMapId's.
--
-- So if a contract has a storage of type @T@, when we call the Tezos RPC
-- to retrieve it, we must deserialize the micheline expression to the type @AsRPC T@.
--
-- > AsRPC (BigMap Integer MText) ~ BigMapId Integer MText
-- > AsRPC [BigMap Integer MText] ~ [BigMapId Integer MText]
-- > AsRPC (MText, (Address, BigMap Integer MText)) ~ (MText, (Address, BigMapId Integer MText))
--
-- The following law holds IFF a type @t@ has an IsoValue instance:
--
-- > ToT (AsRPC t) ~ AsRPC (ToT t)
--
type family AsRPC (a :: k) :: k

-- Value
type instance AsRPC (Value' instr t) = Value' instr (AsRPC t)
type instance AsRPC 'TKey = 'TKey
type instance AsRPC 'TUnit = 'TUnit
type instance AsRPC 'TSignature = 'TSignature
type instance AsRPC 'TChainId = 'TChainId
type instance AsRPC ('TOption t) = 'TOption (AsRPC t)
type instance AsRPC ('TList t) = 'TList (AsRPC t)
type instance AsRPC ('TSet t) = 'TSet t
type instance AsRPC 'TOperation = 'TOperation
type instance AsRPC ('TContract t) = 'TContract t
type instance AsRPC ('TTicket t) = 'TTicket t
type instance AsRPC ('TPair t1 t2) = 'TPair (AsRPC t1) (AsRPC t2)
type instance AsRPC ('TOr t1 t2) = 'TOr (AsRPC t1) (AsRPC t2)
type instance AsRPC ('TLambda t1 t2) = 'TLambda t1 t2
type instance AsRPC ('TMap k v) = 'TMap k (AsRPC v)
type instance AsRPC ('TBigMap _ _) = 'TNat
type instance AsRPC 'TInt = 'TInt
type instance AsRPC 'TNat = 'TNat
type instance AsRPC 'TString = 'TString
type instance AsRPC 'TBytes = 'TBytes
type instance AsRPC 'TMutez = 'TMutez
type instance AsRPC 'TBool = 'TBool
type instance AsRPC 'TKeyHash = 'TKeyHash
type instance AsRPC 'TTimestamp = 'TTimestamp
type instance AsRPC 'TAddress = 'TAddress
type instance AsRPC 'TNever = 'TNever
type instance AsRPC 'TBls12381Fr = 'TBls12381Fr
type instance AsRPC 'TBls12381G1 = 'TBls12381G1
type instance AsRPC 'TBls12381G2 = 'TBls12381G2
type instance AsRPC 'TChest = 'TChest
type instance AsRPC 'TChestKey = 'TChestKey

-- Morley types

-- Note: We don't recursively apply @AsRPC@ to @k@ or @v@ because
-- bigmaps cannot contain nested bigmaps.
-- If this constraint is ever lifted, we'll have to change this instance
-- to @BigMapId k (AsRPC v)@
type instance AsRPC (BigMap k v) = BigMapId k v
type instance AsRPC Integer = Integer
type instance AsRPC Natural = Natural
type instance AsRPC MText = MText
type instance AsRPC Bool = Bool
type instance AsRPC ByteString = ByteString
type instance AsRPC Mutez = Mutez
type instance AsRPC KeyHash = KeyHash
type instance AsRPC Timestamp = Timestamp
type instance AsRPC Address = Address
type instance AsRPC EpAddress = EpAddress
type instance AsRPC (L.TAddress p vd) = L.TAddress p vd
type instance AsRPC (FutureContract p) = FutureContract p
type instance AsRPC PublicKey = PublicKey
type instance AsRPC Signature = Signature
type instance AsRPC ChainId = ChainId
type instance AsRPC Never = Never
type instance AsRPC Bls12381Fr = Bls12381Fr
type instance AsRPC Bls12381G1 = Bls12381G1
type instance AsRPC Bls12381G2 = Bls12381G2
type instance AsRPC () = ()
type instance AsRPC [a] = [AsRPC a]
type instance AsRPC (Maybe a) = Maybe (AsRPC a)
type instance AsRPC (Either l r) = Either (AsRPC l) (AsRPC r)
type instance AsRPC (a, b) = (AsRPC a, AsRPC b)
type instance AsRPC (Set a) = Set a
type instance AsRPC (Map k v) = Map k (AsRPC v)
type instance AsRPC Operation = Operation
type instance AsRPC (Identity a) = Identity (AsRPC a)
type instance AsRPC (NamedF Identity a name) = NamedF Identity (AsRPC a) name
type instance AsRPC (NamedF Maybe a name) = NamedF Maybe (AsRPC a) name
type instance AsRPC (a, b, c) = (AsRPC a, AsRPC b, AsRPC c)
type instance AsRPC (a, b, c, d) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d)
type instance AsRPC (a, b, c, d, e) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e)
type instance AsRPC (a, b, c, d, e, f) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f)
type instance AsRPC (a, b, c, d, e, f, g) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f, AsRPC g)
type instance AsRPC (ContractRef arg) = ContractRef arg
type instance AsRPC Chest = Chest
type instance AsRPC ChestKey = ChestKey

-- Lorentz types
type instance AsRPC (Packed a) = Packed a
type instance AsRPC (L.TSignature a) = L.TSignature a
type instance AsRPC (Hash alg a) = Hash alg a
type instance AsRPC (L.TAddress cp) = L.TAddress cp
type instance AsRPC Empty = Empty
type instance AsRPC (Extensible x) = Extensible x
type instance AsRPC (View_ a r) = View_ a r
type instance AsRPC (Void_ a r) = Void_ a r
type instance AsRPC (UParam entries) = UParam entries
type instance AsRPC (inp :-> out) = inp :-> out
type instance AsRPC (ShouldHaveEntrypoints a) = ShouldHaveEntrypoints a
type instance AsRPC (ParameterWrapper deriv cp) = ParameterWrapper deriv (AsRPC cp)
type instance AsRPC L.OpenChest = L.OpenChest
type instance AsRPC (L.ChestT a) = L.ChestT a
type instance AsRPC (L.OpenChestT a) = L.OpenChestT a

----------------------------------------------------------------------------
-- Derive RPC repr
----------------------------------------------------------------------------

-- | Derive an RPC representation for a type, as well as instances for 'Generic', 'IsoValue' and 'AsRPC'.
--
-- > data ExampleStorage a b = ExampleStorage
-- >   { esField1 :: Integer
-- >   , esField2 :: [BigMap Integer MText]
-- >   , esField3 :: a
-- >   }
-- >   deriving stock Generic
-- >   deriving anyclass IsoValue
-- >
-- > deriveRPC "ExampleStorage"
--
-- Will generate:
--
-- > data ExampleStorageRPC a b = ExampleStorageRPC
-- >   { esField1RPC :: AsRPC Integer
-- >   , esField2RPC :: AsRPC [BigMap Integer MText]
-- >   , esField3RPC :: AsRPC a
-- >   }
-- >
-- > type instance AsRPC (ExampleStorage a b) = ExampleStorageRPC a b
-- > deriving anyclass instance (IsoValue (AsRPC a), IsoValue (AsRPC b)) => IsoValue (ExampleStorageRPC a b)
-- > instance Generic (ExampleStorageRPC a b) where
-- >   ...
deriveRPC :: String -> Q [Dec]
deriveRPC typeStr = deriveRPCWithStrategy typeStr haskellBalanced

-- | Recursively enumerate @data@, @newtype@ and @type@ declarations,
-- and derives an RPC representation for each type that doesn't yet have one.
--
-- You can also pass in a list of types for which you _don't_ want
-- an RPC representation to be derived.
--
-- In this example, 'deriveManyRPC' will generate an RPC
-- representation for @A@ and @B@,
-- but not for @C@ (because we explicitly said we don't want one)
-- or @D@ (because it already has one).
--
-- > data B = B
-- > data C = C
-- > data D = D
-- > deriveRPC "D"
-- >
-- > data A = A B C D
-- > deriveManyRPC "A" ["C"]
deriveManyRPC :: String -> [String] -> Q [Dec]
deriveManyRPC typeStr skipTypes =
  deriveManyRPCWithStrategy typeStr skipTypes haskellBalanced

-- | Same as 'deriveManyRPC', but uses a custom strategy for deriving a 'Generic' instance.
deriveManyRPCWithStrategy :: String -> [String] -> GenericStrategy -> Q [Dec]
deriveManyRPCWithStrategy typeStr skipTypes gs = do
  skipTypeNames <- traverse lookupTypeNameOrFail skipTypes
  typeName <- lookupTypeNameOrFail typeStr
  whenM (isTypeAlias typeName) $ fail $ typeStr <> " is a 'type' alias but not 'data' or 'newtype'."
  allTypeNames <- findWithoutInstance typeName
  join <$> forM (allTypeNames List.\\ skipTypeNames) \name -> deriveRPCWithStrategy' name gs
  where

    -- | Recursively enumerate @data@, @newtype@ and @type@ declarations,
    -- and returns the names of only @data@ and @newtype@ of those that
    -- don't yet have an 'AsRPC' instance. Type aliases don't need instances
    -- and respectively there is no need to derive 'AsRPC' for them.
    findWithoutInstance :: Name -> Q [Name]
    findWithoutInstance typeName =
      fmap fst <$>
        reifyManyTyCons
          (\(name, dec) ->
            ifM (isTypeAlias name)
              (pure (False, decConcreteNames dec))
              (ifM (hasRPCInstance name)
                (pure (False, []))
                (pure (True, decConcreteNames dec)))
          )
          [typeName]

    hasRPCInstance :: Name -> Q Bool
    hasRPCInstance typeName = do
      deriveFullTypeFromName typeName >>= \case
        Nothing ->
          fail $ "Found a field with a type that is neither a 'data' nor a 'newtype' nor a 'type': "
            <> show typeName
        Just typ ->
          not . null <$> reifyInstances ''AsRPC [typ]

    -- | Given a type name, return the corresponding type expression
    -- (applied to any type variables, if necessary).
    --
    -- For example, assuming a data type like @data F a b = ...@ exists in the type environment,
    -- then @deriveFullTypeFromName ''F@ will return the type expression @[t|F a b|]@.
    --
    -- Note that only @data@, @newtype@ and @type@ declarations are supported at the moment.
    deriveFullTypeFromName :: Name -> Q (Maybe Type)
    deriveFullTypeFromName typeName = do
      typeInfo <- reify typeName
      case typeInfo of
        TyConI (DataD _ _ vars mKind _ _) -> Just <$> deriveFullType typeName mKind vars
        TyConI (NewtypeD _ _ vars mKind _ _) -> Just <$> deriveFullType typeName mKind vars
        TyConI (TySynD _ vars _) -> Just <$> deriveFullType typeName Nothing vars
        _ -> pure Nothing

-- | Same as 'deriveRPC', but uses a custom strategy for deriving a 'Generic' instance.
deriveRPCWithStrategy :: String -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy typeStr gs = do
  typeName <- lookupTypeNameOrFail typeStr
  whenM (isTypeAlias typeName) $ fail $ typeStr <> " is a 'type' alias but not 'data' or 'newtype'."
  deriveRPCWithStrategy' typeName gs

deriveRPCWithStrategy' :: Name -> GenericStrategy -> Q [Dec]
deriveRPCWithStrategy' typeName gs = do
  (_, decCxt, mKind, tyVars, constructors) <- reifyDataType typeName

  -- TODO: use `reifyInstances` to check that 'AsRPC' exists for `fieldType`
  -- Print user-friendly error msg if it doesn't.
  let typeNameRPC = convertName typeName
  constructorsRPC <- traverse convertConstructor constructors
  fieldTypesRPC <- getFieldTypes constructorsRPC

  derivedType <- deriveFullType typeName mKind tyVars
  derivedTypeRPC <- deriveFullType typeNameRPC mKind tyVars

  -- Note: we can't use `makeRep0Inline` to derive a `Rep` instance for `derivedTypeRPC`
  -- It internally uses `reify` to lookup info about `derivedTypeRPC`, and because `derivedTypeRPC` hasn't
  -- been spliced *yet*, the lookup fails.
  -- So, instead, we fetch the `Rep` instance for `derivedType`, and
  -- append "RPC" to the type/constructor/field names in its metadata.
  --
  -- If, for some reason, we find out that this approach doesn't work for some edge cases,
  -- we should get rid of it and patch the @generic-deriving@ package to export a version of `makeRep0Inline`
  -- that doesn't use `reify` (it should be easy enough).
  repInstance <- reifyRepInstance typeName derivedType
  currentModuleName <- loc_module <$> location
  let repTypeRPC = convertRep currentModuleName repInstance
  typeDecOfRPC <- mkTypeDeclaration typeName decCxt typeNameRPC tyVars mKind constructorsRPC

  mconcat <$> sequence
    [ pure . one $ typeDecOfRPC
    , mkAsRPCInstance derivedType derivedTypeRPC
    , mkIsoValueInstance fieldTypesRPC derivedTypeRPC
    , customGeneric' (Just repTypeRPC) typeNameRPC derivedTypeRPC constructorsRPC gs
    ]

  where
    -- | Given the field type @FieldType a b@, returns @AsRPC (FieldType a b)@.
    convertFieldType :: Type -> Type
    convertFieldType tp = ConT ''AsRPC `AppT` tp

    convertNameStr :: String -> String
    convertNameStr s = s <> "RPC"

    convertName :: Name -> Name
    convertName = mkName . convertNameStr . nameBase

    -- | Given the constructor
    -- @C { f :: Int }@,
    -- returns the constructor
    -- @CRPC { fRPC :: AsRPC Int }@.
    convertConstructor :: Con -> Q Con
    convertConstructor = \case
      RecC conName fields -> pure $
        RecC
          (convertName conName)
          (fields <&> \(fieldName, fieldBang, fieldType) ->
            (convertName fieldName, fieldBang, convertFieldType fieldType)
          )
      NormalC conName fields -> pure $
        NormalC (convertName conName) (second convertFieldType <$> fields)
      InfixC fieldType1 conName fieldType2 -> pure $
        InfixC (second convertFieldType fieldType1) (convertName conName) (second convertFieldType fieldType2)
      constr -> fail $ "Unsupported constructor for '" <> show typeName <> "': " <> show constr

    -- | Get a list of all the unique types of all the fields of all the given constructors.
    getFieldTypes :: [Con] -> Q [Type]
    getFieldTypes constrs = ordNub . join <$> forM constrs \case
      RecC _ fields -> pure $ fields <&> \(_, _, fieldType) -> fieldType
      NormalC _ fields -> pure $ snd <$> fields
      InfixC field1 _ field2 -> pure [snd field1, snd field2]
      constr -> fail $ "Unsupported constructor for '" <> show typeName <> "': " <> show constr

    mkTypeDeclaration :: Name -> Cxt -> Name -> [TyVarBndr] -> Maybe Kind -> [Con] -> Q Dec
    mkTypeDeclaration tyName decCxt typeNameRPC tyVars mKind constructorsRPC = do
      typeInfo <- reify tyName
      case typeInfo of
        TyConI DataD {} -> pure $ DataD decCxt typeNameRPC tyVars mKind constructorsRPC []
        TyConI NewtypeD {} -> (case constructorsRPC of
          [con] -> pure $ NewtypeD decCxt typeNameRPC tyVars mKind con []
          _ -> fail "Newtype has only one constructor")
        _ -> fail $ "Only newtypes and data types are supported, but '" <>
          show tyName <> "' is:\n" <> show typeInfo

    -- | Traverse a 'Rep' type and:
    --
    -- 1. Inspect its metadata and append @RPC@ to the type/constructor/field names.
    -- 2. Convert field types (e.g. @T@ becomes @AsRPC T@).
    -- 3. Replace the Rep's module name with the name of the module of where this Q is being spliced.
    convertRep :: String -> TySynEqn -> Type
    convertRep currentModuleName (TySynEqn _tyVars _lhs rhs) = go rhs
      where
        go :: Type -> Type
        go = \case
          -- Rename type name and module name
          PromotedT t `AppT` LitT (StrTyLit tyName) `AppT` LitT (StrTyLit _moduleName)
            | t == 'G.MetaData
            -> PromotedT t `AppT` LitT (StrTyLit (convertNameStr tyName)) `AppT` LitT (StrTyLit currentModuleName)
          -- Rename constructor names
          PromotedT t `AppT` LitT (StrTyLit conName)
            | t == 'G.MetaCons
            -> PromotedT t `AppT` LitT (StrTyLit (convertNameStr conName))
          -- Rename field names
          PromotedT t `AppT` (PromotedT just `AppT` LitT (StrTyLit fieldName))
            | t == 'G.MetaSel
            -> PromotedT t `AppT` (PromotedT just `AppT` LitT (StrTyLit (convertNameStr fieldName)))
          -- Replace field type @T@ with @AsRPC T@
          ConT x `AppT` fieldType
            | x == ''G.Rec0
            -> ConT x `AppT` convertFieldType fieldType
          x `AppT` y -> go x `AppT` go y
          x -> x

    -- | Lookup the generic 'Rep' type instance for the given type.
    reifyRepInstance :: Name -> Type -> Q TySynEqn
    reifyRepInstance name tp =
      reifyInstances ''G.Rep [tp] >>= \case
        [TySynInstD repInstance] -> pure repInstance
        (_:_) -> fail $ "Found multiple instances of 'Generic' for '" <> show name <> "'."
        [] -> fail $ "Type '" <> show name <> "' must implement 'Generic'."

    -- | Given the type @Foo a b = Foo a@, generate an 'IsoValue' instance like:
    --
    -- > deriving anyclass instance IsoValue (AsRPC a) => IsoValue (FooRPC a b)
    --
    -- Note that if a type variable @t@ is a phantom type variable, then no @IsoValue (AsRPC t)@
    -- constraint is generated for it.
    mkIsoValueInstance :: [Type] -> Type -> Q [Dec]
    mkIsoValueInstance fieldTypes tp =
      one <$> standaloneDerivWithStrategyD (Just AnyclassStrategy) constraints [t|IsoValue $(pure tp)|]
      where
        constraints :: Q Cxt
        constraints =
          cxt $ filter hasTyVar fieldTypes <&> \fieldType ->
            [t|IsoValue $(pure fieldType)|]

        hasTyVar :: Type -> Bool
        hasTyVar ty =
          flip any (universe ty) \case
            VarT _ -> True
            _ -> False

    mkAsRPCInstance :: Type -> Type -> Q [Dec]
    mkAsRPCInstance tp tpRPC =
      [d|
        type instance AsRPC $(pure tp) = $(pure tpRPC)
      |]

----------------------------------------------------------------------------
-- Conversions
----------------------------------------------------------------------------

-- | Replace all big_maps in a value with the respective big_map IDs.
--
-- Throws an error if it finds a big_map without an ID.
valueAsRPC :: HasCallStack => Value t -> Value (AsRPC t)
valueAsRPC v =
  case v of
    VKey {} -> v
    VUnit {} -> v
    VSignature {} -> v
    VChainId {} -> v
    VChest {} -> v
    VChestKey {} -> v
    VOption (vMaybe :: Maybe (Value elem)) ->
      withDict (rpcSingIEvi @elem) $
        VOption $ valueAsRPC <$> vMaybe
    VList (vList :: [Value elem]) ->
      withDict (rpcSingIEvi @elem) $
        VList $ valueAsRPC <$> vList
    VSet {} -> v
    VOp {} -> v
    VContract {} -> v
    VTicket {} -> v
    VPair (x, y) -> VPair (valueAsRPC x, valueAsRPC y)
    VOr (vEither :: Either (Value l) (Value r)) ->
      withDict (rpcSingIEvi @l *** rpcSingIEvi @r) $
        case vEither of
          Right r -> VOr (Right (valueAsRPC r))
          Left l -> VOr (Left (valueAsRPC l))
    VLam {} -> v
    VMap (vMap :: Map (Value k) (Value v)) ->
      withDict (rpcSingIEvi @v) $
        VMap $ valueAsRPC <$> vMap
    VBigMap (Just bmId) _ -> VNat bmId
    VBigMap Nothing _ ->
      error $ unlines
        [ "Expected all big_maps to have an ID, but at least one big_map didn't."
        , "This is most likely a bug."
        ]
    VInt {} -> v
    VNat {} -> v
    VString {} -> v
    VBytes {} -> v
    VMutez {} -> v
    VBool {} -> v
    VKeyHash {} -> v
    VTimestamp {} -> v
    VAddress {} -> v
    VBls12381Fr {} -> v
    VBls12381G1 {} -> v
    VBls12381G2 {} -> v

-- | Replace all @big_map@ annotations in a value with @nat@ annotations.
notesAsRPC :: Notes t -> Notes (AsRPC t)
notesAsRPC notes =
  case notes of
    NTKey {} -> notes
    NTUnit {} -> notes
    NTSignature {} -> notes
    NTChainId {} -> notes
    NTChest {} -> notes
    NTChestKey {} -> notes
    NTOption typeAnn elemNotes -> NTOption typeAnn $ notesAsRPC elemNotes
    NTList typeAnn elemNotes -> NTList typeAnn $ notesAsRPC elemNotes
    NTSet {} -> notes
    NTOperation {} -> notes
    NTContract {} -> notes
    NTTicket {} -> notes
    NTPair typeAnn fieldAnn1 fieldAnn2 varAnn1 varAnn2 notes1 notes2 ->
      NTPair typeAnn fieldAnn1 fieldAnn2 varAnn1 varAnn2 (notesAsRPC notes1) (notesAsRPC notes2)
    NTOr typeAnn fieldAnn1 fieldAnn2 notes1 notes2 ->
      NTOr typeAnn fieldAnn1 fieldAnn2 (notesAsRPC notes1) (notesAsRPC notes2)
    NTLambda {} -> notes
    NTMap typeAnn keyAnns valueNotes -> NTMap typeAnn keyAnns (notesAsRPC valueNotes)
    NTBigMap typeAnn _ _ -> NTNat typeAnn
    NTInt {} -> notes
    NTNat {} -> notes
    NTString {} -> notes
    NTBytes {} -> notes
    NTMutez {} -> notes
    NTBool {} -> notes
    NTKeyHash {} -> notes
    NTTimestamp {} -> notes
    NTAddress {} -> notes
    NTBls12381Fr {} -> notes
    NTBls12381G1 {} -> notes
    NTBls12381G2 {} -> notes
    NTNever {} -> notes

----------------------------------------------------------------------------
-- Entailments
----------------------------------------------------------------------------

-- | A proof that if a singleton exists for @t@,
-- then so it does for @AsRPC t@.
rpcSingIEvi :: forall (t :: T). SingI t :- SingI (AsRPC t)
rpcSingIEvi =
  Sub $
    case sing @t of
      STKey -> Dict
      STUnit {} -> Dict
      STSignature {} -> Dict
      STChainId {} -> Dict
      STChest {} -> Dict
      STChestKey {} -> Dict
      STOption (s :: Sing elem) -> withSingI s $ Dict \\ rpcSingIEvi @elem
      STList (s :: Sing elem) -> withSingI s $  Dict \\ rpcSingIEvi @elem
      STSet (s :: Sing elem) -> withSingI s $ Dict \\ rpcSingIEvi @elem
      STOperation {} -> Dict
      STContract {} -> Dict
      STTicket {} -> Dict
      STPair (sa :: Sing a) (sb :: Sing b) ->
        withSingI sa $ withSingI sb $
          Dict \\ rpcSingIEvi @a \\ rpcSingIEvi @b
      STOr (sl :: Sing l) (sr :: Sing r) ->
        withSingI sl $ withSingI sr $
          Dict \\ rpcSingIEvi @l \\ rpcSingIEvi @r
      STLambda {} -> Dict
      STMap (sk :: Sing k) (sv :: Sing v) ->
        withSingI sk $ withSingI sv $
          Dict \\ rpcSingIEvi @k \\ rpcSingIEvi @v
      STBigMap {} -> Dict
      STInt {} -> Dict
      STNat {} -> Dict
      STString {} -> Dict
      STBytes {} -> Dict
      STMutez {} -> Dict
      STBool {} -> Dict
      STKeyHash {} -> Dict
      STBls12381Fr {} -> Dict
      STBls12381G1 {} -> Dict
      STBls12381G2 {} -> Dict
      STTimestamp {} -> Dict
      STAddress {} -> Dict
      STNever {} -> Dict

-- | A proof that if @t@ does not contain any operations, then neither does @AsRPC t@.
rpcHasNoOpEvi :: forall (t :: T). (SingI t, HasNoOp t) => HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi = rpcHasNoOpEvi' sing

rpcHasNoOpEvi'
  :: HasNoOp t
  => Sing t
  -> HasNoOp t :- HasNoOp (AsRPC t)
rpcHasNoOpEvi' sng = Sub $ case sng of
  STKey -> Dict
  STUnit {} -> Dict
  STSignature {} -> Dict
  STChainId {} -> Dict
  STChest {} -> Dict
  STChestKey {} -> Dict
  STOption s -> Dict \\ rpcHasNoOpEvi' s
  STList s -> Dict \\ rpcHasNoOpEvi' s
  STSet s -> Dict \\ rpcHasNoOpEvi' s
  STContract {} -> Dict
  STTicket {} -> Dict
  STPair sa sb -> case checkOpPresence sa of
    OpAbsent -> Dict \\ rpcHasNoOpEvi' sa \\ rpcHasNoOpEvi' sb
  STOr sl sr -> case checkOpPresence sl of
    OpAbsent -> Dict \\ rpcHasNoOpEvi' sl \\ rpcHasNoOpEvi' sr
  STLambda {} -> Dict
  STMap _ sv -> case checkOpPresence sv of
    OpAbsent -> Dict \\ rpcHasNoOpEvi' sv
  STBigMap {} -> Dict
  STInt {} -> Dict
  STNat {} -> Dict
  STString {} -> Dict
  STBytes {} -> Dict
  STMutez {} -> Dict
  STBool {} -> Dict
  STKeyHash {} -> Dict
  STBls12381Fr {} -> Dict
  STBls12381G1 {} -> Dict
  STBls12381G2 {} -> Dict
  STTimestamp {} -> Dict
  STAddress {} -> Dict
  STNever {} -> Dict

-- | A proof that @AsRPC (Value t)@ does not contain big_maps.
rpcHasNoBigMapEvi :: forall (t :: T). SingI t => Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi = rpcHasNoBigMapEvi' (sing @t)

rpcHasNoBigMapEvi' :: Sing t -> Dict (HasNoBigMap (AsRPC t))
rpcHasNoBigMapEvi' = \case
  STKey -> Dict
  STUnit {} -> Dict
  STSignature {} -> Dict
  STChainId {} -> Dict
  STChest {} -> Dict
  STChestKey {} -> Dict
  STOption s -> Dict \\ rpcHasNoBigMapEvi' s
  STList s -> Dict \\ rpcHasNoBigMapEvi' s
  STSet s -> Dict \\ rpcHasNoBigMapEvi' s
  STOperation {} -> Dict
  STContract {} -> Dict
  STTicket {} -> Dict
  STPair sa sb -> Dict \\ rpcHasNoBigMapEvi' sa \\ rpcHasNoBigMapEvi' sb
  STOr sl sr -> Dict \\ rpcHasNoBigMapEvi' sl \\ rpcHasNoBigMapEvi' sr
  STLambda {} -> Dict
  STMap sk sv -> Dict \\ rpcHasNoBigMapEvi' sk \\ rpcHasNoBigMapEvi' sv
  STBigMap {} -> Dict
  STInt {} -> Dict
  STNat {} -> Dict
  STString {} -> Dict
  STBytes {} -> Dict
  STMutez {} -> Dict
  STBool {} -> Dict
  STKeyHash {} -> Dict
  STBls12381Fr {} -> Dict
  STBls12381G1 {} -> Dict
  STBls12381G2 {} -> Dict
  STTimestamp {} -> Dict
  STAddress {} -> Dict
  STNever {} -> Dict

-- | A proof that @AsRPC (Value t)@ does not contain big_maps.
rpcHasNoNestedBigMapsEvi
  :: forall (t :: T).
     SingI t
  => Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi = rpcHasNoNestedBigMapsEvi' (sing @t)

rpcHasNoNestedBigMapsEvi' :: Sing t -> Dict (HasNoNestedBigMaps (AsRPC t))
rpcHasNoNestedBigMapsEvi' = \case
  STKey -> Dict
  STUnit {} -> Dict
  STSignature {} -> Dict
  STChainId {} -> Dict
  STChest {} -> Dict
  STChestKey {} -> Dict
  STOption s -> Dict \\ rpcHasNoNestedBigMapsEvi' s
  STList s -> Dict \\ rpcHasNoNestedBigMapsEvi' s
  STSet s -> Dict \\ rpcHasNoNestedBigMapsEvi' s
  STOperation {} -> Dict
  STContract {} -> Dict
  STTicket {} -> Dict
  STPair sa sb ->
    Dict \\ rpcHasNoNestedBigMapsEvi' sa \\ rpcHasNoNestedBigMapsEvi' sb
  STOr sl sr ->
    Dict \\ rpcHasNoNestedBigMapsEvi' sl \\ rpcHasNoNestedBigMapsEvi' sr
  STLambda {} -> Dict
  STMap sk sv ->
    Dict \\ rpcHasNoNestedBigMapsEvi' sk \\ rpcHasNoNestedBigMapsEvi' sv
  STBigMap {} -> Dict
  STInt {} -> Dict
  STNat {} -> Dict
  STString {} -> Dict
  STBytes {} -> Dict
  STMutez {} -> Dict
  STBool {} -> Dict
  STKeyHash {} -> Dict
  STBls12381Fr {} -> Dict
  STBls12381G1 {} -> Dict
  STBls12381G2 {} -> Dict
  STTimestamp {} -> Dict
  STAddress {} -> Dict
  STNever {} -> Dict

-- | A proof that if @t@ does not contain any contract values, then neither does @AsRPC t@.
rpcHasNoContractEvi
  :: forall (t :: T).
     (SingI t, HasNoContract t)
  => HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi = rpcHasNoContractEvi' sing

rpcHasNoContractEvi'
  :: HasNoContract t
  => Sing t
  -> HasNoContract t :- HasNoContract (AsRPC t)
rpcHasNoContractEvi' sng = Sub $ case sng of
  STKey -> Dict
  STUnit {} -> Dict
  STSignature {} -> Dict
  STChainId {} -> Dict
  STChest {} -> Dict
  STChestKey {} -> Dict
  STOption s -> Dict \\ rpcHasNoContractEvi' s
  STList s -> Dict \\ rpcHasNoContractEvi' s
  STSet _ -> Dict
  STOperation {} -> Dict
  STTicket {} -> Dict
  STPair sa sb -> case checkContractTypePresence sa of
    ContractAbsent ->
      Dict \\ rpcHasNoContractEvi' sa \\ rpcHasNoContractEvi' sb
  STOr sl sr -> case checkContractTypePresence sl of
    ContractAbsent ->
      Dict \\ rpcHasNoContractEvi' sl \\ rpcHasNoContractEvi' sr
  STLambda {} -> Dict
  STMap _ sv -> Dict \\ rpcHasNoContractEvi' sv
  STBigMap {} -> Dict
  STInt {} -> Dict
  STNat {} -> Dict
  STString {} -> Dict
  STBytes {} -> Dict
  STMutez {} -> Dict
  STBool {} -> Dict
  STKeyHash {} -> Dict
  STBls12381Fr {} -> Dict
  STBls12381G1 {} -> Dict
  STBls12381G2 {} -> Dict
  STTimestamp {} -> Dict
  STAddress {} -> Dict
  STNever {} -> Dict

-- | A proof that if @t@ is a valid storage type, then so is @AsRPC t@.
rpcStorageScopeEvi :: forall (t :: T). StorageScope t :- StorageScope (AsRPC t)
rpcStorageScopeEvi =
  Sub $ Dict
    \\ rpcSingIEvi @t
    \\ rpcHasNoOpEvi @t
    \\ rpcHasNoNestedBigMapsEvi @t
    \\ rpcHasNoContractEvi @t