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 a to [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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information