[project @ 2001-12-03 11:36:26 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index 6ed91b9..35f3923 100644 (file)
@@ -13,48 +13,45 @@ import {-# SOURCE #-} TcMatches ( tcGRHSs, tcMatchesFun )
 import {-# SOURCE #-} TcExpr  ( tcExpr )
 
 import CmdLineOpts     ( opt_NoMonomorphismRestriction )
-import HsSyn           ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), StmtCtxt(..),
-                         Match(..), collectMonoBinders, andMonoBinds
+import HsSyn           ( HsExpr(..), HsBinds(..), MonoBinds(..), Sig(..), 
+                         Match(..), HsMatchContext(..), 
+                         collectMonoBinders, andMonoBinds,
+                         collectSigTysFromMonoBinds
                        )
 import RnHsSyn         ( RenamedHsBinds, RenamedSig, RenamedMonoBinds )
 import TcHsSyn         ( TcMonoBinds, TcId, zonkId, mkHsLet )
 
 import TcMonad
-import Inst            ( LIE, emptyLIE, mkLIE, plusLIE, lieToList, InstOrigin(..),
-                         newDicts, tyVarsOfInsts, instToId
+import Inst            ( LIE, emptyLIE, mkLIE, plusLIE, InstOrigin(..),
+                         newDicts, instToId
                        )
-import TcEnv           ( tcExtendLocalValEnv,
-                         newSpecPragmaId, newLocalId,
-                         tcGetGlobalTyVars
+import TcEnv           ( tcExtendLocalValEnv, newLocalName )
+import TcUnify         ( unifyTauTyLists, checkSigTyVars, sigCtxt )
+import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyRestricted, tcSimplifyToDicts )
+import TcMonoType      ( tcHsSigType, UserTypeCtxt(..), 
+                         TcSigInfo(..), tcTySig, maybeSig, tcAddScopedTyVars
                        )
-import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, tcSimplifyToDicts )
-import TcMonoType      ( tcHsSigType, checkSigTyVars,
-                         TcSigInfo(..), tcTySig, maybeSig, sigCtxt
-                       )
-import TcPat           ( tcPat )
+import TcPat           ( tcPat, tcSubPat, tcMonoPatBndr )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcType          ( newTyVarTy, newTyVar, zonkTcTyVarsAndFV,
+import TcMType         ( newTyVar, newTyVarTy, newHoleTyVarTy,
                          zonkTcTyVarToTyVar
                        )
-import TcUnify         ( unifyTauTy, unifyTauTyLists )
+import TcType          ( mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
+                         mkPredTy, mkForAllTy, isUnLiftedType, 
+                         unliftedTypeKind, liftedTypeKind, openTypeKind, eqKind
+                       )
 
 import CoreFVs         ( idFreeTyVars )
-import Id              ( mkVanillaId, setInlinePragma )
+import Id              ( mkLocalId, mkSpecPragmaId, setInlinePragma )
 import Var             ( idType, idName )
-import IdInfo          ( InlinePragInfo(..) )
-import Name            ( Name, getOccName, getSrcLoc )
+import Name            ( Name, getSrcLoc )
 import NameSet
-import Type            ( mkTyVarTy, 
-                         mkForAllTys, mkFunTys, tyVarsOfType, 
-                         mkPredTy, mkForAllTy, isUnLiftedType, 
-                         unliftedTypeKind, liftedTypeKind, openTypeKind
-                       )
 import Var             ( tyVarKind )
 import VarSet
 import Bag
-import Util            ( isIn )
-import Maybes          ( maybeToBool )
-import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isNotTopLevel )
+import Util            ( isIn, equalLength )
+import BasicTypes      ( TopLevelFlag(..), RecFlag(..), isNonRec, isNotTopLevel,
+                         isAlwaysActive )
 import FiniteMap       ( listToFM, lookupFM )
 import Outputable
 \end{code}
@@ -120,7 +117,14 @@ tc_binds_and_then top_lvl combiner (ThenBinds b1 b2) do_next
     do_next
 
 tc_binds_and_then top_lvl combiner (MonoBind bind sigs is_rec) do_next
-  =    -- TYPECHECK THE SIGNATURES
+  =    -- BRING ANY SCOPED TYPE VARIABLES INTO SCOPE
+       -- Notice that they scope over 
+       --      a) the type signatures in the binding group
+       --      b) the bindings in the group
+       --      c) the scope of the binding group (the "in" part)
+      tcAddScopedTyVars (collectSigTysFromMonoBinds bind)      $
+
+       -- TYPECHECK THE SIGNATURES
       mapTc tcTySig [sig | sig@(Sig name _ _) <- sigs] `thenTc` \ tc_ty_sigs ->
   
       tcBindWithSigs top_lvl bind tc_ty_sigs
