[project @ 2002-03-25 15:08:38 by simonpj]
[ghc-hetmet.git] / ghc / compiler / typecheck / TcMType.lhs
index 07166d8..451e3fc 100644 (file)
@@ -11,27 +11,27 @@ module TcMType (
 
   --------------------------------
   -- Creating new mutable type variables
-  newTyVar, newHoleTyVarTy,
+  newTyVar, 
   newTyVarTy,          -- Kind -> NF_TcM TcType
   newTyVarTys,         -- Int -> Kind -> NF_TcM [TcType]
   newKindVar, newKindVars, newBoxityVar,
   putTcTyVar, getTcTyVar,
 
+  newHoleTyVarTy, readHoleResult, zapToType,
+
   --------------------------------
   -- Instantiation
-  tcInstTyVar, tcInstTyVars,
-  tcInstSigTyVars, tcInstType, tcInstSigType,
-  tcSplitRhoTyM,
+  tcInstTyVar, tcInstTyVars, tcInstType, 
 
   --------------------------------
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, pprUserTypeCtxt,
   SourceTyCtxt(..), checkValidTheta, 
-  checkValidInstHead, instTypeErr,
+  checkValidInstHead, instTypeErr, checkAmbiguity,
 
   --------------------------------
   -- Zonking
-  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkTcSigTyVars,
+  zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, 
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
   zonkTcPredType, zonkTcTypeToType, zonkTcTyVarToTyVar, zonkKindEnv,
 
@@ -47,10 +47,10 @@ import TypeRep              ( Type(..), SourceType(..), TyNote(..),  -- Friend; can see repr
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          TcTyVarSet, TcKind, TcTyVar, TyVarDetails(..),
                          tcEqType, tcCmpPred,
-                         tcSplitRhoTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
+                         tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
                          tcSplitTyConApp_maybe, tcSplitForAllTys,
-                         tcGetTyVar, tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
+                         tcIsTyVarTy, tcSplitSigmaTy, 
+                         isUnLiftedType, isIPPred, isHoleTyVar,
 
                          mkAppTy, mkTyVarTy, mkTyVarTys, 
                          tyVarsOfPred, getClassPredTys_maybe,
@@ -58,28 +58,30 @@ import TcType               ( TcType, TcThetaType, TcTauType, TcPredType,
                          liftedTypeKind, openTypeKind, defaultKind, superKind,
                          superBoxity, liftedBoxity, typeKind,
                          tyVarsOfType, tyVarsOfTypes, 
-                         eqKind, isTypeKind,
+                         eqKind, isTypeKind, isAnyTypeKind,
 
                          isFFIArgumentTy, isFFIImportResultTy
                        )
+import qualified Type  ( splitFunTys )
 import Subst           ( Subst, mkTopTyVarSubst, substTy )
 import Class           ( Class, classArity, className )
 import TyCon           ( TyCon, mkPrimTyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName )
+                         tyConArity, tyConName, tyConKind )
 import PrimRep         ( PrimRep(VoidRep) )
 import Var             ( TyVar, tyVarKind, tyVarName, isTyVar, mkTyVar, isMutTyVar )
 
 -- others:
 import TcMonad          -- TcType, amongst others
-import TysWiredIn      ( voidTy )
+import TysWiredIn      ( voidTy, listTyCon, tupleTyCon )
 import PrelNames       ( cCallableClassKey, cReturnableClassKey, hasKey )
 import ForeignCall     ( Safety(..) )
 import FunDeps         ( grow )
 import PprType         ( pprPred, pprSourceType, pprTheta, pprClassPred )
-import Name            ( Name, NamedThing(..), setNameUnique, mkSysLocalName,
-                         mkLocalName, mkDerivedTyConOcc
+import Name            ( Name, NamedThing(..), setNameUnique, mkSystemName,
+                         mkInternalName, mkDerivedTyConOcc
                        )
 import VarSet
+import BasicTypes      ( Boxity(Boxed) )
 import CmdLineOpts     ( dopt, DynFlag(..) )
 import Unique          ( Uniquable(..) )
 import SrcLoc          ( noSrcLoc )
@@ -99,25 +101,20 @@ import Outputable
 newTyVar :: Kind -> NF_TcM TcTyVar
 newTyVar kind
   = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("t")) kind VanillaTv
+    tcNewMutTyVar (mkSystemName uniq FSLIT("t")) kind VanillaTv
 
 newTyVarTy  :: Kind -> NF_TcM TcType
 newTyVarTy kind
   = newTyVar kind      `thenNF_Tc` \ tc_tyvar ->
     returnNF_Tc (TyVarTy tc_tyvar)
 
-newHoleTyVarTy :: NF_TcM TcType
-  = tcGetUnique        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("h")) openTypeKind HoleTv  `thenNF_Tc` \ tv ->
-    returnNF_Tc (TyVarTy tv)
-
 newTyVarTys :: Int -> Kind -> NF_TcM [TcType]
 newTyVarTys n kind = mapNF_Tc newTyVarTy (nOfThem n kind)
 
 newKindVar :: NF_TcM TcKind
 newKindVar
   = tcGetUnique                                                        `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("k")) superKind VanillaTv  `thenNF_Tc` \ kv ->
+    tcNewMutTyVar (mkSystemName uniq FSLIT("k")) superKind VanillaTv   `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 
 newKindVars :: Int -> NF_TcM [TcKind]
