X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=ghc%2Fcompiler%2FcoreSyn%2FCoreLint.lhs;h=52b330c730b08d0c12d7303850db19e8081b555b;hb=f714e6b642fd614a9971717045ae47c3d871275e;hp=f42a49e8567f5fd464b25eaf66ff9c2bdcda98db;hpb=e7d21ee4f8ac907665a7e170c71d59e13a01da09;p=ghc-hetmet.git

diff --git a/ghc/compiler/coreSyn/CoreLint.lhs b/ghc/compiler/coreSyn/CoreLint.lhs
index f42a49e..52b330c 100644
--- a/ghc/compiler/coreSyn/CoreLint.lhs
+++ b/ghc/compiler/coreSyn/CoreLint.lhs
@@ -1,406 +1,499 @@
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1993-1995
+% (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
 %
 \section[CoreLint]{A ``lint'' pass to check for Core correctness}
 
 \begin{code}
-#include "HsVersions.h"
-
 module CoreLint (
 	lintCoreBindings,
-	lintUnfolding,
-	
-	PprStyle, CoreBinding, PlainCoreBinding(..), Id
+	lintUnfolding, 
+	showPass, endPass
     ) where
 
-IMPORT_Trace
+#include "HsVersions.h"
+
+import CoreSyn
+import CoreFVs		( idFreeVars )
+import CoreUtils	( findDefault, exprOkForSpeculation, coreBindsSize, mkPiType )
 
-import AbsPrel		( typeOfPrimOp, mkFunTy, PrimOp(..), PrimKind
-			  IF_ATTACK_PRAGMAS(COMMA tagOf_PrimOp)
-			  IF_ATTACK_PRAGMAS(COMMA pprPrimOp)
-			)
-import AbsUniType
 import Bag
-import BasicLit		( typeOfBasicLit, BasicLit )
-import CoreSyn		( pprCoreBinding ) -- ToDo: correctly
-import Id		( getIdUniType, isNullaryDataCon, isBottomingId,
-			  getInstantiatedDataConSig, Id
-			  IF_ATTACK_PRAGMAS(COMMA bottomIsGuaranteed)
+import Literal		( literalType )
+import DataCon		( dataConRepType )
+import Var		( Var, Id, TyVar, idType, tyVarKind, isTyVar, isId, mustHaveLocalBinding )
+import VarSet
+import Subst		( substTyWith )
+import Name		( getSrcLoc )
+import PprCore
+import ErrUtils		( dumpIfSet_core, ghcExit, Message, showPass,
+			  mkLocMessage )
+import SrcLoc		( SrcLoc, noSrcLoc, mkSrcSpan )
+import Type		( Type, tyVarsOfType, eqType,
+			  splitFunTy_maybe, mkTyVarTy,
+			  splitForAllTy_maybe, splitTyConApp_maybe, splitTyConApp,
+			  isUnLiftedType, typeKind, 
+			  isUnboxedTupleType,
+			  isSubKind
 			)
-import Maybes
+import TyCon		( isPrimTyCon )
+import BasicTypes	( RecFlag(..), isNonRec )
+import CmdLineOpts
 import Outputable
-import PlainCore
-import Pretty
-import SrcLoc		( SrcLoc )
-import UniqSet
-import Util
 
-infixr 9 `thenL`, `thenL_`, `thenMaybeL`, `thenMaybeL_`
+#ifdef DEBUG
+import Util             ( notNull )
+#endif
+
+import Maybe
+import IO		( hPutStrLn, stderr )
+
+infixr 9 `thenL`, `seqL`
 \end{code}
 
-Checks for 
-	(a) type errors
-	(b) locally-defined variables used but not defined
+%************************************************************************
+%*									*
+\subsection{End pass}
+%*									*
+%************************************************************************
+
+@showPass@ and @endPass@ don't really belong here, but it makes a convenient
+place for them.  They print out stuff before and after core passes,
+and do Core Lint when necessary.
+
+\begin{code}
+endPass :: DynFlags -> String -> DynFlag -> [CoreBind] -> IO [CoreBind]
+endPass dflags pass_name dump_flag binds
+  = do 
+	-- Report result size if required
+	-- This has the side effect of forcing the intermediate to be evaluated
+	if verbosity dflags >= 2 then
+	   hPutStrLn stderr ("    Result size = " ++ show (coreBindsSize binds))
+	 else
+	   return ()
+
+	-- Report verbosely, if required
+	dumpIfSet_core dflags dump_flag pass_name (pprCoreBindings binds)
+
+	-- Type check
+	lintCoreBindings dflags pass_name binds
+
+	return binds
+\end{code}
 
-Doesn't check for out-of-scope type variables, because they can
-legitimately arise.  Eg
-\begin{verbatim}
-	k = /\a b -> \x::a y::b -> x
-	f = /\c -> \z::c -> k c w z (error w "foo")
-\end{verbatim}
-Here \tr{w} is just a free type variable.
 
 %************************************************************************
 %*									*
-\subsection{``lint'' for various constructs}
+\subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
 %*									*
 %************************************************************************
 
-@lintCoreBindings@ is the top-level interface function.
+Checks that a set of core bindings is well-formed.  The PprStyle and String
+just control what we print in the event of an error.  The Bool value
+indicates whether we have done any specialisation yet (in which case we do
+some extra checks).
+
+We check for
+	(a) type errors
+	(b) Out-of-scope type variables
+	(c) Out-of-scope local variables
+	(d) Ill-kinded types
+
+If we have done specialisation the we check that there are
+	(a) No top-level bindings of primitive (unboxed type)
+
+Outstanding issues:
+
+    --
+    -- Things are *not* OK if:
+    --
+    -- * Unsaturated type app before specialisation has been done;
+    --
+    -- * Oversaturated type app after specialisation (eta reduction
+    --   may well be happening...);
 
 \begin{code}
-lintCoreBindings :: PprStyle -> String -> Bool -> [PlainCoreBinding] -> [PlainCoreBinding]
-
-lintCoreBindings sty whodunnit spec_done binds
-  = BSCC("CoreLint")
-    case (initL (lint_binds binds) spec_done) of
-      Nothing  -> binds
-      Just msg -> pprPanic "" (ppAboves [
-			ppStr ("*** Core Lint Errors: in "++whodunnit++" ***"),
-			msg sty,
-			ppStr "*** Offending Program ***",
-			ppAboves (map (pprCoreBinding sty pprBigCoreBinder pprTypedCoreBinder ppr) binds),
-			ppStr "*** End of Offense ***"])
-    ESCC
+lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
+
+lintCoreBindings dflags whoDunnit binds
+  | not (dopt Opt_DoCoreLinting dflags)
+  = return ()
+
+lintCoreBindings dflags whoDunnit binds
+  = case (initL (lint_binds binds)) of
+      Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
+      Just bad_news -> printDump (display bad_news)	>>
+		       ghcExit 1
   where
-    lint_binds :: [PlainCoreBinding] -> LintM ()
-
-    lint_binds [] = returnL ()
-    lint_binds (bind:binds) 
-      = lintCoreBinds bind 		`thenL` \ binders ->
-	addInScopeVars binders (
-	    lint_binds binds
-	)
+	-- Put all the top-level binders in scope at the start
+	-- This is because transformation rules can bring something
+	-- into use 'unexpectedly'
+    lint_binds binds = addInScopeVars (bindersOfBinds binds) $
+		       mapL lint_bind binds
+
+    lint_bind (Rec prs)		= mapL (lintSingleBinding Recursive) prs	`seqL`
+				  returnL ()
+    lint_bind (NonRec bndr rhs) = lintSingleBinding NonRecursive (bndr,rhs)
+
+    display bad_news
+      = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
+		bad_news,
+		ptext SLIT("*** Offending Program ***"),
+		pprCoreBindings binds,
+		ptext SLIT("*** End of Offense ***")
+	]
 \end{code}
 
+%************************************************************************
+%*									*
+\subsection[lintUnfolding]{lintUnfolding}
+%*									*
+%************************************************************************
+
 We use this to check all unfoldings that come in from interfaces
 (it is very painful to catch errors otherwise):
+
 \begin{code}
-lintUnfolding :: SrcLoc -> PlainCoreExpr -> PlainCoreExpr
-
-lintUnfolding locn expr
-  = case (initL (addLoc (ImportedUnfolding locn) (lintCoreExpr expr)) True{-pretend spec done-}) of
-      Nothing  -> expr
-      Just msg -> error ("ERROR: Type-incorrect unfolding from an interface:\n"++
-			(ppShow 80 (ppAboves [msg PprForUser,
-					ppStr "*** Bad unfolding ***",
-					ppr PprDebug expr,
-					ppStr "*** End of bad unfolding ***"]))) 
+lintUnfolding :: SrcLoc
+	      -> [Var]		-- Treat these as in scope
+	      -> CoreExpr
+	      -> Maybe Message	-- Nothing => OK
+
+lintUnfolding locn vars expr
+  = initL (addLoc (ImportedUnfolding locn) $
+	   addInScopeVars vars	           $
+	   lintCoreExpr expr)
 \end{code}
 
-\begin{code}
-lintCoreAtom :: PlainCoreAtom -> LintM (Maybe UniType)
+%************************************************************************
+%*									*
+\subsection[lintCoreBinding]{lintCoreBinding}
+%*									*
+%************************************************************************
 
-lintCoreAtom (CoLitAtom lit)       = returnL (Just (typeOfBasicLit lit))
-lintCoreAtom a@(CoVarAtom v)
-  = checkInScope v	`thenL_`
-    returnL (Just (getIdUniType v))
-\end{code}
+Check a core binding, returning the list of variables bound.
 
 \begin{code}
-lintCoreBinds :: PlainCoreBinding -> LintM [Id]		-- Returns the binders
-lintCoreBinds (CoNonRec binder rhs)
-  = lint_binds_help (binder,rhs) 	`thenL_`
-    returnL [binder]
-
-lintCoreBinds (CoRec pairs) 
-  = addInScopeVars binders (
-	mapL lint_binds_help pairs `thenL_`
-	returnL binders
-    )
-  where
-    binders = [b | (b,_) <- pairs]
+lintSingleBinding rec_flag (binder,rhs)
+  = addLoc (RhsOf binder) $
 
-lint_binds_help (binder,rhs)
-  = addLoc (RhsOf binder) (
 	-- Check the rhs
-	lintCoreExpr rhs    	`thenL` \ maybe_rhs_ty ->
+    lintCoreExpr rhs				`thenL` \ ty ->
 
 	-- Check match to RHS type
-	(case maybe_rhs_ty of
-	  Nothing     -> returnL ()
-	  Just rhs_ty -> checkTys (getIdUniType binder) 
-				   rhs_ty 
-				   (mkRhsMsg binder rhs_ty)
-	)			`thenL_` 
-
-	-- Check not isPrimType
-	checkL (not (isPrimType (getIdUniType binder)))
-	       (mkRhsPrimMsg binder rhs)
-				`thenL_`
-
-	-- Check unfolding, if any
-	-- Blegh. This is tricky, because the unfolding is a SimplifiableCoreExpr
-	-- Give up for now
-
-	returnL ()
-    )
+    lintBinder binder				`seqL`
+    checkTys binder_ty ty (mkRhsMsg binder ty)	`seqL`
+
+	-- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
+    checkL (not (isUnLiftedType binder_ty)
+            || (isNonRec rec_flag && exprOkForSpeculation rhs))
+ 	   (mkRhsPrimMsg binder rhs)		`seqL`
+
+        -- Check whether binder's specialisations contain any out-of-scope variables
+    mapL (checkBndrIdInScope binder) bndr_vars	`seqL`
+    returnL ()
+	  
+	-- We should check the unfolding, if any, but this is tricky because
+	-- the unfolding is a SimplifiableCoreExpr. Give up for now.
+  where
+    binder_ty = idType binder
+    bndr_vars = varSetElems (idFreeVars binder)
 \end{code}
 
+%************************************************************************
+%*									*
+\subsection[lintCoreExpr]{lintCoreExpr}
+%*									*
+%************************************************************************
+
 \begin{code}
-lintCoreExpr :: PlainCoreExpr -> LintM (Maybe UniType)	-- Nothing if error found
-
-lintCoreExpr (CoVar var)
-  = checkInScope var	`thenL_`
-    returnL (Just ty)
-{-
-    case (splitForalls ty) of { (tyvars, _) ->
-    if null tyvars then
-	returnL (Just ty)
-    else
-	addErrL (mkUnappTyMsg var ty)	`thenL_`
-	returnL Nothing
-    }
--}
+lintCoreExpr :: CoreExpr -> LintM Type
+
+lintCoreExpr (Var var) = checkIdInScope var `seqL` returnL (idType var)
+lintCoreExpr (Lit lit) = returnL (literalType lit)
+
+lintCoreExpr (Note (Coerce to_ty from_ty) expr)
+  = lintCoreExpr expr 	`thenL` \ expr_ty ->
+    lintTy to_ty	`seqL`
+    lintTy from_ty	`seqL`
+    checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)	`seqL`
+    returnL to_ty
+
+lintCoreExpr (Note other_note expr)
+  = lintCoreExpr expr
+
+lintCoreExpr (Let (NonRec bndr rhs) body)
+  = lintSingleBinding NonRecursive (bndr,rhs)	`seqL`
+    addLoc (BodyOfLetRec [bndr])
+	   (addInScopeVars [bndr] (lintCoreExpr body))
+
+lintCoreExpr (Let (Rec pairs) body)
+  = addInScopeVars bndrs	$
+    mapL (lintSingleBinding Recursive) pairs	`seqL`
+    addLoc (BodyOfLetRec bndrs) (lintCoreExpr body)
   where
