syntax for implicit arguments in GF

20 files changed, 309 insertions, 339 deletions

diff --git a/src/GF/Compile/AbsCompute.hs b/src/GF/Compile/AbsCompute.hs
index 48499eb74..3f4c6d061 100644
--- a/src/GF/Compile/AbsCompute.hs
+++ b/src/GF/Compile/AbsCompute.hs
@@ -53,7 +53,7 @@ computeAbsTermIn lookd xs e = errIn (render (text "computing" <+> ppTerm Unquali
     _ -> do
       let t' = beta vv t
       (yy,f,aa) <- termForm t'
-      let vv' = yy ++ vv
+      let vv' = map snd yy ++ vv
       aa'    <- mapM (compt vv') aa
       case look f of
         Just eqs -> tracd (text "\nmatching" <+> ppTerm Unqualified 0 f) $ 
@@ -84,10 +84,10 @@ beta vv c = case c of
   App f         a -> 
     let (a',f') = (beta vv a, beta vv f) in 
     case f' of
-      Abs x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b) 
+      Abs _ x b -> beta vv $ substTerm vv [(x,a')] (beta (x:vv) b) 
       _ ->               (if a'==a && f'==f then id else beta vv) $ App f' a'
-  Prod x a b      -> Prod x (beta vv a) (beta (x:vv) b)
-  Abs x b         -> Abs x (beta (x:vv) b)
+  Prod b x a t      -> Prod b x (beta vv a) (beta (x:vv) t)
+  Abs b x t       -> Abs b x (beta (x:vv) t)
   _               -> c
 
 -- special version of pattern matching, to deal with comp under lambda
@@ -133,7 +133,7 @@ tryMatch (p,t) = do
   notMeta e = case e of
     Meta _  -> False
     App f a -> notMeta f &&  notMeta a  
-    Abs _ b -> notMeta b
+    Abs _ _ b -> notMeta b
     _ -> True
 
   prtm p g = 
diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index 6e6e27c74..98cd17f23 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -134,11 +134,11 @@ checkAbsInfo st m mo c info = do
      Let (x,(_,a)) b -> do
        a' <- compAbsTyp g a
        compAbsTyp ((x, a'):g) b
-     Prod x a b -> do
+     Prod b x a t -> do
        a' <- compAbsTyp g a
-       b' <- compAbsTyp ((x,Vr x):g) b
-       return $ Prod x a' b'
-     Abs _ _ -> return t
+       t' <- compAbsTyp ((x,Vr x):g) t
+       return $ Prod b x a' t'
+     Abs _ _ _ -> return t
      _ -> composOp (compAbsTyp g) t
 
 checkCompleteGrammar :: SourceGrammar -> SourceModInfo -> SourceModInfo -> Check (BinTree Ident Info)
@@ -170,7 +170,7 @@ checkCompleteGrammar gr abs cnc = do
                                                                    return info
                                                 _            -> return info
                                       case info of
-                                        CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs identW) (R []) cxt)
+                                        CncCat (Just (RecType [])) _ _ -> return (foldr (\_ -> Abs Explicit identW) (R []) cxt)
                                         _                              -> Bad "no def lin"
                                 case lookupIdent c js of
                                   Ok (CncFun _   (Just _) _ ) -> return js
@@ -224,7 +224,7 @@ checkResInfo gr mo mm c info = do
       --- this can only be a partial guarantee, since matching
       --- with value type is only possible if expected type is given
       checkUniq $ 
-        sort [t : map snd xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
+        sort [t : map (\(b,x,t) -> t) xs | (_,x) <- tysts1, Ok (xs,t) <- [typeFormCnc x]]
       return (ResOverload os [(y,x) | (x,y) <- tysts'])
 
     ResParam (Just (pcs,_)) -> chIn "parameter type" $ do
@@ -257,7 +257,7 @@ checkCncInfo gr m mo (a,abs) c info = do
       typ        <- checkErr $ lookupFunType gr a c
       cat0       <- checkErr $ valCat typ
       (cont,val) <- linTypeOfType gr m typ         -- creates arg vars
-      (trm',_)   <- check trm (mkFunType (map snd cont) val)  -- erases arg vars
+      (trm',_)   <- check trm (mkFunType (map (\(_,_,ty) -> ty) cont) val)  -- erases arg vars
       checkPrintname gr mpr
       cat        <- return $ snd cat0
       return (CncFun (Just (cat,(cont,val))) (Just trm') mpr)
@@ -286,7 +286,7 @@ checkCncInfo gr m mo (a,abs) c info = do
 computeLType :: SourceGrammar -> Type -> Check Type
 computeLType gr t = do
   g0 <- checkGetContext
-  let g = [(x, Vr x) | (x,_) <- g0]
+  let g = [(b,x, Vr x) | (b,x,_) <- g0]
   checkInContext g $ comp t
  where
   comp ty = case ty of
@@ -303,17 +303,17 @@ computeLType gr t = do
       f' <- comp f
       a' <- comp a
       case f' of
-        Abs x b -> checkInContext [(x,a')] $ comp b
+        Abs b x t -> checkInContext [(b,x,a')] $ comp t
         _ -> return $ App f' a'
 
-    Prod x a b -> do
+    Prod bt x a b -> do
       a' <- comp a
-      b' <- checkInContext [(x,Vr x)] $ comp b
-      return $ Prod x a' b'
+      b' <- checkInContext [(bt,x,Vr x)] $ comp b
+      return $ Prod bt x a' b'
 
-    Abs x b -> do
-      b' <- checkInContext [(x,Vr x)] $ comp b
-      return $ Abs x b'
+    Abs bt x b -> do
+      b' <- checkInContext [(bt,x,Vr x)] $ comp b
+      return $ Abs bt x b'
 
     ExtR r s -> do
       r' <- comp r
@@ -387,11 +387,11 @@ inferLType gr trm = case trm of
          (f',fty) <- infer f
          fty' <- comp fty
          case fty' of
-           Prod z arg val -> do 
+           Prod bt z arg val -> do 
              a' <- justCheck a arg
              ty <- if isWildIdent z 
                       then return val
-                      else substituteLType [(z,a')] val
+                      else substituteLType [(bt,z,a')] val
              return (App f' a',ty) 
            _ -> checkError (text "A function type is expected for" <+> ppTerm Unqualified 0 f <+> text "instead of type" <+> ppType env fty)
 
@@ -502,10 +502,10 @@ inferLType gr trm = case trm of
    Sort _     -> 
      termWith trm $ return typeType
 
-   Prod x a b -> do
+   Prod bt x a b -> do
      a' <- justCheck a typeType
-     b' <- checkInContext [(x,a')] $ justCheck b typeType
-     return (Prod x a' b', typeType)
+     b' <- checkInContext [(bt,x,a')] $ justCheck b typeType
+     return (Prod bt x a' b', typeType)
 
    Table p t  -> do
      p' <- justCheck p typeType --- check p partype! 
@@ -655,7 +655,7 @@ getOverload env@gr mt ot = case appForm ot of
    noProds vfs = [(v,f) | (v,f) <- vfs, noProd v]
 
    noProd ty = case ty of
-     Prod _ _ _ -> False
+     Prod _ _ _ _ -> False
      _ -> True
 
 checkLType :: SourceGrammar -> Term -> Type -> Check (Term, Type)
@@ -665,17 +665,17 @@ checkLType env trm typ0 = do
 
   case trm of
 
-    Abs x c -> do
+    Abs bt x c -> do
       case typ of
-        Prod z a b -> do 
-          checkUpdate (x,a)
+        Prod bt' z a b -> do 
+          checkUpdate (bt,x,a)
           (c',b') <- if isWildIdent z
                         then check c b
                         else do
-                          b' <- checkIn (text "abs") $ substituteLType [(z,Vr x)] b
+                          b' <- checkIn (text "abs") $ substituteLType [(bt',z,Vr x)] b
                           check c b'
           checkReset
-          return $ (Abs x c', Prod x a b')
+          return $ (Abs bt x c', Prod bt' x a b')
         _ -> checkError $ text "function type expected instead of" <+> ppType env typ
 
     App f a -> do
@@ -774,7 +774,7 @@ checkLType env trm typ0 = do
     Let (x,(mty,def)) body -> case mty of
       Just ty -> do
         (def',ty') <- check def ty
-        checkUpdate (x,ty')
+        checkUpdate (Explicit,x,ty')
         body' <- justCheck body typ
         checkReset
         return (Let (x,(Just ty',def')) body', typ)
@@ -827,14 +827,14 @@ checkLType env trm typ0 = do
 
 pattContext :: LTEnv -> Type -> Patt -> Check Context
 pattContext env typ p = case p of
-  PV x -> return [(x,typ)]
+  PV x -> return [(Explicit,x,typ)]
   PP q c ps | q /= cPredef -> do ---- why this /=? AR 6/1/2006
     t <- checkErr $ lookupResType cnc q c
     (cont,v) <- checkErr $ typeFormCnc t
     checkCond (text "wrong number of arguments for constructor in" <+> ppPatt Unqualified 0 p) 
               (length cont == length ps)
     checkEqLType env typ v (patt2term p)
-    mapM (uncurry (pattContext env)) (zip (map snd cont) ps) >>= return . concat
+    mapM (\((_,_,ty),p) -> pattContext env ty p) (zip cont ps) >>= return . concat
   PR r -> do
     typ' <- computeLType env typ
     case typ' of
@@ -849,12 +849,12 @@ pattContext env typ p = case p of
 
   PAs x p -> do
     g <- pattContext env typ p
-    return $ (x,typ):g
+    return $ (Explicit,x,typ):g
 
   PAlt p' q -> do
     g1 <- pattContext env typ p'
     g2 <- pattContext env typ q
-    let pts = nub ([fst pt | pt <- g1, notElem pt g2] ++ [fst pt | pt <- g2, notElem pt g1])
+    let pts = nub ([x | pt@(_,x,_) <- g1, notElem pt g2] ++ [x | pt@(_,x,_) <- g2, notElem pt g1])
     checkCond 
       (text "incompatible bindings of" <+>
        fsep (map ppIdent pts) <+> 
@@ -889,7 +889,7 @@ termWith t ct = do
 -- | light-weight substitution for dep. types
 substituteLType :: Context -> Type -> Check Type
 substituteLType g t = case t of
-  Vr x -> return $ maybe t id $ lookup x g
+  Vr x -> return $ maybe t id $ lookup x [(x,t) | (_,x,t) <- g]
   _ -> composOp (substituteLType g) t
 
 -- | compositional check\/infer of binary operations
@@ -933,7 +933,7 @@ checkIfEqLType env t u trm = do
      (_,u) | u == typeError -> True
 
      -- contravariance
-     (Prod x a b, Prod y c d) -> alpha g c a && alpha ((x,y):g) b d 
+     (Prod _ x a b, Prod _ y c d) -> alpha g c a && alpha ((x,y):g) b d 
                               
      -- record subtyping
      (RecType rs, RecType ts) -> all (\ (l,a) -> 
@@ -975,7 +975,7 @@ checkIfEqLType env t u trm = do
          _:_ -> Bad $ render (text "missing record fields:" <+> fsep (punctuate comma (map ppLabel others)))
          _ -> return locks
      -- contravariance
-     (Prod x a b, Prod y c d) -> do
+     (Prod _ x a b, Prod _ y c d) -> do
         ls1 <- missingLock g c a
         ls2 <- missingLock g b d
         return $ ls1 ++ ls2
@@ -989,11 +989,11 @@ checkIfEqLType env t u trm = do
 ppType :: LTEnv -> Type -> Doc
 ppType env ty =
   case ty of
-    RecType fs -> case filter isLockLabel $ map fst fs of
-                    [lock] -> text (drop 5 (showIdent (label2ident lock)))
-                    _      -> ppTerm Unqualified 0 ty
-    Prod x a b -> ppType env a <+> text "->" <+> ppType env b
-    _          -> ppTerm Unqualified 0 ty
+    RecType fs   -> case filter isLockLabel $ map fst fs of
+                      [lock] -> text (drop 5 (showIdent (label2ident lock)))
+                      _      -> ppTerm Unqualified 0 ty
+    Prod _ x a b -> ppType env a <+> text "->" <+> ppType env b
+    _            -> ppTerm Unqualified 0 ty
 
 -- | linearization types and defaults
 linTypeOfType :: SourceGrammar -> Ident -> Type -> Check (Context,Type)
@@ -1013,7 +1013,7 @@ linTypeOfType cnc m typ = do
                                       text "with" $$
                                       nest 2 (ppTerm Unqualified 0 val))) $
                              plusRecType vars val
-     return (symb,rec)
+     return (Explicit,symb,rec)
    lookLin (_,c) = checks [ --- rather: update with defLinType ?
       checkErr (lookupLincat cnc m c) >>= computeLType cnc
      ,return defLinType
@@ -1036,11 +1036,11 @@ allDependencies ism b =
     opty _ = []
     pts i = case i of
       ResOper pty pt -> [pty,pt]
-      ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,t) <- cont]
+      ResParam (Just (ps,_)) -> [Just t | (_,cont) <- ps, (_,_,t) <- cont]
       CncCat pty _ _ -> [pty]
       CncFun _   pt _ -> [pt]  ---- (Maybe (Ident,(Context,Type))
       AbsFun pty _ ptr -> [pty] --- ptr is def, which can be mutual
-      AbsCat (Just co) _ -> [Just ty | (_,ty) <- co]
+      AbsCat (Just co) _ -> [Just ty | (_,_,ty) <- co]
       _              -> []
 
 topoSortOpers :: [(Ident,[Ident])] -> Err [Ident]
diff --git a/src/GF/Compile/Compute.hs b/src/GF/Compile/Compute.hs
index f764acc52..f4bc61a5b 100644
--- a/src/GF/Compile/Compute.hs
+++ b/src/GF/Compile/Compute.hs
@@ -62,22 +62,22 @@ computeTermOpt rec gr = comput True where
          _ -> comp g t'
 
      -- Abs x@(IA _) b -> do 
-     Abs x b | full -> do 
+     Abs _ _ _ | full -> do 
        let (xs,b1) = termFormCnc t   
-       b' <- comp ([(x,Vr x) | x <- xs] ++ g) b1
+       b' <- comp ([(x,Vr x) | (_,x) <- xs] ++ g) b1
        return $ mkAbs xs b'
      --  b' <- comp (ext x (Vr x) g) b
      --  return $ Abs x b'
-     Abs _ _ -> return t -- hnf
+     Abs _ _ _ -> return t -- hnf
 
      Let (x,(_,a)) b -> do
        a' <- comp g a
        comp (ext x a' g) b
 
-     Prod x a b -> do
+     Prod b x a t -> do
        a' <- comp g a
-       b' <- comp (ext x (Vr x) g) b
-       return $ Prod x a' b'
+       t' <- comp (ext x (Vr x) g) t
+       return $ Prod b x a' t'
 
      -- beta-convert
      App f a -> case appForm t of
@@ -92,9 +92,9 @@ computeTermOpt rec gr = comput True where
             (t',b) <- appPredefined (mkApp h' as')
             if b then return t' else comp g t'
 
-          Abs _ _ -> do
+          Abs _ _ _ -> do
             let (xs,b) = termFormCnc h'
-            let g' = (zip xs as') ++ g
+            let g' = (zip (map snd xs) as') ++ g
             let as2 = drop (length xs) as'
             let xs2 = drop (length as') xs
             b' <- comp g' (mkAbs xs2 b)
@@ -234,11 +234,11 @@ computeTermOpt rec gr = comput True where
        f' <- hnf g f
        a' <- comp g a
        case (f',a') of
-         (Abs x b, FV as) -> 
+         (Abs _ x b, FV as) -> 
            mapM (\c -> comp (ext x c g) b) as >>= return . variants
          (_, FV as)  -> mapM (\c -> comp g (App f' c)) as >>= return . variants
          (FV fs, _)  -> mapM (\c -> comp g (App c a')) fs >>= return . variants
-         (Abs x b,_) -> comp (ext x a' g) b
+         (Abs _ x b,_) -> comp (ext x a' g) b
 
          (QC _ _,_)  -> returnC $ App f' a'
 
diff --git a/src/GF/Compile/GrammarToGFCC.hs b/src/GF/Compile/GrammarToGFCC.hs
index aa84f820c..18e262de7 100644
--- a/src/GF/Compile/GrammarToGFCC.hs
+++ b/src/GF/Compile/GrammarToGFCC.hs
@@ -119,6 +119,10 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
 i2i :: Ident -> CId
 i2i = CId . ident2bs
 
+b2b :: A.BindType -> C.BindType
+b2b A.Explicit = C.Explicit
+b2b A.Implicit = C.Implicit
+
 mkType :: [Ident] -> A.Type -> C.Type
 mkType scope t =
   case GM.typeForm t of
@@ -127,9 +131,9 @@ mkType scope t =
 
 mkExp :: [Ident] -> A.Term -> C.Expr
 mkExp scope t = case GM.termForm t of
-    Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
+    Ok (xs,c,args) -> mkAbs xs (mkApp (map snd (reverse xs)++scope) c (map (mkExp scope) args))
   where
-    mkAbs xs t = foldr (C.EAbs C.Explicit . i2i) t xs
+    mkAbs xs t = foldr (\(b,v) -> C.EAbs (b2b b) (i2i v)) t xs
     mkApp scope c args = case c of
       Q _ c    -> foldl C.EApp (C.EFun (i2i c)) args
       QC _ c   -> foldl C.EApp (C.EFun (i2i c)) args
@@ -154,10 +158,10 @@ mkPatt scope p =
 
 
 mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
-mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
-                                                   in if x == identW
-                                                        then (  scope,(C.Explicit,i2i x,ty'))
-                                                        else (x:scope,(C.Explicit,i2i x,ty'))) scope hyps 
+mkContext scope hyps = mapAccumL (\scope (bt,x,ty) -> let ty' = mkType scope ty
+                                                      in if x == identW
+                                                           then (  scope,(b2b bt,i2i x,ty'))
+                                                           else (x:scope,(b2b bt,i2i x,ty'))) scope hyps 
 
 mkTerm :: Term -> C.Term
 mkTerm tr = case tr of
@@ -179,7 +183,7 @@ mkTerm tr = case tr of
 -----  K (KP ss _) -> C.K (C.KP ss []) ---- TODO: prefix variants
   Empty    -> C.S []
   App _ _  -> prtTrace tr $ C.C 66661          ---- for debugging
-  Abs _ t  -> mkTerm t ---- only on toplevel
+  Abs _ _ t -> mkTerm t ---- only on toplevel
   Alts (td,tvs) -> 
     C.K (C.KP (strings td) [C.Alt (strings u) (strings v) | (u,v) <- tvs])
   _ -> prtTrace tr $ C.S [C.K (C.KS (render (A.ppTerm Unqualified 0 tr <+> int 66662)))] ---- for debugging
@@ -309,9 +313,9 @@ canon2canon opts abs cg0 =
       ResParam (Just (ps,v)) -> 
         ResParam (Just ([(c,concatMap unRec cont) | (c,cont) <- ps],Nothing))
       _ -> j
-  unRec (x,ty) = case ty of
-      RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (identW,typ)] 
-      _ -> [(x,ty)]
+  unRec (bt,x,ty) = case ty of
+      RecType fs -> [ity | (_,typ) <- fs, ity <- unRec (Explicit,identW,typ)] 
+      _ -> [(bt,x,ty)]
 
 ----
   trs v = traceD (render (tr v)) v
diff --git a/src/GF/Compile/Optimize.hs b/src/GF/Compile/Optimize.hs
index 9122b6e5f..e83f0e912 100644
--- a/src/GF/Compile/Optimize.hs
+++ b/src/GF/Compile/Optimize.hs
@@ -117,9 +117,9 @@ evalCncInfo opts gr cnc abs (c,info) = do
   CncCat ptyp pde ppr -> do
     pde' <- case (ptyp,pde) of
       (Just typ, Just de) -> 
-        liftM Just $ pEval ([(varStr, typeStr)], typ) de
+        liftM Just $ pEval ([(Explicit, varStr, typeStr)], typ) de
       (Just typ, Nothing) -> 
-        liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(varStr, typeStr)],typ)
+        liftM Just $ mkLinDefault gr typ >>= partEval noOptions gr ([(Explicit, varStr, typeStr)],typ)
       _ -> return pde   -- indirection
 
     ppr' <- liftM Just $ evalPrintname gr c ppr (Just $ K $ showIdent c)
@@ -142,7 +142,7 @@ evalCncInfo opts gr cnc abs (c,info) = do
 -- | the main function for compiling linearizations
 partEval :: Options -> SourceGrammar -> (Context,Type) -> Term -> Err Term
 partEval opts gr (context, val) trm = errIn (render (text "parteval" <+> ppTerm Qualified 0 trm)) $ do
-  let vars  = map fst context
+  let vars  = map (\(bt,x,t) -> x) context
       args  = map Vr vars
       subst = [(v, Vr v) | v <- vars]
       trm1 = mkApp trm args
@@ -150,7 +150,7 @@ partEval opts gr (context, val) trm = errIn (render (text "parteval" <+> ppTerm
   trm3 <- if rightType trm2
             then computeTerm gr subst trm2
             else recordExpand val trm2 >>= computeTerm gr subst
-  return $ mkAbs vars trm3
+  return $ mkAbs [(Explicit,v) | v <- vars] trm3
   where
     -- don't eta expand records of right length (correct by type checking)
     rightType (R rs) = case val of
@@ -178,8 +178,8 @@ recordExpand typ trm = case typ of
 mkLinDefault :: SourceGrammar -> Type -> Err Term
 mkLinDefault gr typ = do
   case typ of
-    RecType lts -> mapPairsM mkDefField lts >>= (return . Abs varStr . R . mkAssign)
-    _ -> liftM (Abs varStr) $ mkDefField typ
+    RecType lts -> mapPairsM mkDefField lts >>= (return . Abs Explicit varStr . R . mkAssign)
+    _ -> liftM (Abs Explicit varStr) $ mkDefField typ
 ----    _ -> prtBad "linearization type must be a record type, not" typ
  where
    mkDefField typ = case typ of
@@ -211,7 +211,7 @@ evalPrintname gr c ppr lin =
    comp = computeConcrete gr
 
    oneBranch t = case t of
-     Abs _ b   -> oneBranch b
+     Abs _ _ b -> oneBranch b
      R   (r:_) -> oneBranch $ snd $ snd r
      T _ (c:_) -> oneBranch $ snd c
      V _ (c:_) -> oneBranch c
diff --git a/src/GF/Compile/Refresh.hs b/src/GF/Compile/Refresh.hs
index ba6142ddd..04800fcce 100644
--- a/src/GF/Compile/Refresh.hs
+++ b/src/GF/Compile/Refresh.hs
@@ -37,13 +37,13 @@ refresh :: Term -> STM IdState Term
 refresh e = case e of
 
   Vr x    -> liftM  Vr  (lookVar x)
-  Abs x b -> liftM2 Abs (refVarPlus x)  (refresh b)
+  Abs b x t -> liftM2 (Abs b) (refVarPlus x)  (refresh t)
 
-  Prod x a b -> do
+  Prod b x a t -> do
     a'  <- refresh a
     x'  <- refVar  x
-    b'  <- refresh b
-    return $ Prod x' a' b'
+    t'  <- refresh t
+    return $ Prod b x' a' t'
 
   Let (x,(mt,a)) b -> do
     a'  <- refresh a
diff --git a/src/GF/Compile/Rename.hs b/src/GF/Compile/Rename.hs
index 8c563eeed..7d61e8a7d 100644
--- a/src/GF/Compile/Rename.hs
+++ b/src/GF/Compile/Rename.hs
@@ -178,8 +178,8 @@ renPerh ren Nothing  = return Nothing
 renameTerm :: Status -> [Ident] -> Term -> Err Term
 renameTerm env vars = ren vars where
   ren vs trm = case trm of
-    Abs x b    -> liftM  (Abs x) (ren (x:vs) b)
-    Prod x a b -> liftM2 (Prod x) (ren vs a) (ren (x:vs) b)
+    Abs b x t    -> liftM  (Abs b x) (ren (x:vs) t)
+    Prod bt x a b -> liftM2 (Prod bt x) (ren vs a) (ren (x:vs) b)
     Typed a b  -> liftM2 Typed (ren vs a) (ren vs b)
     Vr x      
       | elem x vs -> return trm
@@ -301,16 +301,16 @@ renameParam env (c,co) = do
 renameContext :: Status -> Context -> Err Context
 renameContext b = renc [] where
   renc vs cont = case cont of
-    (x,t) : xts 
+    (bt,x,t) : xts 
       | isWildIdent x -> do
           t'   <- ren vs t
           xts' <- renc vs xts
-          return $ (x,t') : xts'
+          return $ (bt,x,t') : xts'
       | otherwise -> do
           t'   <- ren vs t
           let vs' = x:vs
           xts' <- renc vs' xts
-          return $ (x,t') : xts'
+          return $ (bt,x,t') : xts'
     _ -> return cont
   ren = renameTerm b
 
diff --git a/src/GF/Compile/TC.hs b/src/GF/Compile/TC.hs
index 3999c223b..8cc2ff45b 100644
--- a/src/GF/Compile/TC.hs
+++ b/src/GF/Compile/TC.hs
@@ -77,7 +77,7 @@ whnf v = ---- errIn ("whnf" +++ prt v) $ ---- debug
 
 app :: Val -> Val -> Err Val
 app u v = case u of
-  VClos env (Abs x e) -> eval ((x,v):env) e
+  VClos env (Abs _ x e) -> eval ((x,v):env) e
   _ -> return $ VApp u v
   
 eval :: Env -> Exp -> Err Val
@@ -100,9 +100,9 @@ eqVal k u1 u2 = ---- errIn (prt u1 +++ "<>" +++ prBracket (show k) +++ prt u2) $
   let v = VGen k
   case (w1,w2) of
     (VApp f1 a1, VApp f2 a2) -> liftM2 (++) (eqVal k f1 f2) (eqVal k a1 a2)
-    (VClos env1 (Abs x1 e1), VClos env2 (Abs x2 e2)) ->
+    (VClos env1 (Abs _ x1 e1), VClos env2 (Abs _ x2 e2)) ->
       eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2)
-    (VClos env1 (Prod x1 a1 e1), VClos env2 (Prod x2 a2 e2)) ->
+    (VClos env1 (Prod _ x1 a1 e1), VClos env2 (Prod _ x2 a2 e2)) ->
       liftM2 (++) 
         (eqVal k     (VClos            env1  a1) (VClos            env2  a2))
         (eqVal (k+1) (VClos ((x1,v x1):env1) e1) (VClos ((x2,v x1):env2) e2))
@@ -123,15 +123,15 @@ checkExp th tenv@(k,rho,gamma) e ty = do
   case e of
     Meta m -> return $ (AMeta m typ,[])
 
-    Abs x t -> case typ of
-      VClos env (Prod y a b) -> do
+    Abs _ x t -> case typ of
+      VClos env (Prod _ y a b) -> do
 	a' <- whnf $ VClos env a ---
 	(t',cs) <- checkExp th 
                            (k+1,(x,v x):rho, (x,a'):gamma) t (VClos ((y,v x):env) b)
 	return (AAbs x a' t', cs)
       _ -> Bad (render (text "function type expected for" <+> ppTerm Unqualified 0 e <+> text "instead of" <+> ppValue Unqualified 0 typ))
 
-    Prod x a b -> do
+    Prod _ x a b -> do
       testErr (typ == vType) "expected Type"
       (a',csa) <- checkType th tenv a
       (b',csb) <- checkType th (k+1, (x,v x):rho, (x,VClos rho a):gamma) b
@@ -176,7 +176,7 @@ inferExp th tenv@(k,rho,gamma) e = case e of
     (f',w,csf) <- inferExp th tenv f 
     typ <- whnf w
     case typ of
-      VClos env (Prod x a b) -> do
+      VClos env (Prod _ x a b) -> do
         (a',csa) <- checkExp th tenv t (VClos env a)
 	b' <- whnf $ VClos ((x,VClos rho t):env) b
 	return $ (AApp f' a' b', b', csf ++ csa)
@@ -217,7 +217,7 @@ checkBranch th tenv b@(ps,t) ty = errIn ("branch" +++ show b) $
     p:ps2 -> do
       typ <- whnf ty
       case typ of
-        VClos env (Prod y a b) -> do
+        VClos env (Prod _ y a b) -> do
 	  a' <- whnf $ VClos env a
           (p', sigma, binds, cs1) <- checkP tenv p y a'
           let tenv' = (length binds, sigma ++ rho, binds ++ gamma)
@@ -275,7 +275,7 @@ checkPatt th tenv exp val = do
        (f',w,csf) <- checkExpP tenv f val
        typ <- whnf w
        case typ of
-         VClos env (Prod x a b) -> do
+         VClos env (Prod _ x a b) -> do
            (a',_,csa) <- checkExpP tenv t (VClos env a)
 	   b' <- whnf $ VClos ((x,VClos rho t):env) b
 	   return $ (AApp f' a' b', b', csf ++ csa)
diff --git a/src/GF/Grammar/AppPredefined.hs b/src/GF/Grammar/AppPredefined.hs
index 248445c0c..9e5b0d83a 100644
--- a/src/GF/Grammar/AppPredefined.hs
+++ b/src/GF/Grammar/AppPredefined.hs
@@ -50,11 +50,11 @@ typPredefined f
   | f == cPlus      = return $ mkFunType [typeInt,typeInt] (typeInt)
 ----  "read"   -> (P : Type) -> Tok -> P
   | f == cShow      = return $ mkProd -- (P : PType) -> P -> Tok
-    ([(varP,typePType),(identW,Vr varP)],typeStr,[]) 
+    ([(Explicit,varP,typePType),(Explicit,identW,Vr varP)],typeStr,[]) 
   | f == cToStr     = return $ mkProd -- (L : Type)  -> L -> Str
-    ([(varL,typeType),(identW,Vr varL)],typeStr,[]) 
+    ([(Explicit,varL,typeType),(Explicit,identW,Vr varL)],typeStr,[]) 
   | f == cMapStr    = return $ mkProd -- (L : Type)  -> (Str -> Str) -> L -> L
-    ([(varL,typeType),(identW,mkFunType [typeStr] typeStr),(identW,Vr varL)],Vr varL,[])
+    ([(Explicit,varL,typeType),(Explicit,identW,mkFunType [typeStr] typeStr),(Explicit,identW,Vr varL)],Vr varL,[])
   | f == cTake      = return $ mkFunType [typeInt,typeTok] typeTok
   | f == cTk        = return $ mkFunType [typeInt,typeTok] typeTok
   | otherwise       = Bad (render (text "unknown in Predef:" <+> ppIdent f))
diff --git a/src/GF/Grammar/Binary.hs b/src/GF/Grammar/Binary.hs
index 31e4ea222..e22e1dc87 100644
--- a/src/GF/Grammar/Binary.hs
+++ b/src/GF/Grammar/Binary.hs
@@ -109,6 +109,15 @@ instance Binary Info where
              8 -> get >>= \(x,y)   -> return (AnyInd x y)

              _ -> decodingError

 

+instance Binary BindType where

+  put Explicit = putWord8 0

+  put Implicit = putWord8 1

+  get = do tag <- getWord8

+           case tag of

+             0 -> return Explicit

+             1 -> return Implicit

+             _ -> decodingError

+

 instance Binary Term where

   put (Vr x)        = putWord8 0  >> put x

   put (Cn x)        = putWord8 1  >> put x

@@ -119,9 +128,9 @@ instance Binary Term where
   put (K x)         = putWord8 7  >> put x

   put (Empty)       = putWord8 8

   put (App x y)     = putWord8 9  >> put (x,y)

-  put (Abs x y)     = putWord8 10 >> put (x,y)

+  put (Abs x y z)   = putWord8 10 >> put (x,y,z)

   put (Meta x)      = putWord8 11 >> put x

-  put (Prod x y z)  = putWord8 12 >> put (x,y,z)

+  put (Prod w x y z)= putWord8 12 >> put (w,x,y,z)

   put (Typed x y)   = putWord8 14 >> put (x,y)

   put (Example x y) = putWord8 15 >> put (x,y)

   put (RecType x)   = putWord8 16 >> put x

@@ -159,9 +168,9 @@ instance Binary Term where
              7  -> get >>= \x       -> return (K x)

              8  ->                     return (Empty)

              9  -> get >>= \(x,y)   -> return (App x y)

-             10 -> get >>= \(x,y)   -> return (Abs x y)

+             10 -> get >>= \(x,y,z) -> return (Abs x y z)

              11 -> get >>= \x       -> return (Meta x)

-             12 -> get >>= \(x,y,z) -> return (Prod x y z)

+             12 -> get >>= \(w,x,y,z)->return (Prod w x y z)

              14 -> get >>= \(x,y)   -> return (Typed x y)

              15 -> get >>= \(x,y)   -> return (Example x y)

              16 -> get >>= \x       -> return (RecType x)

diff --git a/src/GF/Grammar/CF.hs b/src/GF/Grammar/CF.hs
index 5d88916cd..2a94bbfdb 100644
--- a/src/GF/Grammar/CF.hs
+++ b/src/GF/Grammar/CF.hs
@@ -112,8 +112,8 @@ cf2rule (fun, (cat, items)) = (def,ldef) where
   f     = identS fun
   def   = (f, AbsFun (Just (mkProd (args', Cn (identS cat), []))) Nothing Nothing)
   args0 = zip (map (identS . ("x" ++) . show) [0..]) items
-  args  = [(v, Cn (identS c)) | (v, Left c) <- args0]
-  args' = [(identS "_", Cn (identS c)) | (_, Left c) <- args0]
+  args  = [((Explicit,v), Cn (identS c)) | (v, Left c) <- args0]
+  args' = [(Explicit,identS "_", Cn (identS c)) | (_, Left c) <- args0]
   ldef  = (f, CncFun 
                Nothing 
                (Just (mkAbs (map fst args) 
diff --git a/src/GF/Grammar/Grammar.hs b/src/GF/Grammar/Grammar.hs
index 8cfc397af..d7af03f22 100644
--- a/src/GF/Grammar/Grammar.hs
+++ b/src/GF/Grammar/Grammar.hs
@@ -15,35 +15,36 @@
 -----------------------------------------------------------------------------
 
 module GF.Grammar.Grammar (SourceGrammar,
-                emptySourceGrammar,                
-		SourceModInfo,
-		SourceModule,
-                mapSourceModule,
-		Info(..),
-                PValues,
-		Type,
-		Cat,
-		Fun,
-		QIdent,
-		Term(..),
-		Patt(..),
-		TInfo(..),
-		Label(..),
-		MetaId,
-		Hypo,
-		Context,
-		Equation,
-		Labelling,
-		Assign,
-		Case,
-		Cases,
-		LocalDef,
-		Param,
-		Altern,
-		Substitution,
-		varLabel, tupleLabel, linLabel, theLinLabel,
-		ident2label, label2ident
-	       ) where
+        emptySourceGrammar,                
+        SourceModInfo,
+        SourceModule,
+        mapSourceModule,
+        Info(..),
+        PValues,
+        Type,
+        Cat,
+        Fun,
+        QIdent,
+        BindType(..),
+        Term(..),
+        Patt(..),
+        TInfo(..),
+        Label(..),
+        MetaId,
+        Hypo,
+        Context,
+        Equation,
+        Labelling,
+        Assign,
+        Case,
+        Cases,
+        LocalDef,
+        Param,
+        Altern,
+        Substitution,
+        varLabel, tupleLabel, linLabel, theLinLabel,
+        ident2label, label2ident
+        ) where
 
 import GF.Infra.Ident
 import GF.Infra.Option ---
@@ -103,57 +104,62 @@ type Fun  = QIdent
 
 type QIdent = (Ident,Ident)
 
+data BindType = 
+    Explicit
+  | Implicit
+  deriving (Eq,Ord,Show)
+
 data Term =
-   Vr Ident             -- ^ variable
- | Cn Ident             -- ^ constant
- | Con Ident            -- ^ constructor
- | Sort Ident           -- ^ basic type
- | EInt Integer         -- ^ integer literal
- | EFloat Double        -- ^ floating point literal
- | K String             -- ^ string literal or token: @\"foo\"@
- | Empty                -- ^ the empty string @[]@
-
- | App Term Term        -- ^ application: @f a@
- | Abs Ident Term       -- ^ abstraction: @\x -> b@
+   Vr Ident                      -- ^ variable
+ | Cn Ident                      -- ^ constant
+ | Con Ident                     -- ^ constructor
+ | Sort Ident                    -- ^ basic type
+ | EInt Integer                  -- ^ integer literal
+ | EFloat Double                 -- ^ floating point literal
+ | K String                      -- ^ string literal or token: @\"foo\"@
+ | Empty                         -- ^ the empty string @[]@
+
+ | App Term Term                 -- ^ application: @f a@
+ | Abs BindType Ident Term       -- ^ abstraction: @\x -> b@
  | Meta {-# UNPACK #-} !MetaId   -- ^ metavariable: @?i@ (only parsable: ? = ?0)
- | Prod Ident Term Term -- ^ function type: @(x : A) -> B@
- | Typed Term Term      -- ^ type-annotated term
+ | Prod BindType Ident Term Term -- ^ function type: @(x : A) -> B@, @A -> B@, @({x} : A) -> B@
+ | Typed Term Term               -- ^ type-annotated term
 --
 -- /below this, the constructors are only for concrete syntax/
- | Example Term String  -- ^ example-based term: @in M.C "foo"
- | RecType [Labelling]  -- ^ record type: @{ p : A ; ...}@
- | R [Assign]           -- ^ record:      @{ p = a ; ...}@
- | P Term Label         -- ^ projection:  @r.p@
- | PI Term Label Int    -- ^ index-annotated projection
- | ExtR Term Term       -- ^ extension:   @R ** {x : A}@ (both types and terms)
+ | Example Term String           -- ^ example-based term: @in M.C "foo"
+ | RecType [Labelling]           -- ^ record type: @{ p : A ; ...}@
+ | R [Assign]                    -- ^ record:      @{ p = a ; ...}@
+ | P Term Label                  -- ^ projection:  @r.p@
+ | PI Term Label Int             -- ^ index-annotated projection
+ | ExtR Term Term                -- ^ extension:   @R ** {x : A}@ (both types and terms)
  
- | Table Term Term      -- ^ table type:  @P => A@
- | T TInfo [Case]       -- ^ table:       @table {p => c ; ...}@
- | TSh TInfo [Cases]    -- ^ table with disjunctive patters (only back end opt)
- | V Type [Term]        -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
- | S Term Term          -- ^ selection:   @t ! p@
- | Val Term Type Int    -- ^ parameter value number: @T # i#
+ | Table Term Term               -- ^ table type:  @P => A@
+ | T TInfo [Case]                -- ^ table:       @table {p => c ; ...}@
+ | TSh TInfo [Cases]             -- ^ table with disjunctive patters (only back end opt)
+ | V Type [Term]                 -- ^ table given as course of values: @table T [c1 ; ... ; cn]@
+ | S Term Term                   -- ^ selection:   @t ! p@
+ | Val Term Type Int             -- ^ parameter value number: @T # i#
 
- | Let LocalDef Term    -- ^ local definition: @let {t : T = a} in b@
+ | Let LocalDef Term             -- ^ local definition: @let {t : T = a} in b@
 
- | Alias Ident Type Term  -- ^ constant and its definition, used in inlining
+ | Alias Ident Type Term         -- ^ constant and its definition, used in inlining
 
- | Q  Ident Ident        -- ^ qualified constant from a package
- | QC Ident Ident        -- ^ qualified constructor from a package
+ | Q  Ident Ident                -- ^ qualified constant from a package
+ | QC Ident Ident                -- ^ qualified constructor from a package
 
- | C Term Term    -- ^ concatenation: @s ++ t@
- | Glue Term Term -- ^ agglutination: @s + t@
+ | C Term Term                   -- ^ concatenation: @s ++ t@
+ | Glue Term Term                -- ^ agglutination: @s + t@
 
- | EPatt Patt     -- ^ pattern (in macro definition): # p
- | EPattType Term -- ^ pattern type: pattern T
+ | EPatt Patt                    -- ^ pattern (in macro definition): # p
+ | EPattType Term                -- ^ pattern type: pattern T
 
- | ELincat Ident Term -- ^ boxed linearization type of Ident
- | ELin Ident Term    -- ^ boxed linearization of type Ident
+ | ELincat Ident Term            -- ^ boxed linearization type of Ident
+ | ELin Ident Term               -- ^ boxed linearization of type Ident
 
- | FV [Term]      -- ^ alternatives in free variation: @variants { s ; ... }@
+ | FV [Term]                     -- ^ alternatives in free variation: @variants { s ; ... }@
 
- | Alts (Term, [(Term, Term)]) -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
- | Strs [Term]                 -- ^ conditioning prefix strings: @strs {s ; ...}@
+ | Alts (Term, [(Term, Term)])   -- ^ alternatives by prefix: @pre {t ; s\/c ; ...}@
+ | Strs [Term]                   -- ^ conditioning prefix strings: @strs {s ; ...}@
 
   deriving (Show, Eq, Ord)
 
@@ -200,8 +206,8 @@ data Label =
 
 type MetaId = Int
 
-type Hypo     = (Ident,Term)  -- (x:A)  (_:A)  A
-type Context  = [Hypo]        -- (x:A)(y:B)   (x,y:A)   (_,_:A)
+type Hypo     = (BindType,Ident,Term)   -- (x:A)  (_:A)  A  ({x}:A)
+type Context  = [Hypo]                  -- (x:A)(y:B)   (x,y:A)   (_,_:A)
 type Equation = ([Patt],Term) 
 
 type Labelling = (Label, Term) 
diff --git a/src/GF/Grammar/Lookup.hs b/src/GF/Grammar/Lookup.hs
index c0cbbe962..a85f54c90 100644
--- a/src/GF/Grammar/Lookup.hs
+++ b/src/GF/Grammar/Lookup.hs
@@ -137,7 +137,7 @@ lookupOverload gr m c = do
     case info of
       ResOverload os tysts -> do
             tss <- mapM (\x -> lookupOverload gr x c) os
-            return $ [(map snd args,(val,tr)) | 
+            return $ [(map (\(b,x,t) -> t) args,(val,tr)) | 
                       (ty,tr) <- tysts, Ok (args,val) <- [typeFormCnc ty]] ++ 
                      concat tss
 
@@ -173,7 +173,7 @@ lookupParamValues gr m c = do
     _ -> liftM concat $ mapM mkPar ps
  where
    mkPar (f,co) = do
-     vs <- liftM combinations $ mapM (\ (_,ty) -> allParamValues gr ty) co
+     vs <- liftM combinations $ mapM (\(_,_,ty) -> allParamValues gr ty) co
      return $ map (mkApp (QC m f)) vs
 
 lookupFirstTag :: SourceGrammar -> Ident -> Ident -> Err Term
diff --git a/src/GF/Grammar/MMacros.hs b/src/GF/Grammar/MMacros.hs
index 0a6c721ed..a0852421d 100644
--- a/src/GF/Grammar/MMacros.hs
+++ b/src/GF/Grammar/MMacros.hs
@@ -143,10 +143,10 @@ substTerm  :: [Ident] -> Substitution -> Term -> Term
 substTerm ss g c = case c of
   Vr x        -> maybe c id $ lookup x g
   App f a     -> App (substTerm ss g f) (substTerm ss g a)
-  Abs x b     -> let y = mkFreshVarX ss x in 
-                   Abs y (substTerm (y:ss) ((x, Vr y):g) b)
-  Prod x a b  -> let y = mkFreshVarX ss x in 
-                   Prod y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) b)
+  Abs b x t   -> let y = mkFreshVarX ss x in 
+                   Abs b y (substTerm (y:ss) ((x, Vr y):g) t)
+  Prod b x a t  -> let y = mkFreshVarX ss x in 
+                   Prod b y (substTerm ss g a) (substTerm (y:ss) ((x,Vr y):g) t)
   _           -> c
 
 metaSubstExp :: MetaSubst -> [(MetaId,Exp)]
@@ -204,64 +204,16 @@ mkProdVal :: Binds -> Val -> Err Val ---
 mkProdVal bs v = do 
   bs' <- mapPairsM val2exp bs
   v'  <- val2exp v
-  return $ vClos $ foldr (uncurry Prod) v' bs'
+  return $ vClos $ foldr (uncurry (Prod Explicit)) v' bs'
 
 freeVarsExp :: Exp -> [Ident]
 freeVarsExp e = case e of
   Vr x -> [x]
   App f c -> freeVarsExp f ++ freeVarsExp c
-  Abs x b -> filter (/=x) (freeVarsExp b)
-  Prod x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
+  Abs _ x b -> filter (/=x) (freeVarsExp b)
+  Prod _ x a b -> freeVarsExp a ++ filter (/=x) (freeVarsExp b)
   _ -> [] --- thus applies to abstract syntax only
 
-ident2string :: Ident -> String
-ident2string = showIdent
-{-
-tree :: (TrNode,[Tree]) -> Tree
-tree = Tr
-
-eqCat :: Cat -> Cat -> Bool
-eqCat = (==)
-
-addBinds :: Binds -> Tree -> Tree
-addBinds b (Tr (N (b0,at,t,c,x),ts)) = Tr (N (b ++ b0,at,t,c,x),ts)
-
-bodyTree :: Tree -> Tree
-bodyTree (Tr (N (_,a,t,c,x),ts)) = Tr (N ([],a,t,c,x),ts)
--}
-
-ref2exp :: [Var] -> Type -> Ref -> Err Exp
-ref2exp bounds typ ref = do
-  cont <- contextOfType typ
-  xx0  <- mapM (typeSkeleton . snd) cont
-  let (xxs,cs) = unzip [(length hs, c) | (hs,c) <- xx0]
-      args     = [mkAbs xs mExp | i <- xxs, let xs = mkFreshVars i bounds]
-  return $ mkApp ref args
-  -- no refreshment of metas
-  
--- | invariant: only 'Con' or 'Var'
-type Ref = Exp 
-
-fun2wrap :: [Var] -> ((Fun,Int),Type) -> Exp -> Err Exp
-fun2wrap oldvars ((fun,i),typ) exp = do
-  cont <- contextOfType typ
-  args <- mapM mkArg (zip [0..] (map snd cont))
-  return $ mkApp (qq fun) args
- where
-  mkArg (n,c) = do
-    cont <- contextOfType c
-    let vars = mkFreshVars (length cont) oldvars
-    return $ mkAbs vars $ if n==i then exp else mExp
-
--- | weak heuristics: sameness of value category
-compatType :: Val -> Type -> Bool
-compatType v t = errVal True $ do
-  cat1 <- val2cat v
-  cat2 <- valCat t
-  return $ cat1 == cat2
-
----
-
 mkJustProd :: Context -> Term -> Term
 mkJustProd cont typ = mkProd (cont,typ,[])
 
@@ -283,8 +235,8 @@ identVar _ = Bad "not a variable"
 qualifTerm :: Ident -> Term -> Term
 qualifTerm m  = qualif [] where
   qualif xs t = case t of
-    Abs x b -> let x' = chV x in Abs x' $ qualif (x':xs) b
-    Prod x a b -> Prod x (qualif xs a) $ qualif (x:xs) b
+    Abs b x t -> let x' = chV x in Abs b x' $ qualif (x':xs) t
+    Prod b x a t -> Prod b x (qualif xs a) $ qualif (x:xs) t
     Vr x -> let x' = chV x in if (elem x' xs) then (Vr x') else (Q m x) 
     Cn c  -> Q m c
     Con c -> QC m c
@@ -300,8 +252,8 @@ string2var s = case BS.unpack s of
 reindexTerm :: Term -> Term
 reindexTerm = qualif (0,[]) where
   qualif dg@(d,g) t = case t of
-    Abs x b    -> let x' = ind x d in Abs x' $ qualif (d+1, (x,x'):g) b
-    Prod x a b -> let x' = ind x d in Prod x' (qualif dg a) $ qualif (d+1, (x,x'):g) b
+    Abs b x t    -> let x' = ind x d in Abs b x' $ qualif (d+1, (x,x'):g) t
+    Prod b x a t -> let x' = ind x d in Prod b x' (qualif dg a) $ qualif (d+1, (x,x'):g) t
     Vr x       -> Vr $ look x g
     _ -> composSafeOp (qualif dg) t
   look x  = maybe x id . lookup x --- if x is not in scope it is unchanged
diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs
index 84a217b26..289531331 100644
--- a/src/GF/Grammar/Macros.hs
+++ b/src/GF/Grammar/Macros.hs
@@ -33,16 +33,16 @@ import Text.PrettyPrint
 
 firstTypeForm :: Type -> Err (Context, Type)
 firstTypeForm t = case t of
-  Prod x a b  -> do
-    (x', val) <- firstTypeForm b 
-    return ((x,a):x',val)
+  Prod b x a t  -> do
+    (x', val) <- firstTypeForm t
+    return ((b,x,a):x',val)
   _ -> return ([],t)
 
 qTypeForm :: Type -> Err (Context, Cat, [Term])
 qTypeForm t = case t of
-  Prod x a b  -> do
-    (x', cat, args) <- qTypeForm b 
-    return ((x,a):x', cat, args)
+  Prod b x a t  -> do
+    (x', cat, args) <- qTypeForm t
+    return ((b,x,a):x', cat, args)
   App c a -> do
     (_,cat, args) <- qTypeForm c
     return ([],cat,args ++ [a])
@@ -61,9 +61,9 @@ typeForm = qTypeForm ---- no need to distinguish any more
 
 typeFormCnc :: Type -> Err (Context, Type)
 typeFormCnc t = case t of
-  Prod x a b  -> do
-    (x', v) <- typeFormCnc b 
-    return ((x,a):x',v)
+  Prod b x a t  -> do
+    (x', v) <- typeFormCnc t
+    return ((b,x,a):x',v)
   _ -> return ([],t)
 
 valCat :: Type -> Err Cat
@@ -84,7 +84,7 @@ valTypeCnc typ =
 typeRawSkeleton :: Type -> Err ([(Int,Type)],Type)
 typeRawSkeleton typ =
   do (cont,typ) <- typeFormCnc typ
-     args <- mapM (typeRawSkeleton . snd) cont
+     args <- mapM (\(b,x,t) -> typeRawSkeleton t) cont
      return ([(length c, v) | (c,v) <- args], typ)
 
 type MCat = (Ident,Ident)
@@ -117,9 +117,9 @@ funsToAndFrom t = errVal undefined $ do ---
 
 typeFormConcrete :: Type -> Err (Context, Type)
 typeFormConcrete t = case t of
-  Prod x a b  -> do 
-    (x', typ) <- typeFormConcrete b 
-    return ((x,a):x', typ)
+  Prod b x a t  -> do 
+    (x', typ) <- typeFormConcrete t
+    return ((b,x,a):x', typ)
   _       -> return ([],t)
 
 isRecursiveType :: Type -> Bool
@@ -130,54 +130,49 @@ isRecursiveType t = errVal False $ do
 isHigherOrderType :: Type -> Bool
 isHigherOrderType t = errVal True $ do  -- pessimistic choice
   co <- contextOfType t
-  return $ not $ null [x | (x,Prod _ _ _) <- co]
+  return $ not $ null [x | (_,x,Prod _ _ _ _) <- co]
 
 contextOfType :: Type -> Err Context
 contextOfType typ = case typ of
-  Prod x a b -> liftM ((x,a):) $ contextOfType b
-  _ -> return [] 
+  Prod b x a t -> liftM ((b,x,a):) $ contextOfType t
+  _            -> return [] 
 
-termForm :: Term -> Err ([(Ident)], Term, [Term])
+termForm :: Term -> Err ([(BindType,Ident)], Term, [Term])
 termForm t = case t of
-   Abs x b  ->
-     do (x', fun, args) <- termForm b 
-        return (x:x', fun, args)
+   Abs b x t  ->
+     do (x', fun, args) <- termForm t
+        return ((b,x):x', fun, args)
    App c a ->
      do (_,fun, args) <- termForm c
         return ([],fun,args ++ [a]) 
    _       -> 
      return ([],t,[])
 
-termFormCnc :: Term -> ([(Ident)], Term)
+termFormCnc :: Term -> ([(BindType,Ident)], Term)
 termFormCnc t = case t of
-   Abs x b  -> (x:xs, t') where (xs,t') = termFormCnc b 
-   _        -> ([],t)
+   Abs b x t  -> ((b,x):xs, t') where (xs,t') = termFormCnc t
+   _          -> ([],t)
 
 appForm :: Term -> (Term, [Term])
 appForm t = case t of
   App c a -> (fun, args ++ [a]) where (fun, args) = appForm c
   _       -> (t,[])
 
-varsOfType :: Type -> [Ident]
-varsOfType t = case t of
-  Prod x _ b -> x : varsOfType b
-  _ -> []
-
 mkProdSimple :: Context -> Term -> Term
 mkProdSimple c t = mkProd (c,t,[])
 
 mkProd :: (Context, Term, [Term]) -> Term
-mkProd ([],typ,args) = mkApp typ args
-mkProd ((x,a):dd, typ, args) = Prod x a (mkProd (dd, typ, args))
+mkProd ([],         typ, args) = mkApp typ args
+mkProd ((b,x,a):dd, typ, args) = Prod b x a (mkProd (dd, typ, args))
 
-mkTerm :: ([(Ident)], Term, [Term]) -> Term
+mkTerm :: ([(BindType,Ident)], Term, [Term]) -> Term
 mkTerm (xx,t,aa) = mkAbs xx (mkApp t aa)
 
 mkApp :: Term -> [Term] -> Term
 mkApp = foldl App
 
-mkAbs :: [Ident] -> Term -> Term
-mkAbs xx t = foldr Abs t xx
+mkAbs :: [(BindType,Ident)] -> Term -> Term
+mkAbs xx t = foldr (uncurry Abs) t xx
 
 appCons :: Ident -> [Term] -> Term
 appCons = mkApp . Cn
@@ -186,7 +181,7 @@ mkLet :: [LocalDef] -> Term -> Term
 mkLet defs t = foldr Let t defs
 
 mkLetUntyped :: Context -> Term -> Term
-mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (x,t) <- defs]
+mkLetUntyped defs = mkLet [(x,(Nothing,t)) | (_,x,t) <- defs]
 
 isVariable :: Term -> Bool
 isVariable (Vr _ ) = True
@@ -272,12 +267,12 @@ mkSelects t tt = foldl S t tt
 mkTable :: [Term] -> Term -> Term
 mkTable tt t = foldr Table t tt
 
-mkCTable :: [Ident] -> Term -> Term
+mkCTable :: [(BindType,Ident)] -> Term -> Term
 mkCTable ids v = foldr ccase v ids where 
-  ccase x t = T TRaw [(PV x,t)]
+  ccase (_,x) t = T TRaw [(PV x,t)]
 
 mkHypo :: Term -> Hypo
-mkHypo typ = (identW, typ)
+mkHypo typ = (Explicit,identW, typ)
 
 eqStrIdent :: Ident -> Ident -> Bool
 eqStrIdent = (==)
@@ -298,7 +293,7 @@ mkWildCases :: Term -> Term
 mkWildCases = mkCases identW
 
 mkFunType :: [Type] -> Type -> Type
-mkFunType tt t = mkProd ([(identW, ty) | ty <- tt], t, []) -- nondep prod
+mkFunType tt t = mkProd ([(Explicit,identW, ty) | ty <- tt], t, []) -- nondep prod
 
 plusRecType :: Type -> Type -> Err Type
 plusRecType t1 t2 = case (t1, t2) of
@@ -510,13 +505,13 @@ composOp co trm =
      do c' <- co c
         a' <- co a
         return (App c' a')
-   Abs x b ->
-     do b' <- co b
-        return (Abs x b')
-   Prod x a b -> 
+   Abs b x t ->
+     do t' <- co t
+        return (Abs b x t')
+   Prod b x a t -> 
      do a' <- co a
-        b' <- co b
-        return (Prod x a' b')
+        t' <- co t
+        return (Prod b x a' t')
    S c a -> 
      do c' <- co c
         a' <- co a
@@ -618,25 +613,25 @@ changeTableType co i = case i of
 
 collectOp :: (Term -> [a]) -> Term -> [a]
 collectOp co trm = case trm of
-  App c a    -> co c ++ co a 
-  Abs _ b    -> co b
-  Prod _ a b -> co a ++ co b 
-  S c a      -> co c ++ co a
-  Table a c  -> co a ++ co c
-  ExtR a c   -> co a ++ co c
-  R r        -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r 
-  RecType r  -> concatMap (co . snd) r 
-  P t i      -> co t
-  T _ cc     -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
-  TSh _ cc   -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
-  V _ cc     -> concatMap co         cc --- nor from type annot
+  App c a      -> co c ++ co a 
+  Abs _ _ b    -> co b
+  Prod _ _ a b -> co a ++ co b 
+  S c a        -> co c ++ co a
+  Table a c    -> co a ++ co c
+  ExtR a c     -> co a ++ co c
+  R r          -> concatMap (\ (_,(mt,a)) -> maybe [] co mt ++ co a) r 
+  RecType r    -> concatMap (co . snd) r 
+  P t i        -> co t
+  T _ cc       -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
+  TSh _ cc     -> concatMap (co . snd) cc -- not from patterns --- nor from type annot
+  V _ cc       -> concatMap co         cc --- nor from type annot
   Let (x,(mt,a)) b -> maybe [] co mt ++ co a ++ co b
-  C s1 s2    -> co s1 ++ co s2 
-  Glue s1 s2 -> co s1 ++ co s2 
-  Alts (t,aa) -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
-  FV ts      -> concatMap co ts
-  Strs tt    -> concatMap co tt
-  _ -> [] -- covers K, Vr, Cn, Sort
+  C s1 s2      -> co s1 ++ co s2 
+  Glue s1 s2   -> co s1 ++ co s2 
+  Alts (t,aa)  -> let (x,y) = unzip aa in co t ++ concatMap co (x ++ y)
+  FV ts        -> concatMap co ts
+  Strs tt      -> concatMap co tt
+  _            -> [] -- covers K, Vr, Cn, Sort
 
 -- | to find the word items in a term
 wordsInTerm :: Term -> [String]
@@ -653,12 +648,6 @@ noExist = FV []
 defaultLinType :: Type
 defaultLinType = mkRecType linLabel [typeStr]
 
--- | from GF1, 20\/9\/2003
-isInOneType :: Type -> Bool
-isInOneType t = case t of
-  Prod _ a b -> a == b
-  _ -> False
-
 -- normalize records and record types; put s first
 
 sortRec :: [(Label,a)] -> [(Label,a)]
diff --git a/src/GF/Grammar/Parser.y b/src/GF/Grammar/Parser.y
index 76458209c..a6d9ca455 100644
--- a/src/GF/Grammar/Parser.y
+++ b/src/GF/Grammar/Parser.y
@@ -344,6 +344,11 @@ ListIdent
   : Ident               { [$1]    } 
   | Ident ',' ListIdent { $1 : $3 }
 
+ListIdent2 :: { [Ident] }
+ListIdent2 
+  : Ident               { [$1]    } 
+  | Ident ListIdent2    { $1 : $2 }
+
 Name :: { Ident }
 Name
   : Ident         { $1          } 
@@ -492,11 +497,6 @@ Patt2
   | '<' ListPattTupleComp '>' { (PR . tuple2recordPatt) $2 }
   | '(' Patt ')'              { $2 }
 
-Arg :: { Ident }
-Arg 
-  : '_'                       { identW }
-  | Ident                     { $1     }
-
 PattAss :: { [(Label,Patt)] }
 PattAss
   : ListIdent '=' Patt { [(LIdent (ident2bs i),$3) | i <- $1] } 
@@ -525,25 +525,32 @@ ListPatt
   : Patt2          { [$1]    } 
   | Patt2 ListPatt { $1 : $2 }
 
-ListArg :: { [Ident] }
+Arg :: { [(BindType,Ident)] }
+Arg 
+  : Ident               { [(Explicit,$1    )]      }
+  | '_'                 { [(Explicit,identW)]      }
+  | '{' ListIdent2 '}'  { [(Implicit,v) | v <- $2] }
+  
+ListArg :: { [(BindType,Ident)] }
 ListArg
-  : Arg         { [$1]    } 
-  | Arg ListArg { $1 : $2 }
+  : Arg                 { $1       } 
+  | Arg ListArg         { $1 ++ $2 }
 
-Bind :: { Ident }
+Bind :: { [(BindType,Ident)] }
 Bind
-  : Ident  { $1     } 
-  | '_'    { identW }
+  : Ident               { [(Explicit,$1    )]      } 
+  | '_'                 { [(Explicit,identW)]      }
+  | '{' ListIdent '}'   { [(Implicit,v) | v <- $2] }
 
-ListBind :: { [Ident] }
+ListBind :: { [(BindType,Ident)] }
 ListBind
-  : Bind              { [$1]    }
-  | Bind ',' ListBind { $1 : $3 }
+  : Bind                { $1       }
+  | Bind ',' ListBind   { $1 ++ $3 }
 
 Decl :: { [Hypo] }
 Decl
-  : '(' ListBind ':' Exp ')' { [(x,$4) | x <- $2] } 
-  | Exp4                     { [mkHypo $1]        }
+  : '(' ListBind ':' Exp ')' { [(b,x,$4) | (b,x) <- $2] } 
+  | Exp4                     { [mkHypo $1]              }
 
 ListTupleComp :: { [Term] }
 ListTupleComp
@@ -577,8 +584,8 @@ ListAltern
 
 DDecl :: { [Hypo] }
 DDecl
-  : '(' ListBind ':' Exp ')' { [(x,$4) | x <- $2] } 
-  | Exp6                     { [mkHypo $1]        }
+  : '(' ListBind ':' Exp ')' { [(b,x,$4) | (b,x) <- $2] } 
+  | Exp6                     { [mkHypo $1]              }
 
 ListDDecl :: { [Hypo] }
 ListDDecl
@@ -603,6 +610,7 @@ mkBaseId = prefixId (BS.pack "Base")
 prefixId :: BS.ByteString -> Ident -> Ident
 prefixId pref id = identC (BS.append pref (ident2bs id))
 
+listCatDef :: Ident -> SrcSpan -> Context -> Int -> [(Ident,SrcSpan,Info)]
 listCatDef id pos cont size = [catd,nilfund,consfund]
   where
     listId = mkListId id
@@ -613,8 +621,8 @@ listCatDef id pos cont size = [catd,nilfund,consfund]
     nilfund  = (baseId, pos, AbsFun (Just niltyp)  Nothing Nothing)
     consfund = (consId, pos, AbsFun (Just constyp) Nothing Nothing)
 
-    cont' = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont]
-    xs = map (Vr . fst) cont'
+    cont' = [(b,mkId x i,ty) | (i,(b,x,ty)) <- zip [0..] cont]
+    xs = map (\(b,x,t) -> Vr x) cont'
     cd = mkHypo (mkApp (Vr id) xs)
     lc = mkApp (Vr listId) xs
 
diff --git a/src/GF/Grammar/PatternMatch.hs b/src/GF/Grammar/PatternMatch.hs
index 0fb23f531..828a2e365 100644
--- a/src/GF/Grammar/PatternMatch.hs
+++ b/src/GF/Grammar/PatternMatch.hs
@@ -146,7 +146,7 @@ isInConstantForm trm = case trm of
     Con _    -> True
     Q _ _    -> True
     QC _ _   -> True
-    Abs _ _  -> True
+    Abs _ _ _ -> True
     C c a    -> isInConstantForm c && isInConstantForm a
     App c a  -> isInConstantForm c && isInConstantForm a
     R r      -> all (isInConstantForm . snd . snd) r
diff --git a/src/GF/Grammar/Printer.hs b/src/GF/Grammar/Printer.hs
index 6a09548cd..e0edadbec 100644
--- a/src/GF/Grammar/Printer.hs
+++ b/src/GF/Grammar/Printer.hs
@@ -116,16 +116,16 @@ ppJudgement q (id, CncCat  ptype pexp pprn) =
      Nothing  -> empty)

 ppJudgement q (id, CncFun  ptype pdef pprn) =

   (case pdef of

-     Just e  -> let (vs,e') = getAbs e

-              in text "lin" <+> ppIdent id <+> hsep (map ppIdent vs) <+> equals <+> ppTerm q 0 e' <+> semi

+     Just e  -> let (xs,e') = getAbs e

+              in text "lin" <+> ppIdent id <+> hsep (map ppBind xs) <+> equals <+> ppTerm q 0 e' <+> semi

      Nothing -> empty) $$

   (case pprn of

      Just prn -> text "printname" <+> text "fun" <+> ppIdent id <+> equals <+> ppTerm q 0 prn <+> semi

      Nothing  -> empty)

 ppJudgement q (id, AnyInd cann mid) = text "ind" <+> ppIdent id <+> equals <+> (if cann then text "canonical" else empty) <+> ppIdent mid <+> semi

 

-ppTerm q d (Abs v e)   = let (vs,e') = getAbs e

-                         in prec d 0 (char '\\' <> commaPunct ppIdent (v:vs) <+> text "->" <+> ppTerm q 0 e')

+ppTerm q d (Abs b v e)   = let (xs,e') = getAbs (Abs b v e)

+                           in prec d 0 (char '\\' <> commaPunct ppBind xs <+> text "->" <+> ppTerm q 0 e')

 ppTerm q d (T TRaw xs) = case getCTable (T TRaw xs) of

                            ([],_) -> text "table" <+> lbrace $$

 	  		             nest 2 (vcat (punctuate semi (map (ppCase q) xs))) $$

@@ -140,9 +140,9 @@ ppTerm q d (T (TComp  t) xs) = text "table" <+> ppTerm q 0 t <+> lbrace $$
 ppTerm q d (T (TWild  t) xs) = text "table" <+> ppTerm q 0 t <+> lbrace $$

 			       nest 2 (vcat (punctuate semi (map (ppCase q) xs))) $$

 			       rbrace

-ppTerm q d (Prod x a b)= if x == identW

-                           then prec d 0 (ppTerm q 4 a <+> text "->" <+> ppTerm q 0 b)

-                           else prec d 0 (parens (ppIdent x <+> colon <+> ppTerm q 0 a) <+> text "->" <+> ppTerm q 0 b)

+ppTerm q d (Prod bt x a b)= if x == identW && bt == Explicit

+                              then prec d 0 (ppTerm q 4 a <+> text "->" <+> ppTerm q 0 b)

+                              else prec d 0 (parens (ppBind (bt,x) <+> colon <+> ppTerm q 0 a) <+> text "->" <+> ppTerm q 0 b)

 ppTerm q d (Table kt vt)=prec d 0 (ppTerm q 3 kt <+> text "=>" <+> ppTerm q 0 vt)

 ppTerm q d (Let l e)    = let (ls,e') = getLet e

                           in prec d 0 (text "let" <+> vcat (map (ppLocDef q) (l:ls)) $$ text "in" <+> ppTerm q 0 e')

@@ -246,11 +246,11 @@ ppEnv e = hcat (map (\(x,t) -> braces (ppIdent x <> text ":=" <> ppValue Unquali
 

 str s = doubleQuotes (text s)

 

-ppDecl q (id,typ)

+ppDecl q (_,id,typ)

   | id == identW = ppTerm q 4 typ

   | otherwise    = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)

 

-ppDDecl q (id,typ)

+ppDDecl q (_,id,typ)

   | id == identW = ppTerm q 6 typ

   | otherwise    = parens (ppIdent id <+> colon <+> ppTerm q 0 typ)

 

@@ -272,6 +272,8 @@ ppLocDef q (id, (mbt, e)) =
   ppIdent id <+>

   (case mbt of {Just t -> colon  <+> ppTerm q 0 t; Nothing -> empty} <+> equals <+> ppTerm q 0 e) <+> semi

 

+ppBind (Explicit,v) = ppIdent v

+ppBind (Implicit,v) = braces (ppIdent v)

 

 ppAltern q (x,y) = ppTerm q 0 x <+> char '/' <+> ppTerm q 0 y

 

@@ -283,10 +285,10 @@ prec d1 d2 doc
   | d1 > d2   = parens doc

   | otherwise = doc

 

-getAbs :: Term -> ([Ident], Term)

-getAbs (Abs v e) = let (vs,e') = getAbs e

-                   in (v:vs,e')

-getAbs e         = ([],e)

+getAbs :: Term -> ([(BindType,Ident)], Term)

+getAbs (Abs bt v e) = let (xs,e') = getAbs e

+                      in ((bt,v):xs,e')

+getAbs e            = ([],e)

 

 getCTable :: Term -> ([Ident], Term)

 getCTable (T TRaw [(PV v,e)]) = let (vs,e') = getCTable e

diff --git a/src/GF/Grammar/Unify.hs b/src/GF/Grammar/Unify.hs
index 8ac5351e1..9bb49cfe2 100644
--- a/src/GF/Grammar/Unify.hs
+++ b/src/GF/Grammar/Unify.hs
@@ -60,8 +60,8 @@ unify e1 e2 g =
   (Q _ a, Q _ b) | (a == b)      -> return g ---- qualif?
   (QC _ a, QC _ b) | (a == b)    -> return g ----
   (Vr x, Vr y) | (x == y)        -> return g 
-  (Abs x b, Abs y c)               -> do let c' = substTerm [x] [(y,Vr x)] c 
-                                         unify b c' g
+  (Abs _ x b, Abs _ y c)         -> do let c' = substTerm [x] [(y,Vr x)] c 
+                                       unify b c' g
   (App c a, App d b)            -> case unify c d g of 
                                      Ok g1 -> unify a b g1 
                                      _     -> Bad (render (text "fail unify" <+> ppTerm Unqualified 0 e1))
@@ -92,6 +92,6 @@ occCheck :: MetaId -> Term -> Bool
 occCheck s u = case u of
     Meta v  -> s == v
     App c a -> occCheck s c || occCheck s a
-    Abs x b -> occCheck s b
+    Abs _ x b -> occCheck s b
     _       -> False
 
diff --git a/src/GF/Infra/CheckM.hs b/src/GF/Infra/CheckM.hs
index efa65118b..a556e5c3a 100644
--- a/src/GF/Infra/CheckM.hs
+++ b/src/GF/Infra/CheckM.hs
@@ -80,9 +80,9 @@ checkGetContext = Check (\ctxt msgs -> Success ctxt ctxt msgs)
 checkLookup :: Ident -> Check Type
 checkLookup x = do
   co <- checkGetContext
-  case lookup x co of
-    Nothing -> checkError (text "unknown variable" <+> ppIdent x)
-    Just ty -> return ty
+  case [ty | (b,y,ty) <- co, x == y] of
+    []     -> checkError (text "unknown variable" <+> ppIdent x)
+    (ty:_) -> return ty
 
 runCheck :: Check a -> Either [Message] (a,Context,[Message])
 runCheck c =