Improve error reporting in Core Lint
[ghc-hetmet.git] / ghc / compiler / coreSyn / CoreLint.lhs
index 02d6e87..be323be 100644 (file)
@@ -7,81 +7,73 @@
 module CoreLint (
        lintCoreBindings,
        lintUnfolding, 
-       beginPass, endPass
+       showPass, endPass
     ) where
 
 #include "HsVersions.h"
 
-import IO      ( hPutStr, hPutStrLn, stderr, stdout )
-
-import CmdLineOpts      ( opt_D_show_passes, opt_DoCoreLinting, opt_PprStyle_Debug )
 import CoreSyn
 import CoreFVs         ( idFreeVars )
-import CoreUtils       ( exprOkForSpeculation, coreBindsSize )
-
+import CoreUtils       ( findDefault, exprOkForSpeculation, coreBindsSize )
+import Unify           ( coreRefineTys )
 import Bag
-import Literal         ( Literal, literalType )
-import DataCon         ( DataCon, dataConRepType )
-import Id              ( mayHaveNoBinding, isDeadBinder )
-import Var             ( Var, Id, TyVar, idType, tyVarKind, isTyVar, isId )
+import Literal         ( literalType )
+import DataCon         ( dataConRepType, isVanillaDataCon, dataConTyCon, dataConWorkId )
+import TysWiredIn      ( tupleCon )
+import Var             ( Var, Id, TyVar, idType, tyVarKind, mustHaveLocalBinding )
 import VarSet
-import Subst           ( mkTyVarSubst, substTy )
-import Name            ( isLocallyDefined, getSrcLoc )
+import Name            ( getSrcLoc )
 import PprCore
-import ErrUtils                ( doIfSet, dumpIfSet, ghcExit, Message, 
-                         ErrMsg, addErrLocHdrLine, pprBagOfErrors )
-import PrimRep         ( PrimRep(..) )
-import SrcLoc          ( SrcLoc, noSrcLoc, isNoSrcLoc )
-import Type            ( Type, Kind, tyVarsOfType,
-                         splitFunTy_maybe, mkPiType, mkTyVarTy, unUsgTy,
+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, 
-                         splitAlgTyConApp_maybe,
-                         isUnboxedTupleType,
-                         hasMoreBoxityInfo
-                       )
-import TyCon           ( TyCon, isPrimTyCon, tyConDataCons )
-import BasicTypes      ( RecFlag(..), isNonRec )
+                         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 Outputable
 
-infixr 9 `thenL`, `seqL`
+#ifdef DEBUG
+import Util             ( notNull )
+#endif
+
+import Maybe
+
 \end{code}
 
 %************************************************************************
 %*                                                                     *
-\subsection{Start and end pass}
+\subsection{End pass}
 %*                                                                     *
 %************************************************************************
 
-@beginPass@ and @endPass@ don't really belong here, but it makes a convenient
+@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}
-beginPass :: String -> IO ()
-beginPass pass_name
-  | opt_D_show_passes
-  = hPutStrLn stderr ("*** " ++ pass_name)
-  | otherwise
-  = return ()
-
-
-endPass :: String -> Bool -> [CoreBind] -> IO [CoreBind]
-endPass pass_name dump_flag binds
+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 opt_D_show_passes then
-          hPutStrLn stdout ("    Result size = " ++ show (coreBindsSize binds))
-        else
-          return ()
+       debugTraceMsg dflags 2 $
+               (text "    Result size =" <+> int (coreBindsSize binds))
 
        -- Report verbosely, if required
-       dumpIfSet dump_flag pass_name
-                 (pprCoreBindings binds)
+       dumpIfSet_core dflags dump_flag pass_name (pprCoreBindings binds)
 
        -- Type check
-       lintCoreBindings pass_name binds
+       lintCoreBindings dflags pass_name binds
 
        return binds
 \end{code}
@@ -112,39 +104,35 @@ Outstanding issues:
     --
     -- Things are *not* OK if:
     --
-    -- * Unsaturated type app before specialisation has been done;
+    --  * Unsaturated type app before specialisation has been done;
     --
