[racket-dev] goofy type hack (was: Re: type-case + typed racket yet?)

On Wed, May 25, 2011 at 1:43 PM, John Clements
<clements at brinckerhoff.org> wrote:
> I see that typed racket doesn't signal an error on a match that doesn't have clauses for all possible inputs, which is entirely reasonable; since that will signal an error, that code should typecheck fine.
>
> However, I might *want* typed racket to check that for me.  I managed to come up with this grozzz hack:
>
> (: g ((U Number False) -> Number))
> (define (g x)
>  (cond [(number? x) (+ x 4)]
>        [(false? x) 13]
>        ;; type of x is now uninhabitable, so no typechecking error
>        [else (begin (string-append x "abc") (error 'foo))]))
>
> In this case, when I comment out the 'false?' clause, the bogus clause suddenly is type-checked (because x's type is no longer the empty union), and I get an error.
>
> So... I can get what I want, but in a very icky way.  Is there a different and more elegant way to force typed racket to check that I'm not failing to match?

I've thought about adding a (fail-to-typecheck) form, but haven't yet.

Unfortunately, coverage checking isn't always perfect, so that
programming style can become painful in Typed Racket.
-- 
sam th
samth at ccs.neu.edu