ConstraintsB can't be derived for data family?

[i-am-tom]

Hello again 😅 Long time no see!

A slightly weird use case: this fails to derive ConstraintsB (but notably is fine with just FunctorB) because of a failure to deduce some Coercible instance.

import Barbies qualified as B

data family T x :: (Type -> Type) -> Type
data instance T () f = C { s :: f Bool }
  deriving stock Generic
  deriving anyclass (B.FunctorB, B.ConstraintsB)

Weirder still, the error suggests that GHC made no progress on Zip at all here, getting immediately stuck at the datatype metadata level:

...: error:
    • Could not deduce: Coercible
                          (barbies-2.0.4.0:Data.Generics.GenericN.Zip
                             (Rep
                                (T (barbies-2.0.4.0:Data.Generics.GenericN.Param 1 ())
                                   (barbies-2.0.4.0:Data.Generics.GenericN.Param 0 f)))
                             (G.D1
                                ('G.MetaData "T" "Main" "main" 'False)
                                (G.C1
                                   ('G.MetaCons "C" 'G.PrefixI 'True)
                                   (G.S1
                                      ('G.MetaSel
                                         ('Just "s")
                                         'G.NoSourceUnpackedness
                                         'G.NoSourceStrictness
                                         'G.DecidedLazy)
                                      (G.Rec0 (f Bool))))))
                          (G.Rec0 (f Bool))
        arising from the 'deriving' clause of a data type declaration
      from the context: B.AllB c (T ())
        bound by the deriving clause for ‘B.ConstraintsB (T ())’
        at ...
    • When deriving the instance for (B.ConstraintsB (T ()))
   |
68 |   deriving anyclass (B.FunctorB, B.ConstraintsB)
   |                                  ^^^^^^^^^^^^^^

I don't understand enough of the Barbies internals to give a good guess as to why, so before I do any rummaging, do you have any idea? Otherwise, I'll see whether I can figure it out.

Thanks!
Tom

[i-am-tom]

Ah, I think I understand what's happening here: T (Param 1 ()) doesn't resolve to the same instance as T (), so it can't be zipped?

[jcpetruzza]

Hey, Tom! Sorry, it took me some time to look into this

So, yeah, I think you are correct. What is happening is that this term gets stuck:

                             (Rep
                                (T (barbies-2.0.4.0:Data.Generics.GenericN.Param 1 ())
                                   (barbies-2.0.4.0:Data.Generics.GenericN.Param 0 f)))

And the reason it gets stuck is that, as you say, T is a type family, and there is no instance for T (Param 1 ()). If T x were instead a type (and not a type family instance), then T (Param 1 ()) would have exactly the same generic representation as T (), and because Param is a newtype, it would be coercible to T (). This slides maybe give an idea of how this works.

Anyway, to avoid this problem, we'd need to somehow know that the first argument of T has a nominal role so we don't tag it with Param 1, but afaik, we don't get this exposed. Maybe @kcsongor knows a way to make this work?