Verifying polymorphic type signatures with more general types

[tilk]

The following definition is somehow accepted, even though the type given for the signature is not valid for the definition (it's more general):

(wrong-foldr : (('a 'b -> 'b) 'b (Listof 'a) -> 'b))
(define (wrong-foldr f acc xs)
  (if (empty? xs) acc (first xs))

Similar behavior can be seen with has-type:

> (has-type wrong-foldr : (('a 'b -> 'b) 'b (Listof 'a) -> 'b))
- (('_a '_a -> '_a) '_a (Listof '_a) -> '_a)

The type checker seems not to recognize that I explicitly want a more general type, and permits the type signature / annotation.