[project @ 2005-03-01 21:40:40 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index f9bcc6d..c4e1b92 100644 (file)
@@ -4,16 +4,17 @@
 \section[TcBinds]{TcBinds}
 
 \begin{code}
-module TcBinds ( tcBindsAndThen, tcTopBinds, tcMonoBinds, tcSpecSigs ) where
+module TcBinds ( tcBindsAndThen, tcTopBinds, tcHsBootSigs, tcMonoBinds, tcSpecSigs ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TcMatches ( tcGRHSsPat, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcCheckSigma, tcCheckRho )
 
-import CmdLineOpts     ( DynFlag(Opt_NoMonomorphismRestriction) )
+import CmdLineOpts     ( DynFlag(Opt_MonomorphismRestriction) )
 import HsSyn           ( HsExpr(..), HsBind(..), LHsBinds, Sig(..),
-                         LSig, Match(..), HsBindGroup(..), IPBind(..),
+                         LSig, Match(..), HsBindGroup(..), IPBind(..), 
+                         HsType(..), hsLTyVarNames, isVanillaLSig,
                          LPat, GRHSs, MatchGroup(..), emptyLHsBinds, isEmptyLHsBinds,
                          collectHsBindBinders, collectPatBinders, pprPatBind
                        )
@@ -21,31 +22,32 @@ import TcHsSyn              ( TcId, TcDictBinds, zonkId, mkHsLet )
 
 import TcRnMonad
 import Inst            ( InstOrigin(..), newDictsAtLoc, newIPDict, instToId )
-import TcEnv           ( tcExtendIdEnv, tcExtendIdEnv2, newLocalName, tcLookupLocalIds )
-import TcUnify         ( Expected(..), tcInfer, checkSigTyVars, sigCtxt )
+import TcEnv           ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 
+                         newLocalName, tcLookupLocalIds, pprBinders,
+                         tcGetGlobalTyVars )
+import TcUnify         ( Expected(..), tcInfer, unifyTheta, 
+                         bleatEscapedTvs, sigCtxt )
 import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, 
                          tcSimplifyToDicts, tcSimplifyIPs )
 import TcHsType                ( tcHsSigType, UserTypeCtxt(..), tcAddLetBoundTyVars,
-                         TcSigInfo(..), TcSigFun, mkTcSig, lookupSig
+                         TcSigInfo(..), TcSigFun, lookupSig
                        )
 import TcPat           ( tcPat, PatCtxt(..) )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcMType         ( newTyFlexiVarTy, tcSkolType, zonkQuantifiedTyVar )
+import TcMType         ( newTyFlexiVarTy, zonkQuantifiedTyVar, 
+                         tcInstSigType, zonkTcTypes, zonkTcTyVar )
 import TcType          ( TcTyVar, SkolemInfo(SigSkol), 
                          TcTauType, TcSigmaType, 
-                         TvSubstEnv, mkTvSubst, substTheta, substTy, 
                          mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
-                         mkForAllTy, isUnLiftedType, tcGetTyVar_maybe, 
-                         mkTyVarTys )
-import Unify           ( tcMatchPreds )
-import Kind            ( argTypeKind, isUnliftedTypeKind )
-import VarEnv          ( lookupVarEnv ) 
+                         mkForAllTy, isUnLiftedType, tcGetTyVar, 
+                         mkTyVarTys, tidyOpenTyVar, tidyOpenType )
+import Kind            ( argTypeKind )
+import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) 
 import TysPrim         ( alphaTyVar )
 import Id              ( mkLocalId, mkSpecPragmaId, setInlinePragma )
 import Var             ( idType, idName )
 import Name            ( Name )
 import NameSet
-import Var             ( tyVarKind )
 import VarSet
 import SrcLoc          ( Located(..), unLoc, noLoc, getLoc )
 import Bag
