diff --git a/src/Language/Syntactic/Sharing/CodeMotion2.hs b/src/Language/Syntactic/Sharing/CodeMotion2.hs
--- a/src/Language/Syntactic/Sharing/CodeMotion2.hs
+++ b/src/Language/Syntactic/Sharing/CodeMotion2.hs
@@ -5,6 +5,7 @@
     , reifySmart2
     ) where
 
+import Control.Arrow
 import Control.Monad.State
 import Control.Monad.Reader
 import Control.Monad.Writer
@@ -23,7 +24,9 @@
 import Language.Syntactic.Constructs.Binding.HigherOrder
 import Language.Syntactic.Sharing.SimpleCodeMotion
 
-
+typeEq :: forall dom a b. (Typeable a, Typeable b) => ASTF dom a -> ASTF dom b -> Bool 
+typeEq a b | Just _ <- (gcast b :: Maybe (ASTF dom a)) = True
+typeEq _ _ = False
 
 isVariable :: PrjDict dom -> ASTF (NodeDomain dom) a -> Bool
 isVariable pd (Sym (C' (InjR (prjVariable pd -> Just _)))) = True
@@ -60,7 +63,10 @@
   where
     Node :: NodeId -> Node (Full a)
 
+instance Render Node where
+  renderSym (Node n) = showNode n
 
+
 type NodeDomain dom = (Node :+: dom) :|| Sat dom
 
 -- | A gathered sub-expression along with information used to decide where and
@@ -107,6 +113,7 @@
 
 lookupGS :: forall dom a
     .  ( AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
+       , ConstrainedBy (NodeDomain dom) Typeable
        , Equality dom)
     => GatherSet dom
     -> ASTF (NodeDomain dom) a
@@ -116,12 +123,16 @@
     look :: [Gathered dom] -> Maybe (Gathered dom)
     look [] = Nothing
     look (g:gs) | ASTB ge <- geExpr g
+                , Dict <- exprDictSub pTypeable ge
+                , Dict <- exprDictSub pTypeable e
                 , alphaEq ge e
+                , typeEq ge e
                 = Just g
     look (g:gs) = look gs
 
 updateGS :: forall dom
     .  ( AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
+       , ConstrainedBy (NodeDomain dom) Typeable
        , Equality dom)
     => GatherSet dom
     -> Gathered dom
@@ -136,9 +147,12 @@
     ins :: [Gathered dom] -> [Gathered dom]
     ins [] = [g]
     ins (x:xs) | ASTB xe <- geExpr x
-                , ASTB ge <- geExpr g
-                , alphaEq xe ge
-                = g : xs
+               , ASTB ge <- geExpr g
+               , Dict <- exprDictSub pTypeable xe
+               , Dict <- exprDictSub pTypeable ge
+               , alphaEq xe ge
+               , typeEq xe ge
+               = g : xs
     ins (x:xs) = x : ins xs
 
 emptyGS :: GatherSet dom
@@ -160,7 +174,7 @@
 
 
 runRebuild :: RebuildMonad dom a -> State VarId a
-runRebuild m = runReaderT m (Map.empty, Set.empty, [0])
+runRebuild m = runReaderT m (Map.empty, Set.empty, [])
 
 addBoundVar :: VarId -> RebuildMonad dom a -> RebuildMonad dom a
 addBoundVar v =  local (\(nm,vs,sn) -> (nm, Set.insert v vs, sn))
@@ -205,11 +219,6 @@
  
 type ShareInfo dom = (NodeId, ASTSAT (NodeDomain dom), GatherInfo)
 
-data ShareMaybe dom a
-  where
-    Share :: Sat dom b => VarId -> InjDict dom b a -> ASTF dom b -> ShareMaybe dom a
-    Not :: Sat dom b => ASTF dom b -> ShareMaybe dom a
-
 rebuild :: forall dom a
     .  ( ConstrainedBy dom Typeable
        , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
@@ -220,7 +229,7 @@
     -> Array NodeId (Gathered dom)
     -> ASTF (NodeDomain dom) a
     -> State VarId (ASTF dom a)
-rebuild pd mkId nodes (Sym (C' (InjL _))) = error ""
+rebuild pd mkId nodes (Sym (C' (InjL _))) = error "rebuild: root is a node"
 rebuild pd mkId nodes a = runRebuild $ rebuild' 0 a
   where
     nodeExpr :: NodeId -> ASTSAT (NodeDomain dom)
@@ -249,68 +258,99 @@
     -- not already been considered at a parent node. Otherwise we will not know
     -- what to do with that node.
     -- Implementation is pretty bizarre right now, but it should be replaced anyway.
-    nodesToConsider :: (NodeId -> Bool) -> Set.Set VarId -> [NodeId] -> [ShareInfo dom]
-    nodesToConsider f bv seenNodes = concatMap mkShareInfo (assocs nodes)
+    nodesToConsider :: NodeId -> (NodeId -> Bool) -> Set.Set VarId -> [NodeId] -> [ShareInfo dom]
+    nodesToConsider n f bv seenNodes = concatMap mkShareInfo (map (\n -> (n, nodes ! n)) (Set.elems (nodeDeps ! n)))
       where
         maximumBy' f [] = []
         maximumBy' f xs = [maximumBy f xs]
-        mkShareInfo (n,g) = map snd $ maximumBy' (compare `on` fst) $ map (\(Just i,x) -> (i,x)) $ filter ((/=Nothing) . fst)
+
+        mkShareInfo (n,g) = map snd $ filter ((/=Nothing) . fst) $ maximumBy' (compare `on` fst)
             [ (elemIndex il seenNodes, (n, geExpr g, gi))
             | (il,gi) <- geInfo g
-            --, i <- elemIndex il seenNodes
-                -- must be shared inside `il`
             , Set.null (freeVars n `Set.difference` bv)
                 -- any free variables in the sub-expression must be bound
+            , il /= n
+                -- this case handled separately
             , f n
             ]
 
+    -- Nodes which has the given node as its inner limit.
+    unshareableNodes :: NodeId -> AST (NodeDomain dom) b -> [ShareInfo dom]
+    unshareableNodes n (Sym s) = []
+    unshareableNodes n (s :$ Sym (C' (InjL (Node n'))))
+        | Just gi <- lookup n (geInfo (nodes ! n'))
+        = (n', geExpr (nodes ! n'), gi) : unshareableNodes n s
+        | Just gi <- lookup n' (geInfo (nodes ! n'))
+        = (n', geExpr (nodes ! n'), gi) : unshareableNodes n s
+    unshareableNodes n (b :$ s) = unshareableNodes n b
+
+    unshareable2Nodes :: Maybe VarId -> ASTF (NodeDomain dom) b -> [ShareInfo dom]
+    unshareable2Nodes Nothing  _ = []
+    unshareable2Nodes (Just v) a = go a []
+      where
+        go :: AST (NodeDomain dom) c -> [ShareInfo dom] -> [ShareInfo dom]
+        go (Sym s) l = l
+        go (s :$ Sym (C' (InjL (Node n')))) l
+            | Set.member v (freeVars n') = go s ((n', geExpr (nodes ! n'), undefined):l)
+            | otherwise                  = go s l
+
     rebuild' :: forall b
         .  NodeId
         -> ASTF (NodeDomain dom) b
         -> RebuildMonad dom (ASTF dom b)
-    rebuild' n (Sym (C' (InjR lam)) :$ ns@(Sym (C' (InjL (Node nb)))))
+    rebuild' n a@(Sym (C' (InjR lam)) :$ ns@(Sym (C' (InjL (Node nb)))))
         | Just v <- prjLambda pd lam
-        = case geExpr (nodes ! nb) of
-            ASTB a
-              | Dict <- exprDictSub pTypeable ns
-              , Dict <- exprDictSub pTypeable a
-              -> case gcast a of
-                Nothing -> error "rebuild: type mistmatch"
-                Just a -> do
-                    a' <- addBoundVar v $ addSeenNode n $ rebuild' nb a
-                    return (Sym lam :$ a')
+        = addSeenNode n $ shareExprsIn (Just v) n a
     rebuild' n (Sym (C' (InjR s))) = return $ Sym s
-    rebuild' n a = addSeenNode n $ shareExprsIn n a
+    rebuild' n a = addSeenNode n $ shareExprsIn Nothing n a
 
     shareExprsIn :: forall b
-        .  NodeId
+        .  Maybe VarId -- if the last argument is a lambda, this contains the lambda VarId, otherwise Nothing.
+        -> NodeId
         -> ASTF (NodeDomain dom) b
         -> RebuildMonad dom (ASTF dom b)
-    shareExprsIn n a = do
+    shareExprsIn mlv n a = do
         bv <- getBoundVars
         seenNodes <- getSeenNodes
         nodeMap <- getNodeExprMap
-        let considered = nodesToConsider (\n' -> n' /= n && not (Map.member n' nodeMap) && Set.member n' (nodeDeps ! n)) bv seenNodes
+        let considered = nodesToConsider n (\n' -> n' /= n && not (Map.member n' nodeMap) && Set.member n' (nodeDeps ! n)) bv seenNodes
         let sorted = sortBy (compare `on` (\(n,_,_) -> n)) considered
-        shareEm sorted a
+        let unshareable = nubBy ((==) `on` (\(n,_,_) -> n)) $ unshareableNodes n a ++ unshareable2Nodes mlv a
+        unshare mlv unshareable $ shareEm mlv sorted a
 
+    unshare :: Maybe VarId -> [ShareInfo dom] -> RebuildMonad dom b -> RebuildMonad dom b
+    unshare mlv []     m = m
+    unshare mlv ((n, ASTB b, gi):sis) m = do
+          b' <- rebuildMaybeUnderLambda mlv n b
+          addNodeExpr n (ASTB b') $ unshare mlv sis m
+
     shareEm
-        :: [ShareInfo dom]
+        :: Maybe VarId
+        -> [ShareInfo dom]
         -> ASTF (NodeDomain dom) b
         -> RebuildMonad dom (ASTF dom b)
-    shareEm [] a = fixNodeExprSub a
-    shareEm ((n, be@(ASTB b), gi) : sis) a = do
-        b' <- rebuild' n b
+    shareEm mlv [] a = fixNodeExprSub a
+    shareEm mlv ((n, ASTB b, gi) : sis) a = do
         bv <- getBoundVars
-        case mkId b' (inlineAll nodeExpr a) of
-            Just id | heuristic bv gi a -> do
+        case mkId (inlineAll nodeExpr b) (inlineAll nodeExpr a) of
+            Just id | heuristic bv gi b -> do
+                b' <- rebuild' n b
                 v <- get; put (v+1)
-                a' <- addNodeExpr n (ASTB (Sym (injVariable id v))) $ shareEm sis a
+                a' <- addNodeExpr n (ASTB (Sym (injVariable id v))) $ shareEm mlv sis a
                 return $ Sym (injLet id) :$ b' :$ (Sym (injLambda id v) :$ a')
             _ -> do
-                a' <- addNodeExpr n (ASTB b') $ shareEm sis a
+                b' <- rebuildMaybeUnderLambda mlv n b
+                a' <- addNodeExpr n (ASTB b') $ shareEm mlv sis a
                 return a'
 
+    rebuildMaybeUnderLambda 
+        :: Maybe VarId
+        -> NodeId
+        -> ASTF (NodeDomain dom) b
+        -> RebuildMonad dom (ASTF dom b)
+    rebuildMaybeUnderLambda (Just lv) n a = addBoundVar lv $ rebuild' n a
+    rebuildMaybeUnderLambda Nothing   n a = rebuild' n a
+
     fixNodeExprSub :: forall b
         .  ( ConstrainedBy dom Typeable
            , AlphaEq dom dom (NodeDomain dom) [(VarId,VarId)]
@@ -337,7 +377,7 @@
                 -> case gcast a of
                     Nothing -> error "rebuild: type mismatch"
                     Just a -> a
-            Nothing -> error "rebuild: lost node"
+            Nothing -> error ("rebuild: lost node: " ++ show n)
 
     heuristic :: Set.Set VarId -> GatherInfo -> ASTF (NodeDomain dom) b -> Bool
     heuristic bv gi b = not (isVariable pd b) && (giCount gi > 1 || not (Set.null (giScopes gi `Set.difference` bv)))
@@ -380,6 +420,7 @@
 data LambdaInfo dom = LambdaInfo
     { liExpr :: ASTSAT dom
     , liLambdaNodeId :: NodeId
+    , liFreeVars :: Set.Set VarId
     }
 
 type GatherMonad dom a = RWS GatherEnv (Set.Set VarId) (GatherState dom) a
@@ -414,13 +455,14 @@
     => Hash
     -> ASTF dom a
     -> NodeId
+    -> Set.Set VarId
     -> LambdaTable dom
     -> LambdaTable dom
-insertLT h e n t = updateWithHS ins h t
+insertLT h e n fv t = updateWithHS ins h t
   where
     ins :: Maybe [LambdaInfo dom] -> Maybe [LambdaInfo dom]
-    ins (Just xs) = Just (LambdaInfo (ASTB e) n : xs)
-    ins Nothing = Just [LambdaInfo (ASTB e) n]
+    ins (Just xs) = Just (LambdaInfo (ASTB e) n fv : xs)
+    ins Nothing = Just [LambdaInfo (ASTB e) n fv]
 
 
 getInnerLimit :: GatherMonad dom NodeId
@@ -459,8 +501,14 @@
 gather hoistOver pd a@(Sym s) | Dict <- exprDict a = (array (1,0) [], Sym (C' (InjR s)))
 gather hoistOver pd a = (gatheredArr, a')
   where
-    (st,a') | Dict <- exprDict a = runGather (gatherRec (hoistOver a) a)
+    (st,a') | Dict <- exprDict a = runGather (gatherRoot a)
 
+    gatherRoot :: ASTF dom b -> GatherMonad dom (ASTF (NodeDomain dom) b)
+    gatherRoot a@(Sym lam :$ _) | Just v <- prjLambda pd lam
+                                , Dict <- exprDict a 
+                                = addScopeVar v $ gatherRec (hoistOver a) a
+    gatherRoot a | Dict <- exprDict a = gatherRec (hoistOver a) a
+
     gths = toListGS (gatherSet st)
 
     idx = map geNodeId gths
@@ -487,16 +535,21 @@
                 (Map.findWithDefault [] (geNodeId g) propagateAdditionals)
 
     propagateAdditionals :: Additional
-    propagateAdditionals = propAddsExpr 0 a' $ additionals st
+    propagateAdditionals = foldr propAdditional (additionals st) $ Map.toDescList (additionals st) 
       where
-        propAddsNode :: NodeId -> Additional -> Additional
-        propAddsNode n ad = liftASTB (propAddsExpr n) (geExpr (preGatheredArr ! n)) ad
+        propAdditional :: (NodeId, [(NodeId, GatherInfo)]) -> Additional -> Additional
+        propAdditional (n, gi) ad = propAdditionalNode n gi ad
 
-        propAddsExpr :: NodeId -> AST (NodeDomain dom) b -> Additional -> Additional
-        propAddsExpr n (Sym s) ad = ad
-        propAddsExpr n (s :$ Sym (C' (InjL (Node n')))) ad = propAddsNode n' ad'
+        propAdditionalNode :: NodeId -> [(NodeId, GatherInfo)] -> Additional -> Additional
+        propAdditionalNode n gi ad = liftASTB (propAdditionalExpr n gi) (geExpr (preGatheredArr ! n)) ad
+
+        propAdditionalExpr :: NodeId -> [(NodeId, GatherInfo)] -> AST (NodeDomain dom) b -> Additional -> Additional
+        propAdditionalExpr n gi (Sym s) ad = ad
+        propAdditionalExpr n gi (s :$ Sym (C' (InjL (Node n')))) ad = ad3
           where
-            ad' = Map.insertWith mergeInfos n' (Map.findWithDefault [] n ad) ad
+            ad1 = Map.insertWith mergeInfos n' gi ad
+            ad2 = propAdditionalNode n' gi ad1
+            ad3 = propAdditionalExpr n gi s ad2
 
     applyAdditionals :: [(NodeId, GatherInfo)] -> Gathered dom -> Gathered dom
     applyAdditionals ad g = g { geInfo = mergeInfos ad (geInfo g) }
@@ -504,25 +557,30 @@
     varHash :: Map.Map VarId Hash
     varHash = lambdaHashes pd a
 
-    gather' :: Bool -> ASTF dom b -> GatherMonad dom (ASTF (NodeDomain dom) b)
+    gather' 
+        :: Bool
+        -> ASTF dom b
+        -> GatherMonad dom (ASTF (NodeDomain dom) b)
     gather' h a@(Sym lam :$ _) | Just v <- prjLambda pd lam
                                , Dict <- exprDict a = do
         lt <- getLambdaTable
         let hash = fromJust (Map.lookup v varHash)
         case lookupLT hash a lt of
             Just li -> do
-                anotherCopyOf (liLambdaNodeId li)
-                return $ Sym $ C' $ InjL $ Node $ liLambdaNodeId li
+                let n = liLambdaNodeId li
+                anotherCopyOf n
+                tell (liFreeVars li)
+                return $ Sym $ C' $ InjL $ Node $ n
             Nothing -> do
                 rec
                     (a',fv) <- listen $ addInnerLimitIf (not h) n $ addScopeVar v $ gatherRec (hoistOver a) a
-                    n <- recordExpr fv a'
-                putLambdaTable (insertLT hash a n lt)
+                    n <- addInnerLimitIf (not h) n $ recordExpr fv a'
+                putLambdaTable (insertLT hash a n fv lt)
                 return $ Sym $ C' $ InjL $ Node n
     gather' h a | Dict <- exprDict a = do
         rec
             (a',fv) <- listen $ addInnerLimitIf (not h) n $ gatherRec (hoistOver a) a
-            n <- recordExpr fv a'
+            n <- addInnerLimitIf (not h) n $ recordExpr fv a'
         return $ Sym $ C' $ InjL $ Node n
 
     addInnerLimitIf True n m = addInnerLimit n m
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        1.13
+Version:        1.14
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .