Morley.Michelson.Typed.Scope

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

• ParameterScope;
• StorageScope;
• ConstantScope.

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 Lorentz.Constraints module.

Scopes

class (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t, HasNoSaplingState t) => ConstantScope t

Set of constraints that Michelson applies to pushed constants.

Not just a type alias in order to be able to partially apply it

Instances

(SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoContract t, HasNoTicket t, HasNoSaplingState t) => ConstantScope t

Defined in Morley.Michelson.Typed.Scope

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoBigMap t a b, WithDeMorganScope HasNoContract t a b, WithDeMorganScope HasNoTicket t a b, WithDeMorganScope HasNoSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope ConstantScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: ConstantScope (t a b) => ((ConstantScope a, ConstantScope b) => ret) -> ret

SingI t => CheckScope (ConstantScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

class (SingI t, HasNoTicket t) => DupableScope t

Alias for constraints which Michelson requires in DUP instruction.

Instances

(SingI t, HasNoTicket t) => DupableScope t

Defined in Morley.Michelson.Typed.Scope

SingI t => CheckScope (DupableScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (DupableScope t))

class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t

Set of constraints that Michelson applies to contract storage.

Not just a type alias in order to be able to partially apply it

Instances

(SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t, HasNoContract t) => StorageScope t

Defined in Morley.Michelson.Typed.Scope

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoNestedBigMaps t a b, WithDeMorganScope HasNoContract t a b, WellTyped a, WellTyped b) => WithDeMorganScope StorageScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: StorageScope (t a b) => ((StorageScope a, StorageScope b) => ret) -> ret

SingI t => CheckScope (StorageScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

class (SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoTicket t, HasNoSaplingState t) => PackedValScope t

Set of constraints that Michelson applies to packed values.

Not just a type alias in order to be able to partially apply it

Instances

(SingI t, WellTyped t, HasNoOp t, HasNoBigMap t, HasNoTicket t, HasNoSaplingState t) => PackedValScope t

Defined in Morley.Michelson.Typed.Scope

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoBigMap t a b, WithDeMorganScope HasNoTicket t a b, WithDeMorganScope HasNoSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope PackedValScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: PackedValScope (t a b) => ((PackedValScope a, PackedValScope b) => ret) -> ret

SingI t => CheckScope (PackedValScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (PackedValScope t))

class (SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t

Set of constraints that Michelson applies to parameters.

Not just a type alias in order to be able to partially apply it

Instances

(SingI t, WellTyped t, HasNoOp t, HasNoNestedBigMaps t) => ParameterScope t

Defined in Morley.Michelson.Typed.Scope

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoNestedBigMaps t a b, WellTyped a, WellTyped b) => WithDeMorganScope ParameterScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: ParameterScope (t a b) => ((ParameterScope a, ParameterScope b) => ret) -> ret

SingI t => CheckScope (ParameterScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ParameterScope t))

type UntypedValScope t = (SingI t, HasNoOp t)

Alias for constraints which are required for untyped representation.

class (WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t

Set of constraints that Michelson applies to unpacked values.

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

Not just a type alias in order to be able to partially apply it

Instances

(WellTyped t, PackedValScope t, ConstantScope t) => UnpackedValScope t

Defined in Morley.Michelson.Typed.Scope

(WithDeMorganScope PackedValScope t a b, WithDeMorganScope ConstantScope t a b, WellTyped a, WellTyped b) => WithDeMorganScope UnpackedValScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: UnpackedValScope (t a b) => ((UnpackedValScope a, UnpackedValScope b) => ret) -> ret

SingI t => CheckScope (UnpackedValScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

class (SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t

Set of constraints that Michelson applies to argument type and return type of views. All info related to views can be found in TZIP.

Not just a type alias in order to be able to partially apply it

Instances

(SingI t, HasNoOp t, HasNoBigMap t, HasNoTicket t) => ViewableScope t

Defined in Morley.Michelson.Typed.Scope

SingI t => CheckScope (ViewableScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ViewableScope t))

type ComparabilityScope t = (SingI t, Comparable t)

Alias for comparable types.

type ProperParameterBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t)

type ProperStorageBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidNestedBigMaps t, ForbidContract t)

type ProperConstantBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidContract t, ForbidTicket t, ForbidSaplingState t)

type ProperDupableBetterErrors t = (SingI t, ForbidTicket t)

type ProperPackedValBetterErrors t = (SingI t, WellTyped t, ForbidOp t, ForbidBigMap t, ForbidTicket t, ForbidSaplingState t)

type ProperUnpackedValBetterErrors t = (ProperPackedValBetterErrors t, ProperConstantBetterErrors t)

type ProperUntypedValBetterErrors t = (SingI t, ForbidOp t)

type ProperViewableBetterErrors t = (SingI t, ForbidOp t, ForbidBigMap t, ForbidTicket t)

type ProperNonComparableValBetterErrors t = (SingI t, ForbidNonComparable t)

type family IsDupableScope (t :: T) :: Bool where ...

Returns whether the type is dupable.

Equations

IsDupableScope t = Not (ContainsTicket t)

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

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

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

properDupableEvi :: forall t. ProperDupableBetterErrors t :- DupableScope t

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

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

properViewableEvi :: forall t. ProperViewableBetterErrors t :- ViewableScope t

properUntypedValEvi :: forall t. ProperUntypedValBetterErrors t :- UntypedValScope t

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

Category (:-)

Possible since GHC 7.8, when Category was made polykinded.

Defined in Data.Constraint

Methods

id :: forall (a :: k). a :- a

(.) :: forall (b :: k) (c :: k) (a :: k). (b :- c) -> (a :- b) -> a :- c

() :=> (Show (a :- b))

Defined in Data.Constraint

Methods

ins :: () :- Show (a :- b)

() :=> (Eq (a :- b))

Defined in Data.Constraint

Methods

ins :: () :- Eq (a :- b)

() :=> (Ord (a :- b))

Defined in Data.Constraint

Methods

ins :: () :- Ord (a :- b)

a => HasDict b (a :- b)

Defined in Data.Constraint

Methods

evidence :: (a :- b) -> Dict b

(Typeable p, Typeable q, p, q) => Data (p :- q)

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)

Show (a :- b)

Defined in Data.Constraint

Methods

showsPrec :: Int -> (a :- b) -> ShowS

show :: (a :- b) -> String

showList :: [a :- b] -> ShowS

a => NFData (a :- b)

Defined in Data.Constraint

Methods

rnf :: (a :- b) -> ()

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Defined in Data.Constraint

Methods

(==) :: (a :- b) -> (a :- b) -> Bool

(/=) :: (a :- b) -> (a :- b) -> Bool

Ord (a :- b)

Assumes IncoherentInstances doesn't exist.

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

data BadTypeForScope

Constructors

BtNotComparable

BtIsOperation

BtHasBigMap

BtHasNestedBigMap

BtHasContract

BtHasTicket

BtHasSaplingState

Instances

Generic BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

Associated Types

type Rep BadTypeForScope :: Type -> Type

Methods

from :: BadTypeForScope -> Rep BadTypeForScope x

to :: Rep BadTypeForScope x -> BadTypeForScope

Show BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

Methods

showsPrec :: Int -> BadTypeForScope -> ShowS

show :: BadTypeForScope -> String

showList :: [BadTypeForScope] -> ShowS

NFData BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

Methods

rnf :: BadTypeForScope -> ()

Buildable BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

Methods

build :: BadTypeForScope -> Builder

Eq BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

Methods

(==) :: BadTypeForScope -> BadTypeForScope -> Bool

(/=) :: BadTypeForScope -> BadTypeForScope -> Bool

RenderDoc BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

Methods

renderDoc :: RenderContext -> BadTypeForScope -> Doc

isRenderable :: BadTypeForScope -> Bool

type Rep BadTypeForScope

Defined in Morley.Michelson.Typed.Scope

type Rep BadTypeForScope = D1 ('MetaData "BadTypeForScope" "Morley.Michelson.Typed.Scope" "morley-1.18.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)) :+: (C1 ('MetaCons "BtHasTicket" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "BtHasSaplingState" 'PrefixI 'False) (U1 :: Type -> Type))))

class CheckScope (c :: Constraint) where

Should be present for common scopes.

Methods

checkScope :: Either BadTypeForScope (Dict c)

Check that constraint hold for a given type.

Instances

SingI t => CheckScope (ComparabilityScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))

SingI t => CheckScope (Comparable t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (Comparable t))

SingI t => CheckScope (ConstantScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ConstantScope t))

SingI t => CheckScope (DupableScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (DupableScope t))

SingI t => CheckScope (HasNoBigMap t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t))

SingI t => CheckScope (HasNoContract t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoContract t))

SingI t => CheckScope (HasNoNestedBigMaps t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t))

SingI t => CheckScope (HasNoOp t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoOp t))

SingI t => CheckScope (HasNoTicket t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoTicket t))

SingI t => CheckScope (PackedValScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (PackedValScope t))

SingI t => CheckScope (ParameterScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ParameterScope t))

SingI t => CheckScope (StorageScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (StorageScope t))

SingI t => CheckScope (UnpackedValScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (UnpackedValScope t))

SingI t => CheckScope (ViewableScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ViewableScope t))

SingI t => CheckScope (WellTyped t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (WellTyped t))

class WithDeMorganScope (c :: T -> Constraint) t a b where

Allows using a scope that can be proven true with a De Morgan law.

Many scopes are defined as not a (or rather a ~ 'False) where a is a negative property we want to avoid as a Constraint. The negative constraints are implemented with a type family that for some combination types resolves to itself applied to the type arguments in an or, e.g. A pair l r has x if l or r contain x.

Because of the De Morgan laws not (a or b) implies (not a) and (not b) or in our case: pair does not contain x -> a and b don't contain x.

Methods

withDeMorganScope :: c (t a b) => ((c a, c b) => ret) -> ret

Instances

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoBigMap t a b, WithDeMorganScope HasNoContract t a b, WithDeMorganScope HasNoTicket t a b, WithDeMorganScope HasNoSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope ConstantScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: ConstantScope (t a b) => ((ConstantScope a, ConstantScope b) => ret) -> ret

SingI a => WithDeMorganScope HasNoBigMap 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoBigMap ('TOr a b) => ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret

SingI a => WithDeMorganScope HasNoBigMap 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoBigMap ('TPair a b) => ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret

SingI a => WithDeMorganScope HasNoContract 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoContract ('TOr a b) => ((HasNoContract a, HasNoContract b) => ret) -> ret

SingI a => WithDeMorganScope HasNoContract 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoContract ('TPair a b) => ((HasNoContract a, HasNoContract b) => ret) -> ret

SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoNestedBigMaps ('TOr a b) => ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret

SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoNestedBigMaps ('TPair a b) => ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret

SingI k => WithDeMorganScope HasNoOp 'TBigMap k v

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TBigMap k v) => ((HasNoOp k, HasNoOp v) => ret) -> ret

SingI k => WithDeMorganScope HasNoOp 'TMap k v

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TMap k v) => ((HasNoOp k, HasNoOp v) => ret) -> ret

SingI a => WithDeMorganScope HasNoOp 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TOr a b) => ((HasNoOp a, HasNoOp b) => ret) -> ret

SingI a => WithDeMorganScope HasNoOp 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TPair a b) => ((HasNoOp a, HasNoOp b) => ret) -> ret

SingI a => WithDeMorganScope HasNoTicket 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoTicket ('TOr a b) => ((HasNoTicket a, HasNoTicket b) => ret) -> ret

SingI a => WithDeMorganScope HasNoTicket 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoTicket ('TPair a b) => ((HasNoTicket a, HasNoTicket b) => ret) -> ret

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoBigMap t a b, WithDeMorganScope HasNoTicket t a b, WithDeMorganScope HasNoSaplingState t a b, WellTyped a, WellTyped b) => WithDeMorganScope PackedValScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: PackedValScope (t a b) => ((PackedValScope a, PackedValScope b) => ret) -> ret

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoNestedBigMaps t a b, WellTyped a, WellTyped b) => WithDeMorganScope ParameterScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: ParameterScope (t a b) => ((ParameterScope a, ParameterScope b) => ret) -> ret

(WithDeMorganScope HasNoOp t a b, WithDeMorganScope HasNoNestedBigMaps t a b, WithDeMorganScope HasNoContract t a b, WellTyped a, WellTyped b) => WithDeMorganScope StorageScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: StorageScope (t a b) => ((StorageScope a, StorageScope b) => ret) -> ret

(WithDeMorganScope PackedValScope t a b, WithDeMorganScope ConstantScope t a b, WellTyped a, WellTyped b) => WithDeMorganScope UnpackedValScope t a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: UnpackedValScope (t a b) => ((UnpackedValScope a, UnpackedValScope b) => ret) -> ret

class (IsComparable t ~ 'True, SingI t, ComparableSuperC t) => Comparable t

Associated Types

type ComparableSuperC t :: Constraint

Constraints required for instance of a given type.

type ComparableSuperC _ = ()

Instances

Comparable 'TAddress

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TAddress

Comparable 'TBool

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TBool

Comparable 'TBytes

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TBytes

Comparable 'TChainId

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TChainId

Comparable 'TInt

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TInt

Comparable 'TKey

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TKey

Comparable 'TKeyHash

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TKeyHash

Comparable 'TMutez

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TMutez

Comparable 'TNat

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TNat

Comparable 'TNever

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TNever

Comparable 'TSignature

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TSignature

Comparable 'TString

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TString

Comparable 'TTimestamp

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TTimestamp

Comparable 'TTxRollupL2Address

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TTxRollupL2Address

Comparable 'TUnit

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC 'TUnit

SingI t => CheckScope (ComparabilityScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))

SingI t => CheckScope (Comparable t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (Comparable t))

ComparableSuperC ('TOption t) => Comparable ('TOption t)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC ('TOption t)

ComparableSuperC ('TOr t1 t2) => Comparable ('TOr t1 t2)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC ('TOr t1 t2)

ComparableSuperC ('TPair t1 t2) => Comparable ('TPair t1 t2)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type ComparableSuperC ('TPair t1 t2)

class (SingI t, WellTypedSuperC t) => WellTyped (t :: T)

This class encodes Michelson rules w.r.t where it requires comparable types. Earlier we had a dedicated type for representing comparable types CT. But then we integreated those types into T. This meant that some of the types that could be formed with various combinations of T would be illegal as per Michelson typing rule. Using this class, we inductively enforce that a type and all types it contains are well typed as per Michelson's rules.

Associated Types

type WellTypedSuperC t :: Constraint

Constraints required for instance of a given type.

type WellTypedSuperC _ = ()

Instances

WellTyped 'TAddress

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TAddress

WellTyped 'TBls12381Fr

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TBls12381Fr

WellTyped 'TBls12381G1

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TBls12381G1

WellTyped 'TBls12381G2

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TBls12381G2

WellTyped 'TBool

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TBool

WellTyped 'TBytes

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TBytes

WellTyped 'TChainId

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TChainId

WellTyped 'TChest

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TChest

WellTyped 'TChestKey

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TChestKey

WellTyped 'TInt

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TInt

WellTyped 'TKey

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TKey

WellTyped 'TKeyHash

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TKeyHash

WellTyped 'TMutez

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TMutez

WellTyped 'TNat

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TNat

WellTyped 'TNever

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TNever

WellTyped 'TOperation

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TOperation

WellTyped 'TSignature

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TSignature

WellTyped 'TString

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TString

WellTyped 'TTimestamp

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TTimestamp

WellTyped 'TTxRollupL2Address

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TTxRollupL2Address

WellTyped 'TUnit

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC 'TUnit

SingI t => CheckScope (WellTyped t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (WellTyped t))

WellTypedSuperC ('TContract t) => WellTyped ('TContract t)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TContract t)

WellTypedSuperC ('TList t) => WellTyped ('TList t)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TList t)

WellTypedSuperC ('TOption t) => WellTyped ('TOption t)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TOption t)

SingI n => WellTyped ('TSaplingState n)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TSaplingState n)

SingI n => WellTyped ('TSaplingTransaction n)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TSaplingTransaction n)

WellTypedSuperC ('TSet t) => WellTyped ('TSet t)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TSet t)

WellTypedSuperC ('TTicket t) => WellTyped ('TTicket t)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TTicket t)

WellTypedSuperC ('TBigMap k v) => WellTyped ('TBigMap k v)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TBigMap k v)

WellTypedSuperC ('TLambda t1 t2) => WellTyped ('TLambda t1 t2)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TLambda t1 t2)

WellTypedSuperC ('TMap k v) => WellTyped ('TMap k v)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TMap k v)

