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

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

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

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

In that case the `a` is still not really "present", i.e. the only inhabitants of `Forall Predicate` would be `MkForall (Predicate \_ -> True)` and `MkForall (Predicate \_ -> False)`, unless, again, I'm totally missing something here. It's true that here if you instead have Predicate Void you gain an additional value `Predicate \case`, but it still stands that you can't actually "use anything about the a", so I'm still curious regarding what the use case here is. On 12/12/25 16:38, Zemyla wrote:

Wait, no, I forgot about values that aren't covariant. Forall $ Predicate $ const True is a valid value.

On Fri, Dec 12, 2025, 08:34 Georgi Lyubenov wrote:

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 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 https://www.google.com/maps/search/27+Old+Gloucester+Street,+London+WC1N+3AX,+England?entry=gmail&source=g _______________________________________________ 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.

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

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

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

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