[GHC] #15827: Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times)

[GHC]

#15827: Explicit foralls in type family equations are pretty-printed inconsistently
(and strangely, at times)
-------------------------------------+-------------------------------------
        Reporter:  RyanGlScott       |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  TypeFamilies
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by RyanGlScott):

 Hm, it appears that fixing this may not be as straightforward as I would
 have hoped. The main issue that I encountered is that `:info` displays
 type family equations by first converting them to their interface file
 equivalents and then pretty-printing them. Take a look at
 [http://git.haskell.org/ghc.git/blob/4427315a65b25db22e1754d41b43dd4b782b022f:/compiler/iface/IfaceSyn.hs#l215
 IfaceAxBranch] (which is the interface file incarnation of a type family
 equation), for instance:

 {{{#!hs
 data IfaceAxBranch = IfaceAxBranch { ifaxbTyVars   :: [IfaceTvBndr]
                                    , ifaxbCoVars   :: [IfaceIdBndr]
                                    , ... }
 }}}

 Notice that this stores type variable information (`ifaxbTyVars`) as
 `IfaceTvBndr`s instead of `IfaceTyConBinder`s. This is an important
 distinction because essentially all of the machinery within `IfaceType`
 that pretty-prints explicit `forall`s works over `IfaceTyConBinder`s, not
 `IfaceTvBndr`s. (This makes some amount of sense since an
 `IfaceTyConBinder` stores visibility information but an `IfaceTvBinder`
 does not.)

 I suppose that we could just convert the `ifaxbTyVars` to
 `IfaceTyConBinder`s (defaulting each variable's visibility to specified)
 before pretty-printing. But there's another challenge: how should we print
 the `ifaxbCoVars`? The
 [http://git.haskell.org/ghc.git/blob/4427315a65b25db22e1754d41b43dd4b782b022f:/compiler/iface/IfaceSyn.hs#l560
 existing code] for pretty-printing `IfaceAxBranch`es actually does take
 `ifaxbCoVars` into account at the moment:

 {{{#!hs
 pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs
                                  , ifaxbCoVars = cvs
                                  , ifaxbLHS = pat_tys
                                  , ifaxbRHS = rhs
                                  , ifaxbIncomps = incomps })
   = hang ppr_binders 2 (hang pp_lhs 2 (equals <+> ppr rhs))
     $+$
     nest 2 maybe_incomps
   where
     ppr_binders = sdocWithDynFlags $ \dflags ->
                   ppWhen (gopt Opt_PrintExplicitForalls dflags)
 ppr_binders'

     ppr_binders'
       | null tvs && null cvs = empty
       | null cvs
       = brackets (pprWithCommas (pprIfaceTvBndr True) tvs)
       | otherwise
       = brackets (pprWithCommas (pprIfaceTvBndr True) tvs <> semi <+>
                   pprWithCommas pprIfaceIdBndr cvs)
 }}}

 I'm not sure what this code should become if we start using the `forall`
 keyword instead. To make things even more confusing, the
 [http://git.haskell.org/ghc.git/blob/4427315a65b25db22e1754d41b43dd4b782b022f:/compiler/types/CoAxiom.hs#l219
 comments] for `CoAxBranch`:

 {{{#!hs
 data CoAxBranch
   = CoAxBranch
     { ...
     , cab_tvs      :: [TyVar]       -- Bound type variables; not
 necessarily fresh
                                     -- See Note [CoAxBranch type
 variables]
                                     -- May be eta-reduded; see FamInstEnv
                                     -- Note [Eta reduction for data
 families]
     , cab_cvs      :: [CoVar]       -- Bound coercion variables
                                     -- Always empty, for now.
                                     -- See Note [Constraints in patterns]
                                     -- in TcTyClsDecls
     , ...
     }
 }}}

 Suggest that the bound coercion variables in a coaxiom branch are always
 empty in practice! So is it even worth fretting over them? Perhaps an
 expert in this area could answer this question, but I'm far from that
 expert.

-- 
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/15827#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler