diff --git a/.gitignore b/.gitignore
index aedc1fd42..678397df2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -56,6 +56,12 @@ DATA_DIR
 
 stack*.yaml.lock
 
+# Generated source files
+src/compiler/api/GF/Grammar/Lexer.hs
+src/compiler/api/GF/Grammar/Parser.hs
+src/compiler/api/PackageInfo_gf.hs
+src/compiler/api/Paths_gf.hs
+
 # Output files for test suite
 *.out
 gf-tests.html
diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs
index 7d7d65c7a..24b92244b 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs
@@ -1,11 +1,13 @@
-{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification #-}
+{-# LANGUAGE RankNTypes, BangPatterns, CPP, ExistentialQuantification, LambdaCase #-}
 
 -- | Functions for computing the values of terms in the concrete syntax, in
 -- | preparation for PMCFG generation.
 module GF.Compile.Compute.Concrete
            ( normalForm, normalFlatForm, normalStringForm
            , Value(..), Thunk, ThunkState(..), Env, Scope, showValue
-           , MetaThunks, Constraint, Globals(..), ConstValue(..)
+           , PredefImpl, Predef(..), PredefCombinator, ($\)
+           , pdForce, pdClosedArgs, pdArity, pdStandard
+           , MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..)
            , EvalM(..), runEvalM, runEvalOneM, reset, evalError, evalWarn
            , eval, apply, force, value2term, patternMatch, stdPredef
            , unsafeIOToEvalM
@@ -26,6 +28,7 @@ import GF.Grammar.Predef
 import GF.Grammar.Lockfield(lockLabel)
 import GF.Grammar.Printer
 import GF.Data.Operations(Err(..))
+import GF.Data.Utilities(splitAt',(<||>),anyM)
 import GF.Infra.CheckM
 import GF.Infra.Option
 import Data.STRef
@@ -142,6 +145,37 @@ showValue (VAlts _ _) = "VAlts"
 showValue (VStrs _) = "VStrs"
 showValue (VSymCat _ _ _) = "VSymCat"
 
+isOpen :: [Ident] -> Term -> EvalM s Bool
+isOpen bound (Vr x) = return $ x `notElem` bound
+isOpen bound (App f x) = isOpen bound f <||> isOpen bound x
+isOpen bound (Abs b x t) = isOpen (x:bound) t
+isOpen bound (ImplArg t) = isOpen bound t
+isOpen bound (Prod b x d cod) = isOpen bound d <||> isOpen (x:bound) cod
+isOpen bound (Typed t ty) = isOpen bound t
+isOpen bound (Example t s) = isOpen bound t
+isOpen bound (RecType fs) = anyM (isOpen bound . snd) fs
+isOpen bound (R fs) = anyM (isOpen bound . snd . snd) fs
+isOpen bound (P t f) = isOpen bound t
+isOpen bound (ExtR t t') = isOpen bound t <||> isOpen bound t'
+isOpen bound (Table d cod) = isOpen bound d <||> isOpen bound cod
+isOpen bound (T (TTyped ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs
+isOpen bound (T (TWild ty) cs) = isOpen bound ty <||> anyM (isOpen bound . snd) cs
+isOpen bound (T _ cs) = anyM (isOpen bound . snd) cs
+isOpen bound (V ty cs) = isOpen bound ty <||> anyM (isOpen bound) cs
+isOpen bound (S t x) = isOpen bound t <||> isOpen bound x
+isOpen bound (Let (x,(ty,d)) t) = isOpen bound d <||> isOpen (x:bound) t
+isOpen bound (C t t') = isOpen bound t <||> isOpen bound t'
+isOpen bound (Glue t t') = isOpen bound t <||> isOpen bound t'
+isOpen bound (EPattType ty) = isOpen bound ty
+isOpen bound (ELincat c ty) = isOpen bound ty
+isOpen bound (ELin c t) = isOpen bound t
+isOpen bound (FV ts) = anyM (isOpen bound) ts
+isOpen bound (Markup tag as ts) = anyM (isOpen bound) ts <||> anyM (isOpen bound . snd) as
+isOpen bound (Reset c t) = isOpen bound t
+isOpen bound (Alts d as) = isOpen bound d <||> anyM (\(x,y) -> isOpen bound x <||> isOpen bound y) as
+isOpen bound (Strs ts) = anyM (isOpen bound) ts
+isOpen _ _ = return False
+
 eval env (Vr x)         vs  = do (tnk,depth) <- lookup x env
                                  withVar depth $ do
                                    v <- force tnk
@@ -206,9 +240,8 @@ eval env (S t1 t2)      vs  = do v1   <- eval env t1 []
                                    v1           -> return v0
 eval env (Let (x,(_,t1)) t2) vs = do tnk <- newThunk env t1
                                      eval ((x,tnk):env) t2 vs
-eval env (Q q@(m,id))   vs
-  | m == cPredef            = do vs' <- mapM force vs
-                                 res <- evalPredef id vs'
+eval env t@(Q q@(m,id)) vs
+  | m == cPredef            = do res <- evalPredef env t id vs
                                  case res of
                                    Const res -> return res
                                    RunTime   -> return (VApp q vs)
@@ -292,25 +325,25 @@ apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs
 apply v                             []  = return v
 
 
-stdPredef :: Map.Map Ident ([Value s] -> EvalM s (ConstValue (Value s)))
+stdPredef :: PredefTable s
 stdPredef = Map.fromList
-  [(cLength, \[v] -> case value2string v of
-                       Const s -> return (Const (VInt (genericLength s)))
-                       _       -> return RunTime)
-  ,(cTake,   \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2))))
-  ,(cDrop,   \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2))))
-  ,(cTk,     \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2))))
-  ,(cDp,     \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2))))
-  ,(cIsUpper,\[v]     -> return (fmap toPBool (liftA (all isUpper) (value2string v))))
-  ,(cToUpper,\[v]     -> return (fmap string2value (liftA (map toUpper) (value2string v))))
-  ,(cToLower,\[v]     -> return (fmap string2value (liftA (map toLower) (value2string v))))
-  ,(cEqStr,  \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2))))
-  ,(cOccur,  \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2))))
-  ,(cOccurs, \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2))))
-  ,(cEqInt,  \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2))))
-  ,(cLessInt,\[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2))))
-  ,(cPlus,   \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2))))
-  ,(cError,  \[v]     -> case value2string v of
+  [(cLength, pdStandard 1 $\ \[v] -> case value2string v of
+                                       Const s -> return (Const (VInt (genericLength s)))
+                                       _       -> return RunTime)
+  ,(cTake,   pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTake (value2int v1) (value2string v2))))
+  ,(cDrop,   pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDrop (value2int v1) (value2string v2))))
+  ,(cTk,     pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericTk (value2int v1) (value2string v2))))
+  ,(cDp,     pdStandard 2 $\ \[v1,v2] -> return (fmap string2value (liftA2 genericDp (value2int v1) (value2string v2))))
+  ,(cIsUpper,pdStandard 1 $\ \[v]     -> return (fmap toPBool (liftA (all isUpper) (value2string v))))
+  ,(cToUpper,pdStandard 1 $\ \[v]     -> return (fmap string2value (liftA (map toUpper) (value2string v))))
+  ,(cToLower,pdStandard 1 $\ \[v]     -> return (fmap string2value (liftA (map toLower) (value2string v))))
+  ,(cEqStr,  pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2string v1) (value2string v2))))
+  ,(cOccur,  pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occur (value2string v1) (value2string v2))))
+  ,(cOccurs, pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 occurs (value2string v1) (value2string v2))))
+  ,(cEqInt,  pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (==) (value2int v1) (value2int v2))))
+  ,(cLessInt,pdStandard 2 $\ \[v1,v2] -> return (fmap toPBool (liftA2 (<) (value2int v1) (value2int v2))))
+  ,(cPlus,   pdStandard 2 $\ \[v1,v2] -> return (fmap VInt (liftA2 (+) (value2int v1) (value2int v2))))
+  ,(cError,  pdStandard 1 $\ \[v]     -> case value2string v of
                            Const msg -> fail msg
                            _         -> fail "Indescribable error appeared")
   ]
