Inferring general typeclass instance from a series of smaller ones?

Question

the title of this is admittedly not very descriptive, but I don't know how else to describe this in a short title. I'd appreciate any recommendations!

I'm going to be presenting a very simplified version of my issue :)

So I have a typeclass

class Known f a where
    known :: f a

That is supposed to be able to generate the canonical construction of a given type at a certain index, useful for working with GADT's and stuff. I'm giving a simplified version of this, with the relavant parts.

So there's obviously an instance for Proxy:

instance Known Proxy a where
    known = Proxy

Which we can use:

> known :: Proxy Monad
Proxy

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

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

infixr 5 (:<)

Where a Prod f '[a,b,c] would be roughly equivalent to a (f a, f b, f c) tuple. Same Functor, different types.

Writing the instance is decently straightforward:

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

Which works out pretty well: (assuming a Show instance)

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

But, I'm in the case where I need to make a "polymorphic" function on all as...but GHC is not liking it.

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

It comes up with this error:

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

Which I guess is saying that GHC can't show that there will be an instance it will pick that will work for any as, or, it doesn't have a strategy to construct known for that instance.

I as a human know that this is the case, but is there any way I can get this to work? The instances are all "in scope" and available...but how can I tell GHC how to construct it in a way that it is satisfied?

Answer 1

If there's no constraint for a class, you can't use its methods. Just add the constraint:

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, there's nothing from which instances could be built runtime in the absence of a dictionary to begin with. It might well be logically true that there exists instances for all inhabitants of a kind, but for programs we need dictionaries - constructive proofs - to run.

Writing out the constraints shouldn't bother us much, since 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 when we want instances for an open type with type family applications. In that case we have to write functions that explicitly build instances at the desired type from other known instances.