Language.Symantic.Typing.Type

Type Type

data Type src vs t where

Constructors

TyConst :: src -> Len vs -> Const src c -> Type src vs c

TyApp :: src -> Type src vs f -> Type src vs a -> Type src vs (f a)

TyVar :: src -> NameVar -> Var src vs v -> Type src vs v

TyFam :: src -> Len vs -> Const src fam -> Types src vs hs -> Type src vs (Fam fam hs)

Instances

AllocVars k (Type k src)

Methods

allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x

allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x

SourceInj (TypeVT src) src => TestEquality k (Type k src vs)

Methods

testEquality :: f a -> f b -> Maybe ((Type k src vs :~: a) b)

SourceInj (TypeVT src) src => KindOf kt (Type kt src vs)

Methods

kindOf :: a t -> Kind (SourceOf (a t)) (Type kt src vs)

Source src => Eq (Type kt src vs t)

Methods

(==) :: Type kt src vs t -> Type kt src vs t -> Bool

(/=) :: Type kt src vs t -> Type kt src vs t -> Bool

Source src => Sourced (Type kt src vs t)

Methods

sourceOf :: Type kt src vs t -> SourceOf (Type kt src vs t)

setSource :: Type kt src vs t -> SourceOf (Type kt src vs t) -> Type kt src vs t

UsedVarsOf (Type kt src vs t)

Methods

usedVarsOf :: UsedVars (SourceOf (Type kt src vs t)) (VarsOf (Type kt src vs t)) vs -> Type kt src vs t -> (forall vs'. UsedVars (SourceOf (Type kt src vs t)) (VarsOf (Type kt src vs t)) vs' -> ret) -> ret

VarOccursIn (Type kt src vs t)

Methods

varOccursIn :: Var kv src (VarsOf (Type kt src vs t)) v -> Type kt src vs t -> Bool

LenVars (Type kt src vs t)

Methods

lenVars :: Type kt src vs t -> Len Type (VarsOf (Type kt src vs t))

ExpandFam (Type kt src vs t)

Methods

expandFam :: Type kt src vs t -> Type kt src vs t

ConstsOf (Type kt src vs t)

Methods

constsOf :: Type kt src vs t -> Set (ConstC (SourceOf (Type kt src vs t)))

Substable (Type kt src vs t)

Methods

substVarUnsafe :: ((* ~ src) (SourceOf (Type kt src vs t)), ([Type] ~ vs) (VarsOf (Type kt src vs t))) => Var kt src vs v -> Type kt src vs v -> Type kt src vs t -> Type kt src vs t

subst :: ((* ~ src) (SourceOf (Type kt src vs t)), ([Type] ~ vs) (VarsOf (Type kt src vs t))) => Subst src vs -> Type kt src vs t -> Type kt src vs t

type SourceOf (Type kt src vs t)

type SourceOf (Type kt src vs t) = src

type VarsOf (Type kt src vs t)

type VarsOf (Type kt src vs t) = vs

tyConst :: forall kc c src vs. Source src => LenInj vs => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Type src vs c

Like TyConst, but using noSource, lenInj and constInj.

FIXME: remove kc when GHC's #12933 is fixed.

tyConstLen :: forall kc c src vs. Source src => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Len vs -> Type src vs c

Like tyConst, but not using lenInj.

tyApp :: Source src => Type src vs f -> Type src vs a -> Type src vs (f a) infixl 9

Like TyApp, but using noSource.

tyVar :: Source src => NameVar -> Var src vs v -> Type src vs v

Like TyVar, but using noSource.

tyFam :: forall kc c as vs src. Source src => LenInj vs => Constable c => KindInjP (Ty_of_Type kc) => Type_of_Ty (Ty_of_Type kc) ~ kc => Types src vs as -> Type src vs (Fam c as)

Like TyFam, but using noSource.

FIXME: remove kc when GHC's #12933 is fixed.

