That's a neat trick, Ross!  It seems really similar to using parametricity to recover the insides of lambdas in PHOAS metaprogramming:

-- HOAS expression language
data Expr (v :: * -> *) a where
    Ap :: Expr v (a -> b) -> Expr v a -> Expr v b
    Var :: v a -> Expr v a
    Lam :: (v a -> Expr v b) -> Expr v (a -> b)

-- some expressions that are paremetric in the variable type
ex_id :: Expr v (a -> a)
ex_id = Lam $ \x -> Var x

ex_const :: Expr v (a -> b -> a)
ex_const = Lam $ \x -> Lam $ \y -> Var x

-- a print function that relies on parametricity to expose the insides of the functions inside "Lam"
printExpr :: (forall v. Expr v a) -> String
printExpr e = pe_helper vars 0 e "" where
   vars = map (:[]) ['a' .. 'z'] ++ map (\n -> "t" ++ show n) [1..]

prec_lam = 1
prec_ap = 2

newtype VarName a = VarName String
pe_helper :: [String] -> Expr VarName a -> Int -> ShowS
pe_helper fv prec (Var (VarName s)) = showString s
pe_helper fv prec (Ap x y) = showParen (prec > prec_ap) (pe_helper fv prec_ap x . showString " " . pe_helper fv (prec_ap+1) y)
pe_helper (v:fv) prec (Lam k) = showParen (prec > prec_lam) (showString "\" . showString v . showString " -> " . pe_helper fv prec_lam e)
   where e = k (VarName v)

-- some test cases
test1 = printExpr ex_const -- "\a -> \b -> a"
test2 = printExpr (ex_id `Ap` ex_const) -- "(\a -> a) (\a -> \b -> a)"