simple integer refinement totality check

It seems reasonable to expect Typed Racket to succeed in checking the following program:

#lang typed/racket #:with-refinements

(define-type SomeInts (Refine [n : Byte] (<= #x13 n #x15)))

    
(: foo (-> SomeInts Symbol))
(define (foo x)
  (case x
    [(#x13) 'RemoteUserTerminated]
    [(#x14) 'RemoteDeviceTerminatedLowResources]
    [(#x15) 'RemoteDeviceTerminatedPowerOff]))

i.e. although there's a nasty implicit else (void) that is inserted by the case macro, we should be able to prove that code is dead. Instead, we get this error message:

Type Checker: type mismatch
  expected: Symbol
  given: Void in: (case x ((19) (quote RemoteUserTerminated)) ((20) (quote RemoteDeviceTerminatedLowResources)) ((21) (quote RemoteDeviceTerminatedPowerOff)))