@@ -94,15 +96,28 @@ tcTopBinds :: [HsBindGroup Name] -> TcM (LHsBinds TcId, TcLclEnv)
        --       want.  The bit we care about is the local bindings
        --       and the free type variables thereof
 tcTopBinds binds
-  = tc_binds_and_then TopLevel glue binds      $
-    getLclEnv                                  `thenM` \ env ->
-    returnM (emptyLHsBinds, env)
+  = tc_binds_and_then TopLevel glue binds $
+           do  { env <- getLclEnv
+               ; return (emptyLHsBinds, env) }
   where
        -- The top level bindings are flattened into a giant 
        -- implicitly-mutually-recursive MonoBinds
     glue (HsBindGroup binds1 _ _) (binds2, env) = (binds1 `unionBags` binds2, env)
+    glue (HsIPBinds _)                   _             = panic "Top-level HsIpBinds"
        -- Can't have a HsIPBinds at top level
 
+tcHsBootSigs :: [HsBindGroup Name] -> TcM (LHsBinds TcId, TcLclEnv)
+-- A hs-boot file has only one BindGroup, and it only has type
+-- signatures in it.  The renamer checked all this
+tcHsBootSigs [HsBindGroup _ sigs _]
+  = do { ids <- mapM (addLocM tc_sig) (filter isVanillaLSig sigs)
+       ; tcExtendIdEnv ids $ do 
+       { env <- getLclEnv
+       ; return (emptyLHsBinds, env) }}
+  where
+    tc_sig (Sig (L _ name) ty)
+      = do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
+          ; return (mkLocalId name sigma_ty) }
 
 tcBindsAndThen
        :: (HsBindGroup TcId -> thing -> thing)         -- Combinator
@@ -237,11 +252,12 @@ tcBindWithSigs    :: TopLevelFlag
                -> [LSig Name]
                -> RecFlag
                -> TcM (LHsBinds TcId, [TcId])
+       -- The returned TcIds are guaranteed zonked
 
 tcBindWithSigs top_lvl mbind sigs is_rec = do  
   {    -- TYPECHECK THE SIGNATURES
     tc_ty_sigs <- recoverM (returnM []) $
-                 tcTySigs [sig | sig@(L _(Sig name _)) <- sigs]
+                 tcTySigs (filter isVanillaLSig sigs)
   ; let lookup_sig = lookupSig tc_ty_sigs
 
        -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
@@ -254,14 +270,29 @@ tcBindWithSigs top_lvl mbind sigs is_rec = do
   ; ((mbind', mono_bind_infos), lie_req) 
        <- getLIE (tcMonoBinds mbind lookup_sig is_rec)
 
-       -- GENERALISE
-  ; is_unres <- isUnRestrictedGroup mbind tc_ty_sigs
+       -- CHECK FOR UNLIFTED BINDINGS
+       -- These must be non-recursive etc, and are not generalised
+       -- They desugar to a case expression in the end
+  ; zonked_mono_tys <- zonkTcTypes (map getMonoType mono_bind_infos)
+  ; if any isUnLiftedType zonked_mono_tys then
+    do {       -- Unlifted bindings
+         checkUnliftedBinds top_lvl is_rec mbind
+       ; extendLIEs lie_req
+       ; let exports  = zipWith mk_export mono_bind_infos zonked_mono_tys
+             mk_export (name, Nothing,  mono_id) mono_ty = ([], mkLocalId name mono_ty, mono_id)
+             mk_export (name, Just sig, mono_id) mono_ty = ([], sig_id sig,             mono_id)
+
+       ; return ( unitBag $ noLoc $ AbsBinds [] [] exports emptyNameSet mbind',
+                  [poly_id | (_, poly_id, _) <- exports]) }    -- Guaranteed zonked
+
+    else do    -- The normal lifted case: GENERALISE
+  { is_unres <- isUnRestrictedGroup mbind tc_ty_sigs
   ; (tyvars_to_gen, dict_binds, dict_ids)
        <- setSrcSpan (getLoc (head (bagToList mbind)))     $
                -- TODO: location a bit awkward, but the mbinds have been
                --       dependency analysed and may no longer be adjacent
           addErrCtxt (genCtxt (bndrNames mono_bind_infos)) $
-          generalise is_unres mono_bind_infos tc_ty_sigs lie_req
+          generalise top_lvl is_unres mono_bind_infos tc_ty_sigs lie_req
 
        -- FINALISE THE QUANTIFIED TYPE VARIABLES
        -- The quantified type variables often include meta type variables
@@ -303,28 +334,16 @@ tcBindWithSigs top_lvl mbind sigs is_rec = do
   ; traceTc (text "binding:" <+> ppr ((dict_ids, dict_binds),
                                      exports, map idType zonked_poly_ids))
 
-       -- Check for an unlifted, non-overloaded group
-       -- In that case we must make extra checks
-  ; if any (isUnLiftedType . idType) zonked_poly_ids
-    then       -- Some bindings are unlifted
-       do { checkUnliftedBinds top_lvl is_rec tyvars_to_gen' mbind
-          ; return (
-                   unitBag $ noLoc $
-                   AbsBinds [] [] exports inlines mbind',
-                       -- Do not generate even any x=y bindings
-                   zonked_poly_ids )}
-
-    else       -- The normal case
-       return (
+  ; return (
            unitBag $ noLoc $
            AbsBinds tyvars_to_gen'
-                dict_ids
-                exports
-                inlines
-                (dict_binds `unionBags` mbind'),
+                    dict_ids
+                    exports
+                    inlines
+                    (dict_binds `unionBags` mbind'),
            zonked_poly_ids
         )
-  } }
+  } } }
 
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise 
@@ -348,26 +367,15 @@ attachInlinePhase inline_phases bndr
 -- Check that non-overloaded unlifted bindings are
 --     a) non-recursive,
 --     b) not top level, 
