diff --git a/atp-haskell.cabal b/atp-haskell.cabal
--- a/atp-haskell.cabal
+++ b/atp-haskell.cabal
@@ -1,5 +1,5 @@
 Name:             atp-haskell
-Version:          1.14
+Version:          1.14.1
 Synopsis:         Translation from Ocaml to Haskell of John Harrison's ATP code
 Description:      This package is a liberal translation from OCaml to Haskell of
                   the automated theorem prover written in OCaml in
@@ -15,13 +15,14 @@
 Cabal-version:    >= 1.9
 Build-Type:       Simple
 Extra-Source-Files: tests/Extra.hs, .travis.yml, .ghci
-Tested-With:      GHC == 7.10.3, GHC == 7.11.*
+Tested-With:      GHC == 7.10.3, GHC == 7.11.*, GHC == 8.6.5
 
 Source-Repository head
   type: git
   location: https://github.com/seereason/atp-haskell
 
 Library
+  Default-Language: Haskell2010
   Build-Depends:
     applicative-extras,
     base >= 4.8 && < 5,
@@ -91,6 +92,7 @@
     -- Data.Logic.ATP.Limitations
 
 Test-Suite atp-haskell-tests
+  Default-Language: Haskell2010
   Type: exitcode-stdio-1.0
   Hs-Source-Dirs: tests
   Main-Is: Main.hs
diff --git a/src/Data/Logic/ATP/Prop.hs b/src/Data/Logic/ATP/Prop.hs
--- a/src/Data/Logic/ATP/Prop.hs
+++ b/src/Data/Logic/ATP/Prop.hs
@@ -1087,8 +1087,8 @@
 simpcnf ca fm =
     foldPropositional (\_ _ _ -> go) (\_ -> go) tf (\_ -> go) fm
     where
-      tf False = Set.empty
-      tf True = singleton Set.empty
+      tf False = singleton Set.empty
+      tf True = Set.empty
       go = let cjs = Set.filter (not . trivial) (purecnf ca fm) in
            Set.filter (\c -> not (setAny (\c' -> Set.isProperSubsetOf c' c) cjs)) cjs
 
@@ -1103,9 +1103,22 @@
 test35 = TestCase $ assertEqual "cnf (p. 61)" expected input
     where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))
           expected = ("(p∨q)∧(p∨r)∧(¬p∨¬r)", True)
+          fm :: PFormula Prop
           fm = (p .|. q .&. r) .&. (((.~.)p) .|. ((.~.)r))
           [p, q, r] = [Atom (P "p"), Atom (P "q"), Atom (P "r")]
 
+test36, test37 :: Test
+test36 = TestCase $ assertEqual "cnf (trivial case: False)" expected input
+    where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))
+          expected = ("⊥", True)
+          fm :: PFormula Prop
+          fm = F
+test37 = TestCase $ assertEqual "cnf (trivial case: True)" expected input
+    where input = (prettyShow (cnf' fm), tautology (Iff fm (cnf' fm)))
+          expected = ("⊤", True)
+          fm :: PFormula Prop
+          fm = T
+
 testProp :: Test
 testProp = TestLabel "Prop" $
            TestList [test00, test01, test02, test03, test04, {-test05,-}
@@ -1114,4 +1127,5 @@
                      test16, test17, test18, test19, test20,
                      test21, test22, test23, test24, test25,
                      test26, test27, test28, test29, test30,
-                     test31, test32, test33, test34, test35]
+                     test31, test32, test33, test34, test35,
+                     test36, test37]
diff --git a/src/Data/Logic/ATP/Quantified.hs b/src/Data/Logic/ATP/Quantified.hs
--- a/src/Data/Logic/ATP/Quantified.hs
+++ b/src/Data/Logic/ATP/Quantified.hs
@@ -89,7 +89,7 @@
       co _ (:<=>:) _ = iffPrec
       ne _ = notPrec
       tf _ = leafPrec
-      at = precedence
+      at = (precedence :: Num a => AtomOf formula -> a)
 
 associativityQuantified :: forall formula. IsQuantified formula => formula -> Associativity
 associativityQuantified = foldQuantified qu co ne tf at