Pretty printing with free monads and GADTs

Question

Consider the expression functor defined by the following GADT:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

import Control.Monad.Free

data ExprF :: * -> * where
  Term :: Foo a -> (a -> r) -> ExprF r

instance Functor ExprF where
  fmap f (Term d k) = Term d (f . k)

type Expr = Free ExprF

where Foo is defined as

data Foo :: * -> * where
  Bar :: Int    -> Foo Int
  Baz :: Double -> Foo Double

instance Show a => Show (Foo a) where
  show (Bar j) = show j
  show (Baz j) = show j

The combination of the (a -> r) field in ExprF and the (otherwise desirably) restrictive GADT constructors seem to make writing a pretty printing interpreter impossible:

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty (k _)

The type hole is what one would expect:

Found hole ‘_’ with type: a1
Where: ‘a1’ is a rigid type variable bound by
            a pattern with constructor
              Term :: forall r a. Foo a -> (a -> r) -> ExprF r,
            in an equation for ‘pretty’
            at Test.hs:23:15
Relevant bindings include
  k :: a1 -> Free ExprF a (bound at Test.hs:23:22)
  f :: Foo a1 (bound at Test.hs:23:20)
  pretty :: Free ExprF a -> String (bound at Test.hs:22:1)
In the first argument of ‘k’, namely ‘_’
In the first argument of ‘pretty’, namely ‘(k _)’
In the second argument of ‘(++)’, namely ‘pretty (k _)’

There seems to be no way to give the continuation a value at the type it requires. That type is encoded in f, and other interpreters I'm using all handle f somehow to extract a value at the appropriate type. But the path to a String representation seems blocked.

Is there some common idiom I'm missing here? How would one go about pretty printing a value of Expr, if it is indeed even possible? If it's not possible, what alternate construction of ExprF might capture the same structure, but also support a pretty printer?

Answer 1

Just pattern match on f. If you do that, the type of k gets refined to match the type contained inside Foo:

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty r where
  r = case f of
    Bar a -> k a
    Baz a -> k a

You might want to factor out this pattern:

applyToFoo :: (a -> r) -> Foo a -> r
applyToFoo f (Bar a) = f a
applyToFoo f (Baz a) = f a

pretty (Pure r)          = show r
pretty (Free (Term f k)) = "Term " ++ show f ++ pretty (applyToFoo k f)