Major change in compilation of instance declarations (fix Trac #955, #2328)
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
index 30917ef..1addfe4 100644 (file)
@@ -9,13 +9,6 @@ This module contains monadic operations over types that contain
 mutable type variables
 
 \begin{code}
-{-# OPTIONS -w #-}
--- The above warning supression flag is a temporary kludge.
--- While working on this module you are encouraged to remove it and fix
--- any warnings in the module. See
---     http://hackage.haskell.org/trac/ghc/wiki/Commentary/CodingStyle#Warnings
--- for details
-
 module TcMType (
   TcTyVar, TcKind, TcType, TcTauType, TcThetaType, TcTyVarSet,
 
@@ -40,8 +33,8 @@ module TcMType (
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
-  tcInstSigTyVars,
-  tcInstSkolTyVar, tcInstSkolTyVars, tcInstSkolType, 
+  tcInstSigType,
+  tcInstSkolTyVars, tcInstSkolType, 
   tcSkolSigType, tcSkolSigTyVars, occurCheckErr,
 
   --------------------------------
@@ -58,7 +51,7 @@ module TcMType (
   zonkType, zonkTcPredType, 
   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
-  zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
+  zonkTcType, zonkTcTypes, zonkTcThetaType,
   zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
 
   readKindVar, writeKindVar
@@ -79,6 +72,7 @@ import Var
 import TcRnMonad          -- TcType, amongst others
 import FunDeps
 import Name
+import VarEnv
 import VarSet
 import ErrUtils
 import DynFlags
@@ -88,8 +82,9 @@ import ListSetOps
 import UniqSupply
 import SrcLoc
 import Outputable
+import FastString
 
-import Control.Monad   ( when, unless )
+import Control.Monad
 import Data.List       ( (\\) )
 \end{code}
 
@@ -159,6 +154,7 @@ updateMeta tv1 ref1 ty2
        }
 
 ----------------
+checkKinds :: Bool -> TyVar -> Type -> TcM ()
 checkKinds swapped tv1 ty2
 -- We're about to unify a type variable tv1 with a non-tyvar-type ty2.
 -- ty2 has been zonked at this stage, which ensures that
@@ -183,7 +179,7 @@ checkTauTvUpdate :: TcTyVar -> TcType -> TcM (Maybe TcType)
 --    (checkTauTvUpdate tv ty)
 -- We are about to update the TauTv tv with ty.
 -- Check (a) that tv doesn't occur in ty (occurs check)
---      (b) that ty is a monotype
+--       (b) that ty is a monotype
 -- Furthermore, in the interest of (b), if you find an
 -- empty box (BoxTv that is Flexi), fill it in with a TauTv
 -- 
@@ -222,7 +218,7 @@ checkTauTvUpdate orig_tv orig_ty
        | isSynTyCon tc  = go_syn tc tys
        | otherwise      = do { tys' <- mapM go tys
                               ; return $ occurs (TyConApp tc) tys' }
-    go (PredTy p)       = do { p' <- go_pred p
+    go (PredTy p)            = do { p' <- go_pred p
                               ; return $ occurs1 PredTy p' }
     go (FunTy arg res)   = do { arg' <- go arg
                               ; res' <- go res
@@ -233,7 +229,7 @@ checkTauTvUpdate orig_tv orig_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.
-    go (ForAllTy tv ty) = notMonoType orig_ty          -- (b)
+    go (ForAllTy _ _) = notMonoType orig_ty            -- (b)
 
     go (TyVarTy tv)
        | orig_tv == tv = return $ Left False           -- (a)
@@ -258,7 +254,7 @@ checkTauTvUpdate orig_tv orig_ty
                  Flexi -> case box of
                                BoxTv -> do { ty <- fillBoxWithTau tv ref
                                             ; return $ Right ty }
-                               other -> return $ Right (TyVarTy tv)
+                               _     -> return $ Right (TyVarTy tv)
             }
 
        -- go_syn is called for synonyms only
@@ -267,7 +263,7 @@ checkTauTvUpdate orig_tv orig_ty
        | not (isTauTyCon tc)
        = notMonoType orig_ty   -- (b) again
        | otherwise
-       = do { (msgs, mb_tys') <- tryTc (mapM go tys)
+       = do { (_msgs, mb_tys') <- tryTc (mapM go tys)
             ; case mb_tys' of
 
                 -- we had a type error => forall in type parameters
@@ -343,22 +339,24 @@ Rather, we should bind t to () (= non_var_ty2).
 Error mesages in case of kind mismatch.
 
 \begin{code}
+unifyKindMisMatch :: TcKind -> TcKind -> TcM ()
 unifyKindMisMatch ty1 ty2 = do
     ty1' <- zonkTcKind ty1
     ty2' <- zonkTcKind ty2
     let
-       msg = hang (ptext SLIT("Couldn't match kind"))
+       msg = hang (ptext (sLit "Couldn't match kind"))
                   2 (sep [quotes (ppr ty1'), 
-                          ptext SLIT("against"), 
+                          ptext (sLit "against"), 
                           quotes (ppr ty2')])
     failWithTc msg
 
+unifyKindCtxt :: Bool -> TyVar -> Type -> TidyEnv -> TcM (TidyEnv, SDoc)
 unifyKindCtxt swapped tv1 ty2 tidy_env -- not swapped => tv1 expected, ty2 inferred
        -- tv1 and ty2 are zonked already
   = return msg
   where
-    msg = (env2, ptext SLIT("When matching the kinds of") <+> 
-                sep [quotes pp_expected <+> ptext SLIT("and"), quotes pp_actual])
+    msg = (env2, ptext (sLit "When matching the kinds of") <+> 
+                sep [quotes pp_expected <+> ptext (sLit "and"), quotes pp_actual])
 
     (pp_expected, pp_actual) | swapped   = (pp2, pp1)
                             | otherwise = (pp1, pp2)
@@ -381,7 +379,7 @@ occurCheckErr ty containingTy
              extra = sep [ppr tidy_ty1, char '=', ppr tidy_ty2]
        ; failWithTcM (env2, hang msg 2 extra) }
   where
-    msg = ptext SLIT("Occurs check: cannot construct the infinite type:")
+    msg = ptext (sLit "Occurs check: cannot construct the infinite type:")
 \end{code}
 
 %************************************************************************
@@ -394,7 +392,7 @@ occurCheckErr ty containingTy
 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
 newCoVars spec
   = do { us <- newUniqueSupply 
-       ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
+       ; return [ mkCoVar (mkSysTvName uniq (fsLit "co"))
                           (mkCoKind ty1 ty2)
                 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
 
@@ -432,17 +430,17 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
                              | tv <- tyvars ]
 
-tcInstSkolTyVar :: SkolemInfo -> Maybe SrcSpan -> TyVar -> TcM TcTyVar
+tcInstSkolTyVar :: SkolemInfo -> (Name -> SrcSpan) -> TyVar -> TcM TcTyVar
 -- Instantiate the tyvar, using 
 --     * the occ-name and kind of the supplied tyvar, 
 --     * the unique from the monad,
 --     * the location either from the tyvar (mb_loc = Nothing)
 --       or from mb_loc (Just loc)
-tcInstSkolTyVar info mb_loc tyvar
+tcInstSkolTyVar info get_loc tyvar
   = do { uniq <- newUnique
        ; let old_name = tyVarName tyvar
              kind     = tyVarKind tyvar
-             loc      = mb_loc `orElse` getSrcSpan old_name
+             loc      = get_loc old_name
              new_name = mkInternalName uniq (nameOccName old_name) loc
        ; return (mkSkolTyVar new_name kind info) }
 
@@ -450,12 +448,21 @@ tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
 -- Get the location from the monad
 tcInstSkolTyVars info tyvars 
   = do         { span <- getSrcSpanM
-       ; mapM (tcInstSkolTyVar info (Just span)) tyvars }
+       ; mapM (tcInstSkolTyVar info (const span)) tyvars }
 
 tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
 -- Instantiate a type with fresh skolem constants
 -- Binding location comes from the monad
 tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
+
+tcInstSigType :: Bool -> SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcRhoType)
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigType use_skols skol_info ty
+  = tcInstType (mapM inst_tyvar) ty
+  where
+    inst_tyvar | use_skols = tcInstSkolTyVar skol_info getSrcSpan
+              | otherwise = instMetaTyVar (SigTv skol_info)
 \end{code}
 
 
@@ -473,9 +480,9 @@ newMetaTyVar box_info kind
        ; ref <- newMutVar Flexi
        ; let name = mkSysTvName uniq fs 
              fs = case box_info of
-                       BoxTv   -> FSLIT("t")
-                       TauTv   -> FSLIT("t")
-                       SigTv _ -> FSLIT("a")
+                       BoxTv   -> fsLit "t"
+                       TauTv   -> fsLit "t"
+                       SigTv _ -> fsLit "a"
                -- We give BoxTv and TauTv the same string, because
                -- otherwise we get user-visible differences in error
                -- messages, which are confusing.  If you want to see
@@ -519,8 +526,8 @@ writeMetaTyVar tyvar ty
     do { ASSERTM2( do { details <- readMetaTyVar tyvar; return (isFlexi details) }, ppr tyvar )
        ; writeMutVar (metaTvRef tyvar) (Indirect ty) }
   where
-    k1 = tyVarKind tyvar
-    k2 = typeKind ty
+    _k1 = tyVarKind tyvar
+    _k2 = typeKind ty
 \end{code}
 
 
@@ -565,16 +572,6 @@ tcInstTyVars tyvars
 %************************************************************************
 
 \begin{code}
-tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with skolems or meta SigTvs; depending on use_skols
--- Always take location info from the supplied tyvars
-tcInstSigTyVars use_skols skol_info tyvars 
-  | use_skols
-  = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
-
-  | otherwise
-  = mapM (instMetaTyVar (SigTv skol_info)) tyvars
-
 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
 zonkSigTyVar sig_tv 
   | isSkolemTyVar sig_tv 
@@ -712,11 +709,6 @@ zonkTcType ty = zonkType (\ tv -> return (TyVarTy tv)) ty
 zonkTcTypes :: [TcType] -> TcM [TcType]
 zonkTcTypes tys = mapM zonkTcType tys
 
-zonkTcClassConstraints cts = mapM zonk cts
-    where zonk (clas, tys) = do
-              new_tys <- zonkTcTypes tys
-              return (clas, new_tys)
-
 zonkTcThetaType :: TcThetaType -> TcM TcThetaType
 zonkTcThetaType theta = mapM zonkTcPredType theta
 
@@ -818,7 +810,7 @@ Consider this:
 * Now abstract over the 'a', but float out the Num (C d a) constraint
   because it does not 'really' mention a.  (see exactTyVarsOfType)
   The arg to foo becomes
-       /\a -> \t -> t+t
+       \/\a -> \t -> t+t
 
 * So we get a dict binding for Num (C d a), which is zonked to give
        a = ()
@@ -827,10 +819,10 @@ Consider this:
   quantification, so the floated dict will still have type (C d a).
   Which renders this whole note moot; happily!]
 
-* Then the /\a abstraction has a zonked 'a' in it.
+* Then the \/\a abstraction has a zonked 'a' in it.
 
 All very silly.   I think its harmless to ignore the problem.  We'll end up with
-a /\a in the final result but all the occurrences of a will be zonked to ()
+a \/\a in the final result but all the occurrences of a will be zonked to ()
 
 Note [Zonking to Skolem]
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1000,35 +992,35 @@ checkValidType ctxt ty = do
     rankn    <- doptM Opt_RankNTypes
     polycomp <- doptM Opt_PolymorphicComponents
     let 
-       rank | rankn = Arbitrary
-            | rank2 = Rank 2
-            | otherwise
-            = case ctxt of     -- Haskell 98
-                GenPatCtxt     -> Rank 0
-                LamPatSigCtxt  -> Rank 0
-                BindPatSigCtxt -> Rank 0
-                DefaultDeclCtxt-> Rank 0
-                ResSigCtxt     -> Rank 0
-                TySynCtxt _    -> Rank 0
-                ExprSigCtxt    -> Rank 1
-                FunSigCtxt _   -> Rank 1
-                ConArgCtxt _   -> if polycomp
-                           then Rank 2
+       gen_rank n | rankn     = ArbitraryRank
+                  | rank2     = Rank 2
+                  | otherwise = Rank n
+       rank
+         = case ctxt of
+                GenPatCtxt     -> MustBeMonoType
+                DefaultDeclCtxt-> MustBeMonoType
+                ResSigCtxt     -> MustBeMonoType
+                LamPatSigCtxt  -> gen_rank 0
+                BindPatSigCtxt -> gen_rank 0
+                TySynCtxt _    -> gen_rank 0
+                ExprSigCtxt    -> gen_rank 1
+                FunSigCtxt _   -> gen_rank 1
+                ConArgCtxt _   | polycomp -> gen_rank 2
                                 -- We are given the type of the entire
                                 -- constructor, hence rank 1
-                           else Rank 1
-                ForSigCtxt _   -> Rank 1
-                SpecInstCtxt   -> Rank 1
+                               | otherwise -> gen_rank 1
+                ForSigCtxt _   -> gen_rank 1
+                SpecInstCtxt   -> gen_rank 1
 
        actual_kind = typeKind ty
 
        kind_ok = case ctxt of
-                       TySynCtxt _  -> True    -- Any kind will do
-                       ResSigCtxt   -> isSubOpenTypeKind        actual_kind
-                       ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
+                       TySynCtxt _  -> True -- Any kind will do
+                       ResSigCtxt   -> isSubOpenTypeKind actual_kind
+                       ExprSigCtxt  -> isSubOpenTypeKind actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
-                       other        -> isSubArgTypeKind    actual_kind
+                       _            -> isSubArgTypeKind actual_kind
        
        ubx_tup = case ctxt of
                      TySynCtxt _ | unboxed -> UT_Ok
@@ -1044,34 +1036,39 @@ checkValidType ctxt ty = do
     traceTc (text "checkValidType done" <+> ppr ty)
 
 checkValidMonoType :: Type -> TcM ()
-checkValidMonoType ty = check_mono_type ty
+checkValidMonoType ty = check_mono_type MustBeMonoType ty
 \end{code}
 
 
 \begin{code}
-data Rank = Rank Int | Arbitrary
+data Rank = ArbitraryRank        -- Any rank ok
+          | MustBeMonoType       -- Monotype regardless of flags
+         | TyConArgMonoType      -- Monotype but could be poly if -XImpredicativeTypes
+          | Rank Int             -- Rank n, but could be more with -XRankNTypes
 
-decRank :: Rank -> Rank
-decRank Arbitrary = Arbitrary
-decRank (Rank n)  = Rank (n-1)
+decRank :: Rank -> Rank                  -- Function arguments
+decRank (Rank 0)   = Rank 0
+decRank (Rank n)   = Rank (n-1)
+decRank other_rank = other_rank
 
 nonZeroRank :: Rank -> Bool
-nonZeroRank (Rank 0) = False
-nonZeroRank _        = True
+nonZeroRank ArbitraryRank = True
+nonZeroRank (Rank n)     = n>0
+nonZeroRank _            = False
 
 ----------------------------------------
 data UbxTupFlag = UT_Ok        | UT_NotOk
-       -- The "Ok" version means "ok if -fglasgow-exts is on"
+       -- The "Ok" version means "ok if UnboxedTuples is on"
 
 ----------------------------------------
-check_mono_type :: Type -> TcM ()      -- No foralls anywhere
-                                       -- No unlifted types of any kind
-check_mono_type ty
-   = do { check_type (Rank 0) UT_NotOk ty
+check_mono_type :: Rank -> Type -> TcM ()      -- No foralls anywhere
+                                               -- No unlifted types of any kind
+check_mono_type rank ty
+   = do { check_type rank UT_NotOk ty
        ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
 
 check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
--- The args say what the *type* context requires, independent
+-- The args say what the *type context* requires, independent
 -- of *flag* settings.  You test the flag settings at usage sites.
 -- 
 -- Rank is allowed rank for function args
@@ -1079,7 +1076,7 @@ check_type :: Rank -> UbxTupFlag -> Type -> TcM ()
 
 check_type rank ubx_tup ty
   | not (null tvs && null theta)
-  = do { checkTc (nonZeroRank rank) (forAllTyErr ty)
+  = do { checkTc (nonZeroRank rank) (forAllTyErr rank ty)
                -- Reject e.g. (Maybe (?x::Int => Int)), 
                -- with a decent error message
        ; check_valid_theta SigmaCtxt theta
@@ -1093,16 +1090,16 @@ check_type rank ubx_tup ty
 --     {-# SPECIALISE instance Ord Char #-}
 -- The Right Thing would be to fix the way that SPECIALISE instance pragmas
 -- are handled, but the quick thing is just to permit PredTys here.
-check_type rank ubx_tup (PredTy sty)
+check_type _ _ (PredTy sty)
   = do { dflags <- getDOpts
        ; check_pred_ty dflags TypeCtxt sty }
 
-check_type rank ubx_tup (TyVarTy _)       = return ()
-check_type rank ubx_tup ty@(FunTy arg_ty res_ty)
+check_type _ _ (TyVarTy _) = return ()
+check_type rank _ (FunTy arg_ty res_ty)
   = do { check_type (decRank rank) UT_NotOk arg_ty
        ; check_type rank           UT_Ok    res_ty }
 
-check_type rank ubx_tup (AppTy ty1 ty2)
+check_type rank _ (AppTy ty1 ty2)
   = do { check_arg_type rank ty1
        ; check_arg_type rank ty2 }
 
@@ -1120,7 +1117,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
        ; liberal <- doptM Opt_LiberalTypeSynonyms
        ; if not liberal || isOpenSynTyCon tc then
                -- For H98 and synonym families, do check the type args
-               mapM_ check_mono_type tys
+               mapM_ (check_mono_type TyConArgMonoType) tys
 
          else  -- In the liberal case (only for closed syns), expand then check
          case tcView ty of   
@@ -1133,7 +1130,7 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
        ; checkTc (ubx_tup_ok ub_tuples_allowed) ubx_tup_msg
 
        ; impred <- doptM Opt_ImpredicativeTypes        
-       ; let rank' = if impred then rank else Rank 0
+       ; let rank' = if impred then ArbitraryRank else TyConArgMonoType
                -- c.f. check_arg_type
                -- However, args are allowed to be unlifted, or
                -- more unboxed tuples, so can't use check_arg_ty
@@ -1143,7 +1140,9 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
   = mapM_ (check_arg_type rank) tys
 
   where
-    ubx_tup_ok ub_tuples_allowed = case ubx_tup of { UT_Ok -> ub_tuples_allowed; other -> False }
+    ubx_tup_ok ub_tuples_allowed = case ubx_tup of
+                                   UT_Ok -> ub_tuples_allowed
+                                   _     -> False
 
     n_args    = length tys
     tc_arity  = tyConArity tc
@@ -1151,6 +1150,8 @@ check_type rank ubx_tup ty@(TyConApp tc tys)
     arity_msg   = arityErr "Type synonym" (tyConName tc) tc_arity n_args
     ubx_tup_msg = ubxArgTyErr ty
 
+check_type _ _ ty = pprPanic "check_type" (ppr ty)
+
 ----------------------------------------
 check_arg_type :: Rank -> Type -> TcM ()
 -- The sort of type that can instantiate a type variable,
@@ -1173,15 +1174,34 @@ check_arg_type :: Rank -> Type -> TcM ()
 
 check_arg_type rank ty 
   = do { impred <- doptM Opt_ImpredicativeTypes
-       ; let rank' = if impred then rank else Rank 0   -- Monotype unless impredicative
+       ; let rank' = if impred then ArbitraryRank  -- Arg of tycon can have arby rank, regardless
+                     else case rank of             -- Predictive => must be monotype
+                       MustBeMonoType -> MustBeMonoType 
+                       _              -> TyConArgMonoType
+                       -- Make sure that MustBeMonoType is propagated, 
+                       -- so that we don't suggest -XImpredicativeTypes in
+                       --    (Ord (forall a.a)) => a -> a
+
        ; check_type rank' UT_NotOk ty
        ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
 
 ----------------------------------------
-forAllTyErr     ty = ptext SLIT("Illegal polymorphic or qualified type:") <+> ppr ty
-unliftedArgErr  ty = ptext SLIT("Illegal unlifted type:") <+> ppr ty
-ubxArgTyErr     ty = ptext SLIT("Illegal unboxed tuple type as function argument:") <+> ppr ty
-kindErr kind       = ptext SLIT("Expecting an ordinary type, but found a type of kind") <+> ppr kind
+forAllTyErr :: Rank -> Type -> SDoc
+forAllTyErr rank ty 
+   = vcat [ hang (ptext (sLit "Illegal polymorphic or qualified type:")) 2 (ppr ty)
+          , suggestion ]
+  where
+    suggestion = case rank of
+                  Rank _ -> ptext (sLit "Perhaps you intended to use -XRankNTypes or -XRank2Types")
+                  TyConArgMonoType -> ptext (sLit "Perhaps you intended to use -XImpredicativeTypes")
+                  _ -> empty      -- Polytype is always illegal
+
+unliftedArgErr, ubxArgTyErr :: Type -> SDoc
+unliftedArgErr  ty = sep [ptext (sLit "Illegal unlifted type:"), ppr ty]
+ubxArgTyErr     ty = sep [ptext (sLit "Illegal unboxed tuple type as function argument:"), ppr ty]
+
+kindErr :: Kind -> SDoc
+kindErr kind       = sep [ptext (sLit "Expecting an ordinary type, but found a type of kind"), ppr kind]
 \end{code}
 
 Note [Liberal type synonyms]
@@ -1238,11 +1258,12 @@ data SourceTyCtxt
   | InstThetaCtxt      -- Context of an instance decl
                        --      instance <S> => C [a] where ...
                
-pprSourceTyCtxt (ClassSCCtxt c) = ptext SLIT("the super-classes of class") <+> quotes (ppr c)
-pprSourceTyCtxt SigmaCtxt       = ptext SLIT("the context of a polymorphic type")
-pprSourceTyCtxt (DataTyCtxt tc) = ptext SLIT("the context of the data type declaration for") <+> quotes (ppr tc)
-pprSourceTyCtxt InstThetaCtxt   = ptext SLIT("the context of an instance declaration")
-pprSourceTyCtxt TypeCtxt        = ptext SLIT("the context of a type")
+pprSourceTyCtxt :: SourceTyCtxt -> SDoc
+pprSourceTyCtxt (ClassSCCtxt c) = ptext (sLit "the super-classes of class") <+> quotes (ppr c)
+pprSourceTyCtxt SigmaCtxt       = ptext (sLit "the context of a polymorphic type")
+pprSourceTyCtxt (DataTyCtxt tc) = ptext (sLit "the context of the data type declaration for") <+> quotes (ppr tc)
+pprSourceTyCtxt InstThetaCtxt   = ptext (sLit "the context of an instance declaration")
+pprSourceTyCtxt TypeCtxt        = ptext (sLit "the context of a type")
 \end{code}
 
 \begin{code}
@@ -1251,7 +1272,8 @@ checkValidTheta ctxt theta
   = addErrCtxt (checkThetaCtxt ctxt theta) (check_valid_theta ctxt theta)
 
 -------------------------
-check_valid_theta ctxt []
+check_valid_theta :: SourceTyCtxt -> [PredType] -> TcM ()
+check_valid_theta _ []
   = return ()
 check_valid_theta ctxt theta = do
     dflags <- getDOpts
@@ -1267,7 +1289,7 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
        ; checkTc (arity == n_tys) arity_err
 
                -- Check the form of the argument types
-       ; mapM_ check_mono_type tys
+       ; mapM_ checkValidMonoType tys
        ; checkTc (check_class_pred_tys dflags ctxt tys)
                 (predTyVarErr pred $$ how_to_allow)
        }
@@ -1276,19 +1298,19 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
     arity      = classArity cls
     n_tys      = length tys
     arity_err  = arityErr "Class" class_name arity n_tys
-    how_to_allow = parens (ptext SLIT("Use -XFlexibleContexts to permit this"))
+    how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
 
-check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
+check_pred_ty dflags _ pred@(EqPred ty1 ty2)
   = do {       -- Equational constraints are valid in all contexts if type
                -- families are permitted
        ; checkTc (dopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
 
                -- Check the form of the argument types
-       ; check_mono_type ty1
-       ; check_mono_type ty2
+       ; checkValidMonoType ty1
+       ; checkValidMonoType ty2
        }
 
-check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty
+check_pred_ty _ SigmaCtxt (IParam _ ty) = checkValidMonoType ty
        -- Implicit parameters only allowed in type
        -- signatures; not in instance decls, superclasses etc
        -- The reason for not allowing implicit params in instances is a bit
@@ -1300,7 +1322,7 @@ check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_mono_type ty
        -- instance decl would show up two uses of ?x.
 
 -- Catch-all
-check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
+check_pred_ty _ _ sty = failWithTc (badPredTyErr sty)
 
 -------------------------
 check_class_pred_tys :: DynFlags -> SourceTyCtxt -> [Type] -> Bool
@@ -1310,12 +1332,13 @@ check_class_pred_tys dflags ctxt tys
        InstThetaCtxt -> flexible_contexts || undecidable_ok || all tcIsTyVarTy tys
                                -- Further checks on head and theta in
                                -- checkInstTermination
-       other         -> flexible_contexts || all tyvar_head tys
+       _             -> flexible_contexts || all tyvar_head tys
   where
     flexible_contexts = dopt Opt_FlexibleContexts dflags
     undecidable_ok = dopt Opt_UndecidableInstances dflags
 
 -------------------------
+tyvar_head :: Type -> Bool
 tyvar_head ty                  -- Haskell 98 allows predicates of form 
   | tcIsTyVarTy ty = True      --      C (a ty1 .. tyn)
   | otherwise                  -- where a is a type variable
@@ -1370,10 +1393,11 @@ checkAmbiguity forall_tyvars theta tau_tyvars
     ambig_var ct_var  = (ct_var `elem` forall_tyvars) &&
                        not (ct_var `elemVarSet` extended_tau_vars)
 
+ambigErr :: PredType -> SDoc
 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 '=>'"))]
+  = 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
@@ -1382,6 +1406,7 @@ in each constraint is in V.  So we disallow a type like
 even in a scope where b is in scope.
 
 \begin{code}
+checkFreeness :: [Var] -> [PredType] -> TcM ()
 checkFreeness forall_tyvars theta
   = do { flexible_contexts <- doptM Opt_FlexibleContexts
        ; unless flexible_contexts $ mapM_ complain (filter is_free theta) }
@@ -1391,50 +1416,57 @@ checkFreeness forall_tyvars theta
     bound_var ct_var = ct_var `elem` forall_tyvars
     complain pred    = addErrTc (freeErr pred)
 
+freeErr :: PredType -> SDoc
 freeErr pred
-  = sep [ ptext SLIT("All of the type variables in the constraint") <+> 
+  = sep [ ptext (sLit "All of the type variables in the constraint") <+> 
           quotes (pprPred pred)
-       , ptext SLIT("are already in scope") <+>
-          ptext SLIT("(at least one must be universally quantified here)")
+       , ptext (sLit "are already in scope") <+>
+          ptext (sLit "(at least one must be universally quantified here)")
        , nest 4 $
-            ptext SLIT("(Use -XFlexibleContexts to lift this restriction)")
+            ptext (sLit "(Use -XFlexibleContexts to lift this restriction)")
         ]
 \end{code}
 
 \begin{code}
+checkThetaCtxt :: SourceTyCtxt -> ThetaType -> SDoc
 checkThetaCtxt ctxt theta
-  = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
-         ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
+  = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
+         ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
 
-badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
-eqPredTyErr  sty = ptext SLIT("Illegal equational constraint") <+> pprPred sty
+badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
+badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
+eqPredTyErr  sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
                   $$
-                  parens (ptext SLIT("Use -XTypeFamilies to permit this"))
-predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
-                         nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
-dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
+                  parens (ptext (sLit "Use -XTypeFamilies to permit this"))
+predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
+                         nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
+dupPredWarn :: [[PredType]] -> SDoc
+dupPredWarn dups   = ptext (sLit "Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
 
+arityErr :: Outputable a => String -> a -> Int -> Int -> SDoc
 arityErr kind name n m
-  = hsep [ text kind, quotes (ppr name), ptext SLIT("should have"),
+  = hsep [ text kind, quotes (ppr name), ptext (sLit "should have"),
           n_arguments <> comma, text "but has been given", int m]
     where
-       n_arguments | n == 0 = ptext SLIT("no arguments")
-                   | n == 1 = ptext SLIT("1 argument")
-                   | True   = hsep [int n, ptext SLIT("arguments")]
+       n_arguments | n == 0 = ptext (sLit "no arguments")
+                   | n == 1 = ptext (sLit "1 argument")
+                   | True   = hsep [int n, ptext (sLit "arguments")]
 
 -----------------
+notMonoType :: TcType -> TcM a
 notMonoType ty
   = do { ty' <- zonkTcType ty
        ; env0 <- tcInitTidyEnv
        ; let (env1, tidy_ty) = tidyOpenType env0 ty'
-             msg = ptext SLIT("Cannot match a monotype with") <+> quotes (ppr tidy_ty)
+             msg = ptext (sLit "Cannot match a monotype with") <+> quotes (ppr tidy_ty)
        ; failWithTcM (env1, msg) }
 
+notMonoArgs :: TcType -> TcM a
 notMonoArgs ty
   = do { ty' <- zonkTcType ty
        ; env0 <- tcInitTidyEnv
        ; let (env1, tidy_ty) = tidyOpenType env0 ty'
-             msg = ptext SLIT("Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
+             msg = ptext (sLit "Arguments of type synonym families must be monotypes") <+> quotes (ppr tidy_ty)
        ; failWithTcM (env1, msg) }
 \end{code}
 
@@ -1467,28 +1499,32 @@ checkValidInstHead ty   -- Should be a source type
         Just (clas,tys) -> do
 
     dflags <- getDOpts
-    mapM_ check_mono_type tys
     check_inst_head dflags clas tys
     return (clas, tys)
     }}
 
+check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
 check_inst_head dflags clas tys
-       -- If GlasgowExts then check at least one isn't a type variable
-  = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
-                all tcInstHeadTyNotSynonym tys)
-               (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
-       checkTc (dopt Opt_FlexibleInstances dflags ||
-                all tcInstHeadTyAppAllTyVars tys)
-               (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
-       checkTc (dopt Opt_MultiParamTypeClasses dflags ||
-                isSingleton tys)
-               (instTypeErr (pprClassPred clas tys) head_one_type_msg)
-       mapM_ check_mono_type tys
+  = do { -- If GlasgowExts then check at least one isn't a type variable
+       ; checkTc (dopt Opt_TypeSynonymInstances dflags ||
+                  all tcInstHeadTyNotSynonym tys)
+                 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+       ; checkTc (dopt Opt_FlexibleInstances dflags ||
+                  all tcInstHeadTyAppAllTyVars tys)
+                 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+       ; checkTc (dopt Opt_MultiParamTypeClasses dflags ||
+                  isSingleton tys)
+                 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+         -- May not contain type family applications
+       ; mapM_ checkTyFamFreeness tys
+
+       ; mapM_ checkValidMonoType tys
        -- For now, I only allow tau-types (not polytypes) in 
        -- the head of an instance decl.  
        --      E.g.  instance C (forall a. a->a) is rejected
        -- One could imagine generalising that, but I'm not sure
        -- what all the consequences might be
+       }
 
   where
     head_type_synonym_msg = parens (
@@ -1506,8 +1542,9 @@ check_inst_head dflags clas tys
                 text "Only one type can be given in an instance head." $$
                 text "Use -XMultiParamTypeClasses if you want to allow more.")
 
+instTypeErr :: SDoc -> SDoc -> SDoc
 instTypeErr pp_ty msg
-  = sep [ptext SLIT("Illegal instance declaration for") <+> quotes pp_ty, 
+  = sep [ptext (sLit "Illegal instance declaration for") <+> quotes pp_ty, 
         nest 4 msg]
 \end{code}
 
@@ -1538,7 +1575,7 @@ checkValidInstance tyvars theta clas inst_tys
                  (instTypeErr (pprClassPred clas inst_tys) msg)
        }
   where
-    msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+    msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
                         undecidableMsg])
 \end{code}
 
@@ -1574,12 +1611,14 @@ checkInstTermination tys theta
       | otherwise
       = Nothing
 
+predUndecErr :: PredType -> SDoc -> SDoc
 predUndecErr pred msg = sep [msg,
-                       nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
+                       nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
 
-nomoreMsg = ptext SLIT("Variable occurs more often in a constraint than in the instance head")
-smallerMsg = ptext SLIT("Constraint is no smaller than the instance head")
-undecidableMsg = ptext SLIT("Use -fallow-undecidable-instances to permit this")
+nomoreMsg, smallerMsg, undecidableMsg :: SDoc
+nomoreMsg = ptext (sLit "Variable occurs more often in a constraint than in the instance head")
+smallerMsg = ptext (sLit "Constraint is no smaller than the instance head")
+undecidableMsg = ptext (sLit "Use -XUndecidableInstances to permit this")
 \end{code}
 
 
@@ -1619,7 +1658,7 @@ should have only type-variable constraints.
 
 Here is another example:
        data Fix f = In (f (Fix f)) deriving( Eq )
-Here, if we are prepared to allow -fallow-undecidable-instances we
+Here, if we are prepared to allow -XUndecidableInstances we
 could derive the instance
        instance Eq (f (Fix f)) => Eq (Fix f)
 but this is so delicate that I don't think it should happen inside
@@ -1643,9 +1682,9 @@ Allow constraints which consist only of type variables, with no repeats.
 
 \begin{code}
 validDerivPred :: PredType -> Bool
-validDerivPred (ClassP cls tys) = hasNoDups fvs && sizeTypes tys == length fvs
-                               where fvs = fvTypes tys
-validDerivPred otehr           = False
+validDerivPred (ClassP _ tys) = hasNoDups fvs && sizeTypes tys == length fvs
+                              where fvs = fvTypes tys
+validDerivPred _              = False
 \end{code}
 
 %************************************************************************
@@ -1656,7 +1695,7 @@ validDerivPred otehr              = False
 
 \begin{code}
 -- Check that a "type instance" is well-formed (which includes decidability
--- unless -fallow-undecidable-instances is given).
+-- unless -XUndecidableInstances is given).
 --
 checkValidTypeInst :: [Type] -> Type -> TcM ()
 checkValidTypeInst typats rhs
@@ -1665,8 +1704,7 @@ checkValidTypeInst typats rhs
        ; mapM_ checkTyFamFreeness typats
 
          -- the right-hand side is a tau type
-       ; checkTc (isTauTy rhs) $ 
-          polyTyErr rhs
+       ; checkValidMonoType rhs
 
          -- we have a decidable instance unless otherwise permitted
        ; undecidable_ok <- doptM Opt_UndecidableInstances
@@ -1704,7 +1742,7 @@ checkFamInst lhsTys famInsts
 checkTyFamFreeness :: Type -> TcM ()
 checkTyFamFreeness ty
   = checkTc (isTyFamFree ty) $
-      tyFamInstInIndexErr ty
+      tyFamInstIllegalErr ty
 
 -- Check that a type does not contain any type family applications.
 --
@@ -1713,23 +1751,22 @@ isTyFamFree = null . tyFamInsts
 
 -- Error messages
 
-tyFamInstInIndexErr ty
-  = hang (ptext SLIT("Illegal type family application in type instance") <> 
+tyFamInstIllegalErr :: Type -> SDoc
+tyFamInstIllegalErr ty
+  = hang (ptext (sLit "Illegal type synonym family application in instance") <> 
          colon) 4 $
       ppr ty
 
-polyTyErr ty 
-  = hang (ptext SLIT("Illegal polymorphic type in type instance") <> colon) 4 $
-      ppr ty
-
+famInstUndecErr :: Type -> SDoc -> SDoc
 famInstUndecErr ty msg 
   = sep [msg, 
-         nest 2 (ptext SLIT("in the type family application:") <+> 
+         nest 2 (ptext (sLit "in the type family application:") <+> 
                  pprType ty)]
 
-nestedMsg     = ptext SLIT("Nested type family application")
-nomoreVarMsg  = ptext SLIT("Variable occurs more often than in instance head")
-smallerAppMsg = ptext SLIT("Application is no smaller than the instance head")
+nestedMsg, nomoreVarMsg, smallerAppMsg :: SDoc
+nestedMsg     = ptext (sLit "Nested type family application")
+nomoreVarMsg  = ptext (sLit "Variable occurs more often than in instance head")
+smallerAppMsg = ptext (sLit "Application is no smaller than the instance head")
 \end{code}