[project @ 1998-12-02 13:17:09 by simonm]
[ghc-hetmet.git] / ghc / compiler / coreSyn / CoreLint.lhs
index 7dada83..b4b58d8 100644 (file)
@@ -1,12 +1,13 @@
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1993-1996
+% (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
 %
 \section[CoreLint]{A ``lint'' pass to check for Core correctness}
 
 \begin{code}
 module CoreLint (
        lintCoreBindings,
-       lintUnfolding
+       lintUnfolding, 
+       beginPass, endPass
     ) where
 
 #include "HsVersions.h"
@@ -15,41 +16,29 @@ import IO   ( hPutStr, stderr )
 
 import CmdLineOpts      ( opt_D_show_passes, opt_DoCoreLinting )
 import CoreSyn
-import CoreUtils       ( idSpecVars )
+import CoreUtils       ( idFreeVars )
 
 import Bag
-import Kind            ( hasMoreBoxityInfo, Kind{-instance-} )
-import Literal         ( literalType, Literal{-instance-} )
-import Id              ( idType, isBottomingId, dataConRepType, isDataCon, isAlgCon,
-                         dataConArgTys, GenId{-instances-},
-                         emptyIdSet, mkIdSet, 
-                         unionIdSets, elementOfIdSet, IdSet,
-                         Id
-                       )
-import Maybes          ( catMaybes )
-import Name            ( isLocallyDefined, getSrcLoc, Name{-instance NamedThing-},
-                         NamedThing(..)
-                       )
+import Const           ( Con(..), DataCon, conType, conOkForApp, conOkForAlt )
+import Id              ( isConstantId, idMustBeINLINEd )
+import Var             ( IdOrTyVar, Id, TyVar, idType, tyVarKind, isTyVar )
+import VarSet
+import VarEnv          ( mkVarEnv )
+import Name            ( isLocallyDefined, getSrcLoc )
 import PprCore
-import ErrUtils                ( doIfSet, ghcExit )
-import PrimOp          ( primOpType )
+import ErrUtils                ( doIfSet, dumpIfSet, ghcExit )
 import PrimRep         ( PrimRep(..) )
 import SrcLoc          ( SrcLoc )
-import Type            ( mkFunTy, splitFunTy_maybe, mkForAllTy,
-                         splitForAllTy_maybe, tyVarsOfType,
-                         isUnpointedType, typeKind, instantiateTy,
-                         splitAlgTyConApp_maybe, Type
-                       )
-import TyCon           ( TyCon, isPrimTyCon, isDataTyCon )
-import TyVar           ( TyVar, tyVarKind, mkTyVarEnv, 
-                         TyVarSet,
-                           emptyTyVarSet, mkTyVarSet, isEmptyTyVarSet, 
-                           minusTyVarSet, elementOfTyVarSet, tyVarSetToList,
-                           unionTyVarSets, intersectTyVarSets
+import Type            ( Type, Kind, tyVarsOfType,
+                         splitFunTy_maybe, mkPiType, mkTyVarTy,
+                         splitForAllTy_maybe, splitTyConApp_maybe,
+                         isUnLiftedType, typeKind, substTy,
+                         splitAlgTyConApp_maybe,
+                         isUnboxedTupleType,
+                         hasMoreBoxityInfo
                        )
+import TyCon           ( TyCon, isPrimTyCon, tyConDataCons )
 import ErrUtils                ( ErrMsg )
-import Unique          ( Unique )
-import Util            ( zipEqual )
 import Outputable
 
 infixr 9 `thenL`, `seqL`, `thenMaybeL`
@@ -57,6 +46,39 @@ infixr 9 `thenL`, `seqL`, `thenMaybeL`
 
 %************************************************************************
 %*                                                                     *
+\subsection{Start and end pass}
+%*                                                                     *
+%************************************************************************
+
+@beginPass@ 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}
+beginPass :: String -> IO ()
+beginPass pass_name
+  | opt_D_show_passes
+  = hPutStr stderr ("*** " ++ pass_name ++ "\n")
+  | otherwise
+  = return ()
+
+
+endPass :: String -> Bool -> [CoreBind] -> IO [CoreBind]
+endPass pass_name dump_flag binds
+  = do 
+       -- Report verbosely, if required
+       dumpIfSet dump_flag pass_name
+                 (pprCoreBindings binds)
+
+       -- Type check
+       lintCoreBindings pass_name binds
+
+       return binds
+\end{code}
+
+
+%************************************************************************
+%*                                                                     *
 \subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
 %*                                                                     *
 %************************************************************************
@@ -84,19 +106,16 @@ Outstanding issues:
     --
     -- * Oversaturated type app after specialisation (eta reduction
     --   may well be happening...);
-    --
-    -- Note: checkTyApp is usually followed by a call to checkSpecTyApp.
-    --
 
 \begin{code}
-lintCoreBindings :: String -> Bool -> [CoreBinding] -> IO ()
+lintCoreBindings :: String -> [CoreBind] -> IO ()
 
-lintCoreBindings whoDunnit spec_done binds
+lintCoreBindings whoDunnit binds
   | not opt_DoCoreLinting
   = return ()
 
-lintCoreBindings whoDunnit spec_done binds
-  = case (initL (lint_binds binds) spec_done) of
+lintCoreBindings whoDunnit binds
+  = case (initL (lint_binds binds)) of
       Nothing       -> doIfSet opt_D_show_passes
                        (hPutStr stderr ("*** Core Linted result of " ++ whoDunnit ++ "\n"))
 
@@ -132,8 +151,7 @@ lintUnfolding :: SrcLoc -> CoreExpr -> Maybe CoreExpr
 
 lintUnfolding locn expr
   = case
-      (initL (addLoc (ImportedUnfolding locn) (lintCoreExpr expr))
-       True{-pretend spec done-})
+      initL (addLoc (ImportedUnfolding locn) (lintCoreExpr expr))
     of
       Nothing  -> Just expr
       Just msg ->
@@ -154,7 +172,7 @@ lintUnfolding locn expr
 Check a core binding, returning the list of variables bound.
 
 \begin{code}
-lintCoreBinding :: CoreBinding -> LintM [Id]
+lintCoreBinding :: CoreBind -> LintM [Id]
 
 lintCoreBinding (NonRec binder rhs)
   = lintSingleBinding (binder,rhs) `seqL` returnL [binder]
@@ -164,33 +182,31 @@ lintCoreBinding (Rec pairs)
       mapL lintSingleBinding pairs `seqL` returnL binders
     )
   where
