kind-apply-0.2.0.0: Utilities to work with lists of types

Safe HaskellSafe
LanguageHaskell2010

Data.PolyKinded.Atom

Documentation

data TyVar d k where Source #

Constructors

VZ :: TyVar (x -> xs) x 
VS :: TyVar xs k -> TyVar (x -> xs) k 

type V0 = Var VZ Source #

type V1 = Var (VS VZ) Source #

type V2 = Var (VS (VS VZ)) Source #

type V3 = Var (VS (VS (VS VZ))) Source #

type V4 = Var (VS (VS (VS (VS VZ)))) Source #

type V5 = Var (VS (VS (VS (VS (VS VZ))))) Source #

type V6 = Var (VS (VS (VS (VS (VS (VS VZ)))))) Source #

type V7 = Var (VS (VS (VS (VS (VS (VS (VS VZ))))))) Source #

type V8 = Var (VS (VS (VS (VS (VS (VS (VS (VS VZ)))))))) Source #

type V9 = Var (VS (VS (VS (VS (VS (VS (VS (VS (VS VZ))))))))) Source #

data Atom d k where Source #

Constructors

Var :: TyVar d k -> Atom d k 
Kon :: k -> Atom d k 
(:@:) :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2 
(:&:) :: Atom d Constraint -> Atom d Constraint -> Atom d Constraint infixr 5 

type (:$:) f x = Kon f :@: x Source #

type (:~:) a b = (Kon (~) :@: a) :@: b Source #

type family Ty (t :: Atom d k) (tys :: LoT d) :: k where ... Source #

Equations

Ty (Var VZ) (t :&&: ts) = t 
Ty (Var (VS v)) (t :&&: ts) = Ty (Var v) ts 
Ty (Kon t) tys = t 
Ty (f :@: x) tys = Ty f tys (Ty x tys) 
Ty (c :&: d) tys = (Ty c tys, Ty d tys) 

type family Satisfies (cs :: [Atom d Constraint]) (tys :: LoT d) :: Constraint where ... Source #

Equations

Satisfies '[] tys = () 
Satisfies (c ': cs) tys = (Ty c tys, Satisfies cs tys)