diff --git a/src/Juvix/Compiler/Asm/Translation/FromCore.hs b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
index 6c03bdaf3d..9feb9c3536 100644
--- a/src/Juvix/Compiler/Asm/Translation/FromCore.hs
+++ b/src/Juvix/Compiler/Asm/Translation/FromCore.hs
@@ -162,7 +162,7 @@ genCode infoTable fi =
     goLet :: Bool -> Int -> BinderList Value -> Core.Let -> Code'
     goLet isTail tempSize refs (Core.Let {..}) =
       DL.append
-        (DL.snoc (go False tempSize refs _letValue) (mkInstr PushTemp))
+        (DL.snoc (go False tempSize refs (_letItem ^. Core.letItemValue)) (mkInstr PushTemp))
         (snocPopTemp isTail $ go isTail (tempSize + 1) (BL.extend (Ref (DRef (TempRef tempSize))) refs) _letBody)
 
     goCase :: Bool -> Int -> BinderList Value -> Core.Case -> Code'
diff --git a/src/Juvix/Compiler/Core/Evaluator.hs b/src/Juvix/Compiler/Core/Evaluator.hs
index 0e2e9e1fca..8aaf05876e 100644
--- a/src/Juvix/Compiler/Core/Evaluator.hs
+++ b/src/Juvix/Compiler/Core/Evaluator.hs
@@ -60,14 +60,14 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
       NCst {} -> n
       NApp (App i l r) ->
         case eval' env l of
-          Closure env' (Lambda _ b) -> let !v = eval' env r in eval' (v : env') b
+          Closure env' (Lambda _ _ b) -> let !v = eval' env r in eval' (v : env') b
           v -> evalError "invalid application" (mkApp i v (substEnv env r))
       NBlt (BuiltinApp _ op args) -> applyBuiltin n env op args
       NCtr (Constr i tag args) -> mkConstr i tag (map' (eval' env) args)
       NLam l@Lambda {} -> Closure env l
-      NLet (Let _ v b) -> let !v' = eval' env v in eval' (v' : env) b
+      NLet (Let _ (LetItem _ v) b) -> let !v' = eval' env v in eval' (v' : env) b
       NRec (LetRec _ vs b) ->
-        let !vs' = map (eval' env') (toList vs)
+        let !vs' = map (eval' env' . (^. letItemValue)) (toList vs)
             !env' = revAppend vs' env
          in foldr GHC.pseq (eval' env' b) vs'
       NCase (Case i v bs def) ->
@@ -86,7 +86,7 @@ eval !ctx !env0 = convertRuntimeNodes . eval' env0
 
     branch :: Node -> Env -> [Node] -> Tag -> Maybe Node -> [CaseBranch] -> Node
     branch n !env !args !tag !def = \case
