"Inference for polymorphic keyword functions not supported"

Question

The following code produces the titular error:

(: f (∀ (a) (-> [#:x a] (U Integer a))))
(define (f #:x [x #f]) (or x 0))

(f #:x 3)

OK, but (f #:x (cast 3 Integer)) still produces the same error. Where is the type variable whose reified value racket is trying to infer, i.e. the type variable whose value I need to explictly specify?

Note: I tried casting (cast (f #:x (cast 3 Integer)) Integer), but DrRacket highlights only the inner (f ...) form wrt the type error.

Answer 1

The way to fix this is by annotating f itself, not the input or the output.

Also, you shouldn't be using cast for this, use ann instead of cast for assigning types to expressions. Using ann looks like (ann 3 Integer).

There are 2 ways to annotate f, either ann or inst will work.

ann

With ann, you can refine f's type to a non-polymorphic version of its type. The original type is (∀ (a) (-> [#:x a] (U Integer a))), so the non-polymorphic version with Integer is (-> [#:x Integer] Integer). Annotating f:

(ann f (-> [#:x Integer] Integer))

In context, annotating f within the function call:

((ann f (-> [#:x Integer] Integer)) #:x 3)

inst

The example with ann is long because it rewrites a specialized version of the type of f. For specializing polymorphic types, the shorter way is with inst:

(inst f Integer)

This automatically specializes the type to (-> [#:x Integer] Integer) for you, by replacing the type-parameter a with Integer. In context, annotating f within the function call:

((inst f Integer) #:x 3)