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