Commit 0940b59a authored by Ryan Scott's avatar Ryan Scott

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.
parent b3e5c678
......@@ -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.
-}
---------------------
......
{-# LANGUAGE ScopedTypeVariables #-}
module T17687 where
x :: forall a -> a -> a
x = x
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
......@@ -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, [''])
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment