Why is GHC contradicting itself when using a Coercible constraint?

Question

Why is GHC inferring unification from coercibility of associated data, and why is it contradicting its own checked type signature to do so?

The problem

{-# 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.

Coercibility

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.

Update!

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.

Pipsissewa

Very weird. I'm tempted to say this looks like plainly a bug in the typechecker. – Tellford

First off, you can simplify your example code just by pointing out that the function test :: forall a b. (Coercible (Bar a) (Bar b)) => Bar a -> Bar b with implementation test = coerce ends up with the type test :: Bar b -> Bar b in GHCi. That said, can you provide an example of using withBaz at any actually concrete type? For instance, for toMaybeBaz, what type do you have in mind that is coercible to MabyeBar (Bar a)? – Congratulant

"what type do you have in mind that is coercible to MabyeBar (Bar a)?" - Bar a, which Bar (Maybe a) is a wrapper around. They clearly have the same representation in memory, so they should be coercible. – Pipsissewa

I've added an update, since @Congratulant 's comment inspired me to look back over some older code that did use coerce in this way, and I found that it had a newtype declaration for the associated data family, rather than a data one. – Pipsissewa

Answer 1

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 as 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 newtypes 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.

Unlimited

SPJ may have a ticket. I have a proposal. I rather unthinkingly deleted the comment Thurs answer is based on... Oooops. – Jemina

"newtypes ... are always immediately coercible through unwrapping ... regardless of the role of the type parameter" - this is an interesting choice of design. Do you know where it comes from? I feel like, if you explicitly write type role MyNewType nominal, that GHC would ignore your specification seems absolutely bonkers. – Pipsissewa

It may help to read the paper. Basically, roles govern coercions between types with the same type constructor and different parametrizations: e.g., can MyNewType FirstType be coerced to MyNewType SecondType. In contrast, coercions from a newtype to its wrapped value (e.g., given newtype MyNewType a = MyNewType a, coercing MyNewType a to a) are governed by having the constructor in scope (with the rationale that it's just a zero-cost alternative to case x of MyNewtype y -> y). – Unlimited

If you want roles to matter with newtypes, arrange to have the constructor out-of-scope, by hiding it in a module, for example. – Unlimited