checking expanded forms at the top level might be problematic

[capfredf]

What version of Racket are you using?

Need TR to be patched by https://github.com/racket/typed-racket/pull/1120

What program did you run?

> (struct foo () #:property prop:custom-write 10)

What should have happened?

A type error

If you got an error message, please include it here.

A contract error:

; guard-for-prop:custom-write: contract violation
;   expected: (procedure-arity-includes?/c 3)
;   given: 10

discussion

When TR is checking a module, it batches all expanded forms in the module, preprocess them (pass 0) and then subsequently do pass 1, pass 1.5 and pass 2 of type checking on each of them. Type checking a struct definition spans across passes. In pass 0, the type check registers the structurue type and types for generated bindings (like accessors and constructors). In pass 2, it checks property values of the structure.

For example, the struct definition above expands to

;; the first form
   (🔒define-values (🔒struct:foo 🔒foo1 🔒foo?)
     🔒(let-values ([(struct: make- ? -ref -set!)
                    (let-values ()
                      (let-values ()
                        (#%app
                         make-struct-type
                         'foo
                         (quote #f)
                         (quote 0)
                         (quote 0)
                         (quote #f)
                         (#%app list (#%app cons prop:custom-write (quote 10)))
                         (#%app current-inspector)
                         (quote #f)
                         '()
                         (quote #f)
                         'foo)))])
        (#%app values struct: make- ?)))

;; the second form
   (🔒define-syntaxes (🔒foo)
     🔒(#%app
       make-self-ctor-checked-struct-info
       (lambda ()
         (#%app
          list
          (quote-syntax 🔒struct:foo)
          (quote-syntax 🔒foo)
          (quote-syntax 🔒foo?)
          (#%app list)
          (#%app list)
          (quote #t)))
       '()
       (#%app list (#%app list) (#%app list))
       (lambda () (quote-syntax foo1))))))

;; the third form
  (define-values
 ()
 (begin
   (quote-syntax
    (define-typed-struct-internal foo foo () #:property prop:custom-write)
    #:local)
   (#%plain-app values)))

Roughly speaking, the type-checker uses the third form to register struct type foo and the first one to check the property value prop:custom-write.

However, this approach doesn't work well with the REPL. At REPL, each form is checked and then evaluated separately. Therefore, the first form gets to run before the whole type check process is finished, and then we see the contract error instead of a type error. In #1120, I rearranged how struct-related forms were checked in line with how they were checked at the module level so that we could have more consistent typechecking results at REPL, e.g.:

> (struct foo () #:property prop:custom-write (lambda ([a : Integer] [b : Integer] [c : Integer]) : Void  (void)))
; readline-input:1:49: Type Checker: type mismatch
;   expected: (-> foo Output-Port (U Boolean One Zero) AnyValues)
;   given: (-> Integer Integer Integer AnyValues)
;   in: (lambda (a b c) (#%expression (#%app void)))
; [,bt for context]

The value for prop:custom-write above meets the contract so we can get around the issue and see the expected type error.

TL;DR At REPL, correlated expanded forms should/can be checked as a whole, but how to evaluate them properly is still unclear to me.

[capfredf]

I bet @samth @rmculpepper @mflatt have some ideas to help me solve this issue.