Incompleteness of solving: D/N cannot rewrite D/R
If we try
data T a type role T nominal type family F a g :: forall b a. (F a ~ T a, Coercible (F a) (T b)) => () g = () f :: forall a. (F a ~ T a) => () f = g @a
This fails because GHC cannot figure out how to instantiate the
a in the type of
b gets instantiated to
[G] F a ~N T a [WD] F alpha ~N T alpha [WD] F alpha ~R T a
The Wanteds aren't of use, so let's just look at Deriveds:
[G] F a ~N T a [D] F alpha ~N T alpha [D] F alpha ~R T a
We would like to use the first Derived to rewrite the second. We would then have
T alpha ~R T a, which can decompose to
alpha ~N a (given the nominal annotation on
T). We set
alpha := a and off we go.
The problem is that a Derived/Nominal equality will not rewrite a Derived/Representational one. See Definition [Can-rewrite relation] in GHC.Tc.Solver.Monad, in particular R2, which would be violated if D/N could rewrite D/R.
We thus accept this bug as an infelicity, not knowing how to do better for now.