I'm curious what it'd take to add a qReifyCoercible method; does the renamer know anything about Coercible?
No, it doesn't, but the Q monad is actually a wrapper around TcM, the type-checker monad. I don't think it would be all that hard to do this. Could be a suitable project for someone new to GHC hacking...