-    binders = [b | (b,_) <- pairs]
+    binders = map fst pairs
 
 lintSingleBinding (binder,rhs)
-  = addLoc (RhsOf binder) (
+  = addLoc (RhsOf binder) $
+
        -- Check the rhs
-       lintCoreExpr rhs
+    lintCoreExpr rhs                           `thenL` \ ty ->
 
-       `thenL` \maybe_ty ->
        -- Check match to RHS type
-       (case maybe_ty of
-         Nothing -> returnL ()
-         Just ty -> checkTys (idType binder) ty (mkRhsMsg binder ty))
+    lintBinder binder                          `seqL`
+    checkTys binder_ty ty (mkRhsMsg binder ty) `seqL`
 
-       `seqL`
-       -- Check (not isUnpointedType)
-       checkIfSpecDoneL (not (isUnpointedType (idType binder)))
-         (mkRhsPrimMsg binder rhs)  `seqL`
+       -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
+    checkL (not (isUnLiftedType binder_ty))
+          (mkRhsPrimMsg binder rhs)            `seqL`
 
         -- Check whether binder's specialisations contain any out-of-scope variables
-        ifSpecDoneL (mapL (checkSpecIdInScope binder) spec_vars `seqL` returnL ())
+    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
-     spec_vars = idSpecVars binder
-
+  where
+    binder_ty = idType binder
+    bndr_vars = varSetElems (idFreeVars binder)
 \end{code}
 
 %************************************************************************
@@ -200,10 +216,10 @@ lintSingleBinding (binder,rhs)
 %************************************************************************
 
 \begin{code}
-lintCoreExpr :: CoreExpr -> LintM (Maybe Type) -- Nothing if error found
+lintCoreExpr :: CoreExpr -> LintM Type
 
 lintCoreExpr (Var var) 
-  | isAlgCon var = returnL (Just (idType var))
+  | isConstantId var = returnL (idType var)
        -- Micro-hack here... Class decls generate applications of their
        -- dictionary constructor, but don't generate a binding for the
        -- constructor (since it would never be used).  After a single round
@@ -213,17 +229,16 @@ lintCoreExpr (Var var)
        -- variables as the function in an application.
        -- The hack here simply doesn't check for out-of-scope-ness for
        -- data constructors (at least, in a function position).
+       -- Ditto primitive Ids
 
-  | otherwise    = checkIdInScope var `seqL` returnL (Just (idType var))
-
-lintCoreExpr (Lit lit) = returnL (Just (literalType lit))
+  | otherwise    = checkIdInScope var `seqL` returnL (idType var)
 
 lintCoreExpr (Note (Coerce to_ty from_ty) expr)
-  = lintCoreExpr expr  `thenMaybeL` \ expr_ty ->
+  = 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 (Just to_ty)
+    returnL to_ty
 
 lintCoreExpr (Note other_note expr)
   = lintCoreExpr expr
@@ -237,37 +252,48 @@ lintCoreExpr (Let binds body)
        (addInScopeVars binders (lintCoreExpr body))
 
 lintCoreExpr e@(Con con args)
-  = checkL (isDataCon con) (mkConErrMsg e)     `seqL`
-    lintCoreArgs {-False-} e (dataConRepType con) args
-    -- Note: we don't check for primitive types in these arguments
-
-lintCoreExpr e@(Prim op args)
-  = lintCoreArgs {-True-} e (primOpType op) args
-    -- Note: we do check for primitive types in these arguments
-
-lintCoreExpr e@(App fun@(Var v) arg) | isBottomingId v
-  = lintCoreExpr fun `thenMaybeL` \ ty -> lintCoreArg {-False-} e ty arg
-    -- Note: we don't check for primitive types in argument to 'error'
+  = addLoc (AnExpr e)  $
+    checkL (conOkForApp con) (mkConAppMsg e)   `seqL`
+    lintCoreArgs (conType con) args
 
 lintCoreExpr e@(App fun arg)
-  = lintCoreExpr fun `thenMaybeL` \ty -> lintCoreArg {-True-} e ty arg
-    -- Note: we do check for primitive types in this argument
-
-lintCoreExpr (Lam vb@(ValBinder var) expr)
-  = addLoc (LambdaBodyOf vb)
-      (addInScopeVars [var]
-       (lintCoreExpr expr `thenMaybeL` \ty ->
-        returnL (Just (mkFunTy (idType var) ty))))
-
-lintCoreExpr (Lam tb@(TyBinder tyvar) expr)
-  = addLoc (LambdaBodyOf tb)  $
-     addInScopeTyVars [tyvar] $
-       lintCoreExpr expr                          `thenMaybeL` \ ty ->
-       returnL (Just(mkForAllTy tyvar ty))
-
-lintCoreExpr e@(Case scrut alts)
- = lintCoreExpr scrut `thenMaybeL` \ty ->
-   lintCoreAlts alts ty
+  = lintCoreExpr fun   `thenL` \ ty ->
+    addLoc (AnExpr e)  $
+    lintCoreArg ty arg
+
+lintCoreExpr (Lam var expr)
+  = addLoc (LambdaBodyOf var)  $
+    checkL (not (isUnboxedTupleType (idType var))) (mkUnboxedTupleMsg var)
+                               `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
+   checkAllCasesCovered 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)
 \end{code}
 
 %************************************************************************
@@ -280,46 +306,33 @@ The boolean argument indicates whether we should flag type
 applications to primitive types as being errors.
 
 \begin{code}
-lintCoreArgs :: {-Bool ->-} CoreExpr -> Type -> [CoreArg] -> LintM (Maybe Type)
+lintCoreArgs :: Type -> [CoreArg] -> LintM Type
 
-lintCoreArgs _ ty [] = returnL (Just ty)
-lintCoreArgs e ty (a : args)
-  = lintCoreArg  e ty  a `thenMaybeL` \ res ->
-    lintCoreArgs e res args
+lintCoreArgs ty [] = returnL ty
+lintCoreArgs ty (a : args)
+  = lintCoreArg  ty a          `thenL` \ res ->
+    lintCoreArgs res args
 \end{code}
 
-%************************************************************************
-%*                                                                     *
-\subsection[lintCoreArg]{lintCoreArg}
-%*                                                                     *
-%************************************************************************
-
 \begin{code}
-lintCoreArg :: {-Bool ->-} CoreExpr -> Type -> CoreArg -> LintM (Maybe Type)
+lintCoreArg :: Type -> CoreArg -> LintM Type
 
-lintCoreArg e ty (LitArg lit)
+lintCoreArg ty a@(Type arg_ty)
+  = lintTy arg_ty                      `seqL`
+    lintTyApp ty arg_ty
+
+lintCoreArg fun_ty arg
   = -- Make sure function type matches argument
-    case (splitFunTy_maybe ty) of
-      Just (arg,res) | (lit_ty == arg) -> returnL(Just res)
-      _ -> addErrL (mkAppMsg ty lit_ty e) `seqL` returnL Nothing
-  where
-    lit_ty = literalType lit
-
-lintCoreArg e ty (VarArg v)
-  = -- Make sure variable is bound
-    checkIdInScope v `seqL`
-    -- Make sure function type matches argument
-    case (splitFunTy_maybe ty) of
-      Just (arg,res) | (var_ty == arg) -> returnL(Just res)
-      _ -> addErrL (mkAppMsg ty var_ty e) `seqL` returnL Nothing
-  where
-    var_ty = idType v
+    lintCoreExpr arg           `thenL` \ arg_ty ->
+    case (splitFunTy_maybe fun_ty) of
+      Just (arg,res) | (arg_ty == arg) -> returnL res
+      _                               -> addErrL (mkAppMsg fun_ty arg_ty)
+\end{code}
 
-lintCoreArg e ty a@(TyArg arg_ty)
-  = lintTy arg_ty                           `seqL`
-    checkTyVarsInScope (tyVarsOfType arg_ty) `seqL`
-    case (splitForAllTy_maybe ty) of
-      Nothing -> addErrL (mkTyAppMsg SLIT("Illegal") ty arg_ty e) `seqL` returnL Nothing
+\begin{code}
+lintTyApp ty arg_ty 
+  = case splitForAllTy_maybe ty of
+      Nothing -> addErrL (mkTyAppMsg ty arg_ty)
 
       Just (tyvar,body) ->
        let
@@ -332,12 +345,20 @@ lintCoreArg e ty a@(TyArg arg_ty)
                --      error :: forall a:*. String -> a
                -- and then apply it to both boxed and unboxed types.
         then
-           returnL(Just(instantiateTy (mkTyVarEnv [(tyvar,arg_ty)]) body))
+           returnL (substTy (mkVarEnv [(tyvar,arg_ty)]) body)
        else
-           pprTrace "lintCoreArg:kinds:" (hsep [ppr tyvar_kind, ppr argty_kind]) $
-           addErrL (mkKindErrMsg tyvar arg_ty e) `seqL` returnL Nothing
+           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[lintCoreAlts]{lintCoreAlts}
@@ -345,83 +366,79 @@ lintCoreArg e ty a@(TyArg arg_ty)
 %************************************************************************
 
 \begin{code}
-lintCoreAlts :: CoreCaseAlts
-            -> Type                    -- Type of scrutinee
---          -> TyCon                   -- TyCon pinned on the case
-            -> LintM (Maybe Type)      -- Type of alternatives
-
-lintCoreAlts whole_alts@(AlgAlts alts deflt) ty --tycon
-  = -- Check tycon is not a primitive tycon
---    addErrIfL (isPrimTyCon tycon) (mkCasePrimMsg tycon)
---    `seqL`
-    -- Check we are scrutinising a proper datatype
-    -- (ToDo: robustify)
---    addErrIfL (not (tyConFamilySize tycon >= 1)) (mkCaseAbstractMsg tycon)
---    `seqL`
-    lintDeflt deflt ty
-    `thenL` \maybe_deflt_ty ->
-    mapL (lintAlgAlt ty {-tycon-}) alts
-    `thenL` \maybe_alt_tys ->
-    -- Check the result types
-    case catMaybes (maybe_deflt_ty : maybe_alt_tys) of
-      []            -> returnL Nothing
-
-      (first_ty:tys) -> mapL check tys `seqL`
-                       returnL (Just first_ty)
-       where
-         check ty = checkTys first_ty ty (mkCaseAltMsg whole_alts)
-
-lintCoreAlts whole_alts@(PrimAlts alts deflt) ty --tycon
-  = -- Check tycon is a primitive tycon
---    addErrIfL (not (isPrimTyCon tycon)) (mkCaseNotPrimMsg tycon)
---    `seqL`
-    mapL (lintPrimAlt ty) alts
-    `thenL` \maybe_alt_tys ->
-    lintDeflt deflt ty
-    `thenL` \maybe_deflt_ty ->
-    -- Check the result types
-    case catMaybes (maybe_deflt_ty : maybe_alt_tys) of
-      []            -> returnL Nothing
-
-      (first_ty:tys) -> mapL check tys `seqL`
-                       returnL (Just first_ty)
-       where
-         check ty = checkTys first_ty ty (mkCaseAltMsg whole_alts)
-
-lintAlgAlt scrut_ty (con,args,rhs)
-  = (case splitAlgTyConApp_maybe scrut_ty of
-      Just (tycon, tys_applied, cons) | isDataTyCon tycon ->
-        let
-          arg_tys = dataConArgTys con tys_applied
-        in
-        checkL (con `elem` cons) (mkAlgAltMsg2 scrut_ty con) `seqL`
-        checkL (length arg_tys == length args) (mkAlgAltMsg3 con args)
-                                                                `seqL`
-        mapL check (zipEqual "lintAlgAlt" arg_tys args)         `seqL`
-        returnL ()
-
-      other -> addErrL (mkAlgAltMsg1 scrut_ty)
-    )                                                           `seqL`
-    addInScopeVars args        (
-        lintCoreExpr rhs
-    )
+checkAllCasesCovered e ty [] = addErrL (mkNullAltsMsg e)
+
+checkAllCasesCovered e ty [(DEFAULT,_,_)] = nopL
+
+checkAllCasesCovered e scrut_ty alts
+  = case splitTyConApp_maybe scrut_ty of {
+       Nothing -> addErrL (badAltsMsg e);
+       Just (tycon, tycon_arg_tys) ->
+
+    if isPrimTyCon tycon then
+       checkL (hasDefault alts) (nonExhaustiveAltsMsg e)
+    else
+#ifdef DEBUG
+       -- Algebraic cases are not necessarily exhaustive, because
+       -- the simplifer correctly eliminates case that can't 
+       -- possibly match.
+       -- This code just emits a message to say so
+    let
+       missing_cons    = filter not_in_alts (tyConDataCons tycon)
+       not_in_alts con = all (not_in_alt con) alts
+       not_in_alt con (DataCon con', _, _) = con /= con'
+       not_in_alt con other                = True
+
+       case_bndr = case e of { Case _ bndr alts -> bndr }
+    in
+    if not (hasDefault alts || null missing_cons) then
+       pprTrace "Exciting (but not a problem)!  Non-exhaustive case:"
+                (ppr case_bndr <+> ppr missing_cons)
+                nopL
+    else
+#endif
+    nopL }
+
+hasDefault []                    = False
+hasDefault ((DEFAULT,_,_) : alts) = True
+hasDefault (alt                  : alts) = hasDefault alts
+\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@(con, args, rhs)
+  = addLoc (CaseAlt alt) (
+
+    checkL (conOkForAlt con) (mkConAltMsg con) `seqL`
+
+    mapL (\arg -> checkL (not (isUnboxedTupleType (idType arg))) 
+                       (mkUnboxedTupleMsg arg)) args `seqL`
+
+    addInScopeVars args (
+
+       -- 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.
+    case splitTyConApp_maybe scrut_ty of { Just (tycon, tycon_arg_tys) ->
+       lintTyApps (conType 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`
+
+       -- Check the RHS
+    lintCoreExpr rhs
+    ))
   where
