Language.Symantic.Typing.Kind

Type Kind

data Kind src k where

Singleton for kind types.

Constructors

KiType :: src -> Kind src Type

KiConstraint :: src -> Kind src Constraint

KiFun :: src -> Kind src ka -> Kind src kb -> Kind src (ka -> kb) infixr 5

Instances

TestEquality (Kind src :: * -> *)

Defined in Language.Symantic.Typing.Kind

Methods

testEquality :: Kind src a -> Kind src b -> Maybe (a :~: b)

Show (Kind src k)

Defined in Language.Symantic.Typing.Kind

Methods

showsPrec :: Int -> Kind src k -> ShowS

show :: Kind src k -> String

showList :: [Kind src k] -> ShowS

Source src => Sourced (Kind src k)

Defined in Language.Symantic.Typing.Kind

Methods

sourceOf :: Kind src k -> SourceOf (Kind src k)

setSource :: Kind src k -> SourceOf (Kind src k) -> Kind src k

type SourceOf (Kind src k)

Defined in Language.Symantic.Typing.Kind

type SourceOf (Kind src k) = src

eqKind :: Kind xs x -> Kind ys y -> Maybe (x :~: y)

Type K

type K (t :: kt) = kt

Class KindOf

class KindOf (a :: kt -> Type) where

Return the Kind of something.

Minimal complete definition

kindOf

Methods

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

Instances

SourceInj (ConstC src) src => KindOf (Const src :: kt -> *)

Defined in Language.Symantic.Typing.Type

Methods

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

SourceInj (EVar src vs) src => KindOf (Var src vs :: kt -> *)

Defined in Language.Symantic.Typing.Variable

Methods

kindOf :: Var src vs t -> Kind (SourceOf (Var src vs t)) kt0

SourceInj (TypeVT src) src => KindOf (Type src vs :: kt -> *)

Defined in Language.Symantic.Typing.Type

Methods

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

Type KindInj

class (KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k

Implicit Kind.

NOTE: GHC-8.0.1's bug #12933 makes it fail to properly build an implicit Kind, this can however be worked around by having the class instances work on a data type Ty instead of Type, hence the introduction of Ty, Ty_of_Type, Type_of_Ty and KindP.Inj

Instances

(KindInjP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => KindInj k

Defined in Language.Symantic.Typing.Kind

kindInj :: forall k src. Source src => KindInj k => Kind src k

Type KindInjP

class KindInjP k where

Minimal complete definition

kindInjP

Methods

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

Instances

KindInjP Constraint

Defined in Language.Symantic.Typing.Kind

Methods

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

KindInjP Ty

Defined in Language.Symantic.Typing.Kind

Methods

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

(KindInjP a, KindInjP b) => KindInjP (a -> b)

Defined in Language.Symantic.Typing.Kind

Methods

kindInjP :: src -> Kind src (Type_of_Ty (a -> b))

Type Ty

data Ty

FIXME: workaround to be removed when #12933 will be fixed.

Instances

KindInjP Ty

Defined in Language.Symantic.Typing.Kind

Methods

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

type Type_of_Ty Ty

Defined in Language.Symantic.Typing.Kind

type Type_of_Ty Ty = Type

Type family Ty_of_Type

type family Ty_of_Type (t :: Type) :: Type

NOTE: As of GHC-8.0.2, using a closed type family does not work here, this notably disables the expansion of Ty_of_Type Any.

Instances

type Ty_of_Type Type

Defined in Language.Symantic.Typing.Kind

type Ty_of_Type Type = Ty

type Ty_of_Type Constraint

Defined in Language.Symantic.Typing.Kind

type Ty_of_Type Constraint = Constraint

type Ty_of_Type (a -> b)

Defined in Language.Symantic.Typing.Kind

type Ty_of_Type (a -> b) = Ty_of_Type a -> Ty_of_Type b

Type family Type_of_Ty

type family Type_of_Ty (t :: Type) :: Type

NOTE: As of GHC-8.0.2, using a closed type family does not work here, this notably disables the expansion of Type_of_Ty Any.

Instances

type Type_of_Ty Constraint

Defined in Language.Symantic.Typing.Kind

type Type_of_Ty Constraint = Constraint

type Type_of_Ty Ty

Defined in Language.Symantic.Typing.Kind

type Type_of_Ty Ty = Type

type Type_of_Ty (a -> b)

Defined in Language.Symantic.Typing.Kind

type Type_of_Ty (a -> b) = Type_of_Ty a -> Type_of_Ty b

Type KindK

data KindK src

Existential for Kind.

Constructors

KindK (Kind src k)

Instances

Eq (KindK src)

Defined in Language.Symantic.Typing.Kind

Methods

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

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

Show (KindK src)

Defined in Language.Symantic.Typing.Kind

Methods

showsPrec :: Int -> KindK src -> ShowS

show :: KindK src -> String

showList :: [KindK src] -> ShowS

SourceInj (KindK (SrcTe inp ss)) (SrcTe inp ss)

Defined in Language.Symantic.Compiling.Read

Methods

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

Type Con_Kind

data Con_Kind src

Constructors

Con_Kind_Eq (KindK src) (KindK src)

Con_Kind_Arrow (KindK src)

Instances

Eq (Con_Kind src)

Defined in Language.Symantic.Typing.Kind

Methods

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

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

Show (Con_Kind src)

Defined in Language.Symantic.Typing.Kind

Methods

showsPrec :: Int -> Con_Kind src -> ShowS

show :: Con_Kind src -> String

showList :: [Con_Kind src] -> ShowS

ErrorInj (Con_Kind src) (Error_Type src)

Defined in Language.Symantic.Typing.Grammar

Methods

errorInj :: Con_Kind src -> Error_Type src

ErrorInj (Con_Kind src) (Error_Unify src)

Defined in Language.Symantic.Typing.Unify

Methods

errorInj :: Con_Kind src -> Error_Unify src

ErrorInj (Con_Kind src) (Error_Term src)

Defined in Language.Symantic.Compiling.Read

Methods

errorInj :: Con_Kind src -> Error_Term src

when_EqKind :: ErrorInj (Con_Kind src) err => Kind src x -> Kind src y -> ((x :~: y) -> Either err ret) -> Either err ret

when_KiFun :: ErrorInj (Con_Kind src) err => SourceInj (KindK src) src => Kind src x -> (forall a b. (x :~: (a -> b)) -> Kind src a -> Kind src b -> Either err ret) -> Either err ret