[project @ 1996-07-25 20:43:49 by partain]
[ghc-hetmet.git] / ghc / compiler / coreSyn / CoreLint.lhs
index f42a49e..99afabc 100644 (file)
@@ -1,5 +1,5 @@
 %
-% (c) The GRASP/AQUA Project, Glasgow University, 1993-1995
+% (c) The GRASP/AQUA Project, Glasgow University, 1993-1996
 %
 \section[CoreLint]{A ``lint'' pass to check for Core correctness}
 
 
 module CoreLint (
        lintCoreBindings,
-       lintUnfolding,
-       
-       PprStyle, CoreBinding, PlainCoreBinding(..), Id
+       lintUnfolding
     ) where
 
-IMPORT_Trace
+IMP_Ubiq()
+
+import CoreSyn
 
-import AbsPrel         ( typeOfPrimOp, mkFunTy, PrimOp(..), PrimKind
-                         IF_ATTACK_PRAGMAS(COMMA tagOf_PrimOp)
-                         IF_ATTACK_PRAGMAS(COMMA pprPrimOp)
-                       )
-import AbsUniType
 import Bag
-import BasicLit                ( typeOfBasicLit, BasicLit )
-import CoreSyn         ( pprCoreBinding ) -- ToDo: correctly
-import Id              ( getIdUniType, isNullaryDataCon, isBottomingId,
-                         getInstantiatedDataConSig, Id
-                         IF_ATTACK_PRAGMAS(COMMA bottomIsGuaranteed)
+import Kind            ( hasMoreBoxityInfo, Kind{-instance-} )
+import Literal         ( literalType, Literal{-instance-} )
+import Id              ( idType, isBottomingId, dataConRepType,
+                         dataConArgTys, GenId{-instances-},
+                         emptyIdSet, mkIdSet, intersectIdSets,
+                         unionIdSets, elementOfIdSet, SYN_IE(IdSet)
                        )
-import Maybes
-import Outputable
-import PlainCore
+import Maybes          ( catMaybes )
+import Name            ( isLocallyDefined, getSrcLoc, Name{-instance NamedThing-} )
+import Outputable      ( Outputable(..){-instance * []-} )
+import PprCore
+import PprStyle                ( PprStyle(..) )
+import PprType         ( GenType, GenTyVar, TyCon )
 import Pretty
+import PrimOp          ( primOpType, PrimOp(..) )
+import PrimRep         ( PrimRep(..) )
 import SrcLoc          ( SrcLoc )
-import UniqSet
-import Util
+import Type            ( mkFunTy,getFunTy_maybe,mkForAllTy,mkForAllTys,getForAllTy_maybe,
+                         getFunTyExpandingDicts_maybe,
+                         getForAllTyExpandingDicts_maybe,
+                         isPrimType,typeKind,instantiateTy,splitSigmaTy,
+                         mkForAllUsageTy,getForAllUsageTy,instantiateUsage,
+                         maybeAppDataTyConExpandingDicts, eqTy
+--                       ,expandTy -- ToDo:rm
+                       )
+import TyCon           ( isPrimTyCon )
+import TyVar           ( tyVarKind, GenTyVar{-instances-} )
+import Unique          ( Unique )
+import Usage           ( GenUsage, SYN_IE(Usage) )
+import Util            ( zipEqual, pprTrace, pprPanic, assertPanic, panic )
 
-infixr 9 `thenL`, `thenL_`, `thenMaybeL`, `thenMaybeL_`
+infixr 9 `thenL`, `seqL`, `thenMaybeL`, `seqMaybeL`
 \end{code}
 
-Checks for 
-       (a) type errors
-       (b) locally-defined variables used but not defined
-
-Doesn't check for out-of-scope type variables, because they can
-legitimately arise.  Eg
-\begin{verbatim}
-       k = /\a b -> \x::a y::b -> x
-       f = /\c -> \z::c -> k c w z (error w "foo")
-\end{verbatim}
-Here \tr{w} is just a free type variable.
-
 %************************************************************************
 %*                                                                     *
-\subsection{``lint'' for various constructs}
+\subsection[lintCoreBindings]{@lintCoreBindings@: Top-level interface}
 %*                                                                     *
 %************************************************************************
 
-@lintCoreBindings@ is the top-level interface function.
+Checks that a set of core bindings is well-formed.  The PprStyle and String
+just control what we print in the event of an error.  The Bool value
+indicates whether we have done any specialisation yet (in which case we do
+some extra checks).
+
+We check for
+       (a) type errors
+       (b) Out-of-scope type variables
+       (c) Out-of-scope local variables
+       (d) Ill-kinded types
+
+If we have done specialisation the we check that there are
+       (a) No top-level bindings of primitive (unboxed type)
+
+Outstanding issues:
+
+    --
+    -- Things are *not* OK if:
+    --
+    -- * Unsaturated type app before specialisation has been done;
+    --
+    -- * Oversaturated type app after specialisation (eta reduction
+    --   may well be happening...);
+    --
+    -- Note: checkTyApp is usually followed by a call to checkSpecTyApp.
+    --
 
 \begin{code}
-lintCoreBindings :: PprStyle -> String -> Bool -> [PlainCoreBinding] -> [PlainCoreBinding]
+lintCoreBindings
+       :: PprStyle -> String -> Bool -> [CoreBinding] -> [CoreBinding]
 
-lintCoreBindings sty whodunnit spec_done binds
-  = BSCC("CoreLint")
-    case (initL (lint_binds binds) spec_done) of
+lintCoreBindings sty whoDunnit spec_done binds
+  = case (initL (lint_binds binds) spec_done) of
       Nothing  -> binds
-      Just msg -> pprPanic "" (ppAboves [
-                       ppStr ("*** Core Lint Errors: in "++whodunnit++" ***"),
-                       msg sty,
-                       ppStr "*** Offending Program ***",
-                       ppAboves (map (pprCoreBinding sty pprBigCoreBinder pprTypedCoreBinder ppr) binds),
-                       ppStr "*** End of Offense ***"])
-    ESCC
+      Just msg ->
+       pprPanic "" (ppAboves [
+         ppStr ("*** Core Lint Errors: in " ++ whoDunnit ++ " ***"),
+         msg sty,
+         ppStr "*** Offending Program ***",
+         ppAboves (map (pprCoreBinding sty) binds),
+         ppStr "*** End of Offense ***"
+       ])
   where
-    lint_binds :: [PlainCoreBinding] -> LintM ()
-
     lint_binds [] = returnL ()
-    lint_binds (bind:binds) 
-      = lintCoreBinds bind             `thenL` \ binders ->
-       addInScopeVars binders (
-           lint_binds binds
-       )
+    lint_binds (bind:binds)
+      = lintCoreBinding bind `thenL` \binders ->
+       addInScopeVars binders (lint_binds binds)
 \end{code}
 
+%************************************************************************
+%*                                                                     *
+\subsection[lintUnfolding]{lintUnfolding}
+%*                                                                     *
+%************************************************************************
+
 We use this to check all unfoldings that come in from interfaces
 (it is very painful to catch errors otherwise):
+
 \begin{code}
-lintUnfolding :: SrcLoc -> PlainCoreExpr -> PlainCoreExpr
+lintUnfolding :: SrcLoc -> CoreExpr -> Maybe CoreExpr
 
 lintUnfolding locn expr
-  = case (initL (addLoc (ImportedUnfolding locn) (lintCoreExpr expr)) True{-pretend spec done-}) of
-      Nothing  -> expr
-      Just msg -> error ("ERROR: Type-incorrect unfolding from an interface:\n"++
-                       (ppShow 80 (ppAboves [msg PprForUser,
-                                       ppStr "*** Bad unfolding ***",
-                                       ppr PprDebug expr,
-                                       ppStr "*** End of bad unfolding ***"]))) 
+  = case
+      (initL (addLoc (ImportedUnfolding locn) (lintCoreExpr expr))
+       True{-pretend spec done-})
+    of
+      Nothing  -> Just expr
+      Just msg ->
+        pprTrace "WARNING: Discarded bad unfolding from interface:\n"
+       (ppAboves [msg PprForUser,
+                  ppStr "*** Bad unfolding ***",
+                  ppr PprDebug expr,
+                  ppStr "*** End unfolding ***"])
+       Nothing
 \end{code}
 
-\begin{code}
-lintCoreAtom :: PlainCoreAtom -> LintM (Maybe UniType)
+%************************************************************************
+%*                                                                     *
+\subsection[lintCoreBinding]{lintCoreBinding}
+%*                                                                     *
+%************************************************************************
 
-lintCoreAtom (CoLitAtom lit)       = returnL (Just (typeOfBasicLit lit))
-lintCoreAtom a@(CoVarAtom v)
-  = checkInScope v     `thenL_`
-    returnL (Just (getIdUniType v))
-\end{code}
+Check a core binding, returning the list of variables bound.
 
 \begin{code}
-lintCoreBinds :: PlainCoreBinding -> LintM [Id]                -- Returns the binders
-lintCoreBinds (CoNonRec binder rhs)
-  = lint_binds_help (binder,rhs)       `thenL_`
-    returnL [binder]
+lintCoreBinding :: CoreBinding -> LintM [Id]
 
-lintCoreBinds (CoRec pairs) 
+lintCoreBinding (NonRec binder rhs)
+  = lintSingleBinding (binder,rhs) `seqL` returnL [binder]
+
+lintCoreBinding (Rec pairs)
   = addInScopeVars binders (
-       mapL lint_binds_help pairs `thenL_`
-       returnL binders
+      mapL lintSingleBinding pairs `seqL` returnL binders
     )
   where
     binders = [b | (b,_) <- pairs]
 
-lint_binds_help (binder,rhs)
+lintSingleBinding (binder,rhs)
   = addLoc (RhsOf binder) (
        -- Check the rhs
-       lintCoreExpr rhs        `thenL` \ maybe_rhs_ty ->
+       lintCoreExpr rhs
 
+       `thenL` \maybe_ty ->
        -- Check match to RHS type
-       (case maybe_rhs_ty of
-         Nothing     -> returnL ()
-         Just rhs_ty -> checkTys (getIdUniType binder) 
-                                  rhs_ty 
-                                  (mkRhsMsg binder rhs_ty)
-       )                       `thenL_` 
-
-       -- Check not isPrimType
-       checkL (not (isPrimType (getIdUniType binder)))
-              (mkRhsPrimMsg binder rhs)
-                               `thenL_`
-
-       -- Check unfolding, if any
-       -- Blegh. This is tricky, because the unfolding is a SimplifiableCoreExpr
-       -- Give up for now
-
-       returnL ()
+       (case maybe_ty of
+         Nothing -> returnL ()
+         Just ty -> checkTys (idType binder) ty (mkRhsMsg binder ty))
+
+       `seqL`
+       -- Check (not isPrimType)
+       checkIfSpecDoneL (not (isPrimType (idType binder)))
+         (mkRhsPrimMsg binder rhs)
+
+       -- We should check the unfolding, if any, but this is tricky because
+       -- the unfolding is a SimplifiableCoreExpr. Give up for now.
     )
 \end{code}
 
+%************************************************************************
+%*                                                                     *
+\subsection[lintCoreExpr]{lintCoreExpr}
+%*                                                                     *
+%************************************************************************
+
 \begin{code}
-lintCoreExpr :: PlainCoreExpr -> LintM (Maybe UniType) -- Nothing if error found
-
-lintCoreExpr (CoVar var)
-  = checkInScope var   `thenL_`
-    returnL (Just ty)
-{-
-    case (splitForalls ty) of { (tyvars, _) ->
-    if null tyvars then
-       returnL (Just ty)
+lintCoreExpr :: CoreExpr -> LintM (Maybe Type) -- Nothing if error found
+
+lintCoreExpr (Var var) = checkInScope var `seqL` returnL (Just (idType var))
+lintCoreExpr (Lit lit) = returnL (Just (literalType lit))
+lintCoreExpr (SCC _ expr) = lintCoreExpr expr
+lintCoreExpr (Coerce _ ty expr)
+  = lintCoreExpr expr `seqL` returnL (Just ty)
+
+lintCoreExpr (Let binds body)
+  = lintCoreBinding binds `thenL` \binders ->
+    if (null binders) then
+       lintCoreExpr body  -- Can't add a new source location
     else
-       addErrL (mkUnappTyMsg var ty)   `thenL_`
-       returnL Nothing
-    }
--}
-  where
-    ty = getIdUniType var
-
-lintCoreExpr (CoLit lit)       = returnL (Just (typeOfBasicLit lit))
-lintCoreExpr (CoSCC label expr)        = lintCoreExpr expr
-
-lintCoreExpr (CoLet binds body)        
-  = lintCoreBinds binds                `thenL` \ binders ->
-    ASSERT(not (null binders))
-    addLoc (BodyOfLetRec binders) (
-    addInScopeVars binders (
-       lintCoreExpr body
-    ))
-
-lintCoreExpr e@(CoCon con tys args)
-  = checkTyApp con_ty tys (mkTyAppMsg e)    `thenMaybeL` \ con_tau_ty ->
-    -- Note: no call to checkSpecTyApp;
-    -- we allow CoCons applied to unboxed types to sail through
-    mapMaybeL lintCoreAtom args                            `thenL` \ maybe_arg_tys ->
-    case maybe_arg_tys of
-      Nothing      -> returnL Nothing
-      Just arg_tys  -> checkFunApp con_tau_ty arg_tys (mkFunAppMsg con_tau_ty arg_tys e)
-  where
-    con_ty = getIdUniType con
-
-lintCoreExpr e@(CoPrim op tys args)
-  = checkTyApp op_ty tys (mkTyAppMsg e)                `thenMaybeL` \ op_tau_ty ->
-    -- checkSpecTyApp e tys (mkSpecTyAppMsg e) `thenMaybeL_`
-    mapMaybeL lintCoreAtom args                        `thenL` \ maybe_arg_tys ->
-    case maybe_arg_tys of
-      Nothing -> returnL Nothing
-      Just arg_tys -> checkFunApp op_tau_ty arg_tys (mkFunAppMsg op_tau_ty arg_tys e)
-  where
-    op_ty = typeOfPrimOp op
+      addLoc (BodyOfLetRec binders)
+       (addInScopeVars binders (lintCoreExpr body))
+
+lintCoreExpr e@(Con con args)
+  = 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'
+
+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 (ValBinder var) expr)
+  = addLoc (LambdaBodyOf var)
+      (addInScopeVars [var]
+       (lintCoreExpr expr `thenMaybeL` \ty ->
+        returnL (Just (mkFunTy (idType var) ty))))
+
+lintCoreExpr (Lam (TyBinder tyvar) expr)
+  = lintCoreExpr expr `thenMaybeL` \ty ->
+    returnL (Just(mkForAllTy tyvar ty))
+    -- ToDo: Should add in-scope type variable at this point
+
+lintCoreExpr e@(Case scrut alts)
+ = lintCoreExpr scrut `thenMaybeL` \ty ->
+   lintCoreAlts alts ty
+\end{code}
 
