diff --git a/src/compiler/api/GF/Compile/Compute/Concrete.hs b/src/compiler/api/GF/Compile/Compute/Concrete.hs
index 24b92244b..edb3d6721 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete.hs
@@ -8,7 +8,7 @@ module GF.Compile.Compute.Concrete
            , PredefImpl, Predef(..), PredefCombinator, ($\)
            , pdForce, pdClosedArgs, pdArity, pdStandard
            , MetaThunks, Constraint, PredefTable, Globals(..), ConstValue(..)
-           , EvalM(..), runEvalM, runEvalOneM, reset, evalError, evalWarn
+           , EvalM(..), runEvalM, runEvalOneM, reset, try, evalError, evalWarn
            , eval, apply, force, value2term, patternMatch, stdPredef
            , unsafeIOToEvalM
            , newThunk, newEvaluatedThunk
@@ -19,7 +19,6 @@ module GF.Compile.Compute.Concrete
            ) where
 
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
-
 import GF.Grammar hiding (Env, VGen, VApp, VRecType)
 import GF.Grammar.Lookup(lookupResDef,lookupResType,
                          lookupOrigInfo,lookupOverloadTypes,
@@ -117,7 +116,6 @@ data Value s
   | VCRecType [(Label, Bool, Constraint s)]
   | VCInts (Maybe Integer) (Maybe Integer)
 
-
 showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")"
 showValue (VMeta _ _) = "VMeta"
 showValue (VSusp _ _ _) = "VSusp"
@@ -504,30 +502,30 @@ vtableSelect v0 ty tnks tnk2 vs = do
                                      "cannot be evaluated at compile time.")
 
 
-susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
+susp i ki = EvalM $ \globals@(Gl gr _) k e mt d r msgs -> do
   s <- readSTRef i
   case s of
     Narrowing id (QC q) -> case lookupOrigInfo gr q of
-                             Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k mt d r msgs s m ps
+                             Ok (m,ResParam (Just (L _ ps)) _) -> bindParam globals k e mt d r msgs s m ps
                              Bad msg -> return (Fail (pp msg) msgs)
     Narrowing id ty
       | Just max <- isTypeInts ty
-                        -> bindInt globals k mt d r msgs s 0 max
+                        -> bindInt globals k e mt d r msgs s 0 max
     Evaluated _ v       -> case ki v of
-                             EvalM f -> f globals k mt d r msgs
+                             EvalM f -> f globals k e mt d r msgs
     _                   -> k (VSusp i ki []) mt d r msgs
   where
-    bindParam gr k mt d r msgs s m []             = return (Success r msgs)
-    bindParam gr k mt d r msgs s m ((p, ctxt):ps) = do
+    bindParam gr k e mt d r msgs s m []             = return (Success r msgs)
+    bindParam gr k e mt d r msgs s m ((p, ctxt):ps) = do
       (mt',tnks) <- mkArgs mt ctxt
       let v = VApp (m,p) tnks
       writeSTRef i (Evaluated 0 v)
       res <- case ki v of
-               EvalM f -> f gr k mt' d r msgs
+               EvalM f -> f gr k e mt' d r msgs
       writeSTRef i s
       case res of
         Fail msg  msgs -> return (Fail msg msgs)
-        Success r msgs -> bindParam gr k mt d r msgs s m ps
+        Success r msgs -> bindParam gr k e mt d r msgs s m ps
 
     mkArgs mt []              = return (mt,[])
     mkArgs mt ((_,_,ty):ctxt) = do
@@ -538,16 +536,16 @@ susp i ki = EvalM $ \globals@(Gl gr _) k mt d r msgs -> do
       (mt,tnks) <- mkArgs (Map.insert i tnk mt) ctxt
       return (mt,tnk:tnks)
 
-    bindInt gr k mt d r msgs s iv max
+    bindInt gr k e mt d r msgs s iv max
       | iv <= max = do
          let v = VInt iv
          writeSTRef i (Evaluated 0 v)
          res <- case ki v of
-                  EvalM f -> f gr k mt d r msgs
+                  EvalM f -> f gr k e mt d r msgs
          writeSTRef i s
          case res of
            Fail msg  msgs -> return (Fail msg msgs)
-           Success r msgs -> bindInt gr k mt d r msgs s (iv+1) max
+           Success r msgs -> bindInt gr k e mt d r msgs s (iv+1) max
       | otherwise = return (Success r msgs)
 
 
@@ -825,122 +823,122 @@ 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])
+type Do s r = [Message] -> ST s (CheckResult r [Message])
+type Cont s r = MetaThunks s -> Int -> r -> Do s r
 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)
+newtype EvalM s a = EvalM (forall r . Globals -> (a -> Cont s r) -> (Message -> Do s r) -> Cont s r)
 
 instance Functor (EvalM s) where
-  fmap f (EvalM g) = EvalM (\gr k -> g gr (k . f))
+  fmap f (EvalM g) = EvalM (\gr k e -> g gr (k . f) e)
 
 instance Applicative (EvalM s) where
-  pure x = EvalM (\gr k -> k x)
-  (EvalM f) <*> (EvalM x) = EvalM (\gr k -> f gr (\f -> x gr (\x -> k (f x))))
+  pure x = EvalM (\gr k e -> k x)
+  (EvalM f) <*> (EvalM x) = EvalM (\gr k e -> f gr (\f -> x gr (\x -> k (f x)) e) e)
 
 instance Monad (EvalM s) where
-  (EvalM f) >>= g = EvalM (\gr k -> f gr (\x -> case g x of
-                                                  EvalM g -> g gr k))
-#if !(MIN_VERSION_base(4,13,0))
-  -- Monad(fail) will be removed in GHC 8.8+
-  fail = Fail.fail
-#endif
+  (EvalM f) >>= g = EvalM (\gr k e -> f gr (\x -> case g x of
+                                                    EvalM g -> g gr k e) e)
 
 instance Fail.MonadFail (EvalM s) where
-  fail msg = EvalM (\gr k _ _ r msgs -> return (Fail (pp msg) msgs))
+  fail msg = EvalM (\gr k e _ _ r -> e (pp msg))
 
 instance Alternative (EvalM s) where
-  empty = EvalM (\gr k _ _ r msgs -> return (Success r msgs))
-  (EvalM f) <|> (EvalM g) = EvalM $ \gr k mt b r msgs -> do
-     res <- f gr k mt b r msgs
+  empty = EvalM (\gr k e _ _ r msgs -> return (Success r msgs))
+  (EvalM f) <|> (EvalM g) = EvalM $ \gr k e mt b r msgs -> do
+     res <- f gr k e mt b r msgs
      case res of
        Fail msg  msgs -> return (Fail msg msgs)
-       Success r msgs -> g gr k mt b r msgs
+       Success r msgs -> g gr k e mt b r msgs
 
 instance MonadPlus (EvalM s) where
 
 runEvalM :: Globals -> (forall s . EvalM s a) -> Check [a]
 runEvalM gr f = Check $ \(es,ws) ->
   case runST (case f of
-                EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
+                EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of
     Fail msg   ws -> Fail msg (es,ws)
     Success xs ws -> Success (reverse xs) (es,ws)
 
-runEvalOneM :: Globals -> (forall s . EvalM s a) -> Check a
+runEvalOneM :: Globals -> (forall s . EvalM s (Term,Type)) -> Check (Term,Type)
 runEvalOneM gr f = Check $ \(es,ws) ->
   case runST (case f of
-                EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) Map.empty maxBound [] ws) of
+                EvalM f -> f gr (\x mt _ xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) Map.empty maxBound [] ws) of
     Fail msg      ws -> Fail msg (es,ws)
     Success []    ws -> Fail (pp "The evaluation produced no results") (es,ws)
-    Success (x:_) ws -> Success x (es,ws)
+    Success xs ws -> Success (FV (map fst xs),snd (head xs)) (es,ws)
 
 reset :: EvalM s a -> EvalM s [a]
-reset (EvalM f) = EvalM $ \gl k mt d r ws -> do
-  res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) mt d [] ws
+reset (EvalM f) = EvalM $ \gl k e mt d r ws -> do
+  res <- f gl (\x mt d xs ws -> return (Success (x:xs) ws)) (\msg ws -> return (Fail msg ws)) mt d [] ws
   case res of
-    Fail msg   ws -> return (Fail msg ws)
+    Fail msg   ws -> e msg ws
     Success xs ws -> k (reverse xs) mt d r ws
 
+try :: EvalM s a -> EvalM s a -> EvalM s a
+try (EvalM f) (EvalM g) = EvalM (\gl k e mt d r ws -> f gl k (\msg _ -> g gl k e mt d r ws) mt d r ws)
+
 evalError :: Message -> EvalM s a
-evalError msg = EvalM (\gr k _ _ r msgs -> return (Fail msg msgs))
+evalError msg = EvalM (\gr k e _ _ r ws -> e msg ws)
   
 evalWarn :: Message -> EvalM s ()
-evalWarn msg = EvalM (\gr k mt d r msgs -> k () mt d r (msg:msgs))
+evalWarn msg = EvalM (\gr k e mt d r msgs -> k () mt d r (msg:msgs))
 
 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 ->
+evalPredef env h id args = EvalM (\globals@(Gl _ predef) k e 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
+    Just (EvalM f) -> f globals k e mt d r msgs
     Nothing        -> k RunTime mt d r msgs)
 
 getResDef :: QIdent -> EvalM s Term
-getResDef q = EvalM $ \(Gl gr _) k mt d r msgs -> do
+getResDef q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
   case lookupResDef gr q of
     Ok t    -> k t mt d r msgs
-    Bad msg -> return (Fail (pp msg) msgs)
+    Bad msg -> e (pp msg) msgs
 
 getInfo :: QIdent -> EvalM s (ModuleName,Info)
-getInfo q = EvalM $ \(Gl gr _) k mt d r msgs -> do
+getInfo q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
   case lookupOrigInfo gr q of
     Ok res  -> k res mt d r msgs
-    Bad msg -> return (Fail (pp msg) msgs)
+    Bad msg -> e (pp msg) msgs
 
 getResType :: QIdent -> EvalM s Type
-getResType q = EvalM $ \(Gl gr _) k mt d r msgs -> do
+getResType q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
   case lookupResType gr q of
     Ok t    -> k t mt d r msgs
-    Bad msg -> return (Fail (pp msg) msgs)
+    Bad msg -> e (pp msg) msgs
 
 getOverload :: Term -> QIdent -> EvalM s (Term,Type)
-getOverload t q = EvalM $ \(Gl gr _) k mt d r msgs -> do
+getOverload t q = EvalM $ \(Gl gr _) k e mt d r msgs -> do
   case lookupOverloadTypes gr q of
     Ok ttys -> let err = "Overload resolution failed" $$
                          "of term   " <+> pp t $$
                          "with types" <+> vcat [ppTerm Terse 0 ty | (_,ty) <- ttys]
 
-                   go []         = return (Fail err msgs)
-                   go (tty:ttys) = do res <- k tty mt d r msgs
-                                      case res of
-                                        Fail _ _       -> go ttys
-                                        Success r msgs -> return (Success r msgs)
+                   go r []         = return (Success r msgs)
+                   go r (tty:ttys) = do res <- k tty mt d r msgs
+                                        case res of
+                                          Fail _ _       -> go r ttys
+                                          Success r msgs -> go r ttys
 
-               in go ttys
-    Bad msg -> return (Fail (pp msg) msgs)
+               in go r ttys
+    Bad msg -> e (pp msg) msgs
 
 getAllParamValues :: Type -> EvalM s [Term]
-getAllParamValues ty = EvalM $ \(Gl gr _) k mt d r msgs ->
+getAllParamValues ty = EvalM $ \(Gl gr _) k e mt d r msgs ->
   case allParamValues gr ty of
     Ok ts   -> k ts mt d r msgs
-    Bad msg -> return (Fail (pp msg) msgs)
+    Bad msg -> e (pp msg) msgs
 
-newThunk env t = EvalM $ \gr k mt d r msgs -> do
+newThunk env t = EvalM $ \gr k e mt d r msgs -> do
  tnk <- newSTRef (Unevaluated env t)
  k tnk mt d r msgs
 
-newEvaluatedThunk v = EvalM $ \gr k mt d r msgs -> do
+newEvaluatedThunk v = EvalM $ \gr k e mt d r msgs -> do
  tnk <- newSTRef (Evaluated maxBound v)
  k tnk mt d r msgs
 
-newHole i = EvalM $ \gr k mt d r msgs ->
+newHole i = EvalM $ \gr k e mt d r msgs ->
   if i == 0
     then do tnk <- newSTRef (Hole i)
             k tnk mt d r msgs
@@ -949,22 +947,22 @@ newHole i = EvalM $ \gr k mt d r msgs ->
            Nothing  -> do tnk <- newSTRef (Hole i)
                           k tnk (Map.insert i tnk mt) d r msgs
 
-newResiduation scope = EvalM $ \gr k mt d r msgs -> do
+newResiduation scope = EvalM $ \gr k e mt d r msgs -> do
   let i = Map.size mt + 1
   tnk <- newSTRef (Residuation i scope Nothing)
   k (i,tnk) (Map.insert i tnk mt) d r msgs
 
-newNarrowing ty = EvalM $ \gr k mt d r msgs -> do
+newNarrowing ty = EvalM $ \gr k e mt d r msgs -> do
   let i = Map.size mt + 1
   tnk <- newSTRef (Narrowing i ty)
   k (i,tnk) (Map.insert i tnk mt) d r msgs
 
-withVar d0 (EvalM f) = EvalM $ \gr k mt d1 r msgs ->
+withVar d0 (EvalM f) = EvalM $ \gr k e mt d1 r msgs ->
                                   let !d = min d0 d1
-                                  in f gr k mt d r msgs
+                                  in f gr k e mt d r msgs
 
 getVariables :: EvalM s [(LVar,LIndex)]
-getVariables = EvalM $ \(Gl gr _) k mt d ws r -> do
+getVariables = EvalM $ \(Gl gr _) k e mt d ws r -> do
   ps <- metas2params gr (Map.elems mt)
   k ps mt d ws r
   where
@@ -981,15 +979,15 @@ getVariables = EvalM $ \(Gl gr _) k mt d ws r -> do
                                else return params
         _              -> metas2params gr tnks
 
-getRef tnk = EvalM $ \gr k mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs
-setRef tnk st = EvalM $ \gr k mt d r msgs -> do
+getRef tnk = EvalM $ \gr k e mt d r msgs -> readSTRef tnk >>= \st -> k st mt d r msgs
+setRef tnk st = EvalM $ \gr k e mt d r msgs -> do
   old <- readSTRef tnk
   writeSTRef tnk st
   res <- k () mt d r msgs
   writeSTRef tnk old
   return res
 
-force tnk = EvalM $ \gr k mt d r msgs -> do
+force tnk = EvalM $ \gr k e mt d r msgs -> do
   s <- readSTRef tnk
   case s of
     Unevaluated env t -> case eval env t [] of
@@ -997,14 +995,14 @@ force tnk = EvalM $ \gr k mt d r msgs -> do
                                                                  writeSTRef tnk (Evaluated d v)
                                                                  r <- k v mt d r msgs
                                                                  writeSTRef tnk s
-                                                                 return r) mt d r msgs
+                                                                 return r) e mt d r msgs
     Evaluated d v     -> k v mt d r msgs
     Hole _            -> k (VMeta tnk []) mt d r msgs
     Residuation _ _ _ -> k (VMeta tnk []) mt d r msgs
     Narrowing _ _     -> k (VMeta tnk []) mt d r msgs
 
 tnk2term True  xs tnk = force tnk >>= value2term True xs
-tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
+tnk2term False xs tnk = EvalM $ \gr k e mt d r msgs ->
   let join f g = do res <- f
                     case res of
                       Fail msg  msgs -> return (Fail msg msgs)
@@ -1018,21 +1016,23 @@ tnk2term False xs tnk = EvalM $ \gr k mt d r msgs ->
         | d < d0    = flush xs (\mt r msgs -> join (k x mt d r msgs) (\r msgs -> return (Success (r,c+1,[]) msgs))) mt r msgs
         | otherwise = return (Success (r,c+1,x:xs) msgs)
 
+      err msg msgs = return (Fail msg msgs)
+
   in do s <- readSTRef tnk
         case s of
           Unevaluated env t -> do let d0 = length env
                                   res <- case eval env t [] of
                                            EvalM f -> f gr (\v mt d msgs r -> do writeSTRef tnk (Evaluated d0 v)
                                                                                  r <- case value2term False xs v of
-                                                                                        EvalM f -> f gr (acc d0) mt d msgs r
+                                                                                        EvalM f -> f gr (acc d0) err mt d msgs r
                                                                                  writeSTRef tnk s
-                                                                                 return r) mt maxBound (r,0,[]) msgs
+                                                                                 return r) err mt maxBound (r,0,[]) msgs
                                   case res of
                                     Fail msg msgs         -> return (Fail msg msgs)
                                     Success (r,0,xs) msgs -> k (FV []) mt d r msgs
                                     Success (r,c,xs) msgs -> flush xs (\mt msgs r -> return (Success msgs r)) mt r msgs
           Evaluated d0 v    -> do res <- case value2term False xs v of
-                                           EvalM f -> f gr (acc d0) mt maxBound (r,0,[]) msgs
+                                           EvalM f -> f gr (acc d0) err mt maxBound (r,0,[]) msgs
                                   case res of
                                     Fail msg msgs         -> return (Fail msg msgs)
                                     Success (r,0,xs) msgs -> k (FV []) mt d r msgs
