Okay, submitted as bug. Many thanks to Matthias for reducing the example. John
> On Apr 30, 2021, at 4:12 AM, Sam Tobin-Hochstadt <[email protected]> wrote: > > This is a bug. It's not the the contract is unsatisfiable, it's that it's too > satisfiable. The contract system could probably make this work, but Typed > Racket should probably avoid this situation. > > Sam > > On Fri, Apr 30, 2021, 2:07 AM 'John Clements' via Racket Users > <[email protected]> wrote: > It seems that the conversion of TR types to contracts can result in contracts > like (or/c (cons/c any/c any/c) (cons/c any/c any/c)) that apparently cause > errors when run. > > I’m too tired to do a good job of providing a full example… no, actually, > it’s pretty easy. Run this program: > > #lang racket > > > (module foo typed/racket > > (provide val->autorun-table) > > (define-type Autorun-Result > (U (Pair 'success Any) > (Pair 'fail Any))) > > (define-type Autorun-Entry > (List String Autorun-Result)) > (define-predicate autorun-entry? Autorun-Entry) > > (define-type Autorun-Table (Listof Autorun-Entry)) > (define-predicate autorun-table? Autorun-Table) > > (define (val->autorun-table [val : Any]) > : (U False Autorun-Table) > (cond > [(list? val) > (define first-bad (findf (compose not autorun-entry?) val)) > (when first-bad > (fprintf (current-error-port) > "not an expected autorun entry:\n~e\n" > first-bad)) > (cast val Autorun-Table)] > [else > (error 'maybe-fetch-autorun-results > "result of read wasn't a list. moreinfo.")]))) > > (require 'foo) > > (val->autorun-table '(("1234" (fail (zz 1234) (d 9))))) > > > … see this error: > > val->autorun-table: broke its own contract > two of the clauses in the or/c might both match: (cons/c any/c Any) and > (cons/c any/c Any) > produced: '(fail (zz 1234) (d 9)) > in: the 2nd element of > an element of > a part of the or/c of > the range of > (-> > any/c > (or/c > #f > (listof > (list/c > any/c > (or/c > (cons/c any/c Any) > (cons/c any/c Any)))))) > contract from: (anonymous-module foo) > blaming: (anonymous-module foo) > (assuming the contract is correct) > at: 38-unsaved-editor:20.11 > > > Basically, it looks like the type is getting simplified a bit as it’s being > translated into a contract, and unfortunately, the resulting contract is > unsatisfiable? > > Is this a bug, or a known limitation? > > John > > > -- > You received this message because you are subscribed to the Google Groups > "Racket Users" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/racket-users/295471a4-99d9-4bbe-8e7b-351c1bb75e96%40mtasv.net. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/090e59fd-3e81-4ab9-9eea-85d643d095ab%40mtasv.net.
