Re: Soundness of forall mixed with Coercible

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.