Commit f5d20838 authored by Ryan Scott's avatar Ryan Scott Committed by Ben Gamari

Overhaul -fprint-explicit-kinds to use VKA

This patch changes the behavior of `-fprint-explicit-kinds`
so that it displays kind argument using visible kind application.
In other words, the flag now:

1. Prints instantiations of specified variables with `@(...)`.
2. Prints instantiations of inferred variables with `@{...}`.

In addition, this patch removes the `Use -fprint-explicit-kinds to
see the kind arguments` error message that often arises when a type
mismatch occurs due to different kinds. Instead, whenever there is a
kind mismatch, we now enable the `-fprint-explicit-kinds` flag
locally to help cue to the programmer where the error lies.
(See `Note [Kind arguments in error messages]` in `TcErrors`.)
As a result, these funny `@{...}` things can now appear to the user
even without turning on the `-fprint-explicit-kinds` flag explicitly,
so I took the liberty of documenting them in the users' guide.

Test Plan: ./validate

Reviewers: goldfire, simonpj, bgamari

Reviewed By: simonpj

Subscribers: rwbarton, carter

GHC Trac Issues: #15871

Differential Revision: https://phabricator.haskell.org/D5314
parent ff619555
......@@ -740,6 +740,6 @@ rnIfaceForAllBndr :: Rename IfaceForAllBndr
rnIfaceForAllBndr (Bndr tv vis) = Bndr <$> rnIfaceBndr tv <*> pure vis
rnIfaceAppArgs :: Rename IfaceAppArgs
rnIfaceAppArgs (IA_Invis t ts) = IA_Invis <$> rnIfaceType t <*> rnIfaceAppArgs ts
rnIfaceAppArgs (IA_Vis t ts) = IA_Vis <$> rnIfaceType t <*> rnIfaceAppArgs ts
rnIfaceAppArgs (IA_Arg t a ts) = IA_Arg <$> rnIfaceType t <*> pure a
<*> rnIfaceAppArgs ts
rnIfaceAppArgs IA_Nil = pure IA_Nil
......@@ -385,7 +385,7 @@ updateVarTypeM f id = do { ty' <- f (varType id)
-- See Note [VarBndrs, TyCoVarBinders, TyConBinders, and visibility] in TyCoRep
data ArgFlag = Inferred | Specified | Required
deriving (Eq, Ord, Data)
-- (<) on ArgFlag meant "is less visible than"
-- (<) on ArgFlag means "is less visible than"
-- | Does this 'ArgFlag' classify an argument that is written in Haskell?
isVisibleArgFlag :: ArgFlag -> Bool
......
......@@ -954,9 +954,7 @@ pprIfaceTyConParent :: IfaceTyConParent -> SDoc
pprIfaceTyConParent IfNoParent
= Outputable.empty
pprIfaceTyConParent (IfDataInstance _ tc tys)
= sdocWithDynFlags $ \dflags ->
let ftys = stripInvisArgs dflags tys
in pprIfaceTypeApp topPrec tc ftys
= pprIfaceTypeApp topPrec tc tys
pprIfaceDeclHead :: IfaceContext -> ShowSub -> Name
-> [IfaceTyConBinder] -- of the tycon, for invisible-suppression
......@@ -1414,8 +1412,7 @@ freeNamesIfKind :: IfaceType -> NameSet
freeNamesIfKind = freeNamesIfType
freeNamesIfAppArgs :: IfaceAppArgs -> NameSet
freeNamesIfAppArgs (IA_Vis t ts) = freeNamesIfType t &&& freeNamesIfAppArgs ts
freeNamesIfAppArgs (IA_Invis k ks) = freeNamesIfKind k &&& freeNamesIfAppArgs ks
freeNamesIfAppArgs (IA_Arg t _ ts) = freeNamesIfType t &&& freeNamesIfAppArgs ts
freeNamesIfAppArgs IA_Nil = emptyNameSet
freeNamesIfType :: IfaceType -> NameSet
......
This diff is collapsed.
......@@ -305,14 +305,13 @@ toIfaceAppArgsX fr kind ty_args
| Just ty' <- coreView ty
= go env ty' ts
go env (ForAllTy (Bndr tv vis) res) (t:ts)
| isVisibleArgFlag vis = IA_Vis t' ts'
| otherwise = IA_Invis t' ts'
= IA_Arg t' vis ts'
where
t' = toIfaceTypeX fr t
ts' = go (extendTCvSubst env tv t) res ts
go env (FunTy _ res) (t:ts) -- No type-class args in tycon apps
= IA_Vis (toIfaceTypeX fr t) (go env res ts)
= IA_Arg (toIfaceTypeX fr t) Required (go env res ts)
go env ty ts@(t1:ts1)
| not (isEmptyTCvSubst env)
......@@ -326,7 +325,7 @@ toIfaceAppArgsX fr kind ty_args
-- carry on as if it were FunTy. Without the test for
-- isEmptyTCvSubst we'd get an infinite loop (Trac #15473)
WARN( True, ppr kind $$ ppr ty_args )
IA_Vis (toIfaceTypeX fr t1) (go env ty ts1)
IA_Arg (toIfaceTypeX fr t1) Required (go env ty ts1)
tidyToIfaceType :: TidyEnv -> Type -> IfaceType
tidyToIfaceType env ty = toIfaceType (tidyType env ty)
......
......@@ -894,8 +894,9 @@ conflictInjInstErr conflictingEqns errorBuilder tyfamEqn
unusedInjectiveVarsErr :: Pair TyVarSet -> InjErrorBuilder -> CoAxBranch
-> (SDoc, SrcSpan)
unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
= errorBuilder (injectivityErrorHerald True $$ msg)
[tyfamEqn]
= let (doc, loc) = errorBuilder (injectivityErrorHerald True $$ msg)
[tyfamEqn]
in (pprWithExplicitKindsWhen has_kinds doc, loc)
where
tvs = invis_vars `unionVarSet` vis_vars
has_types = not $ isEmptyVarSet vis_vars
......@@ -909,9 +910,7 @@ unusedInjectiveVarsErr (Pair invis_vars vis_vars) errorBuilder tyfamEqn
(True, False) -> text "Type"
(False, True) -> text "Kind"
(False, False) -> pprPanic "mkUnusedInjectiveVarsErr" $ ppr tvs
print_kinds_info = ppWhen has_kinds ppSuggestExplicitKinds
msg = doc $$ print_kinds_info $$
text "In the type family equation:"
msg = doc $$ text "In the type family equation:"
-- | Build error message for equation that has a type family call at the top
-- level of RHS
......
......@@ -394,7 +394,9 @@ checkInstCoverage be_liberal clas theta inst_taus
undet_set = fold undetermined_tvs
msg = vcat [ -- text "ls_tvs" <+> ppr ls_tvs
msg = pprWithExplicitKindsWhen
(isEmptyVarSet $ pSnd undetermined_tvs) $
vcat [ -- text "ls_tvs" <+> ppr ls_tvs
-- , text "closed ls_tvs" <+> ppr (closeOverKinds ls_tvs)
-- , text "theta" <+> ppr theta
-- , text "oclose" <+> ppr (oclose theta (closeOverKinds ls_tvs))
......@@ -414,8 +416,6 @@ checkInstCoverage be_liberal clas theta inst_taus
<+> pprQuotedList rs ]
, text "Un-determined variable" <> pluralVarSet undet_set <> colon
<+> pprVarSet undet_set (pprWithCommas ppr)
, ppWhen (isEmptyVarSet $ pSnd undetermined_tvs) $
ppSuggestExplicitKinds
, ppWhen (not be_liberal &&
and (isEmptyVarSet <$> liberal_undet_tvs)) $
text "Using UndecidableInstances might help" ]
......
......@@ -1762,9 +1762,8 @@ mkEqInfoMsg :: Ct -> TcType -> TcType -> SDoc
-- (b) warning about injectivity if both sides are the same
-- type function application F a ~ F b
-- See Note [Non-injective type functions]
-- (c) warning about -fprint-explicit-kinds if that might be helpful
mkEqInfoMsg ct ty1 ty2
= tyfun_msg $$ ambig_msg $$ invis_msg
= tyfun_msg $$ ambig_msg
where
mb_fun1 = isTyFun_maybe ty1
mb_fun2 = isTyFun_maybe ty2
......@@ -1773,19 +1772,6 @@ mkEqInfoMsg ct ty1 ty2
= snd (mkAmbigMsg False ct)
| otherwise = empty
-- better to check the exp/act types in the CtOrigin than the actual
-- mismatched types for suggestion about -fprint-explicit-kinds
(act_ty, exp_ty) = case ctOrigin ct of
TypeEqOrigin { uo_actual = act
, uo_expected = exp } -> (act, exp)
_ -> (ty1, ty2)
invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
, not vis
= ppSuggestExplicitKinds
| otherwise
= empty
tyfun_msg | Just tc1 <- mb_fun1
, Just tc2 <- mb_fun2
, tc1 == tc2
......@@ -1940,6 +1926,7 @@ misMatchMsg ct oriented ty1 ty2
| otherwise -- So now we have Nothing or (Just IsSwapped)
-- For some reason we treat Nothing like IsSwapped
= addArising orig $
pprWithExplicitKindsWhenMismatch ty1 ty2 (ctOrigin ct) $
sep [ text herald1 <+> quotes (ppr ty1)
, nest padding $
text herald2 <+> quotes (ppr ty2)
......@@ -1974,13 +1961,37 @@ misMatchMsg ct oriented ty1 ty2
= addArising orig $
text "Couldn't match a lifted type with an unlifted type"
-- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a
-- type mismatch occurs to due invisible kind arguments.
--
-- This function first checks to see if the 'CtOrigin' argument is a
-- 'TypeEqOrigin', and if so, uses the expected/actual types from that to
-- check for a kind mismatch (as these types typically have more surrounding
-- types and are likelier to be able to glean information about whether a
-- mismatch occurred in an invisible argument position or not). If the
-- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types
-- themselves.
pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
-> SDoc -> SDoc
pprWithExplicitKindsWhenMismatch ty1 ty2 ct =
pprWithExplicitKindsWhen mismatch
where
(act_ty, exp_ty) = case ct of
TypeEqOrigin { uo_actual = act
, uo_expected = exp } -> (act, exp)
_ -> (ty1, ty2)
mismatch | Just vis <- tcEqTypeVis act_ty exp_ty
= not vis
| otherwise
= False
mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
-> (Bool, Maybe SwapFlag, SDoc)
-- NotSwapped means (actual, expected), IsSwapped is the reverse
-- First return val is whether or not to print a herald above this msg
mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
, uo_expected = exp
, uo_thing = maybe_thing })
mkExpectedActualMsg ty1 ty2 ct@(TypeEqOrigin { uo_actual = act
, uo_expected = exp
, uo_thing = maybe_thing })
m_level printExpanded
| KindLevel <- level, occurs_check_error = (True, Nothing, empty)
| isUnliftedTypeKind act, isLiftedTypeKind exp = (False, Nothing, msg2)
......@@ -2014,7 +2025,8 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
-> msg5 th
_ | not (act `pickyEqType` exp)
-> vcat [ text "Expected" <+> sort <> colon <+> ppr exp
-> pprWithExplicitKindsWhenMismatch ty1 ty2 ct $
vcat [ text "Expected" <+> sort <> colon <+> ppr exp
, text " Actual" <+> sort <> colon <+> ppr act
, if printExpanded then expandedTys else empty ]
......@@ -2036,7 +2048,8 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
maybe_thing
, quotes (pprWithTYPE act) ]
msg5 th = hang (text "Expected" <+> kind_desc <> comma)
msg5 th = pprWithExplicitKindsWhenMismatch ty1 ty2 ct $
hang (text "Expected" <+> kind_desc <> comma)
2 (text "but" <+> quotes th <+> text "has kind" <+>
quotes (ppr act))
where
......@@ -2819,15 +2832,26 @@ Re-flattening is pretty easy, because we don't need to keep track of
evidence. We don't re-use the code in TcCanonical because that's in
the TcS monad, and we are in TcM here.
Note [Suggest -fprint-explicit-kinds]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Note [Kind arguments in error messages]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
It can be terribly confusing to get an error message like (Trac #9171)
Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
The reason may be that the kinds don't match up. Typically you'll get
more useful information, but not when it's as a result of ambiguity.
This test suggests -fprint-explicit-kinds when all the ambiguous type
variables are kind variables.
To mitigate this, GHC attempts to enable the -fprint-explicit-kinds flag
whenever any error message arises due to a kind mismatch. This means that
the above error message would instead be displayed as:
Couldn't match expected type
‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
with actual type
‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’
Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
-}
mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
......@@ -2847,10 +2871,8 @@ mkAmbigMsg prepend_msg ct
| not (null ambig_tvs)
= pp_ambig (text "type") ambig_tvs
| otherwise -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
-- See Note [Suggest -fprint-explicit-kinds]
= vcat [ pp_ambig (text "kind") ambig_kvs
, ppSuggestExplicitKinds ]
| otherwise
= pp_ambig (text "kind") ambig_kvs
pp_ambig what tkvs
| prepend_msg -- "Ambiguous type variable 't0'"
......
......@@ -100,7 +100,7 @@ module TcType (
isImprovementPred,
-- * Finding type instances
tcTyFamInsts, isTyFamFree,
tcTyFamInsts, tcTyFamInstsAndVis, tcTyConAppTyFamInstsAndVis, isTyFamFree,
-- * Finding "exact" (non-dead) type variables
exactTyCoVarsOfType, exactTyCoVarsOfTypes,
......@@ -858,20 +858,85 @@ promoteSkolemsX tclvl = mapAccumL (promoteSkolemX tclvl)
-- we don't need to take <big type> into account when asking if
-- the calls on the RHS are smaller than the LHS
tcTyFamInsts :: Type -> [(TyCon, [Type])]
tcTyFamInsts ty
| Just exp_ty <- tcView ty = tcTyFamInsts exp_ty
tcTyFamInsts (TyVarTy _) = []
tcTyFamInsts (TyConApp tc tys)
| isTypeFamilyTyCon tc = [(tc, take (tyConArity tc) tys)]
| otherwise = concat (map tcTyFamInsts tys)
tcTyFamInsts (LitTy {}) = []
tcTyFamInsts (ForAllTy bndr ty) = tcTyFamInsts (binderType bndr)
++ tcTyFamInsts ty
tcTyFamInsts (FunTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
tcTyFamInsts (AppTy ty1 ty2) = tcTyFamInsts ty1 ++ tcTyFamInsts ty2
tcTyFamInsts (CastTy ty _) = tcTyFamInsts ty
tcTyFamInsts (CoercionTy _) = [] -- don't count tyfams in coercions,
-- as they never get normalized, anyway
tcTyFamInsts = map (\(_,b,c) -> (b,c)) . tcTyFamInstsAndVis
-- | Like 'tcTyFamInsts', except that the output records whether the
-- type family and its arguments occur as an /invisible/ argument in
-- some type application. This information is useful because it helps GHC know
-- when to turn on @-fprint-explicit-kinds@ during error reporting so that
-- users can actually see the type family being mentioned.
--
-- As an example, consider:
--
-- @
-- class C a
-- data T (a :: k)
-- type family F a :: k
-- instance C (T @(F Int) (F Bool))
-- @
--
-- There are two occurrences of the type family `F` in that `C` instance, so
-- @'tcTyFamInstsAndVis' (C (T \@(F Int) (F Bool)))@ will return:
--
-- @
-- [ ('True', F, [Int])
-- , ('False', F, [Bool]) ]
-- @
--
-- @F Int@ is paired with 'True' since it appears as an /invisible/ argument
-- to @C@, whereas @F Bool@ is paired with 'False' since it appears an a
-- /visible/ argument to @C@.
--
-- See also @Note [Kind arguments in error messages]@ in "TcErrors".
tcTyFamInstsAndVis :: Type -> [(Bool, TyCon, [Type])]
tcTyFamInstsAndVis = tcTyFamInstsAndVisX False
tcTyFamInstsAndVisX
:: Bool -- ^ Is this an invisible argument to some type application?
-> Type -> [(Bool, TyCon, [Type])]
tcTyFamInstsAndVisX = go
where
go is_invis_arg ty
| Just exp_ty <- tcView ty = go is_invis_arg exp_ty
go _ (TyVarTy _) = []
go is_invis_arg (TyConApp tc tys)
| isTypeFamilyTyCon tc
= [(is_invis_arg, tc, take (tyConArity tc) tys)]
| otherwise
= tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys
go _ (LitTy {}) = []
go is_invis_arg (ForAllTy bndr ty) = go is_invis_arg (binderType bndr)
++ go is_invis_arg ty
go is_invis_arg (FunTy ty1 ty2) = go is_invis_arg ty1
++ go is_invis_arg ty2
go is_invis_arg ty@(AppTy _ _) =
let (ty_head, ty_args) = splitAppTys ty
ty_arg_flags = appTyArgFlags ty_head ty_args
in go is_invis_arg ty_head
++ concat (zipWith (\flag -> go (isInvisibleArgFlag flag))
ty_arg_flags ty_args)
go is_invis_arg (CastTy ty _) = go is_invis_arg ty
go _ (CoercionTy _) = [] -- don't count tyfams in coercions,
-- as they never get normalized,
-- anyway
-- | In an application of a 'TyCon' to some arguments, find the outermost
-- occurrences of type family applications within the arguments. This function
-- will not consider the 'TyCon' itself when checking for type family
-- applications.
--
-- See 'tcTyFamInstsAndVis' for more details on how this works (as this
-- function is called inside of 'tcTyFamInstsAndVis').
tcTyConAppTyFamInstsAndVis :: TyCon -> [Type] -> [(Bool, TyCon, [Type])]
tcTyConAppTyFamInstsAndVis = tcTyConAppTyFamInstsAndVisX False
tcTyConAppTyFamInstsAndVisX
:: Bool -- ^ Is this an invisible argument to some type application?
-> TyCon -> [Type] -> [(Bool, TyCon, [Type])]
tcTyConAppTyFamInstsAndVisX is_invis_arg tc tys =
let (invis_tys, vis_tys) = partitionInvisibleTypes tc tys
in concat $ map (tcTyFamInstsAndVisX True) invis_tys
++ map (tcTyFamInstsAndVisX is_invis_arg) vis_tys
isTyFamFree :: Type -> Bool
-- ^ Check that a type does not contain any type family applications.
......
......@@ -1788,7 +1788,7 @@ checkConsistentFamInst (Just (clas, inst_tvs, mini_env)) fam_tc at_tys pp_hs_pat
-- And now kind args
; checkTcM (all check_arg kind_shapes)
(tidy_env2, pp_wrong_at_arg $$ ppSuggestExplicitKinds)
(tidy_env2, pprWithExplicitKindsWhen True pp_wrong_at_arg)
; traceTc "checkConsistentFamInst" (vcat [ ppr inst_tvs
, ppr arg_shapes
......@@ -2001,41 +2001,27 @@ checkValidFamPats mb_clsinfo fam_tc tvs cvs user_ty_pats extra_ty_pats pp_hs_pat
-- | Checks for occurrences of type families in class instances and type/data
-- family instances.
checkValidTypePats :: TyCon -> [Type] -> TcM ()
checkValidTypePats tc pat_ty_args =
traverse_ (check_valid_type_pat False) invis_ty_args *>
traverse_ (check_valid_type_pat True) vis_ty_args
checkValidTypePats tc pat_ty_args = do
-- Check that each of pat_ty_args is a monotype.
-- One could imagine generalising to allow
-- instance C (forall a. a->a)
-- but we don't know what all the consequences might be.
traverse_ checkValidMonoType pat_ty_args
-- Ensure that no type family instances occur a type pattern
case tcTyConAppTyFamInstsAndVis tc pat_ty_args of
[] -> pure ()
((tf_is_invis_arg, tf_tc, tf_args):_) -> failWithTc $
ty_fam_inst_illegal_err tf_is_invis_arg (mkTyConApp tf_tc tf_args)
where
(invis_ty_args, vis_ty_args) = partitionInvisibleTypes tc pat_ty_args
inst_ty = mkTyConApp tc pat_ty_args
check_valid_type_pat
:: Bool -- True if this is an /visible/ argument to the TyCon.
-> Type -> TcM ()
-- Used for type patterns in class instances,
-- and in type/data family instances
check_valid_type_pat vis_arg pat_ty
= do { -- Check that pat_ty is a monotype
checkValidMonoType pat_ty
-- One could imagine generalising to allow
-- instance C (forall a. a->a)
-- but we don't know what all the consequences might be
-- Ensure that no type family instances occur a type pattern
; case tcTyFamInsts pat_ty of
[] -> pure ()
((tf_tc, tf_args):_) ->
failWithTc $
ty_fam_inst_illegal_err vis_arg (mkTyConApp tf_tc tf_args) }
ty_fam_inst_illegal_err :: Bool -> Type -> SDoc
ty_fam_inst_illegal_err vis_arg ty
= sdocWithDynFlags $ \dflags ->
ty_fam_inst_illegal_err invis_arg ty
= pprWithExplicitKindsWhen invis_arg $
hang (text "Illegal type synonym family application"
<+> quotes (ppr ty) <+> text "in instance" <>
colon) 2 $
vcat [ ppr inst_ty
, ppUnless (vis_arg || gopt Opt_PrintExplicitKinds dflags) $
text "Use -fprint-explicit-kinds to see the kind arguments" ]
<+> quotes (ppr ty) <+> text "in instance" <> colon)
2 (ppr inst_ty)
-- Error messages
......
......@@ -69,7 +69,7 @@ module TyCoRep (
pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprTyLit,
PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
pprDataCons, ppSuggestExplicitKinds,
pprDataCons, pprWithExplicitKindsWhen,
pprCo, pprParendCo,
......@@ -3356,13 +3356,14 @@ pprTypeApp tc tys
-- TODO: toIfaceTcArgs seems rather wasteful here
------------------
ppSuggestExplicitKinds :: SDoc
-- Print a helpful suggstion about -fprint-explicit-kinds,
-- if it is not already on
ppSuggestExplicitKinds
= sdocWithDynFlags $ \ dflags ->
ppUnless (gopt Opt_PrintExplicitKinds dflags) $
text "Use -fprint-explicit-kinds to see the kind arguments"
-- | Display all kind information (with @-fprint-explicit-kinds@) when the
-- provided 'Bool' argument is 'True'.
-- See @Note [Kind arguments in error messages]@ in "TcErrors".
pprWithExplicitKindsWhen :: Bool -> SDoc -> SDoc
pprWithExplicitKindsWhen b
= updSDocDynFlags $ \dflags ->
if b then gopt_set dflags Opt_PrintExplicitKinds
else dflags
{-
%************************************************************************
......
......@@ -204,7 +204,7 @@ module Type (
pprType, pprParendType, pprPrecType,
pprTypeApp, pprTyThingCategory, pprShortTyThing,
pprTCvBndr, pprTCvBndrs, pprForAll, pprUserForAll,
pprSigmaType, ppSuggestExplicitKinds,
pprSigmaType, pprWithExplicitKindsWhen,
pprTheta, pprThetaArrowTy, pprClassPred,
pprKind, pprParendKind, pprSourceTyCon,
PprPrec(..), topPrec, sigPrec, opPrec, funPrec, appPrec, maybeParen,
......@@ -1617,6 +1617,8 @@ appTyArgFlags ty = fun_kind_arg_flags (typeKind ty)
fun_kind_arg_flags :: Kind -> [Type] -> [ArgFlag]
fun_kind_arg_flags = go emptyTCvSubst
where
go subst ki arg_tys
| Just ki' <- coreView ki = go subst ki' arg_tys
go _ _ [] = []
go subst (ForAllTy (Bndr tv argf) res_ki) (arg_ty:arg_tys)
= argf : go subst' res_ki arg_tys
......
......@@ -306,7 +306,7 @@ The available mode flags are:
:shortdesc: Stop after generating C (``.hc`` file)
:type: mode
:category: phases
Stop after generating C (``.hc`` file)
.. ghc-flag:: -S
......@@ -320,7 +320,7 @@ The available mode flags are:
:shortdesc: Stop after generating object (``.o``) file
:type: mode
:category: phases
Stop after generating object (``.o``) file
This is the traditional batch-compiler mode, in which GHC can
......@@ -770,7 +770,7 @@ messages and in GHCi:
This flag also enables the printing of *inferred* type variables
inside braces. See :ref:`inferred-vs-specified`.
.. ghc-flag:: -fprint-explicit-kinds
:shortdesc: Print explicit kind foralls and kind arguments in types.
See also :ghc-flag:`-XKindSignatures`
......@@ -785,15 +785,27 @@ messages and in GHCi:
.. code-block:: none
ghci> :set -XPolyKinds
ghci> data T a = MkT
ghci> data T a (b :: l) = MkT
ghci> :t MkT
MkT :: forall (k :: Type) (a :: k). T a
MkT :: forall k l (a :: k) (b :: l). T a b
ghci> :set -fprint-explicit-kinds
ghci> :t MkT
MkT :: forall (k :: Type) (a :: k). T k a
MkT :: forall k l (a :: k) (b :: l). T @{k} @l a b
ghci> :set -XNoPolyKinds
ghci> :t MkT
MkT :: T * a
MkT :: T @{*} @* a b
In the output above, observe that ``T`` has two kind variables
(``k`` and ``l``) and two type variables (``a`` and ``b``). Note that
``k`` is an *inferred* variable and ``l`` is a *specified* variable
(see :ref:`inferred-vs-specified`), so as a result, they are displayed
using slightly different syntax in the type ``T @{k} @l a b``. The
application of ``l`` (with ``@l``) is the standard syntax for visible
type application (see :ref:`visible-type-application`). The application
of ``k`` (with ``@{k}``), however, uses a hypothetical syntax for visible
type application of inferred type variables. This syntax is not currently
exposed to the programmer, but it is nevertheless displayed when
:ghc-flag:`-fprint-explicit-kinds` is enabled.
.. ghc-flag:: -fprint-explicit-runtime-reps
:shortdesc: Print ``RuntimeRep`` variables in types which are
......
T15825.hs:14:29: error:
• Illegal type synonym family application ‘GHC.Types.Any’ in instance:
X a
• Illegal type synonym family application ‘GHC.Types.Any
@k’ in instance:
X (a @(GHC.Types.Any @k))
• In the instance declaration for ‘X (a :: *)’
......@@ -14,4 +14,4 @@ $(unboxedTupleT 2) :: forall (k0 :: RuntimeRep) (k1 :: RuntimeRep).
-> TYPE k1
-> TYPE
('TupleRep
((':) RuntimeRep k0 ((':) RuntimeRep k1 ('[] RuntimeRep))))
((':) @RuntimeRep k0 ((':) @RuntimeRep k1 ('[] @RuntimeRep))))
bar @Int :: Int -> b -> Int
bar @Int :: forall {b}. Int -> b -> Int
prox :: forall {k} {a :: k}. Prox k a
prox @Int :: Prox * Int
Prox :: forall {k} {a :: k}. Prox k a
Prox @Int :: Prox * Int
prox :: forall {k} {a :: k}. Prox @{k} a
prox @Int :: Prox @{*} Int
Prox :: forall {k} {a :: k}. Prox @{k} a
Prox @Int :: Prox @{*} Int
type family Foo (a :: k) :: k
where 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 Foo @k a = a
-- Defined at T15341.hs:5:1
......@@ -40,33 +40,31 @@
<interactive>:55:41: error:
Type family equation violates injectivity annotation.
Kind variable ‘k2’ cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
PolyKindVarsF '[] = '[] -- Defined at <interactive>:55:41
PolyKindVarsF @{[k2]} @[k1] ('[] @k2) = '[] @k1
-- Defined at <interactive>:55:41
<interactive>:60:15: error:
Type family equation violates injectivity annotation.
Kind variable ‘k1’ cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
PolyKindVars '[] = '[] -- Defined at <interactive>:60:15
PolyKindVars @[k1] @[k2] ('[] @k1) = '[] @k2
-- Defined at <interactive>:60:15
<interactive>:64:15: error:
Type family equation violates injectivity annotation.
Kind variable ‘k’ cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
forall k (a :: k) (b :: k).
Fc a b = Int -- Defined at <interactive>:64:15
Fc @k a b = Int -- Defined at <interactive>:64:15
<interactive>:68:15: error:
Type family equation violates injectivity annotation.
Type and kind variables ‘k’, ‘a’, ‘b’
cannot be inferred from the right-hand side.
Use -fprint-explicit-kinds to see the kind arguments
In the type family equation:
forall k (a :: k) (b :: k).
Gc a b = Int -- Defined at <interactive>:68:15
Gc @k a b = Int -- Defined at <interactive>:68:15
<interactive>:81:15: error:
Type family equations violate injectivity annotation:
......
T9171.hs:10:20: error:
• Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
with actual type ‘GetParam Base (GetParam Base Int)’
• Couldn't match expected type ‘GetParam
@* @k2 @* Base (GetParam @* @* @k2 Base Int)’
with actual type ‘GetParam
@* @k20 @* Base (GetParam @* @* @k20 Base Int)’
NB: ‘GetParam’ is a non-injective type family
The type variable ‘k20’ is ambiguous
Use -fprint-explicit-kinds to see the kind arguments
• In the ambiguity check for an expression type signature
To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
In an expression type signature: GetParam Base (GetParam Base Int)
......
......@@ -37,21 +37,21 @@ T15039b.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
ex3 :: Dict ((a :: *) ~~ (b :: k)) -> () (bound at T15039b.hs:25:1)
T15039b.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘Dict (Coercible * a b)’
• Found type wildcard ‘_’ standing for ‘Dict (Coercible @* a b)’
Where: ‘a’, ‘b’ are rigid type variables bound by
the type signature for:
ex6 :: forall a b. Dict (Coercible * a b) -> ()
ex6 :: forall a b. Dict (Coercible @* a b) -> ()
at T15039b.hs:32:1-53
• In a pattern type signature: _
In the pattern: Dict :: _
In an equation for ‘ex6’: ex6 (Dict :: _) = ()
• Relevant bindings include
ex6 :: Dict (Coercible * a b) -> () (bound at T15039b.hs:33:1)
ex6 :: Dict (Coercible @* a b) -> () (bound at T15039b.hs:33:1)
T15039b.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘Coercible * a b’
• Found type wildcard ‘_’ standing for ‘Coercible @* a b’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of ex7 :: Coercible * a b => Coercion * a b
the inferred type of ex7 :: Coercible @* a b => Coercion @{*} a b
at T15039b.hs:36:1-14
• In the type signature:
ex7 :: _ => Coercion (a :: Type) (b :: Type)
......@@ -38,21 +38,21 @@ T15039d.hs:25:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
ex3 :: Dict ((a :: *) ~~ (b :: k)) -> () (bound at T15039d.hs:25:1)
T15039d.hs:33:14: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘Dict (Coercible * a b)’
• Found type wildcard ‘_’ standing for ‘Dict (Coercible @* a b)’
Where: ‘a’, ‘b’ are rigid type variables bound by
the type signature for:
ex6 :: forall a b. Dict (Coercible * a b) -> ()
ex6 :: forall a b. Dict (Coercible @* a b) -> ()
at T15039d.hs:32:1-53
• In a pattern type signature: _
In the pattern: Dict :: _
In an equation for ‘ex6’: ex6 (Dict :: _) = ()
• Relevant bindings include
ex6 :: Dict (Coercible * a b) -> () (bound at T15039d.hs:33:1)
ex6 :: Dict (Coercible @* a b) -> () (bound at T15039d.hs:33:1)
T15039d.hs:35:8: warning: [-Wpartial-type-signatures (in -Wdefault)]
• Found type wildcard ‘_’ standing for ‘Coercible * a b’
• Found type wildcard ‘_’ standing for ‘Coercible @* a b’
Where: ‘a’, ‘b’ are rigid type variables bound by
the inferred type of ex7 :: Coercible * a b => Coercion * a b
the inferred type of ex7 :: Coercible @* a b => Coercion @{*} a b
at T15039d.hs:36:1-14
• In the type signature:
ex7 :: _ => Coercion (a :: Type) (b :: Type)
......@@ -3,7 +3,6 @@ T10570.hs:10:10: error:
• Illegal instance declaration for ‘ConsByIdx2 Int a Proxy cls’
The coverage condition fails in class ‘ConsByIdx2’
for functional dependency: ‘x -> m’
Reason: lhs type ‘Int’ does not determine rhs type ‘Proxy’