Subtyping involving functions with keyword arguments causes TR to make unsound assumptions about argument types about typed-racket HOT 4 OPEN

After some more investigation, this typechecks as well.

(: f (Number [#:y Boolean] [#:z Nothing] -> Number))
(define (f x #:y [y #f] #:z [z 'this-can-be-anything])
  (if y "y is truthy" x))

I'm not sure why giving a parameter the Nothing type makes the typechecker do this. I'll keep looking into it, but I'm not completely sure where I should be looking.

from typed-racket.

Also, this produces an internal error with no useful information.

(: g (Nothing -> Any))
(define (g [x 'x] [y 'y]) 'g)

Internal Typechecker Error: no type for (if y11 y9 (quote y)) at: #f line #f col #f
while typechecking:
here
originally:
here

EDIT: Looks like this is actually a bug in the optimizer, since turning off optimizations stops it from erroring, though it feels indicative of a larger problem.

from typed-racket.

I believe I’ve independently encountered this bug. The function f1 compiles, but loses its types (the types of 'bool' and 'syms' are reported as Any).

But if I add a dummy keyword argument, as in f2, then everything typechecks fine: 'bool' is reported as a Boolean and 'syms' is (Listof Symbol).

(: f1 (() (Boolean) #:rest Symbol . ->* . Any))
(define (f1 [bool #t] . syms)
 bool
 syms)

(: f2 (() (Boolean #:x Integer) #:rest Symbol . ->* . Any))
(define (f2 [bool #t] #:x [x 42] . syms)
 bool
 syms)

from typed-racket.

@mbutterick I've filed a separate bug report for that case, #58, based on your information. It may turn out to be related, but I'm not sure, and I think it's quite possible that they're different.

from typed-racket.