Are `Coercible` constraints free?

Lets say I have the data type:

data T a where
  T :: Coercible a b => U b -> T a 

If U is a Functor, we can then have this:

fromT :: T a -> U a
fromT (T x) = coerce <$> x

Does GHC remove the Coercible constraint at runtime to produce:

data T a where
  T :: U b -> T a 

I don't see the point of storing the Coercible dictionary, as coerce is always going to do nothing. That's exactly what coerce does, nothing, that's the point, it only works when types are representably equal.

Because without the free coerce, I'll have to make sure any coercions on T are valid myself, like so:

type role T representational
data T a where
  T :: U b -> T a 

makeT :: U a -> T a
makeT = T

fromT :: T a -> U a
fromT (T x) = unsafeCoerce x

And not exposing the T constructor.

Which is fine, but I'd rather the typechecker handle this than me just being very careful, but I don't want to incur the runtime size/cost unnecessarily.

Edit

Why am I doing this?

Because I have a class that's like this:

class C a where
  getU :: U a

But this is the problem. The role of a in U is nominal, not representational. So I can't do:

instance C Alice where
  getU = ...

newtype Bob = Bob Alice 
  deriving newtype C

I'm using newtyping a lot, so having to manually write instances (even if they're simple) is not only annoying, but I think it might add quite a bit of indirection (I'm not sure coerce <$> x will be able to be optimised away).

This approach does add one layer of indirection, but at least constant, it doesn't matter how many newtype wraps there are.

In reality, I'm calling getU getU', and defining:

getU :: C a => U a
getU = fromT . getU'

So I maintain the simpler interface for anyone not actually defining an instance.

I've also realised that I think what I've created is much like Coyoneda, which I've used one before to get around this issue with newtype deriving.

So any thoughts on a relatively cost free approach on this are appreciated.

Edit 2

Looks like I've had a similar issue six years ago. So when I've said I've used Coyoneda to get around this once I've lied it's actually been twice:

Generalised newtype deriving on class functions with Functors

Edit 3:

More particulars. What I'm actually dealing with is the type Codec and the class HasCodec.

I find if I redefine HasCodec like follows:

data WrappedJSONCodec value where
  WrappedJSONCodec :: Coercible baseValue value => JSONCodec baseValue -> WrappedJSONCodec value

class HasCodec value where
  codec' :: WrappedJSONCodec value

wrapJSONCodec :: JSONCodec value -> WrappedJSONCodec value
wrapJSONCodec = WrappedJSONCodec

unwrapJSONCodec :: forall value. WrappedJSONCodec value -> JSONCodec value
unwrapJSONCodec (WrappedJSONCodec @baseValue baseCodec) = 
  dimapCodec (coerce :: baseValue -> value) (coerce :: value -> baseValue) baseCodec

codec :: HasCodec value => JSONCodec value
codec = unwrapJSONCodec codec'

I've now got newtype deriving, at the small expense of having to call wrapJSONCodec for all the instance definitions.

I can then also get rid of layers of instance definitions like this:

newtype FirstName = FirstName { unFirstName :: Text }

instance HasCodec FirstName where
  codec = dimapCodec FirstName unFirstName codec

(sometimes there's more than one layer of newtype also)

In my app there are far more newtype definitions than novel ones, as whilst there's more than a hundred different "business" types, their serialisation/deserialisation generally follows half a dozen or so common patterns (i.e. text, integers, decimals, datetimes etc). So being able to newtype derive is a big win for readability, more than the cost of having to call wrapJSONCodec in instance definitions.

The dictionary remains part of the GADT and is not optimized away.

In particular, compiling the module:

module Coercible where

import Data.Coerce

newtype U b = U b

data T a where
  T :: Coercible a b => U b -> T a

toU :: T a -> U a
toU (T x) = coerce x

with:

ghc -Wall -O2 -ddump-simpl -dsuppress-all -dsuppress-uniques -fforce-recomp Coercible.hs

shows that the dictionary remains in place in the definition of toU in the optimized core (and remains in the STG, CMM, and assembly):

toU
  = \ @a ds ->
      case ds of { T @b $dCoercible x ->
      case coercible_sel $dCoercible of co { __DEFAULT ->
      x `cast` <Co:4> :: ...
      }
      }

and is part of the definition of the datatype T.