Add in let-poly bugs

also, misc clean ups of let-poly

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/apply-diffs.rkt

@@ -11,6 +11,7 @@
 (define directories (list "stlc"
                           "stlc-sub"
                           "poly-stlc"
+                          "let-poly"
                           "rbtrees"
                           "delim-cont"
                           "list-machine"

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff

@@ -0,0 +1,12 @@
+3c3
+< (define the-error "no error")
+---
+> (define the-error "use a lambda-bound variable where a type variable should have been")
+106c106
+<    (tc-down (x y Γ) M (λ y κ) σ_ans)
+---
+>    (tc-down (x y Γ) M (λ x κ) σ_ans)
+496a497,499
+> 
+> (define small-counter-example '(hd ((λ x x) 1)))
+> (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff

@@ -0,0 +1,25 @@
+3c3
+< (define the-error "no error")
+---
+> (define the-error "the classic polymorphic let + references bug")
+114c114
+<   [(where N_2 (subst N x v))
+---
+>   [(where N_2 (subst N x M))
+116c116
+<    (tc-down Γ ((λ y N_2) v) κ σ_2)
+---
+>    (tc-down Γ ((λ y N_2) M) κ σ_2)
+118,122d117
+<    (tc-down Γ (let ([x v]) N) κ σ_2)]
+< 
+<   [(where #t (not-v? M))
+<    (tc-down Γ ((λ x N) M) κ σ_2)
+<    ---------------------------------
+496a492,497
+> 
+> (define small-counter-example '(let ([x (new nil)])
+>                                  ((λ ignore
+>                                     ((hd (get x)) 1))
+>                                   ((set x) ((cons 5) nil)))))
+> (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff

@@ -0,0 +1,13 @@
+3c3
+< (define the-error "no error")
+---
+> (define the-error "mix up types in the function case")
+137c137
+<    (where G (unify τ_2 (τ_1 → x)))
+---
+>    (where G (unify τ_1 (τ_2 → x)))
+496a497,500
+> 
+> 
+> (define small-counter-example (term (1 cons)))
+> (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff

@@ -0,0 +1,14 @@
+3c3,5
+< (define the-error "no error")
+---
+> (define the-error
+>   (string-append "misspelled the name of a metafunction in a side-condition, "
+>                  "causing the occurs check to not happen"))
+212c214
+<   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+---
+>   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
+496a499,501
+> 
+> (define small-counter-example (term ((λ x (x x)) (λ x x))))
+> (check-equal? (check small-counter-example #f))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff

@@ -0,0 +1,18 @@
+3c3
+< (define the-error "no error")
+---
+> (define the-error "eliminate-G was written as if it always gets a Gx as input")
+225,226c225,228
+<   [(eliminate-G x τ (σ_1 σ_2 G))
+<    ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+---
+>   [(eliminate-G x τ (x σ G))
+>    (τ (eliminate-τ x τ σ) (eliminate-G x τ G))]
+>   [(eliminate-G x τ (y σ G))
+>    (y (eliminate-τ x τ σ) (eliminate-G x τ G))])
+496a499,503
+> 
+> (define small-counter-example (term (cons 1)))
+> (test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+>               (check small-counter-example))
+>             #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff

@@ -0,0 +1,14 @@
+3c3
+< (define the-error "no error")
+---
+> (define the-error "∨ has an incorrect duplicated variable, leading to an uncovered case")
+240c240
+<   [(∨ boolean_1 boolean_2) #t])
+---
+>   [(∨ boolean boolean) #t])
+496a497,501
+> 
+> (define small-counter-example (term ((λ x x) 1)))
+> (test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+>                (check small-counter-example))
+>             #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff

@@ -0,0 +1,21 @@
+3c3,5
+< (define the-error "no error")
+---
+> (define the-error
+>   (string-append "used let --> left-left-λ rewrite rule for let, "
+>                  "but the right-hand side is less polymorphic"))
+44,45c46
+<      (v E)
+<      (let ([x E]) M))
+---
+>      (v E))
+306,307c307,308
+<    (--> (Σ (in-hole E (let ([x v]) M)))
+<         (Σ (in-hole E (subst M x v)))
+---
+>    (--> (Σ (in-hole E (let ([x M]) N)))
+>         (Σ (in-hole E ((λ x N) M)))
+496a498,500
+> 
+> (define small-counter-example (term (let ((x (λ y y))) (x x))))
+> (test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt

@@ -0,0 +1,499 @@
+#lang racket/base
+
+(define the-error "use a lambda-bound variable where a type variable should have been")
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E)
+     (let ([x E]) M))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ x κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x v))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x v]) N) κ σ_2)]
+
+  [(where #t (not-v? M))
+   (tc-down Γ ((λ x N) M) κ σ_2)
+   ---------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_2 (τ_1 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean_1 boolean_2) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x v]) M)))
+        (Σ (in-hole E (subst M x v)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+(define small-counter-example '(hd ((λ x x) 1)))
+(test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt

@@ -0,0 +1,497 @@
+#lang racket/base
+
+(define the-error "the classic polymorphic let + references bug")
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E)
+     (let ([x E]) M))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x M))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) M) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_2 (τ_1 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean_1 boolean_2) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x v]) M)))
+        (Σ (in-hole E (subst M x v)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+(define small-counter-example '(let ([x (new nil)])
+                                 ((λ ignore
+                                    ((hd (get x)) 1))
+                                  ((set x) ((cons 5) nil)))))
+(test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt

@@ -0,0 +1,500 @@
+#lang racket/base
+
+(define the-error "mix up types in the function case")
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E)
+     (let ([x E]) M))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x v))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x v]) N) κ σ_2)]
+
+  [(where #t (not-v? M))
+   (tc-down Γ ((λ x N) M) κ σ_2)
+   ---------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_1 (τ_2 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean_1 boolean_2) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x v]) M)))
+        (Σ (in-hole E (subst M x v)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+
+(define small-counter-example (term (1 cons)))
+(test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt

@@ -0,0 +1,501 @@
+#lang racket/base
+
+(define the-error
+  (string-append "misspelled the name of a metafunction in a side-condition, "
+                 "causing the occurs check to not happen"))
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E)
+     (let ([x E]) M))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x v))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x v]) N) κ σ_2)]
+
+  [(where #t (not-v? M))
+   (tc-down Γ ((λ x N) M) κ σ_2)
+   ---------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_2 (τ_1 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean_1 boolean_2) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x v]) M)))
+        (Σ (in-hole E (subst M x v)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+(define small-counter-example (term ((λ x (x x)) (λ x x))))
+(test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt

@@ -1,6 +1,6 @@
 #lang racket/base
 
-(define the-error "no error")
+(define the-error "eliminate-G was written as if it always gets a Gx as input")
 
 (require redex/reduction-semantics
          (only-in redex/private/generate-term pick-an-index)
@@ -60,6 +60,22 @@
 (define M? (redex-match? stlc M))
 (define Σ-M? (redex-match? stlc (Σ M)))
 
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
 (define-judgment-form stlc
   #:mode (typeof I O)
   #:contract (typeof M σ)
@@ -87,7 +103,7 @@
    (tc-down Γ x κ σ_ans)]
   
   [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
-   (tc-down (x y Γ) M (λ y κ) σ_ans)  ;; BUG: the continuation had 'x' not 'y' in it
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
    ------------------------------------------------
    (tc-down Γ (λ x M) κ σ_ans)]
   
@@ -95,25 +111,10 @@
    --------------------------
    (tc-down Γ (M_1 M_2) κ σ_2)]
 
-#|
+  [(where N_2 (subst N x v))
-  ;; BUG: this is the classic bug -- it replaces the last two rules below
+   (where y ,(variable-not-in (term N_2) 'l))
-  [(where y ,(variable-not-in (term (x M N κ)) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
-   (tc-down Γ ((λ y (subst N x M)) M) κ σ_2)
+   ------------------------------------------
-   -----------------------------------------
-   (tc-down Γ (let ([x M]) N) κ σ_2)]
-|#
-  
-#|
-;; BUG: doesn't type check 'v' when x doesn't occur free in N
-;; I knew about this and yet STILL forgot to do it properly!
-  [(tc-down Γ (subst N x v) κ σ_2)
-   ----------------------------------
-   (tc-down Γ (let ([x v]) N) κ σ_2)]
-|#
-  
-  [(where y ,(variable-not-in (term (x v N κ)) 'l))
-   (tc-down Γ ((λ y (subst N x v)) v) κ σ_2)
-   ----------------------------------
    (tc-down Γ (let ([x v]) N) κ σ_2)]
 
   [(where #t (not-v? M))
@@ -133,29 +134,38 @@
    (tc-up τ (1 Γ M κ) σ_ans)]
   
   [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
-   (where G (unify τ_2 (τ_1 → x)))  ;; BUG: swap τ_2 and τ_1 in this line
+   (where G (unify τ_2 (τ_1 → x)))
    (tc-up (apply-subst-τ G x)
           (apply-subst-κ G κ)
           σ_ans)
    ---------------------------------------------------
    (tc-up τ_1 (2 τ_2 κ) σ_ans)]
   
-#|  
-  ;; BUG: this case was written assuming that τ_2 was 
-  ;; already an arrow type (which is wrong only when it is
-  ;; a variable:
-  [(where G (unify τ_1 τ_2))
-   (tc-up (apply-subst-τ G τ_3)
-          (apply-subst-κ G κ)
-          σ_ans)
-   -----------------------------------
-   (tc-up τ_1 (2 (τ_2 → τ_3) κ) σ_ans)]
-|#  
-  
   [(tc-up (τ_1 → τ_2) κ σ_ans)
    ---------------------------
    (tc-up τ_2 (λ τ_1 κ) σ_ans)])
 
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
 (define-metafunction stlc
   unify : τ τ -> Gx or ⊥
   [(unify τ σ) (uh (τ σ ·) · #f)])
@@ -166,17 +176,21 @@ Algorithm copied from _An Efficient Unification Algorithm_ by
 Alberto Martelli and Ugo Montanari (section 2).
 http://www.nsl.com/misc/papers/martelli-montanari.pdf
 
-The two iterate and the terminate rule are just how this code
+This isn't the eponymous algorithm; it is an earlier one
-searches for places to apply the rules; they are not from that 
+in the paper that's simpler.
-section in the paper.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
 
 |#
 
 (define-metafunction stlc
   uh : G G boolean -> Gx or ⊥
-  ;; iterate
+
   [(uh · G #t) (uh G · #f)]
-  ;; terminate
   [(uh · G #f) G]
   
   ;; (a)
@@ -195,7 +209,6 @@ section in the paper.
   [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
   
   ;; (d) -- x occurs in τ case
-  ;; BUG: had (in-vars? x τ) not (in-vars-τ? x τ)
   [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
   
   ;; (d) -- x does not occur in τ case
@@ -203,17 +216,9 @@ section in the paper.
    (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
    (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
   
-  ;; iterate
+  ;; no rules applied; try next equation, if any.
   [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
 
-(define-metafunction stlc
-  eliminate-G : x τ G -> G
-  [(eliminate-G x τ ·) ·]
-  [(eliminate-G x τ (σ_1 σ_2 G))
-   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
-
-#|
-;; BUG: eliminate-G was written as if it was getting a Gx as input:
 (define-metafunction stlc
   eliminate-G : x τ G -> G
   [(eliminate-G x τ ·) ·]
@@ -221,7 +226,6 @@ section in the paper.
    (τ (eliminate-τ x τ σ) (eliminate-G x τ G))]
   [(eliminate-G x τ (y σ G))
    (y (eliminate-τ x τ σ) (eliminate-G x τ G))])
-|#
 
 (define-metafunction stlc
   eliminate-τ : x τ σ -> σ
@@ -235,9 +239,6 @@ section in the paper.
 (define-metafunction stlc
   ∨ : boolean boolean -> boolean
   [(∨ #f #f) #f]
-  
-  ;; BUG: this case was [(∨ boolean boolean) #t]
-  ;; (which, of course, means that the two bools have to be the same)
   [(∨ boolean_1 boolean_2) #t])
 
 (define-metafunction stlc
@@ -284,32 +285,20 @@ section in the paper.
   [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
   [(apply-subst-Γ Gx ·) ·])
 
-(define-metafunction stlc
-  const-type0 : c -> σ
-  [(const-type0 +) (int → (int → int))]
-  [(const-type0 integer) int])
-
-(define-metafunction stlc
-  const-type1 : x c -> σ
-  [(const-type1 x nil) (list x)]
-  [(const-type1 x cons) (x → ((list x) → (list x)))]
-  [(const-type1 x hd) ((list x) → x)]
-  [(const-type1 x tl) ((list x) → (list x))]
-  [(const-type1 x new) (x → (ref x))]
-  [(const-type1 x get) ((ref x) → x)]
-  [(const-type1 x set) ((ref x) → (x → x))])
-
-(define-metafunction stlc
-  lookup-Γ : Γ x -> σ or #f
-  [(lookup-Γ (x σ Γ) x) σ]
-  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
-  [(lookup-Γ · x) #f])
-
 (define-metafunction stlc
   not-v? : M -> boolean
   [(not-v? v) #f]
   [(not-v? M) #t])
 
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
 (define red
   (reduction-relation
    stlc
@@ -319,15 +308,6 @@ section in the paper.
    (--> (Σ (in-hole E (let ([x v]) M)))
         (Σ (in-hole E (subst M x v)))
         "let")
-   #|
-;; BUG: this rule in place of the one above,
-;; plus no evaluation contexts of 'let'
-;; this bug is D because it only fails due to polymorphism -- subtle
-   (--> (Σ (in-hole E (let ([x M]) N)))
-        (Σ (in-hole E ((λ x N) M)))
-        "let")
-   |#
-   
    (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
         (Σ (in-hole E v_1))
         "hd")
@@ -354,6 +334,13 @@ section in the paper.
         (Σ (in-hole E (lookup-Σ Σ x)))
         "get")))
    
+#|
+
+Capture avoiding substitution
+
+|#
+
+
 (define-metafunction stlc
   subst : M x M -> M
   [(subst x x M_x)
@@ -393,6 +380,12 @@ section in the paper.
   [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
   [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
 
+#|
+
+A top-level evaluator
+
+|#
+
 (define/contract (Eval M)
   (-> M? (or/c "error" 'list 'λ 'ref number?))
   (define M-t (judgment-holds (typeof ,M τ) τ))
@@ -425,6 +418,12 @@ section in the paper.
   [(Σ->lets · M) M]
   [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
 
+#|
+
+A top-level type checker.
+
+|#
+
 (define/contract (type-check M)
   (-> M? (or/c τ? #f))
   (define M-t (judgment-holds (typeof ,M τ) τ))
@@ -436,11 +435,11 @@ section in the paper.
     [else
      (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
 
-(define (progress-holds? M)
+#|
-  (if (type-check M)
+
-      (or (v? M)
+Random generators
-          (not (null? (apply-reduction-relation red (term (· ,M))))))
+
-      #t))
+|#
 
 (define (generate-M-term)
   (generate-term stlc M 5))
@@ -448,37 +447,22 @@ section in the paper.
 (define (generate-typed-term)
   (match (generate-term stlc 
                         #:satisfying
-                        (typeof · M τ)
+                        (typeof M τ)
                         5)
-    [`(typeof · ,M ,τ)
+    [`(typeof ,M ,τ)
      M]
     [#f #f]))
 
 (define (typed-generator)
   (let ([g (redex-generator stlc 
-                            (typeof · M τ)
+                            (typeof M τ)
                             5)])
     (λ () 
       (match (g)
-        [`(typeof · ,M ,τ)
+        [`(typeof ,M ,τ)
          M]
         [#f #f]))))
 
-(define (check M)
-  (or (not M)
-      (v? M)
-      (let ([t-type (type-check M)])
-        (implies
-         t-type
-         (let ([red-res (apply-reduction-relation red `(· ,M))])
-           (and (= (length red-res) 1)
-                (let ([red-t (car red-res)])
-                  (or (equal? red-t "error")
-                      (match red-t
-                        [`(,Σ ,N)
-                         (let ([red-type (type-check (term (Σ->lets ,Σ ,N)))])
-                           (consistent-with? t-type red-type))])))))))))
-
 (define (generate-enum-term)
   (generate-term stlc M #:i-th (pick-an-index 0.035)))
 
@@ -489,4 +473,31 @@ section in the paper.
         (generate-term stlc M #:i-th index)
         (set! index (add1 index))))))
 
-;(time (redex-check stlc M (check (term M)) #:attempts 100000))
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+(define small-counter-example (term (cons 1)))
+(test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+              (check small-counter-example))
+            #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt

@@ -0,0 +1,501 @@
+#lang racket/base
+
+(define the-error "∨ has an incorrect duplicated variable, leading to an uncovered case")
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E)
+     (let ([x E]) M))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x v))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x v]) N) κ σ_2)]
+
+  [(where #t (not-v? M))
+   (tc-down Γ ((λ x N) M) κ σ_2)
+   ---------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_2 (τ_1 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean boolean) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x v]) M)))
+        (Σ (in-hole E (subst M x v)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+(define small-counter-example (term ((λ x x) 1)))
+(test-equal (with-handlers ([exn:fail? (λ (x) #f)])
+               (check small-counter-example))
+            #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt

@@ -0,0 +1,500 @@
+#lang racket/base
+
+(define the-error
+  (string-append "used let --> left-left-λ rewrite rule for let, "
+                 "but the right-hand side is less polymorphic"))
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x v))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x v]) N) κ σ_2)]
+
+  [(where #t (not-v? M))
+   (tc-down Γ ((λ x N) M) κ σ_2)
+   ---------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_2 (τ_1 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean_1 boolean_2) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x M]) N)))
+        (Σ (in-hole E ((λ x N) M)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))
+
+(define small-counter-example (term (let ((x (λ y y))) (x x))))
+(test-equal (check small-counter-example) #f)

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt

@@ -0,0 +1,496 @@
+#lang racket/base
+
+(define the-error "no error")
+
+(require redex/reduction-semantics
+         (only-in redex/private/generate-term pick-an-index)
+         racket/match
+         racket/list
+         racket/contract
+         racket/bool
+         (only-in "../stlc/tests-lib.rkt" consistent-with?))
+
+(provide (all-defined-out))
+
+(define-language stlc
+  (M N ::= 
+     (λ x M)
+     (M N)
+     x
+     c
+     (let ([x M]) N))
+  (Γ (x σ Γ)
+     ·)
+  (σ τ ::=
+     int
+     (σ → τ)
+     (list τ)
+     (ref τ)
+     x)
+  (c d ::= c0 c1)
+  (c0 ::= + integer)
+  (c1 ::= cons nil hd tl new get set)
+  (x y r ::= variable-not-otherwise-mentioned)
+  
+  (v (λ x M)
+     c
+     ((cons v) v)
+     (cons v)
+     (+ v)
+     (set v)
+     r)
+  (E hole
+     (E M)
+     (v E)
+     (let ([x E]) M))
+  (Σ ::= · (r v Σ))
+
+  (κ ::= 
+     · 
+     (λ τ κ)
+     (1 Γ M κ)
+     (2 τ κ))
+  
+  (G  ::= · (τ σ G))
+  (Gx ::= · (x σ Gx)))
+
+(define v? (redex-match? stlc v))
+(define τ? (redex-match? stlc τ))
+(define x? (redex-match? stlc x))
+(define M? (redex-match? stlc M))
+(define Σ-M? (redex-match? stlc (Σ M)))
+
+#|
+
+The typing judgment has no rule with multiple 
+(self-referential) premises. Instead, it explicitly
+manipulates a continuation so that it can, when it
+discovers a type equality, simply do the substitution
+through the continuation. This also makes it possible
+to easily generate fresh variables by picking ones
+that aren't in the expression or the continuation.
+
+The 'tc-down' rules recur thru the term to find a type
+of the left-most subexpression and the 'tc-up' rules
+bring that type back, recurring on the continuation.
+
+|#
+
+(define-judgment-form stlc
+  #:mode (typeof I O)
+  #:contract (typeof M σ)
+  
+  [(tc-down · M · σ)
+   -------------
+   (typeof M σ)])
+
+(define-judgment-form stlc
+  #:mode (tc-down I I I O)
+  #:contract (tc-down Γ M κ σ)
+  
+  [(tc-up (const-type0 c0) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c0 κ σ_ans)]
+  
+  [(where x ,(variable-not-in (term (Γ κ)) 'γ))
+   (tc-up (const-type1 x c1) κ σ_ans)
+   ------------------------------
+   (tc-down Γ c1 κ σ_ans)]
+  
+  [(where τ (lookup-Γ Γ x))
+   (tc-up τ κ σ_ans)
+   ---------------------------
+   (tc-down Γ x κ σ_ans)]
+  
+  [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-))
+   (tc-down (x y Γ) M (λ y κ) σ_ans)
+   ------------------------------------------------
+   (tc-down Γ (λ x M) κ σ_ans)]
+  
+  [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2)
+   --------------------------
+   (tc-down Γ (M_1 M_2) κ σ_2)]
+
+  [(where N_2 (subst N x v))
+   (where y ,(variable-not-in (term N_2) 'l))
+   (tc-down Γ ((λ y N_2) v) κ σ_2)
+   ------------------------------------------
+   (tc-down Γ (let ([x v]) N) κ σ_2)]
+
+  [(where #t (not-v? M))
+   (tc-down Γ ((λ x N) M) κ σ_2)
+   ---------------------------------
+   (tc-down Γ (let ([x M]) N) κ σ_2)])
+
+(define-judgment-form stlc
+  #:mode (tc-up I I O)
+  #:contract (tc-up τ κ σ)
+
+  [---------------------
+   (tc-up σ_ans · σ_ans)]
+  
+  [(tc-down Γ M (2 τ κ) σ_ans)
+   ---------------------------
+   (tc-up τ (1 Γ M κ) σ_ans)]
+  
+  [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-))
+   (where G (unify τ_2 (τ_1 → x)))
+   (tc-up (apply-subst-τ G x)
+          (apply-subst-κ G κ)
+          σ_ans)
+   ---------------------------------------------------
+   (tc-up τ_1 (2 τ_2 κ) σ_ans)]
+  
+  [(tc-up (τ_1 → τ_2) κ σ_ans)
+   ---------------------------
+   (tc-up τ_2 (λ τ_1 κ) σ_ans)])
+
+(define-metafunction stlc
+  const-type0 : c0 -> σ
+  [(const-type0 +) (int → (int → int))]
+  [(const-type0 integer) int])
+
+(define-metafunction stlc
+  const-type1 : x c1 -> σ
+  [(const-type1 x nil) (list x)]
+  [(const-type1 x cons) (x → ((list x) → (list x)))]
+  [(const-type1 x hd) ((list x) → x)]
+  [(const-type1 x tl) ((list x) → (list x))]
+  [(const-type1 x new) (x → (ref x))]
+  [(const-type1 x get) ((ref x) → x)]
+  [(const-type1 x set) ((ref x) → (x → x))])
+
+(define-metafunction stlc
+  lookup-Γ : Γ x -> σ or #f
+  [(lookup-Γ (x σ Γ) x) σ]
+  [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)]
+  [(lookup-Γ · x) #f])
+
+(define-metafunction stlc
+  unify : τ τ -> Gx or ⊥
+  [(unify τ σ) (uh (τ σ ·) · #f)])
+
+#|
+
+Algorithm copied from _An Efficient Unification Algorithm_ by 
+Alberto Martelli and Ugo Montanari (section 2).
+http://www.nsl.com/misc/papers/martelli-montanari.pdf
+
+This isn't the eponymous algorithm; it is an earlier one
+in the paper that's simpler.
+
+The 'uh' function iterates over a set of equations applying the
+rules from the paper, moving them from the first argument to
+the second argument and tracking when something changes.
+It runs until there are no more changes. The (a), (b),
+(c), and (d) are the rule labels from the paper.
+
+|#
+
+(define-metafunction stlc
+  uh : G G boolean -> Gx or ⊥
+
+  [(uh · G #t) (uh G · #f)]
+  [(uh · G #f) G]
+  
+  ;; (a)
+  [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))]
+  
+  ;; (b)
+  [(uh (x x G) G_r boolean) (uh G G_r #t)]
+  
+  ;; (c) -- term reduction
+  [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)]
+  [(uh ((list τ)    (list σ)    G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh ((ref τ)     (ref σ)     G) G_r boolean) (uh (τ σ G)               G_r #t)]
+  [(uh (int         int         G) G_r boolean) (uh G                     G_r #t)]
+  
+  ;; (c) -- failure
+  [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))]
+  
+  ;; (d) -- x occurs in τ case
+  [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))]
+  
+  ;; (d) -- x does not occur in τ case
+  [(uh (x τ G) G_r boolean)
+   (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t)
+   (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))]
+  
+  ;; no rules applied; try next equation, if any.
+  [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)])
+
+(define-metafunction stlc
+  eliminate-G : x τ G -> G
+  [(eliminate-G x τ ·) ·]
+  [(eliminate-G x τ (σ_1 σ_2 G))
+   ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))])
+
+(define-metafunction stlc
+  eliminate-τ : x τ σ -> σ
+  [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))]
+  [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))]
+  [(eliminate-τ x τ int) int]
+  [(eliminate-τ x τ x) τ]
+  [(eliminate-τ x τ y) y])
+
+(define-metafunction stlc
+  ∨ : boolean boolean -> boolean
+  [(∨ #f #f) #f]
+  [(∨ boolean_1 boolean_2) #t])
+
+(define-metafunction stlc
+  not-var? : τ -> boolean
+  [(not-var? x) #f]
+  [(not-var? τ) #t])
+
+(define-metafunction stlc
+  in-vars-τ? : x τ -> boolean
+  [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))]
+  [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)]
+  [(in-vars-τ? x int) #f]
+  [(in-vars-τ? x x) #t]
+  [(in-vars-τ? x y) #f])
+
+(define-metafunction stlc
+  in-vars-G? : x G -> boolean
+  [(in-vars-G? x ·) #f]
+  [(in-vars-G? x (x τ G)) #t]
+  [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) 
+                             (∨ (in-vars-τ? x τ)
+                                (in-vars-G? x G)))])
+
+(define-metafunction stlc
+  apply-subst-τ : Gx τ -> τ
+  [(apply-subst-τ · τ) τ]
+  [(apply-subst-τ (x τ G) σ)
+   (apply-subst-τ G (eliminate-τ x τ σ))])
+
+(define-metafunction stlc
+  apply-subst-κ : Gx κ -> κ
+  [(apply-subst-κ Gx ·) ·]
+  [(apply-subst-κ Gx (λ σ κ)) 
+   (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (1 Γ M κ))
+   (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))]
+  [(apply-subst-κ Gx (2 σ κ))
+   (2 (apply-subst-τ Gx σ)
+      (apply-subst-κ Gx κ))])
+
+(define-metafunction stlc
+  apply-subst-Γ : Gx Γ -> Γ
+  [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))]
+  [(apply-subst-Γ Gx ·) ·])
+
+(define-metafunction stlc
+  not-v? : M -> boolean
+  [(not-v? v) #f]
+  [(not-v? M) #t])
+
+#|
+
+The reduction relation rewrites a pair of
+a store and an expression to a new store
+and a new expression or into the string
+ "error" (for hd and tl of the empty list)
+
+|#
+
+(define red
+  (reduction-relation
+   stlc
+   (--> (Σ (in-hole E ((λ x M) v)))
+        (Σ (in-hole E (subst M x v)))
+        "βv")
+   (--> (Σ (in-hole E (let ([x v]) M)))
+        (Σ (in-hole E (subst M x v)))
+        "let")
+   (--> (Σ (in-hole E (hd ((cons v_1) v_2))))
+        (Σ (in-hole E v_1))
+        "hd")
+   (--> (Σ (in-hole E (tl ((cons v_1) v_2))))
+        (Σ (in-hole E v_2))
+        "tl")
+   (--> (Σ (in-hole E (hd nil)))
+        "error"
+        "hd-err")
+   (--> (Σ (in-hole E (tl nil)))
+        "error"
+        "tl-err")
+   (--> (Σ (in-hole E ((+ integer_1) integer_2)))
+        (Σ (in-hole E ,(+ (term integer_1) (term integer_2))))
+        "+")
+   (--> (Σ (in-hole E (new v)))
+        ((r v Σ) (in-hole E r))
+        (fresh r)
+        "ref")
+   (--> (Σ (in-hole E ((set x) v)))
+        ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x)))
+        "set")
+   (--> (Σ (in-hole E (get x)))
+        (Σ (in-hole E (lookup-Σ Σ x)))
+        "get")))
+   
+#|
+
+Capture avoiding substitution
+
+|#
+
+
+(define-metafunction stlc
+  subst : M x M -> M
+  [(subst x x M_x)
+   M_x]
+  [(subst (λ x M) x M_x)
+   (λ x M)]
+  [(subst (let ([x M]) N) x M_x)
+   (let ([x (subst M x M_x)]) N)]
+  [(subst (λ y M) x M_x)
+   (λ x_new (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (let ([y N]) M) x M_x)
+   (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x))
+   (where x_new ,(variable-not-in (term (x y M))
+                                  (term y)))]
+  [(subst (M N) x M_x)
+   ((subst M x M_x) (subst N x M_x))]
+  [(subst M x M_z)
+   M])
+
+(define-metafunction stlc
+  [(replace (any_1 ...) x_1 x_new)
+   ((replace any_1 x_1 x_new) ...)]
+  [(replace x_1 x_1 x_new)
+   x_new]
+  [(replace any_1 x_1 x_new)
+   any_1])
+
+(define-metafunction stlc
+  lookup-Σ : Σ x -> v
+  [(lookup-Σ (x v Σ) x) v]
+  [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)])
+
+(define-metafunction stlc
+  update-Σ : Σ x v -> Σ
+  [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)]
+  [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))])
+
+#|
+
+A top-level evaluator
+
+|#
+
+(define/contract (Eval M)
+  (-> M? (or/c "error" 'list 'λ 'ref number?))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (unless (pair? M-t)
+    (error 'Eval "doesn't typecheck: ~s" M))
+  (define res (apply-reduction-relation* red (term (· ,M))))
+  (unless (= 1 (length res))
+    (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res))
+  (define ans (car res))
+  (match (car res)
+    ["error" "error"]
+    [`(,Σ ,N)
+     (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ))
+     (unless (equal? M-t ans-t)
+       (error 'Eval "internal error: type soundness fails for ~s" M))
+     (match N
+       [(? x?) (cond
+                 [(term (in-dom? ,Σ ,N))
+                  'ref]
+                 [else
+                  (error 'Eval "internal error: reduced to a free variable ~s"
+                         M)])]
+       [(or `((cons ,_) ,_) `nil) 'list]
+       [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ]
+       [(? number?) N]
+       [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])]))
+
+(define-metafunction stlc
+  Σ->lets : Σ M -> M
+  [(Σ->lets · M) M]
+  [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))])
+
+#|
+
+A top-level type checker.
+
+|#
+
+(define/contract (type-check M)
+  (-> M? (or/c τ? #f))
+  (define M-t (judgment-holds (typeof ,M τ) τ))
+  (cond
+    [(empty? M-t)
+     #f]
+    [(null? (cdr M-t))
+     (car M-t)]
+    [else
+     (error 'type-check "non-unique type: ~s : ~s" M M-t)]))
+
+#|
+
+Random generators
+
+|#
+
+(define (generate-M-term)
+  (generate-term stlc M 5))
+
+(define (generate-typed-term)
+  (match (generate-term stlc 
+                        #:satisfying
+                        (typeof M τ)
+                        5)
+    [`(typeof ,M ,τ)
+     M]
+    [#f #f]))
+
+(define (typed-generator)
+  (let ([g (redex-generator stlc 
+                            (typeof M τ)
+                            5)])
+    (λ () 
+      (match (g)
+        [`(typeof ,M ,τ)
+         M]
+        [#f #f]))))
+
+(define (generate-enum-term)
+  (generate-term stlc M #:i-th (pick-an-index 0.035)))
+
+(define (ordered-enum-generator)
+  (let ([index 0])
+    (λ ()
+      (begin0
+        (generate-term stlc M #:i-th index)
+        (set! index (add1 index))))))
+
+#|
+
+Check to see if a combination of preservation
+and progress holds for every single term reachable
+from the given term.
+
+|#
+
+(define (check M)
+  (or (not M)
+      (let ([t-type (type-check M)])
+        (implies
+         t-type
+         (let loop ([Σ+M `(· ,M)])
+           (define new-type 
+             (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1)))))
+           (and (consistent-with? t-type new-type)
+                (or (v? (list-ref Σ+M 1))
+                    (let ([red-res (apply-reduction-relation red Σ+M)])
+                      (and (= (length red-res) 1)
+                           (let ([red-t (car red-res)])
+                             (or (equal? red-t "error")
+                                 (loop red-t))))))))))))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt

@@ -1,5 +1,5 @@
 #lang racket/base
-(require "let-poly-stlc-base.rkt" 
+(require "let-poly-base.rkt" 
          (only-in "../stlc/tests-lib.rkt" consistent-with?)
          redex/reduction-semantics)
 
@@ -38,8 +38,9 @@
 (test-equal (consistent-with? (term (subst (let ([z 11]) (let ([z1 12]) z)) q 1))
                               (term (let ([z 11]) (let ([z1 12]) z))))
             #t)
-
+(test-equal (consistent-with? (term (subst (let ((|| +)) ||) |1| (λ x1 x1)))
-
+                              (term (let ((|| +)) ||)))
+            #t)
 
 (test-equal (term (unify x int))
             (term (x int ·)))

pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt

@@ -14,7 +14,7 @@
       [(and (symbol? t1) 
             (symbol? t2)
             (not (equal? t1 t2))
-            (same-first-char? t1 t2))
+            (same-first-char-or-empty-and-numbers? t1 t2))
        (cond
          [(equal? t1 t2) #t]
          [else
@@ -26,12 +26,16 @@
              #t])])]
       [else (equal? t1 t2)])))
 
-(define (same-first-char? t1 t2)
+(define (same-first-char-or-empty-and-numbers? t1 t2)
   (define (first-char s) (string-ref (symbol->string s) 0))
-  (and (not (equal? t1 '||))
+  (cond
-       (not (equal? t2 '||))
+    [(equal? t1 '||)
+     (regexp-match #rx"[^[0-9]*$" (symbol->string t2))]
+    [(equal? t2 '||)
+     (regexp-match #rx"[^[0-9]*$" (symbol->string t1))]
+    [else
      (equal? (first-char t1)
-               (first-char t2))))
+             (first-char t2))]))
 
 (define-syntax-rule
   (stlc-tests uses-bound-var?