-    -- * Oversaturated type app after specialisation (eta reduction
+    --  * Oversaturated type app after specialisation (eta reduction
     --   may well be happening...);
 
 \begin{code}
-lintCoreBindings :: String -> [CoreBind] -> IO ()
+lintCoreBindings :: DynFlags -> String -> [CoreBind] -> IO ()
 
-lintCoreBindings whoDunnit binds
-  | not opt_DoCoreLinting
+lintCoreBindings dflags whoDunnit binds
+  | not (dopt Opt_DoCoreLinting dflags)
   = return ()
 
-lintCoreBindings whoDunnit binds
+lintCoreBindings dflags whoDunnit binds
   = case (initL (lint_binds binds)) of
-      Nothing       -> doIfSet opt_D_show_passes
-                       (hPutStr stderr ("*** Core Linted result of " ++ whoDunnit ++ "\n"))
-
+      Nothing       -> showPass dflags ("Core Linted result of " ++ whoDunnit)
       Just bad_news -> printDump (display bad_news)    >>
-                      ghcExit 1
+                      ghcExit dflags 1
   where
        -- 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
+                      mapM lint_bind binds 
 
-    lint_bind (Rec prs)                = mapL (lintSingleBinding Recursive) prs        `seqL`
-                                 returnL ()
+    lint_bind (Rec prs)                = mapM_ (lintSingleBinding Recursive) prs
     lint_bind (NonRec bndr rhs) = lintSingleBinding NonRecursive (bndr,rhs)
 
     display bad_news
-      = vcat [
-               text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
+      = vcat [  text ("*** Core Lint Errors: in result of " ++ whoDunnit ++ " ***"),
                bad_news,
                ptext SLIT("*** Offending Program ***"),
                pprCoreBindings binds,
@@ -165,16 +153,12 @@ We use this to check all unfoldings that come in from interfaces
 lintUnfolding :: SrcLoc
              -> [Var]          -- Treat these as in scope
              -> CoreExpr
-             -> Maybe Message          -- Nothing => OK
+             -> Maybe Message  -- Nothing => OK
 
 lintUnfolding locn vars expr
-  | not opt_DoCoreLinting
-  = Nothing
-
-  | otherwise
   = initL (addLoc (ImportedUnfolding locn) $
-            addInScopeVars vars             $
-            lintCoreExpr expr)
+          addInScopeVars vars             $
+          lintCoreExpr expr)
 \end{code}
 
 %************************************************************************
@@ -188,21 +172,17 @@ Check a core binding, returning the list of variables bound.
 \begin{code}
 lintSingleBinding rec_flag (binder,rhs)
   = addLoc (RhsOf binder) $
-
-       -- Check the rhs
-    lintCoreExpr rhs                           `thenL` \ ty ->
-
-       -- Check match to RHS type
-    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 the rhs 
+    do { ty <- lintCoreExpr rhs        
+       ; lintBinder binder -- Check match to RHS type
+       ; binder_ty <- applySubst binder_ty
+       ; checkTys binder_ty ty (mkRhsMsg binder ty)
+        -- Check (not isUnLiftedType) (also checks for bogus unboxed tuples)
+       ; checkL (not (isUnLiftedType binder_ty)
+            || (isNonRec rec_flag && exprOkForSpeculation rhs))
+          (mkRhsPrimMsg binder rhs)
         -- Check whether binder's specialisations contain any out-of-scope variables
-    mapL (checkBndrIdInScope binder) bndr_vars `seqL`
-    returnL ()
+       ; mapM_ (checkBndrIdInScope binder) bndr_vars }
          
        -- We should check the unfolding, if any, but this is tricky because
        -- the unfolding is a SimplifiableCoreExpr. Give up for now.
@@ -218,71 +198,119 @@ lintSingleBinding rec_flag (binder,rhs)
 %************************************************************************
 
 \begin{code}
-lintCoreExpr :: CoreExpr -> LintM Type
+type InType  = Type    -- Substitution not yet applied
+type OutType = Type    -- Substitution has been applied to this
+
+lintCoreExpr :: CoreExpr -> LintM OutType
+-- The returned type has the substitution from the monad 
+-- already applied to it:
+--     lintCoreExpr e subst = exprType (subst e)
 
-lintCoreExpr (Var var) = checkIdInScope var `seqL` returnL (idType var)
-lintCoreExpr (Lit lit) = returnL (literalType lit)
+lintCoreExpr (Var var)
+  = do { checkIdInScope var 
+       ; applySubst (idType var) }
+
+lintCoreExpr (Lit lit)
+  = return (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 (unUsgTy expr_ty) (mkCoerceErr from_ty expr_ty)   `seqL`
-    returnL to_ty
+  = 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 other_note expr)
   = lintCoreExpr expr
 
 lintCoreExpr (Let (NonRec bndr rhs) body)
-  = lintSingleBinding NonRecursive (bndr,rhs)  `seqL`
-    addLoc (BodyOfLetRec [bndr])
-          (addInScopeVars [bndr] (lintCoreExpr body))
+  = do { lintSingleBinding NonRecursive (bndr,rhs)
+       ; addLoc (BodyOfLetRec [bndr])
+                (addInScopeVars [bndr] (lintCoreExpr body)) }
 
-lintCoreExpr (Let (Rec pairs) body)
+lintCoreExpr (Let (Rec pairs) body) 
   = addInScopeVars bndrs       $
-    mapL (lintSingleBinding Recursive) pairs   `seqL`
-    addLoc (BodyOfLetRec bndrs) (lintCoreExpr body)
+    do { mapM (lintSingleBinding 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.
+  = addLoc (AnExpr e) $
+    go fun [ty]
+  where
+    go (App fun (Type ty)) tys
+       = 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'
+               -- Now extend the substitution so we 
+               -- take advantage of it in the body
+             ; addInScopeVars [tv] $
+               extendSubstL tv ty' $
+               go body tys }
+    go fun tys
+       = do  { fun_ty <- lintCoreExpr fun
+             ; lintCoreArgs fun_ty (map Type tys) }
+
 lintCoreExpr e@(App fun arg)
-  = lintCoreExpr fun   `thenL` \ ty ->
-    addLoc (AnExpr e)  $
-    lintCoreArg ty arg
+  = do { fun_ty <- lintCoreExpr fun
+       ; addLoc (AnExpr e) $
+          lintCoreArg fun_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)
+  = 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)
+       }
+       -- The applySubst is needed to apply the subst to var
+
+lintCoreExpr e@(Case scrut var alt_ty alts) =
+       -- Check the scrutinee
+  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
+
+     ; checkTys var_ty scrut_ty (mkScrutMsg var scrut_ty)
+
+     -- 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 $
+       do { -- Check the alternatives
+            checkCaseAlts e scrut_ty alts
+          ; mapM (lintCoreAlt scrut_ty alt_ty) alts
+          ; return alt_ty } }
 
 lintCoreExpr e@(Type ty)
   = addErrL (mkStrangeTyMsg e)
