[Haskell-cafe] Soundness of forall mixed with Coercible

11 Dec 2025

      Is it sound to define

    forallCoercible ::
      forall f g.
      (forall a. Coercible (f a) (g a)) =>
      Coercion (Forall f) (Forall g)
    forallCoercible =
      unsafeCoerce (Coercion @(f Any) @(g Any))

I'm having trouble coming up with a reason why it is not, but my
intuition for these things is not very good.  Thanks,

Tom

[Haskell-cafe] Soundness of forall mixed with Coercible

Tom Ellis