[racket] Syntax certificate question

Okay, I don't understand what's going on, but I've fixed the program.
First I had to apply the result of (syntax-local-certifier #t)
directly to the reference to identity.  I don't know why this is.  I
also had to expand the body of with-macro in the internal definition
context I created, so that references to lhs don't escape the
expansion of with-macro.  That part makes sense to me.

#lang racket/load

(module A racket
  (provide with-macro)
  (require (for-syntax racket/syntax syntax/parse))
  (define-for-syntax (identity x) x)
  (define-syntax with-macro
    (syntax-parser
      [(_ lhs:id rhs:expr e:expr)
       (define ctx (syntax-local-make-definition-context))
       (syntax-local-bind-syntaxes
         (list #'lhs)
         #`(#,((syntax-local-certifier #t) #'identity) rhs)
         ctx)
       (internal-definition-context-seal ctx)
       (local-expand #'e (list (gensym 'with-macro)) null ctx)])))

(module B racket
  (require 'A (for-syntax syntax/parse))
  (with-macro thunk (syntax-parser [(_ e:expr) #'(lambda () e)])
    (thunk (printf "Boo!\n"))))

On Sat, Jun 4, 2011 at 3:13 PM, Carl Eastlund <cce at ccs.neu.edu> wrote:
> A question for the syntax certificate connoisseurs out there.  The
> program below produces the following error message:
>
>  compile: access from an uncertified context to unexported variable
> from module: "A" in: identity
>
> Why is the reference to identity from within the module that binds it
> illegal?  Is that syntax object somehow not certified correctly, or
> does syntax-local-bind-syntaxes result in some illegal destructuring
> of its input?  I imagine I can work around this by providing identity
> so that the certificate system ignores it, but I'd like to at least
> understand what's causing this error.
>
> #lang racket/load
>
> (module A racket
>  (provide with-macro)
>  (require (for-syntax racket/syntax syntax/parse))
>  (define-for-syntax (identity x) x)
>  (define-syntax with-macro
>    (syntax-parser
>      [(_ lhs:id rhs:expr e:expr)
>       (define ctx (syntax-local-make-definition-context))
>       (syntax-local-bind-syntaxes (list #'lhs) #'(identity rhs) ctx)
>       (internal-definition-context-seal ctx)
>       (internal-definition-context-apply ctx #'e)])))
>
> (module B racket
>  (require 'A (for-syntax syntax/parse))
>  (with-macro thunk (syntax-parser [(_ e:expr) #'(lambda () e)])
>    (thunk (printf "Boo!\n"))))
>