Wouldn't the only inhabited value of Forall [] be []?
On Fri, Dec 12, 2025, 02:18 Adam Gundry
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 -- haskell-cafe@haskell.org To (un)subscribe, modify options or view archives go to: Only members subscribed via the mailman list are allowed to post.