[racket-dev] Typed Racket does not play nice with submodules

After playing around with Asumu’s branch to use require again instead of local-require, submodules still don’t work. I’m not sure why, but I’ve collected a series of examples of how different things fail in different ways. Perhaps someone more intimately familiar with the internals of Typed Racket and Racket’s module system can help to figure something out from this information.

First, I have this simple program:

#lang typed/racket/base

(require (for-syntax racket/base
                     syntax/parse
                     typed-racket/private/syntax-properties))

(define-syntax (begin-ignored stx)
  (syntax-parse stx
    [(_ ex:expr ...)
     (quasisyntax/loc stx
       #,(ignore #'(begin ex ...)))]))

(module foo racket
  (define x 7)
  (provide x))

(require 'foo)

(begin-ignored
  x)

This fails with the following error message:

link: module mismatch;
 possibly, bytecode file needs re-compile because dependencies changed
  importing module: 'explode
  exporting module: (submod "/tmp/explode.rkt" foo)
  exporting phase level: 0
  internal explanation: variable not provided (directly or indirectly) in: x

This is bizarre, and rather unhelpful. Note that this shouldn't involve any typechecking at all—using ignore should prevent that from happening—but somehow TR’s still making this fail. However, swapping typed/racket/base for typed/racket/base/no-check (perhaps unsurprisingly) makes it work fine.

Next up, I tried cheating a bit by using two submodules instead of just one. I hoped the following program would be a hacky workaround:

#lang typed/racket/base

(module foo racket/base
  (define x 7)
  (provide x))

(module bar typed/racket/base
  (require/typed
   (submod ".." foo)
   [x Number])
  (define y : Number x)
  (provide y))

(require 'bar)
y

Like the above, this program typechecks. However, it still fails with the exact same error message. Still, I was able to glean some more information from this oddity. Removing the final line of the program causes it to run successfully, as expected. Now, evaluating y in the REPL gives me a different error message:

Type Checker: missing type for identifier;
 consider using `require/typed' to import it
  identifier: y
  from module: (submod . bar) in: y

If anything, this feels even stranger. The provided variable is clearly typed, but apparently TR has decided it’s not. Why? I don’t know.

As a semi-interesting side note, simply changing the #lang declaration of the above program to racket/base makes it work without a hitch, demonstrating that the problem doesn’t seem to be within the require/typed form itself, but somehow has something to do with how TR handles the resulting binding?

Any ideas on what’s happening here? I’ve tried digging through some of the Typed Racket source, but I’m really too unfamiliar with how everything fits together to figure it out just yet.

Also, Asumu, a related problem: are there any issues with changing local-require back to require that would break anything else? Or can you possibly implement that change in TR with no issues?

> On Jan 12, 2015, at 08:06, Asumu Takikawa <asumu at ccs.neu.edu <mailto:asumu at ccs.neu.edu>> wrote:
> 
> On 2015-01-11 23:29:28 -0800, Alexis King wrote:
>>   This is a real problem, since Typed Racket’s require/typed form uses
>>   local-require, which in turn uses syntax-local-lift-require. This means
>>   that require/typed currently cannot require submodules.
> 
> Interesting, thanks for tracking this down! IIRC Typed Racket switched
> to using `local-require` in order to support uses of `require/typed` in
> the REPL/top-level.
> 
> (as the comment on
> https://github.com/racket/typed-racket/blob/master/typed-racket-lib/typed-racket/utils/require-contract.rkt#L57 <https://github.com/racket/typed-racket/blob/master/typed-racket-lib/typed-racket/utils/require-contract.rkt#L57>
> notes)
> 
> So one possible solution is to switch back to using `require` but also
> overhaul how TR handles the REPL to avoid these issues.
> 
> (for the REPL, local expanding everything at once doesn't work well
> because an early definition in a `begin` has to be registered
> before later clauses are typechecked)
> 
> Cheers,
> Asumu

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20150113/80c990de/attachment-0001.html>