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!)

diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs
index e9681f6..2afa91d 100644 (file)
--- a/compiler/main/DynFlags.hs
+++ b/compiler/main/DynFlags.hs
@@ -1335,7 +1335,10 @@ xFlags = [
 
 impliedFlags :: [(DynFlag, [DynFlag])]
 impliedFlags = [
 
 impliedFlags :: [(DynFlag, [DynFlag])]
 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 = [

diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs
index aab8f01..db1a37a 100644 (file)
--- a/compiler/typecheck/TcBinds.lhs
+++ b/compiler/typecheck/TcBinds.lhs
@@ -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
        --        (b) bring (rigid) scoped type variables into scope
     setSrcSpan b_loc   $
        -- we can (a) use genuine, rigid skolem constants for the type variables
        --        (b) bring (rigid) scoped type variables into scope
     setSrcSpan b_loc   $

-    do { tc_sig <- tcInstSig True name scoped_tvs
+    do { tc_sig <- tcInstSig True name

        ; mono_name <- newLocalName name
        ; let mono_ty = sig_tau tc_sig
              mono_id = mkLocalId mono_name mono_ty
              rhs_tvs = [ (name, mkTyVarTy tv)
        ; mono_name <- newLocalName name
        ; let mono_ty = sig_tau tc_sig
              mono_id = mkLocalId mono_name mono_ty
              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
 
        ; let fun_bind' = FunBind { fun_id = L nm_loc mono_id, 
                               tcMatchesFun mono_name inf matches mono_ty
 
        ; let fun_bind' = FunBind { fun_id = L nm_loc mono_id, 

@@ -574,7 +577,7 @@ tcMonoBinds binds sig_fn non_rec
                                -- A monomorphic binding for each term variable that lacks 
                                -- a type sig.  (Ones with a sig are already in scope.)
 
                                -- A monomorphic binding for each term variable that lacks 
                                -- 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) 
                                                         | (n,id) <- rhs_id_env]) `thenM_`
                    mapM (wrapLocM tcRhs) tc_binds
                    traceTc (text "tcMonoBinds" <+> vcat [ ppr n <+> ppr id <+> ppr (idType id) 
                                                         | (n,id) <- rhs_id_env]) `thenM_`
                    mapM (wrapLocM tcRhs) tc_binds

@@ -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 
                                            matches (idType mono_id)
        ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',
   = do { (co_fn, matches') <- tcMatchesFun (idName mono_id) inf 
                                            matches (idType mono_id)
        ; return (FunBind { fun_id = fun', fun_infix = inf, fun_matches = matches',

@@ -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
 been instantiated.
 
 the variable's type, and after that checked to see whether they've
 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}
 type TcSigFun = Name -> Maybe [Name]   -- Maps a let-binder to the list of
                                        -- type variables brought into scope
 \begin{code}
 type TcSigFun = Name -> Maybe [Name]   -- Maps a let-binder to the list of
                                        -- type variables brought into scope

@@ -986,7 +1031,7 @@ mkTcSigFun sigs = lookupNameEnv env
                    | L span (TypeSig (L _ name) lhs_ty) <- sigs]
        -- The scoped names are the ones explicitly mentioned
        -- in the HsForAll.  (There may be more in sigma_ty, because
                    | L span (TypeSig (L _ name) lhs_ty) <- sigs]
        -- The scoped names are the ones explicitly mentioned
        -- 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
   = TcSigInfo {
        sig_id     :: TcId,             --  *Polymorphic* binder for this value...
 
   = TcSigInfo {
        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
                                        -- See Note [Instantiate sig]
 
        sig_tvs    :: [TcTyVar],        -- Instantiated type variables
                                        -- See Note [Instantiate sig]
 

@@ -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]
 -- It's vital to instantiate a type signature with fresh variables.
 -- For example:
 --     Note [Instantiate sig]
 -- It's vital to instantiate a type signature with fresh variables.
 -- For example:

@@ -1060,10 +1090,12 @@ tcInstSig_maybe :: TcSigFun -> Name -> TcM (Maybe TcSigInfo)
 tcInstSig_maybe sig_fn name 
   = case sig_fn name of
        Nothing  -> return Nothing
 tcInstSig_maybe sig_fn name 
   = case sig_fn name of
        Nothing  -> return Nothing

-       Just tvs -> do  { tc_sig <- tcInstSig False name tvs
-                       ; return (Just tc_sig) }
+       Just scoped_tvs -> do   { tc_sig <- tcInstSig False name
+                               ; 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
 -- depending on the use_skols boolean.  This variable is set True
 -- when we are typechecking a single function binding; and False for
 -- Instantiate the signature, with either skolems or meta-type variables
 -- depending on the use_skols boolean.  This variable is set True
 -- when we are typechecking a single function binding; and False for

@@ -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 
                                        -- scope when starting the binding group
        ; let skol_info = SigSkol (FunSigCtxt name)
   = do { poly_id <- tcLookupId name    -- Cannot fail; the poly ids are put into 
                                        -- scope when starting the binding group
        ; let skol_info = SigSkol (FunSigCtxt name)

@@ -1091,15 +1123,7 @@ tcInstSig use_skols name scoped_names
        ; loc <- getInstLoc (SigOrigin skol_info)
        ; return (TcSigInfo { sig_id = poly_id,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
        ; loc <- getInstLoc (SigOrigin skol_info)
        ; return (TcSigInfo { sig_id = poly_id,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 

-                             sig_scoped = final_scoped_names, 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 = []
+                             sig_loc = loc }) }

 
 -------------------
 isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool
 
 -------------------
 isMonoGroup :: DynFlags -> [LHsBind Name] -> Bool

diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 3b83551..9b4dc58 100644 (file)
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -2400,7 +2400,7 @@ may use different notation to that implemented in GHC.
 </para>
 <para>
 The rest of this section outlines the extensions to GHC that support GADTs.   The extension is enabled with 
 </para>
 <para>
 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>
 <listitem><para>
 A GADT can only be declared using GADT-style syntax (<xref linkend="gadt-style"/>); 
 <itemizedlist>
 <listitem><para>
 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
 it becomes possible to do so.
 </para>
 <para>Lexically-scoped type variables are enabled by
 it becomes possible to do so.
 </para>
 <para>Lexically-scoped type variables are enabled by

-<option>-fglasgow-exts</option>.
+<option>-XScopedTypeVariables</option>.  This flag implies <option>-XRelaxedPolyRec</option>.

 </para>
 <para>Note: GHC 6.6 contains substantial changes to the way that scoped type
 variables work, compared to earlier releases.  Read this section
 </para>
 <para>Note: GHC 6.6 contains substantial changes to the way that scoped type
 variables work, compared to earlier releases.  Read this section

@@ -4602,7 +4602,7 @@ then
 <para>A declaration type signature that has <emphasis>explicit</emphasis>
 quantification (using <literal>forall</literal>) brings into scope the
 explicitly-quantified
 <para>A declaration type signature that has <emphasis>explicit</emphasis>
 quantification (using <literal>forall</literal>) brings into scope the
 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>
   f :: forall a. [a] -> [a]
   f (x:xs) = xs ++ [ x :: a ]
 <programlisting>
   f :: forall a. [a] -> [a]
   f (x:xs) = xs ++ [ x :: a ]

@@ -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 definition of "<literal>f</literal>".
 </para>
 The "<literal>forall a</literal>" brings "<literal>a</literal>" into scope in
 the definition of "<literal>f</literal>".
 </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:
 <programlisting>
   g :: [a] -> [a]
 signature is explicit.  For example:
 <programlisting>
   g :: [a] -> [a]

@@ -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>"
 means "<literal>x::forall a. a</literal>" by Haskell's usual implicit
 quantification rules.
 over the definition of "<literal>f</literal>", so "<literal>x::a</literal>"
 means "<literal>x::forall a. a</literal>" by Haskell's usual implicit
 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>
 </sect3>
 
 </para>
 </sect3>