diff --git a/collects/tests/typed-racket/fail/procedure-top.rkt b/collects/tests/typed-racket/fail/procedure-top.rkt
new file mode 100644
index 00000000..645af28b
--- /dev/null
+++ b/collects/tests/typed-racket/fail/procedure-top.rkt
@@ -0,0 +1,23 @@
+#;
+(exn-pred exn:fail:contract:arity?)
+#lang racket/load
+
+;; fail version
+
+(module example typed/racket
+  ;; coerces into unapplicable function
+  (: id (Procedure -> Procedure))
+  (define (id x) x)
+
+  (: f (Integer -> Integer))
+  (define (f x) (+ x 1))
+
+  (define g (id f))
+
+  ;; contract here should make sure g is not applicable
+  (provide g))
+
+(require 'example)
+
+;; g should now be unapplicable via case-> contract
+(g 3)
diff --git a/collects/tests/typed-racket/succeed/procedure-top.rkt b/collects/tests/typed-racket/succeed/procedure-top.rkt
new file mode 100644
index 00000000..338bccc2
--- /dev/null
+++ b/collects/tests/typed-racket/succeed/procedure-top.rkt
@@ -0,0 +1,21 @@
+#lang racket
+
+;; succeed version
+
+(module example typed/racket
+  ;; coerces into unapplicable function
+  (: id (Procedure -> Procedure))
+  (define (id x) x)
+
+  (: f (Integer -> Integer))
+  (define (f x) (+ x 1))
+
+  (define g (id f))
+
+  ;; contract here should allow application
+  (provide id))
+
+(require 'example)
+
+;; id's argument is procedure?, result is (case->)
+(id +)
diff --git a/collects/typed-racket/private/type-contract.rkt b/collects/typed-racket/private/type-contract.rkt
index 383e3af7..9f087587 100644
--- a/collects/typed-racket/private/type-contract.rkt
+++ b/collects/typed-racket/private/type-contract.rkt
@@ -129,7 +129,7 @@
         (loop t (not pos?) (not from-typed?) structs-seen kind))
       (define (t->c/fun f #:method [method? #f])
         (match f
-          [(Function: (list (top-arr:))) #'procedure?]
+          [(Function: (list (top-arr:))) (if pos? #'(case->) #'procedure?)]
           [(Function: arrs)
            (set-chaperone!)
            ;; Try to generate a single `->*' contract if possible.