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