[project @ 1997-05-26 01:52:30 by sof]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcBinds.lhs
index 3ce5967..d8f3a6c 100644 (file)
@@ -6,47 +6,69 @@
 \begin{code}
 #include "HsVersions.h"
 
-module TcBinds ( tcBindsAndThen, tcPragmaSigs ) where
+module TcBinds ( tcBindsAndThen, tcPragmaSigs, checkSigTyVars, tcBindWithSigs, TcSigInfo(..) ) where
 
 IMP_Ubiq()
 
-import HsSyn           ( HsBinds(..), Bind(..), Sig(..), MonoBinds(..), 
-                         HsExpr, Match, HsType, InPat, OutPat(..),
-                         GRHSsAndBinds, ArithSeqInfo, HsLit, Fake,
-                         collectBinders )
-import RnHsSyn         ( SYN_IE(RenamedHsBinds), SYN_IE(RenamedBind), RenamedSig(..), 
+import HsSyn           ( HsBinds(..), Sig(..), MonoBinds(..), 
+                         Match, HsType, InPat(..), OutPat(..), HsExpr(..),
+                         SYN_IE(RecFlag), nonRecursive,
+                         GRHSsAndBinds, ArithSeqInfo, HsLit, Fake, Stmt, DoOrListComp, Fixity, 
+                         collectMonoBinders )
+import RnHsSyn         ( SYN_IE(RenamedHsBinds), RenamedSig(..), 
                          SYN_IE(RenamedMonoBinds)
                        )
-import TcHsSyn         ( SYN_IE(TcHsBinds), SYN_IE(TcBind), SYN_IE(TcMonoBinds),
-                         TcIdOcc(..), SYN_IE(TcIdBndr) )
+import TcHsSyn         ( SYN_IE(TcHsBinds), SYN_IE(TcMonoBinds),
+                         TcIdOcc(..), SYN_IE(TcIdBndr), SYN_IE(TcExpr), 
+                         tcIdType
+                       )
 
 import TcMonad
-import GenSpecEtc      ( checkSigTyVars, genBinds, TcSigInfo(..) )
-import Inst            ( Inst, SYN_IE(LIE), emptyLIE, plusLIE, InstOrigin(..) )
-import TcEnv           ( tcExtendLocalValEnv, tcLookupLocalValueOK, newMonoIds )
+import Inst            ( Inst, SYN_IE(LIE), emptyLIE, plusLIE, InstOrigin(..),
+                         newDicts, tyVarsOfInst, instToId
+                       )
+import TcEnv           ( tcExtendLocalValEnv, tcLookupLocalValueOK, newMonoIds,
+                         tcGetGlobalTyVars, tcExtendGlobalTyVars
+                       )
 import SpecEnv         ( SpecEnv )
 IMPORT_DELOOPER(TcLoop)                ( tcGRHSsAndBinds )
 import TcMatches       ( tcMatchesFun )
+import TcSimplify      ( tcSimplify, tcSimplifyAndCheck )
 import TcMonoType      ( tcHsType )
 import TcPat           ( tcPat )
 import TcSimplify      ( bindInstsOfLocalFuns )
-import TcType          ( newTcTyVar, tcInstSigType, newTyVarTys )
-import Unify           ( unifyTauTy )
+import TcType          ( SYN_IE(TcType), SYN_IE(TcThetaType), SYN_IE(TcTauType), 
+                         SYN_IE(TcTyVarSet), SYN_IE(TcTyVar),
+                         newTyVarTy, zonkTcType, zonkTcTyVar, zonkTcTyVars,
+                         newTcTyVar, tcInstSigType, newTyVarTys
+                       )
+import Unify           ( unifyTauTy, unifyTauTyLists )
 
-import Kind            ( mkBoxedTypeKind, mkTypeKind )
+import Kind            ( isUnboxedTypeKind, mkTypeKind, isTypeKind, mkBoxedTypeKind )
 import Id              ( GenId, idType, mkUserLocal, mkUserId )
 import IdInfo          ( noIdInfo )
-import Maybes          ( assocMaybe, catMaybes )
-import Name            ( pprNonSym, getOccName, getSrcLoc, Name )
+import Maybes          ( maybeToBool, assocMaybe, catMaybes )
+import Name            ( getOccName, getSrcLoc, Name )
 import PragmaInfo      ( PragmaInfo(..) )
 import Pretty
-import Type            ( mkTyVarTy, mkTyVarTys, isTyVarTy,
-                         mkSigmaTy, splitSigmaTy,
+import Type            ( mkTyVarTy, mkTyVarTys, isTyVarTy, tyVarsOfTypes, eqSimpleTheta, 
+                         mkSigmaTy, splitSigmaTy, mkForAllTys, mkFunTys, getTyVar, mkDictTy,
                          splitRhoTy, mkForAllTy, splitForAllTy )
-import Bag             ( bagToList )
-import Util            ( isIn, zipEqual, zipWith3Equal, panic )
+import TyVar           ( GenTyVar, SYN_IE(TyVar), tyVarKind, minusTyVarSet, emptyTyVarSet,
+                         elementOfTyVarSet, unionTyVarSets, tyVarSetToList )
+import Bag             ( bagToList, foldrBag, isEmptyBag )
+import Util            ( isIn, zipEqual, zipWithEqual, zipWith3Equal, hasNoDups, assoc,
+                         assertPanic, panic, pprTrace )
+import PprType         ( GenClass, GenType, GenTyVar )
+import Unique          ( Unique )
+import SrcLoc           ( SrcLoc )
+
+import Outputable      --( interppSP, interpp'SP )
+
+
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Type-checking bindings}
@@ -64,7 +86,7 @@ specialising the things bound.
 @tcBindsAndThen@ also takes a "combiner" which glues together the
 bindings and the "thing" to make a new "thing".
 
-The real work is done by @tcBindAndThen@.
+The real work is done by @tcBindWithSigsAndThen@.
 
 Recursive and non-recursive binds are handled in essentially the same
 way: because of uniques there are no scoping issues left.  The only
@@ -82,21 +104,55 @@ dictionaries, which we resolve at the module level.
 tcBindsAndThen
        :: (TcHsBinds s -> thing -> thing)              -- Combinator
        -> RenamedHsBinds
-       -> TcM s (thing, LIE s, thing_ty)
-       -> TcM s (thing, LIE s, thing_ty)
+       -> TcM s (thing, LIE s)
+       -> TcM s (thing, LIE s)
 
 tcBindsAndThen combiner EmptyBinds do_next
-  = do_next    `thenTc` \ (thing, lie, thing_ty) ->
-    returnTc (combiner EmptyBinds thing, lie, thing_ty)
-
-tcBindsAndThen combiner (SingleBind bind) do_next
-  = tcBindAndThen combiner bind [] do_next
-
-tcBindsAndThen combiner (BindWith bind sigs) do_next
-  = tcBindAndThen combiner bind sigs do_next
+  = do_next    `thenTc` \ (thing, lie) ->
+    returnTc (combiner EmptyBinds thing, lie)
 
 tcBindsAndThen combiner (ThenBinds binds1 binds2) do_next
   = tcBindsAndThen combiner binds1 (tcBindsAndThen combiner binds2 do_next)
+
+tcBindsAndThen combiner (MonoBind bind sigs is_rec) do_next
+  = fixTc (\ ~(prag_info_fn, _) ->
+       -- This is the usual prag_info fix; the PragmaInfo field of an Id
+       -- is not inspected till ages later in the compiler, so there
+       -- should be no black-hole problems here.
+
+       -- TYPECHECK THE SIGNATURES
+    mapTc (tcTySig prag_info_fn) ty_sigs               `thenTc` \ tc_ty_sigs ->
+
+    tcBindWithSigs binder_names bind 
+                  tc_ty_sigs is_rec prag_info_fn       `thenTc` \ (poly_binds, poly_lie, poly_ids) ->
+
+       -- Extend the environment to bind the new polymorphic Ids
+    tcExtendLocalValEnv binder_names poly_ids $
+
+       -- Build bindings and IdInfos corresponding to user pragmas
+    tcPragmaSigs sigs                  `thenTc` \ (prag_info_fn, prag_binds, prag_lie) ->
+
+       -- Now do whatever happens next, in the augmented envt
+    do_next                            `thenTc` \ (thing, thing_lie) ->
+
+       -- Create specialisations of functions bound here
+    bindInstsOfLocalFuns (prag_lie `plusLIE` thing_lie)
+                         poly_ids      `thenTc` \ (lie2, inst_mbinds) ->
+
+       -- All done
+    let
+       final_lie   = lie2 `plusLIE` poly_lie
+       final_binds = MonoBind poly_binds  [] is_rec            `ThenBinds`
+                     MonoBind inst_mbinds [] nonRecursive      `ThenBinds`
+                     prag_binds
+    in
+    returnTc (prag_info_fn, (combiner final_binds thing, final_lie))
+    )                                  `thenTc` \ (_, result) ->
+    returnTc result
+  where
+    binder_names = map fst (bagToList (collectMonoBinders bind))
+    ty_sigs      = [sig  | sig@(Sig name _ _) <- sigs]
+
 \end{code}
 
 An aside.  The original version of @tcBindsAndThen@ which lacks a
@@ -115,212 +171,168 @@ tcBindsAndThen EmptyBinds do_next
   = do_next            `thenTc` \ (thing, lie, thing_ty) ->
     returnTc ((EmptyBinds, thing), lie, thing_ty)
 
-tcBindsAndThen (SingleBind bind) do_next
-  = tcBindAndThen bind [] do_next
-
-tcBindsAndThen (BindWith bind sigs) do_next
-  = tcBindAndThen bind sigs do_next
-
 tcBindsAndThen (ThenBinds binds1 binds2) do_next
   = tcBindsAndThen binds1 (tcBindsAndThen binds2 do_next)
        `thenTc` \ ((binds1', (binds2', thing')), lie1, thing_ty) ->
 
     returnTc ((binds1' `ThenBinds` binds2', thing'), lie1, thing_ty)
+
+tcBindsAndThen (MonoBind bind sigs is_rec) do_next
+  = tcBindAndThen bind sigs do_next
 \end{pseudocode}
 
+
 %************************************************************************
 %*                                                                     *
-\subsection{Bind}
+\subsection{tcBindWithSigs}
 %*                                                                     *
 %************************************************************************
 
-\begin{code}
-tcBindAndThen
-       :: (TcHsBinds s -> thing -> thing)                -- Combinator
-       -> RenamedBind                                    -- The Bind to typecheck
-       -> [RenamedSig]                                   -- ...and its signatures
-       -> TcM s (thing, LIE s, thing_ty)                 -- Thing to type check in
-                                                         -- augmented envt
-       -> TcM s (thing, LIE s, thing_ty)                 -- Results, incl the
-
-tcBindAndThen combiner bind sigs do_next
-  = fixTc (\ ~(prag_info_fn, _) ->
-       -- This is the usual prag_info fix; the PragmaInfo field of an Id
-       -- is not inspected till ages later in the compiler, so there
-       -- should be no black-hole problems here.
-    
-    tcBindAndSigs binder_names bind 
-                 sigs prag_info_fn     `thenTc` \ (poly_binds, poly_lie, poly_ids) ->
-
-       -- Extend the environment to bind the new polymorphic Ids
-    tcExtendLocalValEnv binder_names poly_ids $
+@tcBindWithSigs@ deals with a single binding group.  It does generalisation,
+so all the clever stuff is in here.
 
-       -- Build bindings and IdInfos corresponding to user pragmas
-    tcPragmaSigs sigs                  `thenTc` \ (prag_info_fn, prag_binds, prag_lie) ->
+* binder_names and mbind must define the same set of Names
 
-       -- Now do whatever happens next, in the augmented envt
-    do_next                            `thenTc` \ (thing, thing_lie, thing_ty) ->
+* The Names in tc_ty_sigs must be a subset of binder_names
 
-       -- Create specialisations of functions bound here
-    bindInstsOfLocalFuns (prag_lie `plusLIE` thing_lie)
-                         poly_ids      `thenTc` \ (lie2, inst_mbinds) ->
-
-       -- All done
-    let
-       final_lie   = lie2 `plusLIE` poly_lie
-       final_binds = poly_binds `ThenBinds`
-                     SingleBind (NonRecBind inst_mbinds) `ThenBinds`
-                     prag_binds
-    in
-    returnTc (prag_info_fn, (combiner final_binds thing, final_lie, thing_ty))
-    )                                  `thenTc` \ (_, result) ->
-    returnTc result
-  where
-    binder_names = map fst (bagToList (collectBinders bind))
+* The Ids in tc_ty_sigs don't necessarily have to have the same name
+  as the Name in the tc_ty_sig
 
-
-tcBindAndSigs binder_names bind sigs prag_info_fn
+\begin{code}
+tcBindWithSigs 
+       :: [Name]
+       -> RenamedMonoBinds
+       -> [TcSigInfo s]
+       -> RecFlag
+       -> (Name -> PragmaInfo)
+       -> TcM s (TcMonoBinds s, LIE s, [TcIdBndr s])
+
+tcBindWithSigs binder_names mbind tc_ty_sigs is_rec prag_info_fn
   = recoverTc (
        -- If typechecking the binds fails, then return with each
-       -- binder given type (forall a.a), to minimise subsequent
+       -- signature-less binder given type (forall a.a), to minimise subsequent
        -- error messages
        newTcTyVar mkBoxedTypeKind              `thenNF_Tc` \ alpha_tv ->
        let
          forall_a_a = mkForAllTy alpha_tv (mkTyVarTy alpha_tv)
-         poly_ids   = [ mkUserId name forall_a_a (prag_info_fn name)
-                      | name <- binder_names]
+         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 -> mkUserId name forall_a_a NoPragmaInfo    -- No signature
        in
-       returnTc (EmptyBinds, emptyLIE, poly_ids)
+       returnTc (EmptyMonoBinds, emptyLIE, poly_ids)
     ) $
 
-       -- Create a new identifier for each binder, with each being given
+       -- Create a new identifier for each binder, with each being given
        -- a fresh unique, and a type-variable type.
     tcGetUniques no_of_binders                 `thenNF_Tc` \ uniqs ->
-    newTyVarTys no_of_binders kind             `thenNF_Tc` \ tys ->
+    mapNF_Tc mk_mono_id_ty binder_names        `thenNF_Tc` \ mono_id_tys ->
     let
-       mono_ids           = zipWith3Equal "tcBindAndSigs" mk_id binder_names uniqs tys
+       mono_id_tyvars     = tyVarsOfTypes mono_id_tys
+       mono_ids           = zipWith3Equal "tcBindAndSigs" mk_id binder_names uniqs mono_id_tys
        mk_id name uniq ty = mkUserLocal (getOccName name) uniq ty (getSrcLoc name)
     in
-    tcExtendLocalValEnv binder_names mono_ids (
-           tcTySigs sigs               `thenTc` \ sig_info ->
-           tc_bind bind                `thenTc` \ (bind', lie) ->
-           returnTc (bind', lie, sig_info)
-    )
-           `thenTc` \ (bind', lie, sig_info) ->
-
-           -- Notice that genBinds gets the old (non-extended) environment
-    genBinds binder_names mono_ids bind' lie sig_info prag_info_fn
-  where
-    no_of_binders = length binder_names
-    kind = case bind of
-               NonRecBind _ -> mkTypeKind      -- Recursive, so no unboxed types
-               RecBind _    -> mkBoxedTypeKind -- Non-recursive, so we permit unboxed types
-\end{code}
-
-
-===========
-\begin{code}
-{-
 
-data SigInfo
-  = SigInfo    Name
-               (TcIdBndr s)            -- Polymorpic version
-               (TcIdBndr s)            -- Monomorphic verstion
-               [TcType s] [TcIdOcc s]  -- Instance information for the monomorphic version
-
-
-
-       -- Deal with type signatures
-    tcTySigs sigs              `thenTc` \ sig_infos ->
+       -- TYPECHECK THE BINDINGS
+    tcMonoBinds mbind binder_names mono_ids tc_ty_sigs `thenTc` \ (mbind', lie) ->
+
+       -- CHECK THAT THE SIGNATURES MATCH
+       -- (must do this before getTyVarsToGen)
+    checkSigMatch tc_ty_sigs                           `thenTc` \ sig_theta ->
+       
+       -- COMPUTE VARIABLES OVER WHICH TO QUANTIFY, namely tyvars_to_gen
+       -- The tyvars_not_to_gen are free in the environment, and hence
+       -- candidates for generalisation, but sometimes the monomorphism
+       -- restriction means we can't generalise them nevertheless
+    getTyVarsToGen is_unrestricted mono_id_tyvars lie  `thenTc` \ (tyvars_not_to_gen, tyvars_to_gen) ->
+
+       -- DEAL WITH TYPE VARIABLE KINDS
+    mapTc defaultUncommittedTyVar (tyVarSetToList tyvars_to_gen)       `thenTc` \ tyvars_to_gen_list ->
+               -- It's important that the final list (tyvars_to_gen_list) is fully
+               -- zonked, *including boxity*, because they'll be included in the forall types of
+               -- the polymorphic Ids, and instances of these Ids will be generated from them.
+               --
+               -- This step can do unification => keep other zonking after this
+
+       -- SIMPLIFY THE LIE
+    tcExtendGlobalTyVars tyvars_not_to_gen (
+       if null tc_ty_sigs then
+               -- No signatures, so just simplify the lie
+           tcSimplify tyvars_to_gen lie                `thenTc` \ (lie_free, dict_binds, lie_bound) ->
+           returnTc (lie_free, dict_binds, map instToId (bagToList lie_bound))
+
+       else
+           zonk_theta sig_theta                        `thenNF_Tc` \ sig_theta' ->
+           newDicts SignatureOrigin sig_theta'         `thenNF_Tc` \ (dicts_sig, dict_ids) ->
+               -- It's important that sig_theta is zonked, because
+               -- dict_id is later used to form the type of the polymorphic thing,
+               -- and forall-types must be zonked so far as their bound variables
+               -- are concerned
+
+               -- Check that the needed dicts can be expressed in
+               -- terms of the signature ones
+           tcAddErrCtxt (sigsCtxt tysig_names) $
+           tcSimplifyAndCheck tyvars_to_gen dicts_sig lie      `thenTc` \ (lie_free, dict_binds) ->
+           returnTc (lie_free, dict_binds, dict_ids)
+
+    )                                          `thenTc` \ (lie_free, dict_binds, dicts_bound) ->
+
+    ASSERT( not (any (isUnboxedTypeKind . tyVarKind) tyvars_to_gen_list) )
+               -- 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.
+
+        -- BUILD THE POLYMORPHIC RESULT IDs
+    mapNF_Tc zonkTcType mono_id_tys                    `thenNF_Tc` \ zonked_mono_id_types ->
     let
-       sig_binders   = [binder      | SigInfo binder _ _ _ _  <- sig_infos]
-       poly_sigs     = [(name,poly) | SigInfo name poly _ _ _ <- sig_infos]
-       mono_sigs     = [(name,mono) | SigInfo name _ mono _ _ <- sig_infos]
-       nosig_binders = binders `minusList` sig_binders
+       exports  = zipWith3 mk_export binder_names mono_ids zonked_mono_id_types
+       dict_tys = map tcIdType dicts_bound
+
+       mk_export binder_name mono_id zonked_mono_id_ty
+         | maybeToBool maybe_sig = (sig_tyvars,         TcId sig_poly_id, TcId mono_id)
+         | otherwise             = (tyvars_to_gen_list, TcId poly_id,     TcId mono_id)
+         where
+           maybe_sig = maybeSig tc_ty_sigs binder_name
+           Just (TySigInfo _ sig_poly_id sig_tyvars _ _ _) = maybe_sig
+           poly_id = mkUserId binder_name poly_ty (prag_info_fn binder_name)
+           poly_ty = mkForAllTys tyvars_to_gen_list $ mkFunTys dict_tys $ zonked_mono_id_ty
+                               -- 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
+                               -- it appears to have free tyvars that aren't actually free at all.
     in
 
+        -- BUILD RESULTS
+    returnTc (
+        AbsBinds tyvars_to_gen_list
+                 dicts_bound
+                 exports
+                 (dict_binds `AndMonoBinds` mbind'),
+        lie_free,
+        [poly_id | (_, TcId poly_id, _) <- exports]
+    )
+  where
+    no_of_binders = length binder_names
 
-       -- Typecheck the binding group
-    tcExtendLocalEnv poly_sigs         (
-    newLocalIds nosig_binders kind     (\ nosig_local_ids ->
-           tcMonoBinds mono_sigs mono_binds    `thenTc` \ binds_w_lies ->
-           returnTc (nosig_local_ids, binds_w_lies)
-    ))                                 `thenTc` \ (nosig_local_ids, binds_w_lies) ->
-
-
-       -- Decide what to generalise over
-    getImplicitStuffToGen sig_ids binds_w_lies 
-                       `thenTc` \ (tyvars_not_to_gen, tyvars_to_gen, lie_to_gen) ->
-
-
-       *** CHECK FOR UNBOXED TYVARS HERE! ***
-
-
+    mk_mono_id_ty binder_name = case maybeSig tc_ty_sigs binder_name of
+                                 Just (TySigInfo name _ _ _ tau_ty _) -> returnNF_Tc tau_ty -- There's a signature
+                                 otherwise                            -> newTyVarTy kind    -- No signature
 
-       -- Make poly_ids for all the binders that don't have type signatures
-    let
-       tys_to_gen   = mkTyVarTys tyvars_to_gen
-       dicts_to_gen = map instToId (bagToList lie_to_gen)
-       dict_tys     = map tcIdType dicts_to_gen
-
-       mk_poly binder local_id = mkUserId (getName binder) ty noPragmaInfo
-                      where
-                         ty = mkForAllTys tyvars_to_gen $
-                              mkFunTys dict_tys $
-                              tcIdType local_id
-
-       more_sig_infos = [ SigInfo binder (mk_poly binder local_id) 
-                                  local_id tys_to_gen dicts_to_gen lie_to_gen
-                        | (binder, local_id) <- zipEqual "???" nosig_binders nosig_local_ids
-                        ]
-
-       all_sig_infos = sig_infos ++ more_sig_infos     -- Contains a "signature" for each binder
-    in
+    tysig_names     = [name | (TySigInfo name _ _ _ _ _) <- tc_ty_sigs]
+    is_unrestricted = isUnRestrictedGroup tysig_names mbind
 
+    kind | is_rec    = mkBoxedTypeKind -- Recursive, so no unboxed types
+        | otherwise = mkTypeKind               -- Non-recursive, so we permit unboxed types
 
-       -- Now generalise the bindings
-    let
-       -- local_binds is a bunch of bindings of the form
-       --      f_mono = f_poly tyvars dicts
-       -- one for each binder, f, that lacks a type signature.
-       -- This bunch of bindings is put at the top of the RHS of every
-       -- binding in the group, so as to bind all the f_monos.
-               
-       local_binds = [ (local_id, mkHsDictApp (mkHsTyApp (HsVar local_id) tys_to_gen) dicts_to_gen)
-                     | local_id <- nosig_local_ids
-                     ]
-
-        find_sig lid = head [ (pid, tvs, ds, lie) 
-                         | SigInfo _ pid lid' tvs ds lie, 
-                           lid==lid'
-                         ]
-
-      gen_bind (bind, lie)
-       = tcSimplifyWithExtraGlobals tyvars_not_to_gen tyvars_to_gen avail lie
-                                   `thenTc` \ (lie_free, dict_binds) ->
-         returnTc (AbsBind tyvars_to_gen_here
-                           dicts
-                           (zipEqual "gen_bind" local_ids poly_ids)
-                           (dict_binds ++ local_binds)
-                           bind,
-                   lie_free)
+zonk_theta theta = mapNF_Tc zonk theta
        where
-         local_ids  = bindersOf bind
-         local_sigs = [sig | sig@(SigInfo _ _ local_id _ _) <- all_sig_infos,
-                             local_id `elem` local_ids
-                      ]
-
-         (tyvars_to_gen_here, dicts, avail) 
-               = case (local_ids, sigs) of
-
-                   ([local_id], [SigInfo _ _ _ tyvars_to_gen dicts lie])
-                         -> (tyvars_to_gen, dicts, lie)
-
-                   other -> (tyvars_to_gen, dicts, avail)
+         zonk (c,t) = zonkTcType t     `thenNF_Tc` \ t' ->
+                      returnNF_Tc (c,t')
 \end{code}
 
-@getImplicitStuffToGen@ decides what type variables
-and LIE to generalise over.
+@getImplicitStuffToGen@ decides what type variables generalise over.
 
 For a "restricted group" -- see the monomorphism restriction
 for a definition -- we bind no dictionaries, and
@@ -336,9 +348,10 @@ stuff.  If we simplify only at the f-binding (not the xs-binding)
 we'll know that the literals are all Ints, and we can just produce
 Int literals!
 
-Find all the type variables involved in overloading, the "constrained_tyvars"
-These are the ones we *aren't* going to generalise.
-We must be careful about doing this:
+Find all the type variables involved in overloading, the
+"constrained_tyvars".  These are the ones we *aren't* going to
+generalise.  We must be careful about doing this:
+
  (a) If we fail to generalise a tyvar which is not actually
        constrained, then it will never, ever get bound, and lands
        up printed out in interface files!  Notorious example:
@@ -347,6 +360,7 @@ We must be careful about doing this:
        Another, more common, example is when there's a Method inst in
        the LIE, whose type might very well involve non-overloaded
        type variables.
+
  (b) On the other hand, we mustn't generalise tyvars which are constrained,
        because we are going to pass on out the unmodified LIE, with those
        tyvars in it.  They won't be in scope if we've generalised them.
@@ -356,86 +370,107 @@ constrained tyvars. We don't use any of the results, except to
 find which tyvars are constrained.
 
 \begin{code}
-getImplicitStuffToGen is_restricted sig_ids binds_w_lies
-  | isUnRestrictedGroup tysig_vars bind
-  = tcSimplify tyvars_to_gen lie       `thenTc` \ (_, _, dicts_to_gen) ->
-    returnNF_Tc (emptyTyVarSet, tyvars_to_gen, dicts_to_gen)
-
-  | otherwise
-  = tcSimplify tyvars_to_gen lie           `thenTc` \ (_, _, constrained_dicts) ->
-     let
+getTyVarsToGen is_unrestricted mono_tyvars lie
+  = tcGetGlobalTyVars                          `thenNF_Tc` \ free_tyvars ->
+    zonkTcTyVars mono_tyvars                   `thenNF_Tc` \ mentioned_tyvars ->
+    let
+       tyvars_to_gen    = mentioned_tyvars `minusTyVarSet` free_tyvars
+    in
+    if is_unrestricted
+    then
+       returnTc (emptyTyVarSet, tyvars_to_gen)
+    else
+       tcSimplify tyvars_to_gen lie        `thenTc` \ (_, _, constrained_dicts) ->
+       let
          -- ASSERT: dicts_sig is already zonked!
-         constrained_tyvars    = foldBag unionTyVarSets tyVarsOfInst emptyTyVarSet constrained_dicts
-         reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
-     in
-     returnTc (constrained_tyvars, reduced_tyvars_to_gen, emptyLIE)
-
-  where
-    sig_vars   = [sig_var | (TySigInfo sig_var _ _ _ _) <- ty_sigs]
-
-    (tyvars_to_gen, lie) = foldBag (\(tv1,lie2) (tv2,lie2) -> (tv1 `unionTyVarSets` tv2,
-                                                              lie1 `plusLIE` lie2))
-                                   get
-                                   (emptyTyVarSet, emptyLIE)
-                                   binds_w_lies
-    get (bind, lie)
-      = case bindersOf bind of
-         [local_id] | local_id `in` sig_ids ->         -- A simple binding with
-                                                       -- a type signature
-                       (emptyTyVarSet, emptyLIE)
-
-         local_ids ->                                  -- Complex binding or no type sig
-                       (foldr (unionTyVarSets . tcIdType) emptyTyVarSet local_ids, 
-                        lie)
--}
+           constrained_tyvars    = foldrBag (unionTyVarSets . tyVarsOfInst) emptyTyVarSet constrained_dicts
+           reduced_tyvars_to_gen = tyvars_to_gen `minusTyVarSet` constrained_tyvars
+        in
+        returnTc (constrained_tyvars, reduced_tyvars_to_gen)
 \end{code}
-                          
 
 
 \begin{code}
-tc_bind :: RenamedBind -> TcM s (TcBind s, LIE s)
+isUnRestrictedGroup :: [Name]          -- Signatures given for these
+                   -> RenamedMonoBinds
+                   -> Bool
 
-tc_bind (NonRecBind mono_binds)
-  = tcMonoBinds mono_binds     `thenTc` \ (mono_binds2, lie) ->
-    returnTc  (NonRecBind mono_binds2, lie)
+is_elem v vs = isIn "isUnResMono" v vs
 
-tc_bind (RecBind mono_binds)
-  = tcMonoBinds mono_binds     `thenTc` \ (mono_binds2, lie) ->
-    returnTc  (RecBind mono_binds2, lie)
+isUnRestrictedGroup sigs (PatMonoBind (VarPatIn v) _ _) = v `is_elem` sigs
+isUnRestrictedGroup sigs (PatMonoBind other      _ _)  = False
+isUnRestrictedGroup sigs (VarMonoBind v _)             = v `is_elem` sigs
+isUnRestrictedGroup sigs (FunMonoBind _ _ _ _)         = True
+isUnRestrictedGroup sigs (AndMonoBinds mb1 mb2)                = isUnRestrictedGroup sigs mb1 &&
+                                                         isUnRestrictedGroup sigs mb2
+isUnRestrictedGroup sigs EmptyMonoBinds                        = True
 \end{code}
 
-\begin{code}
-tcMonoBinds :: RenamedMonoBinds -> TcM s (TcMonoBinds s, LIE s)
-
-tcMonoBinds EmptyMonoBinds = returnTc (EmptyMonoBinds, emptyLIE)
-
-tcMonoBinds (AndMonoBinds mb1 mb2)
-  = tcMonoBinds mb1            `thenTc` \ (mb1a, lie1) ->
-    tcMonoBinds mb2            `thenTc` \ (mb2a, lie2) ->
-    returnTc (AndMonoBinds mb1a mb2a, lie1 `plusLIE` lie2)
+@defaultUncommittedTyVar@ checks for generalisation over unboxed
+types, and defaults any TypeKind TyVars to BoxedTypeKind.
 
-tcMonoBinds bind@(PatMonoBind pat grhss_and_binds locn)
-  = tcAddSrcLoc locn            $
+\begin{code}
+defaultUncommittedTyVar tyvar
+  | isTypeKind (tyVarKind tyvar)
+  = newTcTyVar mkBoxedTypeKind                                 `thenNF_Tc` \ boxed_tyvar ->
+    unifyTauTy (mkTyVarTy boxed_tyvar) (mkTyVarTy tyvar)       `thenTc_`
+    returnTc boxed_tyvar
 
-       -- LEFT HAND SIDE
-    tcPat pat                          `thenTc` \ (pat2, lie_pat, pat_ty) ->
+  | otherwise
+  = returnTc tyvar
+\end{code}
 
-       -- BINDINGS AND GRHSS
-    tcGRHSsAndBinds grhss_and_binds    `thenTc` \ (grhss_and_binds2, lie, grhss_ty) ->
 
-       -- Unify the two sides
-    tcAddErrCtxt (patMonoBindsCtxt bind) $
-       unifyTauTy pat_ty grhss_ty                      `thenTc_`
+%************************************************************************
+%*                                                                     *
+\subsection{tcMonoBind}
+%*                                                                     *
+%************************************************************************
 
-       -- RETURN
-    returnTc (PatMonoBind pat2 grhss_and_binds2 locn,
-             plusLIE lie_pat lie)
+@tcMonoBinds@ deals with a single @MonoBind@.  
+The signatures have been dealt with already.
 
-tcMonoBinds (FunMonoBind name inf matches locn)
-  = tcAddSrcLoc locn                           $
-    tcLookupLocalValueOK "tcMonoBinds" name    `thenNF_Tc` \ id ->
-    tcMatchesFun name (idType id) matches      `thenTc` \ (matches', lie) ->
-    returnTc (FunMonoBind (TcId id) inf matches' locn, lie)
+\begin{code}
+tcMonoBinds :: RenamedMonoBinds 
+           -> [Name] -> [TcIdBndr s]
+           -> [TcSigInfo s]
+           -> TcM s (TcMonoBinds s, LIE s)
+
+tcMonoBinds mbind binder_names mono_ids tc_ty_sigs
+  = tcExtendLocalValEnv binder_names mono_ids (
+       tc_mono_binds mbind
+    )
+  where
+    sig_names = [name | (TySigInfo name _ _ _ _ _) <- tc_ty_sigs]
+    sig_ids   = [id   | (TySigInfo _   id _ _ _ _) <- tc_ty_sigs]
+
+    tc_mono_binds EmptyMonoBinds = returnTc (EmptyMonoBinds, emptyLIE)
+
+    tc_mono_binds (AndMonoBinds mb1 mb2)
+      = tc_mono_binds mb1              `thenTc` \ (mb1a, lie1) ->
+        tc_mono_binds mb2              `thenTc` \ (mb2a, lie2) ->
+        returnTc (AndMonoBinds mb1a mb2a, lie1 `plusLIE` lie2)
+
+    tc_mono_binds (FunMonoBind name inf matches locn)
+      = tcAddSrcLoc locn                               $
+       tcLookupLocalValueOK "tc_mono_binds" name       `thenNF_Tc` \ id ->
+
+               -- Before checking the RHS, extend the envt with
+               -- bindings for the *polymorphic* Ids from any type signatures
+       tcExtendLocalValEnv sig_names sig_ids           $
+       tcMatchesFun name (idType id) matches           `thenTc` \ (matches', lie) ->
+
+       returnTc (FunMonoBind (TcId id) inf matches' locn, lie)
+
+    tc_mono_binds bind@(PatMonoBind pat grhss_and_binds locn)
+      = tcAddSrcLoc locn                       $
+       tcPat pat                               `thenTc` \ (pat2, lie_pat, pat_ty) ->
+       tcExtendLocalValEnv sig_names sig_ids   $
+       tcGRHSsAndBinds grhss_and_binds         `thenTc` \ (grhss_and_binds2, lie, grhss_ty) ->
+       tcAddErrCtxt (patMonoBindsCtxt bind)    $
+       unifyTauTy pat_ty grhss_ty              `thenTc_`
+       returnTc (PatMonoBind pat2 grhss_and_binds2 locn,
+                 plusLIE lie_pat lie)
 \end{code}
 
 %************************************************************************
@@ -449,28 +484,138 @@ tcMonoBinds (FunMonoBind name inf matches locn)
 split up, and have fresh type variables installed.  All non-type-signature
 "RenamedSigs" are ignored.
 
+The @TcSigInfo@ contains @TcTypes@ because they are unified with
+the variable's type, and after that checked to see whether they've
+been instantiated.
+
 \begin{code}
-tcTySigs :: [RenamedSig] -> TcM s [TcSigInfo s]
+data TcSigInfo s
+  = TySigInfo      Name
+                   (TcIdBndr s)        -- *Polymorphic* binder for this value...
+                   [TcTyVar s] (TcThetaType s) (TcTauType s)
+                   SrcLoc
+
+
+maybeSig :: [TcSigInfo s] -> Name -> Maybe (TcSigInfo s)
+       -- Search for a particular signature
+maybeSig [] name = Nothing
+maybeSig (sig@(TySigInfo sig_name _ _ _ _ _) : sigs) name
+  | name == sig_name = Just sig
+  | otherwise       = maybeSig sigs name
+\end{code}
 
-tcTySigs (Sig v ty src_loc : other_sigs)
- = tcAddSrcLoc src_loc (
-       tcHsType ty                     `thenTc` \ sigma_ty ->
-       tcInstSigType sigma_ty          `thenNF_Tc` \ sigma_ty' ->
-       let
-           (tyvars', theta', tau') = splitSigmaTy sigma_ty'
-       in
 
-       tcLookupLocalValueOK "tcSig1" v `thenNF_Tc` \ val ->
-       unifyTauTy (idType val) tau'    `thenTc_`
+\begin{code}
+tcTySig :: (Name -> PragmaInfo)
+       -> RenamedSig
+       -> TcM s (TcSigInfo s)
+
+tcTySig prag_info_fn (Sig v ty src_loc)
+ = tcAddSrcLoc src_loc $
+   tcHsType ty                 `thenTc` \ sigma_ty ->
+   tcInstSigType sigma_ty      `thenNF_Tc` \ sigma_ty' ->
+   let
+     poly_id = mkUserId v sigma_ty' (prag_info_fn v)
+     (tyvars', theta', tau') = splitSigmaTy sigma_ty'
+       -- This splitSigmaTy tries hard to make sure that tau' is a type synonym
+       -- wherever possible, which can improve interface files.
+   in
+   returnTc (TySigInfo v poly_id tyvars' theta' tau' src_loc)
+\end{code}
+
+@checkSigMatch@ does the next step in checking signature matching.
+The tau-type part has already been unified.  What we do here is to
+check that this unification has not over-constrained the (polymorphic)
+type variables of the original signature type.
+
+The error message here is somewhat unsatisfactory, but it'll do for
+now (ToDo).
+
+\begin{code}
+checkSigMatch []
+  = returnTc (error "checkSigMatch")
+
+checkSigMatch tc_ty_sigs
+  =    -- 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).
+       --
+       -- We unify them because, with polymorphic recursion, their types
+       -- might not otherwise be related.  This is a rather subtle issue.
+       -- ToDo: amplify
+    tcAddErrCtxt (sigContextsCtxt tc_ty_sigs) (
+       mapTc (unifyTauTyLists dict_tys1) dict_tys_s
+    )                                          `thenTc_`
+    
+       -- CHECK THAT THE SIGNATURE TYVARS AND TAU_TYPES ARE OK
+       -- Doesn't affect substitution
+    mapTc check_one_sig tc_ty_sigs     `thenTc_`
+
+    returnTc theta1
+  where
+    (theta1:thetas)          = [theta | TySigInfo _ _ _ theta _ _ <- tc_ty_sigs]
+    (dict_tys1 : dict_tys_s) = map mk_dict_tys (theta1 : thetas)
+    mk_dict_tys theta       = [mkDictTy c t | (c,t) <- theta]
+
+    check_one_sig (TySigInfo name id sig_tyvars _ sig_tau src_loc)
+      = tcAddSrcLoc src_loc    $
+       tcAddErrCtxt (sigCtxt id) $
+       checkSigTyVars sig_tyvars sig_tau
+\end{code}
+
+
+@checkSigTyVars@ is used after the type in a type signature has been unified with
+the actual type found.  It then checks that the type variables of the type signature
+are
+       (a) still all type variables
+               eg matching signature [a] against inferred type [(p,q)]
+               [then a will be unified to a non-type variable]
+
+       (b) still all distinct
+               eg matching signature [(a,b)] against inferred type [(p,p)]
+               [then a and b will be unified together]
+
+BUT ACTUALLY THESE FIRST TWO ARE FORCED BY USING DontBind TYVARS
 
-       returnTc (TySigInfo val tyvars' theta' tau' src_loc)
-   )           `thenTc` \ sig_info1 ->
+       (c) not mentioned in the environment
+               eg the signature for f in this:
 
-   tcTySigs other_sigs `thenTc` \ sig_infos ->
-   returnTc (sig_info1 : sig_infos)
+                       g x = ... where
+                                       f :: a->[a]
+                                       f y = [x,y]
 
-tcTySigs (other : sigs) = tcTySigs sigs
-tcTySigs []            = returnTc []
+               Here, f is forced to be monorphic by the free occurence of x.
+
+Before doing this, the substitution is applied to the signature type variable.
+
+\begin{code}
+checkSigTyVars :: [TcTyVar s]          -- The original signature type variables
+              -> TcType s              -- signature type (for err msg)
+              -> TcM s ()
+
+checkSigTyVars sig_tyvars sig_tau
+  = tcGetGlobalTyVars                  `thenNF_Tc` \ globals ->
+    let
+       mono_tyvars = filter (`elementOfTyVarSet` globals) sig_tyvars
+    in
+       -- TEMPORARY FIX
+       -- Until the final Bind-handling stuff is in, several type signatures in the same
+       -- bindings group can cause the signature type variable from the different
+       -- signatures to be unified.  So we still need to zonk and check point (b).
+       -- Remove when activating the new binding code
+    mapNF_Tc zonkTcTyVar sig_tyvars    `thenNF_Tc` \ sig_tys ->
+    checkTcM (hasNoDups (map (getTyVar "checkSigTyVars") sig_tys))
+            (zonkTcType sig_tau        `thenNF_Tc` \ sig_tau' ->
+             failTc (badMatchErr sig_tau sig_tau')
+            )                          `thenTc_`
+
+
+       -- Check point (c)
+       -- We want to report errors in terms of the original signature tyvars,
+       -- ie sig_tyvars, NOT sig_tyvars'.  sig_tys and sig_tyvars' correspond
+       -- 1-1 with sig_tyvars, so we can just map back.
+    checkTc (null mono_tyvars)
+           (notAsPolyAsSigErr sig_tau mono_tyvars)
 \end{code}
 
 
@@ -492,7 +637,15 @@ tcPragmaSigs :: [RenamedSig]                       -- The pragma signatures
                       TcHsBinds s,
                       LIE s)
 
-tcPragmaSigs sigs = returnTc ( \name -> NoPragmaInfo, EmptyBinds, emptyLIE )
+-- For now we just deal with INLINE pragmas
+tcPragmaSigs sigs = returnTc (prag_fn, EmptyBinds, emptyLIE )
+  where
+    prag_fn name | any has_inline sigs = IWantToBeINLINEd
+                | otherwise           = NoPragmaInfo
+                where
+                   has_inline (InlineSig n _) = (n == name)
+                   has_inline other           = False
+               
 
 {- 
 tcPragmaSigs sigs
@@ -653,76 +806,83 @@ tcPragmaSig (SpecSig name poly_ty maybe_spec_name src_loc)
 
 %************************************************************************
 %*                                                                     *
-\subsection[TcBinds-monomorphism]{The monomorphism restriction}
+\subsection[TcBinds-errors]{Error contexts and messages}
 %*                                                                     *
 %************************************************************************
 
-Not exported:
 
 \begin{code}
-{-      In GenSpec at the moment
+patMonoBindsCtxt bind sty
+  = hang (ptext SLIT("In a pattern binding:")) 4 (ppr sty bind)
 
-isUnRestrictedGroup :: [TcIdBndr s]            -- Signatures given for these
-                   -> TcBind s
-                   -> Bool
+-----------------------------------------------
+valSpecSigCtxt v ty sty
+  = hang (ptext SLIT("In a SPECIALIZE pragma for a value:"))
+        4 (sep [(<>) (ppr sty v) (ptext SLIT(" ::")),
+                 ppr sty ty])
 
-isUnRestrictedGroup sigs EmptyBind              = True
-isUnRestrictedGroup sigs (NonRecBind monobinds) = isUnResMono sigs monobinds
-isUnRestrictedGroup sigs (RecBind monobinds)    = isUnResMono sigs monobinds
 
-is_elem v vs = isIn "isUnResMono" v vs
 
-isUnResMono sigs (PatMonoBind (VarPat (TcId v)) _ _)   = v `is_elem` sigs
-isUnResMono sigs (PatMonoBind other      _ _)          = False
-isUnResMono sigs (VarMonoBind (TcId v) _)              = v `is_elem` sigs
-isUnResMono sigs (FunMonoBind _ _ _ _)                 = True
-isUnResMono sigs (AndMonoBinds mb1 mb2)                        = isUnResMono sigs mb1 &&
-                                                         isUnResMono sigs mb2
-isUnResMono sigs EmptyMonoBinds                                = True
--}
-\end{code}
+-----------------------------------------------
+notAsPolyAsSigErr sig_tau mono_tyvars sty
+  = hang (ptext SLIT("A type signature is more polymorphic than the inferred type"))
+       4  (vcat [text "Some type variables in the inferred type can't be forall'd, namely:",
+                     interpp'SP sty mono_tyvars,
+                     ptext SLIT("Possible cause: the RHS mentions something subject to the monomorphism restriction")
+                    ])
 
+-----------------------------------------------
+badMatchErr sig_ty inferred_ty sty
+  = hang (ptext SLIT("Type signature doesn't match inferred type"))
+        4 (vcat [hang (ptext SLIT("Signature:")) 4 (ppr sty sig_ty),
+                     hang (ptext SLIT("Inferred :")) 4 (ppr sty inferred_ty)
+          ])
 
-%************************************************************************
-%*                                                                     *
-\subsection[TcBinds-errors]{Error contexts and messages}
-%*                                                                     *
-%************************************************************************
+-----------------------------------------------
+sigCtxt id sty 
+  = sep [ptext SLIT("When checking signature for"), ppr sty id]
+sigsCtxt ids sty 
+  = sep [ptext SLIT("When checking signature(s) for:"), interpp'SP sty ids]
 
+-----------------------------------------------
+sigContextsCtxt ty_sigs sty
+  = hang (ptext SLIT("When matching the contexts of the signatures of a recursive group"))
+        4 (vcat (map ppr_tc_ty_sig ty_sigs))
+  where
+    ppr_tc_ty_sig (TySigInfo val _ tyvars theta tau_ty _)
+      = hang ((<>) (ppr sty val) (ptext SLIT(" :: ")))
+            4 (if null theta
+               then empty
+               else hcat [parens (hsep (punctuate comma (map (ppr_inst sty) theta))), 
+                          text " => ..."])
+    ppr_inst sty (clas, ty) = hsep [ppr sty clas, ppr sty ty]
 
-\begin{code}
-patMonoBindsCtxt bind sty
-  = ppHang (ppPStr SLIT("In a pattern binding:")) 4 (ppr sty bind)
+-----------------------------------------------
+specGroundnessCtxt
+  = panic "specGroundnessCtxt"
 
 --------------------------------------------
 specContextGroundnessCtxt -- err_ctxt dicts sty
   = panic "specContextGroundnessCtxt"
 {-
-  = ppHang (
-       ppSep [ppBesides [ppStr "In the SPECIALIZE pragma for `", ppr sty name, ppStr "'"],
-              ppBesides [ppStr " specialised to the type `", ppr sty spec_ty,  ppStr "'"],
-              pp_spec_id sty,
-              ppStr "... not all overloaded type variables were instantiated",
-              ppStr "to ground types:"])
-      4 (ppAboves [ppCat [ppr sty c, ppr sty t]
+  = hang (
+       sep [hsep [ptext SLIT("In the SPECIALIZE pragma for"), ppr sty name],
+            hcat [ptext SLIT(" specialised to the type"), ppr sty spec_ty],
+            pp_spec_id sty,
+            ptext SLIT("... not all overloaded type variables were instantiated"),
+            ptext SLIT("to ground types:")])
+      4 (vcat [hsep [ppr sty c, ppr sty t]
                  | (c,t) <- map getDictClassAndType dicts])
   where
     (name, spec_ty, locn, pp_spec_id)
       = case err_ctxt of
-         ValSpecSigCtxt    n ty loc      -> (n, ty, loc, \ x -> ppNil)
+         ValSpecSigCtxt    n ty loc      -> (n, ty, loc, \ x -> empty)
          ValSpecSpecIdCtxt n ty spec loc ->
            (n, ty, loc,
-            \ sty -> ppBesides [ppStr "... type of explicit id `", ppr sty spec, ppStr "'"])
+            \ sty -> hsep [ptext SLIT("... type of explicit id"), ppr sty spec])
 -}
+\end{code}
 
------------------------------------------------
-specGroundnessCtxt
-  = panic "specGroundnessCtxt"
 
 
-valSpecSigCtxt v ty sty
-  = ppHang (ppPStr SLIT("In a SPECIALIZE pragma for a value:"))
-        4 (ppSep [ppBeside (pprNonSym sty v) (ppPStr SLIT(" ::")),
-                 ppr sty ty])
-\end{code}