@@ -671,6 +704,16 @@ instance Applicative ConstValue where
   liftA2 f _         RunTime   = RunTime
 #endif
 
+instance Foldable ConstValue where
+  foldr f a (Const x) = f x a
+  foldr f a RunTime   = a
+  foldr f a NonExist  = a
+
+instance Traversable ConstValue where
+  traverse f (Const x) = Const <$> f x
+  traverse f RunTime   = pure RunTime
+  traverse f NonExist  = pure NonExist
+
 value2string v = fmap (\(_,ws,_) -> unwords ws) (value2string' v False [] [])
 
 value2string' (VStr w1)   True (w2:ws) qs = Const (False,(w1++w2):ws,qs)
@@ -728,12 +771,63 @@ string2value' (w:ws) = VC (VStr w) (string2value' ws)
 value2int (VInt n) = Const n
 value2int _        = RunTime
 
+-----------------------------------------------------------------------
+-- * Global/built-in definitions
+
+type PredefImpl a s = [a] -> EvalM s (ConstValue (Value s))
+newtype Predef a s = Predef { runPredef :: Term -> Env s -> PredefImpl a s }
+type PredefCombinator a b s = Predef a s -> Predef b s
+
+infix 0 $\\
+
+($\) :: PredefCombinator a b s -> PredefImpl a s -> Predef b s
+k $\ f = k (Predef (\_ _ -> f))
+
+pdForce :: PredefCombinator (Value s) (Thunk s) s
+pdForce def = Predef $ \h env args -> do
+  argValues <- mapM force args
+  runPredef def h env argValues
+
+pdClosedArgs :: PredefCombinator (Value s) (Value s) s
+pdClosedArgs def = Predef $ \h env args -> do
+  open <- anyM (value2term True [] >=> isOpen []) args
+  if open then return RunTime else runPredef def h env args
+
+pdArity :: Int -> PredefCombinator (Thunk s) (Thunk s) s
+pdArity n def = Predef $ \h env args ->
+  case splitAt' n args of
+    Nothing -> do
+      t <- papply env h args
+      let t' = abstract 0 (n - length args) t
+      Const <$> eval env t' []
+    Just (usedArgs, remArgs) -> do
+      res <- runPredef def h env usedArgs
+      forM res $ \v -> case remArgs of
+        [] -> return v
+        _  -> do
+          t <- value2term False (fst <$> env) v
+          eval env t remArgs
+  where
+    papply env t []         = return t
+    papply env t (arg:args) = do
+      arg <- tnk2term False (fst <$> env) arg
+      papply env (App t arg) args
+    
+    abstract i n t
+      | n <= 0    = t
+      | otherwise = let x = identV (rawIdentS "a") i
+                    in  Abs Explicit x (abstract (i + 1) (n - 1) (App t (Vr x)))
+
+pdStandard :: Int -> PredefCombinator (Value s) (Thunk s) s
+pdStandard n = pdArity n . pdForce . pdClosedArgs
+
 -----------------------------------------------------------------------
 -- * Evaluation monad
 
 type MetaThunks s = Map.Map MetaId (Thunk s)
 type Cont s r = MetaThunks s -> Int -> r -> [Message] -> ST s (CheckResult r [Message])