-lintCoreExpr e@(CoApp fun arg)
-  = lce e []
-  where
-    lce (CoApp fun arg) arg_tys = lintCoreAtom arg     `thenMaybeL` \ arg_ty ->
-                                 lce fun (arg_ty:arg_tys)
+%************************************************************************
+%*                                                                     *
+\subsection[lintCoreArgs]{lintCoreArgs}
+%*                                                                     *
+%************************************************************************
+
+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 _ ty [] = returnL (Just ty)
+lintCoreArgs e ty (a : args)
+  = lintCoreArg  e ty  a `thenMaybeL` \ res ->
+    lintCoreArgs e res args
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+\subsection[lintCoreArg]{lintCoreArg}
+%*                                                                     *
+%************************************************************************
 
-    lce other_fun arg_tys = lintCoreExpr other_fun     `thenMaybeL` \ fun_ty ->
-                           checkFunApp fun_ty arg_tys (mkFunAppMsg fun_ty arg_tys e)
+\begin{code}
+lintCoreArg :: {-Bool ->-} CoreExpr -> Type -> CoreArg -> LintM (Maybe Type)
 
-lintCoreExpr e@(CoTyApp fun ty_arg)
-  = lce e []
+lintCoreArg e ty (LitArg lit)
+  = -- Make sure function type matches argument
+    case (getFunTyExpandingDicts_maybe False{-no peeking in newtypes-} ty) of
+      Just (arg,res) | (lit_ty `eqTy` 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
+    checkInScope v `seqL`
+    -- Make sure function type matches argument
+    case (getFunTyExpandingDicts_maybe False{-as above-} ty) of
+      Just (arg,res) | (var_ty `eqTy` arg) -> returnL(Just res)
+      _ -> addErrL (mkAppMsg ty var_ty e) `seqL` returnL Nothing
   where
-    lce (CoTyApp fun ty_arg) ty_args = lce fun (ty_arg:ty_args)
-
-    lce other_fun ty_args = lintCoreExpr other_fun     `thenMaybeL` \ fun_ty ->
-                           checkTyApp fun_ty ty_args (mkTyAppMsg e)
-                                                       `thenMaybeL` \ res_ty ->
-                           checkSpecTyApp other_fun ty_args (mkSpecTyAppMsg e)
-                                                       `thenMaybeL_`
-                           returnL (Just res_ty)
-
-lintCoreExpr (CoLam binders expr)
-  = ASSERT (not (null binders))
-    addLoc (LambdaBodyOf binders) (
-    addInScopeVars binders (
-       lintCoreExpr expr   `thenMaybeL` \ body_ty ->
-       returnL (Just (foldr (mkFunTy . getIdUniType) body_ty binders))
-    ))
-
-lintCoreExpr (CoTyLam tyvar expr)
-  = lintCoreExpr expr          `thenMaybeL` \ body_ty ->
-    case quantifyTy [tyvar] body_ty of
-      (_, ty) -> returnL (Just ty) -- not worried about the TyVarTemplates that come back
-
-lintCoreExpr e@(CoCase scrut alts)
- = lintCoreExpr scrut          `thenMaybeL` \ scrut_ty ->
-
-       -- Check that it is a data type
-   case getUniDataTyCon_maybe scrut_ty of
-       Nothing -> addErrL (mkCaseDataConMsg e) `thenL_`
-                  returnL Nothing
-       Just (tycon, _, _)
-               -> lintCoreAlts alts scrut_ty tycon
-
-lintCoreAlts :: PlainCoreCaseAlternatives
-            -> UniType                 -- Type of scrutinee
-            -> TyCon                   -- TyCon pinned on the case
-            -> LintM (Maybe UniType)   -- Type of alternatives
-
-lintCoreAlts alts scrut_ty case_tycon
-  = (case alts of
-        CoAlgAlts alg_alts deflt ->  
-          chk_prim_type False case_tycon       `thenL_`
-          chk_non_abstract_type case_tycon     `thenL_`
-          mapL (lintAlgAlt scrut_ty) alg_alts  `thenL` \ maybe_alt_tys ->
-          lintDeflt deflt scrut_ty             `thenL` \ maybe_deflt_ty ->
-          returnL (maybe_deflt_ty : maybe_alt_tys)
-
-        CoPrimAlts prim_alts deflt -> 
-          chk_prim_type True case_tycon         `thenL_`
-          mapL (lintPrimAlt scrut_ty) prim_alts `thenL` \ maybe_alt_tys ->
-          lintDeflt deflt scrut_ty              `thenL` \ maybe_deflt_ty ->
-          returnL (maybe_deflt_ty : maybe_alt_tys)
-    )                                           `thenL` \ maybe_result_tys ->
-        -- Check the result types
-    case catMaybes (maybe_result_tys) of
+    var_ty = idType v
+
+lintCoreArg e ty a@(TyArg arg_ty)
+  = -- ToDo: Check that ty is well-kinded and has no unbound tyvars
+    checkIfSpecDoneL (not (isPrimType arg_ty)) (mkSpecTyAppMsg a)
+    `seqL`
+    case (getForAllTyExpandingDicts_maybe ty) of
+      Nothing -> addErrL (mkTyAppMsg SLIT("Illegal") ty arg_ty e) `seqL` returnL Nothing
+
+      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(Just(instantiateTy [(tyvar,arg_ty)] body))
+       else
+           pprTrace "lintCoreArg:kinds:" (ppCat [ppr PprDebug tyvar_kind, ppr PprDebug argty_kind]) $
+           addErrL (mkTyAppMsg SLIT("Kinds not right in") ty arg_ty e) `seqL` returnL Nothing
+       
+lintCoreArg e ty (UsageArg u)
+  = -- ToDo: Check that usage has no unbound usage variables
+    case (getForAllUsageTy ty) of
+      Just (uvar,bounds,body) ->
+        -- ToDo: Check argument satisfies bounds
+        returnL(Just(panic "lintCoreArg:instantiateUsage uvar u body"))
+      _ -> addErrL (mkUsageAppMsg ty u e) `seqL` returnL Nothing
+\end{code}
+
+%************************************************************************
+%*                                                                     *
+\subsection[lintCoreAlts]{lintCoreAlts}
+%*                                                                     *
+%************************************************************************
+
+\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 `thenL_`
+      (first_ty:tys) -> mapL check tys `seqL`
                        returnL (Just first_ty)
        where
-         check ty = checkTys first_ty ty (mkCaseAltMsg alts)
-  where
-    chk_prim_type prim_required tycon
-      = if (isPrimTyCon tycon == prim_required) then
-           returnL ()
-       else
-           addErrL (mkCasePrimMsg prim_required tycon)
-
-    chk_non_abstract_type tycon
-      = case (getTyConFamilySize tycon) of
-         Nothing -> addErrL (mkCaseAbstractMsg tycon)
-         Just  _ -> returnL ()
+         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 getUniDataTyCon_maybe scrut_ty of
-      Nothing -> 
+lintAlgAlt scrut_ty {-tycon-ToDo: use it!-} (con,args,rhs)
+  = (case maybeAppDataTyConExpandingDicts scrut_ty of
+      Nothing ->
         addErrL (mkAlgAltMsg1 scrut_ty)
       Just (tycon, tys_applied, cons) ->
         let
-          (_, arg_tys, _) = getInstantiatedDataConSig con tys_applied
+          arg_tys = dataConArgTys con tys_applied
         in
-        checkL (con `elem` cons) (mkAlgAltMsg2 scrut_ty con) `thenL_`
-        checkL (length arg_tys == length args) (mkAlgAltMsg3 con args) 
-                                                                `thenL_`
-        mapL check (arg_tys `zipEqual` args)                    `thenL_`
+        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 ()
-    )                                                           `thenL_`
+    )                                                           `seqL`
     addInScopeVars args        (
         lintCoreExpr rhs
     )
   where
