[racket-dev] A more useful struct type predicate for structs with contravariant blah-de-blah?

A while ago, on PR 12903 (I don't know why it's not closed yet, FWIW, 
because I think it's fixed), we had this discussion:

Me: I think this should work.

#lang typed/racket

(struct: (A) bar ([proc : (A -> Any)]))
(define-predicate -bar? (bar Any))


Sam: That's evil; here's why. Suppose `bar` had a predicate with type 
(Any -> Boolean : (bar Any)). You could do this:

(define: v : Any (bar (lambda: ([x : Integer]) (add1 x))))
(when (my-bar? v) ;; check that `v` is a `(bar Any)`
   (define: f : (Any -> Any) (bar-proc v)) ;; type-correct: A = Any
   (f "not an integer"))


Me: Got it. [Consults this answer every time it comes up, because he 
forgets why a useful `bar?' predicate is bad.]


So here's my latest question. Say we have these definitions:

#lang typed/racket

(struct: (A) foo ())
(struct: (A) bar foo ([proc : (A -> Any)]))


Could `bar?' have the type (All (A) ((foo A) -> Boolean : (bar A)))? 
Then (I think), something like this should type:

(: maybe-foo-proc (All (A) ((foo A) -> (U #f (A -> Any)))))
(define (maybe-foo-proc v)
   (if (bar? v) (bar-proc v) #f))


(Well, it wouldn't currently; the error is "Expected (bar A); given 
#(struct:#<syntax:4:13 bar> ((Nothing -> Any)))".)

Is that also evil? I hope not, because the useless type of `bar?' is 
precluding a possibly important performance enhancement.

Neil ⊥