Add gcoerceWith to Data.Type.Coercion

Haskell libraries mailing list discussion: https://mail.haskell.org/pipermail/libraries/2016-July/027207.html

In Data.Type.Equality, we have both

castWith :: (a :~: b) -> a -> b

and

gcastWith :: (a :~: b) -> (a ~ b => r) -> r

But in Data.Type.Coercion we only have

coerceWith :: Coercion a b -> a -> b

It seems to me that for the sake of consistency, we should add

gcoerceWith :: Coercion a b -> (Coercible a b => r) -> r
gcoerceWith Coercion a = a

David Feuer

I've wanted this too. Patch incoming.

Trac metadata

Trac field	Value
Version	8.0.1
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	libraries/base
Test case
Differential revisions
BlockedBy
Related
Blocking
CC	core-libraries-committee@haskell.org, dfeuer
Operating system
Architecture