-    ty = getIdUniType var
+    bndrs = map fst pairs
+
+lintCoreExpr e@(App fun arg)
+  = lintCoreExpr fun 	`thenL` \ ty ->
+    addLoc (AnExpr e)	$
+    lintCoreArg ty arg
+
+lintCoreExpr (Lam var expr)
+  = addLoc (LambdaBodyOf var)	$
+    (if isId var then    
+       checkL (not (isUnboxedTupleType (idType var))) (mkUnboxedTupleMsg var)
+     else
+       returnL ())
+				`seqL`
+    (addInScopeVars [var]	$
+     lintCoreExpr expr		`thenL` \ ty ->
+
+     returnL (mkPiType var ty))
+
+lintCoreExpr e@(Case scrut var alts)
+ = 	-- Check the scrutinee
+   lintCoreExpr scrut			`thenL` \ scrut_ty ->
+
+	-- Check the binder
+   lintBinder var						`seqL`
+
+    	-- If this is an unboxed tuple case, then the binder must be dead
+   {-
+   checkL (if isUnboxedTupleType (idType var) 
+		then isDeadBinder var 
+		else True) (mkUnboxedTupleMsg var)		`seqL`
+   -}
+		
+   checkTys (idType var) scrut_ty (mkScrutMsg var scrut_ty)	`seqL`
+
+   addInScopeVars [var]				(
+
+	-- Check the alternatives
+   checkCaseAlts e scrut_ty alts		`seqL`
+
+   mapL (lintCoreAlt scrut_ty) alts		`thenL` \ (alt_ty : alt_tys) ->
+   mapL (check alt_ty) alt_tys			`seqL`
+   returnL alt_ty)
+ where
+   check alt_ty1 alt_ty2 = checkTys alt_ty1 alt_ty2 (mkCaseAltMsg e)
+
+lintCoreExpr e@(Type ty)
+  = addErrL (mkStrangeTyMsg e)
+\end{code}
 
