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

Safe HaskellNone
LanguageHaskell2010

Language.Symantic.Typing.Kind

Contents

Synopsis

Type Kind

data Kind src k where Source #

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

Defined in Language.Symantic.Typing.Kind

Methods

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

Show (Kind src k) Source # 
Instance details

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 => Sourceable (Kind src k) Source # 
Instance details

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

Defined in Language.Symantic.Typing.Kind

type SourceOf (Kind src k) = src

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

Type K

type K (t :: kt) = kt Source #

Class KindOf

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

Return the Kind of something.

Methods

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

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 #

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

Defined in Language.Symantic.Typing.Variable

Methods

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

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 #

Type KindInj

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

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

Defined in Language.Symantic.Typing.Kind

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

Type KindInjP

class KindInjP k where Source #

Methods

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

Instances
KindInjP Constraint Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

Methods

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

KindInjP Ty Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

Methods

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

(KindInjP a, KindInjP b) => KindInjP (a -> b) Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

Methods

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

Type Ty

data Ty Source #

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

Instances
KindInjP Ty Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

Methods

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

type Type_of_Ty Ty Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

Type family Ty_of_Type

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

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

Defined in Language.Symantic.Typing.Kind

type Ty_of_Type Constraint Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

type Ty_of_Type (a -> b) Source # 
Instance details

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

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

Defined in Language.Symantic.Typing.Kind

type Type_of_Ty Ty Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

type Type_of_Ty (a -> b) Source # 
Instance details

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

Existential for Kind.

Constructors

KindK (Kind src k) 
Instances
Eq (KindK src) Source # 
Instance details

Defined in Language.Symantic.Typing.Kind

Methods

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

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

Show (KindK src) Source # 
Instance details

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

Defined in Language.Symantic.Compiling.Read

Methods

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

Type Con_Kind

data Con_Kind src Source #

Constructors

Con_Kind_Eq (KindK src) (KindK src) 
Con_Kind_Arrow (KindK src) 
Instances
Eq (Con_Kind src) Source # 
Instance details

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

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

Defined in Language.Symantic.Typing.Grammar

Methods

errorInj :: Con_Kind src -> Error_Type src #

ErrorInj (Con_Kind src) (Error_Unify src) Source # 
Instance details

Defined in Language.Symantic.Typing.Unify

Methods

errorInj :: Con_Kind src -> Error_Unify src #

ErrorInj (Con_Kind src) (Error_Term src) Source # 
Instance details

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

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