Make Opaque types correspond to positive predicates

[AlexKnauth]

This PR provides an RFC and an implementation to do 3 things to address #457 :

1. Change require/typed [#:opaque t pred] to give pred the type (-> Any Boolean : #:+ t) instead of type (-> Any Boolean : t). So if (pred x) returns true and then returns false, x still has type t after that.

2. Add make-positive-predicate and define-positive-predicate, to take a type and produce a predicate with only the positive #:+ proposition. So (make-positive-predicate t) will produce a predicate with the type (-> Any Boolean : #:+ t).

3. Change make-predicate to give a warning on Opaque types.

Things to clean up before it's ready:

• The warning for make-predicate on Opaque types should be improved, to recognize what form it came from and suggest alternative forms. When the warning is triggered by make-predicate, it should suggest using make-positive-predicate instead.

[AlexKnauth]

I'm not sure whether the warning message can be improved much further without adding more fields to the contract-def prefab structure just for this one warning message. Since that doesn't seem worth it, I hope this warning message will be enough:

warning: cannot safely generate exact predicate for Opaque type
  consider generating a positive-predicate instead
  type: Foo
  pred: foo?

[AlexKnauth]

After talking with @bennn, we've found a way to improve the warning message to recognize which form was used and suggest the positive version of that.

define-predicate: warning: cannot safely generate exact predicate for Opaque type
  (consider using define-positive-predicate instead)
  type: Foo
  pred: foo?
 in: (define-predicate is-foo? Foo)

[samth]

I think we should start with the backwards-compatibility issue here.

1. Does this break anything in the existing main-distribution (including tests/docs)?
2. Does this break anything in the package catalog (including tests/docs)?

2 can be checked using the pkg-build package -- @capfredf has some experience here.

[AlexKnauth]

The Main Distribution compiles without any new warnings. I haven’t run all the tests for those yet, but the runtime code shouldn’t be affected.

I haven’t tested everything on the package server (I’m not sure on the best way to do that, I’ll listen to @capfredf), put of the packages I already use, pict3d has new warnings for 2 uses of define-predicate, but those don’t stop compilation and can be fixed by define-positive-predicate without any errors.

[samth]

You should start by looking at https://github.com/racket/pkg-build and following the readme steps.

[capfredf]

@AlexKnauth Before building packages with an on-going version of typed-racket, you need to build a racket bundled with that version of TR. Here is what I did 8 months ago:

if the pkd-build runs on Ubuntu, then make installers and make site-from-installer must be run on Ubuntu as well

1. dowload/get latest version of racket. Use the corresponding raco to copy cataglog:
   raco pkg catalog-copy --from-config <target-catalog-dir>
2. adjust entries to the typed-racket collections in the <target-catalog-dir/pkg/> and point them to the version you want to test, i.e. the git url of your on-going typed racket
3. delete <target-catalog-dir/pkgs-all>
4. get a clean Racket repo
5. run make installers PKG="typed-racket" SRC_CATALOG= <target-catalog-dir>
6. run make site-from-installers
7. go to the build/site and start a http server. Make sure the server is accessible from other vms.
8. follow the steps in the readme of pkg-build, but you need to point the catalog url to the address of the http server.

if you run into any trouble, I'll be very happy to help you work them out.

[AlexKnauth]

@bennn and I are part-way through running pkg-build on this, and we've gotten an error on the admiral-edu-server package. In admiral-edu/pages/responses.rkt, there's an #:opaque type defined like this:

(require/typed web-server/servlet
               [#:opaque Response response?]
               ...)

On this require/typed the response? predicate is given a weaker type, (-> Any Boolean : #:+ Response) instead of (-> Any Boolean : Response). And there is a cond expression in admiral-edu/dispatch-typed.rkt that relies on the negative side:

     (cond [(response? page-result) page-result]
           [else (plain-page
                  "Assignments"
                  page-result)])

The else branch has less information known to the typechecker because response? is not guaranteed to return true on all values of type Response.

[samth]

What is the type of page-result? Could you just add a predicate for that instead of else?

In general, open PRs that fix everything that would break is probably the minimum needed for the backwards-incompatibility here.

[AlexKnauth]

The type of page-result is already Result, so the result? predicate check should be unnecessary. I've submitted a pull request to admiral-edu-server to fix it at jbclements/admiral-edu-server#42.

[bennn]

I ran a pkg-build. It seems to have failed (see below), but found a few packages that this PR breaks:

• graphics fix PR
• admiral-edu-server fix PR
• my-cond fix commit
• remap
• z3

This is the error that the log ends on:

Resolving "handy" via http://localhost:18333/built/catalog/
pkg: resolving via http://localhost:18333/built/catalog/pkg/handy?version=7.5.0.11
pkg: catalog response: #hash((author . "david.storrs@gmail.com") (checksum . "eebf73f88615dd7ee1f3ff83e174e04a74dfc792") (dependencies . (("html-parsing") ("base") ("db-lib") ("rackunit-lib") ("sxml") ("at-exp-lib"))) (description . "Utility functions that are missing from Racket -- e.g. 'say' (variadic displayln), 'multi-partition' (partition into more than two lists), better exception creation / trapping, database management, etc") (modules . ((lib "handy/sql.rkt") (lib "handy/test-more.rkt") (lib "handy/hash.rkt") (lib "handy/db.rkt") (lib "handy/deprecated/list-utils.rkt") (lib "handy/main.rkt") (lib "handy/list-utils.rkt") (lib "handy/net.rkt") (lib "handy/json.rkt") (lib "handy/try.rkt") (lib "handy/fsmonitor.rkt") (lib "handy/web.rkt") (lib "handy/struct.rkt") (lib "handy/utils.rkt") (lib "handy/thread.rkt") (lib "handy/HTML-TreeBuilder.rkt") (lib "handy/files/compression.rkt") (lib "handy/HTML-Element.rkt") (lib "handy/exceptions.rkt"))) (name . "handy") (ring . 2) (source . "http://localhost:18333/built/pkgs/handy.zip") (tags . ("database" "exceptions" "utility" "web")))
pkg: 	Assuming URL names a file
pkg: 		Downloading http://localhost:18333/built/pkgs/handy.zip to /var/tmp/15763982081576398208468-handy.zip
Downloading http://localhost:18333/built/pkgs/handy.zip
pkg: caching for ("http://localhost:18333/built/pkgs/handy.zip" "eebf73f88615dd7ee1f3ff83e174e04a74dfc792")
pkg: 	Downloading done, installing /var/tmp/15763982081576398208468-handy.zip as handy
user break
Timeout after 600 seconds
ssh: failed
  context...:
   /home/ben/code/racket/pkg-build-test/pkg-build/main.rkt:1397:5
   /home/ben/code/racket/pkg-build-test/pkg-build/main.rkt:123:0: build-pkgs57
   "/home/ben/code/racket/pkg-build-test/run.rkt": [running body]
   temp37_0
   for-loop
   run-module-instance!125
   perform-require!78
Stopping VirtualBox machine "Racket pkg-build"
0%...10%...20%...30%...40%...50%...60%...70%...80%...90%...100%