Make the forall-or-nothing rule only apply to invisible foralls (#18660)

This fixes #18660 by changing `isLHsForAllTy` to
`isLHsInvisForAllTy`, which is sufficient to make the
`forall`-or-nothing rule only apply to invisible `forall`s. I also
updated some related documentation and Notes while I was in the
neighborhood.

compiler/GHC/Hs/Type.hs

@@ -61,7 +61,7 @@ module GHC.Hs.Type (
         mkEmptyImplicitBndrs, mkEmptyWildCardBndrs,
         mkHsForAllVisTele, mkHsForAllInvisTele,
         mkHsQTvs, hsQTvExplicit, emptyLHsQTvs,
-        isHsKindedTyVar, hsTvbAllKinded, isLHsForAllTy,
+        isHsKindedTyVar, hsTvbAllKinded, isLHsInvisForAllTy,
         hsScopedTvs, hsWcScopedTvs, dropWildCards,
         hsTyVarName, hsAllLTyVarNames, hsLTyVarLocNames,
         hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
@@ -1278,9 +1278,12 @@ ignoreParens :: LHsType (GhcPass p) -> LHsType (GhcPass p)
 ignoreParens (L _ (HsParTy _ ty)) = ignoreParens ty
 ignoreParens ty                   = ty
 
-isLHsForAllTy :: LHsType (GhcPass p) -> Bool
-isLHsForAllTy (L _ (HsForAllTy {})) = True
-isLHsForAllTy _                     = False
+-- | Is this type headed by an invisible @forall@? This is used to determine
+-- if the type variables in a type should be implicitly quantified.
+-- See @Note [forall-or-nothing rule]@ in "GHC.Rename.HsType".
+isLHsInvisForAllTy :: LHsType (GhcPass p) -> Bool
+isLHsInvisForAllTy (L _ (HsForAllTy{hst_tele = HsForAllInvis{}})) = True
+isLHsInvisForAllTy _                                              = False
 
 {-
 ************************************************************************

compiler/GHC/Rename/HsType.hs

@@ -168,7 +168,7 @@ rn_hs_sig_wc_type scoping ctxt hs_ty thing_inside
        ; let nwc_rdrs = nubL nwc_rdrs'
        ; implicit_bndrs <- case scoping of
            AlwaysBind       -> pure tv_rdrs
-           BindUnlessForall -> forAllOrNothing (isLHsForAllTy hs_ty) tv_rdrs
+           BindUnlessForall -> forAllOrNothing (isLHsInvisForAllTy hs_ty) tv_rdrs
            NeverBind        -> pure []
        ; rnImplicitBndrs Nothing implicit_bndrs $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
@@ -321,7 +321,7 @@ rnHsSigType :: HsDocContext
 rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
        ; rdr_env <- getLocalRdrEnv
-       ; vars0 <- forAllOrNothing (isLHsForAllTy hs_ty)
+       ; vars0 <- forAllOrNothing (isLHsInvisForAllTy hs_ty)
            $ filterInScope rdr_env
            $ extractHsTyRdrTyVars hs_ty
        ; rnImplicitBndrs Nothing vars0 $ \ vars ->
@@ -331,17 +331,43 @@ rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
                        , hsib_body = body' }
                 , fvs ) } }
 
--- Note [forall-or-nothing rule]
--- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--- Free variables in signatures are usually bound in an implicit
--- 'forall' at the beginning of user-written signatures. However, if the
--- signature has an explicit forall at the beginning, this is disabled.
---
--- The idea is nested foralls express something which is only
--- expressible explicitly, while a top level forall could (usually) be
--- replaced with an implicit binding. Top-level foralls alone ("forall.") are
--- therefore an indication that the user is trying to be fastidious, so
--- we don't implicitly bind any variables.
+{-
+Note [forall-or-nothing rule]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Free variables in signatures are usually bound in an implicit 'forall' at the
+beginning of user-written signatures. However, if the signature has an
+explicit, invisible forall at the beginning, this is disabled.
+
+The idea is nested foralls express something which is only expressible
+explicitly, while a top level forall could (usually) be replaced with an
+implicit binding. Top-level foralls alone ("forall.") are therefore an
+indication that the user is trying to be fastidious, so we don't implicitly
+bind any variables.
+
+Note that this rule only applies to outermost /in/visible 'forall's, and not
+outermost visible 'forall's. See #18660 for more on this point.
+
+Here are some concrete examples to demonstrate the forall-or-nothing rule in
+action:
+
+  type F1 :: a -> b -> b                    -- Legal; a,b are implicitly quantified.
+                                            -- Equivalently: forall a b. a -> b -> b
+
+  type F2 :: forall a b. a -> b -> b        -- Legal; explicitly quantified
+
+  type F3 :: forall a. a -> b -> b          -- Illegal; the forall-or-nothing rule says that
+                                            -- if you quantify a, you must also quantify b
+
+  type F4 :: forall a -> b -> b             -- Legal; the top quantifier (forall a) is a /visible/
+                                            -- quantifer, so the "nothing" part of the forall-or-nothing
+                                            -- rule applies, and b is therefore implicitly quantified.
+                                            -- Equivalently: forall b. forall a -> b -> b
+
+  type F5 :: forall b. forall a -> b -> c   -- Illegal; the forall-or-nothing rule says that
+                                            -- if you quantify b, you must also quantify c
+
+  type F6 :: forall a -> forall b. b -> c   -- Legal: just like F4.
+-}
 
 -- | See @Note [forall-or-nothing rule]@. This tiny little function is used
 -- (rather than its small body inlined) to indicate that we are implementing

