GitLab

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.