From 0940b59accb6926aaede045bcd5f5bdc77c7075d Mon Sep 17 00:00:00 2001
From: Ryan Scott <ryan.gl.scott@gmail.com>
Date: Wed, 15 Jan 2020 11:01:03 -0500
Subject: Do not bring visible foralls into scope in hsScopedTvs

Previously, `hsScopedTvs` (and its cousin `hsWcScopedTvs`) pretended
that visible dependent quantification could not possibly happen at
the term level, and cemented that assumption with an `ASSERT`:

```hs
    hsScopedTvs (HsForAllTy { hst_fvf = vis_flag, ... }) =
      ASSERT( vis_flag == ForallInvis )
      ...
```

It turns out that this assumption is wrong. You can end up tripping
this `ASSERT` if you stick it to the man and write a type for a term
that uses visible dependent quantification anyway, like in this
example:

```hs
{-# LANGUAGE ScopedTypeVariables #-}

x :: forall a -> a -> a
x = x
```

That won't typecheck, but that's not the point. Before the
typechecker has a chance to reject this, the renamer will try
to use `hsScopedTvs` to bring `a` into scope over the body of `x`,
since `a` is quantified by a `forall`. This, in turn, causes the
`ASSERT` to fail. Bummer.

Instead of walking on this dangerous ground, this patch makes GHC
adopt a more hardline stance by pattern-matching directly on
`ForallInvis` in `hsScopedTvs`:

```hs
    hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ...
```

Now `a` will not be brought over the body of `x` at all (which is how
it should be), there's no chance of the `ASSERT` failing anymore (as
it's gone), and best of all, the behavior of `hsScopedTvs` does not
change. Everyone wins!

Fixes #17687.
---
 compiler/GHC/Hs/Types.hs | 32 ++++++++++++++++++--------------
 1 file changed, 18 insertions(+), 14 deletions(-)

(limited to 'compiler')

diff --git a/compiler/GHC/Hs/Types.hs b/compiler/GHC/Hs/Types.hs
index 78d03c5859..c250ec013e 100644
--- a/compiler/GHC/Hs/Types.hs
+++ b/compiler/GHC/Hs/Types.hs
@@ -92,7 +92,7 @@ import SrcLoc
 import Outputable
 import FastString
 import Maybes( isJust )
-import Util ( count, debugIsOn )
+import Util ( count )
 
 import Data.Data hiding ( Fixity, Prefix, Infix )
 
@@ -965,9 +965,8 @@ hsWcScopedTvs sig_ty
   , HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty1
   = case sig_ty2 of
-      L _ (HsForAllTy { hst_fvf = vis_flag
+      L _ (HsForAllTy { hst_fvf = ForallInvis -- See Note [hsScopedTvs vis_flag]
                       , hst_bndrs = tvs }) ->
-        ASSERT( vis_flag == ForallInvis ) -- See Note [hsScopedTvs vis_flag]
         vars ++ nwcs ++ hsLTyVarNames tvs
       _                                    -> nwcs
 hsWcScopedTvs (HsWC _ (XHsImplicitBndrs nec)) = noExtCon nec
@@ -978,10 +977,9 @@ hsScopedTvs :: LHsSigType GhcRn -> [Name]
 hsScopedTvs sig_ty
   | HsIB { hsib_ext = vars
          , hsib_body = sig_ty2 } <- sig_ty
-  , L _ (HsForAllTy { hst_fvf = vis_flag
+  , L _ (HsForAllTy { hst_fvf = ForallInvis -- See Note [hsScopedTvs vis_flag]
                     , hst_bndrs = tvs }) <- sig_ty2
-  = ASSERT( vis_flag == ForallInvis ) -- See Note [hsScopedTvs vis_flag]
-    vars ++ hsLTyVarNames tvs
+  = vars ++ hsLTyVarNames tvs
   | otherwise
   = []
 
@@ -1027,17 +1025,23 @@ The conclusion of these discussions can be summarized as follows:
   >     vfn :: forall x y -> tau(x,y)
   >     vfn x y = \a b -> ...         -- bad!
 
-At the moment, GHC does not support visible 'forall' in terms, so we simply cement
-our assumptions with an assert:
+We cement this design by pattern-matching on ForallInvis in hsScopedTvs:
 
-    hsScopedTvs (HsForAllTy { hst_fvf = vis_flag, ... }) =
-      ASSERT( vis_flag == ForallInvis )
-      ...
+    hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ...
 
-In the future, this assert can be safely turned into a pattern match to support
-visible forall in terms:
+At the moment, GHC does not support visible 'forall' in terms. Nevertheless,
+it is still possible to write erroneous programs that use visible 'forall's in
+terms, such as this example:
 
-    hsScopedTvs (HsForAllTy { hst_fvf = ForallInvis, ... }) = ...
+    x :: forall a -> a -> a
+    x = x
+
+If we do not pattern-match on ForallInvis in hsScopedTvs, then `a` would
+erroneously be brought into scope over the body of `x` when renaming it.
+Although the typechecker would later reject this (see `TcValidity.vdqAllowed`),
+it is still possible for this to wreak havoc in the renamer before it gets to
+that point (see #17687 for an example of this).
+Bottom line: nip problems in the bud by matching on ForallInvis from the start.
 -}
 
 ---------------------
-- 
cgit v1.2.1