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

bennn commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 year ago

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 commented 1 month ago

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 commented 3 weeks ago

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.

racket / typed-racket