Fixes handling of pattern variables that look like metafunctions

collects/redex/private/reduction-semantics.rkt

@@ -1895,15 +1895,18 @@
             (loop (cdr rest-modes) rest-terms rest-ctcs (+ 1 pos)))))))
 
 (define-for-syntax (mode-check mode clauses nts syn-err-name)
-  (define ((check-template named-vars) temp bound)
+  (define ((check-template bound-anywhere) temp bound)
     (let check ([t temp])
       (syntax-case t (unquote)
         [(unquote . _)
          (raise-syntax-error syn-err-name "unquote unsupported" t)]
         [x
          (identifier? #'x)
-         (when (and (or (id-binds? nts #t #'x) (free-id-table-ref named-vars #'x #f))
+         (unless (cond [(free-id-table-ref bound-anywhere #'x #f)
-                    (not (free-id-table-ref bound #'x #f)))
+                        (free-id-table-ref bound #'x #f)]
+                       [(id-binds? nts #t #'x)
+                        (term-fn? (syntax-local-value #'x (λ () #f)))]
+                       [else #t])
            (raise-syntax-error syn-err-name "unbound pattern variable" #'x))]
         [(u ...)
          (for-each check (syntax->list #'(u ...)))]
@@ -1956,7 +1959,7 @@
   (for ([clause clauses])
        (define do-tmpl
          (check-template
-          (fold-clause (bind 'name-only) void (make-immutable-free-id-table) clause)))
+          (fold-clause (bind 'rhs-only) void (make-immutable-free-id-table) clause)))
        (fold-clause (bind 'rhs-only) do-tmpl (make-immutable-free-id-table) clause)))
 
 ;; Defined as a macro instead of an ordinary phase 1 function so that the

collects/redex/private/rewrite-side-conditions.rkt

@@ -161,8 +161,7 @@
                  (and (identifier? (syntax x))
                       ((case mode
                          [(rhs-only) binds-in-right-hand-side?]
-                         [(binds-anywhere) binds?]
+                         [(binds-anywhere) binds?])
-                         [(name-only) (λ (_1 _2 _3) #f)])
                        all-nts bind-names? (syntax x)))
                  (cons (make-id/depth (syntax x) depth) names)]
                 [else names]))]

collects/redex/tests/syn-err-tests/judgment-form-definition.rktd

@@ -183,3 +183,27 @@
      [(name binder)
       premise ellipsis])
    (void)))
+
+(#rx"unbound pattern variable"
+ ([x f_7])
+ (let ()
+   (define-language L
+     (f any))
+   (define-judgment-form L
+     #:mode (J1 O)
+     [(J1 x)])
+   (void)))
+
+(#rx"unbound pattern variable"
+ ([use f_2]) ([outer-def f_2] [inner-def f_2])
+ (let ()
+   (define-language L
+     (f any))
+   (define-metafunction L
+     [(outer-def) ()])
+   (define-judgment-form L
+     #:mode (K I I O)
+     [(K a any_1 x)
+      (K b (use) (name inner-def any))]
+     [(K b any K-b-out)])
+   (void)))

collects/redex/tests/tl-test.rkt

@@ -1823,6 +1823,19 @@
              'a)
             '(a b)))
     
+    ; a call to a metafunction that looks like a pattern variable
+    (let ()
+      (define result 'result)
+      (define-language L
+        (f any))
+      (define-judgment-form L
+        #:mode (J O)
+        [(J (f_2))])
+      (define-metafunction L
+        [(f_2) ,result])
+      (test (judgment-holds (J any) any)
+            (list result)))
+  
     ;                                                                 
     ;                                                                 
     ;                    ;;                        ;;