invoke-unit and unit-from-context can trigger an internal typechecker error

[lexi-lambda]

Update: this is no longer a soundness hole, see https://github.com/racket/typed-racket/issues/1305#issuecomment-1425010424.

---

The following program is accepted and produces garbage or segfaults on Racket 8.7:

#lang typed/racket

(define-signature a^ ([x : (Pairof Integer Integer)]))

(define-unit get-x@
  (import a^)
  (export)
  x)

(define v : (Pairof Integer Integer)
  (let ()
    (define-syntax (x stx)
      #'(quote not-an-integer))
    (invoke-unit get-x@ (import a^))))

(+ (car v) (cdr v))

[jbclements]

Your timing is ... well, I'm just about to start the final build. I think that this has been failing for quite a while:

Grossvogel:~/plt-admin (git)-[master]- clements> racket /tmp/zz.rkt
invalid memory reference.  Some debugging context lost
  context...:
   body of "/tmp/zz.rkt"
Grossvogel:~/plt-admin (git)-[master]- clements> /Applications/Racket\ v8.7/bin/racket /tmp/zz.rkt
invalid memory reference.  Some debugging context lost
  context...:
   body of "/tmp/zz.rkt"
Grossvogel:~/plt-admin (git)-[master]- clements> /Applications/Racket\ v8.6/bin/racket /tmp/zz.rkt
invalid memory reference.  Some debugging context lost
  context...:
   body of "/tmp/zz.rkt"
Grossvogel:~/plt-admin (git)-[master]- clements> /Applications/Racket\ v8.5/bin/racket /tmp/zz.rkt
invalid memory reference.  Some debugging context lost
  context...:
   body of "/tmp/zz.rkt"
Grossvogel:~/plt-admin (git)-[master]- clements> /Applications/Racket\ v8.4/bin/racket /tmp/zz.rkt
+: contract violation
  expected: number?
  given: #<garbage>
  context...:
   body of "/tmp/zz.rkt"
Grossvogel:~/plt-admin (git)-[master]- clements> /Applications/Racket\ v8.3/bin/racket /tmp/zz.rkt
invalid memory reference.  Some debugging context lost
  context...:
   body of "/tmp/zz.rkt"

... so I'm going to suggest that this should not block the release, even if the fix is simple.

[lexi-lambda]

Yes, I would not expect it to be a new issue. Definitely don’t worry about it for v8.8!

[samth]

That program is very worrying to me because I don't see how TR could ever be expected to handle that, and because I thought you had to define a unit from context to make that work.

[lexi-lambda]

I don’t think I understand your comment. Why don’t you think TR could ever be expected to handle that, and what do you mean by “I thought you had to define a unit from context to make that work”? invoke-unit with an import clause imports from the local context. (In fact, internally, it expands to unit-from-context.)

[lexi-lambda]

Here’s another related program that also triggers a segfault but does not require the definition of a local macro:

#lang racket

(module untyped racket
  (provide a^)
  (define-signature a^
    [x
     (define-values-for-export [x] 'not-a-pair)]))

(module typed typed/racket
  (require/typed (submod ".." untyped)
                 [#:signature a^ ([x : (Pairof Integer Integer)])])

  (define-unit get-x@
    (import a^)
    (export)
    x)

  (define v : (Pairof Integer Integer)
    (invoke-unit get-x@ (import a^)))

  (+ (car v) (cdr v)))

(require 'typed)

[lexi-lambda]

Some good news: #1306 downgrades this issue from a soundness hole to a typechecking failure. The first program now fails with the following error:

Internal Typechecker Error: cannot typecheck non-identifier export from unit-from-context
  export name: 'x
  export expression: #<syntax:tr-bug1.rkt:13:8 (quote not-an-integer)>

The second program fails with this one:

tr-bug2.rkt:19:4: Type Checker: missing type for identifier;
 consider adding a type annotation with `:'
  identifier: x6
  in: (invoke-unit get-x@ (import a^))

Both these programs are ultimately ill-typed, but they could in theory be modified to be well-typed. The second program probably ought to be rejected regardless, as TR is not supposed to support signatures containing definitions at all, which could be easily fixed. The first program, however, is more legitimate.

To summarize, I think this is still a bug, but it is much less serious, and unless someone actually runs into it in a real program, it may not be worth worrying about.