Re: Soundness of forall mixed with Coercible

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

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