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.