-    check (ty, arg) = checkTys ty (getIdUniType arg) (mkAlgAltMsg4 ty arg)
+    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
@@ -308,18 +382,15 @@ lintAlgAlt scrut_ty (con,args,rhs)
     elem _ []      = False
     elem x (y:ys)   = x==y || elem x ys
 
-lintPrimAlt scrut_ty alt@(lit,rhs)
- = checkTys (typeOfBasicLit lit) scrut_ty (mkPrimAltMsg alt)   `thenL_`
+lintPrimAlt ty alt@(lit,rhs)
+ = checkTys (literalType lit) ty (mkPrimAltMsg alt) `seqL`
    lintCoreExpr rhs
-   
-lintDeflt CoNoDefault scrut_ty = returnL Nothing
-lintDeflt deflt@(CoBindDefault binder rhs) scrut_ty 
-  = checkTys (getIdUniType binder) scrut_ty (mkDefltMsg deflt) `thenL_`
-    addInScopeVars [binder] (
-       lintCoreExpr rhs
-    )
-\end{code}
 
+lintDeflt NoDefault _ = returnL Nothing
+lintDeflt deflt@(BindDefault binder rhs) ty
+  = checkTys (idType binder) ty (mkDefltMsg deflt) `seqL`
+    addInScopeVars [binder] (lintCoreExpr rhs)
+\end{code}
 
 %************************************************************************
 %*                                                                     *
