symantic-6.3.0.20170807: 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) Source # 

Methods

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

Show (Kind src k) Source # 

Methods

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

show :: Kind src k -> String #

showList :: [Kind src k] -> ShowS #

Source src => Sourced (Kind src k) Source # 

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 # 
type SourceOf (Kind src k) = src

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

Type K

type K t = kt Source #

Class KindOf

class KindOf a where Source #

Return the Kind of something.

Minimal complete definition

kindOf

Methods

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

Instances

SourceInj (ConstC src) src => KindOf kt (Const kt src) Source # 

Methods

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

SourceInj (EVar src vs) src => KindOf kt (Var kt src vs) Source # 

Methods

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

SourceInj (TypeVT src) src => KindOf kt (Type kt src vs) Source # 

Methods

kindOf :: a t -> Kind (SourceOf (a t)) (Type kt src vs) 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

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

Type KindInjP

class KindInjP k where Source #

Minimal complete definition

kindInjP

Methods

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

Instances

KindInjP Constraint Source # 

Methods

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

KindInjP Ty Source # 

Methods

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

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

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

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.

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 KindK

data KindK src Source #

Existential for Kind.

Constructors

KindK (Kind src k) 

Instances

Eq (KindK src) Source # 

Methods

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

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

Show (KindK src) Source # 

Methods

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

show :: KindK src -> String #

showList :: [KindK src] -> ShowS #

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

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 # 

Methods

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

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

Show (Con_Kind src) Source # 

Methods

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

show :: Con_Kind src -> String #

showList :: [Con_Kind src] -> ShowS #

ErrorInj (Con_Kind src) (Error_Type src) # 

Methods

errorInj :: Con_Kind src -> Error_Type src #

ErrorInj (Con_Kind src) (Error_Unify src) # 

Methods

errorInj :: Con_Kind src -> Error_Unify src #

ErrorInj (Con_Kind src) (Error_Term src) # 

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 #