diff --git a/examples/NanoFeldspar/Core.hs b/examples/NanoFeldspar/Core.hs
--- a/examples/NanoFeldspar/Core.hs
+++ b/examples/NanoFeldspar/Core.hs
@@ -146,10 +146,8 @@
 class    (Syntactic a, Domain a ~ FeldDomainAll, Type (Internal a)) => Syntax a
 instance (Syntactic a, Domain a ~ FeldDomainAll, Type (Internal a)) => Syntax a
 
--- | A predicate deciding which constructs can be shared. Variables, lambdas and literals are not
--- shared.
+-- | A predicate deciding which constructs can be shared. Lambdas and literals are not shared.
 canShare :: ASTF (FODomain FeldSyms Typeable Top) a -> Maybe (Dict (Top a))
-canShare (prjP (P::P (Variable :|| Top)) -> Just _) = Nothing
 canShare (prjP (P::P (CLambda Top))      -> Just _) = Nothing
 canShare (prj -> Just (Literal _)) = Nothing
 canShare _  = Just Dict
diff --git a/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs b/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs
--- a/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs
+++ b/src/Language/Syntactic/Sharing/SimpleCodeMotion.hs
@@ -81,10 +81,6 @@
     cnt (f :$ b) = cnt f + count a b
     cnt _        = 0
 
-nonTerminal :: AST dom a -> Bool
-nonTerminal (_ :$ _) = True
-nonTerminal _        = False
-
 -- | Environment for the expression in the 'choose' function
 data Env dom = Env
     { inLambda :: Bool  -- ^ Whether the current expression is inside a lambda
@@ -101,53 +97,60 @@
 independent pd env (f :$ a) = independent pd env f && independent pd env a
 independent _ _ _ = True
 
+isVariable :: PrjDict dom -> ASTF dom a -> Bool
+isVariable pd (Sym (prjVariable pd -> Just _)) = True
+isVariable pd _ = False
+
 -- | Checks whether a sub-expression in a given environment can be lifted out
 liftable :: PrjDict dom -> Env dom -> ASTF dom a -> Bool
-liftable pd env a = independent pd env a && heuristic
+liftable pd env a = independent pd env a && not (isVariable pd a) && heuristic
     -- Lifting dependent expressions is semantically incorrect
+    -- Lifting variables would cause `codeMotion` to loop
   where
-    heuristic =  nonTerminal a && (inLambda env || (counter env (ASTE a) > 1))
+    heuristic = inLambda env || (counter env (ASTE a) > 1)
 
+
+
+-- | A sub-expression chosen to be shared together with an evidence that it can actually be shared
+-- in the whole expression under consideration
+data Chosen dom a
+  where
+    Chosen :: InjDict dom b a -> ASTF dom b -> Chosen dom a
+
 -- | Choose a sub-expression to share
-choose
-    :: (AlphaEq dom dom dom [(VarId,VarId)])
+choose :: forall dom a
+    .  AlphaEq dom dom dom [(VarId,VarId)]
     => PrjDict dom
+    -> MkInjDict dom
     -> ASTF dom a
-    -> Maybe (ASTE dom)
-choose pd a = chooseEnv pd env a
+    -> Maybe (Chosen dom a)
+choose pd mkId a = chooseEnv initEnv a
   where
-    env = Env
+    initEnv = Env
         { inLambda     = False
         , counter      = \(ASTE b) -> count b a
         , dependencies = empty
         }
 
--- | Choose a sub-expression to share in an 'Env' environment
-chooseEnv :: forall dom a
-    .  PrjDict dom
-    -> Env dom
-    -> ASTF dom a
-    -> Maybe (ASTE dom)
-chooseEnv pd env a
-    | liftable pd env a = Just (ASTE a)
-chooseEnv pd env a = chooseEnvSub pd env a
+    chooseEnv :: Env dom -> ASTF dom b -> Maybe (Chosen dom a)
+    chooseEnv env b
+        | liftable pd env b = do
+            id <- mkId b a
+            return $ Chosen id b
+    chooseEnv env b = chooseEnvSub env b
 
--- | Like 'chooseEnv', but does not consider the top expression for sharing
-chooseEnvSub
-    :: PrjDict dom
-    -> Env dom
-    -> AST dom a
-    -> Maybe (ASTE dom)
-chooseEnvSub pd env (Sym lam :$ a)
-    | Just v <- prjLambda pd lam
-    = chooseEnv pd (env' v) a
-  where
-    env' v = env
-        { inLambda     = True
-        , dependencies = insert v (dependencies env)
-        }
-chooseEnvSub pd env (f :$ a) = chooseEnvSub pd env f `mplus` chooseEnv pd env a
-chooseEnvSub _ _ _ = Nothing
+    -- | Like 'chooseEnv', but does not consider the top expression for sharing
+    chooseEnvSub :: Env dom -> AST dom b -> Maybe (Chosen dom a)
+    chooseEnvSub env (Sym lam :$ b)
+        | Just v <- prjLambda pd lam
+        = chooseEnv (env' v) b
+      where
+        env' v = env
+            { inLambda     = True
+            , dependencies = insert v (dependencies env)
+            }
+    chooseEnvSub env (s :$ b) = chooseEnvSub env s `mplus` chooseEnv env b
+    chooseEnvSub _ _ = Nothing
 
 
 
@@ -161,7 +164,7 @@
     -> ASTF dom a
     -> State VarId (ASTF dom a)
 codeMotion pd mkId a
-    | Just (ASTE b) <- choose pd a, Just id <- mkId b a = share id b
+    | Just (Chosen id b) <- choose pd mkId a = share id b
     | otherwise = descend a
   where
     share :: InjDict dom b a -> ASTF dom b -> State VarId (ASTF dom a)
diff --git a/syntactic.cabal b/syntactic.cabal
--- a/syntactic.cabal
+++ b/syntactic.cabal
@@ -1,5 +1,5 @@
 Name:           syntactic
-Version:        1.3
+Version:        1.4
 Synopsis:       Generic abstract syntax, and utilities for embedded languages
 Description:    This library provides:
                 .