#:opaque allows passing higher-order values out with a flat contract, is unsound

[samth]

This program errors in the typed module.

#lang racket

(module m1 racket
  (provide f g)
  (define (f x) #t)
  (define (g x) (x 0)))

(module m2 typed/racket
  (require/typed (submod ".." m1)
                 [#:opaque F f]
                 [g (F -> Any)])
  (: fun : String -> String)
  (define (fun z) (string-append "hi" z))
  (if (f fun)
      (g fun)
      #t))

(require 'm2)

Possible solutions:

• F could turn into (and/c any-wrap/c f)
• we could generate some sort of cast at the site of the implicit upcast here (the call to g).
• ....

[samth]

See also: http://bugs.racket-lang.org/query/?cmd=view%20audit-trail&database=default&pr=13961