[Haskell-cafe] Missing feature of Coercible, or necessary caution?

[Tom Ellis]

Consider the following program.

    {-# LANGUAGE TypeApplications #-}
    
    import Data.IntMap (IntMap, mapKeysMonotonic, Key)
    import Data.Coerce (coerce)
    
    newtype MyMap = MyMap (IntMap Bool)
    
    doesn'tWork :: (Key -> Key) -> MyMap -> MyMap
    doesn'tWork = coerce mapKeysMonotonic
    
    works :: (Key -> Key) -> MyMap -> MyMap
    works = coerce (mapKeysMonotonic @Bool)
    
mapKeysmonotonic has type

    (Key -> Key) -> IntMap a -> IntMap a

and we attempt to  coerce  it to type

    (Key -> Key) -> MyMap -> MyMap

since  MyMap  is a  newtype  around  IntMap Bool  this ends up
generating the constraint

    Coercible a Bool

and there is no way to specify that constraint given that  a  doesn't
otherwise appear in the top-level type. Hence  doesn'tWork  will not
type check.  If I force the type of  a  to be  Bool  using a
TypeApplication  then it does type check (works).

But is this a missing feature of GHC's  Coercible  system?  Since  a  is
not otherwise constrained is it not valid for GHC to choose it to be
Bool ?  Coercible  instances contain now observable content so no
observable behaviour could depend on the particular choice of  Coercible a Bool
instance, and choosing  a ~ Bool  is the natural one.

Is there some violation of type safety or otherwise broken behaviour
that could arise from choosing arbitrary  Coercible  instances on type
variables that are not otherwise constrained?

Tom