Safe Haskell	None
Language	Haskell2010

Language.Symantic.Typing.Type

Contents

Type Type
Type Const
Type '(->)'
Type Qual
Type family Fam
- Class TypeInstancesFor
- Class ExpandFam
Type Types
Class TypeOf
Orphan instances

Synopsis

Type `Type`

data Type src vs t where Source #

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) Source #
Methods allocVarsL :: Len Type len -> a vs x -> a ((Type ++ len) vs) x Source # allocVarsR :: Len Type len -> a vs x -> a ((Type ++ vs) len) x Source #
SourceInj (TypeVT src) src => TestEquality k (Type k src vs) Source #
Methods testEquality :: f a -> f b -> Maybe ((Type k src vs :~: a) b) #
SourceInj (TypeVT src) src => KindOf kt (Type kt src vs) Source #
Methods kindOf :: a t -> Kind (SourceOf (a t)) (Type kt src vs) Source #
Source src => Eq (Type kt src vs t) Source #
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) Source #
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) Source #
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 Source #
VarOccursIn (Type kt src vs t) Source #
Methods varOccursIn :: Var kv src (VarsOf (Type kt src vs t)) v -> Type kt src vs t -> Bool Source #
LenVars (Type kt src vs t) Source #
Methods lenVars :: Type kt src vs t -> Len Type (VarsOf (Type kt src vs t)) Source #
ExpandFam (Type kt src vs t) Source #
Methods expandFam :: Type kt src vs t -> Type kt src vs t Source #
ConstsOf (Type kt src vs t) Source #
Methods constsOf :: Type kt src vs t -> Set (ConstC (SourceOf (Type kt src vs t))) Source #
Substable (Type kt src vs t) Source #
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 Source # 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 Source #
type SourceOf (Type kt src vs t) Source #
type SourceOf (Type kt src vs t) = src
type VarsOf (Type kt src vs t) Source #
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 Source #

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 Source #

Like tyConst, but not using lenInj.

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

Like TyApp, but using noSource.

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

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) Source #

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 Source #

Qualify a Type.

Type `TypeK`

data TypeK src vs kt Source #

Existential Type of a known Kind.

Constructors

TypeK (Type src vs t)

Instances

Source src => Eq (TypeK src vs ki) Source #
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) Source #
type SourceOf (TypeK src vs ki) = src
type VarsOf (TypeK src vs ki) Source #
type VarsOf (TypeK src vs ki) = vs

Type `TypeT`

data TypeT src vs Source #

Existential for Type.

Constructors

TypeT (Type src vs t)

Instances

Source src => Eq (TypeT src vs) Source #
Methods (==) :: TypeT src vs -> TypeT src vs -> Bool # (/=) :: TypeT src vs -> TypeT src vs -> Bool #
type SourceOf (TypeT src vs) Source #
type SourceOf (TypeT src vs) = src
type VarsOf (TypeT src vs) Source #
type VarsOf (TypeT src vs) = vs

Type `TypeVT`

data TypeVT src Source #

Existential polymorphic Type.

Constructors

TypeVT (Type src vs t)

Instances

Source src => Eq (TypeVT src) Source #
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) Source #
type SourceOf (TypeVT src) = src

Type `Const`

data Const src c where Source #

Type constant.

Constructors

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

Instances

SourceInj (ConstC src) src => KindOf kt (Const kt src) Source #
Methods kindOf :: a t -> Kind (SourceOf (a t)) (Const kt src) Source #
Eq (Const kc src c) Source #
Methods (==) :: Const kc src c -> Const kc src c -> Bool # (/=) :: Const kc src c -> Const kc src c -> Bool #
Ord (Const kc src c) Source #
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) Source #
Methods constsOf :: Const kc src c -> Set (ConstC (SourceOf (Const kc src c))) Source #
type SourceOf (Const kc src c) Source #
type SourceOf (Const kc src c) = src

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

Class `Constable`

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

Instances

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

Class `ConstsOf`

class ConstsOf a where Source #

Return the Consts used by something.

Minimal complete definition

constsOf

Methods

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

Instances

