[plt-scheme] Predicates from Types

Hi all,

I have been using typed-scheme and funny thing is, it is so powerful
and flexible I sometimes start doing things with it I am not so sure I
should.

One example is the following:
I have several predicate forms, represented by structures: Quantifier,
Logic-Predicate, Relational-Predicate.

I could have all of these, inheriting from an empty structure
Predicate and the I would have Predicate? for free, however, it seems
given that I have typed scheme a bit nonsense to be doing this because
Predicate really has no fields and was just used to say, hey, all of
those are predicates. Then if a function received a predicate I would
check:
(unless (Predicate? x) (error ...))

With typed scheme I can remove that non-sensical structure and just do:
(define-type-alias Predicate (U Quantifier Logic-Predicate
Relational-Predicate))

and the function that should receive a predicate loses the guard and
is typed as receiving an argument of type predicate, but now I just
noticed... there are sometimes where I still need the Predicate?
predicate, and so what do I do now? Great would be to extract a
predicate from the type. On the other hand I could just go back to the
previous solution and I would have the type and the predicate by
defining the structure but hey, I don't need no make-Predicate or
anything so that would just be extra garbage that would be created
with the structure and not needed.

Is there then a way to extract a predicate from a type? Given I assume
the answer is no, what's the best solution for this?
Right now I had to define :
(: Predicate? (Any -> Boolean))
(define (Predicate? u)
     (or (Quantifier? u) (Logic-Predicate? u) ...))

Any hints on this issue would be great.

At the end of the day, I just noticed two things:
1 - Types help A LOT! Errors given by typed-scheme improve your code
and show problems with your code that you would only realize much
later if not using typed-scheme.
2 - I do not yet understand fully how to program with types using
scheme, such that porting a model checker to typed-scheme is not only
giving me a lot of headaches but is also in some way making me
re-design the whole system [which in a way I didn't want given that my
PhD has a deadline... :)].

Cheers,

-- 
Paulo Jorge Matos - pocmatos at gmail.com
Webpage: http://www.personal.soton.ac.uk/pocm