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.

3 files changed, 13 insertions, 0 deletions

diff --git a/testsuite/tests/dependent/should_fail/T17687.hs b/testsuite/tests/dependent/should_fail/T17687.hs
new file mode 100644
index 0000000000..b47363929e
--- /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 0000000000..e4ac034f93
--- /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 dde686af7a..d3d155f163 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, [''])