@@ -294,61 +322,64 @@ lintCoreExpr e@(Type ty)
 %*                                                                     *
 %************************************************************************
 
-The boolean argument indicates whether we should flag type
-applications to primitive types as being errors.
+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
-
-lintCoreArgs ty [] = returnL ty
-lintCoreArgs ty (a : args)
-  = lintCoreArg  ty a          `thenL` \ res ->
-    lintCoreArgs res args
+lintCoreArg  :: Type -> CoreArg   -> LintM Type
+-- First argument has already had substitution applied to it
 \end{code}
 
 \begin{code}
-lintCoreArg :: Type -> CoreArg -> LintM Type
-
-lintCoreArg ty a@(Type arg_ty)
-  = lintTy arg_ty                      `seqL`
-    lintTyApp ty arg_ty
-
-lintCoreArg fun_ty arg
-  = -- Make sure function type matches argument
-    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)
+lintCoreArgs ty [] = return ty
+lintCoreArgs ty (a : args) = 
+  do { res <- lintCoreArg ty a
+     ; lintCoreArgs res args }
+
+lintCoreArg fun_ty a@(Type arg_ty) = 
+  do { arg_ty <- lintTy arg_ty 
+     ; lintTyApp fun_ty 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
+     ; case splitFunTy_maybe fun_ty of
+        Just (arg,res) -> 
+          do { checkTys arg arg_ty err 
+             ; return res }
+        _ -> addErrL err }
 \end{code}
 
 \begin{code}
