Node code compiling with debruijn-indexed terms

node/src/Main.hs

@@ -8,15 +8,13 @@ import Unison.Note as N
 import Unison.Syntax.Var as V
 
 identity :: E.Term
-identity = E.lam1 $ \x -> x
-
-(@) = E.App
+identity = E.unscope (E.lam E.var)
 
 constant :: E.Term
-constant = E.lam2 $ \x y -> x
+constant = E.unscope (E.lam (E.lam (E.weaken E.var)))
 
 apply :: E.Term
-apply = E.lam2 $ \f x -> f `E.App` x
+apply = E.unscope (E.lam (E.lam (E.weaken E.var `E.app` E.var)))
 
 -- type Any = forall r . (forall a . a -> r) -> r
 anyT :: Type

node/src/Unison/Edit/Term.hs

@@ -39,8 +39,7 @@ invalid loc ctx = "invalid path " ++ show loc ++ " in:\n" ++ show ctx
 -- todo: if the location references any free variables, make these
 -- function parameters of the
 abstract :: Applicative f => P.Path -> E.Term -> Noted f E.Term
-abstract loc ctx =
-  N.liftMaybe (invalid loc ctx) $ E.lam1 <$> P.set' loc ctx
+abstract loc ctx = N.failure "todo: Edit.Term.abstract"
 
 -- | Compute the allowed type of a replacement for a given subterm.
 -- Example, in @\g -> map g [1,2,3]@, @g@ has an admissible type of
@@ -55,11 +54,10 @@ admissibleTypeOf :: Applicative f
                  -> P.Path
                  -> E.Term
                  -> Noted f T.Type
-admissibleTypeOf synthLit loc ctx = case P.at' loc ctx of
+admissibleTypeOf synthLit loc ctx = case P.introduceAt1' loc E.app ctx of
   Nothing -> N.failure $ invalid loc ctx
-  Just (sub,replace) ->
-    let ctx = E.lam1 $ \f -> replace (f `E.App` sub)
-        go (T.Arrow (T.Arrow _ tsub) _) = tsub
+  Just ctx ->
+    let go (T.Arrow (T.Arrow _ tsub) _) = tsub
         go (T.Forall n t) = T.Forall n (go t)
         go _ = error "impossible, f had better be a function"
     in (T.gc . go) <$> synthesize synthLit ctx
@@ -96,31 +94,34 @@ eta loc ctx =
 -- This function returns a path to the floated subexpression (@42@ and @f x@ in
 -- the above examples.)
 letFloat :: Applicative f => P.Path -> E.Term -> Noted f (E.Term, P.Path)
-letFloat loc ctx = case P.at loc ctx of
-  Nothing  -> N.failure $ invalid loc ctx
-  Just sub ->
-    let
-      free = E.freeVars sub
-      minVar = if S.null free then Nothing else Just (S.findMin free)
-      trimmedPath = P.trimToV minVar loc
-      remainderPath = P.Path $ drop (length . P.elements $ trimmedPath) (P.elements loc)
-      letBody = do
-        body <- P.at trimmedPath ctx
-        E.lam1 <$> P.set' remainderPath body
-    in
-      N.liftMaybe (invalid loc ctx) $ do
-        body <- letBody
-        ctx' <- P.set trimmedPath (body `E.App` sub) ctx
-        loc' <- pure $ P.extend P.Arg trimmedPath
-        pure (ctx', loc')
+letFloat loc ctx = N.failure "Term.letFloat todo"
+
+--case P.at loc ctx of
+--  Nothing  -> N.failure $ invalid loc ctx
+--  Just sub ->
+--    let
+--      free = E.freeVars sub
+--      minVar = if S.null free then Nothing else Just (S.findMin free)
+--      trimmedPath = P.trimToV minVar loc
+--      remainderPath = P.Path $ drop (length . P.elements $ trimmedPath) (P.elements loc)
+--      letBody = do
+--        body <- P.at trimmedPath ctx
+--        E.lam1 <$> P.set' remainderPath body
+--    in
+--      N.liftMaybe (invalid loc ctx) $ do
+--        body <- letBody
+--        ctx' <- P.set trimmedPath (body `E.App` sub) ctx
+--        loc' <- pure $ P.extend P.Arg trimmedPath
+--        pure (ctx', loc')
 
 -- | Return the type of all local variables in scope at the given location
 locals :: Applicative f => T.Env f -> P.Path -> E.Term -> Noted f [(V.Var, T.Type)]
 locals synthLit path ctx | E.isClosed ctx =