@@ -1045,4 +1045,5 @@ scopeEnv   scope = zipWithM (\x i -> newEvaluatedThunk (VGen i []) >>= \tnk -> r
 
 
 unsafeIOToEvalM :: IO a -> EvalM s a
-unsafeIOToEvalM f = EvalM (\gr k mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs)
+unsafeIOToEvalM f = EvalM (\gr k e mt d r msgs -> unsafeIOToST f >>= \x -> k x mt d r msgs)
+
diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
new file mode 100644
index 000000000..7bb6f2b1f
--- /dev/null
+++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
@@ -0,0 +1,808 @@
+{-# LANGUAGE RankNTypes, BangPatterns, GeneralizedNewtypeDeriving #-}
+
+module GF.Compile.Compute.Concrete2
+           (Env, Scope, Value(..), Constraint, ConstValue(..), Globals(..), PredefTable, EvalM,
+            runEvalM, stdPredef, globals, pdArity,
+            normalForm, normalFlatForm,
+            eval, apply, value2term, value2termM, patternMatch, vtableSelect,
+            newBinding, newResiduation, getMeta, setMeta, MetaState(..), variants, try,
+            evalError, evalWarn, ppValue, Choice, unit, split, split4, mapC, mapCM) where
+
+import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
+import GF.Infra.Ident
+import GF.Infra.CheckM
+import GF.Data.Operations(Err(..))
+import GF.Data.Utilities(splitAt',(<||>),anyM)
+import GF.Grammar.Lookup(lookupResDef,lookupOrigInfo)
+import GF.Grammar.Grammar
+import GF.Grammar.Macros
+import GF.Grammar.Predef
+import GF.Grammar.Printer hiding (ppValue)
+import GF.Grammar.Lockfield(lockLabel)
+import GF.Text.Pretty hiding (empty)
+import Control.Monad
+import Control.Applicative hiding (Const)
+import qualified Control.Applicative as A
+import qualified Data.Map as Map
+import Data.Maybe (fromMaybe,fromJust)
+import Data.List
+import Data.Char
+
+type Env  = [(Ident,Value)]
+type Scope = [(Ident,Value)]
+type Predef a = Globals -> Choice -> [Value] -> ConstValue a
+type PredefCombinator a = Predef a -> Predef a
+type PredefTable = Map.Map Ident (Predef Value)
+data Globals = Gl Grammar PredefTable
+
+data Value
+  = VApp QIdent [Value]
+  | VMeta MetaId [Value]
+  | VSusp MetaId (Value -> Value) [Value]
+  | VGen  {-# UNPACK #-} !Int [Value]
+  | VClosure Env Choice Term
+  | VProd BindType Ident Value Value
+  | VRecType [(Label, Value)]
+  | VR [(Label, Value)]
+  | VP Value Label [Value]
+  | VExtR Value Value
+  | VTable Value Value
+  | VT Value Env Choice [Case]
+  | VV Value [Value]
+  | VS Value Value [Value]
+  | VSort Ident
+  | VInt Integer
+  | VFlt Double
+  | VStr String
+  | VEmpty
+  | VC Value Value
+  | VGlue Value Value
+  | VPatt Int (Maybe Int) Patt
+  | VPattType Value
+  | VFV Choice [Value]
+  | VAlts Value [(Value, Value)]
+  | VStrs [Value]
+  | VSymCat Int LIndex [(LIndex, (Value, Type))]
+  | VError Doc
+    -- These two constructors are only used internally
+    -- in the type checker.
+  | VCRecType [(Label, Bool, Value)]
+  | VCInts (Maybe Integer) (Maybe Integer)
+
+data ConstValue a
+  = Const a
+  | CSusp MetaId (Value -> ConstValue a)
+  | CFV Choice [ConstValue a]
+  | RunTime
+  | NonExist
+
+instance Functor ConstValue where
+  fmap f (Const c) = Const (f c)
+  fmap f (CFV i vs) = CFV i (map (fmap f) vs)
+  fmap f (CSusp i k) = CSusp i (fmap f . k)
+  fmap f RunTime   = RunTime
+  fmap f NonExist  = NonExist
+
+instance Applicative ConstValue where
+  pure = Const
+
+  (Const f)     <*> (Const x)     = Const (f x)
+  (CFV s vs)    <*> v2            = CFV s [v1 <*> v2 | v1 <- vs]
+  v1            <*> (CFV s vs)    = CFV s [v1 <*> v2 | v2 <- vs]
+  (CSusp i k)   <*> v2            = CSusp i (\v -> k v <*> v2)
+  v1            <*> (CSusp i k)   = CSusp i (\v -> v1 <*> k v)
+  NonExist      <*> _             = NonExist
+  _             <*> NonExist      = NonExist
+  RunTime       <*>  _            = RunTime
+  _             <*>  RunTime      = RunTime
+
+normalForm :: Globals -> Term -> Check Term
+normalForm g t = value2term g [] (eval g [] unit t [])
+
+normalFlatForm :: Globals -> Term -> Check [Term]
+normalFlatForm g t = runEvalM g (value2termM False [] (eval g [] unit t []))
+
+eval :: Globals -> Env -> Choice -> Term -> [Value] -> Value
+eval g env s (Vr x)         vs  = case lookup x env of
+                                    Nothing -> VError ("Variable" <+> pp x <+> "is not in scope")
+                                    Just v  -> apply g v vs
+eval g env s (Sort sort)    []
+  | sort == cTok                = VSort cStr
+  | otherwise                   = VSort sort
+eval g env s (EInt n)       []  = VInt n
+eval g env s (EFloat d)     []  = VFlt d
+eval g env s (K t)          []  = VStr t
+eval g env s Empty          []  = VEmpty
+eval g env s (App t1 t2)    vs  = let (s1,s2) = split s
+                                  in eval g env s1 t1 (eval g env s2 t2 [] : vs)
+eval g env s (Abs b x t)    []  = VClosure env s (Abs b x t)
+eval g env s (Abs b x t) (v:vs) = eval g ((x,v):env) s t vs
+eval g env s (Meta i)       vs  = VMeta i vs
+eval g env s (ImplArg t)    []  = eval g env s t []
+eval g env s (Prod b x t1 t2)[] = let (s1,s2) = split s
+                                  in VProd b x (eval g env s1 t1 []) (VClosure env s2 t2)
+eval g env s (Typed t ty)   vs  = eval g env s t vs
+eval g env s (RecType lbls) []  = VRecType (mapC (\s (lbl,ty) -> (lbl, eval g env s ty [])) s lbls)
+eval g env s (R as)         []  = VR (mapC (\s (lbl,(ty,t)) -> (lbl, eval g env s t [])) s as)
+eval g env s (P t lbl)      vs  = let project (VR as)        = case lookup lbl as of
+                                                                 Nothing -> VError ("Missing value for label" <+> pp lbl $$
+                                                                                    "in" <+> pp (P t lbl))
+                                                                 Just v  -> apply g v vs
+                                      project (VFV s fvs)    = VFV s (map project fvs)
+                                      project (VMeta i vs)   = VSusp i (\v -> project (apply g v vs)) []
+                                      project (VSusp i k vs) = VSusp i (\v -> project (apply g (k v) vs)) []
+                                      project v              = VP v lbl vs
+                                  in project (eval g env s t [])
+eval g env s (ExtR t1 t2)   []  = let (s1,s2) = split s
+
+                                      extend (VR       as1) (VR       as2)   = VR       (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
+                                      extend (VRecType as1) (VRecType as2)   = VRecType (foldl (\as (lbl,v) -> update lbl v as) as1 as2)
+                                      extend (VFV i fvs)    v2               = VFV i [extend v1 v2 | v1 <- fvs]
+                                      extend v1             (VFV i fvs)      = VFV i [extend v1 v2 | v2 <- fvs]
+                                      extend (VMeta i vs)   v2               = VSusp i (\v -> extend (apply g v vs) v2) []
+                                      extend v1             (VMeta i vs)     = VSusp i (\v -> extend v1 (apply g v vs)) []
+                                      extend (VSusp i k vs) v2               = VSusp i (\v -> extend (apply g (k v) vs) v2) []
+                                      extend v1             (VSusp i k vs)   = VSusp i (\v -> extend v1 (apply g (k v) vs)) []
+                                      extend v1             v2               = VExtR v1 v2
+
+                                  in extend (eval g env s1 t1 []) (eval g env s2 t2 [])
+eval g env s (Table t1 t2)  []  = let (!s1,!s2) = split s
+                                  in VTable (eval g env s1 t1 []) (eval g env s2 t2 [])
+eval g env s (T (TTyped ty) cs)[]=let (!s1,!s2) = split s
+                                  in VT (eval g env s1 ty []) env s2 cs
+eval g env s (T (TWild ty) cs) []=let (!s1,!s2) = split s
+                                  in VT (eval g env s1 ty []) env s2 cs
+eval g env s (V ty ts)      []  = let (!s1,!s2) = split s
+                                  in VV (eval g env s1 ty []) (mapC (\s t -> eval g env s t []) s2 ts)
+eval g env s (S t1 t2)      vs  = let (!s1,!s2) = split s
+                                      v1 = eval g env s1 t1 []
+                                      v2 = eval g env s2 t2 []
+                                      v0 = VS v1 v2 vs
+
+                                      select (VT _  env s cs) = patternMatch g s v0 (map (\(p,t) -> (env,[p],v2:vs,t)) cs)
+                                      select (VV vty tvs)     = case value2termM False (map fst env) vty of
+                                                                  EvalM f -> case f g (\x state xs ws -> Success (x:xs) ws) empty [] [] of
+                                                                               Fail   msg  ws -> VError msg
+                                                                               Success tys ws -> case tys of
+                                                                                                   [ty] -> vtableSelect g v0 ty tvs v2 vs
+                                                                                                   tys  -> vtableSelect g v0 (FV (reverse tys)) tvs v2 vs
+                                      select (VFV i fvs)      = VFV i [select v1 | v1 <- fvs]
+                                      select (VMeta i vs)     = VSusp i (\v -> select (apply g v vs)) []
+                                      select (VSusp i k vs)   = VSusp i (\v -> select (apply g (k v) vs)) []
+                                      select v1               = v0
+                                          
+                                      empty = State Map.empty Map.empty
+
+                                in select v1
+eval g env s (Let (x,(_,t1)) t2) vs = let (!s1,!s2) = split s
+                                      in eval g ((x,eval g env s1 t1 []):env) s2 t2 vs
+eval g env c (Q q@(m,id))  vs
+  | m == cPredef              = case Map.lookup id predef of
+                                  Nothing -> VApp q vs
+                                  Just fn -> let valueOf (Const res) = res
+                                                 valueOf (CFV i vs)  = VFV i (map valueOf vs)
+                                                 valueOf (CSusp i k) = VSusp i (valueOf . k) []
+                                                 valueOf RunTime     = VApp q vs
+                                                 valueOf NonExist    = VApp (cPredef,cNonExist) []
+                                             in valueOf (fn g c vs)
+  | otherwise                 = case lookupResDef gr q of
+                                  Ok t    -> eval g env c t vs
+                                  Bad msg -> error msg
+  where
+    Gl gr predef = g
+eval g env s (QC q)         vs  = VApp q vs
+eval g env s (C t1 t2)      []  = let (!s1,!s2) = split s
+
+                                      concat v1           VEmpty = v1
+                                      concat VEmpty           v2 = v2
+                                      concat (VFV i fvs)      v2 = VFV i [concat v1 v2 | v1 <- fvs]
+                                      concat v1      (VFV i fvs) = VFV i [concat v1 v2 | v2 <- fvs]
+                                      concat (VMeta i vs)     v2 = VSusp i (\v -> concat (apply g v vs) v2) []
+                                      concat v1     (VMeta i vs) = VSusp i (\v -> concat v1 (apply g v vs)) []
+                                      concat (VSusp i k vs)   v2 = VSusp i (\v -> concat (apply g (k v) vs) v2) []
+                                      concat v1   (VSusp i k vs) = VSusp i (\v -> concat v1 (apply g (k v) vs)) []
+                                      concat v1               v2 = VC v1 v2
+
+                                  in concat (eval g env s1 t1 []) (eval g env s2 t2 [])
+eval g env s (Glue t1 t2)   []  = let (!s1,!s2) = split s
+
+                                      glue VEmpty        v             = v
+                                      glue (VC v1 v2)    v             = VC v1 (glue v2 v)
+                                      glue (VApp q [])   v
+                                        | q == (cPredef,cNonExist)     = VApp q []
+                                      glue v             VEmpty        = v
+                                      glue v             (VC v1 v2)    = VC (glue v v1) v2
+                                      glue v             (VApp q [])
+                                        | q == (cPredef,cNonExist)     = VApp q []
+                                      glue (VStr s1)     (VStr s2)     = VStr (s1++s2)
+                                      glue v             (VAlts d vas) = VAlts (glue v d) [(glue v v',ss) | (v',ss) <- vas]
+                                      glue (VAlts d vas) (VStr s)      = pre d vas s
+                                      glue (VAlts d vas) v             = glue d v
+                                      glue (VFV i fvs)   v2            = VFV i [glue v1 v2 | v1 <- fvs]
+                                      glue v1            (VFV i fvs)   = VFV i [glue v1 v2 | v2 <- fvs]
+                                      glue (VMeta i vs)  v2            = VSusp i (\v -> glue (apply g v vs) v2) []
+                                      glue v1            (VMeta i vs)  = VSusp i (\v -> glue v1 (apply g v vs)) []
+                                      glue (VSusp i k vs) v2           = VSusp i (\v -> glue (apply g (k v) vs) v2) []
+                                      glue v1            (VSusp i k vs)= VSusp i (\v -> glue v1 (apply g (k v) vs)) []
+                                      glue v1            v2            = VGlue v1 v2
+
+                                      pre vd []                 s              = glue vd (VStr s)
+                                      pre vd ((v,VStrs ss):vas) s
+                                        | or [startsWith s' s | VStr s' <- ss] = glue v (VStr s)
+                                        | otherwise                            = pre vd vas s
+
+                                  in glue (eval g env s1 t1 []) (eval g env s2 t2 [])
+eval g env s (EPatt min max p) [] = VPatt min max p
+eval g env s (EPattType t)  []  = VPattType (eval g env s t [])
+eval g env s (ELincat c ty) []  = let lbl = lockLabel c
+                                      lty = RecType []
+                                  in eval g env s (ExtR ty (RecType [(lbl,lty)])) []
+eval g env s (ELin c t)     []  = let lbl = lockLabel c
+                                      lt  = R []
+                                  in eval g env s (ExtR t (R [(lbl,(Nothing,lt))])) []
+eval g env s (FV ts)        vs  = VFV s (mapC (\s t -> eval g env s t vs) s ts)
+eval g env s (Alts d as)    []  = let (!s1,!s2) = split s
+                                      vd  = eval g env s1 d []
+                                      vas = mapC (\s (t1,t2) -> let (!s1,!s2) = split s
+                                                              in (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as
+                                  in VAlts vd vas
+eval g env s (Strs ts)      []  = VStrs (mapC (\s t -> eval g env s t []) s ts)
+eval g env s (TSymCat d r rs) []= VSymCat d r [(i,(fromJust (lookup pv env),ty)) | (i,(pv,ty)) <- rs]
+eval g env s t              vs  = VError ("Cannot reduce term" <+> pp t)
+
+stdPredef :: Globals -> PredefTable
+stdPredef g = Map.fromList
+  [(cLength, pdArity 1 $ \g c [v] -> fmap (VInt . genericLength) (value2string g v))
+  ,(cTake,   pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTake (value2int g v1) (value2string g v2)))
+  ,(cDrop,   pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDrop (value2int g v1) (value2string g v2)))
+  ,(cTk,     pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericTk (value2int g v1) (value2string g v2)))
+  ,(cDp,     pdArity 2 $ \g c [v1,v2] -> fmap string2value (liftA2 genericDp (value2int g v1) (value2string g v2)))
+  ,(cIsUpper,pdArity 1 $ \g c [v]     -> fmap toPBool (liftA (all isUpper) (value2string g v)))
+  ,(cToUpper,pdArity 1 $ \g c [v]     -> fmap string2value (liftA (map toUpper) (value2string g v)))
+  ,(cToLower,pdArity 1 $ \g c [v]     -> fmap string2value (liftA (map toLower) (value2string g v)))
+  ,(cEqStr,  pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2string g v1) (value2string g v2)))
+  ,(cOccur,  pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occur (value2string g v1) (value2string g v2)))
+  ,(cOccurs, pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 occurs (value2string g v1) (value2string g v2)))
+  ,(cEqInt,  pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (==) (value2int g v1) (value2int g v2)))
+  ,(cLessInt,pdArity 2 $ \g c [v1,v2] -> fmap toPBool (liftA2 (<) (value2int g v1) (value2int g v2)))
+  ,(cPlus,   pdArity 2 $ \g c [v1,v2] -> fmap VInt (liftA2 (+) (value2int g v1) (value2int g v2)))
+  ,(cError,  pdArity 1 $ \g c [v]     -> fmap (VError . pp) (value2string g v))
+  ]
+  where
+    genericTk n = reverse . genericDrop n . reverse
+    genericDp n = reverse . genericTake n . reverse
+
+apply g (VMeta i vs0)                   vs  = VMeta i   (vs0++vs)
+apply g (VSusp i k vs0)                 vs  = VSusp i k (vs0++vs)
+apply g (VApp f  vs0)                   vs  = VApp f (vs0++vs)
+apply g (VGen i  vs0)                   vs  = VGen i (vs0++vs)
+apply g (VFV i fvs)                     vs  = VFV i [apply g v vs | v <- fvs]
+apply g (VClosure env s (Abs b x t)) (v:vs) = eval g ((x,v):env) s t vs
+apply g v                               []  = v
+
+toPBool True  = VApp (cPredef,cPTrue)  []
+toPBool False = VApp (cPredef,cPFalse) []
+
+occur s1 []          = False
+occur s1 s2@(_:tail) = check s1 s2
+  where
+    check xs        []  = False
+    check []        ys  = True
+    check (x:xs) (y:ys)
+      | x == y          = check xs ys
+    check _      _      = occur s1 tail
+
+occurs cs s2 = any (\c -> elem c s2) cs
+
+update lbl v []              = [(lbl,v)]
+update lbl v (a@(lbl',_):as)
+  | lbl==lbl'                = (lbl,v) : as
+  | otherwise                = a : update lbl v as
+
+patternMatch g s v0 []                      = v0
+patternMatch g s v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
+  where
+    match env []              eqs      args  = eval g env s t args
+    match env (PT ty p   :ps) eqs      args  = match env (p:ps) eqs args
+    match env (PAlt p1 p2:ps) eqs      args  = match env (p1:ps) ((env,p2:ps,args,t):eqs) args
+    match env (PM q      :ps) eqs      args  = case lookupResDef gr q of
+                                                 Ok t    -> case eval g [] unit t [] of
+                                                              VPatt _ _ p -> match env (p:ps) eqs args
+                                                              _ -> error $ render (hang "Expected pattern macro:" 4
+                                                                                        (pp t))
+                                                 Bad msg -> error msg
+                                               where
+                                                 Gl gr _ = g
+    match env (PV v      :ps) eqs (arg:args) = match ((v,arg):env) ps eqs args
+    match env (PAs v p   :ps) eqs (arg:args) = match ((v,arg):env) (p:ps) eqs (arg:args)
+    match env (PW        :ps) eqs (arg:args) = match env ps eqs args
+    match env (PTilde _  :ps) eqs (arg:args) = match env ps eqs args
+    match env (p         :ps) eqs (arg:args) = match' env p ps eqs arg args
+
+    match' env p ps eqs arg args =
+      case (p,arg) of
+        (p,       VMeta i   vs) -> VSusp i (\v -> match' env p ps eqs (apply g v vs) args) []
+        (p,     VGen    i   vs) -> v0
+        (p,       VSusp i k vs) -> VSusp i (\v -> match' env p ps eqs (apply g (k v) vs) args) []
+        (p,           VFV s vs) -> VFV s [match' env p ps eqs arg args | arg <- vs]
+        (PP q qs,    VApp r vs)
+          | q == r              -> match env (qs++ps) eqs (vs++args)
+        (PR pas,  VR as)        -> matchRec env (reverse pas) as ps eqs args
+        (PString s1, VStr s2)
+          | s1 == s2            -> match env ps eqs args
+        (PString s1, VEmpty)
+          | null s1             -> match env ps eqs args
+        (PSeq min1 max1 p1 min2 max2 p2,v)
+                          -> case value2string g v of
+                               Const str -> let n  = length str
+                                                lo = min1 `max` (n-fromMaybe n max2)
+                                                hi = (n-min2) `min` fromMaybe n max1
+                                                (ds,cs) = splitAt lo str
+
+                                                eqs' = matchStr env (p1:p2:ps) eqs (hi-lo) (reverse ds) cs args
+
+                                            in patternMatch g s v0 eqs'
+                               RunTime   -> v0
+                               NonExist  -> patternMatch g s v0 eqs
+        (PRep minp maxp p, v)
+                          -> case value2string g v of
+                               Const str -> let n = length (str::String) `div` (max minp 1)
+                                                eqs' = matchRep env n minp maxp p minp maxp p ps ((env,PString []:ps,(arg:args),t) : eqs) (arg:args)
+                                            in patternMatch g s v0 eqs'
+                               RunTime   -> v0
+                               NonExist  -> patternMatch g s v0 eqs
+        (PChar, VStr [_]) -> match env ps eqs args
+        (PChars cs, VStr [c])
+          | elem c cs     -> match env ps eqs args
+        (PInt n, VInt m)
+          | n == m        -> match env ps eqs args
+        (PFloat n, VFlt m)
+          | n == m        -> match env ps eqs args
+        _                 -> patternMatch g s v0 eqs
+
+    matchRec env []            as ps eqs args = match env ps eqs args
+    matchRec env ((lbl,p):pas) as ps eqs args =
+      case lookup lbl as of
+        Just tnk -> matchRec env pas as (p:ps) eqs (tnk:args)
+        Nothing  -> VError ("Missing value for label" <+> pp lbl)
+
+    matchStr env ps eqs i ds []     args =
+      (env,ps,(string2value (reverse ds)):(string2value []):args,t) : eqs
+    matchStr env ps eqs 0 ds cs     args =
+      (env,ps,(string2value (reverse ds)):(string2value cs):args,t) : eqs
+    matchStr env ps eqs i ds (c:cs) args =
+      (env,ps,(string2value (reverse ds)):(string2value (c:cs)):args,t) :
+      matchStr env ps eqs (i-1 :: Int) (c:ds) cs args
+
+    matchRep env 0 minp maxp p minq maxq q ps eqs args = eqs
+    matchRep env n minp maxp p minq maxq q ps eqs args =
+      matchRep env (n-1) minp maxp p (minp+minq) (liftM2 (+) maxp maxq) (PSeq minp maxp p minq maxq q) ps ((env,q:ps,args,t) : eqs) args
+
+vtableSelect g v0 ty cs v2 vs =
+  apply g (select (value2index v2 ty)) vs
+  where
+    select (Const (i,_)) = cs !! i
+    select (CSusp i k)   = VSusp i (\v -> select (k v)) []
+    select (CFV s vs)    = VFV s (map select vs)
+    select _             = VError ("the parameter:" <+> ppValue Unqualified 0 v2 $$
+                                   "cannot be evaluated at compile time.")
+
+    value2index (VMeta i vs)      ty = CSusp i (\v -> value2index (apply g v vs) ty)
+    value2index (VSusp i k vs)    ty = CSusp i (\v -> value2index (apply g (k v) vs) ty)
+    value2index (VR as) (RecType lbls) = compute lbls
+      where
+        compute []              = pure (0,1)
+        compute ((lbl,ty):lbls) =
+          case lookup lbl as of
+            Just v  -> liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt'))
+                              (value2index v ty)
+                              (compute lbls)
+            Nothing -> error (show ("Missing value for label" <+> pp lbl $$
+                                    "among" <+> hsep (punctuate (pp ',') (map fst as))))
+    value2index (VApp q tnks) ty =
+      let (r ,ctxt,cnt ) = getIdxCnt q
+      in fmap (\(r', cnt') -> (r+r',cnt)) (compute ctxt tnks)
+      where
+        getIdxCnt q =
+          let (_,ResValue (L _ ty) idx) = getInfo q
+              (ctxt,QC p) = typeFormCnc ty
+              (_,ResParam _ (Just (_,cnt))) = getInfo p
+          in (idx,ctxt,cnt)
+
+        compute []              []     = pure (0,1)
+        compute ((_,_,ty):ctxt) (v:vs) =
+          liftA2 (\(r, cnt) (r',cnt') -> (r*cnt'+r',cnt*cnt'))
+                 (value2index v ty)
+                 (compute ctxt vs)
+
+        getInfo :: QIdent -> (ModuleName,Info)
+        getInfo q =
+          case lookupOrigInfo gr q of
+            Ok res  -> res
+            Bad msg -> error msg
+
+        Gl gr _ = g
+    value2index (VInt n)          ty
+      | Just max <- isTypeInts ty    = Const (fromIntegral n,fromIntegral max+1)
+    value2index (VFV i vs)        ty = CFV i [value2index v ty | v <- vs]
+    value2index v ty = RunTime
+
+
+value2term :: Globals -> [Ident] -> Value -> Check Term
+value2term g xs v = do
+  res <- runEvalM g (value2termM False xs v)
+  case res of
+    [t] -> return t
+    ts  -> return (FV ts)
+
+type Constraint = Value
+data MetaState
+  = Bound Int Value
+  | Narrowing   Type
+  | Residuation Scope (Maybe Constraint)
+data State
+  = State 
+      { choices  :: Map.Map Choice Int
+      , metaVars :: Map.Map MetaId MetaState
+      }
+type Cont r = State -> r -> [Message] -> CheckResult r [Message]
+newtype EvalM a = EvalM (forall r . Globals -> (a -> Cont r) -> Cont r)
+
+instance Functor EvalM where
+  fmap f (EvalM m) = EvalM (\g k -> m g (k . f))
+
+instance Applicative EvalM where
+  pure x = EvalM (\g k -> k x)
+  (EvalM f) <*> (EvalM h) = EvalM (\g k -> f g (\fn -> h g (\x -> k (fn x))))
+
+instance Alternative EvalM where
+  empty = EvalM (\g k _ r msgs -> Success r msgs)
+  (EvalM f) <|> (EvalM g) = EvalM $ \gl k state r msgs ->
+     case f gl k state r msgs of
+       Fail msg  msgs -> Fail msg msgs
+       Success r msgs -> g gl k state r msgs
+
+instance Monad EvalM where
+  (EvalM f) >>= h = EvalM (\g k -> f g (\x -> case h x of {EvalM h -> h g k}))
+
+instance MonadFail EvalM where
+  fail msg = EvalM (\g k _ _ msgs -> Fail (pp msg) msgs)
+
+instance MonadPlus EvalM where
+
+evalError msg = EvalM (\g k _ _ msgs -> Fail msg msgs)
+
+evalWarn msg = EvalM (\g k state r msgs -> k () state r (msg:msgs))
+
+runEvalM :: Globals -> EvalM a -> Check [a]
+runEvalM g (EvalM f) = Check $ \(es,ws) ->
+  case f g (\x state xs ws -> Success (x:xs) ws) empty [] ws of
+    Fail   msg ws -> Fail msg (es,ws)
+    Success xs ws -> Success (reverse xs) (es,ws)
+  where
+    empty = State Map.empty Map.empty
+
+globals :: EvalM Globals
+globals = EvalM (\g k -> k g)
+
+variants :: Choice -> [a] -> EvalM a
+variants c xs = EvalM (\g k state@(State choices metas) r msgs ->
+  case Map.lookup c choices of
+    Just j  -> k (xs !! j) state r msgs
+    Nothing -> backtrack 0 xs k choices metas r msgs)
+  where
+    backtrack j []     k choices metas r msgs = Success r msgs
+    backtrack j (x:xs) k choices metas r msgs =
+      case k x (State (Map.insert c j choices) metas) r msgs of
+        Fail    msg msgs -> Fail msg msgs
+        Success r   msgs -> backtrack (j+1) xs k choices metas r msgs
+
+try :: (a -> EvalM b) -> [a] -> Message -> EvalM b
+try f xs msg = EvalM (\g k state r msgs ->
+  let (res,msgs') = backtrack g xs state [] msgs
+  in case res of
+       []  -> Fail msg msgs'
+       res -> continue g k res r msgs')
+  where
+    backtrack g []     state res msgs = (res,msgs)
+    backtrack g (x:xs) state res msgs =
+      case f x of
+        EvalM f -> case f g (\x state res msgs -> Success ((x,state):res) msgs) state res msgs of
+                     Fail msg _       -> backtrack g xs state res msgs
+                     Success res msgs -> backtrack g xs state res msgs
+
+    continue g k []              r msgs = Success r msgs
+    continue g k ((x,state):res) r msgs =
+      case k x state r msgs of
+        Fail msg msgs  -> Fail msg msgs
+        Success r msgs -> continue g k res r msgs
+
+newBinding :: Value -> EvalM MetaId
+newBinding v = EvalM (\g k (State choices metas) r msgs ->
+  let meta_id = Map.size metas+1
+  in k meta_id (State choices (Map.insert meta_id (Bound 0 v) metas)) r msgs)
+
+newResiduation :: Scope -> EvalM MetaId
+newResiduation scope = EvalM (\g k (State choices metas) r msgs ->
+  let meta_id = Map.size metas+1
+  in k meta_id (State choices (Map.insert meta_id (Residuation scope Nothing) metas)) r msgs)
+
+getMeta :: MetaId -> EvalM MetaState
+getMeta i = EvalM (\g k state r msgs ->
+  case Map.lookup i (metaVars state) of
+    Just ms -> k ms state r msgs
+    Nothing -> Fail ("Metavariable ?"<>pp i<+>"is not defined") msgs) 
+
+setMeta :: MetaId -> MetaState -> EvalM ()
+setMeta i ms = EvalM (\g k (State choices metas) r msgs ->
+  let state' = State choices (Map.insert i ms metas)
+  in k () state' r msgs)
+
+value2termM :: Bool -> [Ident] -> Value -> EvalM Term
+value2termM flat xs (VApp q vs) =
+  foldM (\t v -> fmap (App t) (value2termM flat xs v)) (if fst q == cPredef then Q q else QC q) vs
+value2termM flat xs (VMeta i vs) = do
+  mv <- getMeta i
+  case mv of
+    Bound _ v    -> do g <- globals
+                       value2termM flat xs (apply g v vs)
+    Residuation _ mb_ctr ->
+      case mb_ctr of
+        Just ctr -> do g <- globals
+                       value2termM flat xs (apply g ctr vs)
+        Nothing  -> foldM (\t v -> fmap (App t) (value2termM flat xs v)) (Meta i) vs
+value2termM flat xs (VSusp j k vs) =
+  let v = k (VGen maxBound vs)
+  in value2termM flat xs v
+value2termM flat xs (VGen j tnks) =
+  foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (Vr (reverse xs !! j)) tnks
+value2termM flat xs (VClosure env s (Abs b x t)) = do
+  g <- globals
+  let v  = eval g ((x,VGen (length xs) []):env) s t []
+      x' = mkFreshVar xs x
+  t <- value2termM flat (x':xs) v
+  return (Abs b x' t)
+value2termM flat xs (VProd b x v1 v2)
+  | x == identW = do t1 <- value2termM flat xs v1
+                     v2 <- case v2 of
+                             VClosure env s t2 -> do g <- globals
+                                                     return (eval g env s t2 [])
+                             v2                -> return v2
+                     t2 <- value2termM flat xs v2
+                     return (Prod b x t1 t2)
+  | otherwise   = do t1 <- value2termM flat xs v1
+                     v2 <- case v2 of
+                             VClosure env s t2 -> do g <- globals
+                                                     return (eval g ((x,VGen (length xs) []):env) s t2 [])
+                             v2                -> return v2
+                     t2 <- value2termM flat (x:xs) v2
+                     return (Prod b (mkFreshVar xs x) t1 t2)
+value2termM flat xs (VRecType lbls) = do
+  lbls <- mapM (\(lbl,v) -> fmap ((,) lbl) (value2termM flat xs v)) lbls
+  return (RecType lbls)
+value2termM flat xs (VR as) = do
+  as <- mapM (\(lbl,v) -> fmap (\t -> (lbl,(Nothing,t))) (value2termM flat xs v)) as
+  return (R as)
+value2termM flat xs (VP v lbl vs) = do
+  t <- value2termM flat xs v
+  foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (P t lbl) vs
+value2termM flat xs (VExtR v1 v2) = do
+  t1 <- value2termM flat xs v1
+  t2 <- value2termM flat xs v2
+  return (ExtR t1 t2) 
+value2termM flat xs (VTable v1 v2) = do
+  t1 <- value2termM flat xs v1
+  t2 <- value2termM flat xs v2
+  return (Table t1 t2)
+value2termM flat xs (VT vty env s cs)= do
+  ty <- value2termM flat xs vty
+  cs <- forM cs $ \(p,t) -> do
+          let (_,xs',env') = pattVars (length xs,xs,env) p
+          g <- globals
+          t <- value2termM flat xs' (eval g env' s t [])
+          return (p,t)
+  return (T (TTyped ty) cs)
+value2termM flat xs (VV vty vs)= do
+  ty <- value2termM flat xs vty
+  ts <- mapM (value2termM flat xs) vs
+  return (V ty ts)
+value2termM flat xs (VS v1 v2 vs) = do
+  t1 <- value2termM flat xs v1
+  t2 <- value2termM flat xs v2
+  foldM (\e1 tnk -> fmap (App e1) (value2termM flat xs tnk)) (S t1 t2) vs
+value2termM flat xs (VSort s) = return (Sort s)
+value2termM flat xs (VStr tok) = return (K tok)
+value2termM flat xs (VInt n) = return (EInt n)
+value2termM flat xs (VFlt n) = return (EFloat n)
+value2termM flat xs VEmpty = return Empty
+value2termM flat xs (VC v1 v2) = do
+  t1 <- value2termM flat xs v1
+  t2 <- value2termM flat xs v2
+  return (C t1 t2)
+value2termM flat xs (VGlue v1 v2) = do
+  t1 <- value2termM flat xs v1
+  t2 <- value2termM flat xs v2
+  return (Glue t1 t2)
+value2termM flat xs (VFV i vs) = do
+  v <- variants i vs
+  value2termM flat xs v
+value2termM flat xs (VPatt min max p) = return (EPatt min max p)
+value2termM flat xs (VPattType v) = do t <- value2termM flat xs v
+                                       return (EPattType t)
+value2termM flat xs (VAlts vd vas) = do
+  d <- value2termM flat xs vd
+  as <- forM vas $ \(vt,vs) -> do
+           t <- value2termM flat xs vt
+           s <- value2termM flat xs vs
+           return (t,s)
+  return (Alts d as)
+value2termM flat xs (VStrs vs) = do
+  ts <- mapM (value2termM flat xs) vs
+  return (Strs ts)
+value2termM flat xs (VError msg) = evalError msg
+value2termM flat xs (VCInts Nothing    Nothing) = return (App (QC (cPredef,cInts)) (Meta 0))
+value2termM flat xs (VCInts (Just min) Nothing) = return (App (QC (cPredef,cInts)) (EInt min))
+value2termM flat xs (VCInts _       (Just max)) = return (App (QC (cPredef,cInts)) (EInt max))
+value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
+
+
+pattVars st (PP _ ps)    = foldl pattVars st ps
+pattVars st (PV x)       = case st of
+                             (i,xs,env) -> (i+1,x:xs,(x,VGen i []):env)
+pattVars st (PR as)      = foldl (\st (_,p) -> pattVars st p) st as
+pattVars st (PT ty p)    = pattVars st p
+pattVars st (PAs x p)    = case st of
+                             (i,xs,env) -> pattVars (i+1,x:xs,(x,VGen i []):env) p
+pattVars st (PImplArg p) = pattVars st p
+pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
+pattVars st _            = st
+
+
+ppValue q d (VApp c vs) = prec d 4 (hsep (ppQIdent q c : map (ppValue q 5) vs))
+ppValue q d (VMeta i vs) = prec d 4 (hsep ((if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
+ppValue q d (VSusp i k vs) = prec d 4 (hsep (pp "#susp" : (if i > 0 then pp "?" <> pp i else pp "?") : map (ppValue q 5) vs))
+ppValue q d (VGen _ _) = pp "VGen"
+ppValue q d (VClosure env c t) = pp "[|" <> ppTerm q 4 t <> pp "|]"
+ppValue q d (VProd _ _ _ _) = pp "VProd"
+ppValue q d (VRecType _) = pp "VRecType"
+ppValue q d (VR _) = pp "VR"
+ppValue q d (VP v l vs) = prec d 5 (hsep (ppValue q 5 v <> '.' <> l : map (ppValue q 5) vs))
+ppValue q d (VExtR _ _) = pp "VExtR"
+ppValue q d (VTable _ _) = pp "VTable"
+ppValue q d (VT t _ _ cs) = "table" <+> ppValue q 0 t <+> '{' $$
+                               nest 2 (vcat (punctuate ';' (map (ppCase q) cs))) $$
+                            '}'
+                            where
+                              ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e
+ppValue q d (VV _ _) = pp "VV"
+ppValue q d (VS v1 v2 vs) = prec d 3 (hsep (hang (ppValue q 3 v1) 2 ("!" <+> ppValue q 4 v2) : map (ppValue q 5) vs))
+ppValue q d (VSort s) = pp s
+ppValue q d (VInt n) = pp n
+ppValue q d (VFlt f) = pp f
+ppValue q d (VStr s) = ppTerm q d (K s)
+ppValue q d VEmpty = pp "[]"
+ppValue q d (VC v1 v2) = prec d 1 (hang (ppValue q 2 v1) 2 ("++" <+> ppValue q 1 v2))
+ppValue q d (VGlue v1 v2) = prec d 2 (ppValue q 3 v1 <+> '+'  <+> ppValue q 2 v2)
+ppValue q d (VPatt _ _ _) = pp "VPatt"
+ppValue q d (VPattType _) = pp "VPattType"
+ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) vs))))
+ppValue q d (VAlts e xs) = prec d 4 ("pre" <+> braces (ppValue q 0 e <> ';' <+> fsep (punctuate ';' (map (ppAltern q) xs))))
+ppValue q d (VStrs _) = pp "VStrs"
+ppValue q d (VSymCat i r rs) = pp '<' <> pp i <> pp ',' <> pp r <> pp '>'
+ppValue q d (VError msg) = prec d 4 (pp "error" <+> ppTerm q 5 (K (show msg)))
+ppValue q d (VCInts Nothing    Nothing)    = prec d 4 (pp "Ints ?")
+ppValue q d (VCInts (Just min) Nothing)    = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
+ppValue q d (VCInts Nothing    (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
+ppValue q d (VCInts (Just min) (Just max))
+   | min == max                            = prec d 4 (pp "Ints" <+> min)
+   | otherwise                             = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
+
+ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y
+
+prec d1 d2 doc
+  | d1 > d2   = parens doc
+  | otherwise = doc
+
+value2string g v = fmap (\(_,ws,_) -> unwords ws) (value2string' g v False [] [])
+
+value2string' g (VMeta i vs)   b ws        qs = CSusp i (\v -> value2string' g (apply g v vs) b ws qs)
+value2string' g (VSusp i k vs) b ws        qs = CSusp i (\v -> value2string' g (apply g (k v) vs) b ws qs)
+value2string' g (VStr w1)     True (w2:ws) qs = Const (False,(w1++w2):ws,qs)
+value2string' g (VStr w)         _ ws      qs = Const (False,w       :ws,qs)
+value2string' g VEmpty           b ws      qs = Const (b,ws,qs)
+value2string' g (VC v1 v2)       b ws      qs = concat v1 (value2string' g v2 b ws qs)
+  where
+    concat v1 (Const (b,ws,qs)) = value2string' g v1 b ws qs
+    concat v1 (CFV i vs)        = CFV i [concat v1 v2 | v2 <- vs]
+    concat v1 res               = res
+value2string' g (VApp q []) b    ws      qs
+  | q == (cPredef,cNonExist)              = NonExist
+value2string' g (VApp q []) b    ws      qs
+  | q == (cPredef,cSOFT_SPACE)            = if null ws
+                                              then Const (b,ws,q:qs)
+                                              else Const (b,ws,qs)
+value2string' g (VApp q []) b     ws     qs
+  | q == (cPredef,cBIND) || q == (cPredef,cSOFT_BIND) 
+                                          = if null ws
+                                              then Const (True,ws,q:qs)
+                                              else Const (True,ws,qs)
+value2string' g (VApp q []) b     ws     qs
+  | q == (cPredef,cCAPIT) = capit ws
+  where
+    capit []            = Const (b,[],q:qs)
+    capit ((c:cs) : ws) = Const (b,(toUpper c : cs) : ws,qs)
+    capit ws            = Const (b,ws,qs)
+value2string' g (VApp q []) b     ws     qs
+  | q == (cPredef,cALL_CAPIT) = all_capit ws
+  where
+    all_capit []       = Const (b,[],q:qs)
+    all_capit (w : ws) = Const (b,map toUpper w : ws,qs)
+value2string' g (VAlts vd vas) b  ws     qs =
+  case ws of
+    []    -> value2string' g vd b ws qs
+    (w:_) -> pre vd vas w b ws qs
+  where
+    pre vd []                 w            = value2string' g vd
+    pre vd ((v,VStrs ss):vas) w
+      | or [startsWith s w | VStr s <- ss] = value2string' g v
+      | otherwise                          = pre vd vas w
+value2string' g (VFV s vs) b      ws     qs =
+  CFV s [value2string' g v b ws qs | v <- vs]
+value2string' _ _ _ _ _ = RunTime
+
+startsWith []          _ = True
+startsWith (x:xs) (y:ys)
+  | x == y               = startsWith xs ys
+startsWith      _      _ = False
+
+string2value s = string2value' (words s)
+
+string2value' []     = VEmpty
+string2value' [w]    = VStr w
+string2value' (w:ws) = VC (VStr w) (string2value' ws)
+
+value2int g (VMeta i vs)     = CSusp i (\v -> value2int g (apply g v vs))
+value2int g (VSusp i k vs)   = CSusp i (\v -> value2int g (apply g (k v) vs))
+value2int g (VInt n)         = Const n
+value2int g (VFV s vs)       = CFV s (map (value2int g) vs)
+value2int g _                = RunTime
+
+newtype Choice = Choice Integer deriving (Eq,Ord,Pretty)
+
+unit :: Choice
+unit = Choice 1
+
+split :: Choice -> (Choice,Choice)
+split (Choice c) = (Choice (2*c), Choice (2*c+1))
+
+split4 :: Choice -> (Choice,Choice,Choice,Choice)
+split4 (Choice c) = (Choice (4*c), Choice (4*c+1), Choice (4*c+2), Choice (4*c+3))
+
+mapC :: (Choice -> a -> b) -> Choice -> [a] -> [b]
+mapC f c []     = []
+mapC f c [x]    = [f c x]
+mapC f c (x:xs) =
+  let (!c1,!c2) = split c
+  in f c1 x : mapC f c2 xs
+
+mapCM :: Monad m => (Choice -> a -> m b) -> Choice -> [a] -> m [b]
+mapCM f c []     = return []
+mapCM f c [x]    = do y <- f c x
+                      return [y]
+mapCM f c (x:xs) = do
+  let (!c1,!c2) = split c
+  y  <- f c1 x
+  ys <- mapCM f c2 xs
+  return (y:ys)
+
+pdArity :: Int -> PredefCombinator Value
+pdArity n def = \g c args ->
+  case splitAt' n args of
+    Nothing -> RunTime
+    Just (usedArgs, remArgs) ->
+      fmap (\v -> apply g v remArgs) (def g c usedArgs)
+  where
+    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)))
diff --git a/src/compiler/api/GF/Compile/Repl.hs b/src/compiler/api/GF/Compile/Repl.hs
index f3b748361..b13dde7be 100644
--- a/src/compiler/api/GF/Compile/Repl.hs
+++ b/src/compiler/api/GF/Compile/Repl.hs
@@ -15,7 +15,7 @@ import System.Console.Haskeline (InputT, Settings(..), noCompletion, runInputT,
 import System.Directory (getAppUserDataDirectory)
 
 import GF.Compile (batchCompile)
-import GF.Compile.Compute.Concrete (Globals(Gl), stdPredef, normalFlatForm)
+import GF.Compile.Compute.Concrete2 (Globals(Gl), stdPredef, normalFlatForm)
 import GF.Compile.Rename (renameSourceTerm)
 import GF.Compile.TypeCheck.ConcreteNew (inferLType)
 import GF.Data.ErrM (Err(..))
@@ -30,7 +30,7 @@ import GF.Grammar.Grammar
   , ModuleStatus(MSComplete)
   , OpenSpec(OSimple)
   , Location (NoLoc)
-  , Term
+  , Term(Typed)
   , prependModule
   )
 import GF.Grammar.Lexer (Posn(..), Lang(GF), runLangP)
@@ -99,8 +99,12 @@ runRepl' gl@(Gl g _) = do
 
     command "t" arg = do
       parseThen g arg $ \main ->
-        execCheck (inferLType gl main) $ \(_, ty) ->
-          outputStrLn $ render (ppTerm Unqualified 0 ty)
+        execCheck (inferLType gl main) $ \res ->
+          forM_ res $ \(t, ty) ->
+            let t' = case t of
+                       Typed _ _ -> t
+                       t         -> Typed t ty
+            in outputStrLn $ render (ppTerm Unqualified 0 t')
       outputStrLn "" >> repl
     
     command "q" _ = outputStrLn "Bye!"
@@ -111,7 +115,7 @@ runRepl' gl@(Gl g _) = do
 
     evalPrintLoop code = do -- TODO bindings
       parseThen g code $ \main ->
-        execCheck (inferLType gl main >>= \(t, _) -> normalFlatForm gl t) $ \nfs ->
+        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
@@ -138,4 +142,5 @@ runRepl (ReplOpts noPrelude inputFiles) = do
       , mseqs   = Nothing
       , jments  = Map.empty
       }
-  runRepl' (Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef))
+    g = Gl (prependModule g0 (replModName, modInfo)) (if noPrelude then Map.empty else stdPredef g)
+  runRepl' g
diff --git a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
index f4ceef45d..c7cb917dd 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -1,16 +1,16 @@
 {-# LANGUAGE RankNTypes, CPP, TupleSections, LambdaCase #-}
-module GF.Compile.TypeCheck.ConcreteNew( checkLType, checkLType', inferLType, inferLType' ) where
+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.
 -- Practical type inference for arbitrary-rank types.
 -- 14 September 2011
 
-import GF.Grammar hiding (Env, VGen, VApp, VRecType)
+import GF.Grammar hiding (Env, VGen, VApp, VRecType, ppValue)
 import GF.Grammar.Lookup
 import GF.Grammar.Predef
 import GF.Grammar.Lockfield
-import GF.Compile.Compute.Concrete
+import GF.Compile.Compute.Concrete2
 import GF.Infra.CheckM
 import GF.Data.ErrM ( Err(Ok, Bad) )
 import Control.Applicative(Applicative(..))
@@ -24,29 +24,34 @@ 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 (checkLType' t ty)
+checkLType :: Globals -> Term -> Type -> Check [(Term, Type)]
+checkLType globals t ty = runEvalM globals $
+  do let (c1,c2) = split unit
+     (t,vty) <- checkLType' c1 t (eval globals [] c2 ty [])
+     ty <- value2termM True [] vty
+     return (t,ty)
 
-checkLType' :: Term -> Type -> EvalM s (Term, Type)
-checkLType' t ty = do
-  vty <- eval [] ty []
-  (t,_) <- tcRho [] t (Just vty)
+checkLType' :: Choice -> Term -> Constraint -> EvalM (Term, Constraint)
+checkLType' c t vty = do
+  (t,vty) <- tcRho [] c t (Just vty)
   t <- zonkTerm [] t
+  return (t,vty)
+
+inferLType :: Globals -> Term -> Check [(Term, Type)]
+inferLType globals t = runEvalM globals $ do
+  (t,vty) <- inferLType' t
+  ty <- value2termM True [] vty
   return (t,ty)
 
-inferLType :: Globals -> Term -> Check (Term, Type)
-inferLType globals t = runEvalOneM globals (inferLType' t)
-
-inferLType' :: Term -> EvalM s (Term, Type)
+inferLType' :: Term -> EvalM (Term, Constraint)
 inferLType' t = do
-  (t,ty) <- inferSigma [] t
-  t  <- zonkTerm [] t
-  ty <- value2term False [] ty
-  return (t,ty)
+  (t,vty) <- inferSigma [] unit t
+  t <- zonkTerm [] t
+  return (t,vty)
 
-inferSigma :: Scope s -> Term -> EvalM s (Term,Sigma s)
-inferSigma scope t = do                                      -- GEN1
-  (t,ty) <- tcRho scope t Nothing
+inferSigma :: Scope -> Choice -> Term -> EvalM (Term,Sigma)
+inferSigma scope s t = do                                      -- GEN1
+  (t,ty) <- tcRho scope s t Nothing
   env_tvs <- getMetaVars (scopeTypes scope)
   res_tvs <- getMetaVars [(scope,ty)]
   let forall_tvs = res_tvs \\ env_tvs
@@ -54,35 +59,38 @@ inferSigma scope t = do                                      -- GEN1
 
 vtypeInt   = VApp (cPredef,cInt) []
 vtypeFloat = VApp (cPredef,cFloat) []
-vtypeInts i= newEvaluatedThunk (VInt i) >>= \tnk -> return (VApp (cPredef,cInts) [tnk])
+vtypeInts i= VApp (cPredef,cInts) [VInt i]
 vtypeStr   = VSort cStr
 vtypeStrs  = VSort cStrs
 vtypeType  = VSort cType
 vtypePType = VSort cPType
 vtypeMarkup= VApp (cPredef,cMarkup) []
 
-tcRho :: Scope s -> Term -> Maybe (Rho s) -> EvalM s (Term, Rho s)
-tcRho scope t@(EInt i)   mb_ty = vtypeInts i >>= \sigma -> instSigma scope t sigma mb_ty -- INT
-tcRho scope t@(EFloat _) mb_ty = instSigma scope t vtypeFloat mb_ty    -- FLOAT
-tcRho scope t@(K _)      mb_ty = instSigma scope t vtypeStr   mb_ty    -- STR
-tcRho scope t@(Empty)    mb_ty = instSigma scope t vtypeStr   mb_ty
-tcRho scope t@(Vr v)     mb_ty = do                          -- VAR
+tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho)
+tcRho scope s t@(EInt i)   mb_ty = instSigma scope s t (vtypeInts i) mb_ty -- INT
+tcRho scope s t@(EFloat _) mb_ty = instSigma scope s t vtypeFloat mb_ty    -- FLOAT
+tcRho scope s t@(K _)      mb_ty = instSigma scope s t vtypeStr   mb_ty    -- STR
+tcRho scope s t@(Empty)    mb_ty = instSigma scope s t vtypeStr   mb_ty
+tcRho scope s t@(Vr v)     mb_ty = do                          -- VAR
   case lookup v scope of
-    Just v_sigma -> instSigma scope t v_sigma mb_ty
+    Just v_sigma -> instSigma scope s t v_sigma mb_ty
     Nothing      -> evalError ("Unknown variable" <+> v)
-tcRho scope t@(Q id)     mb_ty = do
-  (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 []
-  instSigma scope t ty mb_ty
-tcRho scope t@(App fun arg) mb_ty = do
-  (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
-  let arg_ty = VMeta tnk []
-  (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing
+tcRho scope c t@(Q id)     mb_ty = do
+  let (c1,c2) = split c
+  (t,ty) <- tcApp scope c1 t t []
+  instSigma scope c2 t ty mb_ty
+tcRho scope c t@(QC id)    mb_ty = do
+  let (c1,c2) = split c
+  (t,ty) <- tcApp scope c1 t t []
+  instSigma scope c2 t ty mb_ty
+tcRho scope c t@(App fun arg) mb_ty = do
+  let (c1,c2) = split c
+  (t,ty) <- tcApp scope c1 t t []
+  instSigma scope c2 t ty mb_ty
+tcRho scope c (Abs bt var body) Nothing = do                   -- ABS1
+  i <- newResiduation scope
+  let arg_ty = VMeta i []
+  (body,body_ty) <- tcRho ((var,arg_ty):scope) c body Nothing
   let m = length scope
       n = m+1
   (b,used_bndrs) <- check m n (False,[]) body_ty
@@ -91,44 +99,42 @@ tcRho scope (Abs bt var body) Nothing = do                   -- ABS1
          in return (Abs bt var body, (VProd bt v arg_ty body_ty))
     else return (Abs bt var body, (VProd bt identW arg_ty body_ty))
   where
-    check m n st (VApp f vs)       = foldM (follow m n) st vs
+    check m n st (VApp f vs)       = foldM (check m n) st vs
     check m n st (VMeta i vs)      = do
-      s <- getRef i
-      case s of
-        Evaluated _ v -> do v <- apply v vs
-                            check m n st v
-        _             -> foldM (follow m n) st vs
+      state <- getMeta i
+      case state of
+        Bound _ v -> do g <- globals
+                        check m n st (apply g v vs)
+        _         -> foldM (check m n) st vs
     check m n st@(b,xs) (VGen i vs)
       | i == m                     = return (True, xs)
       | otherwise                  = return st
-    check m n st (VClosure env (Abs bt x t)) = do
-      tnk <- newEvaluatedThunk (VGen n [])
-      v <- eval ((x,tnk):env) t []
-      check m (n+1) st v
+    check m n st (VClosure env c (Abs bt x t)) = do
+      g <- globals
+      check m (n+1) st (eval g ((x,VGen n []):env) c t [])
     check m n st (VProd _ x v1 v2) = do
       st@(b,xs) <- check m n st v1
       case v2 of
-        VClosure env t -> do tnk <- newEvaluatedThunk (VGen n [])
-                             v2 <- eval ((x,tnk):env) t []
-                             check m (n+1) (b,x:xs) v2
-        v2             -> check m n st v2
+        VClosure env c t -> do g  <- globals
+                               check m (n+1) (b,x:xs) (eval g ((x,VGen n []):env) c t [])
+        v2               -> check m n st 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
+      foldM (\st (lbl,tnk) -> check m n st tnk) st as
     check m n st (VP v l vs)       =
-      check m n st v >>= \st -> foldM (follow m n) st vs
+      check m n st v >>= \st -> foldM (check m n) st vs
     check m n st (VExtR v1 v2)     =
       check m n st v1 >>= \st -> check m n st v2
     check m n st (VTable v1 v2)    =
       check m n st v1 >>= \st -> check m n st v2
-    check m n st (VT ty env cs)    =
+    check m n st (VT ty env c cs)    =
       check m n st ty    -- Traverse cs as well
     check m n st (VV ty cs)        =
-      check m n st ty >>= \st -> foldM (follow m n) st cs
+      check m n st ty >>= \st -> foldM (check m n) st cs
     check m n st (VS v1 tnk vs)    = do
       st <- check m n st v1
-      st <- follow m n st tnk
-      foldM (follow m n) st vs
+      st <- check m n st tnk
+      foldM (check m n) st vs
     check m n st (VSort _)         = return st
     check m n st (VInt _)          = return st
     check m n st (VFlt _)          = return st
@@ -145,398 +151,464 @@ tcRho scope (Abs bt var body) Nothing = do                   -- ABS1
       foldM (\st (v1,v2) -> check m n st v1 >>= \st -> check m n st v2) st vs
     check m n st (VStrs vs)        =
       foldM (check m n) st vs
-    check m n st v                 = error (showValue v)
-
-    follow m n st tnk = force tnk >>= \v -> check m n st v
-
-tcRho scope t@(Abs Implicit var body) (Just ty) = do         -- ABS2
+tcRho scope c t@(Abs Implicit var body) (Just ty) = do         -- ABS2
   (bt, x, var_ty, body_ty) <- unifyFun scope ty
   if bt == Implicit
     then return ()
     else evalError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
   body_ty <- evalCodomain scope x body_ty
-  (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
+  (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty)
   return (Abs Implicit var body,ty)
-tcRho scope (Abs Explicit var body) (Just ty) = do           -- ABS3
+tcRho scope c (Abs Explicit var body) (Just ty) = do           -- ABS3
   (scope,f,ty') <- skolemise scope ty
   (_,x,var_ty,body_ty) <- unifyFun scope ty'
   body_ty <- evalCodomain scope x body_ty
-  (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
+  (body, body_ty) <- tcRho ((var,var_ty):scope) c body (Just body_ty)
   return (f (Abs Explicit var body),ty)
-tcRho scope (Meta _) mb_ty = do
-  (i,_) <- newResiduation scope
+tcRho scope c (Meta _) mb_ty = do
+  i <- newResiduation scope
   ty <- case mb_ty of
           Just ty -> return ty
-          Nothing -> do (_,tnk) <- newResiduation scope
-                        return (VMeta tnk [])
+          Nothing -> do j <- newResiduation scope
+                        return (VMeta j [])
   return (Meta i, ty)
-tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do    -- LET
-  (rhs,var_ty) <- case mb_ann_ty of
-                    Nothing     -> tcRho scope rhs Nothing
-                    Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
-                                      env <- scopeEnv scope
-                                      v_ann_ty <- eval env ann_ty []
-                                      (rhs,_) <- tcRho scope rhs (Just v_ann_ty)
-                                      return (rhs, v_ann_ty)
-  (body, body_ty) <- tcRho ((var,var_ty):scope) body mb_ty
-  var_ty <- value2term True (scopeVars scope) var_ty
+tcRho scope c (Let (var, (Nothing, rhs)) body) mb_ty = do      -- LET
+  let (c1,c2) = split c
+  (rhs,var_ty) <- tcRho scope c1 rhs Nothing
+  (body, body_ty) <- tcRho ((var,var_ty):scope) c2 body mb_ty
+  var_ty <- value2termM True (scopeVars scope) var_ty
   return (Let (var, (Just var_ty, rhs)) body, body_ty)
-tcRho scope (Typed body ann_ty) mb_ty = do                   -- ANNOT
-  (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
-  env <- scopeEnv scope
-  v_ann_ty <- eval env ann_ty []
-  (body,_) <- tcRho scope body (Just v_ann_ty)
-  (res1,res2) <- instSigma scope (Typed body ann_ty) v_ann_ty mb_ty
-  return (res1,res2)
-tcRho scope (FV ts) mb_ty = do
+tcRho scope c (Let (var, (Just ann_ty, rhs)) body) mb_ty = do  -- LET
+  let (c1,c2,c3,c4) = split4 c
+  (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType)
+  g <- globals
+  let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty []
+  (rhs,_) <- tcRho scope c3 rhs (Just v_ann_ty)
+  (body, body_ty) <- tcRho ((var,v_ann_ty):scope) c4 body mb_ty
+  var_ty <- value2termM True (scopeVars scope) v_ann_ty
+  return (Let (var, (Just var_ty, rhs)) body, body_ty)
+tcRho scope c (Typed body ann_ty) mb_ty = do                   -- ANNOT
+  let (c1,c2,c3,c4) = split4 c
+  (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType)
+  g <- globals
+  let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty []
+  (body,_) <- tcRho scope c3 body (Just v_ann_ty)
+  instSigma scope c4 (Typed body ann_ty) v_ann_ty mb_ty
+tcRho scope c (FV ts) mb_ty = do
   (ty,subsume) <-
     case mb_ty of
       Just ty -> do return (ty, \t ty' -> return t)
-      Nothing -> do (i,tnk) <- newResiduation scope
-                    let ty = VMeta tnk []
+      Nothing -> do i <- newResiduation scope
+                    let ty = VMeta i []
                     return (ty, \t ty' -> subsCheckRho scope t ty' ty)
 
-  let go t = do (t, ty) <- tcRho scope t mb_ty
-                subsume t ty
+  let go c t = do (t, ty) <- tcRho scope c t mb_ty
+                  subsume t ty
 
-  ts <- mapM go ts
+  ts <- mapCM go c ts
   return (FV ts, ty)
-tcRho scope t@(Sort s) mb_ty = do
-  instSigma scope t vtypeType mb_ty
-tcRho scope t@(RecType rs) Nothing   = do
-  (rs,mb_ty) <- tcRecTypeFields scope rs Nothing
+tcRho scope s t@(Sort _) mb_ty = do
+  instSigma scope s t vtypeType mb_ty
+tcRho scope c t@(RecType rs) Nothing   = do
+  (rs,mb_ty) <- tcRecTypeFields scope c rs Nothing
   return (RecType rs,fromMaybe vtypePType mb_ty)
-tcRho scope t@(RecType rs) (Just ty) = do
+tcRho scope c t@(RecType rs) (Just ty) = do
   (scope,f,ty') <- skolemise scope ty
   case ty' of
     VSort s
       | s == cType  -> return ()
       | s == cPType -> return ()
-    VMeta i vs  -> case rs of
-                     [] -> unifyVar scope i vs vtypePType
-                     _  -> return ()
-    ty          -> do ty <- value2term False (scopeVars scope) ty
-                      evalError ("The record type" <+> ppTerm Unqualified 0 t $$
-                                 "cannot be of type" <+> ppTerm Unqualified 0 ty)
-  (rs,mb_ty) <- tcRecTypeFields scope rs (Just ty')
+    VMeta i vs-> case rs of
+                   [] -> unifyVar scope i vs vtypePType
+                   _  -> return ()
+    ty        -> do ty <- value2termM False (scopeVars scope) ty
+                    evalError ("The record type" <+> ppTerm Unqualified 0 t $$
+                               "cannot be of type" <+> ppTerm Unqualified 0 ty)
+  (rs,mb_ty) <- tcRecTypeFields scope c rs (Just ty')
   return (f (RecType rs),ty)
-tcRho scope t@(Table p res) mb_ty = do
-  (p,  p_ty)   <- tcRho scope p   (Just vtypePType)
-  (res,res_ty) <- tcRho scope res (Just vtypeType)
-  instSigma scope (Table p res) vtypeType mb_ty
-tcRho scope (Prod bt x ty1 ty2) mb_ty = do
-  (ty1,ty1_ty) <- tcRho scope ty1 (Just vtypeType)
-  env <- scopeEnv scope
-  vty1 <- eval env ty1 []
-  (ty2,ty2_ty) <- tcRho ((x,vty1):scope) ty2 (Just vtypeType)
-  instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty
-tcRho scope (S t p) mb_ty = do
-  let mk_val (_,tnk) = VMeta tnk []
+tcRho scope s t@(Table p res) mb_ty = do
+  let (s1,s23) = split s
+      (s2,s3)  = split s23
+  (p,  p_ty)   <- tcRho scope s1 p   (Just vtypePType)
+  (res,res_ty) <- tcRho scope s2 res (Just vtypeType)
+  instSigma scope s3 (Table p res) vtypeType mb_ty
+tcRho scope c (Prod bt x ty1 ty2) mb_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  (ty1,ty1_ty) <- tcRho scope c1 ty1 (Just vtypeType)
+  g <- globals
+  (ty2,ty2_ty) <- tcRho ((x,eval g (scopeEnv scope) c2 ty1 []):scope) c3 ty2 (Just vtypeType)
+  instSigma scope c4 (Prod bt x ty1 ty2) vtypeType mb_ty
+tcRho scope c (S t p) mb_ty = do
+  let (c1,c2) = split c
+  let mk_val i = VMeta i []
   p_ty   <- fmap mk_val $ newResiduation scope
   res_ty <- case mb_ty of
               Nothing -> fmap mk_val $ newResiduation scope
               Just ty -> return ty
   let t_ty = VTable p_ty res_ty
-  (t,t_ty) <- tcRho scope t (Just t_ty)
-  (p,_) <- tcRho scope p (Just p_ty)
+  (t,t_ty) <- tcRho scope c1 t (Just t_ty)
+  (p,_) <- tcRho scope c2 p (Just p_ty)
   return (S t p, res_ty)
-tcRho scope (T tt ps) Nothing = do                           -- ABS1/AABS1 for tables
-  let mk_val (_,tnk) = VMeta tnk []
+tcRho scope c (T tt ps) Nothing = do                           -- ABS1/AABS1 for tables
+  let (c1,c2) = split c
+  let mk_val i = VMeta i []
   p_ty   <- case tt of
               TRaw      -> fmap mk_val $ newResiduation scope
-              TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType)
-                              env <- scopeEnv scope
-                              eval env ty []
+              TTyped ty -> do let (c3,c4) = split c1
+                              (ty, _) <- tcRho scope c3 ty (Just vtypeType)
+                              g <- globals
+                              return (eval g (scopeEnv scope) c4 ty [])
   res_ty <- fmap mk_val $ newResiduation scope
-  ps <- tcCases scope ps p_ty res_ty
-  p_ty_t <- value2term True [] p_ty
+  ps <- tcCases scope c2 ps p_ty res_ty
+  p_ty_t <- value2termM True [] p_ty
   return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
-tcRho scope (T tt ps) (Just ty) = do                         -- ABS2/AABS2 for tables
+tcRho scope c (T tt ps) (Just ty) = do                         -- ABS2/AABS2 for tables
+  let (c12,c34) = split c
+      (c3,c4)   = split c34
   (scope,f,ty') <- skolemise scope ty
   (p_ty, res_ty) <- unifyTbl scope ty'
   case tt of
     TRaw      -> return ()
-    TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType)
-                    env <- scopeEnv scope
-                    ty <- eval env ty []
-                    unify scope ty p_ty
-  ps <- tcCases scope ps p_ty res_ty
-  p_ty_t <- value2term True (scopeVars scope) p_ty
+    TTyped ty -> do let (c1,c2) = split c12
+                    (ty, _) <- tcRho scope c1 ty (Just vtypeType)
+                    g <- globals
+                    unify scope (eval g (scopeEnv scope) c2 ty []) p_ty
+  ps <- tcCases scope c3 ps p_ty res_ty
+  p_ty_t <- value2termM True (scopeVars scope) p_ty
   return (f (T (TTyped p_ty_t) ps), VTable p_ty res_ty)
-tcRho scope (V p_ty ts) Nothing = do
-  (p_ty, _) <- tcRho scope p_ty (Just vtypeType)
-  (i,tnk) <- newResiduation scope
-  let res_ty = VMeta tnk []
+tcRho scope c (V p_ty ts) Nothing = do
+  let (c1,c2,c3,c4) = split4 c
+  (p_ty, _) <- tcRho scope c1 p_ty (Just vtypeType)
+  i <- newResiduation scope
+  let res_ty = VMeta i []
 
-  let go t = do (t, ty) <- tcRho scope t Nothing
-                subsCheckRho scope t ty res_ty
+  let go c t = do (t, ty) <- tcRho scope c t Nothing
+                  subsCheckRho scope t ty res_ty
 
-  ts <- mapM go ts
-  env <- scopeEnv scope
-  p_vty <- eval env p_ty []
-  return (V p_ty ts, VTable p_vty res_ty)
-tcRho scope (V p_ty0 ts) (Just ty) = do
+  ts <- mapCM go c2 ts
+  g <- globals
+  return (V p_ty ts, VTable (eval g (scopeEnv scope) c3 p_ty []) res_ty)
+tcRho scope c (V p_ty0 ts) (Just ty) = do
+  let (c1,c2,c3,c4) = split4 c
   (scope,f,ty') <- skolemise scope ty
   (p_ty, res_ty) <- unifyTbl scope ty'
-  (p_ty0, _) <- tcRho scope p_ty0 (Just vtypeType)
-  env <- scopeEnv scope
-  p_vty0 <- eval env p_ty0 []
+  (p_ty0, _) <- tcRho scope c1 p_ty0 (Just vtypeType)
+  g <- globals
+  let p_vty0 = eval g (scopeEnv scope) c2 p_ty0 []
   unify scope p_ty p_vty0
-  ts <- mapM (\t -> fmap fst $ tcRho scope t (Just res_ty)) ts
+  ts <- mapCM (\c t -> fmap fst $ tcRho scope c t (Just res_ty)) c3 ts
   return (V p_ty0 ts, VTable p_ty res_ty)
-tcRho scope (R rs) Nothing = do
-  lttys <- inferRecFields scope rs
-  rs <- mapM (\(l,t,ty) -> value2term True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
+tcRho scope c (R rs) Nothing = do
+  lttys <- inferRecFields scope c rs
+  rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
   return (R        rs,
           VRecType [(l, ty) | (l,t,ty) <- lttys]
          )
-tcRho scope (R rs) (Just ty) = do
+tcRho scope c (R rs) (Just ty) = do
   (scope,f,ty') <- skolemise scope ty
   case ty' of
-    (VRecType ltys) -> do lttys <- checkRecFields scope rs ltys
-                          rs <- mapM (\(l,t,ty) -> value2term True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
+    (VRecType ltys) -> do lttys <- checkRecFields scope c rs ltys
+                          rs <- mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
                           return ((f . R)  rs,
                                   VRecType [(l, ty) | (l,t,ty) <- lttys]
                                  )
-    ty              -> do lttys <- inferRecFields scope rs
-                          t <- liftM (f . R) (mapM (\(l,t,ty) -> value2term True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
+    ty              -> do lttys <- inferRecFields scope c rs
+                          t <- liftM (f . R) (mapM (\(l,t,ty) -> value2termM True (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
                           let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
                           t <- subsCheckRho scope t ty' ty
                           return (t, ty')
-tcRho scope (P t l) mb_ty = do
+tcRho scope c (P t l) mb_ty = do
   l_ty   <- case mb_ty of
               Just ty -> return ty
-              Nothing -> do (i,tnk) <- newResiduation scope
-                            return (VMeta tnk [])
-  (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)]))
+              Nothing -> do i <- newResiduation scope
+                            return (VMeta i [])
+  (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,l_ty)]))
   return (P t l,l_ty)
-tcRho scope (C t1 t2) mb_ty = do
-  (t1,t1_ty) <- tcRho scope t1 (Just vtypeStr)
-  (t2,t2_ty) <- tcRho scope t2 (Just vtypeStr)
-  instSigma scope (C t1 t2) vtypeStr mb_ty
-tcRho scope (Glue t1 t2) mb_ty = do
-  (t1,t1_ty) <- tcRho scope t1 (Just vtypeStr)
-  (t2,t2_ty) <- tcRho scope t2 (Just vtypeStr)
-  instSigma scope (Glue t1 t2) vtypeStr mb_ty
-tcRho scope t@(ExtR t1 t2) mb_ty = do
-  (t1,t1_ty) <- tcRho scope t1 Nothing
-  (t2,t2_ty) <- tcRho scope t2 Nothing
+tcRho scope c (C t1 t2) mb_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr)
+  (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr)
+  instSigma scope c3 (C t1 t2) vtypeStr mb_ty
+tcRho scope c (Glue t1 t2) mb_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  (t1,t1_ty) <- tcRho scope c1 t1 (Just vtypeStr)
+  (t2,t2_ty) <- tcRho scope c2 t2 (Just vtypeStr)
+  instSigma scope c3 (Glue t1 t2) vtypeStr mb_ty
+tcRho scope c t@(ExtR t1 t2) mb_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  (t1,t1_ty) <- tcRho scope c1 t1 Nothing
+  (t2,t2_ty) <- tcRho scope c2 t2 Nothing
   case (t1_ty,t2_ty) of
     (VSort s1,VSort s2)
        | (s1 == cType || s1 == cPType) &&
          (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType
                                                    | otherwise                    = cType
-                                          in instSigma scope (ExtR t1 t2) (VSort sort) mb_ty
-    (VRecType rs1, VRecType rs2)       -> instSigma scope (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty
+                                          in instSigma scope c3 (ExtR t1 t2) (VSort sort) mb_ty
+    (VRecType rs1, VRecType rs2)       -> instSigma scope c3 (ExtR t1 t2) (VRecType (rs2++rs1)) mb_ty
     _                                  -> evalError ("Cannot type check" <+> ppTerm Unqualified 0 t)
-tcRho scope (ELin cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
-  tcRho scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
-tcRho scope (ELincat cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
-  tcRho scope (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
-tcRho scope (Alts t ss) mb_ty = do
-  (t,_) <- tcRho scope t (Just vtypeStr)
-  ss    <- flip mapM ss $ \(t1,t2) -> do
-              (t1,_) <- tcRho scope t1 (Just vtypeStr)
-              (t2,_) <- tcRho scope t2 (Just vtypeStrs)
-              return (t1,t2)
-  instSigma scope (Alts t ss) vtypeStr mb_ty
-tcRho scope (Strs ss) mb_ty = do
-  ss <- flip mapM ss $ \t -> do
-           (t,_) <- tcRho scope t (Just vtypeStr)
-           return t
-  instSigma scope (Strs ss) vtypeStrs mb_ty
-tcRho scope (EPattType ty) mb_ty = do
-  (ty, _) <- tcRho scope ty (Just vtypeType)
-  instSigma scope (EPattType ty) vtypeType mb_ty
-tcRho scope t@(EPatt min max p) mb_ty = do
+tcRho scope c (ELin cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
+  tcRho scope c (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
+tcRho scope c (ELincat cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
+  tcRho scope c (ExtR t (RecType [(lockLabel cat,RecType [])])) mb_ty
+tcRho scope c (Alts t ss) mb_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  (t,_) <- tcRho scope c1 t (Just vtypeStr)
+  ss    <- mapCM (\c (t1,t2) -> do
+                          let (c1,c2) = split c
+                          (t1,_) <- tcRho scope c1 t1 (Just vtypeStr)
+                          (t2,_) <- tcRho scope c2 t2 (Just vtypeStrs)
+                          return (t1,t2))
+                 c2 ss
+  instSigma scope c3 (Alts t ss) vtypeStr mb_ty
+tcRho scope c (Strs ss) mb_ty = do
+  let (c1,c2) = split c
+  ss <- mapCM (\c t -> do (t,_) <- tcRho scope c t (Just vtypeStr)
+                          return t)
+              c1 ss
+  instSigma scope c2 (Strs ss) vtypeStrs mb_ty
+tcRho scope c (EPattType ty) mb_ty = do
+  let (c1,c2) = split c
+  (ty, _) <- tcRho scope c1 ty (Just vtypeType)
+  instSigma scope c2 (EPattType ty) vtypeType mb_ty
+tcRho scope c t@(EPatt min max p) mb_ty = do
   (scope,f,ty) <- case mb_ty of
-                    Nothing -> do (i,tnk) <- newResiduation scope
-                                  return (scope,id,VMeta tnk [])
+                    Nothing -> do i <- newResiduation scope
+                                  return (scope,id,VMeta i [])
                     Just ty -> do (scope,f,ty) <- skolemise scope ty
                                   case ty of
                                     VPattType ty -> return (scope,f,ty)
                                     _            -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
-  tcPatt scope p ty
+  tcPatt scope c p ty
   return (f (EPatt min max p), ty)
-tcRho scope (Markup tag attrs children) mb_ty = do
-  attrs <- forM attrs $ \(id,t) -> do
-              (t,_) <- tcRho scope t Nothing
-              return (id,t)
-  res <- mapM (\child -> tcRho scope child Nothing) children
-  instSigma scope (Markup tag attrs (map fst res)) vtypeMarkup mb_ty
-tcRho scope (Reset c t) mb_ty = do
-  (t,_) <- tcRho scope t Nothing
-  instSigma scope (Reset c t) vtypeMarkup mb_ty
-tcRho scope t _ = unimplemented ("tcRho "++show t)
+tcRho scope c (Markup tag attrs children) mb_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  attrs <- mapCM (\c (id,t) -> do
+                       (t,_) <- tcRho scope c t Nothing
+                       return (id,t))
+                 c1 attrs
+  res <- mapCM (\c child -> tcRho scope c child Nothing) c2 children
+  instSigma scope c3 (Markup tag attrs (map fst res)) vtypeMarkup mb_ty
+tcRho scope c (Reset ctl t) mb_ty = do
+  let (c1,c2) = split c
+  (t,_) <- tcRho scope c1 t Nothing
+  instSigma scope c2 (Reset ctl t) vtypeMarkup mb_ty
+tcRho scope s 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 -> Ident -> Value -> EvalM Value
+evalCodomain scope x (VClosure env c t) = do
+  g <- globals
+  return (eval g ((x,VGen (length scope) []):env) c 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
-  (t,_)  <- tcRho scope' t (Just res_ty)
-  cs <- tcCases scope cs p_ty res_ty
+tcCases scope c []         p_ty res_ty = return []
+tcCases scope c ((p,t):cs) p_ty res_ty = do
+  let (c1,c2,c3,c4) = split4 c
+  scope' <- tcPatt scope c1 p p_ty
+  (t,_)  <- tcRho scope' c2 t (Just res_ty)
+  cs <- tcCases scope c3 cs p_ty res_ty
   return ((p,t):cs)
 
-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
+tcApp scope c t0 (App fun arg) args = tcApp scope c t0 fun (arg:args)     -- APP
+tcApp scope c t0 t@(Q id)      args = resolveOverloads scope c t0 id args -- VAR (global)
+tcApp scope c t0 t@(QC id)     args = resolveOverloads scope c t0 id args -- VAR (global)
+tcApp scope c t0 t             args = do
+  let (c1,c2) = split c
+  (t,ty) <- tcRho scope c1 t Nothing
+  reapply1 scope c2 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
+reapply1 :: Scope -> Choice -> Term -> Value -> [Term] -> EvalM (Term,Rho)
+reapply1 scope c fun fun_ty []                   = return (fun,fun_ty)
+reapply1 scope c fun fun_ty ((ImplArg arg):args) = do -- Implicit arg case
+  let (c1,c2,c3,c4) = split4 c
   (bt, x, arg_ty, res_ty) <- unifyFun scope fun_ty
-  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)
+  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 c1 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
-  reapply scope (App fun (ImplArg arg)) res_ty args
-reapply scope fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case
+              VClosure res_env res_c res_ty -> do g <- globals
+                                                  return (eval g ((x,eval g (scopeEnv scope) c2 arg []):res_env) res_c res_ty [])
+              res_ty                        -> return res_ty
+  reapply1 scope c3 (App fun (ImplArg arg)) res_ty args
+reapply1 scope c fun fun_ty (arg:args) = do -- Explicit arg (fallthrough) case
+  let (c1,c2,c3,c4) = split4 c
   (fun,fun_ty) <- instantiate scope fun fun_ty
   (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty
-  (arg,_) <- tcRho scope arg (Just arg_ty)
+  (arg,_) <- tcRho scope c1 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 []
+              VClosure res_env res_c res_ty -> do g <- globals
+                                                  return (eval g ((x,eval g (scopeEnv scope) c2 arg []):res_env) res_c res_ty [])
               res_ty                  -> return res_ty
-  reapply scope (App fun arg) res_ty args
+  reapply1 scope c3 (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 ->
+resolveOverloads :: Scope -> Choice -> Term -> QIdent -> [Term] -> EvalM (Term,Rho)
+resolveOverloads scope c t0 q args = do
+  g@(Gl gr _) <- globals
   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
+    Bad msg  -> evalError (pp msg)
+    Ok [(t,ty)] -> do let (c1,c2) = split c
+                      reapply1 scope c1 t (eval g [] c2 ty []) args
+    Ok ttys     -> do let (c1,c2) = split c
+                      arg_tys <- mapCM (checkArg g) c1 args
+                      let v_ttys = mapC (\c (t,ty) -> (t,eval g [] c ty [])) c2 ttys
+                      try (\(fun,fun_ty) -> reapply2 scope fun fun_ty arg_tys) v_ttys (pp "Overload resolution failed")
   where
-    try (t,ty) = case eval [] ty [] >>= \vty -> reapply scope t vty args of EvalM f -> f
+    checkArg g c (ImplArg arg) = do
+      let (c1,c2) = split c
+      (arg,arg_ty) <- tcRho scope c1 arg Nothing
+      let v = eval g (scopeEnv scope) c2 arg []
+      return (ImplArg arg,v,arg_ty)
+    checkArg g c arg = do
+      let (c1,c2) = split c
+      (arg,arg_ty) <- tcRho scope c1 arg Nothing
+      let v = eval g (scopeEnv scope) c2 arg []
+      return (arg,v,arg_ty)
 
-    isSuccess (tty, Success r msg) = Just (tty,r,msg)
-    isSuccess (_, Fail _ _)        = Nothing
+reapply2 :: Scope -> Term -> Value -> [(Term,Value,Value)] -> EvalM (Term,Rho)
+reapply2 scope fun fun_ty []                                = return (fun,fun_ty)
+reapply2 scope fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) = do -- Implicit arg case
+  (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty
+  unless (bt == Implicit) $
+     evalError (ppTerm Unqualified 0 (App fun (ImplArg arg)) <+>
+                "is an implicit argument application, but no implicit argument is expected")
+  arg <- subsCheckRho scope arg arg_ty' arg_ty
+  res_ty <- case res_ty of
+              VClosure res_env res_c res_ty -> do g <- globals
+                                                  return (eval g ((x,arg_v):res_env) res_c res_ty [])
+              res_ty                        -> return res_ty
+  reapply2 scope (App fun (ImplArg arg)) res_ty args
+reapply2 scope fun fun_ty ((arg,arg_v,arg_ty):args) = do -- Explicit arg (fallthrough) case
+  (fun,fun_ty) <- instantiate scope fun fun_ty
+  (_, x, arg_ty', res_ty) <- unifyFun scope fun_ty
+  arg <- subsCheckRho scope arg arg_ty arg_ty'
+  res_ty <- case res_ty of
+              VClosure res_env res_c res_ty -> do g <- globals
+                                                  return (eval g ((x,arg_v):res_env) res_c res_ty [])
+              res_ty                  -> return res_ty
+  reapply2 scope (App fun arg) res_ty args
 
-    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)
+{-tcApp scope c t0 t@(App fun (ImplArg arg)) = do                  -- APP1
+  let (c1,c2,c3,c4) = split4 c
+  (fun,fun_ty) <- tcApp scope c1 t0 fun
+  (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")
+  (arg,_) <- tcRho scope c2 arg (Just arg_ty)
+  res_ty <- case res_ty of
+              VClosure res_env res_c res_ty -> do g <- globals
+                                                  return (eval g ((x,eval g (scopeEnv scope) c3 arg []):res_env) res_c res_ty [])
+              res_ty                        -> return res_ty
+  return (App fun (ImplArg arg), res_ty)
+tcApp scope c t0 (App fun arg) = do                              -- APP2
+  let (c1,c2,c3,c4) = split4 c
+  (fun,fun_ty) <- tcApp scope c1 t0 fun
+  (fun,fun_ty) <- instantiate scope fun fun_ty
+  (_, x, arg_ty, res_ty) <- unifyFun scope fun_ty
+  (arg,_) <- tcRho scope c2 arg (Just arg_ty)
+  g <- globals
+  let res_ty' = foo g (x,eval g (scopeEnv scope) c3 arg []) res_ty
+  return (App fun arg, res_ty')
+  where
+    foo g arg (VClosure env c res_ty) = eval g (arg:env) c res_ty []
+    foo g arg (VFV c vs)              = VFV c (map (foo g arg) vs)
+    foo g arg res_ty                  = res_ty
+tcApp scope c t0 (Q id)        = getOverloads scope c t0 id -- VAR (global)
+tcApp scope c t0 (QC id)       = getOverloads scope c t0 id -- VAR (global)
+tcApp scope c t0 t             = tcRho scope c t Nothing
+-}
+getOverloads :: Scope -> Choice -> Term -> QIdent -> EvalM (Term,Rho)
+getOverloads scope c t q = do
+  g@(Gl gr _) <- globals
+  case lookupOverloadTypes gr q of
+    Bad msg     -> evalError (pp msg)
+    Ok [(t,ty)] -> return (t, eval g [] c ty [])
+    Ok ttys    -> do let (c1,c2,c3,c4) = split4 c
+                         vs   = mapC (\c (t,ty) -> eval g [] c t  []) c1 ttys
+                         vtys = mapC (\c (t,ty) -> eval g [] c ty []) c2 ttys
+                     i <- newBinding (VFV c3 vs)
+                     return (Meta i, VFV c3 vtys)
 
-    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 =
+tcPatt scope c PW        ty0 =
   return scope
-tcPatt scope (PV x)    ty0 =
+tcPatt scope c (PV x)    ty0 =
   return ((x,ty0):scope)
-tcPatt scope (PP c ps) ty0 = do
-  ty <- getResType c
-  let go scope ty []     = return (scope,ty)
-      go scope ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty
-                              scope <- tcPatt scope p arg_ty
-                              go scope res_ty ps
-  vty <- eval [] ty []
-  (scope,ty) <- go scope vty ps
+tcPatt scope c (PP q ps) ty0 = do
+  g@(Gl gr _) <- globals
+  ty <- case lookupResType gr q of
+          Ok ty   -> return ty
+          Bad msg -> evalError (pp msg)
+  let go scope c ty []     = return (scope,ty)
+      go scope c ty (p:ps) = do (_,_,arg_ty,res_ty) <- unifyFun scope ty
+                                let (c1,c2) = split c
+                                scope <- tcPatt scope c1 p arg_ty
+                                go scope c2 res_ty ps
+  let (c1,c2) = split c
+  (scope,ty) <- go scope c1 (eval g [] c2 ty []) ps
   unify scope ty0 ty
   return scope
-tcPatt scope (PInt i) ty0 = do
-  ty <- vtypeInts i
-  unify scope ty ty0
+tcPatt scope c (PInt i) ty0 = do
+  unify scope (vtypeInts i) ty0
   return scope
-tcPatt scope (PString s) ty0 = do
+tcPatt scope c (PString s) ty0 = do
   unify scope ty0 vtypeStr
   return scope
-tcPatt scope PChar ty0 = do
+tcPatt scope c PChar ty0 = do
   unify scope ty0 vtypeStr
   return scope
-tcPatt scope (PSeq _ _ p1 _ _ p2) ty0 = do
+tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do
   unify scope ty0 vtypeStr
-  scope <- tcPatt scope p1 vtypeStr
-  scope <- tcPatt scope p2 vtypeStr
+  let (c1,c2) = split c
+  scope <- tcPatt scope c1 p1 vtypeStr
+  scope <- tcPatt scope c2 p2 vtypeStr
   return scope
-tcPatt scope (PAs x p) ty0 = do
-  tcPatt ((x,ty0):scope) p ty0
-tcPatt scope (PR rs) ty0 = do
-  let mk_ltys  []            = return []
-      mk_ltys  ((l,p):rs)    = do (_,tnk) <- newResiduation scope
-                                  ltys <- mk_ltys rs
-                                  return ((l,p,VMeta tnk []) : ltys)
-      go scope []            = return scope
-      go scope ((l,p,ty):rs) = do scope <- tcPatt scope p ty
-                                  go scope rs
+tcPatt scope c (PAs x p) ty0 = do
+  tcPatt ((x,ty0):scope) c p ty0
+tcPatt scope c (PR rs) ty0 = do
+  let mk_ltys []            = return []
+      mk_ltys ((l,p):rs)    = do i <- newResiduation scope
+                                 ltys <- mk_ltys rs
+                                 return ((l,p,VMeta i []) : ltys)
+      go scope c []            = return scope
+      go scope c ((l,p,ty):rs) = do let (c1,c2) = split c
+                                    scope <- tcPatt scope c1 p ty
+                                    go scope c2 rs
   ltys <- mk_ltys rs
   subsCheckRho scope (EPatt 0 Nothing (PR rs)) (VRecType [(l,ty) | (l,p,ty) <- ltys]) ty0
-  go scope ltys
-tcPatt scope (PAlt p1 p2) ty0 = do
-  tcPatt scope p1 ty0
-  tcPatt scope p2 ty0
+  go scope c ltys
+tcPatt scope c (PAlt p1 p2) ty0 = do
+  let (c1,c2) = split c
+  tcPatt scope c1 p1 ty0
+  tcPatt scope c2 p2 ty0
   return scope
-tcPatt scope (PM q) ty0 = do
-  ty <- getResType q
+tcPatt scope c (PM q) ty0 = do
+  g@(Gl gr _) <- globals
+  ty <- case lookupResType gr q of
+          Ok ty   -> return ty
+          Bad msg -> evalError (pp msg)
   case ty of
     EPattType ty
-            -> do vty <- eval [] ty []
-                  unify scope ty0 vty
+            -> do unify scope ty0 (eval g [] c ty [])
                   return scope
     ty   -> evalError ("Pattern type expected but " <+> pp ty <+> " found.")
-tcPatt scope p ty = unimplemented ("tcPatt "++show p)
+tcPatt scope c p ty = unimplemented ("tcPatt "++show p)
 
-inferRecFields scope rs =
-  mapM (\(l,r) -> tcRecField scope l r Nothing) rs
+inferRecFields scope c rs =
+  mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs
 
-checkRecFields scope []          ltys
+checkRecFields scope c []          ltys
   | null ltys                            = return []
   | otherwise                            = evalError ("Missing fields:" <+> hsep (map fst ltys))
-checkRecFields scope ((l,t):lts) ltys =
+checkRecFields scope c ((l,t):lts) ltys =
   case takeIt l ltys of
-    (Just ty,ltys) -> do ltty  <- tcRecField scope l t (Just ty)
-                         lttys <- checkRecFields scope lts ltys
+    (Just ty,ltys) -> do let (c1,c2) = split c
+                         ltty  <- tcRecField scope c1 l t (Just ty)
+                         lttys <- checkRecFields scope c2 lts ltys
                          return (ltty : lttys)
     (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l)
-                         ltty  <- tcRecField scope l t Nothing
-                         lttys <- checkRecFields scope lts ltys
+                         let (c1,c2) = split c
+                         ltty  <- tcRecField scope c1 l t Nothing
+                         lttys <- checkRecFields scope c2 lts ltys
                          return lttys     -- ignore the field
   where
     takeIt l1 []  = (Nothing, [])
@@ -545,91 +617,94 @@ checkRecFields scope ((l,t):lts) ltys =
       | otherwise = let (mb_ty,ltys') = takeIt l1 ltys
                     in (mb_ty,lty:ltys')
 
-tcRecField scope l (mb_ann_ty,t) mb_ty = do
+tcRecField scope c l (mb_ann_ty,t) mb_ty = do
   (t,ty) <- case mb_ann_ty of
-              Just ann_ty -> do (ann_ty, _) <- tcRho scope ann_ty (Just vtypeType)
-                                env <- scopeEnv scope
-                                v_ann_ty <- eval env ann_ty []
-                                (t,_) <- tcRho scope t (Just v_ann_ty)
-                                instSigma scope t v_ann_ty mb_ty
-              Nothing     -> tcRho scope t mb_ty
+              Just ann_ty -> do let (c1,c2,c3,c4) = split4 c
+                                (ann_ty, _) <- tcRho scope c1 ann_ty (Just vtypeType)
+                                g <- globals
+                                let v_ann_ty = eval g (scopeEnv scope) c2 ann_ty []
+                                (t,_) <- tcRho scope c3 t (Just v_ann_ty)
+                                instSigma scope c4 t v_ann_ty mb_ty
+              Nothing     -> tcRho scope c t mb_ty
   return (l,t,ty)
 
-tcRecTypeFields scope []          mb_ty = return ([],mb_ty)
-tcRecTypeFields scope ((l,ty):rs) mb_ty = do
-  (ty,sort) <- tcRho scope ty mb_ty
+tcRecTypeFields scope c []          mb_ty = return ([],mb_ty)
+tcRecTypeFields scope c ((l,ty):rs) mb_ty = do
+  let (c1,c2) = split c
+  (ty,sort) <- tcRho scope c1 ty mb_ty
   mb_ty <- case sort of
              VSort s
                | s == cType  -> return (Just sort)
                | s == cPType -> return mb_ty
              VMeta _ _       -> return mb_ty
-             _               -> do sort <- value2term False (scopeVars scope) sort
+             _               -> do sort <- value2termM False (scopeVars scope) sort
                                    evalError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$
                                               "cannot be of type" <+> ppTerm Unqualified 0 sort)
-  (rs,mb_ty) <- tcRecTypeFields scope rs mb_ty
+  (rs,mb_ty) <- tcRecTypeFields scope c2 rs mb_ty
   return ((l,ty):rs,mb_ty)
 
 -- | Invariant: if the third argument is (Just rho),
 --              then rho is in weak-prenex form
-instSigma :: Scope s -> Term -> Sigma s -> Maybe (Rho s) -> EvalM s (Term, Rho s)
-instSigma scope t ty1 Nothing    = return (t,ty1)           -- INST1
-instSigma scope t ty1 (Just ty2) = do                       -- INST2
+instSigma :: Scope -> Choice -> Term -> Sigma -> Maybe Rho -> EvalM (Term, Rho)
+instSigma scope s t ty1 Nothing    = return (t,ty1)           -- INST1
+instSigma scope s t ty1 (Just ty2) = do                       -- INST2
   t <- subsCheckRho scope t ty1 ty2
   return (t,ty2)
 
 -- | Invariant: the second argument is in weak-prenex form
-subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> EvalM s Term
+subsCheckRho :: Scope -> Term -> Sigma -> Rho -> EvalM Term
 subsCheckRho scope t (VMeta i vs1) (VMeta j vs2)
-  | i  == j   = do sequence_ (zipWith (unifyThunk scope) vs1 vs2)
+  | i  == j   = do sequence_ (zipWith (unify scope) vs1 vs2)
                    return t
   | otherwise = do
-      mv <- getRef i
+      mv <- getMeta i
       case mv of
-        Evaluated _ v1 -> do
-          v1 <- apply v1 vs1
-          subsCheckRho scope t v1 (VMeta j vs2)
-        Residuation _ scope1 _ -> do
-          mv <- getRef j
+        Bound _ v1 -> do
+          g <- globals
+          subsCheckRho scope t (apply g v1 vs1) (VMeta j vs2)
+        Residuation scope1 _ -> do
+          mv <- getMeta j
           case mv of
-            Evaluated _ v2 -> do
-              v2 <- apply v2 vs2
-              subsCheckRho scope t (VMeta i vs1) v2
-            Residuation _ scope2 _
-              | m > n     -> do setRef i (Evaluated m (VMeta j vs2))
+            Bound _ v2 -> do
+              g <- globals
+              subsCheckRho scope t (VMeta i vs1) (apply g v2 vs2)
+            Residuation scope2 _
+              | m > n     -> do setMeta i (Bound m (VMeta j vs2))
                                 return t
-              | otherwise -> do setRef j (Evaluated n (VMeta i vs2))
+              | otherwise -> do setMeta j (Bound n (VMeta i vs2))
                                 return t
               where
                 m = length scope1
                 n = length scope2
-subsCheckRho scope t ty1@(VMeta tnk vs) ty2 = do
-  mv <- getRef tnk
+subsCheckRho scope t ty1@(VMeta i vs) ty2 = do
+  mv <- getMeta i
   case mv of
-    Evaluated _ ty1 -> do
-      ty1 <- apply ty1 vs
-      subsCheckRho scope t ty1 ty2
-    Residuation i scope' ctr -> do
-      occursCheck scope' tnk scope ty2
+    Bound _ ty1 -> do
+      g <- globals
+      subsCheckRho scope t (apply g ty1 vs) ty2
+    Residuation scope' ctr -> do
+      occursCheck scope' i scope ty2
       ctr <- subtype scope ctr ty2
-      setRef tnk (Residuation i scope' (Just ctr))
+      setMeta i (Residuation scope' (Just ctr))
       return t
-subsCheckRho scope t ty1 ty2@(VMeta tnk vs) = do
-  mv <- getRef tnk
+subsCheckRho scope t ty1 ty2@(VMeta i vs) = do
+  mv <- getMeta i
   case mv of
-    Evaluated _ ty2 -> do
-      ty2 <- apply ty2 vs
-      subsCheckRho scope t ty1 ty2
-    Residuation i scope' ctr -> do
-      occursCheck scope' tnk scope ty1
+    Bound _ ty2 -> do
+      g <- globals
+      subsCheckRho scope t ty1 (apply g ty2 vs)
+    Residuation scope' ctr -> do
+      occursCheck scope' i scope ty1
       ctr <- supertype scope ctr ty1
-      setRef tnk (Residuation i scope' (Just ctr))
+      setMeta i (Residuation scope' (Just ctr))
       return t
 subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do     -- Rule SPEC
-  (i,tnk) <- newResiduation scope
-  ty2 <- case ty2 of
-           VClosure env ty2 -> eval ((x,tnk):env) ty2 []
-           ty2              -> return ty2
-  subsCheckRho scope (App t (ImplArg (Meta i))) ty2 rho2
+  i <- newResiduation scope
+  g <- globals
+  let ty2' = case ty2 of
+               VClosure env c ty2 -> eval g ((x,VMeta i []):env) c ty2 []
+               ty2                -> ty2
+  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 <- evalCodomain scope x ty2
@@ -651,10 +726,8 @@ subsCheckRho scope t (VSort s1) (VSort s2)                    -- Rule PTYPE
   | s1 == cPType && s2 == cType = return t
 subsCheckRho scope t (VApp p1 _) (VApp p2 _)                  -- Rule INT1
   | p1 == (cPredef,cInts) && p2 == (cPredef,cInt) = return t
-subsCheckRho scope t (VApp p1 [tnk1]) (VApp p2 [tnk2])        -- Rule INT2
+subsCheckRho scope t (VApp p1 [VInt i]) (VApp p2 [VInt j])        -- Rule INT2
   | p1 == (cPredef,cInts) && p2 == (cPredef,cInts) = do
-      VInt i <- force tnk1
-      VInt j <- force tnk2
       if i <= j
         then return t
         else evalError ("Ints" <+> i <+> "is not a subtype of" <+> "Ints" <+> j)
@@ -697,39 +770,43 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
                           "there are no values for fields:" <+> hsep missing)
   rs <- sequence [mkField scope l t ty1 ty2 | (l,ty2,Just ty1) <- fields, Just t <- [mkProj l]]
   return (mkWrap (R rs))
+subsCheckRho scope t tau1 (VFV c vs) = do
+  tau2 <- variants c vs
+  subsCheckRho scope t tau1 tau2
+subsCheckRho scope t (VFV c vs) tau2 = do
+  tau1 <- variants c vs
+  subsCheckRho scope t tau1 tau2
 subsCheckRho scope t tau1 tau2 = do                           -- Rule EQ
   unify scope tau1 tau2                                 -- Revert to ordinary unification
   return t
 
-subsCheckFun :: Scope s -> Term -> Sigma s -> Value s -> Sigma s -> Value s -> EvalM s Term
+subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM Term
 subsCheckFun scope t a1 r1 a2 r2 = do
   let v   = newVar scope
   vt <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1
-  tnk <- newEvaluatedThunk (VGen (length scope) [])
-  r1 <- case r1 of
-          VClosure env r1 -> eval ((v,tnk):env) r1 []
-          r1              -> return r1
-  r2 <- case r2 of
-          VClosure env r2 -> eval ((v,tnk):env) r2 []
-          r2              -> return r2
+  g  <- globals
+  let r1 = case r1 of
+             VClosure env c r1 -> eval g ((v,(VGen (length scope) [])):env) c r1 []
+             r1                -> r1
+  let r2 = case r2 of
+             VClosure env c r2 -> eval g ((v,(VGen (length scope) [])):env) c r2 []
+             r2                -> r2
   t  <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1 r2
   return (Abs Explicit v t)
 
-subsCheckTbl :: Scope s -> Term -> Sigma s -> Rho s -> Sigma s -> Rho s -> EvalM s Term
+subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho  -> EvalM Term
 subsCheckTbl scope t p1 r1 p2 r2 = do
   let x = newVar scope
   xt <- subsCheckRho scope (Vr x) p2 p1
   t  <- subsCheckRho ((x,vtypePType):scope) (S t xt) r1 r2
-  p2 <- value2term True (scopeVars scope) p2
+  p2 <- value2termM True (scopeVars scope) p2
   return (T (TTyped p2) [(PV x,t)])
 
-subtype scope Nothing (VApp p [tnk])
+subtype scope Nothing (VApp p [VInt i])
   | p == (cPredef,cInts) = do
-      VInt i <- force tnk
       return (VCInts Nothing (Just i))
-subtype scope (Just (VCInts i j)) (VApp p [tnk])
+subtype scope (Just (VCInts i j)) (VApp p [VInt k])
   | p == (cPredef,cInts) = do
-      VInt k <- force tnk
       return (VCInts j (Just (maybe k (min k) i)))
 subtype scope Nothing (VRecType ltys) = do
   lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,True,ctr)) ltys
@@ -750,13 +827,11 @@ subtype scope (Just ctr) ty = do
   unify scope ctr ty
   return ty
 
-supertype scope Nothing (VApp p [tnk])
+supertype scope Nothing (VApp p [VInt i])
   | p == (cPredef,cInts) = do
-      VInt i <- force tnk
       return (VCInts (Just i) Nothing)
-supertype scope (Just (VCInts i j)) (VApp p [tnk])
+supertype scope (Just (VCInts i j)) (VApp p [VInt k])
   | p == (cPredef,cInts) = do
-      VInt k <- force tnk
       return (VCInts (Just (maybe k (max k) i)) j)
 supertype scope Nothing (VRecType ltys) = do
   lctrs <- mapM (\(l,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys
@@ -775,58 +850,60 @@ supertype scope (Just ctr) ty = do
   unify scope ctr ty
   return ty
 
-
 -----------------------------------------------------------------------
 -- Unification
 -----------------------------------------------------------------------
 
-unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Ident, Sigma s, Rho s)
+unifyFun :: Scope -> Rho -> EvalM (BindType, Ident, Sigma, Rho)
 unifyFun scope (VProd bt x arg res) =
   return (bt,x,arg,res)
+unifyFun scope (VFV c vs) = do
+  res <- mapM (unifyFun scope) vs
+  return (Explicit, identW, VFV c [sigma | (_,_,sigma,rho) <- res], VFV c [rho | (_,_,sigma,rho) <- res])
 unifyFun scope tau = do
-  let mk_val (_,tnk) = VMeta tnk []
+  let mk_val i = VMeta i []
   arg <- fmap mk_val $ newResiduation scope
   res <- fmap mk_val $ newResiduation scope
   let bt = Explicit
   unify scope tau (VProd bt identW arg res)
   return (bt,identW,arg,res)
 
-unifyTbl :: Scope s -> Rho s -> EvalM s (Sigma s, Rho s)
+unifyTbl :: Scope -> Rho -> EvalM (Sigma, Rho)
 unifyTbl scope (VTable arg res) =
   return (arg,res)
 unifyTbl scope tau = do
-  let mk_val (i,tnk) = VMeta tnk []
+  let mk_val i = VMeta i []
   arg <- fmap mk_val $ newResiduation scope
   res <- fmap mk_val $ newResiduation scope
   unify scope tau (VTable arg res)
   return (arg,res)
 
 unify scope (VApp f1 vs1) (VApp f2 vs2)
-  | f1 == f2  = sequence_ (zipWith (unifyThunk scope) vs1 vs2)
+  | f1 == f2  = sequence_ (zipWith (unify scope) vs1 vs2)
 unify scope (VMeta i vs1) (VMeta j vs2)
-  | i  == j   = sequence_ (zipWith (unifyThunk scope) vs1 vs2)
+  | i  == j   = sequence_ (zipWith (unify scope) vs1 vs2)
   | otherwise = do 
-      mv <- getRef i
+      mv <- getMeta i
       case mv of
-        Evaluated _ v1 -> do
-          v1 <- apply v1 vs1
-          unify scope v1 (VMeta j vs2)
-        Residuation _ scope1 _ -> do
-          mv <- getRef j
+        Bound _ v1 -> do
+          g <- globals
+          unify scope (apply g v1 vs1) (VMeta j vs2)
+        Residuation scope1 _ -> do
+          mv <- getMeta j
           case mv of
-            Evaluated _ v2 -> do
-              v2 <- apply v2 vs2
-              unify scope (VMeta i vs1) v2
-            Residuation _ scope2 _
-              | m > n     -> setRef i (Evaluated m (VMeta j vs2))
-              | otherwise -> setRef j (Evaluated n (VMeta i vs2))
+            Bound _ v2 -> do
+              g <- globals
+              unify scope (VMeta i vs1) (apply g v2 vs2)
+            Residuation scope2 _
+              | m > n     -> setMeta i (Bound m (VMeta j vs2))
+              | otherwise -> setMeta j (Bound n (VMeta i vs2))
               where
                 m = length scope1
                 n = length scope2 
 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)
+  | i == j                     = sequence_ (zipWith (unify scope) vs1 vs2)
 unify scope (VProd b x d cod) (VProd b' x' d' cod')
   | b == b'                    = do
       unify scope d d'
@@ -846,75 +923,68 @@ unify scope (VStr s1) (VStr s2)
   | s1 == s2                   = return ()
 unify scope VEmpty VEmpty      = return ()
 unify scope v1 v2 = do
-  t1 <- value2term False (scopeVars scope) v1
-  t2 <- value2term False (scopeVars scope) v2
+  t1 <- value2termM False (scopeVars scope) v1
+  t2 <- value2termM False (scopeVars scope) v2
   evalError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$
                                         ppTerm Unqualified 0 t2))
 
-unifyThunk scope tnk1 tnk2 = do
-  res1 <- getRef tnk1
-  res2 <- getRef tnk2
-  case (res1,res2) of
-    (Evaluated _ v1,Evaluated _ v2) -> unify scope v1 v2
 
 -- | Invariant: tv1 is a flexible type variable
-unifyVar :: Scope s -> Thunk s -> [Thunk s] -> Tau s -> EvalM s ()
-unifyVar scope tnk vs ty2 = do            -- Check whether i is bound
-  mv <- getRef tnk
+unifyVar :: Scope -> MetaId -> [Value] -> Tau -> EvalM ()
+unifyVar scope metaid vs ty2 = do            -- Check whether i is bound
+  mv <- getMeta metaid
   case mv of
-    Evaluated _ ty1        -> do ty1 <- apply ty1 vs
-                                 unify scope ty1 ty2
-    Residuation i scope' _ -> do occursCheck scope' tnk scope ty2
-                                 setRef tnk (Evaluated (length scope') ty2)
+    Bound _ ty1          -> do g <- globals
+                               unify scope (apply g ty1 vs) ty2
+    Residuation scope' _ -> do occursCheck scope' metaid scope ty2
+                               setMeta metaid (Bound (length scope') ty2)
 
-occursCheck scope' tnk scope v =
+occursCheck scope' i0 scope v =
   let m = length scope'
       n = length scope
   in check m n v
   where
-    check m n (VApp f vs) = mapM_ (follow m n) vs
+    check m n (VApp f vs) = mapM_ (check m n) vs
     check m n (VMeta i vs)
-      | tnk == i  = do ty1 <- value2term False (scopeVars scope) (VMeta i vs)
-                       ty2 <- value2term False (scopeVars scope) v
-                       evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$
-                                  nest 2 (ppTerm Unqualified 0 ty2))
+      | i0 == i  = do ty1 <- value2termM False (scopeVars scope) (VMeta i vs)
+                      ty2 <- value2termM False (scopeVars scope) v
+                      evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$
+                                 nest 2 (ppTerm Unqualified 0 ty2))
       | otherwise = do
-          s <- getRef i
+          s <- getMeta i
           case s of
-            Evaluated _ v -> do v <- apply v vs
-                                check m n v
-            _             -> mapM_ (follow m n) vs
+            Bound _ v -> do g <- globals
+                            check m n (apply g v vs)
+            _         -> mapM_ (check m n) vs
     check m n (VGen i vs)
       | i > m     = let (v,_) = reverse scope !! i
                     in evalError ("Variable" <+> pp v <+> "has escaped")
-      | otherwise = mapM_ (follow m n) vs
-    check m n (VClosure env (Abs bt x t)) = do
-      tnk <- newEvaluatedThunk (VGen n [])
-      v <- eval ((x,tnk):env) t []
-      check (m+1) (n+1) v
+      | otherwise = mapM_ (check m n) vs
+    check m n (VClosure env c (Abs bt x t)) = do
+      g <- globals
+      check (m+1) (n+1) (eval g ((x,VGen n []):env) c t [])
     check m n (VProd bt x ty1 ty2) = do
       check m n ty1
       case ty2 of
-        VClosure env t -> do tnk <- newEvaluatedThunk (VGen n [])
-                             v <- eval ((x,tnk):env) t []
-                             check (m+1) (n+1) v
-        _              -> check m n ty2
+        VClosure env c t -> do g <- globals
+                               check (m+1) (n+1) (eval g ((x,VGen n []):env) c t [])
+        _                -> check m n ty2
     check m n (VRecType as) =
       mapM_ (\(lbl,v) -> check m n v) as
     check m n (VR as) =
-      mapM_ (\(lbl,tnk) -> follow m n tnk) as
+      mapM_ (\(lbl,v) -> check m n v) as
     check m n (VP v l vs) =
-      check m n v >> mapM_ (follow m n) vs
+      check m n v >> mapM_ (check m n) vs
     check m n (VExtR v1 v2) =
       check m n v1 >> check m n v2
     check m n (VTable v1 v2) =
       check m n v1 >> check m n v2
-    check m n (VT ty env cs) =
+    check m n (VT ty env c cs) =
       check m n ty      -- Traverse cs as well
     check m n (VV ty cs) =
-      check m n ty >> mapM_ (follow m n) cs
-    check m n (VS v1 tnk vs) =
-      check m n v1 >> follow m n tnk >> mapM_ (follow m n) vs
+      check m n ty >> mapM_ (check m n) cs
+    check m n (VS v1 v2 vs) =
+      check m n v1 >> check m n v2 >> mapM_ (check m n) vs
     check m n (VSort _) = return ()
     check m n (VInt _) = return ()
     check m n (VFlt _) = return ()
@@ -927,40 +997,41 @@ occursCheck scope' tnk scope v =
     check m n (VPatt _ _ _) = return ()
     check m n (VPattType v) =
       check m n v
+    check m n (VFV c vs) =
+      mapM_ (check m n) vs
     check m n (VAlts v vs) =
       check m n v >> mapM_ (\(v1,v2) -> check m n v1 >> check m n v2) vs
     check m n (VStrs vs) =
       mapM_ (check m n) vs
 
-    follow m n tnk = check m n =<< force tnk
-
 -----------------------------------------------------------------------
 -- Instantiation and quantification
 -----------------------------------------------------------------------
 
 -- | Instantiate the topmost implicit arguments with metavariables
-instantiate :: Scope s -> Term -> Sigma s -> EvalM s (Term,Rho s)
+instantiate :: Scope -> Term -> Sigma -> EvalM (Term,Rho)
 instantiate scope t (VProd Implicit x ty1 ty2) = do
-  (i,tnk) <- newResiduation scope
+  i <- newResiduation scope
   ty2 <- case ty2 of
-           VClosure env ty2 -> eval ((x,tnk):env) ty2 []
-           ty2              -> return ty2
+           VClosure env c ty2 -> do g <- globals
+                                    return (eval g ((x,VMeta i []):env) c 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@(VMeta i args) = getMeta i >>= \case
+  Bound _ 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)
 
 -- | Build fresh lambda abstractions for the topmost implicit arguments
-skolemise :: Scope s -> Sigma s -> EvalM s (Scope s, Term->Term, Rho s)
+skolemise :: Scope -> Sigma -> EvalM (Scope, Term->Term, Rho)
 skolemise scope ty@(VMeta i vs) = do
-  mv <- getRef i
+  mv <- getMeta i
   case mv of
-    Residuation _ _ _ -> return (scope,id,ty)                   -- guarded constant?
-    Evaluated _ ty    -> do ty <- apply ty vs
-                            skolemise scope ty
+    Residuation _ _ -> return (scope,id,ty)                   -- guarded constant?
+    Bound _ ty      -> do g <- globals
+                          skolemise scope (apply g ty vs)
 skolemise scope (VProd Implicit x ty1 ty2) = do
   let v = newVar scope
   ty2 <- evalCodomain scope x ty2
@@ -970,7 +1041,7 @@ skolemise scope ty = do
   return (scope,id,ty)
 
 -- | Quantify over the specified type variables (all flexible)
-quantify :: Scope s -> Term -> [Thunk s] -> Rho s -> EvalM s (Term,Sigma s)
+quantify :: Scope -> Term -> [MetaId] -> Rho -> EvalM (Term,Sigma)
 quantify scope t tvs ty = do
   let m = length tvs
       n = length scope
@@ -980,41 +1051,40 @@ quantify scope t tvs ty = do
   let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs
   return (foldr (Abs Implicit) t new_bndrs,ty')
   where
-    bind (i, tnk, name) = setRef tnk (Evaluated (length scope) (VGen i []))
+    bind (i, meta_id, name) = setMeta meta_id (Bound (length scope) (VGen i []))
 
     check m n xs (VApp f vs)       = do
-      (xs,vs) <- mapAccumM (follow m n) xs vs
+      (xs,vs) <- mapAccumM (check m n) xs vs
       return (xs,VApp f vs)
     check m n xs (VMeta i vs)      = do
-      s <- getRef i
+      s <- getMeta i
       case s of
-        Evaluated _ v -> do v <- apply v vs
-                            check m n xs v
-        _             -> do (xs,vs) <- mapAccumM (follow m n) xs vs
-                            return (xs,VMeta i vs)
+        Bound _ v -> do g <- globals
+                        check m n xs (apply g v vs)
+        _         -> do (xs,vs) <- mapAccumM (check m n) xs vs
+                        return (xs,VMeta i vs)
     check m n st (VGen i vs)= do
-      (st,vs) <- mapAccumM (follow m n) st vs
+      (st,vs) <- mapAccumM (check m n) st vs
       return (st, VGen (m+i) vs)
-    check m n st (VClosure env (Abs bt x t)) = do
-      (st,env) <- mapAccumM (\st (x,tnk) -> follow m n st tnk >>= \(st,tnk) -> return (st,(x,tnk))) st env
-      return (st,VClosure env (Abs bt x t))
+    check m n st (VClosure env c (Abs bt x t)) = do
+      (st,env) <- mapAccumM (\st (x,v) -> check m n st v >>= \(st,v) -> return (st,(x,v))) st env
+      return (st,VClosure env c (Abs bt x t))
     check m n xs (VProd bt x v1 v2) = do
       (xs,v1) <- check m n xs v1
       case v2 of
-        VClosure env t -> do tnk <- newEvaluatedThunk (VGen n [])
-                             (st,env) <- mapAccumM (\xs (x,tnk) -> follow m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env
-                             return (x:xs,VProd bt x v1 (VClosure env t))
-        v2             -> do (xs,v2) <- check m (n+1) xs v2
-                             return (x:xs,VProd bt x v1 v2)
+        VClosure env c t -> do (st,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env
+                               return (x:xs,VProd bt x v1 (VClosure env c t))
+        v2               -> do (xs,v2) <- check m (n+1) xs v2
+                               return (x:xs,VProd bt x v1 v2)
     check m n xs (VRecType as)     = do
       (xs,as) <- mapAccumM (\xs (l,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,v))) xs as
       return (xs,VRecType as)
     check m n xs (VR as)           = do
-      (xs,as) <- mapAccumM (\xs (lbl,tnk) -> follow m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as
+      (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as
       return (xs,VR as)
     check m n xs (VP v l vs)       = do
       (xs,v)  <- check m n xs v
-      (xs,vs) <- mapAccumM (follow m n) xs vs
+      (xs,vs) <- mapAccumM (check m n) xs vs
       return (xs,VP v l vs)
     check m n xs (VExtR v1 v2)     = do
       (xs,v1) <- check m n xs v1
@@ -1024,18 +1094,18 @@ quantify scope t tvs ty = do
       (xs,v1) <- check m n xs v1
       (xs,v2) <- check m n xs v2
       return (xs,VTable v1 v2)
-    check m n xs (VT ty env cs)    = do
+    check m n xs (VT ty env c cs)    = do
       (xs,ty) <- check m n xs ty
-      (xs,env) <- mapAccumM (\xs (x,tnk) -> follow m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env
-      return (xs,VT ty env cs)
+      (xs,env) <- mapAccumM (\xs (x,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(x,tnk))) xs env
+      return (xs,VT ty env c cs)
     check m n xs (VV ty cs)        = do
       (xs,ty) <- check m n xs ty
-      (xs,cs) <- mapAccumM (follow m n) xs cs
+      (xs,cs) <- mapAccumM (check m n) xs cs
       return (xs,VV ty cs)
     check m n xs (VS v1 tnk vs)    = do
       (xs,v1)  <- check m n xs v1
-      (xs,tnk) <- follow m n xs tnk
-      (xs,vs)  <- mapAccumM (follow m n) xs vs
+      (xs,tnk) <- check m n xs tnk
+      (xs,vs)  <- mapAccumM (check m n) xs vs
       return (xs,VS v1 tnk vs)
     check m n xs v@(VSort _)       = return (xs,v)
     check m n xs v@(VInt _)        = return (xs,v)
@@ -1054,6 +1124,9 @@ quantify scope t tvs ty = do
     check m n xs (VPattType v)     = do
       (xs,v) <- check m n xs v
       return (xs,VPattType v)
+    check m n xs (VFV c vs)       = do
+      (xs,vs) <- mapAccumM (check m n) xs vs
+      return (xs,VFV c vs)
     check m n xs (VAlts v vs)      = do
       (xs,v)  <- check m n xs v
       (xs,vs) <- mapAccumM (\xs (v1,v2) -> do (xs,v1) <- check m n xs v1
@@ -1064,13 +1137,7 @@ quantify scope t tvs ty = do
     check m n xs (VStrs vs)        = do
       (xs,vs) <- mapAccumM (check m n) xs vs
       return (xs,VStrs vs)
-    check m n st v                 = error (showValue v)
-
-    follow m n st tnk = do
-      v      <- force tnk
-      (st,v) <- check m n st v
-      tnk    <- newEvaluatedThunk v
-      return (st,tnk)
+    check m n xs v = unimplemented ("check "++show (ppValue Unqualified 5 v))
 
     mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c])
     mapAccumM f s []     = return (s,[])
@@ -1083,18 +1150,17 @@ 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']]
 
-
 -----------------------------------------------------------------------
 -- Helpers
 -----------------------------------------------------------------------
 
-type Sigma s = Value s
-type Rho s   = Value s -- No top-level ForAll
-type Tau s   = Value s -- No ForAlls anywhere
+type Sigma = Value
+type Rho   = Value -- No top-level ForAll
+type Tau   = Value -- No ForAlls anywhere
 
 unimplemented str = fail ("Unimplemented: "++str)
 
-newVar :: Scope s -> Ident
+newVar :: Scope -> Ident
 newVar scope = head [x | i <- [1..],
                          let x = identS ('v':show i),
                          isFree scope x]
@@ -1102,38 +1168,38 @@ newVar scope = head [x | i <- [1..],
     isFree []            x = True
     isFree ((y,_):scope) x = x /= y && isFree scope x
 
-scopeEnv   scope = zipWithM (\(x,ty) i -> newEvaluatedThunk (VGen i []) >>= \tnk -> return (x,tnk)) (reverse scope) [0..]
+scopeEnv   scope = zipWith (\(x,ty) i -> (x,VGen i [])) (reverse scope) [0..]
 scopeVars  scope = map fst scope
 scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)
 
 -- | This function takes account of zonking, and returns a set
 -- (no duplicates) of unbound meta-type variables
-getMetaVars :: [(Scope s,Sigma s)] -> EvalM s [Thunk s]
-getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys
+getMetaVars :: [(Scope,Sigma)] -> EvalM [MetaId]
+getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
   where
-    follow acc tnk = force tnk >>= \v -> go v acc
-
     -- Get the MetaIds from a term; no duplicates in result
-    go (VGen i args)     acc = foldM follow acc args
-    go (VSort s)         acc = return acc
-    go (VInt _)          acc = return acc
-    go (VRecType as)     acc = foldM (\acc (lbl,v) -> go v acc) acc as
-    go (VClosure _ _)    acc = return acc
-    go (VProd b x v1 v2) acc = go v2 acc >>= go v1
-    go (VTable v1 v2)    acc = go v2 acc >>= go v1
-    go (VMeta m args)    acc
+    go acc (VGen i args)     = foldM go acc args
+    go acc (VSort s)         = return acc
+    go acc (VInt _)          = return acc
+    go acc (VRecType as)     = foldM (\acc (lbl,v) -> go acc v) acc as
+    go acc (VClosure _ _ _)  = return acc
+    go acc (VProd b x v1 v2) = go acc v2 >>= \acc -> go acc v1
+    go acc (VTable v1 v2)    = go acc v2 >>= \acc -> go acc v1
+    go acc (VMeta m args)
       | m `elem` acc         = return acc
-      | otherwise            = do res <- getRef m
+      | otherwise            = do res <- getMeta m
                                   case res of
-                                    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)
+                                    Bound _ v              -> go acc v
+                                    Residuation _ Nothing  -> foldM go (m:acc) args
+                                    Residuation _ (Just v) -> go acc v
+                                    _                      -> return acc
+    go acc (VApp f args)     = foldM go acc args
+    go acc (VFV c vs)        = foldM go acc vs
+    go acc (VCInts _ _)      = return acc
+    go acc v                 = unimplemented ("go "++show (ppValue Unqualified 5 v))
 
 -- | Eliminate any substitutions in a term
-zonkTerm :: [Ident] -> Term -> EvalM s Term
+zonkTerm :: [Ident] -> Term -> EvalM Term
 zonkTerm xs (Abs b x t) = do
   t <- zonkTerm (x:xs) t
   return (Abs b x t)
@@ -1145,16 +1211,11 @@ zonkTerm xs (Prod b x t1 t2) = do
     xs' | x == identW = xs
         | otherwise   = x:xs
 zonkTerm xs (Meta i) = do
-  tnk <- EvalM $ \gr k mt d r msgs -> 
-           case Map.lookup i mt of
-             Just v  -> k v mt d r msgs
-             Nothing -> return (Fail (pp "Undefined meta variable") msgs)
-  st <- getRef tnk
+  st <- getMeta i
   case st of
-    Hole _            -> return (Meta i)
-    Residuation _ scope v -> case v of
-                              Just v  -> zonkTerm xs =<< value2term False (map fst scope) v
-                              Nothing -> return (Meta i)
-    Narrowing _ _     -> return (Meta i)
-    Evaluated _ v     -> zonkTerm xs =<< value2term False xs v
+    Bound _ v           -> zonkTerm xs =<< value2termM False xs v
+    Residuation scope v -> case v of
+                            Just v  -> zonkTerm xs =<< value2termM False (map fst scope) v
+                            Nothing -> return (Meta i)
+    Narrowing _         -> return (Meta i)
 zonkTerm xs t = composOp (zonkTerm xs) t
diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y
index 136f5220a..5586e9dea 100644
--- a/src/compiler/api/GF/Grammar/Parser.y
+++ b/src/compiler/api/GF/Grammar/Parser.y
@@ -711,8 +711,8 @@ ERHS3 :: { ERHS }
 
 NLG :: { Map.Map Ident Info }
   : ListNLGDef     { Map.fromList $1 }
-  | Posn Tag Posn  { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (Abs Explicit (identS "qid") (Abs Explicit (identS "lang") $2))))) }
-  | Posn Exp Posn  { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (Abs Explicit (identS "qid") (Abs Explicit (identS "lang") $2))))) }
+  | Posn Tag Posn  { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
+  | Posn Exp Posn  { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
 
 ListNLGDef :: { [(Ident,Info)] }
 ListNLGDef
diff --git a/src/compiler/gf.cabal b/src/compiler/gf.cabal
index 1a36c9602..fa0d34358 100644
--- a/src/compiler/gf.cabal
+++ b/src/compiler/gf.cabal
@@ -107,6 +107,7 @@ library
     GF.Compile.CFGtoPGF
     GF.Compile.CheckGrammar
     GF.Compile.Compute.Concrete
+    GF.Compile.Compute.Concrete2
     GF.Compile.ExampleBased
     GF.Compile.Export
     GF.Compile.GenerateBC