-lintCoreExpr (CoLit lit)	= returnL (Just (typeOfBasicLit lit))
-lintCoreExpr (CoSCC label expr)	= lintCoreExpr expr
+%************************************************************************
+%*									*
+\subsection[lintCoreArgs]{lintCoreArgs}
+%*									*
+%************************************************************************
 
-lintCoreExpr (CoLet binds body)	
-  = lintCoreBinds binds		`thenL` \ binders ->
-    ASSERT(not (null binders))
-    addLoc (BodyOfLetRec binders) (
-    addInScopeVars binders (
-	lintCoreExpr body
-    ))
+The basic version of these functions checks that the argument is a
+subtype of the required type, as one would expect.
 
-lintCoreExpr e@(CoCon con tys args)
-  = checkTyApp con_ty tys (mkTyAppMsg e)    `thenMaybeL` \ con_tau_ty ->
-    -- Note: no call to checkSpecTyApp;
-    -- we allow CoCons applied to unboxed types to sail through
-    mapMaybeL lintCoreAtom args			    `thenL` \ maybe_arg_tys ->
-    case maybe_arg_tys of
-      Nothing 	    -> returnL Nothing
-      Just arg_tys  -> checkFunApp con_tau_ty arg_tys (mkFunAppMsg con_tau_ty arg_tys e)
-  where
-    con_ty = getIdUniType con
-
-lintCoreExpr e@(CoPrim op tys args)
-  = checkTyApp op_ty tys (mkTyAppMsg e)		`thenMaybeL` \ op_tau_ty ->
-    -- checkSpecTyApp e tys (mkSpecTyAppMsg e)	`thenMaybeL_`
-    mapMaybeL lintCoreAtom args			`thenL` \ maybe_arg_tys ->
-    case maybe_arg_tys of
-      Nothing -> returnL Nothing
-      Just arg_tys -> checkFunApp op_tau_ty arg_tys (mkFunAppMsg op_tau_ty arg_tys e)
-  where
-    op_ty = typeOfPrimOp op
+\begin{code}
+lintCoreArgs :: Type -> [CoreArg] -> LintM Type
+lintCoreArgs = lintCoreArgs0 checkTys
 
-lintCoreExpr e@(CoApp fun arg)
-  = lce e []
-  where
-    lce (CoApp fun arg) arg_tys = lintCoreAtom arg	`thenMaybeL` \ arg_ty ->
-			          lce fun (arg_ty:arg_tys)
+lintCoreArg :: Type -> CoreArg -> LintM Type
+lintCoreArg = lintCoreArg0 checkTys
+\end{code}
 
-    lce other_fun arg_tys = lintCoreExpr other_fun	`thenMaybeL` \ fun_ty ->
-			    checkFunApp fun_ty arg_tys (mkFunAppMsg fun_ty arg_tys e)
+The primitive version of these functions takes a check argument,
+allowing a different comparison.
 
-lintCoreExpr e@(CoTyApp fun ty_arg)
-  = lce e []
-  where
-    lce (CoTyApp fun ty_arg) ty_args = lce fun (ty_arg:ty_args)
-
-    lce other_fun ty_args = lintCoreExpr other_fun	`thenMaybeL` \ fun_ty ->
-			    checkTyApp fun_ty ty_args (mkTyAppMsg e)
-							`thenMaybeL` \ res_ty ->
-			    checkSpecTyApp other_fun ty_args (mkSpecTyAppMsg e)
-							`thenMaybeL_`
-			    returnL (Just res_ty)
-
-lintCoreExpr (CoLam binders expr)
-  = ASSERT (not (null binders))
-    addLoc (LambdaBodyOf binders) (
-    addInScopeVars binders (
-	lintCoreExpr expr   `thenMaybeL` \ body_ty ->
-	returnL (Just (foldr (mkFunTy . getIdUniType) body_ty binders))
-    ))
+\begin{code}
+lintCoreArgs0 check_tys ty [] = returnL ty
+lintCoreArgs0 check_tys ty (a : args)
+  = lintCoreArg0  check_tys ty a	`thenL` \ res ->
+    lintCoreArgs0 check_tys res args
+
+lintCoreArg0 check_tys ty a@(Type arg_ty)
+  = lintTy arg_ty			`seqL`
+    lintTyApp ty arg_ty
+
+lintCoreArg0 check_tys fun_ty arg
+  = -- Make sure function type matches argument
+    lintCoreExpr arg		`thenL` \ arg_ty ->
+    let
+      err = mkAppMsg fun_ty arg_ty
+    in
+    case splitFunTy_maybe fun_ty of
+      Just (arg,res) -> check_tys arg arg_ty err `seqL`
+                        returnL res
+      _              -> addErrL err
+\end{code}
 