+-- Both args have had substitution applied
 lintTyApp ty arg_ty 
   = case splitForAllTy_maybe ty of
       Nothing -> addErrL (mkTyAppMsg ty arg_ty)
 
-      Just (tyvar,body) ->
-       let
-           tyvar_kind = tyVarKind tyvar
-           argty_kind = typeKind arg_ty
-       in
-       if argty_kind `hasMoreBoxityInfo` 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 (substTy (mkTyVarSubst [tyvar] [arg_ty]) body)
-       else
-           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}
+      Just (tyvar,body)
+        -> do  { checkL (isTyVar tyvar) (mkTyAppMsg 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)
+          (mkKindErrMsg tyvar arg_ty)
+  where
+    tyvar_kind = tyVarKind tyvar
+    argty_kind = typeKind arg_ty
+\end{code}
 
 
 %************************************************************************
@@ -358,87 +389,108 @@ lintTyApps fun_ty (arg_ty : arg_tys)
 %************************************************************************
 
 \begin{code}
-checkAllCasesCovered e ty [] = addErrL (mkNullAltsMsg e)
-
-checkAllCasesCovered e ty [(DEFAULT,_,_)] = nopL
+checkCaseAlts :: CoreExpr -> OutType -> [CoreAlt] -> LintM ()
+-- a) Check that the alts are non-empty
+-- b1) Check that the DEFAULT comes first, if it exists
+-- b2) Check that the others are in increasing order
+-- 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 = 
+  do { checkL (all non_deflt con_alts) (mkNonDefltMsg e)
+     ; checkL (increasing_tag con_alts) (mkNonIncreasingAltsMsg e)
+     ; checkL (isJust maybe_deflt || not is_infinite_ty)
+          (nonExhaustiveAltsMsg e) }
+  where
+    (con_alts, maybe_deflt) = findDefault alts
 
