More liberally kinded coercions for newtypes
Consider the infinite data family (possible thanks to #12369 (closed)):
data family I :: k -> k newtype instance I a = I0 (a) newtype instance I a x = I1 (a x) newtype instance I a x y = I2 (a x y) newtype instance I a x y z = I3 (a x y z) ...
We end up with a family of eta-contracted coercions:
forall (a :: *). a ~R I a forall (a :: k -> *). a ~R I a forall (a :: k -> l -> *). a ~R I a forall (a :: k -> l -> m -> *). a ~R I a ...
What if we could somehow indicate that we desire a polykinded newtype (so to speak) with a coercion
forall (a :: k). a ~R I a
Maybe even do so by default:
newtype I a = I0 a would create such a polykinded coercion. Though the
I0 data constructor and pattern would still only use the *-kinded restriction of it.
We could then recover other constructors with:
i1 :: a x -> I a x i1 = coerce ...