---     c) non-polymorphic
---     d) not a multiple-binding group (more or less implied by (a))
-
-checkUnliftedBinds top_lvl is_rec tyvars_to_gen mbind
-  = ASSERT( not (any (isUnliftedTypeKind . tyVarKind) tyvars_to_gen) )
-               -- The instCantBeGeneralised stuff in tcSimplify should have
-               -- already raised an error if we're trying to generalise an 
-               -- unboxed tyvar (NB: unboxed tyvars are always introduced 
-               -- along with a class constraint) and it's better done there 
-               -- because we have more precise origin information.
-               -- That's why we just use an ASSERT here.
-
-    checkTc (isNotTopLevel top_lvl)
+--     c) not a multiple-binding group (more or less implied by (a))
+
+checkUnliftedBinds top_lvl is_rec mbind
+  = checkTc (isNotTopLevel top_lvl)
            (unliftedBindErr "Top-level" mbind)         `thenM_`
     checkTc (isNonRec is_rec)
            (unliftedBindErr "Recursive" mbind)         `thenM_`
     checkTc (isSingletonBag mbind)
-           (unliftedBindErr "Multiple" mbind)          `thenM_`
-    checkTc (null tyvars_to_gen)
-           (unliftedBindErr "Polymorphic" mbind)
+           (unliftedBindErr "Multiple" mbind)
 \end{code}
 
 
@@ -441,22 +449,27 @@ tcMonoBinds :: LHsBinds Name
            -> TcSigFun -> RecFlag
            -> TcM (LHsBinds TcId, [MonoBindInfo])
 
