Quantified equality constraints are not used for rewriting
If I say
type family F a b where F [_] b = b f :: forall a b. (a ~ [b]) => F a b -> b f x = x
GHC smiles upon me: the equality constraint rewrites
[b], and then
F [b] b can reduce to
b, and all is well.
But if I say
type family F a b where F [_] b = b class Truth instance Truth f :: forall a b. (Truth => a ~ [b]) => F a b -> b f x = x
I get an error, saying
F a b does not match
b. This is because the equality, hidden behind
Truth, is not used for rewriting, and thus GHC cannot figure out that
F a b can reduce.
I don't see an easy solution here.
This isn't just me grousing: a problem on !4149 (closed) could be worked around if GHC used such equalities for rewriting. And so if we can solve this problem, we can solve the other one. My expectation is that we won't solve this one, though.