How to do define-for-syntax in typed racket?

This works

#lang racket

(begin-for-syntax
  (define (foo n)
    (+ n 3)))

So I would also expect this to work

#lang typed/racket

(: foo : Real -> Real)
(define-for-syntax (foo n)
  (+ n 3))

But if fails with

; :: undefined;
;  cannot reference an identifier before its definition

After that I tried each of the following in turn in typed/racket

(define-for-syntax (foo (n : Real)) : Real
  (+ n 3))

(begin-for-syntax
  (: foo (-> Real Real))
  (define (foo n)
    (+ n 3)))

(begin-for-syntax
  (define (foo (n : Real)) : Real
    (+ n 3)))

Each failed for one reason or another. Could it be that typed/racket can't handle {begin|define}-for-syntax?

Solution

#lang typed/racket

(: foo : Real -> Real)
(define-for-syntax (foo n)
  (+ n 3))

fails with:

Type Checker: Declaration for `foo' provided, but `foo' has no definition

for me, which totally makes sense. foo is defined in phase 1, so the type declaration couldn't find its definition in phase 0.

(begin-for-syntax
  (: foo (-> Real Real))
  (define (foo n)
    (+ n 3)))

is more "correct", but still has a lot of problems. The code is in phase 1, but : is imported by #lang typed/racket in phase 0, so you get an error:

:: undefined

However, another major problem is that even if you manage to import : in phase 1, the type checker will still not work correctly.

To cut it short, here's how you could make it work.

#lang typed/racket

(module for-syntax-mod typed/racket
  (provide foo)
  (: foo (-> Real Real))
  (define (foo n)
    (+ n 3)))

(require (for-syntax 'for-syntax-mod))

(begin-for-syntax (println (foo 10)))

This declares foo in a submodule for-syntax-mod of the language typed/racket, so the type checker will now work on this submodule as expected. We then import this submodule at phase 1, so now foo is available inside begin-for-syntax. Note that code in begin-for-syntax is still not type checked statically.