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

-- | 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.AsRPC
  ( TAsRPC
  , HasRPCRepr(..)
  , MaybeRPC(..)
  , deriveRPC
  , deriveRPCWithStrategy
  , deriveManyRPC
  , deriveManyRPCWithStrategy
  -- * Conversions
  , valueAsRPC
  , replaceBigMapIds
  , notesAsRPC
  -- * Entailments
  , rpcSingIEvi
  , rpcHasNoOpEvi
  , rpcHasNoBigMapEvi
  , rpcHasNoNestedBigMapsEvi
  , rpcHasNoContractEvi
  , rpcStorageScopeEvi
  ) where

import Prelude hiding (Type)
import Prelude qualified

import Control.Lens.Plated (universe)
import Data.Constraint (Dict(..), (***), (:-)(Sub), (\\))
import Data.List qualified as List ((\\))
import Data.Singletons (Sing, withSingI)
import GHC.Generics qualified 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, instanceD, location, mkName, nameBase, ppr, reify,
  reifyInstances, standaloneDerivWithStrategyD)
import Language.Haskell.TH.ReifyMany (reifyManyTyCons)
import Language.Haskell.TH.ReifyMany.Internal (decConcreteNames)

import Morley.Micheline (ToExpression(..))
import Morley.Michelson.Text (MText)
import Morley.Michelson.Typed
  (BigMap, BigMapId, ContractPresence(ContractAbsent), ContractRef, EpAddress, HasNoBigMap,
  HasNoContract, HasNoNestedBigMaps, HasNoOp, IsoValue, Notes(..), OpPresence(..), Operation,
  SingI(sing), SingT(..), StorageScope, T(..), ToT, Value, Value'(..), WellTyped,
  checkContractTypePresence, checkOpPresence, toVal, withDict)
