singletons-2.2: A framework for generating singleton types

Copyright(C) 2014 Jan Stolarek
LicenseBSD-style (see LICENSE)
MaintainerJan Stolarek (jan.stolarek@p.lodz.pl)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Promotion.Prelude.Eq

Description

Provided promoted definitions related to type-level equality.

Synopsis

Documentation

class kproxy ~ Proxy => PEq kproxy #

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 #

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

Instances

PEq Bool (Proxy * Bool) # 

Associated Types

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

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

PEq Ordering (Proxy * Ordering) # 

Associated Types

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

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

PEq () (Proxy * ()) # 

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

Associated Types

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

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

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

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 #

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 #

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

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 #

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 #

data (:==$) l #

Instances

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

Methods

suppressUnusedWarnings :: Proxy ((:==$) a6989586621679492109) t -> () #

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

data l :==$$ l #

Instances

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

Methods

suppressUnusedWarnings :: Proxy ((:==$$) a6989586621679492109) t -> () #

type Apply a6989586621679492109 Bool ((:==$$) a6989586621679492109 l0) l1 # 
type Apply a6989586621679492109 Bool ((:==$$) a6989586621679492109 l0) l1 = (:==$$$) a6989586621679492109 l0 l1

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

data (:/=$) l #

Instances

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

Methods

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

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

data l :/=$$ l #

Instances

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

Methods

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

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

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