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