[racket] Typed Racket: problem with interaction between typed/untyped modules

Greetings,

I'm trying to implement a function wrapper, that given any function returns
a function of the same type, but that maybe applies a different argument.
So far I haven't been successful, and based on previous questions to the
mail list it seemed that I needed to go to an untyped module because I
couldn't constraint values to a given type.

With this approach I encountered a problem, that originates in the
contracts for polymorphic functions, I made a minimal example of my problem
below:

Module1
#lang racket
; (All (A B) ((A -> (T B)) A -> (T B)))
(define (untyped-wrap fun value)
  (fun "blabla"))

(provide untyped-wrap)

Module2
#lang typed/racket
(struct: (A) T ([value : A]))

(require/typed "untyped-wrap.rkt"
               [untyped-wrap (All (A B) ((A -> (T B)) A -> (T B)))])

(: wrap (All (A B) ((A -> (T B)) A -> (T B))))
(define (wrap fun value)
  (untyped-wrap fun value))

(: f (Any -> (T One)))
(define (f x) (T 1))

When I, from the typed Module1, evaluate:

(wrap f 1)

I get the error:

untyped-wrap: self-contract violation, expected a(n) A16; got: "blabla"
  contract from: (interface for untyped-wrap), blaming: (interface for
untyped-wrap)
  contract:
    (recursive-contract
     (parametric->/c
      (A16 B17) .......

My guesses:

First I thought that this should work because at the time I apply
untyped-wrap it is known that A = Any and B = One. But then I realized that
the typesystem can't prove that "blabla" is the right type for all A.

 Then I thought about instantiating the polymorphic function this way:

(: wrap (All (A B) ((A -> (T B)) A -> (T B))))
(define (wrap fun value)
  ( (inst untyped-wrap A B) fun value))

guessing again that A = Any and B = One should be known

but it fails with the same error....

When I write the concrete types it works.

I've been trying to write code to deal with functions in a general way,
while preserving the type, but it seems very hard to do right now in
typed/racket :-(

For instance, I had to make an ad-hoc cast going to an untyped module to
implement a function with type
(All (C D) (EL (C -> (EL D))) -> (EL (C -> (EL D)))), and then I tried the
same approach here, but this new error came up

I think it should be useful to provide a 'cast' operation. I think then I
could say something like, relying on contracts for checking at runtime:

Module2
#lang typed/racket
(struct: (A) T ([value : A]))

(require/typed "untyped-wrap.rkt"
               [untyped-wrap (Procedure Any -> (T Any))])
(: wrap (All (A B) ((A -> (T B)) A -> (T B))))
(define (wrap fun value)
  [CAST (untyped-wrap fun value) (T B)])

(: f (Any -> (T One)))
(define (f x) (T 1))

any suggestions on how can I achieve the behavior I want??

Thanks

-- 
Ismael
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/users/archive/attachments/20111202/53cccb6b/attachment.html>