Add {-# OPTIONS_GHC -w #-} and some blurb to all compiler modules
[ghc-hetmet.git] / compiler / coreSyn / CoreLint.lhs
index dda8290..18b65d5 100644 (file)
@@ -1,9 +1,18 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1993-1998
 %
-\section[CoreLint]{A ``lint'' pass to check for Core correctness}
+
+A ``lint'' pass to check for Core correctness
 
 \begin{code}
+{-# OPTIONS_GHC -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/WorkingConventions#Warnings
+-- for details
+
 module CoreLint (
        lintCoreBindings,
        lintUnfolding, 
@@ -12,42 +21,35 @@ module CoreLint (
 
 #include "HsVersions.h"
 
+import NewDemand
 import CoreSyn
-import CoreFVs         ( idFreeVars )
-import CoreUtils       ( findDefault, exprOkForSpeculation, coreBindsSize )
-import Unify           ( coreRefineTys )
+import CoreFVs
+import CoreUtils
 import Bag
-import Literal         ( literalType )
-import DataCon         ( dataConRepType, isVanillaDataCon, dataConTyCon, dataConWorkId )
-import TysWiredIn      ( tupleCon )
-import Var             ( Var, Id, TyVar, idType, tyVarKind, mustHaveLocalBinding )
+import Literal
+import DataCon
+import TysWiredIn
+import Var
+import VarEnv
 import VarSet
-import Name            ( getSrcLoc )
+import Name
+import Id
 import PprCore
-import ErrUtils                ( dumpIfSet_core, ghcExit, Message, showPass,
-                         mkLocMessage, debugTraceMsg )
-import SrcLoc          ( SrcLoc, noSrcLoc, mkSrcSpan )
-import Type            ( Type, tyVarsOfType, coreEqType,
-                         splitFunTy_maybe, mkTyVarTys,
-                         splitForAllTy_maybe, splitTyConApp_maybe,
-                         isUnLiftedType, typeKind, mkForAllTy, mkFunTy,
-                         isUnboxedTupleType, isSubKind,
-                         substTyWith, emptyTvSubst, extendTvInScope, 
-                         TvSubst, TvSubstEnv, mkTvSubst, setTvSubstEnv, substTy,
-                         extendTvSubst, composeTvSubst, isInScope,
-                         getTvSubstEnv, getTvInScope )
-import TyCon           ( isPrimTyCon )
-import BasicTypes      ( RecFlag(..), Boxity(..), isNonRec )
-import StaticFlags     ( opt_PprStyle_Debug )
-import DynFlags                ( DynFlags, DynFlag(..), dopt )
+import ErrUtils
+import SrcLoc
+import Type
+import Coercion
+import TyCon
+import BasicTypes
+import StaticFlags
+import DynFlags
 import Outputable
 
 #ifdef DEBUG
 import Util             ( notNull )
 #endif
 
-import Maybe
-
+import Data.Maybe
 \end{code}
 
 %************************************************************************
@@ -109,6 +111,60 @@ Outstanding issues:
     --  * Oversaturated type app after specialisation (eta reduction
     --   may well be happening...);
 
+
+Note [Type lets]
+~~~~~~~~~~~~~~~~
+In the desugarer, it's very very convenient to be able to say (in effect)
+       let a = Int in <body>
+That is, use a type let.  (See notes just below for why we want this.)
+
+We don't have type lets in Core, so the desugarer uses type lambda
+       (/\a. <body>) Int
+However, in the lambda form, we'd get lint errors from:
+       (/\a. let x::a = 4 in <body>) Int
+because (x::a) doesn't look compatible with (4::Int).
+
+So (HACK ALERT) the Lint phase does type-beta reduction "on the fly",
+as it were.  It carries a type substitution (in this example [a -> Int])
+and applies this substitution before comparing types.  The functin
+       lintTy :: Type -> LintM Type
+returns a substituted type; that's the only reason it returns anything.
+
+When we encounter a binder (like x::a) we must apply the substitution
+to the type of the binding variable.  lintBinders does this.
+
+For Ids, the type-substituted Id is added to the in_scope set (which 
+itself is part of the TvSubst we are carrying down), and when we
+find an occurence of an Id, we fetch it from the in-scope set.
+
+
+Why we need type let
+~~~~~~~~~~~~~~~~~~~~
+It's needed when dealing with desugarer output for GADTs. Consider
+  data T = forall a. T a (a->Int) Bool
+   f :: T -> ... -> 
+   f (T x f True)  = <e1>
+   f (T y g False) = <e2>
+After desugaring we get
+       f t b = case t of 
+                 T a (x::a) (f::a->Int) (b:Bool) ->
+                   case b of 
+                       True -> <e1>
+                       False -> (/\b. let y=x; g=f in <e2>) a
+And for a reason I now forget, the ...<e2>... can mention a; so 
+we want Lint to know that b=a.  Ugh.
+
+I tried quite hard to make the necessity for this go away, by changing the 
+desugarer, but the fundamental problem is this:
+       
+       T a (x::a) (y::Int) -> let fail::a = ...
+                              in (/\b. ...(case ... of       
+                                               True  -> x::b
+                                               False -> fail)
+                                 ) a
+Now the inner case look as though it has incompatible branches.
+
+
 \begin{code}
 lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
 
@@ -128,8 +184,8 @@ lintCoreBindings dflags whoDunnit binds
     lint_binds binds = addInScopeVars (bindersOfBinds binds) $
                       mapM lint_bind binds 
 
-    lint_bind (Rec prs)                = mapM_ (lintSingleBinding Recursive) prs
-    lint_bind (NonRec bndr rhs) = lintSingleBinding NonRecursive (bndr,rhs)
+    lint_bind (Rec prs)                = mapM_ (lintSingleBinding TopLevel Recursive) prs
+    lint_bind (NonRec bndr rhs) = lintSingleBinding TopLevel NonRecursive (bndr,rhs)
 
     display bad_news
       = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
@@ -170,7 +226,7 @@ lintUnfolding locn vars expr
 Check a core binding, returning the list of variables bound.
 
 \begin{code}
-lintSingleBinding rec_flag (binder,rhs)
+lintSingleBinding top_lvl_flag rec_flag (binder,rhs)
   = addLoc (RhsOf binder) $
          -- Check the rhs 
     do { ty <- lintCoreExpr rhs        
@@ -181,14 +237,28 @@ lintSingleBinding rec_flag (binder,rhs)
        ; checkL (not (isUnLiftedType binder_ty)
             || (isNonRec rec_flag && exprOkForSpeculation rhs))
           (mkRhsPrimMsg binder rhs)
+        -- Check that if the binder is top-level or recursive, it's not demanded
+       ; checkL (not (isStrictId binder)
+            || (isNonRec rec_flag && not (isTopLevel top_lvl_flag)))
+           (mkStrictMsg binder)
         -- Check whether binder's specialisations contain any out-of-scope variables
-       ; mapM_ (checkBndrIdInScope binder) bndr_vars }
+       ; mapM_ (checkBndrIdInScope binder) bndr_vars 
+
+      -- Check whether arity and demand type are consistent (only if demand analysis
+      -- already happened)
+       ; checkL (case maybeDmdTy of
+                  Just (StrictSig dmd_ty) -> idArity binder >= dmdTypeDepth dmd_ty || exprIsTrivial rhs
+                  Nothing -> True)
+           (mkArityMsg binder) }
          
        -- 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)
+       -- the unfolding is a SimplifiableCoreExpr. Give up for now.
+   where
+    binder_ty                  = idType binder
+    maybeDmdTy                 = idNewStrictness_maybe binder
+    bndr_vars                  = varSetElems (idFreeVars binder)
+    lintBinder var | isId var  = lintIdBndr var $ \_ -> (return ())
+                  | otherwise = return ()
 \end{code}
 
 %************************************************************************
@@ -207,59 +277,46 @@ lintCoreExpr :: CoreExpr -> LintM OutType
 --     lintCoreExpr e subst = exprType (subst e)
 
 lintCoreExpr (Var var)
-  = do { checkIdInScope var 
-       ; applySubst (idType var) }
+  = do { checkL (not (var == oneTupleDataConId))
+                (ptext SLIT("Illegal one-tuple"))
+       ; var' <- lookupIdInScope var
+        ; return (idType var')
+        }
 
 lintCoreExpr (Lit lit)
   = return (literalType lit)
 
-lintCoreExpr (Note (Coerce to_ty from_ty) expr)
-  = do { expr_ty <- lintCoreExpr expr
-       ; to_ty <- lintTy to_ty
-       ; from_ty <- lintTy from_ty     
-       ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
-       ; return to_ty }
+--lintCoreExpr (Note (Coerce to_ty from_ty) expr)
+--  = do       { expr_ty <- lintCoreExpr expr
+--     ; to_ty <- lintTy to_ty
+--     ; from_ty <- lintTy from_ty     
+--     ; checkTys from_ty expr_ty (mkCoerceErr from_ty expr_ty)
+--     ; return to_ty }
+
+lintCoreExpr (Cast expr co)
+  = do { expr_ty <- lintCoreExpr expr
+       ; co' <- lintTy co
+       ; let (from_ty, to_ty) = coercionKind co'
+       ; checkTys from_ty expr_ty (mkCastErr from_ty expr_ty)
+       ; return to_ty }
 
 lintCoreExpr (Note other_note expr)
   = lintCoreExpr expr
 
 lintCoreExpr (Let (NonRec bndr rhs) body)
-  = do { lintSingleBinding NonRecursive (bndr,rhs)
+  = do { lintSingleBinding NotTopLevel NonRecursive (bndr,rhs)
        ; addLoc (BodyOfLetRec [bndr])
-                (addInScopeVars [bndr] (lintCoreExpr body)) }
+                (lintAndScopeId bndr $ \_ -> (lintCoreExpr body)) }
 
 lintCoreExpr (Let (Rec pairs) body) 
-  = addInScopeVars bndrs       $
-    do { mapM (lintSingleBinding Recursive) pairs      
+  = lintAndScopeIds bndrs      $ \_ ->
+    do { mapM (lintSingleBinding NotTopLevel Recursive) pairs  
        ; addLoc (BodyOfLetRec bndrs) (lintCoreExpr body) }
   where
     bndrs = map fst pairs
 
 lintCoreExpr e@(App fun (Type ty))
--- This is like 'let' for types
--- It's needed when dealing with desugarer output for GADTs. Consider
---   data T = forall a. T a (a->Int) Bool
---    f :: T -> ... -> 
---    f (T x f True)  = <e1>
---    f (T y g False) = <e2>
--- After desugaring we get
---     f t b = case t of 
---               T a (x::a) (f::a->Int) (b:Bool) ->
---                 case b of 
---                     True -> <e1>
---                     False -> (/\b. let y=x; g=f in <e2>) a
--- And for a reason I now forget, the ...<e2>... can mention a; so 
--- we want Lint to know that b=a.  Ugh.
---
--- I tried quite hard to make the necessity for this go away, by changing the 
--- desugarer, but the fundamental problem is this:
---     
---     T a (x::a) (y::Int) -> let fail::a = ...
---                            in (/\b. ...(case ... of       
---                                             True  -> x::b
---                                             False -> fail)
---                               ) a
--- Now the inner case look as though it has incompatible branches.
+-- See Note [Type let] above
   = addLoc (AnExpr e) $
     go fun [ty]
   where
@@ -267,12 +324,15 @@ lintCoreExpr e@(App fun (Type ty))
        = do { go fun (ty:tys) }
     go (Lam tv body) (ty:tys)
        = do  { checkL (isTyVar tv) (mkKindErrMsg tv ty)        -- Not quite accurate
-             ; ty' <- lintTy ty; 
-             ; checkKinds tv ty'
+             ; ty' <- lintTy ty 
+              ; let kind = tyVarKind tv
+              ; kind' <- lintTy kind
+              ; let tv' = setTyVarKind tv kind'
+             ; checkKinds tv' ty'              
                -- Now extend the substitution so we 
                -- take advantage of it in the body
-             ; addInScopeVars [tv] $
-               extendSubstL tv ty' $
+             ; addInScopeVars [tv'] $
+               extendSubstL tv' ty' $
                go body tys }
     go fun tys
        = do  { fun_ty <- lintCoreExpr fun
@@ -285,14 +345,13 @@ lintCoreExpr e@(App fun arg)
 
 lintCoreExpr (Lam var expr)
   = addLoc (LambdaBodyOf var) $
-    do { body_ty <- addInScopeVars [var] $
-                     lintCoreExpr expr
-       ; if isId var then do
-               { var_ty <- lintId var  
-               ; return (mkFunTy var_ty body_ty) }
-         else
-               return (mkForAllTy var body_ty)
-       }
+    lintBinders [var] $ \[var'] -> 
+    do { body_ty <- lintCoreExpr expr
+       ; if isId var' then 
+             return (mkFunTy (idType var') body_ty) 
+        else
+            return (mkForAllTy var' body_ty)
+       }
        -- The applySubst is needed to apply the subst to var
 
 lintCoreExpr e@(Case scrut var alt_ty alts) =
@@ -300,17 +359,22 @@ lintCoreExpr e@(Case scrut var alt_ty alts) =
   do { scrut_ty <- lintCoreExpr scrut
      ; alt_ty   <- lintTy alt_ty  
      ; var_ty   <- lintTy (idType var) 
-       -- Don't use lintId on var, because unboxed tuple is legitimate
+       -- Don't use lintIdBndr on var, because unboxed tuple is legitimate
 
-     ; checkTys var_ty scrut_ty (mkScrutMsg var scrut_ty)
+     ; subst <- getTvSubst 
+     ; checkTys var_ty scrut_ty (mkScrutMsg var var_ty scrut_ty subst)
 
      -- If the binder is an unboxed tuple type, don't put it in scope
-     ; let vars = if (isUnboxedTupleType (idType var)) then [] else [var]
-     ; addInScopeVars vars $
+     ; let scope = if (isUnboxedTupleType (idType var)) then 
+                       pass_var 
+                   else lintAndScopeId var
+     ; scope $ \_ ->
        do { -- Check the alternatives
             checkCaseAlts e scrut_ty alts
           ; mapM (lintCoreAlt scrut_ty alt_ty) alts
           ; return alt_ty } }
+  where
+    pass_var f = f var
 
 lintCoreExpr e@(Type ty)
   = addErrL (mkStrangeTyMsg e)
@@ -326,8 +390,8 @@ The basic version of these functions checks that the argument is a
 subtype of the required type, as one would expect.
 
 \begin{code}
-lintCoreArgs :: Type -> [CoreArg] -> LintM Type
-lintCoreArg  :: Type -> CoreArg   -> LintM Type
+lintCoreArgs :: OutType -> [CoreArg] -> LintM OutType
+lintCoreArg  :: OutType -> CoreArg   -> LintM OutType
 -- First argument has already had substitution applied to it
 \end{code}
 
@@ -344,16 +408,18 @@ lintCoreArg fun_ty a@(Type arg_ty) =
 lintCoreArg fun_ty arg = 
        -- Make sure function type matches argument
   do { arg_ty <- lintCoreExpr arg
-     ; let err = mkAppMsg fun_ty arg_ty arg
+     ; let err1 =  mkAppMsg fun_ty arg_ty arg
+           err2 = mkNonFunAppMsg fun_ty arg_ty arg
      ; case splitFunTy_maybe fun_ty of
         Just (arg,res) -> 
-          do { checkTys arg arg_ty err 
+          do { checkTys arg arg_ty err1
              ; return res }
-        _ -> addErrL err }
+        _ -> addErrL err2 }
 \end{code}
 
 \begin{code}
 -- Both args have had substitution applied
+lintTyApp :: OutType -> OutType -> LintM OutType
 lintTyApp ty arg_ty 
   = case splitForAllTy_maybe ty of
       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
@@ -363,22 +429,17 @@ lintTyApp ty arg_ty
                ; checkKinds tyvar arg_ty
                ; return (substTyWith [tyvar] [arg_ty] body) }
 
-lintTyApps fun_ty [] = return fun_ty
-
-lintTyApps fun_ty (arg_ty : arg_tys) = 
-  do { fun_ty' <- lintTyApp fun_ty arg_ty
-     ; lintTyApps fun_ty' arg_tys }
-
 checkKinds tyvar arg_ty
        -- 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.
-  = checkL (argty_kind `isSubKind` tyvar_kind)
+  = checkL (arg_kind `isSubKind` tyvar_kind)
           (mkKindErrMsg tyvar arg_ty)
   where
     tyvar_kind = tyVarKind tyvar
-    argty_kind = typeKind arg_ty
+    arg_kind | isCoVar tyvar = coercionKindPredTy arg_ty
+            | otherwise     = typeKind arg_ty
 \end{code}
 
 
@@ -444,50 +505,29 @@ lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) =
     lit_ty = literalType lit
 
 lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
-  | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty,
-    tycon == dataConTyCon con
-  = addLoc (CaseAlt alt) $
-    addInScopeVars args $      -- Put the args in scope before lintBinder,
-                               -- because the Ids mention the type variables
-    if isVanillaDataCon con then
-    do { addLoc (CasePat alt) $ do
-         { mapM lintBinder args 
-               -- FIX! Add check that all args are Ids.
-                -- Check the pattern
+  | isNewTyCon (dataConTyCon con) = addErrL (mkNewTyDataConAltMsg scrut_ty alt)
+  | Just (tycon, tycon_arg_tys) <- splitTyConApp_maybe scrut_ty
+  = addLoc (CaseAlt alt) $  do
+    {   -- First instantiate the universally quantified 
+       -- type variables of the data constructor
+       -- We've already check
+      checkL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
+    ; let con_payload_ty = applyTys (dataConRepType con) tycon_arg_tys
+
+       -- And now bring the new binders into scope
+    ; lintBinders args $ \ args -> do
+    { addLoc (CasePat alt) $ do
+         {    -- 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
 
-         ; con_type <- lintTyApps (dataConRepType con) tycon_arg_tys
-                 -- Can just map Var as we know that this is a vanilla datacon
-         ; con_result_ty <- lintCoreArgs con_type (map Var args)
+         ; con_result_ty <- lintCoreArgs con_payload_ty (varsToCoreExprs args)
          ; checkTys con_result_ty scrut_ty (mkBadPatMsg con_result_ty scrut_ty) 
          }
               -- Check the RHS
-       ; checkAltExpr rhs alt_ty }
-
-    else       -- GADT
-    do { let (tvs,ids) = span isTyVar args
-        ; subst <- getTvSubst 
-       ; let in_scope  = getTvInScope subst
-             subst_env = getTvSubstEnv subst
-        ; case coreRefineTys con tvs scrut_ty of {
-             Nothing          -> return () ;   -- Alternative is dead code
-             Just (refine, _) -> updateTvSubstEnv (composeTvSubst in_scope refine subst_env) $
-    do         { addLoc (CasePat alt) $ do
-         { tvs'     <- mapM lintTy (mkTyVarTys tvs)
-         ; con_type <- lintTyApps (dataConRepType con) tvs'
-         ; mapM lintBinder ids -- Lint Ids in the refined world
-         ; lintCoreArgs con_type (map Var ids)
-         }
-
-       ; let refined_alt_ty = substTy (mkTvSubst in_scope refine) alt_ty
-               -- alt_ty is already an OutType, so don't re-apply 
-               -- the current substitution.  But we must apply the
-               -- refinement so that the check in checkAltExpr is ok
-       ; checkAltExpr rhs refined_alt_ty
-    } } }
+    ; checkAltExpr rhs alt_ty } }
 
   | otherwise  -- Scrut-ty is wrong shape
   = addErrL (mkBadAltMsg scrut_ty alt)
@@ -500,24 +540,59 @@ lintCoreAlt scrut_ty alt_ty alt@(DataAlt con, args, rhs)
 %************************************************************************
 
 \begin{code}
-lintBinder :: Var -> LintM ()
-lintBinder var | isId var  = lintId var >> return ()
-              | otherwise = return ()
-
-lintId :: Var -> LintM OutType
+-- When we lint binders, we (one at a time and in order):
+--  1. Lint var types or kinds (possibly substituting)
+--  2. Add the binder to the in scope set, and if its a coercion var,
+--     we may extend the substitution to reflect its (possibly) new kind
+lintBinders :: [Var] -> ([Var] -> LintM a) -> LintM a
+lintBinders [] linterF = linterF []
+lintBinders (var:vars) linterF = lintBinder var $ \var' ->
+                                lintBinders vars $ \ vars' ->
+                                linterF (var':vars')
+
+lintBinder :: Var -> (Var -> LintM a) -> LintM a
+lintBinder var linterF
+  | isTyVar var = lint_ty_bndr
+  | otherwise   = lintIdBndr var linterF
+  where
+    lint_ty_bndr = do { lintTy (tyVarKind var)
+                     ; subst <- getTvSubst
+                     ; let (subst', tv') = substTyVarBndr subst var
+                     ; updateTvSubst subst' (linterF tv') }
+
+lintIdBndr :: Var -> (Var -> LintM a) -> LintM a
+-- Do substitution on the type of a binder and add the var with this 
+-- new type to the in-scope set of the second argument
 -- ToDo: lint its rules
-lintId id
+lintIdBndr id linterF 
   = do         { checkL (not (isUnboxedTupleType (idType id))) 
                 (mkUnboxedTupleMsg id)
                -- No variable can be bound to an unboxed tuple.
-       ; lintTy (idType id) }
+        ; lintAndScopeId id $ \id' -> linterF id'
+        }
+
+lintAndScopeIds :: [Var] -> ([Var] -> LintM a) -> LintM a
+lintAndScopeIds ids linterF 
+  = go ids
+  where
+    go []       = linterF []
+    go (id:ids) = do { lintAndScopeId id $ \id ->
+                           lintAndScopeIds ids $ \ids ->
+                           linterF (id:ids) }
+
+lintAndScopeId :: Var -> (Var -> LintM a) -> LintM a
+lintAndScopeId id linterF 
+  = do { ty <- lintTy (idType id)
+       ; let id' = Var.setIdType id ty
+       ; addInScopeVars [id'] $ (linterF id')
+       }
 
 lintTy :: InType -> LintM OutType
 -- Check the type, and apply the substitution to it
 -- ToDo: check the kind structure of the type
 lintTy ty 
   = do { ty' <- applySubst ty
-       ; mapM_ checkIdInScope (varSetElems (tyVarsOfType ty'))
+       ; mapM_ checkTyVarInScope (varSetElems (tyVarsOfType ty'))
        ; return ty' }
 \end{code}
 
@@ -538,6 +613,21 @@ newtype LintM a =
            Bag Message ->           -- Error messages so far
            (Maybe a, Bag Message) } -- Result and error messages (if any)
 
+{-     Note [Type substitution]
+       ~~~~~~~~~~~~~~~~~~~~~~~~
+Why do we need a type substitution?  Consider
+       /\(a:*). \(x:a). /\(a:*). id a x
+This is ill typed, because (renaming variables) it is really
+       /\(a:*). \(x:a). /\(b:*). id b x
+Hence, when checking an application, we can't naively compare x's type
+(at its binding site) with its expected type (at a use site).  So we
+rename type binders as we go, maintaining a substitution.
+
+The same substitution also supports let-type, current expressed as
+       (/\(a:*). body) ty
+Here we substitute 'ty' for 'a' in 'body', on the fly.
+-}
+
 instance Monad LintM where
   return x = LintM (\ loc subst errs -> (Just x, errs))
   fail err = LintM (\ loc subst errs -> (Nothing, addErr subst errs (text err) loc))
@@ -595,9 +685,9 @@ addInScopeVars :: [Var] -> LintM a -> LintM a
 addInScopeVars vars m = 
   LintM (\ loc subst errs -> unLintM m loc (extendTvInScope subst vars) errs)
 
-updateTvSubstEnv :: TvSubstEnv -> LintM a -> LintM a
-updateTvSubstEnv substenv m = 
-  LintM (\ loc subst errs -> unLintM m loc (setTvSubstEnv subst substenv) errs)
+updateTvSubst :: TvSubst -> LintM a -> LintM a
+updateTvSubst subst' m = 
+  LintM (\ loc subst errs -> unLintM m loc subst' errs)
 
 getTvSubst :: LintM TvSubst
 getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))
@@ -611,11 +701,19 @@ extendSubstL tv ty m
 \end{code}
 
 \begin{code}
-checkIdInScope :: Var -> LintM ()
-checkIdInScope id 
-  = do { checkL (not (id == oneTupleDataConId))
-               (ptext SLIT("Illegal one-tuple"))
-       ; checkInScope (ptext SLIT("is out of scope")) id }
+lookupIdInScope :: Id -> LintM Id
+lookupIdInScope id 
+  | not (mustHaveLocalBinding id)
+  = return id  -- An imported Id
+  | otherwise  
+  = do { subst <- getTvSubst
+       ; case lookupInScope (getTvInScope subst) id of
+               Just v  -> return v
+               Nothing -> do { addErrL out_of_scope
+                             ; return id } }
+  where
+    out_of_scope = ppr id <+> ptext SLIT("is out of scope")
+
 
 oneTupleDataConId :: Id        -- Should not happen
 oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
@@ -627,6 +725,9 @@ checkBndrIdInScope binder id
      msg = ptext SLIT("is out of scope inside info for") <+> 
           ppr binder
 
+checkTyVarInScope :: TyVar -> LintM ()
+checkTyVarInScope tv = checkInScope (ptext SLIT("is out of scope")) tv
+
 checkInScope :: SDoc -> Var -> LintM ()
 checkInScope loc_msg var =
  do { subst <- getTvSubst
@@ -698,12 +799,12 @@ mkCaseAltMsg e ty1 ty2
   = hang (text "Type of case alternatives not the same as the annotation on case:")
         4 (vcat [ppr ty1, ppr ty2, ppr e])
 
-mkScrutMsg :: Id -> Type -> Message
-mkScrutMsg var scrut_ty
+mkScrutMsg :: Id -> Type -> Type -> TvSubst -> Message
+mkScrutMsg var var_ty scrut_ty subst
   = 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]
-
+         text "Result binder type:" <+> ppr var_ty,--(idType var),
+         text "Scrutinee type:" <+> ppr scrut_ty,
+     hsep [ptext SLIT("Current TV subst"), ppr subst]]
 
 mkNonDefltMsg e
   = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
@@ -714,6 +815,14 @@ nonExhaustiveAltsMsg :: CoreExpr -> Message
 nonExhaustiveAltsMsg e
   = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
 
+mkBadConMsg :: TyCon -> DataCon -> Message
+mkBadConMsg tycon datacon
+  = vcat [
+       text "In a case alternative, data constructor isn't in scrutinee type:",
+       text "Scrutinee type constructor:" <+> ppr tycon,
+       text "Data con:" <+> ppr datacon
+    ]
+
 mkBadPatMsg :: Type -> Type -> Message
 mkBadPatMsg con_result_ty scrut_ty
   = vcat [
@@ -728,6 +837,13 @@ mkBadAltMsg scrut_ty alt
           text "Scrutinee type:" <+> ppr scrut_ty,
           text "Alternative:" <+> pprCoreAlt alt ]
 
+mkNewTyDataConAltMsg :: Type -> CoreAlt -> Message
+mkNewTyDataConAltMsg scrut_ty alt
+  = vcat [ text "Data alternative for newtype datacon",
+          text "Scrutinee type:" <+> ppr scrut_ty,
+          text "Alternative:" <+> pprCoreAlt alt ]
+
+
 ------------------------------------------------------
 --     Other error messages
 
@@ -738,6 +854,13 @@ mkAppMsg fun_ty arg_ty arg
              hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
              hang (ptext SLIT("Arg:")) 4 (ppr arg)]
 
+mkNonFunAppMsg :: Type -> Type -> CoreExpr -> Message
+mkNonFunAppMsg fun_ty arg_ty arg
+  = vcat [ptext SLIT("Non-function type in function position"),
+             hang (ptext SLIT("Fun type:")) 4 (ppr fun_ty),
+             hang (ptext SLIT("Arg type:")) 4 (ppr arg_ty),
+             hang (ptext SLIT("Arg:")) 4 (ppr arg)]
+
 mkKindErrMsg :: TyVar -> Type -> Message
 mkKindErrMsg tyvar arg_ty
   = vcat [ptext SLIT("Kinds don't match in type application:"),
@@ -769,13 +892,33 @@ mkRhsPrimMsg binder rhs
              hsep [ptext SLIT("Binder's type:"), ppr (idType binder)]
             ]
 
+mkStrictMsg :: Id -> Message
+mkStrictMsg binder
+  = vcat [hsep [ptext SLIT("Recursive or top-level binder has strict demand info:"),
+                    ppr binder],
+             hsep [ptext SLIT("Binder's demand info:"), ppr (idNewDemandInfo binder)]
+            ]
+
+mkArityMsg :: Id -> Message
+mkArityMsg binder
+  = vcat [hsep [ptext SLIT("Demand type has "),
+                     ppr (dmdTypeDepth dmd_ty),
+                     ptext SLIT(" arguments, rhs has "),
+                     ppr (idArity binder),
+                     ptext SLIT("arguments, "),
+                    ppr binder],
+             hsep [ptext SLIT("Binder's strictness signature:"), ppr dmd_ty]
+
+         ]
+           where (StrictSig dmd_ty) = idNewStrictness binder
+
 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)]]
 
-mkCoerceErr from_ty expr_ty
-  = vcat [ptext SLIT("From-type of Coerce differs from type of enclosed expression"),
+mkCastErr from_ty expr_ty
+  = vcat [ptext SLIT("From-type of Cast differs from type of enclosed expression"),
          ptext SLIT("From-type:") <+> ppr from_ty,
          ptext SLIT("Type of enclosed expr:") <+> ppr expr_ty
     ]