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?