Singletons for Data.Functor.Product.Product?

[ocharles]

This seems to be left out of the Prelude stuff, but I'm also unable to run genSingletons on this type:

genSingletons [''Data.Functor.Product.Product]

Produces

    • Expected kind ‘* -> *’, but ‘f_a3Ku’ has kind ‘*’
    • In the first argument of ‘Data.Functor.Product.Product’, namely
        ‘f_a3Ku’
      In the first argument of ‘SingKind’, namely
        ‘(Data.Functor.Product.Product f_a3Ku g_a3Kv a_a3Kw)’
      In the instance declaration for
        ‘SingKind (Data.Functor.Product.Product f_a3Ku g_a3Kv a_a3Kw)’
   |
34 | genSingletons [''Data.Functor.Product.Product]
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Am I doing something wrong, or missing a language extension?

[ocharles]

My goal is to be able to turn the type 'Pair foo bar x into the corresponding value of type Product foo bar x, which I was trying to with demote.

[RyanGlScott]

You're not doing anything wrong per se. It's more that singletons isn't smart enough to handle the complexities of Product (or really, any data type with higher-kinded arguments).

In particular, genSingletons always tries to generate an instance of SingKind. Given a data type D a_1 ... a_n, genSingletons will attempt to generate the following code:

instance (SingKind a_1, ..., SingKind a_n) => SingKind (D a_1 ... a_n) where
  type Demote (D a_1 ... a_n) = D (Demote a_1) ... (Demote a_n)
  fromSing = ...
  toSing = ...

This works fine as long as a_1 through a_n all have kind Type. When you have type parameters that don't have kind Type, on the other hand, things get tricky. For example, the second argument to Const is of kind k. For this reason, we manually define Const's SingKind instance to work around this:

instance SingKind a => SingKind (Const a b) where
  type Demote (Const a b) = Const (Demote a) b
  fromSing = ...
  toSing = ...

We are able to get away with using b, not Demote b, in the RHS of the Demote instance since nothing of type b is ever used in the fields of the Const data constructor. Unfortunately, the same cannot be said of Product. Here is a naïve attempt at defining a SingKind instance for Product that demonstrates the issue:

instance SingKind (Product f g a) where
  type Demote (Product f g a) = Product f g a
  fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
  toSing = ...

This will fail to compile thusly:

Foo.hs:19:36: error:
    • Could not deduce: Demote (f a) ~ f a
      from the context: a1 ~ 'Pair n n1
        bound by a pattern with constructor:
                   SPair :: forall k (f :: k -> *) (g :: k -> *) (a :: k) (n1 :: f a)
                                   (n2 :: g a).
                            Sing n1 -> Sing n2 -> SProduct ('Pair n1 n2),
                 in an equation for ‘fromSing’
        at Foo.hs:19:13-25
    • In the first argument of ‘Pair’, namely ‘(fromSing sfa)’
      In the expression: Pair (fromSing sfa) (fromSing sga)
      In an equation for ‘fromSing’:
          fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
    • Relevant bindings include
        sga :: Sing n1 (bound at Foo.hs:19:23)
        sfa :: Sing n (bound at Foo.hs:19:19)
        fromSing :: Sing a1 -> Demote (Product f g a)
          (bound at Foo.hs:19:3)
   |
19 |   fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
   |                                    ^^^^^^^^^^^^

Foo.hs:19:51: error:
    • Could not deduce: Demote (g a) ~ g a
      from the context: a1 ~ 'Pair n n1
        bound by a pattern with constructor:
                   SPair :: forall k (f :: k -> *) (g :: k -> *) (a :: k) (n1 :: f a)
                                   (n2 :: g a).
                            Sing n1 -> Sing n2 -> SProduct ('Pair n1 n2),
                 in an equation for ‘fromSing’
        at Foo.hs:19:13-25
    • In the second argument of ‘Pair’, namely ‘(fromSing sga)’
      In the expression: Pair (fromSing sfa) (fromSing sga)
      In an equation for ‘fromSing’:
          fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
    • Relevant bindings include
        sga :: Sing n1 (bound at Foo.hs:19:23)
        sfa :: Sing n (bound at Foo.hs:19:19)
        fromSing :: Sing a1 -> Demote (Product f g a)
          (bound at Foo.hs:19:3)
   |
19 |   fromSing (SPair sfa sga) = Pair (fromSing sfa) (fromSing sga)
   |                                                   ^^^^^^^^^^^^

fromSing expects the fields of Pair to be of types Demote (f a) and Demote (g a), respectively, but due to the way we declared our Demote instance, they're actually of types f a and g a. You'll run into similar issues if you attempt to implement toSing. Alas, I don't see an easy way around this issue. #150 proposes an alternative design for SingKind that might make this possible, although I have not investigated this particular example yet.

Is all hope lost? Not necessarily. You can just as well omit the generation of SingKind instances by tweaking the Options a little bit:

$(withOptions defaultOptions{genSingKindInsts = False} (genSingletons [''Product]))

But since you explicitly mentioned that you wanted to use demote, I'm not sure if that is a satisfactory solution for you. demote requires a SingKind constraint, after all.

[ocharles]

Thank you for the very thorough explanation! Before even looking at singletons, I did just have this:

class ToValue (a :: k) where
  value :: k

type class, and that seemed to work. I could define an instance of this for 'Pair, so it sounds like I might just have to go back to that. Ultimately what I'm doing is constructing something in a type family, and then I want to turn that back into a value later. If singletons doesn't fit, that's not the end of the world. I have closed set of types to work with anyway, so I can define my own class to do demoting.

[RyanGlScott]

Indeed, I think you may have to stick with the ToValue approach you suggest. In theory, SingI + SingKind subsumes ToValue, but in practice, that combination is only as useful as things you can define SingKind instances for. I do hope that we can define a SingKind instance for Product some day, so I'll bring it up the topic on #150 to see if anyone has any ideas for how to redesign SingKind to make it work.

[RyanGlScott]

There is an interesting conversation starting here about how one might define a SingKind instance for Product. The tl;dr version is that this is likely blocked until at least one of two things happens:

1. Promote GADTs #150 is fixed (which itself is blocked on GHC#12088).
2. The UnsaturatedTypeFamilies GHC proposal is implemented.