Is there an unsafe cast function in Typed Racket?

Is there an unsafe version of the cast function in Typed Racket?

I'd like to use this to be able to add a proposition that I logically know about, but the type system can't figure out.

For instance, I might have a predicate that checks that a list has exactly two elements:

#lang typed/racket

(: func (-> (Listof String) Boolean))
(define (func x) (eq? (length x) 2))

I'd like to inform the type system of a proposition that the input list has exactly two elements:

(: func2 (-> (Listof String) Boolean : (List String String)))
(define func2
  (cast func (-> (Listof String) Boolean : (List String String))))

However, when trying to do this, I get an error like the following:

Type Checker: Type (-> (Listof String) Boolean : (List String String))
could not be converted to a contract: cannot generate contract for
function type with props or objects.                              
in: (-> (Listof String) Boolean : (List String String))

Is there some version of the cast function where I can tell the type system, "Just trust me here."

I'm imagining this function being similar to unsafeCoerce in Haskell.

Solution

It is possible to define an unsafe-cast with the type (All (A) (-> Any A)) by using unsafe-require/typed. However if you do this, please turn off the optimizer.

If the typed racket optimizer is on, it will trust the types to the point of breaking memory safety if they're off. You might also want to turn off the optimizer not just in the module you use unsafe-cast in, but also other typed modules that interact with it.

Turn off the optimizer for a typed racket module using #:no-optimize:

#lang typed/racket #:no-optimize

And then, with great care, and putting #:no-optimize on probably every typed module in your program, you can use unsafe-require/typed:

#lang typed/racket #:no-optimize
(require typed/racket/unsafe)
(unsafe-require/typed racket/function
                      [(identity unsafe-cast)
                       (All (A) (-> Any A))])

However, for your particular example, I personally would try to avoid unsafe-cast by rewriting the function:

(: func2 (-> (Listof String) Boolean : (List String String)))
(define (func2 x)
  (and (cons? x) (cons? (rest x)) (empty? (rest (rest x)))))

This function avoids computing the length of long lists when it doesn't need to, and passes the typechecker with the (List String String) proposition.