Error messages (or something) going on with `verify-contract`

[dbp]

So this involves strings, so I expect it not to work (unless Rosette can do some magic and figure out they are constants, but...), but the error is not helpful:

(: letter-grade (-> Integer String))
(define (letter-grade n)
  (cond [(>= n 90) "A"]
        [(>= n 80) "B"]
        [(>= n 70) "C"]
        [(>= n 60) "D"]
        [else "F"]))
(check-contract letter-grade)

(: letter-grade-prop (-> Integer True))
(define (letter-grade-prop n)
  (let ([l (letter-grade n)])
    (member? l (list "A" "B" "C" "D" "F"))))
(check-contract letter-grade-prop)

(verify-contract letter-grade-prop)

Produces:

--------------------
unit tests > Unnamed test
FAILURE
name:       verify-contract
location:   /Users/dbp/code/lsl/lsl-lib/main.rkt:371:19
params:     '(#<procedure:...sl/lsl-lib/main.rkt:371:36>)

letter-grade-prop: contract violation
  expected: True
  given: #f
  blaming: /Users/dbp/teaching/logics24/website/lectures/6.rkt
--------------------
2 success(es) 1 failure(s) 0 error(s) 3 test(s) run

[camoy]

So this actually does verify because Rosette will represent the output of letter-grade as an exact union. It didn't do so only because member wasn't lifted so the symbolic union was causing an error. You're right, though, that we could do something better about the error. It's not exactly wrong, per se, since it is showing the value that makes the contract fail. However, it isn't showing the generated values that eventually caused the error. We'll have to think more carefully about how to best display that information because in general there may be many generated values.