Safe Haskell	None
Language	Haskell2010

Michelson.Typed.Scope

Contents

Scopes
Implementation internals
Re-exports

Description

Module, containing restrictions imposed by instruction or value scope.

Michelson have multiple restrictions on values, examples:

operation type cannot appear in parameter.
big_map type cannot appear in PUSH-able constants.
contract type cannot appear in type we UNPACK to.

Thus we declare multiple "scopes" - constraints applied in corresponding situations, for instance

Also we separate multiple "classes" of scope-related constraints.

ParameterScope and similar ones are used within Michelson engine, they are understandable by GHC but produce not very clarifying errors.
ProperParameterBetterErrors and similar ones are middle-layer constraints, they produce human-readable errors but GHC cannot make conclusions from them. They are supposed to be used only by eDSLs to define their own high-level constraints.
Lorentz and other eDSLs may declare their own constraints, in most cases you should use them. For example see Constraints module.

Synopsis

type ConstantScope t = (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t)
type StorageScope t = (KnownT t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t)
type PackedValScope t = (SingI t, HasNoOp t, HasNoBigMap t)
type ParameterScope t = (KnownT t, HasNoOp t, HasNoNestedBigMaps t)
type PrintedValScope t = (SingI t, HasNoOp t)
type UnpackedValScope t = (PackedValScope t, ConstantScope t)
type ProperParameterBetterErrors t = (KnownT t, ForbidOp t, ForbidNestedBigMaps t)
type ProperStorageBetterErrors t = (KnownT t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)
type ProperConstantBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t)
type ProperPackedValBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t)
type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)
type ProperPrintedValBetterErrors t = (SingI t, ForbidOp t)
properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t
properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t
properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t
properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t
properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t
properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t
newtype a :- b = Sub (a => Dict b)
data BadTypeForScope
- = BtNotComparable
- | BtIsOperation
- | BtHasBigMap
- | BtHasNestedBigMap
- | BtHasContract
class CheckScope (c :: Constraint) where
- checkScope :: Either BadTypeForScope (Dict c)
class ContainsBigMap t ~ 'False => HasNoBigMap t
class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t
class ContainsOp t ~ 'False => HasNoOp t
class ContainsContract t ~ 'False => HasNoContract t
type family ContainsBigMap (t :: T) :: Bool where ...
type family ContainsNestedBigMaps (t :: T) :: Bool where ...
type ForbidOp t = FailOnOperationFound (ContainsOp t)
type ForbidContract t = FailOnContractFound (ContainsContract t)
type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)
type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)
type family FailOnBigMapFound (enabled :: Bool) :: Constraint where ...
type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where ...
type family FailOnOperationFound (enabled :: Bool) :: Constraint where ...
data OpPresence (t :: T)
- = ContainsOp t ~ 'True => OpPresent
- | ContainsOp t ~ 'False => OpAbsent
data ContractPresence (t :: T)
- = ContainsContract t ~ 'True => ContractPresent
- | ContainsContract t ~ 'False => ContractAbsent
data BigMapPresence (t :: T)
- = ContainsBigMap t ~ 'True => BigMapPresent
- | ContainsBigMap t ~ 'False => BigMapAbsent
data NestedBigMapsPresence (t :: T)
- = ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
- | ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent
checkOpPresence :: Sing (ty :: T) -> OpPresence ty
checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty
checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty
checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty
opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t)
contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t)
bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t)
nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t)
forbiddenOp :: forall t a. (SingI t, ForbidOp t) => (HasNoOp t => a) -> a
forbiddenContractType :: forall t a. (SingI t, ForbidContract t) => (HasNoContract t => a) -> a
forbiddenBigMap :: forall t a. (SingI t, ForbidBigMap t) => (HasNoBigMap t => a) -> a
forbiddenNestedBigMaps :: forall t a. (SingI t, ForbidNestedBigMaps t) => (HasNoNestedBigMaps t => a) -> a
withDict :: HasDict c e => e -> (c => r) -> r
class SingI (a :: k) where
- sing :: Sing a

Scopes

type ConstantScope t = (SingI t, HasNoOp t, HasNoBigMap t, HasNoContract t) Source #

Alias for constraints which Michelson applies to pushed constants.

type StorageScope t = (KnownT t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) Source #

Alias for constraints which Michelson applies to contract storage.

type PackedValScope t = (SingI t, HasNoOp t, HasNoBigMap t) Source #

Alias for constraints which Michelson applies to packed values.

type ParameterScope t = (KnownT t, HasNoOp t, HasNoNestedBigMaps t) Source #

Alias for constraints which Michelson applies to parameter.

type PrintedValScope t = (SingI t, HasNoOp t) Source #

Alias for constraints which are required for printing.

type UnpackedValScope t = (PackedValScope t, ConstantScope t) Source #

Alias for constraints which Michelson applies to unpacked values.

It is different from PackedValScope, e.g. contract type cannot appear in a value we unpack to.

type ProperParameterBetterErrors t = (KnownT t, ForbidOp t, ForbidNestedBigMaps t) Source #

type ProperStorageBetterErrors t = (KnownT t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t) Source #

type ProperConstantBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidContract t) Source #

type ProperPackedValBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t) Source #

type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t) Source #

type ProperPrintedValBetterErrors t = (SingI t, ForbidOp t) Source #

properParameterEvi :: forall t. ProperParameterBetterErrors t :- ParameterScope t Source #

properStorageEvi :: forall t. ProperStorageBetterErrors t :- StorageScope t Source #

properConstantEvi :: forall t. ProperConstantBetterErrors t :- ConstantScope t Source #

properPackedValEvi :: forall t. ProperPackedValBetterErrors t :- PackedValScope t Source #

properUnpackedValEvi :: forall t. ProperUnpackedValBetterErrors t :- UnpackedValScope t Source #

properPrintedValEvi :: forall t. ProperPrintedValBetterErrors t :- PrintedValScope t Source #

newtype a :- b infixr 9 #

This is the type of entailment.

a :- b is read as a "entails" b.

With this we can actually build a category for Constraint resolution.

e.g.

Because Eq a is a superclass of Ord a, we can show that Ord a entails Eq a.

Because instance Ord a => Ord [a] exists, we can show that Ord a entails Ord [a] as well.

This relationship is captured in the :- entailment type here.

Since p :- p and entailment composes, :- forms the arrows of a Category of constraints. However, Category only became sufficiently general to support this instance in GHC 7.8, so prior to 7.8 this instance is unavailable.

But due to the coherence of instance resolution in Haskell, this Category has some very interesting properties. Notably, in the absence of IncoherentInstances, this category is "thin", which is to say that between any two objects (constraints) there is at most one distinguishable arrow.

This means that for instance, even though there are two ways to derive Ord a :- Eq [a], the answers from these two paths _must_ by construction be equal. This is a property that Haskell offers that is pretty much unique in the space of languages with things they call "type classes".

What are the two ways?

Well, we can go from Ord a :- Eq a via the superclass relationship, and then from Eq a :- Eq [a] via the instance, or we can go from Ord a :- Ord [a] via the instance then from Ord [a] :- Eq [a] through the superclass relationship and this diagram by definition must "commute".

Diagrammatically,

                   Ord a
               ins /     \ cls
                  v       v
            Ord [a]     Eq a
               cls \     / ins
                    v   v
                   Eq [a]

This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.

Constructors

Sub (a => Dict b)

Instances

Instances details

