DrRacket incorrectly marks required files as unused in certain cases

[vraid]

On DrRacket 6.4 An example program:

#lang typed/racket
(require math/flonum)
(fl 1)

Mouseover on "math/flonum" will show an arrow to the fl binding saying "1 bound occurrence", yet the file is marked red as though unused.

This seems to occur consistently for all files which are only required and used for type annotations, and for certain other bindings such as the above.

On the other hand, mouseover works as expected if fl is not used in a function call, e.g

#lang typed/racket
(require math/flonum)
fl

[rfindler]

This looks like a bug in Check Syntax, but if some kind TR maintainer were to make a racket/base program that did that, I'd be very thankful.

[samth]

I think the bug is that the require highlighting doesn't take into account 'disappeared-use properties, but I'll try to make a small test case.

[rfindler]

This example works, so it isn't that simple:

#lang racket/base
(require racket/list
         (for-syntax racket/base))

(define-syntax (m stx)
  (syntax-case stx ()
    [(_ x)
     (syntax-property
      #'(void)
      'disappeared-use (syntax-local-introduce #'x))]))

(m second)

[samth]

One clue: the problem goes away for the example at the top if we use #:no-optimize.

[samth]

@rfindler I've put some time into this, but can't make it happen without the TR optimizer, so I think maybe investigating from the check syntax end would be more fruitful. Or maybe @stamourv has ideas?

[stamourv]

I looked into it last month, but didn't find anything obvious.

[rfindler]

I looked into this a little bit (sorry it has taken so long to get back to it) and I noticed that TR is adding strange things. For example, with the program below, TR says that the character that's between positions 829 and 830 has the type (-> Positive-Integer Positive-Flonum), marked with an X in the code below. (There is another one, too.)

#lang typed/racket
(require math/flonum)
(fl 1)
fl
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;X;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

[rfindler]

Okay I think I understand what's happening and I believe it is a TR problem, not a DrRacket problem.

