Commit 6655ec73 authored by Richard Eisenberg's avatar Richard Eisenberg Committed by Marge Bot

Improve documentation around empty tuples/lists

This patch also changes the way we handle empty lists, simplifying
them somewhat. See Note [Empty lists]. Previously, we had to
special-case empty lists in the type-checker. Now no more!

Finally, this patch improves some documentation around the ir_inst
field used in the type-checker.

This breaks a test case, but I really think the problem is #17251,
not really related to this patch.

Test case: typecheck/should_compile/T13680
parent 67bf734c
......@@ -390,6 +390,7 @@ data HsExpr p
-- 'ApiAnnotation.AnnClose'
-- For details on above see note [Api annotations] in ApiAnnotation
-- Note [ExplicitTuple]
| ExplicitTuple
(XExplicitTuple p)
[LHsTupArg p]
......@@ -468,6 +469,7 @@ data HsExpr p
-- 'ApiAnnotation.AnnClose' @']'@
-- For details on above see note [Api annotations] in ApiAnnotation
-- See Note [Empty lists]
| ExplicitList
(XExplicitList p) -- Gives type of components of list
(Maybe (SyntaxExpr p))
......@@ -841,6 +843,71 @@ in the ParsedSource.
There are unfortunately enough differences between the ParsedSource and the
RenamedSource that the API Annotations cannot be used directly with
RenamedSource, so this allows a simple mapping to be used based on the location.
Note [ExplicitTuple]
~~~~~~~~~~~~~~~~~~~~
An ExplicitTuple is never just a data constructor like (,,,).
That is, the `[LHsTupArg p]` argument of `ExplicitTuple` has at least
one `Present` member (and is thus never empty).
A tuple data constructor like () or (,,,) is parsed as an `HsVar`, not an
`ExplicitTuple`, and stays that way. This is important for two reasons:
1. We don't need -XTupleSections for (,,,)
2. The type variables in (,,,) can be instantiated with visible type application.
That is,
(,,) :: forall a b c. a -> b -> c -> (a,b,c)
(True,,) :: forall {b} {c}. b -> c -> (Bool,b,c)
Note that the tuple section has *inferred* arguments, while the data
constructor has *specified* ones.
(See Note [Required, Specified, and Inferred for types] in TcTyClsDecls
for background.)
Sadly, the grammar for this is actually ambiguous, and it's only thanks to the
preference of a shift in a shift/reduce conflict that the parser works as this
Note details. Search for a reference to this Note in Parser.y for further
explanation.
Note [Empty lists]
~~~~~~~~~~~~~~~~~~
An empty list could be considered either a data constructor (stored with
HsVar) or an ExplicitList. This Note describes how empty lists flow through the
various phases and why.
Parsing
-------
An empty list is parsed by the sysdcon nonterminal. It thus comes to life via
HsVar nilDataCon (defined in TysWiredIn). A freshly-parsed (HsExpr GhcPs) empty list
is never a ExplicitList.
Renaming
--------
If -XOverloadedLists is enabled, we must type-check the empty list as if it
were a call to fromListN. (This is true regardless of the setting of
-XRebindableSyntax.) This is very easy if the empty list is an ExplicitList,
but an annoying special case if it's an HsVar. So the renamer changes a
HsVar nilDataCon to an ExplicitList [], but only if -XOverloadedLists is on.
(Why not always? Read on, dear friend.) This happens in the HsVar case of rnExpr.
Type-checking
-------------
We want to accept an expression like [] @Int. To do this, we must infer that
[] :: forall a. [a]. This is easy if [] is a HsVar with the right DataCon inside.
However, the type-checking for explicit lists works differently: [x,y,z] is never
polymorphic. Instead, we unify the types of x, y, and z together, and use the
unified type as the argument to the cons and nil constructors. Thus, treating
[] as an empty ExplicitList in the type-checker would prevent [] @Int from working.
However, if -XOverloadedLists is on, then [] @Int really shouldn't be allowed:
it's just like fromListN 0 [] @Int. Since
fromListN :: forall list. IsList list => Int -> [Item list] -> list
that expression really should be rejected. Thus, the renamer's behaviour is
exactly what we want: treat [] as a datacon when -XNoOverloadedLists, and as
an empty ExplicitList when -XOverloadedLists.
See also #13680, which requested [] @Int to work.
-}
instance (p ~ GhcPass pass, OutputableBndrId p) => Outputable (HsExpr p) where
......
......@@ -259,6 +259,8 @@ from the Haskell98 data constructor for a tuple. Shift resolves in
favor of sysdcon, which is good because a tuple section will get rejected
if -XTupleSections is not specified.
See also Note [ExplicitTuple] in GHC.Hs.Expr.
-------------------------------------------------------------------------------
state 408 contains 1 shift/reduce conflicts.
......@@ -2934,6 +2936,9 @@ texp :: { ECP }
amms (mkHsViewPatPV (comb2 $1 $>) $1 $3) [mu AnnRarrow $2] }
-- Always at least one comma or bar.
-- Though this can parse just commas (without any expressions), it won't
-- in practice, because (,,,) is parsed as a name. See Note [ExplicitTuple]
-- in GHC.Hs.Expr.
tup_exprs :: { forall b. DisambECP b => PV ([AddAnn],SumOrTuple b) }
: texp commas_tup_tail
{ runECP_PV $1 >>= \ $1 ->
......@@ -2978,6 +2983,7 @@ tup_tail :: { forall b. DisambECP b => PV [Located (Maybe (Located b))] }
-- The rules below are little bit contorted to keep lexps left-recursive while
-- avoiding another shift/reduce-conflict.
-- Never empty.
list :: { forall b. DisambECP b => SrcSpan -> PV (Located b) }
: texp { \loc -> runECP_PV $1 >>= \ $1 ->
mkHsExplicitListPV loc [$1] }
......@@ -3399,6 +3405,7 @@ con_list : con { sL1 $1 [$1] }
| con ',' con_list {% addAnnotation (gl $1) AnnComma (gl $2) >>
return (sLL $1 $> ($1 : unLoc $3)) }
-- See Note [ExplicitTuple] in GHC.Hs.Expr
sysdcon_nolist :: { Located DataCon } -- Wired in data constructors
: '(' ')' {% ams (sLL $1 $> unitDataCon) [mop $1,mcp $2] }
| '(' commas ')' {% ams (sLL $1 $> $ tupleDataCon Boxed (snd $2 + 1))
......@@ -3407,6 +3414,7 @@ sysdcon_nolist :: { Located DataCon } -- Wired in data constructors
| '(#' commas '#)' {% ams (sLL $1 $> $ tupleDataCon Unboxed (snd $2 + 1))
(mo $1:mc $3:(mcommas (fst $2))) }
-- See Note [Empty lists] in GHC.Hs.Expr
sysdcon :: { Located DataCon }
: sysdcon_nolist { $1 }
| '[' ']' {% ams (sLL $1 $> nilDataCon) [mos $1,mcs $2] }
......
......@@ -1492,6 +1492,7 @@ listTyCon =
False
(VanillaAlgTyCon $ mkPrelTyConRepName listTyConName)
-- See also Note [Empty lists] in GHC.Hs.Expr.
nilDataCon :: DataCon
nilDataCon = pcDataCon nilDataConName alpha_tyvar [] listTyCon
......
......@@ -121,11 +121,14 @@ rnUnboundVar v
rnExpr (HsVar _ (L l v))
= do { opt_DuplicateRecordFields <- xoptM LangExt.DuplicateRecordFields
; mb_name <- lookupOccRn_overloaded opt_DuplicateRecordFields v
; dflags <- getDynFlags
; case mb_name of {
Nothing -> rnUnboundVar v ;
Just (Left name)
| name == nilDataConName -- Treat [] as an ExplicitList, so that
-- OverloadedLists works correctly
-- Note [Empty lists] in GHC.Hs.Expr
, xopt LangExt.OverloadedLists dflags
-> rnExpr (ExplicitList noExtField Nothing [])
| otherwise
......
......@@ -509,6 +509,8 @@ tcExpr (ExplicitSum _ alt arity expr) res_ty
; expr' <- tcPolyExpr expr (arg_tys' `getNth` (alt - 1))
; return $ mkHsWrapCo coi (ExplicitSum arg_tys' alt arity expr' ) }
-- This will see the empty list only when -XOverloadedLists.
-- See Note [Empty lists] in GHC.Hs.Expr.
tcExpr (ExplicitList _ witness exprs) res_ty
= case witness of
Nothing -> do { res_ty <- expTypeToType res_ty
......@@ -1179,16 +1181,6 @@ tcApp m_herald fun@(L loc (HsVar _ (L _ fun_id))) args res_ty
where
n_val_args = count isHsValArg args
tcApp _ (L loc (ExplicitList _ Nothing [])) [HsTypeArg _ ty_arg] res_ty
-- See Note [Visible type application for the empty list constructor]
= do { ty_arg' <- tcHsTypeApp ty_arg liftedTypeKind
; let list_ty = TyConApp listTyCon [ty_arg']
; _ <- tcSubTypeDS (OccurrenceOf nilDataConName) GenSigCtxt
list_ty res_ty
; let expr :: LHsExpr GhcTcId
expr = L loc $ ExplicitList ty_arg' Nothing []
; return (idHsWrapper, expr, []) }
tcApp m_herald fun args res_ty
= do { (tc_fun, fun_ty) <- tcInferFun fun
; tcFunApp m_herald fun tc_fun fun_ty args res_ty }
......@@ -1240,26 +1232,6 @@ mk_app_msg fun args = sep [ text "The" <+> text what <+> quotes (ppr expr)
mk_op_msg :: LHsExpr GhcRn -> SDoc
mk_op_msg op = text "The operator" <+> quotes (ppr op) <+> text "takes"
{-
Note [Visible type application for the empty list constructor]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Getting the expression [] @Int to typecheck is slightly tricky since [] isn't
an ordinary data constructor. By default, when tcExpr typechecks a list
expression, it wraps the expression in a coercion, which gives it a type to the
effect of p[a]. It isn't until later zonking that the type becomes
forall a. [a], but that's too late for visible type application.
The workaround is to check for empty list expressions that have a visible type
argument in tcApp, and if so, directly typecheck [] @ty data constructor name.
This avoids the intermediate coercion and produces an expression of type [ty],
as one would intuitively expect.
Unfortunately, this workaround isn't terribly robust, since more involved
expressions such as (let in []) @Int won't work. Until a more elegant fix comes
along, however, this at least allows direct type application on [] to work,
which is better than before.
-}
----------------
tcInferFun :: LHsExpr GhcRn -> TcM (LHsExpr GhcTcId, TcSigmaType)
-- Infer type of a function
......
......@@ -927,35 +927,63 @@ In some cases we want to deeply instantiate before filling in
an InferResult, and in some cases not. That's why InferReult
has the ir_inst flag.
* ir_inst = True: deeply instantiate
ir_inst = True: deeply instantiate
----------------------------------
Consider
1. Consider
f x = (*)
We want to instantiate the type of (*) before returning, else we
will infer the type
f :: forall {a}. a -> forall b. Num b => b -> b -> b
This is surely confusing for users.
We want to instantiate the type of (*) before returning, else we
will infer the type
f :: forall {a}. a -> forall b. Num b => b -> b -> b
This is surely confusing for users.
And worse, the monomorphism restriction won't work properly. The MR is
dealt with in simplifyInfer, and simplifyInfer has no way of
instantiating. This could perhaps be worked around, but it may be
hard to know even when instantiation should happen.
And worse, the monomorphism restriction won't work properly. The MR is
dealt with in simplifyInfer, and simplifyInfer has no way of
instantiating. This could perhaps be worked around, but it may be
hard to know even when instantiation should happen.
Another reason. Consider
2. Another reason. Consider
f :: (?x :: Int) => a -> a
g y = let ?x = 3::Int in f
Here want to instantiate f's type so that the ?x::Int constraint
gets discharged by the enclosing implicit-parameter binding.
Here want to instantiate f's type so that the ?x::Int constraint
gets discharged by the enclosing implicit-parameter binding.
* ir_inst = False: do not instantiate
ir_inst = False: do not instantiate
-----------------------------------
Consider this (which uses visible type application):
1. Consider this (which uses visible type application):
(let { f :: forall a. a -> a; f x = x } in f) @Int
We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
And we don't want to instantite the type of 'f' when we reach it,
else the outer visible type application won't work
We'll call TcExpr.tcInferFun to infer the type of the (let .. in f)
And we don't want to instantite the type of 'f' when we reach it,
else the outer visible type application won't work
2. :type +v. When we say
:type +v const @Int
we really want `forall b. Int -> b -> Int`. Note that this is *not*
instantiated.
3. Pattern bindings. For example:
foo x
| blah <- const @Int
= (blah x False, blah x 'z')
Note that `blah` is polymorphic. (This isn't a terribly compelling
reason, but the choice of ir_inst does matter here.)
Discussion
----------
We thought that we should just remove the ir_inst flag, in favor of
always instantiating. Essentially: motivations (1) and (3) for ir_inst = False
are not terribly exciting. However, motivation (2) is quite important.
Furthermore, there really was not much of a simplification of the code
in removing ir_inst, and working around it to enable flows like what we
see in (2) is annoying. This was done in #17173.
-}
{- *********************************************************************
......
......@@ -4,4 +4,4 @@ T5892a.hs:12:8: error: [-Wmissing-fields (in -Wdefault), -Werror=missing-fields]
• In the expression: Node {..}
In the expression: let rootLabel = [] in Node {..}
In an equation for ‘foo’:
foo (Node {..}) = let rootLabel = ... in Node {..}
foo (Node {..}) = let rootLabel = [] in Node {..}
......@@ -8,8 +8,7 @@ T10945.hs:7:4: error:
[SigD
(mkName "m")
(ForallT
[PlainTV (mkName "a")]
[]
[PlainTV (mkName "a")] []
(AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]]
In the Template Haskell splice
......@@ -17,8 +16,7 @@ T10945.hs:7:4: error:
[SigD
(mkName "m")
(ForallT
[PlainTV (mkName "a")]
[]
[PlainTV (mkName "a")] []
(AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
FunD (mkName "m") [Clause [...] (NormalB (VarE (mkName "x"))) []]])
In the expression:
......@@ -26,7 +24,6 @@ T10945.hs:7:4: error:
[SigD
(mkName "m")
(ForallT
[PlainTV (mkName "a")]
[]
[PlainTV (mkName "a")] []
(AppT (AppT ArrowT (VarT (mkName "a"))) (VarT (mkName "a")))),
FunD (mkName "m") [Clause ... (NormalB (VarE (mkName "x"))) ...]])
FunD (mkName "m") [Clause ... (NormalB (VarE (mkName "x"))) []]])
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