diff --git a/src/GF/Compile.hs b/src/GF/Compile.hs
index e3bdee456..0b928d430 100644
--- a/src/GF/Compile.hs
+++ b/src/GF/Compile.hs
@@ -24,6 +24,7 @@ import GF.Infra.Ident
 import GF.Infra.Option
 import GF.Infra.Modules
 import GF.Infra.UseIO
+import GF.Infra.CheckM
 
 import GF.Data.Operations
 
@@ -205,10 +206,11 @@ compileSourceModule opts env@(k,gr,_) mo@(i,mi) = do
     _ -> do
       let mos = modules gr
 
-      mo2:_ <- putpp "  renaming " $ ioeErr $ renameModule mos mo1b
+      (mo2,warnings) <- putpp "  renaming " $ ioeErr $ runCheck (renameModule mos mo1b)
+      if null warnings then return () else puts warnings $ return ()
       intermOut opts DumpRename (ppModule Qualified mo2)
 
-      (mo3:_,warnings) <- putpp "  type checking" $ ioeErr $ showCheckModule mos mo2
+      (mo3,warnings) <- putpp "  type checking" $ ioeErr $ runCheck (checkModule mos mo2)
       if null warnings then return () else puts warnings $ return ()
       intermOut opts DumpTypeCheck (ppModule Qualified mo3)
 
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index 67526b5b5..e73a9ae07 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -22,7 +22,7 @@
 -----------------------------------------------------------------------------
 
 module GF.Compile.CheckGrammar (
-  showCheckModule, justCheckLTerm, allOperDependencies, topoSortOpers) where
+  checkModule, inferLType, allOperDependencies, topoSortOpers) where
 
 import GF.Infra.Ident
 import GF.Infra.Modules
@@ -48,14 +48,8 @@ import qualified Data.Set as Set
 import Control.Monad
 import Text.PrettyPrint
 
-showCheckModule :: [SourceModule] -> SourceModule -> Err ([SourceModule],String)
-showCheckModule mos m =
-  case runCheck (checkModule mos m) of
-    Left        msgs  -> Bad (   render (vcat (reverse msgs)))
-    Right (st,_,msgs) -> Ok (st, render (vcat (reverse msgs)))
-
 -- | checking is performed in the dependency order of modules
-checkModule :: [SourceModule] -> SourceModule -> Check [SourceModule]
+checkModule :: [SourceModule] -> SourceModule -> Check SourceModule
 checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ do
     let js = jments mo
     checkRestrictedInheritance ms (name, mo)
@@ -75,7 +69,7 @@ checkModule ms (name,mo) = checkIn (text "checking module" <+> ppIdent name) $ d
       MTInstance a -> do
         checkMap (checkResInfo gr name mo) js
 