Specifically, TR is sending back inconsistent/incomplete information in syntax objects when the program type checks. It needs to not do that as Check Syntax is trusting that information (in particular, it sends back information that says that there is a require that isn't referenced in this case).

You can see this because this program:

#lang typed/racket
(require math/flonum)
(fl 1)
(1 1)

has the correct arrows, since TR sends no extra information and thus DrRacket uses only the actual fully expanded program. If you remove the bogus application from the program, then DrRacket sees a number of extra syntax objects that contain bogus (or maybe just incomplete) information.

After thinking a little bit about what this specific example contains, I'm not seeing how DrRacket can react properly to the extra information in general in a reasonable way. Thus my belief is that TR should just stop doing that instead of asking DrRacket to somehow try to connect the original information and figure out that there is a subset of the information and do something reasonable with it.

Hope that helps.

[rfindler]

PS: you may wish to write some tests that involve Check Syntax's take on the syntax objects you're providing. You can do so using the drracket/check-syntax library. Here's an example:

https://github.com/racket/redex/blob/master/redex-test/redex/tests/check-syntax-test.rkt

[rfindler]

(Assuming it works out, I recommend you test that there is nothing in the syntax objects except the type annotations.)

[samth]

Here's the information that Typed Racket sends to check syntax:

1. It sends the fully-expanded program to Check Syntax before running type checking, so that syntax coloring comes up before the potentially-long typechecking process finishes.
2. It send some syntax objects (which are always #'(void)) to check syntax with tooltip information for both the types of expressions in the program and any type errors in the program.
3. Once it's done type checking, online check syntax gets the fully-expanded syntax implicitly.

I think the wrong positions that @rfindler noticed are in the syntax objects in 2, but that this bug is because of a disagreement between 1 & 3.

@rfindler How can I see what syntax objects are confusing check syntax so that I can test this hypothesis?

Unfortunately, if that hypothesis is correct, I don't see what to do about this bug -- neither syntax object is changed by TR in any interesting way before being handed to CS.

[rfindler]

You can use the code I pointed you to earlier to see how CS reacts to the syntax objects. You can also put a printf on the x in process-trace-element in gui.rkt to save you the trouble and see the same information.

My read from the information that Check Syntax got is that your claims about 1 and 3 are incorrect and one of them is not seeing the reference to fl (in the program that has only one reference to fl in it). I had assumed this was because TR optimized it in some way. Are you sure they are the same?

[rfindler]

Just to be sure, when this program is processed:

#lang typed/racket
(require math/flonum)
(fl 1)

Check Syntax receives these four syntax objects:

(#%require math/flonum)
(#%app real->double-flonum '1)
(void)
(module anonymous-module typed/racket
  (#%module-begin
   (module configure-runtime '#%kernel
     (#%module-begin (#%require racket/runtime-config) (#%app configure '#f)))
   (begin-for-syntax
    (module*
     #%type-decl
     #f
     (#%plain-module-begin
      (#%declare #:empty-namespace)
      (#%require typed-racket/types/numeric-tower)
      (#%require typed-racket/env/type-name-env)
      (#%require typed-racket/env/global-env)
      (#%require typed-racket/env/type-alias-env)
      (#%require typed-racket/types/struct-table)
      (#%require typed-racket/types/abbrev)
      (#%require
       (just-meta 0 (rename racket/private/sort raw-sort sort))
       (only racket/private/sort)))))
   (begin-for-syntax
    (#%app
     add-mod!
     (#%app variable-reference->module-path-index (#%variable-reference))))
   (define-values
    (blame1)
    (#%app
     module-name-fixup
     (#%app variable-reference->module-source/submod (#%variable-reference))
     (#%app list)))
   (begin-for-syntax
    (#%require typed-racket/utils/redirect-contract)
    (module #%contract-defs-reference racket/base
      (#%module-begin
       (module configure-runtime '#%kernel
         (#%module-begin
          (#%require racket/runtime-config)
          (#%app configure '#f)))
       (#%require racket/runtime-path)
       (#%require (for-meta 1 racket/base))
       (define-values
        (contract-defs-submod)
        (let-values (((contract-defs-submod)
                      (let-values (((runtime?) '#t))
                        (#%app
                         list
                         'module
                         '(submod ".." #%contract-defs)
                         (#%variable-reference)))))
          (let-values (((get-dir) void))
            (#%app
             apply
             values
             (#%app
              resolve-paths
              (#%variable-reference)
              get-dir
              (#%app list contract-defs-submod))))))
       (begin-for-syntax
        (#%app
         register-ext-files
         (#%variable-reference)
         (let-values (((contract-defs-submod)
                       (let-values (((runtime?) '#f))
                         (#%app
                          list
                          'module
                          '(submod ".." #%contract-defs)
                          (#%variable-reference)))))
           (#%app list contract-defs-submod))))
       (#%provide contract-defs-submod)))
    (#%require (submod "." #%contract-defs-reference))
    (define-values
     (make-redirect2)
     (#%app make-make-redirect-to-contract contract-defs-submod)))
   (module*
    #%contract-defs
    #f
    (#%plain-module-begin
     (#%declare #:empty-namespace)
     (#%require (submod typed-racket/private/type-contract predicates))
     (#%require typed-racket/utils/utils)
     (#%require (for-meta 1 typed-racket/utils/utils))
     (#%require typed-racket/utils/any-wrap)
     (#%require typed-racket/utils/struct-type-c)
     (#%require typed-racket/utils/opaque-object)
     (#%require typed-racket/utils/evt-contract)
     (#%require typed-racket/utils/sealing-contract)
     (#%require typed-racket/utils/promise-not-name-contract)
     (#%require typed-racket/utils/simple-result-arrow)
     (#%require racket/sequence)
     (#%require racket/contract/parametric)))
   (#%require math/flonum)
   (#%app call-with-values (lambda () (#%app ->fl '1)) print-values)
   (#%provide)
   (#%app void)))

The first two come in a single message from TR, the the third comes in a single message, and finally the fourth. (I think that the fourth one is the one from the final expansion but I didn't confirm that specifically.)

So, all that is to say that I think you write things that are incorrect. Can you please double check?

[samth]

I think your experiments agree with what I wrote, although I see I was a little unclear.

What's sent in step 1 is the first two forms.

(#%require math/flonum)
(#%app real->double-flonum '1)

That's produced by these lines: https://github.com/racket/typed-racket/blob/master/typed-racket-lib/typed-racket/tc-setup.rkt#L63-L66 This is the result of fully expanding the program before type checking. Right now, it sends a list of forms to CS but it could include the (module ...) around it if that would help. I tried sending (syntax-local-introduce expanded-stx) (which begins (#%plain-module-begin ...)) but that still has the bug, and also caused the arrow for fl not to be drawn.

Then step 2 here is just the expression (void), which here won't have any interesting 'disappeared-use properties.

Step 3 is the last big form, which is the final result after TR is done with everything, and thus has all the extra metadata submodules that are there, along with the optimized version of (read->double-flonum 1) which is now (->fl 1).

[samth]

@rfindler I've been doing more digging with the show-content function, and I've encountered some behavior I don't understand that maybe you can help me with.

What I did was add this code to tc-setup.rkt inside the same (when (pair? exprs) ...):

          (printf ">>> initial CS output\n")
          (for-each (lambda (e) (pretty-print (show-content e))) (cdr exprs))
          (printf "<<< initial CS output\n")

Then I get this output for the very simple test file we've been using:

'(#(syncheck:add-background-color 25 32 "palegreen")
  #(syncheck:add-docs-menu
    25
    32
    require
    "View documentation for “require” from racket/base, racket"
    #<path:/home/samth/sw/plt/racket/doc/reference/require.html>
    (form ((lib "racket/private/base.rkt") require))
    "(form._((lib._racket/private/base..rkt)._require))"))
'(#(syncheck:add-background-color 25 32 "palegreen")
  #(syncheck:add-docs-menu
    25
    32
    require
    "View documentation for “require” from racket/base, racket"
    #<path:/home/samth/sw/plt/racket/doc/reference/require.html>
    (form ((lib "racket/private/base.rkt") require))
    "(form._((lib._racket/private/base..rkt)._require))"))
'(#(syncheck:add-background-color 59 61 "palegreen")
  #(syncheck:add-docs-menu
    59
    61
    fl
    "View documentation for “fl” from math/flonum"
    #<path:/home/samth/sw/plt/racket/doc/math/flonum.html>
    (def ((lib "math/flonum.rkt") fl))
    "(def._((lib._math/flonum..rkt)._fl))"))

But if I change the expression to (void (fl 1)), then there's no longer an entry for fl in the show-content output. Why does it disappear? Also, why are there two entries for require?

Then I tried adding this code:

          (printf ">>> initial CS output -- full module\n")
          (pretty-print (show-content (syntax-local-introduce expanded-stx)))
          (printf "<<< initial CS output -- full module\n")

and I got this error, which I was surprised by:

/tmp/x.rkt:1:0: #%plain-module-begin: illegal use (not a module body)
  in: (#%plain-module-begin (#%require math/flonum) (#%require racket/list) (#%app real->double-flonum (quote 1)))
  context...:
   /home/samth/sw/plt/extra-pkgs/drracket/drracket-tool-lib/drracket/check-syntax.rkt:51:0: show-content
   /home/samth/sw/plt/racket/collects/racket/contract/private/arrow-val-first.rkt:357:18
   /home/samth/sw/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/tc-setup.rkt:42:0: tc-setup
   /home/samth/sw/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/typed-racket.rkt:23:4

So I'm confused. I'll keep looking at the other places where TR communicates with CS, but I wanted to document my progress and questions so far.

[samth]

Also, I've now figured out why TR puts tooltips in weird places -- it's adding tooltips based on the location of syntax objects from other files. We should be able to fix this pretty easily, but I don't think it's what's causing the issue with require here.

[samth]

Taking out the code that logs the syntax object with the wrong locations doesn't change the behavior with require.

[rfindler]

Please don't send syntax object to check syntax that are program fragments and not complete programs.

[samth]

I'm happy to change TR to send different syntax objects, but I'm not sure what complete programs I should send. For step 1, TR calls local-expand on a syntax object of the form (#%plain-module-begin ...). Does the result of that call to local-expand count as a complete program for Check Syntax? If not, what should I do to produce a complete program instead?

For step 2, TR wants to send just some annotations that live in the 'mouse-over-tooltips syntax property, without sending any binding information. At the point that TR sends that, there isn't a new complete program, and TR doesn't want to communicate anything extra in the syntax object anyway. Do I need to send the same complete program again as in step 1? That seems like it would make extra work for Check Syntax. Is there some other complete program I could use?

[rfindler]

1) when you take a complete program of the form (module <stuff1> <stuff2> <stuff3>) and then remove the (module and some other bits from it, this is no longer the complete program.

In particular, from CS's point of view, you are sending over a sequence of top-level interactions (indeed, you are always sending over a sequence of top-level interactions from CS's point of view, it is just that sometimes they are top-level modules which is, I hope you agree, the case you want to be in).

2) The last expression that is sent from TR to CS does not contain any reference to fl in it, as far as I can tell. This is, I believe, the reason that the require line is turning red. If I don't miss my guess, the fl has turned into a reference to ->fl defined in optimizer/float.rkt on line 241 in my copy of TR.

[samth]

On 1) I understand what you mean by a complete program, but I'm trying to understand what TR should do here. TR doesn't work with a complete program in this sense, because it's entirely inside the expansion of (#%module-begin ...) and therefore doesn't even have access to to the "complete program" including the (module ...) form.

What TR wants to do is communicate the results of (local-expand (#%plain-module-begin ...)) early on, before type checking. I can see several ways to do that:

1. Just don't do it -- users have to wait until type checking is done before getting check syntax results. This is the way it used to work, but I'd be sad to have to go back to that.
2. Send the full results of that call to local-expand (which is still not a whole program). When I try that currently it gives slightly worse results than we currently get on the program in this bug, but maybe that'll be easier to make work sensibly long-term.
3. Synthesize a (module name lang []) wrapper around the results of the call to local-expand, and give that to CS. This seemed like it behaved roughly the same as option 1 when I tried it. It's not obvious where to get things like the name and language, or the syntactic context/source location for them, but we can probably come up with the right answers here if this is the right thing for CS.
4. Send the individual forms in the body of (#%plain-module-begin body ...) to CS one at a time. This is what TR currently does.

I'm happy to do any of 1-4 if you tell me which one works best for Check Syntax.

[samth]

On 2) Indeed that module doesn't explicitly refer to fl but I think there should be a 'disappeared-use property pointing to fl (really a property pointing to real->double-flonum which as a property pointing to fl but that indirection is something CS understands). Looking in the macro stepper tells me that it's on the (void) at the end of the file.

[rfindler]

On 1) you are free to generate any syntax objects that you wish to send to check syntax. Check syntax will do its best with them, but if you send something that is a series of expressions outside of a module, check syntax will treat them like a series of expressions outside of a module. It isn't about what "works best" for check syntax. It processes what it is given as if it were given a program. Give the program you want it to process.

On 2) are you using the same macro stepper that I am? Mine reports these identifiers on that (void) expression and none of them are fl and none of them come from the original program.

#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/flonum/flonum-functions.rkt:27:36 real->double-flonum>
#<syntax:/Users/robby/git/plt/racket/collects/racket/private/kw.rkt:929:26 #%app>
#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/flonum/flonum-polyfun.rkt:9:9 make-quotient-flpolyfun>
#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/flonum/flonum-polyfun.rkt:8:9 make-odd-flpolyfun>
#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/flonum/flonum-polyfun.rkt:6:9 make-flpolyfun>
#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/flonum/flonum-polyfun.rkt:7:9 make-even-flpolyfun>
#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/polynomial/chebyshev.rkt:14:9 inline-chebyshev-flpoly-fun>
#<syntax:/Users/robby/git/plt/racket/share/pkgs/math-lib/math/private/polynomial/chebyshev.rkt:10:9 chebyshev-poly>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:105:24 exn:fail:network>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:97:24 exn:fail:filesystem>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:97:24 exn:fail:filesystem>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:97:24 exn:fail:filesystem>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:97:24 exn:fail:filesystem>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:92:24 exn:fail:read>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:92:24 exn:fail:read>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:87:24 exn:fail:syntax>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:87:24 exn:fail:syntax>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:80:24 exn:fail:contract>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:80:24 exn:fail:contract>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:80:24 exn:fail:contract>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:80:24 exn:fail:contract>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:80:24 exn:fail:contract>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:78:22 exn:fail>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:41:29 exn>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:72:22 exn:break>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:72:22 exn:break>
#<syntax:/Users/robby/git/plt/extra-pkgs/typed-racket/typed-racket-lib/typed-racket/base-env/base-structs.rkt:41:29 exn>