-    check (ty, arg) = checkTys ty (idType 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 ty alt@(lit,rhs)
- = checkTys (literalType lit) ty (mkPrimAltMsg alt) `seqL`
-   lintCoreExpr rhs
-
-lintDeflt NoDefault _ = returnL Nothing
-lintDeflt deflt@(BindDefault binder rhs) ty
-  = checkTys (idType binder) ty (mkDefltMsg deflt) `seqL`
-    addInScopeVars [binder] (lintCoreExpr rhs)
+    mk_arg b | isTyVar b = Type (mkTyVarTy b)
+            | otherwise = Var b
 \end{code}
 
 %************************************************************************
@@ -431,9 +448,14 @@ lintDeflt deflt@(BindDefault binder rhs) ty
 %************************************************************************
 
 \begin{code}
+lintBinder :: IdOrTyVar -> LintM ()
+lintBinder v = nopL
+-- ToDo: lint its type
+
 lintTy :: Type -> LintM ()
-lintTy ty = returnL ()
--- ToDo: Check that ty is well-kinded and has no unbound tyvars
+lintTy ty = mapL checkIdInScope (varSetElems (tyVarsOfType ty))        `seqL`
+           returnL ()
+       -- ToDo: check the kind structure of the type
 \end{code}
 
     
@@ -444,51 +466,24 @@ lintTy ty = returnL ()
 %************************************************************************
 
 \begin{code}
-type LintM a = Bool            -- True <=> specialisation has been done
-           -> [LintLocInfo]    -- Locations
+type LintM a = [LintLocInfo]   -- Locations
            -> IdSet            -- Local vars in scope
-           -> TyVarSet         -- Local tyvars in scope
            -> Bag ErrMsg       -- Error messages so far
-           -> (a, Bag ErrMsg)  -- Result and error messages (if any)
+           -> (Maybe a, Bag ErrMsg)    -- Result and error messages (if any)
 
 data LintLocInfo
-  = RhsOf Id                   -- The variable bound
-  | LambdaBodyOf CoreBinder    -- The lambda-binder
-  | BodyOfLetRec [Id]          -- One of the binders
-  | ImportedUnfolding SrcLoc    -- Some imported unfolding (ToDo: say which)
-
-instance Outputable LintLocInfo where
-    ppr (RhsOf v)
-      = ppr (getSrcLoc v) <> colon <+> 
-       brackets (ptext SLIT("RHS of") <+> pp_binders [v])
-
-    ppr (LambdaBodyOf (ValBinder b))
-      = ppr (getSrcLoc b) <> colon <+>
-       brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b)
-
-    ppr (LambdaBodyOf (TyBinder b))
-      = ppr (getSrcLoc b) <> colon <+>
-       brackets (ptext SLIT("in body of lambda with type binder") <+> ppr b)
-
-    ppr (BodyOfLetRec bs)
-      = ppr (getSrcLoc (head bs)) <> colon <+>
-       brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs)
-
-    ppr (ImportedUnfolding locn)
-      = ppr locn <> colon <+>
-       brackets (ptext SLIT("in an imported unfolding"))
-
-pp_binders :: [Id] -> SDoc
-pp_binders bs = sep (punctuate comma (map pp_binder bs))
-
-pp_binder :: Id -> SDoc
-pp_binder b = hsep [ppr b, text "::", ppr (idType b)]
+  = 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 -> Bool -> Maybe ErrMsg
-initL m spec_done
-  = case (m spec_done [] emptyIdSet emptyTyVarSet emptyBag) of { (_, errs) ->
+initL :: LintM a -> Maybe ErrMsg
+initL m
+  = case (m [] emptyVarSet emptyBag) of { (_, errs) ->
     if isEmptyBag errs then
        Nothing
     else
@@ -496,23 +491,21 @@ initL m spec_done
     }
 
 returnL :: a -> LintM a
-returnL r spec loc scope tyscope 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 tyscope errs
-  = case m spec loc scope tyscope errs of
-      (r, errs') -> k r spec loc scope tyscope errs'
+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 spec loc scope tyscope errs
-  = case m spec loc scope tyscope errs of
-      (_, errs') -> k spec loc scope tyscope errs'
-
-thenMaybeL :: LintM (Maybe a) -> (a -> LintM (Maybe b)) -> LintM (Maybe b)
-thenMaybeL m k spec loc scope tyscope errs
-  = case m spec loc scope tyscope errs of
-      (Nothing, errs2) -> (Nothing, errs2)
-      (Just r,  errs2) -> k r spec loc scope tyscope errs2
+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 []
@@ -520,188 +513,173 @@ 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 tyscope errs = ((), errs)
-checkL False msg spec loc scope tyscope errs = ((), addErr errs msg loc)
-
-checkIfSpecDoneL :: Bool -> ErrMsg -> LintM ()
-checkIfSpecDoneL True  msg spec  loc scope tyscope errs = ((), errs)
-checkIfSpecDoneL False msg True  loc scope tyscope errs = ((), addErr errs msg loc)
-checkIfSpecDoneL False msg False loc scope tyscope errs = ((), errs)
-
-ifSpecDoneL :: LintM () -> LintM ()
-ifSpecDoneL m False loc scope tyscope errs = ((), errs)
-ifSpecDoneL m True  loc scope tyscope errs = m True loc scope tyscope errs
+checkL True  msg loc scope errs = (Nothing, errs)
+checkL False msg loc scope errs = (Nothing, addErr errs msg loc)
 
-addErrL :: ErrMsg -> LintM ()
-addErrL msg spec loc scope tyscope errs = ((), addErr errs msg loc)
+addErrL :: ErrMsg -> LintM a
+addErrL msg loc scope errs = (Nothing, addErr errs msg loc)
 
 addErr :: Bag ErrMsg -> ErrMsg -> [LintLocInfo] -> Bag ErrMsg
 
 addErr errs_so_far msg locs
   = ASSERT (not (null locs))
-    errs_so_far `snocBag` (hang (ppr (head locs)) 4 msg)
+    errs_so_far `snocBag` (hang (pprLoc (head locs)) 4 msg)
 
 addLoc :: LintLocInfo -> LintM a -> LintM a
-addLoc extra_loc m spec loc scope tyscope errs
-  = m spec (extra_loc:loc) scope tyscope errs
-
-addInScopeVars :: [Id] -> LintM a -> LintM a
-addInScopeVars ids m spec loc scope tyscope 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 = mkIdSet ids
+addLoc extra_loc m loc scope errs
+  = m (extra_loc:loc) scope errs
 
---     shadowed = scope `intersectIdSets` 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 (uniqSetToList shadowed))) (
-    m spec loc (scope `unionIdSets` new_set) tyscope errs
---  )
-
-addInScopeTyVars :: [TyVar] -> LintM a -> LintM a
-addInScopeTyVars tyvars m spec loc scope tyscope errs
-  = m spec loc scope (tyscope `unionTyVarSets` new_set) errs
-    where
-     new_set   = mkTyVarSet tyvars
-    
+addInScopeVars :: [IdOrTyVar] -> LintM a -> LintM a
+addInScopeVars ids m loc scope errs
+  = m loc (scope `unionVarSet` mkVarSet ids) errs
 \end{code}
 
 \begin{code}
-checkIdInScope :: Id -> LintM ()
+checkIdInScope :: IdOrTyVar -> LintM ()
 checkIdInScope id 
   = checkInScope (ptext SLIT("is out of scope")) id
 
-checkSpecIdInScope :: Id -> Id -> LintM ()
-checkSpecIdInScope binder id 
+checkBndrIdInScope :: IdOrTyVar -> IdOrTyVar -> LintM ()
+checkBndrIdInScope binder id 
   = checkInScope msg id
     where
-     msg = ptext SLIT("is out of scope inside specialisation info for") <+> 
+     msg = ptext SLIT("is out of scope inside info for") <+> 
           ppr binder
 
-checkInScope :: SDoc -> Id -> LintM ()
-checkInScope loc_msg id spec loc scope tyscope errs
-  = let
-       id_name = getName id
-    in
-    if isLocallyDefined id_name && not (id `elementOfIdSet` scope) then
-      ((), addErr errs (hsep [ppr id, loc_msg]) loc)
-    else
-      ((),errs)
-
-checkTyVarsInScope :: TyVarSet -> LintM ()
-checkTyVarsInScope tyvars spec loc scope tyscope errs
--- | not (isEmptyTyVarSet out_of_scope) = ((), errs')
- | otherwise                   = ((), errs)
-   where
-    out_of_scope = tyvars `minusTyVarSet` tyscope
-    errs'        = 
-       foldr (\ tv errs -> addErr errs (hsep [ppr tv, ptext SLIT("is out of scope")]) loc)
-            errs
-            (tyVarSetToList out_of_scope)
+checkInScope :: SDoc -> IdOrTyVar -> LintM ()
+checkInScope loc_msg id loc scope errs
+  |  isLocallyDefined id 
+  && not (id `elemVarSet` scope)
+  && not (idMustBeINLINEd id)  -- Constructors and dict selectors 
+                               -- don't have bindings, 
+                               -- just MustInline prags
+  = (Nothing, addErr errs (hsep [ppr id, loc_msg]) loc)
+  | otherwise
+  = (Nothing,errs)
 
 checkTys :: Type -> Type -> ErrMsg -> LintM ()
-checkTys ty1 ty2 msg spec loc scope tyscope errs
-  = if ty1 == ty2 then ((), errs) else ((), addErr errs msg loc)
+checkTys ty1 ty2 msg loc scope errs
+  | ty1 == ty2 = (Nothing, errs)
+  | otherwise  = (Nothing, addErr errs msg loc)
 \end{code}
 
+
+%************************************************************************
+%*                                                                     *
+\subsection{Error messages}
+%*                                                                     *
+%************************************************************************
+
 \begin{code}
-mkConErrMsg e
-  = ($$) (ptext SLIT("Application of newtype constructor:"))
-           (ppr e)
+pprLoc (RhsOf v)
+  = ppr (getSrcLoc v) <> colon <+> 
+       brackets (ptext SLIT("RHS of") <+> pp_binders [v])
+
+pprLoc (LambdaBodyOf b)
+  = ppr (getSrcLoc b) <> colon <+>
+       brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b)
 
+pprLoc (BodyOfLetRec bs)
+  = ppr (getSrcLoc (head bs)) <> colon <+>
+       brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs)
+
+pprLoc (AnExpr e)
+  = text "In the expression:" <+> ppr e
 
