[plt-scheme] typed-scheme: conditional branches and parametric polymorphism

2010/1/28 Jon Zeppieri <zeppieri at gmail.com>:
> I'm using typed-scheme in 4.2.3 and running into the following:
>
> (: || (All (A T) ((Parser A T) (Parser A T) -> (Parser A T))))
> (define (|| p1 p2)
>   (λ (tks ncur nmax)
>     (let ((r1 (p1 tks ncur nmax)))
>       (cond ((Ok? r1) r1)
>             (else (p2 tks ncur nmax))))))
>
> This fails to typecheck, with the message:
> typecheck: Expected (U (Ok A T) Fail), but got #(struct:Ok (Any
> (Susp14 (U Stream-Null10 (Stream-Pair12 Any))) Integer Integer)) in:
> r1
>
> ... where the "r1" at the end of the message refers to the body of the
> first cond branch.
>
> Both type variables, A and T, are (it seems) instantiated as Any
> inside the branch.  It looks like the application of Ok? forces the
> instantiation.  To work around this, I can do:
>
> (: || (All (A T) ((Parser A T) (Parser A T) -> (Parser A T))))
> (define (|| p1 p2)
>  (λ (tks ncur nmax)
>    (let* ((r1 (p1 tks ncur nmax))
>           (cpy r1))
>      (cond ((Ok? cpy) r1)
>            (else (p2 tks ncur nmax))))))
>
> ... where, although r1 and cpy are synonyms, Ok? is never applied to
> r1, so its type variables are never instantiated. This code
> typechecks.
>
> Is this expected behavior?
>
> -Jon

Jon,

Try giving the binding of r1 an explicit type annotation in the
original version of the program (using the #{r1 : type} syntax).
Typed Scheme might need a little extra help in figuring out how to
instantiate its type.

--Carl