Coerce #f and pointer in typed racket

There is a function glfwCreateWindow. The last two arguments of this function are of type _pointer. How to properly import and annotate this function in typed/racket?

Here is what I'm doing right now:

(require/typed ffi/unsafe
  [#:opaque Pointer cpointer?])

(require/typed glfw3
  [glfwCreateWindow (-> Integer Integer String Pointer Pointer Pointer)])

(glfwCreateWindow 640 480 "My Window" #f #f)

But the type checker gives an error telling that it expects Pointer but given False. Even though (cpointer? #f) is true.

From my limited understanding of Typed Racket, you need to give it a chance to check whether (cpointer? #f) is true. So maybe something like

Welcome to DrRacket, version 8.11.1.4 [cs].
Language: typed/racket, with debugging [custom]; memory limit: 256 MB.
> (require/typed racket/bool
    [false Pointer])
> false
- : Pointer
#f

or

> (cast #f Pointer)
- : Pointer
#f
1 Like

What an #:opaque type means is that the only ways to construct it are to import it or to test a value with the specified predicate. So you can do something like this:

(glfwCreateWindow 640 480 "My Window" (assert #f cpointer?) (assert #f cpointer?))

Or you can change the type of glfwCreateWindow to explicitly include #f:

(require/typed glfw3
  [glfwCreateWindow (-> Integer Integer String (U Pointer #f) (U Pointer #f) Pointer)])
1 Like

Thank you guys for quick response :slight_smile:

All of three suggestions fixed compilation, but there is still a run-time warning:

cpointer?: contract violation
  any-wrap/c: Unable to protect opaque value passed as `Any`
  value: #<cpointer>
  This warning will become an error in a future release.
  in: the 1st argument of
      a part of the or/c of
      (or/c
       struct-predicate-procedure?/c
       (-> Any boolean?))
  contract from: (interface for cpointer?)

caused by

(require/typed ffi/unsafe
  [#:opaque Pointer cpointer?])

This and this gave me an idea of why I'm having this warning.

The final working version of my code is:

(require typed/racket/unsafe)

(unsafe-require/typed ffi/unsafe
  [#:opaque Pointer cpointer?])

(require/typed glfw3
  [glfwCreateWindow (-> Integer Integer String Pointer Pointer Pointer)])

(glfwCreateWindow 640 480 "My Window" (assert #f cpointer?) (assert #f cpointer?))

Thank you all for helping :slight_smile: