GitLab

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