Data.Constraint.Trivial

Trivial classes

class Unconstrained0

A constraint that is always/unconditionally fulfilled. This behaves the same way as (), when appearing in a constraint-tuple, i.e. it does not change anything about the constraints. It is thus the identity of the (,) monoid in the constraint kind.

Instances

Unconstrained0

Defined in Data.Constraint.Trivial

class Disallowed "Impossible0" => Impossible0

A constraint that never is fulfilled, in other words it is guaranteed that something whose context contains this constraint will never actually be invoked in a program.

class Unconstrained t

A parametric non-constraint. This can be used, for instance, when you have an existential that contains endo-functions of any type of some specified constraint.

data GenEndo c where
  GenEndo :: c a => (a -> a) -> GenEndo c

Then, you can have values like GenEndo abs :: GenEndo Num. It is also possible to have GenEndo id :: GenEndo Num, but here the num constraint is not actually required. So what to use as the c argument? It should be a constraint on a type which does not actually constrain the type.

idEndo :: GenEndo Unconstrained
idEndo = GenEndo id

Instances

Unconstrained (t :: k)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible" => Impossible t

This constraint can never be fulfilled. One application in which this can be useful is as a default for a class-associated constraint; this basically disables any method with that constraint: so it can safely be left undefined. We provide the nope method as a special form of undefined, which actually guarantees it is safe through the type system. For instance, the old monad class with its controversial fail method could be changed to

class Applicative m => Monad m where
  (return,(>>=)) :: ...
  type FailableResult m :: * -> Constraint
  type FailableResult m = Impossible  -- fail disabled by default
  fail :: FailableResult m a => String -> m a
  fail = nope

This would turn any use of fail in a “pure” monad (which does not actually define fail) into a type error. Meanwhile, “safe” uses of fail, such as in the IO monad, could be kept as-is, by making the instance

instance Monad IO where
  (return,(>>=)) = ...
  type FailableResult m = Unconstrained
  fail = throwErrow

Other instances could support the fail method only selectively for particular result types, again by picking a suitable FailableResult constraint (e.g. Monoid).

class Unconstrained2 t s

Like Unconstrained, but with kind signature k -> k -> Constraint (two unconstrained types).

Instances

Unconstrained2 (t :: k1) (s :: k2)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible2" => Impossible2 t s

class Unconstrained3 t s r

Instances

Unconstrained3 (t :: k1) (s :: k2) (r :: k3)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible3" => Impossible3 t s r

class Unconstrained4 t s r q

Instances

Unconstrained4 (t :: k1) (s :: k2) (r :: k3) (q :: k4)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible4" => Impossible4 t s r q

class Unconstrained5 t s r q p

Instances

Unconstrained5 (t :: k1) (s :: k2) (r :: k3) (q :: k4) (p :: k5)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible5" => Impossible5 t s r q p

class Unconstrained6 t s r q p o

Instances

Unconstrained6 (t :: k1) (s :: k2) (r :: k3) (q :: k4) (p :: k5) (o :: k6)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible6" => Impossible6 t s r q p o

class Unconstrained7 t s r q p o n

Instances

Unconstrained7 (t :: k1) (s :: k2) (r :: k3) (q :: k4) (p :: k5) (o :: k6) (n :: k7)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible7" => Impossible7 t s r q p o n

class Unconstrained8 t s r q p o n m

Instances

Unconstrained8 (t :: k1) (s :: k2) (r :: k3) (q :: k4) (p :: k5) (o :: k6) (n :: k7) (m :: k8)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible8" => Impossible8 t s r q p o n m

class Unconstrained9 t s r q p o n m l

Instances

Unconstrained9 (t :: k1) (s :: k2) (r :: k3) (q :: k4) (p :: k5) (o :: k6) (n :: k7) (m :: k8) (l :: k9)

Defined in Data.Constraint.Trivial

class Disallowed "Impossible9" => Impossible9 t s r q p o n m l

Utility

class (Bottom, TypeError (('Text "All instances of " :<>: 'Text t) :<>: 'Text " are disallowed.")) => Disallowed t

nope :: forall rep (a :: TYPE rep). Bottom => a

A term-level witness that the context contains a Disallowed constraint, i.e. one of the Impossible0, Impossible ... constraints. In such a context, because you are guaranteed that it can under no circumstances actually be invoked, you are allowed to to anything whatsoever, even create a value of an uninhabited unlifted type.