Coercible constraint solver misses one

When I say

import Data.Type.Coercion
import Data.Coerce

eta :: Coercible f g => Coercion (f a) (g a)
eta = Coercion

I get

    Could not coerce from ‘f a’ to ‘g a’
      because ‘f a’ and ‘g a’ are different types.
      arising from a use of ‘Coercion’
    from the context (Coercible f g)
      bound by the type signature for
                 eta :: Coercible f g => Coercion (f a) (g a)
      at /Users/rae/temp/Roles.hs:6:8-44
    In the expression: Coercion
    In an equation for ‘eta’: eta = Coercion

But, this coercion is easily expressible in Core. If (co :: f ~R# g) then (co <a> :: f a ~R# g a), where <a> is the notation for a reflexivity coercion for the type a. The constraint solver should be able to do this.

Trac metadata

Trac field	Value
Version	7.8.2
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture