diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,3 +1,8 @@
+2024-01-07
+        * Version bump (3.18). (#487)
+        * Add type annotation to help type inference engine. (#469)
+        * Rename forall to forAll. (#470)
+
 2023-11-07
         * Version bump (3.17). (#466)
 
diff --git a/copilot-language.cabal b/copilot-language.cabal
--- a/copilot-language.cabal
+++ b/copilot-language.cabal
@@ -1,6 +1,6 @@
 cabal-version:       >=1.10
 name:                copilot-language
-version:             3.17
+version:             3.18
 synopsis:            A Haskell-embedded DSL for monitoring hard real-time
                      distributed systems.
 description:
@@ -42,9 +42,9 @@
                , data-reify            >= 0.6 && < 0.7
                , mtl                   >= 2.0 && < 3
 
-               , copilot-core          >= 3.17 && < 3.18
-               , copilot-interpreter   >= 3.17 && < 3.18
-               , copilot-theorem       >= 3.17 && < 3.18
+               , copilot-core          >= 3.18 && < 3.19
+               , copilot-interpreter   >= 3.18 && < 3.19
+               , copilot-theorem       >= 3.18 && < 3.19
 
   exposed-modules: Copilot.Language
                  , Copilot.Language.Operators.BitWise
diff --git a/src/Copilot/Language.hs b/src/Copilot/Language.hs
--- a/src/Copilot/Language.hs
+++ b/src/Copilot/Language.hs
@@ -37,6 +37,7 @@
   , arg
   , prop
   , theorem
+  , forAll
   , forall, exists
   ) where
 
diff --git a/src/Copilot/Language/Spec.hs b/src/Copilot/Language/Spec.hs
--- a/src/Copilot/Language/Spec.hs
+++ b/src/Copilot/Language/Spec.hs
@@ -27,6 +27,7 @@
   , Prop (..)
   , prop, properties
   , theorem, theorems
+  , forAll
   , forall, exists
   , extractProp
   , Universal, Existential
@@ -161,8 +162,13 @@
   Exists :: Stream Bool -> Prop Existential
 
 -- | Universal quantification of boolean streams over time.
+forAll :: Stream Bool -> Prop Universal
+forAll = Forall
+
+{-# DEPRECATED forall "Use forAll instead." #-}
+-- | Universal quantification of boolean streams over time.
 forall :: Stream Bool -> Prop Universal
-forall = Forall
+forall = forAll
 
 -- | Existential quantification of boolean streams over time.
 exists :: Stream Bool -> Prop Existential
diff --git a/tests/Test/Copilot/Language/Reify.hs b/tests/Test/Copilot/Language/Reify.hs
--- a/tests/Test/Copilot/Language/Reify.hs
+++ b/tests/Test/Copilot/Language/Reify.hs
@@ -31,7 +31,7 @@
 import qualified Copilot.Language.Operators.Mux      as Copilot
 import qualified Copilot.Language.Operators.Ord      as Copilot
 import           Copilot.Language.Reify              (reify)
-import           Copilot.Language.Spec               (observer)
+import           Copilot.Language.Spec               (Spec, observer)
 import           Copilot.Language.Stream             (Stream)
 import qualified Copilot.Language.Stream             as Copilot
 
@@ -732,7 +732,11 @@
 checkSemanticsP :: Int -> [a] -> SemanticsP -> IO Bool
 checkSemanticsP steps _streams (SemanticsP (expr, exprList)) = do
     -- Spec with just one observer of one expression.
-    let spec = observer testObserverName expr
+    --
+    -- Because SemanticsP is an existential type, we need to help GHC figure
+    -- out the type of spec.
+    let spec :: Spec
+        spec = observer testObserverName expr
 
     -- Reified stream (low-level)
     llSpec <- reify spec