ConstsOf (Types src vs ts) Source #
Methods constsOf :: Types src vs ts -> Set (ConstC (SourceOf (Types src vs ts))) Source #
ConstsOf (Const kc src c) Source #
Methods constsOf :: Const kc src c -> Set (ConstC (SourceOf (Const kc src c))) Source #
ConstsOf (Type kt src vs t) Source #
Methods constsOf :: Type kt src vs t -> Set (ConstC (SourceOf (Type kt src vs t))) Source #
ConstsOf (Term src ss ts vs t) Source #
Methods constsOf :: Term src ss ts vs t -> Set (ConstC (SourceOf (Term src ss ts vs t))) Source #

Type `ConstC`

data ConstC src Source #

Constructors

ConstC (Const src c)

Instances

Eq (ConstC src) Source #
Methods (==) :: ConstC src -> ConstC src -> Bool # (/=) :: ConstC src -> ConstC src -> Bool #
Ord (ConstC src) Source #
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 Source #

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

Type family `FunArg`

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

Equations

FunArg (q #> f) = FunArg f
FunArg (a -> b) = a

Type family `FunRes`

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

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)) Source #

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

Type `(#>)`

newtype q #> a infixr 0 Source #

Type constant to qualify a Type.

Constructors

Qual (q => a)

Instances

