#%elaborate-top combined with begin

[AlexKnauth]

When a begin appears within #%elaborate-top, and that begin defines and uses an identifier with define-syntax, it expands the whole thing using local-expand+elaborate [1, 2], instead of letting the define-syntax go through to define the identifier.

Here's an example:

#lang hackett

(require (only-in racket/base define-syntax for-syntax begin))
(require (for-syntax racket/base
                     hackett/private/expand+elaborate))

(define-syntax m
  (λ (stx)
    (syntax-local-elaborate-top
     #'(begin
         (define-syntax x 5)
         (local-value x)))))

(define-syntax local-value
  (λ (stx)
    (syntax-case stx []
      [(_ x) #`#,(syntax-local-value #'x)])))

;; In the REPL:
;; > (m)
;; ;syntax-local-value: unbound identifier: #<syntax x>

[lexi-lambda]

This is not a bug; it is the intended behavior of syntax-local-elaborate-top. The top level is hopeless. Getting it right in the context of all the partial expansion Hackett currently does is incredibly subtle. See the following comment:

https://github.com/lexi-lambda/hackett/blob/4da7848901165c21e0f2e7c9d1fb00df693acf87/hackett-lib/hackett/private/expand%2Belaborate.rkt#L193-L198

Usually, at the top level, we want to perform partial expansion to discover definitions and expressions and trampoline to allow their expansion and evaluation to be interleaved. The existing comment at the top of toplevel.rkt explains this in gory detail. Unfortunately, sometimes this partial expansion goes wrong… we might expand too much! For example, it’s possible that we accidentally partially expand a form that requires elaboration to be happening already. If we partially expand this form, expansion will explode.

Therefore, forms can opt out of this partial expansion process using syntax-local-elaborate-top—that is, they can request to be treated as one unit to be elaborated all at once. This means they give up the interleaving of expansion and evaluation they were previously promised! In return, they get a new, incompatible guarantee: they will be expanded during elaboration. Currently, syntax-local-elaborate-top is only used in one spot in all of Hackett, which is def without explicit type annotation, since it forces expansion itself.

This is definitely a crude hack, but such is life at the top level. Sadly, we cannot have our cake and eat it, too, here: the whole point of elaboration is that it happens after the whole program is expanded (and therefore typechecked), but at the top level, we do not have the whole program at our disposal. Therefore, macros that request earlier elaboration really can’t enjoy that same interleaving of expansion and evaluation, since they have to be expanded all at once.

By the way, this very issue is why I started a mailing list thread requesting a less hopeless REPL. While I was working on this, the problem seemed intractable, and I almost gave up. I managed to find a hack that worked in this case, but I would not be surprised if eventually, the top level becomes unmanageable for Hackett’s REPL, and we need to throw the whole thing away and find something better. Just not yet.

[AlexKnauth]

Okay. Thank you for that explanation. I need to find a way to do this without syntax-local-elaborate-top then.