diff options
author | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-11-26 12:59:09 -0500 |
---|---|---|
committer | Ryan Scott <ryan.gl.scott@gmail.com> | 2018-11-26 12:59:11 -0500 |
commit | f932b1aa42f45625658c8abaf862cc570507c5ca (patch) | |
tree | 0755ee1ce530f0afee8a6b5ec44f22e53eee3cc5 /compiler/iface | |
parent | df570d920fa66db631f936fa377e598fe92bd2a1 (diff) | |
download | haskell-f932b1aa42f45625658c8abaf862cc570507c5ca.tar.gz |
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
Diffstat (limited to 'compiler/iface')
-rw-r--r-- | compiler/iface/IfaceSyn.hs | 46 | ||||
-rw-r--r-- | compiler/iface/IfaceType.hs | 53 |
2 files changed, 77 insertions, 22 deletions
diff --git a/compiler/iface/IfaceSyn.hs b/compiler/iface/IfaceSyn.hs index 4d70b11973..2e63fbc22f 100644 --- a/compiler/iface/IfaceSyn.hs +++ b/compiler/iface/IfaceSyn.hs @@ -64,12 +64,11 @@ import SrcLoc import Fingerprint import Binary import BooleanFormula ( BooleanFormula, pprBooleanFormula, isTrue ) -import Var( VarBndr(..) ) +import Var( VarBndr(..), binderVar ) import TyCon ( Role (..), Injectivity(..) ) import Util( dropList, filterByList ) import DataCon (SrcStrictness(..), SrcUnpackedness(..)) import Lexeme (isLexSym) -import DynFlags import Control.Monad import System.IO.Unsafe @@ -558,7 +557,6 @@ pprAxBranch :: SDoc -> IfaceAxBranch -> SDoc -- be a branch for an imported TyCon, so it would be an ExtName -- So it's easier to take an SDoc here pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs - , ifaxbCoVars = cvs , ifaxbLHS = pat_tys , ifaxbRHS = rhs , ifaxbIncomps = incomps }) @@ -566,16 +564,8 @@ pprAxBranch pp_tc (IfaceAxBranch { ifaxbTyVars = tvs $+$ 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) + -- See Note [Printing foralls in type family instances] in IfaceType + ppr_binders = pprUserIfaceForAll $ map (mkIfaceForAllTvBndr Specified) tvs pp_lhs = hang pp_tc 2 (pprParendIfaceAppArgs pat_tys) maybe_incomps = ppUnless (null incomps) $ parens $ text "incompatible indices:" <+> ppr incomps @@ -718,6 +708,12 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, , nest 2 $ ppShowIface ss pp_extra ] where is_data_instance = isIfaceDataInstance parent + -- See Note [Printing foralls in type family instances] in IfaceType + pp_data_inst_forall :: SDoc + pp_data_inst_forall = pprUserIfaceForAll forall_bndrs + + forall_bndrs :: [IfaceForAllBndr] + forall_bndrs = [Bndr (binderVar tc_bndr) Specified | tc_bndr <- binders] cons = visibleIfConDecls condecls pp_where = ppWhen (gadt && not (null cons)) $ text "where" @@ -728,7 +724,9 @@ pprIfaceDecl ss (IfaceData { ifName = tycon, ifCType = ctype, pp_lhs = case parent of IfNoParent -> pprIfaceDeclHead context ss tycon binders Nothing - _ -> text "instance" <+> pprIfaceTyConParent parent + IfDataInstance{} + -> text "instance" <+> pp_data_inst_forall + <+> pprIfaceTyConParent parent pp_roles | is_data_instance = empty @@ -821,11 +819,16 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon = text "data family" <+> pprIfaceDeclHead [] ss tycon binders Nothing | otherwise - = hang (text "type family" <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind)) + = hang (text "type family" + <+> pprIfaceDeclHead [] ss tycon binders (Just res_kind) + <+> ppShowRhs ss (pp_where rhs)) 2 (pp_inj res_var inj <+> ppShowRhs ss (pp_rhs rhs)) $$ nest 2 (ppShowRhs ss (pp_branches rhs)) where + pp_where (IfaceClosedSynFamilyTyCon {}) = text "where" + pp_where _ = empty + pp_inj Nothing _ = empty pp_inj (Just res) inj | Injective injectivity <- inj = hsep [ equals, ppr res @@ -848,13 +851,12 @@ pprIfaceDecl ss (IfaceFamily { ifName = tycon = ppShowIface ss (text "built-in") pp_branches (IfaceClosedSynFamilyTyCon (Just (ax, brs))) - = hang (text "where") - 2 (vcat (map (pprAxBranch - (pprPrefixIfDeclBndr - (ss_how_much ss) - (occName tycon)) - ) brs) - $$ ppShowIface ss (text "axiom" <+> ppr ax)) + = vcat (map (pprAxBranch + (pprPrefixIfDeclBndr + (ss_how_much ss) + (occName tycon)) + ) brs) + $$ ppShowIface ss (text "axiom" <+> ppr ax) pp_branches _ = Outputable.empty pprIfaceDecl _ (IfacePatSyn { ifName = name, diff --git a/compiler/iface/IfaceType.hs b/compiler/iface/IfaceType.hs index e2ea655194..25000737a6 100644 --- a/compiler/iface/IfaceType.hs +++ b/compiler/iface/IfaceType.hs @@ -21,6 +21,7 @@ module IfaceType ( IfaceContext, IfaceBndr(..), IfaceOneShot(..), IfaceLamBndr, IfaceTvBndr, IfaceIdBndr, IfaceTyConBinder, IfaceForAllBndr, ArgFlag(..), ShowForAllFlag(..), + mkIfaceForAllTvBndr, ifForAllBndrVar, ifForAllBndrName, ifTyConBinderVar, ifTyConBinderName, @@ -158,6 +159,10 @@ data IfaceTyLit type IfaceTyConBinder = VarBndr IfaceBndr TyConBndrVis type IfaceForAllBndr = VarBndr IfaceBndr ArgFlag +-- | Make an 'IfaceForAllBndr' from an 'IfaceTvBndr'. +mkIfaceForAllTvBndr :: ArgFlag -> IfaceTvBndr -> IfaceForAllBndr +mkIfaceForAllTvBndr vis var = Bndr (IfaceTvBndr var) vis + -- | Stores the arguments in a type application as a list. -- See @Note [Suppressing invisible arguments]@. data IfaceAppArgs @@ -1091,6 +1096,54 @@ criteria are met: N.B. Until now (Aug 2018) we didn't check anything for coercion variables. +Note [Printing foralls in type family instances] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +We use the same criteria as in Note [When to print foralls] to determine +whether a type family instance should be pretty-printed with an explicit +`forall`. Example: + + type family Foo (a :: k) :: k where + Foo Maybe = [] + Foo (a :: Type) = Int + Foo a = a + +Without -fprint-explicit-foralls enabled, this will be pretty-printed as: + +type family Foo (a :: k) :: k where + Foo Maybe = [] + Foo a = Int + forall k (a :: k). Foo a = a + +Note that only the third equation has an explicit forall, since it has a type +variable with a non-Type kind. (If -fprint-explicit-foralls were enabled, then +the second equation would be preceded with `forall a.`.) + +There is one tricky point in the implementation: what visibility +do we give the type variables in a type family instance? Type family instances +only store type *variables*, not type variable *binders*, and only the latter +has visibility information. We opt to default the visibility of each of these +type variables to Specified because users can't ever instantiate these +variables manually, so the choice of visibility is only relevant to +pretty-printing. (This is why the `k` in `forall k (a :: k). ...` above is +printed the way it is, even though it wasn't written explicitly in the +original source code.) + +We adopt the same strategy for data family instances. Example: + + data family DF (a :: k) + data instance DF '[a, b] = DFList + +That data family instance is pretty-printed as: + + data instance forall j (a :: j) (b :: j). DF '[a, b] = DFList + +This is despite that the representation tycon for this data instance (call it +$DF:List) actually has different visibilities for its binders. +However, the visibilities of these binders are utterly irrelevant to the +programmer, who cares only about the specificity of variables in `DF`'s type, +not $DF:List's type. Therefore, we opt to pretty-print all variables in data +family instances as Specified. + Note [Printing promoted type constructors] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Consider this GHCi session (Trac #14343) |