Representing the function EOF -> False, A -> A ∀ A ≠ EOF in Typed Racket?

Question

I am trying to define the type annotation for the following function in Typed Racket:

(define (neof x)
    (if (eof-object? x) #f x))

Leaving it un-annotated gives the type:

(Any -> Any)

Using this type produces an error:

(: neof (All (A) (case-> 
                  (EOF -> False)
                  (A -> A : #:+ (! EOF))))

  expected: A
  given: False
  in: #f

This is presumably because one can let A = EOF and then we get EOF -> EOF.

The type (: neof (All (A) A -> (U A False) #:- (U EOF False))), while not as clear as the above, also gives errors:

 mismatch in filter
   expected: (Top | Bot)
   given: ((! (U False EOF) @ x) | ((U False EOF) @ x))
   in: (if (eof-object? x) #f x)

My goal was to have a function which I could apply to any output from a port an get either False or the value from the port. I am now reconsidering the need for this, as I've blown way too much time trying to figure out this type.

For completeness, I also tried this definition of neof:

(define/match (neof x)
    [((? eof-object?)) #f]
    [((? (compose not eof-object?))) x])

(Also with the second pattern being _, but that doesn't encode the same amount of type information. At this point I'm more trying to appease the type checker than anything).

So: how can I represent the type of neof?

Answer 1

I think the type you want is this:

(: neof (All (A) (A -> (U False A) :
                    #:+ (! EOF)
                    #:- (or EOF False))))

(The #:- clause is optional, I just included it there for completeness.)

Note: If the #:- clause is included, it will not typecheck in Racket 6.1.1. Removing the clause will allow it to pass on 6.1.1.

The issue here is that all branches of case-> must typecheck independently of one another. For the (A -> A) case, it fails because #f is not an A. The occurrence typing information from the first case cannot influence typechecking on the second case.