Good point. The constraint `Coercible a Bool` will not default `a` to Bool, because `a` could have other valid instantiations, such as `Identity Bool`. But you observe that, if there are no other constraints on `a`, then the choice of `a` does not matter, and so we might as well choose `a := Bool`. This is actually much like the fact that GHC accepts `length []`, even though it does not know what the element type of the list is. I think this can rightly be classed as a bug in GHC. If you submit a bug report, perhaps I will enjoy implementing a fix. :) Thanks, Richard

On Jan 25, 2022, at 9:16 AM, Tom Ellis wrote:

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 _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.