WellTypedSuperC ('TOr t1 t2) => WellTyped ('TOr t1 t2)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TOr t1 t2)

WellTypedSuperC ('TPair t1 t2) => WellTyped ('TPair t1 t2)

Defined in Morley.Michelson.Typed.Scope

Associated Types

type WellTypedSuperC ('TPair t1 t2)

data NotWellTyped

Error type for when a value is not well-typed.

Constructors

NotWellTyped

Fields

• nwtBadType :: T
• nwtCause :: BadTypeForScope

Instances

Buildable NotWellTyped

Defined in Morley.Michelson.Typed.Scope

Methods

build :: NotWellTyped -> Builder

Implementation internals

class ContainsBigMap t ~ 'False => HasNoBigMap t

Constraint which ensures that a value of type t does not contain big_map values.

Instances

ContainsBigMap t ~ 'False => HasNoBigMap t

Defined in Morley.Michelson.Typed.Scope

SingI a => WithDeMorganScope HasNoBigMap 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoBigMap ('TOr a b) => ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret

SingI a => WithDeMorganScope HasNoBigMap 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoBigMap ('TPair a b) => ((HasNoBigMap a, HasNoBigMap b) => ret) -> ret

SingI t => CheckScope (HasNoBigMap t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoBigMap t))

class ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t

Constraint which ensures that there are no nested bigmaps.

Instances

ContainsNestedBigMaps t ~ 'False => HasNoNestedBigMaps t

Defined in Morley.Michelson.Typed.Scope

SingI a => WithDeMorganScope HasNoNestedBigMaps 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoNestedBigMaps ('TOr a b) => ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret

SingI a => WithDeMorganScope HasNoNestedBigMaps 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoNestedBigMaps ('TPair a b) => ((HasNoNestedBigMaps a, HasNoNestedBigMaps b) => ret) -> ret

SingI t => CheckScope (HasNoNestedBigMaps t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoNestedBigMaps t))

class ContainsOp t ~ 'False => HasNoOp t

Constraint which ensures that a value of type t does not contain operations.

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

Instances

ContainsOp t ~ 'False => HasNoOp t

Defined in Morley.Michelson.Typed.Scope

SingI k => WithDeMorganScope HasNoOp 'TBigMap k v

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TBigMap k v) => ((HasNoOp k, HasNoOp v) => ret) -> ret

SingI k => WithDeMorganScope HasNoOp 'TMap k v

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TMap k v) => ((HasNoOp k, HasNoOp v) => ret) -> ret

SingI a => WithDeMorganScope HasNoOp 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TOr a b) => ((HasNoOp a, HasNoOp b) => ret) -> ret

SingI a => WithDeMorganScope HasNoOp 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoOp ('TPair a b) => ((HasNoOp a, HasNoOp b) => ret) -> ret

SingI t => CheckScope (HasNoOp t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoOp t))

class ContainsContract t ~ 'False => HasNoContract t

Constraint which ensures that a value of type t does not contain contract values.

Instances

ContainsContract t ~ 'False => HasNoContract t

Defined in Morley.Michelson.Typed.Scope

SingI a => WithDeMorganScope HasNoContract 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoContract ('TOr a b) => ((HasNoContract a, HasNoContract b) => ret) -> ret

SingI a => WithDeMorganScope HasNoContract 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoContract ('TPair a b) => ((HasNoContract a, HasNoContract b) => ret) -> ret

SingI t => CheckScope (HasNoContract t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoContract t))

class ContainsTicket t ~ 'False => HasNoTicket t

Constraint which ensures that a value of type t does not contain ticket values.

Instances

ContainsTicket t ~ 'False => HasNoTicket t

Defined in Morley.Michelson.Typed.Scope

SingI a => WithDeMorganScope HasNoTicket 'TOr a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoTicket ('TOr a b) => ((HasNoTicket a, HasNoTicket b) => ret) -> ret

SingI a => WithDeMorganScope HasNoTicket 'TPair a b

Defined in Morley.Michelson.Typed.Scope

Methods

withDeMorganScope :: HasNoTicket ('TPair a b) => ((HasNoTicket a, HasNoTicket b) => ret) -> ret

SingI t => CheckScope (HasNoTicket t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (HasNoTicket t))

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

Whether a value of this type _may_ contain a big_map value.

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 _) = 'False

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 ContainsContract (t :: T) :: Bool where ...

Whether a value of this type _may_ contain a contract value.

In some scopes (constants, storage) appearing for contract type is prohibited. Contracts in input/output of lambdas are allowed without limits though.

Equations

ContainsContract 'TKey = 'False

ContainsContract 'TUnit = 'False

ContainsContract 'TSignature = 'False

ContainsContract 'TChainId = 'False

