diff --git a/exec/Main.hs b/exec/Main.hs
--- a/exec/Main.hs
+++ b/exec/Main.hs
@@ -26,7 +26,7 @@
                 (   fullDesc
                 <>  header "morte resolve - Resolve Morte code"
                 <>  progDesc "Transitively replace all remote paths and URLs \
-                             \with the code that they refer to, reading the\
+                             \with the code that they refer to, reading the \
                              \program from standard input and writing the \
                              \fully resolved program to standard output."
                 )
diff --git a/morte.cabal b/morte.cabal
--- a/morte.cabal
+++ b/morte.cabal
@@ -1,8 +1,8 @@
 Name: morte
-Version: 1.6.0
+Version: 1.6.1
 Cabal-Version: >=1.8.0.2
 Build-Type: Simple
-Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2
+Tested-With: GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.2, GHC == 8.0.1
 License: BSD3
 License-File: LICENSE
 Copyright: 2014 Gabriel Gonzalez
@@ -36,7 +36,7 @@
     Build-Depends:
         base                 >= 4        && < 5   ,
         array                >= 0.4.0.0  && < 0.6 ,
-        binary               >= 0.7.0.0  && < 0.8 ,
+        binary               >= 0.7.0.0  && < 0.9 ,
         containers           >= 0.5.0.0  && < 0.6 ,
         deepseq              >= 1.3.0    && < 1.5 ,
         Earley               >= 0.10.1.0 && < 0.12,
@@ -58,7 +58,6 @@
         Morte.Parser,
         Morte.Tutorial
     Build-Tools: alex
-    GHC-Options: -O2
 
 Executable morte
     Hs-Source-Dirs: exec
@@ -73,7 +72,7 @@
     Type: exitcode-stdio-1.0
     HS-Source-Dirs: bench
     Main-Is: Main.hs
-    GHC-Options: -O2 -Wall
+    GHC-Options: -Wall
     Build-Depends:
         base            >= 4        && < 5  ,
         criterion       >= 1.0.0.1  && < 1.2,
@@ -86,7 +85,7 @@
     HS-Source-Dirs: test
     Main-Is:        Main.hs
     Other-Modules:  ClosedWellTyped
-    GHC-Options:    -O2 -Wall
+    GHC-Options:    -Wall
     Build-Depends:
         base             >= 4        && < 5   ,
         mtl              >= 2.2      && < 2.3 ,
diff --git a/src/Morte/Core.hs b/src/Morte/Core.hs
--- a/src/Morte/Core.hs
+++ b/src/Morte/Core.hs
@@ -298,21 +298,26 @@
         go (Lam xL tL bL) (Lam xR tR bR) = do
             ctx <- State.get
             eq1 <- go tL tR
-            State.put ((xL, xR):ctx)
-            eq2 <- go bL bR
-            State.put ctx
-            return (eq1 && eq2)
+            if eq1
+                then do
+                    State.put ((xL, xR):ctx)
+                    eq2 <- go bL bR
+                    State.put ctx
+                    return eq2
+                else return False
         go (Pi xL tL bL) (Pi xR tR bR) = do
             ctx <- State.get
             eq1 <- go tL tR
-            State.put ((xL, xR):ctx)
-            eq2 <- go bL bR
-            State.put ctx
-            return (eq1 && eq2)
+            if eq1
+                then do
+                    State.put ((xL, xR):ctx)
+                    eq2 <- go bL bR
+                    State.put ctx
+                    return eq2
+                else return False
         go (App fL aL) (App fR aR) = do
             b1 <- go fL fR
-            b2 <- go aL aR
-            return (b1 && b2)
+            if b1 then go aL aR else return False
         go (Embed pL) (Embed pR) = return (pL == pR)
         go _ _ = return False
 
@@ -611,7 +616,7 @@
 normalize :: Expr a -> Expr a
 normalize e = case e of
     Lam x _A b -> case b' of
-        App f a -> case a of
+        App f a -> case a' of
             Var v' | v == v' && not (v `freeIn` f) ->
                 shift (-1) x f  -- Eta reduce
                    | otherwise                     ->
@@ -619,6 +624,8 @@
               where
                 v = V x 0
             _                                      -> e'
+          where
+            a' = whnf a
         _       -> e'
       where
         b' = normalize b