From 493fd9dfc6a7a60a7f5fdc126e2c4b731fbb4c3c Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Thu, 10 Jan 2008 11:31:33 +0000 Subject: [PATCH] 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!) --- compiler/main/DynFlags.hs | 5 +- compiler/typecheck/TcBinds.lhs | 92 +++++++++++++++++++++++-------------- docs/users_guide/glasgow_exts.xml | 30 ++++++++++-- 3 files changed, 88 insertions(+), 39 deletions(-) diff --git a/compiler/main/DynFlags.hs b/compiler/main/DynFlags.hs index e9681f6..2afa91d 100644 --- a/compiler/main/DynFlags.hs +++ b/compiler/main/DynFlags.hs @@ -1335,7 +1335,10 @@ xFlags = [ 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 = [ diff --git a/compiler/typecheck/TcBinds.lhs b/compiler/typecheck/TcBinds.lhs index aab8f01..db1a37a 100644 --- 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 $ - 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) - | (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, @@ -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.) - ; 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 @@ -662,7 +665,11 @@ tcLhs sig_fn other_bind = pprPanic "tcLhs" (ppr other_bind) ------------------- 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', @@ -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. +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 @@ -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 - -- 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] --------------- @@ -994,10 +1039,6 @@ data TcSigInfo = 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] @@ -1019,17 +1060,6 @@ data TcSigInfo -- 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: @@ -1060,10 +1090,12 @@ tcInstSig_maybe :: TcSigFun -> Name -> TcM (Maybe TcSigInfo) 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 @@ -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!! -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) @@ -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, - 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 diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 3b83551..9b4dc58 100644 --- 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. The rest of this section outlines the extensions to GHC that support GADTs. The extension is enabled with -. +. The flag also sets . A GADT can only be declared using GADT-style syntax (); @@ -4544,7 +4544,7 @@ a type for ys; a major benefit of scoped type variables is th it becomes possible to do so. Lexically-scoped type variables are enabled by -. +. This flag implies . 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 A declaration type signature that has explicit quantification (using forall) 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: 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 "forall a" brings "a" into scope in the definition of "f". -This only happens if the quantification in f's type +This only happens if: + + The quantification in f's type signature is explicit. For example: g :: [a] -> [a] @@ -4620,6 +4622,26 @@ This program will be rejected, because "a" does not scope over the definition of "f", so "x::a" means "x::forall a. a" by Haskell's usual implicit quantification rules. + + The signature gives a type for a function binding or a bare variable binding, +not a pattern binding. +For example: + + 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! + +The binding for f3 is a pattern binding, and so its type signature +does not bring a into scope. However f1 is a +function binding, and f2 binds a bare variable; in both cases +the type signature brings a into scope. + + -- 1.7.10.4