Print explicit foralls in type family eqns when appropriate
ClosedPublic

Authored by RyanGlScott on Oct 29 2018, 5:42 PM.

Details

Summary

When -fprint-explicit-foralls is enabled, type family
equations are either printed without an explict forall entirely,
or with a bizarre square bracket syntax (in the case of closed type
families). I find neither satisfying, so in this patch, I introduce
support for printing explicit foralls in open type-family, closed
type-family, and data-family equations when appropriate. (By "when
appropriate", I refer to the conditions laid out in
Note [When to print foralls] in IfaceType.)

One tricky point in the implementation is that I had to pick a
visibility for each type variable in a CoAxiom/FamInst in order
to be able to pass it to pprUserIfaceForAll et al. Because
the type variables in a type family instance equation can't be
instantiated by the programmer anyway, the choice only really matters
for pretty-printing purposes, so I simply went with good ol'
trustworthy Specified. (This design choice is documented in
Note [Printing foralls in type family instances] in IfaceType.)

Test Plan

make test TEST=T15827

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
RyanGlScott created this revision.Oct 29 2018, 5:42 PM

Generally great, thank you. One puzzlement.

compiler/iface/IfaceSyn.hs
710–716

But this is a *data* family instance, and we do have [IfaceTyConBinder]. Why are you rejigging them to all be Specified, instead of using whatever they are?

The Note says "Type family instances only store type *variables*, not type variable *binders*, and only the latter has visibility information.". But here that claim is false: we have full IfaceTyConBinders.

Puzzling.

compiler/iface/IfaceType.hs
1103

This Note sorely needs an example, including the desired pretty-printed output.

The example could illustrate that kinds are made visible.

testsuite/tests/ghci/scripts/T15341.stdout
0–1

Can we put the where on the first line, as programmers usually do?

goldfire added inline comments.Nov 1 2018, 8:33 AM
compiler/iface/IfaceSyn.hs
710–716

It's true that data family instances store visibilities... but this information isn't useful to the programmer, because the visibilities properly belong to the data family *instance* tycon, which the programmer never uses.

Let's have a good ol' example:

data family DF (a :: k)  -- DF :: forall k. k -> Type

data instance DF '[a, b] = MkDFList   
-- data DFList a b = MkDFList
-- DFList :: forall {j}. j -> j -> Type
-- "type" instance forall j (a :: j) (b :: j). DF '[a, b] = DFList

Note that the j in the kind of DFList is Inferred, though the k in the type of DF is Specfified. However, this fact about j is utterly irrelevant to the programmer, who cares only about the specificity of variables in DF's type.

I thus agree with Ryan that these should always be printed as Specified.

Really, data family instance tycons have no business storing visibilities, but it seems silly to go to any lengths to remove them.

Regardless, there should be commentary about all this.

RyanGlScott marked 4 inline comments as done.
compiler/iface/IfaceSyn.hs
710–716

I agree with @goldfire's analysis here. I've expanded the Note with a data family example and now mention this particular wrinkle.

compiler/iface/IfaceType.hs
1103

I've expanded this Note with some more examples.

testsuite/tests/ghci/scripts/T15341.stdout
0–1

I've tried my hardest to do so.

simonpj added inline comments.Nov 1 2018, 10:48 AM
compiler/iface/IfaceSyn.hs
710–716

Note that the j in the kind of DFList is Inferred

But *why* is the j Inferred? Since DFList is never mentioned by the programmer, there is essentially no difference between Specified and Inferred. So why not make it Specified in the first place? (Or, equally, not store it at all.)

goldfire added inline comments.Nov 1 2018, 11:03 AM
compiler/iface/IfaceSyn.hs
710–716

But *why* is the j Inferred?

Because GHC invented it. We could special-case data family instances not to do this, but since the visibilities are immaterial, there seems to be no reason to do so.

simonpj added inline comments.Nov 1 2018, 11:15 AM
compiler/iface/IfaceSyn.hs
710–716

Do you happen to know exactly where GHC invents it?

goldfire added inline comments.Nov 2 2018, 3:02 PM
compiler/iface/IfaceSyn.hs
710–716

It turns out I was assuming things that aren't true. Let's have us a concrete example:

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

For the data family DF, we get DF :: forall k. Type -> k -> Type. That's not the issue here. For the rep-tycon DFPP, we get DFPP :: panic! the impossible happened!