@@ -216,7 +220,7 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
          poly_ids      = map mk_dummy binder_names
          mk_dummy name = case maybeSig tc_ty_sigs name of
                            Just (TySigInfo _ poly_id _ _ _ _ _ _) -> poly_id   -- Signature
-                           Nothing -> mkVanillaId name forall_a_a              -- No signature
+                           Nothing -> mkLocalId name forall_a_a                -- No signature
        in
        returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
     )                                          $
@@ -224,10 +228,12 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
        -- TYPECHECK THE BINDINGS
     tcMonoBinds mbind tc_ty_sigs is_rec                `thenTc` \ (mbind', lie_req, binder_names, mono_ids) ->
     let
-       tau_tvs = varSetElems (foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids)
+       tau_tvs = foldr (unionVarSet . tyVarsOfType . idType) emptyVarSet mono_ids
     in
 
        -- GENERALISE
+    tcAddSrcLoc  (minimum (map getSrcLoc binder_names))                $
+    tcAddErrCtxt (genCtxt binder_names)                                $
     generalise binder_names mbind tau_tvs lie_req tc_ty_sigs
                                `thenTc` \ (tc_tyvars_to_gen, lie_free, dict_binds, dict_ids) ->
 
@@ -249,22 +255,16 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
     mapNF_Tc zonkId dict_ids                           `thenNF_Tc` \ zonked_dict_ids ->
     mapNF_Tc zonkId mono_ids                           `thenNF_Tc` \ zonked_mono_ids ->
 
-       -- CHECK FOR BOGUS UNLIFTED BINDINGS
-    checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids `thenTc_`
-
        -- BUILD THE POLYMORPHIC RESULT IDs
     let
        exports  = zipWith mk_export binder_names zonked_mono_ids
+       poly_ids = [poly_id | (_, poly_id, _) <- exports]
        dict_tys = map idType zonked_dict_ids
 
-       inlines    = mkNameSet [name | InlineSig name _ loc <- inline_sigs]
-        no_inlines = listToFM ([(name, IMustNotBeINLINEd False phase) | NoInlineSig name phase loc <- inline_sigs] ++
-                              [(name, IMustNotBeINLINEd True  phase) | InlineSig   name phase loc <- inline_sigs, maybeToBool phase])
-               -- "INLINE n foo" means inline foo, but not until at least phase n
-               -- "NOINLINE n foo" means don't inline foo until at least phase n, and even 
-               --                  then only if it is small enough etc.
-               -- "NOINLINE foo" means don't inline foo ever, which we signal with a (IMustNotBeINLINEd Nothing)
-               -- See comments in CoreUnfold.blackListed for the Authorised Version
+       inlines    = mkNameSet [name | InlineSig True name _ loc <- inline_sigs]
+        no_inlines = listToFM [(name, phase) | InlineSig _ name phase _ <- inline_sigs, 
+                                              not (isAlwaysActive phase)]
+                       -- AlwaysActive is the default, so don't bother with them
 
        mk_export binder_name zonked_mono_id
          = (tyvars, 
@@ -277,10 +277,10 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
                        (sig_tyvars, sig_poly_id)
                  Nothing -> (real_tyvars_to_gen, new_poly_id)
 
-           new_poly_id = mkVanillaId binder_name poly_ty
+           new_poly_id = mkLocalId binder_name poly_ty
            poly_ty = mkForAllTys real_tyvars_to_gen
-                       $ mkFunTys dict_tys 
-                       $ idType zonked_mono_id
+                   $ mkFunTys dict_tys 
+                   $ idType zonked_mono_id
                -- It's important to build a fully-zonked poly_ty, because
                -- we'll slurp out its free type variables when extending the
                -- local environment (tcExtendLocalValEnv); if it's not zonked
@@ -288,17 +288,29 @@ tcBindWithSigs top_lvl mbind tc_ty_sigs inline_sigs is_rec
                -- at all.
     in
 
-        -- BUILD RESULTS
+    traceTc (text "binding:" <+> ppr ((zonked_dict_ids, dict_binds),
+                                     exports, map idType poly_ids)) `thenTc_`
+
+       -- Check for an unlifted, non-overloaded group
+       -- In that case we must make extra checks
+    if any (isUnLiftedType . idType) zonked_mono_ids && null zonked_dict_ids 
+    then       -- Some bindings are unlifted
+       checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind      `thenTc_` 
+       
+       returnTc (
+           AbsBinds [] [] exports inlines mbind',
+           lie_req,            -- Do not generate even any x=y bindings
+           poly_ids
+        )
+
+    else       -- The normal case
     returnTc (
-       -- pprTrace "binding.." (ppr ((zonked_dict_ids, dict_binds), 
-       --                              exports, [idType poly_id | (_, poly_id, _) <- exports])) $
        AbsBinds real_tyvars_to_gen
                 zonked_dict_ids
                 exports
                 inlines
                 (dict_binds `andMonoBinds` mbind'),
-       lie_free,
-       [poly_id | (_, poly_id, _) <- exports]
+       lie_free, poly_ids
     )
 
 attachNoInlinePrag no_inlines bndr
@@ -306,8 +318,14 @@ attachNoInlinePrag no_inlines bndr
        Just prag -> bndr `setInlinePragma` prag
        Nothing   -> bndr
 
-checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids
-  = ASSERT( not (any ((== unliftedTypeKind) . tyVarKind) real_tyvars_to_gen) )
+-- 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 real_tyvars_to_gen mbind
+  = ASSERT( not (any ((eqKind unliftedTypeKind) . tyVarKind) real_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 
@@ -315,34 +333,19 @@ checkUnliftedBinds top_lvl is_rec real_tyvars_to_gen mbind zonked_mono_ids
                -- because we have more precise origin information.
                -- That's why we just use an ASSERT here.
 
-       -- Check that pattern-bound variables are not unlifted
-    (if or [ (idName id `elem` pat_binders) && isUnLiftedType (idType id) 
-          | id <- zonked_mono_ids ] then
-       addErrTc (unliftedBindErr "Pattern" mbind)
-     else
-       returnTc ()
-    )                                                          `thenTc_`
-
-       -- Unlifted bindings must be non-recursive,
-       -- not top level, non-polymorphic, and not pattern bound
-    if any (isUnLiftedType . idType) zonked_mono_ids then
-       checkTc (isNotTopLevel top_lvl)
-               (unliftedBindErr "Top-level" mbind)             `thenTc_`
-       checkTc (isNonRec is_rec)
-               (unliftedBindErr "Recursive" mbind)             `thenTc_`
-       checkTc (null real_tyvars_to_gen)
-               (unliftedBindErr "Polymorphic" mbind)
-     else
-       returnTc ()
+    checkTc (isNotTopLevel top_lvl)
+           (unliftedBindErr "Top-level" mbind)         `thenTc_`
+    checkTc (isNonRec is_rec)
+           (unliftedBindErr "Recursive" mbind)         `thenTc_`
+    checkTc (single_bind mbind)
+           (unliftedBindErr "Multiple" mbind)          `thenTc_`
+    checkTc (null real_tyvars_to_gen)
+           (unliftedBindErr "Polymorphic" mbind)
 
   where
-    pat_binders :: [Name]
-    pat_binders = collectMonoBinders (justPatBindings mbind EmptyMonoBinds)
-
-    justPatBindings bind@(PatMonoBind _ _ _) binds = bind `andMonoBinds` binds
-    justPatBindings (AndMonoBinds b1 b2) binds = 
-           justPatBindings b1 (justPatBindings b2 binds) 
-    justPatBindings other_bind binds = binds
+    single_bind (PatMonoBind _ _ _)   = True
+    single_bind (FunMonoBind _ _ _ _) = True
+    single_bind other                = False
 \end{code}
 
 
@@ -410,59 +413,47 @@ is doing.
 
 \begin{code}
 generalise binder_names mbind tau_tvs lie_req sigs
+  | not is_unrestricted        -- RESTRICTED CASE
+  =    -- Check signature contexts are empty 
+    checkTc (all is_mono_sig sigs)
+           (restrictedBindCtxtErr binder_names)        `thenTc_`
 
------------------------
-  | is_unrestricted && null sigs
-  =    -- INFERENCE CASE: Unrestricted group, no type signatures
-    tcSimplifyInfer (ptext SLIT("bindings for") <+> pprBinders binder_names)
-                   tau_tvs lie_req
+       -- Now simplify with exactly that set of tyvars
+       -- We have to squash those Methods
+    tcSimplifyRestricted doc tau_tvs lie_req           `thenTc` \ (qtvs, lie_free, binds) ->
 
------------------------
-  | is_unrestricted 
+       -- Check that signature type variables are OK
+    checkSigsTyVars sigs                               `thenTc_`
+
+    returnTc (qtvs, lie_free, binds, [])
+
+  | null sigs                  -- UNRESTRICTED CASE, NO TYPE SIGS
+  = tcSimplifyInfer doc tau_tvs lie_req
+
+  | otherwise                  -- UNRESTRICTED CASE, WITH TYPE SIGS
   =    -- CHECKING CASE: Unrestricted group, there are type signatures
        -- Check signature contexts are empty 
     checkSigsCtxts sigs                                `thenTc` \ (sig_avails, sig_dicts) ->
-
+    
        -- Check that the needed dicts can be
        -- expressed in terms of the signature ones
-    tcSimplifyInferCheck check_doc tau_tvs sig_avails lie_req  `thenTc` \ (forall_tvs, lie_free, dict_binds) ->
+    tcSimplifyInferCheck doc tau_tvs sig_avails lie_req        `thenTc` \ (forall_tvs, lie_free, dict_binds) ->
        
        -- Check that signature type variables are OK
     checkSigsTyVars sigs                                       `thenTc_`
 
     returnTc (forall_tvs, lie_free, dict_binds, sig_dicts)
 
------------------------
-  | otherwise          -- RESTRICTED CASE: Restricted group
-  =    -- Check signature contexts are empty 
-    (if null sigs then
-       returnTc ()
-     else
-       checkSigsCtxts sigs     `thenTc` \ (_, sig_dicts) ->
-       checkTc (null sig_dicts)
-               (restrictedBindCtxtErr binder_names)
-    )                                                  `thenTc_`
-
-       -- Identify constrained tyvars
-    tcGetGlobalTyVars                          `thenNF_Tc` \ gbl_tvs ->
-    zonkTcTyVarsAndFV tau_tvs                  `thenNF_Tc` \ tau_tvs' ->
-    zonkTcTyVarsAndFV lie_tvs                  `thenNF_Tc` \ lie_tvs' ->
-    let
-       forall_tvs = tau_tvs' `minusVarSet` (lie_tvs' `unionVarSet` gbl_tvs)
-               -- Don't bother to oclose the gbl_tvs; this is a rare case
-    in
-    returnTc (varSetElems forall_tvs, lie_req, EmptyMonoBinds, [])
-
   where
-    tysig_names     = [name | (TySigInfo name _ _ _ _ _ _ _) <- sigs]
     is_unrestricted | opt_NoMonomorphismRestriction = True
                    | otherwise                     = isUnRestrictedGroup tysig_names mbind
-    lie_tvs = varSetElems (tyVarsOfInsts (lieToList lie_req))
-    check_doc = case tysig_names of
-                  [n]   -> ptext SLIT("type signature for")    <+> quotes (ppr n)
-                  other -> ptext SLIT("type signature(s) for") <+> pprBinders tysig_names
 
+    tysig_names = [name | (TySigInfo name _ _ _ _ _ _ _) <- sigs]
+    is_mono_sig (TySigInfo _ _ _ theta _ _ _ _) = null theta
+
+    doc = ptext SLIT("type signature(s) for") <+> pprBinders binder_names
 
+-----------------------
        -- CHECK THAT ALL THE SIGNATURE CONTEXTS ARE UNIFIABLE
        -- The type signatures on a mutually-recursive group of definitions
        -- must all have the same context (or none).
@@ -470,10 +461,9 @@ generalise binder_names mbind tau_tvs lie_req sigs
        -- We unify them because, with polymorphic recursion, their types
        -- might not otherwise be related.  This is a rather subtle issue.
        -- ToDo: amplify
-       --
-       -- We return a representative 
-checkSigsCtxts sigs@(TySigInfo _ id1 sig_tvs theta1 _ _ _ _ : other_sigs)
-  = mapTc_ check_one other_sigs                `thenTc_` 
+checkSigsCtxts sigs@(TySigInfo _ id1 sig_tvs theta1 _ _ _ src_loc : other_sigs)
+  = tcAddSrcLoc src_loc                        $
+    mapTc_ check_one other_sigs                `thenTc_` 
     if null theta1 then
        returnTc ([], [])               -- Non-overloaded type signatures
     else
@@ -487,23 +477,21 @@ checkSigsCtxts sigs@(TySigInfo _ id1 sig_tvs theta1 _ _ _ _ : other_sigs)
     returnTc (sig_avails, map instToId sig_dicts)
   where
     sig1_dict_tys = map mkPredTy theta1
-    n_sig1_theta  = length theta1
     sig_meths    = concat [insts | TySigInfo _ _ _ _ _ _ insts _ <- sigs]
 
     check_one sig@(TySigInfo _ id _ theta _ _ _ src_loc)
-       = tcAddSrcLoc src_loc                                   $
-        tcAddErrCtxt (sigContextsCtxt id1 id)                  $
-        checkTc (length theta == n_sig1_theta) sigContextsErr  `thenTc_`
+       = tcAddErrCtxt (sigContextsCtxt id1 id)                 $
+        checkTc (equalLength theta theta1) sigContextsErr      `thenTc_`
         unifyTauTyLists sig1_dict_tys (map mkPredTy theta)
 
 checkSigsTyVars sigs = mapTc_ check_one sigs
   where
     check_one (TySigInfo _ id sig_tyvars sig_theta sig_tau _ _ src_loc)
-      = tcAddSrcLoc src_loc                                                    $
-       tcAddErrCtxtM (sigCtxt (sig_msg id) sig_tyvars sig_theta sig_tau)       $
+      = tcAddSrcLoc src_loc                                            $
+       tcAddErrCtxt (ptext SLIT("When checking the type signature for") 
+                     <+> quotes (ppr id))                              $
+       tcAddErrCtxtM (sigCtxt sig_tyvars sig_theta sig_tau)            $
        checkSigTyVars sig_tyvars (idFreeTyVars id)
-
-    sig_msg id = ptext SLIT("When checking the type signature for") <+> quotes (ppr id)
 \end{code}
 
 @getTyVarsToGen@ decides what type variables to generalise over.
@@ -554,14 +542,14 @@ is_elem v vs = isIn "isUnResMono" v vs
 
 isUnRestrictedGroup sigs (PatMonoBind other        _ _) = False
 isUnRestrictedGroup sigs (VarMonoBind v _)             = v `is_elem` sigs
-isUnRestrictedGroup sigs (FunMonoBind v _ matches _)   = any isUnRestrictedMatch matches || 
+isUnRestrictedGroup sigs (FunMonoBind v _ matches _)   = isUnRestrictedMatch matches || 
                                                          v `is_elem` sigs
 isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)                = isUnRestrictedGroup sigs mb1 &&
                                                          isUnRestrictedGroup sigs mb2
 isUnRestrictedGroup sigs EmptyMonoBinds                        = True
 
-isUnRestrictedMatch (Match _ [] Nothing _) = False     -- No args, no signature
-isUnRestrictedMatch other                 = True       -- Some args or a signature
+isUnRestrictedMatch (Match [] _ _ : _) = False -- No args => like a pattern binding
+isUnRestrictedMatch other             = True   -- Some args => a function binding
 \end{code}
 
 
@@ -619,23 +607,6 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
     returnTc (mbinds', lie_req_pat `plusLIE` lie_req_rhss, names, mono_ids)
   where
 
-       -- This function is used when dealing with a LHS binder; 
-       -- we make a monomorphic version of the Id.  
-       -- We check for a type signature; if there is one, we use the mono_id
-       -- from the signature.  This is how we make sure the tau part of the
-       -- signature actually maatches the type of the LHS; then tc_mb_pats
-       -- ensures the LHS and RHS have the same type
-       
-    tc_pat_bndr name pat_ty
-       = case maybeSig tc_ty_sigs name of
-           Nothing
-               -> newLocalId (getOccName name) pat_ty (getSrcLoc name)
-
-           Just (TySigInfo _ _ _ _ _ mono_id _ _)
-               -> tcAddSrcLoc (getSrcLoc name)         $
-                  unifyTauTy (idType mono_id) pat_ty   `thenTc_`
-                  returnTc mono_id
-
     mk_bind (name, mono_id) = case maybeSig tc_ty_sigs name of
                                Nothing                                   -> (name, mono_id)
                                Just (TySigInfo name poly_id _ _ _ _ _ _) -> (name, poly_id)
@@ -658,9 +629,18 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
                  lie_avail1 `plusLIE` lie_avail2)
 
     tc_mb_pats (FunMonoBind name inf matches locn)
-      = newTyVarTy kind                `thenNF_Tc` \ bndr_ty -> 
-       tc_pat_bndr name bndr_ty        `thenTc` \ bndr_id ->
+      = (case maybeSig tc_ty_sigs name of
+           Just (TySigInfo _ _ _ _ _ mono_id _ _) 
+                   -> returnNF_Tc mono_id
+           Nothing -> newLocalName name        `thenNF_Tc` \ bndr_name ->
+                      newTyVarTy openTypeKind  `thenNF_Tc` \ bndr_ty -> 
+                       -- NB: not a 'hole' tyvar; since there is no type 
+                       -- signature, we revert to ordinary H-M typechecking
+                       -- which means the variable gets an inferred tau-type
+                      returnNF_Tc (mkLocalId bndr_name bndr_ty)
+       )                                       `thenNF_Tc` \ bndr_id ->
        let
+          bndr_ty         = idType bndr_id
           complete_it xve = tcAddSrcLoc locn                           $
                             tcMatchesFun xve name bndr_ty  matches     `thenTc` \ (matches', lie) ->
                             returnTc (FunMonoBind bndr_id inf matches' locn, lie)
@@ -669,33 +649,44 @@ tcMonoBinds mbinds tc_ty_sigs is_rec
 
     tc_mb_pats bind@(PatMonoBind pat grhss locn)
       = tcAddSrcLoc locn               $
-       newTyVarTy kind                 `thenNF_Tc` \ pat_ty -> 
+       newHoleTyVarTy                  `thenNF_Tc` \ pat_ty -> 
 
                --      Now typecheck the pattern
-               -- We don't support binding fresh type variables in the
-               -- pattern of a pattern binding.  For example, this is illegal:
+               -- We do now support binding fresh (not-already-in-scope) scoped 
+               -- type variables in the pattern of a pattern binding.  
+               -- For example, this is now legal:
                --      (x::a, y::b) = e
-               -- whereas this is ok
-               --      (x::Int, y::Bool) = e
-               --
-               -- We don't check explicitly for this problem.  Instead, we simply
-               -- type check the pattern with tcPat.  If the pattern mentions any
-               -- fresh tyvars we simply get an out-of-scope type variable error
+               -- The type variables are brought into scope in tc_binds_and_then,
+               -- so we don't have to do anything here.
+
        tcPat tc_pat_bndr pat pat_ty            `thenTc` \ (pat', lie_req, tvs, ids, lie_avail) ->
        let
           complete_it xve = tcAddSrcLoc locn                           $
                             tcAddErrCtxt (patMonoBindsCtxt bind)       $
                             tcExtendLocalValEnv xve                    $
-                            tcGRHSs grhss pat_ty PatBindRhs            `thenTc` \ (grhss', lie) ->
+                            tcGRHSs PatBindRhs grhss pat_ty            `thenTc` \ (grhss', lie) ->
                             returnTc (PatMonoBind pat' grhss' locn, lie)
        in
        returnTc (complete_it, lie_req, tvs, ids, lie_avail)
 
-       -- Figure out the appropriate kind for the pattern,
-       -- and generate a suitable type variable 
-    kind = case is_rec of
-               Recursive    -> liftedTypeKind  -- Recursive, so no unlifted types
-               NonRecursive -> openTypeKind    -- Non-recursive, so we permit unlifted types
+       -- tc_pat_bndr is used when dealing with a LHS binder in a pattern.
+       -- If there was a type sig for that Id, we want to make it much
+       -- as if that type signature had been on the binder as a SigPatIn.
+       -- We check for a type signature; if there is one, we use the mono_id
+       -- from the signature.  This is how we make sure the tau part of the
+       -- signature actually matches the type of the LHS; then tc_mb_pats
+       -- ensures the LHS and RHS have the same type
+       
+    tc_pat_bndr name pat_ty
+       = case maybeSig tc_ty_sigs name of
+           Nothing
+               -> newLocalName name    `thenNF_Tc` \ bndr_name ->
+                  tcMonoPatBndr bndr_name pat_ty
+
+           Just (TySigInfo _ _ _ _ _ mono_id _ _)
+               -> tcAddSrcLoc (getSrcLoc name)         $
+                  tcSubPat pat_ty (idType mono_id)     `thenTc` \ (co_fn, lie) ->
+                  returnTc (co_fn, lie, mono_id)
 \end{code}
 
 
@@ -748,7 +739,7 @@ tcSpecSigs (SpecSig name poly_ty src_loc : sigs)
     tcAddErrCtxt (valSpecSigCtxt name poly_ty) $
 
        -- Get and instantiate its alleged specialised type
-    tcHsSigType poly_ty                                `thenTc` \ sig_ty ->
+    tcHsSigType (FunSigCtxt name) poly_ty      `thenTc` \ sig_ty ->
 
        -- Check that f has a more general type, and build a RHS for
        -- the spec-pragma-id at the same time
@@ -760,11 +751,15 @@ tcSpecSigs (SpecSig name poly_ty src_loc : sigs)
        -- Just specialise "f" by building a SpecPragmaId binding
        -- It is the thing that makes sure we don't prematurely 
        -- dead-code-eliminate the binding we are really interested in.
-    newSpecPragmaId name sig_ty                `thenNF_Tc` \ spec_id ->
+    newLocalName name                  `thenNF_Tc` \ spec_name ->
+    let
+       spec_bind = VarMonoBind (mkSpecPragmaId spec_name sig_ty)
+                               (mkHsLet spec_binds spec_expr)
+    in
 
        -- Do the rest and combine
     tcSpecSigs sigs                    `thenTc` \ (binds_rest, lie_rest) ->
-    returnTc (binds_rest `andMonoBinds` VarMonoBind spec_id (mkHsLet spec_binds spec_expr),
+    returnTc (binds_rest `andMonoBinds` spec_bind,
              lie_rest   `plusLIE`      mkLIE spec_dicts)
 
 tcSpecSigs (other_sig : sigs) = tcSpecSigs sigs
@@ -792,9 +787,10 @@ valSpecSigCtxt v ty
 sigContextsErr = ptext SLIT("Mismatched contexts")
 
 sigContextsCtxt s1 s2
-  = hang (hsep [ptext SLIT("When matching the contexts of the signatures for"), 
-               quotes (ppr s1), ptext SLIT("and"), quotes (ppr s2)])
-        4 (ptext SLIT("(the signature contexts in a mutually recursive group should all be identical)"))
+  = vcat [ptext SLIT("When matching the contexts of the signatures for"), 
+         nest 2 (vcat [ppr s1 <+> dcolon <+> ppr (idType s1),
+                       ppr s2 <+> dcolon <+> ppr (idType s2)]),
+         ptext SLIT("The signature contexts in a mutually recursive group should all be identical")]
 
 -----------------------------------------------
 unliftedBindErr flavour mbind
@@ -814,6 +810,11 @@ restrictedBindCtxtErr binder_names
        4 (vcat [ptext SLIT("in a binding group for") <+> pprBinders binder_names,
                ptext SLIT("that falls under the monomorphism restriction")])
 
+genCtxt binder_names
+  = ptext SLIT("When generalising the type(s) for") <+> pprBinders binder_names
+
 -- Used in error messages
-pprBinders bndrs = braces (pprWithCommas ppr bndrs)
+-- 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}