## First-class apartness checking in type families

I feel like GHC could keep track of apartness a bit more carefully. Consider for instance:

```
type family FKind (k :: Type) :: Type where
FKind Bool = ()
FKind k = k
type family F (x :: k) :: FKind k where
F @Bool _ = '()
F @k a = a
```

In the second equation of `F`

, we have learned that `k`

is apart from `Bool`

. If this information was propagated to the type family application `FKind k`

, GHC would be able to deduce that `FKind k ~ k`

and thus typecheck this program. Currently this doesn't happen, so instead we get:

```
* Occurs check: cannot construct the infinite kind: k ~ FKind k
The type variable `k' is ambiguous
```

This is because GHC does not make use of the apartness information it has learned, and thus can't reduce the type family application `FKind k`

.

I think mechanisms for making GHC aware of apartness would be very useful, especially if they can be put in the hands of the programmer, e.g. if there was a magic built-in apartness constraint `/~`

(like `~`

), together with a data-**kind** witnessing apartness (like `:~:`

but at the type-level):

```
data (:/~:) a b where
Apart :: a /~ b => (:/~:) a b
```

This would need to be built-in (otherwise we run into the problem of unpromotable constraints).

Then one would hope GHC would be able to typecheck:

```
type family SepBool (k :: Type) :: Maybe (Bool :/~: k) where
SepBool Bool = Nothing
SepBool k = Just Apart
type family G (x :: k) (sep :: Bool :/~: k) :: FKind k where
G x Apart = x
```

The first example illustrates the introduction rule: it only type-checks because GHC can check that indeed `k`

and `Bool`

are apart in the second equation.

The second example illustrates the elimination rule: matching on `Apart`

introduces an apartness proof to the type-checker. In this case this apartness proof is then used in reducing the type family application `FKind k`

.