diff --git a/src/compiler/GF/Compile/Compute/Concrete.hs b/src/compiler/GF/Compile/Compute/Concrete.hs
index 3dd8f676c..b8d84116b 100644
--- a/src/compiler/GF/Compile/Compute/Concrete.hs
+++ b/src/compiler/GF/Compile/Compute/Concrete.hs
@@ -56,7 +56,6 @@ data ThunkState s
   | Hole        {-# UNPACK #-} !MetaId
   | Narrowing   {-# UNPACK #-} !MetaId Type
   | Residuation {-# UNPACK #-} !MetaId (Scope s) (Sigma s)
-  | Bound       Term
 
 type Thunk s = STRef s (ThunkState s)
 type Env s = [(Ident,Thunk s)]
@@ -64,8 +63,8 @@ type Scope s = [(Ident,Value s)]
 
 data Value s
   = VApp QIdent [Thunk s]
-  | VMeta (Thunk s) (Env s) [Thunk s]
-  | VSusp (Thunk s) (Env s) (Value s -> EvalM s (Value s)) [Thunk s]
+  | VMeta (Thunk s) [Thunk s]
+  | VSusp (Thunk s) (Value s -> EvalM s (Value s)) [Thunk s]
   | VGen  {-# UNPACK #-} !Int [Thunk s]
   | VClosure (Env s) Term
   | VProd BindType Ident (Value s) (Value s)
@@ -95,9 +94,9 @@ data Value s
 
 
 showValue (VApp q tnks) = "(VApp "++unwords (show q : map (const "_") tnks) ++ ")"
-showValue (VMeta _ _ _) = "VMeta"
-showValue (VSusp _ _ _ _) = "VSusp"
-showValue (VGen _ _) = "VGen"
+showValue (VMeta _ _) = "VMeta"
+showValue (VSusp _ _ _) = "VSusp"
+showValue (VGen i _) = "(VGen "++show i++")"
 showValue (VClosure _ _) = "VClosure"
 showValue (VProd _ x v1 v2) = "VProd ("++show x++") ("++showValue v1++") ("++showValue v2++")"
 showValue (VRecType _) = "VRecType"
@@ -108,7 +107,7 @@ showValue (VTable v1 v2) = "VTable ("++showValue v1++") ("++showValue v2++")"
 showValue (VT _ _ cs) = "(VT "++show cs++")"
 showValue (VV _ _) = "VV"
 showValue (VS v _ _) = "(VS "++showValue v++")"
-showValue (VSort _) = "VSort"
+showValue (VSort s) = "(VSort "++show s++")"
 showValue (VInt _) = "VInt"
 showValue (VFlt _) = "VFlt"
 showValue (VStr s) = "(VStr "++show s++")"
@@ -142,7 +141,7 @@ eval env (App t1 t2)    vs  = do tnk <- newThunk env t2
 eval env (Abs b x t)    []  = return (VClosure env (Abs b x t))
 eval env (Abs b x t) (v:vs) = eval ((x,v):env) t vs
 eval env (Meta i)       vs  = do tnk <- newHole i
-                                 return (VMeta tnk env vs)
+                                 return (VMeta tnk vs)
 eval env (ImplArg t)    []  = eval env t []
 eval env (Prod b x t1 t2)[] = do v1 <- eval env t1 []
                                  return (VProd b x v1 (VClosure env t2))
@@ -256,8 +255,8 @@ eval env (TSymCat d r rs) []= do rs <- forM rs $ \(i,(pv,ty)) ->
 eval env (TSymVar d r)  []  = do return (VSymVar d r)
 eval env t              vs  = evalError ("Cannot reduce term" <+> pp t)
 
-apply (VMeta m env vs0)             vs  = return (VMeta m env   (vs0++vs))
-apply (VSusp m env k vs0)           vs  = return (VSusp m env k (vs0++vs))
+apply (VMeta m vs0)                 vs  = return (VMeta m   (vs0++vs))
+apply (VSusp m k vs0)               vs  = return (VSusp m k (vs0++vs))
 apply (VApp f  vs0)                 vs  = return (VApp f (vs0++vs))
 apply (VGen i  vs0)                 vs  = return (VGen i (vs0++vs))
 apply (VClosure env (Abs b x t)) (v:vs) = eval ((x,v):env) t vs
@@ -345,9 +344,9 @@ patternMatch v0 ((env0,ps,args0,t):eqs) = match env0 ps eqs args0
 
     match' env p ps eqs arg v args = do
       case (p,v) of
-        (p,       VMeta i envi   vs) -> susp i envi (\v -> apply v vs >>= \v -> match' env p ps eqs arg v args)
-        (p,       VGen  i vs       ) -> return v0
-        (p,       VSusp i envi k vs) -> susp i envi (\v -> k v >>= \v -> apply v vs >>= \v -> match' env p ps eqs arg v args)
+        (p,       VMeta i   vs) -> susp i (\v -> apply v vs >>= \v -> match' env p ps eqs arg v args)
+        (p,       VGen  i   vs) -> return v0
+        (p,       VSusp i k vs) -> susp i (\v -> k v >>= \v -> apply v vs >>= \v -> match' env p ps eqs arg v args)
         (PP q qs, VApp r tnks)
           | q == r        -> match env (qs++ps) eqs (tnks++args)
         (PR pas, VR as)   -> matchRec env (reverse pas) as ps eqs args
@@ -443,18 +442,18 @@ vtableSelect v0 ty tnks tnk2 vs = do
           return (r*cnt'+r',cnt*cnt')
     value2index (VInt n)          ty
       | Just max <- isTypeInts ty    = return (fromIntegral n,fromIntegral max+1)
-    value2index (VMeta i envi vs) ty = do
-      v <- susp i envi (\v -> apply v vs)
+    value2index (VMeta i vs) ty = do
+      v <- susp i (\v -> apply v vs)
       value2index v ty
-    value2index (VSusp i envi k vs) ty = do
-      v <- susp i envi (\v -> k v >>= \v -> apply v vs)
+    value2index (VSusp i k vs) ty = do
+      v <- susp i (\v -> k v >>= \v -> apply v vs)
       value2index v ty
     value2index v ty = do t <- value2term [] v
                           evalError ("the parameter:" <+> ppTerm Unqualified 0 t $$
                                      "cannot be evaluated at compile time.")
 
 
-susp i env ki = EvalM $ \gr k mt d r msgs -> do
+susp i ki = EvalM $ \gr k mt d r msgs -> do
   s <- readSTRef i
   case s of
     Narrowing id (QC q) -> case lookupOrigInfo gr q of
@@ -465,13 +464,13 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do
                         -> bindInt gr k mt d r msgs s 0 max
     Evaluated _ v       -> case ki v of
                              EvalM f -> f gr k mt d r msgs
-    _                   -> k (VSusp i env ki []) 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
       (mt',tnks) <- mkArgs mt ctxt
       let v = VApp (m,p) tnks
-      writeSTRef i (Evaluated (length env) v)
+      writeSTRef i (Evaluated 0 v)
       res <- case ki v of
                EvalM f -> f gr k mt' d r msgs
       writeSTRef i s
@@ -491,7 +490,7 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do
     bindInt gr k mt d r msgs s iv max
       | iv <= max = do
          let v = VInt iv
-         writeSTRef i (Evaluated (length env) v)
+         writeSTRef i (Evaluated 0 v)
          res <- case ki v of
                   EvalM f -> f gr k mt d r msgs
          writeSTRef i s
@@ -503,19 +502,17 @@ susp i env ki = EvalM $ \gr k mt d r msgs -> do
 
 value2term xs (VApp q tnks) =
   foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (if fst q == cPredef then Q q else QC q) tnks
-value2term xs (VMeta m env vs) = do
+value2term xs (VMeta m vs) = do
   s <- getRef m
   case s of
     Evaluated _ v     -> do v <- apply v vs
                             value2term xs v
     Unevaluated env t -> do v <- eval env t vs
                             value2term xs v
-    Bound t           -> do v <- eval env t vs
-                            value2term xs v
     Hole i            -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs
     Residuation i _ _ -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs
     Narrowing i _     -> foldM (\e1 tnk -> fmap (App e1) (tnk2term xs tnk)) (Meta i) vs
-value2term xs (VSusp j env k vs) = do
+value2term xs (VSusp j k vs) = do
   v <- k (VGen maxBound vs)
   value2term xs v
 value2term xs (VGen j tnks) =
@@ -861,9 +858,9 @@ force tnk = EvalM $ \gr k mt d r msgs -> do
                                                                  writeSTRef tnk s
                                                                  return r) 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
+    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 xs tnk = EvalM $ \gr k mt d r msgs ->
   let join f g = do res <- f
diff --git a/src/compiler/GF/Compile/GeneratePMCFG.hs b/src/compiler/GF/Compile/GeneratePMCFG.hs
index 8995972e2..0a0b23be4 100644
--- a/src/compiler/GF/Compile/GeneratePMCFG.hs
+++ b/src/compiler/GF/Compile/GeneratePMCFG.hs
@@ -253,7 +253,7 @@ param2int (VApp q tnks) ty = do
       return (r*cnt'+r',combine' cnt rs cnt' rs',cnt*cnt')
 param2int (VInt n)        ty
   | Just max <- isTypeInts ty= return (fromIntegral n,[],fromIntegral max+1)
-param2int (VMeta tnk _ _) ty = do
+param2int (VMeta tnk _) ty = do
   tnk_st <- getRef tnk
   case tnk_st of
     Evaluated _ v  -> param2int v ty
diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
index d7a22cddd..40e99c3bc 100644
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -27,14 +27,14 @@ checkLType :: Grammar -> Term -> Type -> Check (Term, Type)
 checkLType gr t ty = runEvalOneM gr $ do
   vty <- eval [] ty []
   (t,_) <- tcRho [] t (Just vty)
-  t <- zonkTerm t
+  t <- zonkTerm [] t
   return (t,ty)
 
 inferLType :: Grammar -> Term -> Check (Term, Type)
 inferLType gr t = runEvalOneM gr $ do
   (t,ty) <- inferSigma [] t
-  t  <- zonkTerm t
-  ty <- zonkTerm =<< value2term [] ty
+  t  <- zonkTerm [] t
+  ty <- value2term [] ty
   return (t,ty)
 
 inferSigma :: Scope s -> Term -> EvalM s (Term,Sigma s)
@@ -72,21 +72,94 @@ 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
-  (_,tnk) <- newResiduation scope vtypeType
-  env <- scopeEnv scope
-  let arg_ty = VMeta tnk env []
+  (i,tnk) <- newResiduation scope vtypeType
+  let arg_ty = VMeta tnk []
   (body,body_ty) <- tcRho ((var,arg_ty):scope) body Nothing
-  return (Abs bt var body, (VProd bt identW arg_ty body_ty))
+  let m = length scope
+      n = m+1
+  (b,used_bndrs) <- check m n (False,[]) body_ty
+  if b
+    then let v = head (allBinders \\ used_bndrs)
+         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 (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
+    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 (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
+      check m (n+1) (b,x:xs) v2
+    check m n st (VRecType as)     = foldM (\st (l,v) -> check m n st v) st as
+    check m n st (VR as)           =
+      foldM (\st (lbl,tnk) -> follow m n st tnk) st as
+    check m n st (VP v l vs)       =
+      check m n st v >>= \st -> foldM (follow 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 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 (VS v1 tnk vs)    = do
+      st <- check m n st v1
+      st <- follow m n st tnk
+      foldM (follow 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
+    check m n st (VStr _)          = return st
+    check m n st VEmpty            = return st
+    check m n st (VC v1 v2)        =
+      check m n st v1 >>= \st -> check m n st v2
+    check m n st (VGlue v1 v2)     =
+      check m n st v1 >>= \st -> check m n st v2
+    check m n st (VPatt _ _ _)     = return st
+    check m n st (VPattType v)     = check m n st v
+    check m n st (VAlts v vs)      = do
+      st <- check m n st v
+      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
-  (bt, _, var_ty, body_ty) <- unifyFun scope ty
+  (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 <- case body_ty of
+               VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) [])
+                                          eval ((x,tnk):env) body_ty []
+               body_ty              -> return body_ty
   (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
   return (Abs Implicit var body,ty)
 tcRho scope (Abs Explicit var body) (Just ty) = do           -- ABS3
   (scope,f,ty') <- skolemise scope ty
-  (_,_,var_ty,body_ty) <- unifyFun scope ty'
+  (_,x,var_ty,body_ty) <- unifyFun scope ty'
+  body_ty <- case body_ty of
+               VClosure env body_ty -> do tnk <- newEvaluatedThunk (VGen (length scope) [])
+                                          eval ((x,tnk):env) body_ty []
+               body_ty              -> return body_ty
   (body, body_ty) <- tcRho ((var,var_ty):scope) body (Just body_ty)
   return (f (Abs Explicit var body),ty)
 tcRho scope (Meta i) (Just ty) = do
@@ -95,7 +168,7 @@ tcRho scope (Meta i) (Just ty) = do
 tcRho scope (Meta _) Nothing = do
   (_,tnk) <- newResiduation scope vtypeType
   env <- scopeEnv scope
-  let vty = VMeta tnk env []
+  let vty = VMeta tnk []
   (i,_) <- newResiduation scope vty
   return (Meta i, vty)
 tcRho scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do    -- LET
@@ -114,12 +187,12 @@ tcRho scope (Typed body ann_ty) mb_ty = do                   -- ANNOT
   env <- scopeEnv scope
   v_ann_ty <- eval env ann_ty []
   (body,_) <- tcRho scope body (Just v_ann_ty)
-  instSigma scope (Typed body ann_ty) v_ann_ty mb_ty
+  (res1,res2) <- instSigma scope (Typed body ann_ty) v_ann_ty mb_ty
+  return (res1,res2)
 tcRho scope (FV ts) mb_ty = do
   case ts of
     []     -> do (i,tnk) <- newResiduation scope vtypeType
-                 env <- scopeEnv scope
-                 instSigma scope (FV []) (VMeta tnk env []) mb_ty
+                 instSigma scope (FV []) (VMeta tnk []) mb_ty
     (t:ts) -> do (t,ty) <- tcRho scope t mb_ty
 
                  let go []     ty = return ([],ty)
@@ -140,12 +213,12 @@ tcRho scope t@(RecType rs) (Just ty) = do
     VSort s
       | s == cType  -> return ()
       | s == cPType -> return ()
-    VMeta i env vs  -> case rs of
-                         [] -> unifyVar scope i env vs vtypePType
-                         _  -> return ()
-    ty              -> do ty <- zonkTerm =<< value2term (scopeVars scope) ty
-                          evalError ("The record type" <+> ppTerm Unqualified 0 t $$
-                                     "cannot be of type" <+> ppTerm Unqualified 0 ty)
+    VMeta i vs  -> case rs of
+                     [] -> unifyVar scope i vs vtypePType
+                     _  -> return ()
+    ty          -> do ty <- value2term (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')
   return (f (RecType rs),ty)
 tcRho scope t@(Table p res) mb_ty = do
@@ -160,7 +233,7 @@ tcRho scope (Prod bt x ty1 ty2) mb_ty = do
   instSigma scope (Prod bt x ty1 ty2) vtypeType mb_ty
 tcRho scope (S t p) mb_ty = do
   env <- scopeEnv scope
-  let mk_val (_,tnk) = VMeta tnk env []
+  let mk_val (_,tnk) = VMeta tnk []
   p_ty   <- fmap mk_val $ newResiduation scope vtypePType
   res_ty <- case mb_ty of
               Nothing -> fmap mk_val $ newResiduation scope vtypeType
@@ -171,7 +244,7 @@ tcRho scope (S t p) mb_ty = do
   return (S t p, res_ty)
 tcRho scope (T tt ps) Nothing = do                           -- ABS1/AABS1 for tables
   env <- scopeEnv scope
-  let mk_val (_,tnk) = VMeta tnk env []
+  let mk_val (_,tnk) = VMeta tnk []
   p_ty   <- case tt of
               TRaw      -> fmap mk_val $ newResiduation scope vtypePType
               TTyped ty -> do (ty, _) <- tcRho scope ty (Just vtypeType)
@@ -214,9 +287,8 @@ tcRho scope (R rs) (Just ty) = do
 tcRho scope (P t l) mb_ty = do
   l_ty   <- case mb_ty of
               Just ty -> return ty
-              Nothing -> do env <- scopeEnv scope
-                            (i,tnk) <- newResiduation scope vtypeType
-                            return (VMeta tnk env [])
+              Nothing -> do (i,tnk) <- newResiduation scope vtypeType
+                            return (VMeta tnk [])
   (t,t_ty) <- tcRho scope t (Just (VRecType [(l,l_ty)]))
   return (P t l,l_ty)
 tcRho scope (C t1 t2) mb_ty = do
@@ -261,7 +333,7 @@ tcRho scope t@(EPatt min max p) mb_ty = do
   (scope,f,ty) <- case mb_ty of
                     Nothing -> do env <- scopeEnv scope
                                   (i,tnk) <- newResiduation scope vtypeType
-                                  return (scope,id,VMeta tnk env [])
+                                  return (scope,id,VMeta tnk [])
                     Just ty -> do (scope,f,ty) <- skolemise scope ty
                                   case ty of
                                     VPattType ty -> return (scope,f,ty)
@@ -279,13 +351,16 @@ tcCases scope ((p,t):cs) p_ty mb_res_ty = do
 
 tcApp scope t0 t@(App fun (ImplArg arg)) = do                  -- APP1
   (fun,fun_ty) <- tcApp scope t0 fun
-  (bt, _, arg_ty, res_ty) <- unifyFun scope fun_ty
+  (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 arg (Just arg_ty)
-  env <- scopeEnv scope
-  varg <- eval env arg []
+  res_ty <- case res_ty of
+              VClosure res_env res_ty -> do env <- scopeEnv scope
+                                            tnk <- newThunk env arg
+                                            eval ((x,tnk):res_env) res_ty []
+              res_ty              -> return res_ty
   return (App fun (ImplArg arg), res_ty)
 tcApp scope t0 (App fun arg) = do                              -- APP2
   (fun,fun_ty) <- tcApp scope t0 fun
@@ -349,8 +424,7 @@ tcPatt scope (PR rs) ty0 = do
   let mk_ltys  []            = return []
       mk_ltys  ((l,p):rs)    = do (_,tnk) <- newResiduation scope vtypePType
                                   ltys <- mk_ltys rs
-                                  env <- scopeEnv scope
-                                  return ((l,p,VMeta tnk env []) : ltys)
+                                  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
@@ -410,8 +484,8 @@ tcRecTypeFields scope ((l,ty):rs) mb_ty = do
              VSort s
                | s == cType  -> return (Just sort)
                | s == cPType -> return mb_ty
-             VMeta _ _ _     -> return mb_ty
-             _               -> do sort <- zonkTerm =<< value2term (scopeVars scope) sort
+             VMeta _ _       -> return mb_ty
+             _               -> do sort <- value2term (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
@@ -427,20 +501,20 @@ instSigma scope t ty1 (Just ty2) = do                       -- INST2
 
 -- | Invariant: the second argument is in weak-prenex form
 subsCheckRho :: Scope s -> Term -> Sigma s -> Rho s -> EvalM s Term
-subsCheckRho scope t ty1@(VMeta i env vs) ty2 = do
+subsCheckRho scope t ty1@(VMeta i vs) ty2 = do
   mv <- getRef i
   case mv of
     Residuation _ _ _ -> do unify scope ty1 ty2
                             return t
-    Bound ty1         -> do vty1 <- eval env ty1 vs
-                            subsCheckRho scope t vty1 ty2
-subsCheckRho scope t ty1 ty2@(VMeta i env vs) = do
+    Evaluated _ ty1   -> do ty1 <- apply ty1 vs
+                            subsCheckRho scope t ty1 ty2
+subsCheckRho scope t ty1 ty2@(VMeta i vs) = do
   mv <- getRef i
   case mv of
     Residuation _ _ _ -> do unify scope ty1 ty2
                             return t
-    Bound ty2         -> do vty2 <- eval env ty2 vs
-                            subsCheckRho scope t ty1 vty2
+    Evaluated _ ty2   -> do ty2 <- apply ty2 vs
+                            subsCheckRho scope t ty1 ty2
 subsCheckRho scope t (VProd Implicit x ty1 ty2) rho2 = do     -- Rule SPEC
   (i,tnk) <- newResiduation scope ty1
   ty2 <- case ty2 of
@@ -551,7 +625,7 @@ unifyFun :: Scope s -> Rho s -> EvalM s (BindType, Ident, Sigma s, Rho s)
 unifyFun scope (VProd bt x arg res) =
   return (bt,x,arg,res)
 unifyFun scope tau = do
-  let mk_val (_,tnk) = VMeta tnk [] []
+  let mk_val (_,tnk) = VMeta tnk []
   arg <- fmap mk_val $ newResiduation scope vtypeType
   res <- fmap mk_val $ newResiduation scope vtypeType
   let bt = Explicit
@@ -562,8 +636,7 @@ unifyTbl :: Scope s -> Rho s -> EvalM s (Sigma s, Rho s)
 unifyTbl scope (VTable arg res) =
   return (arg,res)
 unifyTbl scope tau = do
-  env <- scopeEnv scope
-  let mk_val (i,tnk) = VMeta tnk env []
+  let mk_val (i,tnk) = VMeta tnk []
   arg <- fmap mk_val $ newResiduation scope vtypePType
   res <- fmap mk_val $ newResiduation scope vtypeType
   unify scope tau (VTable arg res)
@@ -578,17 +651,30 @@ unify scope (VGen i vs1)       (VGen j vs2)
 unify scope (VTable p1 res1) (VTable p2 res2) = do
   unify scope p1   p2
   unify scope res1 res2
-unify scope (VMeta i env1 vs1) (VMeta j env2 vs2)
-  | i  == j                    = sequence_ (zipWith (unifyThunk scope) vs1 vs2)
-  | otherwise                  = do mv <- getRef j
-                                    case mv of
-                                      Bound t2          -> do v2 <- eval env2 t2 vs2
-                                                              unify scope (VMeta i env1 vs1) v2
-                                      Residuation j _ _ -> setRef i (Bound (Meta j))
+unify scope (VMeta i vs1) (VMeta j vs2)
+  | i  == j   = sequence_ (zipWith (unifyThunk scope) vs1 vs2)
+  | otherwise = do 
+      mv <- getRef i
+      case mv of
+        Evaluated _ v1 -> do
+          v1 <- apply v1 vs1
+          unify scope v1 (VMeta j vs2)
+        Residuation _ scope1 _ -> do
+          mv <- getRef 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))
+              where
+                m = length scope1
+                n = length scope2 
 unify scope (VInt i)       (VInt j)
   | i == j                     = return ()
-unify scope (VMeta i env vs) v = unifyVar scope i env vs v
-unify scope v (VMeta i env vs) = unifyVar scope i env vs v
+unify scope (VMeta i vs) v = unifyVar scope i vs v
+unify scope v (VMeta i vs) = unifyVar scope i vs v
 unify scope v1 v2 = do
   t1 <- value2term (scopeVars scope) v1
   t2 <- value2term (scopeVars scope) v2
@@ -602,18 +688,78 @@ unifyThunk scope tnk1 tnk2 = do
     (Evaluated _ v1,Evaluated _ v2) -> unify scope v1 v2
 
 -- | Invariant: tv1 is a flexible type variable
-unifyVar :: Scope s -> Thunk s -> Env s -> [Thunk s] -> Tau s -> EvalM s ()
-unifyVar scope tnk env vs ty2 = do            -- Check whether i is bound
+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
   case mv of
-    Bound ty1              -> do v <- eval env ty1 vs
-                                 unify scope v ty2
-    Residuation i scope' _ -> do ty2' <- value2term (scopeVars scope') ty2
-                                 ms2 <- getMetaVars [(scope,ty2)]
-                                 if tnk `elem` ms2
-                                   then evalError ("Occurs check for" <+> ppMeta i <+> "in:" $$
-                                                   nest 2 (ppTerm Unqualified 0 ty2'))
-                                   else setRef tnk (Bound ty2')
+    Evaluated _ ty1        -> do ty1 <- apply ty1 vs
+                                 unify scope ty1 ty2
+    Residuation i scope' _ -> do let m = length scope'
+                                     n = length scope
+                                 check m n ty2
+                                 setRef tnk (Evaluated m ty2)
+  where
+    check m n (VApp f vs) = mapM_ (follow m n) vs
+    check m n (VMeta i vs)
+      | tnk == i  = do ty1 <- value2term (scopeVars scope) (VMeta tnk vs)
+                       ty2 <- value2term (scopeVars scope) ty2
+                       evalError ("Occurs check for" <+> ppTerm Unqualified 0 ty1 <+> "in:" $$
+                                  nest 2 (ppTerm Unqualified 0 ty2))
+      | otherwise = do
+          s <- getRef i
+          case s of
+            Evaluated _ v -> do v <- apply v vs
+                                check m n v
+            _             -> mapM_ (follow 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
+    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
+    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
+    check m n (VP v l vs) =
+      check m n v >> mapM_ (follow 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 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 (VSort _) = return ()
+    check m n (VInt _) = return ()
+    check m n (VFlt _) = return ()
+    check m n (VStr _) = return ()
+    check m n VEmpty   = return ()
+    check m n (VC v1 v2) =
+      check m n v1 >> check m n v2
+    check m n (VGlue v1 v2) =
+      check m n v1 >> check m n v2
+    check m n (VPatt _ _ _) = return ()
+    check m n (VPattType v) =
+      check m n v
+    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
@@ -632,11 +778,11 @@ instantiate scope t ty = do
 
 -- | Build fresh lambda abstractions for the topmost implicit arguments
 skolemise :: Scope s -> Sigma s -> EvalM s (Scope s, Term->Term, Rho s)
-skolemise scope ty@(VMeta i env vs) = do
+skolemise scope ty@(VMeta i vs) = do
   mv <- getRef i
   case mv of
     Residuation _ _ _ -> return (scope,id,ty)                   -- guarded constant?
-    Bound ty          -> do ty <- eval env ty vs
+    Evaluated _ ty    -> do ty <- apply ty vs
                             skolemise scope ty
 skolemise scope (VProd Implicit x ty1 ty2) = do
   let v = newVar scope
@@ -652,17 +798,112 @@ skolemise scope ty = do
 -- | Quantify over the specified type variables (all flexible)
 quantify :: Scope s -> Term -> [Thunk s] -> Rho s -> EvalM s (Term,Sigma s)
 quantify scope t tvs ty = do
-  let used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
-      new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
-  env <- scopeEnv ([(v,vtypeType) | v <- new_bndrs]++scope)
-  mapM_ (bind env) (zip tvs new_bndrs)
-  let vty = foldr (\v -> VProd Implicit v vtypeType) ty new_bndrs
-  return (foldr (Abs Implicit) t new_bndrs,vty)
+  let m = length tvs
+      n = length scope
+  (used_bndrs,ty) <- check m n [] ty
+  let new_bndrs  = take m (allBinders \\ used_bndrs)
+  mapM_ bind (zip3 [0..] tvs new_bndrs)
+  let ty' = foldr (\ty -> VProd Implicit ty vtypeType) ty new_bndrs
+  return (foldr (Abs Implicit) t new_bndrs,ty')
   where
-    bind env (tnk, name) = setRef tnk (Bound (Vr name))
-
-    bndrs (VProd _ x v1 v2) = [x] ++ bndrs v1  ++ bndrs v2
-    bndrs _                 = []
+    bind (i, tnk, name) = setRef tnk (Evaluated (length scope) (VGen i []))
+
+    check m n xs (VApp f vs)       = do
+      (xs,vs) <- mapAccumM (follow m n) xs vs
+      return (xs,VApp f vs)
+    check m n xs (VMeta i vs)      = do
+      s <- getRef 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)
+    check m n st (VGen i vs)= do
+      (st,vs) <- mapAccumM (follow 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 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)
+    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
+      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
+      return (xs,VP v l vs)
+    check m n xs (VExtR v1 v2)     = do
+      (xs,v1) <- check m n xs v1
+      (xs,v2) <- check m n xs v2
+      return (xs,VExtR v1 v2)
+    check m n xs (VTable v1 v2)    = 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
+      (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)
+    check m n xs (VV ty cs)        = do
+      (xs,ty) <- check m n xs ty
+      (xs,cs) <- mapAccumM (follow 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
+      return (xs,VS v1 tnk vs)
+    check m n xs v@(VSort _)       = return (xs,v)
+    check m n xs v@(VInt _)        = return (xs,v)
+    check m n xs v@(VFlt _)        = return (xs,v)
+    check m n xs v@(VStr _)        = return (xs,v)
+    check m n xs v@VEmpty          = return (xs,v)
+    check m n xs (VC v1 v2)        = do
+      (xs,v1) <- check m n xs v1
+      (xs,v2) <- check m n xs v2
+      return (xs,VC v1 v2)
+    check m n xs (VGlue v1 v2)        = do
+      (xs,v1) <- check m n xs v1
+      (xs,v2) <- check m n xs v2
+      return (xs,VGlue v1 v2)
+    check m n xs v@(VPatt _ _ _)   = return (xs,v)
+    check m n xs (VPattType v)     = do
+      (xs,v) <- check m n xs v
+      return (xs,VPattType v)
+    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
+                                              (xs,v2) <- check m n xs v2
+                                              return (xs,(v1,v2)))
+                           xs vs
+      return (xs,VAlts v vs)
+    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)
+
+    mapAccumM :: Monad m => (a -> b -> m (a,c)) -> a -> [b] -> m (a,[c])
+    mapAccumM f s []     = return (s,[])
+    mapAccumM f s (x:xs) = do
+      (s,y)  <- f s x
+      (s,ys) <- mapAccumM f s xs
+      return (s,y:ys)
 
 allBinders :: [Ident]    -- a,b,..z, a1, b1,... z1, a2, b2,...
 allBinders = [ identS [x]          | x <- ['a'..'z'] ] ++
@@ -699,24 +940,35 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go ty acc) [] sc_tys
     follow acc tnk = force tnk >>= \v -> go v acc
 
     -- Get the MetaIds from a term; no duplicates in result
-    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 env args) acc
-      | m `elem` acc          = return acc
-      | otherwise             = do res <- getRef m
-                                   case res of
-                                     Bound _ -> return acc
-                                     _       -> foldM follow (m:acc) args
-    go (VApp f args)      acc = foldM follow acc args
-    go v                  acc = unimplemented ("go "++showValue v)
+    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
+      | m `elem` acc         = return acc
+      | otherwise            = do res <- getRef m
+                                  case res of
+                                    Evaluated _ v -> go v acc
+                                    _             -> foldM follow (m:acc) args
+    go (VApp f args)     acc = foldM follow acc args
+    go v                 acc = unimplemented ("go "++showValue v)
 
 -- | Eliminate any substitutions in a term
-zonkTerm :: Term -> EvalM s Term
-zonkTerm (Meta i) = do
+zonkTerm :: [Ident] -> Term -> EvalM s Term
+zonkTerm xs (Abs b x t) = do
+  t <- zonkTerm (x:xs) t
+  return (Abs b x t)
+zonkTerm xs (Prod b x t1 t2) = do
+  t1 <- zonkTerm xs  t1
+  t2 <- zonkTerm xs' t2
+  return (Prod b x t1 t2)
+  where
+    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
@@ -726,7 +978,5 @@ zonkTerm (Meta i) = do
     Hole _            -> return (Meta i)
     Residuation _ _ _ -> return (Meta i)
     Narrowing _ _     -> return (Meta i)
-    Bound t           -> do t <- zonkTerm t
-                            setRef tnk (Bound t)     -- "Short out" multiple hops
-                            return t
-zonkTerm t = composOp zonkTerm t
+    Evaluated _ v     -> zonkTerm xs =<< value2term xs v
+zonkTerm xs t = composOp (zonkTerm xs) t