singletons-2.2: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Prelude.Eq

Description

Defines the SEq singleton version of the Eq type class.

Synopsis

Documentation

class kproxy ~ Proxy => PEq kproxy Source #

The promoted analogue of Eq. If you supply no definition for '(:==)', then it defaults to a use of '(==)', from Data.Type.Equality.

Associated Types

type (x :: a) :== (y :: a) :: Bool infix 4 Source #

type (x :: a) :/= (y :: a) :: Bool infix 4 Source #

Instances

PEq Bool (Proxy * Bool) Source # 

Associated Types

type ((Proxy * Bool) :== (x :: Proxy * Bool)) (y :: Proxy * Bool) :: Bool Source #

type ((Proxy * Bool) :/= (x :: Proxy * Bool)) (y :: Proxy * Bool) :: Bool Source #

PEq Ordering (Proxy * Ordering) Source # 

Associated Types

type ((Proxy * Ordering) :== (x :: Proxy * Ordering)) (y :: Proxy * Ordering) :: Bool Source #

type ((Proxy * Ordering) :/= (x :: Proxy * Ordering)) (y :: Proxy * Ordering) :: Bool Source #

PEq () (Proxy * ()) Source # 

Associated Types

type ((Proxy * ()) :== (x :: Proxy * ())) (y :: Proxy * ()) :: Bool Source #

type ((Proxy * ()) :/= (x :: Proxy * ())) (y :: Proxy * ()) :: Bool Source #

PEq [k0] (Proxy * [k0]) Source # 

Associated Types

type ((Proxy * [k0]) :== (x :: Proxy * [k0])) (y :: Proxy * [k0]) :: Bool Source #

type ((Proxy * [k0]) :/= (x :: Proxy * [k0])) (y :: Proxy * [k0]) :: Bool Source #

PEq (Maybe k0) (Proxy * (Maybe k0)) Source # 

Associated Types

type ((Proxy * (Maybe k0)) :== (x :: Proxy * (Maybe k0))) (y :: Proxy * (Maybe k0)) :: Bool Source #

type ((Proxy * (Maybe k0)) :/= (x :: Proxy * (Maybe k0))) (y :: Proxy * (Maybe k0)) :: Bool Source #

PEq (NonEmpty k0) (Proxy * (NonEmpty k0)) Source # 

Associated Types

type ((Proxy * (NonEmpty k0)) :== (x :: Proxy * (NonEmpty k0))) (y :: Proxy * (NonEmpty k0)) :: Bool Source #

type ((Proxy * (NonEmpty k0)) :/= (x :: Proxy * (NonEmpty k0))) (y :: Proxy * (NonEmpty k0)) :: Bool Source #

PEq (Either k0 k1) (Proxy * (Either k0 k1)) Source # 

Associated Types

type ((Proxy * (Either k0 k1)) :== (x :: Proxy * (Either k0 k1))) (y :: Proxy * (Either k0 k1)) :: Bool Source #

type ((Proxy * (Either k0 k1)) :/= (x :: Proxy * (Either k0 k1))) (y :: Proxy * (Either k0 k1)) :: Bool Source #

PEq (k0, k1) (Proxy * (k0, k1)) Source # 

Associated Types

type ((Proxy * (k0, k1)) :== (x :: Proxy * (k0, k1))) (y :: Proxy * (k0, k1)) :: Bool Source #

type ((Proxy * (k0, k1)) :/= (x :: Proxy * (k0, k1))) (y :: Proxy * (k0, k1)) :: Bool Source #

PEq (k0, k1, k2) (Proxy * (k0, k1, k2)) Source # 

Associated Types

type ((Proxy * (k0, k1, k2)) :== (x :: Proxy * (k0, k1, k2))) (y :: Proxy * (k0, k1, k2)) :: Bool Source #

type ((Proxy * (k0, k1, k2)) :/= (x :: Proxy * (k0, k1, k2))) (y :: Proxy * (k0, k1, k2)) :: Bool Source #

PEq (k0, k1, k2, k3) (Proxy * (k0, k1, k2, k3)) Source # 

Associated Types

type ((Proxy * (k0, k1, k2, k3)) :== (x :: Proxy * (k0, k1, k2, k3))) (y :: Proxy * (k0, k1, k2, k3)) :: Bool Source #

type ((Proxy * (k0, k1, k2, k3)) :/= (x :: Proxy * (k0, k1, k2, k3))) (y :: Proxy * (k0, k1, k2, k3)) :: Bool Source #

PEq (k0, k1, k2, k3, k4) (Proxy * (k0, k1, k2, k3, k4)) Source # 

Associated Types