tyQual :: Source src => Type src vs q -> Type src vs t -> (Qual q -> Type src vs t -> Type src vs (q #> t)) -> Type src vs (q #> t) infix 1

Qualify a Type.

Type TypeK

data TypeK src vs kt

Existential Type of a known Kind.

Constructors

TypeK (Type src vs t)

Instances

Source src => Eq (TypeK src vs ki)

Methods

(==) :: TypeK src vs ki -> TypeK src vs ki -> Bool

(/=) :: TypeK src vs ki -> TypeK src vs ki -> Bool

type SourceOf (TypeK src vs ki)

type SourceOf (TypeK src vs ki) = src

type VarsOf (TypeK src vs ki)

type VarsOf (TypeK src vs ki) = vs

Type TypeT

data TypeT src vs

Existential for Type.

Constructors

TypeT (Type src vs t)

Instances

Source src => Eq (TypeT src vs)

Methods

(==) :: TypeT src vs -> TypeT src vs -> Bool

(/=) :: TypeT src vs -> TypeT src vs -> Bool

type SourceOf (TypeT src vs)

type SourceOf (TypeT src vs) = src

type VarsOf (TypeT src vs)

type VarsOf (TypeT src vs) = vs

Type TypeVT

data TypeVT src

Existential polymorphic Type.

Constructors

TypeVT (Type src vs t)

Instances

Source src => Eq (TypeVT src)

Methods

(==) :: TypeVT src -> TypeVT src -> Bool

(/=) :: TypeVT src -> TypeVT src -> Bool

SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss)

Methods

sourceInj :: TypeVT (SrcTe inp ss) -> SrcTe inp ss

type SourceOf (TypeVT src)

type SourceOf (TypeVT src) = src

Type Const

data Const src c where

Type constant.

Constructors

Const :: Constable c => Kind src kc -> Const src (c :: kc)

Instances

SourceInj (ConstC src) src => KindOf kt (Const kt src)

Methods

kindOf :: a t -> Kind (SourceOf (a t)) (Const kt src)

Eq (Const kc src c)

Methods

(==) :: Const kc src c -> Const kc src c -> Bool

(/=) :: Const kc src c -> Const kc src c -> Bool

Ord (Const kc src c)

Methods

compare :: Const kc src c -> Const kc src c -> Ordering

(<) :: Const kc src c -> Const kc src c -> Bool

(<=) :: Const kc src c -> Const kc src c -> Bool

(>) :: Const kc src c -> Const kc src c -> Bool

(>=) :: Const kc src c -> Const kc src c -> Bool

max :: Const kc src c -> Const kc src c -> Const kc src c

min :: Const kc src c -> Const kc src c -> Const kc src c

ConstsOf (Const kc src c)

Methods

constsOf :: Const kc src c -> Set (ConstC (SourceOf (Const kc src c)))

type SourceOf (Const kc src c)

type SourceOf (Const kc src c) = src

kindOfConst :: Const src (t :: kt) -> Kind src kt

Class Constable

class (Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable c

Instances

(Typeable kc c, FixityOf kc c, NameTyOf kc c, ClassInstancesFor kc c, TypeInstancesFor kc c) => Constable kc c

Class ConstsOf

class ConstsOf a where

Return the Consts used by something.

Minimal complete definition

constsOf

Methods

constsOf :: a -> Set (ConstC (SourceOf a))

Instances

ConstsOf (Types src vs ts)

Methods

constsOf :: Types src vs ts -> Set (ConstC (SourceOf (Types src vs ts)))

ConstsOf (Const kc src c)

Methods

constsOf :: Const kc src c -> Set (ConstC (SourceOf (Const kc src c)))

ConstsOf (Type kt src vs t)

Methods

constsOf :: Type kt src vs t -> Set (ConstC (SourceOf (Type kt src vs t)))

ConstsOf (Term src ss ts vs t)

Methods

constsOf :: Term src ss ts vs t -> Set (ConstC (SourceOf (Term src ss ts vs t)))

Type ConstC

data ConstC src

Constructors

ConstC (Const src c)

Instances

Eq (ConstC src)

Methods

(==) :: ConstC src -> ConstC src -> Bool

(/=) :: ConstC src -> ConstC src -> Bool

Ord (ConstC src)

Methods

compare :: ConstC src -> ConstC src -> Ordering

(<) :: ConstC src -> ConstC src -> Bool

(<=) :: ConstC src -> ConstC src -> Bool

(>) :: ConstC src -> ConstC src -> Bool

(>=) :: ConstC src -> ConstC src -> Bool

max :: ConstC src -> ConstC src -> ConstC src

min :: ConstC src -> ConstC src -> ConstC src

Type '(->)'

(~>) :: Source src => Constable (->) => Type src vs a -> Type src vs b -> Type src vs (a -> b) infixr 0

The function Type (->), with an infix notation more readable.

Type family FunArg

type family FunArg (fun :: Type) :: Type where ...

Equations

FunArg (q #> f) = FunArg f

FunArg (a -> b) = a

Type family FunRes

type family FunRes (fun :: Type) :: Type where ...

Equations

FunRes (q #> f) = FunRes f

FunRes (a -> b) = b

unTyFun :: forall t src tys. SourceInj (TypeVT src) src => Constable (->) => Type src tys t -> Maybe (Type src tys (FunArg t), Type src tys (FunRes t))

Return, when the given Type is a function, the argument of that function.

Type (#>)

newtype q #> a infixr 0

Type constant to qualify a Type.

Constructors

Qual (q => a)

Instances

FixityOf (Constraint -> Type -> *) (#>)

Methods

fixityOf :: proxy c -> Maybe Fixity

NameTyOf (Constraint -> Type -> *) (#>)

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

TypeInstancesFor (Constraint -> Type -> *) (#>)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

ClassInstancesFor (Constraint -> Type -> *) (#>)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

(#>) :: Source src => Type src vs q -> Type src vs t -> Type src vs (q #> t) infixr 0

Qualify a Type.

Class (#)

class (x, y) => x # y infixr 2

Constraint union.

Instances

(x, y) => x # y

FixityOf (Constraint -> Constraint -> Constraint) (#)

Methods

fixityOf :: proxy c -> Maybe Fixity

NameTyOf (Constraint -> Constraint -> Constraint) (#)

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

TypeInstancesFor (Constraint -> Constraint -> Constraint) (#)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

ClassInstancesFor (Constraint -> Constraint -> Constraint) (#)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

(#) :: Source src => Type src vs qx -> Type src vs qy -> Type src vs (qx # qy) infixr 2

Unify two Constraints.

Type (() :: Constraint)

noConstraint :: Source src => LenInj vs => Type src vs (() :: Constraint)

Like noConstraintLen, but using lenInj.

noConstraintLen :: Source src => Len vs -> Type src vs (() :: Constraint)

Empty Constraint.

Class (#~)

class x ~ y => x #~ y infixr 2

Type equality Constraint.

Instances

(~) k x y => (#~) k x y

FixityOf (k -> k -> Constraint) ((#~) k)

Methods

fixityOf :: proxy c -> Maybe Fixity

NameTyOf (k -> k -> Constraint) ((#~) k)

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

TypeInstancesFor (k -> k -> Constraint) ((#~) k)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

(KindInj k2, Typeable Type k2) => ClassInstancesFor (k2 -> k2 -> Constraint) ((#~) k2)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

(#~) :: forall k a b src vs. Source src => Typeable k => KindInj k => Type src vs (a :: k) -> Type src vs (b :: k) -> Type src vs (a #~ b) infixr 2

Constraint two Types to be equal.

eqType :: Source src => Type src tys (x :: k) -> Type src tys (y :: k) -> Maybe (x :~: y)

Type equality.

eqTypeKi :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Maybe (x :~~: y)

Heterogeneous type equality: return two proofs when two Types are equals: one for the type and one for the kind.

eqTypes :: Source src => Types src tys x -> Types src tys y -> Maybe (x :~~: y)

Comparison

ordType :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Ordering

Compare two Types.

ordTypes :: Source src => Types src tys x -> Types src tys y -> Ordering

Type Qual

data Qual q where

Captures the proof of a Constraint (and its dictionaries when it contains type classes): pattern matching on the Dict constructor brings the Constraint into scope.

Constructors

Dict :: q => Qual q

Class ClassInstancesFor

class ClassInstancesFor c where

Methods

proveConstraintFor :: Source src => proxy c -> Type src vs q -> Maybe (Qual q)

Instances

ClassInstancesFor Constraint ()

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

ClassInstancesFor (Constraint -> Type -> *) (#>)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

ClassInstancesFor (Constraint -> Constraint -> Constraint) (#)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

(KindInj k2, Typeable Type k2) => ClassInstancesFor (k2 -> k2 -> Constraint) ((#~) k2)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)

Injection

constInj :: forall c src. Source src => Constable c => KindInjP (Ty_of_Type (K c)) => Type_of_Ty (Ty_of_Type (K c)) ~ K c => Const src c

constKiInj :: forall kc c src. Source src => Constable c => Kind src kc -> Const src (c :: kc)

Projection

proj_Const :: forall c u src. Typeable c => Const src u -> Maybe (c :~: u)

Like proj_ConstKi, but with kind equality already known.

proj_ConstTy :: forall c u src vs. Typeable c => Type src vs u -> Maybe (c :~: u)

Like proj_Const, but on a Type.

proj_ConstKi :: forall kc c u src. Typeable c => kc ~ Type_of_Ty (Ty_of_Type kc) => KindInjP (Ty_of_Type kc) => Const src u -> Maybe (c :~~: u)

XXX: proj_ConstKi must be given the kc kind explicitely, when used multiple times in the same pattern match, because of GHC's #12933.

proj_ConstKiTy :: forall kc c u src vs. Typeable c => kc ~ Type_of_Ty (Ty_of_Type kc) => KindInjP (Ty_of_Type kc) => Type src vs u -> Maybe (c :~~: u)

Like proj_ConstKi, but on a Type.

eqConst :: Const src_x (x :: k) -> Const src_y (y :: k) -> Maybe (x :~: y)

eqConstKi :: forall src_x src_y kx ky x y. Const src_x (x :: kx) -> Const src_y (y :: ky) -> Maybe (x :~~: y)

ordConst :: forall src_x src_y kx ky x y. Const src_x (x :: kx) -> Const src_y (y :: ky) -> Ordering

normalizeQualsTy :: Source src => Type src tys (t :: kt) -> TypeK src tys kt

Type family Fam

type family Fam (fam :: k) (hs :: [Type]) :: k

Apply the type family selected by fam to a list of types (within a Proxy).

| NOTE: |Fam|'s Kind MUST be the same than fam's.

Class TypeInstancesFor

class TypeInstancesFor c where

Methods

expandFamFor :: Source src => proxy c -> Len vs -> Const src fam -> Types src vs ts -> Maybe (Type src vs (Fam fam ts))

Instances

TypeInstancesFor Constraint ()

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

TypeInstancesFor (Constraint -> Type -> *) (#>)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

TypeInstancesFor (Constraint -> Constraint -> Constraint) (#)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

TypeInstancesFor (k -> k -> Constraint) ((#~) k)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

Class ExpandFam

class ExpandFam a where

Minimal complete definition

expandFam

Methods

expandFam :: Source (SourceOf a) => a -> a

Instances

ExpandFam (Type kt src vs t)

Methods

expandFam :: Type kt src vs t -> Type kt src vs t

ExpandFam (Term src ss ts vs t)

Methods

expandFam :: Term src ss ts vs t -> Term src ss ts vs t

kindOfType :: Type src vs (t :: kt) -> Kind src kt

Like kindOf but keep the old Source.

normalizeVarsTy :: Type src vs (t :: kt) -> (forall vs'. Type src vs' (t :: kt) -> ret) -> ret

Remove unused Vars from ther context.

Type Types

data Types src vs ts where

Constructors

TypesZ :: Types src vs '[]

TypesS :: Type src vs t -> Types src vs ts -> Types src vs (Proxy t ': ts) infixr 5

Instances

UsedVarsOf (Types src vs ts)

Methods

usedVarsOf :: UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs -> Types src vs ts -> (forall vs'. UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs' -> ret) -> ret

VarOccursIn (Types src vs ts)

Methods

varOccursIn :: Var kv src (VarsOf (Types src vs ts)) v -> Types src vs ts -> Bool

ConstsOf (Types src vs ts)

Methods

constsOf :: Types src vs ts -> Set (ConstC (SourceOf (Types src vs ts)))

Substable (Types src vs ts)

Methods

substVarUnsafe :: ((* ~ src) (SourceOf (Types src vs ts)), ([Type] ~ vs) (VarsOf (Types src vs ts))) => Var kt src vs v -> Type kt src vs v -> Types src vs ts -> Types src vs ts

subst :: ((* ~ src) (SourceOf (Types src vs ts)), ([Type] ~ vs) (VarsOf (Types src vs ts))) => Subst src vs -> Types src vs ts -> Types src vs ts

type SourceOf (Types src vs ts)

type SourceOf (Types src vs ts) = src

type VarsOf (Types src vs ts)

type VarsOf (Types src vs ts) = vs

mapTys :: (forall kt t. Type src vs t -> Type src vs' t) -> Types src vs ts -> Types src vs' ts

foldlTys :: (forall k t. Type src vs t -> acc -> acc) -> Types src vs ts -> acc -> acc

Class TypeOf

class TypeOf a where

Minimal complete definition

typeOf

Methods

typeOf :: a t -> Type (SourceOf (a t)) (VarsOf (a t)) t

Instances

SourceInj (TermT src ss ts vs) src => TypeOf Type (Term src ss ts vs)

Methods

typeOf :: a t -> Type (Term src ss ts vs) (SourceOf (a t)) (VarsOf (a t)) t

data Proxy k t :: forall k. k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

(ModuleFor k src ss s, ModulesInjR src ss rs) => ModulesInjR src ss ((:) * (Proxy k s) rs)

Methods

modulesInjR :: Either Error_Module (Modules src ss)

(Gram_Term_AtomsFor k src ss g t, Gram_Term_AtomsR src ss rs g) => Gram_Term_AtomsR src ss ((:) * (Proxy k t) rs) g

Methods

g_term_atomsR :: [CF g (AST_Term src ss)]

SymInjP k * Zero ((:) * (Proxy k s) ss) s

Methods

symInjP :: TeSym ((* ': Proxy Zero s) [*]) ts t -> TeSym ss ts t

SymInjP k1 * p ss s => SymInjP k1 * (Succ p) ((:) * (Proxy k not_s) ss) s

Methods

symInjP :: TeSym ((* ': Proxy (Succ p) s) [*]) ts t -> TeSym ss ts t

Monad (Proxy *)

Methods

(>>=) :: Proxy * a -> (a -> Proxy * b) -> Proxy * b

(>>) :: Proxy * a -> Proxy * b -> Proxy * b

return :: a -> Proxy * a

fail :: String -> Proxy * a

Functor (Proxy *)

Methods

fmap :: (a -> b) -> Proxy * a -> Proxy * b

(<$) :: a -> Proxy * b -> Proxy * a

Applicative (Proxy *)

Methods

pure :: a -> Proxy * a

(<*>) :: Proxy * (a -> b) -> Proxy * a -> Proxy * b

(*>) :: Proxy * a -> Proxy * b -> Proxy * b

(<*) :: Proxy * a -> Proxy * b -> Proxy * a

Foldable (Proxy *)

Methods

fold :: Monoid m => Proxy * m -> m

foldMap :: Monoid m => (a -> m) -> Proxy * a -> m

foldr :: (a -> b -> b) -> b -> Proxy * a -> b

foldr' :: (a -> b -> b) -> b -> Proxy * a -> b

foldl :: (b -> a -> b) -> b -> Proxy * a -> b

foldl' :: (b -> a -> b) -> b -> Proxy * a -> b

foldr1 :: (a -> a -> a) -> Proxy * a -> a

foldl1 :: (a -> a -> a) -> Proxy * a -> a

toList :: Proxy * a -> [a]

null :: Proxy * a -> Bool

length :: Proxy * a -> Int

elem :: Eq a => a -> Proxy * a -> Bool

maximum :: Ord a => Proxy * a -> a

minimum :: Ord a => Proxy * a -> a

sum :: Num a => Proxy * a -> a

product :: Num a => Proxy * a -> a

Traversable (Proxy *)

Methods

traverse :: Applicative f => (a -> f b) -> Proxy * a -> f (Proxy * b)

sequenceA :: Applicative f => Proxy * (f a) -> f (Proxy * a)

mapM :: Monad m => (a -> m b) -> Proxy * a -> m (Proxy * b)

sequence :: Monad m => Proxy * (m a) -> m (Proxy * a)

Generic1 (Proxy *)

Associated Types

type Rep1 (Proxy * :: * -> *) :: * -> *

Methods

from1 :: Proxy * a -> Rep1 (Proxy *) a

to1 :: Rep1 (Proxy *) a -> Proxy * a

Alternative (Proxy *)

Methods

empty :: Proxy * a

(<|>) :: Proxy * a -> Proxy * a -> Proxy * a

some :: Proxy * a -> Proxy * [a]

many :: Proxy * a -> Proxy * [a]

MonadPlus (Proxy *)

Methods

mzero :: Proxy * a

mplus :: Proxy * a -> Proxy * a -> Proxy * a

(NameTyOf k t, FixityOf k t, ImportTypes [*] ts) => ImportTypes [*] ((:) * (Proxy k t) ts)

Methods

importTypes :: PathMod -> Imports NameTy

(KindInjP (Ty_of_Type (K k c)), (~) * (K k c) (Type_of_Ty (Ty_of_Type (K k c))), Constable k c, ModulesTyInj [*] ts) => ModulesTyInj [*] ((:) * (Proxy k c) ts)

Methods

modulesTyInj :: Source src => ModulesTy src

Bounded (Proxy k s)

Methods

minBound :: Proxy k s

maxBound :: Proxy k s

Enum (Proxy k s)

Methods

succ :: Proxy k s -> Proxy k s

pred :: Proxy k s -> Proxy k s

toEnum :: Int -> Proxy k s

fromEnum :: Proxy k s -> Int

enumFrom :: Proxy k s -> [Proxy k s]

enumFromThen :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromTo :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromThenTo :: Proxy k s -> Proxy k s -> Proxy k s -> [Proxy k s]

Eq (Proxy k s)

Methods

(==) :: Proxy k s -> Proxy k s -> Bool

(/=) :: Proxy k s -> Proxy k s -> Bool

Ord (Proxy k s)

Methods

compare :: Proxy k s -> Proxy k s -> Ordering

(<) :: Proxy k s -> Proxy k s -> Bool

(<=) :: Proxy k s -> Proxy k s -> Bool

(>) :: Proxy k s -> Proxy k s -> Bool

(>=) :: Proxy k s -> Proxy k s -> Bool

max :: Proxy k s -> Proxy k s -> Proxy k s

min :: Proxy k s -> Proxy k s -> Proxy k s

Read (Proxy k s)

Methods

readsPrec :: Int -> ReadS (Proxy k s)

readList :: ReadS [Proxy k s]

readPrec :: ReadPrec (Proxy k s)

readListPrec :: ReadPrec [Proxy k s]

Show (Proxy k s)

Methods

showsPrec :: Int -> Proxy k s -> ShowS

show :: Proxy k s -> String

showList :: [Proxy k s] -> ShowS

Ix (Proxy k s)

Methods

range :: (Proxy k s, Proxy k s) -> [Proxy k s]

index :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

unsafeIndex :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

inRange :: (Proxy k s, Proxy k s) -> Proxy k s -> Bool

rangeSize :: (Proxy k s, Proxy k s) -> Int

unsafeRangeSize :: (Proxy k s, Proxy k s) -> Int

Generic (Proxy k t)

Associated Types

type Rep (Proxy k t) :: * -> *

Methods

from :: Proxy k t -> Rep (Proxy k t) x

to :: Rep (Proxy k t) x -> Proxy k t

Semigroup (Proxy k s)

Methods

(<>) :: Proxy k s -> Proxy k s -> Proxy k s

sconcat :: NonEmpty (Proxy k s) -> Proxy k s

stimes :: Integral b => b -> Proxy k s -> Proxy k s

Monoid (Proxy k s)

Methods

mempty :: Proxy k s

mappend :: Proxy k s -> Proxy k s -> Proxy k s

mconcat :: [Proxy k s] -> Proxy k s

type Rep1 (Proxy *)

type Rep1 (Proxy *) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

type Rep (Proxy k t)

type Rep (Proxy k t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

data (k :~: a) b :: forall k. k -> k -> * where infix 4

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: 4.7.0.0

Constructors

Refl :: (:~:) k a a

Instances

TestEquality k ((:~:) k a)

Methods

testEquality :: f a -> f b -> Maybe (((k :~: a) :~: a) b)

(~) k a b => Bounded ((:~:) k a b)

Methods

minBound :: (k :~: a) b

maxBound :: (k :~: a) b

(~) k a b => Enum ((:~:) k a b)

Methods

succ :: (k :~: a) b -> (k :~: a) b

pred :: (k :~: a) b -> (k :~: a) b

toEnum :: Int -> (k :~: a) b

fromEnum :: (k :~: a) b -> Int

enumFrom :: (k :~: a) b -> [(k :~: a) b]

enumFromThen :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b]

enumFromTo :: (k :~: a) b -> (k :~: a) b -> [(k :~: a) b]

enumFromThenTo :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b -> [(k :~: a) b]

Eq ((:~:) k a b)

Methods

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

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

Ord ((:~:) k a b)

Methods

compare :: (k :~: a) b -> (k :~: a) b -> Ordering

(<) :: (k :~: a) b -> (k :~: a) b -> Bool

(<=) :: (k :~: a) b -> (k :~: a) b -> Bool

(>) :: (k :~: a) b -> (k :~: a) b -> Bool

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

max :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b

min :: (k :~: a) b -> (k :~: a) b -> (k :~: a) b

(~) k a b => Read ((:~:) k a b)

Methods

readsPrec :: Int -> ReadS ((k :~: a) b)

readList :: ReadS [(k :~: a) b]

readPrec :: ReadPrec ((k :~: a) b)

readListPrec :: ReadPrec [(k :~: a) b]

Show ((:~:) k a b)

Methods

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

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

showList :: [(k :~: a) b] -> ShowS

data a :~~: b where

Heterogeneous propositional equality: like (:~:) but prove also that the kinds are equal.

Constructors

HRefl :: a :~~: a

data Constraint :: *

The kind of constraints, like Show a

Instances

KindInjP Constraint

Methods

kindInjP :: src -> Kind src (Type_of_Ty Constraint)

FixityOf Constraint c

Methods

fixityOf :: proxy c -> Maybe Fixity

TypeInstancesFor Constraint ()

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

ClassInstancesFor Constraint ()

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

FixityOf (Constraint -> Type -> *) (#>)

Methods

fixityOf :: proxy c -> Maybe Fixity

FixityOf (Constraint -> Constraint -> Constraint) (#)

Methods

fixityOf :: proxy c -> Maybe Fixity

NameTyOf (Constraint -> Type -> *) (#>)

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

NameTyOf (Constraint -> Constraint -> Constraint) (#)

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

TypeInstancesFor (Constraint -> Type -> *) (#>)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

TypeInstancesFor (Constraint -> Constraint -> Constraint) (#)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

ClassInstancesFor (Constraint -> Type -> *) (#>)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

ClassInstancesFor (Constraint -> Constraint -> Constraint) (#)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

FixityOf (k -> k -> Constraint) ((#~) k)

Methods

fixityOf :: proxy c -> Maybe Fixity

NameTyOf (k -> k -> Constraint) ((#~) k)

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

TypeInstancesFor (k -> k -> Constraint) ((#~) k)

Methods

expandFamFor :: Source src => proxy c -> Len Type vs -> Const kt src fam -> Types src vs ts -> Maybe (Type kt src vs (Fam kt fam ts))

(KindInj k2, Typeable Type k2) => ClassInstancesFor (k2 -> k2 -> Constraint) ((#~) k2)

Methods

proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q)

type Type_of_Ty Constraint

type Type_of_Ty Constraint = Constraint

type Ty_of_Type Constraint

type Ty_of_Type Constraint = Constraint

Orphan instances

NameTyOf Constraint ()

Methods

nameTyOf :: proxy c -> Mod NameTy

isNameTyOp :: proxy c -> Bool

FixityOf (* -> * -> *) (->)

Methods

fixityOf :: proxy c -> Maybe Fixity