From 041577d7bb5ed1e5b9e4eceb56648e81e81f18eb Mon Sep 17 00:00:00 2001
From: Eric Dobson <eric.n.dobson@gmail.com>
Date: Thu, 9 Jan 2014 22:08:55 -0800
Subject: [PATCH] Handle complicated parametric types in TR contract
 generation.

Closes PR 14270.

original commit: f394d3d26069467e8e6d023e5202b3b37e59ea0e
---
 .../static-contracts/equations.rkt            |  2 +-
 .../static-contracts/parametric-check.rkt     | 57 ++++++++++++++-----
 .../unit-tests/contract-tests.rkt             |  6 ++
 3 files changed, 50 insertions(+), 15 deletions(-)

diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/equations.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/equations.rkt
index 05d8bac8..1fb4af07 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/equations.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/equations.rkt
@@ -55,4 +55,4 @@
     values))
 
 (define (variable-ref v)
-  (hash-ref (current-variable-values) v))
+  (hash-ref (current-variable-values) v (lambda () (error 'variable-ref "No value available."))))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt
index 7900dada..ab058ff9 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/parametric-check.rkt
@@ -1,9 +1,16 @@
 #lang racket/base
 
+;; Implements a check that to determine if a part of a static contract has two (or more) parametric
+;; contracts as direct descendents.
+
 (require
   racket/match
-  racket/contract
-  (except-in "structures.rkt" recursive-contract)
+
+  [except-in racket/contract recursive-contract]
+  racket/dict
+  syntax/id-table
+  "structures.rkt"
+  "equations.rkt"
   "combinators/parametric.rkt"
   "combinators/structural.rkt")
 
@@ -11,16 +18,38 @@
   (contract-out
     [parametric-check (static-contract? . -> . boolean?)]))
 
+
 (define (parametric-check sc)
-  (let/ec exit
-    (define (recur sc variance)
-      (match sc
-        [(or/sc: elems ...) (=> continue)
-         (match elems
-           [(list-no-order (parametric-var/sc: _) (parametric-var/sc: _) others ...)
-            (exit #t)]
-           [else (continue)])]
-        [else
-          (sc-traverse sc recur)]))
-    (recur sc 'covariant)
-    #f))
+
+  (define eqs (make-equation-set))
+  (define vars (make-hash))
+  (define rec-vars (make-free-id-table))
+
+  (define (get-var sc)
+    (hash-ref! vars sc (lambda () (add-variable! eqs 0))))
+  (define (get-rec-var id)
+    (dict-ref! rec-vars id (lambda () (add-variable! eqs 0))))
+
+  (define (recur sc variance)
+    (match sc
+      [(or (or/sc: elems ...) (and/sc: elems ...))
+       (add-equation! eqs (get-var sc)
+                      (lambda () (for/sum ((e elems))
+                                   (variable-ref (get-var e)))))]
+      [(parametric-var/sc: id)
+       (add-equation! eqs (get-var sc) (lambda () 1))]
+      [(recursive-contract names values body)
+       (for ([name names] [value values])
+         (add-equation! eqs (get-rec-var name) (lambda () (variable-ref (get-var value)))))
+       (add-equation! eqs (get-var sc) (lambda () (variable-ref (get-var body))))]
+      [(recursive-contract-use id)
+       (add-equation! eqs (get-var sc) (lambda () (variable-ref (get-rec-var id))))]
+      [else
+       (get-var sc)])
+    (sc-traverse sc recur))
+
+  (recur sc 'covariant)
+
+  (for/or ([(k v) (in-hash (resolve-equations eqs))]
+           #:when (>= v 2))
+    #t))
diff --git a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
index d1c66bf3..58c5afaa 100644
--- a/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
+++ b/pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/contract-tests.rkt
@@ -68,11 +68,17 @@
               (t (-poly (a) (-set -Number)))
               (t (-poly (a) (-lst a)))
               (t (-poly (a) (-vec a)))
+              (t (-> (-poly (A B) (-> (Un A (-mu X (Un A (-lst X)))) (Un A (-mu X (Un A (-lst X))))))
+                     (-> -Symbol (-mu X (Un -Symbol (-lst X))))))
 
               (t/fail ((-poly (a) (-vec a)) . -> . -Symbol)
                       "cannot generate contract for non-function polymorphic type")
               (t/fail (-> (-poly (a b) (-> (Un a b) (Un a b))) Univ)
                       "multiple parametric contracts are not supported")
+              (t/fail
+                (-> (-poly (A B) (-> (Un B (-mu X (Un A (-lst X)))) (Un B (-mu X (Un A (-lst X))))))
+                    (-> -Symbol (-mu X (Un -Symbol (-lst X)))))
+                "multiple parametric contracts are not supported")
 
 
               (t/fail