Note [hsScopedTvs and visible foralls]
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) That is, for every type variable of the leading `forall` in the type signature, we add an invisible binder at the term level. This model does not extend to visible forall. (Visible forall is the one written with an arrow instead of a dot, i.e. `forall a ->`. See GHC Proposal #281 and the RequiredTypeArguments extension). Here is an example that demonstrates the issue: 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 particular, `a` and `b` cannot be in scope in <scrutinee> because those type variables are bound by the `\x y ->`. Our solution is simple: ScopedTypeVariables has no effect on visible forall. It follows naturally from the fact that ScopedTypeVariables is already subject to several restrictions: 1. The type signature must be headed by an /explicit/ forall * `f :: forall a. a -> blah` brings `a` into scope in the body * `f :: a -> blah` does not 2. The forall is /not nested/ * `f :: forall a b. blah` brings `a` and `b` into scope in the body * `f :: forall a. forall b. blah` brings `a` but not `b` into scope in the body With the introduction of visible forall, we also introduce a third condition: 3. The forall has to be /invisible/ * `f :: forall a b. blah` brings `a` and `b` into scope in the body * `f :: forall a b -> blah` does not For example: f1 :: forall a. a -> a f1 x = (x::a) -- OK: `a` is in scope in the body f2 :: forall a b. a -> b -> (a, b) f2 x y = (x::a, y::b) -- OK: both `a` and `b` are in scope in the body f3 :: forall a. forall b. a -> b -> (a, b) f3 x y = (x::a, y::b) -- Wrong: the `forall b.` is not the outermost forall f4 :: forall a -> a -> a f4 t (x::t) = (x::a) -- Wrong: the `forall a ->` does not bring `a` into scope This design choice is reflected in the definition of HsOuterSigTyVarBndrs, which are used in every place where ScopedTypeVariables takes effect: data HsOuterTyVarBndrs flag pass = HsOuterImplicit { ... } | HsOuterExplicit { ..., hso_bndrs :: [LHsTyVarBndr flag pass] } | ... type HsOuterSigTyVarBndrs = HsOuterTyVarBndrs Specificity The HsOuterExplicit constructor is only used in type signatures with outermost, /invisible/ 'forall's. Any other type—including those with outermost, /visible/ 'forall's—will use HsOuterImplicit. Therefore, when we determine 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.
References 0
This Note does not link to any other.
Referenced by 4
- GHC.Hs.Type call site ×3
- Lexically scoped type variables Language.Haskell.Syntax.Type