-mkCaseAltMsg :: CoreCaseAlts -> ErrMsg
-mkCaseAltMsg alts
-  = ($$) (ptext SLIT("Type of case alternatives not the same:"))
-           (ppr alts)
+pprLoc (CaseAlt (con, args, rhs))
+  = text "In a case pattern:" <+> parens (ppr con <+> ppr args)
+
+pprLoc (ImportedUnfolding locn)
+  = ppr locn <> colon <+>
+       brackets (ptext SLIT("in an imported unfolding"))
+
+pp_binders :: [Id] -> SDoc
+pp_binders bs = sep (punctuate comma (map pp_binder bs))
+
+pp_binder :: Id -> SDoc
+pp_binder b = hsep [ppr b, text "::", ppr (idType b)]
+\end{code}
 
-mkCaseAbstractMsg :: TyCon -> ErrMsg
-mkCaseAbstractMsg tycon
-  = ($$) (ptext SLIT("An algebraic case on some weird type:"))
-           (ppr tycon)
+\begin{code}
+------------------------------------------------------
+--     Messages for case expressions
+
+mkConAppMsg :: CoreExpr -> ErrMsg 
+mkConAppMsg e
+  = hang (text "Application of newtype constructor:")
+        4 (ppr e)
+
+mkConAltMsg :: Con -> ErrMsg
+mkConAltMsg con
+  = text "PrimOp in case pattern:" <+> ppr con
+
+mkNullAltsMsg :: CoreExpr -> ErrMsg 
+mkNullAltsMsg e 
+  = hang (text "Case expression with no alternatives:")
+        4 (ppr e)
+
+mkDefaultArgsMsg :: [IdOrTyVar] -> ErrMsg 
+mkDefaultArgsMsg args 
+  = hang (text "DEFAULT case with binders")
+        4 (ppr args)
+
+mkCaseAltMsg :: CoreExpr -> ErrMsg 
+mkCaseAltMsg e
+  = hang (text "Type of case alternatives not the same:")
+        4 (ppr e)
+
+mkScrutMsg :: Id -> Type -> ErrMsg
+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]
+
+badAltsMsg :: CoreExpr -> ErrMsg
+badAltsMsg e
+  = hang (text "Case statement scrutinee is not a data type:")
+        4 (ppr e)
+
+nonExhaustiveAltsMsg :: CoreExpr -> ErrMsg
+nonExhaustiveAltsMsg e
+  = hang (text "Case expression with non-exhaustive alternatives")
+        4 (ppr e)
+
+mkBadPatMsg :: Type -> Type -> ErrMsg
+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
+    ]
 
