racket - 了解 `case->` 周围的类型检查器行为

Question

在 REPL 上，这是我检查类型时得到的car

> car
- : (All (a b) (case-> (-> (Pairof a b) a) (-> (Listof a) a)))

当传递一个可能不存在第二个值的对时，它返回一对中第一个类型的元素。

现在我想在一个映射对列表并获取第一个元素的函数中使用它

(: f (-> (Listof (Pairof Integer Symbol)) (Listof Integer))

当我尝试编写如下函数时，类型检查失败

(define (f l) (map car l))
; stdin::9317: Type Checker: Polymorphic function `map' could not be applied to arguments:
; Types: (-> a c) (Pairof a (Listof a)) -> (Pairof c (Listof c))
;        (-> a b ... b c) (Listof a) (Listof b) ... b -> (Listof c)
; Arguments: (All (a b) (case-> (-> (Pairof a b) a) (-> (Listof a) a))) (Listof (Pairof Integer Symbol))
; Expected result: (Listof Integer)
; 
;   in: (map car l)

但是，如果我将 car 函数包装在具有将输入类型指定为 的效果的 lambda 中car，那么我的实现类型检查完美

(define (f l) (map (lambda ([x : (Pairof Integer Symbol)]) (car x)) l))

这里到底发生了什么，为什么类型检查器不够聪明，无法从函数参数的类型注释中推断出它应该使用car函数中两种情况中的第一种？

标签： rackettyped-racket