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 g
. (The b
gets instantiated to f
's a
.)
We have
[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.