[racket] Syntax certificate question

On Sat, Jun 4, 2011 at 3:17 PM, Jay McCarthy <jay.mccarthy at gmail.com> wrote:
> 2011/6/4 Carl Eastlund <cce at ccs.neu.edu>:
>> 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)
>
> Isn't this a phase 1 binding?

Yup.

>>  (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)
>
> And this a phase -1 (template) use, which normally goes for the phase 0 binding

Nope.  The second argument to syntax-local-bind-syntaxes is a
compile-time (phase 1) expression.  It is essentially equivalent to a
syntax definition:

  (define-syntaxes [lhs] (identity rhs))

>>       (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)])
>
> And this is a phase 0 use?
>
> Is that the problem?

Sadly, no.  This would be easier to work out if it were a phase
problem.  The error message clearly says that identity refers to an
unexported variable from A.  If this were a phase problem, it should
instead say that identity is unbound.

--Carl