#15827 closed bug (fixed)

Explicit foralls in type family equations are pretty-printed inconsistently (and strangely, at times)

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

Description

Load the following code into GHCi HEAD (8.7+):

{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module Bug where

import Data.Kind

type family F1 a
type instance forall a. F1 a = Maybe a

type family F2 a where
  forall a. F2 a = Maybe a

data family D a
data instance forall a. D a = MkD (Maybe a)

And make sure you have the -fprint-explicit-foralls flag enabled. Now let's see what happens when we look up the :info for each of these type families:

$ ~/Software/ghc2/inplace/bin/ghc-stage2 --interactive Bug.hs -fprint-explicit-foralls
GHCi, version 8.7.20181029: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 1] Compiling Bug              ( Bug.hs, interpreted )
Ok, one module loaded.
λ> :i F1
type family F1 a :: *   -- Defined at Bug.hs:7:1
type instance F1 a = Maybe a    -- Defined at Bug.hs:8:25
λ> :i F2
type family F2 a :: *
  where [a] F2 a = Maybe a
        -- Defined at Bug.hs:10:1
λ> :i D
data family D a         -- Defined at Bug.hs:13:1
data instance D a = MkD (Maybe a)       -- Defined at Bug.hs:14:25

There are two strange things of note here:

  • The equations for F1 and D do not have any explicit foralls displayed at all, despite the fact that -fprint-explicit-foralls is enabled.
  • The equation for F2 does have an explicit forall displayed, but in a rather bizarre fashion:
λ> :i F2
type family F2 a :: *
  where [a] F2 a = Maybe a
        -- Defined at Bug.hs:10:1

I certainly wasn't expecting to see the type variables in square brackets. I would have hoped to see something like this instead:

λ> :i F2
type family F2 a :: *
  where forall a. F2 a = Maybe a
        -- Defined at Bug.hs:10:1

Now that the "more explicit foralls" proposal is implemented, my hope is that it will be somewhat simple to change the way that this is pretty-printed (we already store the explicit forall information within the AST, after all).

Change History (7)

comment:1 Changed 11 months ago 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 IfaceAxBranch (which is the interface file incarnation of a type family equation), for instance:

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

Notice that this stores type variable information (ifaxbTyVars) as IfaceTvBndrs instead of IfaceTyConBinders. This is an important distinction because essentially all of the machinery within IfaceType that pretty-prints explicit foralls works over IfaceTyConBinders, not IfaceTvBndrs. (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 IfaceTyConBinders (defaulting each variable's visibility to specified) before pretty-printing. But there's another challenge: how should we print the ifaxbCoVars? The existing code for pretty-printing IfaceAxBranches actually does take ifaxbCoVars into account at the moment:

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 comments for CoAxBranch:

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.

comment:2 Changed 11 months ago by goldfire

The covars are always empty. That comment is right. Along the way to -XTypeInType, there were some scenarios where the covars weren't empty. Mutterings to self are memorialized here.

As for pretty-printing behavior, I have a few observations:

  • The AST indeed stores whether or not the user wrote a forall, because some of the warnings, etc., are different based on this choice. However, once a type family equation is accepted, the presence/absence of the forall is immaterial.
  • The order of variables in the forall is immaterial to users. Not sure if this is a problem at all, but there's never a way to manually instantiate the variables, so we don't have to care about order.
  • Visibility/specificity is simply not a thing for the variables bound in a type family equation, also because the user can't ever instantiate these manually.
  • The funny [a] syntax was invented because using forall here is a tiny bit of a lie: forall is a specific construct in Core that does not exist in type family equations (i.e. coercion axioms). I don't think this is useful or friendly to users, though.

Do these design points help?

comment:3 Changed 11 months ago by RyanGlScott

OK. In that case, my tentative plan is to:

  • Not print the coercion variables at all.
  • Pretty-print the type variables by first converting them to IfaceForAllBinders (defaulting their visibilities to specified à la mkSpecForAllTys) and then using a function like pprIfaceForAll to pretty-print them with the explicit forall syntax.

Does that sound reasonable?

comment:4 Changed 11 months ago by goldfire

Yes. Without looking at the implementation, I'm not sure: will this print the kind of the type variables whose kind is not Type? If so (as I imagine it is), then full speed ahead.

comment:5 Changed 11 months ago by RyanGlScott

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

comment:6 Changed 10 months ago by Ryan Scott <ryan.gl.scott@…>

In f932b1a/ghc:

Print explicit foralls in type family eqns when appropriate

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 `forall`s 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

Reviewers: goldfire, bgamari, simonpj

Reviewed By: simonpj

Subscribers: simonpj, rwbarton, carter

GHC Trac Issues: #15827

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

comment:7 Changed 10 months ago by RyanGlScott

Resolution: fixed
Status: patchclosed
Test Case: ghci/scripts/T15827
Note: See TracTickets for help on using tickets.