# Occurs-check-y Givens rewrite once, but not twice

GHC remarkably accepts this program:

```
type family UnMaybe a where
UnMaybe (Maybe b) = b
class C c where
meth :: c
instance C (Maybe d) where
meth = Nothing
f :: (e ~ Maybe (UnMaybe e)) => e
f = meth
```

This is remarkable because satisfying the `C e`

constraint arising from the use of `meth`

requires using the `e ~ Maybe (UnMaybe e)`

given, despite the fact that it has an occurs-check failure. That is, GHC must rewrite `e`

to `Maybe (UnMaybe e)`

to solve the class constraint, yet not fall into a look trying to expand `e`

further. This works due to the way GHC currently uses flattening-skolems to deal with type family applications. (The program above does not work on the current tip of !4149 (closed), which avoids this flattening mechanism.)

However, GHC rejects this program:

```
type family G a b where
G (Maybe c) d = d
h :: (e ~ Maybe (G e f)) => e -> f
h (Just x) = x
```

Here, `h`

has a similar given with an occurs-check failure. In contrast to the first example, though, we need to use the equation *twice* in order to accept this program. Specifically, we have

```
[G] e ~ Maybe (G e f)
[W] e ~ Maybe f
```

Using the Given for rewriting once gives us

`[W] Maybe (G e f) ~ Maybe f`

which decomposes to

`[W] G e f ~ f`

But now, we must use the given *again* to get

`[W] G (Maybe (G e f)) f ~ f`

so that can reduce to

`[W] f ~ f`

and be solved.

I think this will be hard to achieve in practice (rewriting twice). Might we need even more rewrites in pathological scenarios? I don't know.

The purpose of this ticket is more to record the incompleteness than to actively agitate for a solution. This did not arise in a real application and would likely be hard to fix.