Coercion application broken by newtype constructor

Summary

In core-spec there's an inference rule for applying a coercion to an argument (Co_AppCo) that amounts to the following haskell type:

coAppCo :: Coercion f g -> x :~: y -> Coercion (f x) (g y)

and indeed the type-checker is able to use this rule since the following implementation type-checks:

coAppCo Coercion Refl = Coercion

However, if we specialize the type signature by substituting f and g with uses of a newtype type constructor whose data constructor is not in scope, the implementation fails.

import Control.Monad.ST (ST)
coAppCo' :: Coercion (ST s) (ST s') -> x :~: y -> Coercion (ST s x) (ST s' y)
coAppCo' Coercion Refl = Coercion

<interactive>:12:26: error: [GHC-18872]
    • Couldn't match representation of type: ST s x
                               with that of: ST s' x
        arising from a use of ‘Coercion’
        The data constructor ‘GHC.ST.ST’ of newtype ‘ST’ is not in scope
    • In the expression: Coercion
      In an equation for ‘coAppCo'’: coAppCo' Coercion Refl = Coercion
    • Relevant bindings include
        coAppCo' :: Coercion (ST s) (ST s')
                    -> (x :~: y) -> Coercion (ST s x) (ST s' y)
          (bound at <interactive>:12:1)

Note that an implementation that simply delegates to the more general version (coAppCo' = coAppCo) type-checks just fine. Likewise if instead of ST I use something that is not a newtype, it also type-checks just fine.

Steps to reproduce

import Control.Monad.ST (ST)
import Data.Type.Coercion
import Data.Type.Equality

coAppCo' :: Coercion (ST s) (ST s') -> x :~: y -> Coercion (ST s x) (ST s' y)
coAppCo' Coercion Refl = Coercion

Expected behavior

coAppCo' should type-check

Environment

• GHC version used: 9.6.2