“Detached” type declarations with ->* not equivalent to “inline” in lambda

[LiberalArtist]

Summary: Writing “detached” type declarations using ->* (and similar type constructors) is not equivalent to writing the same types “inline” using typed/racket's version of lambda (and the function-header form of define). In particular, “detached” type declarations can work poorly with optional arguments' default value expressions.

What version of Racket are you using?

8.13 [cs]

What program did you run?

#lang typed/racket

(: add (->* [Integer] [(Setof Integer)] (Setof Integer)))
(define (add x [st (set)])
  (set-add st x))

and

#lang typed/racket
(define add-v1 : (->* [Integer] [(Setof Integer)] (Setof Integer))
  (λ (x [st (set)])
    (set-add st x)))

and

#lang typed/racket

(ann (λ (x [st (set)])
       (set-add st x))
     (->* [Integer] [(Setof Integer)] (Setof Integer)))

(Based on a report by Discord user fabricio and followup (1, 2, 3) by Moinate and @soegaard.)

What should have happened?

The programs should typecheck.

If you got an error message, please include it here.

Type Checker: Polymorphic function `set-add' could not be applied to arguments:
Types: (Setof e) e  -> (Setof e)
       (Listof e) e  -> (Listof e)
Arguments: (Setof Any) Integer
Expected result: (Setof Integer)
 in: (set-add st x)

Discussion

The following variants all do typecheck successfully:

#lang typed/racket

(define (add-v2 [x : Integer] [st : (Setof Integer) (set)]) : (Setof Integer)
  (set-add st x))

(: add-v3 (->* [Integer] [(Setof Integer)] (Setof Integer)))
(define (add-v3 x [st (set 80)])
  (set-add st x))

(: add-v4 (->* [Integer] [(Listof Integer)] (Listof Integer)))
(define (add-v4 x [st (list)])
  (set-add st x))

In add-v2, where the types are declared “inline”, the (set) expression is appropriately ascribed the type (Setof Integer), whereas in the problematic add it is over-generalized as (Setof Any), even though the same type information has been written down.

The add-v3 variant illustrates that the “detached” type declaration does work when the default-value expression avoids over-generalization. (Replacing (set 80) with (ann (set) (Setof Integer)) also works.) Also, inspection using :print-type suggests that Typed Racket represents the types of add-v2 and add-v3` differently:

> (:print-type add-v2)
(->* (Integer)
     ((U #<unsafe-undefined> (Setof Integer)))
     ((Setof Integer) : (Top | Bot)))
> (:print-type add-v3)
(->* (Integer) ((Setof Integer)) (Setof Integer))

The add-v4 variant, using lists instead of hash sets, is mostly a motivating example: explaining why add-v4 works when add doesn't requires getting into differences that it would be nicer to be able to treat as implementation details.

In principle, it would be possible to improve things for Setof along the lines of Listof by making a type-level distinction between empty and non-empty sets. However, that would not resolve the difference between “detached” and “inline” declarations.

It strikes me as particularly unfortunate that the “detached” style, which is generally encouraged, is the one with the worse behavior in this example.