diff --git a/src/compiler/api/GF/Compile/CheckGrammar.hs b/src/compiler/api/GF/Compile/CheckGrammar.hs
index b366b55d6..5f0deb696 100644
--- a/src/compiler/api/GF/Compile/CheckGrammar.hs
+++ b/src/compiler/api/GF/Compile/CheckGrammar.hs
@@ -232,12 +232,12 @@ checkInfo opts cwd sgr sm (c,info) = checkInModule cwd (snd sm) NoLoc empty $ do
     ResOverload os tysts -> chIn NoLoc "overloading" $ do
       tysts' <- mapM (uncurry $ flip (\(L loc1 t) (L loc2 ty) -> checkLType g t ty >>= \(t,ty) -> return (L loc1 t, L loc2 ty))) tysts  -- return explicit ones
       tysts0 <- lookupOverload gr (fst sm,c)  -- check against inherited ones too
-      tysts1 <- mapM (uncurry $ flip (checkLType g))
-                  [(mkFunType args val,tr) | (args,(val,tr)) <- tysts0]
+      tysts1 <- sequence
+                  [checkLType g tr (mkFunType args val) | (args,(val,tr)) <- tysts0]
       --- this can only be a partial guarantee, since matching
       --- with value type is only possible if expected type is given
-      checkUniq $
-        sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
+      --checkUniq $
+      --  sort [let (xs,t) = typeFormCnc x in t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1]
       update sm c (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (L loc pcs)) _ -> do
diff --git a/src/compiler/api/GF/Compile/Compute/Concrete2.hs b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
index 464555f1d..8c260cc2b 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
@@ -3,13 +3,13 @@
 module GF.Compile.Compute.Concrete2
            (Env, Scope, Value(..), Variants(..), OptionInfo(..), ChoiceMap, cleanOptions,
             ConstValue(..), ConstVariants(..), Globals(..), PredefTable, EvalM,
-            mapVariants, unvariants, variants2consts, consts2variants,
-            runEvalM, runEvalMWithOpts, stdPredef, globals, withState,
+            mapVariants, mapVariantsC, unvariants, variants2consts, consts2variants,
+            runEvalM, runEvalMWithOpts, stdPredef, globals,
             PredefImpl, Predef(..), ($\),
             pdCanonicalArgs, pdArity,
             normalForm, normalFlatForm,
-            eval, apply, value2term, value2termM, bubble, patternMatch, vtableSelect, State(..),
-            newResiduation, getMeta, setMeta, MetaState(..), variants, try,
+            eval, apply, value2term, value2termM, value2int, value2float, bubble, patternMatch, vtableSelect, State(..),
+            newResiduation, checkpoint, getMeta, setMeta, MetaState(..), variants, try,
             evalError, evalWarn, ppValue, Choice(..), unit, poison, split, split3, split4, mapC, mapCM) where
 
 import Prelude hiding ((<>)) -- GHC 8.4.1 clash with Text.PrettyPrint
@@ -24,6 +24,7 @@ import GF.Grammar.Predef
 import GF.Grammar.Printer hiding (ppValue)
 import GF.Grammar.Lockfield(lockLabel)
 import GF.Text.Pretty hiding (empty)
+import qualified GF.Text.Pretty as PP
 import Control.Monad
 import Control.Applicative hiding (Const)
 import qualified Control.Applicative as A
@@ -65,7 +66,7 @@ data Value
   | VGen  {-# UNPACK #-} !Int [Value]
   | VClosure Env Choice Term
   | VProd BindType Ident Value Value
-  | VRecType [(Label, Bool, Value)]
+  | VRecType [(Label, Bool, Value)] Bool
   | VR [(Label, Value)]
   | VP Value Label [Value]
   | VExtR Value Value
@@ -89,16 +90,20 @@ data Value
   | VReset Ident (Maybe Value) Value (Maybe QIdent)
   | VSymCat Int LIndex [(LIndex, (Value, Type))]
   | VError Doc
-  | VInts (Maybe Integer) (Maybe Integer)
+  | VInts Integer Bool
 
 data Variants
   = VarFree [Value]
-  | VarOpts Value [(Value, Value)]
+  | VarOpts Value [(Maybe Value, Value)]
 
 mapVariants :: (Value -> Value) -> Variants -> Variants
 mapVariants f (VarFree vs)   = VarFree (f <$> vs)
 mapVariants f (VarOpts n cs) = VarOpts n (second f <$> cs)
 
+mapVariantsC :: (Choice -> Value -> Value) -> Choice -> Variants -> Variants
+mapVariantsC f c (VarFree vs)   = VarFree (mapC f c vs)
+mapVariantsC f c (VarOpts n cs) = VarOpts n (mapC (\c (x,y) -> (x,f c y)) c cs)
+
 unvariants :: Variants -> [Value]
 unvariants (VarFree vs)   = vs
 unvariants (VarOpts n cs) = snd <$> cs
@@ -106,7 +111,7 @@ unvariants (VarOpts n cs) = snd <$> cs
 isCanonicalForm :: Bool -> Value -> Bool
 isCanonicalForm flat  (VClosure {})       = True
 isCanonicalForm flat  (VProd b x d cod)   = isCanonicalForm flat d && isCanonicalForm flat cod
-isCanonicalForm flat  (VRecType fs)       = all (\(l,_,ty) -> isCanonicalForm flat ty) fs
+isCanonicalForm flat  (VRecType fs _)     = all (\(l,_,ty) -> isCanonicalForm flat ty) fs
 isCanonicalForm flat  (VR {})             = True
 isCanonicalForm flat  (VTable d cod)      = isCanonicalForm flat d && isCanonicalForm flat cod
 isCanonicalForm flat  (VT {})             = True
@@ -133,7 +138,7 @@ data ConstValue a
 
 data ConstVariants a
   = ConstFree [ConstValue a]
-  | ConstOpts Value [(Value, ConstValue a)]
+  | ConstOpts Value [(Maybe Value, ConstValue a)]
 
 mapConstVs :: (ConstValue a -> ConstValue b) -> ConstVariants a -> ConstVariants b
 mapConstVs f (ConstFree vs)   = ConstFree (f <$> vs)
@@ -200,7 +205,7 @@ eval g env s (Prod b x t1 t2)[]
   | otherwise                   = 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, True, eval g env s ty [])) s lbls)
+eval g env s (RecType lbls) []  = VRecType (mapC (\s (lbl,ty) -> (lbl, True, eval g env s ty [])) s lbls) False
 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 $$
@@ -214,7 +219,7 @@ eval g env s (P t lbl)      vs  = let project (VR as)        = case lookup lbl a
 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,o,v) -> update3 lbl o v as) as1 as2)
+                                      extend (VRecType as1 e1) (VRecType as2 e2)=VRecType (foldl (\as (lbl,o,v) -> update3 lbl o v as) as1 as2) (e1 || e2)
                                       extend (VFV i fvs)    v2               = VFV i (mapVariants (`extend` v2) fvs)
                                       extend v1             (VFV i fvs)      = VFV i (mapVariants (v1 `extend`) fvs)
                                       extend (VMeta i vs)   v2               = VSusp i (\v -> extend (apply g v vs) v2) []
@@ -316,7 +321,7 @@ eval g env s (FV ts)        vs  = VFV s (VarFree (mapC (\s t -> eval g env s t v
 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 (eval g env s1 t1 [],eval g env s2 t2 [])) s2 as
                                   in VAlts vd vas
 eval g env c (Strs ts)      []  = VStrs (mapC (\c t -> eval g env c t []) c ts)
 eval g env c (Markup tag as ts) [] =
@@ -332,7 +337,8 @@ eval g env c t@(Opts n cs)  vs  = if null cs
                                            vn = eval g env c1 n []
                                            vcs = mapC evalOpt c cs
                                        in VFV c3 (VarOpts vn vcs)
-  where evalOpt c' (l,t) = let (c1,c2) = split c' in (eval g env c1 l [], eval g env c2 t vs)
+  where evalOpt c' (Just l, t) = let (c1,c2) = split c' in (Just (eval g env c1 l []), eval g env c2 t vs)
+        evalOpt c' (Nothing,t) = let (c1,c2) = split c' in (Nothing,                   eval g env c2 t vs)
 eval g env c t              vs  = VError ("Cannot reduce term" <+> pp t)
 
 evalPredef :: Globals -> Choice -> Ident -> [Value] -> Value
@@ -348,7 +354,7 @@ evalPredef g@(Gl gr pds) c n args =
 
 stdPredef :: Globals -> PredefTable
 stdPredef g = Map.fromList
-  [(cInts,   pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts (Just i) (Just i); vs -> VApp c (cPredef,cInts) vs}))
+  [(cInts,   pdArity 1 $\ \g c vs -> Const (case vs of {[VInt i] -> VInts i False; vs -> VApp c (cPredef,cInts) vs}))
   ,(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)))
@@ -392,9 +398,9 @@ bubble v = snd (bubble v)
     bubble (VGen i vs) = liftL (VGen i) vs
     bubble (VClosure env c t) = liftL' (\env -> VClosure env c t) env
     bubble (VProd bt x v1 v2) = lift2 (VProd bt x) v1 v2
