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 4cafea9b4..0182c93ff 100644
--- a/src/compiler/api/GF/Compile/Compute/Concrete2.hs
+++ b/src/compiler/api/GF/Compile/Compute/Concrete2.hs
@@ -65,7 +65,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,7 +89,7 @@ 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]
@@ -106,7 +106,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
@@ -200,7 +200,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 +214,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) []
@@ -348,7 +348,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 +392,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
@@ -830,7 +830,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
@@ -974,9 +974,7 @@ value2termM flat xs (VReset ctl mb_cv v mb_qid) = do
     listify mn cat (t1:ts) = do t2 <- listify mn cat ts
                                 return (App (App (QC (mn,identS ("Cons"++cat))) t1) t2)
 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)
 
 
@@ -1001,13 +999,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"
@@ -1027,17 +1025,16 @@ 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 (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
 
diff --git a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
index a48a954ae..954c31452 100644
--- a/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
+++ b/src/compiler/api/GF/Compile/TypeCheck/Concrete.hs
@@ -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,12 +324,21 @@ 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 (mb_ty,t2) of
+    (Just (VRecType ltys ext),R ss) -> do
+       let ll2 = map fst ss
+           (c1,c2) = split c
+       (t1,t1_ty) <- tcRho scope c1 t1 (Just (VRecType [field | field@(l,_,_) <- ltys, not (elem l ll2)] ext))
+       (t2,t2_ty) <- tcRho scope c2 t2 (Just (VRecType [field | field@(l,_,_) <- ltys, elem l ll2] ext))
+       ty <- join t1_ty t2_ty
+       return (ExtR t1 t2, 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
   where
     join (VMeta i vs) ty2 = do
       mv <- getMeta i
@@ -349,9 +357,9 @@ tcRho scope c t@(ExtR t1 t2) mb_ty = do
          (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)
@@ -388,15 +396,14 @@ tcRho scope c (EPattType ty) mb_ty = do
   (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)
+  (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
+  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
@@ -471,13 +478,13 @@ 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
+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)
+  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)
@@ -581,11 +588,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
@@ -593,111 +607,153 @@ 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
+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 []          ltys
+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)
@@ -716,20 +772,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
@@ -824,26 +882,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) ->
@@ -883,6 +927,8 @@ subsCheckRho scope t ty1 (VFV c (VarFree vs)) = do
 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)
@@ -909,29 +955,16 @@ subsCheckTbl scope t p1 r1 p2 r2 = do
   p2_t <- value2termM True (scopeVars scope) p2
   return (T (TTyped p2_t) [(PV x,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)]
@@ -958,24 +991,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)
@@ -1077,9 +1102,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)
 
@@ -1124,7 +1147,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
@@ -1231,9 +1254,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)
@@ -1324,6 +1347,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),
@@ -1345,7 +1373,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
@@ -1357,7 +1385,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