-lintCoreExpr (CoTyLam tyvar expr)
-  = lintCoreExpr expr		`thenMaybeL` \ body_ty ->
-    case quantifyTy [tyvar] body_ty of
-      (_, ty) -> returnL (Just ty) -- not worried about the TyVarTemplates that come back
-
-lintCoreExpr e@(CoCase scrut alts)
- = lintCoreExpr scrut		`thenMaybeL` \ scrut_ty ->
-
-	-- Check that it is a data type
-   case getUniDataTyCon_maybe scrut_ty of
-	Nothing -> addErrL (mkCaseDataConMsg e)	`thenL_`
-		   returnL Nothing
-	Just (tycon, _, _)
-		-> lintCoreAlts alts scrut_ty tycon
-
-lintCoreAlts :: PlainCoreCaseAlternatives
-	     -> UniType 		-- Type of scrutinee
-	     -> TyCon			-- TyCon pinned on the case
-	     -> LintM (Maybe UniType)	-- Type of alternatives
-
-lintCoreAlts alts scrut_ty case_tycon
-  = (case alts of
-	 CoAlgAlts alg_alts deflt ->  
-	   chk_prim_type False case_tycon	`thenL_`
-	   chk_non_abstract_type case_tycon	`thenL_`
-	   mapL (lintAlgAlt scrut_ty) alg_alts 	`thenL` \ maybe_alt_tys ->
-	   lintDeflt deflt scrut_ty		`thenL` \ maybe_deflt_ty ->
-	   returnL (maybe_deflt_ty : maybe_alt_tys)
-
-	 CoPrimAlts prim_alts deflt -> 
-	   chk_prim_type True case_tycon	 `thenL_`
-	   mapL (lintPrimAlt scrut_ty) prim_alts `thenL` \ maybe_alt_tys ->
-	   lintDeflt deflt scrut_ty		 `thenL` \ maybe_deflt_ty ->
-	   returnL (maybe_deflt_ty : maybe_alt_tys)
-    )						 `thenL` \ maybe_result_tys ->
-	 -- Check the result types
-    case catMaybes (maybe_result_tys) of
-      []	     -> returnL Nothing
-
-      (first_ty:tys) -> mapL check tys	`thenL_`
-			returnL (Just first_ty)
-	where
-	  check ty = checkTys first_ty ty (mkCaseAltMsg alts)
-  where
-    chk_prim_type prim_required tycon
-      = if (isPrimTyCon tycon == prim_required) then
-	    returnL ()
+\begin{code}
+lintTyApp ty arg_ty 
+  = case splitForAllTy_maybe ty of
+      Nothing -> addErrL (mkTyAppMsg ty arg_ty)
+
+      Just (tyvar,body) ->
+        if not (isTyVar tyvar) then addErrL (mkTyAppMsg ty arg_ty) else
+	let
+	    tyvar_kind = tyVarKind tyvar
+	    argty_kind = typeKind arg_ty
+	in
+	if argty_kind `isSubKind` tyvar_kind
+		-- Arg type might be boxed for a function with an uncommitted
+		-- tyvar; notably this is used so that we can give
+		-- 	error :: forall a:*. String -> a
+		-- and then apply it to both boxed and unboxed types.
+	 then
+	    returnL (substTyWith [tyvar] [arg_ty] body)
 	else
-	    addErrL (mkCasePrimMsg prim_required tycon)
-
-    chk_non_abstract_type tycon
-      = case (getTyConFamilySize tycon) of
-	  Nothing -> addErrL (mkCaseAbstractMsg tycon)
-	  Just  _ -> returnL ()
-
-
-lintAlgAlt scrut_ty (con,args,rhs)
-  = (case getUniDataTyCon_maybe scrut_ty of
-      Nothing -> 
-	 addErrL (mkAlgAltMsg1 scrut_ty)
-      Just (tycon, tys_applied, cons) ->
-	 let
-	   (_, arg_tys, _) = getInstantiatedDataConSig con tys_applied
-	 in
-	 checkL (con `elem` cons) (mkAlgAltMsg2 scrut_ty con) `thenL_`
-	 checkL (length arg_tys == length args) (mkAlgAltMsg3 con args)	
-								 `thenL_`
-	 mapL check (arg_tys `zipEqual` args)			 `thenL_`
-	 returnL ()
-    )								 `thenL_`
-    addInScopeVars args 	(
-	 lintCoreExpr rhs
-    )
-  where
-    check (ty, arg) = checkTys ty (getIdUniType arg) (mkAlgAltMsg4 ty arg)
-
-    -- elem: yes, the elem-list here can sometimes be long-ish,
-    -- but as it's use-once, probably not worth doing anything different
-    -- We give it its own copy, so it isn't overloaded.
-    elem _ []	    = False
-    elem x (y:ys)   = x==y || elem x ys
-
-lintPrimAlt scrut_ty alt@(lit,rhs)
- = checkTys (typeOfBasicLit lit) scrut_ty (mkPrimAltMsg alt)	`thenL_`
-   lintCoreExpr rhs
-   
-lintDeflt CoNoDefault scrut_ty = returnL Nothing
-lintDeflt deflt@(CoBindDefault binder rhs) scrut_ty 
-  = checkTys (getIdUniType binder) scrut_ty (mkDefltMsg deflt)	`thenL_`
-    addInScopeVars [binder] (
-	lintCoreExpr rhs
-    )
+	    addErrL (mkKindErrMsg tyvar arg_ty)
+
+lintTyApps fun_ty []
+  = returnL fun_ty
+
+lintTyApps fun_ty (arg_ty : arg_tys)
+  = lintTyApp fun_ty arg_ty		`thenL` \ fun_ty' ->
+    lintTyApps fun_ty' arg_tys
 \end{code}
 
 
+
 %************************************************************************
 %*									*
-\subsection[lint-monad]{The Lint monad}
+\subsection[lintCoreAlts]{lintCoreAlts}
 %*									*
 %************************************************************************
 
 \begin{code}
