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

[Tom Ellis]

Bug report submitted and assigned to you :)

    https://gitlab.haskell.org/ghc/ghc/-/issues/21003

On Tue, Jan 25, 2022 at 04:56:14PM +0000, Richard Eisenberg wrote:
> 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. :)
> 
> > On Jan 25, 2022, at 9:16 AM, Tom Ellis <tom-lists-haskell-cafe-2017 at jaguarpaw.co.uk> 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?