summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
authorRyan Scott <ryan.gl.scott@gmail.com>2020-01-15 11:01:03 -0500
committerRyan Scott <ryan.gl.scott@gmail.com>2020-01-25 08:15:05 -0500
commit0940b59accb6926aaede045bcd5f5bdc77c7075d (patch)
treeb4c2b12377f02897ddc27e48e1f88a2201c655e3 /compiler
parentb3e5c678851ed73897b0eb337e656ff377d242c9 (diff)
downloadhaskell-0940b59accb6926aaede045bcd5f5bdc77c7075d.tar.gz
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.
Diffstat (limited to 'compiler')
-rw-r--r--compiler/GHC/Hs/Types.hs32
1 files changed, 18 insertions, 14 deletions
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.
-}
---------------------