[racket] Typed racket puzzle (ii)

Greetings, all.

I'm terribly puzzled by a typed-racket error message I'm getting (I seem to be rather abusing this list today -- apologies -- but I'm busy reminding myself why it's useful not to do two interesting develoments with a project at one time).

If I run the following in DrRacket:

#lang typed/racket

(: my-func (String String -> String))
(define (my-func s1 s2)
  (string-append s1 ":" s2))

(my-func "Hello" "World")

(: call-func ((List String String) -> String))
(define (call-func string-list)
  ((inst apply String String) my-func string-list)
  ;(apply my-func string-list)
  )

(call-func '("Hello" "There"))

...I get an error message

> Type Checker: Cannot instantiate non-polymorphic type ((String * -> String) (Listof String) -> String) in: apply

Dr Racket also tells me that:

    > apply
    - : (All (a b) ((a * -> b) (Listof a) -> b))

Which makes sense, in that it corresponds to the message I'm seeing.

Now, I don't _really_ follow the logic of Typed Racket in a fully formal way (I know, I should have another go at The Little MLer), but the only way I can really make sense of this message is if the type (String String -> String) is not a subtype of (String * -> String), or if (List String String) is not a subtype of (Listof String).  Both of these would be a little unexpected.

Is that the right interpretation (in which case, where could I find the hierarchy of types?); or is APPLY being more particular about its types than is appropriate?

Thanks for any pointers.

Best wishes,

Norman


-- 
Norman Gray  :  http://nxg.me.uk
School of Physics and Astronomy, University of Glasgow, UK