diff --git a/compiler/Language/Haskell/Syntax/Type.hs b/compiler/Language/Haskell/Syntax/Type.hs index 731df9c3e03d1521d8366dab9f0b6c2b82ab8d71..d03357ba4ee4b7ed17708b141875140d179eeb1a 100644 --- a/compiler/Language/Haskell/Syntax/Type.hs +++ b/compiler/Language/Haskell/Syntax/Type.hs @@ -1146,8 +1146,8 @@ I don't know if this is a good idea, but there it is. {- Note [hsScopedTvs and visible foralls] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ --XScopedTypeVariables can be defined in terms of a desugaring to --XTypeAbstractions (GHC Proposal #50): +ScopedTypeVariables can be defined in terms of a desugaring to TypeAbstractions +(GHC Proposals #155 and #448): fn :: forall a b c. tau(a,b,c) fn :: forall a b c. tau(a,b,c) fn = defn(a,b,c) ==> fn @x @y @z = defn(x,y,z) @@ -1160,19 +1160,16 @@ This model does not extend to visible forall, as discussed here: * https://gitlab.haskell.org/ghc/ghc/issues/16734#note_203412 * https://github.com/ghc-proposals/ghc-proposals/pull/238 -The conclusion of these discussions can be summarized as follows: +Here is a simple example that demonstrates the issue: - > Assuming support for visible 'forall' in terms, consider this example: - > - > vfn :: forall x y -> tau(x,y) - > vfn = \a b -> ... - > - > The user has written their own binders 'a' and 'b' to stand for 'x' and - > 'y', and we definitely should not desugar this into: - > - > vfn :: forall x y -> tau(x,y) - > vfn x y = \a b -> ... -- bad! + vfn :: forall a b -> tau(a, b) + vfn = case <scrutinee> of (p,q) -> \x y -> ... +The `a` and `b` cannot scope over the equations of `vfn`, in particural over +the <scrutinee>, because those type variables aren't bound until the `\x y ->` +that comes later. + +Bottom line: ScopedTypeVariables does not affect visible forall. This design choice is reflected in the design of HsOuterSigTyVarBndrs, which are used in every place that ScopedTypeVariables takes effect: @@ -1189,21 +1186,6 @@ which type variables to bring into scope over the body of a function (in hsScopedTvs), we /only/ bring the type variables bound by the hso_bndrs in an HsOuterExplicit into scope. If we have an HsOuterImplicit instead, then we do not bring any type variables into scope over the body of a function at all. - -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: - - x :: forall a -> a -> a - x = x - -Previous versions of GHC would bring `a` into scope over the body of `x` in the -hopes that the typechecker would error out later -(see `GHC.Tc.Validity.vdqAllowed`). However, this can wreak havoc in the -renamer before GHC gets to that point (see #17687 for an example of this). -Bottom line: nip problems in the bud by refraining from bringing any type -variables in an HsOuterImplicit into scope over the body of a function, even -if they correspond to a visible 'forall'. -} {-