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

2010/1/28 Carl Eastlund <carl.eastlund at gmail.com>:
> 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
>

I've tried.  If I annotate r1 at the point where it's bound, that's
too early.  The type system doesn't consider r1's type variables
instantiated outside of the cond body expression.  And if I try to
annotate within the body expression, that's too late; it's an invalid
universalization.

-Jon