Commit 493fd9df authored by simonpj@microsoft.com's avatar simonpj@microsoft.com
Browse files

Fix 2030: make -XScopedTypeVariables imply -XRelaxedPolyRec

The type checker doesn't support lexically scoped type variables 
unless we are using the RelaxedPolyRec option.  Reasons: see
Note [Scoped tyvars] in TcBinds.

So I've changed DynFlags to add this implication, improved the 
documentation, and simplified the code in TcBinds somewhat.
(It's longer but only because of comments!)
 
parent 46379cbb
...@@ -1335,7 +1335,10 @@ xFlags = [ ...@@ -1335,7 +1335,10 @@ xFlags = [
impliedFlags :: [(DynFlag, [DynFlag])] impliedFlags :: [(DynFlag, [DynFlag])]
impliedFlags = [ impliedFlags = [
( Opt_GADTs, [Opt_RelaxedPolyRec] ) -- We want type-sig variables to be completely rigid for GADTs ( Opt_GADTs, [Opt_RelaxedPolyRec] ) -- We want type-sig variables to
-- be completely rigid for GADTs
, ( Opt_ScopedTypeVariables, [Opt_RelaxedPolyRec] ) -- Ditto for scoped type variables; see
-- Note [Scoped tyvars] in TcBinds
] ]
glasgowExtsFlags = [ glasgowExtsFlags = [
......
...@@ -548,14 +548,17 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf, ...@@ -548,14 +548,17 @@ tcMonoBinds [L b_loc (FunBind { fun_id = L nm_loc name, fun_infix = inf,
-- we can (a) use genuine, rigid skolem constants for the type variables -- we can (a) use genuine, rigid skolem constants for the type variables
-- (b) bring (rigid) scoped type variables into scope -- (b) bring (rigid) scoped type variables into scope
setSrcSpan b_loc $ setSrcSpan b_loc $
do { tc_sig <- tcInstSig True name scoped_tvs do { tc_sig <- tcInstSig True name
; mono_name <- newLocalName name ; mono_name <- newLocalName name
; let mono_ty = sig_tau tc_sig ; let mono_ty = sig_tau tc_sig
mono_id = mkLocalId mono_name mono_ty mono_id = mkLocalId mono_name mono_ty
rhs_tvs = [ (name, mkTyVarTy tv) rhs_tvs = [ (name, mkTyVarTy tv)
| (name, tv) <- sig_scoped tc_sig `zip` sig_tvs tc_sig ] | (name, tv) <- scoped_tvs `zip` sig_tvs tc_sig ]
-- See Note [More instantiated than scoped]
-- Note that the scoped_tvs and the (sig_tvs sig)
-- may have different Names. That's quite ok.
; (co_fn, matches') <- tcExtendTyVarEnv2 rhs_tvs $ ; (co_fn, matches') <- tcExtendTyVarEnv2 rhs_tvs $
tcMatchesFun mono_name inf matches mono_ty tcMatchesFun mono_name inf matches mono_ty
; let fun_bind' = FunBind { fun_id = L nm_loc mono_id, ; let fun_bind' = FunBind { fun_id = L nm_loc mono_id,
...@@ -574,7 +577,7 @@ tcMonoBinds binds sig_fn non_rec ...@@ -574,7 +577,7 @@ tcMonoBinds binds sig_fn non_rec
-- A monomorphic binding for each term variable that lacks -- A monomorphic binding for each term variable that lacks
-- a type sig. (Ones with a sig are already in scope.) -- a type sig. (Ones with a sig are already in scope.)
; binds' <- tcExtendIdEnv2 rhs_id_env $ ; binds' <- tcExtendIdEnv2 rhs_id_env $
traceTc (text "tcMonoBinds" <+> vcat [ ppr n <+> ppr id <+> ppr (idType id) traceTc (text "tcMonoBinds" <+> vcat [ ppr n <+> ppr id <+> ppr (idType id)
| (n,id) <- rhs_id_env]) `thenM_` | (n,id) <- rhs_id_env]) `thenM_`
mapM (wrapLocM tcRhs) tc_binds mapM (wrapLocM tcRhs) tc_binds
...@@ -662,7 +665,11 @@ tcLhs sig_fn other_bind = pprPanic "tcLhs" (ppr other_bind) ...@@ -662,7 +665,11 @@ tcLhs sig_fn other_bind = pprPanic "tcLhs" (ppr other_bind)
------------------- -------------------
tcRhs :: TcMonoBind -> TcM (HsBind TcId) tcRhs :: TcMonoBind -> TcM (HsBind TcId)
tcRhs (TcFunBind info fun'@(L _ mono_id) inf matches) -- When we are doing pattern bindings, or multiple function bindings at a time
-- we *don't* bring any scoped type variables into scope
-- Wny not? They are not completely rigid.
-- That's why we have the special case for a single FunBind in tcMonoBinds
tcRhs (TcFunBind (_,_,mono_id) fun' inf matches)
= do { (co_fn, matches') <- tcMatchesFun (idName mono_id) inf = do { (co_fn, matches') <- tcMatchesFun (idName mono_id) inf
matches (idType mono_id) matches (idType mono_id)
; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches', ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',
...@@ -970,6 +977,44 @@ The @TcSigInfo@ contains @TcTypes@ because they are unified with ...@@ -970,6 +977,44 @@ The @TcSigInfo@ contains @TcTypes@ because they are unified with
the variable's type, and after that checked to see whether they've the variable's type, and after that checked to see whether they've
been instantiated. been instantiated.
Note [Scoped tyvars]
~~~~~~~~~~~~~~~~~~~~
The -XScopedTypeVariables flag brings lexically-scoped type variables
into scope for any explicitly forall-quantified type variables:
f :: forall a. a -> a
f x = e
Then 'a' is in scope inside 'e'.
However, we do *not* support this
- For pattern bindings e.g
f :: forall a. a->a
(f,g) = e
- For multiple function bindings, unless Opt_RelaxedPolyRec is on
f :: forall a. a -> a
f = g
g :: forall b. b -> b
g = ...f...
Reason: we use mutable variables for 'a' and 'b', since they may
unify to each other, and that means the scoped type variable would
not stand for a completely rigid variable.
Currently, we simply make Opt_ScopedTypeVariables imply Opt_RelaxedPolyRec
Note [More instantiated than scoped]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
There may be more instantiated type variables than lexically-scoped
ones. For example:
type T a = forall b. b -> (a,b)
f :: forall c. T c
Here, the signature for f will have one scoped type variable, c,
but two instantiated type variables, c' and b'.
We assume that the scoped ones are at the *front* of sig_tvs,
and remember the names from the original HsForAllTy in the TcSigFun.
\begin{code} \begin{code}
type TcSigFun = Name -> Maybe [Name] -- Maps a let-binder to the list of type TcSigFun = Name -> Maybe [Name] -- Maps a let-binder to the list of
-- type variables brought into scope -- type variables brought into scope
...@@ -986,7 +1031,7 @@ mkTcSigFun sigs = lookupNameEnv env ...@@ -986,7 +1031,7 @@ mkTcSigFun sigs = lookupNameEnv env
| L span (TypeSig (L _ name) lhs_ty) <- sigs] | L span (TypeSig (L _ name) lhs_ty) <- sigs]
-- The scoped names are the ones explicitly mentioned -- The scoped names are the ones explicitly mentioned
-- in the HsForAll. (There may be more in sigma_ty, because -- in the HsForAll. (There may be more in sigma_ty, because
-- of nested type synonyms. See Note [Scoped] with TcSigInfo.) -- of nested type synonyms. See Note [More instantiated than scoped].)
-- See Note [Only scoped tyvars are in the TyVarEnv] -- See Note [Only scoped tyvars are in the TyVarEnv]
--------------- ---------------
...@@ -994,10 +1039,6 @@ data TcSigInfo ...@@ -994,10 +1039,6 @@ data TcSigInfo
= TcSigInfo { = TcSigInfo {
sig_id :: TcId, -- *Polymorphic* binder for this value... sig_id :: TcId, -- *Polymorphic* binder for this value...
sig_scoped :: [Name], -- Names for any scoped type variables
-- Invariant: correspond 1-1 with an initial
-- segment of sig_tvs (see Note [Scoped])
sig_tvs :: [TcTyVar], -- Instantiated type variables sig_tvs :: [TcTyVar], -- Instantiated type variables
-- See Note [Instantiate sig] -- See Note [Instantiate sig]
...@@ -1019,17 +1060,6 @@ data TcSigInfo ...@@ -1019,17 +1060,6 @@ data TcSigInfo
-- only the lexically scoped ones into the environment. -- only the lexically scoped ones into the environment.
-- Note [Scoped]
-- There may be more instantiated type variables than scoped
-- ones. For example:
-- type T a = forall b. b -> (a,b)
-- f :: forall c. T c
-- Here, the signature for f will have one scoped type variable, c,
-- but two instantiated type variables, c' and b'.
--
-- We assume that the scoped ones are at the *front* of sig_tvs,
-- and remember the names from the original HsForAllTy in sig_scoped
-- Note [Instantiate sig] -- Note [Instantiate sig]
-- It's vital to instantiate a type signature with fresh variables. -- It's vital to instantiate a type signature with fresh variables.
-- For example: -- For example:
...@@ -1060,10 +1090,12 @@ tcInstSig_maybe :: TcSigFun -> Name -> TcM (Maybe TcSigInfo) ...@@ -1060,10 +1090,12 @@ tcInstSig_maybe :: TcSigFun -> Name -> TcM (Maybe TcSigInfo)
tcInstSig_maybe sig_fn name tcInstSig_maybe sig_fn name
= case sig_fn name of = case sig_fn name of
Nothing -> return Nothing Nothing -> return Nothing
Just tvs -> do { tc_sig <- tcInstSig False name tvs Just scoped_tvs -> do { tc_sig <- tcInstSig False name
; return (Just tc_sig) } ; return (Just tc_sig) }
-- NB: the scoped_tvs may be non-empty, but we can
-- just ignore them. See Note [Scoped tyvars].
tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo tcInstSig :: Bool -> Name -> TcM TcSigInfo
-- Instantiate the signature, with either skolems or meta-type variables -- Instantiate the signature, with either skolems or meta-type variables
-- depending on the use_skols boolean. This variable is set True -- depending on the use_skols boolean. This variable is set True
-- when we are typechecking a single function binding; and False for -- when we are typechecking a single function binding; and False for
...@@ -1082,7 +1114,7 @@ tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo ...@@ -1082,7 +1114,7 @@ tcInstSig :: Bool -> Name -> [Name] -> TcM TcSigInfo
-- --
-- We must not use the same 'a' from the defn of T at both places!! -- We must not use the same 'a' from the defn of T at both places!!
tcInstSig use_skols name scoped_names tcInstSig use_skols name
= do { poly_id <- tcLookupId name -- Cannot fail; the poly ids are put into = do { poly_id <- tcLookupId name -- Cannot fail; the poly ids are put into
-- scope when starting the binding group -- scope when starting the binding group
; let skol_info = SigSkol (FunSigCtxt name) ; let skol_info = SigSkol (FunSigCtxt name)
...@@ -1091,15 +1123,7 @@ tcInstSig use_skols name scoped_names ...@@ -1091,15 +1123,7 @@ tcInstSig use_skols name scoped_names
; loc <- getInstLoc (SigOrigin skol_info) ; loc <- getInstLoc (SigOrigin skol_info)
; return (TcSigInfo { sig_id = poly_id, ; return (TcSigInfo { sig_id = poly_id,
sig_tvs = tvs, sig_theta = theta, sig_tau = tau, sig_tvs = tvs, sig_theta = theta, sig_tau = tau,
sig_scoped = final_scoped_names, sig_loc = loc }) } sig_loc = loc }) }
-- Note that the scoped_names and the sig_tvs will have
-- different Names. That's quite ok; when we bring the
-- scoped_names into scope, we just bind them to the sig_tvs
where
-- We also only have scoped type variables when we are instantiating
-- with true skolems
final_scoped_names | use_skols = scoped_names
| otherwise = []
------------------- -------------------
isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool
......
...@@ -2400,7 +2400,7 @@ may use different notation to that implemented in GHC. ...@@ -2400,7 +2400,7 @@ may use different notation to that implemented in GHC.
</para> </para>
<para> <para>
The rest of this section outlines the extensions to GHC that support GADTs. The extension is enabled with The rest of this section outlines the extensions to GHC that support GADTs. The extension is enabled with
<option>-XGADTs</option>. <option>-XGADTs</option>. The <option>-XGADTs</option> flag also sets <option>-XRelaxedPolyRec</option>.
<itemizedlist> <itemizedlist>
<listitem><para> <listitem><para>
A GADT can only be declared using GADT-style syntax (<xref linkend="gadt-style"/>); A GADT can only be declared using GADT-style syntax (<xref linkend="gadt-style"/>);
...@@ -4544,7 +4544,7 @@ a type for <varname>ys</varname>; a major benefit of scoped type variables is th ...@@ -4544,7 +4544,7 @@ a type for <varname>ys</varname>; a major benefit of scoped type variables is th
it becomes possible to do so. it becomes possible to do so.
</para> </para>
<para>Lexically-scoped type variables are enabled by <para>Lexically-scoped type variables are enabled by
<option>-fglasgow-exts</option>. <option>-XScopedTypeVariables</option>. This flag implies <option>-XRelaxedPolyRec</option>.
</para> </para>
<para>Note: GHC 6.6 contains substantial changes to the way that scoped type <para>Note: GHC 6.6 contains substantial changes to the way that scoped type
variables work, compared to earlier releases. Read this section variables work, compared to earlier releases. Read this section
...@@ -4602,7 +4602,7 @@ then ...@@ -4602,7 +4602,7 @@ then
<para>A declaration type signature that has <emphasis>explicit</emphasis> <para>A declaration type signature that has <emphasis>explicit</emphasis>
quantification (using <literal>forall</literal>) brings into scope the quantification (using <literal>forall</literal>) brings into scope the
explicitly-quantified explicitly-quantified
type variables, in the definition of the named function(s). For example: type variables, in the definition of the named function. For example:
<programlisting> <programlisting>
f :: forall a. [a] -> [a] f :: forall a. [a] -> [a]
f (x:xs) = xs ++ [ x :: a ] f (x:xs) = xs ++ [ x :: a ]
...@@ -4610,7 +4610,9 @@ type variables, in the definition of the named function(s). For example: ...@@ -4610,7 +4610,9 @@ type variables, in the definition of the named function(s). For example:
The "<literal>forall a</literal>" brings "<literal>a</literal>" into scope in The "<literal>forall a</literal>" brings "<literal>a</literal>" into scope in
the definition of "<literal>f</literal>". the definition of "<literal>f</literal>".
</para> </para>
<para>This only happens if the quantification in <literal>f</literal>'s type <para>This only happens if:
<itemizedlist>
<listitem><para> The quantification in <literal>f</literal>'s type
signature is explicit. For example: signature is explicit. For example:
<programlisting> <programlisting>
g :: [a] -> [a] g :: [a] -> [a]
...@@ -4620,6 +4622,26 @@ This program will be rejected, because "<literal>a</literal>" does not scope ...@@ -4620,6 +4622,26 @@ This program will be rejected, because "<literal>a</literal>" does not scope
over the definition of "<literal>f</literal>", so "<literal>x::a</literal>" over the definition of "<literal>f</literal>", so "<literal>x::a</literal>"
means "<literal>x::forall a. a</literal>" by Haskell's usual implicit means "<literal>x::forall a. a</literal>" by Haskell's usual implicit
quantification rules. quantification rules.
</para></listitem>
<listitem><para> The signature gives a type for a function binding or a bare variable binding,
not a pattern binding.
For example:
<programlisting>
f1 :: forall a. [a] -> [a]
f1 (x:xs) = xs ++ [ x :: a ] -- OK
f2 :: forall a. [a] -> [a]
f2 = \(x:xs) -> xs ++ [ x :: a ] -- OK
f3 :: forall a. [a] -> [a]
Just f3 = Just (\(x:xs) -> xs ++ [ x :: a ]) -- Not OK!
</programlisting>
The binding for <literal>f3</literal> is a pattern binding, and so its type signature
does not bring <literal>a</literal> into scope. However <literal>f1</literal> is a
function binding, and <literal>f2</literal> binds a bare variable; in both cases
the type signature brings <literal>a</literal> into scope.
</para></listitem>
</itemizedlist>
</para> </para>
</sect3> </sect3>
......
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