<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Fri, Jul 18, 2014 at 12:17 AM, Alexander D. Knauth <span dir="ltr"><<a href="mailto:alexander@knauth.org" target="_blank">alexander@knauth.org</a>></span> wrote:<br>

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

<div>      (if (null? x)</div><div>          (error "Less than one")</div><div>          (if (null? (cdr x))</div><div>              (car x)</div><div>              (error "More than one"))))) </div><div>

<br></div><div>Best,</div><div>António.</div></div></div></div>