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 <
racket-users@googlegroups.com> 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 racket-users+unsubscr...@googlegroups.com.
> 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 racket-users+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BYQymMfEN9yoA_4q8oCLJo2FWaVHw%2B6HQuTJ219-K0d0A%40mail.gmail.com.