-checkAllCasesCovered e scrut_ty alts
-  = case splitTyConApp_maybe scrut_ty of {
-       Nothing -> addErrL (badAltsMsg e);
-       Just (tycon, tycon_arg_tys) ->
+       -- Check that successive alternatives have increasing tags 
+    increasing_tag (alt1 : rest@( alt2 : _)) = alt1 `ltAlt` alt2 && increasing_tag rest
+    increasing_tag other                    = True
 
-    if isPrimTyCon tycon then
-       checkL (hasDefault alts) (nonExhaustiveAltsMsg e)
-    else
-{-             No longer needed
-#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 }
+    non_deflt (DEFAULT, _, _) = False
+    non_deflt alt            = True
 
-hasDefault []                    = False
-hasDefault ((DEFAULT,_,_) : alts) = True
-hasDefault (alt                  : alts) = hasDefault alts
+    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
+checkAltExpr :: CoreExpr -> OutType -> LintM ()
+checkAltExpr expr ann_ty
+  = do { actual_ty <- lintCoreExpr expr 
+       ; checkTys actual_ty ann_ty (mkCaseAltMsg expr actual_ty ann_ty) }
+
+lintCoreAlt :: OutType                 -- Type of scrutinee
+            -> OutType          -- Type of the alternative
            -> CoreAlt
-           -> LintM Type               -- Type of alternatives
+           -> LintM ()
 
-lintCoreAlt scrut_ty alt@(DEFAULT, args, rhs)
-  = checkL (null args) (mkDefaultArgsMsg args) `seqL`
-    lintCoreExpr rhs
+lintCoreAlt scrut_ty alt_ty alt@(DEFAULT, args, rhs) = 
+  do { checkL (null args) (mkDefaultArgsMsg args)
+     ; checkAltExpr rhs alt_ty }
 
-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
+lintCoreAlt scrut_ty alt_ty alt@(LitAlt lit, args, rhs) = 
+  do { checkL (null args) (mkDefaultArgsMsg args)
+     ; checkTys lit_ty scrut_ty (mkBadPatMsg lit_ty scrut_ty)  
+     ; checkAltExpr rhs alt_ty } 
   where
     lit_ty = literalType lit
 
-lintCoreAlt scrut_ty alt@(DataAlt con, args, rhs)
-  = addLoc (CaseAlt alt) (
-
-    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 (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`
-
-       -- Check the RHS
-    lintCoreExpr rhs
-    ))
-  where
-    mk_arg b | isTyVar b = Type (mkTyVarTy b)
-            | otherwise = Var b
+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
+                -- 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)
+         ; 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 in_scope 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
+    } } }
+
+  | otherwise  -- Scrut-ty is wrong shape
+  = addErrL (mkBadAltMsg scrut_ty alt)
 \end{code}
 
 %************************************************************************
@@ -449,13 +501,24 @@ lintCoreAlt scrut_ty alt@(DataAlt con, args, rhs)
 
 \begin{code}
 lintBinder :: Var -> LintM ()
-lintBinder v = nopL
--- ToDo: lint its type
-
-lintTy :: Type -> LintM ()
-lintTy ty = mapL checkIdInScope (varSetElems (tyVarsOfType ty))        `seqL`
-           returnL ()
-       -- ToDo: check the kind structure of the type
+lintBinder var | isId var  = lintId var >> return ()
+              | otherwise = return ()
+
+lintId :: Var -> LintM OutType
+-- ToDo: lint its rules
+lintId id
+  = do         { checkL (not (isUnboxedTupleType (idType id))) 
+                (mkUnboxedTupleMsg id)
+               -- No variable can be bound to an unboxed tuple.
+       ; lintTy (idType 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'))
+       ; return ty' }
 \end{code}
 
     
@@ -466,91 +529,96 @@ lintTy ty = mapL checkIdInScope (varSetElems (tyVarsOfType ty))   `seqL`
 %************************************************************************
 
 \begin{code}
-type LintM a = [LintLocInfo]   -- Locations
-           -> IdSet            -- Local vars in scope
-           -> Bag ErrMsg       -- Error messages so far
-           -> (Maybe a, Bag ErrMsg)    -- Result and error messages (if any)
+newtype LintM a = 
+   LintM { unLintM :: 
+            [LintLocInfo] ->         -- Locations
+            TvSubst ->               -- Current type substitution; we also use this
+                                    -- to keep track of all the variables in scope,
+                                    -- both Ids and TyVars
+           Bag Message ->           -- Error messages so far
+           (Maybe a, Bag Message) } -- Result and error messages (if any)
+
+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))
+  m >>= k  = LintM (\ loc subst errs -> 
+                       let (res, errs') = unLintM m loc subst errs in
+                         case res of
+                           Just r -> unLintM (k r) loc subst errs'
+                           Nothing -> (Nothing, errs'))
 
 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
+  | CaseAlt CoreAlt    -- Case alternative
+  | CasePat CoreAlt    -- *Pattern* of the case alternative
   | AnExpr CoreExpr    -- Some expression
   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 \end{code}
 
+                 
 \begin{code}
-initL :: LintM a -> Maybe Message
+initL :: LintM a -> Maybe Message {- errors -}
 initL m
-  = case (m [] emptyVarSet emptyBag) of { (_, errs) ->
-    if isEmptyBag errs then
-       Nothing
-    else
-       Just (pprBagOfErrors errs)
-    }
-
-returnL :: a -> LintM a
-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 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 []
-mapL f (x:xs)
-  = f x        `thenL` \ r ->
-    mapL f xs  `thenL` \ rs ->
-    returnL (r:rs)
+  = case unLintM m [] emptyTvSubst emptyBag of
+      (_, errs) | isEmptyBag errs -> Nothing
+               | otherwise       -> Just (vcat (punctuate (text "") (bagToList errs)))
 \end{code}
 
 \begin{code}
 checkL :: Bool -> Message -> LintM ()
-checkL True  msg loc scope errs = (Nothing, errs)
-checkL False msg loc scope errs = (Nothing, addErr errs msg loc)
+checkL True  msg = return ()
+checkL False msg = addErrL msg
 
 addErrL :: Message -> LintM a
-addErrL msg loc scope errs = (Nothing, addErr errs msg loc)
-
-addErr :: Bag ErrMsg -> Message -> [LintLocInfo] -> Bag ErrMsg
+addErrL msg = LintM (\ loc subst errs -> (Nothing, addErr subst errs msg loc))
 
-addErr errs_so_far msg locs
-  = ASSERT (not (null locs))
+addErr :: TvSubst -> Bag Message -> Message -> [LintLocInfo] -> Bag Message
+addErr subst errs_so_far msg locs
+  = 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
+   context     | opt_PprStyle_Debug = vcat (reverse cxts) $$ cxt1 $$
+                                     ptext SLIT("Substitution:") <+> ppr subst
               | otherwise          = cxt1
  
-   mk_msg msg
-     | isNoSrcLoc loc = (loc, hang context 4 msg)
-     | otherwise      = addErrLocHdrLine loc context msg
+   mk_msg msg = mkLocMessage (mkSrcSpan loc loc) (context $$ msg)
 
 addLoc :: LintLocInfo -> LintM a -> LintM a
-addLoc extra_loc m loc scope errs
-  = m (extra_loc:loc) scope errs
+addLoc extra_loc m =
+  LintM (\ loc subst errs -> unLintM m (extra_loc:loc) subst errs)
 
 addInScopeVars :: [Var] -> LintM a -> LintM a
-addInScopeVars ids m loc scope errs
-  = m loc (scope `unionVarSet` mkVarSet ids) errs
+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)
+
+getTvSubst :: LintM TvSubst
+getTvSubst = LintM (\ loc subst errs -> (Just subst, errs))
+
+applySubst :: Type -> LintM Type
+applySubst ty = do { subst <- getTvSubst; return (substTy subst ty) }
+
+extendSubstL :: TyVar -> Type -> LintM a -> LintM a
+extendSubstL tv ty m
+  = LintM (\ loc subst errs -> unLintM m loc (extendTvSubst subst tv ty) errs)
 \end{code}
 
 \begin{code}
 checkIdInScope :: Var -> LintM ()
 checkIdInScope id 
-  = checkInScope (ptext SLIT("is out of scope")) id
+  = do { checkL (not (id == oneTupleDataConId))
+               (ptext SLIT("Illegal one-tuple"))
+       ; checkInScope (ptext SLIT("is out of scope")) id }
+
+oneTupleDataConId :: Id        -- Should not happen
+oneTupleDataConId = dataConWorkId (tupleCon Boxed 1)
 
 checkBndrIdInScope :: Var -> Var -> LintM ()
 checkBndrIdInScope binder id 
@@ -560,31 +628,18 @@ checkBndrIdInScope binder id
           ppr binder
 
 checkInScope :: SDoc -> Var -> LintM ()
-checkInScope loc_msg var loc scope errs
-  |  isLocallyDefined var 
-  && not (var `elemVarSet` scope)
-  && not (isId var && mayHaveNoBinding 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
-       -- of simplification, these dictionary constructors have been
-       -- inlined (from their UnfoldInfo) to CoCons.  Just between
-       -- desugaring and simplfication, though, they appear as naked, unbound
-       -- 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
-  = (Nothing, addErr errs (hsep [ppr var, loc_msg]) loc)
-  | otherwise
-  = (Nothing,errs)
+checkInScope loc_msg var =
+ do { subst <- getTvSubst
+    ; checkL (not (mustHaveLocalBinding var) || (var `isInScope` subst))
+             (hsep [ppr var, loc_msg]) }
 
 checkTys :: Type -> Type -> Message -> LintM ()
-checkTys ty1 ty2 msg loc scope errs
-  | ty1 == ty2 = (Nothing, errs)
-  | otherwise  = (Nothing, addErr errs msg loc)
+-- check ty2 is subtype of ty1 (ie, has same structure but usage
+-- annotations need only be consistent, not equal)
+-- Assumes ty1,ty2 are have alrady had the substitution applied
+checkTys ty1 ty2 msg = checkL (ty1 `coreEqType` ty2) msg
 \end{code}
 
-
 %************************************************************************
 %*                                                                     *
 \subsection{Error messages}
@@ -598,23 +653,30 @@ dumpLoc (RhsOf v)
 dumpLoc (LambdaBodyOf b)
   = (getSrcLoc b, brackets (ptext SLIT("in body of lambda with binder") <+> pp_binder b))
 
-dumpLoc (BodyOfLetRec bs)
+dumpLoc (BodyOfLetRec [])
+  = (noSrcLoc, brackets (ptext SLIT("In body of a letrec with no binders")))
+
+dumpLoc (BodyOfLetRec bs@(_:_))
   = ( getSrcLoc (head bs), brackets (ptext SLIT("in body of letrec with binders") <+> pp_binders bs))
 
 dumpLoc (AnExpr e)
   = (noSrcLoc, text "In the expression:" <+> ppr e)
 
 dumpLoc (CaseAlt (con, args, rhs))
-  = (noSrcLoc, text "In a case pattern:" <+> parens (ppr con <+> ppr args))
+  = (noSrcLoc, text "In a case alternative:" <+> parens (ppr con <+> pp_binders args))
+
+dumpLoc (CasePat (con, args, rhs))
+  = (noSrcLoc, text "In the pattern of a case alternative:" <+> parens (ppr con <+> pp_binders args))
 
 dumpLoc (ImportedUnfolding locn)
   = (locn, brackets (ptext SLIT("in an imported unfolding")))
 
-pp_binders :: [Id] -> SDoc
+pp_binders :: [Var] -> SDoc
 pp_binders bs = sep (punctuate comma (map pp_binder bs))
 
-pp_binder :: Id -> SDoc
-pp_binder b = hsep [ppr b, dcolon, ppr (idType b)]
+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}
 
 \begin{code}
@@ -631,10 +693,10 @@ 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)
+mkCaseAltMsg :: CoreExpr -> Type -> Type -> Message
+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
@@ -642,15 +704,15 @@ mkScrutMsg var scrut_ty
          text "Result binder type:" <+> ppr (idType var),
          text "Scrutinee type:" <+> ppr scrut_ty]
 
-badAltsMsg :: CoreExpr -> Message
-badAltsMsg e
-  = hang (text "Case statement scrutinee is not a data type:")
-        4 (ppr e)
+
+mkNonDefltMsg e
+  = hang (text "Case expression with DEFAULT not at the beginnning") 4 (ppr e)
+mkNonIncreasingAltsMsg e
+  = hang (text "Case expression with badly-ordered alternatives") 4 (ppr e)
 
 nonExhaustiveAltsMsg :: CoreExpr -> Message
 nonExhaustiveAltsMsg e
-  = hang (text "Case expression with non-exhaustive alternatives")
-        4 (ppr e)
+  = hang (text "Case expression with non-exhaustive alternatives") 4 (ppr e)
 
 mkBadPatMsg :: Type -> Type -> Message
 mkBadPatMsg con_result_ty scrut_ty
@@ -660,13 +722,21 @@ mkBadPatMsg con_result_ty scrut_ty
        text "Scrutinee type:" <+> ppr scrut_ty
     ]
 
+mkBadAltMsg :: Type -> CoreAlt -> Message
+mkBadAltMsg scrut_ty alt
+  = vcat [ text "Data alternative when scrutinee is not a tycon application",
+          text "Scrutinee type:" <+> ppr scrut_ty,
+          text "Alternative:" <+> pprCoreAlt alt ]
+
 ------------------------------------------------------
 --     Other error messages
 
-mkAppMsg fun arg
+mkAppMsg :: Type -> Type -> CoreExpr -> Message
+mkAppMsg fun_ty arg_ty 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("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