-mkDefltMsg :: CoreCaseDefault -> ErrMsg
-mkDefltMsg deflt
-  = ($$) (ptext SLIT("Binder in case default doesn't match type of scrutinee:"))
-           (ppr deflt)
+------------------------------------------------------
+--     Other error messages
 
-mkAppMsg :: Type -> Type -> CoreExpr -> ErrMsg
-mkAppMsg fun arg expr
+mkAppMsg :: Type -> Type -> ErrMsg
+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),
-             hang (ptext SLIT("Expression:")) 4 (pprCoreExpr expr)]
+             hang (ptext SLIT("Arg type:")) 4 (ppr arg)]
 
-mkKindErrMsg :: TyVar -> Type -> CoreExpr -> ErrMsg
-mkKindErrMsg tyvar arg_ty expr
+mkKindErrMsg :: TyVar -> Type -> ErrMsg
+mkKindErrMsg tyvar arg_ty
   = vcat [ptext SLIT("Kinds don't match in type application:"),
          hang (ptext SLIT("Type variable:"))
                 4 (ppr tyvar <+> ptext SLIT("::") <+> ppr (tyVarKind tyvar)),
          hang (ptext SLIT("Arg type:"))   
-                4 (ppr arg_ty <+> ptext SLIT("::") <+> ppr (typeKind arg_ty)),
-         hang (ptext SLIT("Expression:")) 4 (pprCoreExpr expr)]
+                4 (ppr arg_ty <+> ptext SLIT("::") <+> ppr (typeKind arg_ty))]
 
