[racket] Help regarding typed racket and opaque types

On Fri, Jul 18, 2014 at 12:17 AM, Alexander D. Knauth <alexander at knauth.org>
wrote:

>
> On Jul 17, 2014, at 7:07 PM, Antonio Menezes Leitao <
> antonio.menezes.leitao at ist.utl.pt> wrote:
>
> > Hi,
> >
> > The following program typechecks:
> >
> > #lang typed/racket
> >
> > (define-type R Real)
> > (define-type Rs (Listof R))
> > (define-type ROrRs (U R Rs))
> >
> > (define (test [x : ROrRs]) : R
> >   (if (list? x)
> >       (if (null? x)
> >           (error "Less than one")
> >           (if (null? (cdr x))
> >               (car x)
> >               (error "More than one")))
> >       x))
> >
> > However, if we define R as an opaque type, e.g., using
> >
> > (require/typed racket [#:opaque MyReal real?])
> > (define-type R MyReal)
> >
> > then the program does not typecheck.
> >
> > I was expecting that the program should typecheck independently of the
> actual type being used for R. What am I missing?
>
> This doesn’t type check because as far as the type checker knows R could
> include a list type.
>
> Thanks. Now it's obvious.  Changing the code to use the opaque type
predicate solves the problem.

(define (test [x : ROrRs]) : R
  (if (real? x)
      x
      (if (null? x)
          (error "Less than one")
          (if (null? (cdr x))
              (car x)
              (error "More than one")))))

Best,
António.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20140718/e6aef2a3/attachment.html>