-type LintM a = Bool		-- True <=> specialisation has been done
-	    -> [LintLocInfo] 	-- Locations
-	    -> UniqSet Id	-- Local vars in scope
-	    -> Bag ErrMsg	-- Error messages so far
-	    -> (a, Bag ErrMsg)	-- Result and error messages (if any)
+checkCaseAlts :: CoreExpr -> Type -> [CoreAlt] -> LintM ()
+-- a) Check that the alts are non-empty
+-- b) Check that the DEFAULT comes first, if it exists
+-- c) Check that there's a default for infinite types
+-- NB: Algebraic cases are not necessarily exhaustive, because
+--     the simplifer correctly eliminates case that can't 
+--     possibly match.
+
+checkCaseAlts e ty [] 
+  = addErrL (mkNullAltsMsg e)
+
+checkCaseAlts e ty alts
+  = checkL (all non_deflt con_alts) (mkNonDefltMsg e)	`seqL`
+    checkL (isJust maybe_deflt || not is_infinite_ty)
+	   (nonExhaustiveAltsMsg e)
+  where
+    (con_alts, maybe_deflt) = findDefault alts
 
-type ErrMsg = PprStyle -> Pretty
+    non_deflt (DEFAULT, _, _) = False
+    non_deflt alt	      = True
 
-data LintLocInfo
-  = RhsOf Id		-- The variable bound
-  | LambdaBodyOf [Id]	-- The lambda-binder
-  | BodyOfLetRec [Id]	-- One of the binders
-  | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
+    is_infinite_ty = case splitTyConApp_maybe ty of
+			Nothing			    -> False
+			Just (tycon, tycon_arg_tys) -> isPrimTyCon tycon
+\end{code}
+
+\begin{code}
+lintCoreAlt :: Type  			-- Type of scrutinee
+	    -> CoreAlt
+	    -> LintM Type		-- Type of alternatives
+
+lintCoreAlt scrut_ty alt@(DEFAULT, args, rhs)
+  = checkL (null args) (mkDefaultArgsMsg args)	`seqL`
+    lintCoreExpr rhs
+
+lintCoreAlt scrut_ty alt@(LitAlt lit, args, rhs)
+  = checkL (null args) (mkDefaultArgsMsg args)	`seqL`
+    checkTys lit_ty scrut_ty
+	     (mkBadPatMsg lit_ty scrut_ty)	`seqL`
+    lintCoreExpr rhs
+  where
+    lit_ty = literalType lit
 
-instance Outputable LintLocInfo where
-    ppr sty (RhsOf v)
-      = ppBesides [ppr sty (getSrcLoc v), ppStr ": [RHS of ", pp_binders sty [v], ppStr "]"]
+lintCoreAlt scrut_ty alt@(DataAlt con, args, rhs)
+  = addLoc (CaseAlt alt) (
 
-    ppr sty (LambdaBodyOf bs)
-      = ppBesides [ppr sty (getSrcLoc (head bs)),
-		ppStr ": [in body of lambda with binders ", pp_binders sty bs, ppStr "]"]
+    mapL (\arg -> checkL (not (isId arg && isUnboxedTupleType (idType arg)))
+			 (mkUnboxedTupleMsg arg)) args `seqL`
 
-    ppr sty (BodyOfLetRec bs)
-      = ppBesides [ppr sty (getSrcLoc (head bs)),
-		ppStr ": [in body of letrec with binders ", pp_binders sty bs, ppStr "]"]
+    addInScopeVars args (
 
-    ppr sty (ImportedUnfolding locn)
-      = ppBeside (ppr sty locn) (ppStr ": [in an imported unfolding]")
+	-- Check the pattern
+	-- Scrutinee type must be a tycon applicn; checked by caller
+	-- This code is remarkably compact considering what it does!
+	-- NB: args must be in scope here so that the lintCoreArgs line works.
+	-- NB: relies on existential type args coming *after* ordinary type args
+    case splitTyConApp scrut_ty of { (tycon, tycon_arg_tys) ->
+	lintTyApps (dataConRepType con) tycon_arg_tys	`thenL` \ con_type ->
+	lintCoreArgs con_type (map mk_arg args)		`thenL` \ con_result_ty ->
+	checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty)
+    }						`seqL`
 
-pp_binders :: PprStyle -> [Id] -> Pretty
-pp_binders sty bs
-  = ppInterleave ppComma (map pp_binder bs)
+	-- Check the RHS
+    lintCoreExpr rhs
+    ))
   where
-    pp_binder b
-      = ppCat [ppr sty b, ppStr "::", ppr sty (getIdUniType b)]
+    mk_arg b | isTyVar b = Type (mkTyVarTy b)
+	     | isId    b = Var b
+             | otherwise = pprPanic "lintCoreAlt:mk_arg " (ppr b)
 \end{code}
 
+%************************************************************************
+%*									*
+\subsection[lint-types]{Types}
+%*									*
+%************************************************************************
+
 \begin{code}
-initL :: LintM a -> Bool -> Maybe ErrMsg
-initL m spec_done
-  = case (m spec_done [] emptyUniqSet emptyBag) of { (_, errs) ->
-    if isEmptyBag errs then
-	Nothing
-    else
-	Just ( \ sty ->
-	  ppAboves [ msg sty | msg <- bagToList errs ]
-	)
-    }
+lintBinder :: Var -> LintM ()
+lintBinder v = nopL
+-- ToDo: lint its type
+-- ToDo: lint its rules
+
+lintTy :: Type -> LintM ()
+lintTy ty = mapL checkIdInScope (varSetElems (tyVarsOfType ty))	`seqL`
+	    returnL ()
+	-- ToDo: check the kind structure of the type
+\end{code}
+
+    
+%************************************************************************
+%*									*
+\subsection[lint-monad]{The Lint monad}
+%*									*
+%************************************************************************
+
+\begin{code}
+type LintM a = [LintLocInfo] 	-- Locations
+	    -> IdSet		-- Local vars in scope
+	    -> Bag Message	-- Error messages so far
+	    -> (Maybe a, Bag Message)  -- Result and error messages (if any)
+
+data LintLocInfo
+  = RhsOf Id		-- The variable bound
+  | LambdaBodyOf Id	-- The lambda-binder
+  | BodyOfLetRec [Id]	-- One of the binders
+  | CaseAlt CoreAlt	-- Pattern of a case alternative
+  | AnExpr CoreExpr	-- Some expression
+  | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
+\end{code}
+
+\begin{code}
+initL :: LintM a -> Maybe Message {- errors -}
+initL m
+  = case m [] emptyVarSet emptyBag of
+      (_, errs) | isEmptyBag errs -> Nothing
+		| otherwise	  -> Just (vcat (punctuate (text "") (bagToList errs)))
 
 returnL :: a -> LintM a
-returnL r spec loc scope errs = (r, errs)
+returnL r loc scope errs = (Just r, errs)
+
+nopL :: LintM a
+nopL loc scope errs = (Nothing, errs)
 
 thenL :: LintM a -> (a -> LintM b) -> LintM b
-thenL m k spec loc scope errs
-  = case m spec loc scope errs of 
-      (r, errs') -> k r spec loc scope errs'
-
-thenL_ :: LintM a -> LintM b -> LintM b
-thenL_ m k spec loc scope errs
-  = case m spec loc scope errs of 
-      (_, errs') -> k spec loc scope errs'
-
-thenMaybeL :: LintM (Maybe a) -> (a -> LintM (Maybe b)) -> LintM (Maybe b)
-thenMaybeL m k spec loc scope errs
-  = case m spec loc scope errs of
-      (Nothing, errs2) -> (Nothing, errs2)
-      (Just r,  errs2) -> k r spec loc scope errs2
-
-thenMaybeL_ :: LintM (Maybe a) -> LintM (Maybe b) -> LintM (Maybe b)
-thenMaybeL_ m k spec loc scope errs
-  = case m spec loc scope errs of
-      (Nothing, errs2) -> (Nothing, errs2)
-      (Just _,  errs2) -> k spec loc scope errs2
+thenL m k loc scope errs
+  = case m loc scope errs of
+      (Just r, errs')  -> k r loc scope errs'
+      (Nothing, errs') -> (Nothing, errs')
+
+seqL :: LintM a -> LintM b -> LintM b
+seqL m k loc scope errs
+  = case m loc scope errs of
+      (_, errs') -> k loc scope errs'
 
 mapL :: (a -> LintM b) -> [a] -> LintM [b]
 mapL f [] = returnL []
@@ -408,244 +501,193 @@ mapL f (x:xs)
   = f x 	`thenL` \ r ->
     mapL f xs	`thenL` \ rs ->
     returnL (r:rs)
-
-mapMaybeL :: (a -> LintM (Maybe b)) -> [a] -> LintM (Maybe [b])
-	-- Returns Nothing if anything fails
-mapMaybeL f [] = returnL (Just [])
-mapMaybeL f (x:xs)
-  = f x	    	    `thenMaybeL` \ r ->
-    mapMaybeL f xs  `thenMaybeL` \ rs ->
-    returnL (Just (r:rs))
 \end{code}
 
 \begin{code}
-checkL :: Bool -> ErrMsg -> LintM ()
-checkL True  msg spec loc scope errs = ((), errs)
-checkL False msg spec loc scope errs = ((), addErr errs msg loc)
-
-addErrL :: ErrMsg -> LintM ()
-addErrL msg spec loc scope errs = ((), addErr errs msg loc)
+checkL :: Bool -> Message -> LintM ()
+checkL True  msg = nopL
+checkL False msg = addErrL msg
 
-addErr :: Bag ErrMsg -> ErrMsg -> [LintLocInfo] -> Bag ErrMsg
+addErrL :: Message -> LintM a
+addErrL msg loc scope errs = (Nothing, addErr errs msg loc)
 
+addErr :: Bag Message -> Message -> [LintLocInfo] -> Bag Message
 addErr errs_so_far msg locs
-  = ASSERT (not (null locs))
-    errs_so_far `snocBag` ( \ sty ->
-    ppHang (ppr sty (head locs)) 4 (msg sty)
-    )
+  = ASSERT( notNull locs )
+    errs_so_far `snocBag` mk_msg msg
+  where
+   (loc, cxt1) = dumpLoc (head locs)
+   cxts        = [snd (dumpLoc loc) | loc <- locs]   
+   context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1
+	       | otherwise	    = cxt1
+ 
+   mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 
 addLoc :: LintLocInfo -> LintM a -> LintM a
-addLoc extra_loc m spec loc scope errs
-  = m spec (extra_loc:loc) scope errs
-
-addInScopeVars :: [Id] -> LintM a -> LintM a
-addInScopeVars ids m spec loc scope errs
-  = -- We check if these "new" ids are already
-    -- in scope, i.e., we have *shadowing* going on.
-    -- For now, it's just a "trace"; we may make
-    -- a real error out of it...
-    let
-	new_set = mkUniqSet ids
+addLoc extra_loc m loc scope errs
+  = m (extra_loc:loc) scope errs
 
-	shadowed = scope `intersectUniqSets` new_set
-    in
---  After adding -fliberate-case, Simon decided he likes shadowed
---  names after all.  WDP 94/07
---  (if isEmptyUniqSet shadowed
---  then id
---  else pprTrace "Shadowed vars:" (ppr PprDebug (uniqSetToList shadowed))) (
-    m spec loc (scope `unionUniqSets` new_set) errs
---  )
+addInScopeVars :: [Var] -> LintM a -> LintM a
+addInScopeVars ids m loc scope errs
+  = m loc (extendVarSetList scope ids) errs
 \end{code}
 
 \begin{code}
-checkTyApp :: UniType
-	   -> [UniType]
-	   -> ErrMsg
-	   -> LintM (Maybe UniType)
-
-checkTyApp forall_ty ty_args msg spec_done loc scope errs
-  = if (not spec_done && n_ty_args /= n_tyvars)
-    || (spec_done     && n_ty_args  > n_tyvars)
-    --
-    -- Things are *not* OK if:
-    --
-    -- * Unsaturated type app before specialisation has been done;
-    --
-    -- * Oversaturated type app after specialisation (eta reduction
-    --   may well be happening...);
-    --
-    -- Note: checkTyApp is usually followed by a call to checkSpecTyApp.
-    --
-    then (Nothing,     addErr errs msg loc)
-    else (Just res_ty, errs)
-  where
-    (tyvars, rho_ty) = splitForalls forall_ty
-    n_tyvars = length tyvars
-    n_ty_args = length ty_args
-    leftover_tyvars = drop n_ty_args tyvars
-    inst_env = tyvars `zip` ty_args
-    res_ty = mkForallTy leftover_tyvars (instantiateTy inst_env rho_ty)
+checkIdInScope :: Var -> LintM ()
+checkIdInScope id 
+  = checkInScope (ptext SLIT("is out of scope")) id
+
+checkBndrIdInScope :: Var -> Var -> LintM ()
+checkBndrIdInScope binder id 
+  = checkInScope msg id
+    where
+     msg = ptext SLIT("is out of scope inside info for") <+> 
+	   ppr binder
+
+checkInScope :: SDoc -> Var -> LintM ()
+checkInScope loc_msg var loc scope errs
+  |  mustHaveLocalBinding var && not (var `elemVarSet` scope)
+  = (Nothing, addErr errs (hsep [ppr var, loc_msg]) loc)
+  | otherwise
+  = nopL loc scope errs
+
+checkTys :: Type -> Type -> Message -> LintM ()
+-- check ty2 is subtype of ty1 (ie, has same structure but usage
+-- annotations need only be consistent, not equal)
+checkTys ty1 ty2 msg
+  | ty1 `eqType` ty2 = nopL
+  | otherwise        = addErrL msg
 \end{code}
 
-\begin{code}
-checkSpecTyApp :: PlainCoreExpr -> [UniType] -> ErrMsg -> LintM (Maybe ())
-
-checkSpecTyApp expr ty_args msg spec_done loc scope errs
-  = if spec_done
-    && any isUnboxedDataType ty_args
-    && not (an_application_of_error expr)
-    then (Nothing, addErr errs msg loc)
-    else (Just (), errs)
-  where
-     -- always safe (but maybe unfriendly) to say "False"
-    an_application_of_error (CoVar id) | isBottomingId id = True
-    an_application_of_error _ = False
-\end{code}
+
+%************************************************************************
+%*									*
+\subsection{Error messages}
+%*									*
+%************************************************************************
 
 \begin{code}
-checkFunApp :: UniType 		-- The function type
-	    -> [UniType] 	-- The arg type(s)
-	    -> ErrMsg 		-- Error messgae
-	    -> LintM (Maybe UniType)	-- The result type
+dumpLoc (RhsOf v)
+  = (getSrcLoc v, brackets (ptext SLIT("RHS of") <+> pp_binders [v]))
 
-checkFunApp fun_ty arg_tys msg spec loc scope errs
-  = cfa res_ty expected_arg_tys arg_tys
-  where
-    (expected_arg_tys, res_ty) = splitTyArgs fun_ty
+dumpLoc (LambdaBodyOf b)
+  = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
 
-    cfa res_ty expected []	-- Args have run out; that's fine
-	= (Just (glueTyArgs expected res_ty), errs)
+dumpLoc (BodyOfLetRec [])
+  = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))
 
-    cfa res_ty [] arg_tys	-- Expected arg tys ran out first; maybe res_ty is a 
-				-- dictionary type which is actually a function?
-	= case splitTyArgs (unDictifyTy res_ty) of
-	    ([], _) 		    -> (Nothing, addErr errs msg loc)	-- Too many args
-	    (new_expected, new_res) -> cfa new_res new_expected arg_tys
+dumpLoc (BodyOfLetRec bs@(_:_))
+  = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
 
-    cfa res_ty (expected_arg_ty:expected_arg_tys) (arg_ty:arg_tys)
-	= case (cmpUniType True{-properly-} expected_arg_ty arg_ty) of
-		EQ_ -> cfa res_ty expected_arg_tys arg_tys
-		other -> (Nothing, addErr errs msg loc)			-- Arg mis-match
-\end{code}
+dumpLoc (AnExpr e)
+  = (noSrcLoc, text "In the expression:" <+> ppr e)
 
-\begin{code}
-checkInScope :: Id -> LintM ()
-checkInScope id spec loc scope errs
-  = if isLocallyDefined id && not (id `elementOfUniqSet` scope) then
-	((), addErr errs (\ sty -> ppCat [ppr sty id, ppStr "is out of scope"]) loc)
-    else
-	((), errs)
-
-checkTys :: UniType -> UniType -> ErrMsg -> LintM ()
-checkTys ty1 ty2 msg spec loc scope errs
-  = case (cmpUniType True{-properly-} ty1 ty2) of
-	EQ_   -> ((), errs)
-	other -> ((), addErr errs msg loc)
-\end{code}
+dumpLoc (CaseAlt (con, args, rhs))
+  = (noSrcLoc, text "In a case pattern:" <+> parens (ppr con <+> ppr args))
 
-\begin{code}
-mkCaseAltMsg :: PlainCoreCaseAlternatives -> ErrMsg
-mkCaseAltMsg alts sty
-  = ppAbove (ppStr "In some case alternatives, type of alternatives not all same:")
-	    (ppr sty alts)
-
-mkCaseDataConMsg :: PlainCoreExpr -> ErrMsg
-mkCaseDataConMsg expr sty
-  = ppAbove (ppStr "A case scrutinee not a type-constructor type:")
-	    (pp_expr sty expr)
-
-mkCasePrimMsg :: Bool -> TyCon -> ErrMsg
-mkCasePrimMsg True tycon sty
-  = ppAbove (ppStr "A primitive case on a non-primitive type:")
-	    (ppr sty tycon)
-mkCasePrimMsg False tycon sty
-  = ppAbove (ppStr "An algebraic case on a primitive type:")
-	    (ppr sty tycon)
-
-mkCaseAbstractMsg :: TyCon -> ErrMsg
-mkCaseAbstractMsg tycon sty
-  = ppAbove (ppStr "An algebraic case on an abstract type:")
-	    (ppr sty tycon)
-
-mkDefltMsg :: PlainCoreCaseDefault -> ErrMsg
-mkDefltMsg deflt sty
-  = ppAbove (ppStr "Binder in default case of a case expression doesn't match type of scrutinee:")
-	    (ppr sty deflt)
-
-mkFunAppMsg :: UniType -> [UniType] -> PlainCoreExpr -> ErrMsg
-mkFunAppMsg fun_ty arg_tys expr sty
-  = ppAboves [ppStr "In a function application, function type doesn't match arg types:",
-	      ppHang (ppStr "Function type:") 4 (ppr sty fun_ty),
-	      ppHang (ppStr "Arg types:") 4 (ppAboves (map (ppr sty) arg_tys)),
-	      ppHang (ppStr "Expression:") 4 (pp_expr sty expr)]
-
-mkUnappTyMsg :: Id -> UniType -> ErrMsg
-mkUnappTyMsg var ty sty
-  = ppAboves [ppStr "Variable has a for-all type, but isn't applied to any types.",
-	      ppBeside (ppStr "Var:      ") (ppr sty var),
-	      ppBeside (ppStr "Its type: ") (ppr sty ty)]
-
-mkAlgAltMsg1 :: UniType -> ErrMsg
-mkAlgAltMsg1 ty sty
-  = ppAbove (ppStr "In some case statement, type of scrutinee is not a data type:")
-	    (ppr sty ty)
-
-mkAlgAltMsg2 :: UniType -> Id -> ErrMsg
-mkAlgAltMsg2 ty con sty
-  = ppAboves [
-	ppStr "In some algebraic case alternative, constructor is not a constructor of scrutinee type:",
-	ppr sty ty,
-	ppr sty con
-    ]
+dumpLoc (ImportedUnfolding locn)
+  = (locn, brackets (ptext SLIT("in an imported unfolding")))
 
-mkAlgAltMsg3 :: Id -> [Id] -> ErrMsg
-mkAlgAltMsg3 con alts sty
-  = ppAboves [
-	ppStr "In some algebraic case alternative, number of arguments doesn't match constructor:",
-	ppr sty con,
-	ppr sty alts
-    ]
+pp_binders :: [Var] -> SDoc
+pp_binders bs = sep (punctuate comma (map pp_binder bs))
 
-mkAlgAltMsg4 :: UniType -> Id -> ErrMsg
-mkAlgAltMsg4 ty arg sty
-  = ppAboves [
-	ppStr "In some algebraic case alternative, type of argument doesn't match data constructor:",
-	ppr sty ty,
-	ppr sty arg
-    ]
+pp_binder :: Var -> SDoc
+pp_binder b | isId b    = hsep [ppr b, dcolon, ppr (idType b)]
+            | isTyVar b = hsep [ppr b, dcolon, ppr (tyVarKind b)]
+\end{code}
 
-mkPrimAltMsg :: (BasicLit, PlainCoreExpr) -> ErrMsg
-mkPrimAltMsg alt sty
-  = ppAbove (ppStr "In a primitive case alternative, type of literal doesn't match type of scrutinee:")
-	    (ppr sty alt)
-
-mkRhsMsg :: Id -> UniType -> ErrMsg
-mkRhsMsg binder ty sty
-  = ppAboves [ppCat [ppStr "The type of this binder doesn't match the type of its RHS:", 
-		     ppr sty binder],
-	      ppCat [ppStr "Binder's type:", ppr sty (getIdUniType binder)],
-	      ppCat [ppStr "Rhs type:", ppr sty ty]
-	     ]
+\begin{code}
+------------------------------------------------------
+--	Messages for case expressions
+
+mkNullAltsMsg :: CoreExpr -> Message
+mkNullAltsMsg e 
+  = hang (text "Case expression with no alternatives:")
+	 4 (ppr e)
+
+mkDefaultArgsMsg :: [Var] -> Message
+mkDefaultArgsMsg args 
+  = hang (text "DEFAULT case with binders")
+	 4 (ppr args)
+
+mkCaseAltMsg :: CoreExpr -> Message
+mkCaseAltMsg e
+  = hang (text "Type of case alternatives not the same:")
+	 4 (ppr e)
+
+mkScrutMsg :: Id -> Type -> Message
+mkScrutMsg var scrut_ty
+  = vcat [text "Result binder in case doesn't match scrutinee:" <+> ppr var,
+	  text "Result binder type:" <+> ppr (idType var),
+	  text "Scrutinee type:" <+> ppr scrut_ty]
+
+
+mkNonDefltMsg e
+  = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
+
+nonExhaustiveAltsMsg :: CoreExpr -> Message
+nonExhaustiveAltsMsg e
+  = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
+
+mkBadPatMsg :: Type -> Type -> Message
+mkBadPatMsg con_result_ty scrut_ty
+  = vcat [
+	text "In a case alternative, pattern result type doesn't match scrutinee type:",
+	text "Pattern result type:" <+> ppr con_result_ty,
+	text "Scrutinee type:" <+> ppr scrut_ty
+    ]
 
-mkRhsPrimMsg :: Id -> PlainCoreExpr -> ErrMsg
-mkRhsPrimMsg binder rhs sty
-  = ppAboves [ppCat [ppStr "The type of this binder is primitive:", 
-		     ppr sty binder],
-	      ppCat [ppStr "Binder's type:", ppr sty (getIdUniType binder)]
+------------------------------------------------------
+--	Other error messages
+
+mkAppMsg :: Type -> Type -> Message
+mkAppMsg fun arg
+  = vcat [ptext SLIT("Argument value doesn't match argument type:"),
+	      hang (ptext SLIT("Fun type:")) 4 (ppr fun),
+	      hang (ptext SLIT("Arg type:")) 4 (ppr arg)]
+
+mkKindErrMsg :: TyVar -> Type -> Message
+mkKindErrMsg tyvar arg_ty
+  = vcat [ptext SLIT("Kinds don't match in type application:"),
+	  hang (ptext SLIT("Type variable:"))
+		 4 (ppr tyvar <+> dcolon <+> ppr (tyVarKind tyvar)),
+	  hang (ptext SLIT("Arg type:"))   
+	         4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
+
+mkTyAppMsg :: Type -> Type -> Message
+mkTyAppMsg ty arg_ty
+  = vcat [text "Illegal type application:",
+	      hang (ptext SLIT("Exp type:"))
+		 4 (ppr ty <+> dcolon <+> ppr (typeKind ty)),
+	      hang (ptext SLIT("Arg type:"))   
+	         4 (ppr arg_ty <+> dcolon <+> ppr (typeKind arg_ty))]
+
+mkRhsMsg :: Id -> Type -> Message
+mkRhsMsg binder ty
+  = vcat
+    [hsep [ptext SLIT("The type of this binder doesn't match the type of its RHS:"),
+	    ppr binder],
+     hsep [ptext SLIT("Binder's type:"), ppr (idType binder)],
+     hsep [ptext SLIT("Rhs type:"), ppr ty]]
+
+mkRhsPrimMsg :: Id -> CoreExpr -> Message
+mkRhsPrimMsg binder rhs
+  = vcat [hsep [ptext SLIT("The type of this binder is primitive:"),
+		     ppr binder],
+	      hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
 	     ]
 
-mkTyAppMsg :: PlainCoreExpr -> ErrMsg
-mkTyAppMsg expr sty
-  = ppAboves [ppStr "In a type application, either the function's type doesn't match",
-	      ppStr "the argument types, or an argument type is primitive:",
-	      pp_expr sty expr]
+mkUnboxedTupleMsg :: Id -> Message
+mkUnboxedTupleMsg binder
+  = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
+	  hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]
 
-mkSpecTyAppMsg :: PlainCoreExpr -> ErrMsg
-mkSpecTyAppMsg expr sty
-  = ppAbove (ppStr "Unboxed types in a type application (after specialisation):")
-	    (pp_expr sty expr)
+mkCoerceErr from_ty expr_ty
+  = vcat [ptext SLIT("From-type of Coerce differs from type of enclosed expression"),
+	  ptext SLIT("From-type:") <+> ppr from_ty,
+	  ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
+    ]
 
-pp_expr sty expr
-  = pprCoreExpr sty pprBigCoreBinder pprTypedCoreBinder pprTypedCoreBinder expr
+mkStrangeTyMsg e
+  = ptext SLIT("Type where expression expected:") <+> ppr e
 \end{code}