Excuse me. I was lazily evaluating my understanding above, and I panicked. When I ran the above example through GHC with -ddump-types, I got

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

Note that a isn't on the RHS. That's clearly bogus. I will report a bug shortly.

In any case, what *should* happen is DFPP :: forall k1 k2 -> k1 -> forall (j :: k2) -> Proxy j -> Type. Note: no Inferred variables. Why? Because while the quantification is done in tcFamTyPats, tcDataFamInstDecl converts the quantified tyvars from tcFamTyPats into TyConBinders, and makes them all Required. The one possible exception to this is if there is a forall x y z. in the kind signature of the instance. tcDataKindSig will produce a Specified. In any case, no Inferred variables here.

The ordering of variables comes from a combination of decisions in tcFamTyPats and tcDataFamInstDecl, but need not concern us.

RyanGlScott added inline comments.Nov 5 2018, 11:53 AM
compiler/iface/IfaceSyn.hs
710–716

OK. Do you think I should revise the Note I've written in this Diff to include this more accurate visibility information, or is it fine as-is?

goldfire added inline comments.Nov 5 2018, 12:30 PM
compiler/iface/IfaceSyn.hs
710–716

I think it's fine. Simon may differ...

simonpj added inline comments.Nov 6 2018, 4:05 AM
compiler/iface/IfaceSyn.hs
710–716

That's clearly bogus. I will report a bug shortly.

Is that done?

In any case, what *should* happen is DFPP :: forall k1 k2 -> k1 -> forall (j :: k2) -> Proxy j -> Type. Note: no Inferred variables.

I'm lost here. I think you are talking about the kind of the rep-tycon, and what the visiblities of its variables should be? It' sounds subtle enough to document!

compiler/iface/IfaceType.hs
1115

Looking at this, I do wonder if item (2) of Note [When to print foralls] is sensible. An alternative would be to stick with (1) and (3). That's orthogonal to this discussion, I know. But it's odd that the forall pops up here.

1141

You mean Inferred not Invisible?

1143

I'm still puzzled about why we don't just make j Specified in the first place, when we build the representation TyCon. As you point out, it's a bit arbitrary, but it'd mean less fiddling here.

RyanGlScott updated this revision to Diff 18601.Nov 6 2018, 4:46 AM
RyanGlScott marked 10 inline comments as done.
  • Fix typo
compiler/iface/IfaceSyn.hs
710–716

Is that done?

Yes. See Trac #15852.

I'm lost here. I think you are talking about the kind of the rep-tycon, and what the visiblities of its variables should be?

