Re: Soundness of forall mixed with Coercible

This is (somewhat) tangent to your question, but what are you using 
Forall for? Forall seems like it should just be the same as Void, but 
maybe I'm totally missing something.

On 12/11/25 19:58, Tom Ellis wrote:
> Oh, I forgot to give the definition of Forall, so I may as well define
> it in its full glory, imports, extensions and all:
>
> {-# LANGUAGE QuantifiedConstraints #-}
>
> import Data.Coerce (Coercible)
> import Data.Type.Coercion (Coercion (Coercion))
> import GHC.Exts (Any)
> import Unsafe.Coerce (unsafeCoerce)
>
> newtype Forall f = MkForall (forall a. f a)
>
> forallCoercible ::
>    forall f g.
>    (forall a. Coercible (f a) (g a)) =>
>    Coercion (Forall f) (Forall g)
> forallCoercible =
>    unsafeCoerce (Coercion @(f Any) @(g Any))
> 	
> On Thu, Dec 11, 2025 at 05:47:25PM +0000, Tom Ellis wrote:
>>      forallCoercible ::
>>        forall f g.
>>        (forall a. Coercible (f a) (g a)) =>
>>        Coercion (Forall f) (Forall g)
>>      forallCoercible =
>>        unsafeCoerce (Coercion @(f Any) @(g Any))
> _______________________________________________
> 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.
_______________________________________________
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.