[plt-dev] certificates, #%module-begin, and typed-scheme's soundness

The example below is independent of Typed Scheme.

The problem is that a macro introduces `f' by itself. As soon as that
macro returns, the identifier `f' is certified to stand alone.

The result seems wrong, particularly since the macro that expanded to
`f' is not itself exported, but that's how the system is currently
defined. In other words, you've run into a limitation of the design, as
opposed to merely a bug in the implementation.

I think the certification of `f' should instead depend on staying in
the context where `p-ex' was certified. (To be continued.)

----------------------------------------

#lang scheme/load

(module m scheme
  (define (f x) x)
  (define-syntax (p-ex stx)
    #'f)
  (define-syntax (ex stx)
    #'((p-ex) 10))
  (provide ex))

(module n scheme
  (require 'm)
  (define-syntax (cheater stx)
    (define v (local-expand #'(ex) 
                            'expression 
                            null))
    (syntax-case v ()
      [(app f v)  #'f]))
  ((cheater) 3))

(require 'n)