Coercion and roles - cannot compile with GHCi's type signature

Question

Typing the following in GHCi

>:set -XAllowAmbiguousTypes
>import Data.Coerce
>fcm f = coerce . foldMap (coerce . f)
>:t fcm
fcm
  :: (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) =>
     (a3 -> a2) -> t a3 -> c

Ok, that is what I expect. Copy paste that into a file.

{-# LANGUAGE AllowAmbiguousTypes #-}

import Data.Coerce

fcm :: (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) 
    => (a3 -> a2) -> t a3 -> c
fcm f = coerce . foldMap (coerce . f)

Now if you load this into GHCi, you get an error -

Weird.hs:7:9: error:
    • Couldn't match representation of type ‘a0’ with that of ‘c’
    arising from a use of ‘coerce’
      ‘c’ is a rigid type variable bound by
    the type signature for:
      fcm :: forall (t :: * -> *) a1 c a2 a3.
             (Foldable t, Monoid a1, Coercible a1 c, Coercible a2 a1) =>
             (a3 -> a2) -> t a3 -> c
    at Weird.hs:(5,1)-(6,30)
    • In the first argument of ‘(.)’, namely ‘coerce’
      In the expression: coerce . foldMap (coerce . f)
      In an equation for ‘fcm’: fcm f = coerce . foldMap (coerce . f)
    • Relevant bindings include
    fcm :: (a3 -> a2) -> t a3 -> c (bound at Weird.hs:7:1)

Huh? Where did a0 come from? If you delete the type signature, the code compiles fine again. Looks like we now have a function whose type we can't explain to the compiler and GHCi cannot tell us what that type is (it can only give us errors). GHC seems to be talking about internal type variables (in this case a0) which are not user facing.

Does this have something to do with the black magic surrounding Coercible? From GHC.Types:

Note [Kind-changing of (~) and Coercible]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

(~) and Coercible are tricky to define. To the user, they must appear as
constraints, but we cannot define them as such in Haskell. But we also cannot
just define them only in GHC.Prim (like (->)), because we need a real module
for them, e.g. to compile the constructor's info table.

Furthermore the type of MkCoercible cannot be written in Haskell
(no syntax for ~#R).

So we define them as regular data types in GHC.Types, and do magic in TysWiredIn,
inside GHC, to change the kind and type.

Am I understanding things correctly? Or is it possible to write a type signature for the function AND have the code compile successfully? For what it's worth, the thing I'm interested in being able to write is slightly simpler -

fcm :: (Monoid m, Coercible m b, Coercible b m, Foldable f) => (a -> b) -> f a -> b
fcm f = coerce . foldMap (coerce . f)

sumBy = fcm @Sum

chi chi · Accepted Answer · 2018-11-15T09:44:17

Here's what's happening, on a simpler example:

> :set -XAllowAmbiguousTypes
> import Data.Coerce
> f = coerce . coerce
> :t f
f :: (Coercible a1 c, Coercible a2 a1) => a2 -> c

So far, so good. Everything looks reasonable. However, if the following code will fail to compile:

f :: (Coercible a1 c, Coercible a2 a1) => a2 -> c
f = coerce . coerce

• Couldn't match representation of type ‘a0’ with that of ‘c’
    arising from a use of ‘coerce’
  ‘c’ is a rigid type variable bound by
    the type signature for:
      f :: forall a1 c a2. (Coercible a1 c, Coercible a2 a1) => a2 -> c

Why is this happening? Where does a0 come from?

Simply put, in coerce . coerce GHC has to choose an intermediate type, the result of the first coercion. This in principle could be anything, so GHC generates a fresh type variable for it: above, a0 is chosen for this.

The code then is type checked, and will require the constraints Coercible a0 c, Coercible a2 a0. The ones provided by the signature are different. Here, GHC will NOT try to "match" them and choose a0 = a1. Indeed, in some type class contexts, that might be the wrong choice.

For instance: (contrived example)

foo :: Read a => String -> ...
foo s = let
   x = read s && True
   in ...

It would be wrong to use the Read a constraint for resolving read s. Indeed, for that we need to use the global instance Read Bool, and ignore the constraint. Maybe later on in the code there is another read s call where we do need the constraint, but here we must not commit to it.

To fix your code, you need to be explicit on your coercions, telling GHC you really want to use your constraints. For instance, the following type checks (ScopedTypeVariables on).

f :: forall a1 a2 c . (Coercible a1 c, Coercible a2 a1) => a2 -> c
f = coerce . (coerce :: a2 -> a1)

Now we tell GHC that the intermediate type is indeed our a1.

You can fix your code by adding similar type annotations.

Coercion and roles - cannot compile with GHCi's type signature

1 Answers