Pretty-printing of type variables (Help needed for #8776)

[Dr. ERDI Gergo]

Hi,

Ticket #8776 (https://ghc.haskell.org/trac/ghc/ticket/8776) is about the 
output formatting of pattern synonym type signatures. With -dppr-debug, 
the problematic signature looks like this:

(base:GHC.Num.Num{tc 2b} t{tv aQa} [sk],
  ghc-prim:GHC.Classes.Eq{tc 23} t{tv aQb} [sk]) =>
main:Main.P{d rs2} :: main:Main.A{tc rpC} t{tv aQa} [sk] t1{tv aQb} [sk]

The problem is that the two type variables occuring in the provided 
context both have "t" as their user-visible name; even though the second 
one is projected as "t1" in the tau type on the right-hand side.

The code to generate this output is in HsBinds.ppr_sig, using pprPatSynSig 
which just adds the "pattern" keyword and the separating "=>" symbols etc:

ppr_sig (PatSynSig name arg_tys ty prov req)
   = pprPatSynSig (unLoc name) False args (ppr ty) (pprCtx prov) (pprCtx req)
   where
     args = fmap ppr arg_tys

     pprCtx lctx = case unLoc lctx of
         [] -> Nothing
         ctx -> Just (pprHsContextNoArrow ctx)


My guess is that the problem is 'pprHsContextNoArrow' projects individual 
constraints one-by-one and so doesn't notice the name clash on 
't' between the two constraints in the example; whereas 'ppr ty' walks the 
whole right-hand tau type and thus has the opportunity to maintain a set 
of type variable names used.

My question is, where is that logic, and how can I use that in this 
instance? My hope is to be shown a design where I can run 'ppr ty', 
'pprCtx prov' and 'pprCtx req' in the same "naming environment" (I hope 
such a thing exists) so that they use a consistent naming scheme. This 
looks like a problem that must have popped up at a lot of places in GHC 
already and must have an idiomatic solution.

Thanks,
 	Gergo