Re: Soundness of forall mixed with Coercible

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.