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
_______________________________________________
Haskell-Cafe mailing list -- [email protected]
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.