Add `typecheck-fail' form for explicit type errors.

collects/tests/typed-racket/fail/explicit-fail.rkt

@@ -0,0 +1,14 @@
+#;
+(exn-fail "incomplete coverage; missing coverage of Negative-Integer")
+#lang typed/racket
+
+(define-syntax (cond* stx)
+  (syntax-case stx ()
+    [(_ x clause ...)
+     #`(cond clause ... [else (typecheck-fail #,stx "incomplete coverage" #:covered-id x)])]))
+
+(: f : (U String Integer) -> Boolean)
+(define (f x)
+  (cond* x
+         [(string? x) #t]
+         [(exact-nonnegative-integer? x) #f]))

collects/typed-racket/base-env/prims.rkt

@@ -822,3 +822,14 @@ This file defines two sorts of primitives. All of them are provided into any mod
         (cond c.cond-clause
               ...
               [else body ...]))]))
+
+(define-syntax (typecheck-fail stx)
+  (syntax-parse stx    
+    [(_ orig msg:str #:covered-id var:id)
+     #'(quote-syntax (typecheck-fail-internal orig msg var))]
+    [(_ orig msg:str)
+     #'(quote-syntax (typecheck-fail-internal orig msg #f))]
+    [(_ orig #:covered-id var:id)
+     #'(quote-syntax (typecheck-fail-internal orig "Incomplete case coverage" var))]
+    [(_ orig)
+     #'(quote-syntax (typecheck-fail-internal orig "Incomplete case coverage" #f))]))

collects/typed-racket/scribblings/reference/utilities.scrbl

@@ -43,4 +43,31 @@ program errors. These assertions behave like @racket[assert].
 @defproc[(index? [v any/c]) boolean?]{A predicate for the @racket[Index]
 type.}
 
+@defform*/subs[[(typecheck-fail orig-stx maybe-msg maybe-id)]
+               ([maybe-msg code:blank (code:line msg-string)]
+	        [maybe-id code:blank (code:line #:covered-id id)])]{
+Explicitly produce a type error, with the source location or
+@racket[orig-stx].  If @racket[msg-string] is present, it must be a literal string, it is used as
+the error message, otherwise the error message 
+@racket["Incomplete case coverage"] is used.
+If @racket[id] is present and has 
+type @racket[T], then the message @racket["missing coverage of T"] is added to
+the error message.   
+
+@examples[#:eval the-top-eval #:escape UNSYNTAX
+(define-syntax (cond* stx)
+  (syntax-case stx ()
+    [(_ x clause ...)
+     #`(cond clause ... [else (typecheck-fail #,stx "incomplete coverage"
+                                              #:covered-id x)])]))
+
+(define: (f [x  : (U String Integer)]) : Boolean
+  (cond* x
+         [(string? x) #t]
+         [(exact-nonnegative-integer? x) #f]))
+]
+
+}
+
 @(close-eval the-eval)
+@(close-eval the-top-eval)

collects/typed-racket/typecheck/internal-forms.rkt

@@ -17,5 +17,6 @@
  define-typed-struct/exec-internal
  assert-predicate-internal
  declare-refinement-internal
- :-internal)
+ :-internal
+ typecheck-fail-internal)
 

collects/typed-racket/typecheck/tc-expr-unit.rkt

@@ -14,7 +14,8 @@
          racket/private/class-internal
          (except-in syntax/parse id)
          unstable/function #;unstable/debug
-         (only-in srfi/1 split-at))
+         (only-in srfi/1 split-at)
+         (for-template "internal-forms.rkt"))
 
 (require (for-template scheme/base racket/private/class-internal))
 
@@ -229,6 +230,15 @@
                     (add-typeof-expr form t)
                     t)]))))
 
+(define (explicit-fail stx msg var)
+  (cond [(and (identifier? var) (lookup-type/lexical var #:fail (λ _ #f)))
+         =>
+         (λ (t)
+           (tc-error/expr #:return (ret (Un)) #:stx stx
+                          (string-append (syntax-e msg) "; missing coverage of ~a")
+                          t))]
+         [else (tc-error/expr #:return (ret (Un)) #:stx stx (syntax-e msg))]))
+
 ;; tc-expr/check : syntax tc-results -> tc-results
 (define/cond-contract (tc-expr/check/internal form expected)
   (--> syntax? tc-results? tc-results?)
@@ -255,6 +265,9 @@
            (unless ty
              (int-err "internal error: ignore-some"))
            (check-below ty expected))]
+        ;; explicit failure
+        [(quote-syntax ((~literal typecheck-fail-internal) stx msg:str var))
+         (explicit-fail #'stx #'msg #'var)]
         ;; data
         [(quote #f) (ret (-val #f) false-filter)]
         [(quote #t) (ret (-val #t) true-filter)]
@@ -349,7 +362,9 @@
          (unless ty
            (int-err "internal error: ignore-some"))
          ty)]
-
+      ;; explicit failure
+      [(quote-syntax ((~literal typecheck-fail-internal) stx msg var))
+       (explicit-fail #'stx #'msg #'var)]
       ;; data
       [(quote #f) (ret (-val #f) false-filter)]
       [(quote #t) (ret (-val #t) true-filter)]