694 B
694 B
Type Level
data Coercion (a :: k) (b :: k) where
Coercion :: forall (k :: BOX) (a :: k) (b :: k). Coercible a b => Coercion a b
coerceWith :: Coercion a b -> a -> b
Empty
data Void
absurd :: Void -> a
vacuous :: Functor f => f Void -> f a
Proxy
data Proxy (t :: k) = Proxy
Type Equality
(:~:) :: k -> k -> *
(==) :: k -> k -> Bool
sym :: a :~: b -> b :~: a
trans :: a :~: b -> b :~: c -> a :~: c
castWith :: a :~: b -> a -> b
gcastWith :: a :~: b -> ((a ~ b) => r) -> r