Re: Soundness of forall mixed with Coercible

Yeah, I think this is my intuition which I was trying to get at with my 
"isn't this Void" comment - it seems to me that in all cases where you 
have a `forall a. f a` that would be the same thing as having an `f 
Void`, i.e. the `a` is never relevant or alternatively the f a inside a 
Forall will never actually contain an a.

Is there still something else that I'm missing?

What's the concrete use case for Forall?

On 12/12/25 16:03, Zemyla wrote:
> Wouldn't the only inhabited value of Forall [] be []?
>
> On Fri, Dec 12, 2025, 02:18 Adam Gundry <[email protected]> wrote:
>
>     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 -- [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.

_______________________________________________
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.