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
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
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.