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/87ab865f1a7c246374df2d381d26ada96308ba0e#diff-a6f1b01c2f813ba98bbdbb57516f3268c0b122aa0548c4a4536ee40b8e2ef487R818-R834

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 <[email protected]>
> > 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 <[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))
_______________________________________________
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.