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