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

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).
• ....

Run the Racket program in the issue to reproduce the unsound higher-order value flow. Start by tracing require/typed handling of #:opaque and the implicit upcast at the call to g. Done means the typed module no longer permits higher-order values to escape through a flat contract unsafely, with a sound behavior chosen and validated.