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

8 files changed, 132 insertions, 56 deletions

diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index 2ea1ae3f73..cd1a9f62bd 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -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
diff --git a/compiler/parser/Parser.y b/compiler/parser/Parser.y
index 21737b46e6..997f497510 100644
--- a/compiler/parser/Parser.y
+++ b/compiler/parser/Parser.y
@@ -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] }
diff --git a/compiler/prelude/TysWiredIn.hs b/compiler/prelude/TysWiredIn.hs
index 4d6b7f8027..0798f05195 100644
--- a/compiler/prelude/TysWiredIn.hs
+++ b/compiler/prelude/TysWiredIn.hs
@@ -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
 
diff --git a/compiler/rename/RnExpr.hs b/compiler/rename/RnExpr.hs
index 6485c004a6..f2f0685159 100644
--- a/compiler/rename/RnExpr.hs
+++ b/compiler/rename/RnExpr.hs
@@ -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
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 88896fc266..7ae1e8b4e7 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -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
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index e1fed8d2b3..37190a63fb 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -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.
+
 -}
 
 {- *********************************************************************
diff --git a/testsuite/tests/rename/should_fail/T5892a.stderr b/testsuite/tests/rename/should_fail/T5892a.stderr
index 0779538b1e..f1041796d9 100644
--- a/testsuite/tests/rename/should_fail/T5892a.stderr
+++ b/testsuite/tests/rename/should_fail/T5892a.stderr
@@ -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 {..}
diff --git a/testsuite/tests/th/T10945.stderr b/testsuite/tests/th/T10945.stderr
index c84fa38b61..786a0befa5 100644
--- a/testsuite/tests/th/T10945.stderr
+++ b/testsuite/tests/th/T10945.stderr
@@ -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"))) []]])