@@ -126,41 +123,46 @@ newKindVars n = mapNF_Tc (\ _ -> newKindVar) (nOfThem n ())
 newBoxityVar :: NF_TcM TcKind
 newBoxityVar
   = tcGetUnique                                                          `thenNF_Tc` \ uniq ->
-    tcNewMutTyVar (mkSysLocalName uniq SLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
+    tcNewMutTyVar (mkSystemName uniq FSLIT("bx")) superBoxity VanillaTv  `thenNF_Tc` \ kv ->
     returnNF_Tc (TyVarTy kv)
 \end{code}
 
 
 %************************************************************************
 %*                                                                     *
-\subsection{Type instantiation}
+\subsection{'hole' type variables}
 %*                                                                     *
 %************************************************************************
 
-I don't understand why this is needed
-An old comments says "No need for tcSplitForAllTyM because a type 
-       variable can't be instantiated to a for-all type"
-But the same is true of rho types!
-
 \begin{code}
-tcSplitRhoTyM :: TcType -> NF_TcM (TcThetaType, TcType)
-tcSplitRhoTyM t
-  = go t t []
- where
-       -- A type variable is never instantiated to a dictionary type,
-       -- so we don't need to do a tcReadVar on the "arg".
-    go syn_t (FunTy arg res) ts = case tcSplitPredTy_maybe arg of
-                                       Just pair -> go res res (pair:ts)
-                                       Nothing   -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t (NoteTy n t)    ts = go syn_t t ts
-    go syn_t (TyVarTy tv)    ts = getTcTyVar tv                `thenNF_Tc` \ maybe_ty ->
-                                 case maybe_ty of
-                                   Just ty | not (tcIsTyVarTy ty) -> go syn_t ty ts
-                                   other                          -> returnNF_Tc (reverse ts, syn_t)
-    go syn_t (UsageTy _ t)   ts = go syn_t t ts
-    go syn_t t              ts = returnNF_Tc (reverse ts, syn_t)
-\end{code}
+newHoleTyVarTy :: NF_TcM TcType
+  = tcGetUnique        `thenNF_Tc` \ uniq ->
+    tcNewMutTyVar (mkSystemName uniq FSLIT("h")) openTypeKind HoleTv   `thenNF_Tc` \ tv ->
+    returnNF_Tc (TyVarTy tv)
 
+readHoleResult :: TcType -> NF_TcM TcType
+-- Read the answer out of a hole, constructed by newHoleTyVarTy
+readHoleResult (TyVarTy tv)
+  = ASSERT( isHoleTyVar tv )
+    getTcTyVar tv              `thenNF_Tc` \ maybe_res ->
+    case maybe_res of
+       Just ty -> returnNF_Tc ty
+       Nothing ->  pprPanic "readHoleResult: empty" (ppr tv)
+readHoleResult ty = pprPanic "readHoleResult: not hole" (ppr ty)
+
+zapToType :: TcType -> NF_TcM TcType
+zapToType (TyVarTy tv)
+  | isHoleTyVar tv
+  = getTcTyVar tv              `thenNF_Tc` \ maybe_res ->
+    case maybe_res of
+       Nothing -> newTyVarTy openTypeKind      `thenNF_Tc` \ ty ->
+                  putTcTyVar tv ty             `thenNF_Tc_`
+                  returnNF_Tc ty
+       Just ty  -> returnNF_Tc ty      -- No need to loop; we never
+                                       -- have chains of holes
+
+zapToType other_ty = returnNF_Tc other_ty
+\end{code}                
 
 %************************************************************************
 %*                                                                     *
@@ -171,11 +173,11 @@ tcSplitRhoTyM t
 Instantiating a bunch of type variables
 
 \begin{code}
-tcInstTyVars :: [TyVar] 
+tcInstTyVars :: TyVarDetails -> [TyVar] 
             -> NF_TcM ([TcTyVar], [TcType], Subst)
 
-tcInstTyVars tyvars
-  = mapNF_Tc tcInstTyVar tyvars        `thenNF_Tc` \ tc_tyvars ->
+tcInstTyVars tv_details tyvars
+  = mapNF_Tc (tcInstTyVar tv_details) tyvars   `thenNF_Tc` \ tc_tyvars ->
     let
        tys = mkTyVarTys tc_tyvars
     in
@@ -184,7 +186,7 @@ tcInstTyVars tyvars
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence mkTopTyVarSubst
 
-tcInstTyVar tyvar
+tcInstTyVar tv_details tyvar
   = tcGetUnique                `thenNF_Tc` \ uniq ->
     let
        name = setNameUnique (tyVarName tyvar) uniq
@@ -193,66 +195,31 @@ tcInstTyVar tyvar
        -- that two different tyvars will print the same way 
        -- in an error message.  -dppr-debug will show up the difference
        -- Better watch out for this.  If worst comes to worst, just
-       -- use mkSysLocalName.
+       -- use mkSystemName.
     in
-    tcNewMutTyVar name (tyVarKind tyvar) VanillaTv
-
-tcInstSigTyVars :: TyVarDetails -> [TyVar] -> NF_TcM [TcTyVar]
-tcInstSigTyVars details tyvars -- Very similar to tcInstTyVar
-  = tcGetUniques       `thenNF_Tc` \ uniqs ->
-    listTc [ ASSERT( not (kind `eqKind` openTypeKind) )        -- Shouldn't happen
-            tcNewMutTyVar name kind details
-          | (tyvar, uniq) <- tyvars `zip` uniqs,
-            let name = setNameUnique (tyVarName tyvar) uniq, 
-            let kind = tyVarKind tyvar
-          ]
-\end{code}
-
-@tcInstType@ instantiates the outer-level for-alls of a TcType with
-fresh type variables, splits off the dictionary part, and returns the results.
+    tcNewMutTyVar name (tyVarKind tyvar) tv_details
 
-\begin{code}
-tcInstType :: TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
-tcInstType ty
+tcInstType :: TyVarDetails -> TcType -> NF_TcM ([TcTyVar], TcThetaType, TcType)
+-- tcInstType instantiates the outer-level for-alls of a TcType with
+-- fresh (mutable) type variables, splits off the dictionary part, 
+-- and returns the pieces.
+tcInstType tv_details ty
   = case tcSplitForAllTys ty of
-       ([],     rho) ->        -- There may be overloading but no type variables;
+       ([],     rho) ->        -- There may be overloading despite no type variables;
                                --      (?x :: Int) => Int -> Int
                         let
-                          (theta, tau) = tcSplitRhoTy rho      -- Used to be tcSplitRhoTyM
+                          (theta, tau) = tcSplitPhiTy rho
                         in
                         returnNF_Tc ([], theta, tau)
 
-       (tyvars, rho) -> tcInstTyVars tyvars                    `thenNF_Tc` \ (tyvars', _, tenv)  ->
+       (tyvars, rho) -> tcInstTyVars tv_details tyvars         `thenNF_Tc` \ (tyvars', _, tenv) ->
                         let
-                          (theta, tau) = tcSplitRhoTy (substTy tenv rho)       -- Used to be tcSplitRhoTyM
+                          (theta, tau) = tcSplitPhiTy (substTy tenv rho)
                         in
                         returnNF_Tc (tyvars', theta, tau)
-
-
-tcInstSigType :: TyVarDetails -> Type -> NF_TcM ([TcTyVar], TcThetaType, TcType)
--- Very similar to tcInstSigType, but uses signature type variables
--- Also, somewhat arbitrarily, don't deal with the monomorphic case so efficiently
-tcInstSigType tv_details poly_ty
- = let
-       (tyvars, rho) = tcSplitForAllTys poly_ty
-   in
-   tcInstSigTyVars tv_details tyvars           `thenNF_Tc` \ tyvars' ->
-       -- Make *signature* type variables
-
-   let
-     tyvar_tys' = mkTyVarTys tyvars'
-     rho' = substTy (mkTopTyVarSubst tyvars tyvar_tys') rho
-       -- mkTopTyVarSubst because the tyvars' are fresh
-
-     (theta', tau') = tcSplitRhoTy rho'
-       -- This splitRhoTy tries hard to make sure that tau' is a type synonym
-       -- wherever possible, which can improve interface files.
-   in
-   returnNF_Tc (tyvars', theta', tau')
 \end{code}
 
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{Putting and getting  mutable type variables}
@@ -274,7 +241,6 @@ putTcTyVar tyvar ty
 
   | otherwise
   = ASSERT( isMutTyVar tyvar )
-    UASSERT2( not (isUTy ty), ppr tyvar <+> ppr ty )
     tcWriteMutTyVar tyvar (Just ty)    `thenNF_Tc_`
     returnNF_Tc ty
 \end{code}
@@ -343,14 +309,6 @@ zonkTcTyVarsAndFV tyvars = mapNF_Tc zonkTcTyVar tyvars     `thenNF_Tc` \ tys ->
 
 zonkTcTyVar :: TcTyVar -> NF_TcM TcType
 zonkTcTyVar tyvar = zonkTyVar (\ tv -> returnNF_Tc (TyVarTy tv)) tyvar
-
-zonkTcSigTyVars :: [TcTyVar] -> NF_TcM [TcTyVar]
--- This guy is to zonk the tyvars we're about to feed into tcSimplify
--- Usually this job is done by checkSigTyVars, but in a couple of places
--- that is overkill, so we use this simpler chap
-zonkTcSigTyVars tyvars
-  = zonkTcTyVars tyvars        `thenNF_Tc` \ tys ->
-    returnNF_Tc (map (tcGetTyVar "zonkTcSigTyVars") tys)
 \end{code}
 
 -----------------  Types
@@ -400,32 +358,64 @@ zonkKindEnv pairs
 zonkTcTypeToType :: TcType -> NF_TcM Type
 zonkTcTypeToType ty = zonkType zonk_unbound_tyvar ty
   where
-       -- Zonk a mutable but unbound type variable to
-       --      Void            if it has kind Lifted
-       --      :Void           otherwise
+       -- Zonk a mutable but unbound type variable to an arbitrary type
        -- We know it's unbound even though we don't carry an environment,
        -- because at the binding site for a type variable we bind the
        -- mutable tyvar to a fresh immutable one.  So the mutable store
        -- plays the role of an environment.  If we come across a mutable
        -- type variable that isn't so bound, it must be completely free.
-    zonk_unbound_tyvar tv
-       | kind `eqKind` liftedTypeKind || kind `eqKind` openTypeKind
-       = putTcTyVar tv voidTy  -- Just to avoid creating a new tycon in
-                               -- this vastly common case
-       | otherwise
-       = putTcTyVar tv (TyConApp (mk_void_tycon tv kind) [])
-       where
-         kind = tyVarKind tv
-
-    mk_void_tycon tv kind      -- Make a new TyCon with the same kind as the 
-                               -- type variable tv.  Same name too, apart from
-                               -- making it start with a colon (sigh)
+    zonk_unbound_tyvar tv = putTcTyVar tv (mkArbitraryType tv)
+
+
+-- When the type checker finds a type variable with no binding,
+-- which means it can be instantiated with an arbitrary type, it
+-- usually instantiates it to Void.  Eg.
+-- 
+--     length []
+-- ===>
+--     length Void (Nil Void)
+-- 
+-- But in really obscure programs, the type variable might have
+-- a kind other than *, so we need to invent a suitably-kinded type.
+-- 
+-- This commit uses
+--     Void for kind *
+--     List for kind *->*
+--     Tuple for kind *->...*->*
+-- 
+-- which deals with most cases.  (Previously, it only dealt with
+-- kind *.)   
+-- 
+-- In the other cases, it just makes up a TyCon with a suitable
+-- kind.  If this gets into an interface file, anyone reading that
+-- file won't understand it.  This is fixable (by making the client
+-- of the interface file make up a TyCon too) but it is tiresome and
+-- never happens, so I am leaving it 
+
+mkArbitraryType :: TcTyVar -> Type
+-- Make up an arbitrary type whose kind is the same as the tyvar.
+-- We'll use this to instantiate the (unbound) tyvar.
+mkArbitraryType tv 
+  | isAnyTypeKind kind = voidTy                -- The vastly common case
+  | otherwise         = TyConApp tycon []
+  where
+    kind       = tyVarKind tv
+    (args,res) = Type.splitFunTys kind -- Kinds are simple; use Type.splitFunTys
+
+    tycon | kind `eqKind` tyConKind listTyCon  -- *->*
+         = listTyCon                           -- No tuples this size
+
+         | all isTypeKind args && isTypeKind res
+         = tupleTyCon Boxed (length args)      -- *-> ... ->*->*
+
+         | otherwise
+         = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
+           mkPrimTyCon tc_name kind 0 [] VoidRep
+               -- Same name as the tyvar, apart from making it start with a colon (sigh)
                -- I dread to think what will happen if this gets out into an 
                -- interface file.  Catastrophe likely.  Major sigh.
-       = pprTrace "Urk! Inventing strangely-kinded void TyCon" (ppr tc_name) $
-         mkPrimTyCon tc_name kind 0 [] VoidRep
-       where
-         tc_name = mkLocalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
+
+    tc_name = mkInternalName (getUnique tv) (mkDerivedTyConOcc (getOccName tv)) noSrcLoc
 
 -- zonkTcTyVarToTyVar is applied to the *binding* occurrence 
 -- of a type variable, at the *end* of type checking.  It changes
@@ -497,10 +487,9 @@ zonkType unbound_var_fn ty
     go (AppTy fun arg)           = go fun              `thenNF_Tc` \ fun' ->
                                    go arg              `thenNF_Tc` \ arg' ->
                                    returnNF_Tc (mkAppTy fun' arg')
-
-    go (UsageTy u ty)             = go u                `thenNF_Tc` \ u'  ->
-                                    go ty               `thenNF_Tc` \ ty' ->
-                                    returnNF_Tc (UsageTy u' ty')
+               -- NB the mkAppTy; we might have instantiated a
+               -- type variable to a type constructor, so we need
+               -- to pull the TyConApp to the top.
 
        -- The two interesting cases!
     go (TyVarTy tyvar)     = zonkTyVar unbound_var_fn tyvar
@@ -634,6 +623,14 @@ checkValidType ctxt ty
                        GenPatCtxt   -> actual_kind_is_lifted
                        ForSigCtxt _ -> actual_kind_is_lifted
                        other        -> isTypeKind actual_kind
+       
+       ubx_tup | not gla_exts = UT_NotOk
+               | otherwise    = case ctxt of
+                                  TySynCtxt _ -> UT_Ok
+                                  other       -> UT_NotOk
+               -- Unboxed tuples ok in function results,
+               -- but for type synonyms we allow them even at
+               -- top level
     in
     tcAddErrCtxt (checkTypeCtxt ctxt ty)       $
 
@@ -641,7 +638,7 @@ checkValidType ctxt ty
     checkTc kind_ok (kindErr actual_kind)      `thenTc_`
 
        -- Check the internal validity of the type itself
-    check_poly_type rank ty
+    check_poly_type rank ubx_tup ty
 
 
 checkTypeCtxt ctxt ty
@@ -670,17 +667,23 @@ decRank :: Rank -> Rank
 decRank Arbitrary = Arbitrary
 decRank (Rank n)  = Rank (n-1)
 
-check_poly_type :: Rank -> Type -> TcM ()
-check_poly_type (Rank 0) ty 
-  = check_tau_type (Rank 0) False ty
+----------------------------------------
+data UbxTupFlag = UT_Ok        | UT_NotOk
+       -- The "Ok" version means "ok if -fglasgow-exts is on"
 
-check_poly_type rank ty 
+----------------------------------------
+check_poly_type :: Rank -> UbxTupFlag -> Type -> TcM ()
+check_poly_type (Rank 0) ubx_tup ty 
+  = check_tau_type (Rank 0) ubx_tup ty
+
+check_poly_type rank ubx_tup ty 
   = let
        (tvs, theta, tau) = tcSplitSigmaTy ty
     in
     check_valid_theta SigmaCtxt theta          `thenTc_`
-    check_tau_type (decRank rank) False tau    `thenTc_`
-    checkAmbiguity tvs theta tau
+    check_tau_type (decRank rank) ubx_tup tau  `thenTc_`
+    checkFreeness tvs theta                    `thenTc_`
+    checkAmbiguity tvs theta (tyVarsOfType tau)
 
 ----------------------------------------
 check_arg_type :: Type -> TcM ()
@@ -699,49 +702,58 @@ check_arg_type :: Type -> TcM ()
 -- NB: unboxed tuples can have polymorphic or unboxed args.
 --     This happens in the workers for functions returning
 --     product types with polymorphic components.
---     But not in user code
--- 
--- Question: what about nested unboxed tuples?
---          Currently rejected.
+--     But not in user code.
+-- Anyway, they are dealt with by a special case in check_tau_type
+
 check_arg_type ty 
-  = check_tau_type (Rank 0) False ty   `thenTc_` 
+  = check_tau_type (Rank 0) UT_NotOk ty                `thenTc_` 
     checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty)
 
 ----------------------------------------
-check_tau_type :: Rank -> Bool -> Type -> TcM ()
+check_tau_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 -- Rank is allowed rank for function args
 -- No foralls otherwise
--- Bool is True iff unboxed tuple are allowed here
-
-check_tau_type rank ubx_tup_ok ty@(UsageTy _ _)  = failWithTc (usageTyErr ty)
-check_tau_type rank ubx_tup_ok ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
-check_tau_type rank ubx_tup_ok (SourceTy sty)    = getDOptsTc          `thenNF_Tc` \ dflags ->
-                                                  check_source_ty dflags TypeCtxt sty
-check_tau_type rank ubx_tup_ok (TyVarTy _)       = returnTc ()
-check_tau_type rank ubx_tup_ok ty@(FunTy arg_ty res_ty)
-  = check_poly_type rank      arg_ty   `thenTc_`
-    check_tau_type  rank True res_ty
-
-check_tau_type rank ubx_tup_ok (AppTy ty1 ty2)
-  = check_arg_type ty1 `thenTc_` check_arg_type ty2
 
-check_tau_type rank ubx_tup_ok (NoteTy note ty)
-  = check_note note `thenTc_` check_tau_type rank ubx_tup_ok ty
+check_tau_type rank ubx_tup ty@(ForAllTy _ _) = failWithTc (forAllTyErr ty)
+check_tau_type rank ubx_tup (SourceTy sty)    = getDOptsTc             `thenNF_Tc` \ dflags ->
+                                               check_source_ty dflags TypeCtxt sty
+check_tau_type rank ubx_tup (TyVarTy _)       = returnTc ()
+check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+  = check_poly_type rank UT_NotOk arg_ty       `thenTc_`
+    check_tau_type  rank UT_Ok    res_ty
 
-check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
-  | isSynTyCon tc
-  = checkTc syn_arity_ok arity_msg     `thenTc_`
+check_tau_type rank ubx_tup (AppTy ty1 ty2)
+  = check_arg_type ty1 `thenTc_` check_arg_type ty2
+
+check_tau_type rank ubx_tup (NoteTy note ty)
+  = check_tau_type rank ubx_tup ty
+       -- Synonym notes are built only when the synonym is 
+       -- saturated (see Type.mkSynTy)
+       -- Not checking the 'note' part allows us to instantiate a synonym
+       -- defn with a for-all type, or with a partially-applied type synonym,
+       -- but that seems OK too
+
+check_tau_type rank ubx_tup ty@(TyConApp tc tys)
+  | isSynTyCon tc      
+  =    -- NB: Type.mkSynTy builds a TyConApp (not a NoteTy) for an unsaturated
+       -- synonym application, leaving it to checkValidType (i.e. right here
+       -- to find the error
+    checkTc syn_arity_ok arity_msg     `thenTc_`
     mapTc_ check_arg_type tys
     
   | isUnboxedTupleTyCon tc
-  = checkTc ubx_tup_ok ubx_tup_msg     `thenTc_`
-    mapTc_ (check_tau_type (Rank 0) True) tys  -- Args are allowed to be unlifted, or
-                                               -- more unboxed tuples, so can't use check_arg_ty
+  = doptsTc Opt_GlasgowExts                    `thenNF_Tc` \ gla_exts ->
+    checkTc (ubx_tup_ok gla_exts) ubx_tup_msg  `thenTc_`
+    mapTc_ (check_tau_type (Rank 0) UT_Ok) tys 
+                       -- Args are allowed to be unlifted, or
+                       -- more unboxed tuples, so can't use check_arg_ty
 
   | otherwise
   = mapTc_ check_arg_type tys
 
   where
+    ubx_tup_ok gla_exts = case ubx_tup of { UT_Ok -> gla_exts; other -> False }
+
     syn_arity_ok = tc_arity <= n_args
                -- It's OK to have an *over-applied* type synonym
                --      data Tree a b = ...
@@ -754,8 +766,10 @@ check_tau_type rank ubx_tup_ok ty@(TyConApp tc tys)
     ubx_tup_msg = ubxArgTyErr ty
 
 ----------------------------------------
-check_note (FTVNote _)  = returnTc ()
-check_note (SynNote ty) = check_tau_type (Rank 0) False ty
+forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
+unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
+ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
+kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 \end{code}
 
 Check for ambiguity
@@ -771,12 +785,6 @@ 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.
-
 NB; the ambiguity check is only used for *user* types, not for types
 coming from inteface files.  The latter can legitimately have
 ambiguous types. Example
@@ -795,46 +803,47 @@ don't need to check for ambiguity either, because the test can't fail
 (see is_ambig).
 
 \begin{code}
-checkAmbiguity :: [TyVar] -> ThetaType -> Type -> TcM ()
-checkAmbiguity forall_tyvars theta tau
-  = mapTc_ check_pred theta    `thenTc_`
-    returnTc ()
+checkAmbiguity :: [TyVar] -> ThetaType -> TyVarSet -> TcM ()
+checkAmbiguity forall_tyvars theta tau_tyvars
+  = mapTc_ complain (filter is_ambig theta)
   where
-    tau_vars         = tyVarsOfType tau
-    extended_tau_vars = grow theta tau_vars
+    complain pred     = addErrTc (ambigErr pred)
+    extended_tau_vars = grow theta tau_tyvars
+    is_ambig pred     = any ambig_var (varSetElems (tyVarsOfPred pred))
 
-    is_ambig ct_var   = (ct_var `elem` forall_tyvars) &&
+    ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
                        not (ct_var `elemVarSet` extended_tau_vars)
+
     is_free ct_var    = not (ct_var `elem` forall_tyvars)
-    
-    check_pred pred = checkTc (not any_ambig)                 (ambigErr pred) `thenTc_`
-                     checkTc (isIPPred pred || not all_free) (freeErr  pred)
-             where 
-               ct_vars   = varSetElems (tyVarsOfPred pred)
-               all_free  = all is_free ct_vars
-               any_ambig = any is_ambig ct_vars
-\end{code}
 
-\begin{code}
 ambigErr pred
   = sep [ptext SLIT("Ambiguous constraint") <+> quotes (pprPred pred),
         nest 4 (ptext SLIT("At least one of the forall'd type variables mentioned by the constraint") $$
                 ptext SLIT("must be reachable from the type after the '=>'"))]
+\end{code}
+    
+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.
 
+\begin{code}
+checkFreeness forall_tyvars theta
+  = mapTc_ complain (filter is_free theta)
+  where    
+    is_free pred     =  not (isIPPred pred)
+                    && not (any bound_var (varSetElems (tyVarsOfPred pred)))
+    bound_var ct_var = ct_var `elem` forall_tyvars
+    complain pred    = addErrTc (freeErr pred)
 
 freeErr pred
   = sep [ptext SLIT("All of the type variables in the constraint") <+> quotes (pprPred pred) <+>
                   ptext SLIT("are already in scope"),
         nest 4 (ptext SLIT("At least one must be universally quantified here"))
     ]
-
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic type:") <+> ppr_ty ty
-usageTyErr      ty = ptext SLIT("Illegal usage type:") <+> ppr_ty ty
-unliftedArgErr  ty = ptext SLIT("Illegal unlifted type argument:") <+> ppr_ty ty
-ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr_ty ty
-kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
 \end{code}
 
+
 %************************************************************************
 %*                                                                     *
 \subsection{Checking a theta or source type}
@@ -876,7 +885,7 @@ check_valid_theta ctxt theta
 -------------------------
 check_source_ty dflags ctxt pred@(ClassP cls tys)
   =    -- Class predicates are valid in all contexts
-    mapTc_ check_arg_type tys                  `thenTc_`
+    mapTc_ check_arg_type tys          `thenTc_`
     checkTc (arity == n_tys) arity_err         `thenTc_`
     checkTc (all tyvar_head tys || arby_preds_ok)
            (predTyVarErr pred $$ how_to_allow)
@@ -1023,5 +1032,3 @@ nonBoxedPrimCCallErr clas inst_ty
   = hang (ptext SLIT("Unacceptable instance type for ccall-ish class"))
         4 (pprClassPred clas [inst_ty])
 \end{code}
-
-