-    bubble v@(VRecType lbls) =
+    bubble v@(VRecType lbls ext) =
       let (union,lbls') = mapAccumL descendR Map.empty lbls
-      in (union, addVariants (VRecType lbls') union)
+      in (union, addVariants (VRecType lbls' ext) union)
     bubble (VR as) = liftL' VR as
     bubble (VP v l vs) = lift1L (\v vs -> VP v l vs) v vs
     bubble (VExtR v1 v2) = lift2 VExtR v1 v2
@@ -414,18 +420,20 @@ bubble v = snd (bubble v)
     bubble v@(VFV c (VarFree vs))
       | null vs   = (Map.empty, v)
       | otherwise = let (union,vs') = mapAccumL descend Map.empty vs
-                    in (Map.insert c (BubbleFree (length vs),1) union, addVariants (VFV c (VarFree vs')) union)
+                    in (Map.insert c (BubbleFree (length vs),1) union, VFV c (VarFree vs'))
     bubble v@(VFV c (VarOpts n os))
       | null os   = (Map.empty, v)
       | otherwise = let (union,os') = mapAccumL (\acc (k,v) -> second (k,) $ descend acc v) Map.empty os
-                    in (Map.insert c (BubbleOpts n (fst <$> os),1) union, addVariants (VFV c (VarOpts n os')) union)
+                    in (Map.insert c (BubbleOpts n (map (\(l,t) -> fromMaybe t l) os),1) union, VFV c (VarOpts n os'))
     bubble (VAlts v vs) = lift1L2 VAlts v vs
     bubble (VStrs vs) = liftL VStrs vs
     bubble (VMarkup tag attrs vs) =
       let (union1,attrs') = mapAccumL descend' Map.empty attrs
           (union2,vs')    = mapAccumL descend  union1 vs
       in (union2, VMarkup tag attrs' vs')
-    bubble (VReset ctl mb_cv v id) = lift1 (\v -> VReset ctl mb_cv v id) v
+    bubble (VReset ctl mb_cv v id) =
+      let (union,v') = bubble v
+      in (Map.empty,VReset ctl mb_cv v' id)
     bubble (VSymCat d i0 vs) =
       let (union,vs') = mapAccumL descendC Map.empty vs
       in (union, addVariants (VSymCat d i0 vs') union)
@@ -501,7 +509,7 @@ bubble v = snd (bubble v)
         addVariant c (bvs,cnt) v
           | cnt > 1   = VFV c $ case bvs of
                                   BubbleFree k    -> VarFree (replicate k v)
-                                  BubbleOpts n os -> VarOpts n ((,v) <$> os)
+                                  BubbleOpts n os -> VarOpts n (map (\l -> (Just l,v)) os)
           | otherwise = v
 
     unitfy = fmap (\(n,_) -> (n,1))
@@ -733,9 +741,6 @@ runEvalMWithOpts g cs (EvalM f) = Check $ \(es,ws) ->
   where
     init = State cs Map.empty []
 
-withState :: State -> EvalM a -> EvalM a
-withState state (EvalM f) = EvalM $ \g k _ r ws -> f g k state r ws
-
 reset :: EvalM a -> EvalM [a]
 reset (EvalM f) = EvalM $ \g k state r ws ->
   case f g (\x state xs ws -> Success (x:xs) ws) state [] ws of
@@ -773,24 +778,36 @@ variants' c f xs = EvalM (\g k state@(State choices metas opts) r msgs ->
                      Fail    msg msgs -> Fail msg msgs
                      Success ts  msgs -> backtrack g (j+1) xs choices metas opts ts msgs
 
-try :: (a -> EvalM b) -> ([(b,State)] -> EvalM b) -> [a] -> EvalM b
-try f select xs = EvalM (\g k state r msgs ->
-  let (res,msgs') = backtrack g xs state [] msgs
+try :: Int -> (a -> EvalM b) -> ([b] -> EvalM b) -> [a] -> EvalM b
+try sz f select xs = EvalM (\g k state r msgs ->
+  let (state',res,msgs') = backtrack sz g xs state [] msgs
   in case select res of
-       EvalM f' -> f' g k state r msgs')
+       EvalM f' -> f' g k state' r msgs')
   where
-    backtrack g []     state res msgs = (res,msgs)
-    backtrack g (x:xs) state res msgs =
+    backtrack sz g []     state res msgs = (state,res,msgs)
+    backtrack sz 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
+        EvalM f -> case f g (\y state' (_,ys) msgs -> Success (cut sz state state',y:ys) msgs) state (state,res) msgs of
+                     Fail msg _               -> backtrack sz g xs state res msgs
+                     Success (state,res) msgs -> backtrack sz g xs state res msgs
+
+    cut sz state state' = state'{metaVars=Map.mapWithKey select (metaVars state')}
+      where
+        select k ms
+          | k <= sz   = ms
+          | otherwise = case Map.lookup k (metaVars state) of
+                          Just ms -> ms
+                          Nothing -> ms
 
 newResiduation :: Scope -> EvalM MetaId
 newResiduation scope = EvalM (\g k (State choices metas opts) r msgs ->
   let meta_id = Map.size metas+1
   in k meta_id (State choices (Map.insert meta_id (Residuation scope) metas) opts) r msgs)
 
+checkpoint :: EvalM Int
+checkpoint = EvalM (\g k state r msgs ->
+  k (Map.size (metaVars state)) state r msgs)
+
 getMeta :: MetaId -> EvalM MetaState
 getMeta i = EvalM (\g k state r msgs ->
   case Map.lookup i (metaVars state) of
@@ -833,7 +850,7 @@ value2termM flat xs (VProd b x v1 v2) = do
   t1 <- value2termM flat xs v1
   t2 <- value2termM flat xs v2
   return (Prod b x t1 t2)
-value2termM flat xs (VRecType lbls) = do
+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
@@ -908,7 +925,7 @@ value2termM flat xs (VFV i (VarOpts n os)) =
     let j = fromMaybe 0 (Map.lookup i choices)
     in case os `maybeAt` j of
          Just (l,t) -> case value2termM flat xs t of
-                         EvalM f -> let oi = OptionInfo i n (fst <$> os)
+                         EvalM f -> let oi = OptionInfo i n (map (\(l,t) -> fromMaybe t l) os)
                                     in f g k (State choices metas (oi:opts)) r msgs
          Nothing    -> Fail ("Index" <+> j <+> "out of bounds for option:" $$ ppValue Unqualified 0 n) msgs
 value2termM flat xs (VPatt min max p) = return (EPatt min max p)
@@ -941,11 +958,36 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
          case ts of
            [t] -> return t
            ts  -> return (Markup identW [] ts)
+      | ctl == cConcat' = do
+         ts <- case mb_cv of
+                 Just (VInt n) -> return (genericTake n ts)
+                 Nothing       -> return ts
+                 _             -> evalError (pp "[concat: .. | ..] requires an integer constant")
+         case ts of
+           []  -> mzero
+           [t] -> return t
+           ts  -> return (Markup identW [] ts)
       | ctl == cOne =
          case (ts,mb_cv) of
            ([]  ,Nothing) -> mzero
            ([]  ,Just v)  -> value2termM flat xs v
            (t:ts,_)       -> return t
+      | ctl == cSelect =
+         case mb_cv of
+           Just (VInt n) | n >= 0    -> select n      ts'
+                         | otherwise -> select (-n-1) (reverse ts')
+                         where
+                           ts' = sortBy compareKey ts
+
+                           select _ []     = mzero
+                           select 0 (t:ts) =
+                             case t of
+                               R rs -> case lookup (ident2label cp1) rs  of
+                                         Just (_,t) -> return t
+                                         Nothing    -> evalError (pp "Missing label p1")
+                               _    -> evalError (pp "The term must be a record")
+                           select n (t:ts) = select (n-1) ts
+           _             -> evalError (pp "[select: .. | ..] requires an integer constant")
       | ctl == cDefault =
          case (ts,mb_cv) of
            ([]  ,Nothing) -> mzero
@@ -962,15 +1004,23 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
                 t <- listify mn cat ts
                 return (App (App (QC (mn,identS ("Conj"++cat))) ct) t)
            _             -> evalError (pp "[list: .. | ..] requires an argument")
+      | ctl == cLen =
+         case mb_cv of
+           Just cv  -> do g <- globals
+                          value2termM True xs (apply g cv [VInt (genericLength ts)])
+           Nothing  -> return (EInt (genericLength ts))
       | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
 
     listify mn cat [t1,t2] = do return (App (App (QC (mn,identS ("Base"++cat))) t1) t2)
     listify mn cat (t1:ts) = do t2 <- listify mn cat ts
                                 return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)
+
+    compareKey (R rs1) (R rs2) =
+      case (lookup (ident2label cp2) rs1, lookup (ident2label cp2) rs2) of
+        (Just (_,K s1), Just (_,K s2)) -> compare s1 s2
+
 value2termM flat xs (VError msg) = evalError msg
-value2termM flat xs (VInts Nothing    Nothing) = return (App (Q (cPredef,cInts)) (Meta 0))
-value2termM flat xs (VInts (Just min) Nothing) = return (App (Q (cPredef,cInts)) (EInt min))
-value2termM flat xs (VInts _       (Just max)) = return (App (Q (cPredef,cInts)) (EInt max))
+value2termM flat xs (VInts n _) = return (App (Q (cPredef,cInts)) (EInt n))
 value2termM flat xs v = evalError ("value2termM" <+> ppValue Unqualified 5 v)
 
 
@@ -986,6 +1036,7 @@ pattVars st (PSeq _ _ p1 _ _ p2) = pattVars (pattVars st p1) p2
 pattVars st _            = st
 
 
+
 ppValue q d (VApp c f vs) = prec d 4 (hsep (ppQIdent q f : 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))
@@ -995,13 +1046,13 @@ ppValue q d (VProd bt x a b) =
   if x == identW && bt == Explicit
     then prec d 0 (ppValue q 4 a <+> "->" <+> ppValue q 0 b)
     else prec d 0 (parens (ppBind (bt,x) <+> ':' <+> ppValue q 0 a) <+> "->" <+> ppValue q 0 b)
-ppValue q d (VRecType xs)
+ppValue q d (VRecType xs ext)
   | q == Terse         = case [cat | (l,_,_) <- xs, let (p,cat) = splitAt 5 (showIdent (label2ident l)), p == "lock_"] of
                            [cat] -> pp cat
                            _     -> doc
   | otherwise          = doc
   where
-    doc = braces (fsep (punctuate ';' [l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs]))
+    doc = braces (fsep (punctuate ';' ([l <+> (if o then ":" else ":?") <+> ppValue q 0 v | (l,o,v) <- xs] ++ [pp ".." | ext])))
 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"
@@ -1021,17 +1072,20 @@ 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 (VPattType v) = prec d 4 ("pattern" <+> ppValue q 0 v)
 ppValue q d (VFV i vs) = prec d 4 ("variants" <+> pp i <+> braces (fsep (punctuate ';' (map (ppValue q 0) (unvariants 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 (VMarkup _ _ _) = pp "VMarkup"
+ppValue q d (VReset ctl ct t _) = pp "[" <> pp ctl <> 
+                                  maybe PP.empty (\v -> pp ':' <+> ppValue q 6 v) ct <>
+                                  pp "|" <> ppValue q 0 t <>
+                                  pp "]"
 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 (VInts Nothing    Nothing)    = prec d 4 (pp "Ints ?")
-ppValue q d (VInts (Just min) Nothing)    = prec d 4 (pp "Ints" <+> brackets (pp min <> ".."))
-ppValue q d (VInts Nothing    (Just max)) = prec d 4 (pp "Ints" <+> brackets (".." <> pp max))
-ppValue q d (VInts (Just min) (Just max)) = prec d 4 (pp "Ints" <+> brackets (pp min <> ".." <> pp max))
+ppValue q d (VInts n ext)
+  | ext       = prec d 4 (pp "Ints" <+> brackets (pp n <> ".."))
+  | otherwise = prec d 4 (pp "Ints" <+> pp n)
 
 ppAltern q (x,y) = ppValue q 0 x <+> '/' <+> ppValue q 0 y
 
@@ -1103,6 +1157,12 @@ value2int g (VInt n)         = Const n
 value2int g (VFV s vs)       = CFV s (variants2consts (value2int g) vs)
 value2int g _                = RunTime
 
+value2float g (VMeta i vs)     = CSusp i (\v -> value2float g (apply g v vs))
+value2float g (VSusp i k vs)   = CSusp i (\v -> value2float g (apply g (k v) vs))
+value2float g (VFlt f)         = Const f
+value2float g (VFV s vs)       = CFV s (variants2consts (value2float g) vs)
+value2float g _                = RunTime
+
 newtype Choice = Choice { unchoice :: Integer }
   deriving (Eq,Ord,Pretty,Show)
 
diff --git a/src/compiler/api/GF/Compile/GeneratePMCFG.hs b/src/compiler/api/GF/Compile/GeneratePMCFG.hs
index b5861b350..0ff244c3d 100644
--- a/src/compiler/api/GF/Compile/GeneratePMCFG.hs
+++ b/src/compiler/api/GF/Compile/GeneratePMCFG.hs
@@ -214,11 +214,28 @@ str2lin (VSymCat d r rs) = do (r, rs) <- compute r rs
 str2lin (VSymVar d r)    = return [SymVar d r]
 str2lin VEmpty           = return []
 str2lin (VC v1 v2)       = liftM2 (++) (str2lin v1) (str2lin v2)
-str2lin (VAlts def alts) = do def <- str2lin def
-                              alts <- forM alts $ \(v,VStrs vs) -> do
-                                lin <- str2lin v
-                                return (lin,[s | VStr s <- vs])
+str2lin v0@(VAlts def alts)
+                         = do def <- str2lin def
+                              alts <- forM alts $ \(v1,v2) -> do
+                                lin <- str2lin v1
+                                ss  <- to_strs v2
+                                return (lin,ss)
                               return [SymKP def alts]
+  where
+    to_strs (VStrs vs)    = mapM to_str vs
+    to_strs (VPatt _ _ p) = from_patt p
+    to_strs v             = fail
+
+    to_str (VStr s) = return s
+    to_str _        = fail
+
+    from_patt (PAlt p1 p2) = liftM2 (++) (from_patt p1) (from_patt p2)
+    from_patt (PSeq _ _ p1 _ _ p2) = liftM2 (liftM2 (++)) (from_patt p1) (from_patt p2)
+    from_patt (PString s)  = return [s]
+    from_patt (PChars cs)  = return (map (:[]) cs)
+    from_patt _            = fail
+
+    fail = evalError ("Complex patterns are not supported in:" $$ nest 2 (pp (showValue v0)))
 str2lin v                = do t <- value2term False [] v
                               evalError ("the string:" <+> ppTerm Unqualified 0 t $$
                                          "cannot be evaluated at compile time.")
diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
index c90564296..d85972e95 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
@@ -14,7 +14,7 @@ import GF.Compile.Compute.Concrete2
 import GF.Infra.CheckM
 import GF.Data.ErrM ( Err(Ok, Bad) )
 import Control.Applicative(Applicative(..),(<|>))
-import Control.Monad(ap,liftM,mplus,foldM,zipWithM,forM,filterM,unless)
+import Control.Monad(ap,liftM,liftM2,mplus,foldM,zipWithM,forM,filterM,unless)
 import Control.Monad.ST
 import GF.Text.Pretty
 import Data.STRef
@@ -75,7 +75,7 @@ vtypePType = VSort cPType
 vtypeMarkup= VApp poison (cPredef,cMarkup) []
 
 tcRho :: Scope -> Choice -> Term -> Maybe Rho -> EvalM (Term, Rho)
-tcRho scope s t@(EInt i)   mb_ty = instSigma scope s t (VInts (Just i) Nothing) mb_ty -- INT
+tcRho scope s t@(EInt i)   mb_ty = instSigma scope s t (VInts i True) 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
@@ -117,7 +117,7 @@ tcRho scope c (Abs bt var body) Nothing = do                   -- ABS1
         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 (VRecType as _)   = foldM (\st (l,_,v) -> check m n st v) st as
     check m n st (VR as)           =
       foldM (\st (lbl,tnk) -> check m n st tnk) st as
     check m n st (VP v l vs)       =
@@ -200,7 +200,7 @@ tcRho scope c (FV ts) mb_ty = do
 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
+  (rs,mb_ty) <- tcRecTypeFields scope c [] rs Nothing
   return (RecType rs,fromMaybe vtypePType mb_ty)
 tcRho scope c t@(RecType rs) (Just ty) = do
   (scope,f,ty') <- skolemise scope ty
@@ -214,7 +214,7 @@ tcRho scope c t@(RecType rs) (Just ty) = do
     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')
+  (rs,mb_ty) <- tcRecTypeFields scope c [] rs (Just ty')
   return (f (RecType rs),ty)
 tcRho scope s t@(Table p res) mb_ty = do
   let (s1,s23) = split s
@@ -241,15 +241,13 @@ tcRho scope c (S t p) mb_ty = do
   return (S t p, res_ty)
 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 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 c2 ps p_ty res_ty
+  mb_p_ty <- case tt of
+               TRaw      -> return Nothing
+               TTyped ty -> do let (c3,c4) = split c1
+                               (ty, _) <- tcRho scope c3 ty (Just vtypeType)
+                               g <- globals
+                               return (Just (eval g (scopeEnv scope) c4 ty []))
+  (ps,p_ty,res_ty) <- tcCases scope c2 ps mb_p_ty Nothing
   p_ty_t <- value2termM True [] p_ty
   return (T (TTyped p_ty_t) ps, VTable p_ty res_ty)
 tcRho scope c (T tt ps) (Just ty) = do                         -- ABS2/AABS2 for tables
@@ -262,8 +260,9 @@ tcRho scope c (T tt ps) (Just ty) = do                         -- ABS2/AABS2 for
     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
+                    subsCheckRho scope (Meta 0) (eval g (scopeEnv scope) c2 ty []) p_ty
+                    return ()
+  (ps,p_ty,res_ty) <- tcCases scope c3 ps (Just p_ty) (Just 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 c (V p_ty ts) Nothing = do
@@ -290,22 +289,22 @@ tcRho scope c (V p_ty0 ts) (Just ty) = do
   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 c (R rs) Nothing = do
-  lttys <- inferRecFields scope c rs
+  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,True,ty) | (l,t,ty) <- lttys]
+          VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
          )
 tcRho scope c (R rs) (Just ty) = do
   (scope,f,ty') <- skolemise scope ty
   case ty' of
-    (VRecType ltys) -> do lttys <- checkRecFields scope c rs ltys
+    (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,True,ty) | (l,t,ty) <- lttys]
+                                  VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
                                  )
-    ty              -> do lttys <- inferRecFields scope c rs
+    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,True,ty) | (l,t,ty) <- lttys]
+                          let ty' = VRecType [(l,True,ty) | (l,t,ty) <- lttys] False
                           (t,_,_) <- subsCheckRho scope t ty' ty
                           return (t, ty')
 tcRho scope c (P t l) mb_ty = do
@@ -313,7 +312,7 @@ tcRho scope c (P t l) mb_ty = do
               Just ty -> return ty
               Nothing -> do i <- newResiduation scope
                             return (VMeta i [])
-  (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)]))
+  (t,t_ty) <- tcRho scope c t (Just (VRecType [(l,True,l_ty)] True))
   return (P t l,l_ty)
 tcRho scope c (C t1 t2) mb_ty = do
   let (c1,c2,c3,c4) = split4 c
@@ -325,33 +324,83 @@ tcRho scope c (Glue t1 t2) mb_ty = do
   (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
-  ty <- join t1_ty t2_ty
-  instSigma scope c3 (ExtR t1 t2) ty mb_ty
+tcRho scope c t@(ExtR t1 t2) mb_ty =
+  case (t2,mb_ty) of
+    (R rs,Just (VRecType ltys ext)) -> do
+       let ll2   = map fst rs
+           (c1,c2) = split c
+
+       (t1,ty1@(VRecType ltys1 ext)) <- tcRho scope c1 t1 (Just (VRecType [field | field@(l,_,_) <- ltys, not (elem l ll2)] ext))
+       let (scope',proj1,wrap) = access scope t1 ty1
+
+       lttys2 <- checkRecFields scope' c2 [] rs [field | field@(l,_,_) <- ltys, elem l ll2]
+       let proj2 l =
+             case [(Nothing,t) | (l',t,_) <- lttys2, l'==l] of
+               []    -> Nothing
+               (x:_) -> Just x
+
+       return (wrap (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]]),
+               VRecType ltys False
+              )
+    _ -> do
+       let (c1,c2,c3,c4) = split4 c
+       (t1,t1_ty) <- tcRho scope c1 t1 Nothing
+       (t2,t2_ty) <- tcRho scope c2 t2 Nothing
+       ty <- join t1_ty t2_ty
+       let (scope1,proj1,wrap1) = access scope  t1 t1_ty
+           (scope2,proj2,wrap2) = access scope1 t2 t2_ty
+       let t = case (mb_ty,ty,t2_ty) of
+                 (Just (VRecType ltys False), _, VRecType ltys2 False) ->
+                    let ll2 = [l | (l,_,_) <- ltys2]
+                    in (wrap1 . wrap2) (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]])
+                 (_, VRecType ltys False, VRecType ltys2 False) ->
+                    let ll2 = [l | (l,_,_) <- ltys2]
+                    in (wrap1 . wrap2) (R [(l,t) | (l,_,_) <- ltys, Just t <- [if elem l ll2 then proj2 l else proj1 l]])
+                 _ -> ExtR t1 t2
+       return (t,ty)
   where
+    access scope (R rs) ty = (scope
+                             ,\l -> lookup l rs
+                             ,id
+                             )
+    access scope (RecType rs) ty
+                           = (scope
+                             ,\l -> fmap ((,) Nothing) (lookup l rs)
+                             ,id
+                             )
+    access scope t@(Vr x) ty
+                           = (scope
+                             ,\l  -> return (Nothing,P t l)
+                             ,id
+                             )
+    access scope t      ty = let x = newVar scope
+                             in (((x,ty):scope)
+                                ,\l  -> return (Nothing,P (Vr x) l)
+                                ,Let (x, (Nothing, t))
+                                )
+
     join (VMeta i vs) ty2 = do
       mv <- getMeta i
       case mv of
         Bound _ v -> do
           g <- globals
           join (apply g v vs) ty2
+        _ -> evalError (pp "Cannot type check record extensions when one of the types is a meta variable")
     join ty1 (VMeta j vs) = do
       mv <- getMeta j
       case mv of
         Bound _ v -> do
           g <- globals
           join ty1 (apply g v vs)
+        _ -> evalError (pp "Cannot type check record extensions when one of the types is a meta variable")
     join (VSort s1) (VSort s2)
        | (s1 == cType || s1 == cPType) &&
          (s2 == cType || s2 == cPType) = let sort | s1 == cPType && s2 == cPType = cPType
                                                   | otherwise                    = cType
                                          in return (VSort sort)
-    join (VRecType rs1) (VRecType rs2) = do
+    join (VRecType rs1 ext1) (VRecType rs2 ext2) = do
       rs <- foldM (\rs (l,o,ctr) -> extend l o ctr rs) rs1 rs2
-      return (VRecType rs)
+      return (VRecType rs (ext1 || ext2))
       where
         extend l o1 ty1 [] = do return [(l,o1,ty1)]
         extend l o1 ty1 ((l',o2,ty2):rs)
@@ -387,16 +436,16 @@ 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 <- 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 c p ty
-  return (f (EPatt min max p), ty)
+tcRho scope c t@(EPatt _ _ p) mb_ty = do
+  (scope,f,mb_ty) <- case mb_ty of
+                       Nothing -> return (scope,id,Nothing)
+                       Just ty -> do (scope,f,ty) <- skolemise scope ty
+                                     case ty of
+                                       VPattType ty -> return (scope,f,Just ty)
+                                       _            -> evalError (ppTerm Unqualified 0 t <+> "must be of pattern type but" <+> ppTerm Unqualified 0 t <+> "is expected")
+  (_,ty) <- tcPatt scope c p mb_ty
+  (min,max,p) <- measurePatt p
+  return (f (EPatt min max p), VPattType ty)
 tcRho scope c (Markup tag attrs children) mb_ty = do
   let (c1,c2,c3,c4) = split4 c
   attrs <- mapCM (\c (id,t) -> do
@@ -406,7 +455,7 @@ tcRho scope c (Markup tag attrs children) mb_ty = do
   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 mb_ct t qid) mb_ty
-  | ctl == cConcat = do
+  | ctl == cConcat || ctl == cConcat' = do
       let (c1,c23) = split c
           (c2,c3 ) = split c23
       (t,_) <- tcRho scope c1 t Nothing
@@ -423,6 +472,21 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
                                     return (Just ct,ty)
                       Nothing -> return (Nothing,ty)
       return (Reset ctl mb_ct t qid,ty)
+  | ctl == cSelect = do
+      let (c1,c2) = split c
+      ty <- case mb_ty of
+              Just ty -> return ty
+              Nothing -> do i <- newResiduation scope
+                            return (VMeta i [])
+      let rec_ty = VRecType [ (ident2label cp1, True, ty)
+                            , (ident2label cp2, True, VSort cStr)
+                            ] False
+      mb_ct <- case mb_ct of
+                 Just ct -> do (ct,_) <- tcRho scope c2 ct (Just vtypeInt)
+                               return (Just ct)
+                 Nothing -> evalError (pp "[select: .. | ..] requires an integer argument")
+      (t,_) <- tcRho scope c1 t (Just rec_ty)
+      return (Reset ctl mb_ct t qid,ty)
   | ctl == cDefault = do
       let (c1,c2) = split c
       (t,ty)     <- tcRho scope c1 t mb_ty
@@ -441,11 +505,22 @@ tcRho scope c (Reset ctl mb_ct t qid) mb_ty
          case ty of
            VApp c qid [] -> return (Reset ctl mb_ct t (Just qid), ty)
            _             -> evalError (pp "Needs atomic type"<+>ppValue Unqualified 0 ty)
+  | ctl == cLen = do
+      do let (c1,c2) = split c
+         (t,_) <- tcRho scope c1 t Nothing
+         case mb_ct of
+           Just ct -> do res_ty <- case mb_ty of
+                                     Just ty -> return ty
+                                     Nothing -> do i <- newResiduation scope
+                                                   return (VMeta i [])
+                         (ct,_) <- tcRho scope c2 ct (Just (VProd Explicit identW vtypeInt res_ty))
+                         return (Reset ctl (Just ct) t Nothing, res_ty)
+           Nothing -> instSigma scope c2 (Reset ctl Nothing t Nothing) vtypeInt mb_ty
   | otherwise = evalError (pp "Operator" <+> pp ctl <+> pp "is not defined")
 tcRho scope s (Opts n cs) mb_ty = do
   let (s1,s2,s3) = split3 s
   (n,_) <- tcRho scope s1 n Nothing
-  (ls,_) <- tcUnifying scope s2 (fst <$> cs) Nothing
+  (ls,_)  <- tcUnifyingMaybe scope s2 (fst <$> cs) Nothing
   (ts,ty) <- tcUnifying scope s3 (snd <$> cs) mb_ty
   return (Opts n (zip ls ts), ty)
 tcRho scope s t _ = unimplemented ("tcRho "++show t)
@@ -471,13 +546,30 @@ tcUnifying scope c ts mb_ty = do
   ts <- mapCM go c ts
   return (ts,ty)
 
-tcCases scope c []         p_ty res_ty = return []
-tcCases scope c ((p,t):cs) p_ty res_ty = do
+tcUnifyingMaybe :: Scope -> Choice -> [Maybe Term] -> Maybe Rho -> EvalM ([Maybe Term], Value)
+tcUnifyingMaybe scope c ts mb_ty = do
+  (ty,subsume) <-
+    case mb_ty of
+      Just ty -> do return (ty, \t ty' -> return t)
+      Nothing -> do i <- newResiduation scope
+                    let ty = VMeta i []
+                    return (ty, \t ty' -> subsCheckRho scope t ty' ty >>= \(t,_,_) -> return t)
+
+  let go c (Just t) = do (t, ty) <- tcRho scope c t mb_ty
+                         fmap Just $ subsume t ty
+      go c Nothing  = do return Nothing
+
+  ts <- mapCM go c ts
+  return (ts,ty)
+
+tcCases scope c []         (Just p_ty) (Just res_ty) = return ([],p_ty,res_ty)
+tcCases scope c ((p,t):cs) mb_p_ty     mb_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)
+  (scope',p_ty) <- tcPatt scope c1 p mb_p_ty
+  (t,res_ty)  <- tcRho scope' c2 t mb_res_ty
+  (cs,p_ty,res_ty) <- tcCases scope c3 cs (Just p_ty) (Just res_ty)
+  (_,_,p) <- measurePatt p
+  return ((p,t):cs,p_ty,res_ty)
 
 tcApp scope c t0 (App fun arg) args mb_ty = tcApp scope c t0 fun (arg:args) mb_ty     -- APP
 tcApp scope c t0 t@(Q id)      args mb_ty = resolveOverloads scope c t0 id args mb_ty -- VAR (global)
@@ -521,9 +613,11 @@ resolveOverloads scope c t0 q args mb_ty = do
                       instSigma scope c3 t ty mb_ty
     Ok ttys     -> do let (c1,c23) = split c
                           (c2,c3)  = split c23
+                      sz <- checkpoint
                       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 c3 fun fun_ty arg_tys mb_ty)
+                      try sz
+                          (\(fun,fun_ty) -> reapply2 scope c3 fun fun_ty arg_tys mb_ty)
                           (\ttys -> fmap (\(ts,ty) -> (mkFV ts,ty)) (snd (minimum g ttys)))
                           v_ttys
   where
@@ -544,43 +638,31 @@ resolveOverloads scope c t0 q args mb_ty = do
     minimum g []                    = (maxBound,err)
       where
         err = evalError (pp "Overload resolution failed")
-    minimum g (tty@((t,ty),state):ttys) =
-      let ty'      = zonk ty
-          a        = arity ty'
+    minimum g (tty@(t,ty):ttys) =
+      let a        = arity ty
           (a',res) = minimum g ttys
       in case compare a a' of
            GT -> (a',res)
-           EQ -> (a',join t ty' state res)
-           LT -> (a ,one  t ty' state)
+           EQ -> (a',join t ty res)
+           LT -> (a ,one  t ty)
       where
         arity :: Value -> Int
         arity (VProd _ _ _ ty) = 1 + arity ty
         arity _                = 0
 
-        zonk :: Value -> Value
-        zonk (VProd bt x ty1 ty2) = VProd bt x (zonk ty1) (zonk ty2)
-        zonk (VMeta i vs)         =
-          case Map.lookup i (metaVars state) of
-            Just (Bound _ v)     -> zonk (apply g v vs)
-            _                    -> VMeta i (map zonk vs)
-        zonk (VSusp i k vs)       =
-          case Map.lookup i (metaVars state) of
-            Just (Bound _ v)     -> zonk (apply g (k v) vs)
-            _                    -> VSusp i k (map zonk vs)
-        zonk v                    = v
-
-        one t ty state = do
-          t <- withState state (zonkTerm [] t)
+        one t ty = do
           return ([t],ty)
 
-        join t ty state res = do
-          t <- withState state (zonkTerm [] t)
+        join t ty res = do
           (ts,ty') <- res
           ty <- supertype scope (Just ty) ty'
           return (t:ts,ty)
 
 reapply2 :: Scope -> Choice -> Term -> Value -> [(Term,Value,Value)] -> Maybe Rho -> EvalM (Term,Rho)
-reapply2 scope c fun fun_ty []                                mb_ty = instSigma scope c fun fun_ty mb_ty
+reapply2 scope c fun fun_ty []                                mb_ty = do
+  (fun,fun_ty) <- instSigma scope c fun fun_ty mb_ty
+  fun <- zonkTerm (scopeVars scope) fun
+  return (fun,fun_ty)
 reapply2 scope c fun fun_ty ((ImplArg arg,arg_v,arg_ty):args) mb_ty = do -- Implicit arg case
   (bt, x, arg_ty', res_ty) <- unifyFun scope fun_ty
   unless (bt == Implicit) $
@@ -596,11 +678,18 @@ reapply2 scope c fun fun_ty ((arg,arg_v,arg_ty):args) mb_ty = do -- Explicit arg
   res_ty <- evalCodomain x arg_v res_ty
   reapply2 scope c (App fun arg) res_ty args mb_ty
 
-tcPatt scope c PW        ty0 =
-  return scope
-tcPatt scope c (PV x)    ty0 =
-  return ((x,ty0):scope)
-tcPatt scope c (PP q ps) ty0 = do
+tcPatt scope c PW        Nothing    = do
+  i <- newResiduation scope
+  return (scope,VMeta i [])
+tcPatt scope c PW        (Just ty0) =
+  return (scope,ty0)
+tcPatt scope c (PV x)    Nothing    = do
+  i <- newResiduation scope
+  let ty = VMeta i []
+  return ((x,ty):scope,ty)
+tcPatt scope c (PV x)    (Just ty) =
+  return ((x,ty):scope,ty)
+tcPatt scope c (PP q ps) mb_ty = do
   g@(Gl gr _) <- globals
   ty <- case lookupResType gr q of
           Ok ty   -> return ty
@@ -608,111 +697,197 @@ tcPatt scope c (PP q ps) ty0 = do
   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
+                                (scope,arg_ty) <- tcPatt scope c1 p (Just 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 c p@(PInt i) ty0 =
-  case ty0 of
-    VInts min max
-       | i <= fromMaybe i max -> return scope
-       | otherwise            -> evalError ("Ints" <+> i <+> "is not a subtype of" <+> ppValue Unqualified 0 ty0)
-    VMeta k vs -> do
+  (scope,res_ty) <- go scope c1 (eval g [] c2 ty []) ps
+  case mb_ty of
+    Just ty -> unify scope ty res_ty
+    Nothing -> return ()
+  return (scope,res_ty)
+tcPatt scope c p@(PInt i) mb_ty =
+  case mb_ty of
+    Just ty0@(VInts n ext)
+       | i <= n    -> return (scope,ty0)
+       | ext       -> return (scope,VInts i ext)
+       | otherwise -> evalError ("Ints" <+> i <+> "is not a subtype of" <+> ppValue Unqualified 0 ty0)
+    Just ty0@(VMeta k vs) -> do
        mv <- getMeta k
        case mv of
-         Bound _ v -> do
+         Bound scope1 v -> do
            g  <- globals
-           tcPatt scope c p (apply g v vs)
+           (scope,ty) <- tcPatt scope c p (Just (apply g v vs))
+           setMeta k (Bound scope1 ty)
+           return (scope,ty0)
          Residuation scope1 -> do
-           setMeta k (Bound scope1 (VInts (Just i) Nothing))
-           return scope
+           setMeta k (Bound scope1 (VInts i True))
+           return (scope,ty0)
+    Nothing -> return (scope,VInts i True)
     _ -> evalError (pp "An integer must have an Int or Ints n type")
-tcPatt scope c (PString s) ty0 = do
-  unify scope ty0 vtypeStr
-  return scope
-tcPatt scope c PChar ty0 = do
-  unify scope ty0 vtypeStr
-  return scope
-tcPatt scope c (PChars cs) ty0 = do
-  unify scope ty0 vtypeStr
-  return scope
-tcPatt scope c (PSeq _ _ p1 _ _ p2) ty0 = do
-  unify scope ty0 vtypeStr
+tcPatt scope c (PString s) mb_ty = do
+  case mb_ty of
+    Just ty -> unify scope ty vtypeStr
+    Nothing -> return ()
+  return (scope,vtypeStr)
+tcPatt scope c PChar mb_ty = do
+  case mb_ty of
+    Just ty -> unify scope ty vtypeStr
+    Nothing -> return ()
+  return (scope,vtypeStr)
+tcPatt scope c (PChars cs) mb_ty = do
+  case mb_ty of
+    Just ty -> unify scope ty vtypeStr
+    Nothing -> return ()
+  return (scope,vtypeStr)
+tcPatt scope c (PSeq _ _ p1 _ _ p2) mb_ty = do
+  case mb_ty of
+    Just ty -> unify scope ty vtypeStr
+    Nothing -> return ()
   let (c1,c2) = split c
-  scope <- tcPatt scope c1 p1 vtypeStr
-  scope <- tcPatt scope c2 p2 vtypeStr
-  return scope
-tcPatt scope c (PRep _ _ p) ty0 = do
-  unify scope ty0 vtypeStr
-  tcPatt scope c p vtypeStr
-tcPatt scope c (PAs x p) ty0 = do
-  tcPatt ((x,ty0):scope) c p ty0
-tcPatt scope c p@(PR rs) ty0 =
-  case ty0 of
-    VRecType ltys ->
-       let go scope c []         = return scope
-           go scope c ((l,p):rs) =
-             case lookup3 l ltys of
-               Just ty -> do let (c1,c2) = split c
-                             scope <- tcPatt scope c1 p ty
-                             go scope c2 rs
-               Nothing -> do ty <- value2termM False (scopeVars scope) ty0
-                             evalError (pp "Label" <+> pp l <+> " is not defined in the type of the pattern:" $$
-                                        nest 4 (ppTerm Unqualified 0 ty))
-       in go scope c rs
-    VMeta i vs -> do
-       g  <- globals
+  (scope,_) <- tcPatt scope c1 p1 (Just vtypeStr)
+  (scope,_) <- tcPatt scope c2 p2 (Just vtypeStr)
+  return (scope,vtypeStr)
+tcPatt scope c (PRep _ _ p) mb_ty = do
+  case mb_ty of
+    Just ty -> unify scope ty vtypeStr
+    Nothing -> return ()
+  tcPatt scope c p (Just vtypeStr)
+tcPatt scope c (PAs x p) mb_ty = do
+  ty <- case mb_ty of
+          Just ty -> return ty
+          Nothing -> do i <- newResiduation scope
+                        return (VMeta i [])
+  tcPatt ((x,ty):scope) c p (Just ty)
+tcPatt scope c p@(PR rs) mb_ty =
+  case mb_ty of
+    Just (VRecType ltys ext) -> check scope c rs ltys ext
+    Just ty0@(VMeta i vs) -> do
        mv <- getMeta i
        case mv of
-         Bound _ v ->
-           tcPatt scope c p (apply g v vs)
+         Bound scope1 v ->
+              do g <- globals
+                 (scope,ty) <- tcPatt scope c p (Just (apply g v vs))
+                 setMeta i (Bound scope1 ty)
+                 return (scope,ty0)
          Residuation scope1 ->
-           let go scope c []         = return (scope,[])
-               go scope c ((l,p):rs) = do
-                 i <- newResiduation scope
-                 let ty      = VMeta i []
-                     (c1,c2) = split c
-                 scope <- tcPatt scope c1 p ty
-                 (scope,ltys) <- go scope c2 rs
-                 return (scope,(l,True,ty):ltys)
-           in do (scope,ltys) <- go scope c rs
-                 setMeta i (Bound scope1 (VRecType ltys))
-                 return scope
+              do (scope,ltys) <- infer scope c rs
+                 setMeta i (Bound scope1 (VRecType ltys True))
+                 return (scope,ty0)
+    Nothing ->do (scope,ltys) <- infer scope c rs
+                 return (scope,VRecType ltys True)
     _ -> evalError (pp "An record must have an record type")
-tcPatt scope c (PAlt p1 p2) ty0 = do
+  where
+    check scope c []         ltys ext = return (scope,VRecType ltys ext)
+    check scope c ((l,p):rs) ltys ext =
+      case lookup3 l ltys of
+        Just ty -> do let (c1,c2) = split c
+                      (scope,ty) <- tcPatt scope c1 p (Just ty)
+                      check scope c2 rs (update3 l True ty ltys) ext
+        Nothing
+          | ext -> do let (c1,c2) = split c
+                      (scope,ty) <- tcPatt scope c1 p Nothing
+                      check scope c2 rs (ltys++[(l,True,ty)]) ext
+          | otherwise
+                -> do ty <- value2termM False (scopeVars scope) (VRecType ltys ext)
+                      evalError (pp "Label" <+> pp l <+> " is not defined in the type of the pattern:" $$
+                                 nest 4 (ppTerm Unqualified 0 ty))
+
+    infer scope c []         = return (scope,[])
+    infer scope c ((l,p):rs) = do
+      let (c1,c2) = split c
+      (scope,ty) <- tcPatt scope c1 p Nothing
+      (scope,ltys) <- infer scope c2 rs
+      return (scope,(l,True,ty):ltys)
+tcPatt scope c (PNeg p) mb_ty = do
+  (_,ty) <- tcPatt scope c p mb_ty
+  return (scope, ty)
+tcPatt scope c (PAlt p1 p2) mb_ty = do
   let (c1,c2) = split c
-  tcPatt scope c1 p1 ty0
-  tcPatt scope c2 p2 ty0
-  return scope
-tcPatt scope c (PM q) ty0 = do
+  (_,ty) <- tcPatt scope c1 p1 mb_ty
+  (_,ty) <- tcPatt scope c2 p2 (Just ty)
+  return (scope,ty)
+tcPatt scope c (PM q) mb_ty = 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 unify scope ty0 (eval g [] c ty [])
-                  return scope
+         -> do let vty = eval g [] c ty []
+               case mb_ty of
+                 Just ty0 -> unify scope ty0 vty
+                 Nothing  -> return ()
+               return (scope,vty)
     ty   -> evalError ("Pattern type expected but " <+> pp ty <+> " found.")
 tcPatt scope c p ty = unimplemented ("tcPatt "++show p)
 
-inferRecFields scope c rs =
-  mapCM (\c (l,r) -> tcRecField scope c l r Nothing) c rs
+measurePatt p =
+  case p of
+    PM q       -> do g <- globals
+                     case eval g [] unit (Q q) [] of
+                       VPatt minp maxp _ -> return (minp,maxp,p)
+                       v                 -> evalError ("Expected pattern macro, but found:" $$ nest 2 (ppValue Unqualified 0 v))
+    PR ass     -> do ass <- mapM (\(lbl,p) -> measurePatt p >>= \(_,_,p') -> return (lbl,p')) ass
+                     return (0,Nothing,PR ass)
+    PString s  -> do let len=length s
+                     return (len,Just len,p)
+    PT t p     -> do (min,max,p') <- measurePatt p
+                     return (min,max,PT t p')
+    PAs x p    -> do (min,max,p) <- measurePatt p
+                     case p of
+                       PW -> return (0,Nothing,PV x)
+                       _  -> return (min,max,PAs x p)
+    PImplArg p -> do (min,max,p') <- measurePatt p
+                     return (min,max,PImplArg p')
+    PNeg p     -> do (_,_,p') <- measurePatt p
+                     return (0,Nothing,PNeg p')
+    PAlt p1 p2 -> do (min1,max1,p1) <- measurePatt p1
+                     (min2,max2,p2) <- measurePatt p2
+                     case (p1,p2) of
+                       (PString [c1],PString [c2]) -> return (1,Just 1,PChars [c1,c2])
+                       (PString [c], PChars cs)    -> return (1,Just 1,PChars ([c]++cs))
+                       (PChars cs,   PString [c])  -> return (1,Just 1,PChars (cs++[c]))
+                       (PChars cs1,  PChars cs2)   -> return (1,Just 1,PChars (cs1++cs2))
+                       _                           -> return (min min1 min2,liftM2 max max1 max2,PAlt p1 p2)
+    PSeq _ _ p1 _ _ p2
+               -> do (min1,max1,p1) <- measurePatt p1
+                     (min2,max2,p2) <- measurePatt p2
+                     case (p1,p2) of
+                       (PW,        PW        ) -> return (0,Nothing,PW)
+                       (PString s1,PString s2) -> return (min1+min2,liftM2 (+) max1 max2,PString (s1++s2))
+                       _                       -> return (min1+min2,liftM2 (+) max1 max2,PSeq min1 max1 p1 min2 max2 p2)
+    PRep _ _ p -> do (minp,maxp,p) <- measurePatt p
+                     case p of
+                       PW    -> return (0,Nothing,PW)
+                       PChar -> return (0,Nothing,PW)
+                       _     -> return (0,Nothing,PRep minp maxp p)
+    PChar      -> return (1,Just 1,p)
+    PChars _   -> return (1,Just 1,p)
+    _          -> return (0,Nothing,p)
 
-checkRecFields scope c []          ltys
+inferRecFields scope c ls []          = return []
+inferRecFields scope c ls ((l,t):lts)
+  | elem l ls = evalError ("Repeated definition for field" <+> l)
+  | otherwise = do
+      let (c1,c2) = split c
+      lt  <- tcRecField scope c1 l t Nothing
+      lts <- inferRecFields scope c2 (l:ls) lts
+      return (lt:lts)
+
+checkRecFields scope c ls []          ltys
   | null ltys                            = return []
   | otherwise                            = evalError ("Missing fields:" <+> hsep [l | (l,_,_) <- ltys])
-checkRecFields scope c ((l,t):lts) ltys =
-  case takeIt l ltys of
-    (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)
-                         lttys <- checkRecFields scope c lts ltys
-                         return lttys     -- ignore the field
+checkRecFields scope c ls ((l,t):lts) ltys
+  | elem l ls = evalError ("Repeated definition for field" <+> l)
+  | otherwise =
+      case takeIt l ltys of
+        (Just ty,ltys) -> do let (c1,c2) = split c
+                             ltty  <- tcRecField scope c1 l t (Just ty)
+                             lttys <- checkRecFields scope c2 ls lts ltys
+                             return (ltty : lttys)
+        (Nothing,ltys) -> do evalWarn ("Discarded field:" <+> l)
+                             lttys <- checkRecFields scope c ls lts ltys
+                             return lttys     -- ignore the field
   where
     takeIt l1 []  = (Nothing, [])
     takeIt l1 (lty@(l2,_,ty):ltys)
@@ -731,20 +906,22 @@ tcRecField scope c l (mb_ann_ty,t) mb_ty = do
               Nothing     -> tcRho scope c t mb_ty
   return (l,t,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 <- 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 c2 rs mb_ty
-  return ((l,ty):rs,mb_ty)
+tcRecTypeFields scope c ls []          mb_ty = return ([],mb_ty)
+tcRecTypeFields scope c ls ((l,ty):rs) mb_ty
+  | elem l ls = evalError ("Repeated definition for field" <+> l)
+  | otherwise = 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 <- 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 c2 (l:ls) rs mb_ty
+      return ((l,ty):rs,mb_ty)
 
 -- | Invariant: if the third argument is (Just rho),
 --              then rho is in weak-prenex form
@@ -839,26 +1016,12 @@ subsCheckRho scope t ty1@(VApp _ p _) ty2@(VInts _ _)         -- This is not cor
   | p == (cPredef,cInt) = return (t,ty1,ty2)                  -- Should be only a temporary hack.
 subsCheckRho scope t ty1@(VInts _ _) ty2@(VApp _ p _)         -- Rule INT1
   | p == (cPredef,cInt) = return (t,ty1,ty2)
-subsCheckRho scope t ty1@(VInts i1 j1) ty2@(VInts i2 j2)      -- Rule INT2
-  | j1  `less1` i2  = return (t,ty1,ty2)
-  | j1' `less1` i2' = return (t,VInts i1 j1',VInts i2' j2)
-  | otherwise       = evalError ("In the term" <+> ppTerm Unqualified 0 t $$
-                                 ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2)
-  where
-    less1 (Just x) (Just y) = x <= y
-    less1 _        _        = False
-
-    less2 (Just x) (Just y) = x <= y
-    less2 Nothing  (Just y) = True
-    less2 _        _        = False
-
-    less3 (Just x) (Just y) = x <= y
-    less3 (Just x) Nothing  = True
-    less3 _        _        = False
-
-    j1' = if i1 `less2` i2 then i2 else j1
-    i2' = if j1 `less3` j2 then j1 else i2
-subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
+subsCheckRho scope t ty1@(VInts n1 ext1) ty2@(VInts n2 ext2)  -- Rule INT2
+  | n1 <= n2  = return (t,ty1,ty2)
+  | ext2      = return (t,ty1,VInts n1 ext2)
+  | otherwise = evalError ("In the term" <+> ppTerm Unqualified 0 t $$
+                           ppValue Terse 0 ty1 <+> "is not a subtype of" <+> ppValue Terse 0 ty2)
+subsCheckRho scope t ty1@(VRecType rs1 ext1) ty2@(VRecType rs2 ext2) = do      -- Rule REC
   let mkAccess scope t =
         case t of
           ExtR t1 (R rs) ->
@@ -873,80 +1036,115 @@ subsCheckRho scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do      -- Rule REC
                             ,\l -> lookup l rs
                             ,id
                             )
+          Vr x  -> return (scope
+                          ,\l  -> return (Nothing,P t l)
+                          ,\t' -> if is_trivial x t' then t else t'
+                          )
           t    -> let x = newVar scope
                   in return (((x,ty1):scope)
                             ,\l  -> return (Nothing,P (Vr x) l)
-                            ,Let (x, (Nothing, t))
+                            ,\t' -> if is_trivial x t' then t else Let (x, (Nothing, t)) t'
                             )
 
-      mkField scope l (mb_ty,t) ty1 ty2 = do
-        (t,_,_) <- subsCheckRho scope t ty1 ty2
-        return (l, (mb_ty,t))
+      is_trivial x (R rs) = all is_selection rs
+        where
+          is_selection (l, (_, P (Vr u) l'))
+            | l == l' && u == x = True
+          is_selection _        = False
+      is_trivial x _      = False
 
-  (scope,mkProj,mkWrap) <- mkAccess scope t
+      mkField scope l (mb_ty,t) (Just ty1) ty2 = do
+        (t,ty1,ty2) <- subsCheckRho scope t ty1 ty2
+        return ((l, (mb_ty,t)), (l, True, ty1))
+      mkField scope l (mb_ty,t) Nothing    ty2
+        | isLockLabel l = return ((l, (Just (RecType []),R [])), (l, True, ty2))
+        | otherwise     = return ((l, (mb_ty,t)), (l, True, ty2))
 
-  let fields = [(l,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2]
-  case [l | (l,_,Nothing) <- fields, not (isLockLabel l)] of
+  (scope,mkProj,wrap) <- mkAccess scope t
+
+  let fields = [(l,o2,ty2,lookup3 l rs1) | (l,o2,ty2) <- rs2]
+  case [l | (l,_,_,Nothing) <- fields, not ext1 && not (isLockLabel l)] of
     []      -> return ()
     missing -> evalError ("In the term" <+> pp t $$
                           "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++[(l, (Just (RecType []),R [])) | (l,_,Nothing) <- fields, isLockLabel l])),ty1,ty2)
+  rs <- sequence [mkField scope l t mb_ty1 ty2 | (l,_,ty2,mb_ty1) <- fields, Just t <- [mkProj l]]
+  return (wrap (R (map fst rs)),VRecType (foldl (\rs (_,(l,o,ty)) -> update3 l o ty rs) rs1 rs) ext2,ty2)
 subsCheckRho scope t ty1 (VFV c (VarFree vs)) = do
   ty2 <- variants c vs
   subsCheckRho scope t ty1 ty2
 subsCheckRho scope t (VFV c (VarFree vs)) ty2 = do
   ty1 <- variants c vs
   subsCheckRho scope t ty1 ty2
+subsCheckRho scope t ty1@(VPattType (VSort s1)) ty2@(VSort s2)      -- for backwards compatibility
+  | s1 == cStr && s2 == cStrs = return (t,ty1,ty2)
 subsCheckRho scope t ty1 ty2 = do                           -- Rule EQ
   unify scope ty1 ty2                                  -- Revert to ordinary unification
   return (t,ty1,ty2)
 
 subsCheckFun :: Scope -> Term -> Sigma -> Value -> Sigma -> Value -> EvalM (Term,Value,Value)
 subsCheckFun scope t a1 r1 a2 r2 = do
-  let v   = newVar scope
-  (vt,a2,a1) <- subsCheckRho ((v,a2):scope) (Vr v) a2 a1
+  let x = newVar scope
+  (xt,a2,a1) <- subsCheckRho ((x,a2):scope) (Vr x) a2 a1
   g  <- globals
-  let (v1',r1') = case r1 of
-                    VClosure env c r1 -> (v,eval g ((v,(VGen (length scope) [])):env) c r1 [])
+  let (x1',r1') = case r1 of
+                    VClosure env c r1 -> (x,eval g ((x,(VGen (length scope) [])):env) c r1 [])
                     r1                -> (identW,r1)
-      (v2',r2') = case r2 of
-                    VClosure env c r2 -> (v,eval g ((v,(VGen (length scope) [])):env) c r2 [])
+      (x2',r2') = case r2 of
+                    VClosure env c r2 -> (x,eval g ((x,(VGen (length scope) [])):env) c r2 [])
                     r2                -> (identW,r2)
-  (t,r1,r2)  <- subsCheckRho ((v,vtypeType):scope) (App t vt) r1' r2'
-  return (Abs Explicit v t, VProd Explicit v1' a1 r1, VProd Explicit v2' a2 r2)
+  (t,r1,r2)  <- subsCheckRho ((x,a2):scope) (App t xt) r1' r2'
+  case t of
+    App t (Vr u) | u == x -> return (t, VProd Explicit x1' a1 r1, VProd Explicit x2' a2 r2)
+    _                     -> return (Abs Explicit x t, VProd Explicit x1' a1 r1, VProd Explicit x2' a2 r2)
 
 subsCheckTbl :: Scope -> Term -> Sigma -> Rho -> Sigma -> Rho  -> EvalM (Term,Value,Value)
 subsCheckTbl scope t p1 r1 p2 r2 = do
-  let x = newVar scope
-  (xt,p2,p1) <- subsCheckRho ((x,p2):scope) (Vr x) p2 p1
-  (t,r1,r2)  <- subsCheckRho ((x,p2):scope) (S t xt) r1 r2
+  (scope,y,sel,wrap) <-
+        case t of
+          Vr x -> let y = newVar scope
+                  in return ((y,p2):scope
+                            ,y
+                            ,\t -> S (Vr x) t
+                            ,\p2 t' -> case t' of
+                                         S (Vr u) (Vr v) | u == x && v == y -> t
+                                         _                                  -> T (TTyped p2) [(PV y,t')]
+                            )
+          T _ [(PV x,t')] ->
+                  let scope' = (x,p1):scope
+                      y      = newVar scope'
+                  in return (((y,p2):scope')
+                            ,y
+                            ,\t  -> Let (x, (Nothing, t)) t'
+                            ,\p2 t -> case t of
+                                        Let (u, (Nothing, Vr v)) t | u == x && v == y -> T (TTyped p2) [(PV x,t)]
+                                        _                                             -> T (TTyped p2) [(PV y,t)]
+                            )
+          t    -> let x = newVar scope
+                      scope' = (x,VTable p1 r1):scope
+                      y = newVar scope'
+                  in return (((y,VTable p1 r1):scope')
+                            ,y
+                            ,\t  -> S (Vr x) t
+                            ,\p2 t' -> case t' of
+                                         S (Vr u) (Vr v) | u == x && v == y -> t
+                                         _                                  -> Let (x, (Nothing, t)) (T (TTyped p2) [(PV y,t')])
+                            )
+  (yt,p2,p1) <- subsCheckRho scope (Vr y) p2 p1
+  (t,r1,r2)  <- subsCheckRho scope (sel yt) r1 r2
   p2_t <- value2termM True (scopeVars scope) p2
-  return (T (TTyped p2_t) [(PV x,t)],VTable p1 r1,VTable p2 r2)
+  return (wrap p2_t t,VTable p1 r1,VTable p2 r2)
 
-{-subtype scope Nothing              (VInts i2 j2) =
-  return (VInts Nothing j2)
-subtype scope (Just (VMeta i vs))  ty2 = do
-  g  <- globals
-  mv <- getMeta i
-  case mv of
-    Bound _ v -> subtype scope (Just (apply g v vs)) ty2-}
-subtype scope (Just (VInts i1 j1)) (VInts i2 j2) =
-  case VInts (lift max i1 i2) (lift min j1 j2) of
-    ty@(VInts (Just i) (Just j))
-      | i > j -> evalError (ppValue Unqualified 0 ty <+> "is an empty type")
-    ty        -> return ty
-  where
-    lift f Nothing  Nothing  = Nothing
-    lift f (Just x) Nothing  = Just x
-    lift f Nothing  (Just y) = Just y
-    lift f (Just x) (Just y) = Just (f x y)
-subtype scope Nothing (VRecType ltys) = do
+
+subtype scope Nothing              (VInts i2 _) =
+  return (VInts i2 True)
+subtype scope (Just (VInts n1 _))  (VInts n2 _) =
+  return (VInts (min n1 n2) False)
+subtype scope Nothing (VRecType ltys ext) = do
   lctrs <- mapM (\(l,o,ty) -> subtype scope Nothing ty >>= \ctr -> return (l,o,ctr)) ltys
-  return (VRecType lctrs)
-subtype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do
+  return (VRecType lctrs ext)
+subtype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do
   lctrs <- foldM (\lctrs (l,o,ctr) -> union l o ctr lctrs) lctrs1 lctrs2
-  return (VRecType lctrs)
+  return (VRecType lctrs (ext1 || ext2))
   where
     union l o1 ctr1 [] = do ctr <- subtype scope Nothing ctr1
                             return [(l,True,ctr)]
@@ -973,24 +1171,16 @@ subtype scope (Just ctr) ty = do
   unify scope ctr ty
   return ty
 
-supertype scope Nothing (VInts i2 j2) =
-  return (VInts i2 Nothing)
-supertype scope (Just (VInts i1 j1)) (VInts i2 j2) =
-  case VInts (lift min i1 i2) (lift max j1 j2) of
-    ty@(VInts (Just i) (Just j))
-      | i > j -> evalError (ppValue Unqualified 0 ty <+> "is an empty type")
-    ty        -> return ty
-  where
-    lift f Nothing  Nothing  = Nothing
-    lift f (Just x) Nothing  = Nothing
-    lift f Nothing  (Just y) = Nothing
-    lift f (Just x) (Just y) = Just (f x y)
-supertype scope Nothing (VRecType ltys) = do
+supertype scope Nothing (VInts n2 _) =
+  return (VInts n2 True)
+supertype scope (Just (VInts n1 _)) (VInts n2 _) =
+  return (VInts (max n1 n2) True)
+supertype scope Nothing (VRecType ltys ext) = do
   lctrs <- mapM (\(l,o,ty) -> supertype scope Nothing ty >>= \ctr -> return (l,False,ctr)) ltys
-  return (VRecType lctrs)
-supertype scope (Just (VRecType lctrs1)) (VRecType lctrs2) = do
+  return (VRecType lctrs ext)
+supertype scope (Just (VRecType lctrs1 ext1)) (VRecType lctrs2 ext2) = do
   lctrs <- foldM (\lctrs (l,o,ctr) -> intersect l o ctr lctrs lctrs2) [] lctrs1
-  return (VRecType lctrs)
+  return (VRecType lctrs (ext1 || ext2))
   where
     intersect l o1 ctr1 lctrs [] = return lctrs
     intersect l o1 ctr1 lctrs ((l',o2,ctr2):lctrs2)
@@ -1092,9 +1282,7 @@ unify scope (VFlt x)  (VFlt y)
 unify scope (VStr s1) (VStr s2)
   | s1 == s2                   = return ()
 unify scope VEmpty VEmpty      = return ()
-unify scope v1 v2 = do
-  t1 <- value2termM False (scopeVars scope) v1
-  t2 <- value2termM False (scopeVars scope) v2
+unify scope v1 v2 =
   evalError ("Cannot unify:" <+> ppValue Qualified 0 v1 $$
              "        with:" <+> ppValue Qualified 0 v2)
 
@@ -1139,7 +1327,7 @@ occursCheck scope' i0 scope v =
         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) =
+    check m n (VRecType as _) =
       mapM_ (\(_,_,v) -> check m n v) as
     check m n (VR as) =
       mapM_ (\(lbl,v) -> check m n v) as
@@ -1246,9 +1434,9 @@ quantify scope t tvs ty = do
                                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
+    check m n xs (VRecType as ext)     = do
       (xs,as) <- mapAccumM (\xs (l,o,v) -> check m n xs v >>= \(xs,v) -> return (xs,(l,o,v))) xs as
-      return (xs,VRecType as)
+      return (xs,VRecType as ext)
     check m n xs (VR as)           = do
       (xs,as) <- mapAccumM (\xs (lbl,tnk) -> check m n xs tnk >>= \(xs,tnk) -> return (xs,(lbl,tnk))) xs as
       return (xs,VR as)
@@ -1339,6 +1527,11 @@ lookup3 l ((l',_,v):rs)
   | l == l'   = Just v
   | otherwise = lookup3 l rs
 
+update3 l o v []  = [(l,o,v)]
+update3 l o v (r@(l',_,_):rs)
+  | l == l'   = (l,o,v) : rs
+  | otherwise = r : update3 l o v rs
+
 newVar :: Scope -> Ident
 newVar scope = head [x | i <- [1..],
                          let x = identS ('v':show i),
@@ -1360,7 +1553,7 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
     go acc (VGen i args)     = foldM go acc args
     go acc (VSort s)         = return acc
     go acc (VInt _)          = return acc
-    go acc (VRecType vs)    = foldM (\acc (lbl,_,v) -> go acc v) acc vs
+    go acc (VRecType vs _)   = foldM (\acc (lbl,_,v) -> go acc v) acc vs
     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
@@ -1372,7 +1565,8 @@ getMetaVars sc_tys = foldM (\acc (scope,ty) -> go acc ty) [] sc_tys
                                     _         -> foldM go (m:acc) args
     go acc (VApp c f args)   = foldM go acc args
     go acc (VFV c vs)        = foldM go acc (unvariants vs)
-    go acc (VInts _ _)      = return acc
+    go acc (VInts _ _)       = return acc
+    go acc (VPattType v)     = go acc v
     go acc v                 = unimplemented ("go "++show (ppValue Unqualified 5 v))
 
 -- | Eliminate any substitutions in a term
@@ -1393,3 +1587,24 @@ zonkTerm xs (Meta i) = do
     Bound _ v -> zonkTerm xs =<< value2termM False xs v
     _         -> return (Meta i)
 zonkTerm xs t = composOp (zonkTerm xs) t
+
+zonkValue :: Value -> EvalM Value
+zonkValue (VProd bt x ty1 ty2) = do
+  ty1 <- zonkValue ty1
+  ty2 <- zonkValue ty2
+  return (VProd bt x ty1 ty2)
+zonkValue (VMeta i vs)         = do
+  g  <- globals
+  st <- getMeta i
+  case st of
+    Bound _ v              -> zonkValue (apply g v vs)
+    _                      -> do vs <- mapM zonkValue vs
+                                 return (VMeta i vs)
+zonkValue (VSusp i k vs)       = do
+  g  <- globals
+  st <- getMeta i
+  case st of
+    Bound _ v              -> zonkValue (apply g (k v) vs)
+    _                      -> do vs <- mapM zonkValue vs
+                                 return (VSusp i k vs)
+zonkValue v                    = return v
diff --git a/src/compiler/api/GF/Grammar/Grammar.hs b/src/compiler/api/GF/Grammar/Grammar.hs
index c2ad8660a..74433c076 100644
--- a/src/compiler/api/GF/Grammar/Grammar.hs
+++ b/src/compiler/api/GF/Grammar/Grammar.hs
@@ -466,7 +466,7 @@ type Equation = ([Patt],Term)
 
 type Labelling = (Label, Type) 
 type Assign = (Label, (Maybe Type, Term)) 
-type Option = (Term, Term)
+type Option = (Maybe Term, Term)
 type Case = (Patt, Term) 
 --type Cases = ([Patt], Term) 
 type LocalDef = (Ident, (Maybe Type, Term))
diff --git a/src/compiler/api/GF/Grammar/Macros.hs b/src/compiler/api/GF/Grammar/Macros.hs
index 92de22594..4c24b9b0e 100644
--- a/src/compiler/api/GF/Grammar/Macros.hs
+++ b/src/compiler/api/GF/Grammar/Macros.hs
@@ -404,6 +404,7 @@ composOp co trm =
    RecType r        -> liftM RecType (mapPairsM co r)
    P t i            -> liftM2 P (co t) (return i)
    ExtR a c         -> liftM2 ExtR (co a) (co c)
+   Opts t os        -> liftM2 Opts (co t) (mapM (\(t1,t2) -> liftM2 (,) (maybe (return Nothing) (liftM Just . co) t1) (co t2)) os)
    T i cc           -> liftM2 (flip T) (mapPairsM co cc) (changeTableType co i)
    V ty vs          -> liftM2 V (co ty) (mapM co vs)
    Let (x,(mt,a)) b -> liftM3 let' (co a) (T.mapM co mt) (co b)
@@ -450,7 +451,7 @@ collectOp co trm = case trm of
   S c a        -> co c <> co a
   Table a c    -> co a <> co c
   ExtR a c     -> co a <> co c
-  Opts t os    -> co t <> mconcatMap (\(a,b) -> co a <> co b) os
+  Opts t os    -> co t <> mconcatMap (\(a,b) -> maybe mempty co a <> co b) os
   R r          -> mconcatMap (\ (_,(mt,a)) -> maybe mempty co mt <> co a) r
   RecType r    -> mconcatMap (co . snd) r
   P t i        -> co t
diff --git a/src/compiler/api/GF/Grammar/Parser.y b/src/compiler/api/GF/Grammar/Parser.y
index 9167e5c1c..a6e04dd3a 100644
--- a/src/compiler/api/GF/Grammar/Parser.y
+++ b/src/compiler/api/GF/Grammar/Parser.y
@@ -275,10 +275,10 @@ ParamDef
 
 OperDef :: { [(Ident,Info)] }
 OperDef
-  : Posn LhsNames ':' Exp ';'        Posn { [(i, info) | i <- $2,   info <- mkOverload (Just (mkL $1 $6 $4)) Nothing  ] }
-  | Posn LhsNames '=' Markup         Posn { [(i, info) | i <- $2,   info <- mkOverload Nothing   (Just (mkL $1 $5 $4))] }
-  | Posn LhsName ListArg '=' Markup  Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing   (Just (mkL $1 $6 (mkAbs $3 $5)))] }
-  | Posn LhsNames ':' Exp '=' Markup Posn { [(i, info) | i <- $2,   info <- mkOverload (Just (mkL $1 $7 $4)) (Just (mkL $1 $7 $6))] }
+  : Posn LhsNames ':' Exp ';'         Posn { [(i, info) | i <- $2,   info <- mkOverload (Just (mkL $1 $6 $4)) Nothing  ] }
+  | Posn LhsNames '=' Exp ';'         Posn { [(i, info) | i <- $2,   info <- mkOverload Nothing   (Just (mkL $1 $6 $4))] }
+  | Posn LhsName ListArg '=' Exp ';'  Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing   (Just (mkL $1 $7 (mkAbs $3 $5)))] }
+  | Posn LhsNames ':' Exp '=' Exp ';' Posn { [(i, info) | i <- $2,   info <- mkOverload (Just (mkL $1 $8 $4)) (Just (mkL $1 $8 $6))] }
 
 LinDef :: { [(Ident,Info)] }
 LinDef
@@ -452,7 +452,11 @@ Exp4 :: { Term }
 Exp4
   : Exp4 Exp5                        { App $1 $2 }
   | Exp4 '{' Exp '}'                 { App $1 (ImplArg $3) } 
-  | 'option' Exp 'of' '{' ListOpt '}' { Opts $2 $5 }
+  | 'option' Exp 'of' '{' ListExp '}' { let toOption t =
+                                              case t of
+                                                Table x y -> (Just x,  y)
+                                                y         -> (Nothing, y)
+                                        in Opts $2 (map toOption $5) }
   | 'case' Exp 'of' '{' ListCase '}' { let annot = case $2 of
                                              Typed _ t -> TTyped t
                                              _         -> TRaw
@@ -487,8 +491,7 @@ Exp6
   | '{' ListLocDef '}'    {% mkR $2 }
   | '<' ListTupleComp '>' { R (tuple2record $2) }
   | '<' Exp ':' Exp '>'   { Typed $2 $4      }
-  | '[' Control '|' Tag ']'      { Reset (fst $2) (snd $2) $4 Nothing }
-  | '[' Control '|' Exp ']'      { Reset (fst $2) (snd $2) $4 Nothing }
+  | '[' Control '|' ListMarkup ']'      { Reset (fst $2) (snd $2) (mkMarkup $4) Nothing }
   | '(' Exp ')'           { $2 }
 
 ListExp :: { [Term] }
@@ -609,15 +612,6 @@ ListPattTupleComp
   | Patt                       { [$1]    }
   | Patt ',' ListPattTupleComp { $1 : $3 }
 
-Opt :: { Option }
-Opt
-  : '(' Exp ')' '=>' Exp { ($2,$5) }
-
-ListOpt :: { [Option] }
-ListOpt
-  : Opt             { [$1]    }
-  | Opt ';' ListOpt { $1 : $3 }
-
 Case :: { Case }
 Case
   : Patt '=>' Exp { ($1,$3) } 
@@ -720,14 +714,21 @@ ERHS3 :: { ERHS }
   | '(' ERHS0 ')'         { $2         }
 
 NLG :: { Map.Map Ident Info }
-  : ListNLGDef     { Map.fromList $1 }
-  | 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             { Map.fromList $1 }
+  | Posn Exp         Posn  { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 $2))) }
+  | Posn ListMarkup2 Posn  { Map.singleton (identS "main") (ResOper Nothing (Just (mkL $1 $3 (mkMarkup $2)))) }
 
 ListNLGDef :: { [(Ident,Info)] }
 ListNLGDef
-  : {- empty -}               { []       }
-  | 'oper' OperDef ListNLGDef { $2 ++ $3 }
+  : 'oper' NLGDef            { []       }
+  | 'oper' NLGDef ListNLGDef { $2 ++ $3 }
+
+NLGDef :: { [(Ident,Info)] }
+NLGDef
+  : Posn LhsNames ':' Exp ';'             Posn { [(i, info) | i <- $2,   info <- mkOverload (Just (mkL $1 $6 $4)) Nothing  ] }
+  | Posn LhsNames '=' ListMarkup2         Posn { [(i, info) | i <- $2,   info <- mkOverload Nothing   (Just (mkL $1 $5 (mkMarkup $4)))] }
+  | Posn LhsName ListArg '=' ListMarkup2  Posn { [(i, info) | i <- [$2], info <- mkOverload Nothing   (Just (mkL $1 $6 (mkAbs $3 (mkMarkup $5))))] }
+  | Posn LhsNames ':' Exp '=' ListMarkup2 Posn { [(i, info) | i <- $2,   info <- mkOverload (Just (mkL $1 $7 $4)) (Just (mkL $1 $7 (mkMarkup $6)))] }
 
 Markup :: { Term }
 Markup
@@ -746,6 +747,10 @@ ListMarkup :: { [Term] }
   | Exp                { [$1]    }
   | Markup ListMarkup  { $1 : $2 }
 
+ListMarkup2 :: { [Term] }
+  : Markup              { [$1]    }
+  | Markup ListMarkup2  { $1 : $2 }
+
 Control :: { (Ident,Maybe Term) }
   : Ident            { ($1, Nothing) }
   | Ident ':' Exp6   { ($1, Just $3) }
@@ -884,4 +889,7 @@ mkAlts cs = case cs of
 mkL :: Posn -> Posn -> x -> L x
 mkL (Pn l1 _) (Pn l2 _) x = L (Local l1 l2) x
 
+mkMarkup [t] = t
+mkMarkup ts  = Markup identW [] ts
+
 }
diff --git a/src/compiler/api/GF/Grammar/Predef.hs b/src/compiler/api/GF/Grammar/Predef.hs
index 4313042fa..f807d762a 100644
--- a/src/compiler/api/GF/Grammar/Predef.hs
+++ b/src/compiler/api/GF/Grammar/Predef.hs
@@ -63,9 +63,15 @@ cError = identS "error"
 
 -- * Used in the delimited continuations
 cConcat = identS "concat"
+cConcat' = identS "concat'"
 cOne = identS "one"
+cSelect = identS "select"
 cDefault = identS "default"
 cList = identS "list"
+cLen = identS "len"
+
+cp1 = identS "p1"
+cp2 = identS "p2"
 
 -- * Hacks: dummy identifiers used in various places.
 -- Not very nice!
diff --git a/src/compiler/api/GF/Grammar/Printer.hs b/src/compiler/api/GF/Grammar/Printer.hs
index e9947b494..ef6bc9eec 100644
--- a/src/compiler/api/GF/Grammar/Printer.hs
+++ b/src/compiler/api/GF/Grammar/Printer.hs
@@ -218,6 +218,9 @@ ppTerm q d (S x y)     = case x of
                                            '}'
                            _          -> prec d 3 (hang (ppTerm q 3 x) 2 ("!" <+> ppTerm q 4 y))
 ppTerm q d (ExtR x y)  = prec d 3 (ppTerm q 3 x <+> "**" <+> ppTerm q 4 y)
+ppTerm q d (Opts t opts) = "option" <+> ppTerm q 0 t <+>"of" <+> '{' $$
+                              nest 2 (vcat (punctuate ';' (map (ppOpt q) opts))) $$
+                           '}'
 ppTerm q d (App x y)   = prec d 4 (ppTerm q 4 x <+> ppTerm q 5 y)
 ppTerm q d (V e es)    = hang "table" 2 (sep [ppTerm q 6 e,brackets (fsep (punctuate ';' (map (ppTerm q 0) es)))])
 ppTerm q d (FV es)     = prec d 4 ("variants" <+> braces (fsep (punctuate ';' (map (ppTerm q 0) es))))
@@ -269,6 +272,9 @@ ppEquation q (ps,e) = hcat (map (ppPatt q 2) ps) <+> "->" <+> ppTerm q 0 e
 
 ppCase q (p,e) = ppPatt q 0 p <+> "=>" <+> ppTerm q 0 e
 
+ppOpt q (Just p, e) = ppTerm q 0 p <+> "=>" <+> ppTerm q 0 e
+ppOpt q (Nothing,e) = ppTerm q 0 e
+
 ppControl q (id,Nothing) = pp id
 ppControl q (id,Just t ) = pp id <> ':' <+> ppTerm q 6 t