Why is GHC inferring unification from coercibility of associated data, and why is it contradicting its own checked type signature to do so?
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeFamilies #-}
module Lib
(
) where
import Data.Coerce
class Foo a where
data Bar a
data Baz a = Baz
{ foo :: a
, bar :: Bar a
}
type BarSame a b = (Coercible (Bar a) (Bar b), Coercible (Bar b) (Bar a))
withBaz :: forall a b. BarSame a b => (a -> b) -> Baz a -> Baz b
withBaz f Baz{..} = Baz
{ foo = f foo
, bar = coerce bar
}
This is all well and good - GHC will happily compile this code, and is confident that withBaz
has the declared signature.
Now, let's try to use it!
instance (Foo a) => Foo (Maybe a) where
data Bar (Maybe a) = MabyeBar (Bar a)
toMaybeBaz :: Baz a -> Baz (Maybe a)
toMaybeBaz = withBaz Just
This gives an error - but a really weird one:
withBaz Just
^^^^^^^^^^^^
cannot construct the infinite type: a ~ Maybe a
Indeed, if I go into GHCi, and ask it to give me the type of withBaz
:
ghc>:t withBaz
withBaz :: (b -> b) -> Baz b -> Baz b
That's not the signature I gave it.
I suspect that GHC is treating the type arguments of withBaz
as though they have to unify, because it's inferring Coercible a b
from Coercible (Bar a) (Bar b)
. But because it's a data family, they don't even need to be Coercible
- certainly not unifiable.
The following change fixes the compilation:
instance (Foo a) => Foo (Maybe a) where
newtype Bar (Maybe a) = MabyeBar (Bar a)
That is - declare the data family as a newtype
, instead of a data
. This seems consistent with GHC's treatment of Coercible
in the language in general, in that
data Id a = Id a
will not cause a Coercible
instance to be generated - even though it should definitely be coercible to a
. With the above declaration, this will error:
wrapId :: a -> Id a
wrapId = coerce
But with a newtype
declaration:
newtype Id a = Id a
then the Coercible
instance exists, and wrapId
compiles.
I believe @dfeuer's since-deleted comment about lack of "role" support for type/data families provides the answer.
For a top-level, data
-defined parametrized type:
data Foo a = ...
the coercibility of types Foo a
and Foo b
depends on the role of the parameter a
. In particular, if a
s role is nominal, then Foo a
and Foo b
are coercible if and only if a
and b
are precisely the same type.
So, in the program:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RoleAnnotations #-}
import Data.Coerce
type role Foo nominal
data Foo a = Foo
foo :: (Coercible (Foo a) (Foo b)) => a -> b
foo = undefined
because of the nominal
role of the parameter a
in Foo a
, the type of foo
is actually simplified to b -> b
:
λ> :t foo
foo :: b -> b
If the role annotation is changed from nominal
to representational
, the type is simplified to Coercible a b => a -> b
, and if the role is changed to phantom
(the default for this particular declaration of Foo
, as a
does not appear on the right-hand side), the type is simplified to a -> b
. This is all as expected and corresponds to the definition of each of these roles.
Note that if you replaced the declaration of Foo
with:
data Foo a = Foo a
then the phantom
role would not longer be permitted, but the inferred types for foo
under the other two roles would be exactly as before.
However, there's an important difference if you switch from a data
to a newtype
. With:
newtype Foo a = Foo a
you'd discover that even with type role Foo nominal
, the inferred type for foo
would be Coercible b a => a -> b
instead of b -> b
. That's because the algorithm for type-safe coercions handles newtype
s differently than "equivalent" data
types, as you've noted in your question -- they are always immediately coercible through unwrapping whenever the constructor is in scope, regardless of the role of the type parameter.
So, with all that being said, your experience with associated data families is consistent with the role of the family's type parameter being set to nominal
. Though I couldn't find it documented in the GHC manual, this appears to be as-designed behavior, and there's an open ticket that acknowledges all data/type families have all parameters assigned nominal
role and proposes relaxing this restriction, and @dfeuer actually has a detailed proposal from this past October.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With