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

(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)


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
   (submod ".." foo)
   [x Number])
  (define y : Number x)
  (provide y))

(require 'bar)

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 < 
> <>> 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
> <>
> 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

  Racket Developers list:

Reply via email to