diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt
index d8adc5f..6893e73 100644
--- a/turnstile/examples/rosette/lib/synthax.rkt
+++ b/turnstile/examples/rosette/lib/synthax.rkt
@@ -12,8 +12,18 @@
    #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
    --------
    [⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]]
-  [(qq pred : ty:type) ≫
+  [(qq pred?) ≫
    #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
-   [⊢ [pred ≫ pred- ⇐ : (t/ro:C→ ty.norm t/ro:Bool)]]
+   [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]]
+   #:fail-unless (syntax-e #'s?)
+                 (format "Must provide a Rosette-solvable type, given ~a." 
+                         (syntax->datum #'pred?))
+   #:fail-when (syntax-e #'f?)
+               (format "Must provide a non-function Rosette type, given ~a." 
+                       (syntax->datum #'pred?))
    --------
-   [⊢ [_ ≫ (??/progsrc pred-) ⇒ : ty.norm]]])
+   [⊢ [_ ≫ (??/progsrc pred?-) ⇒ : ty]]])
+  
+(define-syntax print-forms
+  (make-variable-like-transformer
+   (assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
index f8eed48..10873f0 100644
--- a/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt
@@ -110,9 +110,18 @@
 ;; 2.3.3 Synthesis
 
 (require "../../rosette/lib/synthax.rkt")
+(check-type (??) : Int)
+(check-type (?? boolean?) : Bool)
+(typecheck-fail (?? positive?) 
+ #:with-msg "Must provide a Rosette-solvable type, given.*positive?")
+(typecheck-fail (?? (~> integer?))
+ #:with-msg "Must provide a non-function Rosette type, given.*integer?")
+
+
 (define (factored/?? [x : Int] -> Int)
  (* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??))))
 
+
 (define binding
   (synthesize #:forall (list i)
               #:guarantee (same poly factored/?? i)))