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

[Richard Eisenberg]

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