Commit f932b1aa authored by Ryan Scott's avatar Ryan Scott

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
parent df570d92
......@@ -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,
......
......@@ -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)
......
......@@ -21,7 +21,7 @@ module PprTyThing (
import GhcPrelude
import Type ( TyThing(..) )
import Type ( ArgFlag(..), TyThing(..), mkTyVarBinders, pprUserForAll )
import IfaceSyn ( ShowSub(..), ShowHowMuch(..), AltPpr(..)
, showToHeader, pprIfaceDecl )
import CoAxiom ( coAxiomTyCon )
......@@ -117,9 +117,13 @@ pprFamInst (FamInst { fi_flavor = DataFamilyInst rep_tc })
= pprTyThingInContextLoc (ATyCon rep_tc)
pprFamInst (FamInst { fi_flavor = SynFamilyInst, fi_axiom = axiom
, fi_tys = lhs_tys, fi_rhs = rhs })
, fi_tvs = tvs, fi_tys = lhs_tys, fi_rhs = rhs })
= showWithLoc (pprDefinedAt (getName axiom)) $
hang (text "type instance" <+> pprTypeApp (coAxiomTyCon axiom) lhs_tys)
hang (text "type instance"
<+> pprUserForAll (mkTyVarBinders Specified tvs)
-- See Note [Printing foralls in type family instances]
-- in IfaceType
<+> pprTypeApp (coAxiomTyCon axiom) lhs_tys)
2 (equals <+> ppr rhs)
----------------------------
......
type family F a :: *
where
F [Int] = Bool
F [a] = Double
F (a b) = Char
type family F a :: * where
F [Int] = Bool
F [a] = Double
F (a b) = Char
-- Defined at T13420.hs:4:1
type family Foo (a :: k) :: k
where Foo a = a
type family Foo (a :: k) :: k where
forall k (a :: k). Foo a = a
-- Defined at T15341.hs:5:1
type family Foo @k (a :: k) :: k
where Foo @k a = a
type family Foo @k (a :: k) :: k where
forall k (a :: k). Foo @k a = a
-- Defined at T15341.hs:5:1
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
module T15827 where
import Data.Kind
import Data.Proxy
type family F1 (a :: k)
type instance forall k (a :: k). F1 a = Proxy a
type family F2 (a :: k) :: Type where
forall k (a :: k). F2 a = Proxy a
data family D (a :: k)
data instance forall k (a :: k). D a = MkD (Proxy a)
:load T15827
:info F1
:info F2
:info D
type family F1 (a :: k) :: * -- Defined at T15827.hs:9:1
type instance forall k (a :: k). F1 a = Proxy a
-- Defined at T15827.hs:10:34
type family F2 (a :: k) :: * where
forall k (a :: k). F2 a = Proxy a
-- Defined at T15827.hs:12:1
data family D (a :: k) -- Defined at T15827.hs:15:1
data instance forall k (a :: k). D a = MkD (Proxy a)
-- Defined at T15827.hs:16:34
......@@ -11,10 +11,9 @@ class C a where
-- Defined at T4175.hs:16:5
type instance D () () = Bool -- Defined at T4175.hs:22:10
type instance D Int () = String -- Defined at T4175.hs:19:10
type family E a :: *
where
E () = Bool
E Int = String
type family E a :: * where
E () = Bool
E Int = String
-- Defined at T4175.hs:24:1
data () = () -- Defined in ‘GHC.Tuple’
instance [safe] C () -- Defined at T4175.hs:21:10
......
......@@ -5,23 +5,21 @@ Bar :: k -> * -> *
type family F a :: * -- Defined at T7939.hs:8:1
type instance F Int = Bool -- Defined at T7939.hs:9:15
F :: * -> *
type family G a :: *
where G Int = Bool
type family G a :: * where
G Int = Bool
-- Defined at T7939.hs:11:1
G :: * -> *
type family H (a :: Bool) :: Bool
where H 'False = 'True
type family H (a :: Bool) :: Bool where
H 'False = 'True
-- Defined at T7939.hs:14:1
H :: Bool -> Bool
type family J (a :: [k]) :: Bool
where
J '[] = 'False
J (h : t) = 'True
type family J (a :: [k]) :: Bool where
J '[] = 'False
forall k (h :: k) (t :: [k]). J (h : t) = 'True
-- Defined at T7939.hs:17:1
J :: [k] -> Bool
type family K (a1 :: [a]) :: Maybe a
where
K '[] = 'Nothing
K (h : t) = 'Just h
type family K (a1 :: [a]) :: Maybe a where
K '[] = 'Nothing
forall a (h :: a) (t :: [a]). K (h : t) = 'Just h
-- Defined at T7939.hs:21:1
K :: [a] -> Maybe a
data family Sing (a :: k) -- Defined at T8674.hs:4:1
data instance Sing Bool = SBool -- Defined at T8674.hs:6:15
data instance Sing a = SNil -- Defined at T8674.hs:5:15
data instance forall k (a :: [k]). Sing a = SNil
-- Defined at T8674.hs:5:15
......@@ -21,7 +21,7 @@ data GHC.TypeLits.SomeSymbol
GHC.TypeLits.KnownSymbol n =>
GHC.TypeLits.SomeSymbol (Data.Proxy.Proxy n)
type family GHC.TypeLits.TypeError (a :: GHC.TypeLits.ErrorMessage)
:: b
:: b where
GHC.TypeLits.natVal ::
GHC.TypeNats.KnownNat n => proxy n -> Integer
GHC.TypeLits.natVal' ::
......
......@@ -288,4 +288,5 @@ test('T15568', normal, ghci_script, ['T15568.script'])
test('T15325', normal, ghci_script, ['T15325.script'])
test('T15591', normal, ghci_script, ['T15591.script'])
test('T15743b', normal, ghci_script, ['T15743b.script'])
test('T15827', normal, ghci_script, ['T15827.script'])
test('T15898', normal, ghci_script, ['T15898.script'])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment