How are QuantifiedConstraints translated into dictionary passing style?

Question

QuantifiedConstraints¹ has landed in GHC 8.6, I am reading Deriving Type Classes (section 7)² where it was first suggested. However I can't understand, in operational terms, how QuantifiedConstraints are translated into dictionaries. Following is the excerpt from the paper.

data Rose a = Branch a [(Rose a)]
data GRose f a = GBranch a (f (GRose f a))
class Binary a where
  showBin :: a -> String

-- assuming following exists
-- instance (Binary a) => Binary [a]

instance (Binary a) => Binary (Rose a) where
  showBin (Branch x ts) = showBin x ++ showBin ts 

-- illegal
instance ( Binary a
         , Binary (f (GRose f a))
         ) => Binary (GRose f a) where
   showBin (GBranch x ts) = showBin x ++ showBin ts

What we need is a way to simplify the predicate f (GRose f a). The trick is to take the "constant" instance declaration that we assumed for Binary [a] above, and abstract over it:

-- using QuantifiedConstraints
instance ( Binary a
         , forall b. (Binary b) => Binary (f b)
         ) => Binary (GRose f a) where
  showBin (GBranch x ts) = showBin x ++ showBin ts

Now, as well as (Binary a), the context also contains a polymorphic predicate. This predicate can be used to reduce the predicate Binary (f (GRose f a)) to just Binary (GRose f a), and we have an instance declaration for that.

Viewed in operational terms, the predicate (Binary a) in a context corresponds to passing a dictionary for class Binary. A predicate forall b. Binary b => Binary (f b) corresponds to passing a dictionary transformer to the function.

In particular I can't grok the following:

1. Reduce the predicate Binary (f (GRose f a)) to just Binary (GRose f a)

2. A predicate corresponds to passing a dictionary transformer to the function.

Answer 1

For regular constraints, the translation maps

class Colored a where
   isRed :: a -> Bool

foo :: Colored a => T

to

newtype ColoredDict a = CD (a -> Bool)

foo :: ColoredDict a -> T

Similarly,

bar :: (forall a. Colored a => Colored [a]) => U

can be translated as

bar :: (forall a. ColoredDict a -> ColoredDict [a]) -> U

2) A predicate corresponds to passing a dictionary transformer to the function.

The first argument of bar is the "dictionary transformer" the OP mentions.

bar involves a rank-2 type, but Haskell has been using these for a long time.

1) Reduce the predicate Binary (f (GRose f a)) to just Binary (GRose f a)

The point is: every time bar need to resolve a constraint Colored [t], it can exploit the quantified constraint and instead try to resolve the simpler constraint Colored a.