-      (CaseBranch _ tag' _ b) : _ | tag' == tag -> eval' (revAppend args env) b
+      (CaseBranch _ tag' _ _ b) : _ | tag' == tag -> eval' (revAppend args env) b
       _ : bs' -> branch n env args tag def bs'
       [] -> case def of
         Just b -> eval' env b
diff --git a/src/Juvix/Compiler/Core/Extra.hs b/src/Juvix/Compiler/Core/Extra.hs
index 63adb5fff2..536bfb7a04 100644
--- a/src/Juvix/Compiler/Core/Extra.hs
+++ b/src/Juvix/Compiler/Core/Extra.hs
@@ -80,7 +80,7 @@ cosmos f = ufoldA reassemble f
 -- binder of the variable.
 -- if fv = x1, x2, .., xn
 -- the result is of the form λx1 λx2 .. λ xn b
-captureFreeVars :: [(Index, Info)] -> Node -> Node
+captureFreeVars :: [(Index, Binder)] -> Node -> Node
 captureFreeVars fv
   | n == 0 = id
   | otherwise = mkLambdasB infos . mapFreeVars
@@ -116,7 +116,7 @@ developBeta = umap go
   where
     go :: Node -> Node
     go n = case n of
-      NApp (App _ (NLam (Lambda _ body)) arg) -> subst arg body
+      NApp (App _ (NLam (Lambda {..})) arg) -> subst arg _lambdaBody
       _ -> n
 
 etaExpand :: Int -> Node -> Node
@@ -138,12 +138,21 @@ convertClosures = umap go
   where
     go :: Node -> Node
     go n = case n of
-      Closure env (Lambda i b) -> substEnv env (mkLambda i b)
+      Closure env (Lambda i bi b) -> substEnv env (mkLambda i bi b)
       _ -> n
 
 convertRuntimeNodes :: Node -> Node
 convertRuntimeNodes = convertClosures
 
+argumentInfoFromBinder :: Binder -> ArgumentInfo
+argumentInfoFromBinder i =
+  ArgumentInfo
+    { _argumentName = i ^. binderName,
+      _argumentType = i ^. binderType,
+      _argumentIsImplicit = Explicit
+    }
+
+-- TODO remove ?
 argumentInfoFromInfo :: Info -> ArgumentInfo
 argumentInfoFromInfo i =
   ArgumentInfo
diff --git a/src/Juvix/Compiler/Core/Extra/Base.hs b/src/Juvix/Compiler/Core/Extra/Base.hs
index aa10b6e6a5..036c5bec41 100644
--- a/src/Juvix/Compiler/Core/Extra/Base.hs
+++ b/src/Juvix/Compiler/Core/Extra/Base.hs
@@ -2,7 +2,6 @@ module Juvix.Compiler.Core.Extra.Base where
 
 import Data.Functor.Identity
 import Data.List qualified as List
-import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Core.Info qualified as Info
 import Juvix.Compiler.Core.Language
 
@@ -45,23 +44,30 @@ mkConstr i tag args = NCtr (Constr i tag args)
 mkConstr' :: Tag -> [Node] -> Node
 mkConstr' = mkConstr Info.empty
 
+-- TODO remove
+mkLambdaOld :: Info -> Node -> Node
+mkLambdaOld i b = NLam (Lambda i emptyBinder b)
+
 mkLambda :: Info -> Binder -> Node -> Node
 mkLambda i bi b = NLam (Lambda i bi b)
 
 mkLambda' :: Node -> Node
 mkLambda' = mkLambda Info.empty emptyBinder
 
+mkLetItem' :: Node -> LetItem
+mkLetItem' = LetItem emptyBinder
+
 mkLet :: Info -> Binder -> Node -> Node -> Node
-mkLet i bi v b = NLet (Let i bi v b)
+mkLet i bi v b = NLet (Let i (LetItem bi v) b)
 
 mkLet' :: Node -> Node -> Node
 mkLet' = mkLet Info.empty emptyBinder
 
-mkLetRec :: Info -> NonEmpty (Binder, Node) -> Node -> Node
+mkLetRec :: Info -> NonEmpty LetItem -> Node -> Node
 mkLetRec i vs b = NRec (LetRec i vs b)
 
 mkLetRec' :: NonEmpty Node -> Node -> Node
-mkLetRec' = mkLetRec Info.empty . NonEmpty.zip (NonEmpty.repeat emptyBinder)
+mkLetRec' = mkLetRec Info.empty . fmap mkLetItem'
 
 mkCase :: Info -> Node -> [CaseBranch] -> Maybe Node -> Node
 mkCase i v bs def = NCase (Case i v bs def)
@@ -76,7 +82,16 @@ mkMatch' :: NonEmpty Node -> [MatchBranch] -> Node
 mkMatch' = mkMatch Info.empty
 
 mkIf :: Info -> Node -> Node -> Node -> Node
-mkIf i v b1 b2 = mkCase i v [CaseBranch Info.empty (BuiltinTag TagTrue) 0 b1] (Just b2)
+mkIf i v b1 b2 = mkCase i v [br] (Just b2)
+  where
+    br =
+      CaseBranch
+        { _caseBranchInfo = mempty,
+          _caseBranchTag = BuiltinTag TagTrue,
+          _caseBranchBinders = [],
+          _caseBranchBindersNum = 0,
+          _caseBranchBody = b1
+        }
 
 mkIf' :: Node -> Node -> Node -> Node
 mkIf' = mkIf Info.empty
@@ -84,14 +99,20 @@ mkIf' = mkIf Info.empty
 {------------------------------------------------------------------------}
 {- Type constructors -}
 
-mkPi :: Info -> Type -> Type -> Type
-mkPi i ty b = NPi (Pi i ty b)
+mkPi :: Info -> Binder -> Type -> Type
+mkPi i bi b = NPi (Pi i bi b)
 
 mkPi' :: Type -> Type -> Type
-mkPi' = mkPi Info.empty
+mkPi' = mkPi Info.empty . Binder Nothing
 
-mkPis :: [(Info, Type)] -> Type -> Type
-mkPis tys ty = foldr (uncurry mkPi) ty tys
+mkPis :: [Binder] -> Type -> Type
+mkPis tys ty = foldr (mkPi mempty) ty tys
+
+rePi :: PiLhs -> Type -> Type
+rePi PiLhs {..} = mkPi _piLhsInfo _piLhsBinder
+
+rePis :: [PiLhs] -> Type -> Type
+rePis tys ty = foldr rePi ty tys
 
 mkPis' :: [Type] -> Type -> Type
 mkPis' tys ty = foldr mkPi' ty tys
@@ -142,16 +163,18 @@ mkDynamic' = mkDynamic Info.empty
 {- functions on Type -}
 
 -- | Unfold a type into the target and the arguments (left-to-right)
-unfoldType :: Type -> (Type, [(Info, Type)])
-unfoldType ty = case ty of
-  NPi (Pi i l r) -> let (tgt, args) = unfoldType r in (tgt, (i, l) : args)
-  _ -> (ty, [])
+unfoldPi :: Type -> ([PiLhs], Type)
+unfoldPi ty = case ty of
+  NPi (Pi i bi r) ->
+    let (args, target) = unfoldPi r
+     in (PiLhs i bi : args, target)
+  _ -> ([], ty)
 
 typeArgs :: Type -> [Type]
-typeArgs = map snd . snd . unfoldType
+typeArgs = map (^. piLhsBinder . binderType) . fst . unfoldPi
 
 typeTarget :: Type -> Type
-typeTarget = fst . unfoldType
+typeTarget = snd . unfoldPi
 
 isDynamic :: Type -> Bool
 isDynamic = \case
@@ -163,12 +186,12 @@ isDynamic = \case
 -- `expandType [int, string] (int -> any) = int -> string -> any`.
 expandType :: [Type] -> Type -> Type
 expandType argtys ty =
-  let (tgt, tyargs) = unfoldType ty
+  let (tyargs, target) = unfoldPi ty
    in if
           | length tyargs >= length argtys ->
               ty
-          | isDynamic tgt ->
-              mkPis tyargs (mkPis' (drop (length tyargs) argtys) tgt)
+          | isDynamic target ->
+              rePis tyargs (mkPis' (drop (length tyargs) argtys) target)
           | otherwise ->
               impossible
 
@@ -193,14 +216,20 @@ unfoldApps' :: Node -> (Node, [Node])
 unfoldApps' = second (map snd) . unfoldApps
 
 mkLambdas :: [Info] -> Node -> Node
-mkLambdas is n = foldl' (flip mkLambda) n (reverse is)
+mkLambdas is n = foldl' (flip mkLambdaOld) n (reverse is)
+
+reLambda :: LambdaLhs -> Node -> Node
+reLambda lhs = mkLambda (lhs ^. lambdaLhsInfo) (lhs ^. lambdaLhsBinder)
+
+reLambdas :: [LambdaLhs] -> Node -> Node
+reLambdas is n = foldl' (flip reLambda) n (reverse is)
 
 -- | the given info corresponds to the binder info
-mkLambdaB :: Info -> Node -> Node
-mkLambdaB = mkLambda . singletonInfoBinder
+mkLambdaB :: Binder -> Node -> Node
+mkLambdaB = mkLambda mempty
 
 -- | the given infos correspond to the binder infos
-mkLambdasB :: [Info] -> Node -> Node
+mkLambdasB :: [Binder] -> Node -> Node
 mkLambdasB is n = foldl' (flip mkLambdaB) n (reverse is)
 
 mkLambdas' :: Int -> Node -> Node
@@ -208,7 +237,7 @@ mkLambdas' k
   | k < 0 = impossible
   | otherwise = mkLambdas (replicate k Info.empty)
 
-unfoldLambdasRev :: Node -> ([Info], Node)
+unfoldLambdasRev :: Node -> ([LambdaLhs], Node)
 unfoldLambdasRev = go []
   where
     go :: [LambdaLhs] -> Node -> ([LambdaLhs], Node)
@@ -216,7 +245,7 @@ unfoldLambdasRev = go []
       NLam (Lambda i bi b) -> go (LambdaLhs i bi : acc) b
       _ -> (acc, n)
 
-unfoldLambdas :: Node -> ([Info], Node)
+unfoldLambdas :: Node -> ([LambdaLhs], Node)
 unfoldLambdas = first reverse . unfoldLambdasRev
 
 unfoldLambdas' :: Node -> (Int, Node)
@@ -240,7 +269,7 @@ getPatternInfos = go []
     go :: [Info] -> Pattern -> [Info]
     go acc = \case
       PatConstr PatternConstr {..} -> foldl' go (_patternConstrInfo : acc) _patternConstrArgs
-      PatBinder PatternBinder {..} -> go (_patternBinderInfo : acc) _patternBinderPattern
+      PatBinder PatternBinder {..} -> go acc _patternBinderPattern
       PatWildcard PatternWildcard {..} -> _patternWildcardInfo : acc
 
 {------------------------------------------------------------------------}
@@ -268,7 +297,7 @@ data NodeDetails = NodeDetails
     -- the children (which should be in the same fixed order as in the
     -- 'nodeSubinfos' and 'nodeChildren' component).
     -- TODO can we zip the lists?
-    _nodeReassemble :: Info -> [Info] -> [Binder] -> [Node] -> Node
+    _nodeReassemble :: Info -> [Info] -> [[Binder]] -> [Node] -> Node
   }
 
 makeLenses ''NodeDetails
@@ -338,7 +367,7 @@ destruct = \case
         _nodeChildren = [b],
         _nodeChildBindersNum = [1],
         _nodeChildBindersInfo = [[bi]],
-        _nodeReassemble = \i' _ binders args' -> mkLambda i' (hd binders) (hd args')
+        _nodeReassemble = \i' _ binders' args' -> mkLambda i' (hd (hd binders')) (hd args')
       }
   NLet (Let i (LetItem bi v) b) ->
     NodeDetails
@@ -347,7 +376,7 @@ destruct = \case
         _nodeChildren = [v, b],
         _nodeChildBindersNum = [0, 1],
         _nodeChildBindersInfo = [[], [bi]],
-        _nodeReassemble = \i' _ binders args' -> mkLet i' (hd binders) (hd args') (args' !! 1)
+        _nodeReassemble = \i' _ binders' args' -> mkLet i' (hd (hd binders')) (hd args') (args' !! 1)
       }
   NRec (LetRec i vs b) ->
     let n = length vs
@@ -357,70 +386,75 @@ destruct = \case
             _nodeChildren = b : map (^. letItemValue) (toList vs),
             _nodeChildBindersNum = replicate (n + 1) n,
             _nodeChildBindersInfo = replicate (n + 1) (map (^. letItemBinder) (toList vs)),
-            _nodeReassemble = \i' _ binders args' -> mkLetRec i' (nonEmpty' (tl (zip binders args'))) (hd args')
+            _nodeReassemble = \i' _ binders' args' ->
+              mkLetRec i' (nonEmpty' (zipWithExact LetItem (hd binders') (tl args'))) (hd args')
           }
-  NCase (Case i v bs Nothing) ->
-    let branchBinderNums = map (^. caseBranchBindersNum) bs
-        branchBinderInfos = map (\CaseBranch {..} -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
-     in NodeDetails
-          { _nodeInfo = i,
-            _nodeSubinfos = map (^. caseBranchInfo) bs,
-            _nodeChildren = v : map (^. caseBranchBody) bs,
-            _nodeChildBindersNum = 0 : branchBinderNums,
-            _nodeChildBindersInfo = [] : branchBinderInfos,
-            _nodeReassemble = \i' is' args' ->
-              mkCase
-                i'
-                (hd args')
-                ( zipWith3Exact
-                    ( \br is body' ->
-                        br
-                          { _caseBranchInfo = is,
-                            _caseBranchBody = body'
-                          }
+  NCase (Case i v brs mdef) ->
+    let branchBinderNums = map (^. caseBranchBindersNum) brs
+        branchBinderInfos :: [[Binder]]
+        branchBinderInfos = map (^. caseBranchBinders) brs
+     in case mdef of
+          Nothing ->
+            NodeDetails
+              { _nodeInfo = i,
+                _nodeSubinfos = map (^. caseBranchInfo) brs,
+                _nodeChildren = v : map (^. caseBranchBody) brs,
+                _nodeChildBindersNum = 0 : branchBinderNums,
+                _nodeChildBindersInfo = [] : branchBinderInfos,
+                _nodeReassemble = \i' is' _ args' ->
+                  mkCase
+                    i'
+                    (hd args')
+                    ( zipWith3Exact
+                        ( \br is body' ->
+                            br
+                              { _caseBranchInfo = is,
+                                _caseBranchBody = body'
+                              }
+                        )
+                        brs
+                        is'
+                        (tl args')
                     )
-                    bs
-                    is'
-                    (tl args')
-                )
-                Nothing
-          }
-  NCase (Case i v bs (Just def)) ->
-    let branchBinderNums = map (^. caseBranchBindersNum) bs
-        branchBinderInfos = map (\CaseBranch {..} -> getInfoBinders _caseBranchBindersNum _caseBranchInfo) bs
-     in NodeDetails
-          { _nodeInfo = i,
-            _nodeSubinfos = map (^. caseBranchInfo) bs,
-            _nodeChildren = v : def : map (^. caseBranchBody) bs,
-            _nodeChildBindersNum = 0 : 0 : branchBinderNums,
-            _nodeChildBindersInfo = [] : [] : branchBinderInfos,
-            _nodeReassemble = \i' is' args' ->
-              mkCase
-                i'
-                (hd args')
-                ( zipWith3Exact
-                    ( \br is body' ->
-                        br
-                          { _caseBranchInfo = is,
-                            _caseBranchBody = body'
-                          }
+                    Nothing
+              }
+          Just def ->
+            NodeDetails
+              { _nodeInfo = i,
+                _nodeSubinfos = map (^. caseBranchInfo) brs,
+                _nodeChildren = v : def : map (^. caseBranchBody) brs,
+                _nodeChildBindersNum = 0 : 0 : branchBinderNums,
+                _nodeChildBindersInfo = [] : [] : branchBinderInfos,
+                _nodeReassemble = \i' is' binders' args' ->
+                  mkCase
+                    i'
+                    (hd args')
+                    ( zipWith3Exact
+                        ( \br (bis, is) body' ->
+                            br
+                              { _caseBranchInfo = is,
+                                _caseBranchBinders = bis,
+                                _caseBranchBody = body'
+                              }
+                        )
+                        brs
+                        (zipExact binders' is')
+                        (tl (tl args'))
                     )
-                    bs
-                    is'
-                    (tl (tl args'))
-                )
-                (Just (hd (tl args')))
-          }
-  NMatch (Match i vs bs) ->
-    let branchBinderInfos =
+                    (Just (hd (tl args')))
+              }
+  NMatch (Match i vs branches) ->
+    let branchBinders :: [[Binder]]
+        branchBinders =
           map
             ( \br ->
                 concatMap
                   getBinderPatternInfos
                   (reverse (toList (br ^. matchBranchPatterns)))
             )
-            bs
-        branchBinderNums = map length branchBinderInfos
+            branches
+        branchBinderNums = map length branchBinders
+        branchPatternInfos :: [Info]
         branchPatternInfos =
           concatMap
             ( \br ->
@@ -428,28 +462,28 @@ destruct = \case
                   (reverse . getPatternInfos)
                   (br ^. matchBranchPatterns)
             )
-            bs
+            branches
         n = length vs
      in NodeDetails
           { _nodeInfo = i,
             _nodeSubinfos = branchPatternInfos,
-            _nodeChildren = toList vs ++ map (^. matchBranchBody) bs,
+            _nodeChildren = toList vs ++ map (^. matchBranchBody) branches,
             _nodeChildBindersNum = replicate n 0 ++ branchBinderNums,
-            _nodeChildBindersInfo = replicate n [] ++ branchBinderInfos,
-            _nodeReassemble = \i' is' args' ->
+            _nodeChildBindersInfo = replicate n [] ++ branchBinders,
+            _nodeReassemble = \i' is' binders' args' ->
               mkMatch
                 i'
                 (nonEmpty' $ take n args')
                 ( zipWithExact
-                    ( \br body' ->
+                    ( \br (brbinders', body') ->
                         br
                           { _matchBranchPatterns =
-                              nonEmpty' $ setPatternsInfos is' (toList (br ^. matchBranchPatterns)),
+                              nonEmpty' $ setPatternsInfos brbinders' is' (toList (br ^. matchBranchPatterns)),
                             _matchBranchBody = body'
                           }
                     )
-                    bs
-                    (drop n args')
+                    branches
+                    (drop n (zipExact binders' args'))
                 )
           }
   NPi (Pi i bi b) ->
@@ -459,7 +493,14 @@ destruct = \case
         _nodeChildren = [bi ^. binderType, b],
         _nodeChildBindersNum = [0, 1],
         _nodeChildBindersInfo = [[], [bi]],
-        _nodeReassemble = \i' _ args' -> mkPi i' (hd args') (args' !! 1)
+        _nodeReassemble = \i' _ binders' args' ->
+          -- NOTE the binder type here is treated as a node
+          -- TODO should we get the type from args' or binders'?
+          let ty :: Type
+              ty = hd args'
+              bi' :: Binder
+              bi' = set binderType ty (hd (binders' !! 1))
+           in mkPi i' bi' (args' !! 1)
       }
   NUniv (Univ i l) ->
     NodeDetails
@@ -468,7 +509,7 @@ destruct = \case
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ _ -> mkUniv i' l
+        _nodeReassemble = \i' _ _ _ -> mkUniv i' l
       }
   NTyp (TypeConstr i sym args) ->
     NodeDetails
@@ -477,7 +518,7 @@ destruct = \case
         _nodeChildren = args,
         _nodeChildBindersNum = map (const 0) args,
         _nodeChildBindersInfo = map (const []) args,
-        _nodeReassemble = \i' _ args' -> mkTypeConstr i' sym args'
+        _nodeReassemble = \i' _ _ args' -> mkTypeConstr i' sym args'
       }
   NPrim (TypePrim i prim) ->
     NodeDetails
@@ -486,7 +527,7 @@ destruct = \case
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ _ -> mkTypePrim i' prim
+        _nodeReassemble = \i' _ _ _ -> mkTypePrim i' prim
       }
   NDyn (Dynamic i) ->
     NodeDetails
@@ -495,7 +536,7 @@ destruct = \case
         _nodeChildren = [],
         _nodeChildBindersNum = [],
         _nodeChildBindersInfo = [],
-        _nodeReassemble = \i' _ _ -> mkDynamic i'
+        _nodeReassemble = \i' _ _ _ -> mkDynamic i'
       }
   Closure env (Lambda i bi b) ->
     NodeDetails
@@ -504,32 +545,28 @@ destruct = \case
         _nodeChildren = b : env,
         _nodeChildBindersNum = 1 : map (const 0) env,
         _nodeChildBindersInfo = [bi] : map (const []) env,
-        _nodeReassemble = \i' _ args' -> Closure (tl args') (Lambda i' bi (hd args'))
+        _nodeReassemble = \i' _ _ args' -> Closure (tl args') (Lambda i' bi (hd args'))
       }
   where
-    fetchBinderInfo :: Info -> [Info]
-    -- fetchBinderInfo i = [getInfoBinder i]
-    fetchBinderInfo i = undefined
-
-    setPatternsInfos :: [Info] -> [Pattern] -> [Pattern]
-    setPatternsInfos is ps = snd $ setPatternsInfos' is ps
-
-    setPatternsInfos' :: [Info] -> [Pattern] -> ([Info], [Pattern])
-    setPatternsInfos' is [] = (is, [])
-    setPatternsInfos' is (p : ps) =
-      let (is', p') = setPatInfos is p
-          (is'', ps') = setPatternsInfos' is' ps
-       in (is'', p' : ps')
-
-    setPatInfos :: [Info] -> Pattern -> ([Info], Pattern)
-    setPatInfos is = \case
-      PatWildcard x ->
-        (tl is, PatWildcard (x {_patternWildcardInfo = hd is}))
-      PatBinder x ->
-        (tl is, PatBinder (x {_patternBinderInfo = hd is}))
-      PatConstr x ->
-        let (is', ps) = setPatternsInfos' (tl is) (x ^. patternConstrArgs)
-         in (is', PatConstr (x {_patternConstrInfo = hd is, _patternConstrArgs = ps}))
+    setPatternsInfos :: [Binder] -> [Info] -> [Pattern] -> [Pattern]
+    setPatternsInfos binders infos = snd . setPatternsInfos' binders infos
+      where
+        setPatternsInfos' :: [Binder] -> [Info] -> [Pattern] -> (([Binder], [Info]), [Pattern])
+        setPatternsInfos' bs is [] = ((bs, is), [])
+        setPatternsInfos' bs is (p : ps) =
+          let ((bs', is'), p') = setPatInfos bs is p
+              (bis'', ps') = setPatternsInfos' bs' is' ps
+           in (bis'', p' : ps')
+
+        setPatInfos :: [Binder] -> [Info] -> Pattern -> (([Binder], [Info]), Pattern)
+        setPatInfos bs is = \case
+          PatWildcard x ->
+            ((bs, tl is), PatWildcard (x {_patternWildcardInfo = hd is}))
+          PatBinder x ->
+            ((tl bs, is), PatBinder (x {_patternBinder = hd bs}))
+          PatConstr x ->
+            let (bis', ps) = setPatternsInfos' bs (tl is) (x ^. patternConstrArgs)
+             in (bis', PatConstr (x {_patternConstrInfo = hd is, _patternConstrArgs = ps}))
 
     hd :: [a] -> a
     hd = List.head
@@ -538,20 +575,21 @@ destruct = \case
     tl = List.tail
 
 reassemble :: Node -> [Node] -> Node
-reassemble n = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos)
+reassemble n = (d ^. nodeReassemble) (d ^. nodeInfo) (d ^. nodeSubinfos) (d ^. nodeChildBindersInfo)
   where
+    d :: NodeDetails
     d = destruct n
 
 children :: Node -> [Node]
 children = (^. nodeChildren) . destruct
 
--- children together with the number of binders
+-- | children together with the number of binders
 bchildren :: Node -> [(Int, Node)]
 bchildren n =
   let ni = destruct n
    in zipExact (ni ^. nodeChildBindersNum) (ni ^. nodeChildren)
 
--- shallow children: not under binders
+-- | shallow children: not under binders
 schildren :: Node -> [Node]
 schildren = map snd . filter (\p -> fst p == 0) . bchildren
 
@@ -564,7 +602,7 @@ modifyInfoM f n =
    in do
         i' <- f (ni ^. nodeInfo)
         is' <- mapM f (ni ^. nodeSubinfos)
-        return ((ni ^. nodeReassemble) i' is' (ni ^. nodeChildren))
+        return ((ni ^. nodeReassemble) i' is' (ni ^. nodeChildBindersInfo) (ni ^. nodeChildren))
 
 modifyInfo :: (Info -> Info) -> Node -> Node
 modifyInfo f n = runIdentity $ modifyInfoM (pure . f) n
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Collector.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Collector.hs
index 94d4e6a009..94fc24195f 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Collector.hs
+++ b/src/Juvix/Compiler/Core/Extra/Recursors/Collector.hs
@@ -16,19 +16,19 @@ makeLenses ''Collector
 unitCollector :: Collector a ()
 unitCollector = Collector () (\_ _ -> ())
 
-binderInfoCollector' :: BinderList Info -> Collector (Int, [Info]) (BinderList Info)
+binderInfoCollector' :: BinderList Binder -> Collector (Int, [Binder]) (BinderList Binder)
 binderInfoCollector' ini = Collector ini collect
   where
-    collect :: (Int, [Info]) -> BinderList Info -> BinderList Info
+    collect :: (Int, [Binder]) -> BinderList Binder -> BinderList Binder
     collect (k, bi) c
       | k == 0 = c
       | otherwise = BL.prepend (reverse bi) c
 
-binderInfoCollector :: Collector (Int, [Info]) (BinderList Info)
+binderInfoCollector :: Collector (Int, [Binder]) (BinderList Binder)
 binderInfoCollector = binderInfoCollector' mempty
 
-binderNumCollector' :: Int -> Collector (Int, [Info]) Index
+binderNumCollector' :: Int -> Collector (Int, [Binder]) Index
 binderNumCollector' ini = Collector ini (\(k, _) c -> c + k)
 
-binderNumCollector :: Collector (Int, [Info]) Index
+binderNumCollector :: Collector (Int, [Binder]) Index
 binderNumCollector = binderNumCollector' 0
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Fold.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Fold.hs
index 62f5ed3151..3a0c89c612 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Fold.hs
+++ b/src/Juvix/Compiler/Core/Extra/Recursors/Fold.hs
@@ -7,7 +7,7 @@ import Juvix.Compiler.Core.Extra.Recursors.Base
 ufoldG ::
   forall c a f.
   Applicative f =>
-  Collector (Int, [Info]) c ->
+  Collector (Int, [Binder]) c ->
   (a -> [a] -> a) ->
   (c -> Node -> f a) ->
   Node ->
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
index 46692dbfe4..8c2d73ad94 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
+++ b/src/Juvix/Compiler/Core/Extra/Recursors/Fold/Named.hs
@@ -7,7 +7,7 @@ import Juvix.Compiler.Core.Extra.Recursors.Fold
 ufoldA :: Applicative f => (a -> [a] -> a) -> (Node -> f a) -> Node -> f a
 ufoldA uplus f = ufoldG unitCollector uplus (const f)
 
-ufoldLA :: Applicative f => (a -> [a] -> a) -> (BinderList Info -> Node -> f a) -> Node -> f a
+ufoldLA :: Applicative f => (a -> [a] -> a) -> (BinderList Binder -> Node -> f a) -> Node -> f a
 ufoldLA uplus f = ufoldG binderInfoCollector uplus f
 
 ufoldNA :: Applicative f => (a -> [a] -> a) -> (Index -> Node -> f a) -> Node -> f a
@@ -19,13 +19,13 @@ walk = ufoldA (foldr mappend)
 walkN :: Applicative f => (Index -> Node -> f ()) -> Node -> f ()
 walkN = ufoldNA (foldr mappend)
 
-walkL :: Applicative f => (BinderList Info -> Node -> f ()) -> Node -> f ()
+walkL :: Applicative f => (BinderList Binder -> Node -> f ()) -> Node -> f ()
 walkL = ufoldLA (foldr mappend)
 
 ufold :: (a -> [a] -> a) -> (Node -> a) -> Node -> a
 ufold uplus f = runIdentity . ufoldA uplus (return . f)
 
-ufoldL :: (a -> [a] -> a) -> (BinderList Info -> Node -> a) -> Node -> a
+ufoldL :: (a -> [a] -> a) -> (BinderList Binder -> Node -> a) -> Node -> a
 ufoldL uplus f = runIdentity . ufoldLA uplus (\is -> return . f is)
 
 ufoldN :: (a -> [a] -> a) -> (Index -> Node -> a) -> Node -> a
@@ -34,7 +34,7 @@ ufoldN uplus f = runIdentity . ufoldNA uplus (\idx -> return . f idx)
 gather :: (a -> Node -> a) -> a -> Node -> a
 gather f acc = run . execState acc . walk (\n' -> modify' (`f` n'))
 
-gatherL :: (BinderList Info -> a -> Node -> a) -> a -> Node -> a
+gatherL :: (BinderList Binder -> a -> Node -> a) -> a -> Node -> a
 gatherL f acc = run . execState acc . walkL (\is n' -> modify' (\a -> f is a n'))
 
 gatherN :: (Index -> a -> Node -> a) -> a -> Node -> a
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
index 3803647d48..842df59bff 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
+++ b/src/Juvix/Compiler/Core/Extra/Recursors/Map.hs
@@ -14,12 +14,12 @@ type family DirTy d = res | res -> d where
   DirTy 'TopDown = Recur
   DirTy 'BottomUp = Node -- For bottom up maps we never recur on the children
 
--- `umapG` maps the nodes bottom-up, i.e., when invoking the mapper function the
+-- | `umapG` maps the nodes bottom-up, i.e., when invoking the mapper function the
 -- recursive subnodes have already been mapped
 umapG ::
   forall c m.
   Monad m =>
-  Collector (Int, [Info]) c ->
+  Collector (Int, [Binder]) c ->
   (c -> Node -> m Node) ->
   Node ->
   m Node
@@ -36,12 +36,12 @@ umapG coll f = go (coll ^. cEmpty)
                   (ni ^. nodeChildren)
                   (ni ^. nodeChildBindersNum)
                   (ni ^. nodeChildBindersInfo)
-            f c ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) ns)
+            f c ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) (ni ^. nodeChildBindersInfo) ns)
 
 dmapG ::
   forall c m.
   Monad m =>
-  Collector (Int, [Info]) c ->
+  Collector (Int, [Binder]) c ->
   (c -> Node -> m Recur) ->
   Node ->
   m Node
@@ -61,14 +61,14 @@ dmapG coll f = go (coll ^. cEmpty)
                 (ni ^. nodeChildren)
                 (ni ^. nodeChildBindersNum)
                 (ni ^. nodeChildBindersInfo)
-          return ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) ns)
+          return ((ni ^. nodeReassemble) (ni ^. nodeInfo) (ni ^. nodeSubinfos) (ni ^. nodeChildBindersInfo) ns)
       where
-        goChild :: Node -> Int -> [Info] -> m Node
+        goChild :: Node -> Int -> [Binder] -> m Node
         goChild n'' k bis = go ((coll ^. cCollect) (k, bis) c) n''
 
 type CtxTy :: Ctx -> GHC.Type
 type family CtxTy x = res | res -> x where
-  CtxTy 'CtxBinderList = BinderList Info
+  CtxTy 'CtxBinderList = BinderList Binder
   CtxTy 'CtxBinderNum = Index
   CtxTy 'CtxNone = ()
 
@@ -83,17 +83,17 @@ type family RetTy m dir mon r = res | res -> mon r where
 
 type BodyTy :: (GHC.Type -> GHC.Type) -> Direction -> Monadic -> Ctx -> Ret -> GHC.Type
 type family BodyTy m dir mon x r = res | res -> x r where
-  BodyTy m dir 'Monadic 'CtxBinderList r = BinderList Info -> Node -> RetTy m dir 'Monadic r
+  BodyTy m dir 'Monadic 'CtxBinderList r = BinderList Binder -> Node -> RetTy m dir 'Monadic r
   BodyTy m dir 'Monadic 'CtxBinderNum r = Int -> Node -> RetTy m dir 'Monadic r
   BodyTy m dir 'Monadic 'CtxNone r = Node -> RetTy m dir 'Monadic r
-  BodyTy _ dir 'NonMonadic 'CtxBinderList r = BinderList Info -> Node -> RetTy Identity dir 'NonMonadic r
+  BodyTy _ dir 'NonMonadic 'CtxBinderList r = BinderList Binder -> Node -> RetTy Identity dir 'NonMonadic r
   BodyTy _ dir 'NonMonadic 'CtxBinderNum r = Int -> Node -> RetTy Identity dir 'NonMonadic r
   BodyTy _ dir 'NonMonadic 'CtxNone r = Node -> RetTy Identity dir 'NonMonadic r
 
 type NodeMapArg :: (GHC.Type -> GHC.Type) -> Direction -> Monadic -> CollectorIni -> Ctx -> Ret -> GHC.Type
 type family NodeMapArg m dir mon i x r = res | res -> i x r where
   NodeMapArg m dir mon 'Ini x r = (CtxTy x, BodyTy m dir mon x r)
-  NodeMapArg m dir mon 'NoIni 'CtxBinderList r = BinderList Info -> Node -> RetTy m dir mon r
+  NodeMapArg m dir mon 'NoIni 'CtxBinderList r = BinderList Binder -> Node -> RetTy m dir mon r
   NodeMapArg m dir mon 'NoIni 'CtxBinderNum r = Int -> Node -> RetTy m dir mon r
   NodeMapArg m dir mon 'NoIni 'CtxNone r = Node -> RetTy m dir mon r
 
@@ -106,7 +106,7 @@ type OverIdentity :: GHC.Type -> GHC.Type
 type family OverIdentity t = res where
   OverIdentity (a -> b) = a -> OverIdentity b
   OverIdentity ((), b) = ((), OverIdentity b)
-  OverIdentity (BinderList Info, b) = (BinderList Info, OverIdentity b)
+  OverIdentity (BinderList Binder, b) = (BinderList Binder, OverIdentity b)
   OverIdentity (Index, b) = (Index, OverIdentity b)
   OverIdentity leaf = Identity leaf
 
@@ -122,7 +122,7 @@ instance EmbedIdentity b => EmbedIdentity ((), b) where
 instance EmbedIdentity b => EmbedIdentity (Index, b) where
   embedIden (a, b) = (a, embedIden b)
 
-instance EmbedIdentity b => EmbedIdentity (BinderList Info, b) where
+instance EmbedIdentity b => EmbedIdentity (BinderList Binder, b) where
   embedIden (a, b) = (a, embedIden b)
 
 instance EmbedIdentity Node where
@@ -201,7 +201,7 @@ nodeMapE sdir smon sini sctx sret f = case smon :: SMonadic mon of
     fromSimple :: forall g. Functor g => g Node -> g Recur
     fromSimple = fmap Recur
     nodeMapG' ::
-      Collector (Int, [Info]) c ->
+      Collector (Int, [Binder]) c ->
       (c -> Node -> m (DirTy dir)) ->
       Node ->
       m Node
diff --git a/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs b/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
index 37e7215bbd..6fb53c3996 100644
--- a/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
+++ b/src/Juvix/Compiler/Core/Extra/Recursors/Map/Named.hs
@@ -4,13 +4,13 @@ import Juvix.Compiler.Core.Extra.Recursors.Base
 import Juvix.Compiler.Core.Extra.Recursors.Map
 import Juvix.Compiler.Core.Extra.Recursors.Parameters
 
-dmapLRM :: Monad m => (BinderList Info -> Node -> m Recur) -> Node -> m Node
+dmapLRM :: Monad m => (BinderList Binder -> Node -> m Recur) -> Node -> m Node
 dmapLRM = nodeMapI STopDown
 
-dmapLM :: Monad m => (BinderList Info -> Node -> m Node) -> Node -> m Node
+dmapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
 dmapLM = nodeMapI STopDown
 
-umapLM :: Monad m => (BinderList Info -> Node -> m Node) -> Node -> m Node
+umapLM :: Monad m => (BinderList Binder -> Node -> m Node) -> Node -> m Node
 umapLM = nodeMapI SBottomUp
 
 dmapNRM :: Monad m => (Index -> Node -> m Recur) -> Node -> m Node
@@ -31,13 +31,13 @@ dmapM = nodeMapI STopDown
 umapM :: Monad m => (Node -> m Node) -> Node -> m Node
 umapM = nodeMapI SBottomUp
 
-dmapLRM' :: Monad m => (BinderList Info, BinderList Info -> Node -> m Recur) -> Node -> m Node
+dmapLRM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Recur) -> Node -> m Node
 dmapLRM' = nodeMapI STopDown
 
-dmapLM' :: Monad m => (BinderList Info, BinderList Info -> Node -> m Node) -> Node -> m Node
+dmapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
 dmapLM' = nodeMapI STopDown
 
-umapLM' :: Monad m => (BinderList Info, BinderList Info -> Node -> m Node) -> Node -> m Node
+umapLM' :: Monad m => (BinderList Binder, BinderList Binder -> Node -> m Node) -> Node -> m Node
 umapLM' = nodeMapI SBottomUp
 
 dmapNRM' :: Monad m => (Index, Index -> Node -> m Recur) -> Node -> m Node
@@ -49,13 +49,13 @@ dmapNM' = nodeMapI STopDown
 umapNM' :: Monad m => (Index, Index -> Node -> m Node) -> Node -> m Node
 umapNM' = nodeMapI SBottomUp
 
-dmapLR :: (BinderList Info -> Node -> Recur) -> Node -> Node
+dmapLR :: (BinderList Binder -> Node -> Recur) -> Node -> Node
 dmapLR = nodeMapI STopDown
 
-dmapL :: (BinderList Info -> Node -> Node) -> Node -> Node
+dmapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
 dmapL = nodeMapI STopDown
 
-umapL :: (BinderList Info -> Node -> Node) -> Node -> Node
+umapL :: (BinderList Binder -> Node -> Node) -> Node -> Node
 umapL = nodeMapI SBottomUp
 
 dmapNR :: (Index -> Node -> Recur) -> Node -> Node
@@ -76,13 +76,13 @@ dmap = nodeMapI STopDown
 umap :: (Node -> Node) -> Node -> Node
 umap = nodeMapI SBottomUp
 
-dmapLR' :: (BinderList Info, BinderList Info -> Node -> Recur) -> Node -> Node
+dmapLR' :: (BinderList Binder, BinderList Binder -> Node -> Recur) -> Node -> Node
 dmapLR' = nodeMapI STopDown
 
-dmapL' :: (BinderList Info, BinderList Info -> Node -> Node) -> Node -> Node
+dmapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
 dmapL' = nodeMapI STopDown
 
-umapL' :: (BinderList Info, BinderList Info -> Node -> Node) -> Node -> Node
+umapL' :: (BinderList Binder, BinderList Binder -> Node -> Node) -> Node -> Node
 umapL' = nodeMapI SBottomUp
 
 dmapNR' :: (Index, Index -> Node -> Recur) -> Node -> Node
diff --git a/src/Juvix/Compiler/Core/Language.hs b/src/Juvix/Compiler/Core/Language.hs
index a54009bc36..ad4d0d0667 100644
--- a/src/Juvix/Compiler/Core/Language.hs
+++ b/src/Juvix/Compiler/Core/Language.hs
@@ -27,6 +27,8 @@ type LambdaLhs = LambdaLhs' Info Node
 
 type Lambda = Lambda' Info Node
 
+type LetItem = LetItem' Node
+
 type Let = Let' Info Node
 
 type LetRec = LetRec' Info Node
@@ -41,12 +43,14 @@ type MatchBranch = MatchBranch' Info Node
 
 type PatternWildcard = PatternWildcard' Info
 
-type PatternBinder = PatternBinder' Info
+type PatternBinder = PatternBinder' Info Node
 
-type PatternConstr = PatternConstr' Info
+type PatternConstr = PatternConstr' Info Node
 
 type Pattern = Pattern' Info Node
 
+type PiLhs = PiLhs' Info Node
+
 type Pi = Pi' Info Node
 
 type Univ = Univ' Info
diff --git a/src/Juvix/Compiler/Core/Language/Nodes.hs b/src/Juvix/Compiler/Core/Language/Nodes.hs
index 432a036c3a..0caebfe216 100644
--- a/src/Juvix/Compiler/Core/Language/Nodes.hs
+++ b/src/Juvix/Compiler/Core/Language/Nodes.hs
@@ -10,13 +10,22 @@ import Juvix.Compiler.Core.Language.Base
 import Juvix.Compiler.Core.Language.Primitives
 
 -- | De Bruijn index of a locally bound variable.
-data Var' i = Var {_varInfo :: i, _varIndex :: !Index}
+data Var' i = Var
+  { _varInfo :: i,
+    _varIndex :: !Index
+  }
 
 -- | Global identifier of a function (with corresponding `Node` in the global
 -- context).
-data Ident' i = Ident {_identInfo :: i, _identSymbol :: !Symbol}
+data Ident' i = Ident
+  { _identInfo :: i,
+    _identSymbol :: !Symbol
+  }
 
-data Constant' i = Constant {_constantInfo :: i, _constantValue :: !ConstantValue}
+data Constant' i = Constant
+  { _constantInfo :: i,
+    _constantValue :: !ConstantValue
+  }
 
 data ConstantValue
   = ConstInteger !Integer
@@ -25,9 +34,8 @@ data ConstantValue
 
 -- | Info about a single binder. Associated with Lambda and Pi.
 data Binder' a = Binder
-  {
-   _binderName :: Maybe Name,
-   _binderType :: a
+  { _binderName :: Maybe Name,
+    _binderType :: a
   }
 
 -- Other things we might need in the future:
@@ -67,9 +75,9 @@ data Constr' i a = Constr
   }
 
 -- | Useful for unfolding lambdas
-data LambdaLhs' i a = LambdaLhs {
-  _lambdaLhsInfo :: i,
-  _lambdaLhsBinder :: Binder' a
+data LambdaLhs' i a = LambdaLhs
+  { _lambdaLhsInfo :: i,
+    _lambdaLhsBinder :: Binder' a
   }
 
 data Lambda' i a = Lambda
@@ -86,9 +94,9 @@ data Let' i a = Let
     _letBody :: !a
   }
 
-data LetItem' a = LetItem {
-  _letItemBinder :: Binder' a,
-  _letItemValue :: a
+data LetItem' a = LetItem
+  { _letItemBinder :: Binder' a,
+    _letItemValue :: a
   }
 
 -- | Represents a block of mutually recursive local definitions. Both in the
@@ -109,12 +117,13 @@ data Case' i bi a = Case
     _caseDefault :: !(Maybe a)
   }
 
--- | `CaseBranch tag argsNum branch`
--- - `argsNum` is the number of arguments of the constructor tagged with `tag`,
---   equal to the number of implicit binders above `branch`
+-- | `CaseBranch tag binders bindersNum branch`
+-- - `binders` are the arguments of the constructor tagged with `tag`,
+--  length of `binders` is equal to `bindersNum`
 data CaseBranch' i a = CaseBranch
   { _caseBranchInfo :: i,
     _caseBranchTag :: !Tag,
+    _caseBranchBinders :: [Binder' a],
     _caseBranchBindersNum :: !Int,
     _caseBranchBody :: !a
   }
@@ -148,8 +157,7 @@ newtype PatternWildcard' i = PatternWildcard
   }
 
 data PatternBinder' i a = PatternBinder
-  { _patternBinderInfo :: i,
-    _patternBinder :: Binder' a,
+  { _patternBinder :: Binder' a,
     _patternBinderPattern :: Pattern' i a
   }
 
@@ -159,6 +167,12 @@ data PatternConstr' i a = PatternConstr
     _patternConstrArgs :: ![Pattern' i a]
   }
 
+-- | Useful for unfolding Pi
+data PiLhs' i a = PiLhs
+  { _piLhsInfo :: i,
+    _piLhsBinder :: Binder' a
+  }
+
 -- | Dependent Pi-type. Compilation-time only. Pi implicitly introduces a binder
 -- in the body, exactly like Lambda. So `Pi info ty body` is `Pi x : ty .
 -- body` in more familiar notation, but references to `x` in `body` are via de
@@ -272,6 +286,8 @@ instance HasAtomicity (Dynamic' i) where
 lambdaFixity :: Fixity
 lambdaFixity = Fixity (PrecNat 0) (Unary AssocPostfix)
 
+makeLenses ''LambdaLhs'
+makeLenses ''PiLhs'
 makeLenses ''Binder'
 makeLenses ''Var'
 makeLenses ''Ident'
@@ -320,7 +336,9 @@ instance Eq a => Eq (Case' i bi a) where
   (Case _ v1 bs1 def1) == (Case _ v2 bs2 def2) = v1 == v2 && bs1 == bs2 && def1 == def2
 
 instance Eq a => Eq (CaseBranch' i a) where
-  (CaseBranch _ tag1 n1 b1) == (CaseBranch _ tag2 n2 b2) = tag1 == tag2 && n1 == n2 && b1 == b2
+  (==) =
+    eqOn (^. caseBranchTag)
+      ..&&.. eqOn (^. caseBranchBody)
 
 instance Eq a => Eq (Match' i a) where
   (Match _ vs1 bs1) == (Match _ vs2 bs2) = vs1 == vs2 && bs1 == bs2
@@ -351,16 +369,19 @@ instance Eq a => Eq (Lambda' i a) where
 
 -- | ignores the binder
 instance Eq a => Eq (Let' i a) where
-  (==) = eqOn (^. letItem)
-    ..&&.. eqOn (^. letBody)
+  (==) =
+    eqOn (^. letItem)
+      ..&&.. eqOn (^. letBody)
 
 instance Eq a => Eq (LetRec' i a) where
-  (==) = eqOn (^. letRecBody)
-    ..&&.. eqOn (^. letRecValues)
+  (==) =
+    eqOn (^. letRecBody)
+      ..&&.. eqOn (^. letRecValues)
 
 instance Eq a => Eq (Pi' i a) where
-  (==) = eqOn (^. piBinder . binderType)
-   ..&&.. eqOn (^. piBody)
+  (==) =
+    eqOn (^. piBinder . binderType)
+      ..&&.. eqOn (^. piBody)
 
 -- | ignores the binder
 instance Eq a => Eq (PatternBinder' i a) where
diff --git a/src/Juvix/Compiler/Core/Language/Stripped.hs b/src/Juvix/Compiler/Core/Language/Stripped.hs
index c014a52a90..e646e957cb 100644
--- a/src/Juvix/Compiler/Core/Language/Stripped.hs
+++ b/src/Juvix/Compiler/Core/Language/Stripped.hs
@@ -56,8 +56,8 @@ type Constant = Constant' ()
 
 type Apps = Apps' Fun () Node
 
-data Fun =
-  FunVar Var
+data Fun
+  = FunVar Var
   | FunIdent Ident
   deriving stock (Eq)
 
diff --git a/src/Juvix/Compiler/Core/Pretty/Base.hs b/src/Juvix/Compiler/Core/Pretty/Base.hs
index 9eb0977c96..2b2f8b4003 100644
--- a/src/Juvix/Compiler/Core/Pretty/Base.hs
+++ b/src/Juvix/Compiler/Core/Pretty/Base.hs
@@ -131,7 +131,7 @@ ppCodeLet' name mty lt = do
   n' <- case name of
     Just nm -> ppCode nm
     Nothing -> return kwQuestion
-  v' <- ppCode (lt ^. letValue)
+  v' <- ppCode (lt ^. letItem . letItemValue)
   b' <- ppCode (lt ^. letBody)
   let tty = case mty of
         Just ty ->
@@ -162,7 +162,7 @@ instance PrettyCode PatternWildcard where
 
 instance PrettyCode PatternBinder where
   ppCode PatternBinder {..} = do
-    n <- case getInfoName _patternBinderInfo of
+    n <- case _patternBinder ^. binderName of
       Just name -> ppCode name
       Nothing -> return kwQuestion
     case _patternBinderPattern of
@@ -204,7 +204,7 @@ instance PrettyCode LetRec where
   ppCode LetRec {..} = do
     let n = length _letRecValues
     ns <- mapM getName (getInfoBinders n _letRecInfo)
-    vs <- mapM ppCode _letRecValues
+    vs <- mapM (ppCode . (^. letItemValue)) _letRecValues
     b' <- ppCode _letRecBody
     return $ case ns of
       [hns] -> kwLetRec <+> hns <+> kwAssign <+> head vs <+> kwIn <+> b'
@@ -238,13 +238,12 @@ instance PrettyCode Node where
     NCtr x ->
       let name = getInfoName (x ^. constrInfo)
        in ppCodeConstr' name x
-    NLam (Lambda i body) -> do
+    NLam (Lambda _ bi body) -> do
       b <- ppCode body
-      let bi = getInfoBinder i
-      lam <- case getInfoName bi of
+      lam <- case bi ^. binderName of
         Just name -> do
           n <- ppCode name
-          case getInfoType bi of
+          case bi ^. binderType of
             NDyn {} -> return $ kwLambda <> n
             ty -> do
               tty <- ppCode ty
@@ -266,16 +265,17 @@ instance PrettyCode Node where
       let bss = bracesIndent $ align $ concatWith (\a b -> a <> kwSemicolon <> line <> b) bs
       return $ kwMatch <+> hsep (punctuate comma (toList vs)) <+> kwWith <+> bss
     NPi Pi {..} ->
-      case getInfoName $ getInfoBinder _piInfo of
-        Just name -> do
-          n <- ppCode name
-          ty <- ppCode _piType
-          b <- ppCode _piBody
-          return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
-        Nothing -> do
-          ty <- ppLeftExpression funFixity _piType
-          b <- ppRightExpression funFixity _piBody
-          return $ ty <+> kwArrow <+> b
+      let piType = _piBinder ^. binderType
+       in case getInfoName $ getInfoBinder _piInfo of
+            Just name -> do
+              n <- ppCode name
+              ty <- ppCode piType
+              b <- ppCode _piBody
+              return $ kwPi <+> n <+> kwColon <+> ty <> comma <+> b
+            Nothing -> do
+              ty <- ppLeftExpression funFixity piType
+              b <- ppRightExpression funFixity _piBody
+              return $ ty <+> kwArrow <+> b
     NUniv Univ {..} ->
       return $ kwType <+> pretty _univLevel
     NPrim TypePrim {..} -> ppCode _typePrimPrimitive
diff --git a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
index 73d0441fbd..c1905af953 100644
--- a/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
+++ b/src/Juvix/Compiler/Core/Transformation/LambdaLifting.hs
@@ -11,19 +11,19 @@ import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Pretty
 import Juvix.Compiler.Core.Transformation.Base
 
-lambdaLiftNode :: forall r. Member InfoTableBuilder r => BinderList Info -> Node -> Sem r Node
+lambdaLiftNode :: forall r. Member InfoTableBuilder r => BinderList Binder -> Node -> Sem r Node
 lambdaLiftNode aboveBl top =
-  mkLambdas topArgs <$> dmapLRM' (topArgsBinderList <> aboveBl, go) body
+  reLambdas topArgs <$> dmapLRM' (topArgsBinderList <> aboveBl, go) body
   where
     (topArgs, body) = unfoldLambdas top
-    topArgsBinderList :: BinderList Info
-    topArgsBinderList = BL.fromList topArgs
+    topArgsBinderList :: BinderList Binder
+    topArgsBinderList = BL.fromList (map (^. lambdaLhsBinder) topArgs)
     typeFromArgs :: [ArgumentInfo] -> Type
     typeFromArgs = \case
       [] -> mkDynamic' -- change this when we have type info about the body
       (a : as) -> mkPi' (a ^. argumentType) (typeFromArgs as)
     -- extracts the argument info from the binder
-    go :: BinderList Info -> Node -> Sem r Recur
+    go :: BinderList Binder -> Node -> Sem r Recur
     go bl = \case
       NLam l -> goLambda l
       m -> return (Recur m)
@@ -32,11 +32,11 @@ lambdaLiftNode aboveBl top =
         goLambda lm = do
           l' <- lambdaLiftNode bl (NLam lm)
           let freevars = toList (getFreeVars l')
-              freevarsAssocs :: [(Index, Info)]
-              freevarsAssocs = [(i, BL.lookup i bl) | i <- map (^. varIndex) freevars]
+              freevarsAssocs :: [(Index, Binder)]
+              freevarsAssocs = [(idx, BL.lookup idx bl) | idx <- map (^. varIndex) freevars]
               fBody' = captureFreeVars freevarsAssocs l'
               argsInfo :: [ArgumentInfo]
-              argsInfo = map (argumentInfoFromInfo . snd) freevarsAssocs
+              argsInfo = map (argumentInfoFromBinder . snd) freevarsAssocs
           f <- freshSymbol
           registerIdent
             IdentifierInfo
diff --git a/src/Juvix/Compiler/Core/Translation/FromSource.hs b/src/Juvix/Compiler/Core/Translation/FromSource.hs
index b2dec0265b..96825b0548 100644
--- a/src/Juvix/Compiler/Core/Translation/FromSource.hs
+++ b/src/Juvix/Compiler/Core/Translation/FromSource.hs
@@ -4,19 +4,18 @@ module Juvix.Compiler.Core.Translation.FromSource
   )
 where
 
+import Control.Monad.Combinators.NonEmpty qualified as NonEmpty
 import Control.Monad.Fail qualified as P
 import Control.Monad.Trans.Class (lift)
 import Data.HashMap.Strict qualified as HashMap
-import Data.List qualified as List
 import Data.List.NonEmpty (fromList)
+import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Core.Data.InfoTable
 import Juvix.Compiler.Core.Data.InfoTableBuilder
 import Juvix.Compiler.Core.Extra
 import Juvix.Compiler.Core.Info qualified as Info
-import Juvix.Compiler.Core.Info.BinderInfo as BinderInfo
 import Juvix.Compiler.Core.Info.LocationInfo as LocationInfo
 import Juvix.Compiler.Core.Info.NameInfo as NameInfo
-import Juvix.Compiler.Core.Info.TypeInfo as TypeInfo
 import Juvix.Compiler.Core.Language
 import Juvix.Compiler.Core.Transformation.Eta
 import Juvix.Compiler.Core.Translation.FromSource.Lexer
@@ -38,10 +37,10 @@ runParser fileName tab input =
     (_, Left err) -> Left (ParserError err)
     (tbl, Right r) -> Right (tbl, r)
 
-binderInfo :: Name -> Type -> Info
-binderInfo name ty =
-  let info = setInfoType ty (Info.singleton (NameInfo name))
-   in Info.singleton (BinderInfo info)
+-- binderInfo :: Name -> Type -> Info
+-- binderInfo name ty =
+--   let info = setInfoType ty (Info.singleton (NameInfo name))
+--    in Info.singleton (BinderInfo info)
 
 freshName ::
   Member NameIdGen r =>
@@ -203,17 +202,15 @@ parseDefinition sym ty = do
         && not (isDynamic (typeTarget ty))
     )
     $ parseFailure off "type mismatch: too many lambdas"
-  lift $ setIdentArgsInfo sym (map toArgumentInfo is)
+  lift $ setIdentArgsInfo sym (map (toArgumentInfo . (^. lambdaLhsBinder)) is)
   where
-    toArgumentInfo :: Info -> ArgumentInfo
-    toArgumentInfo i =
+    toArgumentInfo :: Binder -> ArgumentInfo
+    toArgumentInfo bi =
       ArgumentInfo
-        { _argumentName = getInfoName bi,
-          _argumentType = getInfoType bi,
+        { _argumentName = bi ^. binderName,
+          _argumentType = bi ^. binderType,
           _argumentIsImplicit = Explicit
         }
-      where
-        bi = getInfoBinder i
 
 statementInductive ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -367,7 +364,7 @@ seqExpr' varsNum vars node = do
     mkConstr
       Info.empty
       (BuiltinTag TagBind)
-      [node, mkLambda (binderInfo name mkDynamic') node']
+      [node, mkLambda mempty (Binder (Just name) mkDynamic') node']
 
 cmpExpr ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -569,8 +566,8 @@ atoms ::
   HashMap Text Level ->
   ParsecS r Node
 atoms varsNum vars = do
-  es <- P.some (atom varsNum vars)
-  return $ mkApps' (List.head es) (List.tail es)
+  es <- NonEmpty.some (atom varsNum vars)
+  return $ mkApps' (head es) (NonEmpty.tail es)
 
 atom ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -649,8 +646,9 @@ exprPi varsNum vars = do
   ty <- expr varsNum vars
   kw kwComma
   let vars' = HashMap.insert (name ^. nameText) varsNum vars
+      bi = Binder (Just name) ty
   body <- expr (varsNum + 1) vars'
-  return $ mkPi (binderInfo name ty) ty body
+  return $ mkPi mempty bi body
 
 exprLambda ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -661,8 +659,9 @@ exprLambda varsNum vars = do
   lambda
   (name, mty) <- lambdaName
   let vars' = HashMap.insert (name ^. nameText) varsNum vars
+      bi = Binder (Just name) (fromMaybe mkDynamic' mty)
   body <- bracedExpr (varsNum + 1) vars'
-  return $ mkLambda (binderInfo name (fromMaybe mkDynamic' mty)) body
+  return $ mkLambda mempty bi body
   where
     lambdaName =
       parens
@@ -687,7 +686,9 @@ exprLetrecOne varsNum vars = do
   value <- bracedExpr (varsNum + 1) vars'
   kw kwIn
   body <- bracedExpr (varsNum + 1) vars'
-  return $ mkLetRec (Info.singleton (BindersInfo [Info.singleton (NameInfo name)])) (fromList [value]) body
+  let item :: LetItem
+      item = LetItem (Binder (Just name) mkDynamic') value
+  return $ mkLetRec mempty (pure item) body
 
 exprLetrecMany ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -701,35 +702,35 @@ exprLetrecMany varsNum vars = do
     parseFailure off "expected at least one identifier name in letrec signature"
   let (vars', varsNum') = foldl' (\(vs, k) txt -> (HashMap.insert txt k vs, k + 1)) (vars, varsNum) defNames
   defs <- letrecDefs defNames varsNum' vars'
+  kw kwIn
   body <- bracedExpr varsNum' vars'
-  let infos = map (Info.singleton . NameInfo . fst) defs
-  let values = map snd defs
-  return $ mkLetRec (Info.singleton (BindersInfo infos)) (fromList values) body
+  return $ mkLetRec mempty defs body
 
-letrecNames :: ParsecS r [Text]
-letrecNames = P.between (symbol "[") (symbol "]") (P.many identifier)
+letrecNames :: ParsecS r (NonEmpty Text)
+letrecNames = P.between (symbol "[") (symbol "]") (NonEmpty.some identifier)
 
 letrecDefs ::
+  forall r.
   Members '[InfoTableBuilder, NameIdGen] r =>
-  [Text] ->
-  Index ->
-  HashMap Text Level ->
-  ParsecS r [(Name, Node)]
-letrecDefs names varsNum vars = case names of
-  [] -> return []
-  n : names' -> do
-    off <- P.getOffset
-    (txt, i) <- identifierL
-    when (n /= txt) $
-      parseFailure off "identifier name doesn't match letrec signature"
-    name <- lift $ freshName KNameLocal txt i
-    kw kwAssign
-    v <- bracedExpr varsNum vars
-    if
-        | null names' -> optional (kw kwSemicolon) >> kw kwIn
-        | otherwise -> kw kwSemicolon
-    rest <- letrecDefs names' varsNum vars
-    return $ (name, v) : rest
+  NonEmpty Text ->
+  Index ->
+  HashMap Text Level ->
+  ParsecS r (NonEmpty LetItem)
+letrecDefs names varsNum vars =
+  mapM letrecItem names
+  where
+    letrecItem :: Text -> ParsecS r LetItem
+    letrecItem n = do
+      off <- P.getOffset
+      (txt, i) <- identifierL
+      when (n /= txt) $
+        parseFailure off "identifier name doesn't match letrec signature"
+      name <- lift $ freshName KNameLocal txt i
+      kw kwAssign
+      v <- bracedExpr varsNum vars
+      -- TODO last semicolon optional
+      kw kwSemicolon
+      return $ LetItem (Binder (Just name) mkDynamic') v
 
 letrecDef ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -756,8 +757,9 @@ exprLet varsNum vars = do
   value <- bracedExpr varsNum vars
   kw kwIn
   let vars' = HashMap.insert (name ^. nameText) varsNum vars
+      binder = Binder (Just name) (fromMaybe mkDynamic' mty)
   body <- bracedExpr (varsNum + 1) vars'
-  return $ mkLet (binderInfo name (fromMaybe mkDynamic' mty)) value body
+  return $ mkLet mempty binder value body
 
 exprCase ::
   Members '[InfoTableBuilder, NameIdGen] r =>
@@ -820,12 +822,12 @@ caseMatchingBranch varsNum vars = do
   txt <- identifier
   r <- lift (getIdent txt)
   case r of
-    Just (IdentFun {}) ->
+    Just IdentFun {} ->
       parseFailure off ("not a constructor: " ++ fromText txt)
-    Just (IdentInd {}) ->
+    Just IdentInd {} ->
       parseFailure off ("not a constructor: " ++ fromText txt)
     Just (IdentConstr tag) -> do
-      ns <- P.many parseLocalName
+      ns :: [Name] <- P.many parseLocalName
       let bindersNum = length ns
       ci <- lift $ getConstructorInfo tag
       when
@@ -841,8 +843,9 @@ caseMatchingBranch varsNum vars = do
                 (vars, varsNum)
                 ns
       br <- bracedExpr (varsNum + bindersNum) vars'
-      let info = setInfoName (ci ^. constructorName) $ setInfoBinders (map (Info.singleton . NameInfo) ns) Info.empty
-      return $ CaseBranch info tag bindersNum br
+      let info = setInfoName (ci ^. constructorName) mempty
+          binders = [Binder (Just name) mkDynamic' | name <- ns]
+      return $ CaseBranch info tag binders bindersNum br
     Nothing ->
       parseFailure off ("undeclared identifier: " ++ fromText txt)
 
@@ -894,14 +897,15 @@ matchBranch patsNum varsNum vars = do
   kw kwAssign
   unless (length pats == patsNum) $
     parseFailure off "wrong number of patterns"
-  let pis = concatMap (reverse . getBinderPatternInfos) pats
-  let (vars', varsNum') =
+  let pis :: [Binder]
+      pis = concatMap (reverse . getBinderPatternInfos) pats
+      (vars', varsNum') =
         foldl'
           ( \(vs, k) name ->
               (HashMap.insert (name ^. nameText) k vs, k + 1)
           )
           (vars, varsNum)
-          (map (fromJust . getInfoName) pis)
+          (map (fromJust . (^. binderName)) pis)
   br <- bracedExpr varsNum' vars'
   return $ MatchBranch Info.empty (fromList pats) br
 
@@ -939,7 +943,8 @@ binderOrConstrPattern parseArgs = do
       n <- lift $ freshName KNameLocal txt i
       mp <- optional binderPattern
       let pat = fromMaybe (PatWildcard (PatternWildcard Info.empty)) mp
-      return $ PatBinder (PatternBinder (setInfoName n Info.empty) pat)
+          binder = Binder (Just n) mkDynamic'
+      return $ PatBinder (PatternBinder binder pat)
 
 binderPattern ::
   Members '[InfoTableBuilder, NameIdGen] r =>