Using metafunctions inside modeless judgment premises causes judgment not to hold

[atgeller]

If, in the premise of a modeless judgment rule, there is a recursive call to the modeless judgment where a metafunction is used, the judgment fails to hold on valid derivations. This does not seem to be the case for judgments with modes.

Below is a small test case demonstrating the issue.

#lang racket

(require redex)

(define-language testL
  (e ::= a (box e)))

(define-metafunction testL
  unbox : e -> e
  [(unbox (box e)) e])

(define-judgment-form testL
  #:contract (test1 e e)
  #:mode (test1 I I)

  [---------- "r1"
  (test1 e e)]

  [(where (box _) e_1)
   (test1 (unbox e_1) e_2)
   --------------- "r2"
   (test1 e_1 e_2)])

(test-judgment-holds (test1 (box a) a)) ;; should be #t
;(build-derivations (test1 (box a) a))
;; should output (derivation '(test1 (box a) a) "r2" (list (derivation '(test1 a a) "r1" '())))

(define-judgment-form testL
  #:contract (test2 e e)

  [---------- "r1"
  (test2 e e)]

  [(where (box _) e_1)
   (test2 (unbox e_1) e_2)
   --------------- "r2"
   (test2 e_1 e_2)])

(test-judgment-holds test2 (derivation '(test2 (box a) a) "r2" (list (derivation '(test2 a a) "r1" '())))) ;; should be #t, is #f

[rfindler]

I think the issue here is that the derivations that come from modeless judgment forms are currently not expected to mention the non-modeless parts of them. Here's a simpler example that demonstrates that point:

#lang racket
(require redex/reduction-semantics)

(define-language L)

(define-judgment-form L
  #:mode (J1 I)

  [--------- "r1"
   (J1 1)])

(define-judgment-form L
  [(J1 any)
   ----------- "r2"
   (J2 any)])

(test-judgment-holds
 J2
 (derivation '(J2 1)
             "r2"
             (list (derivation '(J1 1) "r1" '()))))

(test-judgment-holds
 J2
 (derivation '(J2 1)
             "r2"
             (list)))

If you add/remove the #:mode line then the test case that passes changes from one to the other.

Despite what I wrote to @florence in #222 I'm coming around to the idea that the current implementation is wrong. I can certainly agree that it is confusing. Maybe it should allow the moded subderivations to either appear or not and, if they do appear, it should check them (but if they don't appear, then it would just check to see if the judgment holds, as it currently does).

[rfindler]

My thinking now is that one big value of judgment-holds is one can use it to check something that's being typeset in a paper. So in that sense it should have all of the derivations in there (perhaps some of the subderivations might be removed (after the checking) because they're uninteresting). So instead of checking only the modeless things, all of the judgment forms should be checked.

That's not backwards compatible but because everyone seems to think that the current behavior is a bug maybe it really is backwards compatible.