Rank-2 PHOAS

Lately I've been experimenting with finally-tagless (typed) representations and made an attempt to model the (implicitly typed) lambda calculus. However, I wanted to use the parametric higher-order abstract syntax (PHOAS) technique to obtain variable bindings that are automatically well-scoped.
I arrived at this formulation:

class LC rep where
  var :: p → rep
  lam :: (forall p . p → rep) → rep


(I am ignoring applications as they are not important for making my point.)
As Andres Löh has pointed out to me this is not the final-tagless formulation of the regular PHOAS form, as that would add the p type variable as the second class parameter and the rank-2 forall would appear from "outside".
But I liked my simple formulation and the obviously and explicitly parametric lambda body. So I started implementing a rudimentary visualisation instance given a name supply:

instance LC ([String] → String) where
  var = ??? -- const "VAR"
  lam f = \supply → ...


It turns out that implementing var is only possible by giving a constant result, and for lam I am in trouble, because I cannot call f as it expects a polymorphic argument. Both problems are due to the fact that p is too polymorphic. Can we have it a bit less polymorphic in order to make some progress?
Thinking about it I came up with the idea of giving each instance a way to constrain the p variable as it fits. So I changed class LC such:

class LC rep where
  type Restricted rep p :: Constraint
  var :: Restricted rep p ⇒ p → rep
  lam :: (forall p . Restricted rep p ⇒ p → rep) → rep


Now my instance can pick the restriction as it fits:

instance LC ([String] → String) where
  type Restricted ([String] → String) p = ([String] → String) ~ p
  var = id
  lam f = \supply → ...


As you see I chose the restriction to be type equality which essentially cancels parametricity in this instance and gives me simple HOAS. Filling in p becomes easy now.

  lam f = \(n:ns) → "\\" ++ n ++ "." ++ (f $ const n) ns

Let's try it out! But in order to do that we need an instance of Show for name supplies. This could be one:

instance Show ([String] → String) where
  show f = f $ map (('v':) . show) [0..]


Now we can interpret a lambda term as a name supply.

*Main› lam (\x → lam $ \y → var x) :: [String] → String
\v0.\v1.v0

It works™ :-)

But I can go further. After implementing several other instances I observed that I always wanted to destroy parametricity completely and implement var as the identity. So why not have these as defaults and reduce the boilerplate by a nice margin? Here is the final class definition that I arrived at:

class LC rep where
  type Restricted rep p :: Constraint
  type Restricted rep p = rep ~ p
  var :: Restricted rep p ⇒ p → rep
  default var :: rep ~ p ⇒ p → rep
  var = id
  lam :: (forall p . Restricted rep p ⇒ p → rep) → rep


I like it so far.

PS: Here are the prerequisites if you want to compile the above yourself:

{-# LANGUAGE UnicodeSyntax, ConstraintKinds, TypeFamilies, RankNTypes, FlexibleInstances, DefaultSignatures #-}

import GHC.Exts