[project @ 2000-10-12 12:32:11 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMonoType.lhs
index fbf9a71..cc2f96a 100644 (file)
@@ -10,7 +10,7 @@ module TcMonoType ( tcHsType, tcHsSigType, tcHsBoxedSigType,
                        -- Kind checking
                    kcHsTyVar, kcHsTyVars, mkTyClTyVars,
                    kcHsType, kcHsSigType, kcHsBoxedSigType, kcHsContext,
-                   kcTyVarScope, newSigTyVars, mkImmutTyVars,
+                   tcTyVars, tcHsTyVars, mkImmutTyVars,
 
                    TcSigInfo(..), tcTySig, mkTcSig, maybeSig,
                    checkSigTyVars, sigCtxt, sigPatCtxt
@@ -24,10 +24,10 @@ import RnHsSyn              ( RenamedHsType, RenamedHsPred, RenamedContext, RenamedSig )
 import TcHsSyn         ( TcId )
 
 import TcMonad
-import TcEnv           ( tcExtendTyVarEnv, tcLookupTy, tcGetValueEnv, tcGetInScopeTyVars,
-                          tcExtendUVarEnv, tcLookupUVar,
-                         tcGetGlobalTyVars, valueEnvIds, 
-                         TyThing(..), tyThingKind, tcExtendKindEnv
+import TcEnv           ( tcExtendTyVarEnv, tcExtendKindEnv, tcLookupTy, 
+                         tcGetEnv, tcEnvTyVars, tcEnvTcIds,
+                         tcGetGlobalTyVars, 
+                         TyThing(..)
                        )
 import TcType          ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
                          newKindVar, tcInstSigVar,
@@ -36,34 +36,35 @@ import TcType               ( TcType, TcKind, TcTyVar, TcThetaType, TcTauType,
 import Inst            ( Inst, InstOrigin(..), newMethodWithGivenTy, instToIdBndr,
                          instFunDeps, instFunDepsOfTheta )
 import FunDeps         ( tyVarFunDep, oclose )
-import TcUnify         ( unifyKind, unifyKinds, unifyOpenTypeKind )
+import TcUnify         ( unifyKind, unifyOpenTypeKind )
 import Type            ( Type, Kind, PredType(..), ThetaType, UsageAnn(..),
                          mkTyVarTy, mkTyVarTys, mkFunTy, mkSynTy, mkUsgTy,
                           mkUsForAllTy, zipFunTys, hoistForAllTys,
-                         mkSigmaTy, mkDictTy, mkPredTy, mkTyConApp,
+                         mkSigmaTy, mkPredTy, mkTyConApp,
                          mkAppTys, splitForAllTys, splitRhoTy, mkRhoTy,
                          boxedTypeKind, unboxedTypeKind, mkArrowKind,
                          mkArrowKinds, getTyVar_maybe, getTyVar, splitFunTy_maybe,
                          tidyOpenType, tidyOpenTypes, tidyTyVar, tidyTyVars,
-                         tyVarsOfType, tyVarsOfTypes, tyVarsOfPred, mkForAllTys,
-                         classesOfPreds
+                         tyVarsOfType, tyVarsOfPred, mkForAllTys,
+                         classesOfPreds, isUnboxedTupleType
                        )
-import PprType         ( pprConstraint, pprType, pprPred )
+import PprType         ( pprType, pprPred )
 import Subst           ( mkTopTyVarSubst, substTy )
 import Id              ( mkVanillaId, idName, idType, idFreeTyVars )
-import Var             ( TyVar, mkTyVar, tyVarKind, mkNamedUVar, varName )
+import Var             ( TyVar, mkTyVar, tyVarKind )
 import VarEnv
 import VarSet
 import ErrUtils                ( Message )
-import TyCon           ( TyCon, isSynTyCon, tyConArity, tyConKind )
+import TyCon           ( TyCon, isSynTyCon, tyConArity, tyConKind, tyConName )
 import Class           ( ClassContext, classArity, classTyCon )
-import Name            ( Name, OccName, isLocallyDefined )
-import TysWiredIn      ( mkListTy, mkTupleTy )
-import UniqFM          ( elemUFM, foldUFM )
+import Name            ( Name, isLocallyDefined )
+import TysWiredIn      ( mkListTy, mkTupleTy, genUnitTyCon )
+import UniqFM          ( elemUFM )
 import BasicTypes      ( Boxity(..) )
 import SrcLoc          ( SrcLoc )
-import Util            ( mapAccumL, isSingleton, removeDups )
+import Util            ( mapAccumL, isSingleton )
 import Outputable
+
 \end{code}
 
 
@@ -90,7 +91,7 @@ To do step 1, we proceed thus:
 1b. Apply the kind checker
 1c. Zonk the resulting kinds
 
-The kind checker is passed to kcTyVarScope as an argument.  
+The kind checker is passed to tcHsTyVars as an argument.  
 
 For example, when we find
        (forall a m. m a -> m a)
@@ -98,7 +99,7 @@ we bind a,m to kind varibles and kind-check (m a -> m a).  This
 makes a get kind *, and m get kind *->*.  Now we typecheck (m a -> m a)
 in an environment that binds a and m suitably.
 
-The kind checker passed to kcTyVarScope needs to look at enough to
+The kind checker passed to tcHsTyVars needs to look at enough to
 establish the kind of the tyvar:
   * For a group of type and class decls, it's just the group, not
        the rest of the program
@@ -116,37 +117,50 @@ But equally valid would be
                                a::(*->*)-> *, b::*->*
 
 \begin{code}
-kcTyVarScope :: [HsTyVarBndr Name] 
-            -> TcM s a                         -- The kind checker
-            -> TcM s [(Name,Kind)]
-       -- Do a kind check to find out the kinds of the type variables
-       -- Then return a bunch of name-kind pairs, from which to 
-       -- construct the type variables.  We don't return the tyvars
-       -- themselves because sometimes we want mutable ones and 
-       -- sometimes we want immutable ones.
-
-kcTyVarScope [] kind_check = returnTc []
+tcHsTyVars :: [HsTyVarBndr Name] 
+          -> TcM a                             -- The kind checker
+          -> ([TyVar] -> TcM b)
+          -> TcM b
+
+tcHsTyVars [] kind_check thing_inside = thing_inside []
        -- A useful short cut for a common case!
   
-kcTyVarScope tv_names kind_check 
+tcHsTyVars tv_names kind_check thing_inside
   = kcHsTyVars tv_names                                `thenNF_Tc` \ tv_names_w_kinds ->
     tcExtendKindEnv tv_names_w_kinds kind_check                `thenTc_`
-    zonkKindEnv tv_names_w_kinds
+    zonkKindEnv tv_names_w_kinds                       `thenNF_Tc` \ tvs_w_kinds ->
+    let
+       tyvars = mkImmutTyVars tvs_w_kinds
+    in
+    tcExtendTyVarEnv tyvars (thing_inside tyvars)
+
+tcTyVars :: [Name] 
+            -> TcM a                           -- The kind checker
+            -> TcM [TyVar]
+tcTyVars [] kind_check = returnTc []
+
+tcTyVars tv_names kind_check
+  = mapNF_Tc newNamedKindVar tv_names          `thenTc` \ kind_env ->
+    tcExtendKindEnv kind_env kind_check                `thenTc_`
+    zonkKindEnv kind_env                       `thenNF_Tc` \ tvs_w_kinds ->
+    listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- tvs_w_kinds]
 \end{code}
     
 
 \begin{code}
-kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM s (name, TcKind)
-kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM s [(name, TcKind)]
+kcHsTyVar  :: HsTyVarBndr name   -> NF_TcM (name, TcKind)
+kcHsTyVars :: [HsTyVarBndr name] -> NF_TcM [(name, TcKind)]
 
-kcHsTyVar (UserTyVar name)       = newKindVar  `thenNF_Tc` \ kind ->
-                                  returnNF_Tc (name, kind)
+kcHsTyVar (UserTyVar name)       = newNamedKindVar name
 kcHsTyVar (IfaceTyVar name kind) = returnNF_Tc (name, kind)
 
 kcHsTyVars tvs = mapNF_Tc kcHsTyVar tvs
 
+newNamedKindVar name = newKindVar      `thenNF_Tc` \ kind ->
+                      returnNF_Tc (name, kind)
+
 ---------------------------
-kcBoxedType :: RenamedHsType -> TcM s ()
+kcBoxedType :: RenamedHsType -> TcM ()
        -- The type ty must be a *boxed* *type*
 kcBoxedType ty
   = kcHsType ty                                `thenTc` \ kind ->
@@ -154,7 +168,7 @@ kcBoxedType ty
     unifyKind boxedTypeKind kind
     
 ---------------------------
-kcTypeType :: RenamedHsType -> TcM s ()
+kcTypeType :: RenamedHsType -> TcM ()
        -- The type ty must be a *type*, but it can be boxed or unboxed.
 kcTypeType ty
   = kcHsType ty                                `thenTc` \ kind ->
@@ -162,21 +176,14 @@ kcTypeType ty
     unifyOpenTypeKind kind
 
 ---------------------------
-kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM s ()
+kcHsSigType, kcHsBoxedSigType :: RenamedHsType -> TcM ()
        -- Used for type signatures
 kcHsSigType     = kcTypeType
 kcHsBoxedSigType = kcBoxedType
 
 ---------------------------
-kcHsType :: RenamedHsType -> TcM s TcKind
-kcHsType (HsTyVar name)              
-  = tcLookupTy name    `thenTc` \ thing ->
-    case thing of
-       ATyVar tv -> returnTc (tyVarKind tv)
-       ATyCon tc -> returnTc (tyConKind tc)
-       AThing k  -> returnTc k
-       other     -> failWithTc (wrongThingErr "type" thing name)
-
+kcHsType :: RenamedHsType -> TcM TcKind
+kcHsType (HsTyVar name)              = kcTyVar name
 kcHsType (HsUsgTy _ ty)       = kcHsType ty
 kcHsType (HsUsgForAllTy _ ty) = kcHsType ty
 
@@ -188,53 +195,88 @@ kcHsType (HsTupleTy (HsTupCon _ Boxed) tys)
   = mapTc kcBoxedType tys      `thenTc_` 
     returnTc boxedTypeKind
 
-kcHsType (HsTupleTy (HsTupCon _ Unboxed) tys)
-  = mapTc kcTypeType tys       `thenTc_` 
-    returnTc unboxedTypeKind
+kcHsType ty@(HsTupleTy (HsTupCon _ Unboxed) tys)
+  = failWithTc (unboxedTupleErr ty)
+       -- Unboxed tuples are illegal everywhere except
+       -- just after a function arrow (see kcFunResType)
 
 kcHsType (HsFunTy ty1 ty2)
   = kcTypeType ty1     `thenTc_`
-    kcTypeType ty2     `thenTc_`
+    kcFunResType ty2   `thenTc_`
     returnTc boxedTypeKind
 
+kcHsType ty@(HsOpTy ty1 op ty2)
+  = kcTyVar op                         `thenTc` \ op_kind ->
+    kcHsType ty1                       `thenTc` \ ty1_kind ->
+    kcHsType ty2                       `thenTc` \ ty2_kind ->
+    tcAddErrCtxt (appKindCtxt (ppr ty))        $
+    kcAppKind op_kind  ty1_kind                `thenTc` \ op_kind' ->
+    kcAppKind op_kind' ty2_kind
+   
 kcHsType (HsPredTy pred)
   = kcHsPred pred              `thenTc_`
     returnTc boxedTypeKind
 
 kcHsType ty@(HsAppTy ty1 ty2)
-  = kcHsType ty1               `thenTc` \ tc_kind ->
-    kcHsType ty2               `thenTc` \ arg_kind ->
-
+  = kcHsType ty1                       `thenTc` \ tc_kind ->
+    kcHsType ty2                       `thenTc` \ arg_kind ->
     tcAddErrCtxt (appKindCtxt (ppr ty))        $
-    case splitFunTy_maybe tc_kind of 
+    kcAppKind tc_kind arg_kind
+
+kcHsType (HsForAllTy (Just tv_names) context ty)
+  = kcHsTyVars tv_names                `thenNF_Tc` \ kind_env ->
+    tcExtendKindEnv kind_env   $
+    kcHsContext context                `thenTc_`
+       -- Context behaves like a function type
+       -- This matters.  Return-unboxed-tuple analysis can
+       -- give overloaded functions like
+       --      f :: forall a. Num a => (# a->a, a->a #)
+       -- And we want these to get through the type checker
+    if null context then
+       kcHsType ty
+    else
+       kcFunResType ty         `thenTc_`
+       returnTc boxedTypeKind
+
+---------------------------
+kcTyVar name   -- Could be a tyvar or a tycon
+  = tcLookup name      `thenTc` \ thing ->
+    case thing of {
+       ATyVar tv -> returnTc (tyVarKind tv) ;
+       AThing k  -> returnTc k ;
+       AGlobal (ATyCon tc) -> returnTc (tyConKind tc) ;
+       other     -> 
+
+    failWithTc (wrongThingErr "type" thing name)
+    }}
+
+---------------------------
+kcFunResType :: RenamedHsType -> TcM TcKind
+-- The only place an unboxed tuple type is allowed
+-- is at the right hand end of an arrow
+kcFunResType (HsTupleTy (HsTupCon _ Unboxed) tys)
+  = mapTc kcTypeType tys       `thenTc_` 
+    returnTc unboxedTypeKind
+
+kcFunResType ty = kcHsType ty
+
+---------------------------
+kcAppKind fun_kind arg_kind
+  = case splitFunTy_maybe fun_kind of 
        Just (arg_kind', res_kind)
                -> unifyKind arg_kind arg_kind' `thenTc_`
                   returnTc res_kind
 
        Nothing -> newKindVar                                           `thenNF_Tc` \ res_kind ->
-                  unifyKind tc_kind (mkArrowKind arg_kind res_kind)    `thenTc_`
+                  unifyKind fun_kind (mkArrowKind arg_kind res_kind)   `thenTc_`
                   returnTc res_kind
 
-kcHsType (HsForAllTy (Just tv_names) context ty)
-  = kcHsTyVars tv_names                        `thenNF_Tc` \ kind_env ->
-    tcExtendKindEnv kind_env           $
-    kcHsContext context                `thenTc_`
-    kcHsType ty                        `thenTc` \ kind ->
-               -- Context behaves like a function type
-               -- This matters.  Return-unboxed-tuple analysis can
-               -- give overloaded functions like
-               --      f :: forall a. Num a => (# a->a, a->a #)
-               -- And we want these to get through the type checker
-    returnTc (if null context then
-                kind
-             else
-                 boxedTypeKind)
 
 ---------------------------
 kcHsContext ctxt = mapTc_ kcHsPred ctxt
 
-kcHsPred :: RenamedHsPred -> TcM s ()
+kcHsPred :: RenamedHsPred -> TcM ()
 kcHsPred pred@(HsPIParam name ty)
   = tcAddErrCtxt (appKindCtxt (ppr pred))      $
     kcBoxedType ty
@@ -245,8 +287,8 @@ kcHsPred pred@(HsPClass cls tys)
     (case thing of
        AClass cls  -> returnTc (tyConKind (classTyCon cls))
        AThing kind -> returnTc kind
-       other -> failWithTc (wrongThingErr "class" thing cls))  `thenTc` \ kind ->
-    mapTc kcHsType tys                                         `thenTc` \ arg_kinds ->
+       other -> failWithTc (wrongThingErr "class" (pp_thing thing) cls))       `thenTc` \ kind ->
+    mapTc kcHsType tys                                                 `thenTc` \ arg_kinds ->
     unifyKind kind (mkArrowKinds arg_kinds boxedTypeKind)
 \end{code}
 
@@ -265,17 +307,18 @@ tcHsSigType and tcHsBoxedSigType are used for type signatures written by the pro
 
   * Notice that we kind-check first, because the type-check assumes
        that the kinds are already checked.
+
   * They are only called when there are no kind vars in the environment
        so the kind returned is indeed a Kind not a TcKind
 
 \begin{code}
-tcHsSigType :: RenamedHsType -> TcM s TcType
+tcHsSigType :: RenamedHsType -> TcM TcType
 tcHsSigType ty
   = kcTypeType ty      `thenTc_`
     tcHsType ty                `thenTc` \ ty' ->
     returnTc (hoistForAllTys ty')
 
-tcHsBoxedSigType :: RenamedHsType -> TcM s Type
+tcHsBoxedSigType :: RenamedHsType -> TcM Type
 tcHsBoxedSigType ty
   = kcBoxedType ty     `thenTc_`
     tcHsType ty                `thenTc` \ ty' ->
@@ -287,7 +330,7 @@ tcHsType, the main work horse
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
-tcHsType :: RenamedHsType -> TcM s Type
+tcHsType :: RenamedHsType -> TcM Type
 tcHsType ty@(HsTyVar name)
   = tc_app ty []
 
@@ -304,6 +347,15 @@ tcHsType (HsFunTy ty1 ty2)
     tcHsType ty2       `thenTc` \ tau_ty2 ->
     returnTc (mkFunTy tau_ty1 tau_ty2)
 
+tcHsType (HsNumTy n)
+  = ASSERT(n== 1)
+    returnTc (mkTyConApp genUnitTyCon [])
+
+tcHsType (HsOpTy ty1 op ty2) =
+  tcHsType ty1 `thenTc` \ tau_ty1 ->
+  tcHsType ty2 `thenTc` \ tau_ty2 ->
+  tc_fun_type op [tau_ty1,tau_ty2]
+
 tcHsType (HsAppTy ty1 ty2)
   = tc_app ty1 [ty2]
 
@@ -311,101 +363,89 @@ tcHsType (HsPredTy pred)
   = tcClassAssertion True pred `thenTc` \ pred' ->
     returnTc (mkPredTy pred')
 
-tcHsType (HsUsgTy usg ty)
-  = newUsg usg                 `thenTc` \ usg' ->
-    tcHsType ty                        `thenTc` \ tc_ty ->
-    returnTc (mkUsgTy usg' tc_ty)
-  where
-    newUsg usg = case usg of
-                   HsUsOnce        -> returnTc UsOnce
-                   HsUsMany        -> returnTc UsMany
-                   HsUsVar uv_name -> tcLookupUVar uv_name `thenTc` \ uv ->
-                                      returnTc (UsVar uv)
-
-tcHsType (HsUsgForAllTy uv_name ty)
-  = let
-        uv = mkNamedUVar uv_name
-    in
-    tcExtendUVarEnv uv_name uv $
-    tcHsType ty                     `thenTc` \ tc_ty ->
-    returnTc (mkUsForAllTy uv tc_ty)
-
 tcHsType full_ty@(HsForAllTy (Just tv_names) ctxt ty)
-  = kcTyVarScope tv_names 
-                (kcHsContext ctxt `thenTc_` kcHsType ty)  `thenTc` \ tv_kinds ->
-    let
-       forall_tyvars = mkImmutTyVars tv_kinds
-    in
-    tcExtendTyVarEnv forall_tyvars     $
-    tcContext ctxt                     `thenTc` \ theta ->
-    tcHsType ty                                `thenTc` \ tau ->
-    let
-       -- Check for ambiguity
-       --   forall V. P => tau
-       -- is ambiguous if P contains generic variables
-       -- (i.e. one of the Vs) that are not mentioned in tau
-       --
-       -- However, we need to take account of functional dependencies
-       -- when we speak of 'mentioned in tau'.  Example:
-       --      class C a b | a -> b where ...
-       -- Then the type
-       --      forall x y. (C x y) => x
-       -- is not ambiguous because x is mentioned and x determines y
-       --
-       -- NOTE: In addition, GHC insists that at least one type variable
-       -- in each constraint is in V.  So we disallow a type like
-       --      forall a. Eq b => b -> b
-       -- even in a scope where b is in scope.
-       -- This is the is_free test below.
-
-       tau_vars            = tyVarsOfType tau
-       fds                 = instFunDepsOfTheta theta
-       tvFundep            = tyVarFunDep fds
-       extended_tau_vars   = oclose tvFundep tau_vars
-       is_ambig ct_var     = (ct_var `elem` forall_tyvars) &&
-                             not (ct_var `elemUFM` extended_tau_vars)
-       is_free ct_var      = not (ct_var `elem` forall_tyvars)
-
-       check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
-                         checkTc (not all_free)  (freeErr  pred full_ty)
-             where 
-               ct_vars   = varSetElems (tyVarsOfPred pred)
-               any_ambig = is_source_polytype && any is_ambig ct_vars
-               all_free  = all is_free  ct_vars
-
-       -- Check ambiguity only for source-program types, not
-       -- for types coming from inteface files.  The latter can
-       -- legitimately have ambiguous types. Example
-       --    class S a where s :: a -> (Int,Int)
-       --    instance S Char where s _ = (1,1)
-       --    f:: S a => [a] -> Int -> (Int,Int)
-       --    f (_::[a]) x = (a*x,b)
-       --      where (a,b) = s (undefined::a)
-       -- Here the worker for f gets the type
-       --      fw :: forall a. S a => Int -> (# Int, Int #)
-       --
-       -- If the list of tv_names is empty, we have a monotype,
-       -- and then we don't need to check for ambiguity either,
-       -- because the test can't fail (see is_ambig).
-       is_source_polytype = case tv_names of
-                               (UserTyVar _ : _) -> True
-                               other             -> False
+  = let
+       kind_check = kcHsContext ctxt `thenTc_` kcFunResType ty
     in
-    mapTc check_pred theta             `thenTc_`
-    returnTc (mkSigmaTy forall_tyvars theta tau)
+    tcHsTyVars tv_names kind_check             $ \ tyvars ->
+    tcContext ctxt                             `thenTc` \ theta ->
+    tcHsType ty                                        `thenTc` \ tau ->
+    checkAmbiguity full_ty tyvars theta tau    `thenTc_`
+    returnTc (mkSigmaTy tyvars theta tau)
+
+  -- Check for ambiguity
+  --   forall V. P => tau
+  -- is ambiguous if P contains generic variables
+  -- (i.e. one of the Vs) that are not mentioned in tau
+  --
+  -- However, we need to take account of functional dependencies
+  -- when we speak of 'mentioned in tau'.  Example:
+  --   class C a b | a -> b where ...
+  -- Then the type
+  --   forall x y. (C x y) => x
+  -- is not ambiguous because x is mentioned and x determines y
+  --
+  -- NOTE: In addition, GHC insists that at least one type variable
+  -- in each constraint is in V.  So we disallow a type like
+  --   forall a. Eq b => b -> b
+  -- even in a scope where b is in scope.
+  -- This is the is_free test below.
+
+checkAmbiguity full_ty forall_tyvars theta tau
+  = mapTc check_pred theta
+  where
+    tau_vars         = tyVarsOfType tau
+    fds                      = instFunDepsOfTheta theta
+    tvFundep         = tyVarFunDep fds
+    extended_tau_vars = oclose tvFundep tau_vars
+
+    is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
+                       not (ct_var `elemUFM` extended_tau_vars)
+    is_free ct_var    = not (ct_var `elem` forall_tyvars)
+    
+    check_pred pred = checkTc (not any_ambig) (ambigErr pred full_ty) `thenTc_`
+                     checkTc (not all_free)  (freeErr  pred full_ty)
+             where 
+               ct_vars   = varSetElems (tyVarsOfPred pred)
+               all_free  = all is_free ct_vars
+               any_ambig = is_source_polytype && any is_ambig ct_vars
+    
+    -- Notes on the 'is_source_polytype' test above
+    -- Check ambiguity only for source-program types, not
+    -- for types coming from inteface files.  The latter can
+    -- legitimately have ambiguous types. Example
+    --    class S a where s :: a -> (Int,Int)
+    --    instance S Char where s _ = (1,1)
+    --    f:: S a => [a] -> Int -> (Int,Int)
+    --    f (_::[a]) x = (a*x,b)
+    -- where (a,b) = s (undefined::a)
+    -- Here the worker for f gets the type
+    -- fw :: forall a. S a => Int -> (# Int, Int #)
+    --
+    -- If the list of tv_names is empty, we have a monotype,
+    -- and then we don't need to check for ambiguity either,
+    -- because the test can't fail (see is_ambig).
+    is_source_polytype 
+       = case full_ty of
+           HsForAllTy (Just (UserTyVar _ : _)) _ _ -> True
+           other                                   -> False
 \end{code}
 
 Help functions for type applications
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 \begin{code}
+tc_app :: RenamedHsType -> [RenamedHsType] -> TcM Type
 tc_app (HsAppTy ty1 ty2) tys
   = tc_app ty1 (ty2:tys)
 
 tc_app ty tys
   = tcAddErrCtxt (appKindCtxt pp_app)  $
     mapTc tcHsType tys                 `thenTc` \ arg_tys ->
-    tc_fun_type ty arg_tys
+    case ty of
+       HsTyVar fun -> tc_fun_type fun arg_tys
+       other       -> tcHsType ty              `thenTc` \ fun_ty ->
+                      returnNF_Tc (mkAppTys fun_ty arg_tys)
   where
     pp_app = ppr ty <+> sep (map pprParendHsType tys)
 
@@ -413,8 +453,8 @@ tc_app ty tys
 -- But not quite; for synonyms it checks the correct arity, and builds a SynTy
 --     hence the rather strange functionality.
 
-tc_fun_type (HsTyVar name) arg_tys
-  = tcLookupTy name                    `thenTc` \ thing ->
+tc_fun_type name arg_tys
+  = tcLookupGlobal name                        `thenTc` \ thing ->
     case thing of
        ATyVar tv -> returnTc (mkAppTys (mkTyVarTy tv) arg_tys)
 
@@ -434,24 +474,20 @@ tc_fun_type (HsTyVar name) arg_tys
                    err_msg = arityErr "Type synonym" name arity n_args
                    n_args  = length arg_tys
 
-       other -> failWithTc (wrongThingErr "type constructor" thing name)
-
-tc_fun_type ty arg_tys
-  = tcHsType ty                `thenTc` \ fun_ty ->
-    returnNF_Tc (mkAppTys fun_ty arg_tys)
+       other -> failWithTc (wrongThingErr "type constructor" (pp_thing thing) name)
 \end{code}
 
 
 Contexts
 ~~~~~~~~
 \begin{code}
-tcClassContext :: RenamedContext -> TcM s ClassContext
+tcClassContext :: RenamedContext -> TcM ClassContext
        -- Used when we are expecting a ClassContext (i.e. no implicit params)
 tcClassContext context
   = tcContext context  `thenTc` \ theta ->
     returnTc (classesOfPreds theta)
 
-tcContext :: RenamedContext -> TcM s ThetaType
+tcContext :: RenamedContext -> TcM ThetaType
 tcContext context = mapTc (tcClassAssertion False) context
 
 tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
@@ -466,7 +502,7 @@ tcClassAssertion ccall_ok assn@(HsPClass class_name tys)
                n_tys = length tys
                err   = arityErr "Class" class_name arity n_tys
 
-       other -> failWithTc (wrongThingErr "class" thing class_name)
+       other -> failWithTc (wrongThingErr "class" (ppr_thing thing) class_name)
 
 tcClassAssertion ccall_ok assn@(HsPIParam name ty)
   = tcAddErrCtxt (appKindCtxt (ppr assn))      $
@@ -483,10 +519,7 @@ tcClassAssertion ccall_ok assn@(HsPIParam name ty)
 
 \begin{code}
 mkImmutTyVars :: [(Name,Kind)] -> [TyVar]
-newSigTyVars  :: [(Name,Kind)] -> NF_TcM s [TcTyVar]
-
 mkImmutTyVars pairs = [mkTyVar name kind | (name, kind) <- pairs]
-newSigTyVars  pairs = listNF_Tc [tcNewSigTyVar name kind | (name,kind) <- pairs]
 
 mkTyClTyVars :: Kind                   -- Kind of the tycon or class
             -> [HsTyVarBndr Name]
@@ -548,7 +581,7 @@ maybeSig (sig@(TySigInfo sig_name _ _ _ _ _ _ _) : sigs) name
 
 
 \begin{code}
-tcTySig :: RenamedSig -> TcM s TcSigInfo
+tcTySig :: RenamedSig -> TcM TcSigInfo
 
 tcTySig (Sig v ty src_loc)
  = tcAddSrcLoc src_loc                         $ 
@@ -557,7 +590,7 @@ tcTySig (Sig v ty src_loc)
    mkTcSig (mkVanillaId v sigma_tc_ty) src_loc `thenNF_Tc` \ sig -> 
    returnTc sig
 
-mkTcSig :: TcId -> SrcLoc -> NF_TcM s TcSigInfo
+mkTcSig :: TcId -> SrcLoc -> NF_TcM TcSigInfo
 mkTcSig poly_id src_loc
   =    -- Instantiate this type
        -- It's important to do this even though in the error-free case
@@ -661,7 +694,7 @@ checkSigTyVars :: [TcTyVar]         -- Universally-quantified type variables in the sig
               -> TcTyVarSet            -- Tyvars that are free in the type signature
                                        -- These should *already* be in the global-var set, and are
                                        -- used here only to improve the error message
-              -> TcM s [TcTyVar]       -- Zonked signature type variables
+              -> TcM [TcTyVar] -- Zonked signature type variables
 
 checkSigTyVars [] free = returnTc []
 
@@ -687,7 +720,10 @@ checkSigTyVars sig_tyvars free_tyvars
        -- from the zonked tyvar to the in-scope one
        -- If any of the in-scope tyvars zonk to a type, then ignore them;
        -- that'll be caught later when we back up to their type sig
-       tcGetInScopeTyVars                      `thenNF_Tc` \ in_scope_tvs ->
+       tcGetEnv                                `thenNF_Tc` \ env ->
+       let
+          in_scope_tvs = tcEnvTyVars env
+       in
        zonkTcTyVars in_scope_tvs               `thenNF_Tc` \ in_scope_tys ->
        let
            in_scope_assoc = [ (zonked_tv, in_scope_tv) 
@@ -728,8 +764,8 @@ checkSigTyVars sig_tyvars free_tyvars
 
            if tv `elemVarSet` globals  -- Error (c)! Type variable escapes
                                        -- The least comprehensible, so put it last
-           then   tcGetValueEnv                                        `thenNF_Tc` \ ve ->
-                  find_globals tv env  [] (valueEnvIds ve)             `thenNF_Tc` \ (env1, globs) ->
+           then   tcGetEnv                                             `thenNF_Tc` \ env ->
+                  find_globals tv env  [] (tcEnvTcIds)                 `thenNF_Tc` \ (env1, globs) ->
                   find_frees   tv env1 [] (varSetElems free_tyvars)    `thenNF_Tc` \ (env2, frees) ->
                   returnNF_Tc (env2, acc, escape_msg sig_tyvar tv globs frees : msgs)
 
@@ -806,7 +842,7 @@ These two context are used with checkSigTyVars
     
 \begin{code}
 sigCtxt :: Message -> [TcTyVar] -> TcThetaType -> TcTauType
-       -> TidyEnv -> NF_TcM s (TidyEnv, Message)
+       -> TidyEnv -> NF_TcM (TidyEnv, Message)
 sigCtxt when sig_tyvars sig_theta sig_tau tidy_env
   = zonkTcType sig_tau         `thenNF_Tc` \ actual_tau ->
     let
@@ -843,8 +879,6 @@ sigPatCtxt bound_tvs bound_ids tidy_env
 \begin{code}
 tcsigCtxt v   = ptext SLIT("In a type signature for") <+> quotes (ppr v)
 
-typeCtxt ty = ptext SLIT("In the type") <+> quotes (ppr ty)
-
 typeKindCtxt :: RenamedHsType -> Message
 typeKindCtxt ty = sep [ptext SLIT("When checking that"),
                       nest 2 (quotes (ppr ty)),
@@ -853,13 +887,16 @@ typeKindCtxt ty = sep [ptext SLIT("When checking that"),
 appKindCtxt :: SDoc -> Message
 appKindCtxt pp = ptext SLIT("When checking kinds in") <+> quotes pp
 
-wrongThingErr expected actual name
-  = pp_actual actual <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
-  where
-    pp_actual (ATyCon _) = ptext SLIT("Type constructor")
-    pp_actual (AClass _) = ptext SLIT("Class")
-    pp_actual (ATyVar _) = ptext SLIT("Type variable")
-    pp_actual (AThing _) = ptext SLIT("Utterly bogus")
+wrongThingErr expected thing name
+  = thing <+> quotes (ppr name) <+> ptext SLIT("used as a") <+> text expected
+
+pp_ty_thing (ATyCon _) = ptext SLIT("Type constructor")
+pp_ty_thing (AClass _) = ptext SLIT("Class")
+pp_ty_thing (AnId   _) = ptext SLIT("Identifier")
+
+pp_tc_ty_thing (ATyVar _) = ptext SLIT("Type variable")
+pp_tc_ty_thing (ATcId _)  = ptext SLIT("Local identifier")
+pp_tc_ty_thing (AThing _) = ptext SLIT("Utterly bogus")
 
 ambigErr pred ty
   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
@@ -871,4 +908,7 @@ freeErr pred ty
                   ptext SLIT("does not mention any of the universally quantified type variables"),
         nest 4 (ptext SLIT("in the type") <+> quotes (ppr ty))
     ]
+
+unboxedTupleErr ty
+  = sep [ptext (SLIT("Illegal unboxed tuple as a function or contructor argument:")), nest 4 (ppr ty)]
 \end{code}