type ((Proxy * (k0, k1, k2, k3, k4)) :== (x :: Proxy * (k0, k1, k2, k3, k4))) (y :: Proxy * (k0, k1, k2, k3, k4)) :: Bool Source #

type ((Proxy * (k0, k1, k2, k3, k4)) :/= (x :: Proxy * (k0, k1, k2, k3, k4))) (y :: Proxy * (k0, k1, k2, k3, k4)) :: Bool Source #

PEq (k0, k1, k2, k3, k4, k5) (Proxy * (k0, k1, k2, k3, k4, k5)) Source # 

Associated Types

type ((Proxy * (k0, k1, k2, k3, k4, k5)) :== (x :: Proxy * (k0, k1, k2, k3, k4, k5))) (y :: Proxy * (k0, k1, k2, k3, k4, k5)) :: Bool Source #

type ((Proxy * (k0, k1, k2, k3, k4, k5)) :/= (x :: Proxy * (k0, k1, k2, k3, k4, k5))) (y :: Proxy * (k0, k1, k2, k3, k4, k5)) :: Bool Source #

PEq (k0, k1, k2, k3, k4, k5, k6) (Proxy * (k0, k1, k2, k3, k4, k5, k6)) Source # 

Associated Types

type ((Proxy * (k0, k1, k2, k3, k4, k5, k6)) :== (x :: Proxy * (k0, k1, k2, k3, k4, k5, k6))) (y :: Proxy * (k0, k1, k2, k3, k4, k5, k6)) :: Bool Source #

type ((Proxy * (k0, k1, k2, k3, k4, k5, k6)) :/= (x :: Proxy * (k0, k1, k2, k3, k4, k5, k6))) (y :: Proxy * (k0, k1, k2, k3, k4, k5, k6)) :: Bool Source #

class SEq k where Source #

The singleton analogue of Eq. Unlike the definition for Eq, it is required that instances define a body for '(%:==)'. You may also supply a body for '(%:/=)'.

Minimal complete definition

(%:==)

Methods

(%:==) :: forall a b. Sing a -> Sing b -> Sing (a :== b) infix 4 Source #

Boolean equality on singletons

(%:/=) :: forall a b. Sing a -> Sing b -> Sing (a :/= b) infix 4 Source #

Boolean disequality on singletons

(%:/=) :: forall a b. (a :/= b) ~ Not (a :== b) => Sing a -> Sing b -> Sing (a :/= b) infix 4 Source #

Boolean disequality on singletons

Instances

SEq Bool Source # 

Methods

(%:==) :: Sing Bool a -> Sing Bool b -> Sing Bool ((Bool :== a) b) Source #

(%:/=) :: Sing Bool a -> Sing Bool b -> Sing Bool ((Bool :/= a) b) Source #

SEq Ordering Source # 
SEq () Source # 

Methods

(%:==) :: Sing () a -> Sing () b -> Sing Bool ((() :== a) b) Source #

(%:/=) :: Sing () a -> Sing () b -> Sing Bool ((() :/= a) b) Source #

SEq a0 => SEq [a0] Source # 

Methods

(%:==) :: Sing [a0] a -> Sing [a0] b -> Sing Bool (([a0] :== a) b) Source #

(%:/=) :: Sing [a0] a -> Sing [a0] b -> Sing Bool (([a0] :/= a) b) Source #

SEq a0 => SEq (Maybe a0) Source # 

Methods

(%:==) :: Sing (Maybe a0) a -> Sing (Maybe a0) b -> Sing Bool ((Maybe a0 :== a) b) Source #

(%:/=) :: Sing (Maybe a0) a -> Sing (Maybe a0) b -> Sing Bool ((Maybe a0 :/= a) b) Source #

SEq a0 => SEq (NonEmpty a0) Source # 

Methods

(%:==) :: Sing (NonEmpty a0) a -> Sing (NonEmpty a0) b -> Sing Bool ((NonEmpty a0 :== a) b) Source #

(%:/=) :: Sing (NonEmpty a0) a -> Sing (NonEmpty a0) b -> Sing Bool ((NonEmpty a0 :/= a) b) Source #

(SEq a0, SEq b0) => SEq (Either a0 b0) Source # 

Methods

(%:==) :: Sing (Either a0 b0) a -> Sing (Either a0 b0) b -> Sing Bool ((Either a0 b0 :== a) b) Source #

(%:/=) :: Sing (Either a0 b0) a -> Sing (Either a0 b0) b -> Sing Bool ((Either a0 b0 :/= a) b) Source #

(SEq a0, SEq b0) => SEq (a0, b0) Source # 

Methods

(%:==) :: Sing (a0, b0) a -> Sing (a0, b0) b -> Sing Bool (((a0, b0) :== a) b) Source #

