diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index 696c06a..2773b58 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -1042,16 +1042,50 @@
 (define-base-types CSolution CPict)
 
 (provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
-                            ; TODO: implement hash
                             [model : (C→ CSolution (CHashTable Any Any))]
                             [sat : (Ccase-> (C→ CSolution)
                                             (C→ (CHashTable Any Any) CSolution))]
                             [sat? : (C→ Any Bool)]
                             [unsat? : (C→ Any Bool)]
                             [unsat : (Ccase-> (C→ CSolution)
-                                              (C→ (CListof Bool) CSolution))]
-                            [forall : (C→ (CListof Any) Bool Bool)]
-                            [exists : (C→ (CListof Any) Bool Bool)]))
+                                              (C→ (CListof Bool) CSolution))]))
+
+;(define-rosette-primop forall : (C→ (CListof Any) Bool Bool))
+;(define-rosette-primop exists : (C→ (CListof Any) Bool Bool))
+(define-typed-syntax forall
+  [(_ vs body) ≫
+   [⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]]
+   #:fail-unless (Constant*? #'ty)
+   (format "Expected list of symbolic constants, given list of ~a" 
+           (type->str #'ty))
+   [⊢ [body ≫ body- ⇐ : Bool]]
+   --------
+   [⊢ [_ ≫ (ro:forall vs- body-) ⇒ : Bool]]]
+  [(_ vs body) ≫
+   [⊢ [vs ≫ vs- ⇒ : (~CList ~! ty ...)]]
+   #:fail-unless (stx-andmap Constant*? #'(ty ...))
+   (format "Expected list of symbolic constants, given list containing: ~a" 
+           (string-join (stx-map type->str #'(ty ...)) ", "))
+   [⊢ [body ≫ body- ⇐ : Bool]]
+   --------
+   [⊢ [_ ≫ (ro:forall vs- body-) ⇒ : Bool]]])
+(define-typed-syntax exists
+  [(_ vs body) ≫
+   [⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]]
+   #:fail-unless (Constant*? #'ty)
+   (format "Expected list of symbolic constants, given list of ~a" 
+           (type->str #'ty))
+   [⊢ [body ≫ body- ⇐ : Bool]]
+   --------
+   [⊢ [_ ≫ (ro:exists vs- body-) ⇒ : Bool]]]
+  [(_ vs body) ≫
+   [⊢ [vs ≫ vs- ⇒ : (~CList ~! ty ...)]]
+   #:fail-unless (stx-andmap Constant*? #'(ty ...))
+   (format "Expected list of symbolic constants, given list containing: ~a" 
+           (string-join (stx-map type->str #'(ty ...)) ", "))
+   [⊢ [body ≫ body- ⇐ : Bool]]
+   --------
+   [⊢ [_ ≫ (ro:exists vs- body-) ⇒ : Bool]]])
 
 (define-typed-syntax verify
   [(_ e) ≫
@@ -1071,7 +1105,7 @@
    --------
    [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]])
 
-
+;; TODO: enforce list of constants?
 (define-typed-syntax synthesize
   [(_ #:forall ie #:guarantee ge) ≫
    [⊢ [ie ≫ ie- ⇐ : (CListof Any)]]
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
index 79ca61c..068ac6d 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
@@ -231,6 +231,17 @@
 (define-symbolic a1 b1 integer?)
 (check-type (forall (list) (= a1 b1)) : Bool -> (= a1 b1))
 (define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
+(check-type (list 1) : (CListof PosInt))
+(check-type (list 1) : (CList PosInt))
+(typecheck-fail (exists (list 1) (= a1 b1)) 
+                #:with-msg "Expected list of symbolic constants, given list containing: PosInt")
+(typecheck-fail (exists (list (+ a1 b1)) (= a1 b1)) 
+                #:with-msg "Expected list of symbolic constants, given list containing: Int")
+(check-type (cons a1 (cons b (list))) : (CList (Constant Int) (Constant Bool)))
+(typecheck-fail (forall (list 1) (= a1 b1)) 
+                #:with-msg "Expected list of symbolic constants, given list containing: PosInt")
+(typecheck-fail (forall (list (+ a1 b1)) (= a1 b1)) 
+                #:with-msg "Expected list of symbolic constants, given list containing: Int")
 ; so the model has no bindings
 (define sol1 (solve (assert f1)))
 (check-type sol1 : CSolution)