## GHC's failure to rewrite in coercions & kinds leads to spurious occurs-check failure

Consider this mess:

```
{-# LANGUAGE ExplicitForAll, PolyKinds, DataKinds, TypeFamilies,
StandaloneKindSignatures, AllowAmbiguousTypes, GADTs,
TypeOperators #-}
module Bug where
import Data.Kind ( Type )
import Data.Type.Equality ( type (~~) )
import Data.Proxy ( Proxy )
type Const :: () -> k1 -> k2 -> k1
type family Const u x y where
Const '() x y = x
type Equals :: k1 -> k2 -> Type
type family Equals a b where
Equals a a = Char
Equals a b = Bool
type IsUnit :: () -> Type
data IsUnit u where
ItIs :: IsUnit '()
f :: forall (u :: ()) (a :: Type) (b :: Const u Type a). (a ~~ b)
=> IsUnit u -> a -> Proxy b -> Equals a b
f ItIs _ _ = 'x'
g = f ItIs
```

GHC fails (in the RHS of `g`

) with an occurs-check, but it should succeed.

The problem is that we end up with

`[W] (alpha :: Type) ~# (beta :: Const upsilon Type alpha)`

where we have already unified `upsilon := '()`

.

But GHC refuses to rewrite in kinds, so the `Const`

never reduces, and we reject the program. Note that a solution exists, with `alpha := Any @Type`

and `beta := Any @Type |> sym (AxConst Type (Any @Type))`

.

Proposed solution:

The wanted above actually gets simplified to become

```
[W] co :: Const '() Type alpha ~# Type
[W] w2 :: (alpha :: Type) ~# ((beta |> co) :: Type)
```

The `co`

is easily solved. Then, when we get to `w2`

, we are in Wrinkle (3) of Note [Equalities with incompatible kinds]. Happily, we should be able to detect that `alpha`

is free in `co`

and reorient, giving

`[W] w3 :: (beta :: Const '() Type alpha) ~# (alpha |> sym co :: Const '() Type alpha)`

which can be solved by unifying `beta := alpha |> sym co`

. `alpha`

will then remain unconstrained and will be zonked to `Any`

.

The key new part is looking at the coercion when deciding whether to reorient.