ContainsContract ('TOption t) = ContainsContract t

ContainsContract ('TList t) = ContainsContract t

ContainsContract ('TSet _) = 'False

ContainsContract 'TOperation = 'False

ContainsContract ('TContract _) = 'True

ContainsContract ('TPair a b) = ContainsContract a || ContainsContract b

ContainsContract ('TOr a b) = ContainsContract a || ContainsContract b

ContainsContract ('TLambda _ _) = 'False

ContainsContract ('TMap _ v) = ContainsContract v

ContainsContract ('TBigMap _ v) = ContainsContract v

ContainsContract _ = 'False

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

Whether a value of this type _may_ contain nested big_maps.

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 don'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 _) = 'False

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 family ContainsOp (t :: T) :: Bool where ...

Whether a value of this type _may_ contain an operation.

In some scopes (constants, parameters, storage) appearing for operation type is prohibited. Operations in input/output of lambdas are allowed without limits though.

Equations

ContainsOp 'TKey = 'False

ContainsOp 'TUnit = 'False

ContainsOp 'TSignature = 'False

ContainsOp 'TChainId = 'False

ContainsOp ('TOption t) = ContainsOp t

ContainsOp ('TList t) = ContainsOp t

ContainsOp ('TSet t) = ContainsOp t

ContainsOp 'TOperation = 'True

ContainsOp ('TContract _) = 'False

ContainsOp ('TTicket t) = ContainsOp t

ContainsOp ('TPair a b) = ContainsOp a || ContainsOp b

ContainsOp ('TOr a b) = ContainsOp a || ContainsOp b

ContainsOp ('TLambda _ _) = 'False

ContainsOp ('TMap k v) = ContainsOp k || ContainsOp v

ContainsOp ('TBigMap k v) = ContainsOp k || ContainsOp v

ContainsOp _ = 'False

type family ContainsTicket (t :: T) :: Bool where ...

Whether a value of this type _may_ contain a ticket value.

Equations

ContainsTicket ('TOption t) = ContainsTicket t

ContainsTicket ('TList t) = ContainsTicket t

ContainsTicket ('TSet _) = 'False

ContainsTicket ('TTicket _) = 'True

ContainsTicket ('TPair a b) = ContainsTicket a || ContainsTicket b

ContainsTicket ('TOr a b) = ContainsTicket a || ContainsTicket b

ContainsTicket ('TLambda _ _) = 'False

ContainsTicket ('TMap _ v) = ContainsTicket v

ContainsTicket ('TBigMap _ v) = ContainsTicket v

ContainsTicket _ = 'False

type family IsComparable (t :: T) :: Bool where ...

Constraint which ensures that type is comparable.

Equations

IsComparable ('TPair a b) = IsComparable a && IsComparable b

IsComparable ('TOption t) = IsComparable t

IsComparable 'TBls12381Fr = 'False

IsComparable 'TBls12381G1 = 'False

IsComparable 'TBls12381G2 = 'False

IsComparable ('TList _) = 'False

IsComparable ('TSet _) = 'False

IsComparable 'TOperation = 'False

IsComparable ('TContract _) = 'False

IsComparable ('TTicket _) = 'False

IsComparable ('TOr a b) = IsComparable a && IsComparable b

IsComparable ('TLambda _ _) = 'False

IsComparable ('TMap _ _) = 'False

IsComparable ('TBigMap _ _) = 'False

IsComparable 'TChest = 'False

IsComparable 'TChestKey = 'False

IsComparable ('TSaplingState _) = 'False

IsComparable ('TSaplingTransaction _) = 'False

IsComparable _ = 'True

type ForbidOp t = FailOnOperationFound (ContainsOp t)

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)

type ForbidTicket t = FailOnTicketFound (ContainsTicket t)

type ForbidBigMap t = FailOnBigMapFound (ContainsBigMap t)

type ForbidNestedBigMaps t = FailOnNestedBigMapsFound (ContainsNestedBigMaps t)

type ForbidNonComparable t = FailOnNonComparableFound (IsComparable t)

Constraint that rises human-readable error message, in case given value can't be compared

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

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 FailOnContractFound (enabled :: Bool) :: Constraint where ...

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

Equations

FailOnContractFound 'True = TypeError ('Text "Type `contract` is not allowed in this scope")

FailOnContractFound 'False = ()

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

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 ...

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 = ()

type family FailOnTicketFound (enabled :: Bool) :: Constraint where ...

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

Equations

FailOnTicketFound 'True = TypeError ('Text "Type `ticket` is not allowed in this scope")

FailOnTicketFound 'False = ()

type family FailOnNonComparableFound (comparable :: Bool) :: Constraint where ...

Report a human-readable error that given value is not comparable

Equations

FailOnNonComparableFound 'True = ()

FailOnNonComparableFound 'False = TypeError ('Text "Only comparable types are allowed here")

data OpPresence (t :: T)

Whether a value of this type _may_ contain an operation.

Constructors

ContainsOp t ~ 'True => OpPresent

A value of type t may or may not contain an operation.

ContainsOp t ~ 'False => OpAbsent

A value of type t cannot contain big_map values.

data ContractPresence (t :: T)

Whether a value of this type _may_ contain a contract value.

Constructors

ContainsContract t ~ 'True => ContractPresent

A value of type t may or may not contain a contract value.

ContainsContract t ~ 'False => ContractAbsent

A value of type t cannot contain contract values.

data TicketPresence (t :: T)

Whether a value of this type _may_ contain a ticket value.

Constructors

ContainsTicket t ~ 'True => TicketPresent

A value of type t may or may not contain a ticket value.

ContainsTicket t ~ 'False => TicketAbsent

A value of type t cannot contain ticket values.

data BigMapPresence (t :: T)

Whether a value of this type _may_ contain a big_map value.

Constructors

ContainsBigMap t ~ 'True => BigMapPresent

A value of type t may or may not contain a big_map value.

ContainsBigMap t ~ 'False => BigMapAbsent

A value of type t cannot contain big_map values.

data NestedBigMapsPresence (t :: T)

Whether a value of this type _may_ contain nested big_maps.

Constructors

ContainsNestedBigMaps t ~ 'True => NestedBigMapsPresent

A value of type t may or may not contain nested big_maps.

ContainsNestedBigMaps t ~ 'False => NestedBigMapsAbsent

A value of type t cannot contain nested big_maps.

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

Check at runtime whether a value of the given type _may_ contain an operation.

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

Check at runtime whether a value of the given type _may_ contain a contract value.

checkTicketPresence :: Sing (ty :: T) -> TicketPresence ty

Check at runtime whether a value of the given type _may_ contain a ticket value.

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

Check at runtime whether a value of the given type _may_ contain a big_map value.

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

Check at runtime whether a value of the given type _may_ contain nested big_maps.

comparabilityPresence :: Sing t -> Maybe (Dict $ Comparable t)

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

Check at runtime that a value of the given type cannot contain operations.

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

Check at runtime that a value of the given type cannot contain contract values.

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

Check at runtime that a value of the given type cannot containt big_map values

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

Check at runtime that a value of the given type cannot contain nested big_maps.

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

Reify HasNoOp contraint from ForbidOp.

Left for backward compatibility.

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

Reify HasNoContract contraint from ForbidContract.

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

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

data Comparability t where

Constructors

CanBeCompared :: Comparable t => Comparability t

CannotBeCompared :: IsComparable t ~ 'False => Comparability t

checkComparability :: Sing t -> Comparability t

getComparableProofS :: Sing (a :: T) -> Maybe (Dict (Comparable a))

getWTP :: forall t. SingI t => Either NotWellTyped (Dict (WellTyped t))

Given a type, provide evidence that it is well typed w.r.t to the Michelson rules regarding where comparable types are required.

getWTP' :: Sing t -> Either NotWellTyped (Dict (WellTyped t))

Version of getWTP that accepts Sing at term-level.

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

SingI 'TAddress

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TAddress

SingI 'TBls12381Fr

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381Fr

SingI 'TBls12381G1

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381G1

SingI 'TBls12381G2

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBls12381G2

SingI 'TBool

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBool

SingI 'TBytes

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TBytes

SingI 'TChainId

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChainId

SingI 'TChest

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChest

SingI 'TChestKey

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TChestKey

SingI 'TInt

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TInt

SingI 'TKey

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TKey

SingI 'TKeyHash

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TKeyHash

SingI 'TMutez

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TMutez

SingI 'TNat

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TNat

SingI 'TNever

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TNever

SingI 'TOperation

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TOperation

SingI 'TSignature

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TSignature

SingI 'TString

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TString

SingI 'TTimestamp

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TTimestamp

SingI 'TTxRollupL2Address

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TTxRollupL2Address

SingI 'TUnit

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing 'TUnit

SingI 'AddressKindContract

Defined in Morley.Tezos.Address.Kinds

Methods

sing :: Sing 'AddressKindContract

SingI 'AddressKindImplicit

Defined in Morley.Tezos.Address.Kinds

Methods

sing :: Sing 'AddressKindImplicit

SingI 'AddressKindTxRollup

Defined in Morley.Tezos.Address.Kinds

Methods

sing :: Sing 'AddressKindTxRollup

SingI 'Z

Defined in Morley.Util.Peano

Methods

sing :: Sing 'Z

SingI n => SingI ('TContract n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TContract n)

SingI n => SingI ('TList n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TList n)

SingI n => SingI ('TOption n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TOption n)

SingI n => SingI ('TSaplingState n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSaplingState n)

SingI n => SingI ('TSaplingTransaction n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSaplingTransaction n)

SingI n => SingI ('TSet n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TSet n)

SingI n => SingI ('TTicket n :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TTicket n)

SingI n => SingI ('S n :: Nat)

Defined in Morley.Util.Peano

Methods

sing :: Sing ('S n)

(SingI n1, SingI n2) => SingI ('TBigMap n1 n2 :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TBigMap n1 n2)

(SingI n1, SingI n2) => SingI ('TLambda n1 n2 :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TLambda n1 n2)

(SingI n1, SingI n2) => SingI ('TMap n1 n2 :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TMap n1 n2)

(SingI n1, SingI n2) => SingI ('TOr n1 n2 :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TOr n1 n2)

(SingI n1, SingI n2) => SingI ('TPair n1 n2 :: T)

Defined in Morley.Michelson.Typed.Sing

Methods

sing :: Sing ('TPair n1 n2)

SingI t => CheckScope (ComparabilityScope t)

Defined in Morley.Michelson.Typed.Scope

Methods

checkScope :: Either BadTypeForScope (Dict (ComparabilityScope t))

SingI n => SingI ('MaxInternal n :: MaxInternal a)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ('MaxInternal n)

SingI n => SingI ('MinInternal n :: MinInternal a)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ('MinInternal n)

SingI GetAllSym0

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetAllSym0

SingI GetAnySym0

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetAnySym0

SingI ThenCmpSym0

Defined in Data.Ord.Singletons

Methods

sing :: Sing ThenCmpSym0

SingI AllSym0

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing AllSym0

SingI All_Sym0

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing All_Sym0

SingI AnySym0

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing AnySym0

SingI Any_Sym0

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing Any_Sym0

SingI ShowParenSym0

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowParenSym0

SingI EfdtNatDnSym0

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EfdtNatDnSym0

SingI EfdtNatSym0

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EfdtNatSym0

SingI EfdtNatUpSym0

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EfdtNatUpSym0

SingI EftNatSym0

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EftNatSym0

SingI ShowCharSym0

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowCharSym0

SingI ShowStringSym0

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowStringSym0

SingI ShowCommaSpaceSym0

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowCommaSpaceSym0

SingI ShowSpaceSym0

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowSpaceSym0

SingI Show_tupleSym0

Defined in Text.Show.Singletons

Methods

sing :: Sing Show_tupleSym0

SingI AndSym0

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing AndSym0

SingI OrSym0

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing OrSym0

SingI UnlinesSym0

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnlinesSym0

SingI UnwordsSym0

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnwordsSym0

SingI (&&@#@$)

Defined in Data.Bool.Singletons

Methods

sing :: Sing (&&@#@$)

SingI (||@#@$)

Defined in Data.Bool.Singletons

Methods

sing :: Sing (||@#@$)

SingI NotSym0

Defined in Data.Bool.Singletons

Methods

sing :: Sing NotSym0

SingI (<=?@#@$)

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing (<=?@#@$)

SingI DivSym0

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing DivSym0

SingI ModSym0

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing ModSym0

SingI (^@#@$)

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing (^@#@$)

SingI Log2Sym0

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing Log2Sym0

SingI (RunIdentitySym0 :: TyFun (Identity a) a -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing RunIdentitySym0

SingI (GetFirstSym0 :: TyFun (First a) (Maybe a) -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing GetFirstSym0

SingI (GetLastSym0 :: TyFun (Last a) (Maybe a) -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing GetLastSym0

SingI (GetDownSym0 :: TyFun (Down a) a -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing GetDownSym0

SingI (GetFirstSym0 :: TyFun (First a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetFirstSym0

SingI (GetLastSym0 :: TyFun (Last a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetLastSym0

SingI (GetMaxSym0 :: TyFun (Max a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetMaxSym0

SingI (GetMinSym0 :: TyFun (Min a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetMinSym0

SingI (UnwrapMonoidSym0 :: TyFun (WrappedMonoid m) m -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing UnwrapMonoidSym0

SingI (GetDualSym0 :: TyFun (Dual a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetDualSym0

SingI (GetProductSym0 :: TyFun (Product a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetProductSym0

SingI (GetSumSym0 :: TyFun (Sum a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing GetSumSym0

SSemigroup a => SingI (SconcatSym0 :: TyFun (NonEmpty a) a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing SconcatSym0

SingI d => SingI (ThenCmpSym1 d :: TyFun Ordering Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ThenCmpSym1 d)

SingI d => SingI (ShowParenSym1 d :: TyFun (Symbol ~> Symbol) (Symbol ~> Symbol) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowParenSym1 d)

SingI (ShowListWithSym0 :: TyFun (a ~> (Symbol ~> Symbol)) ([a] ~> (Symbol ~> Symbol)) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowListWithSym0

SingI (SortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SortBySym0

SingI (ListsortBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsortBySym0

SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MaximumBySym0

SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MinimumBySym0

SingI (InsertBySym0 :: TyFun (a ~> (a ~> Ordering)) (a ~> ([a] ~> [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InsertBySym0

SingI (DeleteFirstsBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DeleteFirstsBySym0

SingI (IntersectBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IntersectBySym0

SingI (UnionBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> ([a] ~> [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnionBySym0

SingI (GroupBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [[a]]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing GroupBySym0

SingI (NubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NubBySym0

SingI (ListnubBySym0 :: TyFun (a ~> (a ~> Bool)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListnubBySym0

SingI (Elem_bySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> Bool)) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Elem_bySym0

SingI (DeleteBySym0 :: TyFun (a ~> (a ~> Bool)) (a ~> ([a] ~> [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DeleteBySym0

SingI (Scanl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Scanl1Sym0

SingI (Scanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Scanr1Sym0

SingI (Listscanr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listscanr1Sym0

SingI (Foldl1'Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldl1'Sym0

SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldl1Sym0

SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldr1Sym0

SingI (Listfoldl1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listfoldl1Sym0

SingI (Listfoldr1Sym0 :: TyFun (a ~> (a ~> a)) ([a] ~> a) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listfoldr1Sym0

SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing UntilSym0

SingI (FindIndexSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe Nat) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing FindIndexSym0

SingI (FindSym0 :: TyFun (a ~> Bool) ([a] ~> Maybe a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing FindSym0

SingI (BreakSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing BreakSym0

SingI (PartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing PartitionSym0

SingI (SpanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SpanSym0

SingI (ListpartitionSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListpartitionSym0

SingI (ListspanSym0 :: TyFun (a ~> Bool) ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListspanSym0

SingI (AllSym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing AllSym0

SingI (AnySym0 :: TyFun (a ~> Bool) ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing AnySym0

SingI (FindIndicesSym0 :: TyFun (a ~> Bool) ([a] ~> [Nat]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing FindIndicesSym0

SingI (DropWhileEndSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DropWhileEndSym0

SingI (DropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DropWhileSym0

SingI (FilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing FilterSym0

SingI (TakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TakeWhileSym0

SingI (ListdropWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListdropWhileSym0

SingI (ListfilterSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListfilterSym0

SingI (ListtakeWhileSym0 :: TyFun (a ~> Bool) ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtakeWhileSym0

SingI (SelectSym0 :: TyFun (a ~> Bool) (a ~> (([a], [a]) ~> ([a], [a]))) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SelectSym0

SingI (AppEndoSym0 :: TyFun (Endo a) (a ~> a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AppEndoSym0

SingI (GetMaxInternalSym0 :: TyFun (MaxInternal a) (Maybe a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing GetMaxInternalSym0

SingI (GetMinInternalSym0 :: TyFun (MinInternal a) (Maybe a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing GetMinInternalSym0

SingI (FirstSym0 :: TyFun (Maybe a) (First a) -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing FirstSym0

SingI (LastSym0 :: TyFun (Maybe a) (Last a) -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing LastSym0

SingI (MaxInternalSym0 :: TyFun (Maybe a) (MaxInternal a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MaxInternalSym0

SingI (MinInternalSym0 :: TyFun (Maybe a) (MinInternal a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MinInternalSym0

SingI (IsJustSym0 :: TyFun (Maybe a) Bool -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing IsJustSym0

SingI (IsNothingSym0 :: TyFun (Maybe a) Bool -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing IsNothingSym0

SingI (MaybeToListSym0 :: TyFun (Maybe a) [a] -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing MaybeToListSym0

SingI (FromJustSym0 :: TyFun (Maybe a) a -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing FromJustSym0

SApplicative f => SingI (UnlessSym0 :: TyFun Bool (f () ~> f ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing UnlessSym0

SApplicative f => SingI (WhenSym0 :: TyFun Bool (f () ~> f ()) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing WhenSym0

SAlternative f => SingI (GuardSym0 :: TyFun Bool (f ()) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing GuardSym0

SingI d => SingI (EfdtNatDnSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatDnSym1 d)

SingI d => SingI (EfdtNatSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatSym1 d)

SingI d => SingI (EfdtNatUpSym1 d :: TyFun Nat (Nat ~> [Nat]) -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatUpSym1 d)

SingI (SplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SplitAtSym0

SingI (ListsplitAtSym0 :: TyFun Nat ([a] ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsplitAtSym0

SingI (DropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DropSym0

SingI (TakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TakeSym0

SingI (ListdropSym0 :: TyFun Nat ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListdropSym0

SingI (ListtakeSym0 :: TyFun Nat ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtakeSym0

SShow a => SingI (ShowsPrecSym0 :: TyFun Nat (a ~> (Symbol ~> Symbol)) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowsPrecSym0

SingI (ReplicateSym0 :: TyFun Nat (a ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ReplicateSym0

SingI d => SingI (EftNatSym1 d :: TyFun Nat [Nat] -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EftNatSym1 d)

SEnum a => SingI (ToEnumSym0 :: TyFun Nat a -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing ToEnumSym0

SNum a => SingI (FromIntegerSym0 :: TyFun Nat a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing FromIntegerSym0

SingI d => SingI (ShowCharSym1 d :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowCharSym1 d)

SingI d => SingI (ShowStringSym1 d :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowStringSym1 d)

SingI d => SingI (Show_tupleSym1 d :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (Show_tupleSym1 d)

SingI (CatMaybesSym0 :: TyFun [Maybe a] [a] -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing CatMaybesSym0

SingI (TransposeSym0 :: TyFun [[a]] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TransposeSym0

SingI (ListtransposeSym0 :: TyFun [[a]] [[a]] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtransposeSym0

SingI (ConcatSym0 :: TyFun [[a]] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ConcatSym0

SingI ((!!@#@$) :: TyFun [a] (Nat ~> a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (!!@#@$)

SingI (ListindexSym0 :: TyFun [a] (Nat ~> a) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListindexSym0

SShow a => SingI (ShowListSym0 :: TyFun [a] (Symbol ~> Symbol) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowListSym0

SingI (IntercalateSym0 :: TyFun [a] ([[a]] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IntercalateSym0

SEq a => SingI (IsInfixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IsInfixOfSym0

SEq a => SingI (IsPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IsPrefixOfSym0

SEq a => SingI (IsSuffixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IsSuffixOfSym0

SEq a => SingI (ListisPrefixOfSym0 :: TyFun [a] ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListisPrefixOfSym0

SEq a => SingI (IntersectSym0 :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IntersectSym0

SEq a => SingI (UnionSym0 :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnionSym0

SEq a => SingI ((\\@#@$) :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (\\@#@$)

SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (++@#@$)

SingI (ListToMaybeSym0 :: TyFun [a] (Maybe a) -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing ListToMaybeSym0

SingI (NullSym0 :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NullSym0

SingI (ListnullSym0 :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListnullSym0

SingI (LengthSym0 :: TyFun [a] Nat -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing LengthSym0

SingI (ListlengthSym0 :: TyFun [a] Nat -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListlengthSym0

SEq a => SingI (GroupSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing GroupSym0

SingI (InitsSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InitsSym0

SingI (NonEmptySubsequencesSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NonEmptySubsequencesSym0

SingI (PermutationsSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing PermutationsSym0

SingI (SubsequencesSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SubsequencesSym0

SingI (TailsSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TailsSym0

SingI (ListinitsSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListinitsSym0

SingI (ListtailsSym0 :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListtailsSym0

SingI (InitSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InitSym0

SEq a => SingI (NubSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NubSym0

SingI (ReverseSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ReverseSym0

SOrd a => SingI (SortSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SortSym0

SingI (TailSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing TailSym0

SingI (ListinitSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListinitSym0

SingI (ListreverseSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListreverseSym0

SOrd a => SingI (ListsortSym0 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsortSym0

SingI (HeadSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing HeadSym0

SingI (LastSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing LastSym0

SOrd a => SingI (MaximumSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MaximumSym0

SOrd a => SingI (MinimumSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MinimumSym0

SNum a => SingI (ProductSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ProductSym0

SNum a => SingI (SumSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing SumSym0

SingI (ListlastSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListlastSym0

SOrd a => SingI (ListmaximumSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListmaximumSym0

SOrd a => SingI (ListminimumSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListminimumSym0

SNum a => SingI (ListproductSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListproductSym0

SNum a => SingI (ListsumSym0 :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListsumSym0

SMonoid a => SingI (MconcatSym0 :: TyFun [a] a -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing MconcatSym0

SingI (IdentitySym0 :: TyFun a (Identity a) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing IdentitySym0

SingI (DownSym0 :: TyFun a (Down a) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing DownSym0

SingI (FirstSym0 :: TyFun a (First a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing FirstSym0

SingI (LastSym0 :: TyFun a (Last a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing LastSym0

SingI (MaxSym0 :: TyFun a (Max a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing MaxSym0

SingI (MinSym0 :: TyFun a (Min a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing MinSym0

SingI (DualSym0 :: TyFun a (Dual a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing DualSym0

SingI (ProductSym0 :: TyFun a (Product a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing ProductSym0

SingI (Product_Sym0 :: TyFun a (Product a) -> Type)

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing Product_Sym0

SingI (SumSym0 :: TyFun a (Sum a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing SumSym0

SingI (Sum_Sym0 :: TyFun a (Sum a) -> Type)

Defined in Data.Semigroup.Singletons.Internal.Disambiguation

Methods

sing :: Sing Sum_Sym0

SingI (FromMaybeSym0 :: TyFun a (Maybe a ~> a) -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing FromMaybeSym0

SShow a => SingI (ShowsSym0 :: TyFun a (Symbol ~> Symbol) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing ShowsSym0

SingI ((:|@#@$) :: TyFun a ([a] ~> NonEmpty a) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (:|@#@$)

SEq a => SingI (ElemIndexSym0 :: TyFun a ([a] ~> Maybe Nat) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ElemIndexSym0

SEq a => SingI (ElemSym0 :: TyFun a ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ElemSym0

SEq a => SingI (NotElemSym0 :: TyFun a ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing NotElemSym0

SEq a => SingI (ListelemSym0 :: TyFun a ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListelemSym0

SEq a => SingI (ElemIndicesSym0 :: TyFun a ([a] ~> [Nat]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ElemIndicesSym0

SEq a => SingI (DeleteSym0 :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing DeleteSym0

SOrd a => SingI (InsertSym0 :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing InsertSym0

SingI (IntersperseSym0 :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing IntersperseSym0

SingI (PrependToAllSym0 :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing PrependToAllSym0

SOrd a => SingI (ListinsertSym0 :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListinsertSym0

SingI (ListintersperseSym0 :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListintersperseSym0

SingI ((:@#@$) :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (:@#@$)

SOrd a => SingI (CompareSym0 :: TyFun a (a ~> Ordering) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing CompareSym0

SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing Bool_Sym0

SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EnumFromThenToSym0

SEq a => SingI ((/=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing (/=@#@$)

SEq a => SingI ((==@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing (==@#@$)

SOrd a => SingI ((<=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (<=@#@$)

SOrd a => SingI ((<@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (<@#@$)

SOrd a => SingI ((>=@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (>=@#@$)

SOrd a => SingI ((>@#@$) :: TyFun a (a ~> Bool) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (>@#@$)

SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing EnumFromToSym0

SMonoid a => SingI (MappendSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing MappendSym0

SOrd a => SingI (MaxSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing MaxSym0

SOrd a => SingI (MinSym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing MinSym0

SOrd a => SingI (Max_Sym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing Max_Sym0

SOrd a => SingI (Min_Sym0 :: TyFun a (a ~> a) -> Type)

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing Min_Sym0

SSemigroup a => SingI ((<>@#@$) :: TyFun a (a ~> a) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing (<>@#@$)

SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing AsTypeOfSym0

SNum a => SingI ((*@#@$) :: TyFun a (a ~> a) -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing (*@#@$)

SNum a => SingI ((+@#@$) :: TyFun a (a ~> a) -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing (+@#@$)

SNum a => SingI ((-@#@$) :: TyFun a (a ~> a) -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing (-@#@$)

SNum a => SingI (SubtractSym0 :: TyFun a (a ~> a) -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing SubtractSym0

SingI (JustSym0 :: TyFun a (Maybe a) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing JustSym0

SEnum a => SingI (FromEnumSym0 :: TyFun a Nat -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing FromEnumSym0

SShow a => SingI (Show_Sym0 :: TyFun a Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing Show_Sym0

SEnum a => SingI (PredSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing PredSym0

SEnum a => SingI (SuccSym0 :: TyFun a a -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing SuccSym0

SingI (IdSym0 :: TyFun a a -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing IdSym0

SNum a => SingI (AbsSym0 :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing AbsSym0

SNum a => SingI (NegateSym0 :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing NegateSym0

SNum a => SingI (SignumSym0 :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing SignumSym0

SingI (WrapMonoidSym0 :: TyFun m (WrappedMonoid m) -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing WrapMonoidSym0

SFoldable t => SingI (AndSym0 :: TyFun (t Bool) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AndSym0

SFoldable t => SingI (OrSym0 :: TyFun (t Bool) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing OrSym0

SingI (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing IfSym0

SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing ((&&@#@$$) x)

SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing ((||@#@$$) x)

SingI x => SingI ((<=?@#@$$) x :: TyFun Nat Bool -> Type)

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing ((<=?@#@$$) x)

SingI x => SingI (DivSym1 x :: TyFun Nat Nat -> Type)

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing (DivSym1 x)

SingI x => SingI (ModSym1 x :: TyFun Nat Nat -> Type)

Defined in GHC.TypeLits.Singletons

Methods

sing :: Sing (ModSym1 x)

SingI x => SingI ((^@#@$$) x :: TyFun Nat Nat -> Type)

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing ((^@#@$$) x)

SingI (IsLeftSym0 :: TyFun (Either a b) Bool -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing IsLeftSym0

SingI (IsRightSym0 :: TyFun (Either a b) Bool -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing IsRightSym0

SFoldable t => SingI (MaximumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MaximumBySym0

SFoldable t => SingI (MinimumBySym0 :: TyFun (a ~> (a ~> Ordering)) (t a ~> a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MinimumBySym0

SFoldable t => SingI (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldl1Sym0

SFoldable t => SingI (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (t a ~> a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldr1Sym0

SingI (ScanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ScanrSym0

SingI (ListscanrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> [b])) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListscanrSym0

SingI (ListfoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListfoldrSym0

SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> ([a] ~> b)) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing FoldrSym0

SingI (MapMaybeSym0 :: TyFun (a ~> Maybe b) ([a] ~> [b]) -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing MapMaybeSym0

SMonadPlus m => SingI (MfilterSym0 :: TyFun (a ~> Bool) (m a ~> m a) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing MfilterSym0

SFoldable t => SingI (FindSym0 :: TyFun (a ~> Bool) (t a ~> Maybe a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FindSym0

SFoldable t => SingI (AllSym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AllSym0

SFoldable t => SingI (AnySym0 :: TyFun (a ~> Bool) (t a ~> Bool) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AnySym0

SingI (ConcatMapSym0 :: TyFun (a ~> [b]) ([a] ~> [b]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ConcatMapSym0

SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (UntilSym1 d)

SingI (ListmapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListmapSym0

SingI (MapSym0 :: TyFun (a ~> b) ([a] ~> [b]) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing MapSym0

SingI (($!@#@$) :: TyFun (a ~> b) (a ~> b) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing ($!@#@$)

SingI (($@#@$) :: TyFun (a ~> b) (a ~> b) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing ($@#@$)

SApplicative m => SingI (FilterMSym0 :: TyFun (a ~> m Bool) ([a] ~> m [a]) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing FilterMSym0

SingI (ScanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ScanlSym0

SingI (ListscanlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> [b])) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListscanlSym0

SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Foldl'Sym0

SingI (Listfoldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing Listfoldl'Sym0

SingI (ListfoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListfoldlSym0

SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> ([a] ~> b)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing FoldlSym0

SingI (UnfoldrSym0 :: TyFun (b ~> Maybe (a, b)) (b ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnfoldrSym0

SOrd a => SingI (ComparingSym0 :: TyFun (b ~> a) (b ~> (b ~> Ordering)) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing ComparingSym0

SingI (RunStateLSym0 :: TyFun (StateL s a) (s ~> (s, a)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing RunStateLSym0

SingI (RunStateRSym0 :: TyFun (StateR s a) (s ~> (s, a)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing RunStateRSym0

SingI d => SingI (FromMaybeSym1 d :: TyFun (Maybe a) a -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (FromMaybeSym1 d)

SingI (SwapSym0 :: TyFun (a, b) (b, a) -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing SwapSym0

SingI (FstSym0 :: TyFun (a, b) a -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing FstSym0

SingI (SndSym0 :: TyFun (a, b) b -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing SndSym0

SApplicative m => SingI (ReplicateM_Sym0 :: TyFun Nat (m a ~> m ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ReplicateM_Sym0

SApplicative m => SingI (ReplicateMSym0 :: TyFun Nat (m a ~> m [a]) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ReplicateMSym0

(SingI d1, SingI d2) => SingI (EfdtNatDnSym2 d1 d2 :: TyFun Nat [Nat] -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatDnSym2 d1 d2)

(SingI d1, SingI d2) => SingI (EfdtNatSym2 d1 d2 :: TyFun Nat [Nat] -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatSym2 d1 d2)

(SingI d1, SingI d2) => SingI (EfdtNatUpSym2 d1 d2 :: TyFun Nat [Nat] -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EfdtNatUpSym2 d1 d2)

SingI d => SingI ((!!@#@$$) d :: TyFun Nat a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ((!!@#@$$) d)

SingI d => SingI (ListindexSym1 d :: TyFun Nat a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListindexSym1 d)

(SShow a, SingI d) => SingI (ShowListSym1 d :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowListSym1 d)

(SingI d1, SingI d2) => SingI (ShowParenSym2 d1 d2 :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowParenSym2 d1 d2)

(SShow a, SingI d) => SingI (ShowsSym1 d :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowsSym1 d)

SingI (ErrorSym0 :: TyFun Symbol a -> Type)

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing ErrorSym0

SingI (ErrorWithoutStackTraceSym0 :: TyFun Symbol a -> Type)

Defined in GHC.TypeLits.Singletons.Internal

Methods

sing :: Sing ErrorWithoutStackTraceSym0

SingI (PartitionEithersSym0 :: TyFun [Either a b] ([a], [b]) -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing PartitionEithersSym0

SingI (LeftsSym0 :: TyFun [Either a b] [a] -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing LeftsSym0

SingI (RightsSym0 :: TyFun [Either a b] [b] -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing RightsSym0

SingI (UnzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing UnzipSym0

SingI (ListunzipSym0 :: TyFun [(a, b)] ([a], [b]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListunzipSym0

SingI d => SingI (IntercalateSym1 d :: TyFun [[a]] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntercalateSym1 d)

SingI d => SingI ((:|@#@$$) d :: TyFun [a] (NonEmpty a) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing ((:|@#@$$) d)

SingI d => SingI (ShowListWithSym1 d :: TyFun [a] (Symbol ~> Symbol) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowListWithSym1 d)

SingI d => SingI (DeleteFirstsBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteFirstsBySym1 d)

SingI d => SingI (IntersectBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersectBySym1 d)

SingI d => SingI (UnionBySym1 d :: TyFun [a] ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnionBySym1 d)

SingI (ZipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ZipSym0

SingI (ListzipSym0 :: TyFun [a] ([b] ~> [(a, b)]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListzipSym0

(SEq a, SingI d) => SingI (ElemIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ElemIndexSym1 d)

SingI d => SingI (FindIndexSym1 d :: TyFun [a] (Maybe Nat) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FindIndexSym1 d)

SingI d => SingI (FindSym1 d :: TyFun [a] (Maybe a) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FindSym1 d)

SingI d => SingI (BreakSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (BreakSym1 d)

SingI d => SingI (PartitionSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (PartitionSym1 d)

SingI d => SingI (SpanSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SpanSym1 d)

SingI d => SingI (SplitAtSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SplitAtSym1 d)

SingI d => SingI (ListpartitionSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListpartitionSym1 d)

SingI d => SingI (ListspanSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListspanSym1 d)

SingI d => SingI (ListsplitAtSym1 d :: TyFun [a] ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListsplitAtSym1 d)

SingI d => SingI (AllSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (AllSym1 d)

SingI d => SingI (AnySym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (AnySym1 d)

(SEq a, SingI d) => SingI (ElemSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ElemSym1 d)

(SEq a, SingI d) => SingI (IsInfixOfSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IsInfixOfSym1 d)

(SEq a, SingI d) => SingI (IsPrefixOfSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IsPrefixOfSym1 d)

(SEq a, SingI d) => SingI (IsSuffixOfSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IsSuffixOfSym1 d)

(SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (NotElemSym1 d)

(SEq a, SingI d) => SingI (ListelemSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListelemSym1 d)

(SEq a, SingI d) => SingI (ListisPrefixOfSym1 d :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListisPrefixOfSym1 d)

(SEq a, SingI d) => SingI (ElemIndicesSym1 d :: TyFun [a] [Nat] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ElemIndicesSym1 d)

SingI d => SingI (FindIndicesSym1 d :: TyFun [a] [Nat] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FindIndicesSym1 d)

SingI d => SingI (GroupBySym1 d :: TyFun [a] [[a]] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (GroupBySym1 d)

(SEq a, SingI d) => SingI (DeleteSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteSym1 d)

SingI d => SingI (DropSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DropSym1 d)

SingI d => SingI (DropWhileEndSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DropWhileEndSym1 d)

SingI d => SingI (DropWhileSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DropWhileSym1 d)

SingI d => SingI (FilterSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (FilterSym1 d)

(SOrd a, SingI d) => SingI (InsertSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (InsertSym1 d)

(SEq a, SingI d) => SingI (IntersectSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersectSym1 d)

SingI d => SingI (IntersperseSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersperseSym1 d)

SingI d => SingI (NubBySym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (NubBySym1 d)

SingI d => SingI (PrependToAllSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (PrependToAllSym1 d)

SingI d => SingI (Scanl1Sym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Scanl1Sym1 d)

SingI d => SingI (Scanr1Sym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Scanr1Sym1 d)

SingI d => SingI (SortBySym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SortBySym1 d)

SingI d => SingI (TakeSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (TakeSym1 d)

SingI d => SingI (TakeWhileSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (TakeWhileSym1 d)

(SEq a, SingI d) => SingI (UnionSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnionSym1 d)

(SEq a, SingI d) => SingI ((\\@#@$$) d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ((\\@#@$$) d)

SingI d => SingI (ListdropSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListdropSym1 d)

SingI d => SingI (ListdropWhileSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListdropWhileSym1 d)

SingI d => SingI (ListfilterSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfilterSym1 d)

(SOrd a, SingI d) => SingI (ListinsertSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListinsertSym1 d)

SingI d => SingI (ListintersperseSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListintersperseSym1 d)

SingI d => SingI (ListnubBySym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListnubBySym1 d)

SingI d => SingI (Listscanr1Sym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listscanr1Sym1 d)

SingI d => SingI (ListsortBySym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListsortBySym1 d)

SingI d => SingI (ListtakeSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListtakeSym1 d)

SingI d => SingI (ListtakeWhileSym1 d :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListtakeWhileSym1 d)

SingI d => SingI ((:@#@$$) d :: TyFun [a] [a] -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing ((:@#@$$) d)

SingI d => SingI ((++@#@$$) d :: TyFun [a] [a] -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing ((++@#@$$) d)

SingI d => SingI (Foldl1'Sym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl1'Sym1 d)

SingI d => SingI (Foldl1Sym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl1Sym1 d)

SingI d => SingI (Foldr1Sym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldr1Sym1 d)

SingI d => SingI (MaximumBySym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MaximumBySym1 d)

SingI d => SingI (MinimumBySym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MinimumBySym1 d)

SingI d => SingI (Listfoldl1Sym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl1Sym1 d)

SingI d => SingI (Listfoldr1Sym1 d :: TyFun [a] a -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldr1Sym1 d)

SNum i => SingI (GenericLengthSym0 :: TyFun [a] i -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing GenericLengthSym0

SingI (LeftSym0 :: TyFun a (Either a b) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing LeftSym0

(SOrd a, SingI d) => SingI (CompareSym1 d :: TyFun a Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (CompareSym1 d)

SingI d => SingI (SelectSym1 d :: TyFun a (([a], [a]) ~> ([a], [a])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SelectSym1 d)

SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing (Bool_Sym1 d)

(SShow a, SingI d) => SingI (ShowsPrecSym1 d :: TyFun a (Symbol ~> Symbol) -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowsPrecSym1 d)

SEq a => SingI (LookupSym0 :: TyFun a ([(a, b)] ~> Maybe b) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing LookupSym0

SingI d => SingI (Elem_bySym1 d :: TyFun a ([a] ~> Bool) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Elem_bySym1 d)

SingI d => SingI (DeleteBySym1 d :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteBySym1 d)

SingI d => SingI (InsertBySym1 d :: TyFun a ([a] ~> [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (InsertBySym1 d)

(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EnumFromThenToSym1 d)

SingI (ArgSym0 :: TyFun a (b ~> Arg a b) -> Type)

Defined in Data.Semigroup.Singletons

Methods

sing :: Sing ArgSym0

SingI (Tuple2Sym0 :: TyFun a (b ~> (a, b)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple2Sym0

SingI (ConstSym0 :: TyFun a (b ~> a) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing ConstSym0

SingI (SeqSym0 :: TyFun a (b ~> b) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing SeqSym0

SingI (AsProxyTypeOfSym0 :: TyFun a (proxy a ~> a) -> Type)

Defined in Data.Proxy.Singletons

Methods

sing :: Sing AsProxyTypeOfSym0

(SFoldable t, SEq a) => SingI (ElemSym0 :: TyFun a (t a ~> Bool) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ElemSym0

(SFoldable t, SEq a) => SingI (NotElemSym0 :: TyFun a (t a ~> Bool) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing NotElemSym0

(SEq a, SingI d) => SingI ((/=@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing ((/=@#@$$) d)

(SEq a, SingI d) => SingI ((==@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Eq.Singletons

Methods

sing :: Sing ((==@#@$$) d)

(SOrd a, SingI d) => SingI ((<=@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing ((<=@#@$$) d)

(SOrd a, SingI d) => SingI ((<@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing ((<@#@$$) d)

(SOrd a, SingI d) => SingI ((>=@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing ((>=@#@$$) d)

(SOrd a, SingI d) => SingI ((>@#@$$) d :: TyFun a Bool -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing ((>@#@$$) d)

SingI d => SingI (ReplicateSym1 d :: TyFun a [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ReplicateSym1 d)

(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EnumFromToSym1 d)

SingI d => SingI (AppEndoSym1 d :: TyFun a a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (AppEndoSym1 d)

(SMonoid a, SingI d) => SingI (MappendSym1 d :: TyFun a a -> Type)

Defined in Data.Monoid.Singletons

Methods

sing :: Sing (MappendSym1 d)

(SOrd a, SingI d) => SingI (MaxSym1 d :: TyFun a a -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (MaxSym1 d)

(SOrd a, SingI d) => SingI (MinSym1 d :: TyFun a a -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (MinSym1 d)

(SOrd a, SingI d) => SingI (Max_Sym1 d :: TyFun a a -> Type)

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing (Max_Sym1 d)

(SOrd a, SingI d) => SingI (Min_Sym1 d :: TyFun a a -> Type)

Defined in Data.Ord.Singletons.Disambiguation

Methods

sing :: Sing (Min_Sym1 d)

(SSemigroup a, SingI d) => SingI ((<>@#@$$) d :: TyFun a a -> Type)

Defined in Data.Semigroup.Singletons.Internal

Methods

sing :: Sing ((<>@#@$$) d)

SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (AsTypeOfSym1 d)

(SNum a, SingI d) => SingI ((*@#@$$) d :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing ((*@#@$$) d)

(SNum a, SingI d) => SingI ((+@#@$$) d :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing ((+@#@$$) d)

(SNum a, SingI d) => SingI ((-@#@$$) d :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing ((-@#@$$) d)

(SNum a, SingI d) => SingI (SubtractSym1 d :: TyFun a a -> Type)

Defined in GHC.Num.Singletons

Methods

sing :: Sing (SubtractSym1 d)

SApplicative f => SingI (PureSym0 :: TyFun a (f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing PureSym0

SMonad m => SingI (ReturnSym0 :: TyFun a (m a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ReturnSym0

SingI (RightSym0 :: TyFun b (Either a b) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing RightSym0

SingI (Maybe_Sym0 :: TyFun b ((a ~> b) ~> (Maybe a ~> b)) -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing Maybe_Sym0

(SApplicative f, SingI d) => SingI (UnlessSym1 d :: TyFun (f ()) (f ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (UnlessSym1 d)

(SApplicative f, SingI d) => SingI (WhenSym1 d :: TyFun (f ()) (f ()) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (WhenSym1 d)

SAlternative f => SingI (OptionalSym0 :: TyFun (f a) (f (Maybe a)) -> Type)

Defined in Control.Applicative.Singletons

Methods

sing :: Sing OptionalSym0

SFunctor f => SingI (VoidSym0 :: TyFun (f a) (f ()) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing VoidSym0

SMonad m => SingI (JoinSym0 :: TyFun (m (m a)) (m a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing JoinSym0

SFoldable t => SingI (ConcatSym0 :: TyFun (t [a]) [a] -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ConcatSym0

SFoldable t => SingI (ToListSym0 :: TyFun (t a) [a] -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ToListSym0

(SFoldable t, SOrd a) => SingI (MaximumSym0 :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MaximumSym0

(SFoldable t, SOrd a) => SingI (MinimumSym0 :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MinimumSym0

(SFoldable t, SNum a) => SingI (ProductSym0 :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ProductSym0

(SFoldable t, SNum a) => SingI (SumSym0 :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing SumSym0

(SFoldable t, SMonoid m) => SingI (FoldSym0 :: TyFun (t m) m -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldSym0

SingI c => SingI (IfSym1 c :: TyFun k (k ~> k) -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing (IfSym1 c)

SingI a => SingI ('WrapSing s :: WrappedSing a)

Defined in Data.Singletons

Methods

sing :: Sing ('WrapSing s)

SingI (GetConstSym0 :: TyFun (Const a b) a -> Type)

Defined in Data.Functor.Const.Singletons

Methods

sing :: Sing GetConstSym0

SingI (CurrySym0 :: TyFun ((a, b) ~> c) (a ~> (b ~> c)) -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing CurrySym0

SFoldable t => SingI (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldr'Sym0

SFoldable t => SingI (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (t a ~> b)) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldrSym0

SingI (UncurrySym0 :: TyFun (a ~> (b ~> c)) ((a, b) ~> c) -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing UncurrySym0

SingI (ZipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ZipWithSym0

SingI (ListzipWithSym0 :: TyFun (a ~> (b ~> c)) ([a] ~> ([b] ~> [c])) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing ListzipWithSym0

SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing FlipSym0

SFoldable t => SingI (ConcatMapSym0 :: TyFun (a ~> [b]) (t a ~> [b]) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ConcatMapSym0

SingI d => SingI (Maybe_Sym1 d :: TyFun (a ~> b) (Maybe a ~> b) -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (Maybe_Sym1 d)

SFunctor f => SingI (FmapSym0 :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing FmapSym0

SApplicative f => SingI (LiftASym0 :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftASym0

SFunctor f => SingI ((<$>@#@$) :: TyFun (a ~> b) (f a ~> f b) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing (<$>@#@$)

SMonad m => SingI ((<$!>@#@$) :: TyFun (a ~> b) (m a ~> m b) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (<$!>@#@$)

STraversable t => SingI (FmapDefaultSym0 :: TyFun (a ~> b) (t a ~> t b) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing FmapDefaultSym0

SingI (Either_Sym0 :: TyFun (a ~> c) ((b ~> c) ~> (Either a b ~> c)) -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing Either_Sym0

(SFoldable t, SMonoid m) => SingI (FoldMapSym0 :: TyFun (a ~> m) (t a ~> m) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldMapSym0

(STraversable t, SMonoid m) => SingI (FoldMapDefaultSym0 :: TyFun (a ~> m) (t a ~> m) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing FoldMapDefaultSym0

SMonad m => SingI ((=<<@#@$) :: TyFun (a ~> m b) (m a ~> m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (=<<@#@$)

SMonad m => SingI (LiftMSym0 :: TyFun (a1 ~> r) (m a1 ~> m r) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftMSym0

SingI (MapAccumLSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MapAccumLSym0

SingI (MapAccumRSym0 :: TyFun (acc ~> (x ~> (acc, y))) (acc ~> ([x] ~> (acc, [y]))) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing MapAccumRSym0

SFoldable t => SingI (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Foldl'Sym0

SFoldable t => SingI (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (t a ~> b)) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldlSym0

SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (.@#@$)

(SingI d1, SingI d2) => SingI (SelectSym2 d1 d2 :: TyFun ([a], [a]) ([a], [a]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (SelectSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing (Bool_Sym2 d1 d2)

(SingI d1, SingI d2) => SingI (ShowListWithSym2 d1 d2 :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowListWithSym2 d1 d2)

(SShow a, SingI d1, SingI d2) => SingI (ShowsPrecSym2 d1 d2 :: TyFun Symbol Symbol -> Type)

Defined in Text.Show.Singletons

Methods

sing :: Sing (ShowsPrecSym2 d1 d2)

(SEq a, SingI d) => SingI (LookupSym1 d :: TyFun [(a, b)] (Maybe b) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (LookupSym1 d)

SingI (Unzip3Sym0 :: TyFun [(a, b, c)] ([a], [b], [c]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip3Sym0

SMonadFail m => SingI (FailSym0 :: TyFun [Char] (m a) -> Type)

Defined in Control.Monad.Fail.Singletons

Methods

sing :: Sing FailSym0

SingI (Zip3Sym0 :: TyFun [a] ([b] ~> ([c] ~> [(a, b, c)])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Zip3Sym0

(SingI d1, SingI d2) => SingI (Elem_bySym2 d1 d2 :: TyFun [a] Bool -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Elem_bySym2 d1 d2)

(SingI d1, SingI d2) => SingI (DeleteBySym2 d1 d2 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (DeleteFirstsBySym2 d1 d2 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (DeleteFirstsBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (InsertBySym2 d1 d2 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (InsertBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (IntersectBySym2 d1 d2 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (IntersectBySym2 d1 d2)

(SingI d1, SingI d2) => SingI (UnionBySym2 d1 d2 :: TyFun [a] [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnionBySym2 d1 d2)

SingI d => SingI (ConcatMapSym1 d :: TyFun [a] [b] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ConcatMapSym1 d)

SingI d => SingI (ListmapSym1 d :: TyFun [a] [b] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListmapSym1 d)

SingI d => SingI (MapMaybeSym1 d :: TyFun [a] [b] -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (MapMaybeSym1 d)

SingI d => SingI (MapSym1 d :: TyFun [a] [b] -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (MapSym1 d)

(SApplicative m, SingI d) => SingI (FilterMSym1 d :: TyFun [a] (m [a]) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FilterMSym1 d)

SingI d => SingI (ZipSym1 d :: TyFun [b] [(a, b)] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipSym1 d)

SingI d => SingI (ListzipSym1 d :: TyFun [b] [(a, b)] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListzipSym1 d)

SingI (Tuple3Sym0 :: TyFun a (b ~> (c ~> (a, b, c))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple3Sym0

SFunctor f => SingI ((<$@#@$) :: TyFun a (f b ~> f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (<$@#@$)

(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type)

Defined in Data.Singletons.Base.Enum

Methods

sing :: Sing (EnumFromThenToSym2 d1 d2)

(SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (UntilSym2 d1 d2)

SingI d => SingI (($!@#@$$) d :: TyFun a b -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (($!@#@$$) d)

SingI d => SingI (($@#@$$) d :: TyFun a b -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (($@#@$$) d)

SingI d => SingI (ArgSym1 d :: TyFun b (Arg a b) -> Type)

Defined in Data.Semigroup.Singletons

Methods

sing :: Sing (ArgSym1 d)

SingI d => SingI (ScanlSym1 d :: TyFun b ([a] ~> [b]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanlSym1 d)

SingI d => SingI (ScanrSym1 d :: TyFun b ([a] ~> [b]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanrSym1 d)

SingI d => SingI (ListscanlSym1 d :: TyFun b ([a] ~> [b]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym1 d)

SingI d => SingI (ListscanrSym1 d :: TyFun b ([a] ~> [b]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym1 d)

SingI d => SingI (Foldl'Sym1 d :: TyFun b ([a] ~> b) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl'Sym1 d)

SingI d => SingI (Listfoldl'Sym1 d :: TyFun b ([a] ~> b) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym1 d)

SingI d => SingI (ListfoldlSym1 d :: TyFun b ([a] ~> b) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym1 d)

SingI d => SingI (ListfoldrSym1 d :: TyFun b ([a] ~> b) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym1 d)

SingI d => SingI (FoldlSym1 d :: TyFun b ([a] ~> b) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (FoldlSym1 d)

SingI d => SingI (FoldrSym1 d :: TyFun b ([a] ~> b) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FoldrSym1 d)

(SOrd a, SingI d) => SingI (ComparingSym1 d :: TyFun b (b ~> Ordering) -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ComparingSym1 d)

SingI d => SingI (Tuple2Sym1 d :: TyFun b (a, b) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple2Sym1 d)

SingI d => SingI (UnfoldrSym1 d :: TyFun b [a] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (UnfoldrSym1 d)

SingI d => SingI (ConstSym1 d :: TyFun b a -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (ConstSym1 d)

SingI d => SingI (SeqSym1 d :: TyFun b b -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (SeqSym1 d)

SApplicative f => SingI ((<*>@#@$) :: TyFun (f (a ~> b)) (f a ~> f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (<*>@#@$)

SFunctor f => SingI ((<&>@#@$) :: TyFun (f a) ((a ~> b) ~> f b) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing (<&>@#@$)

SFunctor f => SingI (($>@#@$) :: TyFun (f a) (b ~> f b) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing ($>@#@$)

SApplicative f => SingI ((<**>@#@$) :: TyFun (f a) (f (a ~> b) ~> f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (<**>@#@$)

SAlternative f => SingI ((<|>@#@$) :: TyFun (f a) (f a ~> f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (<|>@#@$)

(forall (a :: k1). SingI a => SingI (f a), (ApplyTyCon :: (k1 -> kr) -> k1 ~> kr) ~ (ApplyTyConAux1 :: (k1 -> kr) -> TyFun k1 kr -> Type)) => SingI (TyCon1 f :: k1 ~> kr)

Defined in Data.Singletons

Methods

sing :: Sing (TyCon1 f)

SMonad m => SingI (ApSym0 :: TyFun (m (a ~> b)) (m a ~> m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ApSym0

SMonad m => SingI ((>>=@#@$) :: TyFun (m a) ((a ~> m b) ~> m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (>>=@#@$)

SMonadPlus m => SingI (MplusSym0 :: TyFun (m a) (m a ~> m a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing MplusSym0

(SApplicative m, SingI d) => SingI (ReplicateM_Sym1 d :: TyFun (m a) (m ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ReplicateM_Sym1 d)

(SApplicative m, SingI d) => SingI (ReplicateMSym1 d :: TyFun (m a) (m [a]) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ReplicateMSym1 d)

(SMonadPlus m, SingI d) => SingI (MfilterSym1 d :: TyFun (m a) (m a) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (MfilterSym1 d)

SingI d => SingI (AsProxyTypeOfSym1 d :: TyFun (proxy a) a -> Type)

Defined in Data.Proxy.Singletons

Methods

sing :: Sing (AsProxyTypeOfSym1 d)

SingI d => SingI (RunStateLSym1 d :: TyFun s (s, a) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (RunStateLSym1 d)

SingI d => SingI (RunStateRSym1 d :: TyFun s (s, a) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (RunStateRSym1 d)

(SFoldable t, SingI d) => SingI (FindSym1 d :: TyFun (t a) (Maybe a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FindSym1 d)

(SFoldable t, SingI d) => SingI (AllSym1 d :: TyFun (t a) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (AllSym1 d)

(SFoldable t, SingI d) => SingI (AnySym1 d :: TyFun (t a) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (AnySym1 d)

(SFoldable t, SEq a, SingI d) => SingI (ElemSym1 d :: TyFun (t a) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (ElemSym1 d)

(SFoldable t, SEq a, SingI d) => SingI (NotElemSym1 d :: TyFun (t a) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (NotElemSym1 d)

SFoldable t => SingI (NullSym0 :: TyFun (t a) Bool -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing NullSym0

SFoldable t => SingI (LengthSym0 :: TyFun (t a) Nat -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing LengthSym0

(SFoldable t, SingI d) => SingI (Foldl1Sym1 d :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldl1Sym1 d)

(SFoldable t, SingI d) => SingI (Foldr1Sym1 d :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldr1Sym1 d)

(SFoldable t, SingI d) => SingI (MaximumBySym1 d :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (MaximumBySym1 d)

(SFoldable t, SingI d) => SingI (MinimumBySym1 d :: TyFun (t a) a -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (MinimumBySym1 d)

(SFoldable t, SApplicative f) => SingI (SequenceA_Sym0 :: TyFun (t (f a)) (f ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing SequenceA_Sym0

(STraversable t, SApplicative f) => SingI (SequenceASym0 :: TyFun (t (f a)) (f (t a)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing SequenceASym0

(SFoldable t, SMonad m) => SingI (Sequence_Sym0 :: TyFun (t (m a)) (m ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Sequence_Sym0

(STraversable t, SMonad m) => SingI (SequenceSym0 :: TyFun (t (m a)) (m (t a)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing SequenceSym0

SingI (ConstSym0 :: TyFun a (Const a b) -> Type)

Defined in Data.Functor.Const.Singletons

Methods

sing :: Sing ConstSym0

(SingI c, SingI t) => SingI (IfSym2 c t :: TyFun k k -> Type)

Defined in Data.Bool.Singletons

Methods

sing :: Sing (IfSym2 c t)

SingI (ZipWith3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) ([a] ~> ([b] ~> ([c] ~> [d]))) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing ZipWith3Sym0

STraversable t => SingI (MapAccumLSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing MapAccumLSym0

STraversable t => SingI (MapAccumRSym0 :: TyFun (a ~> (b ~> (a, c))) (a ~> (t b ~> (a, t c))) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing MapAccumRSym0

SApplicative f => SingI (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (f a ~> (f b ~> f c)) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftA2Sym0

(SFoldable t, SMonad m) => SingI (FoldrMSym0 :: TyFun (a ~> (b ~> m b)) (b ~> (t a ~> m b)) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldrMSym0

SApplicative m => SingI (ZipWithM_Sym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m ())) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ZipWithM_Sym0

SApplicative m => SingI (ZipWithMSym0 :: TyFun (a ~> (b ~> m c)) ([a] ~> ([b] ~> m [c])) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ZipWithMSym0

SingI d => SingI ((.@#@$$) d :: TyFun (a ~> b) (a ~> c) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing ((.@#@$$) d)

(SFunctor f, SingI d) => SingI ((<&>@#@$$) d :: TyFun (a ~> b) (f b) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing ((<&>@#@$$) d)

(SFoldable t, SApplicative f) => SingI (Traverse_Sym0 :: TyFun (a ~> f b) (t a ~> f ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing Traverse_Sym0

(STraversable t, SApplicative f) => SingI (TraverseSym0 :: TyFun (a ~> f b) (t a ~> f (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing TraverseSym0

SApplicative m => SingI (MapAndUnzipMSym0 :: TyFun (a ~> m (b, c)) ([a] ~> m ([b], [c])) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing MapAndUnzipMSym0

SMonad m => SingI ((>=>@#@$) :: TyFun (a ~> m b) ((b ~> m c) ~> (a ~> m c)) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (>=>@#@$)

(SFoldable t, SMonad m) => SingI (MapM_Sym0 :: TyFun (a ~> m b) (t a ~> m ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MapM_Sym0

(STraversable t, SMonad m) => SingI (MapMSym0 :: TyFun (a ~> m b) (t a ~> m (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing MapMSym0

(SMonad m, SingI d) => SingI ((>>=@#@$$) d :: TyFun (a ~> m b) (m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((>>=@#@$$) d)

SMonad m => SingI (LiftM2Sym0 :: TyFun (a1 ~> (a2 ~> r)) (m a1 ~> (m a2 ~> m r)) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM2Sym0

(SFoldable t, SMonad m) => SingI (FoldM_Sym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m ())) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing FoldM_Sym0

(SFoldable t, SMonad m) => SingI (FoldMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing FoldMSym0

(SFoldable t, SMonad m) => SingI (FoldlMSym0 :: TyFun (b ~> (a ~> m b)) (b ~> (t a ~> m b)) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing FoldlMSym0

SingI d => SingI (Either_Sym1 d :: TyFun (b ~> c) (Either a b ~> c) -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing (Either_Sym1 d)

SMonad m => SingI ((<=<@#@$) :: TyFun (b ~> m c) ((a ~> m b) ~> (a ~> m c)) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (<=<@#@$)

(SingI d1, SingI d2) => SingI (Maybe_Sym2 d1 d2 :: TyFun (Maybe a) b -> Type)

Defined in Data.Maybe.Singletons

Methods

sing :: Sing (Maybe_Sym2 d1 d2)

SingI d => SingI (UncurrySym1 d :: TyFun (a, b) c -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing (UncurrySym1 d)

SingI (Unzip4Sym0 :: TyFun [(a, b, c, d)] ([a], [b], [c], [d]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip4Sym0

SingI d => SingI (ZipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWithSym1 d)

SingI d => SingI (ListzipWithSym1 d :: TyFun [a] ([b] ~> [c]) -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym1 d)

(SingI d1, SingI d2) => SingI (ScanlSym2 d1 d2 :: TyFun [a] [b] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ScanrSym2 d1 d2 :: TyFun [a] [b] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ScanrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListscanlSym2 d1 d2 :: TyFun [a] [b] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListscanrSym2 d1 d2 :: TyFun [a] [b] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListscanrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun [a] b -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Foldl'Sym2 d1 d2)

(SingI d1, SingI d2) => SingI (Listfoldl'Sym2 d1 d2 :: TyFun [a] b -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (Listfoldl'Sym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListfoldlSym2 d1 d2 :: TyFun [a] b -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListfoldrSym2 d1 d2 :: TyFun [a] b -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListfoldrSym2 d1 d2)

(SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun [a] b -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (FoldlSym2 d1 d2)

(SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun [a] b -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FoldrSym2 d1 d2)

SingI d => SingI (Zip3Sym1 d :: TyFun [b] ([c] ~> [(a, b, c)]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Zip3Sym1 d)

SingI (Tuple4Sym0 :: TyFun a (b ~> (c ~> (d ~> (a, b, c, d)))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple4Sym0

SingI d => SingI (CurrySym1 d :: TyFun a (b ~> c) -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing (CurrySym1 d)

SingI d => SingI (MapAccumLSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumLSym1 d)

SingI d => SingI (MapAccumRSym1 d :: TyFun acc ([x] ~> (acc, [y])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumRSym1 d)

(SOrd a, SingI d1, SingI d2) => SingI (ComparingSym2 d1 d2 :: TyFun b Ordering -> Type)

Defined in Data.Ord.Singletons

Methods

sing :: Sing (ComparingSym2 d1 d2)

SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FlipSym1 d)

SingI d => SingI (Tuple3Sym1 d :: TyFun b (c ~> (a, b, c)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple3Sym1 d)

(SFoldable t, SingI d) => SingI (Foldl'Sym1 d :: TyFun b (t a ~> b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldl'Sym1 d)

(SFoldable t, SingI d) => SingI (FoldlSym1 d :: TyFun b (t a ~> b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlSym1 d)

(SFoldable t, SingI d) => SingI (Foldr'Sym1 d :: TyFun b (t a ~> b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldr'Sym1 d)

(SFoldable t, SingI d) => SingI (FoldrSym1 d :: TyFun b (t a ~> b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrSym1 d)

(SFunctor f, SingI d) => SingI (($>@#@$$) d :: TyFun b (f b) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing (($>@#@$$) d)

(SApplicative f, SingI d) => SingI ((<**>@#@$$) d :: TyFun (f (a ~> b)) (f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((<**>@#@$$) d)

SApplicative f => SingI ((<*@#@$) :: TyFun (f a) (f b ~> f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (<*@#@$)

SApplicative f => SingI ((*>@#@$) :: TyFun (f a) (f b ~> f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (*>@#@$)

(SAlternative f, SingI d) => SingI ((<|>@#@$$) d :: TyFun (f a) (f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((<|>@#@$$) d)

(SApplicative f, SingI d) => SingI ((<*>@#@$$) d :: TyFun (f a) (f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((<*>@#@$$) d)

(SFunctor f, SingI d) => SingI (FmapSym1 d :: TyFun (f a) (f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (FmapSym1 d)

(SApplicative f, SingI d) => SingI (LiftASym1 d :: TyFun (f a) (f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftASym1 d)

(SFunctor f, SingI d) => SingI ((<$>@#@$$) d :: TyFun (f a) (f b) -> Type)

Defined in Data.Functor.Singletons

Methods

sing :: Sing ((<$>@#@$$) d)

(SFunctor f, SingI d) => SingI ((<$@#@$$) d :: TyFun (f b) (f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((<$@#@$$) d)

(forall (a :: k1) (b :: k2). (SingI a, SingI b) => SingI (f a b), (ApplyTyCon :: (k2 -> kr) -> k2 ~> kr) ~ (ApplyTyConAux1 :: (k2 -> kr) -> TyFun k2 kr -> Type)) => SingI (TyCon2 f :: k1 ~> (k2 ~> kr))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon2 f)

SMonad m => SingI ((>>@#@$) :: TyFun (m a) (m b ~> m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (>>@#@$)

(SMonadPlus m, SingI d) => SingI (MplusSym1 d :: TyFun (m a) (m a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (MplusSym1 d)

(SMonad m, SingI d) => SingI ((<$!>@#@$$) d :: TyFun (m a) (m b) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ((<$!>@#@$$) d)

(SMonad m, SingI d) => SingI ((=<<@#@$$) d :: TyFun (m a) (m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((=<<@#@$$) d)

(SMonad m, SingI d) => SingI (ApSym1 d :: TyFun (m a) (m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (ApSym1 d)

(SMonad m, SingI d) => SingI (LiftMSym1 d :: TyFun (m a1) (m r) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftMSym1 d)

(SFoldable t, SApplicative f) => SingI (For_Sym0 :: TyFun (t a) ((a ~> f b) ~> f ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing For_Sym0

(STraversable t, SApplicative f) => SingI (ForSym0 :: TyFun (t a) ((a ~> f b) ~> f (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing ForSym0

(SFoldable t, SMonad m) => SingI (ForM_Sym0 :: TyFun (t a) ((a ~> m b) ~> m ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing ForM_Sym0

(STraversable t, SMonad m) => SingI (ForMSym0 :: TyFun (t a) ((a ~> m b) ~> m (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing ForMSym0

(SFoldable t, SingI d) => SingI (ConcatMapSym1 d :: TyFun (t a) [b] -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (ConcatMapSym1 d)

(SFoldable t, SMonoid m, SingI d) => SingI (FoldMapSym1 d :: TyFun (t a) m -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldMapSym1 d)

(STraversable t, SMonoid m, SingI d) => SingI (FoldMapDefaultSym1 d :: TyFun (t a) m -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (FoldMapDefaultSym1 d)

(STraversable t, SingI d) => SingI (FmapDefaultSym1 d :: TyFun (t a) (t b) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (FmapDefaultSym1 d)

(SFoldable t, SAlternative f) => SingI (AsumSym0 :: TyFun (t (f a)) (f a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing AsumSym0

(SFoldable t, SMonadPlus m) => SingI (MsumSym0 :: TyFun (t (m a)) (m a) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing MsumSym0

(SingI d1, SingI d2) => SingI (Either_Sym2 d1 d2 :: TyFun (Either a b) c -> Type)

Defined in Data.Either.Singletons

Methods

sing :: Sing (Either_Sym2 d1 d2)

SApplicative f => SingI (LiftA3Sym0 :: TyFun (a ~> (b ~> (c ~> d))) (f a ~> (f b ~> (f c ~> f d))) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftA3Sym0

(SFoldable t, SApplicative f, SingI d) => SingI (For_Sym1 d :: TyFun (a ~> f b) (f ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (For_Sym1 d)

(STraversable t, SApplicative f, SingI d) => SingI (ForSym1 d :: TyFun (a ~> f b) (f (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (ForSym1 d)

(SMonad m, SingI d) => SingI ((<=<@#@$$) d :: TyFun (a ~> m b) (a ~> m c) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ((<=<@#@$$) d)

(SFoldable t, SMonad m, SingI d) => SingI (ForM_Sym1 d :: TyFun (a ~> m b) (m ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (ForM_Sym1 d)

(STraversable t, SMonad m, SingI d) => SingI (ForMSym1 d :: TyFun (a ~> m b) (m (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (ForMSym1 d)

SMonad m => SingI (LiftM3Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> r))) (m a1 ~> (m a2 ~> (m a3 ~> m r))) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM3Sym0

(SMonad m, SingI d) => SingI ((>=>@#@$$) d :: TyFun (b ~> m c) (a ~> m c) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing ((>=>@#@$$) d)

SingI (Unzip5Sym0 :: TyFun [(a, b, c, d, e)] ([a], [b], [c], [d], [e]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip5Sym0

SingI d2 => SingI (ZipWith3Sym1 d2 :: TyFun [a] ([b] ~> ([c] ~> [d1])) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWith3Sym1 d2)

(SApplicative m, SingI d) => SingI (ZipWithM_Sym1 d :: TyFun [a] ([b] ~> m ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithM_Sym1 d)

(SApplicative m, SingI d) => SingI (ZipWithMSym1 d :: TyFun [a] ([b] ~> m [c]) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithMSym1 d)

(SApplicative m, SingI d) => SingI (MapAndUnzipMSym1 d :: TyFun [a] (m ([b], [c])) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (MapAndUnzipMSym1 d)

(SingI d1, SingI d2) => SingI (ZipWithSym2 d1 d2 :: TyFun [b] [c] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWithSym2 d1 d2)

(SingI d1, SingI d2) => SingI (ListzipWithSym2 d1 d2 :: TyFun [b] [c] -> Type)

Defined in Data.List.Singletons.Internal.Disambiguation

Methods

sing :: Sing (ListzipWithSym2 d1 d2)

(SingI d1, SingI d2) => SingI (Zip3Sym2 d1 d2 :: TyFun [c] [(a, b, c)] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (Zip3Sym2 d1 d2)

(SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumLSym2 d1 d2)

(SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun [x] (acc, [y]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (MapAccumRSym2 d1 d2)

SingI (Tuple5Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (a, b, c, d, e))))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple5Sym0

(STraversable t, SingI d) => SingI (MapAccumLSym1 d :: TyFun a (t b ~> (a, t c)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumLSym1 d)

(STraversable t, SingI d) => SingI (MapAccumRSym1 d :: TyFun a (t b ~> (a, t c)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumRSym1 d)

(SingI d1, SingI d2) => SingI (d1 .@#@$$$ d2 :: TyFun a c -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (d1 .@#@$$$ d2)

(SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type)

Defined in GHC.Base.Singletons

Methods

sing :: Sing (FlipSym2 d1 d2)

SingI d1 => SingI (Tuple4Sym1 d1 :: TyFun b (c ~> (d2 ~> (a, b, c, d2))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple4Sym1 d1)

(SFoldable t, SMonad m, SingI d) => SingI (FoldM_Sym1 d :: TyFun b (t a ~> m ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldM_Sym1 d)

(SFoldable t, SMonad m, SingI d) => SingI (FoldMSym1 d :: TyFun b (t a ~> m b) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldMSym1 d)

(SFoldable t, SMonad m, SingI d) => SingI (FoldlMSym1 d :: TyFun b (t a ~> m b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlMSym1 d)

(SFoldable t, SMonad m, SingI d) => SingI (FoldrMSym1 d :: TyFun b (t a ~> m b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrMSym1 d)

(SingI d1, SingI d2) => SingI (CurrySym2 d1 d2 :: TyFun b c -> Type)

Defined in Data.Tuple.Singletons

Methods

sing :: Sing (CurrySym2 d1 d2)

(SingI d1, SingI d2) => SingI (Tuple3Sym2 d1 d2 :: TyFun c (a, b, c) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple3Sym2 d1 d2)

(SApplicative f, SingI d) => SingI (LiftA2Sym1 d :: TyFun (f a) (f b ~> f c) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA2Sym1 d)

(SApplicative f, SingI d) => SingI ((<*@#@$$) d :: TyFun (f b) (f a) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((<*@#@$$) d)

(SApplicative f, SingI d) => SingI ((*>@#@$$) d :: TyFun (f b) (f b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((*>@#@$$) d)

(forall (a :: k1) (b :: k2) (c :: k3). (SingI a, SingI b, SingI c) => SingI (f a b c), (ApplyTyCon :: (k3 -> kr) -> k3 ~> kr) ~ (ApplyTyConAux1 :: (k3 -> kr) -> TyFun k3 kr -> Type)) => SingI (TyCon3 f :: k1 ~> (k2 ~> (k3 ~> kr)))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon3 f)

(SMonad m, SingI d) => SingI (LiftM2Sym1 d :: TyFun (m a1) (m a2 ~> m r) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM2Sym1 d)

(SMonad m, SingI d) => SingI ((>>@#@$$) d :: TyFun (m b) (m b) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing ((>>@#@$$) d)

(SFoldable t, SingI d1, SingI d2) => SingI (Foldl'Sym2 d1 d2 :: TyFun (t a) b -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldl'Sym2 d1 d2)

(SFoldable t, SingI d1, SingI d2) => SingI (FoldlSym2 d1 d2 :: TyFun (t a) b -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlSym2 d1 d2)

(SFoldable t, SingI d1, SingI d2) => SingI (Foldr'Sym2 d1 d2 :: TyFun (t a) b -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Foldr'Sym2 d1 d2)

(SFoldable t, SingI d1, SingI d2) => SingI (FoldrSym2 d1 d2 :: TyFun (t a) b -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrSym2 d1 d2)

(SFoldable t, SApplicative f, SingI d) => SingI (Traverse_Sym1 d :: TyFun (t a) (f ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (Traverse_Sym1 d)

(STraversable t, SApplicative f, SingI d) => SingI (TraverseSym1 d :: TyFun (t a) (f (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (TraverseSym1 d)

(SFoldable t, SMonad m, SingI d) => SingI (MapM_Sym1 d :: TyFun (t a) (m ()) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (MapM_Sym1 d)

(STraversable t, SMonad m, SingI d) => SingI (MapMSym1 d :: TyFun (t a) (m (t b)) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapMSym1 d)

SMonad m => SingI (LiftM4Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> r)))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> m r)))) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM4Sym0

SingI (Unzip6Sym0 :: TyFun [(a, b, c, d, e, f)] ([a], [b], [c], [d], [e], [f]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip6Sym0

(SingI d2, SingI d3) => SingI (ZipWith3Sym2 d2 d3 :: TyFun [b] ([c] ~> [d1]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWith3Sym2 d2 d3)

(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithM_Sym2 d1 d2 :: TyFun [b] (m ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithM_Sym2 d1 d2)

(SApplicative m, SingI d1, SingI d2) => SingI (ZipWithMSym2 d1 d2 :: TyFun [b] (m [c]) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (ZipWithMSym2 d1 d2)

SingI (Tuple6Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (a, b, c, d, e, f)))))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple6Sym0

(SMonad m, SingI d1, SingI d2) => SingI (d1 <=<@#@$$$ d2 :: TyFun a (m c) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (d1 <=<@#@$$$ d2)

(SMonad m, SingI d1, SingI d2) => SingI (d1 >=>@#@$$$ d2 :: TyFun a (m c) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (d1 >=>@#@$$$ d2)

SingI d1 => SingI (Tuple5Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (a, b, c, d2, e)))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym1 d1)

(SingI d1, SingI d2) => SingI (Tuple4Sym2 d1 d2 :: TyFun c (d3 ~> (a, b, c, d3)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple4Sym2 d1 d2)

(SApplicative f, SingI d2) => SingI (LiftA3Sym1 d2 :: TyFun (f a) (f b ~> (f c ~> f d1)) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA3Sym1 d2)

(SApplicative f, SingI d1, SingI d2) => SingI (LiftA2Sym2 d1 d2 :: TyFun (f b) (f c) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA2Sym2 d1 d2)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4). (SingI a, SingI b, SingI c, SingI d) => SingI (f a b c d), (ApplyTyCon :: (k4 -> kr) -> k4 ~> kr) ~ (ApplyTyConAux1 :: (k4 -> kr) -> TyFun k4 kr -> Type)) => SingI (TyCon4 f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> kr))))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon4 f)

(SMonad m, SingI d) => SingI (LiftM3Sym1 d :: TyFun (m a1) (m a2 ~> (m a3 ~> m r)) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM3Sym1 d)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM2Sym2 d1 d2 :: TyFun (m a2) (m r) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM2Sym2 d1 d2)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldM_Sym2 d1 d2 :: TyFun (t a) (m ()) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldM_Sym2 d1 d2)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldMSym2 d1 d2 :: TyFun (t a) (m b) -> Type)

Defined in Control.Monad.Singletons

Methods

sing :: Sing (FoldMSym2 d1 d2)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldlMSym2 d1 d2 :: TyFun (t a) (m b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldlMSym2 d1 d2)

(SFoldable t, SMonad m, SingI d1, SingI d2) => SingI (FoldrMSym2 d1 d2 :: TyFun (t a) (m b) -> Type)

Defined in Data.Foldable.Singletons

Methods

sing :: Sing (FoldrMSym2 d1 d2)

(STraversable t, SingI d1, SingI d2) => SingI (MapAccumLSym2 d1 d2 :: TyFun (t b) (a, t c) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumLSym2 d1 d2)

(STraversable t, SingI d1, SingI d2) => SingI (MapAccumRSym2 d1 d2 :: TyFun (t b) (a, t c) -> Type)

Defined in Data.Traversable.Singletons

Methods

sing :: Sing (MapAccumRSym2 d1 d2)

SMonad m => SingI (LiftM5Sym0 :: TyFun (a1 ~> (a2 ~> (a3 ~> (a4 ~> (a5 ~> r))))) (m a1 ~> (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r))))) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing LiftM5Sym0

SingI (Unzip7Sym0 :: TyFun [(a, b, c, d, e, f, g)] ([a], [b], [c], [d], [e], [f], [g]) -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing Unzip7Sym0

(SingI d2, SingI d3, SingI d4) => SingI (ZipWith3Sym3 d2 d3 d4 :: TyFun [c] [d1] -> Type)

Defined in Data.List.Singletons.Internal

Methods

sing :: Sing (ZipWith3Sym3 d2 d3 d4)

SingI (Tuple7Sym0 :: TyFun a (b ~> (c ~> (d ~> (e ~> (f ~> (g ~> (a, b, c, d, e, f, g))))))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing Tuple7Sym0

SingI d1 => SingI (Tuple6Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (a, b, c, d2, e, f))))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym1 d1)

(SingI d1, SingI d2) => SingI (Tuple5Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (a, b, c, d3, e))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym2 d1 d2)

(SingI d1, SingI d2, SingI d3) => SingI (Tuple4Sym3 d1 d2 d3 :: TyFun d4 (a, b, c, d4) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple4Sym3 d1 d2 d3)

(SApplicative f, SingI d2, SingI d3) => SingI (LiftA3Sym2 d2 d3 :: TyFun (f b) (f c ~> f d1) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA3Sym2 d2 d3)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5). (SingI a, SingI b, SingI c, SingI d, SingI e) => SingI (f a b c d e), (ApplyTyCon :: (k5 -> kr) -> k5 ~> kr) ~ (ApplyTyConAux1 :: (k5 -> kr) -> TyFun k5 kr -> Type)) => SingI (TyCon5 f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> kr)))))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon5 f)

(SMonad m, SingI d) => SingI (LiftM4Sym1 d :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> m r))) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym1 d)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM3Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> m r) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM3Sym2 d1 d2)

SingI d1 => SingI (Tuple7Sym1 d1 :: TyFun b (c ~> (d2 ~> (e ~> (f ~> (g ~> (a, b, c, d2, e, f, g)))))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym1 d1)

(SingI d1, SingI d2) => SingI (Tuple6Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (a, b, c, d3, e, f)))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym2 d1 d2)

(SingI d1, SingI d2, SingI d3) => SingI (Tuple5Sym3 d1 d2 d3 :: TyFun d4 (e ~> (a, b, c, d4, e)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym3 d1 d2 d3)

(SApplicative f, SingI d2, SingI d3, SingI d4) => SingI (LiftA3Sym3 d2 d3 d4 :: TyFun (f c) (f d1) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftA3Sym3 d2 d3 d4)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f') => SingI (f a b c d e f'), (ApplyTyCon :: (k6 -> kr) -> k6 ~> kr) ~ (ApplyTyConAux1 :: (k6 -> kr) -> TyFun k6 kr -> Type)) => SingI (TyCon6 f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> kr))))))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon6 f)

(SMonad m, SingI d) => SingI (LiftM5Sym1 d :: TyFun (m a1) (m a2 ~> (m a3 ~> (m a4 ~> (m a5 ~> m r)))) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym1 d)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM4Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> m r)) -> Type)

Defined in Control.Monad.Singletons.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)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM3Sym3 d1 d2 d3)

(SingI d1, SingI d2) => SingI (Tuple7Sym2 d1 d2 :: TyFun c (d3 ~> (e ~> (f ~> (g ~> (a, b, c, d3, e, f, g))))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym2 d1 d2)

(SingI d1, SingI d2, SingI d3) => SingI (Tuple6Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (a, b, c, d4, e, f))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym3 d1 d2 d3)

(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple5Sym4 d1 d2 d3 d5 :: TyFun e (a, b, c, d4, e) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple5Sym4 d1 d2 d3 d5)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g) => SingI (f a b c d e f' g), (ApplyTyCon :: (k7 -> kr) -> k7 ~> kr) ~ (ApplyTyConAux1 :: (k7 -> kr) -> TyFun k7 kr -> Type)) => SingI (TyCon7 f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> kr)))))))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon7 f)

(SMonad m, SingI d1, SingI d2) => SingI (LiftM5Sym2 d1 d2 :: TyFun (m a2) (m a3 ~> (m a4 ~> (m a5 ~> m r))) -> Type)

Defined in Control.Monad.Singletons.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)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym3 d1 d2 d3)

(SingI d1, SingI d2, SingI d3) => SingI (Tuple7Sym3 d1 d2 d3 :: TyFun d4 (e ~> (f ~> (g ~> (a, b, c, d4, e, f, g)))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym3 d1 d2 d3)

(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple6Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (a, b, c, d4, e, f)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym4 d1 d2 d3 d5)

(forall (a :: k1) (b :: k2) (c :: k3) (d :: k4) (e :: k5) (f' :: k6) (g :: k7) (h :: k8). (SingI a, SingI b, SingI c, SingI d, SingI e, SingI f', SingI g, SingI h) => SingI (f a b c d e f' g h), (ApplyTyCon :: (k8 -> kr) -> k8 ~> kr) ~ (ApplyTyConAux1 :: (k8 -> kr) -> TyFun k8 kr -> Type)) => SingI (TyCon8 f :: k1 ~> (k2 ~> (k3 ~> (k4 ~> (k5 ~> (k6 ~> (k7 ~> (k8 ~> kr))))))))

Defined in Data.Singletons

Methods

sing :: Sing (TyCon8 f)

(SMonad m, SingI d1, SingI d2, SingI d3) => SingI (LiftM5Sym3 d1 d2 d3 :: TyFun (m a3) (m a4 ~> (m a5 ~> m r)) -> Type)

Defined in Control.Monad.Singletons.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)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM4Sym4 d1 d2 d3 d4)

(SingI d1, SingI d2, SingI d3, SingI d5) => SingI (Tuple7Sym4 d1 d2 d3 d5 :: TyFun e (f ~> (g ~> (a, b, c, d4, e, f, g))) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym4 d1 d2 d3 d5)

(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple6Sym5 d1 d2 d3 d5 d6 :: TyFun f (a, b, c, d4, e, f) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple6Sym5 d1 d2 d3 d5 d6)

(SMonad m, SingI d1, SingI d2, SingI d3, SingI d4) => SingI (LiftM5Sym4 d1 d2 d3 d4 :: TyFun (m a4) (m a5 ~> m r) -> Type)

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym4 d1 d2 d3 d4)

(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6) => SingI (Tuple7Sym5 d1 d2 d3 d5 d6 :: TyFun f (g ~> (a, b, c, d4, e, f, g)) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym5 d1 d2 d3 d5 d6)

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

Defined in Control.Monad.Singletons.Internal

Methods

sing :: Sing (LiftM5Sym5 d1 d2 d3 d4 d5)

(SingI d1, SingI d2, SingI d3, SingI d5, SingI d6, SingI d7) => SingI (Tuple7Sym6 d1 d2 d3 d5 d6 d7 :: TyFun g (a, b, c, d4, e, f, g) -> Type)

Defined in Data.Singletons.Base.Instances

Methods

sing :: Sing (Tuple7Sym6 d1 d2 d3 d5 d6 d7)