Yes, that whole discussion is about what the visibilities of the representation TyCon should be internally (not how they're pretty-printed in :info, which is the nub of this patch).

It' sounds subtle enough to document!

Perhaps so.

As I state in another comment below, I don't think this is the appropriate patch to be fiddling about with the visibility of binders in the representation TyCon (lest there be knock-on effects). If we do decide to mess about with those visibilities in a later patch, I think that patch would be a good candidate to document what the ideal representation TyCon binder visibility story should be, as it will likely have been implemented in said patch.

compiler/iface/IfaceType.hs
1115

I'm not sure why you think it's odd. I would expect the situations under which type family equations print explicit foralls to be the same as any other place in GHC that can contain explicit foralls. I'd argue that the output would look strictly worse without the explicit forall here, since you'd instead get:

type family Foo (a :: k) :: k where
  Foo Maybe = []
  Foo a = Int
  Foo a = a

Here, you have to squint a bit in order to realize that the second and third equations are distinguished by their respective kinds for a.

1141

Indeed I did. Now fixed.

1143

Two comments about this:

  1. It's unclear to me if there'd be any knock-on effects elsewhere from changing the visibility of the binders of the representation TyCon. I'd prefer to keep this patch small.
  2. Even if we did change the visibility of the binders of the representation TyCon, we'd need to hard-code Specified in at least one place in pp_data_inst_forall. That's because a representation TyCon has IfaceTyConBinders (which use TyConBndrVis), whereas pprUserIfaceForAlls (which prints out explicit foralls à la Note [When to print foralls]) requires IfaceForAllBndrs (which use ArgFlag). Converting from a TyConBndrVis to an ArgFlag is not entirely straightforward, since you have to pick some visibility to default to (e.g., Specified) in the case when you're given an AnonTCB as a TyConBndrVis.
goldfire added inline comments.Nov 7 2018, 10:35 AM
compiler/iface/IfaceSyn.hs
710–716

I think we're tilting at windmills here. Visibilities are a user-facing Haskell feature only. They are utterly irrelevant in Core. Because users cannot write a rep-tycon, then the visibility of its binders (and indeed the ordering of its binders) is of utterly no consequence. That fact could be documented, but I think painstakingly describing the current situation is unnecessary. It simply doesn't matter!

simonpj added inline comments.Nov 7 2018, 11:15 AM
compiler/iface/IfaceSyn.hs
710–716

I agree. So let's make them all Specified from the get-go.

Whether that happens in this patch or another doesn't matter -- but this patch has to add code to work around their current visibility flags; so it might be less work to delete that work-around, and fix their birth.

RyanGlScott added inline comments.Nov 7 2018, 11:38 AM
compiler/iface/IfaceSyn.hs
710–716

I'll vote for "do it in another patch", since I'm worried about potentially unforeseen knock-on effects of changing these visibilities (it's possible that some other code is making assumptions about what data family instance representation tycon binders' visibilities are, for instance), and I'd prefer to keep this patch small if I can afford to do so :)

I'll revise the Note to not make any definite statements about what the visibilities actually are so that it's future-proof.

  • Revise language in Note

Does anything else need to be done here?

I'll vote for "do it in another patch", s

Happy for you to commit. Can you either make a new ticket, or leave the current one open, for the task of getting rid of the spurious visibilities?

Can you either make a new ticket, or leave the current one open, for the task of getting rid of the spurious visibilities?

I'm not sure how it would be possible to get rid of the visibilities. Data family instance representation TyCons are, well, TyCons, and all TyCons have TyConBinders (which have visibilities). To me, this suggests that having visibilities is an essential property of being a data family instance representation TyCon. But perhaps I'm missing something.

I'm not sure how it would be possible to get rid of the visibilities. Data family instance representation TyCons are, well, TyCons, and all TyCons have TyConBinders (which have visibilities). To me, this suggests that having visibilities is an essential property of being a data family instance representation TyCon. But perhaps I'm missing something.

You are right, I mis-spoke. I should have said: make all binders in a representation TyCon into Specified, at birth, rather than monkey with them during pretty-printing.

make all binders in a representation TyCon into Specified, at birth

I think you mean Required here...

I think you mean Required here...

If @simonpj did mean Required, then we're already done, since we construct data family instance binders with mkTyConBindersPreferAnon, which always uses Required when it needs to conjure up a visibility.

Thoughts on the discussion above, @simonpj?

simonpj accepted this revision.Nov 23 2018, 7:01 AM

Thoughts on the discussion above, @simonpj?

Trying to page this back in. Let's see if I have it right.

  • For type-family instances we are in pprAxBranch which does not store visibilities at all. So we make them all pretend to be Specified here
+ ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs
  • For data-family instances we in pprIfaceDecl (IfaceData ...). Here we doe have visibilities, but the are all Required or Anon, constructed in tcDataFamInstDecl.

The code I'm querying is in the latter case where you have

   pp_data_inst_forall =
+       pprUserIfaceForAll $
+ map (\tc_bndr -> Bndr (binderVar tc_bndr) Specified) binders

I now understand better what's happening here. We have binders :: [IfaceTyConBinder]. But we about to print a forall that scopes over an equation like this

forall a b.  D [a] (b->b) = blah

Those forall'd variables are really [IfaceForAllBndr. So we need to get from one to the other.

If you just has a local binding for the [IfaceForAllBndr] thus

forall_bndrs :: [IfaceForAllBndr]
forall_bndrs = map (Bndr (binderVar tc_bndr) Specified) | tc_bndr <- binders ]

I think I'd be happy. Thanks!

This revision is now accepted and ready to land.Nov 23 2018, 7:01 AM
RyanGlScott marked 10 inline comments as done.

If you just has a local binding for the [IfaceForAllBndr] thus

forall_bndrs :: [IfaceForAllBndr]
forall_bndrs = map (Bndr (binderVar tc_bndr) Specified) | tc_bndr <- binders ]

I think I'd be happy. Thanks!

Done.

Rebase on top of master

This revision was automatically updated to reflect the committed changes.