[racket] DRRacket Check Syntax Loops Endlessly (Sample Provided)

On Thu, Nov 1, 2012 at 2:46 PM, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
> Since S0 is a function from T :: Type to some Union and TR doesn't allow this, you want to signal a syntax error here. Correct?

No, this program is fine from a typed perspective.  The only problem
is in contract generation, which loops when it should just fail (I
don't think this program has a sensible translation to contracts).

>
>
> On Nov 1, 2012, at 12:16 PM, Sam Tobin-Hochstadt wrote:
>
>> On Thu, Nov 1, 2012 at 12:07 PM, Ray Racine <ray.racine at gmail.com> wrote:
>>> Fresh build from Racket git MASTER, the following causes DRRacket's Check
>>> Syntax to loop without termination.
>>
>> Clearly, this isn't the behavior you want, but I don't think a
>> contract is possible to generate for this code.
>>
>> If you change the type of the S2-x field to `(S0 T)`, then it works.
>> That might even have been what you wanted.
>>
>>>
>>> #lang typed/racket/base
>>>
>>> (provide f)
>>>
>>> (struct: (T) S1 ([x : (Listof String)]))
>>>
>>> (struct: (T) S2 ([x : S0]
>>>                 [g : (T -> Boolean)]))
>>>
>>> (define-type (S0 T) (U (S1 T) (S2 T)))
>>>
>>> (: f (String -> (S0 String)))
>>> (define (f x)
>>>  (S1 '()))
>>>
>>> ____________________
>>>  Racket Users list:
>>>  http://lists.racket-lang.org/users
>>>
>>
>>
>>
>> --
>> sam th
>> samth at ccs.neu.edu
>> ____________________
>>  Racket Users list:
>>  http://lists.racket-lang.org/users
>



--
sam th
samth at ccs.neu.edu