<p><br>
On Jul 5, 2012 8:50 PM, &quot;Neil Toronto&quot; &lt;<a href="mailto:neil.toronto@gmail.com">neil.toronto@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt; I just found this today:<br>
&gt;<br>
&gt;<br>
&gt; #lang typed/racket<br>
&gt;<br>
&gt; (define: b : (Boxof Any) (box 4))<br>
&gt;<br>
&gt; (define-predicate boxof-integer? (Boxof Integer))</p>
<p>This is the bug -- there&#39;s no way to write the boxof-integer? predicate, and define- predicate shouldn&#39;t think it can.</p>
<p>&gt; (define (set-b-box! v) (set-box! b v))<br>
&gt;<br>
&gt; (: a-very-listy-integer (-&gt; Integer))<br>
&gt; (define (a-very-listy-integer)<br>
&gt;   (cond [(boxof-integer? b)  (set-b-box! &#39;(1 2 3))<br>
&gt;                              (unbox b)]<br>
&gt;         [else  (error &#39;a-very-listy-integer &quot;can&#39;t happen&quot;)]))<br>
&gt;<br>
&gt;<br>
&gt; &gt; (a-very-listy-integer)<br>
&gt; - : Integer<br>
&gt; &#39;(1 2 3)<br>
&gt;<br>
&gt;<br>
&gt; Is this a bug or a limitation? It can be replicated with any mutable container type as far as I can tell.</p>
<p>A bug.  Anytime you get a result like that it&#39;s a bug.</p>
<p>&gt;<br>
&gt; Also, if it&#39;s a limitation, can I get (Vectorof Index) to be a subtype of (Vectorof Integer)?</p>
<p>No, that relationship would be unsound for similar reasons.</p>
<p>&gt; Neil ⊥<br>
&gt; _________________________<br>
&gt;  Racket Developers list:<br>
&gt;  <a href="http://lists.racket-lang.org/dev">http://lists.racket-lang.org/dev</a><br>
</p>