#15852 closed bug (fixed)

Bad axiom produced for polykinded data family

Reported by: goldfire Owned by:
Priority: normal Milestone: 8.8.1
Component: Compiler Version: 8.7
Keywords: TypeFamilies, TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s): Phab:D5328
Wiki Page:

Description

When I say

data family DF a (b :: k)
data instance DF (Proxy c) :: Proxy j -> Type

with -ddump-tc, I get

  axiom Scratch.D:R:DFProxyProxy0 ::
    forall k1 k2 (c :: k1) (j :: k2) (a :: Proxy j).
      DF (Proxy c) a = Scratch.R:DFProxyProxy k1 k2 c j

This is bogus, because a should be on the RHS, too. It's not clear to me whether this is a pretty-printing bug or a real one.

Change History (8)

comment:1 Changed 11 months ago by goldfire

My guess is that it is a pretty-printing bug, as if it were anything more serious would have been discovered by now.

I would start by looking at Coercion.pprCoAxiom.

Actually, better than just fixing this bug would be removing Coercion.pprCoAxiom in favor of the IfaceAxiom case of pprIfaceDecl.

Unless it's not a pretty-printing bug.

comment:2 Changed 11 months ago 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 IfaceAxioms) calls pprAxBranch which, judging from its current implementation:
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.

comment:3 Changed 10 months ago by RyanGlScott

IfaceTyConInfo or IfaceTyConSort might be possible candidates for storing this information. Currently, these are defined as:

data IfaceTyConInfo   -- Used to guide pretty-printing
                      -- and to disambiguate D from 'D (they share a name)
  = IfaceTyConInfo { ifaceTyConIsPromoted :: IsPromoted
                   , ifaceTyConSort       :: IfaceTyConSort }

-- | The various types of TyCons which have special, built-in syntax.
data IfaceTyConSort = IfaceNormalTyCon          -- ^ a regular tycon

                    | IfaceTupleTyCon !Arity !TupleSort
                      -- ^ e.g. @(a, b, c)@ or @(#a, b, c#)@.

                    | IfaceSumTyCon !Arity
                      -- ^ e.g. @(a | b | c)@

                    | IfaceEqualityTyCon
                      -- ^ A heterogeneous equality TyCon

(The Haddocks for IfaceTyConSort are misleading, since every IfaceTyCon has one, not just those with special, built-in syntax. Regardless of how we fix this bug, we should change that documentation to reflect reality.)

My vote would be to extend one of these data types with an extra field of type IfaceTyConParent, which would be sufficient to tell if a TyCon came from a data family instance or not. Then it would just be a matter of plumbing this information to pprAxBranch from its call sites.

comment:4 Changed 10 months ago by goldfire

My pointing to pprCoAxiom was from its use in TcRnDriver.ppr_tycons. Given the appearance of "COERCION AXIOMS" in ppr_tycons, I thought it was what produced the output I saw, which also contains that string. Maybe I missed a beat somewhere, but I think you may be barking up the wrong tree.

comment:5 Changed 10 months ago by RyanGlScott

Oh dear. Yes, I was barking up the wrong tree—thank you for setting me straight.

Now that I dig closer into ppr_co_axiom_branch (which is the real culprit), I now understand what went wrong. When implementing etaExpandFamInstLHS, I left this comment:

-- @Note [Eta reduction for data families]@ in "FamInstEnv". Because the
-- right-hand side is where the eta-reduced variables are obtained from, it
-- is not returned from this function (as there is never a need to modify it).

In retrospect, I have no idea what I was smoking when I wrote this comment, because it's completely wrong. The right-hand side is eta-reduced, and that's what we're seeing in -ddump-tc. (Moreover, we aren't obtaining the eta-reduced variables from the RHS at all. They're actually being taken from the tyConTyVars of the representation TyCon.)

This suggests a straightforward fix: just eta expand the RHS as well, and return that from etaExpandFamInstLHS (or really, it just should be called etaExpandFamInst). I'll give that a shot.

comment:6 Changed 10 months ago by RyanGlScott

Differential Rev(s): Phab:D5328
Milestone: 8.8.1
Status: newpatch

comment:7 Changed 10 months ago by Ben Gamari <ben@…>

In 014d6c1/ghc:

Fix #15852 by eta expanding data family instance RHSes, too

When I defined `etaExpandFamInstLHS`, I blatantly forgot
to eta expand the RHSes of data family instances. (Actually, I
claimed that they didn't //need// to be eta expanded. I'm not sure
what I was thinking.)

This fixes the issue by changing `etaExpandFamInstLHS` to
`etaExpandFamInst` and, well, making it actually eta expand the RHS.

Test Plan: make test TEST=T15852

Reviewers: goldfire, bgamari

Reviewed By: goldfire

Subscribers: rwbarton, carter

GHC Trac Issues: #15852

Differential Revision: https://phabricator.haskell.org/D5328

comment:8 Changed 10 months ago by bgamari

Resolution: fixed
Status: patchclosed
Note: See TracTickets for help on using tickets.