(%:/=) :: Sing (a0, b0) a -> Sing (a0, b0) b -> Sing Bool (((a0, b0) :/= a) b) Source #

(SEq a0, SEq b0, SEq c0) => SEq (a0, b0, c0) Source # 

Methods

(%:==) :: Sing (a0, b0, c0) a -> Sing (a0, b0, c0) b -> Sing Bool (((a0, b0, c0) :== a) b) Source #

(%:/=) :: Sing (a0, b0, c0) a -> Sing (a0, b0, c0) b -> Sing Bool (((a0, b0, c0) :/= a) b) Source #

(SEq a0, SEq b0, SEq c0, SEq d0) => SEq (a0, b0, c0, d0) Source # 

Methods

(%:==) :: Sing (a0, b0, c0, d0) a -> Sing (a0, b0, c0, d0) b -> Sing Bool (((a0, b0, c0, d0) :== a) b) Source #

(%:/=) :: Sing (a0, b0, c0, d0) a -> Sing (a0, b0, c0, d0) b -> Sing Bool (((a0, b0, c0, d0) :/= a) b) Source #

(SEq a0, SEq b0, SEq c0, SEq d0, SEq e0) => SEq (a0, b0, c0, d0, e0) Source # 

Methods

(%:==) :: Sing (a0, b0, c0, d0, e0) a -> Sing (a0, b0, c0, d0, e0) b -> Sing Bool (((a0, b0, c0, d0, e0) :== a) b) Source #

(%:/=) :: Sing (a0, b0, c0, d0, e0) a -> Sing (a0, b0, c0, d0, e0) b -> Sing Bool (((a0, b0, c0, d0, e0) :/= a) b) Source #

(SEq a0, SEq b0, SEq c0, SEq d0, SEq e0, SEq f0) => SEq (a0, b0, c0, d0, e0, f0) Source # 

Methods

(%:==) :: Sing (a0, b0, c0, d0, e0, f0) a -> Sing (a0, b0, c0, d0, e0, f0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0) :== a) b) Source #

(%:/=) :: Sing (a0, b0, c0, d0, e0, f0) a -> Sing (a0, b0, c0, d0, e0, f0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0) :/= a) b) Source #

(SEq a0, SEq b0, SEq c0, SEq d0, SEq e0, SEq f0, SEq g0) => SEq (a0, b0, c0, d0, e0, f0, g0) Source # 

Methods

(%:==) :: Sing (a0, b0, c0, d0, e0, f0, g0) a -> Sing (a0, b0, c0, d0, e0, f0, g0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0, g0) :== a) b) Source #

(%:/=) :: Sing (a0, b0, c0, d0, e0, f0, g0) a -> Sing (a0, b0, c0, d0, e0, f0, g0) b -> Sing Bool (((a0, b0, c0, d0, e0, f0, g0) :/= a) b) Source #

data (:==$) l Source #

Instances

SuppressUnusedWarnings (TyFun a1627662065 (TyFun a1627662065 Bool -> Type) -> *) ((:==$) a1627662065) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:==$) a1627662065) t -> () Source #

type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:==$) a1627662065) l0 Source # 
type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:==$) a1627662065) l0 = (:==$$) a1627662065 l0

data l :==$$ l Source #

Instances

SuppressUnusedWarnings (a1627662065 -> TyFun a1627662065 Bool -> *) ((:==$$) a1627662065) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:==$$) a1627662065) t -> () Source #

type Apply a1627662065 Bool ((:==$$) a1627662065 l1) l0 Source # 
type Apply a1627662065 Bool ((:==$$) a1627662065 l1) l0 = (:==$$$) a1627662065 l1 l0

type (:==$$$) t t = (:==) t t Source #

data (:/=$) l Source #

Instances

SuppressUnusedWarnings (TyFun a1627662065 (TyFun a1627662065 Bool -> Type) -> *) ((:/=$) a1627662065) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:/=$) a1627662065) t -> () Source #

type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:/=$) a1627662065) l0 Source # 
type Apply a1627662065 (TyFun a1627662065 Bool -> Type) ((:/=$) a1627662065) l0 = (:/=$$) a1627662065 l0

data l :/=$$ l Source #

Instances

SuppressUnusedWarnings (a1627662065 -> TyFun a1627662065 Bool -> *) ((:/=$$) a1627662065) Source # 

Methods

suppressUnusedWarnings :: Proxy ((:/=$$) a1627662065) t -> () Source #

type Apply a1627662065 Bool ((:/=$$) a1627662065 l1) l0 Source # 
type Apply a1627662065 Bool ((:/=$$) a1627662065 l1) l0 = (:/=$$$) a1627662065 l1 l0

type (:/=$$$) t t = (:/=) t t Source #