FixityOf (Constraint -> Type -> *) (#>) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
NameTyOf (Constraint -> Type -> *) (#>) Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
TypeInstancesFor (Constraint -> Type -> *) (#>) Source #
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)) Source #
ClassInstancesFor (Constraint -> Type -> *) (#>) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #

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

Qualify a Type.

Class `(#)`

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

Constraint union.

Instances

(x, y) => x # y Source #

FixityOf (Constraint -> Constraint -> Constraint) (#) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
NameTyOf (Constraint -> Constraint -> Constraint) (#) Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
TypeInstancesFor (Constraint -> Constraint -> Constraint) (#) Source #
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)) Source #
ClassInstancesFor (Constraint -> Constraint -> Constraint) (#) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #

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

Unify two Constraints.

Type `(() ::` `Constraint)`

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

Like noConstraintLen, but using lenInj.

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

Empty Constraint.

Class `(#~)`

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

Type equality Constraint.

Instances

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

FixityOf (k -> k -> Constraint) ((#~) k) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
NameTyOf (k -> k -> Constraint) ((#~) k) Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
TypeInstancesFor (k -> k -> Constraint) ((#~) k) Source #
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)) Source #
(KindInj k2, Typeable Type k2) => ClassInstancesFor (k2 -> k2 -> Constraint) ((#~) k2) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #

(#~) :: 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 Source #

Constraint two Types to be equal.

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

Type equality.

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

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) Source #

Comparison

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

Compare two Types.

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

Type `Qual`

data Qual q where Source #

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 Source #

Methods

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

Instances

ClassInstancesFor Constraint () Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
ClassInstancesFor (Constraint -> Type -> *) (#>) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
ClassInstancesFor (Constraint -> Constraint -> Constraint) (#) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
(KindInj k2, Typeable Type k2) => ClassInstancesFor (k2 -> k2 -> Constraint) ((#~) k2) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #

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

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 Source #

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

Projection

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

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) Source #

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) Source #

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) Source #

Like proj_ConstKi, but on a Type.

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

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

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

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

Type family `Fam`

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

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 Source #

Methods

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

Instances

TypeInstancesFor Constraint () Source #
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)) Source #
TypeInstancesFor (Constraint -> Type -> *) (#>) Source #
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)) Source #
TypeInstancesFor (Constraint -> Constraint -> Constraint) (#) Source #
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)) Source #
TypeInstancesFor (k -> k -> Constraint) ((#~) k) Source #
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)) Source #

Class `ExpandFam`

class ExpandFam a where Source #

Minimal complete definition

expandFam

Methods

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

Instances

ExpandFam (Type kt src vs t) Source #
Methods expandFam :: Type kt src vs t -> Type kt src vs t Source #
ExpandFam (Term src ss ts vs t) Source #
Methods expandFam :: Term src ss ts vs t -> Term src ss ts vs t Source #

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

Like kindOf but keep the old Source.

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

Remove unused Vars from ther context.

Type `Types`

data Types src vs ts where Source #

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) Source #
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 Source #
VarOccursIn (Types src vs ts) Source #
Methods varOccursIn :: Var kv src (VarsOf (Types src vs ts)) v -> Types src vs ts -> Bool Source #
ConstsOf (Types src vs ts) Source #
Methods constsOf :: Types src vs ts -> Set (ConstC (SourceOf (Types src vs ts))) Source #
Substable (Types src vs ts) Source #
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 Source # 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 Source #
type SourceOf (Types src vs ts) Source #
type SourceOf (Types src vs ts) = src
type VarsOf (Types src vs ts) Source #
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 Source #

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

Class `TypeOf`

class TypeOf a where Source #

Minimal complete definition

typeOf

Methods

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

Instances

SourceInj (TermT src ss ts vs) src => TypeOf Type (Term src ss ts vs) Source #
Methods typeOf :: a t -> Type (Term src ss ts vs) (SourceOf (a t)) (VarsOf (a t)) t Source #

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) Source #
Methods modulesInjR :: Either Error_Module (Modules src ss) Source #
(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 Source #
Methods g_term_atomsR :: [CF g (AST_Term src ss)] Source #
SymInjP k * Zero ((:) * (Proxy k s) ss) s Source #
Methods symInjP :: TeSym ((* ': Proxy Zero s) [*]) ts t -> TeSym ss ts t Source #
SymInjP k1 * p ss s => SymInjP k1 * (Succ p) ((:) * (Proxy k not_s) ss) s Source #
Methods symInjP :: TeSym ((* ': Proxy (Succ p) s) [*]) ts t -> TeSym ss ts t Source #
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) Source #
Methods importTypes :: PathMod -> Imports NameTy Source #
(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) Source #
Methods modulesTyInj :: Source src => ModulesTy src Source #
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 Source #

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 Source #
Methods kindInjP :: src -> Kind src (Type_of_Ty Constraint) Source #
FixityOf Constraint c Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
TypeInstancesFor Constraint () Source #
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)) Source #
ClassInstancesFor Constraint () Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
FixityOf (Constraint -> Type -> *) (#>) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
FixityOf (Constraint -> Constraint -> Constraint) (#) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
NameTyOf (Constraint -> Type -> *) (#>) Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
NameTyOf (Constraint -> Constraint -> Constraint) (#) Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
TypeInstancesFor (Constraint -> Type -> *) (#>) Source #
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)) Source #
TypeInstancesFor (Constraint -> Constraint -> Constraint) (#) Source #
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)) Source #
ClassInstancesFor (Constraint -> Type -> *) (#>) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
ClassInstancesFor (Constraint -> Constraint -> Constraint) (#) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
FixityOf (k -> k -> Constraint) ((#~) k) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #
NameTyOf (k -> k -> Constraint) ((#~) k) Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
TypeInstancesFor (k -> k -> Constraint) ((#~) k) Source #
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)) Source #
(KindInj k2, Typeable Type k2) => ClassInstancesFor (k2 -> k2 -> Constraint) ((#~) k2) Source #
Methods proveConstraintFor :: Source src => proxy c -> Type Constraint src vs q -> Maybe (Qual q) Source #
type Type_of_Ty Constraint Source #
type Type_of_Ty Constraint = Constraint
type Ty_of_Type Constraint Source #
type Ty_of_Type Constraint = Constraint

Orphan instances

NameTyOf Constraint () Source #
Methods nameTyOf :: proxy c -> Mod NameTy Source # isNameTyOp :: proxy c -> Bool Source #
FixityOf (* -> * -> *) (->) Source #
Methods fixityOf :: proxy c -> Maybe Fixity Source #

Type Type

Type TypeK

Type TypeT

Type TypeVT

Type Const

Class Constable

Class ConstsOf

Type ConstC

Type '(->)'

Type family FunArg

Type family FunRes

Type (#>)

Class (#)

Type (() :: Constraint)

Class (#~)

Comparison

Type Qual

Class ClassInstancesFor

Injection

Projection

Type family Fam

Class TypeInstancesFor

Class ExpandFam

Type Types

Class TypeOf

Orphan instances

Type `Type`

Type `TypeK`

Type `TypeT`

Type `TypeVT`

Type `Const`

Class `Constable`

Class `ConstsOf`

Type `ConstC`

Type family `FunArg`

Type family `FunRes`

Type `(#>)`

Class `(#)`

Type `(() ::` `Constraint)`

Class `(#~)`

Type `Qual`

Class `ClassInstancesFor`

Type family `Fam`

Class `TypeInstancesFor`

Class `ExpandFam`

Type `Types`

Class `TypeOf`