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

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

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)

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)