singletons-1.0: 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 ~ KProxy) => PEq kproxy Source

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

Associated Types

type x :== y :: Bool Source

type x :/= y :: Bool Source

Instances

PEq Bool (KProxy Bool) 
PEq Ordering (KProxy Ordering) 
PEq * (KProxy *) 
PEq Nat (KProxy Nat) 
PEq Symbol (KProxy Symbol) 
PEq () (KProxy ()) 
PEq [k] (KProxy [k]) 
PEq (Maybe k) (KProxy (Maybe k)) 
PEq (Either k k) (KProxy (Either k k)) 
PEq ((,) k k) (KProxy ((,) k k)) 
PEq ((,,) k k k) (KProxy ((,,) k k k)) 
PEq ((,,,) k k k k) (KProxy ((,,,) k k k k)) 
PEq ((,,,,) k k k k k) (KProxy ((,,,,) k k k k k)) 
PEq ((,,,,,) k k k k k k) (KProxy ((,,,,,) k k k k k k)) 
PEq ((,,,,,,) k k k k k k k) (KProxy ((,,,,,,) k k k k k k k)) 

class (kparam ~ KProxy) => SEq kparam 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) Source

Boolean equality on singletons

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

Boolean disequality on singletons

Instances

SEq Bool (KProxy Bool) 
SEq Ordering (KProxy Ordering) 
SEq * (KProxy *) 
SEq Nat (KProxy Nat) 
SEq Symbol (KProxy Symbol) 
SEq () (KProxy ()) 
SEq a0 (KProxy a0) => SEq [a] (KProxy [a]) 
SEq a0 (KProxy a0) => SEq (Maybe a) (KProxy (Maybe a)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0)) => SEq (Either a b) (KProxy (Either a b)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0)) => SEq ((,) a b) (KProxy ((,) a b)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0)) => SEq ((,,) a b c) (KProxy ((,,) a b c)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0)) => SEq ((,,,) a b c d) (KProxy ((,,,) a b c d)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0), SEq e0 (KProxy e0)) => SEq ((,,,,) a b c d e) (KProxy ((,,,,) a b c d e)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0), SEq e0 (KProxy e0), SEq f0 (KProxy f0)) => SEq ((,,,,,) a b c d e f) (KProxy ((,,,,,) a b c d e f)) 
(SEq a0 (KProxy a0), SEq b0 (KProxy b0), SEq c0 (KProxy c0), SEq d0 (KProxy d0), SEq e0 (KProxy e0), SEq f0 (KProxy f0), SEq g0 (KProxy g0)) => SEq ((,,,,,,) a b c d e f g) (KProxy ((,,,,,,) a b c d e f g)) 

data (:==$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Bool -> *) -> *) ((:==$) k) 
type Apply (TyFun k Bool -> *) k ((:==$) k) l0 = (:==$$) k l0 

data l :==$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:==$$) k) 
type Apply Bool k ((:==$$) k l1) l0 = (:==$$$) k l1 l0 

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

data (:/=$) l Source

Instances

SuppressUnusedWarnings (TyFun k (TyFun k Bool -> *) -> *) ((:/=$) k) 
type Apply (TyFun k Bool -> *) k ((:/=$) k) l0 = (:/=$$) k l0 

data l :/=$$ l Source

Instances

SuppressUnusedWarnings (k -> TyFun k Bool -> *) ((:/=$$) k) 
type Apply Bool k ((:/=$$) k l1) l0 = (:/=$$$) k l1 l0 

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