-    return $ (name, replaceJudgements mo js') : ms
+    return (name, replaceJudgements mo js')
  where
    gr  = MGrammar $ (name,mo):ms
 
@@ -100,13 +94,6 @@ checkRestrictedInheritance mos (name,mo) = do
                          nest 2 (vcat [ppIdent f <+> text "on" <+> fsep (map ppIdent is) | (f,is) <- cs]))
    allDeps = concatMap (allDependencies (const True) . jments . snd) mos
 
--- | check if a term is typable
-justCheckLTerm :: SourceGrammar -> Term -> Err Term
-justCheckLTerm src t =
-  case runCheck (inferLType src t) of
-    Left msgs          -> Bad (   render (vcat (reverse msgs)))
-    Right ((t',_),_,_) -> Ok t'
-
 checkAbsInfo :: 
   SourceGrammar -> Ident -> SourceModInfo -> Ident -> Info -> Check Info
 checkAbsInfo st m mo c info = do
@@ -206,20 +193,20 @@ checkResInfo gr mo mm c info = do
     ResOper pty pde -> chIn "operation" $ do
       (pty', pde') <- case (pty,pde) of
          (Just ty, Just de) -> do
-           ty'     <- check ty typeType >>= comp . fst
-           (de',_) <- check de ty'
+           ty'     <- checkLType gr [] ty typeType >>= computeLType gr [] . fst
+           (de',_) <- checkLType gr [] de ty'
            return (Just ty', Just de')
          (_      , Just de) -> do
-           (de',ty') <- infer de
+           (de',ty') <- inferLType gr [] de
            return (Just ty', Just de')
          (_      , Nothing) -> do
            checkError (text "No definition given to the operation")
       return (ResOper pty' pde')
 
     ResOverload os tysts -> chIn "overloading" $ do
-      tysts' <- mapM (uncurry $ flip check) tysts  -- return explicit ones
+      tysts' <- mapM (uncurry $ flip (checkLType gr [])) tysts  -- return explicit ones
       tysts0 <- checkErr $ lookupOverload gr mo c  -- check against inherited ones too
-      tysts1 <- mapM (uncurry $ flip check) 
+      tysts1 <- mapM (uncurry $ flip (checkLType gr [])) 
                   [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
       --- this can only be a partial guarantee, since matching
       --- with value type is only possible if expected type is given
@@ -233,15 +220,12 @@ checkResInfo gr mo mm c info = do
 
     _ ->  return info
  where
-   infer = inferLType gr
-   check = checkLType gr
    chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mm c <+> colon)
-   comp = computeLType gr
 
    checkUniq xss = case xss of
      x:y:xs 
       | x == y    -> checkError $ text "ambiguous for type" <+>
-                                  ppType gr (mkFunType (tail x) (head x))  
+                                  ppType (mkFunType (tail x) (head x))  
       | otherwise -> checkUniq $ y:xs
      _ -> return ()
 
@@ -257,7 +241,7 @@ checkCncInfo gr m mo (a,abs) c info = do
       typ        <- checkErr $ lookupFunType gr a c
       let cat0   =  valCat typ
       (cont,val) <- linTypeOfType gr m typ         -- creates arg vars
-      (trm',_)   <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
+      (trm',_)   <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
       checkPrintname gr mpr
       cat        <- return $ snd cat0
       return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
@@ -265,10 +249,10 @@ checkCncInfo gr m mo (a,abs) c info = do
 
     CncCat (Just typ) mdef mpr -> chIn "linearization type of" $ do
       checkErr $ lookupCatContext gr a c
-      typ'  <- computeLType gr typ
+      typ'  <- computeLType gr [] typ
       mdef' <- case mdef of
         Just def -> do
-          (def',_) <- checkLType gr def (mkFunType [typeStr] typ)
+          (def',_) <- checkLType gr [] def (mkFunType [typeStr] typ)
           return $ Just def'
         _ -> return mdef
       checkPrintname gr mpr
@@ -277,66 +261,59 @@ checkCncInfo gr m mo (a,abs) c info = do
     _ -> checkResInfo gr m mo c info
 
  where
-   env = gr
-   infer = inferLType gr
-   comp = computeLType gr 
-   check = checkLType gr
    chIn cat = checkIn (text "Happened in" <+> text cat <+> ppIdent c <+> ppPosition mo c <> colon)
 
-computeLType :: SourceGrammar -> Type -> Check Type
-computeLType gr t = do
-  g0 <- checkGetContext
-  let g = [(b,x, Vr x) | (b,x,_) <- g0]
-  checkInContext g $ comp t
+computeLType :: SourceGrammar -> Context -> Type -> Check Type
+computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
  where
-  comp ty = case ty of
+  comp g ty = case ty of
     _ | Just _ <- isTypeInts ty -> return ty ---- shouldn't be needed
       | isPredefConstant ty     -> return ty ---- shouldn't be needed
 
     Q m ident -> checkIn (text "module" <+> ppIdent m) $ do
       ty' <- checkErr (lookupResDef gr m ident) 
-      if ty' == ty then return ty else comp ty' --- is this necessary to test?
+      if ty' == ty then return ty else comp g ty' --- is this necessary to test?
 
-    Vr ident  -> checkLookup ident -- never needed to compute!
+    Vr ident  -> checkLookup ident g -- never needed to compute!
 
     App f a -> do
-      f' <- comp f
-      a' <- comp a
+      f' <- comp g f
+      a' <- comp g a
       case f' of
-        Abs b x t -> checkInContext [(b,x,a')] $ comp t
+        Abs b x t -> comp ((b,x,a'):g) t
         _ -> return $ App f' a'
 
     Prod bt x a b -> do
-      a' <- comp a
-      b' <- checkInContext [(bt,x,Vr x)] $ comp b
+      a' <- comp g a
+      b' <- comp ((bt,x,Vr x) : g) b
       return $ Prod bt x a' b'
 
     Abs bt x b -> do
-      b' <- checkInContext [(bt,x,Vr x)] $ comp b
+      b' <- comp ((bt,x,Vr x):g) b
       return $ Abs bt x b'
 
     ExtR r s -> do
-      r' <- comp r
-      s' <- comp s
+      r' <- comp g r
+      s' <- comp g s
       case (r',s') of
-        (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp
+        (RecType rs, RecType ss) -> checkErr (plusRecType r' s') >>= comp g
         _ -> return $ ExtR r' s'
 
     RecType fs -> do
       let fs' = sortRec fs
-      liftM RecType $ mapPairsM comp fs'
+      liftM RecType $ mapPairsM (comp g) fs'
 
     ELincat c t -> do
-      t' <- comp t
+      t' <- comp g t
       checkErr $ lockRecType c t' ---- locking to be removed AR 20/6/2009
 
     _ | ty == typeTok -> return typeStr
     _ | isPredefConstant ty -> return ty
 
-    _ -> composOp comp ty
+    _ -> composOp (comp g) ty
 
 checkPrintname :: SourceGrammar -> Maybe Term -> Check ()
-checkPrintname st (Just t) = checkLType st t typeStr >> return ()
+checkPrintname st (Just t) = checkLType st [] t typeStr >> return ()
 checkPrintname _  _        = return ()
 
 -- | for grammars obtained otherwise than by parsing ---- update!!
@@ -347,15 +324,15 @@ checkReservedId x
 
 -- the underlying algorithms
 
-inferLType :: SourceGrammar -> Term -> Check (Term, Type)
-inferLType gr trm = case trm of
+inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
+inferLType gr g trm = case trm of
 
    Q m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
 
    Q m ident -> checks [
-     termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+     termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
      ,
-     checkErr (lookupResDef gr m ident) >>= infer
+     checkErr (lookupResDef gr m ident) >>= inferLType gr g
      ,
      checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
      ]
@@ -363,49 +340,49 @@ inferLType gr trm = case trm of
    QC m ident | isPredef m -> termWith trm $ checkErr (typPredefined ident)
 
    QC m ident -> checks [
-       termWith trm $ checkErr (lookupResType gr m ident) >>= comp
+       termWith trm $ checkErr (lookupResType gr m ident) >>= computeLType gr g
        ,
-       checkErr (lookupResDef gr m ident) >>= infer
+       checkErr (lookupResDef gr m ident) >>= inferLType gr g
        ,
        checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
        ]
 
    Val _ ty i -> termWith trm $ return ty
 
-   Vr ident -> termWith trm $ checkLookup ident
+   Vr ident -> termWith trm $ checkLookup ident g
 
    Typed e t -> do
-     t' <- comp t
-     check e t'
+     t' <- computeLType gr g t
+     checkLType gr g e t'
      return (e,t')
 
    App f a -> do
-     over <- getOverload gr Nothing trm
+     over <- getOverload gr g Nothing trm
      case over of
        Just trty -> return trty
        _ -> do
-         (f',fty) <- infer f
-         fty' <- comp fty
+         (f',fty) <- inferLType gr g f
+         fty' <- computeLType gr g fty
          case fty' of
            Prod bt z arg val -> do 
-             a' <- justCheck a arg
+             a' <- justCheck g a arg
              ty <- if isWildIdent z 
                       then return val
                       else substituteLType [(bt,z,a')] val
              return (App f' a',ty) 
-           _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty)
+           _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType fty)
 
    S f x -> do
-     (f', fty) <- infer f
+     (f', fty) <- inferLType gr g f
      case fty of
        Table arg val -> do
-         x'<- justCheck x arg
+         x'<- justCheck g x arg
          return (S f' x', val)
        _ -> checkError (text "table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
 
    P t i -> do
-     (t',ty) <- infer t   --- ??
-     ty' <- comp ty
+     (t',ty) <- inferLType gr g t   --- ??
+     ty' <- computeLType gr g ty
      let tr2 = P t' i
      termWith tr2 $ case ty' of
        RecType ts -> case lookup i ts of
@@ -413,7 +390,7 @@ inferLType gr trm = case trm of
                        Just x  -> return x
        _          -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
                                  text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
-   PI t i _ -> infer $ P t i
+   PI t i _ -> inferLType gr g $ P t i
 
    R r -> do
      let (ls,fs) = unzip r
@@ -424,10 +401,10 @@ inferLType gr trm = case trm of
 
    T (TTyped arg) pts -> do
      (_,val) <- checks $ map (inferCase (Just arg)) pts
-     check trm (Table arg val)
+     checkLType gr g trm (Table arg val)
    T (TComp arg) pts -> do
      (_,val) <- checks $ map (inferCase (Just arg)) pts
-     check trm (Table arg val)
+     checkLType gr g trm (Table arg val)
    T ti pts -> do  -- tries to guess: good in oper type inference
      let pts' = [pt | pt@(p,_) <- pts, isConstPatt p]
      case pts' of 
@@ -435,9 +412,9 @@ inferLType gr trm = case trm of
 ----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
        _  -> do 
          (arg,val) <- checks $ map (inferCase Nothing) pts'
-         check trm (Table arg val)
+         checkLType gr g trm (Table arg val)
    V arg pts -> do
-     (_,val) <- checks $ map infer pts
+     (_,val) <- checks $ map (inferLType gr g) pts
      return (trm, Table arg val)
 
    K s  -> do
@@ -457,45 +434,45 @@ inferLType gr trm = case trm of
    Empty -> return (trm, typeStr)
 
    C s1 s2 -> 
-     check2 (flip justCheck typeStr) C s1 s2 typeStr
+     check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
 
    Glue s1 s2 -> 
-     check2 (flip justCheck typeStr) Glue s1 s2 typeStr ---- typeTok
+     check2 (flip (justCheck g) typeStr) Glue s1 s2 typeStr ---- typeTok
 
 ---- hack from Rename.identRenameTerm, to live with files with naming conflicts 18/6/2007
    Strs (Cn c : ts) | c == cConflict -> do
      checkWarn (text "unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
-     infer (head ts)
+     inferLType gr g (head ts)
 
    Strs ts -> do
-     ts' <- mapM (\t -> justCheck t typeStr) ts 
+     ts' <- mapM (\t -> justCheck g t typeStr) ts 
      return (Strs ts', typeStrs)
 
    Alts (t,aa) -> do
-     t'  <- justCheck t typeStr
+     t'  <- justCheck g t typeStr
      aa' <- flip mapM aa (\ (c,v) -> do
-        c' <- justCheck c typeStr 
-        v' <- checks $ map (justCheck v) [typeStrs, EPattType typeStr]
+        c' <- justCheck g c typeStr 
+        v' <- checks $ map (justCheck g v) [typeStrs, EPattType typeStr]
         return (c',v'))
      return (Alts (t',aa'), typeStr)
 
    RecType r -> do
      let (ls,ts) = unzip r
-     ts' <- mapM (flip justCheck typeType) ts 
+     ts' <- mapM (flip (justCheck g) typeType) ts 
      return (RecType (zip ls ts'), typeType)
 
    ExtR r s -> do
-     (r',rT) <- infer r 
-     rT'     <- comp rT
-     (s',sT) <- infer s
-     sT'     <- comp sT
+     (r',rT) <- inferLType gr g r 
+     rT'     <- computeLType gr g rT
+     (s',sT) <- inferLType gr g s
+     sT'     <- computeLType gr g sT
 
      let trm' = ExtR r' s'
      ---- trm'    <- checkErr $ plusRecord r' s'
      case (rT', sT') of
        (RecType rs, RecType ss) -> do
          rt <- checkErr $ plusRecType rT' sT'
-         check trm' rt ---- return (trm', rt)
+         checkLType gr g trm' rt ---- return (trm', rt)
        _ | rT' == typeType && sT' == typeType -> return (trm', typeType)
        _ -> checkError (text "records or record types expected in" <+> ppTerm Unqualified 0 trm)
 
@@ -503,58 +480,50 @@ inferLType gr trm = case trm of
      termWith trm $ return typeType
 
    Prod bt x a b -> do
-     a' <- justCheck a typeType
-     b' <- checkInContext [(bt,x,a')] $ justCheck b typeType
+     a' <- justCheck g a typeType
+     b' <- justCheck ((bt,x,a'):g) b typeType
      return (Prod bt x a' b', typeType)
 
    Table p t  -> do
-     p' <- justCheck p typeType --- check p partype! 
-     t' <- justCheck t typeType
+     p' <- justCheck g p typeType --- check p partype! 
+     t' <- justCheck g t typeType
      return $ (Table p' t', typeType)
 
    FV vs -> do
-     (_,ty) <- checks $ map infer vs
+     (_,ty) <- checks $ map (inferLType gr g) vs
 ---     checkIfComplexVariantType trm ty
-     check trm ty
+     checkLType gr g trm ty
 
    EPattType ty -> do
-     ty' <- justCheck ty typeType
+     ty' <- justCheck g ty typeType
      return (EPattType ty',typeType)
    EPatt p -> do
      ty <- inferPatt p
      return (trm, EPattType ty)
 
    ELin c trm -> do
-     (trm',ty) <- infer trm
+     (trm',ty) <- inferLType gr g trm
      ty' <- checkErr $ lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
      return $ (ELin c trm', ty') 
 
    _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
 
  where
-   env = gr
-   infer = inferLType env
-   comp = computeLType env 
-
-   check = checkLType env
-   
    isPredef m = elem m [cPredef,cPredefAbs]
 
-   justCheck ty te = check ty te >>= return . fst
+   justCheck g ty te = checkLType gr g ty te >>= return . fst
 
    -- for record fields, which may be typed
    inferM (mty, t) = do
      (t', ty') <- case mty of
-       Just ty -> check ty t
-       _ -> infer t
+       Just ty -> checkLType gr g ty t
+       _ -> inferLType gr g t
      return (Just ty',t')
 
    inferCase mty (patt,term) = do
      arg  <- maybe (inferPatt patt) return mty
-     cont <- pattContext env arg patt
-     i    <- checkUpdates cont
-     (_,val) <- infer term
-     checkResets i
+     cont <- pattContext gr g arg patt
+     (_,val) <- inferLType gr (reverse cont ++ g) term
      return (arg,val)
    isConstPatt p = case p of
      PC _ ps -> True --- all isConstPatt ps
@@ -582,22 +551,21 @@ inferLType gr trm = case trm of
      PRep _   -> return $ typeStr
      PChar    -> return $ typeStr
      PChars _ -> return $ typeStr
-     _ -> infer (patt2term p) >>= return . snd
+     _ -> inferLType gr g (patt2term p) >>= return . snd
 
 
 -- type inference: Nothing, type checking: Just t
 -- the latter permits matching with value type
-getOverload :: SourceGrammar -> Maybe Type -> Term -> Check (Maybe (Term,Type))
-getOverload env@gr mt ot = case appForm ot of
+getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
+getOverload gr g mt ot = case appForm ot of
      (f@(Q m c), ts) -> case lookupOverload gr m c of
        Ok typs -> do
-         ttys <- mapM infer ts
+         ttys <- mapM (inferLType gr g) ts
          v <- matchOverload f typs ttys
          return $ Just v
        _ -> return Nothing
      _ -> return Nothing
  where
-   infer = inferLType env
    matchOverload f typs ttys = do
      let (tts,tys) = unzip ttys
      let vfs = lookupOverloadInstance tys typs
@@ -610,13 +578,13 @@ getOverload env@gr mt ot = case appForm ot of
          return (mkApp fun tts, val)
        ([],[]) -> do
          ---- let prtType _ = prt  -- to debug grammars
-         let showTypes ty = vcat (map (ppType env) ty)
+         let showTypes ty = vcat (map ppType ty)
          checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
                       text "for" $$
                       nest 2 (showTypes tys) $$
                       text "among" $$
                       nest 2 (vcat [showTypes ty | (ty,_) <- typs]) $$
-                      maybe empty (\x -> text "with value type" <+> ppType env x) mt
+                      maybe empty (\x -> text "with value type" <+> ppType x) mt
 
        (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
          ([(val,fun)],_) -> do
@@ -632,9 +600,9 @@ getOverload env@gr mt ot = case appForm ot of
 
 
          _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
-                           text "for" <+> hsep (map (ppType env) tys) $$ 
+                           text "for" <+> hsep (map ppType tys) $$ 
                            text "with alternatives" $$
-                           nest 2 (vcat [ppType env ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
+                           nest 2 (vcat [ppType ty | (ty,_) <- if null vfs1 then vfs2 else vfs2])
 
    matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
 
@@ -658,47 +626,44 @@ getOverload env@gr mt ot = case appForm ot of
      Prod _ _ _ _ -> False
      _ -> True
 
-checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
-checkLType env trm typ0 = do
+checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
+checkLType gr g trm typ0 = do
 
-  typ <- comp typ0
+  typ <- computeLType gr g typ0
 
   case trm of
 
     Abs bt x c -> do
       case typ of
         Prod bt' z a b -> do 
-          checkUpdate (bt,x,a)
           (c',b') <- if isWildIdent z
-                        then check c b
-                        else do
-                          b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
-                          check c b'
-          checkReset
+                       then checkLType gr ((bt,x,a):g) c b
+                       else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
+                               checkLType gr ((bt,x,a):g) c b'
           return $ (Abs bt x c', Prod bt' x a b')
-        _ -> checkError $ text "function type expected instead of" <+> ppType env typ
+        _ -> checkError $ text "function type expected instead of" <+> ppType typ
 
     App f a -> do
-       over <- getOverload env (Just typ) trm
+       over <- getOverload gr g (Just typ) trm
        case over of
          Just trty -> return trty
          _ -> do
-          (trm',ty') <- infer trm
-          termWith trm' $ checkEq typ ty' trm'
+          (trm',ty') <- inferLType gr g trm
+          termWith trm' $ checkEqLType gr g typ ty' trm'
 
     Q _ _ -> do
-       over <- getOverload env (Just typ) trm
+       over <- getOverload gr g (Just typ) trm
        case over of
          Just trty -> return trty
          _ -> do
-          (trm',ty') <- infer trm
-          termWith trm' $ checkEq typ ty' trm'
+          (trm',ty') <- inferLType gr g trm
+          termWith trm' $ checkEqLType gr g typ ty' trm'
 
     T _ [] ->
       checkError (text "found empty table in type" <+> ppTerm Unqualified 0 typ)
     T _ cs -> case typ of 
       Table arg val -> do 
-        case allParamValues env arg of
+        case allParamValues gr arg of
           Ok vs -> do
             let ps0 = map fst cs
             ps <- checkErr $ testOvershadow ps0 vs
@@ -709,7 +674,7 @@ checkLType env trm typ0 = do
           _ -> return () -- happens with variable types
         cs' <- mapM (checkCase arg val) cs
         return (T (TTyped arg) cs', typ)
-      _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType env typ)
+      _ -> checkError $ text "table type expected for table instead of" $$ nest 2 (ppType typ)
 
     R r -> case typ of --- why needed? because inference may be too difficult
        RecType rr -> do
@@ -721,7 +686,7 @@ checkLType env trm typ0 = do
 
     ExtR r s -> case typ of
        _ | typ == typeType -> do
-         trm' <- comp trm
+         trm' <- computeLType gr g trm
          case trm' of
            RecType _ -> termWith trm $ return typeType
            ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
@@ -729,87 +694,77 @@ checkLType env trm typ0 = do
            _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
        RecType rr -> do
          (r',ty,s') <- checks [
-            do (r',ty) <- infer r
+            do (r',ty) <- inferLType gr g r
                return (r',ty,s)
            ,
-            do (s',ty) <- infer s
+            do (s',ty) <- inferLType gr g s
                return (s',ty,r)
             ]
          case ty of
            RecType rr1 -> do
                 let (rr0,rr2) = recParts rr rr1
-                r2 <- justCheck r' rr0
-                s2 <- justCheck s' rr2
+                r2 <- justCheck g r' rr0
+                s2 <- justCheck g s' rr2
                 return $ (ExtR r2 s2, typ) 
            _ -> checkError (text "record type expected in extension of" <+> ppTerm Unqualified 0 r $$
                             text "but found" <+> ppTerm Unqualified 0 ty)
 
        ExtR ty ex -> do
-         r' <- justCheck r ty
-         s' <- justCheck s ex
+         r' <- justCheck g r ty
+         s' <- justCheck g s ex
          return $ (ExtR r' s', typ) --- is this all?
 
        _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
 
     FV vs -> do
-      ttys <- mapM (flip check typ) vs
+      ttys <- mapM (flip (checkLType gr g) typ) vs
 ---      checkIfComplexVariantType trm typ
       return (FV (map fst ttys), typ) --- typ' ?
 
     S tab arg -> checks [ do
-      (tab',ty) <- infer tab
-      ty'       <- comp ty
+      (tab',ty) <- inferLType gr g tab
+      ty'       <- computeLType gr g ty
       case ty' of
         Table p t -> do
-          (arg',val) <- check arg p
-          checkEq typ t trm
+          (arg',val) <- checkLType gr g arg p
+          checkEqLType gr g typ t trm
           return (S tab' arg', t)
-        _ -> checkError (text "table type expected for applied table instead of" <+> ppType env ty')
+        _ -> checkError (text "table type expected for applied table instead of" <+> ppType ty')
      , do
-      (arg',ty) <- infer arg
-      ty'       <- comp ty
-      (tab',_)  <- check tab (Table ty' typ)
+      (arg',ty) <- inferLType gr g arg
+      ty'       <- computeLType gr g ty
+      (tab',_)  <- checkLType gr g tab (Table ty' typ)
       return (S tab' arg', typ)
       ]
     Let (x,(mty,def)) body -> case mty of
       Just ty -> do
-        (def',ty') <- check def ty
-        checkUpdate (Explicit,x,ty')
-        body' <- justCheck body typ
-        checkReset
+        (def',ty') <- checkLType gr g def ty
+        body' <- justCheck ((Explicit,x,ty'):g) body typ
         return (Let (x,(Just ty',def')) body', typ)
       _ -> do
-        (def',ty) <- infer def  -- tries to infer type of local constant
-        check (Let (x,(Just ty,def')) body) typ
+        (def',ty) <- inferLType gr g def  -- tries to infer type of local constant
+        checkLType gr g (Let (x,(Just ty,def')) body) typ
 
     ELin c tr -> do
       tr1 <- checkErr $ unlockRecord c tr
-      check tr1 typ
+      checkLType gr g tr1 typ
 
     _ -> do
-      (trm',ty') <- infer trm
-      termWith trm' $ checkEq typ ty' trm'
+      (trm',ty') <- inferLType gr g trm
+      termWith trm' $ checkEqLType gr g typ ty' trm'
  where
-   cnc = env
-   infer = inferLType env
-   comp = computeLType env 
-
-   check = checkLType env
-   
-   justCheck ty te = check ty te >>= return . fst
-
-   checkEq = checkEqLType env
+   justCheck g ty te = checkLType gr g ty te >>= return . fst
 
    recParts rr t = (RecType rr1,RecType rr2) where 
      (rr1,rr2) = partition (flip elem (map fst t) . fst) rr 
 
    checkM rms (l,ty) = case lookup l rms of
      Just (Just ty0,t) -> do
-       checkEq ty ty0 t
-       (t',ty') <- check t ty
+       checkEqLType gr g ty ty0 t
+       (t',ty') <- checkLType gr g t ty
        return (l,(Just ty',t'))
      Just (_,t) -> do
-       (t',ty') <- check t ty
+       (t',ty') <- checkLType gr g t ty
        return (l,(Just ty',t'))
      _ -> checkError $ 
             if isLockLabel l 
@@ -819,41 +774,39 @@ checkLType env trm typ0 = do
               else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
 
    checkCase arg val (p,t) = do
-     cont <- pattContext env arg p
-     i    <- checkUpdates cont
-     t'   <- justCheck t val
-     checkResets i
+     cont <- pattContext gr g arg p
+     t' <- justCheck (reverse cont ++ g) t val
      return (p,t')
 
-pattContext :: LTEnv -> Type -> Patt -> Check Context
-pattContext env typ p = case p of
+pattContext :: SourceGrammar -> Context -> Type -> Patt -> Check Context
+pattContext env g typ p = case p of
   PV x -> return [(Explicit,x,typ)]
   PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
-    t <- checkErr $ lookupResType cnc q c
+    t <- checkErr $ lookupResType env q c
     let (cont,v) = typeFormCnc t
     checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
               (length cont == length ps)
-    checkEqLType env typ v (patt2term p)
-    mapM (\((_,_,ty),p) -> pattContext env ty p) (zip cont ps) >>= return . concat
+    checkEqLType env g typ v (patt2term p)
+    mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
   PR r -> do
-    typ' <- computeLType env typ
+    typ' <- computeLType env g typ
     case typ' of
       RecType t -> do
         let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
         ----- checkWarn $ prt p ++++ show pts ----- debug
-        mapM (uncurry (pattContext env)) pts >>= return . concat
+        mapM (uncurry (pattContext env g)) pts >>= return . concat
       _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
   PT t p' -> do
-    checkEqLType env typ t (patt2term p')
-    pattContext env typ p'
+    checkEqLType env g typ t (patt2term p')
+    pattContext env g typ p'
 
   PAs x p -> do
-    g <- pattContext env typ p
-    return $ (Explicit,x,typ):g
+    g' <- pattContext env g typ p
+    return ((Explicit,x,typ):g')
 
   PAlt p' q -> do
-    g1 <- pattContext env typ p'
-    g2 <- pattContext env typ q
+    g1 <- pattContext env g typ p'
+    g2 <- pattContext env g typ q
     let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
     checkCond 
       (text "incompatible bindings of" <+>
@@ -861,17 +814,16 @@ pattContext env typ p = case p of
        text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
     return g1 -- must be g1 == g2
   PSeq p q -> do
-    g1 <- pattContext env typ p
-    g2 <- pattContext env typ q
+    g1 <- pattContext env g typ p
+    g2 <- pattContext env g typ q
     return $ g1 ++ g2
   PRep p' -> noBind typeStr p'
   PNeg p' -> noBind typ p'
 
   _ -> return [] ---- check types!
  where 
-   cnc = env
    noBind typ p' = do
-    co <- pattContext env typ p'
+    co <- pattContext env g typ p'
     if not (null co)
       then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
            >> return []
@@ -879,8 +831,6 @@ pattContext env typ p = case p of
 
 -- auxiliaries
 
-type LTEnv = SourceGrammar
-
 termWith :: Term -> Check Type -> Check (Term, Type)
 termWith t ct = do
   ty <- ct
@@ -900,19 +850,19 @@ check2 chk con a b t = do
   b' <- chk b
   return (con a' b', t)
 
-checkEqLType :: LTEnv -> Type -> Type -> Term -> Check Type
-checkEqLType env t u trm = do
-  (b,t',u',s) <- checkIfEqLType env t u trm
+checkEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check Type
+checkEqLType gr g t u trm = do
+  (b,t',u',s) <- checkIfEqLType gr g t u trm
   case b of
     True  -> return t'
     False -> checkError $ text s <+> text "type of" <+> ppTerm Unqualified 0 trm $$
-                          text "expected:" <+> ppType env t $$
-                          text "inferred:" <+> ppType env u
+                          text "expected:" <+> ppType t $$
+                          text "inferred:" <+> ppType u
 
-checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
-checkIfEqLType env t u trm = do
-  t' <- comp t 
-  u' <- comp u
+checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
+checkIfEqLType gr g t u trm = do
+  t' <- computeLType gr g t
+  u' <- computeLType gr g u
   case t' == u' || alpha [] t' u' of
     True -> return (True,t',u',[])
     -- forgive missing lock fields by only generating a warning.
@@ -947,15 +897,15 @@ checkIfEqLType env t u trm = do
            | t == typeInt,           Just _ <- isTypeInts u -> True ---- why this ???? AR 11/12/2005
 
      ---- this should be made in Rename
-     (Q  m a, Q  n b) | a == b -> elem m (allExtendsPlus env n) 
-                               || elem n (allExtendsPlus env m)
+     (Q  m a, Q  n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
                                || m == n --- for Predef
-     (QC m a, QC n b) | a == b -> elem m (allExtendsPlus env n) 
-                               || elem n (allExtendsPlus env m)
-     (QC m a, Q  n b) | a == b -> elem m (allExtendsPlus env n) 
-                               || elem n (allExtendsPlus env m)
-     (Q  m a, QC n b) | a == b -> elem m (allExtendsPlus env n) 
-                               || elem n (allExtendsPlus env m)
+     (QC m a, QC n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
+     (QC m a, Q  n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
+     (Q  m a, QC n b) | a == b -> elem m (allExtendsPlus gr n) 
+                               || elem n (allExtendsPlus gr m)
 
      (Table a b,  Table c d)  -> alpha g a c && alpha g b d
      (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
@@ -983,16 +933,15 @@ checkIfEqLType env t u trm = do
      _ -> Bad ""
 
    sTypes = [typeStr, typeTok, typeString]
-   comp = computeLType env
 
 -- printing a type with a lock field lock_C as C
-ppType :: LTEnv -> Type -> Doc
-ppType env ty =
+ppType :: Type -> Doc
+ppType ty =
   case ty of
     RecType fs   -> case filter isLockLabel $ map fst fs of
                       [lock] -> text (drop 5 (showIdent (label2ident lock)))
                       _      -> ppTerm Unqualified 0 ty
-    Prod _ x a b -> ppType env a <+> text "->" <+> ppType env b
+    Prod _ x a b -> ppType a <+> text "->" <+> ppType b
     _            -> ppTerm Unqualified 0 ty
 
 -- | linearization types and defaults
@@ -1015,7 +964,7 @@ linTypeOfType cnc m typ = do
                              plusRecType vars val
      return (Explicit,symb,rec)
    lookLin (_,c) = checks [ --- rather: update with defLinType ?
-      checkErr (lookupLincat cnc m c) >>= computeLType cnc
+      checkErr (lookupLincat cnc m c) >>= computeLType cnc []
      ,return defLinType
      ]
 
@@ -1050,3 +999,9 @@ topoSortOpers st = do
     return 
     (\ops -> Bad (render (text "circular definitions:" <+> fsep (map ppIdent (head ops)))))
     eops
+
+checkLookup :: Ident -> Context -> Check Type
+checkLookup x g =
+  case [ty | (b,y,ty) <- g, x == y] of
+    []     -> checkError (text "unknown variable" <+> ppIdent x)
+    (ty:_) -> return ty
diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs
index 7d61e8a7d..aea39e632 100644
--- a/src/GF/Compile/Rename.hs
+++ b/src/GF/Compile/Rename.hs
@@ -22,7 +22,7 @@
 -- Hence we can proceed by @fold@ing "from left to right".
 -----------------------------------------------------------------------------
 
-module GF.Compile.Rename (renameGrammar,
+module GF.Compile.Rename (
 	       renameSourceTerm,
 	       renameModule
 	      ) where
@@ -32,6 +32,7 @@ import GF.Grammar.Values
 import GF.Grammar.Predef
 import GF.Infra.Modules
 import GF.Infra.Ident
+import GF.Infra.CheckM
 import GF.Grammar.Macros
 import GF.Grammar.Printer
 import GF.Grammar.AppPredefined
@@ -41,25 +42,21 @@ import GF.Data.Operations
 
 import Control.Monad
 import Data.List (nub)
-import Debug.Trace (trace)
 import Text.PrettyPrint
 
-renameGrammar :: SourceGrammar -> Err SourceGrammar
-renameGrammar g = liftM (MGrammar . reverse) $ foldM renameModule [] (modules g)
-
 -- | this gives top-level access to renaming term input in the cc command
-renameSourceTerm :: SourceGrammar -> Ident -> Term -> Err Term
+renameSourceTerm :: SourceGrammar -> Ident -> Term -> Check Term
 renameSourceTerm g m t = do
-  mo     <- lookupModule g m
+  mo     <- checkErr $ lookupModule g m
   status <- buildStatus g m mo
   renameTerm status [] t
 
-renameModule :: [SourceModule] -> SourceModule -> Err [SourceModule]
-renameModule ms (name,mo) = errIn ("renaming module" +++ showIdent name) $ do
+renameModule :: [SourceModule] -> SourceModule -> Check SourceModule
+renameModule ms (name,mo) = checkIn (text "renaming module" <+> ppIdent name) $ do
   let js1 = jments mo
   status <- buildStatus (MGrammar ms) name mo
-  js2    <- mapsErrTree (renameInfo mo status) js1
-  return $ (name, mo {opens = map forceQualif (opens mo), jments = js2}) : ms
+  js2    <- checkMap (renameInfo mo status) js1
+  return (name, mo {opens = map forceQualif (opens mo), jments = js2})
 
 type Status = (StatusTree, [(OpenSpec Ident, StatusTree)])
 
@@ -67,20 +64,20 @@ type StatusTree = BinTree Ident StatusInfo
 
 type StatusInfo = Ident -> Term
 
-renameIdentTerm :: Status -> Term -> Err Term
+renameIdentTerm :: Status -> Term -> Check Term
 renameIdentTerm env@(act,imps) t = 
- errIn (render (text "atomic term" <+> ppTerm Unqualified 0 t $$ text "given" <+> hsep (punctuate comma (map (ppIdent . fst) qualifs)))) $
+ checkIn (text "atomic term" <+> ppTerm Qualified 0 t $$ text "given" <+> hsep (punctuate comma (map (ppIdent . fst) qualifs))) $
    case t of
   Vr c -> ident predefAbs c
-  Cn c -> ident (\_ s -> Bad s) c
+  Cn c -> ident (\_ s -> checkError s) c
   Q m' c | m' == cPredef {- && isInPredefined c -} -> return t
   Q m' c -> do
-    m <- lookupErr m' qualifs
+    m <- checkErr (lookupErr m' qualifs)
     f <- lookupTree showIdent c m
     return $ f c
   QC m' c | m' == cPredef {- && isInPredefined c -} -> return t
   QC m' c -> do
-    m <- lookupErr m' qualifs
+    m <- checkErr (lookupErr m' qualifs)
     f <- lookupTree showIdent c m
     return $ f c
   _ -> return t
@@ -92,28 +89,21 @@ renameIdentTerm env@(act,imps) t =
    -- this facility is mainly for BWC with GF1: you need not import PredefAbs
    predefAbs c s
      | isPredefCat c = return $ Q cPredefAbs c
-     | otherwise     = Bad s
+     | otherwise     = checkError s
 
    ident alt c = case lookupTree showIdent c act of
       Ok f -> return $ f c
       _ -> case lookupTreeManyAll showIdent opens c of
         [f] -> return $ f c
-        []  -> alt c (render (text "constant not found:" <+> ppIdent c))
+        []  -> alt c (text "constant not found:" <+> ppIdent c)
         fs -> case nub [f c | f <- fs]  of
           [tr] -> return tr
-          ts@(t:_) -> trace (render (text "Warning: conflict" <+> hsep (punctuate comma (map (ppTerm Qualified 0) ts)))) (return t)
+          ts@(t:_) -> do checkWarn (text "conflict" <+> hsep (punctuate comma (map (ppTerm Qualified 0) ts)))
+                         return t
             -- a warning will be generated in CheckGrammar, and the head returned
             -- in next V: 
             -- Bad $ "conflicting imports:" +++ unwords (map prt ts) 
 
-
---- | would it make sense to optimize this by inlining?
-renameIdentPatt :: Status -> Patt -> Err Patt
-renameIdentPatt env p = do
-  let t = patt2term p
-  t' <- renameIdentTerm env t
-  term2patt t'
-
 info2status :: Maybe Ident -> (Ident,Info) -> StatusInfo
 info2status mq (c,i) = case i of
   AbsFun _ _ Nothing -> maybe Con QC mq
@@ -128,11 +118,11 @@ tree2status o = case o of
   OSimple i   -> mapTree (info2status (Just i))
   OQualif i j -> mapTree (info2status (Just j))
 
-buildStatus :: SourceGrammar -> Ident -> SourceModInfo -> Err Status
+buildStatus :: SourceGrammar -> Ident -> SourceModInfo -> Check Status
 buildStatus gr c mo = let mo' = self2status c mo in do
     let gr1 = MGrammar ((c,mo) : modules gr)
         ops = [OSimple e | e <- allExtends gr1 c] ++ opens mo
-    mods <- mapM (lookupModule gr1 . openedModule) ops
+    mods <- checkErr $ mapM (lookupModule gr1 . openedModule) ops
     let sts = map modInfo2status $ zip ops mods    
     return $ if isModCnc mo
       then (emptyBinTree, reverse sts) -- the module itself does not define any names
@@ -148,10 +138,10 @@ forceQualif o = case o of
   OSimple i   -> OQualif i i
   OQualif _ i -> OQualif i i
   
-renameInfo :: SourceModInfo -> Status -> (Ident,Info) -> Err (Ident,Info)
-renameInfo mo status (i,info) = errIn 
-    (render (text "renaming definition of" <+> ppIdent i <+> ppPosition mo i)) $ 
-                                liftM ((,) i) $ case info of
+renameInfo :: SourceModInfo -> Status -> Ident -> Info -> Check Info
+renameInfo mo status i info = checkIn 
+    (text "renaming definition of" <+> ppIdent i <+> ppPosition mo i) $ 
+                                case info of
   AbsCat pco pfs -> liftM2 AbsCat (renPerh (renameContext status) pco)
                                   (renPerh (mapM rent) pfs)
   AbsFun  pty pa ptr -> liftM3 AbsFun (ren pty) (return pa) (renPerh (mapM (renameEquation status [])) ptr)
@@ -175,7 +165,7 @@ renameInfo mo status (i,info) = errIn
 renPerh ren (Just t) = liftM Just $ ren t
 renPerh ren Nothing  = return Nothing
 
-renameTerm :: Status -> [Ident] -> Term -> Err Term
+renameTerm :: Status -> [Ident] -> Term -> Check Term
 renameTerm env vars = ren vars where
   ren vs trm = case trm of
     Abs b x t    -> liftM  (Abs b x) (ren (x:vs) t)
@@ -202,13 +192,13 @@ renameTerm env vars = ren vars where
       b' <- ren (x:vs) b
       return $ Let (x,(m',a')) b'
 
-    P t@(Vr r) l                     -- for constant t we know it is projection
-      | elem r vs -> return trm                           -- var proj first
-      | otherwise -> case renid (Q r (label2ident l)) of  -- qualif   second
-          Ok t -> return t
-          _ -> case liftM (flip P l) $ renid t of
-            Ok t -> return t                              -- const proj last
-            _ -> Bad (render (text "unknown qualified constant" <+> ppTerm Qualified 0 trm))
+    P t@(Vr r) l                                               -- Here we have $r.l$ and this is ambiguous it could be either 
+                                                               -- record projection from variable or constant $r$ or qualified expression with module $r$
+      | elem r vs -> return trm                                -- try var proj first ..
+      | otherwise -> checks [ renid (Q r (label2ident l))      -- .. and qualified expression second.
+                            , renid t >>= \t -> return (P t l) -- try as a constant at the end
+                            , checkError (text "unknown qualified constant" <+> ppTerm Unqualified 0 trm)
+                            ]
 
     EPatt p -> do
       (p',_) <- renpatt p
@@ -224,40 +214,42 @@ renameTerm env vars = ren vars where
   renpatt = renamePattern env
 
 -- | vars not needed in env, since patterns always overshadow old vars
-renamePattern :: Status -> Patt -> Err (Patt,[Ident])
+renamePattern :: Status -> Patt -> Check (Patt,[Ident])
 renamePattern env patt = case patt of
 
   PMacro c -> do
     c' <- renid $ Vr c
     case c' of
       Q p d -> renp $ PM p d
-      _ -> Bad (render (text "unresolved pattern" <+> ppPatt Unqualified 0 patt))
+      _ -> checkError (text "unresolved pattern" <+> ppPatt Unqualified 0 patt)
 
   PC c ps -> do
     c' <- renid $ Cn c
     case c' of
-      QC m c -> renp $ PP m c ps
-      Q  _ _ -> Bad $ render (text "data constructor expected but" <+> ppTerm Qualified 0 c' <+> text "is found instead")
-      _      -> Bad $ render (text "unresolved data constructor" <+> ppTerm Qualified 0 c')
+      QC m c -> do psvss <- mapM renp ps
+                   let (ps,vs) = unzip psvss
+                   return (PP m c ps, concat vs)
+      Q  _ _ -> checkError (text "data constructor expected but" <+> ppTerm Qualified 0 c' <+> text "is found instead")
+      _      -> checkError (text "unresolved data constructor" <+> ppTerm Qualified 0 c')
 
   PP p c ps -> do
-
-    (p', c') <- case renid (QC p c) of
-      Ok (QC p' c') -> return (p',c')
-      _ -> return (p,c) --- temporarily, for bw compat
+    (QC p' c') <- renid (QC p c)
     psvss <- mapM renp ps
     let (ps',vs) = unzip psvss
     return (PP p' c' ps', concat vs)
 
   PM p c -> do
-    (p', c') <- case renid (Q p c) of
-      Ok (Q p' c') -> return (p',c')
-      _ -> Bad (render (text "not a pattern macro" <+> ppPatt Unqualified 0 patt))
+    x <- renid (Q p c)
+    (p',c') <- case x of
+                 (Q p' c') -> return (p',c')
+                 _         -> checkError (text "not a pattern macro" <+> ppPatt Qualified 0 patt)
     return (PM p' c', [])
 
-  PV x -> do case renid (Vr x) of
-               Ok (QC m c) -> return (PP m c [],[])
-               _           -> return (patt, [x])
+  PV x -> checks [ renid (Vr x) >>= \t' -> case t' of
+                                             QC m c -> return (PP m c [],[])
+                                             _      -> checkError (text "not a constructor")
+                 , return (patt, [x])
+                 ]
 
   PR r -> do
     let (ls,ps) = unzip r
@@ -293,12 +285,12 @@ renamePattern env patt = case patt of
    renp  = renamePattern env
    renid = renameIdentTerm env
 
-renameParam :: Status -> (Ident, Context) -> Err (Ident, Context)
+renameParam :: Status -> (Ident, Context) -> Check (Ident, Context)
 renameParam env (c,co) = do
   co' <- renameContext env co
   return (c,co')
 
-renameContext :: Status -> Context -> Err Context
+renameContext :: Status -> Context -> Check Context
 renameContext b = renc [] where
   renc vs cont = case cont of
     (bt,x,t) : xts 
@@ -315,7 +307,7 @@ renameContext b = renc [] where
   ren = renameTerm b
 
 -- | vars not needed in env, since patterns always overshadow old vars
-renameEquation :: Status -> [Ident] -> Equation -> Err Equation
+renameEquation :: Status -> [Ident] -> Equation -> Check Equation
 renameEquation b vs (ps,t) = do
   (ps',vs') <- liftM unzip $ mapM (renamePattern b) ps
   t'        <- renameTerm b (concat vs' ++ vs) t
diff --git a/src/GF/Grammar/API.hs b/src/GF/Grammar/API.hs
index f1d70e470..8dc86c10e 100644
--- a/src/GF/Grammar/API.hs
+++ b/src/GF/Grammar/API.hs
@@ -8,6 +8,7 @@ module GF.Grammar.API (
   ) where
 
 import GF.Infra.Ident
+import GF.Infra.CheckM
 import GF.Infra.Modules (greatestResource)
 import GF.Compile.GetGrammar
 import GF.Grammar.Macros
@@ -16,7 +17,7 @@ import GF.Grammar.Printer
 import GF.Grammar.Grammar
 
 import GF.Compile.Rename (renameSourceTerm)
-import GF.Compile.CheckGrammar (justCheckLTerm)
+import GF.Compile.CheckGrammar (inferLType)
 import GF.Compile.Compute (computeConcrete)
 
 import GF.Data.Operations
@@ -36,9 +37,10 @@ checkTerm gr t = do
   checkTermAny gr mo t
 
 checkTermAny :: Grammar -> Ident -> Term -> Err Term
-checkTermAny gr m t = do
-  t1 <- renameSourceTerm gr m t
-  justCheckLTerm gr t1
+checkTermAny gr m t = (fmap fst . runCheck) $ do
+  t <- renameSourceTerm gr m t
+  (t,_) <- inferLType gr [] t
+  return t
 
 computeTerm :: Grammar -> Term -> Err Term
 computeTerm = computeConcrete
diff --git a/src/GF/Infra/CheckM.hs b/src/GF/Infra/CheckM.hs
index a556e5c3a..8a1b42cdf 100644
--- a/src/GF/Infra/CheckM.hs
+++ b/src/GF/Infra/CheckM.hs
@@ -14,9 +14,8 @@
 
 module GF.Infra.CheckM
           (Check, Message, runCheck,
-	       checkError, checkCond, checkWarn, checkUpdate, checkInContext,
-	       checkUpdates, checkReset, checkResets, checkGetContext, 
-	       checkLookup, checkErr, checkIn, checkMap
+	       checkError, checkCond, checkWarn, 
+	       checkErr, checkIn, checkMap
 	      ) where
 
 import GF.Data.Operations
@@ -29,21 +28,21 @@ import Text.PrettyPrint
 
 type Message = Doc
 data CheckResult a
-  = Fail              [Message]
-  | Success a Context [Message]
+  = Fail      [Message]
+  | Success a [Message]
 newtype Check a = Check {unCheck :: Context -> [Message] -> CheckResult a}
 
 instance Monad Check where
-  return x = Check (\ctxt msgs -> Success x ctxt msgs)
+  return x = Check (\ctxt msgs -> Success x msgs)
   f >>= g  = Check (\ctxt msgs -> case unCheck f ctxt msgs of
-                                    Success x ctxt msgs -> unCheck (g x) ctxt msgs
-                                    Fail msgs           -> Fail msgs)
+                                    Success x msgs -> unCheck (g x) ctxt msgs
+                                    Fail msgs      -> Fail msgs)
 
 instance ErrorMonad Check where
   raise s = checkError (text s)
   handle f h = Check (\ctxt msgs -> case unCheck f ctxt msgs of
-                                      Success x ctxt msgs -> Success x ctxt msgs
-                                      Fail (msg:msgs)     -> unCheck (h (render msg)) ctxt msgs)
+                                      Success x msgs  -> Success x msgs
+                                      Fail (msg:msgs) -> unCheck (h (render msg)) ctxt msgs)
 
 checkError :: Message -> Check a
 checkError msg = Check (\ctxt msgs -> Fail (msg : msgs))
@@ -53,42 +52,13 @@ checkCond s b = if b then return () else checkError s
 
 -- | warnings should be reversed in the end
 checkWarn :: Message -> Check ()
-checkWarn msg = Check (\ctxt msgs -> Success () ctxt ((text "Warning:" <+> msg) : msgs))
+checkWarn msg = Check (\ctxt msgs -> Success () ((text "Warning:" <+> msg) : msgs))
 
-checkUpdate :: Hypo -> Check ()
-checkUpdate d = Check (\ctxt msgs -> Success () (d:ctxt) msgs)
-
-checkInContext :: [Hypo] -> Check r -> Check r
-checkInContext g ch = do
-  i <- checkUpdates g
-  r <- ch
-  checkResets i
-  return r
-
-checkUpdates :: [Hypo] -> Check Int
-checkUpdates ds = mapM checkUpdate ds >> return (length ds)
-
-checkReset :: Check ()
-checkReset = checkResets 1
-
-checkResets :: Int -> Check ()
-checkResets i = Check (\ctxt msgs -> Success () (drop i ctxt) msgs)
-
-checkGetContext :: Check Context
-checkGetContext = Check (\ctxt msgs -> Success ctxt ctxt msgs)
-
-checkLookup :: Ident -> Check Type
-checkLookup x = do
-  co <- checkGetContext
-  case [ty | (b,y,ty) <- co, x == y] of
-    []     -> checkError (text "unknown variable" <+> ppIdent x)
-    (ty:_) -> return ty
-
-runCheck :: Check a -> Either [Message] (a,Context,[Message])
+runCheck :: Check a -> Err (a,String)
 runCheck c =
   case unCheck c [] [] of
-    Fail msgs           -> Left          msgs
-    Success v ctxt msgs -> Right (v,ctxt,msgs)
+    Fail msgs      -> Bad (   render (vcat (reverse msgs)))
+    Success v msgs -> Ok  (v, render (vcat (reverse msgs)))
 
 checkMap :: (Ord a) => (a -> b -> Check b) -> Map.Map a b -> Check (Map.Map a b)
 checkMap f map = do xs <- mapM (\(k,v) -> do v <- f k v
@@ -102,6 +72,6 @@ checkErr (Bad err) = checkError (text err)
 checkIn :: Doc -> Check a -> Check a
 checkIn msg c = Check $ \ctxt msgs ->
   case unCheck c ctxt [] of
-    Fail            msgs' -> Fail ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
-    Success v ctxt' msgs' | null msgs' -> Success v ctxt' msgs
-                          | otherwise  -> Success v ctxt' ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
+    Fail      msgs' -> Fail ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)
+    Success v msgs' | null msgs' -> Success v msgs
+                    | otherwise  -> Success v ((msg $$ nest 3 (vcat (reverse msgs'))) : msgs)