Deriving a generic instance of typeclass from a series of smaller ones?

Question

the name of this is admittedly not very descriptive, but I don’t know how else to describe it in a short title. I would be grateful for any recommendations!

I am going to present a very simplified version of my problem :)

So I have a class

class Known fa where known :: fa 

It is assumed that he will be able to generate a canonical construction of this type with a specific index, useful for working with GADT, etc. I give a simplified version of this , with relevant details.

So, obviously, there is an instance for Proxy :

 instance Known Proxy a where known = Proxy 

What we can use:

 > known :: Proxy Monad Proxy 

But there is also an instance for this HList-like type :

 data Prod f :: [k] -> * where PNil :: Prod f '[] (:<) :: fa -> Prod f as -> Prod f (a ': as) infixr 5 (:<) 

Where a Prod f '[a,b,c] will be roughly equivalent to the tuple (fa, fb, fc) . The same Functor, different types.

Recording an instance is quite simple:

 instance Known (Prod f) '[] where known = PNil instance (Known fa, Known (Prod f) as) => Known (Prod f) (a ': as) where known = known :< known 

What turns out well: (subject to the Show instance)

 > known :: Prod Proxy '[1,2,3] Proxy :< Proxy :< Proxy :< PNil 

But I am in the case when I need to make a "polymorphic" function on all as ... but I do not like GHC.

 asProds :: forall as. Proxy as -> Prod Proxy as asProds _ = known :: Prod Proxy as 

This error comes up:

 No instance for (Known (Prod f) as) arising from a use of 'known' 

I think this suggests that the GHC cannot show that there will be an instance that it selects that will work for any as , or it does not have a strategy to create known for this instance.

I, as a person, know that this is so, but is there a way to make this work? The instances are all "in scope" and available ... but how can I tell the GHC how to build it in such a way that it is satisfied?

Answer 1

If there are no restrictions for a class, you cannot use its methods. Just add a restriction:

 asProds :: forall as. Known (Prod Proxy) as => Proxy as -> Prod Proxy as asProds _ = known :: Prod Proxy as 

Note that GHC can infer this type:

 asProds (_ :: Proxy as) = known :: Prod Proxy as -- inferred constraint 

Since types are erased, none of which can be built at run time without using a dictionary. It may be logical that there are instances for all residents, but programs need dictionaries - constructive evidence - to run.

Writing off the restrictions should not bother us much, because if we have instances for all cases, then when we need an instance, we can usually get one, with not too frequent exceptions. The exception is that we want instances for an open type to be applied to the type family. In this case, we must write functions that explicitly create instances of the required type from other known instances.