Skip to content

Strengthen decomposition for newtypes

This ticket tracks GHC proposal #549 about strengthing decomposition for newtypes.

One additinoal thought. Suppose we have

newtype N a b = MkN (a, F b)

so that N's roles are representational (for a) and nominal (for b)

We can't decompose [W] (N s1 s2) ~R (N t1 t2) to [W] s1 ~R t1 and [W] s2 ~N t2, at least not without losing completeness. We need all args to be representational.

But what about

      [W] (N s1 ty) ~R (N t1 ty)

where the second argument is the same (eqType). Then we can decompose! Maybe that's a special case worth spotting.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information