Hi Tom,

You may be interested in a ticket where a similar issue was discussed
before: https://gitlab.haskell.org/ghc/ghc/-/issues/20048

Given `forall a . Coercible (f a) (g a)` it seems intuitively obvious
that it should be sound to derive `Coercible f g`, but Core's typing
rules don't currently allow it. Since Core is proof irrelevant it is
probably safe just to add it, but actually proving soundness would take
a bit of work.

That said, you are asking about the subtly different

     Coercible (forall a . f a) (forall a . g a)

which is derivable from `Coercible f g`, but in fact I think is also
derivable from `forall a. Coercible (f a) (g a)` in today's Core type
system. The difficulty seems to be that GHC's constraint solver for
equality/Coercible constraints is incomplete in the presence of
quantified constraints. So unsafeCoerce seems defensible in this case.

Cheers,

Adam


On 11/12/2025 17: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))

--
Adam Gundry, Haskell Consultant
Well-Typed LLP, https://www.well-typed.com/

Registered in England & Wales, OC335890
27 Old Gloucester Street, London WC1N 3AX, England
_______________________________________________
Haskell-Cafe mailing list -- haskell-cafe@haskell.org
To (un)subscribe, modify options or view archives go to:
Only members subscribed via the mailman list are allowed to post.