[racket] TR: Making recursive types as subtypes of non-recursive types

On 02/23/2012 03:16 PM, Sam Tobin-Hochstadt wrote:
> On Thu, Feb 23, 2012 at 1:30 PM, Neil Toronto<neil.toronto at gmail.com>  wrote:
>> (: set-id (All (a) ((Set a) ->  (Set a))))
>> (define (set-id A) A)
>>
>> (: set-id* (All (a) ((Set* a) ->  (Set* a))))
>> (define (set-id* A)
>>   ((inst set-id (U a (Set* a))) A))
>>
>>
>> Using `inst' makes the argument type pass, but I get an error on the return
>> type:
>>
>> Expected  (Rec T (U Empty-Set
>>                     (Opaque-Set (U a T))))
>>
>> but got          (U Empty-Set
>>                     (Opaque-Set (U a (Rec T (U Empty-Set
>>                                                (Opaque-Set (U a T)))))))
>>
>> I've formatted it so that it's easy to see that the body type is just an
>> unfold of the expected type. Is there a way to make TR realize that they're
>> isomorphic?
>
> That really should work, I'm not sure why it doesn't.

I sent a bug report with a more concrete example:

Would it be useful for TR to expose some of its recursive types 
machinery; i.e. provide `Fold' and `Unfold' as type constructors, for 
the cases where inference needs that kind of help? For example, I think 
this would be cleaner than wrapping `set-id' with `inst':

(define (set-id* A)
   (set-id (ann A (Unfold (Set* a)))))

But I don't know whether it would work. :)

Neil ⊥