Merge branch 'master' of https://github.com/GrammaticalFramework/gf-core

18 files changed, 1206 insertions, 1846 deletions

diff --git a/src/compiler/GF/Compile/CFGtoPGF.hs b/src/compiler/GF/Compile/CFGtoPGF.hs
index f9ab8afcf..59448ce97 100644
--- a/src/compiler/GF/Compile/CFGtoPGF.hs
+++ b/src/compiler/GF/Compile/CFGtoPGF.hs
@@ -18,7 +18,7 @@ import Data.List
 --------------------------
 
 cf2pgf :: FilePath -> ParamCFG -> PGF
-cf2pgf fpath cf = 
+cf2pgf fpath cf =
  let pgf = PGF Map.empty aname (cf2abstr cf) (Map.singleton cname (cf2concr cf))
  in updateProductionIndices pgf
  where
@@ -33,7 +33,7 @@ cf2abstr cfg = Abstr aflags afuns acats
 
     acats  = Map.fromList [(cat, ([], [(0,mkRuleName rule) | rule <- rules], 0))
                             | (cat,rules) <- (Map.toList . Map.fromListWith (++))
-                                                [(cat2id cat, catRules cfg cat) | 
+                                                [(cat2id cat, catRules cfg cat) |
                                                      cat <- allCats' cfg]]
     afuns  = Map.fromList [(mkRuleName rule, (cftype [cat2id c | NonTerminal c <- ruleRhs rule] (cat2id (ruleLhs rule)), 0, Nothing, 0))
                             | rule <- allRules cfg]
@@ -52,7 +52,7 @@ cf2concr cfg = Concr Map.empty Map.empty
     cats  = allCats' cfg
     rules = allRules cfg
 
-    sequences0 = Set.fromList (listArray (0,0) [SymCat 0 0] : 
+    sequences0 = Set.fromList (listArray (0,0) [SymCat 0 0] :
                                map mkSequence rules)
     sequences  = listArray (0,Set.size sequences0-1) (Set.toList sequences0)
 
@@ -102,7 +102,7 @@ cf2concr cfg = Concr Map.empty Map.empty
 
     mkLinDefRef (cat,_) =
       (cat2fid cat 0,[0])
-      
+
     addProd prods (fid,prod) =
       case IntMap.lookup fid prods of
         Just set -> IntMap.insert fid (Set.insert prod set) prods
@@ -130,5 +130,5 @@ cf2concr cfg = Concr Map.empty Map.empty
 
 mkRuleName rule =
   case ruleName rule of
-	CFObj n _ -> n
-	_         -> wildCId
+    CFObj n _ -> n
+    _         -> wildCId
diff --git a/src/compiler/GF/Compile/CheckGrammar.hs b/src/compiler/GF/Compile/CheckGrammar.hs
index 24582bba2..7f053f85c 100644
--- a/src/compiler/GF/Compile/CheckGrammar.hs
+++ b/src/compiler/GF/Compile/CheckGrammar.hs
@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/11/11 23:24:33 $ 
+-- > CVS $Date: 2005/11/11 23:24:33 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.31 $
 --
@@ -27,9 +27,9 @@ import GF.Infra.Ident
 import GF.Infra.Option
 
 import GF.Compile.TypeCheck.Abstract
-import GF.Compile.TypeCheck.RConcrete
-import qualified GF.Compile.TypeCheck.ConcreteNew as CN
-import qualified GF.Compile.Compute.ConcreteNew as CN
+import GF.Compile.TypeCheck.Concrete(computeLType,checkLType,inferLType,ppType)
+import qualified GF.Compile.TypeCheck.ConcreteNew as CN(checkLType,inferLType)
+import qualified GF.Compile.Compute.Concrete as CN(normalForm,resourceValues)
 
 import GF.Grammar
 import GF.Grammar.Lexer
@@ -74,9 +74,9 @@ checkRestrictedInheritance cwd sgr (name,mo) = checkInModule cwd mo NoLoc empty
      let (incl,excl) = partition (isInherited mi) (Map.keys (jments m))
      let incld c   = Set.member c (Set.fromList incl)
      let illegal c = Set.member c (Set.fromList excl)
-     let illegals = [(f,is) | 
+     let illegals = [(f,is) |
            (f,cs) <- allDeps, incld f, let is = filter illegal cs, not (null is)]
-     case illegals of 
+     case illegals of
        [] -> return ()
        cs -> checkWarn ("In inherited module" <+> i <> ", dependence of excluded constants:" $$
                          nest 2 (vcat [f <+> "on" <+> fsep is | (f,is) <- cs]))
@@ -92,12 +92,12 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
 
   -- check that all abstract constants are in concrete; build default lin and lincats
   jsc <- foldM checkAbs jsc (Map.toList jsa)
-  
+
   return (cm,cnc{jments=jsc})
   where
    checkAbs js i@(c,info) =
      case info of
-       AbsFun (Just (L loc ty)) _ _ _ 
+       AbsFun (Just (L loc ty)) _ _ _
            -> do let mb_def = do
                        let (cxt,(_,i),_) = typeForm ty
                        info <- lookupIdent i js
@@ -136,11 +136,11 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
            checkWarn ("no linearization type for" <+> c <> ", inserting default {s : Str}")
            return $ Map.insert c (CncCat (Just (L NoLoc defLinType)) Nothing Nothing Nothing Nothing) js
        _ -> return js
-     
+
    checkCnc js (c,info) =
      case info of
        CncFun _ d mn mf -> case lookupOrigInfo gr (am,c) of
-                             Ok (_,AbsFun (Just (L _ ty)) _ _ _) -> 
+                             Ok (_,AbsFun (Just (L _ ty)) _ _ _) ->
                                         do (cont,val) <- linTypeOfType gr cm ty
                                            let linty = (snd (valCat ty),cont,val)
                                            return $ Map.insert c (CncFun (Just linty) d mn mf) js
@@ -159,14 +159,14 @@ checkCompleteGrammar opts cwd gr (am,abs) (cm,cnc) = checkInModule cwd cnc NoLoc
        _ -> return $ Map.insert c info js
 
 
--- | General Principle: only Just-values are checked. 
+-- | General Principle: only Just-values are checked.
 -- A May-value has always been checked in its origin module.
 checkInfo :: Options -> FilePath -> SourceGrammar -> SourceModule -> Ident -> Info -> Check Info
 checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
   checkReservedId c
   case info of
-    AbsCat (Just (L loc cont)) -> 
-      mkCheck loc "the category" $ 
+    AbsCat (Just (L loc cont)) ->
+      mkCheck loc "the category" $
         checkContext gr cont
 
     AbsFun (Just (L loc typ0)) ma md moper -> do
@@ -175,13 +175,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
         checkTyp gr typ
       case md of
         Just eqs -> mapM_ (\(L loc eq) -> mkCheck loc "the definition of function" $
-	                                        checkDef gr (m,c) typ eq) eqs
+                                          checkDef gr (m,c) typ eq) eqs
         Nothing  -> return ()
       return (AbsFun (Just (L loc typ)) ma md moper)
 
     CncCat mty mdef mref mpr mpmcfg -> do
       mty  <- case mty of
-                Just (L loc typ) -> chIn loc "linearization type of" $ 
+                Just (L loc typ) -> chIn loc "linearization type of" $
                                      (if False --flag optNewComp opts
                                         then do (typ,_) <- CN.checkLType (CN.resourceValues opts gr) typ typeType
                                                 typ  <- computeLType gr [] typ
@@ -191,19 +191,19 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
                                                 return (Just (L loc typ)))
                 Nothing          -> return Nothing
       mdef <- case (mty,mdef) of
-                (Just (L _ typ),Just (L loc def)) -> 
+                (Just (L _ typ),Just (L loc def)) ->
                     chIn loc "default linearization of" $ do
                        (def,_) <- checkLType gr [] def (mkFunType [typeStr] typ)
                        return (Just (L loc def))
                 _ -> return Nothing
       mref <- case (mty,mref) of
-                (Just (L _ typ),Just (L loc ref)) -> 
+                (Just (L _ typ),Just (L loc ref)) ->
                     chIn loc "reference linearization of" $ do
                        (ref,_) <- checkLType gr [] ref (mkFunType [typ] typeStr)
                        return (Just (L loc ref))
                 _ -> return Nothing
       mpr  <- case mpr of
-                (Just (L loc t)) -> 
+                (Just (L loc t)) ->
                     chIn loc "print name of" $ do
                        (t,_) <- checkLType gr [] t typeStr
                        return (Just (L loc t))
@@ -212,13 +212,13 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
 
     CncFun mty mt mpr mpmcfg -> do
       mt <- case (mty,mt) of
-              (Just (cat,cont,val),Just (L loc trm)) -> 
+              (Just (cat,cont,val),Just (L loc trm)) ->
                   chIn loc "linearization of" $ do
                      (trm,_) <- checkLType gr [] trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
                      return (Just (L loc trm))
               _ -> return mt
       mpr  <- case mpr of
-                (Just (L loc t)) -> 
+                (Just (L loc t)) ->
                     chIn loc "print name of" $ do
                        (t,_) <- checkLType gr [] t typeStr
                        return (Just (L loc t))
@@ -251,16 +251,16 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
     ResOverload os tysts -> chIn NoLoc "overloading" $ do
       tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType gr [] t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts  -- return explicit ones
       tysts0 <- lookupOverload gr (m,c)  -- check against inherited ones too
-      tysts1 <- mapM (uncurry $ flip (checkLType gr [])) 
+      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
-      checkUniq $ 
+      checkUniq $
         sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
       return (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (L loc pcs)) _ -> do
-      ts <- chIn loc "parameter type" $ 
+      ts <- chIn loc "parameter type" $
               liftM concat $ mapM mkPar pcs
       return (ResParam (Just (L loc pcs)) (Just ts))
 
@@ -274,9 +274,9 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
        return $ map (mkApp (QC (m,f))) vs
 
    checkUniq xss = case xss of
-     x:y:xs 
+     x:y:xs
       | x == y    -> checkError $ "ambiguous for type" <+>
-                                  ppType (mkFunType (tail x) (head x))  
+                                  ppType (mkFunType (tail x) (head x))
       | otherwise -> checkUniq $ y:xs
      _ -> return ()
 
@@ -294,7 +294,7 @@ checkInfo opts cwd sgr (m,mo) c info = checkInModule cwd mo NoLoc empty $ do
        t' <- compAbsTyp ((x,Vr x):g) t
        return $ Prod b x a' t'
      Abs _ _ _ -> return t
-     _ -> composOp (compAbsTyp g) t  
+     _ -> composOp (compAbsTyp g) t
 
 
 -- | for grammars obtained otherwise than by parsing ---- update!!
@@ -316,7 +316,7 @@ linTypeOfType cnc m typ = do
    mkLinArg (i,(n,mc@(m,cat))) = do
      val  <- lookLin mc
      let vars = mkRecType varLabel $ replicate n typeStr
-	 symb = argIdent n cat i
+         symb = argIdent n cat i
      rec <- if n==0 then return val else
                        errIn (render ("extending" $$
                                       nest 2 vars $$
diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs
index f411f2ca0..47e2f5cde 100644
--- a/src/compiler/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/GF/Compile/Compute/Concrete.hs
@@ -1,3 +1,590 @@
-module GF.Compile.Compute.Concrete{-(module M)-} where
---import GF.Compile.Compute.ConcreteLazy as M -- New
---import GF.Compile.Compute.ConcreteStrict as M -- Old, inefficient
+-- | Functions for computing the values of terms in the concrete syntax, in
+-- | preparation for PMCFG generation.
+module GF.Compile.Compute.Concrete
+           (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
+            normalForm,
+            Value(..), Bind(..), Env, value2term, eval, vapply
+           ) where
+import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
+
+import GF.Grammar hiding (Env, VGen, VApp, VRecType)
+import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
+import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
+import GF.Grammar.PatternMatch(matchPattern,measurePatt)
+import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
+import GF.Compile.Compute.Value hiding (Error)
+import GF.Compile.Compute.Predef(predef,predefName,delta)
+import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
+import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
+import GF.Data.Utilities(mapFst,mapSnd)
+import GF.Infra.Option
+import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
+import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
+--import Data.Char (isUpper,toUpper,toLower)
+import GF.Text.Pretty
+import qualified Data.Map as Map
+import Debug.Trace(trace)
+
+-- * Main entry points
+
+normalForm :: GlobalEnv -> L Ident -> Term -> Term
+normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
+
+nfx :: GlobalEnv -> Term -> Err Term
+nfx env@(GE _ _ _ loc) t = do
+  v <- eval env [] t
+  return (value2term loc [] v)
+    -- Old value2term error message:
+    -- Left i  -> fail ("variable #"++show i++" is out of scope")
+
+eval :: GlobalEnv -> Env -> Term -> Err Value
+eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
+  where
+    cenv = CE gr rvs opts loc (map fst env)
+
+--apply env = apply' env
+
+--------------------------------------------------------------------------------
+
+-- * Environments
+
+type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
+
+data GlobalEnv = GE Grammar ResourceValues Options GLocation
+data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
+                       opts::Options,
+                       gloc::GLocation,local::LocalScope}
+type GLocation = L Ident
+type LocalScope = [Ident]
+type Stack = [Value]
+type OpenValue = Stack->Value
+
+geLoc     (GE _ _ _ loc) = loc
+geGrammar (GE gr _ _ _)  = gr
+
+ext b env = env{local=b:local env}
+extend bs env = env{local=bs++local env}
+global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
+
+var :: CompleteEnv -> Ident -> Err OpenValue
+var env x = maybe unbound pick' (elemIndex x (local env))
+  where
+    unbound = fail ("Unknown variable: "++showIdent x)
+    pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
+    err i vs = bug $ "Stack problem: "++showIdent x++": "
+                    ++unwords (map showIdent (local env))
+                    ++" => "++show (i,length vs)
+    ok v = --trace ("var "++show x++" = "++show v) $
+           v
+
+pick :: Int -> Stack -> Maybe Value
+pick 0 (v:_) = Just v
+pick i (_:vs) = pick (i-1) vs
+pick i vs = Nothing -- bug $ "pick "++show (i,vs)
+
+resource env (m,c) =
+--  err bug id $
+    if isPredefCat c
+    then value0 env =<< lockRecType c defLinType -- hmm
+    else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
+  where e = fail $ "Not found: "++render m++"."++showIdent c
+
+-- | Convert operators once, not every time they are looked up
+resourceValues :: Options -> SourceGrammar -> GlobalEnv
+resourceValues opts gr = env
+  where
+    env = GE gr rvs opts (L NoLoc identW)
+    rvs = Map.mapWithKey moduleResources (moduleMap gr)
+    moduleResources m = Map.mapWithKey (moduleResource m) . jments
+    moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
+                                  let loc = L l c
+                                      qloc = L l (Q (m,c))
+                                  eval (GE gr rvs opts loc) [] (traceRes qloc t)
+
+    traceRes = if flag optTrace opts
+               then traceResource
+               else const id
+
+-- * Tracing
+
+-- | Insert a call to the trace function under the top-level lambdas
+traceResource (L l q) t =
+  case termFormCnc t of
+    (abs,body) -> mkAbs abs (mkApp traceQ [args,body])
+      where
+        args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
+        lstr = render (l<>":"<>ppTerm Qualified 0 q)
+        traceQ = Q (cPredef,cTrace)
+
+-- * Computing values
+
+-- | Computing the value of a top-level term
+value0 :: CompleteEnv -> Term -> Err Value
+value0 env = eval (global env) []
+
+-- | Computing the value of a term
+value :: CompleteEnv -> Term -> Err OpenValue
+value env t0 =
+  -- Each terms is traversed only once by this function, using only statically
+  -- available information. Notably, the values of lambda bound variables
+  -- will be unknown during the term traversal phase.
+  -- The result is an OpenValue, which is a function that may be applied many
+  -- times to different dynamic values, but without the term traversal overhead
+  -- and without recomputing other statically known information.
+  -- For this to work, there should be no recursive calls under lambdas here.
+  -- Whenever we need to construct the OpenValue function with an explicit
+  -- lambda, we have to lift the recursive calls outside the lambda.
+  -- (See e.g. the rules for Let, Prod and Abs)
+{-
+  trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
+                                      brackets (fsep (map ppIdent (local env))),
+                                      ppTerm Unqualified 10 t0]) $
+--}
+  errIn (render t0) $
+  case t0 of
+    Vr x   -> var env x
+    Q x@(m,f)
+      | m == cPredef -> if f==cErrorType                -- to be removed
+                        then let p = identS "P"
+                             in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
+                        else if f==cPBool
+                               then const # resource env x
+                               else const . flip VApp [] # predef f
+      | otherwise    -> const # resource env x --valueResDef (fst env) x
+    QC x   -> return $ const (VCApp x [])
+    App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
+    Let (x,(oty,t)) body -> do vb <- value (ext x env) body
+                               vt <- value env t
+                               return $ \ vs -> vb (vt vs:vs)
+    Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
+    Prod bt x t1 t2 ->
+       do vt1 <- value env t1
+          vt2 <- value (ext x env) t2
+          return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
+    Abs bt x t -> do vt <- value (ext x env) t
+                     return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
+    EInt n -> return $ const (VInt n)
+    EFloat f -> return $ const (VFloat f)
+    K s -> return $ const (VString s)
+    Empty -> return $ const (VString "")
+    Sort s | s == cTok -> return $ const (VSort cStr)        -- to be removed
+           | otherwise -> return $ const (VSort s)
+    ImplArg t -> (VImplArg.) # value env t
+    Table p res -> liftM2 VTblType # value env p <# value env res
+    RecType rs -> do lovs <- mapPairsM (value env) rs
+                     return $ \vs->VRecType $ mapSnd ($vs) lovs
+    t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
+    FV ts   -> ((vfv .) # sequence) # mapM (value env) ts
+    R as    -> do lovs <- mapPairsM (value env.snd) as
+                  return $ \ vs->VRec $ mapSnd ($vs) lovs
+    T i cs  -> valueTable env i cs
+    V ty ts -> do pvs <- paramValues env ty
+                  ((VV ty pvs .) . sequence) # mapM (value env) ts
+    C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
+    S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
+    P t l   -> --maybe (bug $ "project "++show l++" from "++show v) id $
+               do ov <- value env t
+                  return $ \ vs -> let v = ov vs
+                                   in maybe (VP v l) id (proj l v)
+    Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
+    Strs ts    -> ((VStrs.) # sequence) # mapM (value env) ts
+    Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
+    ELin c r -> (unlockVRec (gloc env) c.) # value env r
+    EPatt p  -> return $ const (VPatt p) -- hmm
+    EPattType ty -> do vt <- value env ty
+                       return (VPattType . vt)
+    Typed t ty -> value env t
+    t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
+
+vconcat vv@(v1,v2) =
+    case vv of
+      (VString "",_) -> v2
+      (_,VString "") -> v1
+      (VApp NonExist _,_) -> v1
+      (_,VApp NonExist _) -> v2
+      _ -> VC v1 v2
+
+proj l v | isLockLabel l = return (VRec [])
+                ---- a workaround 18/2/2005: take this away and find the reason
+                ---- why earlier compilation destroys the lock field
+proj l v =
+    case v of
+      VFV vs -> liftM vfv (mapM (proj l) vs)
+      VRec rs -> lookup l rs
+--    VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
+      VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
+      _ -> return (ok1 VP v l)
+
+ok1 f v1@(VError {}) _ = v1
+ok1 f v1 v2 = f v1 v2
+
+ok2 f v1@(VError {}) _ = v1
+ok2 f _ v2@(VError {}) = v2
+ok2 f v1 v2 = f v1 v2
+
+ok2p f (v1@VError {},_) = v1
+ok2p f (_,v2@VError {}) = v2
+ok2p f vv = f vv
+
+unlockVRec loc c0 v0 = v0
+{-
+unlockVRec loc c0 v0 = unlockVRec' c0 v0
+  where
+    unlockVRec' ::Ident -> Value -> Value
+    unlockVRec' c v =
+        case v of
+    --    VClosure env t -> err bug (VClosure env) (unlockRecord c t)
+          VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
+          VRec rs        -> plusVRec rs lock
+    --    _              -> VExtR v (VRec lock) -- hmm
+          _              -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
+    --    _              -> bugloc loc $ "unlock non-record "++show v0
+      where
+        lock = [(lockLabel c,VRec [])]
+-}
+
+-- suspicious, but backwards compatible
+plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
+  where ls2 = map fst rs2
+
+extR t vv =
+    case vv of
+      (VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
+      (v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
+      (VRecType rs1, VRecType rs2) ->
+          case intersect (map fst rs1) (map fst rs2) of
+            [] -> VRecType (rs1 ++ rs2)
+            ls -> error $ "clash"<+>show ls
+      (VRec     rs1, VRec     rs2) -> plusVRec rs1 rs2
+      (v1          , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
+      (VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
+--    (v1,v2) -> ok2 VExtR v1 v2 -- hmm
+      (v1,v2) -> error $ "not records" $$ show v1 $$ show v2
+  where
+    error explain = ppbug $ "The term" <+> t
+                            <+> "is not reducible" $$ explain
+
+glue env (v1,v2) = glu v1 v2
+  where
+    glu v1 v2 =
+        case (v1,v2) of
+          (VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
+          (v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
+          (VString s1,VString s2) -> VString (s1++s2)
+          (v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
+             where glx v2 = glu v1 v2
+          (v1@(VAlts {}),v2) ->
+           --err (const (ok2 VGlue v1 v2)) id $
+             err bug id $
+             do y' <- strsFromValue v2
+                x' <- strsFromValue v1
+                return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
+          (VC va vb,v2) -> VC va (glu vb v2)
+          (v1,VC va vb) -> VC (glu v1 va) vb
+          (VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
+          (v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
+          (v1@(VApp NonExist _),_) -> v1
+          (_,v2@(VApp NonExist _)) -> v2
+--        (v1,v2) -> ok2 VGlue v1 v2
+          (v1,v2) -> if flag optPlusAsBind (opts env)
+                       then VC v1 (VC (VApp BIND []) v2)
+                       else let loc  = gloc env
+                                vt v = value2term loc (local env) v
+                                        -- Old value2term error message:
+                                        --  Left i  -> Error ('#':show i)
+                                originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
+                                                               (Glue (vt v1) (vt v2)))
+                                term = render $ pp  $ Glue (vt v1) (vt v2)
+                            in error $ unlines
+                                [originalMsg
+                                ,""
+                                ,"There was a problem in the expression `"++term++"`, either:"
+                                ,"1) You are trying to use + on runtime arguments, possibly via an oper."
+                                ,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
+                                ,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
+                                ]
+
+
+-- | to get a string from a value that represents a sequence of terminals
+strsFromValue :: Value -> Err [Str]
+strsFromValue t = case t of
+  VString s   -> return [str s]
+  VC s t -> do
+    s' <- strsFromValue s
+    t' <- strsFromValue t
+    return [plusStr x y | x <- s', y <- t']
+{-
+  VGlue s t -> do
+    s' <- strsFromValue s
+    t' <- strsFromValue t
+    return [glueStr x y | x <- s', y <- t']
+-}
+  VAlts d vs -> do
+    d0 <- strsFromValue d
+    v0 <- mapM (strsFromValue . fst) vs
+    c0 <- mapM (strsFromValue . snd) vs
+  --let vs' = zip v0 c0
+    return [strTok (str2strings def) vars |
+              def  <- d0,
+              vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] |
+                                                          vv <- sequence v0]
+           ]
+  VFV ts -> concat # mapM strsFromValue ts
+  VStrs ts -> concat # mapM strsFromValue ts
+
+  _ -> fail ("cannot get Str from value " ++ show t)
+
+vfv vs = case nub vs of
+           [v] -> v
+           vs -> VFV vs
+
+select env vv =
+    case vv of
+      (v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
+      (VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
+      (v1@(VV pty vs rs),v2) ->
+         err (const (VS v1 v2)) id $
+         do --ats <- allParamValues (srcgr env) pty
+            --let vs = map (value0 env) ats
+            i <- maybeErr "no match" $ findIndex (==v2) vs
+            return (ix (gloc env) "select" rs i)
+      (VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
+      (v1@(VT _ _ cs),v2) ->
+                 err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
+                 match (gloc env) cs v2
+      (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
+      (v1,v2) -> ok2 VS v1 v2
+
+match loc cs v =
+  err bad return (matchPattern cs (value2term loc [] v))
+    -- Old value2term error message:
+    -- Left i  -> bad ("variable #"++show i++" is out of scope")
+  where
+    bad = fail . ("In pattern matching: "++)
+
+valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
+valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
+
+valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
+valueTable env i cs =
+    case i of
+      TComp ty -> do pvs <- paramValues env ty
+                     ((VV ty pvs .) # sequence) # mapM (value env.snd) cs
+      _ -> do ty <- getTableType i
+              cs' <- mapM valueCase cs
+              err (dynamic cs' ty) return (convert cs' ty)
+  where
+    dynamic cs' ty _ = cases cs' # value env ty
+
+    cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
+      where
+        keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
+                   VT wild (vty vs) (mapSnd ($vs) cs')
+
+    wild = case i of TWild _ -> True; _ -> False
+
+    convertv cs' vty =
+      convert' cs' =<< paramValues'' env (value2term (gloc env) [] vty)
+        -- Old value2term error message: Left i    -> fail ("variable #"++show i++" is out of scope")
+
+    convert cs' ty = convert' cs' =<< paramValues' env ty
+
+    convert' cs' ((pty,vs),pvs) =
+      do sts  <- mapM (matchPattern cs') vs
+         return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
+                                           (mapFst ($vs) sts)
+
+    valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
+                         pvs <- linPattVars p'
+                         vt <- value (extend pvs env) t
+                         return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
+
+    inlinePattMacro p =
+        case p of
+          PM qc -> do r <- resource env qc
+                      case r of
+                        VPatt p' -> inlinePattMacro p'
+                        _ -> ppbug $ hang "Expected pattern macro:" 4
+                                          (show r)
+          _ -> composPattOp inlinePattMacro p
+
+
+paramValues env ty = snd # paramValues' env ty
+
+paramValues' env ty = paramValues'' env =<< nfx (global env) ty
+
+paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
+                           pvs <- mapM (eval (global env) []) ats
+                           return ((pty,ats),pvs)
+
+push' p bs xs = if length bs/=length xs
+                then bug $ "push "++show (p,bs,xs)
+                else push bs xs
+
+push :: Env -> LocalScope -> Stack -> Stack
+push bs [] vs = vs
+push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
+  where  err = bug $ "Unbound pattern variable "++showIdent x
+
+apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
+apply' env t [] = value env t
+apply' env t vs =
+  case t of
+    QC x                   -> return $ \ svs -> VCApp x (map ($svs) vs)
+{-
+    Q x@(m,f) | m==cPredef -> return $
+                              let constr = --trace ("predef "++show x) .
+                                           VApp x
+                              in \ svs -> maybe constr id (Map.lookup f predefs)
+                                          $ map ($svs) vs
+              | otherwise  -> do r <- resource env x
+                                 return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
+-}
+    App t1 t2              -> apply' env t1 . (:vs) =<< value env t2
+    _                      -> do fv <- value env t
+                                 return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
+
+vapply :: GLocation -> Value -> [Value] -> Value
+vapply loc v [] = v
+vapply loc v vs =
+  case v of
+    VError {} -> v
+--  VClosure env (Abs b x t) -> beta gr env b x t vs
+    VAbs bt _ (Bind f) -> vbeta loc bt f vs
+    VApp pre vs1 -> delta' pre (vs1++vs)
+      where
+        delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
+                                  in vtrace loc v1 vr
+        delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
+        --msg = const (VApp pre (vs1++vs))
+        msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
+    VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
+    VFV fs -> vfv [vapply loc f vs|f<-fs]
+    VCApp f vs0 -> VCApp f (vs0++vs)
+    VMeta i env vs0 -> VMeta i env (vs0++vs)
+    VGen i vs0 -> VGen i (vs0++vs)
+    v -> bug $ "vapply "++show v++" "++show vs
+
+vbeta loc bt f (v:vs) =
+  case (bt,v) of
+    (Implicit,VImplArg v) -> ap v
+    (Explicit,         v) -> ap v
+  where
+    ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
+    ap v         = vapply loc (f v) vs
+
+vary (VFV vs) = vs
+vary v = [v]
+varyList = mapM vary
+
+{-
+beta env b x t (v:vs) =
+  case (b,v) of
+    (Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
+    (Explicit,         v) -> apply' (ext (x,v) env) t vs
+-}
+
+vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
+  where
+    pv v = case v of
+             VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
+             _ -> ppV v
+    pf (_,VString n) = pp n
+    pf (_,v) = ppV v
+    pa (_,v) = ppV v
+    ppV v = ppTerm Unqualified 10 (value2term' True loc [] v)
+              -- Old value2term error message:
+              -- Left i  -> "variable #" <> pp i <+> "is out of scope"
+
+-- | Convert a value back to a term
+value2term :: GLocation -> [Ident] -> Value -> Term
+value2term = value2term' False
+
+value2term' :: Bool -> p -> [Ident] -> Value -> Term
+value2term' stop loc xs v0 =
+  case v0 of
+    VApp pre vs    -> applyMany (Q (cPredef,predefName pre)) vs
+    VCApp f vs     -> applyMany (QC f)                       vs
+    VGen j vs      -> applyMany (var j)                      vs
+    VMeta j env vs -> applyMany (Meta j)                     vs
+    VProd bt v x f -> Prod bt x (v2t v)  (v2t' x f)
+    VAbs  bt   x f -> Abs  bt x          (v2t' x f)
+    VInt n         -> EInt n
+    VFloat f       -> EFloat f
+    VString s      -> if null s then Empty else K s
+    VSort s        -> Sort s
+    VImplArg v     -> ImplArg (v2t v)
+    VTblType p res -> Table (v2t p) (v2t res)
+    VRecType rs    -> RecType [(l, v2t v) | (l,v) <- rs]
+    VRec as        -> R       [(l, (Nothing, v2t v)) | (l,v) <- as]
+    VV t _ vs      -> V t     (map v2t vs)
+    VT wild v cs   -> T ((if wild then TWild else TTyped) (v2t v)) (map nfcase cs)
+    VFV vs         -> FV (map v2t vs)
+    VC v1 v2       -> C (v2t v1) (v2t v2)
+    VS v1 v2       -> S (v2t v1) (v2t v2)
+    VP v l         -> P (v2t v) l
+    VPatt p        -> EPatt p
+    VPattType v    -> EPattType $ v2t v
+    VAlts v vvs    -> Alts (v2t v) [(v2t x, v2t y) | (x,y) <- vvs]
+    VStrs vs       -> Strs (map v2t vs)
+--  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
+--  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
+    VError err     -> Error err
+  where
+    applyMany f vs = foldl App f (map v2t vs)
+    v2t = v2txs xs
+    v2txs = value2term' stop loc
+    v2t' x f = v2txs (x:xs) (bind f (gen xs))
+
+    var j
+      | j<length xs = Vr (reverse xs !! j)
+      | otherwise   = error ("variable #"++show j++" is out of scope")
+
+
+    pushs xs e = foldr push e xs
+    push x (env,xs) = ((x,gen xs):env,x:xs)
+    gen xs = VGen (length xs) []
+
+    nfcase (p,f) = (,) p (v2txs xs' (bind f env'))
+      where (env',xs') = pushs (pattVars p) ([],xs)
+
+    bind (Bind f) x = if stop
+                      then VSort (identS "...") -- hmm
+                      else f x
+
+
+linPattVars p =
+    if null dups
+    then return pvs
+    else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
+  where
+    allpvs = allPattVars p
+    pvs = nub allpvs
+    dups = allpvs \\ pvs
+
+pattVars = nub . allPattVars
+allPattVars p =
+    case p of
+      PV i    -> [i]
+      PAs i p -> i:allPattVars p
+      _       -> collectPattOp allPattVars p
+
+---
+ix loc fn xs i =
+    if i<n
+    then xs !! i
+    else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
+  where n = length xs
+
+infixl 1 #,<# --,@@
+
+f # x = fmap f x
+mf <# mx  = ap mf mx
+--m1 @@ m2 = (m1 =<<) . m2
+
+both f (x,y) = (,) # f x <# f y
+
+bugloc loc s = ppbug $ ppL loc s
+
+bug msg = ppbug msg
+ppbug doc = error $ render $ hang "Internal error in Compute.Concrete:" 4 doc
diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
deleted file mode 100644
index ea55e77cb..000000000
--- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs
+++ /dev/null
@@ -1,588 +0,0 @@
--- | Functions for computing the values of terms in the concrete syntax, in
--- | preparation for PMCFG generation.
-module GF.Compile.Compute.ConcreteNew
-           (GlobalEnv, GLocation, resourceValues, geLoc, geGrammar,
-            normalForm,
-            Value(..), Bind(..), Env, value2term, eval, vapply
-           ) where
-import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
-
-import GF.Grammar hiding (Env, VGen, VApp, VRecType)
-import GF.Grammar.Lookup(lookupResDefLoc,allParamValues)
-import GF.Grammar.Predef(cPredef,cErrorType,cTok,cStr,cTrace,cPBool)
-import GF.Grammar.PatternMatch(matchPattern,measurePatt)
-import GF.Grammar.Lockfield(isLockLabel,lockRecType) --unlockRecord,lockLabel
-import GF.Compile.Compute.Value hiding (Error)
-import GF.Compile.Compute.Predef(predef,predefName,delta)
-import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
-import GF.Data.Operations(Err,err,errIn,maybeErr,mapPairsM)
-import GF.Data.Utilities(mapFst,mapSnd)
-import GF.Infra.Option
-import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
-import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
---import Data.Char (isUpper,toUpper,toLower)
-import GF.Text.Pretty
-import qualified Data.Map as Map
-import Debug.Trace(trace)
-
--- * Main entry points
-
-normalForm :: GlobalEnv -> L Ident -> Term -> Term
-normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
-
-nfx env@(GE _ _ _ loc) t = do
-  v <- eval env [] t
-  case value2term loc [] v of
-    Left i  -> fail ("variable #"++show i++" is out of scope")
-    Right t -> return t
-
-eval :: GlobalEnv -> Env -> Term -> Err Value
-eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
-  where
-    cenv = CE gr rvs opts loc (map fst env)
-
---apply env = apply' env
-
---------------------------------------------------------------------------------
-
--- * Environments
-
-type ResourceValues = Map.Map ModuleName (Map.Map Ident (Err Value))
-
-data GlobalEnv = GE Grammar ResourceValues Options GLocation
-data CompleteEnv = CE {srcgr::Grammar,rvs::ResourceValues,
-                       opts::Options,
-                       gloc::GLocation,local::LocalScope}
-type GLocation = L Ident
-type LocalScope = [Ident]
-type Stack = [Value]
-type OpenValue = Stack->Value
-
-geLoc     (GE _ _ _ loc) = loc
-geGrammar (GE gr _ _ _)  = gr
-
-ext b env = env{local=b:local env}
-extend bs env = env{local=bs++local env}
-global env = GE (srcgr env) (rvs env) (opts env) (gloc env)
-
-var :: CompleteEnv -> Ident -> Err OpenValue
-var env x = maybe unbound pick' (elemIndex x (local env))
-  where
-    unbound = fail ("Unknown variable: "++showIdent x)
-    pick' i = return $ \ vs -> maybe (err i vs) ok (pick i vs)
-    err i vs = bug $ "Stack problem: "++showIdent x++": "
-                    ++unwords (map showIdent (local env))
-                    ++" => "++show (i,length vs)
-    ok v = --trace ("var "++show x++" = "++show v) $
-           v
-
-pick :: Int -> Stack -> Maybe Value
-pick 0 (v:_) = Just v
-pick i (_:vs) = pick (i-1) vs
-pick i vs = Nothing -- bug $ "pick "++show (i,vs)
-
-resource env (m,c) =
---  err bug id $
-    if isPredefCat c
-    then value0 env =<< lockRecType c defLinType -- hmm
-    else maybe e id $ Map.lookup c =<< Map.lookup m (rvs env)
-  where e = fail $ "Not found: "++render m++"."++showIdent c
-
--- | Convert operators once, not every time they are looked up
-resourceValues :: Options -> SourceGrammar -> GlobalEnv
-resourceValues opts gr = env
-  where
-    env = GE gr rvs opts (L NoLoc identW)
-    rvs = Map.mapWithKey moduleResources (moduleMap gr)
-    moduleResources m = Map.mapWithKey (moduleResource m) . jments
-    moduleResource m c _info = do L l t <- lookupResDefLoc gr (m,c)
-                                  let loc = L l c
-                                      qloc = L l (Q (m,c))
-                                  eval (GE gr rvs opts loc) [] (traceRes qloc t)
-
-    traceRes = if flag optTrace opts
-               then traceResource
-               else const id
-
--- * Tracing
-
--- | Insert a call to the trace function under the top-level lambdas
-traceResource (L l q) t =
-  case termFormCnc t of
-    (abs,body) -> mkAbs abs (mkApp traceQ [args,body])
-      where
-        args = R $ tuple2record (K lstr:[Vr x|(bt,x)<-abs,bt==Explicit])
-        lstr = render (l<>":"<>ppTerm Qualified 0 q)
-        traceQ = Q (cPredef,cTrace)
-
--- * Computing values
-
--- | Computing the value of a top-level term
-value0 :: CompleteEnv -> Term -> Err Value
-value0 env = eval (global env) []
-
--- | Computing the value of a term
-value :: CompleteEnv -> Term -> Err OpenValue
-value env t0 =
-  -- Each terms is traversed only once by this function, using only statically
-  -- available information. Notably, the values of lambda bound variables 
-  -- will be unknown during the term traversal phase.
-  -- The result is an OpenValue, which is a function that may be applied many
-  -- times to different dynamic values, but without the term traversal overhead
-  -- and without recomputing other statically known information.
-  -- For this to work, there should be no recursive calls under lambdas here.
-  -- Whenever we need to construct the OpenValue function with an explicit
-  -- lambda, we have to lift the recursive calls outside the lambda.
-  -- (See e.g. the rules for Let, Prod and Abs)
-{-
-  trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
-                                      brackets (fsep (map ppIdent (local env))),
-                                      ppTerm Unqualified 10 t0]) $
---}
-  errIn (render t0) $
-  case t0 of
-    Vr x   -> var env x
-    Q x@(m,f)
-      | m == cPredef -> if f==cErrorType                -- to be removed
-                        then let p = identS "P"
-                             in const # value0 env (mkProd [(Implicit,p,typeType)] (Vr p) [])
-                        else if f==cPBool
-                               then const # resource env x
-                               else const . flip VApp [] # predef f
-      | otherwise    -> const # resource env x --valueResDef (fst env) x
-    QC x   -> return $ const (VCApp x [])
-    App e1 e2 -> apply' env e1 . (:[]) =<< value env e2
-    Let (x,(oty,t)) body -> do vb <- value (ext x env) body
-                               vt <- value env t
-                               return $ \ vs -> vb (vt vs:vs)
-    Meta i -> return $ \ vs -> VMeta i (zip (local env) vs) []
-    Prod bt x t1 t2 ->
-       do vt1 <- value env t1
-          vt2 <- value (ext x env) t2
-          return $ \ vs -> VProd bt (vt1 vs) x $ Bind $ \ vx -> vt2 (vx:vs)
-    Abs bt x t -> do vt <- value (ext x env) t
-                     return $ VAbs bt x . Bind . \ vs vx -> vt (vx:vs)
-    EInt n -> return $ const (VInt n)
-    EFloat f -> return $ const (VFloat f)
-    K s -> return $ const (VString s)
-    Empty -> return $ const (VString "")
-    Sort s | s == cTok -> return $ const (VSort cStr)        -- to be removed 
-           | otherwise -> return $ const (VSort s)
-    ImplArg t -> (VImplArg.) # value env t
-    Table p res -> liftM2 VTblType # value env p <# value env res
-    RecType rs -> do lovs <- mapPairsM (value env) rs
-                     return $ \vs->VRecType $ mapSnd ($vs) lovs
-    t@(ExtR t1 t2) -> ((extR t.)# both id) # both (value env) (t1,t2)
-    FV ts   -> ((vfv .) # sequence) # mapM (value env) ts
-    R as    -> do lovs <- mapPairsM (value env.snd) as
-                  return $ \ vs->VRec $ mapSnd ($vs) lovs
-    T i cs  -> valueTable env i cs
-    V ty ts -> do pvs <- paramValues env ty
-                  ((VV ty pvs .) . sequence) # mapM (value env) ts
-    C t1 t2 -> ((ok2p vconcat.) # both id) # both (value env) (t1,t2)
-    S t1 t2 -> ((select env.) # both id) # both (value env) (t1,t2)
-    P t l   -> --maybe (bug $ "project "++show l++" from "++show v) id $
-               do ov <- value env t
-                  return $ \ vs -> let v = ov vs
-                                   in maybe (VP v l) id (proj l v)
-    Alts t tts -> (\v vts -> VAlts # v <# mapM (both id) vts) # value env t <# mapM (both (value env)) tts
-    Strs ts    -> ((VStrs.) # sequence) # mapM (value env) ts
-    Glue t1 t2 -> ((ok2p (glue env).) # both id) # both (value env) (t1,t2)
-    ELin c r -> (unlockVRec (gloc env) c.) # value env r
-    EPatt p  -> return $ const (VPatt p) -- hmm
-    EPattType ty -> do vt <- value env ty
-                       return (VPattType . vt)
-    Typed t ty -> value env t
-    t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
-
-vconcat vv@(v1,v2) =
-    case vv of
-      (VString "",_) -> v2
-      (_,VString "") -> v1
-      (VApp NonExist _,_) -> v1
-      (_,VApp NonExist _) -> v2
-      _ -> VC v1 v2
-
-proj l v | isLockLabel l = return (VRec [])
-                ---- a workaround 18/2/2005: take this away and find the reason
-                ---- why earlier compilation destroys the lock field
-proj l v =
-    case v of
-      VFV vs -> liftM vfv (mapM (proj l) vs)
-      VRec rs -> lookup l rs
---    VExtR v1 v2 -> proj l v2 `mplus` proj l v1 -- hmm
-      VS (VV pty pvs rs) v2 -> flip VS v2 . VV pty pvs # mapM (proj l) rs
-      _ -> return (ok1 VP v l)
-
-ok1 f v1@(VError {}) _ = v1
-ok1 f v1 v2 = f v1 v2
- 
-ok2 f v1@(VError {}) _ = v1
-ok2 f _ v2@(VError {}) = v2
-ok2 f v1 v2 = f v1 v2
-
-ok2p f (v1@VError {},_) = v1
-ok2p f (_,v2@VError {}) = v2
-ok2p f vv = f vv
-
-unlockVRec loc c0 v0 = v0
-{-
-unlockVRec loc c0 v0 = unlockVRec' c0 v0
-  where
-    unlockVRec' ::Ident -> Value -> Value
-    unlockVRec' c v =
-        case v of
-    --    VClosure env t -> err bug (VClosure env) (unlockRecord c t)
-          VAbs bt x (Bind f) -> VAbs bt x (Bind $ \ v -> unlockVRec' c (f v))
-          VRec rs        -> plusVRec rs lock
-    --    _              -> VExtR v (VRec lock) -- hmm
-          _              -> {-trace (render $ ppL loc $ "unlock non-record "++show v0)-} v -- hmm
-    --    _              -> bugloc loc $ "unlock non-record "++show v0
-      where
-        lock = [(lockLabel c,VRec [])]
--}
-
--- suspicious, but backwards compatible
-plusVRec rs1 rs2 = VRec ([(l,v)|(l,v)<-rs1,l `notElem` ls2] ++ rs2)
-  where ls2 = map fst rs2
-
-extR t vv =
-    case vv of
-      (VFV vs,v2) -> vfv [extR t (v1,v2)|v1<-vs]
-      (v1,VFV vs) -> vfv [extR t (v1,v2)|v2<-vs]
-      (VRecType rs1, VRecType rs2) ->
-          case intersect (map fst rs1) (map fst rs2) of
-            [] -> VRecType (rs1 ++ rs2)
-            ls -> error $ "clash"<+>show ls
-      (VRec     rs1, VRec     rs2) -> plusVRec rs1 rs2
-      (v1          , VRec [(l,_)]) | isLockLabel l -> v1 -- hmm
-      (VS (VV t pvs vs) s,v2) -> VS (VV t pvs [extR t (v1,v2)|v1<-vs]) s
---    (v1,v2) -> ok2 VExtR v1 v2 -- hmm
-      (v1,v2) -> error $ "not records" $$ show v1 $$ show v2
-  where
-    error explain = ppbug $ "The term" <+> t
-                            <+> "is not reducible" $$ explain
-
-glue env (v1,v2) = glu v1 v2
-  where
-    glu v1 v2 =
-        case (v1,v2) of
-          (VFV vs,v2) -> vfv [glu v1 v2|v1<-vs]
-          (v1,VFV vs) -> vfv [glu v1 v2|v2<-vs]
-          (VString s1,VString s2) -> VString (s1++s2)
-          (v1,VAlts d vs) -> VAlts (glx d) [(glx v,c) | (v,c) <- vs]
-             where glx v2 = glu v1 v2
-          (v1@(VAlts {}),v2) ->
-           --err (const (ok2 VGlue v1 v2)) id $
-             err bug id $
-             do y' <- strsFromValue v2
-                x' <- strsFromValue v1
-                return $ vfv [foldr1 VC (map VString (str2strings (glueStr v u))) | v <- x', u <- y']
-          (VC va vb,v2) -> VC va (glu vb v2)
-          (v1,VC va vb) -> VC (glu v1 va) vb
-          (VS (VV ty pvs vs) vb,v2) -> VS (VV ty pvs [glu v v2|v<-vs]) vb
-          (v1,VS (VV ty pvs vs) vb) -> VS (VV ty pvs [glu v1 v|v<-vs]) vb
-          (v1@(VApp NonExist _),_) -> v1
-          (_,v2@(VApp NonExist _)) -> v2
---        (v1,v2) -> ok2 VGlue v1 v2
-          (v1,v2) -> if flag optPlusAsBind (opts env)
-                       then VC v1 (VC (VApp BIND []) v2)
-                       else let loc  = gloc env
-                                vt v = case value2term loc (local env) v of
-                                         Left i  -> Error ('#':show i)
-                                         Right t -> t
-                                originalMsg = render $ ppL loc (hang "unsupported token gluing" 4
-                                                               (Glue (vt v1) (vt v2)))
-                                term = render $ pp  $ Glue (vt v1) (vt v2)
-                            in error $ unlines
-                                [originalMsg
-                                ,""
-                                ,"There was a problem in the expression `"++term++"`, either:"
-                                ,"1) You are trying to use + on runtime arguments, possibly via an oper."
-                                ,"2) One of the arguments in `"++term++"` is a bound variable from pattern matching a string, but the cases are non-exhaustive."
-                                ,"For more help see https://github.com/GrammaticalFramework/gf-core/tree/master/doc/errors/gluing.md"
-                                ]
-
-
--- | to get a string from a value that represents a sequence of terminals
-strsFromValue :: Value -> Err [Str]
-strsFromValue t = case t of
-  VString s   -> return [str s]
-  VC s t -> do
-    s' <- strsFromValue s
-    t' <- strsFromValue t
-    return [plusStr x y | x <- s', y <- t']
-{-
-  VGlue s t -> do
-    s' <- strsFromValue s
-    t' <- strsFromValue t
-    return [glueStr x y | x <- s', y <- t']
--}
-  VAlts d vs -> do
-    d0 <- strsFromValue d
-    v0 <- mapM (strsFromValue . fst) vs
-    c0 <- mapM (strsFromValue . snd) vs
-  --let vs' = zip v0 c0
-    return [strTok (str2strings def) vars | 
-              def  <- d0,
-              vars <- [[(str2strings v, map sstr c) | (v,c) <- zip vv c0] | 
-                                                          vv <- sequence v0]
-           ]
-  VFV ts -> concat # mapM strsFromValue ts
-  VStrs ts -> concat # mapM strsFromValue ts
-
-  _ -> fail ("cannot get Str from value " ++ show t)
-
-vfv vs = case nub vs of
-           [v] -> v
-           vs -> VFV vs
-
-select env vv =
-    case vv of
-      (v1,VFV vs) -> vfv [select env (v1,v2)|v2<-vs]
-      (VFV vs,v2) -> vfv [select env (v1,v2)|v1<-vs]
-      (v1@(VV pty vs rs),v2) ->
-         err (const (VS v1 v2)) id $
-         do --ats <- allParamValues (srcgr env) pty
-            --let vs = map (value0 env) ats
-            i <- maybeErr "no match" $ findIndex (==v2) vs
-            return (ix (gloc env) "select" rs i)
-      (VT _ _ [(PW,Bind b)],_) -> {-trace "eliminate wild card table" $-} b []
-      (v1@(VT _ _ cs),v2) ->
-                 err (\_->ok2 VS v1 v2) (err bug id . valueMatch env) $
-                 match (gloc env) cs v2
-      (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
-      (v1,v2) -> ok2 VS v1 v2
-
-match loc cs v = 
-  case value2term loc [] v of
-    Left i  -> bad ("variable #"++show i++" is out of scope")
-    Right t -> err bad return (matchPattern cs t)
-  where
-    bad = fail . ("In pattern matching: "++)
-
-valueMatch :: CompleteEnv -> (Bind Env,Substitution) -> Err Value
-valueMatch env (Bind f,env') = f # mapPairsM (value0 env) env'
-
-valueTable :: CompleteEnv -> TInfo -> [Case] -> Err OpenValue
-valueTable env i cs =
-    case i of
-      TComp ty -> do pvs <- paramValues env ty
-                     ((VV ty pvs .) # sequence) # mapM (value env.snd) cs
-      _ -> do ty <- getTableType i
-              cs' <- mapM valueCase cs
-              err (dynamic cs' ty) return (convert cs' ty)
-  where
-    dynamic cs' ty _ = cases cs' # value env ty
-
-    cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
-      where
-        keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
-                   VT wild (vty vs) (mapSnd ($vs) cs')
-
-    wild = case i of TWild _ -> True; _ -> False
-
-    convertv cs' vty = 
-      case value2term (gloc env) [] vty of
-        Left i    -> fail ("variable #"++show i++" is out of scope")
-        Right pty -> convert' cs' =<< paramValues'' env pty
-
-    convert cs' ty = convert' cs' =<< paramValues' env ty
-
-    convert' cs' ((pty,vs),pvs) =
-      do sts  <- mapM (matchPattern cs') vs
-         return $ \ vs -> VV pty pvs $ map (err bug id . valueMatch env)
-                                           (mapFst ($vs) sts)
-
-    valueCase (p,t) = do p' <- measurePatt # inlinePattMacro p
-                         pvs <- linPattVars p'
-                         vt <- value (extend pvs env) t
-                         return (p',\vs-> Bind $ \bs-> vt (push' p' bs pvs vs))
-
-    inlinePattMacro p =
-        case p of
-          PM qc -> do r <- resource env qc
-                      case r of
-                        VPatt p' -> inlinePattMacro p'
-                        _ -> ppbug $ hang "Expected pattern macro:" 4
-                                          (show r)
-          _ -> composPattOp inlinePattMacro p
-
-
-paramValues env ty = snd # paramValues' env ty
-
-paramValues' env ty = paramValues'' env =<< nfx (global env) ty
-
-paramValues'' env pty = do ats <- allParamValues (srcgr env) pty
-                           pvs <- mapM (eval (global env) []) ats
-                           return ((pty,ats),pvs)
-
-push' p bs xs = if length bs/=length xs
-                then bug $ "push "++show (p,bs,xs)
-                else push bs xs
-
-push :: Env -> LocalScope -> Stack -> Stack
-push bs [] vs = vs
-push bs (x:xs) vs = maybe err id (lookup x bs):push bs xs vs
-  where  err = bug $ "Unbound pattern variable "++showIdent x
-
-apply' :: CompleteEnv -> Term -> [OpenValue] -> Err OpenValue
-apply' env t [] = value env t
-apply' env t vs =
-  case t of
-    QC x                   -> return $ \ svs -> VCApp x (map ($svs) vs)
-{-
-    Q x@(m,f) | m==cPredef -> return $
-                              let constr = --trace ("predef "++show x) .
-                                           VApp x 
-                              in \ svs -> maybe constr id (Map.lookup f predefs)
-                                          $ map ($svs) vs
-              | otherwise  -> do r <- resource env x
-                                 return $ \ svs -> vapply (gloc env) r (map ($svs) vs)
--}
-    App t1 t2              -> apply' env t1 . (:vs) =<< value env t2
-    _                      -> do fv <- value env t
-                                 return $ \ svs -> vapply (gloc env) (fv svs) (map ($svs) vs)
-
-vapply :: GLocation -> Value -> [Value] -> Value
-vapply loc v [] = v
-vapply loc v vs =
-  case v of
-    VError {} -> v
---  VClosure env (Abs b x t) -> beta gr env b x t vs
-    VAbs bt _ (Bind f) -> vbeta loc bt f vs
-    VApp pre vs1 -> delta' pre (vs1++vs)
-      where
-        delta' Trace (v1:v2:vs) = let vr = vapply loc v2 vs
-                                  in vtrace loc v1 vr
-        delta' pre vs = err msg vfv $ mapM (delta pre) (varyList vs)
-        --msg = const (VApp pre (vs1++vs))
-        msg = bug . (("Applying Predef."++showIdent (predefName pre)++": ")++)
-    VS (VV t pvs fs) s -> VS (VV t pvs [vapply loc f vs|f<-fs]) s
-    VFV fs -> vfv [vapply loc f vs|f<-fs]
-    VCApp f vs0 -> VCApp f (vs0++vs)
-    VMeta i env vs0 -> VMeta i env (vs0++vs)
-    VGen i vs0 -> VGen i (vs0++vs)
-    v -> bug $ "vapply "++show v++" "++show vs
-
-vbeta loc bt f (v:vs) =
-  case (bt,v) of
-    (Implicit,VImplArg v) -> ap v
-    (Explicit,         v) -> ap v
-  where
-    ap (VFV avs) = vfv [vapply loc (f v) vs|v<-avs]
-    ap v         = vapply loc (f v) vs
-
-vary (VFV vs) = vs
-vary v = [v]
-varyList = mapM vary
-
-{-
-beta env b x t (v:vs) =
-  case (b,v) of
-    (Implicit,VImplArg v) -> apply' (ext (x,v) env) t vs
-    (Explicit,         v) -> apply' (ext (x,v) env) t vs
--}
-
-vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
-  where
-    pv v = case v of
-             VRec (f:as) -> hang (pf f) 4 (fsep (map pa as))
-             _ -> ppV v
-    pf (_,VString n) = pp n
-    pf (_,v) = ppV v
-    pa (_,v) = ppV v
-    ppV v = case value2term' True loc [] v of
-              Left i  -> "variable #" <> pp i <+> "is out of scope"
-              Right t -> ppTerm Unqualified 10 t
-
--- | Convert a value back to a term
-value2term :: GLocation -> [Ident] -> Value -> Either Int Term
-value2term = value2term' False
-value2term' stop loc xs v0 =
-  case v0 of
-    VApp pre vs    -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
-    VCApp f vs     -> liftM  (foldl App (QC f))   (mapM v2t vs)
-    VGen j vs      -> liftM2 (foldl App) (var j)  (mapM v2t vs)
-    VMeta j env vs -> liftM  (foldl App (Meta j)) (mapM v2t vs)
-    VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
-    VAbs  bt   x f -> liftM  (Abs  bt x)         (v2t' x f)
-    VInt n         -> return (EInt n)
-    VFloat f       -> return (EFloat f)
-    VString s      -> return (if null s then Empty else K s)
-    VSort s        -> return (Sort s)
-    VImplArg v     -> liftM  ImplArg (v2t v)
-    VTblType p res -> liftM2 Table (v2t p) (v2t res)
-    VRecType rs    -> liftM  RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
-    VRec as        -> liftM  R       (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
-    VV t _ vs      -> liftM  (V t)   (mapM v2t vs)
-    VT wild v cs   -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
-    VFV vs         -> liftM  FV (mapM v2t vs)
-    VC v1 v2       -> liftM2 C (v2t v1) (v2t v2)
-    VS v1 v2       -> liftM2 S (v2t v1) (v2t v2)
-    VP v l         -> v2t v >>= \t -> return (P t l)
-    VPatt p        -> return (EPatt p)
-    VPattType v    -> v2t v >>= return . EPattType
-    VAlts v vvs    -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
-    VStrs vs       -> liftM  Strs (mapM v2t vs)
---  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
---  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
-    VError err     -> return (Error err)
-    _              -> bug ("value2term "++show loc++" : "++show v0)
-  where
-    v2t = v2txs xs
-    v2txs = value2term' stop loc
-    v2t' x f = v2txs (x:xs) (bind f (gen xs))
-
-    var j
-      | j<length xs = Right (Vr (reverse xs !! j))
-      | otherwise   = Left  j
-
-
-    pushs xs e = foldr push e xs
-    push x (env,xs) = ((x,gen xs):env,x:xs)
-    gen xs = VGen (length xs) []
-
-    nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
-      where (env',xs') = pushs (pattVars p) ([],xs)
-
-    bind (Bind f) x = if stop
-                      then VSort (identS "...") -- hmm
-                      else f x
-
-
-linPattVars p =
-    if null dups
-    then return pvs
-    else fail.render $ hang "Pattern is not linear. All variable names on the left-hand side must be distinct." 4 (ppPatt Unqualified 0 p)
-  where
-    allpvs = allPattVars p
-    pvs = nub allpvs
-    dups = allpvs \\ pvs
-
-pattVars = nub . allPattVars
-allPattVars p =
-    case p of
-      PV i    -> [i]
-      PAs i p -> i:allPattVars p
-      _       -> collectPattOp allPattVars p
-
----
-ix loc fn xs i =
-    if i<n
-    then xs !! i
-    else bugloc loc $ "(!!): index too large in "++fn++", "++show i++"<"++show n
-  where n = length xs
-
-infixl 1 #,<# --,@@
-
-f # x = fmap f x
-mf <# mx  = ap mf mx
---m1 @@ m2 = (m1 =<<) . m2
-
-both f (x,y) = (,) # f x <# f y
-
-bugloc loc s = ppbug $ ppL loc s
-
-bug msg = ppbug msg
-ppbug doc = error $ render $ hang "Internal error in Compute.ConcreteNew:" 4 doc
diff --git a/src/compiler/GF/Compile/Compute/Predef.hs b/src/compiler/GF/Compile/Compute/Predef.hs
index 609a17798..58b9b3447 100644
--- a/src/compiler/GF/Compile/Compute/Predef.hs
+++ b/src/compiler/GF/Compile/Compute/Predef.hs
@@ -27,6 +27,10 @@ instance Predef Int where
 
 instance Predef Bool where
   toValue = boolV
+  fromValue v = case v of
+    VCApp (mn,i) [] | mn == cPredef && i == cPTrue -> return True
+    VCApp (mn,i) [] | mn == cPredef && i == cPFalse -> return False
+    _ -> verror "Bool" v
 
 instance Predef String where
   toValue = string
diff --git a/src/compiler/GF/Compile/Compute/Value.hs b/src/compiler/GF/Compile/Compute/Value.hs
index 7eb0c3bfb..c3fb83b4b 100644
--- a/src/compiler/GF/Compile/Compute/Value.hs
+++ b/src/compiler/GF/Compile/Compute/Value.hs
@@ -12,8 +12,8 @@ data Value
   | VGen Int [Value] -- for lambda bound variables, possibly applied
   | VMeta MetaId Env [Value]
 -- -- | VClosure Env Term -- used in Typecheck.ConcreteNew
-  | VAbs BindType Ident Binding -- used in Compute.ConcreteNew
-  | VProd BindType Value Ident Binding -- used in Compute.ConcreteNew
+  | VAbs BindType Ident Binding -- used in Compute.Concrete
+  | VProd BindType Value Ident Binding -- used in Compute.Concrete
   | VInt Int
   | VFloat Double
   | VString String
@@ -47,10 +47,10 @@ type Env = [(Ident,Value)]
 
 -- | Predefined functions
 data Predefined = Drop | Take | Tk | Dp | EqStr | Occur | Occurs | ToUpper
-                | ToLower | IsUpper | Length | Plus | EqInt | LessInt 
+                | ToLower | IsUpper | Length | Plus | EqInt | LessInt
              {- | Show | Read | ToStr | MapStr | EqVal -}
                 | Error | Trace
                 -- Canonical values below:
-                | PBool | PFalse | PTrue | Int | Float | Ints | NonExist 
+                | PBool | PFalse | PTrue | Int | Float | Ints | NonExist
                 | BIND | SOFT_BIND | SOFT_SPACE | CAPIT | ALL_CAPIT
                 deriving (Show,Eq,Ord,Ix,Bounded,Enum)
diff --git a/src/compiler/GF/Compile/ConcreteToHaskell.hs b/src/compiler/GF/Compile/ConcreteToHaskell.hs
index d74fcdacd..c9f0438e6 100644
--- a/src/compiler/GF/Compile/ConcreteToHaskell.hs
+++ b/src/compiler/GF/Compile/ConcreteToHaskell.hs
@@ -7,7 +7,7 @@ import GF.Text.Pretty
 --import GF.Grammar.Predef(cPredef,cInts)
 --import GF.Compile.Compute.Predef(predef)
 --import GF.Compile.Compute.Value(Predefined(..))
-import GF.Infra.Ident(Ident,identS,identW,prefixIdent)
+import GF.Infra.Ident(Ident,identC,identS,identW,prefixIdent,showRawIdent,rawIdentS)
 import GF.Infra.Option
 import GF.Haskell as H
 import GF.Grammar.Canonical as C
@@ -21,7 +21,7 @@ concretes2haskell opts absname gr =
      | let Grammar abstr cncs = grammar2canonical opts absname gr,
        cncmod<-cncs,
        let ModId name = concName cncmod
-           filename = name ++ ".hs" :: FilePath
+           filename = showRawIdent name ++ ".hs" :: FilePath
   ]
 
 -- | Generate Haskell code for the given concrete module.
@@ -53,7 +53,7 @@ concrete2haskell opts
     labels = S.difference (S.unions (map S.fromList recs)) common_labels
     common_records = S.fromList [[label_s]]
     common_labels = S.fromList [label_s]
-    label_s = LabelId "s"
+    label_s = LabelId (rawIdentS "s")
 
     signature (CatDef c _) = TypeSig lf (Fun abs (pure lin))
       where
@@ -69,7 +69,7 @@ concrete2haskell opts
       where
      --funcats = S.fromList [c | FunDef f (C.Type _ (TypeApp c _))<-funs]
        allcats = S.fromList [c | CatDef c _<-cats]
-      
+
     gId :: ToIdent i => i -> Ident
     gId = (if haskellOption opts HaskellNoPrefix then id else prefixIdent "G")
           . toIdent
@@ -116,7 +116,7 @@ concrete2haskell opts
               where (ls,ts) = unzip $ sortOn fst [(l,t)|RecordRow l t<-rs]
             StrType -> tcon0 (identS "Str")
             TableType pt lt -> Fun (ppT pt) (ppT lt)
---          TupleType lts -> 
+--          TupleType lts ->
 
     lincatDef (LincatDef c t) = tsyn0 (lincatName c) (convLinType t)
 
@@ -126,7 +126,7 @@ concrete2haskell opts
     linDefs = map eqn . sortOn fst . map linDef
       where eqn (cat,(f,(ps,rhs))) = (cat,Eqn (f,ps) rhs)
 
-    linDef (LinDef f xs rhs0) = 
+    linDef (LinDef f xs rhs0) =
         (cat,(linfunName cat,(lhs,rhs)))
       where
         lhs = [ConP (aId f) (map VarP abs_args)]
@@ -144,7 +144,7 @@ concrete2haskell opts
           where
             vs = [(VarValueId (Unqual x),a)|(VarId x,a)<-zip xs args]
             env= [(VarValueId (Unqual x),lc)|(VarId x,lc)<-zip xs (map arglincat absctx)]
-            
+
         letlin a (TypeBinding _ (C.Type _ (TypeApp acat _))) =
           (a,Ap (Var (linfunName acat)) (Var (abs_arg a)))
 
@@ -187,7 +187,7 @@ concrete2haskell opts
 
         pId p@(ParamId s) =
           if "to_R_" `isPrefixOf` unqual s then toIdent p else gId p -- !! a hack
-          
+
         table cs =
             if all (null.patVars) ps
             then lets ds (LambdaCase [(ppP p,t')|(p,t')<-zip ps ts'])
@@ -315,13 +315,13 @@ instance Records rhs => Records (TableRow rhs) where
 
 -- | Record subtyping is converted into explicit coercions in Haskell
 coerce env ty t =
-  case (ty,t) of 
+  case (ty,t) of
     (_,VariantValue ts) -> VariantValue (map (coerce env ty) ts)
     (TableType ti tv,TableValue _ cs) ->
       TableValue ti [TableRow p (coerce env tv t)|TableRow p t<-cs]
     (RecordType rt,RecordValue r) ->
       RecordValue [RecordRow l (coerce env ft f) |
-                     RecordRow l f<-r,ft<-[ft|RecordRow l' ft<-rt,l'==l]]
+                     RecordRow l f<-r,ft<-[ft | RecordRow l' ft <- rt, l'==l]]
     (RecordType rt,VarValue x)->
       case lookup x env of
         Just ty' | ty'/=ty -> -- better to compare to normal form of ty'
@@ -334,18 +334,17 @@ coerce env ty t =
     _ -> t
   where
     app f ts = ParamConstant (Param f ts) -- !! a hack
-    to_rcon = ParamId . Unqual . to_rcon' . labels
+    to_rcon = ParamId . Unqual . rawIdentS . to_rcon' . labels
 
 patVars p = []
 
-labels r = [l|RecordRow l _<-r]
+labels r = [l | RecordRow l _ <- r]
 
 proj = Var . identS . proj'
-proj' (LabelId l) = "proj_"++l
+proj' (LabelId l) = "proj_" ++ showRawIdent l
 rcon = Var . rcon'
 rcon' = identS . rcon_name
-rcon_name ls = "R"++concat (sort ['_':l|LabelId l<-ls])
-
+rcon_name ls = "R"++concat (sort ['_':showRawIdent l | LabelId l <- ls])
 to_rcon' = ("to_"++) . rcon_name
 
 recordType ls =
@@ -400,17 +399,17 @@ linfunName c = prefixIdent "lin" (toIdent c)
 
 class ToIdent i where toIdent :: i -> Ident
 
-instance ToIdent ParamId where toIdent (ParamId q) = qIdentS q
-instance ToIdent PredefId where toIdent (PredefId s) = identS s
-instance ToIdent CatId   where toIdent (CatId s) = identS s
-instance ToIdent C.FunId where toIdent (FunId s) = identS s
-instance ToIdent VarValueId where toIdent (VarValueId q) = qIdentS q
+instance ToIdent ParamId where toIdent (ParamId q) = qIdentC q
+instance ToIdent PredefId where toIdent (PredefId s) = identC s
+instance ToIdent CatId   where toIdent (CatId s) = identC s
+instance ToIdent C.FunId where toIdent (FunId s) = identC s
+instance ToIdent VarValueId where toIdent (VarValueId q) = qIdentC q
 
-qIdentS = identS . unqual
+qIdentC = identS . unqual
 
-unqual (Qual (ModId m) n) = m++"_"++n
-unqual (Unqual n) = n
+unqual (Qual (ModId m) n) = showRawIdent m++"_"++ showRawIdent n
+unqual (Unqual n) = showRawIdent n
 
 instance ToIdent VarId where
   toIdent Anonymous = identW
-  toIdent (VarId s) = identS s
+  toIdent (VarId s) = identC s
diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs
index ab6476b31..8383f0624 100644
--- a/src/compiler/GF/Compile/GeneratePMCFG.hs
+++ b/src/compiler/GF/Compile/GeneratePMCFG.hs
@@ -25,7 +25,7 @@ import GF.Data.BacktrackM
 import GF.Data.Operations
 import GF.Infra.UseIO (ePutStr,ePutStrLn) -- IOE,
 import GF.Data.Utilities (updateNthM) --updateNth
-import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(normalForm,resourceValues)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import qualified Data.List as List
@@ -82,7 +82,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
                           (goB b1 CNil [])
                           (pres,pargs)
       pmcfg      = getPMCFG pmcfgEnv1
-      
+
       stats      = let PMCFG prods funs = pmcfg
                        (s,e)            = bounds funs
                        !prods_cnt       = length prods
@@ -103,7 +103,7 @@ addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncFun mty@(Just (cat,cont
           newArgs  = map getFIds newArgs'
       in addFunction env0 newCat fun newArgs
 
-addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat)) 
+addPMCFG opts gr cenv opath am cm seqs id (GF.Grammar.CncCat mty@(Just (L _ lincat))
                                                              mdef@(Just (L loc1 def))
                                                              mref@(Just (L loc2 ref))
                                                              mprn
@@ -162,7 +162,7 @@ pgfCncCat :: SourceGrammar -> Type -> Int -> CncCat
 pgfCncCat gr lincat index =
   let ((_,size),schema) = computeCatRange gr lincat
   in PGF.CncCat index (index+size-1)
-                      (mkArray (map (renderStyle style{mode=OneLineMode} . ppPath) 
+                      (mkArray (map (renderStyle style{mode=OneLineMode} . ppPath)
                                     (getStrPaths schema)))
   where
     getStrPaths :: Schema Identity s c -> [Path]
@@ -243,7 +243,7 @@ choices nr path = do (args,_) <- get
                                                                                                                     | (value,index) <- values])
     descend schema       path              rpath = bug $ "descend "++show (schema,path,rpath)
 
-    updateEnv path value gr c (args,seq) = 
+    updateEnv path value gr c (args,seq) =
       case updateNthM (restrictProtoFCat path value) nr args of
         Just args -> c value (args,seq)
         Nothing   -> bug "conflict in updateEnv"
@@ -606,7 +606,7 @@ restrictProtoFCat path v (PFCat cat f schema) = do
                                                        Just index -> return (CPar (m,[(v,index)]))
                                                        Nothing    -> mzero
     addConstraint CNil             v (CStr _)      = bug "restrictProtoFCat: string path"
-    
+
     update k0 f [] = return []
     update k0 f (x@(k,Identity v):xs)
       | k0 == k    = do v <- f v
diff --git a/src/compiler/GF/Compile/GrammarToCanonical.hs b/src/compiler/GF/Compile/GrammarToCanonical.hs
index 33f35ad08..b0e356bc5 100644
--- a/src/compiler/GF/Compile/GrammarToCanonical.hs
+++ b/src/compiler/GF/Compile/GrammarToCanonical.hs
@@ -6,30 +6,35 @@ module GF.Compile.GrammarToCanonical(
        ) where
 import Data.List(nub,partition)
 import qualified Data.Map as M
+import Data.Maybe(fromMaybe)
 import qualified Data.Set as S
 import GF.Data.ErrM
 import GF.Text.Pretty
-import GF.Grammar.Grammar
+import GF.Grammar.Grammar as G
 import GF.Grammar.Lookup(lookupOrigInfo,allOrigInfos,allParamValues)
-import GF.Grammar.Macros(typeForm,collectOp,collectPattOp,mkAbs,mkApp,term2patt)
+import GF.Grammar.Macros(typeForm,collectOp,collectPattOp,composSafeOp,mkAbs,mkApp,term2patt,sortRec)
 import GF.Grammar.Lockfield(isLockLabel)
 import GF.Grammar.Predef(cPredef,cInts)
 import GF.Compile.Compute.Predef(predef)
 import GF.Compile.Compute.Value(Predefined(..))
-import GF.Infra.Ident(ModuleName(..),Ident,prefixIdent,showIdent,isWildIdent)
-import GF.Infra.Option(optionsPGF)
+import GF.Infra.Ident(ModuleName(..),Ident,ident2raw,rawIdentS,showIdent,isWildIdent)
+import GF.Infra.Option(Options,optionsPGF)
 import PGF.Internal(Literal(..))
-import GF.Compile.Compute.ConcreteNew(normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
 import GF.Grammar.Canonical as C
-import Debug.Trace
+import System.FilePath ((</>), (<.>))
+import qualified Debug.Trace as T
+
 
 -- | Generate Canonical code for the named abstract syntax and all associated
 -- concrete syntaxes
+grammar2canonical :: Options -> ModuleName -> G.Grammar -> C.Grammar
 grammar2canonical opts absname gr =
    Grammar (abstract2canonical absname gr)
            (map snd (concretes2canonical opts absname gr))
 
 -- | Generate Canonical code for the named abstract syntax
+abstract2canonical :: ModuleName -> G.Grammar -> Abstract
 abstract2canonical absname gr =
     Abstract (modId absname) (convFlags gr absname) cats funs
   where
@@ -44,6 +49,7 @@ abstract2canonical absname gr =
     convHypo (bt,name,t) =
       case typeForm t of
         ([],(_,cat),[]) -> gId cat -- !!
+        tf -> error $ "abstract2canonical convHypo: " ++ show tf
 
     convType t =
       case typeForm t of
@@ -54,25 +60,26 @@ abstract2canonical absname gr =
 
     convHypo' (bt,name,t) = TypeBinding (gId name) (convType t)
 
-
 -- | Generate Canonical code for the all concrete syntaxes associated with
 -- the named abstract syntax in given the grammar.
+concretes2canonical :: Options -> ModuleName -> G.Grammar -> [(FilePath, Concrete)]
 concretes2canonical opts absname gr =
   [(cncname,concrete2canonical gr cenv absname cnc cncmod)
      | let cenv = resourceValues opts gr,
        cnc<-allConcretes gr absname,
-       let cncname = "canonical/"++render cnc ++ ".gf" :: FilePath
+       let cncname = "canonical" </> render cnc <.> "gf"
            Ok cncmod = lookupModule gr cnc
   ]
 
 -- | Generate Canonical GF for the given concrete module.
+concrete2canonical :: G.Grammar -> GlobalEnv -> ModuleName -> ModuleName -> ModuleInfo -> Concrete
 concrete2canonical gr cenv absname cnc modinfo =
   Concrete (modId cnc) (modId absname) (convFlags gr cnc)
       (neededParamTypes S.empty (params defs))
-      [lincat|(_,Left lincat)<-defs]
-      [lin|(_,Right lin)<-defs]
+      [lincat | (_,Left lincat) <- defs]
+      [lin | (_,Right lin) <- defs]
   where
-    defs = concatMap (toCanonical gr absname cenv) . 
+    defs = concatMap (toCanonical gr absname cenv) .
            M.toList $
            jments modinfo
 
@@ -85,6 +92,7 @@ concrete2canonical gr cenv absname cnc modinfo =
         else let ((got,need),def) = paramType gr q
              in def++neededParamTypes (S.union got have) (S.toList need++qs)
 
+toCanonical :: G.Grammar -> ModuleName -> GlobalEnv -> (Ident, Info) -> [(S.Set QIdent, Either LincatDef LinDef)]
 toCanonical gr absname cenv (name,jment) =
   case jment of
     CncCat (Just (L loc typ)) _ _ pprn _ ->
@@ -97,7 +105,8 @@ toCanonical gr absname cenv (name,jment) =
       where
         tts = tableTypes gr [e']
 
-        e' = unAbs (length params) $
+        e' = cleanupRecordFields lincat $
+             unAbs (length params) $
              nf loc (mkAbs params (mkApp def (map Vr args)))
         params = [(b,x)|(b,x,_)<-ctx]
         args = map snd params
@@ -108,12 +117,12 @@ toCanonical gr absname cenv (name,jment) =
     _ -> []
   where
     nf loc = normalForm cenv (L loc name)
---  aId n = prefixIdent "A." (gId n)
 
     unAbs 0 t = t
     unAbs n (Abs _ _ t) = unAbs (n-1) t
     unAbs _ t = t
 
+tableTypes :: G.Grammar -> [Term] -> S.Set QIdent
 tableTypes gr ts = S.unions (map tabtys ts)
   where
     tabtys t =
@@ -122,6 +131,7 @@ tableTypes gr ts = S.unions (map tabtys ts)
         T (TTyped t) cs -> S.union (paramTypes gr t) (tableTypes gr (map snd cs))
         _ -> collectOp tabtys t
 
+paramTypes :: G.Grammar -> G.Type -> S.Set QIdent
 paramTypes gr t =
   case t of
     RecType fs -> S.unions (map (paramTypes gr.snd) fs)
@@ -140,11 +150,26 @@ paramTypes gr t =
                  Ok (_,ResParam {}) -> S.singleton q
                  _ -> ignore
 
-    ignore = trace ("Ignore: "++show t) S.empty
-
-
+    ignore = T.trace ("Ignore: " ++ show t) S.empty
+
+-- | Filter out record fields from definitions which don't appear in lincat.
+cleanupRecordFields :: G.Type -> Term -> Term
+cleanupRecordFields (RecType ls) (R as) =
+  let defnFields = M.fromList ls
+  in R
+      [ (lbl, (mty, t'))
+      | (lbl, (mty, t)) <- as
+      , M.member lbl defnFields
+      , let Just ty = M.lookup lbl defnFields
+      , let t' = cleanupRecordFields ty t
+      ]
+cleanupRecordFields ty t@(FV _) = composSafeOp (cleanupRecordFields ty) t
+cleanupRecordFields _ t = t
+
+convert :: G.Grammar -> Term -> LinValue
 convert gr = convert' gr []
 
+convert' :: G.Grammar -> [Ident] -> Term -> LinValue
 convert' gr vs = ppT
   where
     ppT0 = convert' gr vs
@@ -162,20 +187,20 @@ convert' gr vs = ppT
         S t p -> selection (ppT t) (ppT p)
         C t1 t2 -> concatValue (ppT t1) (ppT t2)
         App f a -> ap (ppT f) (ppT a)
-        R r -> RecordValue (fields r)
+        R r -> RecordValue (fields (sortRec r))
         P t l -> projection (ppT t) (lblId l)
         Vr x -> VarValue (gId x)
         Cn x -> VarValue (gId x) -- hmm
         Con c -> ParamConstant (Param (gId c) [])
         Sort k -> VarValue (gId k)
         EInt n -> LiteralValue (IntConstant n)
-        Q (m,n) -> if m==cPredef then ppPredef n else VarValue ((gQId m n))
-        QC (m,n) -> ParamConstant (Param ((gQId m n)) [])
+        Q (m,n) -> if m==cPredef then ppPredef n else VarValue (gQId m n)
+        QC (m,n) -> ParamConstant (Param (gQId m n) [])
         K s -> LiteralValue (StrConstant s)
         Empty -> LiteralValue (StrConstant "")
         FV ts -> VariantValue (map ppT ts)
         Alts t' vs -> alts vs (ppT t')
-        _ -> error $ "convert' "++show t
+        _ -> error $ "convert' ppT: " ++ show t
 
     ppCase (p,t) = TableRow (ppP p) (ppTv (patVars p++vs) t)
 
@@ -188,12 +213,12 @@ convert' gr vs = ppT
         Ok ALL_CAPIT  -> p "ALL_CAPIT"
         _ -> VarValue (gQId cPredef n) -- hmm
       where
-       p = PredefValue . PredefId
-      
+       p = PredefValue . PredefId . rawIdentS
+
     ppP p =
       case p of
         PC c ps -> ParamPattern (Param (gId c) (map ppP ps))
-        PP (m,c) ps -> ParamPattern (Param ((gQId m c)) (map ppP ps))
+        PP (m,c) ps -> ParamPattern (Param (gQId m c) (map ppP ps))
         PR r -> RecordPattern (fields r) {-
         PW -> WildPattern
         PV x -> VarP x
@@ -202,6 +227,7 @@ convert' gr vs = ppT
         PFloat x -> Lit (show x)
         PT _ p -> ppP p
         PAs x p -> AsP x (ppP p) -}
+        _ -> error $ "convert' ppP: " ++ show p
       where
         fields = map field . filter (not.isLockLabel.fst)
         field (l,p) = RecordRow (lblId l) (ppP p)
@@ -218,12 +244,12 @@ convert' gr vs = ppT
         pre Empty = [""]  -- Empty == K ""
         pre (Strs ts) = concatMap pre ts
         pre (EPatt p) = pat p
-        pre t = error $ "pre "++show t
+        pre t = error $ "convert' alts pre: " ++ show t
 
         pat (PString s) = [s]
         pat (PAlt p1 p2) = pat p1++pat p2
         pat (PSeq p1 p2) = [s1++s2 | s1<-pat p1, s2<-pat p2]
-        pat p = error $ "pat "++show p
+        pat p = error $ "convert' alts pat: "++show p
 
     fields = map field . filter (not.isLockLabel.fst)
     field (l,(_,t)) = RecordRow (lblId l) (ppT t)
@@ -236,6 +262,7 @@ convert' gr vs = ppT
                  ParamConstant (Param p (ps++[a]))
                _ -> error $ "convert' ap: "++render (ppA f <+> ppA a)
 
+concatValue :: LinValue -> LinValue -> LinValue
 concatValue v1 v2 =
   case (v1,v2) of
     (LiteralValue (StrConstant ""),_) -> v2
@@ -243,21 +270,24 @@ concatValue v1 v2 =
     _ -> ConcatValue v1 v2
 
 -- | Smart constructor for projections
-projection r l = maybe (Projection r l) id (proj r l)
+projection :: LinValue -> LabelId -> LinValue
+projection r l = fromMaybe (Projection r l) (proj r l)
 
+proj :: LinValue -> LabelId -> Maybe LinValue
 proj r l =
   case r of
-    RecordValue r -> case [v|RecordRow l' v<-r,l'==l] of
+    RecordValue r -> case [v | RecordRow l' v <- r, l'==l] of
                           [v] -> Just v
                           _ -> Nothing
     _ -> Nothing
 
 -- | Smart constructor for selections
+selection :: LinValue -> LinValue -> LinValue
 selection t v =
   -- Note: impossible cases can become possible after grammar transformation
   case t of
     TableValue tt r ->
-        case nub [rv|TableRow _ rv<-keep] of
+        case nub [rv | TableRow _ rv <- keep] of
           [rv] -> rv
           _ -> Selection (TableValue tt r') v
       where
@@ -276,13 +306,16 @@ selection t v =
         (keep,discard) = partition (mightMatchRow v) r
     _ -> Selection t v
 
+impossible :: LinValue -> LinValue
 impossible = CommentedValue "impossible"
 
+mightMatchRow :: LinValue -> TableRow rhs -> Bool
 mightMatchRow v (TableRow p _) =
   case p of
     WildPattern -> True
     _ -> mightMatch v p
 
+mightMatch :: LinValue -> LinPattern -> Bool
 mightMatch v p =
   case v of
     ConcatValue _ _ -> False
@@ -294,16 +327,18 @@ mightMatch v p =
     RecordValue rv ->
       case p of
         RecordPattern rp ->
-          and [maybe False (flip mightMatch p) (proj v l) | RecordRow l p<-rp]
+          and [maybe False (`mightMatch` p) (proj v l) | RecordRow l p<-rp]
         _ -> False
     _ -> True
 
+patVars :: Patt -> [Ident]
 patVars p =
   case p of
     PV x -> [x]
     PAs x p -> x:patVars p
     _ -> collectPattOp patVars p
 
+convType :: Term -> LinType
 convType = ppT
   where
     ppT t =
@@ -315,9 +350,9 @@ convType = ppT
         Sort k -> convSort k
 --      EInt n -> tcon0 (identS ("({-"++show n++"-})")) -- type level numeric literal
         FV (t:ts) -> ppT t -- !!
-        QC (m,n) -> ParamType (ParamTypeId ((gQId m n)))
-        Q (m,n) -> ParamType (ParamTypeId ((gQId m n)))
-        _ -> error $ "Missing case in convType for: "++show t
+        QC (m,n) -> ParamType (ParamTypeId (gQId m n))
+        Q (m,n) -> ParamType (ParamTypeId (gQId m n))
+        _ -> error $ "convType ppT: " ++ show t
 
     convFields = map convField . filter (not.isLockLabel.fst)
     convField (l,r) = RecordRow (lblId l) (ppT r)
@@ -326,15 +361,20 @@ convType = ppT
                    "Float" -> FloatType
                    "Int" -> IntType
                    "Str" -> StrType
-                   _ -> error ("convSort "++show k)
+                   _ -> error $ "convType convSort: " ++ show k
 
+toParamType :: Term -> ParamType
 toParamType t = case convType t of
                   ParamType pt -> pt
-                  _ -> error ("toParamType "++show t)
+                  _ -> error $ "toParamType: " ++ show t
 
+toParamId :: Term -> ParamId
 toParamId t = case toParamType t of
                    ParamTypeId p -> p
 
+paramType :: G.Grammar
+             -> (ModuleName, Ident)
+             -> ((S.Set (ModuleName, Ident), S.Set QIdent), [ParamDef])
 paramType gr q@(_,n) =
     case lookupOrigInfo gr q of
       Ok (m,ResParam (Just (L _ ps)) _)
@@ -342,7 +382,7 @@ paramType gr q@(_,n) =
          ((S.singleton (m,n),argTypes ps),
           [ParamDef name (map (param m) ps)]
          )
-       where name = (gQId m n)
+       where name = gQId m n
       Ok (m,ResOper  _ (Just (L _ t)))
         | m==cPredef && n==cInts ->
            ((S.empty,S.empty),[]) {-
@@ -350,36 +390,46 @@ paramType gr q@(_,n) =
             [Type (ConAp ((gQId m n)) [identS "n"]) (TId (identS "Int"))])-}
         | otherwise ->
            ((S.singleton (m,n),paramTypes gr t),
-            [ParamAliasDef ((gQId m n)) (convType t)])
+            [ParamAliasDef (gQId m n) (convType t)])
       _ -> ((S.empty,S.empty),[])
   where
-    param m (n,ctx) = Param ((gQId m n)) [toParamId t|(_,_,t)<-ctx]
+    param m (n,ctx) = Param (gQId m n) [toParamId t|(_,_,t)<-ctx]
     argTypes = S.unions . map argTypes1
     argTypes1 (n,ctx) = S.unions [paramTypes gr t|(_,_,t)<-ctx]
 
-lblId = LabelId . render -- hmm
-modId (MN m) = ModId (showIdent m)
+lblId :: Label -> C.LabelId
+lblId (LIdent ri) = LabelId ri
+lblId (LVar i) = LabelId (rawIdentS (show i)) -- hmm
+
+modId :: ModuleName -> C.ModId
+modId (MN m) = ModId (ident2raw m)
 
-class FromIdent i where gId :: Ident -> i
+class FromIdent i where
+  gId :: Ident -> i
 
 instance FromIdent VarId where
-  gId i = if isWildIdent i then Anonymous else VarId (showIdent i)
+  gId i = if isWildIdent i then Anonymous else VarId (ident2raw i)
 
-instance FromIdent C.FunId where gId = C.FunId . showIdent
-instance FromIdent CatId where gId = CatId . showIdent
+instance FromIdent C.FunId where gId = C.FunId . ident2raw
+instance FromIdent CatId where gId = CatId . ident2raw
 instance FromIdent ParamId where gId = ParamId . unqual
 instance FromIdent VarValueId where gId = VarValueId . unqual
 
-class FromIdent i => QualIdent i where gQId :: ModuleName -> Ident -> i
+class FromIdent i => QualIdent i where
+  gQId :: ModuleName -> Ident -> i
 
-instance QualIdent ParamId    where gQId m n = ParamId (qual m n)
+instance QualIdent ParamId where gQId m n = ParamId (qual m n)
 instance QualIdent VarValueId where gQId m n = VarValueId (qual m n)
 
-qual m n = Qual (modId m) (showIdent n)
-unqual n = Unqual (showIdent n)
+qual :: ModuleName -> Ident -> QualId
+qual m n = Qual (modId m) (ident2raw n)
+
+unqual :: Ident -> QualId
+unqual n = Unqual (ident2raw n)
 
+convFlags :: G.Grammar -> ModuleName -> Flags
 convFlags gr mn =
-  Flags [(n,convLit v) |
+  Flags [(rawIdentS n,convLit v) |
          (n,v)<-err (const []) (optionsPGF.mflags) (lookupModule gr mn)]
   where
     convLit l =
diff --git a/src/compiler/GF/Compile/Optimize.hs b/src/compiler/GF/Compile/Optimize.hs
index 393deb020..ac3fa357c 100644
--- a/src/compiler/GF/Compile/Optimize.hs
+++ b/src/compiler/GF/Compile/Optimize.hs
@@ -6,7 +6,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/09/16 13:56:13 $ 
+-- > CVS $Date: 2005/09/16 13:56:13 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.18 $
 --
@@ -21,7 +21,7 @@ import GF.Grammar.Printer
 import GF.Grammar.Macros
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
-import GF.Compile.Compute.ConcreteNew(GlobalEnv,normalForm,resourceValues)
+import GF.Compile.Compute.Concrete(GlobalEnv,normalForm,resourceValues)
 import GF.Data.Operations
 import GF.Infra.Option
 
@@ -90,7 +90,7 @@ evalInfo opts resenv sgr m c info = do
     let ppr' = fmap (evalPrintname resenv c) ppr
     return $ CncFun mt pde' ppr' mpmcfg -- only cat in type actually needed
 {-
-  ResOper pty pde 
+  ResOper pty pde
     | not new && OptExpand `Set.member` optim -> do
          pde' <- case pde of
                    Just (L loc de) -> do de <- computeConcrete gr de
@@ -171,13 +171,13 @@ mkLinDefault gr typ = liftM (Abs Explicit varStr) $ mkDefField typ
      _ -> Bad (render ("linearization type field cannot be" <+> typ))
 
 mkLinReference :: SourceGrammar -> Type -> Err Term
-mkLinReference gr typ = 
- liftM (Abs Explicit varStr) $ 
+mkLinReference gr typ =
+ liftM (Abs Explicit varStr) $
    case mkDefField typ (Vr varStr) of
      Bad "no string" -> return Empty
      x               -> x
  where
-   mkDefField ty trm = 
+   mkDefField ty trm =
      case ty of
        Table pty ty -> do ps <- allParamValues gr pty
                           case ps of
@@ -203,7 +203,7 @@ factor param c i t =
     T (TComp ty) cs -> factors ty [(p, factor param c (i+1) v) | (p, v) <- cs]
     _               -> composSafeOp (factor param c i) t
   where
-    factors ty pvs0  
+    factors ty pvs0
                  | not param = V ty (map snd pvs0)
     factors ty []            = V ty []
     factors ty pvs0@[(p,v)]  = V ty [v]
@@ -224,7 +224,7 @@ factor param c i t =
 replace :: Term -> Term -> Term -> Term
 replace old new trm =
   case trm of
-    -- these are the important cases, since they can correspond to patterns  
+    -- these are the important cases, since they can correspond to patterns
     QC _     | trm == old -> new
     App _ _  | trm == old -> new
     R _      | trm == old -> new
diff --git a/src/compiler/GF/Compile/PGFtoHaskell.hs b/src/compiler/GF/Compile/PGFtoHaskell.hs
index 6356c9f6d..bc8e59f57 100644
--- a/src/compiler/GF/Compile/PGFtoHaskell.hs
+++ b/src/compiler/GF/Compile/PGFtoHaskell.hs
@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/06/17 12:39:07 $ 
+-- > CVS $Date: 2005/06/17 12:39:07 $
 -- > CVS $Author: bringert $
 -- > CVS $Revision: 1.8 $
 --
@@ -22,7 +22,7 @@ import PGF.Internal
 import GF.Data.Operations
 import GF.Infra.Option
 
-import Data.List --(isPrefixOf, find, intersperse)
+import Data.List(isPrefixOf,find,intercalate,intersperse,groupBy,sortBy)
 import qualified Data.Map as Map
 
 type Prefix = String -> String
@@ -34,11 +34,12 @@ grammar2haskell :: Options
                 -> PGF
                 -> String
 grammar2haskell opts name gr = foldr (++++) [] $
-  pragmas ++ haskPreamble gadt name derivingClause extraImports ++
+  pragmas ++ haskPreamble gadt name derivingClause (extraImports ++ pgfImports) ++
   [types, gfinstances gId lexical gr'] ++ compos
     where gr' = hSkeleton gr
           gadt = haskellOption opts HaskellGADT
           dataExt = haskellOption opts HaskellData
+          pgf2 = haskellOption opts HaskellPGF2
           lexical cat = haskellOption opts HaskellLexical && isLexicalCat opts cat
           gId | haskellOption opts HaskellNoPrefix = rmForbiddenChars
               | otherwise = ("G"++) . rmForbiddenChars
@@ -50,21 +51,23 @@ grammar2haskell opts name gr = foldr (++++) [] $
           derivingClause
                  | dataExt = "deriving (Show,Data)"
                  | otherwise = "deriving Show"
-          extraImports | gadt = ["import Control.Monad.Identity",
-                                 "import Data.Monoid"]
+          extraImports | gadt = ["import Control.Monad.Identity", "import Data.Monoid"]
                        | dataExt = ["import Data.Data"]
                        | otherwise = []
+          pgfImports | pgf2 = ["import PGF2 hiding (Tree)", "", "showCId :: CId -> String", "showCId = id"]
+                     | otherwise = ["import PGF hiding (Tree)"]
           types | gadt = datatypesGADT gId lexical gr'
                 | otherwise = datatypes gId derivingClause lexical gr'
           compos | gadt = prCompos gId lexical gr' ++ composClass
                  | otherwise = []
 
-haskPreamble gadt name derivingClause extraImports =
+haskPreamble :: Bool -> String -> String -> [String] -> [String]
+haskPreamble gadt name derivingClause imports =
  [
   "module " ++ name ++ " where",
   ""
- ] ++ extraImports ++ [
-  "import PGF hiding (Tree)",
+ ] ++ imports ++ [
+  "",
   "----------------------------------------------------",
   "-- automatic translation from GF to Haskell",
   "----------------------------------------------------",
@@ -85,10 +88,11 @@ haskPreamble gadt name derivingClause extraImports =
   ""
  ]
 
+predefInst :: Bool -> String -> String -> String -> String -> String -> String
 predefInst gadt derivingClause gtyp typ destr consr =
   (if gadt
     then []
-    else ("newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ derivingClause ++ "\n\n")
+    else "newtype" +++ gtyp +++ "=" +++ gtyp +++ typ +++ derivingClause ++ "\n\n"
     )
   ++
   "instance Gf" +++ gtyp +++ "where" ++++
@@ -103,10 +107,10 @@ type OIdent = String
 type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
 
 datatypes :: Prefix -> DerivingClause -> (OIdent -> Bool) -> (String,HSkeleton) -> String
-datatypes gId derivingClause lexical = (foldr (+++++) "") . (filter (/="")) . (map (hDatatype gId derivingClause lexical)) . snd
+datatypes gId derivingClause lexical = foldr (+++++) "" . filter (/="") . map (hDatatype gId derivingClause lexical) . snd
 
 gfinstances :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
-gfinstances gId lexical (m,g) = (foldr (+++++) "") $ (filter (/="")) $ (map (gfInstance gId lexical m)) g
+gfinstances gId lexical (m,g) = foldr (+++++) "" $ filter (/="") $ map (gfInstance gId lexical m) g
 
 
 hDatatype  :: Prefix -> DerivingClause -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> String
@@ -131,16 +135,17 @@ nonLexicalRules True rules = [r | r@(f,t) <- rules, not (null t)]
 lexicalConstructor :: OIdent -> String
 lexicalConstructor cat = "Lex" ++ cat
 
+predefTypeSkel :: HSkeleton
 predefTypeSkel = [(c,[]) | c <- ["String", "Int", "Float"]]
 
 -- GADT version of data types
 datatypesGADT :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> String
-datatypesGADT gId lexical (_,skel) = unlines $ 
+datatypesGADT gId lexical (_,skel) = unlines $
     concatMap (hCatTypeGADT gId) (skel ++ predefTypeSkel) ++
-    [ 
-      "", 
+    [
+      "",
       "data Tree :: * -> * where"
-    ] ++ 
+    ] ++
     concatMap (map ("  "++) . hDatatypeGADT gId lexical) skel ++
     [
       "  GString :: String -> Tree GString_",
@@ -164,23 +169,23 @@ hCatTypeGADT gId (cat,rules)
        "data"+++gId cat++"_"]
 
 hDatatypeGADT :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> [String]
-hDatatypeGADT gId lexical (cat, rules) 
+hDatatypeGADT gId lexical (cat, rules)
     | isListCat (cat,rules) = [gId cat+++"::"+++"["++gId (elemCat cat)++"]" +++ "->" +++ t]
     | otherwise =
-        [ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t 
+        [ gId f +++ "::" +++ concatMap (\a -> gId a +++ "-> ") args ++ t
           | (f,args) <- nonLexicalRules (lexical cat) rules ]
         ++ if lexical cat then [lexicalConstructor cat +++ ":: String ->"+++ t] else []
   where t = "Tree" +++ gId cat ++ "_"
 
 hEqGADT :: Prefix -> (OIdent -> Bool) -> (OIdent, [(OIdent, [OIdent])]) -> [String]
 hEqGADT gId lexical (cat, rules)
-  | isListCat (cat,rules) = let r = listr cat in ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ listeqs] 
+  | isListCat (cat,rules) = let r = listr cat in ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ listeqs]
   | otherwise = ["(" ++ patt "x" r ++ "," ++ patt "y" r ++ ") -> " ++ eqs r | r <- nonLexicalRules (lexical cat) rules]
           ++ if lexical cat then ["(" ++ lexicalConstructor cat +++ "x" ++ "," ++ lexicalConstructor cat +++ "y" ++ ") -> x == y"] else []
 
  where
    patt s (f,xs) = unwords (gId f : mkSVars s (length xs))
-   eqs (_,xs) = unwords ("and" : "[" : intersperse "," [x ++ " == " ++ y | 
+   eqs (_,xs) = unwords ("and" : "[" : intersperse "," [x ++ " == " ++ y |
      (x,y) <- zip (mkSVars "x" (length xs)) (mkSVars "y" (length xs)) ] ++ ["]"])
    listr c = (c,["foo"]) -- foo just for length = 1
    listeqs = "and [x == y | (x,y) <- zip x1 y1]"
@@ -189,25 +194,26 @@ prCompos :: Prefix -> (OIdent -> Bool) -> (String,HSkeleton) -> [String]
 prCompos gId lexical (_,catrules) =
     ["instance Compos Tree where",
      "  compos r a f t = case t of"]
-    ++ 
+    ++
     ["    " ++ prComposCons (gId f) xs | (c,rs) <- catrules, not (isListCat (c,rs)),
-                                         (f,xs) <- rs, not (null xs)] 
-    ++ 
+                                         (f,xs) <- rs, not (null xs)]
+    ++
     ["    " ++ prComposCons (gId c) ["x1"] | (c,rs) <- catrules, isListCat (c,rs)]
-    ++ 
+    ++
     ["    _ -> r t"]
   where
-    prComposCons f xs = let vs = mkVars (length xs) in 
+    prComposCons f xs = let vs = mkVars (length xs) in
                         f +++ unwords vs +++ "->" +++ rhs f (zip vs xs)
     rhs f vcs = "r" +++ f +++ unwords (map (prRec f) vcs)
-    prRec f (v,c) 
+    prRec f (v,c)
       | isList f  = "`a` foldr (a . a (r (:)) . f) (r [])" +++ v
       | otherwise = "`a`" +++ "f" +++ v
-    isList f = (gId "List") `isPrefixOf` f
+    isList f = gId "List" `isPrefixOf` f
 
 gfInstance :: Prefix -> (OIdent -> Bool) -> String -> (OIdent, [(OIdent, [OIdent])]) -> String
 gfInstance gId lexical m crs = hInstance gId lexical m crs ++++ fInstance gId lexical m crs
 
+hInstance :: (String -> String) -> (String -> Bool) -> String -> (String, [(OIdent, [OIdent])]) -> String
 ----hInstance m ("Cn",_) = "" --- seems to belong to an old applic. AR 18/5/2004
 hInstance gId _ m (cat,[]) = unlines [
   "instance Show" +++ gId cat,
@@ -216,15 +222,15 @@ hInstance gId _ m (cat,[]) = unlines [
   "  gf _ = undefined",
   "  fg _ = undefined"
   ]
-hInstance gId lexical m (cat,rules) 
+hInstance gId lexical m (cat,rules)
  | isListCat (cat,rules) =
   "instance Gf" +++ gId cat +++ "where" ++++
-     "  gf (" ++ gId cat +++ "[" ++ concat (intersperse "," baseVars) ++ "])" 
+     "  gf (" ++ gId cat +++ "[" ++ intercalate "," baseVars ++ "])"
            +++ "=" +++ mkRHS ("Base"++ec) baseVars ++++
-     "  gf (" ++ gId cat +++ "(x:xs)) = " 
-           ++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")] 
+     "  gf (" ++ gId cat +++ "(x:xs)) = "
+           ++ mkRHS ("Cons"++ec) ["x",prParenth (gId cat+++"xs")]
 -- no show for GADTs
---     ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)" 
+--     ++++ " gf (" ++ gId cat +++ "xs) = error (\"Bad " ++ cat ++ " value: \" ++ show xs)"
  | otherwise =
   "instance Gf" +++ gId cat +++ "where\n" ++
   unlines ([mkInst f xx | (f,xx) <- nonLexicalRules (lexical cat) rules]
@@ -233,19 +239,22 @@ hInstance gId lexical m (cat,rules)
    ec = elemCat cat
    baseVars = mkVars (baseSize (cat,rules))
    mkInst f xx = let xx' = mkVars (length xx) in "  gf " ++
-     (if length xx == 0 then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
+     (if null xx then gId f else prParenth (gId f +++ foldr1 (+++) xx')) +++
      "=" +++ mkRHS f xx'
-   mkRHS f vars = "mkApp (mkCId \"" ++ f ++ "\")" +++ 
-		   "[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
+   mkRHS f vars = "mkApp (mkCId \"" ++ f ++ "\")" +++
+       "[" ++ prTList ", " ["gf" +++ x | x <- vars] ++ "]"
 
+mkVars :: Int -> [String]
 mkVars = mkSVars "x"
+
+mkSVars :: String -> Int -> [String]
 mkSVars s n = [s ++ show i | i <- [1..n]]
 
 ----fInstance m ("Cn",_) = "" ---
 fInstance _ _ m (cat,[]) = ""
 fInstance gId lexical m (cat,rules) =
   "  fg t =" ++++
-  (if isList 
+  (if isList
     then "    " ++ gId cat ++ " (fgs t) where\n     fgs t = case unApp t of"
     else "    case unApp t of") ++++
   unlines [mkInst f xx | (f,xx) <- nonLexicalRules (lexical cat) rules] ++++
@@ -257,27 +266,28 @@ fInstance gId lexical m (cat,rules) =
      "      Just (i," ++
      "[" ++ prTList "," xx' ++ "])" +++
      "| i == mkCId \"" ++ f ++ "\" ->" +++ mkRHS f xx'
-       where xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
-	     mkRHS f vars 
-		 | isList =
-		     if "Base" `isPrefixOf` f 
-                       then "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
-		       else "fg" +++ (vars !! 0) +++ ":" +++ "fgs" +++ (vars !! 1)
-		 | otherwise = 
-		     gId f +++  
-		     prTList " " [prParenth ("fg" +++ x) | x <- vars]
+       where
+         xx' = ["x" ++ show i | (_,i) <- zip xx [1..]]
+         mkRHS f vars
+           | isList =
+               if "Base" `isPrefixOf` f
+                             then "[" ++ prTList ", " [ "fg" +++ x | x <- vars ] ++ "]"
+                 else "fg" +++ (vars !! 0) +++ ":" +++ "fgs" +++ (vars !! 1)
+           | otherwise =
+               gId f +++
+               prTList " " [prParenth ("fg" +++ x) | x <- vars]
 
 --type HSkeleton = [(OIdent, [(OIdent, [OIdent])])]
 hSkeleton :: PGF -> (String,HSkeleton)
-hSkeleton gr = 
-  (showCId (absname gr), 
-   let fs = 
-         [(showCId c, [(showCId f, map showCId cs) | (f, (cs,_)) <- fs]) | 
+hSkeleton gr =
+  (showCId (absname gr),
+   let fs =
+         [(showCId c, [(showCId f, map showCId cs) | (f, (cs,_)) <- fs]) |
                                         fs@((_, (_,c)):_) <- fns]
-   in fs ++ [(sc, []) | c <- cts, let sc = showCId c, notElem sc (["Int", "Float", "String"] ++ map fst fs)]
+   in fs ++ [(sc, []) | c <- cts, let sc = showCId c, sc `notElem` (["Int", "Float", "String"] ++ map fst fs)]
   )
  where
-   cts = Map.keys (cats (abstract gr)) 
+   cts = Map.keys (cats (abstract gr))
    fns = groupBy valtypg (sortBy valtyps (map jty (Map.assocs (funs (abstract gr)))))
    valtyps (_, (_,x)) (_, (_,y)) = compare x y
    valtypg (_, (_,x)) (_, (_,y)) = x == y
@@ -291,9 +301,10 @@ updateSkeleton cat skel rule =
 -}
 isListCat :: (OIdent, [(OIdent, [OIdent])]) -> Bool
 isListCat (cat,rules) = "List" `isPrefixOf` cat && length rules == 2
-		    && ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
-    where c = elemCat cat
-	  fs = map fst rules
+        && ("Base"++c) `elem` fs && ("Cons"++c) `elem` fs
+    where
+      c = elemCat cat
+      fs = map fst rules
 
 -- | Gets the element category of a list category.
 elemCat :: OIdent -> OIdent
@@ -310,7 +321,7 @@ baseSize (_,rules) = length bs
     where Just (_,bs) = find (("Base" `isPrefixOf`) . fst) rules
 
 composClass :: [String]
-composClass = 
+composClass =
     [
      "",
      "class Compos t where",
@@ -337,4 +348,3 @@ composClass =
      "",
      "newtype C b a = C { unC :: b }"
     ]
-
diff --git a/src/compiler/GF/Compile/Rename.hs b/src/compiler/GF/Compile/Rename.hs
index aacf24c5b..41b2cdc67 100644
--- a/src/compiler/GF/Compile/Rename.hs
+++ b/src/compiler/GF/Compile/Rename.hs
@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/05/30 18:39:44 $ 
+-- > CVS $Date: 2005/05/30 18:39:44 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.19 $
 --
@@ -23,9 +23,9 @@
 -----------------------------------------------------------------------------
 
 module GF.Compile.Rename (
-	       renameSourceTerm,
-	       renameModule
-	      ) where
+     renameSourceTerm,
+     renameModule
+    ) where
 
 import GF.Infra.Ident
 import GF.Infra.CheckM
@@ -39,6 +39,7 @@ import GF.Data.Operations
 
 import Control.Monad
 import Data.List (nub,(\\))
+import qualified Data.List as L
 import qualified Data.Map as Map
 import Data.Maybe(mapMaybe)
 import GF.Text.Pretty
@@ -67,7 +68,7 @@ renameIdentTerm env = accumulateError (renameIdentTerm' env)
 
 -- Fails immediately on error, makes it possible to try other possibilities
 renameIdentTerm' :: Status -> Term -> Check Term
-renameIdentTerm' env@(act,imps) t0 = 
+renameIdentTerm' env@(act,imps) t0 =
   case t0 of
     Vr c -> ident predefAbs c
     Cn c -> ident (\_ s -> checkError s) c
@@ -84,8 +85,8 @@ renameIdentTerm' env@(act,imps) t0 =
     _ -> return t0
   where
     opens   = [st  | (OSimple _,st) <- imps]
-    qualifs = [(m, st) | (OQualif m _, st) <- imps] ++ 
-              [(m, st) | (OQualif _ m, st) <- imps] ++ 
+    qualifs = [(m, st) | (OQualif m _, st) <- imps] ++
+              [(m, st) | (OQualif _ m, st) <- imps] ++
               [(m, st) | (OSimple m, st) <- imps] -- qualif is always possible
 
     -- this facility is mainly for BWC with GF1: you need not import PredefAbs
@@ -93,7 +94,7 @@ renameIdentTerm' env@(act,imps) t0 =
       | isPredefCat c = return (Q (cPredefAbs,c))
       | otherwise     = checkError s
 
-    ident alt c = 
+    ident alt c =
       case Map.lookup c act of
         Just f -> return (f c)
         _      -> case mapMaybe (Map.lookup c) opens of
@@ -105,7 +106,26 @@ renameIdentTerm' env@(act,imps) t0 =
                               ts@(t:_) -> do checkWarn ("atomic term" <+> ppTerm Qualified 0 t0 $$
                                                         "conflict" <+> hsep (punctuate ',' (map (ppTerm Qualified 0) ts)) $$
                                                         "given" <+> fsep (punctuate ',' (map fst qualifs)))
-                                             return t
+                                             return (bestTerm ts) -- Heuristic for resource grammar. Returns t for all others.
+       where
+        -- Hotfix for https://github.com/GrammaticalFramework/gf-core/issues/56
+        -- Real bug is probably somewhere deeper in recognising excluded functions. /IL 2020-06-06
+        notFromCommonModule :: Term -> Bool
+        notFromCommonModule term =
+          let t = render $ ppTerm Qualified 0 term :: String
+           in not $ any (\moduleName -> moduleName `L.isPrefixOf` t)
+                        ["CommonX", "ConstructX", "ExtendFunctor"
+                        ,"MarkHTMLX", "ParamX", "TenseX", "TextX"]
+
+        -- If one of the terms comes from the common modules,
+        -- we choose the other one, because that's defined in the grammar.
+        bestTerm :: [Term] -> Term
+        bestTerm [] = error "constant not found" -- not reached: bestTerm is only called for case ts@(t:_)
+        bestTerm ts@(t:_) =
+          let notCommon = [t | t <- ts, notFromCommonModule t]
+           in case notCommon of
+                []    -> t -- All terms are from common modules, return first of original list
+                (u:_) -> u -- ≥1 terms are not from common modules, return first of those
 
 info2status :: Maybe ModuleName -> Ident -> Info -> StatusInfo
 info2status mq c i = case i of
@@ -137,7 +157,7 @@ modInfo2status (o,mo) = (o,tree2status o (jments mo))
 self2status :: ModuleName -> ModuleInfo -> StatusMap
 self2status c m = Map.mapWithKey (info2status (Just c)) (jments m)
 
-  
+
 renameInfo :: FilePath -> Status -> Module -> Ident -> Info -> Check Info
 renameInfo cwd status (m,mi) i info =
   case info of
@@ -188,7 +208,7 @@ renameTerm env vars = ren vars where
     Abs b x t    -> liftM  (Abs b x) (ren (x:vs) t)
     Prod bt x a b -> liftM2 (Prod bt x) (ren vs a) (ren (x:vs) b)
     Typed a b  -> liftM2 Typed (ren vs a) (ren vs b)
-    Vr x      
+    Vr x
       | elem x vs -> return trm
       | otherwise -> renid trm
     Cn _   -> renid trm
@@ -199,7 +219,7 @@ renameTerm env vars = ren vars where
       i' <- case i of
         TTyped ty -> liftM TTyped $ ren vs ty -- the only annotation in source
         _ -> return i
-      liftM (T i') $ mapM (renCase vs) cs  
+      liftM (T i') $ mapM (renCase vs) cs
 
     Let (x,(m,a)) b -> do
       m' <- case m of
@@ -209,7 +229,7 @@ renameTerm env vars = ren vars where
       b' <- ren (x:vs) b
       return $ Let (x,(m',a')) b'
 
-    P t@(Vr r) l                                               -- Here we have $r.l$ and this is ambiguous it could be either 
+    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 (MN r,label2ident l))      -- .. and qualified expression second.
@@ -311,7 +331,7 @@ renamePattern env patt =
 renameContext :: Status -> Context -> Check Context
 renameContext b = renc [] where
   renc vs cont = case cont of
-    (bt,x,t) : xts 
+    (bt,x,t) : xts
       | isWildIdent x -> do
           t'   <- ren vs t
           xts' <- renc vs xts
diff --git a/src/compiler/GF/Compile/TypeCheck/Abstract.hs b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
index 196e1a646..c76660259 100644
--- a/src/compiler/GF/Compile/TypeCheck/Abstract.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Abstract.hs
@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/09/15 16:22:02 $ 
+-- > CVS $Date: 2005/09/15 16:22:02 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.16 $
 --
@@ -13,11 +13,11 @@
 -----------------------------------------------------------------------------
 
 module GF.Compile.TypeCheck.Abstract (-- * top-level type checking functions; TC should not be called directly.
-		  checkContext,
-		  checkTyp,
-		  checkDef,
-		  checkConstrs,
-		 ) where
+    checkContext,
+    checkTyp,
+    checkDef,
+    checkConstrs,
+   ) where
 
 import GF.Data.Operations
 
@@ -33,8 +33,8 @@ import GF.Text.Pretty
 --import Control.Monad (foldM, liftM, liftM2)
 
 -- | invariant way of creating TCEnv from context
-initTCEnv gamma = 
-  (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma) 
+initTCEnv gamma =
+  (length gamma,[(x,VGen i x) | ((x,_),i) <- zip gamma [0..]], gamma)
 
 -- interface to TC type checker
 
diff --git a/src/compiler/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/GF/Compile/TypeCheck/Concrete.hs
index 2afff7c6a..e9420290a 100644
--- a/src/compiler/GF/Compile/TypeCheck/Concrete.hs
+++ b/src/compiler/GF/Compile/TypeCheck/Concrete.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE PatternGuards #-}
-module GF.Compile.TypeCheck.Concrete( {-checkLType, inferLType, computeLType, ppType-} ) where
-{-
+module GF.Compile.TypeCheck.Concrete( checkLType, inferLType, computeLType, ppType ) where
+import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
+
 import GF.Infra.CheckM
 import GF.Data.Operations
 
@@ -22,10 +23,16 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
     _ | 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
+    Q (m,ident) -> checkIn ("module" <+> m) $ do
       ty' <- lookupResDef gr (m,ident)
       if ty' == ty then return ty else comp g ty' --- is this necessary to test?
 
+    AdHocOverload ts -> do
+     over <- getOverload gr g (Just typeType) t
+     case over of
+       Just (tr,_) -> return tr
+       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t)
+
     Vr ident  -> checkLookup ident g -- never needed to compute!
 
     App f a -> do
@@ -62,7 +69,6 @@ computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
       lockRecType c t' ---- locking to be removed AR 20/6/2009
 
     _ | ty == typeTok -> return typeStr
-    _ | isPredefConstant ty -> return ty
 
     _ -> composOp (comp g) ty
 
@@ -73,26 +79,26 @@ inferLType gr g trm = case trm of
 
    Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
                                                 Just ty -> return ty
-                                                Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
+                                                Nothing -> checkError ("unknown in Predef:" <+> ident)
 
    Q ident -> checks [
      termWith trm $ lookupResType gr ident >>= computeLType gr g
      ,
      lookupResDef gr ident >>= inferLType gr g
      ,
-     checkError (text "cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
+     checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
      ]
 
    QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
                                                  Just ty -> return ty
-                                                 Nothing -> checkError (text "unknown in Predef:" <+> ppIdent ident)
+                                                 Nothing -> checkError ("unknown in Predef:" <+> ident)
 
    QC ident -> checks [
        termWith trm $ lookupResType gr ident >>= computeLType gr g
        ,
        lookupResDef gr ident >>= inferLType gr g
        ,
-       checkError (text "cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
+       checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
        ]
 
    Vr ident -> termWith trm $ checkLookup ident g
@@ -100,7 +106,12 @@ inferLType gr g trm = case trm of
    Typed e t -> do
      t' <- computeLType gr g t
      checkLType gr g e t'
-     return (e,t')
+
+   AdHocOverload ts -> do
+     over <- getOverload gr g Nothing trm
+     case over of
+       Just trty -> return trty
+       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
 
    App f a -> do
      over <- getOverload gr g Nothing trm
@@ -110,13 +121,17 @@ inferLType gr g trm = case trm of
          (f',fty) <- inferLType gr g f
          fty' <- computeLType gr g fty
          case fty' of
-           Prod bt z arg val -> do 
+           Prod bt z arg val -> do
              a' <- justCheck g a arg
-             ty <- if isWildIdent z 
+             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 fty)
+             return (App f' a',ty)
+           _ ->
+             let term = ppTerm Unqualified 0 f
+                 funName = pp . head . words .render $ term
+              in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$
+                             "\n   ** Maybe you gave too many arguments to" <+> funName <+> "\n")
 
    S f x -> do
      (f', fty) <- inferLType gr g f
@@ -124,7 +139,7 @@ inferLType gr g trm = case trm of
        Table arg val -> do
          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))
+       _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
 
    P t i -> do
      (t',ty) <- inferLType gr g t   --- ??
@@ -132,16 +147,16 @@ inferLType gr g trm = case trm of
      let tr2 = P t' i
      termWith tr2 $ case ty' of
        RecType ts -> case lookup i ts of
-                       Nothing -> checkError (text "unknown label" <+> ppLabel i <+> text "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
+                       Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
                        Just x  -> return x
-       _          -> checkError (text "record type expected for:" <+> ppTerm Unqualified 0 t $$
-                                 text " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
+       _          -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
+                                 " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
 
    R r -> do
      let (ls,fs) = unzip r
      fsts <- mapM inferM fs
      let ts = [ty | (Just ty,_) <- fsts]
-     checkCond (text "cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
+     checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
      return $ (R (zip ls fsts), RecType (zip ls ts))
 
    T (TTyped arg) pts -> do
@@ -152,10 +167,10 @@ inferLType gr g trm = case trm of
      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 
-       [] -> checkError (text "cannot infer table type of" <+> ppTerm Unqualified 0 trm)
-----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
-       _  -> do 
+     case pts' of
+       [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
+----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts']
+       _  -> do
          (arg,val) <- checks $ map (inferCase Nothing) pts'
          checkLType gr g trm (Table arg val)
    V arg pts -> do
@@ -166,9 +181,9 @@ inferLType gr g trm = case trm of
    K s  -> do
      if elem ' ' s
         then do
-          let ss = foldr C Empty (map K (words s))  
+          let ss = foldr C Empty (map K (words s))
           ----- removed irritating warning AR 24/5/2008
-          ----- checkWarn ("token \"" ++ s ++ 
+          ----- checkWarn ("token \"" ++ s ++
           -----              "\" converted to token list" ++ prt ss)
           return (ss, typeStr)
         else return (trm, typeStr)
@@ -179,50 +194,56 @@ inferLType gr g trm = case trm of
 
    Empty -> return (trm, typeStr)
 
-   C s1 s2 -> 
+   C s1 s2 ->
      check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
 
-   Glue s1 s2 -> 
+   Glue s1 s2 ->
      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))
+     checkWarn ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
      inferLType gr g (head ts)
 
    Strs ts -> do
-     ts' <- mapM (\t -> justCheck g t typeStr) ts 
+     ts' <- mapM (\t -> justCheck g t typeStr) ts
      return (Strs ts', typeStrs)
 
    Alts t aa -> do
      t'  <- justCheck g t typeStr
      aa' <- flip mapM aa (\ (c,v) -> do
-        c' <- justCheck g c 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 g) typeType) ts 
+     ts' <- mapM (flip (justCheck g) typeType) ts
      return (RecType (zip ls ts'), typeType)
 
    ExtR r s -> do
-     (r',rT) <- inferLType gr g r 
+
+---     over <- getOverload gr g Nothing r
+---     let r1 = maybe r fst over
+     let r1 = r ---
+
+     (r',rT) <- inferLType gr g r1
      rT'     <- computeLType gr g rT
+
      (s',sT) <- inferLType gr g s
      sT'     <- computeLType gr g sT
 
      let trm' = ExtR r' s'
-     ---- trm'    <- plusRecord r' s'
      case (rT', sT') of
        (RecType rs, RecType ss) -> do
-         rt <- plusRecType rT' sT'
+         let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields
          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)
+       _ | rT' == typeType && sT' == typeType -> do
+         return (trm', typeType)
+       _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
 
-   Sort _     -> 
+   Sort _     ->
      termWith trm $ return typeType
 
    Prod bt x a b -> do
@@ -231,7 +252,7 @@ inferLType gr g trm = case trm of
      return (Prod bt x a' b', typeType)
 
    Table p t  -> do
-     p' <- justCheck g p typeType --- check p partype! 
+     p' <- justCheck g p typeType --- check p partype!
      t' <- justCheck g t typeType
      return $ (Table p' t', typeType)
 
@@ -250,9 +271,9 @@ inferLType gr g trm = case trm of
    ELin c trm -> do
      (trm',ty) <- inferLType gr g trm
      ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
-     return $ (ELin c trm', ty') 
+     return $ (ELin c trm', ty')
 
-   _ -> checkError (text "cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
+   _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
 
  where
    isPredef m = elem m [cPredef,cPredefAbs]
@@ -299,7 +320,6 @@ inferLType gr g trm = case trm of
      PChars _ -> return $ typeStr
      _ -> inferLType gr g (patt2term p) >>= return . snd
 
-
 -- type inference: Nothing, type checking: Just t
 -- the latter permits matching with value type
 getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
@@ -310,15 +330,28 @@ getOverload gr g mt ot = case appForm ot of
          v <- matchOverload f typs ttys
          return $ Just v
        _ -> return Nothing
+     (AdHocOverload cs@(f:_), ts) -> do     --- the function name f is only used in error messages
+       let typs = concatMap collectOverloads cs
+       ttys <- mapM (inferLType gr g) ts
+       v <- matchOverload f typs ttys
+       return $ Just v
      _ -> return Nothing
+
  where
+   collectOverloads tr@(Q c) = case lookupOverload gr c of
+     Ok typs -> typs
+     _ -> case lookupResType gr c of
+       Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
+       _ -> []
+   collectOverloads _ = [] --- constructors QC
+
    matchOverload f typs ttys = do
      let (tts,tys) = unzip ttys
      let vfs = lookupOverloadInstance tys typs
      let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
      let showTypes ty = hsep (map ppType ty)
 
-    
+
      let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])
 
      -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
@@ -329,50 +362,57 @@ getOverload gr g mt ot = case appForm ot of
      case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
        ([(_,val,fun)],_) -> return (mkApp fun tts, val)
        ([],[(pre,val,fun)]) -> do
-         checkWarn $  text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
-                      text "for" $$
+         checkWarn $  "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
+                      "for" $$
                       nest 2 (showTypes tys) $$
-                      text "using" $$
+                      "using" $$
                       nest 2 (showTypes pre)
          return (mkApp fun tts, val)
        ([],[]) -> do
-         checkError $ text "no overload instance of" <+> ppTerm Unqualified 0 f $$
-                      text "for" $$
+         checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
+                      maybe empty (\x -> "with value type" <+> ppType x) mt $$
+                      "for argument list" $$
                       nest 2 stysError $$
-                      text "among" $$
-                      nest 2 (vcat stypsError) $$
-                      maybe empty (\x -> text "with value type" <+> ppType x) mt
+                      "among alternatives" $$
+                      nest 2 (vcat stypsError)
+
 
        (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
          ([(val,fun)],_) -> do
            return (mkApp fun tts, val)
          ([],[(val,fun)]) -> do
-           checkWarn (text "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
+           checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot)
            return (mkApp fun tts, val)
 
 ----- unsafely exclude irritating warning AR 24/5/2008
------           checkWarn $ "overloading of" +++ prt f +++ 
+-----           checkWarn $ "overloading of" +++ prt f +++
 -----             "resolved by excluding partial applications:" ++++
 -----             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
 
-
-         _ -> checkError $ text "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
-                           text "for" <+> hsep (map ppType tys) $$ 
-                           text "with alternatives" $$
-                           nest 2 (vcat [ppType ty | (_,ty,_) <- if null vfs1 then vfs2 else vfs2])
+--- now forgiving ambiguity with a warning AR 1/2/2014
+--  This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before.
+--  But it also gives a chance to ambiguous overloadings that were banned before.
+         (nps1,nps2) -> do
+              checkWarn $  "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
+                  ----     "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$
+                           "resolved by selecting the first of the alternatives" $$
+                           nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
+              case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
+                 [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
+                 h:_ -> return h
 
    matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
 
    unlocked v = case v of
-     RecType fs -> RecType $ filter (not . isLockLabel . fst) fs
+     RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
      _ -> v
    ---- TODO: accept subtypes
    ---- TODO: use a trie
-   lookupOverloadInstance tys typs = 
-     [((pre,mkFunType rest val, t),isExact) | 
+   lookupOverloadInstance tys typs =
+     [((pre,mkFunType rest val, t),isExact) |
        let lt = length tys,
        (ty,(val,t)) <- typs, length ty >= lt,
-       let (pre,rest) = splitAt lt ty, 
+       let (pre,rest) = splitAt lt ty,
        let isExact = pre == tys,
        isExact || map unlocked pre == map unlocked tys
      ]
@@ -385,20 +425,21 @@ getOverload gr g mt ot = case appForm ot of
 
 checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
 checkLType gr g trm typ0 = do
-
   typ <- computeLType gr g typ0
 
   case trm of
 
     Abs bt x c -> do
       case typ of
-        Prod bt' z a b -> do 
+        Prod bt' z a b -> do
           (c',b') <- if isWildIdent z
                        then checkLType gr ((bt,x,a):g) c b
-                       else do b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
+                       else do b' <- checkIn (pp "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 typ
+          return $ (Abs bt x c', Prod bt' z a b')
+        _ -> checkError $ "function type expected instead of" <+> ppType typ $$
+                          "\n   ** Double-check that the type signature of the operation" $$
+                          "matches the number of arguments given to it.\n"
 
     App f a -> do
        over <- getOverload gr g (Just typ) trm
@@ -408,6 +449,12 @@ checkLType gr g trm typ0 = do
           (trm',ty') <- inferLType gr g trm
           termWith trm' $ checkEqLType gr g typ ty' trm'
 
+    AdHocOverload ts -> do
+      over <- getOverload gr g Nothing trm
+      case over of
+        Just trty -> return trty
+        _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm)
+
     Q _ -> do
        over <- getOverload gr g (Just typ) trm
        case over of
@@ -417,21 +464,21 @@ checkLType gr g trm typ0 = do
           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 
+      checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
+    T _ cs -> case typ of
+      Table arg val -> do
         case allParamValues gr arg of
           Ok vs -> do
             let ps0 = map fst cs
             ps <- testOvershadow ps0 vs
-            if null ps 
-              then return () 
-              else checkWarn (text "patterns never reached:" $$
+            if null ps
+              then return ()
+              else checkWarn ("patterns never reached:" $$
                               nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
           _ -> 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 typ)
+      _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
     V arg0 vs ->
       case typ of
         Table arg1 val ->
@@ -439,51 +486,54 @@ checkLType gr g trm typ0 = do
               vs1 <- allParamValues gr arg1
               if length vs1 == length vs
                  then return ()
-                 else checkError $ text "wrong number of values in table" <+> ppTerm Unqualified 0 trm
+                 else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
               vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
               return (V arg' vs',typ)
 
     R r -> case typ of --- why needed? because inference may be too difficult
        RecType rr -> do
-         let (ls,_) = unzip rr        -- labels of expected type
+       --let (ls,_) = unzip rr        -- labels of expected type
          fsts <- mapM (checkM r) rr   -- check that they are found in the record
          return $ (R fsts, typ)       -- normalize record
 
-       _ -> checkError (text "record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
+       _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
 
     ExtR r s -> case typ of
        _ | typ == typeType -> do
          trm' <- computeLType gr g trm
          case trm' of
-           RecType _ -> termWith trm $ return typeType
-           ExtR (Vr _) (RecType _) -> termWith trm $ return typeType 
+           RecType _ -> termWith trm' $ return typeType
+           ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType
                                       -- ext t = t ** ...
-           _ -> checkError (text "invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
+           _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
 
        RecType rr -> do
-         (r',ty,s') <- checks [
-            do (r',ty) <- inferLType gr g r
-               return (r',ty,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 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)
+
+         ll2 <- case s of
+           R ss -> return $ map fst ss
+           _ -> do
+             (s',typ2) <- inferLType gr g s
+             case typ2 of
+               RecType ss -> return $ map fst ss
+               _ ->  checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
+         let ll1 = [l | (l,_) <- rr, notElem l ll2]
+
+---         over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
+---         let r1 = maybe r fst over
+         let r1 = r ---
+
+         (r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
+         (s',_) <- checkLType gr g s  (RecType [field | field@(l,_) <- rr, elem l ll2])
+
+         let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
+         return (rec, typ)
 
        ExtR ty ex -> do
          r' <- justCheck g r ty
          s' <- justCheck g s ex
          return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
 
-       _ -> checkError (text "record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
+       _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
 
     FV vs -> do
       ttys <- mapM (flip (checkLType gr g) typ) vs
@@ -498,7 +548,7 @@ checkLType gr g trm typ0 = do
           (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 ty')
+        _ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
      , do
       (arg',ty) <- inferLType gr g arg
       ty'       <- computeLType gr g ty
@@ -507,7 +557,8 @@ checkLType gr g trm typ0 = do
       ]
     Let (x,(mty,def)) body -> case mty of
       Just ty -> do
-        (def',ty') <- checkLType gr g def ty
+        (ty0,_)    <- checkLType gr g ty typeType
+        (def',ty') <- checkLType gr g def ty0
         body' <- justCheck ((Explicit,x,ty'):g) body typ
         return (Let (x,(Just ty',def')) body', typ)
       _ -> do
@@ -523,10 +574,10 @@ checkLType gr g trm typ0 = do
       termWith trm' $ checkEqLType gr g typ ty' trm'
  where
    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 
-
+{-
+   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
        checkEqLType gr g ty ty0 t
@@ -535,12 +586,12 @@ checkLType gr g trm typ0 = do
      Just (_,t) -> do
        (t',ty') <- checkLType gr g t ty
        return (l,(Just ty',t'))
-     _ -> checkError $ 
-            if isLockLabel l 
+     _ -> checkError $
+            if isLockLabel l
               then let cat = drop 5 (showIdent (label2ident l))
-                   in ppTerm Unqualified 0 (R rms) <+> text "is not in the lincat of" <+> text cat <> 
-                      text "; try wrapping it with lin" <+> text cat
-              else text "cannot find value for label" <+> ppLabel l <+> text "in" <+> ppTerm Unqualified 0 (R rms)
+                   in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <>
+                      "; try wrapping it with lin" <+> cat
+              else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
 
    checkCase arg val (p,t) = do
      cont <- pattContext gr g arg p
@@ -553,7 +604,7 @@ pattContext env g typ p = case p of
   PP (q,c) ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
     t <- lookupResType env (q,c)
     let (cont,v) = typeFormCnc t
-    checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
+    checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p)
               (length cont == length ps)
     checkEqLType env g typ v (patt2term p)
     mapM (\((_,_,ty),p) -> pattContext env g ty p) (zip cont ps) >>= return . concat
@@ -564,7 +615,7 @@ pattContext env g typ p = case p of
         let pts = [(ty,tr) | (l,tr) <- r, Just ty <- [lookup l t]]
         ----- checkWarn $ prt p ++++ show pts ----- debug
         mapM (uncurry (pattContext env g)) pts >>= return . concat
-      _ -> checkError (text "record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
+      _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
   PT t p' -> do
     checkEqLType env g typ t (patt2term p')
     pattContext env g typ p'
@@ -577,10 +628,10 @@ pattContext env g typ p = case p of
     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" <+>
-       fsep (map ppIdent pts) <+> 
-       text "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
+    checkCond
+      ("incompatible bindings of" <+>
+       fsep pts <+>
+       "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts)
     return g1 -- must be g1 == g2
   PSeq p q -> do
     g1 <- pattContext env g typ p
@@ -590,11 +641,11 @@ pattContext env g typ p = case p of
   PNeg p' -> noBind typ p'
 
   _ -> return [] ---- check types!
- where 
+ where
    noBind typ p' = do
     co <- pattContext env g typ p'
     if not (null co)
-      then checkWarn (text "no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
+      then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p)
            >> return []
       else return []
 
@@ -603,9 +654,31 @@ 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 t $$
-                          text "inferred:" <+> ppType u
+    False ->
+      let inferredType = ppTerm Qualified 0 u
+          expectedType = ppTerm Qualified 0 t
+          term = ppTerm Unqualified 0 trm
+          funName = pp . head . words .render $ term
+          helpfulMsg =
+            case (arrows inferredType, arrows expectedType) of
+              (0,0) -> pp "" -- None of the types is a function
+              _ -> "\n   **" <+>
+                  if expectedType `isLessApplied` inferredType
+                    then "Maybe you gave too few arguments to" <+> funName
+                    else pp "Double-check that type signature and number of arguments match."
+      in checkError $ s <+> "type of" <+> term $$
+                            "expected:" <+> expectedType $$ -- ppqType t u $$
+                            "inferred:" <+> inferredType $$ -- ppqType u t
+                            helpfulMsg
+  where
+    -- count the number of arrows in the prettyprinted term
+    arrows :: Doc -> Int
+    arrows = length . filter (=="->") . words . render
+
+    -- If prettyprinted type t has fewer arrows then prettyprinted type u,
+    -- then t is "less applied", and we can print out more helpful error msg.
+    isLessApplied :: Doc -> Doc -> Bool
+    isLessApplied t u = arrows t < arrows u
 
 checkIfEqLType :: SourceGrammar -> Context -> Type -> Type -> Term -> Check (Bool,Type,Type,String)
 checkIfEqLType gr g t u trm = do
@@ -617,60 +690,62 @@ checkIfEqLType gr g t u trm = do
     --- better: use a flag to forgive? (AR 31/1/2006)
     _ -> case missingLock [] t' u' of
       Ok lo -> do
-        checkWarn $ text "missing lock field" <+> fsep (map ppLabel lo)
+        checkWarn $ "missing lock field" <+> fsep lo
         return (True,t',u',[])
       Bad s -> return (False,t',u',s)
 
   where
 
-   -- t is a subtype of u 
+   -- check that u is a subtype of t
    --- quick hack version of TC.eqVal
-   alpha g t u = case (t,u) of  
+   alpha g t u = case (t,u) of
 
      -- error (the empty type!) is subtype of any other type
      (_,u) | u == typeError -> True
 
      -- contravariance
-     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d 
-                              
+     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d
+
      -- record subtyping
-     (RecType rs, RecType ts) -> all (\ (l,a) -> 
-                                   any (\ (k,b) -> alpha g a b && l == k) ts) rs
+     (RecType rs, RecType ts) -> all (\ (l,a) ->
+                                   any (\ (k,b) -> l == k && alpha g a b) ts) rs
      (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
      (ExtR r s, t) -> alpha g r t || alpha g s t
 
      -- the following say that Ints n is a subset of Int and of Ints m >= n
-     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts t -> m >= n
+     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
+     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
            | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
            | 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 gr n) 
+     (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 gr n) 
+     (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) 
+     (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) 
+     (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
+     -- contravariance
+     (Table a b,  Table c d)  -> alpha g c a && alpha g b d
      (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
-     _                        -> t == u 
+     _                        -> t == u
      --- the following should be one-way coercions only. AR 4/1/2001
                                   || elem t sTypes && elem u sTypes
-                                  || (t == typeType && u == typePType) 
-                                  || (u == typeType && t == typePType) 
+                                  || (t == typeType && u == typePType)
+                                  || (u == typeType && t == typePType)
 
-   missingLock g t u = case (t,u) of  
-     (RecType rs, RecType ts) -> 
-       let 
-         ls = [l | (l,a) <- rs, 
+   missingLock g t u = case (t,u) of
+     (RecType rs, RecType ts) ->
+       let
+         ls = [l | (l,a) <- rs,
                    not (any (\ (k,b) -> alpha g a b && l == k) ts)]
          (locks,others) = partition isLockLabel ls
        in case others of
-         _:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
+         _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
          _ -> return locks
      -- contravariance
      (Prod _ x a b, Prod _ y c d) -> do
@@ -696,7 +771,7 @@ termWith t ct = do
   return (t,ty)
 
 -- | compositional check\/infer of binary operations
-check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> 
+check2 :: (Term -> Check Term) -> (Term -> Term -> Term) ->
           Term -> Term -> Type -> Check (Term,Type)
 check2 chk con a b t = do
   a' <- chk a
@@ -708,14 +783,18 @@ ppType :: Type -> Doc
 ppType ty =
   case ty of
     RecType fs   -> case filter isLockLabel $ map fst fs of
-                      [lock] -> text (drop 5 (showIdent (label2ident lock)))
+                      [lock] -> pp (drop 5 (showIdent (label2ident lock)))
                       _      -> ppTerm Unqualified 0 ty
-    Prod _ x a b -> ppType a <+> text "->" <+> ppType b
+    Prod _ x a b -> ppType a <+> "->" <+> ppType b
     _            -> ppTerm Unqualified 0 ty
-
+{-
+ppqType :: Type -> Type -> Doc
+ppqType t u = case (ppType t, ppType u) of
+  (pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
+  (pt,_) -> pt
+-}
 checkLookup :: Ident -> Context -> Check Type
 checkLookup x g =
   case [ty | (b,y,ty) <- g, x == y] of
-    []     -> checkError (text "unknown variable" <+> ppIdent x)
+    []     -> checkError ("unknown variable" <+> x)
     (ty:_) -> return ty
--}
diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
index b35aaf9ed..ed3a20ce0 100644
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -10,7 +10,7 @@ import GF.Grammar hiding (Env, VGen, VApp, VRecType)
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
 import GF.Grammar.Lockfield
-import GF.Compile.Compute.ConcreteNew
+import GF.Compile.Compute.Concrete
 import GF.Compile.Compute.Predef(predef,predefName)
 import GF.Infra.CheckM
 import GF.Data.Operations
@@ -133,7 +133,7 @@ tcRho ge scope t@(RecType rs) (Just ty) = do
                          [] -> unifyVar ge scope i env vs vtypePType
                          _  -> return ()
     ty              -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
-                          tcError ("The record type" <+> ppTerm Unqualified 0 t $$ 
+                          tcError ("The record type" <+> ppTerm Unqualified 0 t $$
                                    "cannot be of type" <+> ppTerm Unqualified 0 ty)
   (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
   return (f (RecType rs),ty)
@@ -187,7 +187,7 @@ tcRho ge scope (R rs) (Just ty) = do
   case ty' of
     (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
                           rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
-                          return ((f . R)  rs, 
+                          return ((f . R)  rs,
                                   VRecType [(l, ty) | (l,t,ty) <- lttys]
                                  )
     ty              -> do lttys <- inferRecFields ge scope rs
@@ -277,11 +277,11 @@ tcApp ge scope (App fun arg) =                                  -- APP2
         varg <- liftErr (eval ge (scopeEnv scope) arg)
         return (App fun arg, res_ty varg)
 tcApp ge scope (Q id) =                                          -- VAR (global)
-  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> 
+  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
      do ty <- liftErr (eval ge [] ty)
         return (t,ty)
 tcApp ge scope (QC id) =                                         -- VAR (global)
-  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) -> 
+  mkTcA (lookupOverloadTypes (geGrammar ge) id) `bindTcA` \(t,ty) ->
      do ty <- liftErr (eval ge [] ty)
         return (t,ty)
 tcApp ge scope t =
@@ -350,7 +350,7 @@ tcPatt ge scope (PM q) ty0 = do
     Bad err -> tcError (pp err)
 tcPatt ge scope p ty = unimplemented ("tcPatt "++show p)
 
-inferRecFields ge scope rs = 
+inferRecFields ge scope rs =
   mapM (\(l,r) -> tcRecField ge scope l r Nothing) rs
 
 checkRecFields ge scope []          ltys
@@ -368,7 +368,7 @@ checkRecFields ge scope ((l,t):lts) ltys =
   where
     takeIt l1 []  = (Nothing, [])
     takeIt l1 (lty@(l2,ty):ltys)
-      | l1 == l2  = (Just ty,ltys) 
+      | l1 == l2  = (Just ty,ltys)
       | otherwise = let (mb_ty,ltys') = takeIt l1 ltys
                     in (mb_ty,lty:ltys')
 
@@ -390,13 +390,13 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
                | s == cPType -> return mb_ty
              VMeta _ _ _     -> return mb_ty
              _               -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
-                                   tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ 
+                                   tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
                                             "cannot be of type" <+> ppTerm Unqualified 0 sort)
   (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
   return ((l,ty):rs,mb_ty)
 
 -- | Invariant: if the third argument is (Just rho),
--- 	            then rho is in weak-prenex form
+--              then rho is in weak-prenex form
 instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
 instSigma ge scope t ty1 Nothing    = return (t,ty1)           -- INST1
 instSigma ge scope t ty1 (Just ty2) = do                       -- INST2
@@ -444,11 +444,11 @@ subsCheckRho ge scope t (VApp p1 _) (VApp p2 _)                         -- Rule
   | predefName p1 == cInts && predefName p2 == cInt = return t
 subsCheckRho ge scope t (VApp p1 [VInt i]) (VApp p2 [VInt j])           -- Rule INT2
   | predefName p1 == cInts && predefName p2 == cInts =
-      if i <= j 
+      if i <= j
         then return t
         else tcError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
 subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
-  let mkAccess scope t = 
+  let mkAccess scope t =
         case t of
           ExtR t1 t2 -> do (scope,mkProj1,mkWrap1) <- mkAccess scope t1
                            (scope,mkProj2,mkWrap2) <- mkAccess scope t2
@@ -557,7 +557,7 @@ unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
 unify ge scope v1 v2 = do
   t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
   t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
-  tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ 
+  tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
                                       ppTerm Unqualified 0 t2))
 
 -- | Invariant: tv1 is a flexible type variable
@@ -568,9 +568,9 @@ unifyVar ge scope i env vs ty2 = do            -- Check whether i is bound
     Bound ty1       -> do v <- liftErr (eval ge env ty1)
                           unify ge scope (vapply (geLoc ge) v vs) ty2
     Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
-                          Left i     -> let (v,_) = reverse scope !! i
-                                        in tcError ("Variable" <+> pp v <+> "has escaped")
-                          Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
+                          -- Left i     -> let (v,_) = reverse scope !! i
+                          --               in tcError ("Variable" <+> pp v <+> "has escaped")
+                                ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
                                            if i `elem` ms2
                                              then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
                                                            nest 2 (ppTerm Unqualified 0 ty2'))
@@ -609,7 +609,7 @@ quantify ge scope t tvs ty0 = do
   ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
   let used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
       new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
-  mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way 
+  mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way
   ty <- zonkTerm ty                  -- of doing the substitution
   vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
   return (foldr (Abs Implicit) t new_bndrs,vty)
@@ -619,7 +619,7 @@ quantify ge scope t tvs ty0 = do
     bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1  ++ bndrs t2
     bndrs _                = []
 
-allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,... 
+allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,...
 allBinders = [ identS [x]          | x <- ['a'..'z'] ] ++
              [ identS (x : show i) | i <- [1 :: Integer ..], x <- ['a'..'z']]
 
@@ -631,8 +631,8 @@ allBinders = [ identS [x]          | x <- ['a'..'z'] ] ++
 type Scope = [(Ident,Value)]
 
 type Sigma = Value
-type Rho   = Value	-- No top-level ForAll
-type Tau   = Value	-- No ForAlls anywhere
+type Rho   = Value -- No top-level ForAll
+type Tau   = Value -- No ForAlls anywhere
 
 data MetaValue
   = Unbound Scope Sigma
@@ -688,12 +688,12 @@ runTcM f = case unTcM f IntMap.empty [] of
              TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
 
 newMeta :: Scope -> Sigma -> TcM MetaId
-newMeta scope ty = TcM (\ms msgs -> 
+newMeta scope ty = TcM (\ms msgs ->
   let i = IntMap.size ms
   in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
 
 getMeta :: MetaId -> TcM MetaValue
-getMeta i = TcM (\ms msgs -> 
+getMeta i = TcM (\ms msgs ->
   case IntMap.lookup i ms of
     Just mv -> TcOk mv ms msgs
     Nothing -> TcFail (("Unknown metavariable" <+> ppMeta i) : msgs))
@@ -702,7 +702,7 @@ setMeta :: MetaId -> MetaValue -> TcM ()
 setMeta i mv = TcM (\ms msgs -> TcOk () (IntMap.insert i mv ms) msgs)
 
 newVar :: Scope -> Ident
-newVar scope = head [x | i <- [1..], 
+newVar scope = head [x | i <- [1..],
                          let x = identS ('v':show i),
                          isFree scope x]
   where
@@ -721,11 +721,11 @@ getMetaVars loc sc_tys = do
   return (foldr go [] tys)
   where
     -- Get the MetaIds from a term; no duplicates in result
-    go (Vr tv)    acc = acc 
+    go (Vr tv)    acc = acc
     go (App x y)  acc = go x (go y acc)
     go (Meta i)   acc
-	  | i `elem` acc  = acc
-	  | otherwise	  = i : acc
+      | i `elem` acc  = acc
+      | otherwise     = i : acc
     go (Q _)      acc = acc
     go (QC _)     acc = acc
     go (Sort _)   acc = acc
@@ -741,10 +741,10 @@ getFreeVars loc sc_tys = do
   tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
   return (foldr (go []) [] tys)
   where
-    go bound (Vr tv)            acc 
-	  | tv `elem` bound             = acc
-	  | tv `elem` acc               = acc
-	  | otherwise                   = tv : acc
+    go bound (Vr tv)            acc
+      | tv `elem` bound             = acc
+      | tv `elem` acc               = acc
+      | otherwise                   = tv : acc
     go bound (App x y)          acc = go bound x (go bound y acc)
     go bound (Meta _)           acc = acc
     go bound (Q _)              acc = acc
@@ -765,13 +765,13 @@ zonkTerm (Meta i) = do
 zonkTerm t = composOp zonkTerm t
 
 tc_value2term loc xs v =
-  case value2term loc xs v of
-    Left i  -> tcError ("Variable #" <+> pp i <+> "has escaped")
-    Right t -> return t
+  return $ value2term loc xs v
+    -- Old value2term error message:
+    -- Left i  -> tcError ("Variable #" <+> pp i <+> "has escaped")
 
 
 
-data TcA x a 
+data TcA x a
   = TcSingle   (MetaStore -> [Message] -> TcResult a)
   | TcMany [x] (MetaStore -> [Message] -> [(a,MetaStore,[Message])])
 
diff --git a/src/compiler/GF/Compile/TypeCheck/RConcrete.hs b/src/compiler/GF/Compile/TypeCheck/RConcrete.hs
deleted file mode 100644
index aa13d5406..000000000
--- a/src/compiler/GF/Compile/TypeCheck/RConcrete.hs
+++ /dev/null
@@ -1,801 +0,0 @@
-{-# LANGUAGE PatternGuards #-}
-module GF.Compile.TypeCheck.RConcrete( checkLType, inferLType, computeLType, ppType ) where
-import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
-
-import GF.Infra.CheckM
-import GF.Data.Operations
-
-import GF.Grammar
-import GF.Grammar.Lookup
-import GF.Grammar.Predef
-import GF.Grammar.PatternMatch
-import GF.Grammar.Lockfield (isLockLabel, lockRecType, unlockRecord)
-import GF.Compile.TypeCheck.Primitives
-
-import Data.List
-import Control.Monad
-import GF.Text.Pretty
-
-computeLType :: SourceGrammar -> Context -> Type -> Check Type
-computeLType gr g0 t = comp (reverse [(b,x, Vr x) | (b,x,_) <- g0] ++ g0) t
- where
-  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 ("module" <+> m) $ do
-      ty' <- lookupResDef gr (m,ident)
-      if ty' == ty then return ty else comp g ty' --- is this necessary to test?
-
-    AdHocOverload ts -> do
-     over <- getOverload gr g (Just typeType) t
-     case over of
-       Just (tr,_) -> return tr
-       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 t) 
-
-    Vr ident  -> checkLookup ident g -- never needed to compute!
-
-    App f a -> do
-      f' <- comp g f
-      a' <- comp g a
-      case f' of
-        Abs b x t -> comp ((b,x,a'):g) t
-        _ -> return $ App f' a'
-
-    Prod bt x a b -> do
-      a' <- comp g a
-      b' <- comp ((bt,x,Vr x) : g) b
-      return $ Prod bt x a' b'
-
-    Abs bt x b -> do
-      b' <- comp ((bt,x,Vr x):g) b
-      return $ Abs bt x b'
-
-    Let (x,(_,a)) b -> comp ((Explicit,x,a):g) b
-
-    ExtR r s -> do
-      r' <- comp g r
-      s' <- comp g s
-      case (r',s') of
-        (RecType rs, RecType ss) -> plusRecType r' s' >>= comp g
-        _ -> return $ ExtR r' s'
-
-    RecType fs -> do
-      let fs' = sortRec fs
-      liftM RecType $ mapPairsM (comp g) fs'
-
-    ELincat c t -> do
-      t' <- comp g t
-      lockRecType c t' ---- locking to be removed AR 20/6/2009
-
-    _ | ty == typeTok -> return typeStr
-    _ | isPredefConstant ty -> return ty
-
-    _ -> composOp (comp g) ty
-
--- the underlying algorithms
-
-inferLType :: SourceGrammar -> Context -> Term -> Check (Term, Type)
-inferLType gr g trm = case trm of
-
-   Q (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
-                                                Just ty -> return ty
-                                                Nothing -> checkError ("unknown in Predef:" <+> ident)
-
-   Q ident -> checks [
-     termWith trm $ lookupResType gr ident >>= computeLType gr g
-     ,
-     lookupResDef gr ident >>= inferLType gr g
-     ,
-     checkError ("cannot infer type of constant" <+> ppTerm Unqualified 0 trm)
-     ]
-
-   QC (m,ident) | isPredef m -> termWith trm $ case typPredefined ident of
-                                                 Just ty -> return ty
-                                                 Nothing -> checkError ("unknown in Predef:" <+> ident)
-
-   QC ident -> checks [
-       termWith trm $ lookupResType gr ident >>= computeLType gr g
-       ,
-       lookupResDef gr ident >>= inferLType gr g
-       ,
-       checkError ("cannot infer type of canonical constant" <+> ppTerm Unqualified 0 trm)
-       ]
-
-   Vr ident -> termWith trm $ checkLookup ident g
-
-   Typed e t -> do
-     t' <- computeLType gr g t
-     checkLType gr g e t'
-
-   AdHocOverload ts -> do
-     over <- getOverload gr g Nothing trm
-     case over of
-       Just trty -> return trty
-       _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) 
-
-   App f a -> do
-     over <- getOverload gr g Nothing trm
-     case over of
-       Just trty -> return trty
-       _ -> do
-         (f',fty) <- inferLType gr g f
-         fty' <- computeLType gr g fty
-         case fty' of
-           Prod bt z arg val -> do 
-             a' <- justCheck g a arg
-             ty <- if isWildIdent z 
-                      then return val
-                      else substituteLType [(bt,z,a')] val
-             return (App f' a',ty)
-           _ ->
-             let term = ppTerm Unqualified 0 f
-                 funName = pp . head . words .render $ term
-              in checkError ("A function type is expected for" <+> term <+> "instead of type" <+> ppType fty $$
-                             "\n   ** Maybe you gave too many arguments to" <+> funName <+> "\n")
-
-   S f x -> do
-     (f', fty) <- inferLType gr g f
-     case fty of
-       Table arg val -> do
-         x'<- justCheck g x arg
-         return (S f' x', val)
-       _ -> checkError ("table lintype expected for the table in" $$ nest 2 (ppTerm Unqualified 0 trm))
-
-   P t i -> do
-     (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
-                       Nothing -> checkError ("unknown label" <+> i <+> "in" $$ nest 2 (ppTerm Unqualified 0 ty'))
-                       Just x  -> return x
-       _          -> checkError ("record type expected for:" <+> ppTerm Unqualified 0 t $$
-                                 " instead of the inferred:" <+> ppTerm Unqualified 0 ty')
-
-   R r -> do
-     let (ls,fs) = unzip r
-     fsts <- mapM inferM fs
-     let ts = [ty | (Just ty,_) <- fsts]
-     checkCond ("cannot infer type of record" $$ nest 2 (ppTerm Unqualified 0 trm)) (length ts == length fsts)
-     return $ (R (zip ls fsts), RecType (zip ls ts))
-
-   T (TTyped arg) pts -> do
-     (_,val) <- checks $ map (inferCase (Just arg)) pts
-     checkLType gr g trm (Table arg val)
-   T (TComp arg) pts -> do
-     (_,val) <- checks $ map (inferCase (Just arg)) pts
-     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 
-       [] -> checkError ("cannot infer table type of" <+> ppTerm Unqualified 0 trm)
-----       PInt k : _ -> return $ Ints $ max [i | PInt i <- pts'] 
-       _  -> do 
-         (arg,val) <- checks $ map (inferCase Nothing) pts'
-         checkLType gr g trm (Table arg val)
-   V arg pts -> do
-     (_,val) <- checks $ map (inferLType gr g) pts
---   return (trm, Table arg val) -- old, caused issue 68
-     checkLType gr g trm (Table arg val)
-
-   K s  -> do
-     if elem ' ' s
-        then do
-          let ss = foldr C Empty (map K (words s))  
-          ----- removed irritating warning AR 24/5/2008
-          ----- checkWarn ("token \"" ++ s ++ 
-          -----              "\" converted to token list" ++ prt ss)
-          return (ss, typeStr)
-        else return (trm, typeStr)
-
-   EInt i -> return (trm, typeInt)
-
-   EFloat i -> return (trm, typeFloat)
-
-   Empty -> return (trm, typeStr)
-
-   C s1 s2 -> 
-     check2 (flip (justCheck g) typeStr) C s1 s2 typeStr
-
-   Glue s1 s2 -> 
-     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 ("unresolved constant, could be any of" <+> hcat (map (ppTerm Unqualified 0) ts))
-     inferLType gr g (head ts)
-
-   Strs ts -> do
-     ts' <- mapM (\t -> justCheck g t typeStr) ts 
-     return (Strs ts', typeStrs)
-
-   Alts t aa -> do
-     t'  <- justCheck g t typeStr
-     aa' <- flip mapM aa (\ (c,v) -> do
-        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 g) typeType) ts 
-     return (RecType (zip ls ts'), typeType)
-
-   ExtR r s -> do
-   
----     over <- getOverload gr g Nothing r
----     let r1 = maybe r fst over
-     let r1 = r --- 
-
-     (r',rT) <- inferLType gr g r1
-     rT'     <- computeLType gr g rT
-     
-     (s',sT) <- inferLType gr g s
-     sT'     <- computeLType gr g sT
-
-     let trm' = ExtR r' s'
-     case (rT', sT') of
-       (RecType rs, RecType ss) -> do
-         let rt = RecType ([field | field@(l,_) <- rs, notElem l (map fst ss)] ++ ss) -- select types of later fields 
-         checkLType gr g trm' rt ---- return (trm', rt)
-       _ | rT' == typeType && sT' == typeType -> do
-         return (trm', typeType)
-       _ -> checkError ("records or record types expected in" <+> ppTerm Unqualified 0 trm)
-
-   Sort _     -> 
-     termWith trm $ return typeType
-
-   Prod bt x a b -> do
-     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 g p typeType --- check p partype! 
-     t' <- justCheck g t typeType
-     return $ (Table p' t', typeType)
-
-   FV vs -> do
-     (_,ty) <- checks $ map (inferLType gr g) vs
----     checkIfComplexVariantType trm ty
-     checkLType gr g trm ty
-
-   EPattType ty -> do
-     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) <- inferLType gr g trm
-     ty' <- lockRecType c ty ---- lookup c; remove lock AR 20/6/2009
-     return $ (ELin c trm', ty') 
-
-   _ -> checkError ("cannot infer lintype of" <+> ppTerm Unqualified 0 trm)
-
- where
-   isPredef m = elem m [cPredef,cPredefAbs]
-
-   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 -> checkLType gr g t ty
-       _ -> inferLType gr g t
-     return (Just ty',t')
-
-   inferCase mty (patt,term) = do
-     arg  <- maybe (inferPatt patt) return mty
-     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
-     PP _ ps -> True --- all isConstPatt ps
-     PR ps -> all (isConstPatt . snd) ps
-     PT _ p -> isConstPatt p
-     PString _ -> True
-     PInt _ -> True
-     PFloat _ -> True
-     PChar -> True
-     PChars _ -> True
-     PSeq p q -> isConstPatt p && isConstPatt q
-     PAlt p q -> isConstPatt p && isConstPatt q
-     PRep p -> isConstPatt p
-     PNeg p -> isConstPatt p
-     PAs _ p -> isConstPatt p
-     _ -> False
-
-   inferPatt p = case p of
-     PP (q,c) ps | q /= cPredef -> liftM valTypeCnc (lookupResType gr (q,c))
-     PAs _ p  -> inferPatt p
-     PNeg p   -> inferPatt p
-     PAlt p q -> checks [inferPatt p, inferPatt q]
-     PSeq _ _ -> return $ typeStr
-     PRep _   -> return $ typeStr
-     PChar    -> return $ typeStr
-     PChars _ -> return $ typeStr
-     _ -> inferLType gr g (patt2term p) >>= return . snd
-
--- type inference: Nothing, type checking: Just t
--- the latter permits matching with value type
-getOverload :: SourceGrammar -> Context -> Maybe Type -> Term -> Check (Maybe (Term,Type))
-getOverload gr g mt ot = case appForm ot of
-     (f@(Q c), ts) -> case lookupOverload gr c of
-       Ok typs -> do
-         ttys <- mapM (inferLType gr g) ts
-         v <- matchOverload f typs ttys
-         return $ Just v
-       _ -> return Nothing
-     (AdHocOverload cs@(f:_), ts) -> do     --- the function name f is only used in error messages
-       let typs = concatMap collectOverloads cs
-       ttys <- mapM (inferLType gr g) ts
-       v <- matchOverload f typs ttys
-       return $ Just v
-     _ -> return Nothing
-     
- where
-   collectOverloads tr@(Q c) = case lookupOverload gr c of 
-     Ok typs -> typs
-     _ -> case lookupResType gr c of
-       Ok ty -> let (args,val) = typeFormCnc ty in [(map (\(b,x,t) -> t) args,(val,tr))]
-       _ -> []
-   collectOverloads _ = [] --- constructors QC
-
-   matchOverload f typs ttys = do
-     let (tts,tys) = unzip ttys
-     let vfs = lookupOverloadInstance tys typs
-     let matches = [vf | vf@((_,v,_),_) <- vfs, matchVal mt v]
-     let showTypes ty = hsep (map ppType ty)
-
-    
-     let (stys,styps) = (showTypes tys, [showTypes ty | (ty,_) <- typs])
-
-     -- to avoid strange error msg e.g. in case of unmatch record extension, show whole types if needed AR 28/1/2013
-     let (stysError,stypsError) = if elem (render stys) (map render styps)
-            then (hsep (map (ppTerm Unqualified 0) tys), [hsep (map (ppTerm Unqualified 0) ty) | (ty,_) <- typs])
-            else (stys,styps)
-
-     case ([vf | (vf,True) <- matches],[vf | (vf,False) <- matches]) of
-       ([(_,val,fun)],_) -> return (mkApp fun tts, val)
-       ([],[(pre,val,fun)]) -> do
-         checkWarn $  "ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot $$
-                      "for" $$
-                      nest 2 (showTypes tys) $$
-                      "using" $$
-                      nest 2 (showTypes pre)
-         return (mkApp fun tts, val)
-       ([],[]) -> do
-         checkError $ "no overload instance of" <+> ppTerm Qualified 0 f $$
-                      maybe empty (\x -> "with value type" <+> ppType x) mt $$
-                      "for argument list" $$
-                      nest 2 stysError $$
-                      "among alternatives" $$
-                      nest 2 (vcat stypsError) 
-
-
-       (vfs1,vfs2) -> case (noProds vfs1,noProds vfs2) of
-         ([(val,fun)],_) -> do
-           return (mkApp fun tts, val)
-         ([],[(val,fun)]) -> do
-           checkWarn ("ignoring lock fields in resolving" <+> ppTerm Unqualified 0 ot) 
-           return (mkApp fun tts, val)
-
------ unsafely exclude irritating warning AR 24/5/2008
------           checkWarn $ "overloading of" +++ prt f +++ 
------             "resolved by excluding partial applications:" ++++
------             unlines [prtType env ty | (ty,_) <- vfs', not (noProd ty)]
-
---- now forgiving ambiguity with a warning AR 1/2/2014
---  This gives ad hoc overloading the same behaviour as the choice of the first match in renaming did before. 
---  But it also gives a chance to ambiguous overloadings that were banned before. 
-         (nps1,nps2) -> do 
-              checkWarn $  "ambiguous overloading of" <+> ppTerm Unqualified 0 f <+>
-                  ----     "with argument types" <+> hsep (map (ppTerm Qualified 0) tys) $$ 
-                           "resolved by selecting the first of the alternatives" $$
-                           nest 2 (vcat [ppTerm Qualified 0 fun | (_,ty,fun) <- vfs1 ++ if null vfs1 then vfs2 else []])
-              case [(mkApp fun tts,val) | (val,fun) <- nps1 ++ nps2] of
-                 [] -> checkError $ "no alternatives left when resolving" <+> ppTerm Unqualified 0 f
-                 h:_ -> return h
-
-   matchVal mt v = elem mt [Nothing,Just v,Just (unlocked v)]
-
-   unlocked v = case v of
-     RecType fs -> RecType $ filter (not . isLockLabel . fst) (sortRec fs)
-     _ -> v
-   ---- TODO: accept subtypes
-   ---- TODO: use a trie
-   lookupOverloadInstance tys typs = 
-     [((pre,mkFunType rest val, t),isExact) | 
-       let lt = length tys,
-       (ty,(val,t)) <- typs, length ty >= lt,
-       let (pre,rest) = splitAt lt ty, 
-       let isExact = pre == tys,
-       isExact || map unlocked pre == map unlocked tys
-     ]
-
-   noProds vfs = [(v,f) | (_,v,f) <- vfs, noProd v]
-
-   noProd ty = case ty of
-     Prod _ _ _ _ -> False
-     _ -> True
-
-checkLType :: SourceGrammar -> Context -> Term -> Type -> Check (Term, Type)
-checkLType gr g trm typ0 = do
-  typ <- computeLType gr g typ0
-
-  case trm of
-
-    Abs bt x c -> do
-      case typ of
-        Prod bt' z a b -> do 
-          (c',b') <- if isWildIdent z
-                       then checkLType gr ((bt,x,a):g) c b
-                       else do b' <- checkIn (pp "abs") $ substituteLType [(bt',z,Vr x)] b
-                               checkLType gr ((bt,x,a):g) c b'
-          return $ (Abs bt x c', Prod bt' z a b')
-        _ -> checkError $ "function type expected instead of" <+> ppType typ $$
-                          "\n   ** Double-check that the type signature of the operation" $$
-                          "matches the number of arguments given to it.\n"
-
-    App f a -> do
-       over <- getOverload gr g (Just typ) trm
-       case over of
-         Just trty -> return trty
-         _ -> do
-          (trm',ty') <- inferLType gr g trm
-          termWith trm' $ checkEqLType gr g typ ty' trm'
-
-    AdHocOverload ts -> do
-      over <- getOverload gr g Nothing trm
-      case over of
-        Just trty -> return trty
-        _ -> checkError ("unresolved overloading of constants" <+> ppTerm Qualified 0 trm) 
-
-    Q _ -> do
-       over <- getOverload gr g (Just typ) trm
-       case over of
-         Just trty -> return trty
-         _ -> do
-          (trm',ty') <- inferLType gr g trm
-          termWith trm' $ checkEqLType gr g typ ty' trm'
-
-    T _ [] ->
-      checkError ("found empty table in type" <+> ppTerm Unqualified 0 typ)
-    T _ cs -> case typ of 
-      Table arg val -> do 
-        case allParamValues gr arg of
-          Ok vs -> do
-            let ps0 = map fst cs
-            ps <- testOvershadow ps0 vs
-            if null ps 
-              then return () 
-              else checkWarn ("patterns never reached:" $$
-                              nest 2 (vcat (map (ppPatt Unqualified 0) ps)))
-          _ -> return () -- happens with variable types
-        cs' <- mapM (checkCase arg val) cs
-        return (T (TTyped arg) cs', typ)
-      _ -> checkError $ "table type expected for table instead of" $$ nest 2 (ppType typ)
-    V arg0 vs ->
-      case typ of
-        Table arg1 val ->
-           do arg' <- checkEqLType gr g arg0 arg1 trm
-              vs1 <- allParamValues gr arg1
-              if length vs1 == length vs
-                 then return ()
-                 else checkError $ "wrong number of values in table" <+> ppTerm Unqualified 0 trm
-              vs' <- map fst `fmap` sequence [checkLType gr g v val|v<-vs]
-              return (V arg' vs',typ)
-
-    R r -> case typ of --- why needed? because inference may be too difficult
-       RecType rr -> do
-       --let (ls,_) = unzip rr        -- labels of expected type
-         fsts <- mapM (checkM r) rr   -- check that they are found in the record
-         return $ (R fsts, typ)       -- normalize record
-
-       _ -> checkError ("record type expected in type checking instead of" $$ nest 2 (ppTerm Unqualified 0 typ))
-
-    ExtR r s -> case typ of
-       _ | typ == typeType -> do
-         trm' <- computeLType gr g trm
-         case trm' of
-           RecType _ -> termWith trm' $ return typeType
-           ExtR (Vr _) (RecType _) -> termWith trm' $ return typeType 
-                                      -- ext t = t ** ...
-           _ -> checkError ("invalid record type extension" <+> nest 2 (ppTerm Unqualified 0 trm))
-
-       RecType rr -> do
-
-         ll2 <- case s of
-           R ss -> return $ map fst ss
-           _ -> do
-             (s',typ2) <- inferLType gr g s
-             case typ2 of
-               RecType ss -> return $ map fst ss
-               _ ->  checkError ("cannot get labels from" $$ nest 2 (ppTerm Unqualified 0 typ2))
-         let ll1 = [l | (l,_) <- rr, notElem l ll2]
-
----         over <- getOverload gr g Nothing r --- this would solve #66 but fail ParadigmsAra. AR 6/7/2020
----         let r1 = maybe r fst over
-         let r1 = r ---
-         
-         (r',_) <- checkLType gr g r1 (RecType [field | field@(l,_) <- rr, elem l ll1])
-         (s',_) <- checkLType gr g s  (RecType [field | field@(l,_) <- rr, elem l ll2])
-
-         let rec = R ([(l,(Nothing,P r' l)) | l <- ll1] ++ [(l,(Nothing,P s' l)) | l <- ll2])
-         return (rec, typ)
-
-       ExtR ty ex -> do
-         r' <- justCheck g r ty
-         s' <- justCheck g s ex
-         return $ (ExtR r' s', typ) --- is this all? it assumes the same division in trm and typ
-
-       _ -> checkError ("record extension not meaningful for" <+> ppTerm Unqualified 0 typ)
-
-    FV vs -> do
-      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) <- inferLType gr g tab
-      ty'       <- computeLType gr g ty
-      case ty' of
-        Table p t -> do
-          (arg',val) <- checkLType gr g arg p
-          checkEqLType gr g typ t trm
-          return (S tab' arg', t)
-        _ -> checkError ("table type expected for applied table instead of" <+> ppType ty')
-     , do
-      (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
-        (ty0,_)    <- checkLType gr g ty typeType
-        (def',ty') <- checkLType gr g def ty0
-        body' <- justCheck ((Explicit,x,ty'):g) body typ
-        return (Let (x,(Just ty',def')) body', typ)
-      _ -> do
-        (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 <- unlockRecord c tr
-      checkLType gr g tr1 typ
-
-    _ -> do
-      (trm',ty') <- inferLType gr g trm
-      termWith trm' $ checkEqLType gr g typ ty' trm'
- where
-   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
-       checkEqLType gr g ty ty0 t
-       (t',ty') <- checkLType gr g t ty
-       return (l,(Just ty',t'))
-     Just (_,t) -> do
-       (t',ty') <- checkLType gr g t ty
-       return (l,(Just ty',t'))
-     _ -> checkError $ 
-            if isLockLabel l 
-              then let cat = drop 5 (showIdent (label2ident l))
-                   in ppTerm Unqualified 0 (R rms) <+> "is not in the lincat of" <+> cat <> 
-                      "; try wrapping it with lin" <+> cat
-              else "cannot find value for label" <+> l <+> "in" <+> ppTerm Unqualified 0 (R rms)
-
-   checkCase arg val (p,t) = do
-     cont <- pattContext gr g arg p
-     t' <- justCheck (reverse cont ++ g) t val
-     return (p,t')
-
-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 <- lookupResType env (q,c)
-    let (cont,v) = typeFormCnc t
-    checkCond ("wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
-              (length cont == length ps)
-    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 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 g)) pts >>= return . concat
-      _ -> checkError ("record type expected for pattern instead of" <+> ppTerm Unqualified 0 typ')
-  PT t p' -> do
-    checkEqLType env g typ t (patt2term p')
-    pattContext env g typ p'
-
-  PAs x p -> do
-    g' <- pattContext env g typ p
-    return ((Explicit,x,typ):g')
-
-  PAlt p' q -> do
-    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 
-      ("incompatible bindings of" <+>
-       fsep pts <+> 
-       "in pattern alterantives" <+> ppPatt Unqualified 0 p) (null pts) 
-    return g1 -- must be g1 == g2
-  PSeq p q -> do
-    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 
-   noBind typ p' = do
-    co <- pattContext env g typ p'
-    if not (null co)
-      then checkWarn ("no variable bound inside pattern" <+> ppPatt Unqualified 0 p) 
-           >> return []
-      else return []
-
-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 ->
-      let inferredType = ppTerm Qualified 0 u
-          expectedType = ppTerm Qualified 0 t
-          term = ppTerm Unqualified 0 trm
-          funName = pp . head . words .render $ term
-          helpfulMsg =
-            case (arrows inferredType, arrows expectedType) of
-              (0,0) -> pp "" -- None of the types is a function
-              _ -> "\n   **" <+> 
-                  if expectedType `isLessApplied` inferredType
-                    then "Maybe you gave too few arguments to" <+> funName
-                    else pp "Double-check that type signature and number of arguments match."
-      in checkError $ s <+> "type of" <+> term $$
-                            "expected:" <+> expectedType $$ -- ppqType t u $$
-                            "inferred:" <+> inferredType $$ -- ppqType u t
-                            helpfulMsg
-  where
-    -- count the number of arrows in the prettyprinted term
-    arrows :: Doc -> Int
-    arrows = length . filter (=="->") . words . render
-
-    -- If prettyprinted type t has fewer arrows then prettyprinted type u,
-    -- then t is "less applied", and we can print out more helpful error msg.
-    isLessApplied :: Doc -> Doc -> Bool
-    isLessApplied t u = arrows t < arrows 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.
-    --- better: use a flag to forgive? (AR 31/1/2006)
-    _ -> case missingLock [] t' u' of
-      Ok lo -> do
-        checkWarn $ "missing lock field" <+> fsep lo
-        return (True,t',u',[])
-      Bad s -> return (False,t',u',s)
-
-  where
-
-   -- check that u is a subtype of t
-   --- quick hack version of TC.eqVal
-   alpha g t u = case (t,u) of  
-
-     -- error (the empty type!) is subtype of any other type
-     (_,u) | u == typeError -> True
-
-     -- contravariance
-     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d 
-                              
-     -- record subtyping
-     (RecType rs, RecType ts) -> all (\ (l,a) -> 
-                                   any (\ (k,b) -> l == k && alpha g a b) ts) rs
-     (ExtR r s, ExtR r' s') -> alpha g r r' && alpha g s s'
-     (ExtR r s, t) -> alpha g r t || alpha g s t
-
-     -- the following say that Ints n is a subset of Int and of Ints m >= n
-     -- But why does it also allow Int as a subtype of Ints m? /TH 2014-04-04
-     (t,u) | Just m <- isTypeInts t, Just n <- isTypeInts u -> m >= n
-           | Just _ <- isTypeInts t, u == typeInt           -> True ---- check size!
-           | 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 gr n) 
-                                   || elem n (allExtendsPlus gr m)
-                                   || m == n --- for Predef
-     (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)
-
-     -- contravariance
-     (Table a b,  Table c d)  -> alpha g c a && alpha g b d
-     (Vr x,       Vr y)       -> x == y || elem (x,y) g || elem (y,x) g
-     _                        -> t == u 
-     --- the following should be one-way coercions only. AR 4/1/2001
-                                  || elem t sTypes && elem u sTypes
-                                  || (t == typeType && u == typePType) 
-                                  || (u == typeType && t == typePType) 
-
-   missingLock g t u = case (t,u) of  
-     (RecType rs, RecType ts) -> 
-       let 
-         ls = [l | (l,a) <- rs, 
-                   not (any (\ (k,b) -> alpha g a b && l == k) ts)]
-         (locks,others) = partition isLockLabel ls
-       in case others of
-         _:_ -> Bad $ render ("missing record fields:" <+> fsep (punctuate ',' (others)))
-         _ -> return locks
-     -- contravariance
-     (Prod _ x a b, Prod _ y c d) -> do
-        ls1 <- missingLock g c a
-        ls2 <- missingLock g b d
-        return $ ls1 ++ ls2
-
-     _ -> Bad ""
-
-   sTypes = [typeStr, typeTok, typeString]
-
--- auxiliaries
-
--- | light-weight substitution for dep. types
-substituteLType :: Context -> Type -> Check Type
-substituteLType g t = case t of
-  Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
-  _ -> composOp (substituteLType g) t
-
-termWith :: Term -> Check Type -> Check (Term, Type)
-termWith t ct = do
-  ty <- ct
-  return (t,ty)
-
--- | compositional check\/infer of binary operations
-check2 :: (Term -> Check Term) -> (Term -> Term -> Term) -> 
-          Term -> Term -> Type -> Check (Term,Type)
-check2 chk con a b t = do
-  a' <- chk a
-  b' <- chk b
-  return (con a' b', t)
-
--- printing a type with a lock field lock_C as C
-ppType :: Type -> Doc
-ppType ty =
-  case ty of
-    RecType fs   -> case filter isLockLabel $ map fst fs of
-                      [lock] -> pp (drop 5 (showIdent (label2ident lock)))
-                      _      -> ppTerm Unqualified 0 ty
-    Prod _ x a b -> ppType a <+> "->" <+> ppType b
-    _            -> ppTerm Unqualified 0 ty
-{-
-ppqType :: Type -> Type -> Doc
-ppqType t u = case (ppType t, ppType u) of
-  (pt,pu) | render pt == render pu -> ppTerm Qualified 0 t
-  (pt,_) -> pt
--}
-checkLookup :: Ident -> Context -> Check Type
-checkLookup x g =
-  case [ty | (b,y,ty) <- g, x == y] of
-    []     -> checkError ("unknown variable" <+> x)
-    (ty:_) -> return ty
diff --git a/src/compiler/GF/Compile/TypeCheck/TC.hs b/src/compiler/GF/Compile/TypeCheck/TC.hs
index abcb24617..c0df83394 100644
--- a/src/compiler/GF/Compile/TypeCheck/TC.hs
+++ b/src/compiler/GF/Compile/TypeCheck/TC.hs
@@ -5,21 +5,22 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/10/02 20:50:19 $ 
+-- > CVS $Date: 2005/10/02 20:50:19 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.11 $
 --
 -- Thierry Coquand's type checking algorithm that creates a trace
 -----------------------------------------------------------------------------
 
-module GF.Compile.TypeCheck.TC (AExp(..),
-	   Theory,
-	   checkExp,
-	   inferExp,
-	   checkBranch,
-	   eqVal,
-	   whnf
-	  ) where
+module GF.Compile.TypeCheck.TC (
+    AExp(..),
+    Theory,
+    checkExp,
+    inferExp,
+    checkBranch,
+    eqVal,
+    whnf
+  ) where
 
 import GF.Data.Operations
 import GF.Grammar
@@ -31,17 +32,17 @@ import Data.Maybe
 import GF.Text.Pretty
 
 data AExp =
-     AVr   Ident Val 
+     AVr   Ident Val
    | ACn   QIdent Val
-   | AType 
-   | AInt  Int 
+   | AType
+   | AInt  Int
    | AFloat Double
    | AStr  String
    | AMeta MetaId Val
    | ALet  (Ident,(Val,AExp)) AExp
-   | AApp  AExp AExp Val 
-   | AAbs  Ident Val AExp 
-   | AProd Ident AExp AExp 
+   | AApp  AExp AExp Val
+   | AAbs  Ident Val AExp
+   | AProd Ident AExp AExp
 -- -- | AEqs  [([Exp],AExp)] --- not used
    | ARecType [ALabelling]
    | AR    [AAssign]
@@ -50,7 +51,7 @@ data AExp =
    | AData Val
   deriving (Eq,Show)
 
-type ALabelling = (Label, AExp) 
+type ALabelling = (Label, AExp)
 type AAssign = (Label, (Val, AExp))
 
 type Theory = QIdent -> Err Val
@@ -71,7 +72,7 @@ whnf :: Val -> Err Val
 whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
          case v of
   VApp u w -> do
-    u' <- whnf u 
+    u' <- whnf u
     w' <- whnf w
     app u' w'
   VClos env e -> eval env e
@@ -81,9 +82,9 @@ app :: Val -> Val -> Err Val
 app u v = case u of
   VClos env (Abs _ x e) -> eval ((x,v):env) e
   _ -> return $ VApp u v
-  
+
 eval :: Env -> Term -> Err Val
-eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $ 
+eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
              case e of
   Vr x    -> lookupVar env x
   Q c   -> return $ VCn c
@@ -95,23 +96,23 @@ eval env e = ---- errIn ("eval" +++ prt e +++ "in" +++ prEnv env) $
   _ -> return $ VClos env e
 
 eqVal :: Int -> Val -> Val -> Err [(Val,Val)]
-eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $ 
+eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
                 do
   w1 <- whnf u1
-  w2 <- whnf u2 
+  w2 <- whnf u2
   let v = VGen k
   case (w1,w2) of
     (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
     (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
       eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
     (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
-      liftM2 (++) 
+      liftM2 (++)
         (eqVal k     (VClos            env1  a1) (VClos            env2  a2))
         (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
     (VGen i _, VGen j _) -> return [(w1,w2) | i /= j]
-    (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j] 
+    (VCn (_, i), VCn (_,j)) -> return [(w1,w2) | i /= j]
     --- thus ignore qualifications; valid because inheritance cannot
-    --- be qualified. Simplifies annotation. AR 17/3/2005 
+    --- be qualified. Simplifies annotation. AR 17/3/2005
     _ -> return [(w1,w2) | w1 /= w2]
 -- invariant: constraints are in whnf
 
@@ -127,10 +128,10 @@ checkExp th tenv@(k,rho,gamma) e ty = do
 
     Abs _ x t -> case typ of
       VClos env (Prod _ y a b) -> do
-	a' <- whnf $ VClos env a ---
-	(t',cs) <- checkExp th 
-                           (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
-	return (AAbs x a' t', cs)
+                           a' <- whnf $ VClos env a ---
+                           (t',cs) <- checkExp th
+                                          (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
+                           return (AAbs x a' t', cs)
       _ -> Bad (render ("function type expected for" <+> ppTerm Unqualified 0 e <+> "instead of" <+> ppValue Unqualified 0 typ))
 
     Let (x, (mb_typ, e1)) e2 -> do
@@ -150,7 +151,7 @@ checkExp th tenv@(k,rho,gamma) e ty = do
       (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
       return (AProd x a' b', csa ++ csb)
 
-    R xs -> 
+    R xs ->
       case typ of
         VRecType ys -> do case [l | (l,_) <- ys, isNothing (lookup l xs)] of
                             [] -> return ()
@@ -174,7 +175,7 @@ checkInferExp th tenv@(k,_,_) e typ = do
   (e',w,cs1) <- inferExp th tenv e
   cs2 <- eqVal k w typ
   return (e',cs1 ++ cs2)
-      
+
 inferExp :: Theory -> TCEnv -> Term -> Err (AExp, Val, [(Val,Val)])
 inferExp th tenv@(k,rho,gamma) e = case e of
    Vr x -> mkAnnot (AVr x) $ noConstr $ lookupVar gamma x
@@ -200,13 +201,13 @@ inferExp th tenv@(k,rho,gamma) e = case e of
     (e2,val2,cs2) <- inferExp th (k,rho,(x,val1):gamma) e2
     return (ALet (x,(val1,e1)) e2, val2, cs1++cs2)
    App f t -> do
-    (f',w,csf) <- inferExp th tenv f 
+    (f',w,csf) <- inferExp th tenv f
     typ <- whnf w
     case typ of
       VClos env (Prod _ x a b) -> do
         (a',csa) <- checkExp th tenv t (VClos env a)
-	b' <- whnf $ VClos ((x,VClos rho t):env) b
-	return $ (AApp f' a' b', b', csf ++ csa)
+        b' <- whnf $ VClos ((x,VClos rho t):env) b
+        return $ (AApp f' a' b', b', csf ++ csa)
       _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
    _ -> Bad (render ("cannot infer type of expression" <+> ppTerm Unqualified 0 e))
 
@@ -232,9 +233,9 @@ checkAssign th tenv@(k,rho,gamma) typs (lbl,(Nothing,exp)) = do
                    return ((lbl,(val,aexp)),cs)
 
 checkBranch :: Theory -> TCEnv -> Equation -> Val -> Err (([Term],AExp),[(Val,Val)])
-checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $ 
-                                  chB tenv' ps' ty 
- where 
+checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
+                                  chB tenv' ps' ty
+ where
 
   (ps',_,rho2,k') = ps2ts k ps
   tenv' = (k, rho2++rho, gamma) ---- k' ?
@@ -245,11 +246,11 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
       typ <- whnf ty
       case typ of
         VClos env (Prod _ y a b) -> do
-	  a' <- whnf $ VClos env a
+          a' <- whnf $ VClos env a
           (p', sigma, binds, cs1) <- checkP tenv p y a'
           let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
           ((ps',exp),cs2) <- chB tenv' ps2 (VClos ((y,p'):env) b)
-	  return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
+          return ((p:ps',exp), cs1 ++ cs2) -- don't change the patt
         _ -> Bad (render ("Product expected for definiens" <+> ppTerm Unqualified 0 t <+> "instead of" <+> ppValue Unqualified 0 typ))
     [] -> do
       (e,cs) <- checkExp th tenv t ty
@@ -259,15 +260,15 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
      let sigma = [(x, VGen i x) | ((x,_),i) <- zip delta [k..]]
      return (VClos sigma t, sigma, delta, cs)
 
-  ps2ts k = foldr p2t ([],0,[],k) 
+  ps2ts k = foldr p2t ([],0,[],k)
   p2t p (ps,i,g,k) = case p of
-     PW      -> (Meta i : ps, i+1,g,k) 
+     PW      -> (Meta i : ps, i+1,g,k)
      PV x    -> (Vr x   : ps, i, upd x k g,k+1)
      PAs x p -> p2t p (ps,i,g,k)
      PString s -> (K s : ps, i, g, k)
      PInt n -> (EInt n : ps, i, g, k)
      PFloat n -> (EFloat n : ps, i, g, k)
-     PP c xs -> (mkApp (Q c) xss : ps, j, g',k') 
+     PP c xs -> (mkApp (Q c) xss : ps, j, g',k')
                     where (xss,j,g',k') = foldr p2t ([],i,g,k) xs
      PImplArg p -> p2t p (ps,i,g,k)
      PTilde t -> (t : ps, i, g, k)
@@ -307,8 +308,8 @@ checkPatt th tenv exp val = do
        case typ of
          VClos env (Prod _ x a b) -> do
            (a',_,csa) <- checkExpP tenv t (VClos env a)
-	   b' <- whnf $ VClos ((x,VClos rho t):env) b
-	   return $ (AApp f' a' b', b', csf ++ csa)
+           b' <- whnf $ VClos ((x,VClos rho t):env) b
+           return $ (AApp f' a' b', b', csf ++ csa)
          _ -> Bad (render ("Prod expected for function" <+> ppTerm Unqualified 0 f <+> "instead of" <+> ppValue Unqualified 0 typ))
      _ -> Bad (render ("cannot typecheck pattern" <+> ppTerm Unqualified 0 exp))
 
@@ -321,4 +322,3 @@ mkAnnot :: (Val -> AExp) -> Err (Val,[(Val,Val)]) -> Err (AExp,Val,[(Val,Val)])
 mkAnnot a ti = do
   (v,cs) <- ti
   return (a v, v, cs)
-
diff --git a/src/compiler/GF/Compile/Update.hs b/src/compiler/GF/Compile/Update.hs
index 4399405b8..7bbe1d8dc 100644
--- a/src/compiler/GF/Compile/Update.hs
+++ b/src/compiler/GF/Compile/Update.hs
@@ -5,7 +5,7 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/05/30 18:39:44 $ 
+-- > CVS $Date: 2005/05/30 18:39:44 $
 -- > CVS $Author: aarne $
 -- > CVS $Revision: 1.8 $
 --
@@ -34,14 +34,14 @@ buildAnyTree :: Fail.MonadFail m => ModuleName -> [(Ident,Info)] -> m (Map.Map I
 buildAnyTree m = go Map.empty
   where
     go map []         = return map
-    go map ((c,j):is) = do
+    go map ((c,j):is) =
       case Map.lookup c map of
         Just i  -> case unifyAnyInfo m i j of
-		     Ok k  -> go (Map.insert c k map) is
-		     Bad _ -> fail $ render ("conflicting information in module"<+>m $$
-		                             nest 4 (ppJudgement Qualified (c,i)) $$
-		                             "and" $+$
-		                             nest 4 (ppJudgement Qualified (c,j)))
+          Ok k  -> go (Map.insert c k map) is
+          Bad _ -> fail $ render ("conflicting information in module"<+>m $$
+                                  nest 4 (ppJudgement Qualified (c,i)) $$
+                                  "and" $+$
+                                  nest 4 (ppJudgement Qualified (c,j)))
         Nothing -> go (Map.insert c j map) is
 
 extendModule :: FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
@@ -51,14 +51,14 @@ extendModule cwd gr (name,m)
   ---- Should be replaced by real control. AR 4/2/2005
   | mstatus m == MSIncomplete && isModCnc m = return (name,m)
   | otherwise                               = checkInModule cwd m NoLoc empty $ do
-                                                 m' <- foldM extOne m (mextend m) 
+                                                 m' <- foldM extOne m (mextend m)
                                                  return (name,m')
  where
    extOne mo (n,cond) = do
      m0 <- lookupModule gr n
 
      -- test that the module types match, and find out if the old is complete
-     unless (sameMType (mtype m) (mtype mo)) 
+     unless (sameMType (mtype m) (mtype mo))
             (checkError ("illegal extension type to module" <+> name))
 
      let isCompl = isCompleteModule m0
@@ -67,7 +67,7 @@ extendModule cwd gr (name,m)
      js1 <- extendMod gr isCompl ((n,m0), isInherited cond) name (jments mo)
 
      -- if incomplete, throw away extension information
-     return $ 
+     return $
           if isCompl
             then mo {jments = js1}
             else mo {mextend= filter ((/=n) . fst) (mextend mo)
@@ -75,7 +75,7 @@ extendModule cwd gr (name,m)
                     ,jments = js1
                     }
 
--- | rebuilding instance + interface, and "with" modules, prior to renaming. 
+-- | rebuilding instance + interface, and "with" modules, prior to renaming.
 -- AR 24/10/2003
 rebuildModule :: FilePath -> SourceGrammar -> SourceModule -> Check SourceModule
 rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js_)) =
@@ -88,8 +88,8 @@ rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js
 
     -- add the information given in interface into an instance module
     Nothing -> do
-      unless (null is || mstatus mi == MSIncomplete) 
-             (checkError ("module" <+> i <+> 
+      unless (null is || mstatus mi == MSIncomplete)
+             (checkError ("module" <+> i <+>
                           "has open interfaces and must therefore be declared incomplete"))
       case mt of
         MTInstance (i0,mincl) -> do
@@ -113,7 +113,7 @@ rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js
       let stat' = if all (flip elem infs) is
                     then MSComplete
                     else MSIncomplete
-      unless (stat' == MSComplete || stat == MSIncomplete) 
+      unless (stat' == MSComplete || stat == MSIncomplete)
              (checkError ("module" <+> i <+> "remains incomplete"))
       ModInfo mt0 _ fs me' _ ops0 _ fpath _ js <- lookupModule gr ext
       let ops1 = nub $
@@ -141,24 +141,24 @@ rebuildModule cwd gr mo@(i,mi@(ModInfo mt stat fs_ me mw ops_ med_ msrc_ env_ js
 extendMod :: Grammar ->
              Bool -> (Module,Ident -> Bool) -> ModuleName ->
              Map.Map Ident Info -> Check (Map.Map Ident Info)
-extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jments mi) 
+extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jments mi)
   where
     try new (c,i0)
       | not (cond c) = return new
       | otherwise    = case Map.lookup c new of
                          Just j -> case unifyAnyInfo name i j of
-		                     Ok k  -> return $ Map.insert c k new
-		                     Bad _ -> do (base,j) <- case j of 
-		                                               AnyInd _ m -> lookupOrigInfo gr (m,c)
-		                                               _          -> return (base,j)
-		                                 (name,i) <- case i of 
+                                     Ok k  -> return $ Map.insert c k new
+                                     Bad _ -> do (base,j) <- case j of
+                                                               AnyInd _ m -> lookupOrigInfo gr (m,c)
+                                                               _          -> return (base,j)
+                                                 (name,i) <- case i of
                                                                AnyInd _ m -> lookupOrigInfo gr (m,c)
                                                                _          -> return (name,i)
-		                                 checkError ("cannot unify the information" $$ 
-		                                             nest 4 (ppJudgement Qualified (c,i)) $$
-		                                             "in module" <+> name <+> "with" $$
-		                                             nest 4 (ppJudgement Qualified (c,j)) $$
-		                                             "in module" <+> base)
+                                                 checkError ("cannot unify the information" $$
+                                                             nest 4 (ppJudgement Qualified (c,i)) $$
+                                                             "in module" <+> name <+> "with" $$
+                                                             nest 4 (ppJudgement Qualified (c,j)) $$
+                                                             "in module" <+> base)
                          Nothing-> if isCompl
                                      then return $ Map.insert c (indirInfo name i) new
                                      else return $ Map.insert c i new
@@ -166,11 +166,11 @@ extendMod gr isCompl ((name,mi),cond) base new = foldM try new $ Map.toList (jme
         i = globalizeLoc (msrc mi) i0
 
     indirInfo :: ModuleName -> Info -> Info
-    indirInfo n info = AnyInd b n' where 
+    indirInfo n info = AnyInd b n' where
       (b,n') = case info of
         ResValue _ -> (True,n)
         ResParam _ _ -> (True,n)
-        AbsFun _ _ Nothing _ -> (True,n) 
+        AbsFun _ _ Nothing _ -> (True,n)
         AnyInd b k -> (b,k)
         _ -> (False,n) ---- canonical in Abs
 
@@ -194,24 +194,24 @@ globalizeLoc fpath i =
 
 unifyAnyInfo :: ModuleName -> Info -> Info -> Err Info
 unifyAnyInfo m i j = case (i,j) of
-  (AbsCat mc1, AbsCat mc2) -> 
+  (AbsCat mc1, AbsCat mc2) ->
     liftM AbsCat (unifyMaybeL mc1 mc2)
-  (AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) -> 
+  (AbsFun mt1 ma1 md1 moper1, AbsFun mt2 ma2 md2 moper2) ->
     liftM4 AbsFun (unifyMaybeL mt1 mt2) (unifAbsArrity ma1 ma2) (unifAbsDefs md1 md2) (unifyMaybe moper1 moper2) -- adding defs
 
   (ResParam mt1 mv1, ResParam mt2 mv2) ->
     liftM2 ResParam (unifyMaybeL mt1 mt2) (unifyMaybe mv1 mv2)
-  (ResValue (L l1 t1), ResValue (L l2 t2)) 
+  (ResValue (L l1 t1), ResValue (L l2 t2))
       | t1==t2    -> return (ResValue (L l1 t1))
       | otherwise -> fail ""
   (_, ResOverload ms t) | elem m ms ->
     return $ ResOverload ms t
-  (ResOper mt1 m1, ResOper mt2 m2) -> 
+  (ResOper mt1 m1, ResOper mt2 m2) ->
     liftM2 ResOper (unifyMaybeL mt1 mt2) (unifyMaybeL m1 m2)
 
-  (CncCat mc1 md1 mr1 mp1 mpmcfg1, CncCat mc2 md2 mr2 mp2 mpmcfg2) -> 
+  (CncCat mc1 md1 mr1 mp1 mpmcfg1, CncCat mc2 md2 mr2 mp2 mpmcfg2) ->
     liftM5 CncCat (unifyMaybeL mc1 mc2) (unifyMaybeL md1 md2) (unifyMaybeL mr1 mr2) (unifyMaybeL mp1 mp2)  (unifyMaybe mpmcfg1 mpmcfg2)
-  (CncFun m mt1 md1 mpmcfg1, CncFun _ mt2 md2 mpmcfg2) -> 
+  (CncFun m mt1 md1 mpmcfg1, CncFun _ mt2 md2 mpmcfg2) ->
     liftM3 (CncFun m) (unifyMaybeL mt1 mt2) (unifyMaybeL md1 md2) (unifyMaybe mpmcfg1 mpmcfg2)
 
   (AnyInd b1 m1, AnyInd b2 m2) -> do