diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf
index 05526b365..1ab4c2abd 100644
--- a/examples/logic/ArithmEng.gf
+++ b/examples/logic/ArithmEng.gf
@@ -29,15 +29,15 @@ lin
 
   evax1 = 
     proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
-      (mkS (pred (regA "even") (UsePN (regPN "zero")))) ;
+      (mkS (predA (regA "even") (UsePN (regPN "zero")))) ;
   evax2 n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the second axiom of evenness ,"]))) 
-        (mkS (pred (regA "odd") (appN2 (regN2 "successor") n)))) ;
+        (mkS (predA (regA "odd") (appN2 (regN2 "successor") n)))) ;
   evax3 n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the third axiom of evenness ,"]))) 
-        (mkS (pred (regA "even") (appN2 (regN2 "successor") n)))) ;
+        (mkS (predA (regA "even") (appN2 (regN2 "successor") n)))) ;
 
 
   eqax1 = 
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
index f8eaf6aa2..1f9b08e41 100644
--- a/examples/logic/LogicI.gf
+++ b/examples/logic/LogicI.gf
@@ -18,9 +18,9 @@ lincat
 lin
   ThmWithProof = theorem ;
 
-  Conj A = coord and_Conj A ;
-  Disj A B = coord or_Conj A B ;
-  Impl A B = coord ifthen_DConj A B ;
+  Conj = coord and_Conj ;
+  Disj = coord or_Conj ;
+  Impl = coord ifthen_DConj ;
 
   Abs = 
     mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet IndefArt) contradiction_N)) ;
@@ -28,21 +28,21 @@ lin
   Univ A B = 
     AdvS 
       (mkAdv for_Prep (mkNP all_Predet 
-        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
+        (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0)))))
       B ;
 
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
   DisjIr A B b = proof b (proof afortiori (coord or_Conj A B)) ;
 
-  DisjE A B C c b1 b2 =
+  DisjE A B C c d e =
     appendText
       c 
       (appendText
         (appendText
            (cases (mkNum n2)) 
            (proofs 
-             (appendText (assumption A) b1)
-             (appendText (assumption B) b2)))
+             (appendText (assumption A) d)
+             (appendText (assumption B) e)))
         (proof therefore C)) ;
 
   ImplI A B b = 
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf
index 3a5a61894..4c193740a 100644
--- a/examples/logic/Prooftext.gf
+++ b/examples/logic/Prooftext.gf
@@ -32,7 +32,7 @@ oper
 
   definition : Decls -> Object -> Object -> Section 
     = \decl,a,b -> 
-        appendText decl (mkUtt (mkS (pred b a))) ;
+        appendText decl (mkText (mkPhr (mkUtt (mkS (pred b a)))) TEmpty) ;
 
   theorem : Prop -> Proof -> Section 
     = \prop,prf -> appendText (mkText (mkPhr prop) TEmpty) prf ;
@@ -64,17 +64,17 @@ oper
     = appendText ;
 
   cases : Num -> Branching 
-    = \nu -> 
-        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet nu) case_N)) ;
+    = \n -> 
+        mkS (pred have_V2 (mkNP we_Pron) (mkNP (mkDet n) case_N)) ;
 
   by : Ref -> Adverb 
-    = \h -> mkAdv by8means_Prep h ;
+    = \h -> C.mkPConj (mkAdv by8means_Prep h).s ;
   therefore : Adverb
     = therefore_PConj ;
   afortiori : Adverb
     = C.mkPConj ["a fortiori"] ;
   hypothesis : Adverb