-  N.scoped ("locals@"++show path ++ " " ++ show ctx) (filterInScope . pushDown <$> lambdaTypes)
+  N.scoped ("locals@"++show path ++ " " ++ show ctx)
+           (filterInScope . label . pushDown <$> lambdaTypes)
   where
     pointsToLambda path = case P.at path ctx of
-      Just (E.Lam _ _) -> True
+      Just (E.Lam _) -> True
       _ -> False
 
     lambdas :: [P.Path]
@@ -133,12 +134,16 @@ locals synthLit path ctx | E.isClosed ctx =
 
     -- not sure about this impl, or if it matters
     -- we prefer type information obtained higher in the syntax tree
-    pushDown :: [[(V.Var, T.Type)]] -> [(V.Var, T.Type)]
+    pushDown :: [[T.Type]] -> [T.Type]
     pushDown [] = []
     pushDown (env0 : tl) = env0 ++ pushDown (drop (length env0) tl)
 
-    extract :: E.Term -> T.Type -> [(V.Var, T.Type)]
-    extract (E.Lam n body) (T.Arrow i o) = (n, i) : extract body o
+    -- todo, not sure this is correct
+    label :: [T.Type] -> [(V.Var,T.Type)]
+    label ts = iterate V.succ V.bound1 `zip` reverse ts
+
+    extract :: E.Term -> T.Type -> [T.Type]
+    extract (E.Lam body) (T.Arrow i o) = i : extract body o
     extract ctx (T.Forall _ t) = extract ctx t
     extract _ _ = []
 
@@ -146,7 +151,7 @@ locals synthLit path ctx | E.isClosed ctx =
     filterInScope locals = filter (\(v,_) -> S.member v inScope) locals
       where inScope = S.fromList (P.inScopeAt path ctx)
 locals _ _ ctx =
-  N.failure $ "Term.locals: term contains free variables - " ++ show (E.freeVars ctx)
+  N.failure $ "Term.locals: term contains free variables - " ++ show ctx
 
 -- | Produce `e`, `e _`, `e _ _`, `e _ _ _` and so on,
 -- until the result is no longer a function type
@@ -163,20 +168,19 @@ applications e t = e : go e t
 -- and @map@ will have a type of @forall a b . (a -> b) -> [a] -> [b]@.
 typeOf :: Applicative f => T.Env f -> P.Path -> E.Term -> Noted f T.Type
 typeOf synthLit (P.Path []) ctx = N.scoped ("typeOf: " ++ show ctx) $ synthesize synthLit ctx
-typeOf synthLit loc ctx = N.scoped ("typeOf@"++show loc ++ " " ++ show ctx) $ case P.at' loc ctx of
-  Nothing -> N.failure $ invalid loc ctx
-  Just (sub,replace) ->
-    let sub' = sub
-        ctx = E.lam1 $ \f -> replace (ksub f)
-        -- we annotate `f` as returning `Number` so as not to introduce
-        -- any new quantified variables in the inferred type
-        -- copy the subtree so type is unconstrained by local usage
-        -- problem is that sub may contain variables that need freshening
-        ksub f = E.lam2 (\x _ -> x) `E.App` sub' `E.App` (f `E.App` sub `E.Ann` T.Unit T.Number)
-        go (T.Arrow (T.Arrow tsub _) _) = tsub
-        go (T.Forall n t) = T.Forall n (go t)
-        go _ = error "impossible, f had better be a function"
-    in (T.gc . go) <$> synthesize synthLit ctx
+typeOf synthLit loc ctx = N.scoped ("typeOf@"++show loc ++ " " ++ show ctx) $
+  case P.introduceAt1' loc replace ctx of
+    Nothing -> N.failure $ invalid loc ctx
+    Just ctx -> T.gc . extract <$> synthesize synthLit ctx
+  where
+    extract (T.Arrow (T.Arrow tsub _) _) = tsub
+    extract (T.Forall n t) = T.Forall n (extract t)
+    extract _ = error "impossible, f had better be a function"
+    k = E.lam (E.lam (E.weaken E.var)) -- `\x y -> x`, in debruijn notation
+    replace f focus =
+      -- annotate `f` as returning `Number` just so no new quantifiers are
+      -- introduced in the inferred type
+      k `E.app` focus `E.app` (f `E.app` focus `E.ann` T.Unit T.Number)
 
 -- | Evaluate the given location to weak head normal form.
 -- If the location contains any free variables, this noops.
