[racket] occurrence typing for case?

From: Alexander D. Knauth (alexander at knauth.org)
Date: Sun May 11 19:10:03 EDT 2014

It seems like case doesn’t do occurrence typing, when it seems like it would be easiest for case, because of singleton types.  
For example:
#lang typed/racket

(define (f x)
  (case x
    [(thing) (g x)]
    ))

(: g ('thing -> 'thing))
(define (g x) x)

Gives me this:
. Type Checker: type mismatch
  expected: 'thing
  given: Any in: x

This isn’t much of a problem (I can easily just do a cast), but It just seems like it should be really easy for typed racket to figure out that x has the type ‘thing if it gets into that clause.  

By the way is there something like case/type that would be something like this?:
(case/type x
  [Type-1 body …]
  [Type-2 body …]
  …
  )
And would use (make-predicate Type) to do it so that it would do occurrence typing?  Maybe something like this:
(define-syntax-rule
  (case/type x-expr
    [t body …] …)
  (let ([x x-expr])
    (cond [((make-predicate t) x) body …] …))
  )

I tried it, but it didn’t work like I expected it to do with occurrence typing:
#lang typed/racket
(require typed/rackunit)

(define-syntax-rule
  (case/type x-expr
    [t1 body ...] ...)
  (let ([x x-expr])
    (cond [((make-predicate t1) x) body ...] ...))
  )

(define (my-length x)
  (case/type x
    [String (string-length x)]
    [(Listof Any) ((inst length Any) x)]
    [VectorTop (vector-length x)]
    ))
(check-equal? (my-length "12345") 5)
(check-equal? (my-length '(1 2 3 4 5)) 5)
(check-equal? (my-length #(1 2 3 4 5)) 5)

It gave me these errors:
. Type Checker: type mismatch
  expected: String
  given: Any in: x
. Type Checker: type mismatch
  expected: (Listof Any)
  given: Any in: x
. Type Checker: type mismatch
  expected: VectorTop
  given: Any in: x

So I guess it didn’t do occurrence typing for that either, even though it uses make-predicate.  Is there anything I can do to help it do occurrence typing for this?

By the way why is length polymorphic?  

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140511/883d0421/attachment.html>

Posted on the users mailing list.