require/untyped-contract leads to errors in no-check, Shallow, and Optional

[bennn]

What version of Racket are you using?

Welcome to Racket v8.6.0.9 [cs].

What program did you run?

This program is ok with normal TR and not okay for shallow, optional, and no-check

server.rkt

#lang typed/racket/shallow ;optional ;no-check

(provide mynum check-array-shape)

(define mynum 42)

(define-type (MVec T) (Mutable-Vectorof T))

(define-type Indexes (MVec Index))
(define-type In-Indexes (U (MVec Integer) Indexes))

(: check-array-shape (In-Indexes (-> Nothing) -> Indexes))
(define (check-array-shape ds fail)
  (define dims (vector-length ds))
  (define: new-ds : Indexes (make-vector dims 0))
  (let loop ([#{i : Nonnegative-Fixnum} 0])
    (cond [(i . < . dims)
           (define di (vector-ref ds i))
           (cond [(index? di)  (vector-set! new-ds i di)
                               (loop (+ i 1))]
                 [else  (fail)])]
          [else  new-ds])))

main.rkt

#lang racket/base

(require typed/untyped-utils
         typed/racket/no-check
         (except-in "server.rkt"
                    check-array-shape))

(require/untyped-contract
 "server.rkt"
 [check-array-shape  ((Vectorof Integer) (-> Nothing) -> (Vectorof Index))])

(check-array-shape (vector 1 2 3) (lambda () (error 'die)))

What should have happened?

No error

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

Shallow

/home/ben/code/racket/fork/extra-pkgs/typed-racket/typed-racket-lib/typed/untyped-utils.rkt:64:13:
Type Checker: type mismatch
  expected: (-> (Vectorof Integer) (-> Nothing) (Vectorof Index))
  given: (-> In-Indexes (-> Nothing) Indexes)
  in: (define check-array-shape check-array-shape2)

no-check

/home/ben/code/racket/fork/extra-pkgs/typed-racket/typed-racket-lib/typed/untyped-utils.rkt:64:13:
Type Checker: missing type for identifier;
 consider using `require/typed' to import it
  identifier: check-array-shape2
  from module: test-ruc-server.rkt
  in: (define check-array-shape check-array-shape2)

PS thanks to @Rscho314 for the report in https://github.com/racket/math/issues/75

[bennn]

Ideas:

• let require/untyped-contract know what language the server is using
• use unsafe-require/typed somehow inside require/untyped-contract --- which probably means we need to fix unsafe-require/typed to work for optional/shallow => deep

[Rscho314]

Hi @bennn ,

I have posted some seemingly working code to add a language specification to require/untyped-contract. Two questions:

• I guess I should make the language spec argument optional, to avoid breaking existing code?
• Another idea would be fetching the language spec automatically from the imported module. Do you think that's worth pursuing?

Best, Raoul

[racket-discourse-github-bot]

This issue has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/replacing-lexical-context-in-a-macro/2004/1

[bennn]

Yes, language spec should be optional.

Fetching automatically seems too hard. It may have trouble with identifiers that get reprovided by TR languages (Shallow -> Deep -> require/untyped-contract).

[bennn]

I'm confused now. Does it even make sense to use require/untyped-contract on a shallow module? EDIT: I think not, because shallow contract gen doesn't take a fail callback the way deep does [link]. It can still error if the match fails, but that's not supposed to happen.

(It doesn't make sense for no-check because that language doesn't generate contracts at all.)

Maybe the right thing is just a better error message.