Category (:-)	Possible since GHC 7.8, when `Category` was made polykinded.
Instance details Defined in Data.Constraint Methods id :: forall (a :: k). a :- a # (.) :: forall (b :: k) (c :: k) (a :: k). (b :- c) -> (a :- b) -> a :- c #
() :=> (Eq (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Eq (a :- b) #
() :=> (Ord (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Ord (a :- b) #
() :=> (Show (a :- b))
Instance details Defined in Data.Constraint Methods ins :: () :- Show (a :- b) #
a => HasDict b (a :- b)
Instance details Defined in Data.Constraint Methods evidence :: (a :- b) -> Dict b #
Eq (a :- b)	Assumes `IncoherentInstances` doesn't exist.
Instance details Defined in Data.Constraint Methods (==) :: (a :- b) -> (a :- b) -> Bool # (/=) :: (a :- b) -> (a :- b) -> Bool #
(Typeable p, Typeable q, p, q) => Data (p :- q)
Instance details Defined in Data.Constraint Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (p :- q) -> c (p :- q) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (p :- q) # toConstr :: (p :- q) -> Constr # dataTypeOf :: (p :- q) -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (p :- q)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) # gmapT :: (forall b. Data b => b -> b) -> (p :- q) -> p :- q # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r # gmapQ :: (forall d. Data d => d -> u) -> (p :- q) -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> (p :- q) -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #
Ord (a :- b)	Assumes `IncoherentInstances` doesn't exist.
Instance details Defined in Data.Constraint Methods compare :: (a :- b) -> (a :- b) -> Ordering # (<) :: (a :- b) -> (a :- b) -> Bool # (<=) :: (a :- b) -> (a :- b) -> Bool # (>) :: (a :- b) -> (a :- b) -> Bool # (>=) :: (a :- b) -> (a :- b) -> Bool # max :: (a :- b) -> (a :- b) -> a :- b # min :: (a :- b) -> (a :- b) -> a :- b #
Show (a :- b)
Instance details Defined in Data.Constraint Methods showsPrec :: Int -> (a :- b) -> ShowS # show :: (a :- b) -> String # showList :: [a :- b] -> ShowS #
a => NFData (a :- b)
Instance details Defined in Data.Constraint Methods rnf :: (a :- b) -> () #

data BadTypeForScope Source #

Constructors

BtNotComparable
BtIsOperation
BtHasBigMap
BtHasNestedBigMap
BtHasContract

Instances

Instances details

Eq BadTypeForScope Source #
Instance details Defined in Michelson.Typed.Scope Methods (==) :: BadTypeForScope -> BadTypeForScope -> Bool # (/=) :: BadTypeForScope -> BadTypeForScope -> Bool #
Show BadTypeForScope Source #
Instance details Defined in Michelson.Typed.Scope Methods showsPrec :: Int -> BadTypeForScope -> ShowS # show :: BadTypeForScope -> String # showList :: [BadTypeForScope] -> ShowS #
Generic BadTypeForScope Source #
Instance details Defined in Michelson.Typed.Scope Associated Types type Rep BadTypeForScope :: Type -> Type # Methods from :: BadTypeForScope -> Rep BadTypeForScope x # to :: Rep BadTypeForScope x -> BadTypeForScope #
NFData BadTypeForScope Source #
Instance details Defined in Michelson.Typed.Scope Methods rnf :: BadTypeForScope -> () #
Buildable BadTypeForScope Source #
Instance details Defined in Michelson.Typed.Scope Methods build :: BadTypeForScope -> Builder #
type Rep BadTypeForScope Source #
Instance details Defined in Michelson.Typed.Scope type Rep BadTypeForScope = D1 ('MetaData "BadTypeForScope" "Michelson.Typed.Scope" "morley-1.12.0-inplace" 'False) ((C1 ('MetaCons "BtNotComparable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtIsOperation" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "BtHasBigMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "BtHasNestedBigMap" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtHasContract" 'PrefixI 'False) (U1 :: Type -> Type))))

class CheckScope (c :: Constraint) where Source #

Should be present for common scopes.

Methods

checkScope :: Either BadTypeForScope (Dict c) Source #

Check that constraint hold for a given type.

Instances

Instances details

KnownT t => CheckScope (UnpackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source #
KnownT t => CheckScope (PackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (PackedValScope t)) Source #
KnownT t => CheckScope (ConstantScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source #
KnownT t => CheckScope (StorageScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (StorageScope t)) Source #
KnownT t => CheckScope (ParameterScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ParameterScope t)) Source #
SingI t => CheckScope (HasNoNestedBigMaps t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t)) Source #
SingI t => CheckScope (HasNoBigMap t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t)) Source #
SingI t => CheckScope (HasNoContract t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoContract t)) Source #
SingI t => CheckScope (HasNoOp t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoOp t)) Source #
KnownT t => CheckScope (ComparabilityScope t) Source #
Instance details Defined in Michelson.Typed.Value Methods checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t)) Source #
SingI t => CheckScope (Comparable t) Source #
Instance details Defined in Michelson.Typed.Value Methods checkScope :: Either BadTypeForScope (Dict (Comparable t)) Source #

Implementation internals

class ContainsBigMap t ~ 'False => HasNoBigMap t Source #

Constraint which ensures that bigmap does not appear in a given type.

Instances

Instances details

ContainsBigMap t ~ 'False => HasNoBigMap t Source #
Instance details Defined in Michelson.Typed.Scope
KnownT t => CheckScope (UnpackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source #
KnownT t => CheckScope (PackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (PackedValScope t)) Source #
KnownT t => CheckScope (ConstantScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source #
SingI t => CheckScope (HasNoBigMap t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t)) Source #

class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source #

Constraint which ensures that there are no nested bigmaps.

Instances

Instances details

ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t Source #
Instance details Defined in Michelson.Typed.Scope
KnownT t => CheckScope (StorageScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (StorageScope t)) Source #
KnownT t => CheckScope (ParameterScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ParameterScope t)) Source #
SingI t => CheckScope (HasNoNestedBigMaps t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t)) Source #

class ContainsOp t ~ 'False => HasNoOp t Source #

Constraint which ensures that operation type does not appear in a given type.

Not just a type alias in order to be able to partially apply it (e.g. in Each).

Instances

Instances details

ContainsOp t ~ 'False => HasNoOp t Source #
Instance details Defined in Michelson.Typed.Scope
KnownT t => CheckScope (UnpackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source #
KnownT t => CheckScope (PackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (PackedValScope t)) Source #
KnownT t => CheckScope (ConstantScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source #
KnownT t => CheckScope (StorageScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (StorageScope t)) Source #
KnownT t => CheckScope (ParameterScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ParameterScope t)) Source #
SingI t => CheckScope (HasNoOp t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoOp t)) Source #

class ContainsContract t ~ 'False => HasNoContract t Source #

Constraint which ensures that contract type does not appear in a given type.

Instances

Instances details

ContainsContract t ~ 'False => HasNoContract t Source #
Instance details Defined in Michelson.Typed.Scope
KnownT t => CheckScope (UnpackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source #
KnownT t => CheckScope (ConstantScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source #
KnownT t => CheckScope (StorageScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (StorageScope t)) Source #
SingI t => CheckScope (HasNoContract t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (HasNoContract t)) Source #

type family ContainsBigMap (t :: T) :: Bool where ... Source #

Whether this type contains TBigMap type.

Equations

ContainsBigMap 'TKey = 'False
ContainsBigMap 'TUnit = 'False
ContainsBigMap 'TSignature = 'False
ContainsBigMap 'TChainId = 'False
ContainsBigMap ('TOption t) = ContainsBigMap t
ContainsBigMap ('TList t) = ContainsBigMap t
ContainsBigMap ('TSet _) = 'False
ContainsBigMap 'TOperation = 'False
ContainsBigMap ('TContract t) = ContainsBigMap t
ContainsBigMap ('TPair a b) = ContainsBigMap a \|\| ContainsBigMap b
ContainsBigMap ('TOr a b) = ContainsBigMap a \|\| ContainsBigMap b
ContainsBigMap ('TLambda _ _) = 'False
ContainsBigMap ('TMap _ v) = ContainsBigMap v
ContainsBigMap ('TBigMap _ _) = 'True
ContainsBigMap _ = 'False

type family ContainsNestedBigMaps (t :: T) :: Bool where ... Source #

Whether this type contains a type with nested TBigMaps .

Nested big_maps (i.e. big_map which contains another big_map inside of it's value type). Are prohibited in all contexts. Some context such as PUSH, APPLY, PACK/UNPACK instructions are more strict because they doesn't work with big_map at all.

Equations

ContainsNestedBigMaps 'TKey = 'False
ContainsNestedBigMaps 'TUnit = 'False
ContainsNestedBigMaps 'TSignature = 'False
ContainsNestedBigMaps 'TChainId = 'False
ContainsNestedBigMaps ('TOption t) = ContainsNestedBigMaps t
ContainsNestedBigMaps ('TList t) = ContainsNestedBigMaps t
ContainsNestedBigMaps ('TSet _) = 'False
ContainsNestedBigMaps 'TOperation = 'False
ContainsNestedBigMaps ('TContract t) = ContainsNestedBigMaps t
ContainsNestedBigMaps ('TPair a b) = ContainsNestedBigMaps a \|\| ContainsNestedBigMaps b
ContainsNestedBigMaps ('TOr a b) = ContainsNestedBigMaps a \|\| ContainsNestedBigMaps b
ContainsNestedBigMaps ('TLambda _ _) = 'False
ContainsNestedBigMaps ('TMap _ v) = ContainsNestedBigMaps v
ContainsNestedBigMaps ('TBigMap _ v) = ContainsBigMap v
ContainsNestedBigMaps _ = 'False

type ForbidOp t = FailOnOperationFound (ContainsOp t) Source #

This is like HasNoOp, it raises a more human-readable error when t type is concrete, but GHC cannot make any conclusions from such constraint as it can for HasNoOp. Though, hopefully, it will someday: #11503.

Use this constraint in our eDSL.

type ForbidContract t = FailOnContractFound (ContainsContract t) Source #

type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t) Source #

type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t) Source #

type family FailOnBigMapFound (enabled :: Bool) :: Constraint where ... Source #

Report a human-readable error about TBigMap at a wrong place.

Equations

FailOnBigMapFound 'True = TypeError ('Text "BigMaps are not allowed in this scope")
FailOnBigMapFound 'False = ()

type family FailOnNestedBigMapsFound (enabled :: Bool) :: Constraint where ... Source #

Report a human-readable error that TBigMap contains another TBigMap

Equations

FailOnNestedBigMapsFound 'True = TypeError ('Text "Nested BigMaps are not allowed")
FailOnNestedBigMapsFound 'False = ()

type family FailOnOperationFound (enabled :: Bool) :: Constraint where ... Source #

Report a human-readable error about TOperation at a wrong place.

Equations

FailOnOperationFound 'True = TypeError ('Text "Operations are not allowed in this scope")
FailOnOperationFound 'False = ()

data OpPresence (t :: T) Source #

Whether the type contains TOperation, with proof.

Constructors

ContainsOp t ~ 'True => OpPresent
ContainsOp t ~ 'False => OpAbsent

data ContractPresence (t :: T) Source #

Constructors

ContainsContract t ~ 'True => ContractPresent
ContainsContract t ~ 'False => ContractAbsent

data BigMapPresence (t :: T) Source #

Constructors

ContainsBigMap t ~ 'True => BigMapPresent
ContainsBigMap t ~ 'False => BigMapAbsent

data NestedBigMapsPresence (t :: T) Source #

Constructors

ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent
ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent

checkOpPresence :: Sing (ty :: T) -> OpPresence ty Source #

Check at runtime whether the given type contains TOperation.

checkContractTypePresence :: Sing (ty :: T) -> ContractPresence ty Source #

Check at runtime whether the given type contains TContract.

checkBigMapPresence :: Sing (ty :: T) -> BigMapPresence ty Source #

Check at runtime whether the given type contains TBigMap.

checkNestedBigMapsPresence :: Sing (ty :: T) -> NestedBigMapsPresence ty Source #

Check at runtime whether the given type contains TBigMap.

opAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoOp t) Source #

Check at runtime that the given type does not contain TOperation.

contractTypeAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoContract t) Source #

Check at runtime that the given type does not contain TContract.

bigMapAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoBigMap t) Source #

Check at runtime that the given type does not containt TBigMap

nestedBigMapsAbsense :: Sing (t :: T) -> Maybe (Dict $ HasNoNestedBigMaps t) Source #

Check at runtime that the given type does not contain nested TBigMap

forbiddenOp :: forall t a. (SingI t, ForbidOp t) => (HasNoOp t => a) -> a Source #

Reify HasNoOp contraint from ForbidOp.

Left for backward compatibility.

forbiddenContractType :: forall t a. (SingI t, ForbidContract t) => (HasNoContract t => a) -> a Source #

Reify HasNoContract contraint from ForbidContract.

forbiddenBigMap :: forall t a. (SingI t, ForbidBigMap t) => (HasNoBigMap t => a) -> a Source #

forbiddenNestedBigMaps :: forall t a. (SingI t, ForbidNestedBigMaps t) => (HasNoNestedBigMaps t => a) -> a Source #

Re-exports

withDict :: HasDict c e => e -> (c => r) -> r #

From a Dict, takes a value in an environment where the instance witnessed by the Dict is in scope, and evaluates it.

Essentially a deconstruction of a Dict into its continuation-style form.

Can also be used to deconstruct an entailment, a :- b, using a context a.

withDict :: Dict c -> (c => r) -> r
withDict :: a => (a :- c) -> (c => r) -> r

class SingI (a :: k) where #

A SingI constraint is essentially an implicitly-passed singleton. If you need to satisfy this constraint with an explicit singleton, please see withSingI or the Sing pattern synonym.

Methods

sing :: Sing a #

Produce the singleton explicitly. You will likely need the ScopedTypeVariables extension to use this method the way you want.

Instances

Instances details

SingI 'Z Source #
Instance details Defined in Util.Peano Methods sing :: Sing 'Z #
SingI 'TKey Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TKey #
SingI 'TUnit Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TUnit #
SingI 'TSignature Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TSignature #
SingI 'TChainId Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TChainId #
SingI 'TOperation Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TOperation #
SingI 'TInt Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TInt #
SingI 'TNat Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TNat #
SingI 'TString Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TString #
SingI 'TBytes Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TBytes #
SingI 'TMutez Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TMutez #
SingI 'TBool Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TBool #
SingI 'TKeyHash Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TKeyHash #
SingI 'TTimestamp Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TTimestamp #
SingI 'TAddress Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing 'TAddress #
(SingI n, KnownPeano n) => SingI ('S n :: Nat) Source #
Instance details Defined in Util.Peano Methods sing :: Sing ('S n) #
KnownT a => SingI ('TOption a :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TOption a) #
KnownT a => SingI ('TList a :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TList a) #
KnownT a => SingI ('TSet a :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TSet a) #
KnownT a => SingI ('TContract a :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TContract a) #
(KnownT a, KnownT b) => SingI ('TPair a b :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TPair a b) #
(KnownT a, KnownT b) => SingI ('TOr a b :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TOr a b) #
(KnownT a, KnownT b) => SingI ('TLambda a b :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TLambda a b) #
(KnownT a, KnownT b) => SingI ('TMap a b :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TMap a b) #
(KnownT a, KnownT b) => SingI ('TBigMap a b :: T) Source #
Instance details Defined in Michelson.Typed.Sing Methods sing :: Sing ('TBigMap a b) #
KnownT t => CheckScope (UnpackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t)) Source #
KnownT t => CheckScope (PackedValScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (PackedValScope t)) Source #
KnownT t => CheckScope (ConstantScope t) Source #
Instance details Defined in Michelson.Typed.Scope Methods checkScope :: Either BadTypeForScope (Dict (ConstantScope t)) Source #
SingI NotSym0
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing NotSym0 #
SingI (\|\|@#@$)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (\|\|@#@$) #
SingI (&&@#@$)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (&&@#@$) #
SingI Log2Sym0
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing Log2Sym0 #
SingI (<=?@#@$)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (<=?@#@$) #
SingI ModSym0
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing ModSym0 #
SingI DivSym0
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing DivSym0 #
SingI (^@#@$)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing (^@#@$) #
SingI AllSym0
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing AllSym0 #
SingI AnySym0
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing AnySym0 #
SingI ShowParenSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowParenSym0 #
SingI OrSym0
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing OrSym0 #
SingI AndSym0
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing AndSym0 #
SingI UnwordsSym0
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnwordsSym0 #
SingI UnlinesSym0
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnlinesSym0 #
SingI Show_tupleSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing Show_tupleSym0 #
SingI ThenCmpSym0
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ThenCmpSym0 #
SingI EftNatSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EftNatSym0 #
SingI EfdtNatSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EfdtNatSym0 #
SingI EfdtNatDnSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EfdtNatDnSym0 #
SingI EfdtNatUpSym0
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EfdtNatUpSym0 #
SingI ShowCommaSpaceSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCommaSpaceSym0 #
SingI ShowSpaceSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowSpaceSym0 #
SingI ShowStringSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowStringSym0 #
SingI ShowCharSym0
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowCharSym0 #
SingI x => SingI ((\|\|@#@$$) x :: TyFun Bool Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing ((\|\|@#@$$) x) #
SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing ((&&@#@$$) x) #
SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((<=?@#@$$) x) #
SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (ModSym1 x) #
SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits Methods sing :: Sing (DivSym1 x) #
SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ((^@#@$$) x) #
SAlternative f => SingI (GuardSym0 :: TyFun Bool (f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing GuardSym0 #
SApplicative f => SingI (WhenSym0 :: TyFun Bool (f () ~> f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing WhenSym0 #
SingI (ListtransposeSym0 :: TyFun [[a]] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListtransposeSym0 #
SingI (TransposeSym0 :: TyFun [[a]] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TransposeSym0 #
SingI (ConcatSym0 :: TyFun [[a]] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ConcatSym0 #
SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing CatMaybesSym0 #
SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListSym0 #
SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing ListToMaybeSym0 #
SingI (ListtailsSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListtailsSym0 #
SNum a => SingI (ListsumSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListsumSym0 #
SOrd a => SingI (ListsortSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListsortSym0 #
SingI (ListreverseSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListreverseSym0 #
SNum a => SingI (ListproductSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListproductSym0 #
SingI (ListnullSym0 :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListnullSym0 #
SOrd a => SingI (ListminimumSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListminimumSym0 #
SOrd a => SingI (ListmaximumSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListmaximumSym0 #
SingI (ListlengthSym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListlengthSym0 #
SingI (ListlastSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListlastSym0 #
SEq a => SingI (ListisPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListisPrefixOfSym0 #
SingI (ListinitsSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListinitsSym0 #
SingI (ListinitSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListinitSym0 #
SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListindexSym0 #
SEq a => SingI ((\\@#@$) :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (\\@#@$) #
SEq a => SingI (UnionSym0 :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnionSym0 #
SingI (TailsSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TailsSym0 #
SingI (TailSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TailSym0 #
SNum a => SingI (SumSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SumSym0 #
SingI (SubsequencesSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SubsequencesSym0 #
SOrd a => SingI (SortSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SortSym0 #
SingI (ReverseSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReverseSym0 #
SNum a => SingI (ProductSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ProductSym0 #
SingI (PermutationsSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing PermutationsSym0 #
SingI (NullSym0 :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NullSym0 #
SEq a => SingI (NubSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NubSym0 #
SingI (NonEmptySubsequencesSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NonEmptySubsequencesSym0 #
SOrd a => SingI (MinimumSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing MinimumSym0 #
SOrd a => SingI (MaximumSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing MaximumSym0 #
SingI (LengthSym0 :: TyFun [a] Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing LengthSym0 #
SingI (LastSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing LastSym0 #
SEq a => SingI (IsSuffixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IsSuffixOfSym0 #
SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IsPrefixOfSym0 #
SEq a => SingI (IsInfixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IsInfixOfSym0 #
SEq a => SingI (IntersectSym0 :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntersectSym0 #
SingI (IntercalateSym0 :: TyFun [a] ([[a]] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntercalateSym0 #
SingI (InitsSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InitsSym0 #
SingI (InitSym0 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InitSym0 #
SingI (HeadSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing HeadSym0 #
SEq a => SingI (GroupSym0 :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing GroupSym0 #
SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (!!@#@$) #
SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (++@#@$) #
SMonoid a => SingI (MconcatSym0 :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing MconcatSym0 #
SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing MaybeToListSym0 #
SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing IsNothingSym0 #
SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing IsJustSym0 #
SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing FromJustSym0 #
SingI (OptionSym0 :: TyFun (Maybe a) (Option a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing OptionSym0 #
SingI (LastSym0 :: TyFun (Maybe a) (Last a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing LastSym0 #
SingI (FirstSym0 :: TyFun (Maybe a) (First a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing FirstSym0 #
SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ThenCmpSym1 d) #
SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EftNatSym1 d) #
SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing FromIntegerSym0 #
SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing ToEnumSym0 #
SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListtakeSym0 #
SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListsplitAtSym0 #
SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListdropSym0 #
SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeSym0 #
SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SplitAtSym0 #
SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropSym0 #
SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatSym1 d) #
SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatDnSym1 d) #
SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatUpSym1 d) #
SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsPrecSym0 #
SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ReplicateSym0 #
SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowStringSym1 d) #
SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowCharSym1 d) #
SingI d => SingI (Show_tupleSym1 d :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (Show_tupleSym1 d) #
SIsString a => SingI (FromStringSym0 :: TyFun Symbol a -> Type)
Instance details Defined in Data.Singletons.Prelude.IsString Methods sing :: Sing FromStringSym0 #
SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowsSym0 #
SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing Show_Sym0 #
SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SubtractSym0 #
SNum a => SingI (SignumSym0 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing SignumSym0 #
SNum a => SingI (NegateSym0 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing NegateSym0 #
SNum a => SingI (AbsSym0 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing AbsSym0 #
SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (-@#@$) #
SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (+@#@$) #
SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (*@#@$) #
SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing FromMaybeSym0 #
SingI (ListintersperseSym0 :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListintersperseSym0 #
SOrd a => SingI (ListinsertSym0 :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListinsertSym0 #
SEq a => SingI (ListelemSym0 :: TyFun a ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListelemSym0 #
SingI (PrependToAllSym0 :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing PrependToAllSym0 #
SEq a => SingI (NotElemSym0 :: TyFun a ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NotElemSym0 #
SingI (IntersperseSym0 :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntersperseSym0 #
SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InsertSym0 #
SEq a => SingI (ElemSym0 :: TyFun a ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemSym0 #
SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndicesSym0 #
SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ElemIndexSym0 #
SEq a => SingI (DeleteSym0 :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DeleteSym0 #
SFoldable t => SingI (OrSym0 :: TyFun (t Bool) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing OrSym0 #
SFoldable t => SingI (AndSym0 :: TyFun (t Bool) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AndSym0 #
SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing (==@#@$) #
SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing (/=@#@$) #
SEnum a => SingI (SuccSym0 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing SuccSym0 #
SEnum a => SingI (PredSym0 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing PredSym0 #
SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing FromEnumSym0 #
SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromToSym0 #
SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing EnumFromThenToSym0 #
SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing Bool_Sym0 #
SingI (IdSym0 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing IdSym0 #
SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing AsTypeOfSym0 #
SingI (JustSym0 :: TyFun a (Maybe a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing JustSym0 #
SingI (IdentitySym0 :: TyFun a (Identity a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing IdentitySym0 #
SingI ((:\|@#@$) :: TyFun a ([a] ~> NonEmpty a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (:\|@#@$) #
SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (:@#@$) #
SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing MinSym0 #
SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing MaxSym0 #
SingI (DownSym0 :: TyFun a (Down a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing DownSym0 #
SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing CompareSym0 #
SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (>@#@$) #
SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (>=@#@$) #
SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (<@#@$) #
SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (<=@#@$) #
SingI (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing WrapMonoidSym0 #
SingI (SumSym0 :: TyFun a (Sum a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing SumSym0 #
SingI (ProductSym0 :: TyFun a (Product a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing ProductSym0 #
SingI (MinSym0 :: TyFun a (Min a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing MinSym0 #
SingI (MaxSym0 :: TyFun a (Max a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing MaxSym0 #
SingI (LastSym0 :: TyFun a (Last a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing LastSym0 #
SingI (FirstSym0 :: TyFun a (First a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing FirstSym0 #
SingI (DualSym0 :: TyFun a (Dual a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing DualSym0 #
SSemigroup a => SingI ((<>@#@$) :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing (<>@#@$) #
SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing MappendSym0 #
SSemigroup a => SingI (SconcatSym0 :: TyFun (NonEmpty a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing SconcatSym0 #
SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym1 d) #
SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing ShowListWithSym0 #
SingI (ListtakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListtakeWhileSym0 #
SingI (ListspanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListspanSym0 #
SingI (ListsortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListsortBySym0 #
SingI (Listscanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing Listscanr1Sym0 #
SingI (ListpartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListpartitionSym0 #
SingI (ListnubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListnubBySym0 #
SingI (Listfoldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing Listfoldr1Sym0 #
SingI (Listfoldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing Listfoldl1Sym0 #
SingI (ListfilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListfilterSym0 #
SingI (ListdropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListdropWhileSym0 #
SingI (UnionBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnionBySym0 #
SingI (TakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing TakeWhileSym0 #
SingI (SpanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SpanSym0 #
SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SortBySym0 #
SingI (SelectSym0 :: TyFun (a ~> Bool) (a ~> (([a], [a]) ~> ([a], [a]))) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing SelectSym0 #
SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Scanr1Sym0 #
SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Scanl1Sym0 #
SingI (PartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing PartitionSym0 #
SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing NubBySym0 #
SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing MinimumBySym0 #
SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing MaximumBySym0 #
SingI (IntersectBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing IntersectBySym0 #
SingI (InsertBySym0 :: TyFun (a ~> (a ~> Ordering)) (a ~> ([a] ~> [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing InsertBySym0 #
SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [[a]]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing GroupBySym0 #
SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Foldr1Sym0 #
SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Foldl1Sym0 #
SingI (Foldl1'Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Foldl1'Sym0 #
SingI (FindSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindSym0 #
SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndicesSym0 #
SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FindIndexSym0 #
SingI (FilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing FilterSym0 #
SingI (Elem_bySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> Bool)) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Elem_bySym0 #
SingI (DropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropWhileSym0 #
SingI (DropWhileEndSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DropWhileEndSym0 #
SingI (DeleteFirstsBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DeleteFirstsBySym0 #
SingI (DeleteBySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing DeleteBySym0 #
SingI (BreakSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing BreakSym0 #
SingI (AnySym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing AnySym0 #
SingI (AllSym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing AllSym0 #
SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing UntilSym0 #
SingI d => SingI (IntercalateSym1 d :: TyFun [[a]] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntercalateSym1 d) #
SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing RightsSym0 #
SingI (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing PartitionEithersSym0 #
SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing LeftsSym0 #
SingI (ListunzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListunzipSym0 #
SingI (UnzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnzipSym0 #
SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym1 d) #
SingI (ListzipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListzipSym0 #
SingI d => SingI (ListtakeWhileSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListtakeWhileSym1 d) #
SingI d => SingI (ListtakeSym1 d a :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListtakeSym1 d a) #
SingI d => SingI (ListsplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListsplitAtSym1 d a) #
SingI d => SingI (ListspanSym1 d :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListspanSym1 d) #
SingI d => SingI (ListsortBySym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListsortBySym1 d) #
SingI d => SingI (Listscanr1Sym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (Listscanr1Sym1 d) #
SingI d => SingI (ListpartitionSym1 d :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListpartitionSym1 d) #
SingI d => SingI (ListnubBySym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListnubBySym1 d) #
(SEq a, SingI d) => SingI (ListisPrefixOfSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListisPrefixOfSym1 d) #
SingI d => SingI (ListintersperseSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListintersperseSym1 d) #
(SOrd a, SingI d) => SingI (ListinsertSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListinsertSym1 d) #
SingI d => SingI (Listfoldr1Sym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (Listfoldr1Sym1 d) #
SingI d => SingI (Listfoldl1Sym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (Listfoldl1Sym1 d) #
SingI d => SingI (ListfilterSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListfilterSym1 d) #
(SEq a, SingI d) => SingI (ListelemSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListelemSym1 d) #
SingI d => SingI (ListdropWhileSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListdropWhileSym1 d) #
SingI d => SingI (ListdropSym1 d a :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListdropSym1 d a) #
(SEq a, SingI d) => SingI ((\\@#@$$) d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((\\@#@$$) d) #
SingI (ZipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ZipSym0 #
(SEq a, SingI d) => SingI (UnionSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnionSym1 d) #
SingI d => SingI (UnionBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnionBySym1 d) #
SingI d => SingI (TakeWhileSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (TakeWhileSym1 d) #
SingI d => SingI (TakeSym1 d a :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (TakeSym1 d a) #
SingI d => SingI (SplitAtSym1 d a :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SplitAtSym1 d a) #
SingI d => SingI (SpanSym1 d :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SpanSym1 d) #
SingI d => SingI (SortBySym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SortBySym1 d) #
SingI d => SingI (Scanr1Sym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Scanr1Sym1 d) #
SingI d => SingI (Scanl1Sym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Scanl1Sym1 d) #
SingI d => SingI (PrependToAllSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (PrependToAllSym1 d) #
SingI d => SingI (PartitionSym1 d :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (PartitionSym1 d) #
SingI d => SingI (NubBySym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (NubBySym1 d) #
(SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (NotElemSym1 d) #
SingI d => SingI (MinimumBySym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (MinimumBySym1 d) #
SingI d => SingI (MaximumBySym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (MaximumBySym1 d) #
(SEq a, SingI d) => SingI (IsSuffixOfSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IsSuffixOfSym1 d) #
(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IsPrefixOfSym1 d) #
(SEq a, SingI d) => SingI (IsInfixOfSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IsInfixOfSym1 d) #
SingI d => SingI (IntersperseSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersperseSym1 d) #
(SEq a, SingI d) => SingI (IntersectSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersectSym1 d) #
SingI d => SingI (IntersectBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersectBySym1 d) #
(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (InsertSym1 d) #
SingI d => SingI (GroupBySym1 d :: TyFun [a] [[a]] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (GroupBySym1 d) #
SNum i => SingI (GenericLengthSym0 :: TyFun [a] i -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing GenericLengthSym0 #
SingI d => SingI (Foldr1Sym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Foldr1Sym1 d) #
SingI d => SingI (Foldl1Sym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Foldl1Sym1 d) #
SingI d => SingI (Foldl1'Sym1 d :: TyFun [a] a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Foldl1'Sym1 d) #
SingI d => SingI (FindSym1 d :: TyFun [a] (Maybe a) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindSym1 d) #
SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndicesSym1 d) #
SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FindIndexSym1 d) #
SingI d => SingI (FilterSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (FilterSym1 d) #
(SEq a, SingI d) => SingI (ElemSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemSym1 d) #
(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndicesSym1 d) #
(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ElemIndexSym1 d) #
SingI d => SingI (DropWhileSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DropWhileSym1 d) #
SingI d => SingI (DropWhileEndSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DropWhileEndSym1 d) #
SingI d => SingI (DropSym1 d a :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DropSym1 d a) #
(SEq a, SingI d) => SingI (DeleteSym1 d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteSym1 d) #
SingI d => SingI (DeleteFirstsBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteFirstsBySym1 d) #
SingI d => SingI (BreakSym1 d :: TyFun [a] ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (BreakSym1 d) #
SingI d => SingI (AnySym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (AnySym1 d) #
SingI d => SingI (AllSym1 d :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (AllSym1 d) #
SingI d => SingI ((++@#@$$) d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ((++@#@$$) d) #
SingI d => SingI ((:\|@#@$$) d :: TyFun [a] (NonEmpty a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing ((:\|@#@$$) d) #
SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing ((:@#@$$) d) #
SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (FromMaybeSym1 d) #
SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsRightSym0 #
SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing IsLeftSym0 #
(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatDnSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EfdtNatUpSym2 d1 d2) #
SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListindexSym1 d) #
SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ((!!@#@$$) d) #
(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowParenSym2 d1 d2) #
(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsSym1 d) #
(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListSym1 d) #
SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorWithoutStackTraceSym0 #
SingI (ErrorSym0 :: TyFun Symbol a -> Type)
Instance details Defined in Data.Singletons.TypeLits.Internal Methods sing :: Sing ErrorSym0 #
SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing SwapSym0 #
SingI (SndSym0 :: TyFun (a, b) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing SndSym0 #
SingI (FstSym0 :: TyFun (a, b) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing FstSym0 #
(SShow a, SingI d) => SingI (ShowsPrecSym1 d a :: TyFun a (Symbol ~> Symbol) -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym1 d a) #
(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing (SubtractSym1 d) #
(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((-@#@$$) d) #
(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((+@#@$$) d) #
(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Num Methods sing :: Sing ((*@#@$$) d) #
SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing Maybe_Sym0 #
SingI d => SingI (SelectSym1 d :: TyFun a (([a], [a]) ~> ([a], [a])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SelectSym1 d) #
SingI d => SingI (ReplicateSym1 d a :: TyFun a [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ReplicateSym1 d a) #
SEq a => SingI (LookupSym0 :: TyFun a ([(a, b)] ~> Maybe b) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing LookupSym0 #
SingI d => SingI (InsertBySym1 d :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (InsertBySym1 d) #
SingI d => SingI (Elem_bySym1 d :: TyFun a ([a] ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Elem_bySym1 d) #
SingI d => SingI (DeleteBySym1 d :: TyFun a ([a] ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteBySym1 d) #
(SApplicative f, SingI d) => SingI (WhenSym1 d f :: TyFun (f ()) (f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (WhenSym1 d f) #
SMonad m => SingI (ReturnSym0 :: TyFun a (m a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ReturnSym0 #
SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing PureSym0 #
SMonad m => SingI (JoinSym0 :: TyFun (m (m a)) (m a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing JoinSym0 #
SFoldable t => SingI (ToListSym0 :: TyFun (t a) [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ToListSym0 #
(SFoldable t, SNum a) => SingI (SumSym0 :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing SumSym0 #
(SFoldable t, SNum a) => SingI (ProductSym0 :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ProductSym0 #
(SFoldable t, SEq a) => SingI (NotElemSym0 :: TyFun a (t a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing NotElemSym0 #
(SFoldable t, SOrd a) => SingI (MinimumSym0 :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MinimumSym0 #
(SFoldable t, SOrd a) => SingI (MaximumSym0 :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MaximumSym0 #
(SFoldable t, SMonoid m) => SingI (FoldSym0 :: TyFun (t m) m -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldSym0 #
(SFoldable t, SEq a) => SingI (ElemSym0 :: TyFun a (t a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ElemSym0 #
SFoldable t => SingI (ConcatSym0 :: TyFun (t [a]) [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ConcatSym0 #
(SEq a, SingI x) => SingI ((==@#@$$) x :: TyFun a Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing ((==@#@$$) x) #
(SEq a, SingI x) => SingI ((/=@#@$$) x :: TyFun a Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Eq Methods sing :: Sing ((/=@#@$$) x) #
(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromToSym1 d) #
(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym1 d) #
SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (Bool_Sym1 d) #
SingI (SeqSym0 :: TyFun a (b ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing SeqSym0 #
SingI (ConstSym0 :: TyFun a (b ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ConstSym0 #
SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (AsTypeOfSym1 d) #
SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple2Sym0 #
SingI (RightSym0 :: TyFun b (Either a b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing RightSym0 #
SingI (LeftSym0 :: TyFun a (Either a b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing LeftSym0 #
(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (MinSym1 d) #
(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (MaxSym1 d) #
(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (CompareSym1 d) #
(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((>@#@$$) d) #
(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((>=@#@$$) d) #
(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((<@#@$$) d) #
(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ((<=@#@$$) d) #
(SSemigroup a, SingI d) => SingI ((<>@#@$$) d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal Methods sing :: Sing ((<>@#@$$) d) #
(SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Monoid Methods sing :: Sing (MappendSym1 d) #
SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing VoidSym0 #
SingI (Option_Sym0 :: TyFun b ((a ~> b) ~> (Option a ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing Option_Sym0 #
SingI (ArgSym0 :: TyFun a (b ~> Arg a b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing ArgSym0 #
SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing MapMaybeSym0 #
SingI (ListscanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListscanrSym0 #
SingI (ListscanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListscanlSym0 #
SingI (ListmapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListmapSym0 #
SingI (ListfoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListfoldrSym0 #
SingI (ListfoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListfoldlSym0 #
SingI (Listfoldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing Listfoldl'Sym0 #
SingI (UnfoldrSym0 :: TyFun (b ~> Maybe (a, b)) (b ~> [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing UnfoldrSym0 #
SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ScanrSym0 #
SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ScanlSym0 #
SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Foldl'Sym0 #
SingI (ConcatMapSym0 :: TyFun (a ~> [b]) ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ConcatMapSym0 #
SFoldable t => SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MinimumBySym0 #
SFoldable t => SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MaximumBySym0 #
SFoldable t => SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldr1Sym0 #
SFoldable t => SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldl1Sym0 #
SFoldable t => SingI (FindSym0 :: TyFun (a ~> Bool) (t a ~> Maybe a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FindSym0 #
SFoldable t => SingI (AnySym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AnySym0 #
SFoldable t => SingI (AllSym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AllSym0 #
SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (UntilSym1 d) #
SingI (MapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing MapSym0 #
SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing FoldrSym0 #
SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ($@#@$) #
SingI (($!@#@$) :: TyFun (a ~> b) (a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing ($!@#@$) #
SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing FoldlSym0 #
SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing ComparingSym0 #
SingI (ConstSym0 :: TyFun a6989586621679095649 (Const a6989586621679095649 b6989586621679095650) -> Type)
Instance details Defined in Data.Singletons.Prelude.Const Methods sing :: Sing ConstSym0 #
SingI a => SingI ('WrapSing s :: WrappedSing a)
Instance details Defined in Data.Singletons.Internal Methods sing :: Sing ('WrapSing s) #
(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type)
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (Bool_Sym2 d1 d2) #
(SEq a, SingI d) => SingI (LookupSym1 d b :: TyFun [(a, b)] (Maybe b) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (LookupSym1 d b) #
SingI (Unzip3Sym0 :: TyFun [(a, b, c)] ([a], [b], [c]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip3Sym0 #
SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (MapMaybeSym1 d) #
SingI d => SingI (ListzipSym1 d b :: TyFun [b] [(a, b)] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListzipSym1 d b) #
SingI d => SingI (ListmapSym1 d :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListmapSym1 d) #
SingI d => SingI (ZipSym1 d b :: TyFun [b] [(a, b)] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipSym1 d b) #
SingI (Zip3Sym0 :: TyFun [a] ([b] ~> ([c] ~> [(a, b, c)])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Zip3Sym0 #
(SingI d1, SingI d2) => SingI (UnionBySym2 d1 d2 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnionBySym2 d1 d2) #
(SingI d1, SingI d2) => SingI (IntersectBySym2 d1 d2 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (IntersectBySym2 d1 d2) #
(SingI d1, SingI d2) => SingI (InsertBySym2 d1 d2 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (InsertBySym2 d1 d2) #
(SingI d1, SingI d2) => SingI (Elem_bySym2 d1 d2 :: TyFun [a] Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Elem_bySym2 d1 d2) #
(SingI d1, SingI d2) => SingI (DeleteFirstsBySym2 d1 d2 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteFirstsBySym2 d1 d2) #
(SingI d1, SingI d2) => SingI (DeleteBySym2 d1 d2 :: TyFun [a] [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (DeleteBySym2 d1 d2) #
SingI d => SingI (ConcatMapSym1 d :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ConcatMapSym1 d) #
SingI d => SingI (MapSym1 d :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (MapSym1 d) #
(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowListWithSym2 d1 d2) #
(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type)
Instance details Defined in Data.Singletons.Prelude.Show Methods sing :: Sing (ShowsPrecSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (SelectSym2 d1 d2 :: TyFun ([a], [a]) ([a], [a]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (SelectSym2 d1 d2) #
(STraversable t, SMonad m) => SingI (SequenceSym0 :: TyFun (t (m a)) (m (t a)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing SequenceSym0 #
(STraversable t, SApplicative f) => SingI (SequenceASym0 :: TyFun (t (f a)) (f (t a)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing SequenceASym0 #
SingI d => SingI (ListscanrSym1 d :: TyFun b ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListscanrSym1 d) #
SingI d => SingI (ListscanlSym1 d :: TyFun b ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListscanlSym1 d) #
SingI d => SingI (ListfoldrSym1 d :: TyFun b ([a] ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListfoldrSym1 d) #
SingI d => SingI (ListfoldlSym1 d :: TyFun b ([a] ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListfoldlSym1 d) #
SingI d => SingI (Listfoldl'Sym1 d :: TyFun b ([a] ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (Listfoldl'Sym1 d) #
SingI d => SingI (UnfoldrSym1 d :: TyFun b [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (UnfoldrSym1 d) #
SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanrSym1 d) #
SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanlSym1 d) #
SingI d => SingI (Foldl'Sym1 d :: TyFun b ([a] ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Foldl'Sym1 d) #
SMonadPlus m => SingI (MplusSym0 :: TyFun (m a) (m a ~> m a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing MplusSym0 #
SMonad m => SingI (ApSym0 :: TyFun (m (a ~> b)) (m a ~> m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ApSym0 #
SMonad m => SingI ((>>=@#@$) :: TyFun (m a) ((a ~> m b) ~> m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (>>=@#@$) #
SAlternative f => SingI ((<\|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<\|>@#@$) #
SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<*>@#@$) #
SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<**>@#@$) #
SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<$@#@$) #
(SFoldable t, SMonad m) => SingI (Sequence_Sym0 :: TyFun (t (m a)) (m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Sequence_Sym0 #
(SFoldable t, SApplicative f) => SingI (SequenceA_Sym0 :: TyFun (t (f a)) (f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing SequenceA_Sym0 #
SFoldable t => SingI (NullSym0 :: TyFun (t a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing NullSym0 #
(SFoldable t, SEq a, SingI d) => SingI (NotElemSym1 d t :: TyFun (t a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (NotElemSym1 d t) #
(SFoldable t, SingI d) => SingI (MinimumBySym1 d t :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (MinimumBySym1 d t) #
(SFoldable t, SingI d) => SingI (MaximumBySym1 d t :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (MaximumBySym1 d t) #
SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing LengthSym0 #
(SFoldable t, SingI d) => SingI (Foldr1Sym1 d t :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldr1Sym1 d t) #
(SFoldable t, SingI d) => SingI (Foldl1Sym1 d t :: TyFun (t a) a -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldl1Sym1 d t) #
(SFoldable t, SingI d) => SingI (FindSym1 d t :: TyFun (t a) (Maybe a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FindSym1 d t) #
(SFoldable t, SEq a, SingI d) => SingI (ElemSym1 d t :: TyFun (t a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (ElemSym1 d t) #
(SFoldable t, SingI d) => SingI (AnySym1 d t :: TyFun (t a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (AnySym1 d t) #
(SFoldable t, SingI d) => SingI (AllSym1 d t :: TyFun (t a) Bool -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (AllSym1 d t) #
(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type)
Instance details Defined in Data.Singletons.Prelude.Enum Methods sing :: Sing (EnumFromThenToSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (UntilSym2 d1 d2) #
SingI d => SingI (SeqSym1 d b :: TyFun b b -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (SeqSym1 d b) #
SingI d => SingI (FoldrSym1 d :: TyFun b ([a] ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FoldrSym1 d) #
SingI d => SingI (ConstSym1 d b :: TyFun b a -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (ConstSym1 d b) #
SingI d => SingI (($@#@$$) d :: TyFun a b -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (($@#@$$) d) #
SingI d => SingI (($!@#@$$) d :: TyFun a b -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (($!@#@$$) d) #
SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple3Sym0 #
SingI d => SingI (Tuple2Sym1 d b :: TyFun b (a, b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple2Sym1 d b) #
SingI d => SingI (FoldlSym1 d :: TyFun b ([a] ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (FoldlSym1 d) #
(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym1 d) #
SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (<&>@#@$) #
SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing ($>@#@$) #
SingI d => SingI (ArgSym1 d b :: TyFun b (Arg a b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (ArgSym1 d b) #
SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing CurrySym0 #
SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing UncurrySym0 #
(STraversable t, SMonoid m) => SingI (FoldMapDefaultSym0 :: TyFun (a ~> m) (t a ~> m) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing FoldMapDefaultSym0 #
STraversable t => SingI (FmapDefaultSym0 :: TyFun (a ~> b) (t a ~> t b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing FmapDefaultSym0 #
SingI d => SingI (Maybe_Sym1 d a :: TyFun (a ~> b) (Maybe a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (Maybe_Sym1 d a) #
SingI (ListzipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing ListzipWithSym0 #
SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ZipWithSym0 #
SingI (MapAccumRSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing MapAccumRSym0 #
SingI (MapAccumLSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing MapAccumLSym0 #
SMonad m => SingI (LiftMSym0 :: TyFun (a1 ~> r) (m a1 ~> m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftMSym0 #
SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftASym0 #
SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing FmapSym0 #
SMonad m => SingI ((=<<@#@$) :: TyFun (a ~> m b) (m a ~> m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (=<<@#@$) #
SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldrSym0 #
SFoldable t => SingI (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldr'Sym0 #
SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldlSym0 #
SFoldable t => SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Foldl'Sym0 #
(SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldMapSym0 #
SFoldable t => SingI (ConcatMapSym0 :: TyFun (a ~> [b]) (t a ~> [b]) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ConcatMapSym0 #
SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing Either_Sym0 #
SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing FlipSym0 #
SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (.@#@$) #
SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (<$>@#@$) #
SingI d => SingI (Option_Sym1 d a :: TyFun (a ~> b) (Option a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (Option_Sym1 d a) #
SingI (Unzip4Sym0 :: TyFun [(a, b, c, d)] ([a], [b], [c], [d]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip4Sym0 #
SingI d => SingI (ListzipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListzipWithSym1 d) #
(SingI d1, SingI d2) => SingI (ListscanrSym2 d1 d2 :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListscanrSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (ListscanlSym2 d1 d2 :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListscanlSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (ListfoldrSym2 d1 d2 :: TyFun [a] b -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListfoldrSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (ListfoldlSym2 d1 d2 :: TyFun [a] b -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListfoldlSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (Listfoldl'Sym2 d1 d2 :: TyFun [a] b -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (Listfoldl'Sym2 d1 d2) #
SingI d => SingI (ZipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWithSym1 d) #
SingI d => SingI (Zip3Sym1 d b c :: TyFun [b] ([c] ~> [(a, b, c)]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Zip3Sym1 d b c) #
(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanrSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ScanlSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun [a] b -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Foldl'Sym2 d1 d2) #
(SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun [a] b -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FoldrSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun [a] b -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (FoldlSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Maybe Methods sing :: Sing (Maybe_Sym2 d1 d2) #
SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing (UncurrySym1 d) #
SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing (CurrySym1 d) #
(STraversable t, SApplicative f) => SingI (ForSym0 :: TyFun (t a) ((a ~> f b) ~> f (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing ForSym0 #
(STraversable t, SMonad m) => SingI (ForMSym0 :: TyFun (t a) ((a ~> m b) ~> m (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing ForMSym0 #
(STraversable t, SMonoid m, SingI d) => SingI (FoldMapDefaultSym1 d t :: TyFun (t a) m -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (FoldMapDefaultSym1 d t) #
(STraversable t, SingI d) => SingI (FmapDefaultSym1 d t :: TyFun (t a) (t b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (FmapDefaultSym1 d t) #
SingI d => SingI (MapAccumRSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (MapAccumRSym1 d) #
SingI d => SingI (MapAccumLSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (MapAccumLSym1 d) #
(SMonadPlus m, SingI d) => SingI (MplusSym1 d :: TyFun (m a) (m a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (MplusSym1 d) #
(SMonad m, SingI d) => SingI (LiftMSym1 d m :: TyFun (m a1) (m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftMSym1 d m) #
(SApplicative f, SingI d) => SingI (LiftASym1 d f :: TyFun (f a) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftASym1 d f) #
(SFunctor f, SingI d) => SingI (FmapSym1 d f :: TyFun (f a) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (FmapSym1 d f) #
(SMonad m, SingI d) => SingI (ApSym1 d :: TyFun (m a) (m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (ApSym1 d) #
SMonad m => SingI ((>>@#@$) :: TyFun (m a) (m b ~> m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (>>@#@$) #
(SMonad m, SingI d) => SingI ((=<<@#@$$) d :: TyFun (m a) (m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((=<<@#@$$) d) #
(SAlternative f, SingI d) => SingI ((<\|>@#@$$) d :: TyFun (f a) (f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<\|>@#@$$) d) #
SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (<*@#@$) #
(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((<*>@#@$$) d) #
(SApplicative f, SingI d) => SingI (d <**>@#@$$ b :: TyFun (f (a ~> b)) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d <**>@#@$$ b) #
(SFunctor f, SingI d) => SingI ((d <$@#@$$ f) b :: TyFun (f b) (f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing ((d <$@#@$$ f) b) #
SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (*>@#@$) #
(SFoldable t, SMonadPlus m) => SingI (MsumSym0 :: TyFun (t (m a)) (m a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MsumSym0 #
(SFoldable t, SApplicative f) => SingI (For_Sym0 :: TyFun (t a) ((a ~> f b) ~> f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing For_Sym0 #
(SFoldable t, SMonad m) => SingI (ForM_Sym0 :: TyFun (t a) ((a ~> m b) ~> m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing ForM_Sym0 #
(SFoldable t, SingI d) => SingI (FoldrSym1 d t :: TyFun b (t a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrSym1 d t) #
(SFoldable t, SingI d) => SingI (Foldr'Sym1 d t :: TyFun b (t a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldr'Sym1 d t) #
(SFoldable t, SingI d) => SingI (FoldlSym1 d t :: TyFun b (t a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlSym1 d t) #
(SFoldable t, SingI d) => SingI (Foldl'Sym1 d t :: TyFun b (t a ~> b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldl'Sym1 d t) #
(SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d t :: TyFun (t a) m -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldMapSym1 d t) #
(SFoldable t, SingI d) => SingI (ConcatMapSym1 d t :: TyFun (t a) [b] -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (ConcatMapSym1 d t) #
(SFoldable t, SAlternative f) => SingI (AsumSym0 :: TyFun (t (f a)) (f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing AsumSym0 #
SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FlipSym1 d) #
SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple4Sym0 #
SingI d => SingI (Tuple3Sym1 d b c :: TyFun b (c ~> (a, b, c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple3Sym1 d b c) #
(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type)
Instance details Defined in Data.Singletons.Prelude.Ord Methods sing :: Sing (ComparingSym2 d1 d2) #
(SFunctor f, SingI d) => SingI (d <$>@#@$$ f :: TyFun (f a) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d <$>@#@$$ f) #
(SFunctor f, SingI d) => SingI (d $>@#@$$ b :: TyFun b (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d $>@#@$$ b) #
(SingI d1, SingI d2) => SingI (Option_Sym2 d1 d2 :: TyFun (Option a) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods sing :: Sing (Option_Sym2 d1 d2) #
(STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing TraverseSym0 #
(STraversable t, SMonad m) => SingI (MapMSym0 :: TyFun (a ~> m b) (t a ~> m (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing MapMSym0 #
STraversable t => SingI (MapAccumRSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing MapAccumRSym0 #
STraversable t => SingI (MapAccumLSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing MapAccumLSym0 #
SingI (ZipWith3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) ([a] ~> ([b] ~> ([c] ~> [d]))) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing ZipWith3Sym0 #
SMonad m => SingI (LiftM2Sym0 :: TyFun (a1 ~> (a2 ~> r)) (m a1 ~> (m a2 ~> m r)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftM2Sym0 #
SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA2Sym0 #
(SMonad m, SingI d) => SingI (d >>=@#@$$ b :: TyFun (a ~> m b) (m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d >>=@#@$$ b) #
(SFoldable t, SApplicative f) => SingI (Traverse_Sym0 :: TyFun (a ~> f b) (t a ~> f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing Traverse_Sym0 #
(SFoldable t, SMonad m) => SingI (MapM_Sym0 :: TyFun (a ~> m b) (t a ~> m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing MapM_Sym0 #
(SFoldable t, SMonad m) => SingI (FoldrMSym0 :: TyFun (a ~> (b ~> m b)) (b ~> (t a ~> m b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldrMSym0 #
(SFoldable t, SMonad m) => SingI (FoldlMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing FoldlMSym0 #
SingI d => SingI (Either_Sym1 d b :: TyFun (b ~> c) (Either a b ~> c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym1 d b) #
SingI d => SingI (d .@#@$$ a :: TyFun (a ~> b) (a ~> c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (d .@#@$$ a) #
(SFunctor f, SingI d) => SingI (d <&>@#@$$ b :: TyFun (a ~> b) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Functor Methods sing :: Sing (d <&>@#@$$ b) #
SingI (Unzip5Sym0 :: TyFun [(a, b, c, d, e)] ([a], [b], [c], [d], [e]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip5Sym0 #
(SingI d1, SingI d2) => SingI (ListzipWithSym2 d1 d2 :: TyFun [b] [c] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal.Disambiguation Methods sing :: Sing (ListzipWithSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun [b] [c] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWithSym2 d1 d2) #
SingI d2 => SingI (ZipWith3Sym1 d2 :: TyFun [a] ([b] ~> ([c] ~> [d1])) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWith3Sym1 d2) #
(SingI d1, SingI d2) => SingI (Zip3Sym2 d1 d2 c :: TyFun [c] [(a, b, c)] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (Zip3Sym2 d1 d2 c) #
(SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (MapAccumRSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (MapAccumLSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type)
Instance details Defined in Data.Singletons.Prelude.Either Methods sing :: Sing (Either_Sym2 d1 d2) #
(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type)
Instance details Defined in Data.Singletons.Prelude.Tuple Methods sing :: Sing (CurrySym2 d1 d2) #
(STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d t :: TyFun (t a) (f (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (TraverseSym1 d t) #
(STraversable t, SMonad m, SingI d) => SingI (MapMSym1 d t :: TyFun (t a) (m (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapMSym1 d t) #
(STraversable t, SingI d) => SingI (MapAccumRSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumRSym1 d t) #
(STraversable t, SingI d) => SingI (MapAccumLSym1 d t :: TyFun a (t b ~> (a, t c)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumLSym1 d t) #
(SMonad m, SingI d) => SingI (LiftM2Sym1 d m :: TyFun (m a1) (m a2 ~> m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM2Sym1 d m) #
(SApplicative f, SingI d) => SingI (LiftA2Sym1 d f :: TyFun (f a) (f b ~> f c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym1 d f) #
(SMonad m, SingI d) => SingI (d >>@#@$$ b :: TyFun (m b) (m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d >>@#@$$ b) #
(SApplicative f, SingI d) => SingI (d <*@#@$$ b :: TyFun (f b) (f a) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d <*@#@$$ b) #
(SApplicative f, SingI d) => SingI (d *>@#@$$ b :: TyFun (f b) (f b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (d *>@#@$$ b) #
(SFoldable t, SApplicative f, SingI d) => SingI (Traverse_Sym1 d t :: TyFun (t a) (f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Traverse_Sym1 d t) #
(SFoldable t, SMonad m, SingI d) => SingI (MapM_Sym1 d t :: TyFun (t a) (m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (MapM_Sym1 d t) #
(SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 t :: TyFun (t a) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrSym2 d1 d2 t) #
(SFoldable t, SMonad m, SingI d) => SingI (FoldrMSym1 d t :: TyFun b (t a ~> m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrMSym1 d t) #
(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 t :: TyFun (t a) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldr'Sym2 d1 d2 t) #
(SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 t :: TyFun (t a) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlSym2 d1 d2 t) #
(SFoldable t, SMonad m, SingI d) => SingI (FoldlMSym1 d t :: TyFun b (t a ~> m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlMSym1 d t) #
(SFoldable t, SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 t :: TyFun (t a) b -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (Foldl'Sym2 d1 d2 t) #
(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (FlipSym2 d1 d2) #
(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type)
Instance details Defined in Data.Singletons.Prelude.Base Methods sing :: Sing (d1 .@#@$$$ d2) #
SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple5Sym0 #
SingI d2 => SingI (Tuple4Sym1 d2 b c d1 :: TyFun b (c ~> (d1 ~> (a, b, c, d1))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym1 d2 b c d1) #
(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 c :: TyFun c (a, b, c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple3Sym2 d1 d2 c) #
(STraversable t, SApplicative f, SingI d) => SingI (ForSym1 d f b :: TyFun (a ~> f b) (f (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (ForSym1 d f b) #
(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d m b :: TyFun (a ~> m b) (m (t b)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (ForMSym1 d m b) #
SMonad m => SingI (LiftM3Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> r))) (m a1 ~> (m a2 ~> (m a3 ~> m r))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftM3Sym0 #
SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftA3Sym0 #
(SFoldable t, SApplicative f, SingI d) => SingI (For_Sym1 d f b :: TyFun (a ~> f b) (f ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (For_Sym1 d f b) #
(SFoldable t, SMonad m, SingI d) => SingI (ForM_Sym1 d m b :: TyFun (a ~> m b) (m ()) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (ForM_Sym1 d m b) #
SingI (Unzip6Sym0 :: TyFun [(a, b, c, d, e, f)] ([a], [b], [c], [d], [e], [f]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip6Sym0 #
(SingI d2, SingI d3) => SingI (ZipWith3Sym2 d2 d3 :: TyFun [b] ([c] ~> [d1]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWith3Sym2 d2 d3) #
(STraversable t, SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumRSym2 d1 d2 t) #
(STraversable t, SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 t :: TyFun (t b) (a, t c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Traversable Methods sing :: Sing (MapAccumLSym2 d1 d2 t) #
(SMonad m, SingI d) => SingI (LiftM3Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> m r)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM3Sym1 d m) #
(SMonad m, SingI d1, SingI d2) => SingI (LiftM2Sym2 d1 d2 :: TyFun (m a2) (m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM2Sym2 d1 d2) #
(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 f :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym1 d2 f) #
(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA2Sym2 d1 d2) #
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldrMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldrMSym2 d1 d2 t) #
(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldlMSym2 d1 d2 t :: TyFun (t a) (m b) -> Type)
Instance details Defined in Data.Singletons.Prelude.Foldable Methods sing :: Sing (FoldlMSym2 d1 d2 t) #
SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple6Sym0 #
SingI d2 => SingI (Tuple5Sym1 d2 b c d1 e :: TyFun b (c ~> (d1 ~> (e ~> (a, b, c, d1, e)))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym1 d2 b c d1 e) #
(SingI d2, SingI d3) => SingI (Tuple4Sym2 d2 d3 c d1 :: TyFun c (d1 ~> (a, b, c, d1)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym2 d2 d3 c d1) #
SMonad m => SingI (LiftM4Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> r)))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> m r)))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftM4Sym0 #
SingI (Unzip7Sym0 :: TyFun [(a, b, c, d, e, f, g)] ([a], [b], [c], [d], [e], [f], [g]) -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing Unzip7Sym0 #
(SingI d2, SingI d3, SingI d4) => SingI (ZipWith3Sym3 d2 d3 d4 :: TyFun [c] [d1] -> Type)
Instance details Defined in Data.Singletons.Prelude.List.Internal Methods sing :: Sing (ZipWith3Sym3 d2 d3 d4) #
(SMonad m, SingI d) => SingI (LiftM4Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> m r))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM4Sym1 d m) #
(SMonad m, SingI d1, SingI d2) => SingI (LiftM3Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM3Sym2 d1 d2) #
(SApplicative f, SingI d2, SingI d3) => SingI (LiftA3Sym2 d2 d3 :: TyFun (f b) (f c ~> f d1) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym2 d2 d3) #
SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing Tuple7Sym0 #
SingI d2 => SingI (Tuple6Sym1 d2 b c d1 e f :: TyFun b (c ~> (d1 ~> (e ~> (f ~> (a, b, c, d1, e, f))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym1 d2 b c d1 e f) #
(SingI d2, SingI d3) => SingI (Tuple5Sym2 d2 d3 c d1 e :: TyFun c (d1 ~> (e ~> (a, b, c, d1, e))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym2 d2 d3 c d1 e) #
(SingI d2, SingI d3, SingI d4) => SingI (Tuple4Sym3 d2 d3 d4 d1 :: TyFun d1 (a, b, c, d1) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple4Sym3 d2 d3 d4 d1) #
SMonad m => SingI (LiftM5Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> r))))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing LiftM5Sym0 #
(SMonad m, SingI d) => SingI (LiftM5Sym1 d m :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r)))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM5Sym1 d m) #
(SMonad m, SingI d1, SingI d2) => SingI (LiftM4Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> m r)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM4Sym2 d1 d2) #
(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM3Sym3 d1 d2 d3 :: TyFun (m a3) (m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM3Sym3 d1 d2 d3) #
(SApplicative f, SingI d2, SingI d3, SingI d4) => SingI (LiftA3Sym3 d2 d3 d4 :: TyFun (f c) (f d1) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftA3Sym3 d2 d3 d4) #
SingI d2 => SingI (Tuple7Sym1 d2 b c d1 e f g :: TyFun b (c ~> (d1 ~> (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g)))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym1 d2 b c d1 e f g) #
(SingI d2, SingI d3) => SingI (Tuple6Sym2 d2 d3 c d1 e f :: TyFun c (d1 ~> (e ~> (f ~> (a, b, c, d1, e, f)))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym2 d2 d3 c d1 e f) #
(SingI d2, SingI d3, SingI d4) => SingI (Tuple5Sym3 d2 d3 d4 d1 e :: TyFun d1 (e ~> (a, b, c, d1, e)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym3 d2 d3 d4 d1 e) #
(SMonad m, SingI d1, SingI d2) => SingI (LiftM5Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> (m a5 ~> m r))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM5Sym2 d1 d2) #
(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM4Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM4Sym3 d1 d2 d3) #
(SingI d2, SingI d3) => SingI (Tuple7Sym2 d2 d3 c d1 e f g :: TyFun c (d1 ~> (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g))))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym2 d2 d3 c d1 e f g) #
(SingI d2, SingI d3, SingI d4) => SingI (Tuple6Sym3 d2 d3 d4 d1 e f :: TyFun d1 (e ~> (f ~> (a, b, c, d1, e, f))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym3 d2 d3 d4 d1 e f) #
(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple5Sym4 d2 d3 d4 d5 e :: TyFun e (a, b, c, d1, e) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple5Sym4 d2 d3 d4 d5 e) #
(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM5Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> (m a5 ~> m r)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM5Sym3 d1 d2 d3) #
(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM4Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM4Sym4 d1 d2 d3 d4) #
(SingI d2, SingI d3, SingI d4) => SingI (Tuple7Sym3 d2 d3 d4 d1 e f g :: TyFun d1 (e ~> (f ~> (g ~> (a, b, c, d1, e, f, g)))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym3 d2 d3 d4 d1 e f g) #
(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple6Sym4 d2 d3 d4 d5 e f :: TyFun e (f ~> (a, b, c, d1, e, f)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym4 d2 d3 d4 d5 e f) #
(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM5Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m a5 ~> m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM5Sym4 d1 d2 d3 d4) #
(SingI d2, SingI d3, SingI d4, SingI d5) => SingI (Tuple7Sym4 d2 d3 d4 d5 e f g :: TyFun e (f ~> (g ~> (a, b, c, d1, e, f, g))) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym4 d2 d3 d4 d5 e f g) #
(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (Tuple6Sym5 d2 d3 d4 d5 d6 f :: TyFun f (a, b, c, d1, e, f) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple6Sym5 d2 d3 d4 d5 d6 f) #
(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4, SingI d5) => SingI (LiftM5Sym5 d1 d2 d3 d4 d5 :: TyFun (m a5) (m r) -> Type)
Instance details Defined in Data.Singletons.Prelude.Monad.Internal Methods sing :: Sing (LiftM5Sym5 d1 d2 d3 d4 d5) #
(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6) => SingI (Tuple7Sym5 d2 d3 d4 d5 d6 f g :: TyFun f (g ~> (a, b, c, d1, e, f, g)) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym5 d2 d3 d4 d5 d6 f g) #
(SingI d2, SingI d3, SingI d4, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g :: TyFun g (a, b, c, d1, e, f, g) -> Type)
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing (Tuple7Sym6 d2 d3 d4 d5 d6 d7 g) #