Writing an instance of the form `(forall a . Class a => Class (f a)) => Class (Type f)`

Question

I perform default resolution in one of my programs by performing a natural transformation from MyType Maybe to MyType Identity. I want to derive a ToJSON instance for these types. I know that Maybe and Identity have instances ToJSON a => ToJSON (Maybe a) and ToJSON a => ToJSON (Identity a).

I would like to declare an instance of the following form:

instance (forall a . ToJSON a => ToJSON (f a)) => ToJSON (MyType f)

This seems like a reasonable request to put forth to the type system. I want to demonstrate a ToJSON instance for MyType f, provided that I can always get a ToJSON (f a) for every ToJSON a. In logical notation, this is like saying that I can demonstrate (P(a) ⇒ P(f(a))) ⇒ P(h(f)) for some property P. This seems well formed to me.

Unfortunately, I get the following error with the syntax as is:

• Illegal polymorphic type: forall a. ToJSON a => ToJSON (f a)
  A constraint must be a monotype
• In the context: (forall a. ToJSON a => ToJSON (f a))
  While checking an instance declaration
  In the instance declaration for ‘ToJSON (GpgParams f)’

It looks like the QuantifiedConstraints proposal would provide this syntax, but it has not been implemented yet.

I can try to work around this constraint by implementing my own class JSONable.

class JSONable f where
  jsonize :: f a -> Value

  default jsonize :: (ToJSON a, ToJSON (f a)) => f a -> Value
  jsonize = toJSON

Unfortunately this means giving up all functions in the standard library that use require a ToJSON constraint.

As far as I can tell the best tradeoff in this case is to simply give up and write explicit instances for:

instance ToJSON (MyType Maybe)
instance ToJSON (MyType Identity)

Is it true that this is simply as powerful as the language gets? Is the desired instance simply ill-formed? Or is it in fact possible to declare such an instance in Haskell for an existing typeclass?

Answer 1

Until QuantifiedConstraints arrive, there is a standard solution to encode a constraint like forall a. ToJSON a => ToJSON (f a), that seems like what you mentioned, but we don't have to give up functions that use a ToJSON constraint.

forall a. ToJSON a => ToJSON (f a) is a constraint on f: we can define that as a typeclass. Luckily, aeson already has ToJSON1.

class ToJSON1 f where  -- encoding of `forall a. ToJSON a => ToJSON (f a)`
  ...

And to use that class there is a function

toJSON1 :: (ToJSON1 f, ToJSON a) => f a -> Value

If any type F has an instance ToJSON1 F, then it is expected that its ToJSON instance is equivalent to

instance ToJSON a => ToJSON (F a) where
  toJSON = toJSON1

So that ToJSON1 F indeed encodes forall a. ToJSON a => ToJSON1 (F a).

One thing that seems missing from aeson is a way to solve a ToJSON (f a) constraint given ToJSON1 f and ToJSON a, but you can also encode it using the following newtype (higher-kinded version of Identity):

newtype Id1 f a = Id1 { unId1 :: f a }

instance (ToJSON1 f, ToJSON a) => ToJSON (Id1 f a) where
  toJSON = toJSON1 . unId1

Then to define ToJSON (MyType f), we can first apply coerce :: MyType f -> MyType (Id1 f).

import Data.Coerce

instance ToJSON1 f => ToJSON (MyType f) where
  toJSON = (...) . (coerce :: MyType f -> MyType (Id1 f))
    {- in "(...)" we can use functions that require "ToJSON (Id1 f a)", which is informally equivalent to "ToJSON (f a)" -}