symantic-6.3.3.20190614: Library for Typed Tagless-Final Higher-Order Composable DSL

Safe HaskellNone
LanguageHaskell2010

Language.Symantic.Typing.Type

Contents

Synopsis

Documentation

class TypeOf a where Source #

Methods

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

Instances
SourceInj (TermT src ss ts vs) src => TypeOf (Term src ss ts vs :: Type -> Type) Source # 
Instance details

Defined in Language.Symantic.Compiling.Term

Methods

typeOf :: Term src ss ts vs t -> Type0 (SourceOf (Term src ss ts vs t)) (VarsOf (Term src ss ts vs t)) t Source #

data Types src vs (ts :: [Type]) 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
Source src => Show (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Show

Methods

showsPrec :: Int -> Types src vs ts -> ShowS #

show :: Types src vs ts -> String #

showList :: [Types src vs ts] -> ShowS #

UsedVarsOf (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

usedVarsOf :: UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs0 -> Types src vs ts -> (forall (vs' :: [Type]). UsedVars (SourceOf (Types src vs ts)) (VarsOf (Types src vs ts)) vs' -> ret) -> ret Source #

VarOccursIn (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

varOccursIn :: Var src0 (VarsOf (Types src vs ts)) v -> Types src vs ts -> Bool Source #

ConstsOf (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

Substable (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

substVarUnsafe :: (src0 ~ SourceOf (Types src vs ts), vs0 ~ VarsOf (Types src vs ts)) => Var src0 vs0 v -> Type src0 vs0 v -> Types src vs ts -> Types src vs ts Source #

subst :: (src0 ~ SourceOf (Types src vs ts), vs0 ~ VarsOf (Types src vs ts)) => Subst src0 vs0 -> Types src vs ts -> Types src vs ts Source #

type SourceOf (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type SourceOf (Types src vs ts) = src
type VarsOf (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type VarsOf (Types src vs ts) = vs

class ExpandFam a where Source #

Methods

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

Instances
ExpandFam (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

expandFam :: Type src vs t -> Type src vs t Source #

ExpandFam (Term src ss ts vs t) Source # 
Instance details

Defined in Language.Symantic.Compiling.Term

Methods

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

class TypeInstancesFor (c :: kc) where Source #

Minimal complete definition

Nothing

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 () Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

TypeInstancesFor (#>) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

TypeInstancesFor (#) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

TypeInstancesFor ((#~) :: k -> k -> Constraint) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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 ClassInstancesFor c where Source #

Minimal complete definition

Nothing

Methods

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

Instances
ClassInstancesFor () Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ClassInstancesFor (#>) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ClassInstancesFor (#) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

(KindInj k, Typeable k) => ClassInstancesFor ((#~) :: k -> k -> Constraint) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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 x ~ y => x #~ y infixr 2 Source #

Type equality Constraint.

Instances
x ~ y => (x :: k) #~ (y :: k) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

FixityOf ((#~) :: k -> k -> Constraint) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

fixityOf :: proxy (#~) -> Maybe Fixity Source #

NameTyOf ((#~) :: k -> k -> Constraint) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

nameTyOf :: proxy (#~) -> Mod NameTy Source #

isNameTyOp :: proxy (#~) -> Bool Source #

TypeInstancesFor ((#~) :: k -> k -> Constraint) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

(KindInj k, Typeable k) => ClassInstancesFor ((#~) :: k -> k -> Constraint) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Constraint union.

Instances
(x, y) => x # y Source # 
Instance details

Defined in Language.Symantic.Typing.Type

FixityOf (#) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

fixityOf :: proxy (#) -> Maybe Fixity Source #

NameTyOf (#) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

nameTyOf :: proxy (#) -> Mod NameTy Source #

isNameTyOp :: proxy (#) -> Bool Source #

TypeInstancesFor (#) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ClassInstancesFor (#) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

newtype (q :: Constraint) #> (a :: Type) infixr 0 Source #

Type constant to qualify a Type.

Constructors

Qual (q => a) 
Instances
FixityOf (#>) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

fixityOf :: proxy (#>) -> Maybe Fixity Source #

NameTyOf (#>) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

nameTyOf :: proxy (#>) -> Mod NameTy Source #

isNameTyOp :: proxy (#>) -> Bool Source #

TypeInstancesFor (#>) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ClassInstancesFor (#>) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Equations

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

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

Equations

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

data ConstC src Source #

Constructors

ConstC (Const src c) 
Instances
Eq (ConstC src) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Ord (ConstC src) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

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 #

class ConstsOf a where Source #

Return the Consts used by something.

Methods

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

Instances
ConstsOf (Types src vs ts) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ConstsOf (Const src c) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ConstsOf (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ConstsOf (Term src ss ts vs t) Source # 
Instance details

Defined in Language.Symantic.Compiling.Term

Methods

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

data Const src (c :: kc) where Source #

Type constant.

Constructors

Const :: Constable c => Kind src kc -> Const src (c :: kc) 
Instances
SourceInj (ConstC src) src => KindOf (Const src :: kt -> Type) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

kindOf :: Const src t -> Kind (SourceOf (Const src t)) kt0 Source #

Eq (Const src c) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Ord (Const src c) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

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

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

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

max :: Const src c -> Const src c -> Const src c #

min :: Const src c -> Const src c -> Const src c #

NameTyOf c => Show (Const src c) Source # 
Instance details

Defined in Language.Symantic.Typing.Show

Methods

showsPrec :: Int -> Const src c -> ShowS #

show :: Const src c -> String #

showList :: [Const src c] -> ShowS #

ConstsOf (Const src c) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

type SourceOf (Const src c) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type SourceOf (Const src c) = src

data TypeVT src Source #

Existential polymorphic Type.

Constructors

TypeVT (Type src vs t) 
Instances
Source src => Eq (TypeVT src) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Source src => Show (TypeVT src) Source # 
Instance details

Defined in Language.Symantic.Typing.Show

Methods

showsPrec :: Int -> TypeVT src -> ShowS #

show :: TypeVT src -> String #

showList :: [TypeVT src] -> ShowS #

SourceInj (TypeVT (SrcTe inp ss)) (SrcTe inp ss) Source # 
Instance details

Defined in Language.Symantic.Compiling.Read

Methods

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

type SourceOf (TypeVT src) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type SourceOf (TypeVT src) = src

data TypeT src vs Source #

Existential for Type.

Constructors

TypeT (Type src vs t) 
Instances
Source src => Eq (TypeT src vs) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Source src => Show (TypeT src vs) Source # 
Instance details

Defined in Language.Symantic.Typing.Show

Methods

showsPrec :: Int -> TypeT src vs -> ShowS #

show :: TypeT src vs -> String #

showList :: [TypeT src vs] -> ShowS #

type SourceOf (TypeT src vs) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type SourceOf (TypeT src vs) = src
type VarsOf (TypeT src vs) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type VarsOf (TypeT src vs) = vs

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 # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Source src => Show (TypeK src vs kt) Source # 
Instance details

Defined in Language.Symantic.Typing.Show

Methods

showsPrec :: Int -> TypeK src vs kt -> ShowS #

show :: TypeK src vs kt -> String #

showList :: [TypeK src vs kt] -> ShowS #

type SourceOf (TypeK src vs ki) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type SourceOf (TypeK src vs ki) = src
type VarsOf (TypeK src vs ki) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type VarsOf (TypeK src vs ki) = vs

data Type (src :: Type) (vs :: [Type]) (t :: kt) 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 (Type src :: [Type] -> k -> Type) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

allocVarsL :: Len len -> Type src vs x -> Type src (len ++ vs) x Source #

allocVarsR :: Len len -> Type src vs x -> Type src (vs ++ len) x Source #

SourceInj (TypeVT src) src => TestEquality (Type src vs :: k -> Type) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

SourceInj (TypeVT src) src => KindOf (Type src vs :: kt -> Type) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

kindOf :: Type src vs t -> Kind (SourceOf (Type src vs t)) kt0 Source #

Source src => Eq (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

Source src => Show (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Show

Methods

showsPrec :: Int -> Type src vs t -> ShowS #

show :: Type src vs t -> String #

showList :: [Type src vs t] -> ShowS #

Source src => Sourceable (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

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

UsedVarsOf (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

usedVarsOf :: UsedVars (SourceOf (Type src vs t)) (VarsOf (Type src vs t)) vs0 -> Type src vs t -> (forall (vs' :: [Type0]). UsedVars (SourceOf (Type src vs t)) (VarsOf (Type src vs t)) vs' -> ret) -> ret Source #

VarOccursIn (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

varOccursIn :: Var src0 (VarsOf (Type src vs t)) v -> Type src vs t -> Bool Source #

LenVars (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

ExpandFam (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

expandFam :: Type src vs t -> Type src vs t Source #

ConstsOf (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

Methods

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

Substable (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

substVarUnsafe :: (src0 ~ SourceOf (Type src vs t), vs0 ~ VarsOf (Type src vs t)) => Var src0 vs0 v -> Type src0 vs0 v -> Type src vs t -> Type src vs t Source #

subst :: (src0 ~ SourceOf (Type src vs t), vs0 ~ VarsOf (Type src vs t)) => Subst src0 vs0 -> Type src vs t -> Type src vs t Source #

type SourceOf (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type SourceOf (Type src vs t) = src
type VarsOf (Type src vs t) Source # 
Instance details

Defined in Language.Symantic.Typing.Type

type VarsOf (Type src vs t) = vs

pattern (:@) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). t ~# f a => Type src vs f -> Type src vs a -> Type src vs t infixl 9 Source #

pattern (:$) :: forall kt src (vs :: [Type]) (t :: kt). () => forall k (f :: k -> kt) (a :: k). t ~# f a => Type src vs f -> Type src vs a -> Type src vs t infixr 0 Source #

tyConst :: forall kc (c :: kc) 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 :: kc) 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 :: kc) 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.

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

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

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.

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

Qualify a Type.

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

Unify two Constraints.

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.

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

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 #

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

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 #

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 :: kc) 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 :: kc) 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 #

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

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

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

data Proxy (t :: k) :: forall k. k -> Type #

Proxy is a type that holds no data, but has a phantom parameter of arbitrary type (or even kind). Its use is to provide type information, even though there is no value available of that type (or it may be too costly to create one).

Historically, Proxy :: Proxy a is a safer alternative to the 'undefined :: a' idiom.

>>> Proxy :: Proxy (Void, Int -> Int)
Proxy

Proxy can even hold types of higher kinds,

>>> Proxy :: Proxy Either
Proxy
>>> Proxy :: Proxy Functor
Proxy
>>> Proxy :: Proxy complicatedStructure
Proxy

Constructors

Proxy 
Instances
(ModuleFor src ss s, ModulesInjR src ss rs) => ModulesInjR src ss (Proxy s ': rs) Source # 
Instance details

Defined in Language.Symantic.Compiling.Module

(Gram_Term_AtomsFor src ss g t, Gram_Term_AtomsR src ss rs g) => Gram_Term_AtomsR src ss (Proxy t ': rs) g Source # 
Instance details

Defined in Language.Symantic.Compiling.Grammar

Methods

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

Generic1 (Proxy :: k -> Type) 
Instance details

Defined in GHC.Generics

Associated Types

type Rep1 Proxy :: k -> Type #

Methods

from1 :: Proxy a -> Rep1 Proxy a #

to1 :: Rep1 Proxy a -> Proxy a #

Monad (Proxy :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.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 :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

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

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

Applicative (Proxy :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

pure :: a -> Proxy a #

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

liftA2 :: (a -> b -> c) -> Proxy a -> Proxy b -> Proxy c #

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

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

Foldable (Proxy :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Foldable

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 :: Type -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Traversable

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

Eq1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Classes

Methods

liftEq :: (a -> b -> Bool) -> Proxy a -> Proxy b -> Bool #

Ord1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Classes

Methods

liftCompare :: (a -> b -> Ordering) -> Proxy a -> Proxy b -> Ordering #

Read1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Classes

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Proxy a) #

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Proxy a] #

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Proxy a) #

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Proxy a] #

Show1 (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Functor.Classes

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Proxy a -> ShowS #

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Proxy a] -> ShowS #

Alternative (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Proxy

Methods

empty :: Proxy a #

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

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

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

MonadPlus (Proxy :: Type -> Type)

Since: base-4.9.0.0

Instance details

Defined in Data.Proxy

Methods

mzero :: Proxy a #

mplus :: Proxy a -> Proxy a -> Proxy a #

SymInjP Zero (Proxy s ': ss) (s :: k) Source # 
Instance details

Defined in Language.Symantic.Compiling.Term

Methods

symInjP :: TeSym (Proxy s ': []) ts t -> TeSym (Proxy s ': ss) ts t Source #

SymInjP p ss s => SymInjP (Succ p :: Type) (Proxy not_s ': ss) (s :: k2) Source # 
Instance details

Defined in Language.Symantic.Compiling.Term

Methods

symInjP :: TeSym (Proxy s ': []) ts t -> TeSym (Proxy not_s ': ss) ts t Source #

(NameTyOf t, FixityOf t, ImportTypes ts) => ImportTypes (Proxy t ': ts :: [Type]) Source # 
Instance details

Defined in Language.Symantic.Typing.Module

(KindInjP (Ty_of_Type (K c)), K c ~ Type_of_Ty (Ty_of_Type (K c)), Constable c, ModulesTyInj ts) => ModulesTyInj (Proxy c ': ts :: [Type]) Source # 
Instance details

Defined in Language.Symantic.Typing.Grammar

Methods

modulesTyInj :: Source src => ModulesTy src Source #

Bounded (Proxy t)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

minBound :: Proxy t #

maxBound :: Proxy t #

Enum (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

succ :: Proxy s -> Proxy s #

pred :: Proxy s -> Proxy s #

toEnum :: Int -> Proxy s #

fromEnum :: Proxy s -> Int #

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

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

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

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

Eq (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

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

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

Ord (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

compare :: Proxy s -> Proxy s -> Ordering #

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

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

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

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

max :: Proxy s -> Proxy s -> Proxy s #

min :: Proxy s -> Proxy s -> Proxy s #

Read (Proxy t)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Show (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

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

show :: Proxy s -> String #

showList :: [Proxy s] -> ShowS #

Ix (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

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

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

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

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

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

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

Generic (Proxy t) 
Instance details

Defined in GHC.Generics

Associated Types

type Rep (Proxy t) :: Type -> Type #

Methods

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

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

Semigroup (Proxy s)

Since: base-4.9.0.0

Instance details

Defined in Data.Proxy

Methods

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

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

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

Monoid (Proxy s)

Since: base-4.7.0.0

Instance details

Defined in Data.Proxy

Methods

mempty :: Proxy s #

mappend :: Proxy s -> Proxy s -> Proxy s #

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

type Rep1 (Proxy :: k -> Type)

Since: base-4.6.0.0

Instance details

Defined in GHC.Generics

type Rep1 (Proxy :: k -> Type) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> Type))
type Rep (Proxy t)

Since: base-4.6.0.0

Instance details

Defined in GHC.Generics

type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: Type -> Type))

data (a :: k) :~: (b :: k) :: forall k. k -> k -> Type 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: base-4.7.0.0

Constructors

Refl :: forall k (a :: k) (b :: k). a :~: a 
Instances
TestEquality ((:~:) a :: k -> Type)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #

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

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~: b #

maxBound :: a :~: b #

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

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~: b #

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

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

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

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

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

Eq (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

Ord (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

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 #

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

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

readList :: ReadS [a :~: b] #

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

readListPrec :: ReadPrec [a :~: b] #

Show (a :~: b)

Since: base-4.7.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

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

data (a :: k1) :~~: (b :: k2) :: forall k1 k2. k1 -> k2 -> Type where infix 4 #

Kind heterogeneous propositional equality. Like :~:, a :~~: b is inhabited by a terminating value if and only if a is the same type as b.

Since: base-4.10.0.0

Constructors

HRefl :: forall k1 k2 (a :: k1) (b :: k2). a :~~: a 
Instances
TestEquality ((:~~:) a :: k -> Type)

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

testEquality :: (a :~~: a0) -> (a :~~: b) -> Maybe (a0 :~: b) #

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

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

minBound :: a :~~: b #

maxBound :: a :~~: b #

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

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

toEnum :: Int -> a :~~: b #

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

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

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

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

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

Eq (a :~~: b)

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

Ord (a :~~: b)

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

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 #

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

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

readList :: ReadS [a :~~: b] #

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

readListPrec :: ReadPrec [a :~~: b] #

Show (a :~~: b)

Since: base-4.10.0.0

Instance details

Defined in Data.Type.Equality

Methods

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

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

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

data Constraint #

The kind of constraints, like Show a

Orphan instances

NameTyOf () Source # 
Instance details

Methods

nameTyOf :: proxy () -> Mod NameTy Source #

isNameTyOp :: proxy () -> Bool Source #

FixityOf ((->) :: Type -> Type -> Type) Source # 
Instance details

Methods

fixityOf :: proxy (->) -> Maybe Fixity Source #