Soundness of forall mixed with Coercible

Tom Ellis <[email protected]> Thu, 11 Dec 2025 17:47:25 +0000

Newsgroups	gmane.comp.lang.haskell.cafe
Message-ID	<aTsDrTqGN99agKpE@cloudinit-builder>

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