Re: [racket-users] A bug in the Typed Racket system?

2017-08-11 Thread Sourav Datta
Thanks for the clarification. On 09-Aug-2017 3:29 AM, "Sam Tobin-Hochstadt" wrote: > The reason that Typed Racket chooses the istantiation `Nothing` here > is that because `a` is used in both a positive and negative position > (both as an input and an output) in the type

Re: [racket-users] A bug in the Typed Racket system?

2017-08-08 Thread Sam Tobin-Hochstadt
The reason that Typed Racket chooses the istantiation `Nothing` here is that because `a` is used in both a positive and negative position (both as an input and an output) in the type of the `val` field, there's no way to pick a "best" choice for `a`. `(Foo Integer)` is not a subtype of `(Foo

Re: [racket-users] A bug in the Typed Racket system?

2017-07-21 Thread Sourav Datta
On Friday, July 21, 2017 at 9:06:16 PM UTC+5:30, Ben Greenman wrote: > Type inference is failing you again. Yes, well, that seems to be a common theme whenever I hover around the these type of areas which are uncommon but works perfectly fine in untyped Racket. > > > If you instantiate

Re: [racket-users] A bug in the Typed Racket system?

2017-07-21 Thread Ben Greenman
Type inference is failing you again. If you instantiate `foo/s`, you get the type you expect: #lang typed/racket (struct (a) Foo ([val : (-> a a)])) (: foo/s (All (a b) (-> (-> a b) (-> (Foo a) (Foo b) (Foo b)

[racket-users] A bug in the Typed Racket system?

2017-07-21 Thread Sourav Datta
Consider this program, #lang typed/racket (struct (a) Foo ([val : (-> a)])) (: foo/s (All (a b) (-> (-> a b) (-> (Foo a) (Foo b) (Foo b) (define (foo/s f) (λ ([f1 : (Foo a)] [f2 : (Foo b)]) f2))