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