Re: [GHC] #15852: Bad axiom produced for polykinded data family

3 Nov 2018

      #15852: Bad axiom produced for polykinded data family
-------------------------------------+-------------------------------------
        Reporter:  goldfire          |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  normal            |            Milestone:
       Component:  Compiler          |              Version:  8.7
      Resolution:                    |             Keywords:  TypeFamilies,
                                     |  TypeInType
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):

 I think your hunch about it being a pretty-printing bug is right on the
 money. Moreover, I believe the `IfaceAxiom` case of `pprIfaceDecl`
 actually //is// the culprit, since:

 * `Coercion.pprCoAxiom` just calls `Coercion.ppr_co_ax_branch`, which
 already eta-expands the LHSes of data family instances.
 * `pprIfaceDecl` (for `IfaceAxiom`s) calls `pprAxBranch` which, judging
 from its current implementation:

 {{{#!hs
 pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc
 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)
     pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys)
     maybe_incomps = ppUnless (null incomps) $ parens $
                     text "incompatible indices:" <+> ppr incomps
 }}}

   Doesn't perform any sort of eta-expansion.

 In order to fix this, it looks like we'll need some equivalent of
 `etaExpandFamInstLHS`, but for iface data types. There's one major wrinkle
 that presents itself: how do we know that we're dealing with a data family
 instance in `pprAxBranch`? It's not obvious to me if that information is
 stored somewhere (I couldn't find anything in `IfaceTyCon`, for instance),
 and if not, where it //ought// to be stored.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/15852#comment:2
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler