diff --git a/doc/gf-history.html b/doc/gf-history.html
index 8d60df09f..8f92aa582 100644
--- a/doc/gf-history.html
+++ b/doc/gf-history.html
@@ -14,6 +14,33 @@ Changes in functionality since May 17, 2005, release of GF Version 2.2
 
 <p>
 
+21/12 (AR) Overloading rules for GF version 2.7:
+<ol>
+<li> If a unique instance is found by exact match with argument types,
+  that instance is used.
+<li> Otherwise, if exact match with the expected value type gives a
+  uniques instance, that instance is used.
+<li> Otherwise, if among possible instances only one returns a non-function
+  type, that instance is used, but a warning is issued.
+<li> Otherwise, an error results, and the list of possible instances is shown.
+</ol>
+These rules are still temporary, but all future developments will guarantee
+that their type-correct use will work. Rule (3) is only needed because the 
+current type checker does not always know an expected type. It can give
+an incorrect result which is captured later in the compilation. To be noticed,
+in particular, is that exact match is required. Match by subtyping will be
+investigated later.
+
+<p>
+
+20/11 (AR) Type error messages in concrete syntax are printed with a
+heuristic where a type of the form <tt>{... ; lock_C : {} ; ...}</tt>
+is printed as <tt>C</tt>. This gives more readable error messages, but
+can produce wrong results if lock fields are hand-written or if subtypes
+of lock-fielded categories are used.
+
+<p>
+
 17/11 (AR) Operation overloading: an <tt>oper</tt> can have many types,
 from which one is picked at compile time. The types must have different
 argument lists. Exact match with the arguments given to the <tt>oper</tt>
diff --git a/examples/logic/ArithmEng.gf b/examples/logic/ArithmEng.gf
index 1ab4c2abd..21b68dd03 100644
--- a/examples/logic/ArithmEng.gf
+++ b/examples/logic/ArithmEng.gf
@@ -24,8 +24,8 @@ lin
 
   one = UsePN (regPN "one") ;
   two = UsePN (regPN "two") ;
-  sum = appColl (regN2 "sum") ;
-  prod = appColl (regN2 "product") ;
+  sum = app (regN2 "sum") ;
+  prod = app (regN2 "product") ;
 
   evax1 = 
     proof (by (ref (mkLabel ["the first axiom of evenness ,"]))) 
@@ -42,14 +42,14 @@ lin
 
   eqax1 = 
     proof (by (ref (mkLabel ["the first axiom of equality ,"]))) 
-      (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) 
+      (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
          (UsePN (regPN "zero")) 
          (UsePN (regPN "zero")))) ;
 
   eqax2 m n c = 
     appendText c 
       (proof (by (ref (mkLabel ["the second axiom of equality ,"]))) 
-        (mkS (predA2 (mkA2 (regA "equal") (mkPrep "to")) 
+        (mkS (pred (mkA2 (regA "equal") (mkPrep "to")) 
           (appN2 (regN2 "successor") m) (appN2 (regN2 "successor") n)))) ;
 
   IndNat C d e = {s = 
diff --git a/examples/logic/LogicI.gf b/examples/logic/LogicI.gf
index 1f9b08e41..3598022ac 100644
--- a/examples/logic/LogicI.gf
+++ b/examples/logic/LogicI.gf
@@ -28,7 +28,7 @@ lin
   Univ A B = 
     AdvS 
       (mkAdv for_Prep (mkNP all_Predet 
-        (mkNP (mkDet (PlQuant IndefArt) NoNum NoOrd) (mkCN A (symb B.$0)))))
+        (mkNP (mkDet (PlQuant IndefArt)) (mkCN A (symb B.$0)))))
       B ;
 
   DisjIl A B a = proof a (proof afortiori (coord or_Conj A B)) ;
diff --git a/examples/logic/Prooftext.gf b/examples/logic/Prooftext.gf
index 4c193740a..1833d6308 100644
--- a/examples/logic/Prooftext.gf
+++ b/examples/logic/Prooftext.gf
@@ -55,7 +55,7 @@ oper
     proof : Decl -> Proof
       = \d -> d ;
     proof : Proof -> Proof -> Proof
-      = \p,q -> appendText p q ;
+      = appendText ;
     proof : Branching -> Proofs -> Proof
       = \b,ps -> mkText (mkPhr b) ps
     } ;
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index 86c761e89..53c8dbab9 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -211,7 +211,7 @@ checkResInfo gr mo (c,info) = do
    checkUniq xss = case xss of
      x:y:xs 
       | x == y -> raise $ "ambiguous for argument list" +++ 
-                         unwords (map prtType x)  
+                         unwords (map (prtType gr) x)  
       | otherwise -> checkUniq $ y:xs
      _ -> return ()
 
