more progress on the typechecker

2 files changed, 228 insertions, 219 deletions

diff --git a/src/compiler/GF/Compile/Compute/ConcreteNew.hs b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
index f7551f373..d6754c905 100644
--- a/src/compiler/GF/Compile/Compute/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/Compute/ConcreteNew.hs
@@ -15,7 +15,7 @@ import GF.Compile.Compute.Value hiding (Error)
 import GF.Compile.Compute.Predef(predef,predefName,delta)
 import GF.Data.Str(Str,glueStr,str2strings,str,sstr,plusStr,strTok)
 import GF.Data.Operations(Err,err,errIn,maybeErr,combinations,mapPairsM)
-import GF.Data.Utilities(mapFst,mapSnd,mapBoth)
+import GF.Data.Utilities(mapFst,mapSnd)
 import GF.Infra.Option
 import Control.Monad(ap,liftM,liftM2) -- ,unless,mplus
 import Data.List (findIndex,intersect,nub,elemIndex,(\\)) --,isInfixOf
@@ -29,7 +29,11 @@ import Debug.Trace(trace)
 normalForm :: GlobalEnv -> L Ident -> Term -> Term
 normalForm (GE gr rv opts _) loc = err (bugloc loc) id . nfx (GE gr rv opts loc)
 
-nfx env@(GE _ _ _ loc) t = value2term loc [] # eval env [] t
+nfx env@(GE _ _ _ loc) t = do
+  v <- eval env [] t
+  case value2term loc [] v of
+    Left i  -> fail ("variable #"++show i++" is out of scope")
+    Right t -> return t
 
 eval :: GlobalEnv -> Env -> Term -> Err Value
 eval (GE gr rvs opts loc) env t = ($ (map snd env)) # value cenv t
@@ -132,7 +136,7 @@ value env t0 =
 {-
   trace (render $ text "value"<+>sep [ppL (gloc env)<>text ":",
                                       brackets (fsep (map ppIdent (local env))),
-                                      ppT 10 t0]) $
+                                      ppTerm Unqualified 10 t0]) $
 --}
   errIn (render t0) $
   case t0 of
@@ -186,7 +190,7 @@ value env t0 =
     ELin c r -> (unlockVRec (gloc env) c.) # value env r
     EPatt p  -> return $ const (VPatt p) -- hmm
     Typed t ty -> value env t
-    t -> fail.render $ "value"<+>ppT 10 t $$ show t
+    t -> fail.render $ "value"<+>ppTerm Unqualified 10 t $$ show t
 
 vconcat vv@(v1,v2) =
     case vv of
@@ -280,12 +284,14 @@ glue env (v1,v2) = glu v1 v2
 --        (v1,v2) -> ok2 VGlue v1 v2
           (v1,v2) -> if flag optPlusAsBind (opts env)
                        then VC v1 (VC (VApp BIND []) v2)
-                       else error . render $
-                                      ppL loc (hang "unsupported token gluing:" 4
-                                                    (Glue (vt v1) (vt v2)))
+                       else let loc  = gloc env
+                                vt v = case value2term loc (local env) v of
+                                         Left i  -> Error ('#':show i)
+                                         Right t -> t
+                            in error . render $
+                                         ppL loc (hang "unsupported token gluing:" 4
+                                                        (Glue (vt v1) (vt v2)))
 
-    vt = value2term loc (local env)
-    loc = gloc env
 
 -- | to get a string from a value that represents a sequence of terminals
 strsFromValue :: Value -> Err [Str]
@@ -337,7 +343,10 @@ select env vv =
       (VS (VV pty pvs rs) v12,v2) -> VS (VV pty pvs [select env (v11,v2)|v11<-rs]) v12
       (v1,v2) -> ok2 VS v1 v2
 
-match loc cs = err bad return . matchPattern cs . value2term loc []
+match loc cs v = 
+  case value2term loc [] v of
+    Left i  -> bad ("variable #"++show i++" is out of scope")
+    Right t -> err bad return (matchPattern cs t)
   where
     bad = fail . ("In pattern matching: "++)
 
@@ -357,13 +366,15 @@ valueTable env i cs =
 
     cases cs' vty vs = err keep ($vs) (convertv cs' (vty vs))
       where
