Syntactic closures behave unexpectedly (different from MIT scheme)

[karlosz]

Here's an example where sc-macro-transformer behaves differently than on MIT scheme. The MIT scheme version behaves more in line with what I expect.

(define-syntax loop
  (sc-macro-transformer
   (lambda (exp env)
     (let ((body (cdr exp)))
       `(call-with-current-continuation
         (lambda (exit)
           (let f ()
             ,@(map (lambda (exp)
                      (make-syntactic-closure env '(exit)
                                              exp))
                    body)
             (f))))))))

(define-syntax wrapper
  (sc-macro-transformer
   (lambda (exp env)
     `(loop
       (,(make-syntactic-closure env '() (cadr exp)) "Hello, World!")
       (newline)
       (exit 4)))))

(let ((exit display))
  (wrapper exit))

On MIT Scheme, this code displays "Hello, World!" and returns 3, as I would expect. On Chibi, this simply returns "Hello, World!". The behavior on MIT Scheme seems more intuitive, since loop only introduces exit in the environment of the macro definition of wrapper, so the exit identifier bound by let should not be captured by the free reference to exit in loop, which should be resolved in the environment of the wrapper macro definition.

Futhermore, on both implementations, defining wrapper with syntax-rules like so

(define-syntax wrapper
  (syntax-rules ()
    ((wrapper display)
     (loop
      (display "Hello, World!")
      (newline)
      (exit 4)))))

causes both implementations to return the 'wrong' result. I think this is a problem with how syntax-rules is implemented. It should behave exactly the same as how the sc-macro-transformer definition of wrapper behaves in MIT Scheme. I believe this is what led Marc Nieper-Wißkirchen to claim here https://groups.google.com/g/comp.lang.scheme/c/2gFSbX-Wcy4 that syntactic closures as is can't be used to define unhygienic macros reliably. On the contrary, I believe these are implementation bugs with how the free-names parameter of syntactic closures are handled in Chibi, and how syntax-rules interacts with syntactic environments (the definition should convert the pattern in an isolated environment as MIT scheme does with sc-macro-transformer), and that theoretically syntactic closures can deal with these cases fine.

[ashinn]

Thanks for the report! This is something of a known issue, though I don't have time to work on it now. Yes, I think a faithful syntactic closure implementation can deal with unhygienic macros just fine.

[mnieper]

MIT Scheme's syntactic closure implementation (which I think can be called faithful) cannot implement correct unhygienic macros that work together with hygienic syntax-rules macros seamlessly. To make it work, at least, you would have to stay completely in the world of syntactic closure macros, which is not feasible.

[karlosz]

I believe that MIT scheme'a syntactic closure implementation is 'faithful', but I suspect that its syntax-rules transformer implementation is bugged in how it interacts with syntactic closures. I don't see why syntax-rules can't be made to work fine on top of syntactic closures so that the example works. After all, the implementation should theoretically be able to implement the 'wrapper' example with syntax-rules by rewriting it to the equivalent macro purely 'inside the world of syntactic closures', which works.

[mnieper]

A syntax-rules transformer is dumb. It cannot know in which contexts the identifiers of the macro input and of the templates will eventually end up, so it is not clear what such a "rewriting" implementation should look like. Another problem is that make-syntactic-closure would need already renamed identifiers (in the terminology of syntax-rules) as free names. Moreover, the transformer of a syntactic closure macro (containing free identifiers literally) may already be the result of a syntax-rules invocation. Regardless of compatibility with syntax-rules, a final problem is that syntactic closures cannot express all unhygienic macros, e.g. define-record-type from R6RS or from SRFI 99 where the constructor, accessor, etc. names are derived from the record name and not from the macro keyword, i.e., one needs to get hold of the syntactic environment of some input identifier that is not the macro keyword.

[ashinn]

Sorry, I don't follow your argument that a syntax-rules transformer is "dumb" and therefore can't work with unhygienic macros, much less how syntactic closures differs from syntax-case here.

Regarding define-record-type. you don't need to get hold of the syntactic environment through objects (though you can), it's passed explicitly.

[karlosz]

I assume MIT scheme also expands syntax-rules into an er transformer, as chibi does. This indeed doesn't work, as it wouldn't work to use an er transformer to define the wrapper macro above, though using sc-transformer does. The problem.

er transformers are strictly less powerful, as syntactic closures have a free-names parameter, and you can also get fine grained environment capture with capture-syntactic-environment. As alexshinn points out, sc-macro-transformers macros are passed in the environment of the usage, though it implicitly wraps the form returned in the environment of the macro keyword.

A working syntax-rules macro in terms of syntactic closures would wrap the entire expanded template in the macro keyword's environment. The sub parts of the template filled by the actual input form via the pattern matching variables are wrapped in a syntactic closure with the passed in environment. This causes any unhygienic macro use in the syntax rule template to expand in the isolated environment of the macro keyword, so that the unhygienic binding introduced don't leak to the usage environment or vice versa, that any names in the usage environment (like exit in the above example) do not identify with any unhygienic names introduced by an unhygienic macro in the template.

Notice how er-macro-transformer doesn't let you do this type of isolation, since it can only rename and it doesn't have a free-names parameter to offer fine grained control over how raw symbol names are processed. Chibi should switch to this way of defining syntax-rules so that the example in the top-level issue post works. I will try to get a POC implementation of syntax-rules with raw syntactic closures working as soon as I understand how the ellipses processing works.

[mnieper]

I assume MIT scheme also expands syntax-rules into an er transformer, as chibi does. This indeed doesn't work, as it wouldn't work to use an er transformer to define the wrapper macro above, though using sc-transformer does. The problem.

er transformers are strictly less powerful, as syntactic closures have a free-names parameter, and you can also get fine grained environment capture with capture-syntactic-environment. As alexshinn points out, sc-macro-transformers macros are passed in the environment of the usage, though it implicitly wraps the form returned in the environment of the macro keyword.

There are unhygienic macros (where the non-hygiene comes from constructing names) where knowledge of the environment of the usage is not enough and where the macro needs to be able to wrap a constructed identifier in the syntactic environment of an input identifier that is not the macro keyword.

define-record-type of SRFI 99 is a practical example, here is one to demonstrate the issue:

(define-syntax predicate
  (lambda (stx)
    (syntax-case stx ()
      ((_ name) (identifier? #'name)
       (datum->syntax #'name (string->symbol (string-append (symbol->string (syntax->datum #'name)) "?")))))))

For example (predicate foo) expands into foo? so that the syntactic environment of foo? is the syntactic environment of foo (and not of predicate).

A working syntax-rules macro in terms of syntactic closures would wrap the entire expanded template in the macro keyword's environment. The sub parts of the template filled by the actual input form via the pattern matching variables are wrapped in a syntactic closure with the passed in environment. This causes any unhygienic macro use in the syntax rule template to expand in the isolated environment of the macro keyword, so that the unhygienic binding introduced don't leak to the usage environment or vice versa, that any names in the usage environment (like exit in the above example) do not identify with any unhygienic names introduced by an unhygienic macro in the template.

Consider a syntax-rules macro output of the form (bar* x y* z) where the starred parts come from the macro input (and the unstarred parts from the template). It would not be enough to wrap the entire output in the macro env and the starred identifiers in the usage env because when bar* is eventually invoked, it would happen in the usage env and x and z would no longer see the macro env.

Thus, the syntax-rules transformer would have to wrap each identifier of the input and the template individually. For example, the output of (wrapper) with

(define-syntax wrapper
  (syntax-rules ()
    ((_) (loop (exit 3)))))

would have to be something like (loop* (exit* 3)) where the * marks a wrapping in the syntactic environment of the transformer environment (the macro environment of wrapper) menv. This expands into the equivalent of:

(call-with-current-continuation
  (lambda (exit)
    (let f ()
      (make-syntactic-closure env '(exit) `(,(close-syntax 'exit menv) 3))
      (f))))

The problem here, however, is that the meaning of exit in the body of f will ultimately be derived from the environment menv, so making exit free doesn't help.

[mnieper]

Sorry, I don't follow your argument that a syntax-rules transformer is "dumb" and therefore can't work with unhygienic macros, [...]

What I meant by "dumb" is that a syntax-rules transformer is a general rewriting engine that cannot know the semantic meaning of its input and its output. It has to enclose parts of its output in syntactic closures in a uniform way. There is no uniform way, however, that works together with all possible unhygienic SC macros. (This problem does not appear with syntax-case, which is a different system; syntax-case is designed to be an extension of syntax-rules.)

[...] much less how syntactic closures differs from syntax-case here.

Regarding define-record-type. you don't need to get hold of the syntactic environment through objects (though you can), it's passed explicitly.

I hope the rest was clarified by my previous post.

[ashinn]

Sorry, I don't follow your argument that a syntax-rules transformer is "dumb" and therefore can't work with unhygienic macros, [...]

What I meant by "dumb" is that a syntax-rules transformer is a general rewriting engine that cannot know the semantic meaning of its input and its output. It has to enclose parts of its output in syntactic closures in a uniform way. There is no uniform way, however, that works together with all possible unhygienic SC macros. (This problem does not appear with syntax-case, which is a different system; syntax-case is designed to be an extension of syntax-rules.)

I believe what you're saying is that the syntax-rules in most syntax-case systems is just a special case and parses any syntax objects the same. Whereas e.g. the syntax-rules in Chibi is a layer on top of er-macro-transformer macros, assuming it doesn't need to descend into any non-identifier syntactic closures. But there's no reason it couldn't.

[mnieper]

Sorry, I don't follow your argument that a syntax-rules transformer is "dumb" and therefore can't work with unhygienic macros, [...]

What I meant by "dumb" is that a syntax-rules transformer is a general rewriting engine that cannot know the semantic meaning of its input and its output. It has to enclose parts of its output in syntactic closures in a uniform way. There is no uniform way, however, that works together with all possible unhygienic SC macros. (This problem does not appear with syntax-case, which is a different system; syntax-case is designed to be an extension of syntax-rules.)

I believe what you're saying is that the syntax-rules in most syntax-case systems is just a special case and parses any syntax objects the same. Whereas e.g. the syntax-rules in Chibi is a layer on top of er-macro-transformer macros, assuming it doesn't need to descend into any non-identifier syntactic closures. But there's no reason it couldn't.

Of course, it could, but that wouldn't be of any help in the wrapper example where the syntax-rules macro expands into a SC macro and not vice versa.

[karlosz]

There are unhygienic macros (where the non-hygiene comes from constructing names) where knowledge of the environment of the usage is not enough and where the macro needs to be able to wrap a constructed identifier in the syntactic environment of an input identifier that is not the macro keyword.

define-record-type of SRFI 99 is a practical example, here is one to demonstrate the issue: [...]

Yes, this is true. To make this work you need to provide a function that gets the environment of an input identifier.

A working syntax-rules macro in terms of syntactic closures would wrap the entire expanded template in the macro keyword's environment. The sub parts of the template filled by the actual input form via the pattern matching variables are wrapped in a syntactic closure with the passed in environment. This causes any unhygienic macro use in the syntax rule template to expand in the isolated environment of the macro keyword, so that the unhygienic binding introduced don't leak to the usage environment or vice versa, that any names in the usage environment (like exit in the above example) do not identify with any unhygienic names introduced by an unhygienic macro in the template.

Consider a syntax-rules macro output of the form (bar* x y* z) where the starred parts come from the macro input (and the unstarred parts from the template). It would not be enough to wrap the entire output in the macro env and the starred identifiers in the usage env because when bar* is eventually invoked, it would happen in the usage env and x and z would no longer see the macro env.

Thus, the syntax-rules transformer would have to wrap each identifier of the input and the template individually. For example, the output of (wrapper) with

(define-syntax wrapper
  (syntax-rules ()
    ((_) (loop (exit 3)))))

would have to be something like (loop* (exit* 3)) where the * marks a wrapping in the syntactic environment of the transformer environment (the macro environment of wrapper) menv. This expands into the equivalent of:

(call-with-current-continuation
  (lambda (exit)
    (let f ()
      (make-syntactic-closure env '(exit) `(,(close-syntax 'exit menv) 3))
      (f))))

The problem here, however, is that the meaning of exit in the body of f will ultimately be derived from the environment menv, so making exit free doesn't help.

No, this is not how syntax-rules on top of sc-macro-transformer would work. Instead of wrapping free identifiers in the template in the usage environment, the result of the pattern matching variables in the template should be wrapped in the usage environment instead, whereas the whole form gets wrapped in the usage environment. That causes the binding of exit introduced by loop to not leak out of the macro definition of wrapper. I don't understand what you're trying to say with your (bar* x y* z) example. If you wrap the whole form (bar* x y* z) in the macro definition environment and then wrap bar* and y* in the usage environment, what breaks with x and z?

By the way, I've implemented this strategy with some debugging code enabled in this gist: https://gist.github.com/karlosz/c0af67d5ad6e4e975a1fc3e60b60a0d0. You can load this gist into mit scheme (it should work in any scheme with 'faithful' syntactic closures with srfi-1 and pretty-print defined), and it will redefine syntax-rules to get expanded in terms of sc-macro-transformer the way I've outlined. Then you can try the wrapper example cited in the original post and it will work. The implementation is not complete and is probably buggy but gets the main idea across: the only hygiene part needed is in hygienify which wraps the pattern matching variables appearing in the template in the usage environment. So I think this proves it's possible to make syntax-rules work correctly on top of sc-macro-transformer so that composing unhygienic macros works as expected. Maybe you can try to make your bar* counterexample more concrete against this implementation.

[mnieper]

In the following discussion, I write e[u] for the syntactic closure of the expression e in the environment u. Consider the macro

(define-syntax foo
  (syntax-rules ()
    ((_ a) (bar (loop (exit a))))))

and a macro invocation of the form (foo a). Let us call the transformer environment t and the usage environment u. In Chibi's and MIT's implementation of syntax-rules, the expansion of (foo a) looks like

(bar[t] (loop[t] (exit[t] a[u])))[t] 

I think we agree that your initial post in this thread shows that this does not play well with unhygienic SC macros, so we are looking for a better solution. If I understand you correctly, you propose that the expansion should look like

(bar (loop (exit a[u])))[t]

Assume that bar is defined (in the environment t) as follows:

(define-syntax bar
  (syntax-rules ()
    ((_ a) (a))))

Let s be the corresponding transformer environment. The expansion of (bar (loop (exit a[u])))[t] now gives, according to your proposal:

(loop[t] (exit[t] a[u][t]))[s]

This is equivalent to:

(loop[t] (exit[t] a[u]))[s]

We see that we end up with an expansion of the form we had to rule out earlier. The identifier exit is closed over the environment t, so it does not reference the binding of exit introduced by loop.

[karlosz]

In Chibi's and MIT's implementation of syntax-rules, the expansion of (foo a) looks like

(bar[t] (loop[t] (exit[t] a[u])))[t] 

I think we agree that your initial post in this thread shows that this does not play well with unhygienic SC macros, so we are looking for a better solution.

Agree.

If I understand you correctly, you propose that the expansion should look like

(bar (loop (exit a[u])))[t]

Assume that bar is defined (in the environment t) as follows:

(define-syntax bar
  (syntax-rules ()
    ((_ a) (a))))

Let s be the corresponding transformer environment. The expansion of (bar (loop (exit a[u])))[t] now gives, according to your proposal:

(loop[t] (exit[t] a[u][t]))[s]

Shouldn't this be (in your notation):

(loop (exit a[u]))[t][s]

? Why have you distributed the environment t to the individual identifiers? That isn't how syntactic closures would work; the forms are closed over and the evaluator evaluates the form in the closed over environment wholesale; there is no preprocess phase during macro expansion where such a distributive operation would be done.

Under this interpretation, exit does the right thing still. In fact, I tried to transcribe your argument as I understood it as follows, and loaded it into the implementation I posted in the gist, which you can load with MIT scheme:

(define-syntax loop
  (sc-macro-transformer
   (lambda (exp env)
     (let ((body (cdr exp)))
       `(call-with-current-continuation
         (lambda (exit)
           (let f ()
             ,@(map (lambda (exp)
                      (make-syntactic-closure env '(exit)
                                              exp))
                    body)
             (f))))))))

(define-syntax bar
   (syntax-rules ()
      ((_ a) (a))))

(define-syntax foo
   (syntax-rules ()
      ((_ a) (bar (loop (exit a))))))

(foo (lambda () 1))

I don't get any undefined variable error here (presumably it would have been with exit). It returns 1, as I (we?) would expect.

[mnieper]

If I understand you correctly, you propose that the expansion should look like

(bar (loop (exit a[u])))[t]

Assume that bar is defined (in the environment t) as follows:

(define-syntax bar
  (syntax-rules ()
    ((_ a) (a))))

Let s be the corresponding transformer environment. The expansion of (bar (loop (exit a[u])))[t] now gives, according to your proposal:

(loop[t] (exit[t] a[u][t]))[s]

Shouldn't this be (in your notation):

(loop (exit a[u]))[t][s]

? Why have you distributed the environment t to the individual identifiers? That isn't how syntactic closures would work; the forms are closed over and the evaluator evaluates the form in the closed over environment wholesale; there is no preprocess phase during macro expansion where such a distributive operation would be done.

When (bar (loop (exit a[u])))[t] is expanded, the current environment becomes t and (bar (loop (exit a[u]))) is expanded in this environment, which is, therefore, the usage environment of the invocation of the bar macro. The bar macro is a syntax-rules macro, which, according to your proposal, closes the input parts into the usage environment, which is t. As the given definition of bar (see note below) should be equivalent to

(define-syntax bar
  (syntax-rules ()
    ((_ (a (b c)) (a (b c)))
    ((_ a) a))) 

I concluded that the implementation of syntax-rules has to distribute the usage environment over the pieces coming from the input. Note that the distribution does not happen inside the expander (I know how syntactic closures work) but during the evaluation of the syntax-rules transformer.

Under this interpretation, exit does the right thing still. In fact, I tried to transcribe your argument as I understood it as follows, and loaded it into the implementation I posted in the gist, which you can load with MIT scheme:

(define-syntax loop
  (sc-macro-transformer
   (lambda (exp env)
     (let ((body (cdr exp)))
       `(call-with-current-continuation
         (lambda (exit)
           (let f ()
             ,@(map (lambda (exp)
                      (make-syntactic-closure env '(exit)
                                              exp))
                    body)
             (f))))))))

(define-syntax bar
   (syntax-rules ()
      ((_ a) (a))))

(define-syntax foo
   (syntax-rules ()
      ((_ a) (bar (loop (exit a))))))

(foo (lambda () 1))

I don't get any undefined variable error here (presumably it would have been with exit). It returns 1, as I (we?) would expect.

NB: I had a typo in my code; there is one pair of parentheses too much in my original definition of bar. It should have looked like:

(define-syntax bar
  (syntax-rules ()
    ((_ a) a)))

Then, the extra wrapping in lambda is not needed.

So, check this please:

(define-syntax loop
  (sc-macro-transformer
   (lambda (exp env)
     (let ((body (cdr exp)))
       `(call-with-current-continuation
         (lambda (exit)
           (let f ()
             ,@(map (lambda (exp)
                      (make-syntactic-closure env '(exit)
                                              exp))
                    body)
             (f))))))))

(define-syntax bar
   (syntax-rules ()
     ((_ (a (b c))) (a (b c))) 
     ((_ a) a)))

;; Redefine global exit so that the Scheme process won't be terminated.
(define (exit ?) (display "EXIT\n"))

(define-syntax foo
   (syntax-rules ()
      ((_ a) (bar (loop (exit a))))))

(foo 1)

[mnieper]

PS For the record and to have something to experiment with, we are aiming for a solution that works as flawlessly as the following syntax-case macro:

(define-syntax loop
  (lambda (stx)
    (syntax-case stx ()
      ((k e ...)
       (with-implicit (k exit)
         #'(call-with-current-continuation
             (lambda (exit)
               (let f ()
                 e ...
                 (f)))))))))

You can readily load this and the rest of the last test code into Chez, and it will work. For clarity, I used Chez's with-implicit, which is not part of R6RS. You can replace (with-implicit (k exit) ---) with (with-syntax ((exit (datum->syntax #'k 'exit))) ---) if your Scheme doesn't have with-implicit (which is just a simple wrapper [1]).

--

[1] https://github.com/cisco/ChezScheme/blob/3d1579e6c67e145895e6a0e7d0f9bf2b8853fbb3/s/syntax.ss#L7595

[mnieper]

Another, different problem with your implementation is that your syntax-rules implementation does not descent into syntactic closures (see also Alex' post from above), which it has to in your implementation strategy. The following example (which does not involve any explicit SC macros) breaks with an error:

(define-syntax foo
  (syntax-rules ()
    ((_ (f a)) (f a))))

(define-syntax bar
  (syntax-rules ()
    ((_ (x y)) x)))

(let ((x 1) (y 2))
  (foo (bar (x y))))

If you want to fix the syntax-rules pattern matcher so that it unwraps syntactic closures, you need a bit of information not present in the syntactic closure itself, namely the time when it was created in order to implement the renaming mechanism of syntax-rules correctly as the standard ER implementation of syntax-rules does. The standard ER implementation works with a renaming table, which works because the renaming is applied eagerly. In your proposal, the unwrapping would happen lazily, and you have to get hold of the right renaming table somehow.

I don't have a formal proof for it, but I bet that you will end up with a system isomorphic to syntax-case if you fix everything.

[mnieper]

I should add one more comment concerning syntactic closures: Syntactic closures are forms and close over forms. This is explained in detail in [1]. Arbitrary syntax objects aren't forms. A transformer that creates a syntactic closure over a syntax object that does not end up as a form is violating the specification.

Thus, any implementation of syntax-rules has only two options: It can create a syntactic closure over its output form, or it can create syntactic closures over individual identifiers, creating aliases as described in [2]. It must not create syntactic closures over arbitrary subforms because it cannot know which of them won't end up as forms. (This is why I used the word "dumb" earlier.)

Syntactic closures and syntax-rules are really two unlike macro systems. The former works on the level of forms; the latter is a pattern-matching and templating engine working on the level of syntax objects.

For example, the R5RS macro

(define-syntax fast+
  (syntax-rules ()
    ((fast+ 0 y) y)
    ((fast+ x y) (+ x y))))

is incompatible with syntactic closures, hygienic or not, and cannot be written as an SC macro (playing well with syntactic closures). An obvious (but failing) attempt to write fast+ as an SC macro is:

(define-syntax fast+
  (sc-macro-transformer
    (lambda (exp env)
     (if (eqv? (cadr exp) 0) 
          (close-syntax (caddr exp) env)
          `(+ ,(close-syntax (cadr exp) env) ,(close-syntax (caddr exp) env))))))

The problem here is the test (eqv? (cadr exp) 0). It is (cadr exp) a form and may thus be a syntactic closure arising from some earlier macro invocation. In this case, the test fails, although the syntactic closure may just wrap the form 0.

We see that in the syntactic closure system, a macro is not allowed to destructure forms. It may only destructure the clauses of the form it represents, e.g. the cond macro is allowed to destructure its clauses, but it is not allowed to destructure the forms appearing in its clauses.

This problem has not shown up in Chibi because SC macros are basically not used outside the definition of er-macro-transformer. While any "sane" syntax-rules macro should not destructure and analyse forms except the form corresponding to its own use, it nevertheless is an incompatibility between syntactic closures and syntax-rules of R5RS.

By the above, fast+ is not a "sane" macro, and, indeed, it isn't: Given the definition

(define-syntax zero
  (syntax-rules ()
    ((zero) 0)))

the macro fast+ does not understand to simplify (fast+ (zero) y).

--

[1] https://www.gnu.org/software/mit-scheme/documentation/stable/mit-scheme-ref/Syntax-Terminology.html [2] https://www.gnu.org/software/mit-scheme/documentation/stable/mit-scheme-ref/SC-Identifiers.html

[karlosz]

I don't have a formal proof for it, but I bet that you will end up with a system isomorphic to syntax-case if you fix everything.

I think you are right here; by fixing the issues you point out with destructuring above, we need to descend into syntactic closures. In doing so, syntactic closures would need to be wrapped and unwrapped before doing any list operation (such as car, cdr, or map), exactly as a syntax-case system would require. So, I think the issues you list could be fixed by coming up with the equivalent of syntax-car, syntax-cdr and syntax-map and using these in the definition of syntax-rules on top of syntactic closures.

The isomorphism would then be pretty clear, I think. strip-syntactic-closures in both chibi and mit scheme correspond to syntax->datum, the 4-arg identifier=? in the syntactic closures system would correspond to the various foo-identifer=? procedures, and of course close-syntax is like datum->syntax with an explicit environment argument. You just need to have procedures that peel and reapply the wrapped environments of a given syntactic closures to fully have the power of the syntax-case primitives to allow destructuring of arbitrary syntax forms.

[ashinn]

Sorry, you guys seem to be having fun but I'm afraid I'm too busy join in just now :sweat_smile:

[mnieper]

I don't have a formal proof for it, but I bet that you will end up with a system isomorphic to syntax-case if you fix everything.

I think you are right here; by fixing the issues you point out with destructuring above, we need to descend into syntactic closures. In doing so, syntactic closures would need to be wrapped and unwrapped before doing any list operation (such as car, cdr, or map), exactly as a syntax-case system would require. So, I think the issues you list could be fixed by coming up with the equivalent of syntax-car, syntax-cdr and syntax-map and using these in the definition of syntax-rules on top of syntactic closures.

The problem would be that the resulting macros would be incompatible with SC and ER macros that do not expect wrapped subforms. Moreover, we have seen above that unwrapping is incompatible with the FREE argument to SC's make-synthetic-closure. The upshot is that there is no backwards-compatible extension of SC that makes it fully compatible with syntax-rules macros. Concerning Chibi, the direct use of SC macros should, therefore, be considered "dangerous". Instead of reinventing the syntax-case system ad hoc, it would be much better to implement it in its standardized form. It is the only standardized Scheme macro system that can work flawlessly and seamlessly with hygienic and unhygienic macros. The low-level primitives for syntax-case are defined in the appendix of R4RS.

The isomorphism would then be pretty clear, I think. strip-syntactic-closures in both chibi and mit scheme correspond to syntax->datum, the 4-arg identifier=? in the syntactic closures system would correspond to the various foo-identifer=? procedures, and of course close-syntax is like datum->syntax with an explicit environment argument. You just need to have procedures that peel and reapply the wrapped environments of a given syntactic closures to fully have the power of the syntax-case primitives to allow destructuring of arbitrary syntax forms.

In the syntax-case system, there is bound-identifier=? and free-identifier=?. Only the latter corresponds to identifier=?. The first is eqv? in the syntactic closures system of MIT/GNU Scheme.