-mkTyAppMsg :: FAST_STRING -> Type -> Type -> CoreExpr -> ErrMsg
-mkTyAppMsg msg ty arg expr
-  = vcat [hsep [ptext msg, ptext SLIT("type application:")],
+mkTyAppMsg :: Type -> Type -> ErrMsg
+mkTyAppMsg ty arg_ty
+  = vcat [text "Illegal type application:",
              hang (ptext SLIT("Exp type:"))
                 4 (ppr ty <+> ptext SLIT("::") <+> ppr (typeKind ty)),
              hang (ptext SLIT("Arg type:"))   
-                4 (ppr arg <+> ptext SLIT("::") <+> ppr (typeKind arg)),
-             hang (ptext SLIT("Expression:")) 4 (pprCoreExpr expr)]
-
-mkAlgAltMsg1 :: Type -> ErrMsg
-mkAlgAltMsg1 ty
-  = ($$) (text "In some case statement, type of scrutinee is not a data type:")
-           (ppr ty)
-
-mkAlgAltMsg2 :: Type -> Id -> ErrMsg
-mkAlgAltMsg2 ty con
-  = vcat [
-       text "In some algebraic case alternative, constructor is not a constructor of scrutinee type:",
-       ppr ty,
-       ppr con
-    ]
-
-mkAlgAltMsg3 :: Id -> [Id] -> ErrMsg
-mkAlgAltMsg3 con alts
-  = vcat [
-       text "In some algebraic case alternative, number of arguments doesn't match constructor:",
-       ppr con,
-       ppr alts
-    ]
-
-mkAlgAltMsg4 :: Type -> Id -> ErrMsg
-mkAlgAltMsg4 ty arg
-  = vcat [
-       text "In some algebraic case alternative, type of argument doesn't match data constructor:",
-       ppr ty,
-       ppr arg
-    ]
-
-mkPrimAltMsg :: (Literal, CoreExpr) -> ErrMsg
-mkPrimAltMsg alt
-  = ($$)
-    (text "In a primitive case alternative, type of literal doesn't match type of scrutinee:")
-           (ppr alt)
+                4 (ppr arg_ty <+> ptext SLIT("::") <+> ppr (typeKind arg_ty))]
 
 mkRhsMsg :: Id -> Type -> ErrMsg
 mkRhsMsg binder ty
@@ -718,6 +696,11 @@ mkRhsPrimMsg binder rhs
              hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
             ]
 
+mkUnboxedTupleMsg :: Id -> ErrMsg
+mkUnboxedTupleMsg binder
+  = vcat [hsep [ptext SLIT("A variable has unboxed tuple type:"), ppr binder],
+         hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]]
+
 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,