refine if: create sym val only when test is sym bool

turnstile/examples/rosette/rosette2.rkt

@@ -491,10 +491,14 @@
 ;; ---------------------------------
 ;; if
 
+;; TODO: this is not precise enough
+;; specifically, a symbolic non-bool should produce a concrete val
 (define-typed-syntax if
   [(_ e_tst e1 e2) ≫
    [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]]
-   #:when (concrete? #'ty_tst)
+   #:when (or (concrete? #'ty_tst) ; either concrete
+              ; or non-bool symbolic
+              (not (typecheck? #'ty_tst ((current-type-eval) #'Bool))))
    [⊢ [e1 ≫ e1- ⇒ : ty1]]
    [⊢ [e2 ≫ e2- ⇒ : ty2]]
    #:when (and (concrete? #'ty1) (concrete? #'ty2))

turnstile/examples/tests/rosette/rosette2-tests.rkt

@@ -107,6 +107,7 @@
  #:with-msg "Constant requires a symbolic type")
 (check-type b0 : Bool -> b0)
 (check-type b0 : (Constant Bool) -> b0)
+(check-not-type b0 : CBool)
 (check-type i0 : Int -> i0)
 (check-type i0 : (Constant Int) -> i0)
 (check-type (if b0 1 2) : Int)