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

{-# OPTIONS_GHC -fno-warn-orphans #-}

-- | Module, providing singleton boilerplate for
-- 'T' data types.
--
-- Some functions from Data.Singletons are provided alternative version here.
-- Some instances which are usually generated with TH are manually implemented
-- as they require some specific constraints, namely 'Typeable' and/or
-- 'Converge', not provided in instances generated by TH.

module Michelson.Typed.Sing
  ( SingT (..)
  , KnownT
  , withSomeSingT
  , fromSingT
  ) where

import Data.Singletons (Sing, SingI(..), SingKind(..), SomeSing(..))

import Michelson.Typed.T (T(..))


-- | Instance of data family 'Sing' for 'T'.
-- Custom instance is implemented in order to inject 'Typeable'
-- constraint for some of constructors.
data SingT :: T -> Type where
  STKey :: SingT  'TKey
  STUnit :: SingT  'TUnit
  STSignature :: SingT  'TSignature
  STChainId :: SingT  'TChainId
  STOption :: KnownT a => Sing a -> SingT ( 'TOption a)
  STList :: KnownT a => Sing a -> SingT ( 'TList a )
  STSet :: KnownT a => Sing a -> SingT ( 'TSet a )
  STOperation  :: SingT 'TOperation
  STContract   :: (KnownT a)
               => Sing a -> SingT ( 'TContract a )
  STPair       :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TPair a b)
  STOr         :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TOr a b)
  STLambda     :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TLambda a b)
  STMap        :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TMap a b)
  STBigMap     :: (KnownT a, KnownT b)
               => Sing a -> Sing b -> SingT ('TBigMap a b)
  STInt :: SingT  'TInt
  STNat :: SingT  'TNat
  STString :: SingT  'TString
  STBytes :: SingT  'TBytes
  STMutez :: SingT  'TMutez
  STBool :: SingT  'TBool
  STKeyHash :: SingT  'TKeyHash
  STBls12381Fr :: SingT  'TBls12381Fr
  STBls12381G1 :: SingT  'TBls12381G1
  STBls12381G2 :: SingT  'TBls12381G2
  STTimestamp :: SingT  'TTimestamp
  STAddress :: SingT  'TAddress
  STNever :: SingT  'TNever

type instance Sing = SingT

---------------------------------------------
-- Singleton-related helpers for T
--------------------------------------------

-- | 'Typeable' + 'SingI' constraints.
--
-- This restricts a type to be a constructible type of 'T' kind.
class (Typeable t, SingI t) => KnownT (t :: T)
instance (Typeable t, SingI t) => KnownT t

-- | Version of 'SomeSing' with 'Typeable' constraint,
-- specialized for use with 'T' kind.
data SomeSingT where
  SomeSingT :: forall (a :: T). (KnownT a)
            => Sing a -> SomeSingT

-- | Version of 'withSomeSing' with 'Typeable' constraint
-- provided to processing function.
--
-- Required for not to erase these useful constraints when doing
-- conversion from value of type 'T' to its singleton representation.
withSomeSingT
  :: T
  -> (forall (a :: T). (KnownT a) => Sing a -> r)
  -> r
withSomeSingT :: T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t forall (a :: T). KnownT a => Sing a -> r
f = (\(SomeSingT Sing a
s) -> Sing a -> r
forall (a :: T). KnownT a => Sing a -> r
f Sing a
s) (T -> SomeSingT
toSingT T
t)

-- | Version of 'fromSing' specialized for use with
-- @data instance Sing :: T -> Type@ which requires 'Typeable'
-- constraint for some of its constructors
fromSingT :: Sing (a :: T) -> T
fromSingT :: Sing a -> T
fromSingT = \case
  Sing a
STKey -> T
TKey
  Sing a
STUnit -> T
TUnit
  Sing a
STSignature -> T
TSignature
  Sing a
STChainId -> T
TChainId
  STOption t -> T -> T
TOption (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
  STList t -> T -> T
TList (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
  STSet t -> T -> T
TSet (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
  Sing a
STOperation -> T
TOperation
  STContract t -> T -> T
TContract (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
t)
  STPair a b -> T -> T -> T
TPair (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
  STOr a b -> T -> T -> T
TOr (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
  STLambda a b -> T -> T -> T
TLambda (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
  STMap a b -> T -> T -> T
TMap (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
  STBigMap a b -> T -> T -> T
TBigMap (Sing a -> T
forall (a :: T). Sing a -> T
fromSingT Sing a
a) (Sing b -> T
forall (a :: T). Sing a -> T
fromSingT Sing b
b)
  Sing a
STInt -> T
TInt
  Sing a
STNat -> T
TNat
  Sing a
STString -> T
TString
  Sing a
STBytes -> T
TBytes
  Sing a
STMutez -> T
TMutez
  Sing a
STBool -> T
TBool
  Sing a
STKeyHash -> T
TKeyHash
  Sing a
STBls12381Fr -> T
TBls12381Fr
  Sing a
STBls12381G1 -> T
TBls12381G1
  Sing a
STBls12381G2 -> T
TBls12381G2
  Sing a
STTimestamp -> T
TTimestamp
  Sing a
STAddress -> T
TAddress
  Sing a
STNever -> T
TNever

-- | Version of 'toSing' which creates 'SomeSingT'.
toSingT :: T -> SomeSingT
toSingT :: T -> SomeSingT
toSingT = \case
  T
TKey -> Sing 'TKey -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TKey
SingT 'TKey
STKey
  T
TUnit -> Sing 'TUnit -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TUnit
SingT 'TUnit
STUnit
  T
TSignature -> Sing 'TSignature -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TSignature
SingT 'TSignature
STSignature
  T
TChainId -> Sing 'TChainId -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TChainId
SingT 'TChainId
STChainId
  TOption T
t -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
tSing -> Sing ('TOption a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TOption a) -> SomeSingT) -> Sing ('TOption a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TOption a)
forall (a :: T). KnownT a => Sing a -> SingT ('TOption a)
STOption Sing a
tSing
  TList T
t -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
tSing -> Sing ('TList a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TList a) -> SomeSingT) -> Sing ('TList a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TList a)
forall (a :: T). KnownT a => Sing a -> SingT ('TList a)
STList Sing a
tSing
  TSet T
ct -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
ct ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
ctSing -> Sing ('TSet a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TSet a) -> SomeSingT) -> Sing ('TSet a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TSet a)
forall (a :: T). KnownT a => Sing a -> SingT ('TSet a)
STSet Sing a
ctSing
  T
TOperation -> Sing 'TOperation -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TOperation
SingT 'TOperation
STOperation
  TContract T
t -> T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
t ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
tSing -> Sing ('TContract a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TContract a) -> SomeSingT)
-> Sing ('TContract a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> SingT ('TContract a)
forall (a :: T). KnownT a => Sing a -> SingT ('TContract a)
STContract Sing a
tSing
  TPair T
l T
r ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
lSing ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
rSing ->
      Sing ('TPair a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TPair a a) -> SomeSingT) -> Sing ('TPair a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TPair a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TPair a a)
STPair Sing a
lSing Sing a
rSing
  TOr T
l T
r ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
lSing ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
rSing ->
      Sing ('TOr a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TOr a a) -> SomeSingT) -> Sing ('TOr a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TOr a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TOr a a)
STOr Sing a
lSing Sing a
rSing
  TLambda T
l T
r ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
lSing ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
rSing ->
      Sing ('TLambda a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TLambda a a) -> SomeSingT)
-> Sing ('TLambda a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TLambda a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TLambda a a)
STLambda Sing a
lSing Sing a
rSing
  TMap T
l T
r ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
lSing ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
rSing ->
      Sing ('TMap a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TMap a a) -> SomeSingT) -> Sing ('TMap a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TMap a a)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TMap a a)
STMap Sing a
lSing Sing a
rSing
  TBigMap T
l T
r ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
l ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
lSing ->
    T
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall r. T -> (forall (a :: T). KnownT a => Sing a -> r) -> r
withSomeSingT T
r ((forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT)
-> (forall (a :: T). KnownT a => Sing a -> SomeSingT) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ \Sing a
rSing ->
      Sing ('TBigMap a a) -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT (Sing ('TBigMap a a) -> SomeSingT)
-> Sing ('TBigMap a a) -> SomeSingT
forall a b. (a -> b) -> a -> b
$ Sing a -> Sing a -> SingT ('TBigMap a a)
forall (a :: T) (b :: T).
(KnownT a, KnownT b) =>
Sing a -> Sing b -> SingT ('TBigMap a b)
STBigMap Sing a
lSing Sing a
rSing
  T
TInt -> Sing 'TInt -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TInt
SingT 'TInt
STInt
  T
TNat -> Sing 'TNat -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TNat
SingT 'TNat
STNat
  T
TString -> Sing 'TString -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TString
SingT 'TString
STString
  T
TBytes -> Sing 'TBytes -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBytes
SingT 'TBytes
STBytes
  T
TMutez -> Sing 'TMutez -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TMutez
SingT 'TMutez
STMutez
  T
TBool -> Sing 'TBool -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBool
SingT 'TBool
STBool
  T
TKeyHash -> Sing 'TKeyHash -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TKeyHash
SingT 'TKeyHash
STKeyHash
  T
TBls12381Fr -> Sing 'TBls12381Fr -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBls12381Fr
SingT 'TBls12381Fr
STBls12381Fr
  T
TBls12381G1 -> Sing 'TBls12381G1 -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBls12381G1
SingT 'TBls12381G1
STBls12381G1
  T
TBls12381G2 -> Sing 'TBls12381G2 -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TBls12381G2
SingT 'TBls12381G2
STBls12381G2
  T
TTimestamp -> Sing 'TTimestamp -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TTimestamp
SingT 'TTimestamp
STTimestamp
  T
TAddress -> Sing 'TAddress -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TAddress
SingT 'TAddress
STAddress
  T
TNever -> Sing 'TNever -> SomeSingT
forall (a :: T). KnownT a => Sing a -> SomeSingT
SomeSingT Sing 'TNever
SingT 'TNever
STNever

instance SingKind T where
  type Demote T = T
  fromSing :: Sing a -> Demote T
fromSing  = Sing a -> Demote T
forall (a :: T). Sing a -> T
fromSingT
  toSing :: Demote T -> SomeSing T
toSing Demote T
t = case T -> SomeSingT
toSingT Demote T
T
t of SomeSingT Sing a
s -> Sing a -> SomeSing T
forall k (a :: k). Sing a -> SomeSing k
SomeSing Sing a
s

instance SingI  'TKey where
  sing :: Sing 'TKey
sing = Sing 'TKey
SingT 'TKey
STKey
instance SingI  'TUnit where
  sing :: Sing 'TUnit
sing = Sing 'TUnit
SingT 'TUnit
STUnit
instance SingI  'TSignature where
  sing :: Sing 'TSignature
sing = Sing 'TSignature
SingT 'TSignature
STSignature
instance SingI  'TChainId where
  sing :: Sing 'TChainId
sing = Sing 'TChainId
SingT 'TChainId
STChainId
instance SingI  'TNever where
  sing :: Sing 'TNever
sing = Sing 'TNever
SingT 'TNever
STNever
instance (KnownT a) => SingI ( 'TOption (a :: T)) where
  sing :: Sing ('TOption a)
sing = Sing a -> SingT ('TOption a)
forall (a :: T). KnownT a => Sing a -> SingT ('TOption a)
STOption Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a) => SingI ( 'TList (a :: T)) where
  sing :: Sing ('TList a)
sing = Sing a -> SingT ('TList a)
forall (a :: T). KnownT a => Sing a -> SingT ('TList a)
STList Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a) => SingI ( 'TSet (a :: T)) where
  sing :: Sing ('TSet a)
sing = Sing a -> SingT ('TSet a)
forall (a :: T). KnownT a => Sing a -> SingT ('TSet a)
STSet Sing a
forall k (a :: k). SingI a => Sing a
sing
instance SingI 'TOperation where
  sing :: Sing 'TOperation
sing = Sing 'TOperation
SingT 'TOperation
STOperation
instance (KnownT a) =>
          SingI ( 'TContract (a :: T)) where
  sing :: Sing ('TContract a)
sing = Sing a -> SingT ('TContract a)
forall (a :: T). KnownT a => Sing a -> SingT ('TContract a)
STContract Sing a
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TPair a b) where
  sing :: Sing ('TPair a b)
sing = Sing a -> Sing b -> SingT ('TPair a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TPair a a)
STPair Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TOr a b) where
  sing :: Sing ('TOr a b)
sing = Sing a -> Sing b -> SingT ('TOr a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TOr a a)
STOr Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TLambda a b) where
  sing :: Sing ('TLambda a b)
sing = Sing a -> Sing b -> SingT ('TLambda a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TLambda a a)
STLambda Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TMap a b) where
  sing :: Sing ('TMap a b)
sing = Sing a -> Sing b -> SingT ('TMap a b)
forall (a :: T) (a :: T).
(KnownT a, KnownT a) =>
Sing a -> Sing a -> SingT ('TMap a a)
STMap Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance (KnownT a, KnownT b) =>
          SingI ( 'TBigMap a b) where
  sing :: Sing ('TBigMap a b)
sing = Sing a -> Sing b -> SingT ('TBigMap a b)
forall (a :: T) (b :: T).
(KnownT a, KnownT b) =>
Sing a -> Sing b -> SingT ('TBigMap a b)
STBigMap Sing a
forall k (a :: k). SingI a => Sing a
sing Sing b
forall k (a :: k). SingI a => Sing a
sing
instance SingI  'TInt where
  sing :: Sing 'TInt
sing = Sing 'TInt
SingT 'TInt
STInt
instance SingI  'TNat where
  sing :: Sing 'TNat
sing = Sing 'TNat
SingT 'TNat
STNat
instance SingI  'TString where
  sing :: Sing 'TString
sing = Sing 'TString
SingT 'TString
STString
instance SingI  'TBytes where
  sing :: Sing 'TBytes
sing = Sing 'TBytes
SingT 'TBytes
STBytes
instance SingI  'TMutez where
  sing :: Sing 'TMutez
sing = Sing 'TMutez
SingT 'TMutez
STMutez
instance SingI  'TBool where
  sing :: Sing 'TBool
sing = Sing 'TBool
SingT 'TBool
STBool
instance SingI  'TKeyHash where
  sing :: Sing 'TKeyHash
sing = Sing 'TKeyHash
SingT 'TKeyHash
STKeyHash
instance SingI  'TBls12381Fr where
  sing :: Sing 'TBls12381Fr
sing = Sing 'TBls12381Fr
SingT 'TBls12381Fr
STBls12381Fr
instance SingI  'TBls12381G1 where
  sing :: Sing 'TBls12381G1
sing = Sing 'TBls12381G1
SingT 'TBls12381G1
STBls12381G1
instance SingI  'TBls12381G2 where
  sing :: Sing 'TBls12381G2
sing = Sing 'TBls12381G2
SingT 'TBls12381G2
STBls12381G2
instance SingI  'TTimestamp where
  sing :: Sing 'TTimestamp
sing = Sing 'TTimestamp
SingT 'TTimestamp
STTimestamp
instance SingI  'TAddress where
  sing :: Sing 'TAddress
sing = Sing 'TAddress
SingT 'TAddress
STAddress