-data Globals = Gl Grammar (forall s . Map.Map Ident ([Value s] -> EvalM s (ConstValue (Value s))))
+type PredefTable s = Map.Map Ident (Predef (Thunk s) s)
+data Globals = Gl Grammar (forall s . PredefTable s)
 newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> Cont s r)
 
 instance Functor (EvalM s) where
@@ -792,9 +886,9 @@ evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs))
 evalWarn :: Message -> EvalM s ()
 evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs))
 
-evalPredef :: Ident -> [Value s] -> EvalM s (ConstValue (Value s))
-evalPredef id vs = EvalM (\globals@(Gl _ predef) k mt d r msgs ->
-  case fmap (\f -> f vs) (Map.lookup id predef) of
+evalPredef :: Env s -> Term -> Ident -> [Thunk s] -> EvalM s (ConstValue (Value s))
+evalPredef env h id args = EvalM (\globals@(Gl _ predef) k mt d r msgs ->
+  case fmap (\def -> runPredef def h env args) (Map.lookup id predef) of
     Just (EvalM f) -> f globals k mt d r msgs
     Nothing        -> k RunTime mt d r msgs)
 
diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs
new file mode 100644
index 000000000..f3b748361
--- /dev/null
+++ b/src/compiler/api/GF/Compile/Repl.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE LambdaCase #-}
+
+module GF.Compile.Repl (ReplOpts(..), defaultReplOpts, replOptDescrs, getReplOpts, runRepl, runRepl') where
+
+import Control.Monad (unless, forM_, foldM)
+import Control.Monad.IO.Class (MonadIO)
+import qualified Data.ByteString.Char8 as BS
+import Data.Char (isSpace)
+import Data.Function ((&))
+import Data.Functor ((<&>))
+import qualified Data.Map as Map
+
+import System.Console.GetOpt (ArgOrder(RequireOrder), OptDescr(..), ArgDescr(..), getOpt, usageInfo)
+import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT, getInputLine, outputStrLn)
+import System.Directory (getAppUserDataDirectory)
+
+import GF.Compile (batchCompile)
+import GF.Compile.Compute.Concrete (Globals(Gl), stdPredef, normalFlatForm)
+import GF.Compile.Rename (renameSourceTerm)
+import GF.Compile.TypeCheck.ConcreteNew (inferLType)
+import GF.Data.ErrM (Err(..))
+import GF.Grammar.Grammar
+  ( Grammar
+  , mGrammar
+  , Info
+  , Module
+  , ModuleName
+  , ModuleInfo(..)
+  , ModuleType(MTResource)
+  , ModuleStatus(MSComplete)
+  , OpenSpec(OSimple)
+  , Location (NoLoc)
+  , Term
+  , prependModule
+  )
+import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP)
+import GF.Grammar.Parser (pTerm)
+import GF.Grammar.Printer (TermPrintQual(Unqualified), ppTerm)
+import GF.Infra.CheckM (Check, runCheck)
+import GF.Infra.Ident (moduleNameS)
+import GF.Infra.Option (noOptions)
+import GF.Infra.UseIO (justModuleName)
+import GF.Text.Pretty (render)
+
+data ReplOpts = ReplOpts
+  { noPrelude :: Bool
+  , inputFiles :: [String]
+  }
+
+defaultReplOpts :: ReplOpts
+defaultReplOpts = ReplOpts False []
+
+type Errs a = Either [String] a
+type ReplOptsOp = ReplOpts -> Errs ReplOpts
+
+replOptDescrs :: [OptDescr ReplOptsOp]
+replOptDescrs =
+  [ Option ['h'] ["help"] (NoArg $ \o -> Left [usageInfo "gfci" replOptDescrs]) "Display help."
+  , Option [] ["no-prelude"] (flag $ \o -> o { noPrelude = True }) "Don't load the prelude."
+  ]
+  where
+    flag f = NoArg $ \o -> pure (f o)
+
+getReplOpts :: [String] -> Errs ReplOpts
+getReplOpts args = case errs of
+  [] -> foldM (&) defaultReplOpts flags <&> \o -> o { inputFiles = inputFiles }
+  _  -> Left errs
+  where
+    (flags, inputFiles, errs) = getOpt RequireOrder replOptDescrs args
+
+execCheck :: MonadIO m => Check a -> (a -> InputT m ()) -> InputT m ()
+execCheck c k = case runCheck c of
+  Ok (a, warn) -> do
+    unless (null warn) $ outputStrLn warn
+    k a
+  Bad err -> outputStrLn err
+
+replModNameStr :: String
+replModNameStr = "<repl>"
+
+replModName :: ModuleName
+replModName = moduleNameS replModNameStr
+
+parseThen :: MonadIO m => Grammar -> String -> (Term -> InputT m ()) -> InputT m ()
+parseThen g s k = case runLangP GF pTerm (BS.pack s) of
+  Left (Pn l c, err) -> outputStrLn $ err ++ " (" ++ show l ++ ":" ++ show c ++ ")"
+  Right t -> execCheck (renameSourceTerm g replModName t) $ \t -> k t
+
+runRepl' :: Globals -> IO ()
+runRepl' gl@(Gl g _) = do
+  historyFile <- getAppUserDataDirectory "gfci_history"
+  runInputT (Settings noCompletion (Just historyFile) True) repl -- TODO tab completion
+  where
+    repl = do
+      getInputLine "gfci> " >>= \case
+        Nothing -> repl
+        Just (':' : l) -> let (cmd, arg) = break isSpace l in command cmd (dropWhile isSpace arg)
+        Just code -> evalPrintLoop code
+
+    command "t" arg = do
+      parseThen g arg $ \main ->
+        execCheck (inferLType gl main) $ \(_, ty) ->
+          outputStrLn $ render (ppTerm Unqualified 0 ty)
+      outputStrLn "" >> repl
+    
+    command "q" _ = outputStrLn "Bye!"
+
+    command cmd _ = do
+      outputStrLn $ "Unknown REPL command: " ++ cmd
+      outputStrLn "" >> repl
+
+    evalPrintLoop code = do -- TODO bindings
+      parseThen g code $ \main ->
+        execCheck (inferLType gl main >>= \(t, _) -> normalFlatForm gl t) $ \nfs ->
+          forM_ (zip [1..] nfs) $ \(i, nf) ->
+            outputStrLn $ show i ++ ". " ++ render (ppTerm Unqualified 0 nf)
+      outputStrLn "" >> repl
+
+runRepl :: ReplOpts -> IO ()
+runRepl (ReplOpts noPrelude inputFiles) = do
+  -- TODO accept an ngf grammar
+  let toLoad = if noPrelude then inputFiles else "prelude/Predef.gfo" : inputFiles
+  (g0, opens) <- case toLoad of
+    [] -> pure (mGrammar [], [])
+    _ -> do
+      (_, (_, g0)) <- batchCompile noOptions Nothing toLoad
+      pure (g0, OSimple . moduleNameS . justModuleName <$> toLoad)
+  let
+    modInfo = ModInfo
+      { mtype   = MTResource
+      , mstatus = MSComplete
+      , mflags  = noOptions
+      , mextend = []
+      , mwith   = Nothing
+      , mopens  = opens
+      , mexdeps = []
+      , msrc    = replModNameStr
+      , mseqs   = Nothing
+      , jments  = Map.empty
+      }
+  runRepl' (Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef))
diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
index a314aed49..f4ceef45d 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -1,5 +1,5 @@
-{-# LANGUAGE RankNTypes, CPP #-}
-module GF.Compile.TypeCheck.ConcreteNew( checkLType, inferLType ) where
+{-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-}
+module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where
 
 -- The code here is based on the paper:
 -- Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich.
@@ -12,26 +12,33 @@ import GF.Grammar.Predef
 import GF.Grammar.Lockfield
 import GF.Compile.Compute.Concrete
 import GF.Infra.CheckM
-import GF.Data.Operations
+import GF.Data.ErrM ( Err(Ok, Bad) )
 import Control.Applicative(Applicative(..))
-import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM)
+import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless)
 import Control.Monad.ST
 import GF.Text.Pretty
 import Data.STRef
 import Data.List (nub, (\\), tails)
 import qualified Data.Map as Map