-        keep msg = --trace (msg++"\n"++render (ppT 0 (T i cs))) $
+        keep msg = --trace (msg++"\n"++render (ppTerm Unqualified 0 (T i cs))) $
                    VT wild (vty vs) (mapSnd ($vs) cs')
 
     wild = case i of TWild _ -> True; _ -> False
 
-    convertv cs' vty = convert' cs' =<< paramValues'' env pty
-      where pty = value2term (gloc env) [] vty
+    convertv cs' vty = 
+      case value2term (gloc env) [] vty of
+        Left i    -> fail ("variable #"++show i++" is out of scope")
+        Right pty -> convert' cs' =<< paramValues'' env pty
 
     convert cs' ty = convert' cs' =<< paramValues' env ty
 
@@ -470,72 +481,64 @@ vtrace loc arg res = trace (render (hang (pv arg) 4 ("->"<+>pv res))) res
     pf (_,VString n) = pp n
     pf (_,v) = ppV v
     pa (_,v) = ppV v
-    ppV v = ppT 10 (trace2term loc [] v)
-
---  tr s f vs = trace (s++" "++show vs++" = "++show r) r where r = f vs
-
--- | When tracing, we need to avoid printing under lambdas...
-trace2term = value2term' True
+    ppV v = case value2term' True loc [] v of
+              Left i  -> "variable #" <> pp i <+> "is out of scope"
+              Right t -> ppTerm Unqualified 10 t
 
 -- | Convert a value back to a term
-value2term :: GLocation -> [Ident] -> Value -> Term
+value2term :: GLocation -> [Ident] -> Value -> Either Int Term
 value2term = value2term' False
 value2term' stop loc xs v0 =
   case v0 of
-    VApp pre vs    -> foldl App (Q (cPredef,predefName pre)) (map v2t vs)
-    VCApp f vs     -> foldl App (QC f)                 (map v2t vs)
---  VGen j vs      -> foldl App (Vr (ix loc "value2term" (reverse xs) j)) (map v2t vs)
-    VGen j vs      -> foldl App (var j) (map v2t vs)
-    VMeta j env vs -> foldl App (Meta j)               (map v2t vs)
---  VClosure env (Prod bt x t1 t2) -> Prod bt x (v2t  (eval gr env t1))
---                                              (nf gr (push x (env,xs)) t2)
---  VClosure env (Abs  bt x t)     -> Abs  bt x (nf gr (push x (env,xs)) t)
-    VProd bt v x f -> Prod bt x (v2t v) (v2t' x f)
-    VAbs  bt   x f -> Abs  bt x         (v2t' x f)
-    VInt n         -> EInt n
-    VFloat f       -> EFloat f
-    VString s      -> if null s then Empty else K s
-    VSort s        -> Sort s
-    VImplArg v     -> ImplArg (v2t v)
-    VTblType p res -> Table (v2t p) (v2t res)
-    VRecType rs    -> RecType [(l,v2t v) | (l,v) <- rs]
-    VRec as        -> R [(l,(Nothing,v2t v))|(l,v) <- as]
-    VV t _ vs      -> V t (map v2t vs)
-    VT wild v cs   -> T ((if wild then TWild else TTyped) (v2t v))
-                        (map nfcase cs)
-    VFV vs         -> FV (map v2t vs)
-    VC v1 v2       -> C (v2t v1) (v2t v2)
-    VS v1 v2       -> S (v2t v1) (v2t v2)
-    VP v l         -> P (v2t v) l
-    VPatt p        -> EPatt p -- hmm
+    VApp pre vs    -> liftM (foldl App (Q (cPredef,predefName pre))) (mapM v2t vs)
+    VCApp f vs     -> liftM  (foldl App (QC f))   (mapM v2t vs)
+    VGen j vs      -> liftM2 (foldl App) (var j)  (mapM v2t vs)
+    VMeta j env vs -> liftM  (foldl App (Meta j)) (mapM v2t vs)
+    VProd bt v x f -> liftM2 (Prod bt x) (v2t v) (v2t' x f)
+    VAbs  bt   x f -> liftM  (Abs  bt x)         (v2t' x f)
+    VInt n         -> return (EInt n)
+    VFloat f       -> return (EFloat f)
+    VString s      -> return (if null s then Empty else K s)
+    VSort s        -> return (Sort s)
+    VImplArg v     -> liftM  ImplArg (v2t v)
+    VTblType p res -> liftM2 Table (v2t p) (v2t res)
+    VRecType rs    -> liftM  RecType (mapM (\(l,v) -> fmap ((,) l) (v2t v)) rs)
+    VRec as        -> liftM  R       (mapM (\(l,v) -> v2t v >>= \t -> return (l,(Nothing,t))) as)
+    VV t _ vs      -> liftM  (V t)   (mapM v2t vs)
+    VT wild v cs   -> v2t v >>= \t -> liftM (T ((if wild then TWild else TTyped) t)) (mapM nfcase cs)
+    VFV vs         -> liftM  FV (mapM v2t vs)
+    VC v1 v2       -> liftM2 C (v2t v1) (v2t v2)
+    VS v1 v2       -> liftM2 S (v2t v1) (v2t v2)
+    VP v l         -> v2t v >>= \t -> return (P t l)
+    VPatt p        -> return (EPatt p) -- hmm
 --  VPattType v    -> ...
-    VAlts v vvs    -> Alts (v2t v) (mapBoth v2t vvs)
-    VStrs vs       -> Strs (map v2t vs)
+    VAlts v vvs    -> liftM2 Alts (v2t v) (mapM (\(x,y) -> liftM2 (,) (v2t x) (v2t y)) vvs)
+    VStrs vs       -> liftM  Strs (mapM v2t vs)
 --  VGlue v1 v2    -> Glue (v2t v1) (v2t v2)
 --  VExtR v1 v2    -> ExtR (v2t v1) (v2t v2)
-    VError err     -> Error err
+    VError err     -> return (Error err)
     _              -> bug ("value2term "++show loc++" : "++show v0)
   where
     v2t = v2txs xs
     v2txs = value2term' stop loc
     v2t' x f = v2txs (x:xs) (bind f (gen xs))
 
-    var j = if j<n
-            then Vr (reverse xs !! j)
-            else Error ("VGen "++show j++" "++show xs) -- bug hunting
-      where n = length xs
+    var j
+      | j<length xs = Right (Vr (reverse xs !! j))
+      | otherwise   = Left  j
+
 
     pushs xs e = foldr push e xs
     push x (env,xs) = ((x,gen xs):env,x:xs)
     gen xs = VGen (length xs) []
 
-    nfcase (p,f) = (p,v2txs xs' (bind f env'))
+    nfcase (p,f) = liftM ((,) p) (v2txs xs' (bind f env'))
       where (env',xs') = pushs (pattVars p) ([],xs)
 
     bind (Bind f) x = if stop
                       then VSort (identS "...") -- hmm
                       else f x
---  nf gr (env,xs) = value2term xs . eval gr env
+
 
 linPattVars p =
     if null dups
@@ -568,8 +571,6 @@ mf <# mx  = ap mf mx
 
 both f (x,y) = (,) # f x <# f y
 
-ppT = ppTerm Unqualified
-
 bugloc loc s = ppbug $ ppL loc s
 
 bug msg = ppbug msg
diff --git a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
index 42a54edbc..e58d7a4b7 100644
--- a/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
+++ b/src/compiler/GF/Compile/TypeCheck/ConcreteNew.hs
@@ -14,8 +14,7 @@ import GF.Compile.Compute.Predef(predef,predefName)
 import GF.Infra.CheckM
 import GF.Data.Operations
 import Control.Applicative(Applicative(..))
-import Control.Monad(ap)
-
+import Control.Monad(ap,liftM)
 import GF.Text.Pretty
 import Data.List (nub, (\\), tails)
 import qualified Data.IntMap as IntMap
@@ -32,7 +31,7 @@ inferLType :: GlobalEnv -> Term -> Check (Term, Type)
 inferLType ge t = runTcM $ do
   (t,ty) <- inferSigma ge [] t
   t  <- zonkTerm t
-  ty <- zonkTerm (value2term (geLoc ge) [] ty)
+  ty <- zonkTerm =<< tc_value2term (geLoc ge) [] ty
   return (t,ty)
 
 inferSigma :: GlobalEnv -> Scope -> Term -> TcM (Term,Sigma)
@@ -45,14 +44,8 @@ inferSigma ge scope t = do                                      -- GEN1
 
 checkSigma :: GlobalEnv -> Scope -> Term -> Sigma -> TcM Term
 checkSigma ge scope t sigma = do                                -- GEN2
-  (abs, scope, t, rho) <- skolemise id scope t sigma
-  let skol_tvs = []
-  (t,rho) <- tcRho ge scope t (Just rho)
-  esc_tvs <- getFreeVars (geLoc ge) ((scope,sigma) : scopeTypes scope)
-  let bad_tvs = filter (`elem` esc_tvs) skol_tvs
-  if null bad_tvs
-    then return (abs t)
-    else tcError (pp "Type not polymorphic enough")
+  (t,rho) <- tcRho ge scope t (Just sigma)
+  return t
 
 Just vtypeInt   = fmap (flip VApp []) (predef cInt)
 Just vtypeFloat = fmap (flip VApp []) (predef cFloat)
@@ -81,21 +74,39 @@ tcRho ge scope t@(QC id)     mb_ty =
     Ok ty   -> do vty <- liftErr (eval ge [] ty)
                   instSigma ge scope t vty mb_ty
     Bad err -> tcError (pp err)
-tcRho ge scope (App fun arg) mb_ty = do                         -- APP
+tcRho ge scope t@(App fun (ImplArg arg)) mb_ty = do             -- APP1
+  (fun,fun_ty) <- tcRho ge scope fun Nothing
+  (bt, arg_ty, res_ty) <- unifyFun ge scope fun_ty
+  if (bt == Implicit)
+    then return ()
+    else tcError (ppTerm Unqualified 0 t <+> "is an implicit argument application, but no implicit argument is expected")
+  arg <- checkSigma ge scope arg arg_ty
+  varg <- liftErr (eval ge (scopeEnv scope) arg)
+  instSigma ge scope (App fun (ImplArg arg)) (res_ty varg) mb_ty
+tcRho ge scope (App fun arg) mb_ty = do                         -- APP2
   (fun,fun_ty) <- tcRho ge scope fun Nothing
-  (arg_ty, res_ty) <- unifyFun ge scope fun_ty
+  (fun,fun_ty) <- instantiate scope fun fun_ty
+  (_, arg_ty, res_ty) <- unifyFun ge scope fun_ty
   arg <- checkSigma ge scope arg arg_ty
   varg <- liftErr (eval ge (scopeEnv scope) arg)
   instSigma ge scope (App fun arg) (res_ty varg) mb_ty
 tcRho ge scope (Abs bt var body) Nothing = do                   -- ABS1
-  i <- newMeta vtypeType
+  i <- newMeta scope vtypeType
   let arg_ty = VMeta i (scopeEnv scope) []
   (body,body_ty) <- tcRho ge ((var,arg_ty):scope) body Nothing
   return (Abs bt var body, (VProd bt arg_ty identW (Bind (const body_ty))))
-tcRho ge scope (Abs bt var body) (Just ty) = do                 -- ABS2
-  (var_ty, body_ty) <- unifyFun ge scope ty
+tcRho ge scope t@(Abs Implicit var body) (Just ty) = do         -- ABS2
+  (bt, var_ty, body_ty) <- unifyFun ge scope ty
+  if bt == Implicit
+    then return ()
+    else tcError (ppTerm Unqualified 0 t <+> "is an implicit function, but no implicit function is expected")
   (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
-  return (Abs bt var body,ty)
+  return (Abs Implicit var body,ty)
+tcRho ge scope (Abs Explicit var body) (Just ty) = do           -- ABS3
+  (scope,f,ty') <- skolemise scope ty
+  (_,var_ty,body_ty) <- unifyFun ge scope ty'
+  (body, body_ty) <- tcRho ge ((var,var_ty):scope) body (Just (body_ty (VGen (length scope) [])))
+  return (f (Abs Explicit var body),ty)
 tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do    -- LET
   (rhs,var_ty) <- case mb_ann_ty of
                     Nothing     -> inferSigma ge scope rhs
@@ -104,7 +115,8 @@ tcRho ge scope (Let (var, (mb_ann_ty, rhs)) body) mb_ty = do    -- LET
                                       rhs <- checkSigma ge scope rhs v_ann_ty
                                       return (rhs, v_ann_ty)
   (body, body_ty) <- tcRho ge ((var,var_ty):scope) body mb_ty
-  return (Let (var, (Just (value2term (geLoc ge) (scopeVars scope) var_ty), rhs)) body, body_ty)
+  var_ty <- tc_value2term (geLoc ge) (scopeVars scope) var_ty
+  return (Let (var, (Just var_ty, rhs)) body, body_ty)
 tcRho ge scope (Typed body ann_ty) mb_ty = do                   -- ANNOT
   (ann_ty, _) <- tcRho ge scope ann_ty (Just vtypeType)
   v_ann_ty <- liftErr (eval ge (scopeEnv scope) ann_ty)
@@ -112,7 +124,7 @@ tcRho ge scope (Typed body ann_ty) mb_ty = do                   -- ANNOT
   instSigma ge scope (Typed body ann_ty) v_ann_ty mb_ty
 tcRho ge scope (FV ts) mb_ty = do
   case ts of
-    []     -> do i <- newMeta vtypeType
+    []     -> do i <- newMeta scope vtypeType
                  instSigma ge scope (FV []) (VMeta i (scopeEnv scope) []) mb_ty
     (t:ts) -> do (t,ty) <- tcRho ge scope t mb_ty
     
@@ -125,75 +137,86 @@ tcRho ge scope (FV ts) mb_ty = do
                  return (FV (t:ts), ty)
 tcRho ge scope t@(Sort s) mb_ty = do
   instSigma ge scope t vtypeType mb_ty
-tcRho ge scope t@(RecType rs) mb_ty = do
-  case mb_ty of
-    Nothing           -> return ()
-    Just ty@(VSort s)
-      | s == cType    -> return ()
-      | s == cPType   -> return ()
-    Just (VMeta _ _ _)-> return ()
-    Just ty           -> do ty <- zonkTerm (value2term (geLoc ge) (scopeVars scope) ty)
-                            tcError ("The record type" <+> ppTerm Unqualified 0 t $$ 
-                                     "cannot be of type" <+> ppTerm Unqualified 0 ty)
-  (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
+tcRho ge scope t@(RecType rs) Nothing   = do
+  (rs,mb_ty) <- tcRecTypeFields ge scope rs Nothing
   return (RecType rs,fromMaybe vtypePType mb_ty)
+tcRho ge scope t@(RecType rs) (Just ty) = do
+  (scope,f,ty') <- skolemise scope ty
+  case ty' of
+    VSort s
+      | s == cType  -> return ()
+      | s == cPType -> return ()
+    VMeta i env vs  -> case rs of
+                         [] -> unifyVar ge scope i env vs vtypePType
+                         _  -> return ()
+    ty              -> do ty <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) ty
+                          tcError ("The record type" <+> ppTerm Unqualified 0 t $$ 
+                                   "cannot be of type" <+> ppTerm Unqualified 0 ty)
+  (rs,mb_ty) <- tcRecTypeFields ge scope rs (Just ty')
+  return (f (RecType rs),ty)
 tcRho ge scope t@(Table p res) mb_ty = do
   (p,  p_ty)   <- tcRho ge scope p   (Just vtypePType)
-  (res,res_ty) <- tcRho ge scope res Nothing
-  subsCheckRho ge scope t res_ty vtypeType
-  instSigma ge scope (Table p res) res_ty mb_ty
+  (res,res_ty) <- tcRho ge scope res (Just vtypeType)
+  instSigma ge scope (Table p res) vtypeType mb_ty
 tcRho ge scope (Prod bt x ty1 ty2) mb_ty = do
   (ty1,ty1_ty) <- tcRho ge scope ty1 (Just vtypeType)
   vty1 <- liftErr (eval ge (scopeEnv scope) ty1)
   (ty2,ty2_ty) <- tcRho ge ((x,vty1):scope) ty2 (Just vtypeType)
   instSigma ge scope (Prod bt x ty1 ty2) vtypeType mb_ty
 tcRho ge scope (S t p) mb_ty = do
-  p_ty   <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType
-  res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType
+  p_ty   <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType
+  res_ty <- fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
   let t_ty = VTblType p_ty res_ty
   (t,t_ty) <- tcRho ge scope t (Just t_ty)
   p <- checkSigma ge scope p p_ty
   instSigma ge scope (S t p) res_ty mb_ty
 tcRho ge scope (T tt ps) Nothing = do                           -- ABS1/AABS1 for tables
   p_ty   <- case tt of
-              TRaw      -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypePType
+              TRaw      -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypePType
               TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
                               liftErr (eval ge (scopeEnv scope) ty)
   (ps,mb_res_ty) <- tcCases ge scope ps p_ty Nothing
   res_ty <- case mb_res_ty of
               Just res_ty -> return res_ty
-              Nothing     -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta vtypeType
-  return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty)
+              Nothing     -> fmap (\i -> VMeta i (scopeEnv scope) []) $ newMeta scope vtypeType
+  p_ty_t <- tc_value2term (geLoc ge) [] p_ty
+  return (T (TTyped p_ty_t) ps, VTblType p_ty res_ty)
 tcRho ge scope (T tt ps) (Just ty) = do                         -- ABS2/AABS2 for tables
-  (p_ty, res_ty) <- unifyTbl ge scope ty
+  (scope,f,ty') <- skolemise scope ty
+  (p_ty, res_ty) <- unifyTbl ge scope ty'
   case tt of
     TRaw      -> return ()
     TTyped ty -> do (ty, _) <- tcRho ge scope ty (Just vtypeType)
                     return ()--subsCheckRho ge scope -> Term ty res_ty
   (ps,Just res_ty) <- tcCases ge scope ps p_ty (Just res_ty)
-  return (T (TTyped (value2term (geLoc ge) [] p_ty)) ps, VTblType p_ty res_ty)
-tcRho ge scope (R rs) mb_ty = do
-  case mb_ty of
-    Nothing              -> do lttys <- inferRecFields ge scope rs
-                               return (R        [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], 
-                                       VRecType [(l, ty) | (l,t,ty) <- lttys]
-                                      )
-    Just (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
-                               return (R        [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys], 
-                                       VRecType [(l, ty) | (l,t,ty) <- lttys]
-                                      )
-    Just ty              -> do lttys <- inferRecFields ge scope rs
-                               let t   = R        [(l, (Just (value2term (geLoc ge) (scopeVars scope) ty), t)) | (l,t,ty) <- lttys]
-                                   ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
-                               t <- subsCheckRho ge scope t ty' ty
-                               return (t, ty')
+  p_ty_t <- tc_value2term (geLoc ge) [] p_ty
+  return (f (T (TTyped p_ty_t) ps), VTblType p_ty res_ty)
+tcRho ge scope (R rs) Nothing = do
+  lttys <- inferRecFields ge scope rs
+  rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
+  return (R        rs,
+          VRecType [(l, ty) | (l,t,ty) <- lttys]
+         )
+tcRho ge scope (R rs) (Just ty) = do
+  (scope,f,ty') <- skolemise scope ty
+  case ty' of
+    (VRecType ltys) -> do lttys <- checkRecFields ge scope rs ltys
+                          rs <- mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys
+                          return ((f . R)  rs, 
+                                  VRecType [(l, ty) | (l,t,ty) <- lttys]
+                                 )
+    ty              -> do lttys <- inferRecFields ge scope rs
+                          t <- liftM (f . R) (mapM (\(l,t,ty) -> tc_value2term (geLoc ge) (scopeVars scope) ty >>= \ty -> return (l, (Just ty, t))) lttys)
+                          let ty' = VRecType [(l, ty) | (l,t,ty) <- lttys]
+                          t <- subsCheckRho ge scope t ty' ty
+                          return (t, ty')
 tcRho ge scope (P t l) mb_ty = do
-  x_ty   <- case mb_ty of
+  l_ty   <- case mb_ty of
               Just ty -> return ty
-              Nothing -> do i <- newMeta vtypeType
+              Nothing -> do i <- newMeta scope vtypeType
                             return (VMeta i (scopeEnv scope) [])
-  (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,x_ty)]))
-  return (P t l,x_ty)
+  (t,t_ty) <- tcRho ge scope t (Just (VRecType [(l,l_ty)]))
+  return (P t l,l_ty)
 tcRho ge scope (C t1 t2) mb_ty = do
   (t1,t1_ty) <- tcRho ge scope t1 (Just vtypeStr)
   (t2,t2_ty) <- tcRho ge scope t2 (Just vtypeStr)
@@ -207,10 +230,13 @@ tcRho ge scope t@(ExtR t1 t2) mb_ty = do
   (t2,t2_ty) <- tcRho ge scope t2 Nothing
   case (t1_ty,t2_ty) of
     (VSort s1,VSort s2)
-       | s1 == cType && s2 == cType -> instSigma ge scope (ExtR t1 t2) (VSort cType) mb_ty
-    (VRecType rs1, VRecType rs2) 
-       | otherwise                  -> instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty
-    _                               -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
+       | (s1 == cType || s1 == cPType) &&
+         (s2 == cType || s2 == cPType) -> let sort | s1 == cPType && s2 == cPType = cPType
+                                                   | otherwise                    = cType
+                                          in instSigma ge scope (ExtR t1 t2) (VSort sort) mb_ty
+    (VRecType rs1, VRecType rs2)
+       | otherwise                     -> instSigma ge scope (ExtR t1 t2) (VRecType (rs1 ++ rs2)) mb_ty
+    _                                  -> tcError ("Cannot type check" <+> ppTerm Unqualified 0 t)
 tcRho ge scope (ELin cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
   tcRho ge scope (ExtR t (R [(lockLabel cat,(Just (RecType []),R []))])) mb_ty
 tcRho ge scope (ELincat cat t) mb_ty = do  -- this could be done earlier, i.e. in the parser
@@ -243,7 +269,7 @@ tcPatt ge scope (PV x)    ty0 =
 tcPatt ge scope (PP c ps) ty0 =
   case lookupResType (geGrammar ge) c of
     Ok ty  -> do let go scope ty []     = return (scope,ty)
-                     go scope ty (p:ps) = do (arg_ty,res_ty) <- unifyFun ge scope ty
+                     go scope ty (p:ps) = do (_,arg_ty,res_ty) <- unifyFun ge scope ty
                                              scope <- tcPatt ge scope p arg_ty
                                              go scope (res_ty (VGen (length scope) [])) ps
                  vty <- liftErr (eval ge [] ty)
@@ -269,7 +295,7 @@ tcPatt ge scope (PAs x p) ty0 = do
   tcPatt ge ((x,ty0):scope) p ty0
 tcPatt ge scope (PR rs) ty0 = do
   let mk_ltys  []            = return []
-      mk_ltys  ((l,p):rs)    = do i <- newMeta vtypePType
+      mk_ltys  ((l,p):rs)    = do i <- newMeta scope vtypePType
                                   ltys <- mk_ltys rs
                                   return ((l,p,VMeta i (scopeEnv scope) []) : ltys)
       go scope []            = return scope
@@ -323,7 +349,7 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
                | s == cType  -> return (Just sort)
                | s == cPType -> return mb_ty
              VMeta _ _ _     -> return mb_ty
-             _               -> do sort <- zonkTerm (value2term (geLoc ge) (scopeVars scope) sort)
+             _               -> do sort <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) sort
                                    tcError ("The record type field" <+> l <+> ':' <+> ppTerm Unqualified 0 ty $$ 
                                             "cannot be of type" <+> ppTerm Unqualified 0 sort)
   (rs,mb_ty) <- tcRecTypeFields ge scope rs mb_ty
@@ -332,37 +358,25 @@ tcRecTypeFields ge scope ((l,ty):rs) mb_ty = do
 -- | Invariant: if the third argument is (Just rho),
 -- 	            then rho is in weak-prenex form
 instSigma :: GlobalEnv -> Scope -> Term -> Sigma -> Maybe Rho -> TcM (Term, Rho)
-instSigma ge scope t ty1 Nothing    = instantiate t ty1        -- INST1
+instSigma ge scope t ty1 Nothing    = return (t,ty1)           -- INST1
 instSigma ge scope t ty1 (Just ty2) = do                       -- INST2
   t <- subsCheckRho ge scope t ty1 ty2
   return (t,ty2)
 
--- | (subsCheck scope args off exp) checks that 
---     'off' is at least as polymorphic as 'args -> exp'
-subsCheck :: GlobalEnv -> Scope -> Term -> Sigma -> Sigma -> TcM Term
-subsCheck ge scope t sigma1 sigma2 = do                        -- DEEP-SKOL
-  (abs, scope, t, rho2) <- skolemise id scope t sigma2
-  let skol_tvs = []
-  t <- subsCheckRho ge scope t sigma1 rho2
-  esc_tvs <- getFreeVars (geLoc ge) [(scope,sigma1),(scope,sigma2)]
-  let bad_tvs = filter (`elem` esc_tvs) skol_tvs
-  if null bad_tvs
-    then return (abs t)
-    else tcError (vcat [pp "Subsumption check failed:",
-                        nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) sigma1)),
-                        pp "is not as polymorphic as",
-                        nest 2 (ppTerm Unqualified 0 (value2term (geLoc ge) (scopeVars scope) sigma2))])
-
 -- | Invariant: the second argument is in weak-prenex form
 subsCheckRho :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> TcM Term
-subsCheckRho ge scope t sigma1@(VProd Implicit _ _ _) rho2 = do         -- Rule SPEC
-  (t,rho1) <- instantiate t sigma1
-  subsCheckRho ge scope t rho1 rho2
+subsCheckRho ge scope t (VProd Implicit ty1 x (Bind ty2)) rho2 = do     -- Rule SPEC1
+  i <- newMeta scope ty1
+  subsCheckRho ge scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] [])) rho2
+subsCheckRho ge scope t rho1 (VProd Implicit ty1 x (Bind ty2)) = do     -- Rule SPEC2
+  let v = newVar scope
+  t <- subsCheckRho ge ((v,ty1):scope) t rho1 (ty2 (VGen (length scope) []))
+  return (Abs Implicit v t)
 subsCheckRho ge scope t rho1 (VProd Explicit a2 _ (Bind r2)) = do       -- Rule FUN
-  (a1,r1) <- unifyFun ge scope rho1
+  (_,a1,r1) <- unifyFun ge scope rho1
   subsCheckFun ge scope t a1 r1 a2 r2
 subsCheckRho ge scope t (VProd Explicit a1 _ (Bind r1)) rho2 = do       -- Rule FUN
-  (a2,r2) <- unifyFun ge scope rho2
+  (bt,a2,r2) <- unifyFun ge scope rho2
   subsCheckFun ge scope t a1 r1 a2 r2
 subsCheckRho ge scope t rho1 (VTblType p2 r2) = do                      -- Rule FUN for table types
   (p1,r1) <- unifyTbl ge scope rho1
@@ -397,7 +411,7 @@ subsCheckRho ge scope t ty1@(VRecType rs1) ty2@(VRecType rs2) = do
   let mkField f (l,(mb_ty,t)) = do
         t <- f t
         return (l,(mb_ty,t))
-  rs <- sequence [mkField (\t -> subsCheck ge scope t ty1 ty2) (mkProj l) | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
+  rs <- sequence [mkField (\t -> subsCheckRho ge scope t ty1 ty2) (mkProj l) | (l,ty1) <- rs1, Just ty2 <- [lookup l rs2]]
   return (mkRec rs)
 subsCheckRho ge scope t tau1 tau2 = do                                  -- Rule MONO
   unify ge scope tau1 tau2                                 -- Revert to ordinary unification
@@ -405,40 +419,42 @@ subsCheckRho ge scope t tau1 tau2 = do                                  -- Rule
 
 subsCheckFun :: GlobalEnv -> Scope -> Term -> Sigma -> (Value -> Rho) -> Sigma -> (Value -> Rho) -> TcM Term
 subsCheckFun ge scope t a1 r1 a2 r2 = do
-  let x   = newVar scope
+  let v   = newVar scope
   let val = VGen (length scope) []
-  xt <- subsCheck ge scope (Vr x) a2 a1
-  t  <- subsCheckRho ge ((x,vtypeType):scope) (App t xt) (r1 val) (r2 val);
-  return (Abs Explicit x t)
+  vt <- subsCheckRho ge ((v,vtypeType):scope) (Vr v) a2 a1
+  t  <- subsCheckRho ge ((v,vtypeType):scope) (App t vt) (r1 val) (r2 val);
+  return (Abs Explicit v t)
 
 subsCheckTbl :: GlobalEnv -> Scope -> Term -> Sigma -> Rho -> Sigma -> Rho -> TcM Term
 subsCheckTbl ge scope t p1 r1 p2 r2 = do
   let x = newVar scope
-  xt <- subsCheck ge scope (Vr x) p2 p1
+  xt <- subsCheckRho ge scope (Vr x) p2 p1
   t  <- subsCheckRho ge ((x,vtypePType):scope) (S t xt) r1 r2 ;
-  return (T (TTyped (value2term (geLoc ge) (scopeVars scope) p2)) [(PV x,t)])
+  p2 <- tc_value2term (geLoc ge) (scopeVars scope) p2
+  return (T (TTyped p2) [(PV x,t)])
 
 -----------------------------------------------------------------------
 -- Unification
 -----------------------------------------------------------------------
 
-unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Value -> Rho)
-unifyFun ge scope (VProd Explicit arg x (Bind res)) =
-  return (arg,res)
+unifyFun :: GlobalEnv -> Scope -> Rho -> TcM (BindType, Sigma, Value -> Rho)
+unifyFun ge scope (VProd bt arg x (Bind res)) =
+  return (bt,arg,res)
 unifyFun ge scope tau = do
   let mk_val ty = VMeta ty [] []
-  arg <- fmap mk_val $ newMeta vtypeType
-  res <- fmap mk_val $ newMeta vtypeType
-  unify ge scope tau (VProd Explicit arg identW (Bind (const res)))
-  return (arg,const res)
+  arg <- fmap mk_val $ newMeta scope vtypeType
+  res <- fmap mk_val $ newMeta scope vtypeType
+  let bt = Explicit
+  unify ge scope tau (VProd bt arg identW (Bind (const res)))
+  return (bt,arg,const res)
 
 unifyTbl :: GlobalEnv -> Scope -> Rho -> TcM (Sigma, Rho)
 unifyTbl ge scope (VTblType arg res) =
   return (arg,res)
 unifyTbl ge scope tau = do
   let mk_val ty = VMeta ty [] []
-  arg <- fmap mk_val $ newMeta vtypePType
-  res <- fmap mk_val $ newMeta vtypeType
+  arg <- fmap mk_val $ newMeta scope vtypePType
+  res <- fmap mk_val $ newMeta scope vtypeType
   unify ge scope tau (VTblType arg res)
   return (arg,res)
 
@@ -450,24 +466,24 @@ unify ge scope (VSort s1)         (VSort s2)
   | s1 == s2                   = return ()
 unify ge scope (VGen i vs1)       (VGen j vs2)
   | i == j                     = sequence_ (zipWith (unify ge scope) vs1 vs2)
+unify ge scope (VTblType p1 res1) (VTblType p2 res2) = do
+  unify ge scope p1   p2
+  unify ge scope res1 res2
 unify ge scope (VMeta i env1 vs1) (VMeta j env2 vs2)
   | i  == j                    = sequence_ (zipWith (unify ge scope) vs1 vs2)
   | otherwise                  = do mv <- getMeta j
                                     case mv of
-                                      Bound t2  -> do v2 <- liftErr (eval ge env2 t2)
-                                                      unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
-                                      Unbound _ -> setMeta i (Bound (Meta j))
+                                      Bound t2    -> do v2 <- liftErr (eval ge env2 t2)
+                                                        unify ge scope (VMeta i env1 vs1) (vapply (geLoc ge) v2 vs2)
+                                      Unbound _ _ -> setMeta i (Bound (Meta j))
 unify ge scope (VInt i)       (VInt j)
   | i == j                     = return ()
 unify ge scope (VMeta i env vs) v = unifyVar ge scope i env vs v
 unify ge scope v (VMeta i env vs) = unifyVar ge scope i env vs v
-unify ge scope (VTblType p1 res1) (VTblType p2 res2) = do
-  unify ge scope p1   p2
-  unify ge scope res1 res2
 unify ge scope v1 v2 = do
-  t1 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v1)
-  t2 <- zonkTerm (value2term (geLoc ge) (scopeVars scope) v2)
-  tcError ("Cannot unify types:" <+> (ppTerm Unqualified 0 t1 $$ 
+  t1 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v1
+  t2 <- zonkTerm =<< tc_value2term (geLoc ge) (scopeVars scope) v2
+  tcError ("Cannot unify terms:" <+> (ppTerm Unqualified 0 t1 $$ 
                                       ppTerm Unqualified 0 t2))
 
 -- | Invariant: tv1 is a flexible type variable
@@ -475,60 +491,49 @@ unifyVar :: GlobalEnv -> Scope -> MetaId -> Env -> [Value] -> Tau -> TcM ()
 unifyVar ge scope i env vs ty2 = do            -- Check whether i is bound
   mv <- getMeta i
   case mv of
-    Bound ty1 -> do v <- liftErr (eval ge env ty1)
-                    unify ge scope (vapply (geLoc ge) v vs) ty2
-    Unbound _ -> do let ty2' = value2term (geLoc ge) (scopeVars scope) ty2
-                    ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
-                    if i `elem` ms2
-                      then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
-                                    nest 2 (ppTerm Unqualified 0 ty2'))
-                      else setMeta i (Bound ty2')
+    Bound ty1       -> do v <- liftErr (eval ge env ty1)
+                          unify ge scope (vapply (geLoc ge) v vs) ty2
+    Unbound scope' _ -> case value2term (geLoc ge) (scopeVars scope') ty2 of
+                          Left i     -> let (v,_) = reverse scope !! i
+                                        in tcError ("Variable" <+> pp v <+> "has escaped")
+                          Right ty2' -> do ms2 <- getMetaVars (geLoc ge) [(scope,ty2)]
+                                           if i `elem` ms2
+                                             then tcError ("Occurs check for" <+> ppMeta i <+> "in:" $$
+                                                           nest 2 (ppTerm Unqualified 0 ty2'))
+                                             else setMeta i (Bound ty2')
 
 -----------------------------------------------------------------------
 -- Instantiation and quantification
 -----------------------------------------------------------------------
 
--- | Instantiate the topmost for-alls of the argument type
--- with metavariables
-instantiate :: Term -> Sigma -> TcM (Term,Rho)
-instantiate t (VProd Implicit ty1 x (Bind ty2)) = do
-  i <- newMeta ty1
-  instantiate (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
-instantiate t ty = do
+-- | Instantiate the topmost implicit arguments with metavariables
+instantiate :: Scope -> Term -> Sigma -> TcM (Term,Rho)
+instantiate scope t (VProd Implicit ty1 x (Bind ty2)) = do
+  i <- newMeta scope ty1
+  instantiate scope (App t (ImplArg (Meta i))) (ty2 (VMeta i [] []))
+instantiate scope t ty = do
   return (t,ty)
 
-skolemise f scope t (VProd Implicit arg_ty x (Bind res_ty))   -- Rule PRPOLY
-  | x /= identW = 
-      let (y,body) = case t of
-                       Abs Implicit y body -> (y, body)
-                       body                -> (newVar scope, body)
-      in skolemise (f . Abs Implicit y)
-                   ((y,arg_ty):scope) body
-                   (res_ty (VGen (length scope) []))
-skolemise f scope t (VProd Explicit arg_ty x (Bind res_ty))   -- Rule PRFUN
-  | x /= identW =
-      let (y,body) = case t of
-                       Abs Explicit y body -> (y, body)
-                       body                -> let y = newVar scope
-                                              in (y, App body (Vr y))
-      in skolemise (f . Abs Explicit y)
-                   ((y,arg_ty):scope) body
-                   (res_ty (VGen (length scope) []))
-skolemise f scope t ty                                        -- Rule PRMONO
-  = return (f, scope, t, ty)
+-- | Build fresh lambda abstractions for the topmost implicit arguments
+skolemise :: Scope -> Sigma -> TcM (Scope, Term->Term, Rho)
+skolemise scope (VProd Implicit ty1 x (Bind ty2)) = do
+  let v = newVar scope
+  (scope,f,ty2) <- skolemise ((v,ty1):scope) (ty2 (VGen (length scope) []))
+  return (scope,Abs Implicit v . f,ty2)
+skolemise scope ty = do
+  return (scope,id,ty)
 
 -- | Quantify over the specified type variables (all flexible)
 quantify :: GlobalEnv -> Scope -> Term -> [MetaId] -> Rho -> TcM (Term,Sigma)
 quantify ge scope t tvs ty0 = do
+  ty <- tc_value2term (geLoc ge) (scopeVars scope) ty0
+  let used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
+      new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
   mapM_ bind (tvs `zip` new_bndrs)   -- 'bind' is just a cunning way 
   ty <- zonkTerm ty                  -- of doing the substitution
   vty <- liftErr (eval ge [] (foldr (\v ty -> Prod Implicit v typeType ty) ty new_bndrs))
   return (foldr (Abs Implicit) t new_bndrs,vty)
   where
-    ty = value2term (geLoc ge) (scopeVars scope) ty0
-
-    used_bndrs = nub (bndrs ty)  -- Avoid quantified type variables in use
-    new_bndrs  = take (length tvs) (allBinders \\ used_bndrs)
     bind (i, name) = setMeta i (Bound (Vr name))
 
     bndrs (Prod _ x t1 t2) = [x] ++ bndrs t1  ++ bndrs t2
@@ -550,7 +555,7 @@ type Rho   = Value	-- No top-level ForAll
 type Tau   = Value	-- No ForAlls anywhere
 
 data MetaValue
-  = Unbound Sigma
+  = Unbound Scope Sigma
   | Bound   Term
 type MetaStore = IntMap.IntMap MetaValue
 data TcResult a
@@ -593,10 +598,10 @@ runTcM f = case unTcM f IntMap.empty [] of
              TcOk x _ msgs -> do checkWarnings msgs; return x
              TcFail (msg:msgs) -> do checkWarnings msgs; checkError msg
 
-newMeta :: Sigma -> TcM MetaId
-newMeta ty = TcM (\ms msgs -> 
+newMeta :: Scope -> Sigma -> TcM MetaId
+newMeta scope ty = TcM (\ms msgs -> 
   let i = IntMap.size ms
-  in TcOk i (IntMap.insert i (Unbound ty) ms) msgs)
+  in TcOk i (IntMap.insert i (Unbound scope ty) ms) msgs)
 
 getMeta :: MetaId -> TcM MetaValue
 getMeta i = TcM (\ms msgs -> 
@@ -623,7 +628,7 @@ scopeTypes scope = zipWith (\(_,ty) scope -> (scope,ty)) scope (tails scope)
 -- (no duplicates) of unbound meta-type variables
 getMetaVars :: GLocation -> [(Scope,Sigma)] -> TcM [MetaId]
 getMetaVars loc sc_tys = do
-  tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys
+  tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
   return (foldr go [] tys)
   where
     -- Get the MetaIds from a term; no duplicates in result
@@ -644,7 +649,7 @@ getMetaVars loc sc_tys = do
 -- (no duplicates) of free type variables
 getFreeVars :: GLocation -> [(Scope,Sigma)] -> TcM [Ident]
 getFreeVars loc sc_tys = do
-  tys <- mapM (\(scope,ty) -> zonkTerm (value2term loc (scopeVars scope) ty)) sc_tys
+  tys <- mapM (\(scope,ty) -> zonkTerm =<< tc_value2term loc (scopeVars scope) ty) sc_tys
   return (foldr (go []) [] tys)
   where
     go bound (Vr tv)            acc 
@@ -664,10 +669,13 @@ zonkTerm :: Term -> TcM Term
 zonkTerm (Meta i) = do
   mv <- getMeta i
   case mv of
-    Unbound _ -> return (Meta i)
-    Bound t   -> do t <- zonkTerm t
-                    setMeta i (Bound t)       -- "Short out" multiple hops
-                    return t
+    Unbound _ _ -> return (Meta i)
+    Bound t     -> do t <- zonkTerm t
+                      setMeta i (Bound t)       -- "Short out" multiple hops
+                      return t
 zonkTerm t = composOp zonkTerm t
 
-
+tc_value2term loc xs v = 
+  case value2term loc xs v of
+    Left i  -> tcError ("Variable #" <+> pp i <+> "has escaped")
+    Right t -> return t