Its even simpler than that because the cases in case-> are ordered. There are some intricacies when the first order checks of non flat contracts overlap, but with non overlapping first order checks for higher order contracts or only flat contracts it should be doable. I don't have a lot of time for TR hacking currently, but if a bug is filed I may get to it at some point. <div class="gmail_quote">On Nov 17, 2012 11:33 AM, "Robby Findler" <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> This has come up enough times that maybe TR should convert contracts of the form: (case-> (-> <flat> ...) (-> <flat> ...)) into a dependent contract that checks the two 'flat' things? (I guess you'd have to have an ordering on types in case they overlap, but I presume you have this already.) On Sat, Nov 17, 2012 at 1:18 PM, Jens Axel Søgaard <<a href="mailto:jensaxel@soegaard.net">jensaxel@soegaard.net</a>> wrote: > I have the following contract on next-prime : > > (: next-prime : (case-> (N -> N) (Z -> Z)) ) > > It says that for all primes p, positive or negative, (next-prime p) > will be an integer. > Furthermore if p is a natural number, then (next-prime p) will also be > a natural number. > > This type can't be converted to a contract: > Type Checker: The type of next-prime cannot be converted to a > contract in: (next-prime 4) > > My understanding is that a since N is a subset of Z a predicate can't > determine whether > which case to use. Is there an alternative construct, that I can use > in order to get > a contract? > > My temporary solution is to provide untyped-next-prime > > (: untyped-next-prime : Z -> Z) > (define (untyped-next-prime z) > (next-prime z)) > > whose type can be converted to a contract. > > > See details in: > <a href="https://github.com/plt/racket/blob/master/collects/math/private/number-theory/number-theory.rkt" target="_blank">https://github.com/plt/racket/blob/master/collects/math/private/number-theory/number-theory.rkt</a> > > -- > Jens Axel Søgaard > > ____________________ > Racket Users list: > <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> ____________________ Racket Users list: <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a> </blockquote></div>