Coercible constraints should be picked arbitrarily

Summary

Coercible constraints should be picked arbitrarily, in the absence of other, computationally-relevant constraints.

Steps to reproduce

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 no 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.

(Discussed earlier on haskell-cafe)

Expected behavior

GHC picks a ~ Bool.

Environment

GHC 8.10, 9.2