(Typed Racket) -𝒾: contract violation blaming <pkgs>/soft-contract/parse/private.rkt

[bennn]

soft-contract blames itself when it tries to verify a program that depends on a typed racket program.

Example program

"b.rkt"

#lang typed/racket/base

(: f (-> Integer Integer))
(define (f x)
  (+ x 2))

(provide f)

"a.rkt"

#lang racket

(require "b.rkt")

(define (g x)
  (f (f x)))

(provide (contract-out (g (-> integer? integer?))))

Error Message

-𝒾: contract violation
  expected: (or/c String Symbol)
  given: '(#<path:/Users/ben/code/racket/my-pkgs/require-typed-scv/test/gtp/lnm/bug/b.rkt> #%contract-defs)
  in: the 2nd argument of
      (-> Symbol (or/c String Symbol) any)
  contract from: 
      <pkgs>/soft-contract/ast/definition.rkt
  blaming: <pkgs>/soft-contract/parse/private.rkt
   (assuming the contract is correct)
  at: <pkgs>/soft-contract/ast/definition.rkt:58.8
  context...:

[philnguyen]

I fixed the error, which came from the parser. But there are still problems from requiring a typed/racket module.

[philnguyen]

@bennn did you have a rudimentary way to convert types to contracts? Worst case I can try using that to convert everything to contracted untyped modules first...

[bennn]

Yes, very rudimentary. https://github.com/bennn/require-typed-scv/blob/master/private/parse-type.rkt#L17

Just parses surface syntax. It would be better to parse expanded TR syntax ... and I think that is the best we could do without changing TR's type->contract function to have a text backend.