-import Data.Maybe(fromMaybe,isNothing)
+import Data.Maybe(fromMaybe,isNothing,mapMaybe)
+import Data.Functor((<&>))
 import qualified Control.Monad.Fail as Fail
 
 checkLType :: Globals -> Term -> Type -> Check (Term, Type)
-checkLType globals t ty = runEvalOneM globals $ do
+checkLType globals t ty = runEvalOneM globals (checkLType' t ty)
+
+checkLType' :: Term -> Type -> EvalM s (Term, Type)
+checkLType' t ty = do
   vty <- eval [] ty []
   (t,_) <- tcRho [] t (Just vty)
   t <- zonkTerm [] t
   return (t,ty)
 
 inferLType :: Globals -> Term -> Check (Term, Type)
-inferLType globals t = runEvalOneM globals $ do
+inferLType globals t = runEvalOneM globals (inferLType' t)
+
+inferLType' :: Term -> EvalM s (Term, Type)
+inferLType' t = do
   (t,ty) <- inferSigma [] t
   t  <- zonkTerm [] t
   ty <- value2term False [] ty
@@ -64,13 +71,13 @@ tcRho scope t@(Vr v)     mb_ty = do                          -- VAR
     Just v_sigma -> instSigma scope t v_sigma mb_ty
     Nothing      -> evalError ("Unknown variable" <+> v)
 tcRho scope t@(Q id)     mb_ty = do
-  (t,ty) <- tcApp scope t t
+  (t,ty) <- tcApp scope t t []
   instSigma scope t ty mb_ty
 tcRho scope t@(QC id)    mb_ty = do
-  (t,ty) <- tcApp scope t t
+  (t,ty) <- tcApp scope t t []
   instSigma scope t ty mb_ty
 tcRho scope t@(App fun arg) mb_ty = do
-  (t,ty) <- tcApp scope t t
+  (t,ty) <- tcApp scope t t []
   instSigma scope t ty mb_ty
 tcRho scope (Abs bt var body) Nothing = do                   -- ABS1
   (i,tnk) <- newResiduation scope
@@ -105,7 +112,6 @@ tcRho scope (Abs bt var body) Nothing = do                   -- ABS1
                              v2 <- eval ((x,tnk):env) t []
                              check m (n+1) (b,x:xs) v2
         v2             -> check m n st v2
-      check m (n+1) (b,x:xs) v2
     check m n st (VRecType as)     = foldM (\st (l,v) -> check m n st v) st as
     check m n st (VR as)           =
       foldM (\st (lbl,tnk) -> follow m n st tnk) st as
@@ -148,19 +154,13 @@ tcRho scope t@(Abs Implicit var body) (Just ty) = do         -- ABS2
   if bt == Implicit
     then return ()
     else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
-  body_ty <- case body_ty of
-               VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) [])
-                                          eval ((x,tnk):env) body_ty []
-               body_ty              -> return body_ty
+  body_ty <- evalCodomain scope x body_ty
   (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
   return (Abs Implicit var body,ty)
 tcRho scope (Abs Explicit var body) (Just ty) = do           -- ABS3
   (scope,f,ty') <- skolemise scope ty
   (_,x,var_ty,body_ty) <- unifyFun scope ty'
-  body_ty <- case body_ty of
-               VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) [])
-                                          eval ((x,tnk):env) body_ty []
-               body_ty              -> return body_ty
+  body_ty <- evalCodomain scope x body_ty
   (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
   return (f (Abs Explicit var body),ty)
 tcRho scope (Meta _) mb_ty = do
@@ -369,6 +369,12 @@ tcRho scope (Reset c t) mb_ty = do
   instSigma scope (Reset c t) vtypeMarkup mb_ty
 tcRho scope t _ = unimplemented ("tcRho "++show t)
 
+evalCodomain :: Scope s -> Ident -> Value s -> EvalM s (Constraint s)
+evalCodomain scope x (VClosure env t) = do
+  tnk <- newEvaluatedThunk (VGen (length scope) [])
+  eval ((x,tnk):env) t []
+evalCodomain scope x t = return t
+
 tcCases scope []         p_ty res_ty = return []
 tcCases scope ((p,t):cs) p_ty res_ty = do
   scope' <- tcPatt scope p p_ty
@@ -376,21 +382,27 @@ tcCases scope ((p,t):cs) p_ty res_ty = do
   cs <- tcCases scope cs p_ty res_ty
   return ((p,t):cs)
 
-tcApp scope t0 t@(App fun (ImplArg arg)) = do                  -- APP1
-  (fun,fun_ty) <- tcApp scope t0 fun
+tcApp scope t0 (App fun arg) args = tcApp scope t0 fun (arg:args)     -- APP
+tcApp scope t0 (Q id)        args = resolveOverloads scope t0 id args -- VAR (global)
+tcApp scope t0 (QC id)       args = resolveOverloads scope t0 id args -- VAR (global)
+tcApp scope t0 t args = do
+  (t,ty) <- tcRho scope t Nothing
+  reapply scope t ty args
+
+reapply :: Scope s -> Term -> Constraint s -> [Term] -> EvalM s (Term,Rho s)
+reapply scope fun fun_ty [] = return (fun,fun_ty)
+reapply scope fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case
   (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty
-  if (bt == Implicit)
-    then return ()
-    else evalError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
+  unless (bt == Implicit) $ evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+>
+                              "is an implicit argument application, but no implicit argument is expected")
   (arg,_) <- tcRho scope arg (Just arg_ty)
   res_ty <- case res_ty of
               VClosure res_env res_ty -> do env <- scopeEnv scope
                                             tnk <- newThunk env arg
                                             eval ((x,tnk):res_env) res_ty []
-              res_ty              -> return res_ty
-  return (App fun (ImplArg arg), res_ty)
-tcApp scope t0 (App fun arg) = do                              -- APP2
-  (fun,fun_ty) <- tcApp scope t0 fun
+              res_ty                  -> return res_ty
+  reapply scope (App fun (ImplArg arg)) res_ty args
+reapply scope fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case
   (fun,fun_ty) <- instantiate scope fun fun_ty
   (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty
   (arg,_) <- tcRho scope arg (Just arg_ty)
@@ -399,22 +411,61 @@ tcApp scope t0 (App fun arg) = do                              -- APP2
                                             tnk <- newThunk env arg
                                             eval ((x,tnk):res_env) res_ty []
               res_ty                  -> return res_ty
-  return (App fun arg, res_ty)
-tcApp scope t0 (Q id)  = do                                    -- VAR (global)
-  (t,ty) <- getOverload t0 id
-  vty <- eval [] ty []
-  return (t,vty)
-tcApp scope t0 (QC id) = do                                    -- VAR (global)
-  (t,ty) <- getOverload t0 id
-  vty <- eval [] ty []
-  return (t,vty)
-tcApp scope t0 t = tcRho scope t Nothing
+  reapply scope (App fun arg) res_ty args
+
+resolveOverloads :: Scope s -> Term -> QIdent -> [Term] -> EvalM s (Term,Rho s)
+resolveOverloads scope t q args = EvalM $ \gl@(Gl gr _) k mt d r msgs ->
+  case lookupOverloadTypes gr q of
+    Bad msg  -> return $ Fail (pp msg) msgs
+    Ok [tty] -> try tty gl k mt d r msgs -- skip overload resolution if there's only one overload
+    Ok ttys  -> do rs <- mapM (\tty -> (tty,) <$> try tty gl k mt d r msgs) ttys
+                   let successes = mapMaybe isSuccess rs
+                   r <- case successes of
+                     []           -> return $ Fail mempty msgs
+                     [(_,r,msgs)] -> return $ Success r msgs
+                     _            -> case unifyOverloads (successes <&> \(tty,_,_) -> tty) of
+                                       EvalM f -> f gl k mt d r msgs
+                   return $ case r of
+                     s@(Success _ _) -> s
+                     Fail err msgs   -> let h = "Overload resolution failed" $$
+                                                "of term   " <+> pp t $$
+                                                "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]
+                                        in Fail (h $+$ err) msgs
+  where
+    try (t,ty) = case eval [] ty [] >>= \vty -> reapply scope t vty args of EvalM f -> f
+
+    isSuccess (tty, Success r msg) = Just (tty,r,msg)
+    isSuccess (_, Fail _ _)        = Nothing
 
-tcOverloadFailed t ttys =
-  evalError ("Overload resolution failed" $$
-             "of term   " <+> pp t $$
-             "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys])
+    unifyOverloads ttys = do
+      ttys <- forM ttys $ \(t,ty) -> do
+        vty <- eval [] ty []
+        (t,vty) <- papply scope t vty args
+        return (t,vty)
+      (_,tnk) <- newResiduation scope
+      let mv = VMeta tnk []
+      mapM_ (\(_,vty) -> unify scope vty mv) ttys
+      fvty <- force tnk
+      return (FV (fst <$> ttys), fvty)
 
+    papply scope fun fun_ty [] = return (fun,fun_ty)
+    papply scope fun (VProd Implicit x arg_ty res_ty) ((ImplArg arg):args) = do -- Implicit arg case
+      (arg,_) <- tcRho scope arg (Just arg_ty)
+      res_ty <- case res_ty of
+                  VClosure res_env res_ty -> do env <- scopeEnv scope
+                                                tnk <- newThunk env arg
+                                                eval ((x,tnk):res_env) res_ty []
+                  res_ty                  -> return res_ty
+      papply scope (App fun (ImplArg arg)) res_ty args
+    papply scope fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case
+      (fun,VProd Explicit x arg_ty res_ty) <- instantiate scope fun fun_ty
+      (arg,_) <- tcRho scope arg (Just arg_ty)
+      res_ty <- case res_ty of
+                  VClosure res_env res_ty -> do env <- scopeEnv scope
+                                                tnk <- newThunk env arg
+                                                eval ((x,tnk):res_env) res_ty []
+                  res_ty                  -> return res_ty
+      papply scope (App fun arg) res_ty args
 
 tcPatt scope PW        ty0 =
   return scope
@@ -581,10 +632,7 @@ subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do     -- Rule SPEC
   subsCheckRho scope (App t (ImplArg (Meta i))) ty2 rho2
 subsCheckRho scope t rho1 (VProd Implicit x ty1 ty2) = do     -- Rule SKOL
   let v = newVar scope
-  ty2 <- case ty2 of
-           VClosure env ty2 -> do tnk <- newEvaluatedThunk (VGen (length scope) [])
-                                  eval ((x,tnk):env) ty2 []
-           ty2              -> return ty2
+  ty2 <- evalCodomain scope x ty2
   t <- subsCheckRho ((v,ty1):scope) t rho1 ty2
   return (Abs Implicit v t)
 subsCheckRho scope t rho1 (VProd Explicit _ a2 r2) = do       -- Rule FUN
@@ -779,6 +827,12 @@ unify scope (VMeta i vs) v = unifyVar scope i vs v
 unify scope v (VMeta i vs) = unifyVar scope i vs v
 unify scope (VGen i vs1)       (VGen j vs2)
   | i == j                     = sequence_ (zipWith (unifyThunk scope) vs1 vs2)
+unify scope (VProd b x d cod) (VProd b' x' d' cod')
+  | b == b'                    = do
+      unify scope d d'
+      cod <- evalCodomain scope x cod
+      cod' <- evalCodomain scope x' cod'
+      unify scope cod cod'
 unify scope (VTable p1 res1) (VTable p2 res2) = do
   unify scope p2   p1
   unify scope res1 res2
@@ -892,6 +946,10 @@ instantiate scope t (VProd Implicit x ty1 ty2) = do
            VClosure env ty2 -> eval ((x,tnk):env) ty2 []
            ty2              -> return ty2
   instantiate scope (App t (ImplArg (Meta i))) ty2
+instantiate scope t ty@(VMeta thk args) = getRef thk >>= \case
+  Evaluated _ v            -> instantiate scope t v
+  Residuation _ _ (Just v) -> instantiate scope t v
+  _                        -> return (t,ty) -- We don't have enough information to try any instantiation
 instantiate scope t ty = do
   return (t,ty)
 
@@ -905,10 +963,7 @@ skolemise scope ty@(VMeta i vs) = do
                             skolemise scope ty
 skolemise scope (VProd Implicit x ty1 ty2) = do
   let v = newVar scope
-  ty2 <- case ty2 of
-           VClosure env ty2 -> do tnk <- newEvaluatedThunk (VGen (length scope) [])
-                                  eval ((x,tnk) : env) ty2 []
-           ty2              -> return ty2
+  ty2 <- evalCodomain scope x ty2
   (scope,f,ty2) <- skolemise ((v,ty1):scope) ty2
   return (scope,Abs Implicit v . f,ty2)
 skolemise scope ty = do
@@ -1070,9 +1125,10 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys
       | m `elem` acc         = return acc
       | otherwise            = do res <- getRef m
                                   case res of
-                                    Evaluated _ v           -> go v acc
-                                    Residuation _ _ Nothing -> foldM follow (m:acc) args
-                                    _                       -> return acc
+                                    Evaluated _ v            -> go v acc
+                                    Residuation _ _ Nothing  -> foldM follow (m:acc) args
+                                    Residuation _ _ (Just v) -> go v acc
+                                    _                        -> return acc
     go (VApp f args)     acc = foldM follow acc args
     go v                 acc = unimplemented ("go "++showValue v)
 
diff --git a/src/compiler/api/GF/Data/Utilities.hs b/src/compiler/api/GF/Data/Utilities.hs
index 913953b6e..5b3c99a2d 100644
--- a/src/compiler/api/GF/Data/Utilities.hs
+++ b/src/compiler/api/GF/Data/Utilities.hs
@@ -14,9 +14,10 @@
 
 module GF.Data.Utilities(module GF.Data.Utilities) where
 
+import Data.Bifunctor (first)
 import Data.Maybe
 import Data.List
-import Control.Monad (MonadPlus(..),liftM,when)
+import Control.Monad (MonadPlus(..),foldM,liftM,when)
 import qualified Data.Set as Set
 
 -- * functions on lists
@@ -45,6 +46,14 @@ splitBy p [] = ([], [])
 splitBy p (a : as) = if p a then (a:xs, ys) else (xs, a:ys)
     where (xs, ys) = splitBy p as
 
+splitAt' :: Int -> [a] -> Maybe ([a], [a])
+splitAt' n xs
+    | n <= 0    = Just ([], xs)
+    | otherwise = helper n xs
+    where helper 0 xs     = Just ([], xs)
+          helper n []     = Nothing
+          helper n (x:xs) = first (x:) <$> helper (n - 1) xs
+
 foldMerge :: (a -> a -> a) -> a -> [a] -> a
 foldMerge merge zero = fm
     where fm [] = zero
@@ -140,6 +149,25 @@ whenM bm m = flip when m =<< bm
 
 repeatM m = whenM m (repeatM m)
 
+infixr 3 <&&>
+infixr 2 <||>
+
+-- | Boolean conjunction lifted to applicative functors.
+(<&&>) :: Applicative f => f Bool -> f Bool -> f Bool
+(<&&>) = liftA2 (&&)
+
+-- | Boolean disjunction lifted to applicative functors.
+(<||>) :: Applicative f => f Bool -> f Bool -> f Bool
+(<||>) = liftA2 (||)
+
+-- | Check whether a monadic predicate holds for every element of a collection.
+allM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool
+allM p = foldM (\b x -> if b then p x else return False) True
+
+-- | Check whether a monadic predicate holds for any element of a collection.
+anyM :: (Foldable f, Monad m) => (a -> m Bool) -> f a -> m Bool
+anyM p = foldM (\b x -> if b then return True else p x) False
+
 -- * functions on Maybes
 
 -- | Returns true if the argument is Nothing or Just []
diff --git a/src/compiler/api/GF/Interactive.hs b/src/compiler/api/GF/Interactive.hs
index 59d5df5b1..80e60ef8e 100644
--- a/src/compiler/api/GF/Interactive.hs
+++ b/src/compiler/api/GF/Interactive.hs
@@ -39,6 +39,7 @@ import qualified Data.Sequence as Seq
 import qualified Text.ParserCombinators.ReadP as RP
 import System.Directory(getAppUserDataDirectory)
 import Control.Exception(SomeException,fromException,evaluate,try)
+import Control.Monad ((<=<),when,mplus,join)
 import Control.Monad.State hiding (void)
 import qualified GF.System.Signal as IO(runInterruptibly)
 import GF.Command.Messages(welcome)
diff --git a/src/compiler/api/GF/Term.hs b/src/compiler/api/GF/Term.hs
index d9ffc9538..410360ea8 100644
--- a/src/compiler/api/GF/Term.hs
+++ b/src/compiler/api/GF/Term.hs
@@ -2,7 +2,7 @@ module GF.Term (renameSourceTerm,
                 Globals(..), ConstValue(..), EvalM, stdPredef,
                 Value(..), showValue, Thunk, newThunk, newEvaluatedThunk,
                 evalError, evalWarn,
-                inferLType, checkLType,
+                inferLType, inferLType', checkLType, checkLType',
                 normalForm, normalFlatForm, normalStringForm,
                 unsafeIOToEvalM, force
                ) where
diff --git a/src/compiler/gf-repl.hs b/src/compiler/gf-repl.hs
new file mode 100644
index 000000000..5b890fa9e
--- /dev/null
+++ b/src/compiler/gf-repl.hs
@@ -0,0 +1,12 @@
+import GHC.IO.Encoding (setLocaleEncoding, utf8)
+
+import System.Environment (getArgs)
+import GF.Compile.Repl (getReplOpts, runRepl)
+
+main :: IO ()
+main = do
+  setLocaleEncoding utf8
+  args <- getArgs
+  case getReplOpts args of
+    Left errs  -> mapM_ putStrLn errs
+    Right opts -> runRepl opts
diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal
index 6135755ab..cdd18f0a8 100644
--- a/src/compiler/gf.cabal
+++ b/src/compiler/gf.cabal
@@ -70,6 +70,8 @@ library
                  ghc-prim,
                  filepath, directory>=1.2, time,
                  process, haskeline, parallel>=3, json
+  build-tool-depends: alex:alex >= 3.2.4,
+                      happy:happy >= 1.19.9
   exposed-modules:
     GF.Interactive
     GF.Compiler
@@ -120,6 +122,7 @@ library
     GF.Grammar.CanonicalJSON
     GF.Compile.ReadFiles
     GF.Compile.Rename
+    GF.Compile.Repl
     GF.Compile.SubExOpt
     GF.Compile.Tags
     GF.Compile.ToAPI
@@ -200,7 +203,7 @@ library
   else
     build-depends:
       terminfo >=0.4.0 && < 0.5,
-      unix >= 2.7.2 && < 2.8
+      unix >= 2.7.2 && < 2.9
 
   if flag(server)
     build-depends:
@@ -237,6 +240,12 @@ executable gf
   build-depends: base >= 4.6 && <5, directory>=1.2, gf
   ghc-options: -threaded
 
+executable gfci
+  main-is: gf-repl.hs
+  default-language: Haskell2010
+  build-depends: base >= 4.6 && < 5, gf
+  ghc-options: -threaded
+
 test-suite gf-tests
   type: exitcode-stdio-1.0
   main-is: run.hs