[plt-scheme] check-expect and Typed Scheme

On Wed, Sep 3, 2008 at 4:12 PM, David Van Horn <dvanhorn at ccs.neu.edu> wrote:
> Matthias Felleisen wrote:
>>
>> No, not yet.
>
> OK.  On a related note... this doesn't behave as I expected.
>
> #lang typed-scheme
> (require/opaque-type KeyEvent key-event? htdp/world)
>
> Welcome to DrScheme, version 4.1.0.2-svn29aug2008 [3m].
> Language: Module; memory limit: 128 megabytes.
>> key-event?
> - : (Any -> Boolean : ((restrict KeyEvent)) ((remove KeyEvent)))
> #<procedure:pred-cnt>
>> (key-event? 'left)
> - : Boolean
> #t
>> (: k KeyEvent)
>> (define k 'left)
> typecheck: Expected KeyEvent, but got 'left in: (quote left)
>
>
> Is this a bug in Typed Scheme, or am I doing something wrong?

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?
-- 
sam th
samth at ccs.neu.edu