[Git][ghc/ghc][wip/T18660] Make the forall-or-nothing rule only apply to invisible foralls (#18660)
Ryan Scott
gitlab at gitlab.haskell.org
Mon Sep 7 23:06:48 UTC 2020
Ryan Scott pushed to branch wip/T18660 at Glasgow Haskell Compiler / GHC
Commits:
e37bd14b by Ryan Scott at 2020-09-07T19:06:32-04:00
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.
- - - - -
5 changed files:
- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/HsType.hs
- docs/users_guide/exts/explicit_forall.rst
- + testsuite/tests/dependent/should_compile/T18660.hs
- testsuite/tests/dependent/should_compile/all.T
Changes:
=====================================
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
=====================================
@@ -0,0 +1,7 @@
+{-# 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, [''])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e37bd14b85c86eca48345beeb1dc94cdf6bb1327
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/e37bd14b85c86eca48345beeb1dc94cdf6bb1327
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200907/d957932c/attachment-0001.html>
More information about the ghc-commits
mailing list