Commit 2f3ea952 authored by Simon Peyton Jones's avatar Simon Peyton Jones
Browse files

Print for-alls more often (Trac #9018)

We now display the foralls of a type if any of the type variables
is polykinded.  This put kind polymorphism "in your face" a bit more
often, but eliminates a lot of head scratching.

The user manual reflects the new behaviour.
parent 7b967afa
......@@ -156,19 +156,16 @@ pprId ident
pprTypeForUser :: Type -> SDoc
-- We do two things here.
-- a) We tidy the type, regardless
-- b) If Opt_PrintExplicitForAlls is True, we discard the foralls
-- but we do so `deeply'
-- b) Swizzle the foralls to the top, so that without
-- -fprint-explicit-foralls we'll suppress all the foralls
-- Prime example: a class op might have type
-- forall a. C a => forall b. Ord b => stuff
-- Then we want to display
-- (C a, Ord b) => stuff
pprTypeForUser ty
= sdocWithDynFlags $ \ dflags ->
if gopt Opt_PrintExplicitForalls dflags
then ppr tidy_ty
else ppr (mkPhiTy ctxt ty')
= pprSigmaType (mkSigmaTy tvs ctxt tau)
where
(_, ctxt, ty') = tcSplitSigmaTy tidy_ty
(tvs, ctxt, tau) = tcSplitSigmaTy tidy_ty
(_, tidy_ty) = tidyOpenType emptyTidyEnv ty
-- Often the types/kinds we print in ghci are fully generalised
-- and have no free variables, but it turns out that we sometimes
......
......@@ -1741,11 +1741,14 @@ pprSkolInfo ArrowSkol = ptext (sLit "the arrow form")
pprSkolInfo (PatSkol cl mc) = case cl of
RealDataCon dc -> sep [ ptext (sLit "a pattern with constructor")
, nest 2 $ ppr dc <+> dcolon
<+> ppr (dataConUserType dc) <> comma
<+> pprType (dataConUserType dc) <> comma
-- pprType prints forall's regardless of -fprint-explict-foralls
-- which is what we want here, since we might be saying
-- type variable 't' is bound by ...
, ptext (sLit "in") <+> pprMatchContext mc ]
PatSynCon ps -> sep [ ptext (sLit "a pattern with pattern synonym")
, nest 2 $ ppr ps <+> dcolon
<+> ppr (varType (patSynId ps)) <> comma
<+> pprType (varType (patSynId ps)) <> comma
, ptext (sLit "in") <+> pprMatchContext mc ]
pprSkolInfo (InferSkol ids) = sep [ ptext (sLit "the inferred type of")
, vcat [ ppr name <+> dcolon <+> ppr ty
......
......@@ -603,6 +603,8 @@ ppr_type p fun_ty@(FunTy ty1 ty2)
ppr_forall_type :: Prec -> Type -> SDoc
ppr_forall_type p ty
= maybeParen p FunPrec $ ppr_sigma_type True ty
-- True <=> we always print the foralls on *nested* quantifiers
-- Opt_PrintExplicitForalls only affects top-level quantifiers
ppr_tvar :: TyVar -> SDoc
ppr_tvar tv -- Note [Infix type variables]
......@@ -618,24 +620,22 @@ ppr_tylit _ tl =
ppr_sigma_type :: Bool -> Type -> SDoc
-- Bool <=> Show the foralls
ppr_sigma_type show_foralls ty
= sdocWithDynFlags $ \ dflags ->
let filtered_tvs | gopt Opt_PrintExplicitKinds dflags
= tvs
| otherwise
= filterOut isKindVar tvs
in sep [ ppWhen show_foralls (pprForAll filtered_tvs)
, pprThetaArrowTy ctxt
, pprType tau ]
= sep [ ppWhen (show_foralls || any tv_has_kind_var tvs)
(pprForAll tvs)
-- See Note [When to print foralls]
, pprThetaArrowTy ctxt
, pprType tau ]
where
(tvs, rho) = split1 [] ty
(ctxt, tau) = split2 [] rho
split1 tvs (ForAllTy tv ty) = split1 (tv:tvs) ty
split1 tvs ty = (reverse tvs, ty)
split1 tvs ty = (reverse tvs, ty)
split2 ps (ty1 `FunTy` ty2) | isPredTy ty1 = split2 (ty1:ps) ty2
split2 ps ty = (reverse ps, ty)
tv_has_kind_var tv = not (isEmptyVarSet (tyVarsOfType (tyVarKind tv)))
pprSigmaType :: Type -> SDoc
pprSigmaType ty = sdocWithDynFlags $ \dflags ->
......@@ -656,6 +656,24 @@ pprTvBndr tv
kind = tyVarKind tv
\end{code}
Note [When to print foralls]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Mostly we want to print top-level foralls when (and only when) the user specifies
-fprint-explicit-foralls. But when kind polymorphism is at work, that suppresses
too much information; see Trac #9018.
So I'm trying out this rule: print explicit foralls if
a) User specifies -fprint-explicit-foralls, or
b) Any of the quantified type variables has a kind
that mentions a kind variable
This catches common situations, such as a type siguature
f :: m a
which means
f :: forall k. forall (m :: k->*) (a :: k). m a
We really want to see both the "forall k" and the kind signatures
on m and a. The latter comes from pprTvBndr.
Note [Infix type variables]
~~~~~~~~~~~~~~~~~~~~~~~~~~~
With TypeOperators you can say
......
......@@ -899,20 +899,37 @@ ghci> :set -fprint-explicit-foralls
ghci> :t f
f :: forall a. a -> a
</screen>
Using <option>-fprint-explicit-kinds</option> makes GHC print kind-foralls and kind applications
However, regardless of the flag setting, the quantifiers are printed under these circumstances:
<itemizedlist>
<listitem><para>For nested <literal>foralls</literal>, e.g.
<screen>
ghci> :t GHC.ST.runST
GHC.ST.runST :: (forall s. GHC.ST.ST s a) -> a
</screen>
</para></listitem>
<listitem><para>If any of the quantified type variables has a kind
that mentions a kind variable, e.g.
<screen>
ghci> :i Data.Coerce.coerce
coerce ::
forall (k :: BOX) (a :: k) (b :: k). Coercible a b => a -> b
-- Defined in GHC.Prim
</screen>
</para></listitem>
</itemizedlist>
</para>
<para>
Using <option>-fprint-explicit-kinds</option> makes GHC print kind arguments
in types, which are normally suppressed. This can be important when you are using kind polymorphism.
For example:
<screen>
ghci> :set -XPolyKinds
ghci> data T a = MkT
ghci> :t MkT
MkT :: T b
MkT :: forall (k :: BOX) (a :: k). T a
ghci> :set -fprint-explicit-foralls
ghci> :t MkT
MkT :: forall (b::k). T b
ghci> :set -fprint-explicit-kinds
ghci> :t MkT
MkT :: forall (k::BOX) (b:k). T b
MkT :: forall (k :: BOX) (a :: k). T k a
</screen>
</para>
</listitem>
......
data D1 where
MkD1 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D1
MkD1 :: (forall (k :: BOX) (p :: k -> *) (a :: k).
p a -> Int) -> D1
-- Defined at <interactive>:3:1
data D2 where
MkD2 :: (forall (p :: k -> *) (a :: k). p a -> Int) -> D2
......
type role Coercible representational representational
class Coercible (a :: k) (b :: k)
-- Defined in ‘GHC.Types’
coerce :: Coercible a b => a -> b -- Defined in ‘GHC.Prim’
coerce ::
forall (k :: BOX) (a :: k) (b :: k). Coercible a b => a -> b
-- Defined in ‘GHC.Prim’
......@@ -3,7 +3,7 @@ T7786.hs:86:22:
Couldn't match type ‘xxx’ with ‘'Empty’
Inaccessible code in
a pattern with constructor
Nil :: Sing 'Empty,
Nil :: forall (k :: BOX). Sing 'Empty,
in a pattern binding in
'do' block
In the pattern: Nil
......
......@@ -7,13 +7,13 @@ T7230.hs:48:32:
at T7230.hs:47:10-68
or from (xs ~ (x : xs1))
bound by a pattern with constructor
SCons :: forall (x :: k) (xs :: [k]).
SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘crash’
at T7230.hs:48:8-27
or from (xs1 ~ (x1 : xs2))
bound by a pattern with constructor
SCons :: forall (x :: k) (xs :: [k]).
SCons :: forall (k :: BOX) (x :: k) (xs :: [k]).
Sing x -> Sing xs -> Sing (x : xs),
in an equation for ‘crash’
at T7230.hs:48:17-26
......
......@@ -4,7 +4,7 @@ T7438.hs:6:14:
‘t’ is untouchable
inside the constraints (t2 ~ t3)
bound by a pattern with constructor
Nil :: forall (a :: k). Thrist a a,
Nil :: forall (k :: BOX) (a :: k). Thrist a a,
in an equation for ‘go’
at T7438.hs:6:4-6
‘t’ is a rigid type variable bound by
......
......@@ -6,7 +6,8 @@ T8566.hs:31:9:
bound by the instance declaration at T8566.hs:29:10-67
or from ('AA t (a : as) ~ 'AA t1 as1)
bound by a pattern with constructor
A :: forall (r :: [*]) (t :: k) (as :: [U *]). I ('AA t as) r,
A :: forall (r :: [*]) (k :: BOX) (t :: k) (as :: [U *]).
I ('AA t as) r,
in an equation for ‘c’
at T8566.hs:31:5
The type variable ‘fs0’ is ambiguous
......
......@@ -14,7 +14,7 @@ TYPE CONSTRUCTORS
RecFlag NonRecursive, Promotable
= K2 :: forall a. a -> T2 a Stricts: _
FamilyInstance: none
T3 :: k -> *
T3 :: forall (k :: BOX). k -> *
data T3 (k::BOX) (a::k)
No C type associated
Roles: [nominal, phantom]
......@@ -35,14 +35,14 @@ TYPE CONSTRUCTORS
RecFlag NonRecursive, Promotable
= K5 :: forall a. a -> T5 a Stricts: _
FamilyInstance: none
T6 :: k -> *
T6 :: forall (k :: BOX). k -> *
data T6 (k::BOX) (a::k)
No C type associated
Roles: [nominal, phantom]
RecFlag NonRecursive, Not promotable
= K6 :: forall (k::BOX) (a::k). T6 k a
FamilyInstance: none
T7 :: k -> * -> *
T7 :: forall (k :: BOX). k -> * -> *
data T7 (k::BOX) (a::k) b
No C type associated
Roles: [nominal, phantom, representational]
......
TYPE SIGNATURES
TYPE CONSTRUCTORS
T :: k -> *
T :: forall (k :: BOX). k -> *
data T (k::BOX) (a::k)
No C type associated
Roles: [nominal, representational]
......
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