call with keyword incorrectly checks function type

[bdeket]

What version of Racket are you using?

7.7.0.9 (also tested with 7.7.0.7)

What program did you run?

#lang typed/racket/base

(define (root-split [alg : Integer]
                    [make-mid : (-> Integer Integer Integer)]
                    #:checkΔ [Δfct : (-> Integer)#;(λ () 1)]
                    ) : Integer
  (make-mid 0 0)
  1)

(define (test)
  (root-split 1
              (λ ([lst : (Listof (List Integer Integer))]): Integer 1)
              #:checkΔ (λ () 1)))

What should have happened?

Type Checker: type mismatch

extra

Removing argument alg (definition and call) does trigger the typechecker to fail,
Removing the kw of the third argument also triggers the error

adding or removing the optional part of this kw-argument or writing the type with:
(: root-split (->* (Integer (-> Integer Integer Integer) #:check (-> Integer))() Integer))
or
(: root-split (->* (Integer (-> Integer Integer Integer))(#:check (-> Integer)) Integer))
have no effect (ie it type checks)

the call to root-split doesn't need to be in (test), but if not then running the file will immediately trigger a runtime error

[juszczakn]

Slightly-simplified example:

#lang typed/racket

(: f (-> Integer (-> Integer) #:p (-> Integer) Integer))
(define (f x g #:p p)
  1)

(define (test)
  (f 1 (λ () "") #:p (λ () 1)))

• Removing f's x Integer arg causes the type checking to correctly identify that g is (-> String).
• Switching the order of x and g does the same thing, typechecking starts working.
• #:p is typechecked correctly, regardless it seems.
• Removing #:p fixes typechecking.