Data.Ten.Entails

A typeclass of GADT-like types whose existence implies an instance.

Documentation

class Entails k c where

A typeclass of GADT-like types whose existence implies an instance.

For a trivial example, the existence of Int :~: b implies Show b, since we can discover that b is Int and use the Show Int instance.

Methods

entailment :: k a -> Dict1 c a

Instances

(forall (a :: k). c a) => Entails (Proxy :: k -> Type) (c :: k -> Constraint)

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). Proxy a -> Dict1 c a

(forall (a :: k). c a) => Entails (TypeRep :: k -> Type) (c :: k -> Constraint)

Non-GADTy types don't entail anything except parametric instances.

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). TypeRep a -> Dict1 c a

Entails (Dict1 c :: k -> Type) (c :: k -> Constraint)

Dict1s entail their own type parameter.

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). Dict1 c a -> Dict1 c a

c a => Entails ((:~:) a :: k -> Type) (c :: k -> Constraint)

Equality to a particular type entails any instance that type has.

Defined in Data.Ten.Entails

Methods

entailment :: forall (a0 :: k0). (a :~: a0) -> Dict1 c a0

(Constrained10 c f, Applicative10 f) => Entails (Field10 f :: k -> Type) (c :: k -> Constraint)

Defined in Data.Ten.Field

Methods

entailment :: forall (a :: k0). Field10 f a -> Dict1 c a

data Dict1 (c :: k -> Constraint) a

A dictionary for the given arity-1 constraint constructor ("a class").

Constructors

c a => Dict1

Instances

Entails (Dict1 c :: k -> Type) (c :: k -> Constraint)

Dict1s entail their own type parameter.

Defined in Data.Ten.Entails

Methods

entailment :: forall (a :: k0). Dict1 c a -> Dict1 c a

class c (d a) => (c :!: d) a

A utility "typeclass newtype" that's convenient with Entails.

If you want to use entailment to get an instance of the form c (d a), use entailment @(c :!: d). Really I wanted to use the name (:.:), but it's taken, so I just replaced the period with something else that involves a dot near the typographic base line.

Instances

c (d a) => ((c :: k1 -> Constraint) :!: (d :: k2 -> k1)) (a :: k2)

Defined in Data.Ten.Entails

withEntailment :: forall c k a r. Entails k c => k a -> (c a => r) -> r

Bring an instance into scope using an Entails instance.

    ( (k :: Int :~: b) (x :: b) -> withEntailment @Show k (show x)) Refl 2

byEntailment :: forall c k a r. Entails k c => (c a => r) -> k a -> r

flip withEntailment.

This is useful for "consuming" an index off the front of a function type and turning it into an instance, e.g. in the context of an imap10 call.