Do not bring visible foralls into scope in hsScopedTvswip/T17687

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.

4 files changed, 31 insertions, 14 deletions

diff --git a/compiler/GHC/Hs/Types.hs b/compiler/GHC/Hs/Types.hs
index 78d03c5..c250ec0 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.
 -}
 
 ---------------------
diff --git a/testsuite/tests/dependent/should_fail/T17687.hs b/testsuite/tests/dependent/should_fail/T17687.hs
new file mode 100644
index 0000000..b473639
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17687.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module T17687 where
+
+x :: forall a -> a -> a
+x = x
diff --git a/testsuite/tests/dependent/should_fail/T17687.stderr b/testsuite/tests/dependent/should_fail/T17687.stderr
new file mode 100644
index 0000000..e4ac034
--- /dev/null
+++ b/testsuite/tests/dependent/should_fail/T17687.stderr
@@ -0,0 +1,6 @@
+
+T17687.hs:5:6: error:
+    • Illegal visible, dependent quantification in the type of a term:
+        forall a -> a -> a
+      (GHC does not yet support this)
+    • In the type signature: x :: forall a -> a -> a
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index dde686a..d3d155f 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/testsuite/tests/dependent/should_fail/all.T
@@ -64,3 +64,4 @@ test('T14880', normal, compile_fail, [''])
 test('T14880-2', normal, compile_fail, [''])
 test('T15076', normal, compile_fail, [''])
 test('T15076b', normal, compile_fail, [''])
+test('T17687', normal, compile_fail, [''])