Strange lack of subtyping for case->

[LiberalArtist]

On Racket 8.9 CS, this program:

#lang typed/racket

(: f (case->
      (-> 'a 'b)
      (-> 'x 'y)))
(define (f arg)
  (if (eq? 'a arg)
      'b
      'y))

(: a->b (-> 'a 'b))
(define a->b f)

(: x->y (-> 'x 'y))
(define x->y f)

(: x/y->a/b (-> (U 'a 'x) (U 'b 'y)))
(define x/y->a/b f)

fails to typecheck with the error:

Type Checker: type mismatch
  expected: (-> (U 'a 'x) (U 'b 'y))
  given: (case-> (-> 'a 'b) (-> 'x 'y)) in: f

Adding an additional case-> clause can get the program to typecheck:

#lang typed/racket

(: f (case->
      (-> 'a 'b)
      (-> 'x 'y)
      (-> (U 'a 'x) (U 'b 'y))))
(define (f arg)
  (if (eq? 'a arg)
      'b
      'y))

(: a->b (-> 'a 'b))
(define a->b f)

(: x->y (-> 'x 'y))
(define x->y f)

(: x/y->a/b (-> (U 'a 'x) (U 'b 'y)))
(define x/y->a/b f)

I think (-> (U 'a 'x) (U 'b 'y)) should be recognized as a subtype of (case-> (-> 'a 'b) (-> 'x 'y)). I don't know if the implementation issues are related, but the symptoms resemble #1321.

[NoahStoryM]

I'm thinking about the relationship between these types:

1. (-> (U 'a 'x) (U 'b 'y))
2. (case-> (-> 'a (U 'b 'y)) (-> 'x (U 'b 'y)))
3. (case-> (-> (U 'a 'x) 'b) (-> (U 'a 'x) 'y))
4. (case-> (-> 'a 'b) (-> 'x 'y) (-> 'x 'b) (-> 'a 'y))

I think (case-> (-> 'a 'b) (-> 'x 'y)) is a subtype of the 2nd type and should also be considered a supertype of the 4th type. But all four types seem to me to describe the same input-output relationship.