diff --git a/escher/Main.hs b/escher/Main.hs
index add2554..77fbd3f 100644
--- a/escher/Main.hs
+++ b/escher/Main.hs
@@ -10,7 +10,7 @@ import Data.Set (Set)
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Data.List (inits)
-import Data.Maybe (fromMaybe, isJust, maybeToList)
+import Data.Maybe (fromMaybe, isJust, maybeToList, isNothing)
 
 import Debug.Trace (trace)
 import TypeCheck
@@ -54,12 +54,14 @@ matchAnyOutputs outputs = do exprs <- gets syntExprs
 -- generate next step of exprs, remove copies
 forwardStep :: Expr -> [Expr] -> SyntState (Maybe Expr)
 forwardStep comp args = do let expr = fillHoles comp args
-                           outputs <- calcExprOutputs expr
-                           matchedExisting <- gets $ evalState (matchAnyOutputs outputs)
-                           -- TODO: all RecErrors example could be useful on future cases ?
-                           if any isFatalError outputs || all isRecError outputs || matchedExisting then return Nothing else do
-                             modify $ \st -> st { syntExprs = (expr, []) : syntExprs st}
-                             return $ Just expr
+                           typeConf <- gets $ oracleTypes . syntOracle
+                           if isNothing $ checkType typeConf expr then return Nothing else do
+                             outputs <- calcExprOutputs expr
+                             matchedExisting <- gets $ evalState (matchAnyOutputs outputs)
+                             -- TODO: all RecErrors example could be useful on future cases ?
+                             if any isFatalError outputs || all isRecError outputs || matchedExisting then return Nothing else do
+                               modify $ \st -> st { syntExprs = (expr, []) : syntExprs st}
+                               return $ Just expr
 
 splitGoal :: Goal -> [Bool] -> Resolver
 splitGoal resolverGoal@(Goal outputs) selector | length outputs == length selector =
diff --git a/escher/TypeCheck.hs b/escher/TypeCheck.hs
index 876d9c2..fa984fb 100644
--- a/escher/TypeCheck.hs
+++ b/escher/TypeCheck.hs
@@ -18,6 +18,11 @@ isList x | ListT {} <- typeOf x = True
 isTree x | TreeT {} <- typeOf x = True
          | otherwise = False
 
+simpleUnify :: Type -> Type -> Maybe Type
+simpleUnify AnyT u = Just u
+simpleUnify t AnyT = Just t
+simpleUnify _ _ = Nothing
+
 checkType :: TypeConf -> Expr -> Maybe Type
 checkType conf (left :&&: right) = do BoolT <- checkType conf left
                                       BoolT <- checkType conf right
@@ -49,18 +54,22 @@ checkType conf ZeroE = return IntT
 checkType conf (Div2E e) = do IntT <- checkType conf e
                               return IntT
 checkType conf (TailE e) = do ListT t <- checkType conf e
+                              guard $ t /= AnyT -- NOTE: can't take tail from list that is provem empty (?)
+                                                -- TODO: check that AnyT is only for empty list & no bad consequences
                               return $ ListT t
 checkType conf (HeadE e) = do ListT t <- checkType conf e
+                              guard $ t /= AnyT -- NOTE: can't take elem from list that is provem empty (?)
+                                                -- TODO: check that AnyT is only for empty list & no bad consequences
                               return t
 checkType conf (left :++: right) = do ListT t <- checkType conf left
                                       ListT u <- checkType conf right
-                                      guard $ t == u
-                                      return $ ListT t
+                                      w <- simpleUnify t u
+                                      return $ ListT w
 checkType conf (left ::: right) = do t <- checkType conf left
                                      ListT u <- checkType conf right
-                                     guard $ t == u
-                                     return $ ListT t
-checkType conf EmptyListE = return $ ListT AnyT -- TODO FIXME: deal with AnyT
+                                     w <- simpleUnify t u
+                                     return $ ListT w
+checkType conf EmptyListE = return $ ListT AnyT -- NOTE: ListT AnyT - type of generic empty list
 checkType conf (IsLeafE e) = do TreeT _ <- checkType conf e
                                 return BoolT
 checkType conf (TreeValE e) = do TreeT t <- checkType conf e