docs/users_guide/exts/explicit_forall.rst

@@ -56,30 +56,32 @@ The ``forall``-or-nothing rule
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 In certain forms of types, type variables obey what is known as the
-"``forall``-or-nothing" rule: if a type has an outermost, explicit
-``forall``, then all of the type variables in the type must be explicitly
-quantified. These two examples illustrate how the rule works: ::
+"``forall``-or-nothing" rule: if a type has an outermost, explicit,
+invisible ``forall``, then all of the type variables in the type must be
+explicitly quantified. These two examples illustrate how the rule works: ::
 
   f  :: forall a b. a -> b -> b         -- OK, `a` and `b` are explicitly bound
   g  :: forall a. a -> forall b. b -> b -- OK, `a` and `b` are explicitly bound
   h  :: forall a. a -> b -> b           -- Rejected, `b` is not in scope
 
 The type signatures for ``f``, ``g``, and ``h`` all begin with an outermost
-``forall``, so every type variable in these signatures must be explicitly
-bound by a ``forall``. Both ``f`` and ``g`` obey the ``forall``-or-nothing
-rule, since they explicitly quantify ``a`` and ``b``. On the other hand,
-``h`` does not explicitly quantify ``b``, so GHC will reject its type
-signature for being improperly scoped.
+invisible ``forall``, so every type variable in these signatures must be
+explicitly bound by a ``forall``. Both ``f`` and ``g`` obey the
+``forall``-or-nothing rule, since they explicitly quantify ``a`` and ``b``. On
+the other hand, ``h`` does not explicitly quantify ``b``, so GHC will reject
+its type signature for being improperly scoped.
 
 In places where the ``forall``-or-nothing rule takes effect, if a type does
-*not* have an outermost ``forall``, then any type variables that are not
-explicitly bound by a ``forall`` become implicitly quantified. For example: ::
+*not* have an outermost invisible ``forall``, then any type variables that are
+not explicitly bound by a ``forall`` become implicitly quantified. For example: ::
 
   i :: a -> b -> b             -- `a` and `b` are implicitly quantified
   j :: a -> forall b. b -> b   -- `a` is implicitly quantified
   k :: (forall a. a -> b -> b) -- `b` is implicitly quantified
+  type L :: forall a -> b -> b -- `b` is implicitly quantified
 
-GHC will accept ``i``, ``j``, and ``k``'s type signatures. Note that:
+GHC will accept ``i``, ``j``, and ``k``'s type signatures, as well as ``L``'s
+kind signature. Note that:
 
 - ``j``'s signature is accepted despite its mixture of implicit and explicit
   quantification. As long as a ``forall`` is not an outermost one, it is fine
@@ -88,6 +90,9 @@ GHC will accept ``i``, ``j``, and ``k``'s type signatures. Note that:
   the ``forall`` is not an outermost ``forall``. The ``forall``-or-nothing
   rule is one of the few places in GHC where the presence or absence of
   parentheses can be semantically significant!
+- ``L``'s signature begins with an outermost ``forall``, but it is a *visible*
+  ``forall``, not an invisible ``forall``, and therefore does not trigger the
+  ``forall``-or-nothing rule.
 
 The ``forall``-or-nothing rule takes effect in the following places:
 

testsuite/tests/dependent/should_compile/T18660.hs

+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+module T18660 where
+
+type F :: forall a -> b -> b
+type F x y = y

testsuite/tests/dependent/should_compile/all.T

@@ -66,3 +66,4 @@ test('T16326_Compile2', normal, compile, [''])
 test('T16391a', normal, compile, [''])
 test('T16344b', normal, compile, [''])
 test('T16347', normal, compile, [''])
+test('T18660', normal, compile, [''])