Yes, it does look like expanding syntax-case is more expensive than we’d like. I didn’t investigate that level, though, since it was obviously bad in this case at the struct-field-index level.

> I’ve found that, in the past, however, that jumping to the contract-out and then jumping from there to the actual definition is useful. For now, I implemented doing the equivalent of that, so the user does not need to. Effectively, it’s as if the user opened the proximate file (the one that adds the contract wrapper), finds the item, and does another visit-definition. That ends up on the actual define of the item. [Amusingly one example of such a scenario, and how I first noticed this, is make-traversal. :smile: It is defined in private/synchecks/traversals.rkt and provided without a contract. check-syntax.rkt requires that, and re-provides it with a contract-out.]

I think that’s a reasonable strategy for the status quo (for existing and older versions of Racket), for now.

I did start to look at how, for some future version of Racket, contract-out could provide a syntax-property (for example). But I’d need a fair bit of time to absorb and understand e.g. https://github.com/racket/racket/blob/master/racket/collects/racket/contract/private/provide.rkt

I think the thing to focus on isn’t the contract implementation but instead the protocol design and where it should live.

I can adapt contract-out no problem.

Others may want adapt other things.

Ryan may have good ideas too. I would probably try to involve him if I were going to try this.

Thanks. FWIW recently I’ve been adding more tests to the front end Emacs Lisp code. Between ELisp, the nature of Emacs UI, and timing issues when running on CI, it is not always a delightful experience, and kind of a slow slog.

I think the protocol should basically be a syntax property somewhere that says “keep going! Here is a next id to continue with”. Roughly

My starting point is usually “what is the simplest thing that could possibly work?”, and a syntax-property was the only obvious/simple thing I could imagine. But definitely interested in any possible other/better ways! And no urgent need, from my side, to rush out the first idea.

I believe that keyword application already does something similar, but I’d have to check the details

@greg : sure. But it needs to be documented and used by the clients and implemented.

Ah, so I probably underestimated the number of other “wrapping/renaming” things that might exist, and want to do similar. Got it.

Probably the best thing is to define the protocol, make it work on some dumb example and then crack the whip on someone to get contracts to also follow the protocol.

:)

Yes, I’ve been very “view from one foot away” on this lately, not zoomed out. :slightly_smiling_face:

Hi, everyone, I have a redex question, #lang racket (require redex) (define-language TestL [x := variable-not-otherwise-mentioned]) (define-metafunction TestL id : x -> x [(id x) x]) (define-judgment-form TestL #:mode (test123 I O) #:contract (test123 x x) [-------------- (test123 x (id x))]) (test-judgment-holds (test123 x (id x))) ;; changing (id x) to x works Why don’t meta-functions work for output patterns in (test-)judgment-holds?

Never mind, I’ve found the answer in the documentation: > the judgment-holds form checks whether a judgment form holds for any assignment of pattern variables in output positions.