[plt-scheme] check-expect and Typed Scheme

Sam TH wrote:
> So I think the answer is that you're expecting more from Opaque types
> than they provide.  All they give you is a type that you can check
> for.  In particular, if you haven't checked for it, it won't ever be a
> KeyEvent.  The only ways to construct a KeyEvent are to `require' one,
> or test for one with `key-event?'.  So even though (key-event? 'left)
> is #t, the typechecker doesn't know that.
> 
> Does that explain what's going on here?

Yes, thanks for the explanation Sam.  But can you see where I'm coming 
from based on the current documentation?

    The type is defined as precisely those
    values to which pred produces #t.

Since (key-event? 'left) is true, 'left has type KeyEvent.  Or so I 
thought.  Maybe you could update the docs to include some of the 
explanation you gave me?

Also, Richard captured much of what I was going to ask about, so I'm 
interested in hearing the response.

In this particular case, I could've also just defined a type alias 
KeyEvent for (U Symbol Char), without need for inj/proj functions.  Is 
there a benefit to one over the other?

David