@@ -412,7 +412,7 @@ inferLType gr trm = case trm of
                       else substituteLType [(z,a')] val
              return (App f' a',ty) 
            _ -> raise ("function type expected for"+++ 
-                      prt f +++"instead of" +++ prtType fty)
+                      prt f +++"instead of" +++ prtType env fty)
 
    S f x -> do
      (f', fty) <- infer f
@@ -596,14 +596,22 @@ getOverload env@gr mt t = case appForm t of
      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]
+         maybe [] (("when expecting" +++) . prtType env) mt +++
+         "for" +++ unwords (map (prtType env) tys) +++ "among" ++++ 
+         unlines [unwords (map (prtType env) ty) | (ty,_) <- typs]
       ----  ++++ "DEBUG" +++ unwords (map show tys) +++ ";" 
       ----  ++++ unlines (map (show . fst) typs) ----
-       _ -> raise $ "ambiguous overloading of" +++ prt f +++
-         "for" +++ unwords (map prtType tys) ++++ "with alternatives" ++++ 
-         unlines [prtType ty | (ty,_) <- vfs]
+
+       vfs' -> case [(v,f) | (v,f) <- vfs', noProd v] of
+         [(val,fun)] -> do
+           checkWarn $ "WARNING: overloading of" +++ prt f +++ 
+             "resolved by excluding partial applications:" ++++
+             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
+           return (mkApp fun tts, val)
+
+         _ -> raise $ "ambiguous overloading of" +++ prt f +++
+           "for" +++ unwords (map (prtType env) tys) ++++ "with alternatives" ++++ 
+           unlines [prtType env ty | (ty,_) <- vfs']
 
    ---- TODO: accept subtypes
    ---- TODO: use a trie
@@ -614,6 +622,9 @@ getOverload env@gr mt t = case appForm t of
        pre == tys
      ]
 
+   noProd ty = case ty of
+     Prod _ _ _ -> False
+     _ -> True
 
 checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
 checkLType env trm typ0 = do
@@ -633,7 +644,7 @@ checkLType env trm typ0 = do
                           check c b'
           checkReset
           return $ (Abs x c', Prod x a b')
-        _ -> raise $ "product expected instead of" +++ prtType typ
+        _ -> raise $ "product expected instead of" +++ prtType env typ
 
     App f a -> do
        over <- getOverload env (Just typ) trm
@@ -659,7 +670,7 @@ checkLType env trm typ0 = do
           _ -> return () -- happens with variable types
         cs' <- mapM (checkCase arg val) cs
         return (T (TTyped arg) cs', typ)
-      _ -> raise $ "table type expected for table instead of" +++ prtType typ
+      _ -> raise $ "table type expected for table instead of" +++ prtType env typ
 
     R r -> case typ of --- why needed? because inference may be too difficult
        RecType rr -> do
@@ -715,7 +726,7 @@ checkLType env trm typ0 = do
           checkEq typ t trm
           return (S tab' arg', t)
         _ -> raise $ "table type expected for applied table instead of" +++ 
-                   prtType ty'
+                   prtType env ty'
      , do
       (arg',ty) <- infer arg
       ty'       <- comp ty
@@ -844,21 +855,26 @@ check2 chk con a b t = do
 
 checkEqLType :: LTEnv -> Type -> Type -> Term -> Check Type
 checkEqLType env t u trm = do
+  (b,t',u',s) <- checkIfEqLType env t u trm
+  case b of
+    True  -> return t'
+    False -> raise $ s +++ "type of" +++ prt trm +++ 
+                        ": expected:" +++ prtType env t ++++ 
+                        "inferred:" +++ prtType env u
+
+checkIfEqLType :: LTEnv -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
+checkIfEqLType env t u trm = do
   t' <- comp t 
   u' <- comp u
   case t' == u' || alpha [] t' u' of
-    True -> return t'
+    True -> return (True,t',u',[])
     -- forgive missing lock fields by only generating a warning.
     --- better: use a flag to forgive? (AR 31/1/2006)
     _ -> case missingLock [] t' u' of
       Ok lo -> do
         checkWarn $ "WARNING: missing lock field" +++ unwords (map prt lo)
-        return t'
-      Bad s -> raise (s +++ "type of" +++ prt trm +++ 
-                ": expected:" +++ prtType t' ++++ 
-                "inferred:" +++ prtType u'
-            ----    +++++ "DEBUG:" ++++ show t' ++++ show u'
-                )
+        return (True,t',u',[])
+      Bad s -> return (False,t',u',s)
  where
 
    -- t is a subtype of u 
@@ -920,13 +936,17 @@ checkEqLType env t u trm = do
    comp = computeLType env
 
 -- printing a type with a lock field lock_C as C
-prtType :: Type -> String
-prtType ty = case ty of
+prtType :: LTEnv -> Type -> String
+prtType env ty = case ty of
   RecType fs -> case filter isLockLabel $ map fst fs of
     [lock] -> (drop 5 $ prt lock) --- ++++ "Full form" +++ prt ty
-    _ -> prt ty
-  Prod x a b -> prtType a +++ "->" +++ prtType b
-  _ -> prt ty
+    _ -> prtt ty
+  Prod x a b -> prtType env a +++ "->" +++ prtType env b
+  _ -> prtt ty
+ where
+   prtt t = prt t
+   ---- use computeLType gr to check if really equal to the cat with lock
+
 
 -- | linearization types and defaults
 linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)