[racket] Dynamic define-predicate

I'd like to use Typed Racket to create an interpreter for a typed lambda 
calculus, which *inherits* Typed Racket's type system. (In other words, 
I'm lazy and I don't want to make my own type system. But who does? 
Except maybe Sam? :p) I was counting on occurrence typing to allow me to 
do it while threading an Any-valued hash table environment, but I'm stuck.

Here's a snippet containing just the environment lookup function "id" 
and relevant types:

#lang typed/racket

(define-type Env (HashTable Symbol Any))
(define: empty-env : Env (make-immutable-hash empty))

; type of environment idiom/monad computations:
(define-type (I a) (Env -> a))

(: id (All (a) (Symbol -> (I a))))
(define ((id name) env)
   (define-predicate a? a)
   (let ([val  (hash-ref
                env name
                (lambda () (error 'id "not in scope: ~e" name)))])
     (if (a? val)
         val
         (error 'id "runtime type error: unexpected value ~e" val))))


Running it gives:

Type Checker: Cannot apply expression of type False, since it is not a 
function type in: (a? val)


I know the immediate trouble is with (define-predicate a? a). To behave 
like I want it to, the type checker would have to look up or create the 
predicate corresponding to the type of "a" at run time rather than 
compile time.

Is there a deep/theoretical reason it can't work? Is there another way 
to accomplish what I want that doesn't require passing a predicate to 
"id"? (If I did that, I'd have to make the macro that expands to 
expressions of type (I a) either keep track of types as it expands or 
recursively transform ids in lambda bodies.)

Thanks!
Neil T