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
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
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
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)
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))
5 matches
Mail list logo