Fix the stack trace of `check-expect` forms

[shhyou]

In #lang SLs, check-expect and similar forms are not annotated by errortrace. This PR adds the errortrace:annotate syntax property to request for annotation.

Before:

#lang htdp/isl+
;; error at test-engine/racket-tests.rkt:XXX:XX
(check-expect 0 zero?)
;; check failure at lang/private/teachprims.rkt:XXX:XX
(check-expect zero? 0)

After: error at line 3, column 0 and line 5, column 0.

---

In addition to stack trace fixes, this PR refines and fixes somes check-form error messages:

• check-random and check-expect should NOT have identical error messages.
• Have check-expect messages refer to "the second argument" like other check-forms.
• Format the third argument of check-within with ~s instead of ~a for otherwise strings like "NNN.mm" would be printed like numbers (i.e. just NNN.mm).

[mfelleisen]

Thanks for getting this started. I don't have time to review the changes inside the file yet but three of them raise questions already.

[mfelleisen]

Can you do me a favor and check in Guillaume's paper whether "advice on how to fix things should go into error messages"? My recollection is that we should not do so unless obvious. I consider the suggestion in the modified inexact error message non-obvious.

[shhyou]

Can you do me a favor and check in Guillaume's paper whether "advice on how to fix things should go into error messages"? My recollection is that we should not do so unless obvious. I consider the suggestion in the modified inexact error message non-obvious.

Sort of -- Guillaume Marceau (et al.) say

• Error messages should not propose solutions.

but also say that

The second warns against proposing corrections to syntax errors.

which is not directly targeting this error message. The suggestion in the message has been there since 2010, do you want to remove it?

[mfelleisen]

Yes.

This is probably around the time Kathy was handing it over and Guillaume was running his research. If we pay attention to such results we should remove all these suggestions …

[shhyou]

Tests added to module-lang-test.rkt in https://github.com/racket/drracket/pull/689.

[mikesperber]

@rfindler and I had a conversation about this issue at ICFP - Robby, could you look at this?

[shhyou]

Is this ready to be merged?

[rfindler]

I'm sorry, I've lost track of this conversation. I don't see any issues from a look at the diff, but if there is something specific I should be remembering, could you remind me @mikesperber ?