How does Typed Racket's type inference work?

Question

What kind of type inference does Typed Racket do? I found the following snippet on the Racket mailing list:

The Typed Racket type system contains a number of features that go beyond what's supported in Hindley/Milner style type systems, and so we can't use that inference system. Currently, Typed Racket uses local type inference to infer many of the types in your program, but we'd like to infer more of them -- this is an ongoing area of research.

The blurb above uses the term "local type inference", and I've also heard "occurrence typing" used a lot, but I'm not exactly sure what these terms mean.

It seems to me that the type inference system that Typed Racket currently uses is unnecessarily weak. Here's an example of what I mean. The following does not type check:

(struct: pt ([x : Real] [y : Real]))

(define (midpoint p1 p2)
  (pt (/ (+ (pt-x p1) (pt-x p2)) 2)
      (/ (+ (pt-y p1) (pt-y p2)) 2)))

You have to explicitly annotate midpoint with (: midpoint (pt pt -> pt)), otherwise you get the error: Type Checker: Expected pt, but got Any in: p1. Why can't the type checker just conclude from this that the types of p1 and p2 must be pt? Is this a fundamental limitation of the way that Racket implements types (i.e. is this line of reasoning actually wrong sometimes, because of some of Racket's more advanced type features), or is this something that could possibly be implemented in the future?

Answer 1

By default, unannotated top-level functions are assumed to have input and output types of Any. I offer this vague explanation: since Racket's type system is so flexible, it can sometimes infer types that you wouldn't expect, and allow some programs to typecheck when you might prefer them to emit a type error.

Tangent: you can also use the define: form if that is what suits you.

(define: (midpoint [p1 : pt] [p2 : pt]) : pt
  ...)