[Haskell-cafe] Does the constraints library give (a :- b) -> Dict (a |- b)?

[Tom Ellis]

On Thu, Nov 30, 2023 at 01:37:47PM +0000, Tom Ellis wrote:
> The constraints library [1] has
> 
>     implied :: forall a b. (a => b) => a :- b
> 
> from which I can obtain
> 
>     implied' :: Dict (a |- b) -> a :- b
>     implied' Dict = implied
> 
> but can I get the converse of this, that is
> 
>     coimplied :: (a :- b) -> Dict (a |- b)
>     coimplied = error "Can it be done?"
> 
> I don't see how.  The library itself only mentions "|-" in its
> definition.  Would this combinator violate some guarantee that's
> essential for the safe use of type classes?

It seems this question has been asked at least a couple of times of
the GHC bug tracker, firstly in

https://gitlab.haskell.org/ghc/ghc/-/issues/14822

where it was deemed unsound (I don't understand why) and again in

https://gitlab.haskell.org/ghc/ghc/-/issues/14937

where it remains open without having explicitly been deemed unsound.

Tom