Re: Soundness of forall mixed with Coercible

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

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