import Morley.Tezos.Address (Address)
import Morley.Tezos.Core (ChainId, Mutez, Timestamp)
import Morley.Tezos.Crypto
import Morley.Util.CustomGeneric
  (GenericStrategy, customGeneric', deriveFullType, haskellBalanced, reifyDataType)
import Morley.Util.Named hiding (Name)
import Morley.Util.TH (isTypeAlias, lookupTypeNameOrFail)

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

-- $setup
-- >>> import Morley.Michelson.Typed (T(..), BigMap, mkBigMap)
-- >>> import Morley.Michelson.Typed.Haskell.Value (BigMapId(..))
-- >>> import Morley.Michelson.Text (MText)

----------------------------------------------------------------------------
-- TAsRPC
----------------------------------------------------------------------------

{- | A type-level function that maps a Michelson type to its Tezos RPC representation.

For example, when we retrieve a contract's storage using the Tezos RPC,
all its @big_map@s will be replaced by @nat@, representing a big_map ID.

>>> :k! TAsRPC ('TBigMap 'TInt 'TString)
...
= 'TNat

>>> :k! TAsRPC ('TList ('TBigMap 'TInt 'TString))
...
= 'TList 'TNat

>>> :k! TAsRPC ('TPair 'TString ('TPair 'TAddress ('TBigMap 'TInt 'TString)))
...
= 'TPair 'TString ('TPair 'TAddress 'TNat)


NB: As far as we are aware, details of RPC representation of Michelson
types are not documented. We know empirically that @big_map@s are
represented as their ids, and are the only type with an explicitly
different representation.

Whether @TAsRPC@ needs to propagate into type parameters then depends on
whether a value can hold big_map values.

* Values of type @option a@, @list a@, @pair a b@, and @or a b@ can
  contain big_map values, so their RPC representations are @option (TAsRPC a)@,
  @list (TAsRPC a)@, @pair (TAsRPC a) (TAsRPC b)@ and @or (TAsRPC a) (TAsRPC b)@.
* The keys of a @map k v@ cannot be big_maps, but the values can, so its
  RPC representation is @map k (TAsRPC v)@.
* Values of type @set a@ cannot contain big_maps, so its RPC
  representation is just @set a@.
* Values of type @contract a@ cannot contain big_maps either, because
  it's just a wrapper for an address and an entrypoint name, so its RPC
  representation is just @contract a@. The same reasoning applies to
  @ticket a@ and @lambda a b@.

-}
type TAsRPC :: T -> T
type family TAsRPC t where
  TAsRPC 'TKey = 'TKey
  TAsRPC 'TUnit = 'TUnit
  TAsRPC 'TSignature = 'TSignature
  TAsRPC 'TChainId = 'TChainId
  TAsRPC ('TOption t) = 'TOption (TAsRPC t)
  TAsRPC ('TList t) = 'TList (TAsRPC t)
  TAsRPC ('TSet t) = 'TSet t
  TAsRPC 'TOperation = 'TOperation
  TAsRPC ('TContract t) = 'TContract t
  TAsRPC ('TTicket t) = 'TTicket t
  TAsRPC ('TPair t1 t2) = 'TPair (TAsRPC t1) (TAsRPC t2)
  TAsRPC ('TOr t1 t2) = 'TOr (TAsRPC t1) (TAsRPC t2)
  TAsRPC ('TLambda t1 t2) = 'TLambda t1 t2
  TAsRPC ('TMap k v) = 'TMap k (TAsRPC v)
  TAsRPC ('TBigMap _ _) = 'TNat
  TAsRPC 'TInt = 'TInt
  TAsRPC 'TNat = 'TNat
  TAsRPC 'TString = 'TString
  TAsRPC 'TBytes = 'TBytes
  TAsRPC 'TMutez = 'TMutez
  TAsRPC 'TBool = 'TBool
  TAsRPC 'TKeyHash = 'TKeyHash
  TAsRPC 'TTimestamp = 'TTimestamp
  TAsRPC 'TAddress = 'TAddress
  TAsRPC 'TNever = 'TNever
  TAsRPC 'TBls12381Fr = 'TBls12381Fr
  TAsRPC 'TBls12381G1 = 'TBls12381G1
  TAsRPC 'TBls12381G2 = 'TBls12381G2
  TAsRPC 'TChest = 'TChest
  TAsRPC 'TChestKey = 'TChestKey
  TAsRPC ('TSaplingState n) = ('TSaplingState n)
  TAsRPC ('TSaplingTransaction n) = ('TSaplingTransaction n)

----------------------------------------------------------------------------
-- 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 must hold:

> TAsRPC (ToT t) ~ ToT (AsRPC t)

In other words, `ToT` and `AsRPC`/`TAsRPC` must be commutative.

@
   Storage ----------(applying ToT)-------------> ToT Storage
      |                                                |
      |                                                |
      |                                                |
(applying AsRPC)                                (applying TAsRPC)
      |                                                |
      |                                                |
      |                                                |
      |                                                V
      |                                        TAsRPC (ToT Storage)
      V                                                ~
AsRPC Storage ------(applying ToT)-----------> ToT (AsRPC Storage)
@


This law ensures that we can go from some type @Storage@ to @AsRPC Storage@ by
composing @fromVal . valueAsRPC . toVal@.

@
   Storage ------------(toVal)--------------> Value (ToT Storage)
      |                                                |
      |                                                |
      |                                                |
(fromVal . valueAsRPC . toVal)                    (valueAsRPC)
      |                                                |
      |                                                |
      |                                                |
      |                                                V
      |                                   Value (TAsRPC (ToT Storage))
      V                                                ~
AsRPC Storage <--------(fromVal)--------- Value (ToT (AsRPC Storage))
@

-}
class (TAsRPC (ToT t) ~ ToT (AsRPC t)) => HasRPCRepr (t :: Prelude.Type) where
  type AsRPC t :: Prelude.Type

-- 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)@
instance HasRPCRepr (BigMap k v) where type AsRPC (BigMap k v) = BigMapId k v
instance HasRPCRepr (Value t) where type AsRPC (Value t) = Value (TAsRPC t)
instance HasRPCRepr Integer where type AsRPC Integer = Integer
instance HasRPCRepr Natural where type AsRPC Natural = Natural
instance HasRPCRepr MText where type AsRPC MText = MText
instance HasRPCRepr Bool where type AsRPC Bool = Bool
instance HasRPCRepr ByteString where type AsRPC ByteString = ByteString
instance HasRPCRepr Mutez where type AsRPC Mutez = Mutez
instance HasRPCRepr KeyHash where type AsRPC KeyHash = KeyHash
instance HasRPCRepr Timestamp where type AsRPC Timestamp = Timestamp
instance HasRPCRepr Address where type AsRPC Address = Address
instance HasRPCRepr EpAddress where type AsRPC EpAddress = EpAddress
instance HasRPCRepr PublicKey where type AsRPC PublicKey = PublicKey
instance HasRPCRepr Signature where type AsRPC Signature = Signature
instance HasRPCRepr ChainId where type AsRPC ChainId = ChainId
instance HasRPCRepr Bls12381Fr where type AsRPC Bls12381Fr = Bls12381Fr
instance HasRPCRepr Bls12381G1 where type AsRPC Bls12381G1 = Bls12381G1
instance HasRPCRepr Bls12381G2 where type AsRPC Bls12381G2 = Bls12381G2
instance HasRPCRepr () where type AsRPC () = ()
instance HasRPCRepr a => HasRPCRepr [a] where
  type AsRPC [a] = [AsRPC a]
instance HasRPCRepr a => HasRPCRepr (Maybe a) where
  type AsRPC (Maybe a) = Maybe (AsRPC a)
instance (HasRPCRepr l, HasRPCRepr r) => HasRPCRepr (Either l r) where
  type AsRPC (Either l r) = Either (AsRPC l) (AsRPC r)
instance (HasRPCRepr a, HasRPCRepr b) => HasRPCRepr (a, b) where
  type AsRPC (a, b) = (AsRPC a, AsRPC b)
instance HasRPCRepr (Set a) where
  type AsRPC (Set a) = Set a
instance HasRPCRepr v => HasRPCRepr (Map k v) where
  type AsRPC (Map k v) = Map k (AsRPC v)
instance HasRPCRepr Operation where
  type AsRPC Operation = Operation
instance HasRPCRepr a => HasRPCRepr (Identity a) where
  type AsRPC (Identity a) = Identity (AsRPC a)
instance HasRPCRepr a => HasRPCRepr (NamedF Identity a name) where
  type AsRPC (NamedF Identity a name) = NamedF Identity (AsRPC a) name
instance HasRPCRepr a => HasRPCRepr (NamedF Maybe a name) where
  type AsRPC (NamedF Maybe a name) = NamedF Maybe (AsRPC a) name
instance Each '[HasRPCRepr] '[a, b, c] => HasRPCRepr (a, b, c) where
  type AsRPC (a, b, c) = (AsRPC a, AsRPC b, AsRPC c)
instance Each '[HasRPCRepr] '[a, b, c, d] => HasRPCRepr (a, b, c, d) where
  type AsRPC (a, b, c, d) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d)
instance Each '[HasRPCRepr] '[a, b, c, d, e] => HasRPCRepr (a, b, c, d, e) where
  type AsRPC (a, b, c, d, e) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e)
instance Each '[HasRPCRepr] '[a, b, c, d, e, f] => HasRPCRepr (a, b, c, d, e, f) where
  type AsRPC (a, b, c, d, e, f) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f)
instance Each '[HasRPCRepr] '[a, b, c, d, e, f, g] => HasRPCRepr (a, b, c, d, e, f, g) where
  type AsRPC (a, b, c, d, e, f, g) = (AsRPC a, AsRPC b, AsRPC c, AsRPC d, AsRPC e, AsRPC f, AsRPC g)
instance HasRPCRepr (ContractRef arg) where
  type AsRPC (ContractRef arg) = ContractRef arg
instance HasRPCRepr Chest where
  type AsRPC Chest = Chest
instance HasRPCRepr ChestKey where
  type AsRPC ChestKey = ChestKey

----------------------------------------------------------------------------
-- MaybeRPC
----------------------------------------------------------------------------

-- | Represents a value that may or may not be in its RPC representation.
--
-- >>> :t NotRPC @(BigMap Integer MText) (mkBigMap @[(Integer, MText)] [])
-- ...
--   :: MaybeRPC (BigMap Integer MText)
--
-- >>> :t IsRPC @(BigMap Integer MText) (BigMapId 1)
-- ...
--   :: MaybeRPC (BigMap Integer MText)
data MaybeRPC v where
  NotRPC :: IsoValue  v => v -> MaybeRPC v
  IsRPC :: (SingI (ToT v), IsoValue (AsRPC v), HasRPCRepr v) => AsRPC v -> MaybeRPC v

instance HasNoOp (ToT v) => ToExpression (MaybeRPC v) where
  toExpression = \case
    NotRPC v -> toExpression (toVal v)
    IsRPC v -> withDict (rpcHasNoOpEvi @(ToT v)) $ toExpression (toVal v)

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

-- | Derive an RPC representation for a type, as well as instances for 'Generic', 'IsoValue' and 'HasRPCRepr'.
--
-- > 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
-- >   }
-- >
-- > instance HasRPCRepr a => HasRPCRepr (ExampleStorage a b) where
-- >   type 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
  fieldTypes <- getFieldTypes 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
    , one <$> mkAsRPCInstance fieldTypes 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 (ppr 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 (ppr 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 (ppr 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 (Bar a)@, generate an 'IsoValue' instance like:
    --
    -- > deriving anyclass instance IsoValue (AsRPC (Bar 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)|]

    -- | Given the type @Foo a b = Foo (Bar a)@, generate an 'HasRPCRepr' instance like:
    --
    -- > instance HasRPCRepr (Bar a) => HasRPCRepr (Foo a b) where
    -- >   type AsRPC (Foo a b) = FooRPC a b
    --
    -- Note that if a type variable @t@ is a phantom type variable, then no @HasRPCRepr@
    -- constraint is generated for it.
    mkAsRPCInstance :: [Type] -> Type -> Type -> Q Dec
    mkAsRPCInstance fieldTypes tp tpRPC = do
      typeInstance <- [d|type instance AsRPC $(pure tp) = $(pure tpRPC)|]
      instanceD constraints [t|HasRPCRepr $(pure tp)|]
        (pure <$> typeInstance)
      where
        constraints :: Q Cxt
        constraints =
          cxt $ filter hasTyVar fieldTypes <&> \fieldType ->
            [t|HasRPCRepr $(pure fieldType)|]

    -- | Checks if the given type has any type variables.
    hasTyVar :: Type -> Bool
    hasTyVar ty =
      flip any (universe ty) \case
        VarT _ -> True
        _ -> False

----------------------------------------------------------------------------
-- 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 (TAsRPC 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

-- | Replaces all bigmap IDs with their corresponding bigmap values.
-- This is the inverse of `valueAsRPC`.
replaceBigMapIds
  :: forall t m. Monad m
  => (forall k v. (SingI k, SingI v) => Natural -> m (Value ('TBigMap k v)))
  -- ^ A function for looking up a bigmap using its ID.
  -> Sing t -> Value (TAsRPC t) -> m (Value t)
replaceBigMapIds findBigMapById = go
  where
    go :: forall t1. Sing t1 -> Value (TAsRPC t1) -> m (Value t1)
    go s v = case (s, v) of
      (STKey {}, _) -> pure v
      (STUnit {}, _) -> pure v
      (STSignature {}, _) -> pure v
      (STChainId {}, _) -> pure v
      (STChest {}, _) -> pure v
      (STChestKey {}, _) -> pure v
      (STOption sMaybe, VOption vMaybe) ->
        withSingI sMaybe $
          VOption <$> traverse (go sMaybe) vMaybe
      (STList sList, VList vList) ->
        withSingI sList $
          VList <$> traverse (go sList) vList
      (STSet {}, _) -> pure v
      (STOperation {}, _) -> pure v
      (STContract {}, _) -> pure v
      (STTicket {}, _) -> pure v
      (STPair sa sb, VPair (a, b)) -> do
        a' <- go sa a
        b' <- go sb b
        pure $ VPair (a', b')
      (STOr sl sr, VOr vEither) -> withSingI sl $ withSingI sr $
        case vEither of
          Right r -> VOr . Right <$> go sr r
          Left l -> VOr . Left <$> go sl l
      (STLambda {}, _) -> pure v
      (STMap _ sv, VMap vList) ->
        withSingI sv $
          VMap <$> traverse (go sv) vList
      (STBigMap sk sv, VNat bigMapId) -> withSingI sk $ withSingI sv $ findBigMapById bigMapId
      (STInt {}, _) -> pure v
      (STNat {}, _) -> pure v
      (STString {}, _) -> pure v
      (STBytes {}, _) -> pure v
      (STMutez {}, _) -> pure v
      (STBool {}, _) -> pure v
      (STKeyHash {}, _) -> pure v
      (STTimestamp {}, _) -> pure v
      (STAddress {}, _) -> pure v
      (STBls12381Fr {}, _) -> pure v
      (STBls12381G1 {}, _) -> pure v
      (STBls12381G2 {}, _) -> pure v

-- | Replace all @big_map@ annotations in a value with @nat@ annotations.
notesAsRPC :: Notes t -> Notes (TAsRPC 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
    NTSaplingState {} -> notes
    NTSaplingTransaction {} -> notes

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

-- | A proof that if a singleton exists for @t@,
-- then so it does for @TAsRPC t@.
rpcSingIEvi :: forall (t :: T). SingI t :- SingI (TAsRPC 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
      STSaplingState _ -> Dict
      STSaplingTransaction _ -> Dict

-- | A proof that if @t@ is well-typed, then @TAsRPC t@ is also well-typed.
rpcWellTypedEvi :: forall (t :: T). WellTyped t => WellTyped t :- WellTyped (TAsRPC t)
rpcWellTypedEvi = rpcWellTypedEvi' sing

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

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

rpcHasNoOpEvi'
  :: HasNoOp t
  => Sing t
  -> HasNoOp t :- HasNoOp (TAsRPC 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
  STSaplingState {} -> Dict
  STSaplingTransaction {} -> Dict

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

rpcHasNoBigMapEvi' :: Sing t -> Dict (HasNoBigMap (TAsRPC 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
  STSaplingState {} -> Dict
  STSaplingTransaction {} -> Dict

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

rpcHasNoNestedBigMapsEvi' :: Sing t -> Dict (HasNoNestedBigMaps (TAsRPC 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
  STSaplingState {} -> Dict
  STSaplingTransaction {} -> Dict

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

rpcHasNoContractEvi'
  :: HasNoContract t
  => Sing t
  -> HasNoContract t :- HasNoContract (TAsRPC 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
  STSaplingState {} -> Dict
  STSaplingTransaction {} -> Dict

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