Coercible solver does not look through "class newtypes"

The code below makes use of the "class newtype" design pattern:

class    Show a => MyShow a
instance Show a => MyShow a

MyShow is a newtype around Show in the sense that when compiled to Core, a MyShow dictionary is literally a newtype around Show. Unfortunately, this newtype treatment does not extend to the Coercible solver, as the following example demonstrates:

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MonoLocalBinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module Bug where

import Data.Coerce

class    Show a => MyShow a
instance Show a => MyShow a

newtype T1 a = MkT1 (  Show a => a -> a -> String)
newtype T2 a = MkT2 (MyShow a => a -> a -> String)

f :: T1 a -> T2 a
f = coerce

$ /opt/ghc/8.8.1/bin/ghc Bug.hs
[1 of 1] Compiling Bug              ( Bug.hs, Bug.o )

Bug.hs:20:5: error:
    • Couldn't match representation of type ‘MyShow a’
                               with that of ‘Show a’
        arising from a use of ‘coerce’
      The data constructor ‘Bug.C:MyShow’
        of newtype ‘MyShow’ is not in scope
    • In the expression: coerce
      In an equation for ‘f’: f = coerce
    • Relevant bindings include
        f :: T1 a -> T2 a (bound at Bug.hs:20:1)
   |
20 | f = coerce
   |     ^^^^^^

Somewhat surprisingly, this does not work. Even the error message indicates that MyShow is a newtype (which is a bit odd, but whatever), but since the internal C:MyShow constructor is not exposed, the Coercible solver doesn't have enough information to proceed.

If the following change is applied to GHC, then it typechecks:

diff --git a/compiler/typecheck/FamInst.hs b/compiler/typecheck/FamInst.hs
index a339dd7b57..8640b3e3e0 100644
--- a/compiler/typecheck/FamInst.hs
+++ b/compiler/typecheck/FamInst.hs
@@ -41,7 +41,7 @@ import Name
 import Pair
 import Panic
 import VarSet
-import Bag( Bag, unionBags, unitBag )
+import Bag( Bag, emptyBag, unionBags, unitBag )
 import Control.Monad

 #include "HsVersions.h"
@@ -577,6 +577,10 @@ tcTopNormaliseNewTypeTF_maybe faminsts rdr_env ty
       = mapStepResult (\co -> (unitBag gre, co)) $
         unwrapNewTypeStepper rec_nts tc tys

+      | isClassTyCon tc && isNewTyCon tc
+      = mapStepResult (\co -> (emptyBag, co)) $
+        unwrapNewTypeStepper rec_nts tc tys
+
       | otherwise
       = NS_Done

The simplified example above is somewhat contrived, although I have legitimate need of this feature in more complicated scenarios like this one (inspired by Generic Programming of All Kinds):

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
module GOAK where

import Data.Coerce
import Data.Kind

newtype T = MkT ((forall a. Show a) => Int)
type TRep = Field (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0

f :: T -> TRep
f (MkT x) = Field (coerce @((forall a. Show a) => Int)
                          @(Interpret (ForAllQ (Kon Show :@: Var VZ) :=>>: Kon Int) LoT0)
                          x)

-----

infixr 5 :&&:
data LoT :: Type -> Type where
  LoT0    ::                LoT Type
  (:&&:)  :: k -> LoT ks -> LoT (k -> ks)

type family HeadLoT (tys :: LoT (k -> k')) :: k where
  HeadLoT (a :&&: _) = a

type family TailLoT (tys :: LoT (k -> k')) :: LoT k' where
  TailLoT (_ :&&: as) = as

data TyVar :: Type -> Type -> Type where
  VZ :: TyVar (x -> xs) x
  VS :: TyVar xs k -> TyVar (x -> xs) k

data Atom :: Type -> Type -> Type where
  Var     :: TyVar d k -> Atom d k
  Kon     :: k         -> Atom d k
  (:@:)   :: Atom d (k1 -> k2) -> Atom d k1 -> Atom d k2
  (:=>>:) :: Atom d Constraint -> Atom d Type -> Atom d Type
  ForAllQ :: Atom (d1 -> d) Constraint -> Atom d Constraint

type family InterpretVar (t :: TyVar d k) (tys :: LoT d) :: k where
  InterpretVar 'VZ     tys = HeadLoT tys
  InterpretVar ('VS v) tys = InterpretVar v (TailLoT tys)

type family Interpret (t :: Atom d k) (tys :: LoT d) :: k where
  Interpret ('Var v)     tys = InterpretVar v tys
  Interpret ('Kon t)     tys = t
  Interpret (f ':@: x)   tys = (Interpret f tys) (Interpret x tys)
  Interpret (c ':=>>: f) tys = SuchThatI c f tys
  Interpret (ForAllQ f)  tys = ForAllQI f tys

newtype SuchThatI :: Atom d Constraint -> Atom d Type -> LoT d -> Type where
  SuchThatI :: (Interpret c tys => Interpret f tys) -> SuchThatI c f tys

class    (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 -> d) Constraint) (tys :: LoT d)
instance (forall t. WrappedQI f (t ':&&: tys)) => ForAllQI (f :: Atom (d1 -> d) Constraint) (tys :: LoT d)

class    Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)
instance Interpret f tys => WrappedQI (f :: Atom d Constraint) (tys :: LoT d)

newtype Field :: Atom d Type -> LoT d -> Type where
  Field :: { unField :: Interpret t x } -> Field t x

f will not typecheck without the ability to coerce from ForAllQI f tys to forall t. WrappedQI f (t ':&&: tys). Moreover, it would be extremely difficult to write f without coerce.