[Haskell-cafe] Re: Soundness of forall mixed with Coercible

Well, the newtype Forall is about as useful as the forall quantifier. For example, `forall a. a -> a -> a` is isomorphic to `Forall T`, where `newtype T a = MkT (a -> a -> a)`. So why have `Forall` if we have `forall`? Well, I can't abstract over the body of `forall`, so the best I can do is use a one-parameter type variable (say `f`) and use `Forall f` instead. 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`. But the actual use case I have is in my effect system Bluefin, where I want to provide combinators that can be used to build new effects with zero additional overhead (which is why I need the Coercible instance I was asking about): https://github.com/tomjaguarpaw/bluefin/commit/87ab865f1a7c246374df2d381d26a... Tom On Fri, Dec 12, 2025 at 04:50:41PM +0200, Georgi Lyubenov wrote:

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