better checks for pred?s in debug

turnstile/examples/rosette/query/debug.rkt

@@ -26,9 +26,15 @@
               (t/ro:ann (t/ro:begin e ...) : ty_out))))]])
 
 (define-typed-syntax debug
-  [(_ (solvable-pred ...+) e) ≫
-   [⊢ solvable-pred ≫ solvable-pred- ⇐ (t/ro:C→ t/ro:Nothing t/ro:Bool)] ...
+  [(_ (pred? ...+) e) ≫
+   [⊢ [pred? ≫ pred?- (⇒ : _) (⇒ typefor ty) (⇒ solvable? s?) (⇒ function? f?)]] ...
+   #:fail-unless (stx-andmap syntax-e #'(s? ...))
+                 (format "Must provide a Rosette-solvable type, given ~a." 
+                         (syntax->datum #'(pred? ...)))
+   #:fail-when (stx-ormap syntax-e #'(f? ...))
+               (format "Must provide a non-function Rosette type, given ~a." 
+                       (syntax->datum #'(pred? ...)))
    [⊢ [e ≫ e- ⇒ : τ]]
    --------
-   [⊢ [_ ≫ (ro:debug (solvable-pred- ...) e-) ⇒ : t/ro:CSolution]]])
+   [⊢ [_ ≫ (ro:debug (pred?- ...) e-) ⇒ : t/ro:CSolution]]])
   

turnstile/examples/rosette/rosette-notes.txt

@@ -84,6 +84,7 @@ TODOs:
 - orig stx prop confuses distinction between symbolic and non-sym values
 - use variance information in type constructors?
   - instead of special-casing individual constructors
+- ok to say "Rosette type" in type err msgs?
 
 2016-08-25 --------------------
 

turnstile/examples/tests/rosette/rosette-guide-sec2-tests.rkt

@@ -103,6 +103,10 @@
   (* x (+ x 1) (+ x 2) (+ x 2)))
 
 (define ucore (debug [integer?] (same poly factored/d 12)))
+(typecheck-fail (debug [positive?] (same poly factored/d 12))
+ #:with-msg "Must provide a Rosette-solvable type, given.*positive?")
+(typecheck-fail (debug [(~> integer?)] (same poly factored/d 12))
+ #:with-msg "Must provide a non-function Rosette type, given.*~> integer?")
 (check-type ucore : CSolution)
 ;; TESTING TODO: requires visual inspection (in DrRacket)
 (check-type (render ucore) : CPict)