## 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](https://mail.haskell.org/pipermail/haskell-cafe/2022-January/135035.html)) ## Expected behavior GHC picks `a ~ Bool`. ## Environment GHC 8.10, 9.2