Type equality in GADT/TypeFamily context

This is indeed difficult, unfortunately. It’s been discussed by the GHC developers a few times over the years, see in particular this ticket and those linking to it:

GitLab

First-class apartness checking in type families (#17585) · Issues · Glasgow...

I feel like GHC could keep track of apartness a bit more carefully. Consider for instance: