Safe Haskell	None
Language	Haskell2010

Language.Symantic.Typing.Type

Contents

Orphan instances

Synopsis

class TypeOf a where
data Types src vs (ts :: [Type]) where
- TypesZ :: Types src vs '[]
- TypesS :: Type src vs t -> Types src vs ts -> Types src vs (Proxy t ': ts)
class ExpandFam a where
class TypeInstancesFor (c :: kc) where
type family Fam (fam :: k) (hs :: [Type]) :: k
class ClassInstancesFor c where
data Qual q where
- Dict :: q => Qual q
class x ~ y => x #~ y
class (x, y) => x # y
newtype (q :: Constraint) #> (a :: Type) = Qual (q => a)
type family FunRes (fun :: Type) :: Type where ...
type family FunArg (fun :: Type) :: Type where ...
data ConstC src = ConstC (Const src c)
class ConstsOf a where
class (Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable c
data Const src (c :: kc) where
- Const :: Constable c => Kind src kc -> Const src (c :: kc)
data TypeVT src = TypeVT (Type src vs t)
data TypeT src vs = TypeT (Type src vs t)
data TypeK src vs kt = TypeK (Type src vs t)
data Type (src :: Type) (vs :: [Type]) (t :: kt) where
- 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)
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
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
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
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
tyApp :: Source src => Type src vs f -> Type src vs a -> Type src vs (f a)
tyVar :: Source src => NameVar -> Var src vs v -> Type src vs v
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)
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)
kindOfConst :: Const src (t :: kt) -> Kind src kt
(~>) :: Source src => Constable (->) => Type src vs a -> Type src vs b -> Type src vs (a -> 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 src => Type src vs q -> Type src vs t -> Type src vs (q #> t)
(#) :: Source src => Type src vs qx -> Type src vs qy -> Type src vs (qx # qy)
noConstraint :: Source src => LenInj vs => Type src vs (() :: Constraint)
noConstraintLen :: Source src => Len vs -> Type src vs (() :: 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)
eqType :: Source src => Type src tys (x :: k) -> Type src tys (y :: k) -> Maybe (x :~: y)
eqTypeKi :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Maybe (x :~~: y)
eqTypes :: Source src => Types src tys x -> Types src tys y -> Maybe (x :~~: y)
ordType :: Source src => Type src tys (x :: kx) -> Type src tys (y :: ky) -> Ordering
ordTypes :: Source src => Types src tys x -> Types src tys y -> Ordering
proveConstraint :: Source src => Type src vs q -> Maybe (Qual q)
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)
proj_Const :: forall c u src. Typeable c => Const src u -> Maybe (c :~: u)
proj_ConstTy :: forall c u src vs. Typeable c => Type src vs u -> Maybe (c :~: u)
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)
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)
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
kindOfType :: Type src vs (t :: kt) -> Kind src kt
normalizeVarsTy :: Type src vs (t :: kt) -> (forall vs'. Type src vs' (t :: kt) -> ret) -> ret
mapTys :: (forall kt (t :: kt). Type src vs t -> Type src vs' t) -> Types src vs ts -> Types src vs' ts
foldlTys :: (forall k (t :: k). Type src vs t -> acc -> acc) -> Types src vs ts -> acc -> acc
data Proxy (t :: k) :: forall k. k -> * = Proxy
data (a :: k) :~: (b :: k) :: forall k. k -> k -> * where
- Refl :: a :~: a
data (a :: k1) :~~: (b :: k2) :: forall k1 k2. k1 -> k2 -> * where
- HRefl :: a :~~: a
data Constraint

Documentation

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 (Term src ss ts vs :: 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) #
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' :: [*]). 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 #

Minimal complete definition

expandFam

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 #

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 #

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.

Minimal complete definition

constsOf

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 #

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

Instances

(Typeable c, FixityOf c, NameTyOf c, ClassInstancesFor c, TypeInstancesFor c) => Constable (c :: kc) Source #
Instance details Defined in Language.Symantic.Typing.Type

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 -> *) 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) #
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) #
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) #
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) #
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) #
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 -> *) 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 -> *) 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 -> *) 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) #
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 => Sourced (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' :: [*]). 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 -> * #

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 Methods modulesInjR :: Either Error_Module (Modules src ss) Source #
(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 -> *)
Instance details Defined in GHC.Generics Associated Types type Rep1 Proxy :: k -> * # Methods from1 :: Proxy a -> Rep1 Proxy a # to1 :: Rep1 Proxy a -> Proxy a #
Monad (Proxy :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: * -> *)	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 :: *) (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 :: [*]) Source #
Instance details Defined in Language.Symantic.Typing.Module Methods importTypes :: PathMod -> Imports NameTy Source #
(KindInjP (Ty_of_Type (K c)), K c ~ Type_of_Ty (Ty_of_Type (K c)), Constable c, ModulesTyInj ts) => ModulesTyInj (Proxy c ': ts :: [*]) Source #
Instance details Defined in Language.Symantic.Typing.Grammar Methods modulesTyInj :: Source src => ModulesTy src Source #
Bounded (Proxy t)
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 Methods readsPrec :: Int -> ReadS (Proxy t) # readList :: ReadS [Proxy t] # readPrec :: ReadPrec (Proxy t) # readListPrec :: ReadPrec [Proxy t] #
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) :: * -> * # 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 -> *)
Instance details Defined in GHC.Generics type Rep1 (Proxy :: k -> ) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: k -> ))
type Rep (Proxy t)
Instance details Defined in GHC.Generics type Rep (Proxy t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) (U1 :: * -> *))

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

Constructors

Refl :: a :~: a

Instances

TestEquality ((:~:) a :: k -> *)	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)
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b)
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)
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 -> * 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 :: a :~~: a

Instances

TestEquality ((:~~:) a :: k -> *)	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 ((->) :: * -> * -> *) Source #
Instance details Methods fixityOf :: proxy (->) -> Maybe Fixity Source #