-    = mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N) ;
+    = C.mkPConj (mkAdv by8means_Prep (mkNP (mkDet DefArt) hypothesis_N)).s ;
 
   ref : Label -> Ref
     = \h -> h ;
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index b2ea41d2b..86c761e89 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -189,7 +189,10 @@ checkResInfo gr mo (c,info) = do
     ResOverload tysts -> chIn "overloading" $ do
       tysts' <- mapM (uncurry $ flip check) tysts
       let tysts2 = [(y,x) | (x,y) <- tysts']
-      checkUniq $ sort [map snd xs | (x,_) <- tysts2, Ok (xs,_) <- [typeFormCnc x]]
+      --- this can only be a partial guarantee, since matching
+      --- with value type is only possible if expected type is given
+      checkUniq $ 
+        sort [t : map snd xs | (x,_) <- tysts2, Ok (xs,t) <- [typeFormCnc x]]
       return (c,ResOverload tysts2)
 
     ResParam (Yes (pcs,_)) -> chIn "parameter type" $ do
@@ -395,7 +398,7 @@ inferLType gr trm = case trm of
      return (e,t')
 
    App f a -> do
-     over <- getOverload trm
+     over <- getOverload gr Nothing trm
      case over of
        Just trty -> return trty
        _ -> do
@@ -572,7 +575,11 @@ inferLType gr trm = case trm of
      PRep _   -> return $ typeTok
      _ -> infer (patt2term p) >>= return . snd
 
-   getOverload t = case appForm t of
+
+-- 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 t = case appForm t of
      (f@(Q m c), ts) -> case lookupOverload gr m c of
        Ok typs -> do
          ttys <- mapM infer ts
@@ -580,31 +587,34 @@ inferLType gr trm = case trm of
          return $ Just v
        _ -> return Nothing
      _ -> return Nothing
- 
+ where
+   infer = inferLType env
    matchOverload f typs ttys = do
      let (tts,tys) = unzip ttys
-     case lookupOverloadInstance tys typs of
-       [((val,fun),_)] -> return (mkApp fun tts, val)
+     let vfs = lookupOverloadInstance tys typs
+
+     case [vf | vf@(v,f) <- vfs, elem mt [Nothing,Just v]] of
+       [(val,fun)] -> return (mkApp fun tts, val)
        [] -> raise $ "no overload instance of" +++ prt f +++ 
+         maybe [] (("when expecting" +++) . prtType) mt +++
          "for" +++ unwords (map prtType tys) +++ "among" ++++ 
          unlines [unwords (map prtType ty) | (ty,_) <- typs]
       ----  ++++ "DEBUG" +++ unwords (map show tys) +++ ";" 
       ----  ++++ unlines (map (show . fst) typs) ----
-       vfs -> case filter snd vfs of
-         [((val,fun),_)] -> return (mkApp fun tts, val) 
-         _ -> raise $ "ambiguous overloading of" +++ prt f +++
-           "for" +++ unwords (map prtType tys) ++++ "with alternatives" ++++ 
-           unlines [prtType ty | ((ty,_),_) <- vfs]
+       _ -> raise $ "ambiguous overloading of" +++ prt f +++
+         "for" +++ unwords (map prtType tys) ++++ "with alternatives" ++++ 
+         unlines [prtType ty | (ty,_) <- vfs]
 
    ---- TODO: accept subtypes
    ---- TODO: use a trie
    lookupOverloadInstance tys typs = 
-     [((mkFunType rest val, t),null rest) | 
+     [(mkFunType rest val, t) | 
        (ty,(val,t)) <- typs, 
        let (pre,rest) = splitAt (length tys) ty, 
        pre == tys
      ]
 
+
 checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
 checkLType env trm typ0 = do
 
@@ -625,6 +635,14 @@ checkLType env trm typ0 = do
           return $ (Abs x c', Prod x a b')
         _ -> raise $ "product expected instead of" +++ prtType typ
 
+    App f a -> do
+       over <- getOverload env (Just typ) trm
+       case over of
+         Just trty -> return trty
+         _ -> do
+          (trm',ty') <- infer trm
+          termWith trm' $ checkEq typ ty' trm'
+
     T _ [] ->
       prtFail "found empty table in type" typ
     T _ cs -> case typ of 
diff --git a/src/GF/Compile/Compile.hs b/src/GF/Compile/Compile.hs
index 13d2129b7..0e59b1c9d 100644
--- a/src/GF/Compile/Compile.hs
+++ b/src/GF/Compile/Compile.hs
@@ -281,7 +281,7 @@ compileSourceModule opts env@(k,gr,can,eenv) mo@(i,mi) = do
       (mo3:_,warnings) <- putpp "  type checking" $ ioeErr $ showCheckModule mos mo2
       if null warnings then return () else putp warnings $ return ()
 
-      (k',mo3r:_) <- ioeErr $ refreshModule (k,mos) mo3
+      (k',mo3r:_) <- putpp "  refreshing " $ ioeErr $ refreshModule (k,mos) mo3
 
       (mo4,eenv') <- 
         ---- if oElem "check_only" opts