-type MonoBindInfo = (Name, Maybe TcSigInfo, TcId)
-       -- Type signature (if any), and
-       -- the monomorphic bound things
-
-bndrNames :: [MonoBindInfo] -> [Name]
-bndrNames mbi = [n | (n,_,_) <- mbi]
-
-getMonoType :: MonoBindInfo -> TcTauType
-getMonoType (_,_,mono_id) = idType mono_id
-
 tcMonoBinds binds lookup_sig is_rec
   = do { tc_binds <- mapBagM (wrapLocM (tcLhs lookup_sig)) binds
-       ; let mono_info = getMonoBindInfo tc_binds
-       ; binds' <- tcExtendIdEnv2 (rhsEnvExtension mono_info) $
+
+       -- Bring (a) the scoped type variables, and (b) the Ids, into scope for the RHSs
+       -- For (a) it's ok to bring them all into scope at once, even
+       -- though each type sig should scope only over its own RHS,
+       -- because the renamer has sorted all that out.
+       ; let mono_info  = getMonoBindInfo tc_binds
+             rhs_tvs    = [ (name, mkTyVarTy tv)
+                          | (_, Just sig, _) <- mono_info, 
+                            (name, tv) <- sig_scoped sig `zip` sig_tvs sig ]
+             rhs_id_env = map mk mono_info     -- A binding for each term variable
+
+       ; binds' <- tcExtendTyVarEnv2 rhs_tvs   $
+                   tcExtendIdEnv2   rhs_id_env $
+                   traceTc (text "tcMonoBinds" <+> vcat [ppr n <+> ppr id <+> ppr (idType id) | (n,id) <- rhs_id_env]) `thenM_`
                    mapBagM (wrapLocM tcRhs) tc_binds
        ; return (binds', mono_info) }
+   where
+    mk (name, Just sig, _)       = (name, sig_id sig)  -- Use the type sig if there is one
+    mk (name, Nothing,  mono_id) = (name, mono_id)     -- otherwise use a monomorphic version
 
 ------------------------
 -- tcLhs typechecks the LHS of the bindings, to construct the environment in which
@@ -478,6 +491,16 @@ data TcMonoBind            -- Half completed; LHS done, RHS not done
   = TcFunBind  MonoBindInfo  (Located TcId) Bool (MatchGroup Name) 
   | TcPatBind [MonoBindInfo] (LPat TcId) (GRHSs Name) TcSigmaType
 
+type MonoBindInfo = (Name, Maybe TcSigInfo, TcId)
+       -- Type signature (if any), and
+       -- the monomorphic bound things
+
+bndrNames :: [MonoBindInfo] -> [Name]
+bndrNames mbi = [n | (n,_,_) <- mbi]
+
+getMonoType :: MonoBindInfo -> TcTauType
+getMonoType (_,_,mono_id) = idType mono_id
+
 tcLhs :: TcSigFun -> HsBind Name -> TcM TcMonoBind
 tcLhs lookup_sig (FunBind (L nm_loc name) inf matches)
   = do { let mb_sig = lookup_sig name
@@ -511,7 +534,7 @@ tcLhs lookup_sig bind@(PatBind pat grhss _)
 
 -------------------
 tcRhs :: TcMonoBind -> TcM (HsBind TcId)
-tcRhs (TcFunBind _ fun'@(L _ mono_id) inf matches)
+tcRhs (TcFunBind info fun'@(L _ mono_id) inf matches)
   = do { matches' <- tcMatchesFun (idName mono_id) matches 
                                   (Check (idType mono_id))
        ; return (FunBind fun' inf matches') }
@@ -529,15 +552,6 @@ getMonoBindInfo tc_binds
   where
     get_info (TcFunBind info _ _ _)  rest = info : rest
     get_info (TcPatBind infos _ _ _) rest = infos ++ rest
-
----------------------
-rhsEnvExtension :: [MonoBindInfo] -> [(Name, TcId)]
--- Environment for RHS of definitions: use type sig if there is one
-rhsEnvExtension mono_info
-  = map mk mono_info
-  where
-    mk (name, Just sig, _)       = (name, sig_id sig)
-    mk (name, Nothing,  mono_id) = (name, mono_id)
 \end{code}
 
 
@@ -547,6 +561,8 @@ rhsEnvExtension mono_info
 %*                                                                     *
 %************************************************************************
 
+Type signatures are tricky.  See Note [Signature skolems] in TcType
+
 \begin{code}
 tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
 -- The trick here is that all the signatures should have the same
@@ -554,67 +570,50 @@ tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
 -- all the right hand sides agree a common vocabulary for their type
 -- constraints
 tcTySigs [] = return []
-tcTySigs (L span (Sig (L _ name) ty) : sigs)
-  = do  {      -- Typecheck the first signature
-       ; sigma1 <- setSrcSpan span $
-                   tcHsSigType (FunSigCtxt name) ty
-       ; let id1 = mkLocalId name sigma1
-       ; tc_sig1 <- mkTcSig id1
-
-       ; tc_sigs <- mapM (tcTySig tc_sig1) sigs
-       ; return (tc_sig1 : tc_sigs) }
 
-tcTySig sig1 (L span (Sig (L _ name) ty))
+tcTySigs sigs
+  = do { (tc_sig1 : tc_sigs) <- mappM tcTySig sigs
+       ; mapM (check_ctxt tc_sig1) tc_sigs
+        ; return (tc_sig1 : tc_sigs) }
+  where
+       -- Check tha all the signature contexts are the same
+       -- The type signatures on a mutually-recursive group of definitions
+       -- must all have the same context (or none).
+       --
+       -- We unify them because, with polymorphic recursion, their types
+       -- might not otherwise be related.  This is a rather subtle issue.
+    check_ctxt :: TcSigInfo -> TcSigInfo -> TcM ()
+    check_ctxt sig1@(TcSigInfo { sig_theta = theta1 }) sig@(TcSigInfo { sig_theta = theta })
+       = setSrcSpan (instLocSrcSpan (sig_loc sig))     $
+         addErrCtxt (sigContextsCtxt sig1 sig)         $
+         unifyTheta theta1 theta
+
+
+tcTySig :: LSig Name -> TcM TcSigInfo
+tcTySig (L span (Sig (L _ name) ty))
   = setSrcSpan span            $
     do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
-       ; (tvs, theta, tau) <- tcSkolType rigid_info sigma_ty
-       ; let poly_id  = mkLocalId name sigma_ty
-             bale_out = failWithTc $
-                        sigContextsErr (sig_id sig1) name sigma_ty 
-
-       -- Try to match the context of this signature with 
-       -- that of the first signature
-       ; case tcMatchPreds tvs (sig_theta sig1) theta of { 
-           Nothing   -> bale_out
-       ;   Just tenv -> do
-       ; case check_tvs tenv tvs of
-           Nothing   -> bale_out
-           Just tvs' -> do 
-
-       { let subst  = mkTvSubst tenv
-             theta' = substTheta subst theta
-             tau'   = substTy subst tau
-       ; loc <- getInstLoc (SigOrigin rigid_info)
-       ; return (TcSigInfo { sig_id = poly_id, sig_tvs = tvs', 
-                             sig_theta = theta', sig_tau = tau', 
-                             sig_loc = loc }) }}}
-  where
-    rigid_info = SigSkol name
-
-       -- Rather tedious check that the type variables
-       -- have been matched only with another type variable,
-       -- and that two type variables have not been matched
-       -- with the same one
-       -- A return of Nothing indicates that one of the bad
-       -- things has happened
-    check_tvs :: TvSubstEnv -> [TcTyVar] -> Maybe [TcTyVar]
-    check_tvs tenv [] = Just []
-    check_tvs tenv (tv:tvs) 
-       | Just ty <- lookupVarEnv tenv tv
-       = do { tv' <- tcGetTyVar_maybe ty
-            ; tvs' <- check_tvs tenv tvs
-            ; if tv' `elem` tvs'
-              then Nothing
-              else Just (tv':tvs') }
-       | otherwise
-       = do { tvs' <- check_tvs tenv tvs
-            ; Just (tv:tvs') }
+       ; (tvs, theta, tau) <- tcInstSigType name sigma_ty
+       ; loc <- getInstLoc (SigOrigin (SigSkol name))
+
+       ; let poly_id = mkLocalId name sigma_ty
+
+               -- 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.)
+             scoped_names = case ty of
+                               L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
+                               other                      -> []
+
+       ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
+                             sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
+                             sig_loc = loc }) }
 \end{code}
 
 \begin{code}
-generalise :: Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst]
+generalise :: TopLevelFlag -> Bool -> [MonoBindInfo] -> [TcSigInfo] -> [Inst]
           -> TcM ([TcTyVar], TcDictBinds, [TcId])
-generalise is_unrestricted mono_infos sigs lie_req
+generalise top_lvl is_unrestricted mono_infos sigs lie_req
   | not is_unrestricted        -- RESTRICTED CASE
   =    -- Check signature contexts are empty 
     do { checkTc (all is_mono_sig sigs)
@@ -622,7 +621,8 @@ generalise is_unrestricted mono_infos sigs lie_req
 
        -- Now simplify with exactly that set of tyvars
        -- We have to squash those Methods
-       ; (qtvs, binds) <- tcSimplifyRestricted doc tau_tvs lie_req
+       ; (qtvs, binds) <- tcSimplifyRestricted doc top_lvl bndr_names 
+                                               tau_tvs lie_req
 
        -- Check that signature type variables are OK
        ; final_qtvs <- checkSigsTyVars qtvs sigs
@@ -656,34 +656,74 @@ generalise is_unrestricted mono_infos sigs lie_req
     is_mono_sig sig = null (sig_theta sig)
     doc = ptext SLIT("type signature(s) for") <+> pprBinders bndr_names
 
-mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
-                       sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id
-  = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc
+    mkMethInst (TcSigInfo { sig_id = poly_id, sig_tvs = tvs, 
+                           sig_theta = theta, sig_tau = tau, sig_loc = loc }) mono_id
+      = Method mono_id poly_id (mkTyVarTys tvs) theta tau loc
 
 checkSigsTyVars :: [TcTyVar] -> [TcSigInfo] -> TcM [TcTyVar]
 checkSigsTyVars qtvs sigs 
-  = mappM check_one sigs       `thenM` \ sig_tvs_s ->
-    let
-       -- Sigh.  Make sure that all the tyvars in the type sigs
-       -- appear in the returned ty var list, which is what we are
-       -- going to generalise over.  Reason: we occasionally get
-       -- silly types like
-       --      type T a = () -> ()
-       --      f :: T a
-       --      f () = ()
-       -- Here, 'a' won't appear in qtvs, so we have to add it
-
-       sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
-       all_tvs = extendVarSetList sig_tvs qtvs
-    in
-    returnM (varSetElems all_tvs)
+  = do { gbl_tvs <- tcGetGlobalTyVars
+       ; sig_tvs_s <- mappM (check_sig gbl_tvs) sigs
+
+       ; let   -- Sigh.  Make sure that all the tyvars in the type sigs
+               -- appear in the returned ty var list, which is what we are
+               -- going to generalise over.  Reason: we occasionally get
+               -- silly types like
+               --      type T a = () -> ()
+               --      f :: T a
+               --      f () = ()
+               -- Here, 'a' won't appear in qtvs, so we have to add it
+               sig_tvs = foldl extendVarSetList emptyVarSet sig_tvs_s
+               all_tvs = varSetElems (extendVarSetList sig_tvs qtvs)
+       ; returnM all_tvs }
   where
-    check_one (TcSigInfo {sig_id = id, sig_tvs = tvs, sig_theta = theta, sig_tau = tau})
-      = addErrCtxt (ptext SLIT("In the type signature for") 
-                     <+> quotes (ppr id))              $
-       addErrCtxtM (sigCtxt id tvs theta tau)          $
-       do { checkSigTyVars tvs; return tvs }
-\end{code}
+    check_sig gbl_tvs (TcSigInfo {sig_id = id, sig_tvs = tvs, 
+                                 sig_theta = theta, sig_tau = tau})
+      = addErrCtxt (ptext SLIT("In the type signature for") <+> quotes (ppr id))       $
+       addErrCtxtM (sigCtxt id tvs theta tau)                                          $
+       do { tvs' <- checkDistinctTyVars tvs
+          ; ifM (any (`elemVarSet` gbl_tvs) tvs')
+                (bleatEscapedTvs gbl_tvs tvs tvs') 
+          ; return tvs' }
+
+checkDistinctTyVars :: [TcTyVar] -> TcM [TcTyVar]
+-- (checkDistinctTyVars tvs) checks that the tvs from one type signature
+-- are still all type variables, and all distinct from each other.  
+-- It returns a zonked set of type variables.
+-- For example, if the type sig is
+--     f :: forall a b. a -> b -> b
+-- we want to check that 'a' and 'b' haven't 
+--     (a) been unified with a non-tyvar type
+--     (b) been unified with each other (all distinct)
+
+checkDistinctTyVars sig_tvs
+  = do { zonked_tvs <- mapM zonk_one sig_tvs
+       ; foldlM check_dup emptyVarEnv (sig_tvs `zip` zonked_tvs)
+       ; return zonked_tvs }
+  where
+    zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
+                        ; return (tcGetTyVar "checkDistinctTyVars" ty) }
+       -- 'ty' is bound to be a type variable, because SigSkolTvs
+       -- can only be unified with type variables
+
+    check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
+       -- The TyVarEnv maps each zonked type variable back to its
+       -- corresponding user-written signature type variable
+    check_dup acc (sig_tv, zonked_tv)
+       = case lookupVarEnv acc zonked_tv of
+               Just sig_tv' -> bomb_out sig_tv sig_tv'
+
+               Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
+
+    bomb_out sig_tv1 sig_tv2
+       = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1) 
+                    <+> ptext SLIT("is unified with another quantified type variable") 
+                    <+> ppr tidy_tv2)
+       where
+        (env1,  tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1
+        (_env2, tidy_tv2) = tidyOpenTyVar env1         sig_tv2
+\end{code}    
+
 
 @getTyVarsToGen@ decides what type variables to generalise over.
 
@@ -727,8 +767,8 @@ find which tyvars are constrained.
 \begin{code}
 isUnRestrictedGroup :: LHsBinds Name -> [TcSigInfo] -> TcM Bool
 isUnRestrictedGroup binds sigs
-  = do { no_MR <- doptM Opt_NoMonomorphismRestriction
-       ; return (no_MR || all_unrestricted) }
+  = do { mono_restriction <- doptM Opt_MonomorphismRestriction
+       ; return (not mono_restriction || all_unrestricted) }
   where 
     all_unrestricted = all (unrestricted . unLoc) (bagToList binds)
     tysig_names      = map (idName . sig_id) sigs
@@ -841,11 +881,14 @@ valSpecSigCtxt v ty
         nest 4 (ppr v <+> dcolon <+> ppr ty)]
 
 -----------------------------------------------
-sigContextsErr id1 name ty
-  = vcat [ptext SLIT("Mis-match between the contexts of the signatures for"), 
+sigContextsCtxt sig1 sig2
+  = vcat [ptext SLIT("When matching the contexts of the signatures for"), 
          nest 2 (vcat [ppr id1 <+> dcolon <+> ppr (idType id1),
-                       ppr name <+> dcolon <+> ppr ty]),
+                       ppr id2 <+> dcolon <+> ppr (idType id2)]),
          ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
+  where
+    id1 = sig_id sig1
+    id2 = sig_id sig2
 
 
 -----------------------------------------------
@@ -868,9 +911,4 @@ restrictedBindCtxtErr binder_names
 
 genCtxt binder_names
   = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names
-
--- Used in error messages
--- Use quotes for a single one; they look a bit "busy" for several
-pprBinders [bndr] = quotes (ppr bndr)
-pprBinders bndrs  = pprWithCommas ppr bndrs
 \end{code}