exclude #f not always work for Option type

[dannypsnl]

What version of Racket are you using?

8.1 or later [CS]

What program did you run?

(define-type F (Option (-> Void)))

(: foo : F -> Void)
(define (foo f)
  (match f
    [#f (void)]
    [f (f)]))

What should have happened?

type check pass as the following program

(define-type F (Option (-> Void)))

(: foo : F -> Void)
(define (foo f)
  (when f
    (f)))

If you got an error message, please include it here.

Type Checker: Cannot apply expression of type F, since it is not a function type in: (f)

[AlexKnauth]

This is a limitation of match... and the reason Typed Racket doesn't do better here is because the macro is written to allow the user to fail within a match clause body with failure-cont, for example in this normal racket usage of match:

(define (foo f)
  (match f
    [#f (failure-cont)]
    [f (f)]))
(foo #f)

It runs the last case (f) even when f is #f, because the first case aborted in the body. These kinds of features in normal racket's match, and the ways the macro organizes the code to accommodate for them, make the typechecking of match more limited.

[capfredf]

An equivalent problem would be

(: foo : F -> Void)
(define (foo f)
  (if (equal? f #f) (void)
      (f)))

The reason those problem don't type-check as expected is the type of equal? doesn't have any propositions to help refine f's type.

[shhyou]

The expansion is different from the above program though:

(: foo : F -> Void)
(define (foo f)
  (let ([continuation (lambda () (f))])
    (if (equal? f #f)
        (void)
        (continuation))))

Can this program really typecheck?

[samth]

Typed Racket has some tricks to try to make some things like this typecheck, and could do more (obviously we could just inline that function and then typecheck) but it has not seemed like the right thing to do.

[capfredf]

I was about to post the expanded code. @shhyou and @AlexKnauth are right. equal? can be improved, but given that f is a F, there is no way to make the original code type check except for some magic done at TR level