Nested unit fails with "missing type for check-unit"

[philnguyen]

What version of Racket are you using?

v6.9.0.1

What program did you run?

#lang typed/racket/base

(require typed/racket/unit)

(define-unit a@
  (import)
  (export)

  (define-unit b@
    (import)
    (export))

  (define-values/invoke-unit/infer b@))

What should have happened?

Program ok

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

; Type Checker: missing type for identifier;
;  consider using `require/typed' to import it
;   identifier: check-unit
;   from module: private/unit-runtime.rkt
;   in: b@

[dfeltey]

@philnguyen Thanks for the bug report! I've made some progress on figuring out what's going on here, but a general fix is a tricky without a bigger change to typed racket. I'm not sure if I have the time to get to all of these bugs in a timely manner right now, are they blocking progress on your work?

If you don't mind sharing, I'm curious what you're using typed units for?

[philnguyen]

They're not blocking, as I usually figure out hacks to work around, so take your time :)

My contract verification project is written in TR, which normally takes ~6 minutes to compile from scratch. I realized that converting things to units for separate compilation improved compilation time significantly, especially when I repeatedly change files that would have been early in the dependency chain. I used to break some dependencies using parameters, but they get ugly quickly :)

[dfeltey]

Here's the overview of what's currently preventing a general solution to the problem of using define-values/invoke-unit inside of a definition context.

Part of the problem is due to the way that define-values/invoke-unit expands inside of a definition context. Here's an untyped macro that demonstrates the issue with the typed implementation of define-values/invoke-unit:

#lang racket

(define-for-syntax (ignore stx)
  (syntax-property stx 'ignore #t))

(define-syntax (expand-to-definition stx)
  (syntax-case stx ()
    [(_ id)
     (quasisyntax/loc stx
       (begin
         (define-values () (begin (quote-syntax (internal id Integer)) (values)))
         #,(ignore
            (quasisyntax/loc stx (define id 17)))))]))

(let ()
  (expand-to-definition foo)
  foo)

The let expression in this program expands to something that looks like this:

(let-values ()
        (let-values ((() (begin (quote-syntax (internal foo Integer)) (#%app values))))
          (let-values (((foo) (quote 17))) foo))))

With the ignore property around the binding pair ((foo) (quote 17)).

If the typechecking for let could ignore binding pairs that were marked with the tr:ignore property that would make a general solution for this bug fairly straightforward. I understand the problem with ignoring binding pairs generally because those identifiers may be used and need types. In the case of define-values/invoke-unit, however the typed macro leaves behind the syntax of an internal form that should be used to register the types for these identifiers.

Would it be reasonable to change let typechecking to respect the ignore properties on binding pairs like this?