[Haskell-cafe] Re: Soundness of forall mixed with Coercible

On Fri, Dec 12, 2025 at 11:46:53PM +0000, Tom Ellis wrote:

Here's an example of where `Forall f` is very different from `Void`. `Forall L` is the type of lists of elements that can be Ordered and Shown, where `newtype L a where MkL :: (Show a, Ord a) => [a] -> L a`.

Sorry, this should be forall r. (forall a. L a -> r) -> r (i.e. encoding an existential with universal quantification) which you can encode as `Forall T2` where newtype T1 r a = MkT1 (L a -> r) newtype T2 r = MkT2 (Forall (T1 r) -> r) Tom