@@ -188,5 +192,5 @@ whnf :: Applicative f
      -> Noted f E.Term
 whnf eval readTerm loc ctx = case P.at' loc ctx of
   Nothing -> N.failure $ invalid loc ctx
-  Just (sub,replace) | S.null (E.freeVars sub) -> replace <$> Eval.whnf eval readTerm sub
-  Just _             | otherwise               -> pure ctx
+  Just (sub,replace) | E.isClosed sub -> replace <$> Eval.whnf eval readTerm sub
+  Just _             | otherwise      -> pure ctx

node/src/Unison/Edit/Term/Eval/Interpreter.hs

@@ -20,7 +20,7 @@ data Primop f =
 eval :: (Applicative f, Monad f) => Map R.Reference (Primop f) -> Eval f
 eval env = Eval step whnf
   where
-    reduce e@(E.App (E.Lam _ _) _) args =
+    reduce e@(E.App (E.Lam _) _) args =
       return $ Just (foldl E.App (E.betaReduce e) args)
     reduce (E.App (E.Ref h) x) args = case M.lookup h env of
       Nothing -> return Nothing

node/src/Unison/Edit/Term/Path.hs

@@ -1,5 +1,6 @@
-{-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE TemplateHaskell #-}
 
 module Unison.Edit.Term.Path where
 
@@ -46,7 +47,7 @@ at (Path (h:t)) e = go h e where
   go Fn (E.App f _) = at (Path t) f
   go Arg (E.App _ x) = at (Path t) x
   go _ (E.Ann e' _) = at (Path (h:t)) e'
-  go Body (E.Lam _ body) = at (Path t) body
+  go Body (E.Lam body) = at (Path t) body
   go _ _ = Nothing
 
 along :: Path -> E.Term -> [E.Term]
@@ -54,29 +55,13 @@ along (Path path) e = go path e
   where go [] e = [e]
         go (Fn:path) e@(E.App f _) = e : go path f
         go (Arg:path) e@(E.App _ arg) = e : go path arg
-        go (Body:path) e@(E.Lam _ body) = e : go path body
+        go (Body:path) e@(E.Lam body) = e : go path body
         go (Index i:path) e@(E.Vector xs) = e : maybe [] (go path) (xs !? i)
         go _ _ = []
 
 valid :: Path -> E.Term -> Bool
 valid p e = maybe False (const True) (at p e)
 
--- | If the given @Path@ points to a valid subterm, we replace
--- that subterm @e@ with @v e@ and sequence the @Applicative@ effects
--- visit :: Path -> Traversal' E.Term E.Term
-visit :: Applicative f => Path -> (E.Term -> f E.Term) -> E.Term -> f E.Term
-visit (Path []) v e = v e
-visit (Path (h:t)) v e = go h e where
-  go Fn (E.App f arg) = E.App <$> visit (Path t) v f <*> pure arg
-  go Arg (E.App f arg) = E.App <$> pure f <*> visit (Path t) v arg
-  go _ (E.Ann e' typ) = E.Ann <$> visit (Path (h:t)) v e' <*> pure typ
-  go (Index i) e@(E.Vector xs) = let replace xi = E.Vector (xs // [(i,xi)])
-                                     sub = xs !? i
-                                 in maybe (pure e) (\sub -> replace <$> visit (Path t) v sub) sub
-  go Body (E.Lam n body) = fn <$> visit (Path t) v body
-    where fn body = E.lam1 $ \x -> E.betaReduce (E.Lam n body `E.App` x)
-  go _ e = pure e
-
 -- | Like 'at', but returns a function which may be used to modify the focus
 at' :: Path -> E.Term -> Maybe (E.Term, E.Term -> E.Term)
 at' loc ctx = case at loc ctx of
@@ -87,9 +72,10 @@ at' loc ctx = case at loc ctx of
 inScopeAt :: Path -> E.Term -> [V.Var]
 inScopeAt p e =
   let vars = map f (along p e)
-      f (E.Lam n _) = Just n
+      f (E.Lam _) = Just ()
       f _ = Nothing
-  in drop 1 (reverse vars) >>= toList
+      n = length (drop 1 (reverse vars) >>= toList)
+  in take n (iterate V.succ V.bound1)
 
 set :: Path -> E.Term -> E.Term -> Maybe E.Term
 set path focus ctx = impl path ctx where
@@ -102,7 +88,7 @@ set path focus ctx = impl path ctx where
     go Fn (E.App f arg) = E.App <$> impl (Path t) f <*> pure arg
     go Arg (E.App f arg) = E.App f <$> impl (Path t) arg
     go _ (E.Ann x _) = impl (Path (h:t)) x
-    go Body (E.Lam n body) = E.Lam n <$> impl (Path t) body
+    go Body (E.Lam body) = E.Lam <$> impl (Path t) body
     go _ _ = Nothing
 
 -- | Like 'set', but accepts the new focus within the returned @Maybe@.
@@ -114,6 +100,34 @@ modify loc f ctx = do
   x <- at loc ctx
   set loc (f x) ctx
 
+freeAt :: Path -> V.Var
+freeAt path =
+  let used = length [ Body | Body <- elements path ]
+      vars = iterate V.succ V.bound1
+  in head (drop used vars)
+
+-- | @introduceAt1 path (\var focus -> ...) ctx@ introduces a
+-- new free variable at the given path and makes some edit to
+-- the focus using this variable and the current focus.
+introduceAt1 :: Path
+             -> (forall e . E.Scoped e -> E.Scoped e -> E.Scoped e)
+             -> E.Scoped a
+             -> Maybe (E.Scoped (Maybe a))
+introduceAt1 path f ctx = do
+  focus <- E.Scoped <$> at path (E.unscope ctx)
+  focus' <- pure (f (E.Scoped (E.Var (freeAt path))) focus)
+  E.Scoped <$> set path (E.unscope focus') (E.unscope ctx)
+
+-- | Like @introduceAt1@, but takes raw terms, and returns a lambda term
+introduceAt1' :: Path
+             -> (forall e . E.Scoped e -> E.Scoped e -> E.Scoped e)
+             -> E.Term
+             -> Maybe E.Term
+introduceAt1' path f ctx = do
+  ctx' <- E.scoped ctx
+  body <- introduceAt1 path f ctx'
+  pure (E.unscope (E.lam body))
+
 -- | Drop from the right of this 'Path' until reaching the given element
 trimToR :: E -> Path -> Path
 trimToR e (Path p) = Path . reverse . dropWhile (/= e) . reverse $ p

node/src/Unison/Syntax/Term.hs

@@ -7,12 +7,9 @@
 module Unison.Syntax.Term where
 
 import qualified Data.Foldable as Foldable
-import Data.Maybe
 import Data.Traversable
-import Data.List as List
 import Control.Applicative
 import Control.Lens.TH
-import Control.Monad
 import Control.Monad.Writer
 import Data.Aeson.TH
 import qualified Data.Aeson.Encode as JE
@@ -42,7 +39,7 @@ data Term
   | App Term Term
   | Ann Term T.Type
   | Vector (V.Vector Term)
-  | Lam V.Var Term
+  | Lam Term
   deriving (Eq,Ord)
 
 instance Show Term where
@@ -54,37 +51,12 @@ instance Show Term where
   show (App f x@(App _ _)) = show f ++ " (" ++ show x ++ ")"
   show (App f x) = show f ++ " " ++ show x
   show (Ann x t) = "(" ++ show x ++ " : " ++ show t ++ ")"
-  show lam@(Lam _ _) = "(" ++ List.intercalate " " (map show vs) ++ " → " ++ show inner ++ ")"
+  show lam@(Lam _) = "(λ. " ++ show inner ++ ")"
     where
-      (vs,inner) = go lam
+      inner = go lam
       go v = case v of
-        Lam n body -> let (vs,inner) = go body in (Var n : vs, inner)
-        _ -> ([], v)
-
-maxV :: Term -> V.Var
-maxV (App f x) = maxV f `max` maxV x
-maxV (Ann x _) = maxV x
-maxV (Lam n _) = n
-maxV (Vector v) | not (V.null v) = Foldable.foldl max (V.decr V.bound1) (fmap maxV v)
-maxV _         = V.decr V.bound1
-
-lam1M :: Monad f => (Term -> f Term) -> f Term
-lam1M f = return Lam `ap` n `ap` body
-  where
-    n               = liftM (V.succ . maxV) body
-    body            = f =<< (liftM Var n)
-
-lam1 :: (Term -> Term) -> Term
-lam1 f = Lam n body
-  where
-    n = V.succ (maxV body)
-    body = f (Var n)
-
-lam2 :: (Term -> Term -> Term) -> Term
-lam2 f = lam1 $ \x -> lam1 $ \y -> f x y
-
-lam3 :: (Term -> Term -> Term -> Term) -> Term
-lam3 f = lam1 $ \x -> lam1 $ \y -> lam1 $ \z -> f x y z
+        Lam body -> go body
+        _ -> v
 
 -- | Convert all 'Ref' constructors to the corresponding term
 link :: (Applicative f, Monad f) => (H.Hash -> f Term) -> Term -> f Term
@@ -97,8 +69,7 @@ link env e = case e of
     e | otherwise -> link env e
   App fn arg -> App <$> link env fn <*> link env arg
   Vector vs -> Vector <$> traverse (link env) vs
-  Lam n body -> go <$> link env body
-    where go body = lam1 $ \x -> betaReduce (Lam n body `App` x)
+  Lam body -> Lam <$> link env body
   _ -> pure e
 
 dependencies :: Term -> S.Set H.Hash
@@ -111,8 +82,22 @@ dependencies e = case e of
   App fn arg -> dependencies fn `S.union` dependencies arg
   Ann e _ -> dependencies e
   Vector vs -> Foldable.foldMap dependencies vs
-  Lam _ body -> dependencies body
+  Lam body -> dependencies body
 
+isClosed :: Term -> Bool
+isClosed e = go V.bound1 e
+  where
+    go depth e = case e of
+      Lit _ -> True
+      Ref _ -> True
+      Blank -> True
+      Var v -> v < depth
+      App f arg -> go depth f && go depth arg
+      Ann e _ -> go depth e
+      Vector vs -> Foldable.all (go depth) vs
+      Lam body -> go (V.succ depth) body
+
+{-
 freeVars :: Term -> S.Set V.Var
 freeVars e = case e of
   Var v -> S.singleton v
@@ -121,22 +106,38 @@ freeVars e = case e of
   Lam n body -> S.delete n (freeVars body)
   Vector vs -> Foldable.foldMap freeVars vs
   _ -> S.empty
+-}
 
-substitute :: (V.Var -> Maybe Term) -> Term -> Term
-substitute env e = go S.empty e where
-  go bound e = case e of
-    Var v -> if S.member v bound then e else fromMaybe e (env v)
-    App fn arg -> App (go bound fn) (go bound arg)
-    Vector vs -> Vector (fmap (go bound) vs)
-    Lam n body -> Lam n (go (S.insert n bound) body)
-    _ -> e
+newtype Scoped a = Scoped { unscope :: Term }
 
-weaken :: V.Var -> Term -> Term
-weaken v e = substitute (\v' -> Just (Var (V.nest v v'))) e
+scoped :: Term -> Maybe (Scoped a)
+scoped e | isClosed e = Just (Scoped e)
+scoped _ = Nothing
 
-isClosed :: Term -> Bool
-isClosed e | S.null (freeVars e) = True
-isClosed _ = False
+lam :: Scoped (Maybe a) -> Scoped a
+lam (Scoped body) = Scoped (Lam body)
+
+var :: Scoped (Maybe a)
+var = Scoped (Var V.bound1)
+
+app :: Scoped a -> Scoped a -> Scoped a
+app (Scoped f) (Scoped arg) = Scoped (f `App` arg)
+
+ann :: Scoped a -> T.Type -> Scoped a
+ann (Scoped e) t = Scoped (e `Ann` t)
+
+weaken :: Scoped a -> Scoped (Maybe a)
+weaken (Scoped s) = Scoped (go V.bound1 s)
+  where
+    go depth e = case e of
+      Lit _ -> e
+      Ref _ -> e
+      Blank -> e
+      Var v -> if v >= depth then Var (V.succ v) else e
+      App f arg -> App (go depth f) (go depth arg)
+      Ann e t -> Ann (go depth e) t
+      Vector vs -> Vector (fmap (go depth) vs)
+      Lam body -> Lam (go (V.succ depth) body)
 
 stripAnn :: Term -> (Term, Term -> Term)
 stripAnn (Ann e t) = (e, \e' -> Ann e' t)
@@ -150,27 +151,25 @@ arguments _ = []
 -- | If the outermost term is a function application,
 -- perform substitution of the argument into the body
 betaReduce :: Term -> Term
-betaReduce (App (Lam var f) arg) = go f where
-  go :: Term -> Term
-  go body = case body of
-    App f x -> App (go f) (go x)
-    Vector vs -> Vector (fmap go vs)
-    Ann body t -> Ann (go body) t
-    Lam n body | n == var  -> Lam n body -- this lambda shadows var; avoid substituting
-               | otherwise -> Lam n (go body)
-    Var v | v == var -> arg
+betaReduce (App (Lam f) arg) = go V.bound1 f where
+  go depth body = case body of
+    App f x -> App (go depth f) (go depth x)
+    Vector vs -> Vector (fmap (go depth) vs)
+    Ann body t -> Ann (go depth body) t
+    Lam body -> Lam (go (V.succ depth) body)
+    Var v | v == depth -> arg
     _ -> body
 betaReduce e = e
 
 -- | If the outermost term is a lambda of the form @\x -> f x@,
 -- reduce this to @f@.
 etaReduce :: Term -> Term
-etaReduce (Lam n (App f n')) | Var n == n' = f
+etaReduce (Lam (App f (Var v))) | v == V.bound1 = f
 etaReduce e = e
 
--- | Repeatedly apply eta reduction until reaching fixed point
+-- | Repeatedly apply @etaReduce@ until reaching fixed point.
 etaNormalForm :: Term -> Term
-etaNormalForm (Lam n (App f n')) | Var n == n' = etaNormalForm f
+etaNormalForm (Lam (App f (Var v))) | v == V.bound1 = etaNormalForm f
 etaNormalForm e = e
 
 applyN :: Term -> [Term] -> Term
@@ -219,8 +218,7 @@ hashCons e = let (e', hs) = runWriter (go e) in finalize e' hs
       r@(Ref _) -> pure r
       v@(Var _) -> pure v
       Blank     -> pure Blank
-      Lam n body -> go body >>=
-        \body -> save (lam1 $ \x -> betaReduce (Lam n body `App` x))
+      Lam body -> go body >>= (\body -> save (Lam body))
       Ann e t   -> save =<< (Ann <$> go e <*> pure t)
       App f x   -> save =<< (App <$> go f <*> go x)
       Vector vs  -> save =<< (Vector <$> traverse go vs)

node/src/Unison/Type/Context.hs

@@ -279,7 +279,7 @@ check ctx e t | wellformedType ctx t = scope (show e ++ " : " ++ show t) $ go e
     let (x', ctx') = extendUniversal ctx
     in check ctx' e (T.subst body x (T.Universal x'))
        >>= retract (E.Universal x')
-  go fn@(Term.Lam _ _) (T.Arrow i o) = -- =>I
+  go fn@(Term.Lam _) (T.Arrow i o) = -- =>I
     let x' = fresh ctx
         v = Term.Var x'
         ctx' = extend (E.Ann x' i) ctx
@@ -314,7 +314,7 @@ synthesize ctx e = scope ("infer: " ++ show e) $ go e where
   go (Term.App f arg) = do -- ->E
     (ft, ctx') <- synthesize ctx f
     synthesizeApp ctx' (apply ctx' ft) arg
-  go fn@(Term.Lam _ _) = -- ->I=> (Full Damas Milner rule)
+  go fn@(Term.Lam _) = -- ->I=> (Full Damas Milner rule)
     let (arg, i, o) = fresh3 ctx
         ctxTl = context [E.Marker i, E.Existential i, E.Existential o,
                          E.Ann arg (T.Existential i)]
@@ -363,6 +363,6 @@ synthesizeClosed synthRef term = Noted $ synth <$> N.unnote (annotate term)
       Term.Ref h -> Term.Ann (Term.Ref h) <$> synthRef h
       Term.App f arg -> Term.App <$> annotate f <*> annotate arg
       Term.Ann body t -> Term.Ann <$> annotate body <*> pure t
-      Term.Lam n body -> Term.Lam n <$> annotate body
+      Term.Lam body -> Term.Lam <$> annotate body
       Term.Vector terms -> Term.Vector <$> traverse annotate terms
       _ -> pure term'