... | ... | @@ -22,6 +22,10 @@ lower :: (f a :~: f b) -> a :~: b |
|
|
|
|
|
class EqualityT f where
|
|
|
equalsT :: f a -> f b -> Maybe (a :~: b)
|
|
|
|
|
|
type family a == b where
|
|
|
a == a = True
|
|
|
a == b = False
|
|
|
```
|
|
|
|
|
|
## Module `Data.Type.Coercion`
|
... | ... | @@ -124,11 +128,3 @@ These are in no particular order, but they are numbered for easy reference. |
|
|
|
|
|
>
|
|
|
> I've tested this function in a real setting, and it (that is, type inference for it) works great. |
|
|
|
|
|
1. I propose the following, further addition to `Data.Type.Equality`:
|
|
|
|
|
|
```wiki
|
|
|
type family a == b where
|
|
|
a == a = True
|
|
|
a == b = False
|
|
|
``` |
|
|
\ No newline at end of file |