check syntax doesn't consider extensions to non-terminals as uses

[florence]

In the program

#lang racket
(require redex)
(define-language a
  (on ::= 1))
(define-extended-language b a
  (on ::= .... (- 2 1)))

(redex-match? b on (- 2 1))

if i try to fix the typo and rename on to one, I get:

#lang racket
(require redex)
(define-language a
  (one ::= 1))
(define-extended-language b a
  (on ::= .... (- 2 1)))

(redex-match? b one (- 2 1))

where the extension in the language b is still named on.

I would expect that the on in the extended language should be both a usage of on from language a and as a second definition of on when its referred to in the redex-match?

[rfindler]

I can't recall anymore for sure, but I think we had it that way, and that was worse for some reason.

For now, how about just renaming at the reference?

Or maybe @dfeltey will say that check syntax should behave differently?

[dfeltey]

I would think that on in the extended language should be both a binder and a reference, because you can rename from there which renames the non-terminal in the extended language and the use, but now the extended language doesn't make sense because one isn't a non-terminal in the language being extended.

[rfindler]

I thought that that was the way we had it before, I believe, and we changed it so that the extended language was a second binder, but no longer a reference. No?