On Thu, Nov 1, 2012 at 2:46 PM, Matthias Felleisen <matth...@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.rac...@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 >> sa...@ccs.neu.edu >> ____________________ >> Racket Users list: >> http://lists.racket-lang.org/users > -- sam th sa...@ccs.neu.edu ____________________ Racket Users list: http://lists.racket-lang.org/users
