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)

Methods

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

Show (Kind src k)

Methods

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

show :: Kind src k -> String

showList :: [Kind src k] -> ShowS

Source src => Sourced (Kind src k)

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)

type SourceOf (Kind src k) = src

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

Type K

type K t = kt

Class KindOf

class KindOf a where

Return the Kind of something.

Minimal complete definition

kindOf

Methods

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

Instances

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

Methods

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

Inj_Source (EVar src vs) src => KindOf kt (Var kt src vs)

Methods

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

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

Methods

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

Type Inj_Kind

class (Inj_KindP (Ty_of_Type k), Type_of_Ty (Ty_of_Type k) ~ k) => Inj_Kind 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 Inj_KindP.

Instances

(Inj_KindP (Ty_of_Type k), (~) Type (Type_of_Ty (Ty_of_Type k)) k) => Inj_Kind k

inj_Kind :: forall k src. Source src => Inj_Kind k => Kind src k

Type Inj_KindP

class Inj_KindP k where

Minimal complete definition

inj_KindP

Methods

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

Instances

Inj_KindP Constraint

Methods

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

Inj_KindP Ty

Methods

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

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

Methods

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

Type Ty

data Ty

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

Instances

Inj_KindP Ty

Methods

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

type Type_of_Ty Ty

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

type Ty_of_Type Type = Ty

type Ty_of_Type Constraint

type Ty_of_Type Constraint = Constraint

type Ty_of_Type (a -> b)

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

type Type_of_Ty Constraint = Constraint

type Type_of_Ty Ty

type Type_of_Ty Ty = Type

type Type_of_Ty (a -> b)

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)

Methods

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

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

Show (KindK src)

Methods

showsPrec :: Int -> KindK src -> ShowS

show :: KindK src -> String

showList :: [KindK src] -> ShowS

Inj_Source (KindK (SrcTe inp ss)) (SrcTe inp ss)

Methods

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

Methods

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

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

Show (Con_Kind src)

Methods

showsPrec :: Int -> Con_Kind src -> ShowS

show :: Con_Kind src -> String

showList :: [Con_Kind src] -> ShowS

Inj_Error (Con_Kind src) (Error_Type src)

Methods

inj_Error :: Con_Kind src -> Error_Type src

Inj_Error (Con_Kind src) (Error_Unify src)

Methods

inj_Error :: Con_Kind src -> Error_Unify src

Inj_Error (Con_Kind src) (Error_Term src)

Methods

inj_Error :: Con_Kind src -> Error_Term src

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

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