Skip to content

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
...
Edited by mniip
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information