Splicing syntax parameterize disables Typed Racket type annotations

Question

When I run the following, I get a type error as expected:

#lang typed/racket
(require racket/stxparam)
(define-syntax-parameter x #f)
(syntax-parameterize ([x #'foo])
  (: n Number)
  (define n "string")
  'foo)

But when I use splicing-syntax-parameterize instead, suddenly I get no type errors

#lang typed/racket
(require racket/stxparam
         racket/splicing)
(define-syntax-parameter x #f)
(splicing-syntax-parameterize ([x #'foo])
  (: n Number)
  (define n "string"))

Examining at the REPL shows that n has type String, despite the annotation. The documentation for splicing-syntax-parameterize claims that it treats definitions in the same manner as begin:

Like syntax-parameterize, except that in a definition context, the body forms are spliced into the enclosing definition context (in the same way as for begin).

However, if I use begin instead of splicing-syntax-parameterize:

#lang typed/racket
(begin
  (: n Number)
  (define n "string"))

Then I do get a type error. Is there some reason splicing-syntax-parameterize strips away type annotations from definitions, but begin does not? I would hazard a guess it's because the splicing-syntax-parameterize is basing its behavior on the untyped begin form instead of the begin form from Typed Racket, and thus knows absolutely nothing about the : form. If that's the case, how can I work around this?

Answer 1

Yes, this is a bug. It turns out that splicing-syntax-parameterize has a somewhat strange expansion that doesn't play nicely with the way Typed Racket detects and installs type annotations.

I have written a fix for this bug, which you can find here. As expected, your original program now fails to typecheck. This fix should be available in Racket 6.1.1.8 or greater, so if you need this behavior, use a snapshot build or use the newest version of Typed Racket.

Otherwise, this should be included in the next Racket release.