From 33522647fd256c9efb612a0e3984694b955865d1 Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Mon, 29 Apr 2019 17:34:49 -0400
Subject: [PATCH] allow polymorphic function definitions

---
 racket/typed/core-types.rkt        | 28 +++++++++++++++++++++++++++-
 racket/typed/tests/expressions.rkt | 19 +++++++++++++++++++
 2 files changed, 46 insertions(+), 1 deletion(-)

diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index 35cef8e..ef33880 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -1283,7 +1283,33 @@
   [(_ (f [x (~optional (~datum :)) ty] ...)
          e ...+) ≫
    ----------------------------
-   [≻ (define (f [x ty] ... -> ★/t) e ...)]])
+   [≻ (define (f [x ty] ... -> ★/t) e ...)]]
+  ;; Polymorphic definitions
+  [(_ ((~datum ∀) (X:id ...)
+                  (f [x (~optional (~datum :)) ty] ...
+                     (~or (~datum →) (~datum ->)) ty_out))
+      e ...+) ≫
+   #:with e+ #'(Λ (X ...)
+                  (lambda ([x : ty] ...)
+                    (begin e ...)))
+   [[X ≫ X- :: #%type] ... ⊢ e+ ≫ e-
+                       (⇒ : (~and res-ty
+                                  (~∀ (Y ...)
+                                      (~→ (~not (~Computation _ ...)) ...
+                                          (~Computation (~Value τ-v)
+                                                        _ ...)))))]
+   #:fail-unless (<: (type-eval #'(∀ (Y ...) τ-v))
+                     (type-eval #'(∀ (X ...) ty_out)))
+                 (format "expected different return type\n got ~a\n expected ~a\n"
+                         #'τ-v #'ty_out)
+   #:with f- (add-orig (generate-temporary #'f) #'f)
+   -------------------------------------------------------
+   [⊢ (define/intermediate f f- res-ty e-) (⇒ : ★/t)]]
+  [(_ ((~datum ∀) (X:id ...)
+                  (f [x (~optional (~datum :)) ty] ...))
+      e ...+) ≫
+   --------------------------------------------------
+   [≻ (define (∀ (X ...) (f [x ty] ... -> ★/t)) e ...)]])
 
 (define-typed-syntax begin
   [(_ e_unit ... e) ≫
diff --git a/racket/typed/tests/expressions.rkt b/racket/typed/tests/expressions.rkt
index 241474e..8630d2e 100644
--- a/racket/typed/tests/expressions.rkt
+++ b/racket/typed/tests/expressions.rkt
@@ -34,3 +34,22 @@
 (check-type ((inst poly-first Int String) (tuple 13 "XD"))
             : Int
             ⇒ 13)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Polymorphic Definitions
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define (∀ (X) (id2 [x : X] -> X))
+  x)
+
+(check-type ((inst id2 Int) 42)
+            : Int
+            ⇒ 42)
+
+(define (∀ (X) (id3 [x : X]))
+  x)
+
+(check-type (+ ((inst id3 Int) 42) 1)
+            : Int
+            ⇒ 43)
+