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