@@ -330,7 +401,7 @@ lintDeflt deflt@(CoBindDefault binder rhs) scrut_ty
 \begin{code}
 type LintM a = Bool            -- True <=> specialisation has been done
            -> [LintLocInfo]    -- Locations
-           -> UniqSet Id       -- Local vars in scope
+           -> IdSet            -- Local vars in scope
            -> Bag ErrMsg       -- Error messages so far
            -> (a, Bag ErrMsg)  -- Result and error messages (if any)
 
@@ -338,7 +409,7 @@ type ErrMsg = PprStyle -> Pretty
 
 data LintLocInfo
   = RhsOf Id           -- The variable bound
-  | LambdaBodyOf [Id]  -- The lambda-binder
+  | LambdaBodyOf Id    -- The lambda-binder
   | BodyOfLetRec [Id]  -- One of the binders
   | ImportedUnfolding SrcLoc -- Some imported unfolding (ToDo: say which)
 
@@ -346,9 +417,9 @@ instance Outputable LintLocInfo where
     ppr sty (RhsOf v)
       = ppBesides [ppr sty (getSrcLoc v), ppStr ": [RHS of ", pp_binders sty [v], ppStr "]"]
 
-    ppr sty (LambdaBodyOf bs)
-      = ppBesides [ppr sty (getSrcLoc (head bs)),
-               ppStr ": [in body of lambda with binders ", pp_binders sty bs, ppStr "]"]
+    ppr sty (LambdaBodyOf b)
+      = ppBesides [ppr sty (getSrcLoc b),
+               ppStr ": [in body of lambda with binder ", pp_binder sty b, ppStr "]"]
 
     ppr sty (BodyOfLetRec bs)
       = ppBesides [ppr sty (getSrcLoc (head bs)),
@@ -358,17 +429,16 @@ instance Outputable LintLocInfo where
       = ppBeside (ppr sty locn) (ppStr ": [in an imported unfolding]")
 
 pp_binders :: PprStyle -> [Id] -> Pretty
-pp_binders sty bs
-  = ppInterleave ppComma (map pp_binder bs)
-  where
-    pp_binder b
-      = ppCat [ppr sty b, ppStr "::", ppr sty (getIdUniType b)]
+pp_binders sty bs = ppInterleave ppComma (map (pp_binder sty) bs)
+
+pp_binder :: PprStyle -> Id -> Pretty
+pp_binder sty b = ppCat [ppr sty b, ppStr "::", ppr sty (idType b)]
 \end{code}
 
 \begin{code}
 initL :: LintM a -> Bool -> Maybe ErrMsg
 initL m spec_done
-  = case (m spec_done [] emptyUniqSet emptyBag) of { (_, errs) ->
+  = case (m spec_done [] emptyIdSet emptyBag) of { (_, errs) ->
     if isEmptyBag errs then
        Nothing
     else
@@ -382,12 +452,12 @@ returnL r spec loc scope errs = (r, errs)
 
 thenL :: LintM a -> (a -> LintM b) -> LintM b
 thenL m k spec loc scope errs
-  = case m spec loc scope errs of 
+  = case m spec loc scope errs of
       (r, errs') -> k r spec loc scope errs'
 
-thenL_ :: LintM a -> LintM b -> LintM b
-thenL_ m k spec loc scope errs
-  = case m spec loc scope errs of 
+seqL :: LintM a -> LintM b -> LintM b
+seqL m k spec loc scope errs
+  = case m spec loc scope errs of
       (_, errs') -> k spec loc scope errs'
 
 thenMaybeL :: LintM (Maybe a) -> (a -> LintM (Maybe b)) -> LintM (Maybe b)
@@ -396,8 +466,8 @@ thenMaybeL m k spec loc scope errs
       (Nothing, errs2) -> (Nothing, errs2)
       (Just r,  errs2) -> k r spec loc scope errs2
 
-thenMaybeL_ :: LintM (Maybe a) -> LintM (Maybe b) -> LintM (Maybe b)
-thenMaybeL_ m k spec loc scope errs
+seqMaybeL :: LintM (Maybe a) -> LintM (Maybe b) -> LintM (Maybe b)
+seqMaybeL m k spec loc scope errs
   = case m spec loc scope errs of
       (Nothing, errs2) -> (Nothing, errs2)
       (Just _,  errs2) -> k spec loc scope errs2
@@ -423,6 +493,14 @@ checkL :: Bool -> ErrMsg -> LintM ()
 checkL True  msg spec loc scope errs = ((), errs)
 checkL False msg spec loc scope errs = ((), addErr errs msg loc)
 
+checkIfSpecDoneL :: Bool -> ErrMsg -> LintM ()
+checkIfSpecDoneL True  msg spec  loc scope errs = ((), errs)
+checkIfSpecDoneL False msg True  loc scope errs = ((), addErr errs msg loc)
+checkIfSpecDoneL False msg False loc scope errs = ((), errs)
+
+addErrIfL pred spec
+  = if pred then addErrL spec else returnL ()
+
 addErrL :: ErrMsg -> LintM ()
 addErrL msg spec loc scope errs = ((), addErr errs msg loc)
 
@@ -445,153 +523,94 @@ addInScopeVars ids m spec loc scope errs
     -- For now, it's just a "trace"; we may make
     -- a real error out of it...
     let
-       new_set = mkUniqSet ids
+       new_set = mkIdSet ids
 
-       shadowed = scope `intersectUniqSets` new_set
+--     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 PprDebug (uniqSetToList shadowed))) (
-    m spec loc (scope `unionUniqSets` new_set) errs
+    m spec loc (scope `unionIdSets` new_set) errs
 --  )
 \end{code}
 
 \begin{code}
-checkTyApp :: UniType
-          -> [UniType]
-          -> ErrMsg
-          -> LintM (Maybe UniType)
-
-checkTyApp forall_ty ty_args msg spec_done loc scope errs
-  = if (not spec_done && n_ty_args /= n_tyvars)
-    || (spec_done     && n_ty_args  > n_tyvars)
-    --
-    -- Things are *not* OK if:
-    --
-    -- * Unsaturated type app before specialisation has been done;
-    --
-    -- * Oversaturated type app after specialisation (eta reduction
-    --   may well be happening...);
-    --
-    -- Note: checkTyApp is usually followed by a call to checkSpecTyApp.
-    --
-    then (Nothing,     addErr errs msg loc)
-    else (Just res_ty, errs)
-  where
-    (tyvars, rho_ty) = splitForalls forall_ty
-    n_tyvars = length tyvars
-    n_ty_args = length ty_args
-    leftover_tyvars = drop n_ty_args tyvars
-    inst_env = tyvars `zip` ty_args
-    res_ty = mkForallTy leftover_tyvars (instantiateTy inst_env rho_ty)
-\end{code}
-
-\begin{code}
-checkSpecTyApp :: PlainCoreExpr -> [UniType] -> ErrMsg -> LintM (Maybe ())
-
-checkSpecTyApp expr ty_args msg spec_done loc scope errs
-  = if spec_done
-    && any isUnboxedDataType ty_args
-    && not (an_application_of_error expr)
-    then (Nothing, addErr errs msg loc)
-    else (Just (), errs)
-  where
-     -- always safe (but maybe unfriendly) to say "False"
-    an_application_of_error (CoVar id) | isBottomingId id = True
-    an_application_of_error _ = False
-\end{code}
-
-\begin{code}
-checkFunApp :: UniType                 -- The function type
-           -> [UniType]        -- The arg type(s)
-           -> ErrMsg           -- Error messgae
-           -> LintM (Maybe UniType)    -- The result type
-
-checkFunApp fun_ty arg_tys msg spec loc scope errs
-  = cfa res_ty expected_arg_tys arg_tys
-  where
-    (expected_arg_tys, res_ty) = splitTyArgs fun_ty
-
-    cfa res_ty expected []     -- Args have run out; that's fine
-       = (Just (glueTyArgs expected res_ty), errs)
-
-    cfa res_ty [] arg_tys      -- Expected arg tys ran out first; maybe res_ty is a 
-                               -- dictionary type which is actually a function?
-       = case splitTyArgs (unDictifyTy res_ty) of
-           ([], _)                 -> (Nothing, addErr errs msg loc)   -- Too many args
-           (new_expected, new_res) -> cfa new_res new_expected arg_tys
-
-    cfa res_ty (expected_arg_ty:expected_arg_tys) (arg_ty:arg_tys)
-       = case (cmpUniType True{-properly-} expected_arg_ty arg_ty) of
-               EQ_ -> cfa res_ty expected_arg_tys arg_tys
-               other -> (Nothing, addErr errs msg loc)                 -- Arg mis-match
-\end{code}
-
-\begin{code}
 checkInScope :: Id -> LintM ()
 checkInScope id spec loc scope errs
-  = if isLocallyDefined id && not (id `elementOfUniqSet` scope) then
-       ((), addErr errs (\ sty -> ppCat [ppr sty id, ppStr "is out of scope"]) loc)
+  = let
+       id_name = getName id
+    in
+    if isLocallyDefined id_name && not (id `elementOfIdSet` scope) then
+      ((),addErr errs (\sty -> ppCat [ppr sty id, ppStr "is out of scope"]) loc)
     else
-       ((), errs)
+      ((),errs)
 
-checkTys :: UniType -> UniType -> ErrMsg -> LintM ()
+checkTys :: Type -> Type -> ErrMsg -> LintM ()
 checkTys ty1 ty2 msg spec loc scope errs
-  = case (cmpUniType True{-properly-} ty1 ty2) of
-       EQ_   -> ((), errs)
-       other -> ((), addErr errs msg loc)
+  = if ty1 `eqTy` ty2 then ((), errs) else ((), addErr errs msg loc)
 \end{code}
 
 \begin{code}
-mkCaseAltMsg :: PlainCoreCaseAlternatives -> ErrMsg
+mkCaseAltMsg :: CoreCaseAlts -> ErrMsg
 mkCaseAltMsg alts sty
-  = ppAbove (ppStr "In some case alternatives, type of alternatives not all same:")
+  = ppAbove (ppStr "Type of case alternatives not the same:")
            (ppr sty alts)
 
-mkCaseDataConMsg :: PlainCoreExpr -> ErrMsg
+mkCaseDataConMsg :: CoreExpr -> ErrMsg
 mkCaseDataConMsg expr sty
-  = ppAbove (ppStr "A case scrutinee not a type-constructor type:")
+  = ppAbove (ppStr "A case scrutinee not of data constructor type:")
            (pp_expr sty expr)
 
-mkCasePrimMsg :: Bool -> TyCon -> ErrMsg
-mkCasePrimMsg True tycon sty
+mkCaseNotPrimMsg :: TyCon -> ErrMsg
+mkCaseNotPrimMsg tycon sty
   = ppAbove (ppStr "A primitive case on a non-primitive type:")
            (ppr sty tycon)
-mkCasePrimMsg False tycon sty
+
+mkCasePrimMsg :: TyCon -> ErrMsg
+mkCasePrimMsg tycon sty
   = ppAbove (ppStr "An algebraic case on a primitive type:")
            (ppr sty tycon)
 
 mkCaseAbstractMsg :: TyCon -> ErrMsg
 mkCaseAbstractMsg tycon sty
-  = ppAbove (ppStr "An algebraic case on an abstract type:")
+  = ppAbove (ppStr "An algebraic case on some weird type:")
            (ppr sty tycon)
 
-mkDefltMsg :: PlainCoreCaseDefault -> ErrMsg
+mkDefltMsg :: CoreCaseDefault -> ErrMsg
 mkDefltMsg deflt sty
-  = ppAbove (ppStr "Binder in default case of a case expression doesn't match type of scrutinee:")
+  = ppAbove (ppStr "Binder in case default doesn't match type of scrutinee:")
            (ppr sty deflt)
 
-mkFunAppMsg :: UniType -> [UniType] -> PlainCoreExpr -> ErrMsg
-mkFunAppMsg fun_ty arg_tys expr sty
-  = ppAboves [ppStr "In a function application, function type doesn't match arg types:",
-             ppHang (ppStr "Function type:") 4 (ppr sty fun_ty),
-             ppHang (ppStr "Arg types:") 4 (ppAboves (map (ppr sty) arg_tys)),
+mkAppMsg :: Type -> Type -> CoreExpr -> ErrMsg
+mkAppMsg fun arg expr sty
+  = ppAboves [ppStr "Argument value doesn't match argument type:",
+             ppHang (ppStr "Fun type:") 4 (ppr sty fun),
+             ppHang (ppStr "Arg type:") 4 (ppr sty arg),
+             ppHang (ppStr "Expression:") 4 (pp_expr sty expr)]
+
+mkTyAppMsg :: FAST_STRING -> Type -> Type -> CoreExpr -> ErrMsg
+mkTyAppMsg msg ty arg expr sty
+  = ppAboves [ppCat [ppPStr msg, ppStr "type application:"],
+             ppHang (ppStr "Exp type:")   4 (ppr sty ty),
+             ppHang (ppStr "Arg type:")   4 (ppr sty arg),
              ppHang (ppStr "Expression:") 4 (pp_expr sty expr)]
 
-mkUnappTyMsg :: Id -> UniType -> ErrMsg
-mkUnappTyMsg var ty sty
-  = ppAboves [ppStr "Variable has a for-all type, but isn't applied to any types.",
-             ppBeside (ppStr "Var:      ") (ppr sty var),
-             ppBeside (ppStr "Its type: ") (ppr sty ty)]
+mkUsageAppMsg :: Type -> Usage -> CoreExpr -> ErrMsg
+mkUsageAppMsg ty u expr sty
+  = ppAboves [ppStr "Illegal usage application:",
+             ppHang (ppStr "Exp type:") 4 (ppr sty ty),
+             ppHang (ppStr "Usage exp:") 4 (ppr sty u),
+             ppHang (ppStr "Expression:") 4 (pp_expr sty expr)]
 
-mkAlgAltMsg1 :: UniType -> ErrMsg
+mkAlgAltMsg1 :: Type -> ErrMsg
 mkAlgAltMsg1 ty sty
   = ppAbove (ppStr "In some case statement, type of scrutinee is not a data type:")
            (ppr sty ty)
+--         (ppAbove (ppr sty ty) (ppr sty (expandTy ty))) -- ToDo: rm
 
-mkAlgAltMsg2 :: UniType -> Id -> ErrMsg
+mkAlgAltMsg2 :: Type -> Id -> ErrMsg
 mkAlgAltMsg2 ty con sty
   = ppAboves [
        ppStr "In some algebraic case alternative, constructor is not a constructor of scrutinee type:",
@@ -607,7 +626,7 @@ mkAlgAltMsg3 con alts sty
        ppr sty alts
     ]
 
-mkAlgAltMsg4 :: UniType -> Id -> ErrMsg
+mkAlgAltMsg4 :: Type -> Id -> ErrMsg
 mkAlgAltMsg4 ty arg sty
   = ppAboves [
        ppStr "In some algebraic case alternative, type of argument doesn't match data constructor:",
@@ -615,37 +634,34 @@ mkAlgAltMsg4 ty arg sty
        ppr sty arg
     ]
 
-mkPrimAltMsg :: (BasicLit, PlainCoreExpr) -> ErrMsg
+mkPrimAltMsg :: (Literal, CoreExpr) -> ErrMsg
 mkPrimAltMsg alt sty
-  = ppAbove (ppStr "In a primitive case alternative, type of literal doesn't match type of scrutinee:")
+  = ppAbove
+    (ppStr "In a primitive case alternative, type of literal doesn't match type of scrutinee:")
            (ppr sty alt)
 
-mkRhsMsg :: Id -> UniType -> ErrMsg
+mkRhsMsg :: Id -> Type -> ErrMsg
 mkRhsMsg binder ty sty
-  = ppAboves [ppCat [ppStr "The type of this binder doesn't match the type of its RHS:", 
-                    ppr sty binder],
-             ppCat [ppStr "Binder's type:", ppr sty (getIdUniType binder)],
-             ppCat [ppStr "Rhs type:", ppr sty ty]
-            ]
+  = ppAboves
+    [ppCat [ppStr "The type of this binder doesn't match the type of its RHS:",
+           ppr sty binder],
+     ppCat [ppStr "Binder's type:", ppr sty (idType binder)],
+     ppCat [ppStr "Rhs type:", ppr sty ty]]
 
-mkRhsPrimMsg :: Id -> PlainCoreExpr -> ErrMsg
+mkRhsPrimMsg :: Id -> CoreExpr -> ErrMsg
 mkRhsPrimMsg binder rhs sty
-  = ppAboves [ppCat [ppStr "The type of this binder is primitive:", 
+  = ppAboves [ppCat [ppStr "The type of this binder is primitive:",
                     ppr sty binder],
-             ppCat [ppStr "Binder's type:", ppr sty (getIdUniType binder)]
+             ppCat [ppStr "Binder's type:", ppr sty (idType binder)]
             ]
 
-mkTyAppMsg :: PlainCoreExpr -> ErrMsg
-mkTyAppMsg expr sty
-  = ppAboves [ppStr "In a type application, either the function's type doesn't match",
-             ppStr "the argument types, or an argument type is primitive:",
-             pp_expr sty expr]
-
-mkSpecTyAppMsg :: PlainCoreExpr -> ErrMsg
-mkSpecTyAppMsg expr sty
-  = ppAbove (ppStr "Unboxed types in a type application (after specialisation):")
-           (pp_expr sty expr)
+mkSpecTyAppMsg :: CoreArg -> ErrMsg
+mkSpecTyAppMsg arg sty
+  = ppAbove
+      (ppStr "Unboxed types in a type application (after specialisation):")
+      (ppr sty arg)
 
+pp_expr :: PprStyle -> CoreExpr -> Pretty
 pp_expr sty expr
-  = pprCoreExpr sty pprBigCoreBinder pprTypedCoreBinder pprTypedCoreBinder expr
+  = pprCoreExpr sty (pprBigCoreBinder sty) (pprTypedCoreBinder sty) (pprTypedCoreBinder sty) expr
 \end{code}