refactor all implementations to use contracts

14 files changed, 975 insertions, 853 deletions

diff --git a/base.rkt b/base.rkt
index c88a8ee..09cb2e7 100644
--- a/base.rkt
+++ b/base.rkt
@@ -12,10 +12,12 @@
     [`(λ ,x ,e) (format "λ~a.[~a]" x (fmt e))]
     [`((λ ,x ,e1) ,e2) (format "~a = ~a; ~a" x (fmt e2) (fmt e1))]
     [`(λ (,x : ,t) ,e) (format "~a: ~a; ~a" x (fmt t) (fmt e))]
-    [`((λ (,x : ,t) ,e1) ,e2) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))]
+    [`((λ (,x : ,t) ,e1) ,e2)
+      (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e2) (fmt e1))]
     [`(λ ,x ,e ,env) (format "λ~a.[~a]" x (fmt e))]
     [`(μ ,x ,t) (format "μ~a.~a" x (fmt t))]
-    [`(let (,x : ,t) ,e ,in) (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))]
+    [`(let (,x : ,t) ,e ,in)
+      (format "~a: ~a; ~a = ~a; ~a" x (fmt t) x (fmt e) (fmt in))]
     [`(let ,x ,e ,in) (format "~a = ~a; ~a" x (fmt e) (fmt in))]
     [`(set ,x ,e ,in) (format "~a := ~a; ~a" x (fmt e) (fmt in))]
     [`(,a → ,b) (format "(~a → ~a)" (fmt a) (fmt b))]
@@ -25,25 +27,21 @@
     [`(! ,a) (format "!~a" (fmt a))]
     [`(,a ,b) (format "(~a ~a)" (fmt a) (fmt b))]
     [(hash-table (keys values) ...)
-      (format "{~a}" (foldl (λ (k v acc) (format "~a: ~a;" (fmt k) (fmt v))) "" keys values))]
-    [expr (format "~a" expr)]))
+      (format "{~a}"
+        (foldl
+          (λ (k v acc)
+            (format "~a: ~a;" (fmt k) (fmt v)))
+          "" keys values))]
+    [_ (format "~a" expr)]))
 
-;; Removes typing annotations and similar constructs, for interpretation
-(define (strip expr)
-  (match expr
-    [`(,e : ,_) (strip e)]
-    [`(type ,_ ,_ ,e) (strip e)]
-    [`(fold ,_ ,e) `(fold ,(strip e))]
-    [`(unfold ,_ ,e) `(unfold ,(strip e))]
-    [`(,e ...) `(,@(map strip e))]
-    [e e]))
-
-;; Define aliases from higher-level constructs to their core forms
+;; Aliases from higher-level constructs to their core forms.
+;; This lets us elide many typing annotations.
 (define (desugar expr)
   (match expr
     ['⟨⟩ 'sole]
     [`(ref ,e) (desugar `(new ,e))]
     [`(deref ,e) (desugar `(! ,e))]
+    [`(,e ⇑ ,k) (desugar `(,e :: ,k))]
 
     ; set-with-continuation
     [`(set ,e1 ,e2 ,in)
diff --git a/stlc-dll.rkt b/stlc-dll.rkt
index 31c5bcc..1eef6d7 100644
--- a/stlc-dll.rkt
+++ b/stlc-dll.rkt
@@ -1,204 +1,266 @@
 #lang racket
 (require "lib.rkt" "base.rkt")
 (require (only-in "stlc-rec.rkt" replace))
-(require (only-in "stlc-ext.rkt" expand))
-(provide interpret check infer level-type level-body equiv-type)
+(require (only-in "stlc-ext.rkt" type->whnf))
+(provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references,
 ;; plus sums products booleans ascryption etc, to implement doubly-linked lists
 
-;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value ⊕ Err
+;; Checks an expression for syntactic well-formedness.
+(define (stlc-dll/expr? expr)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    [b #:when (boolean? b) #t]
+    [`(,e : ,t)
+      (and (stlc-dll/expr? e) (stlc-dll/type? t))]
+    [`(type ,t1 ,t2 ,e)
+      (and (stlc-dll/type? t1) (stlc-dll/type? t2) (stlc-dll/expr? e))]
+    [(or
+      `(inc ,e)
+      `(car ,e) `(cdr ,e)
+      `(inl ,e) `(inr ,e)
+      `(new ,e)  `(! ,e)
+      `(fold ,e) `(unfold ,e))
+      (stlc-dll/expr? e)]
+    [(or
+      `(pair ,e1 ,e2)
+      `(set ,e1 ,e2)
+      `(,e1 ,e2))
+      (and (stlc-dll/expr? e1) (stlc-dll/expr? e2))]
+    [`(if ,c ,e1 ,e2)
+      (and (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))]
+    [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+      (and (symbol? x1) (symbol? x2)
+        (stlc-dll/expr? c) (stlc-dll/expr? e1) (stlc-dll/expr? e2))]
+    [`(λ (,x : ,t) ,e)
+      (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e))]
+    [_ #f]))
+
+;; Checks a type for syntactic well-formedness.
+(define (stlc-dll/type? type)
+  (match type
+    ; Symbols are only valid if previously bound (by `type` or `μ`).
+    ; We can't check that here, however.
+    [x #:when (symbol? x) #t]
+    [`(Ref ,t) (stlc-dll/type? t)]
+    [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+      (and (stlc-dll/type? t1) (stlc-dll/type? t2))]
+    [`(,t1 → ,k ,t2)
+      (and (stlc-dll/type? t1) (natural? k) (stlc-dll/type? t2))]
+    [`(μ ,x ,t)
+      (and (symbol? x) (stlc-dll/type? t))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc-dll/value? expr)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    [b #:when (boolean? b) #t]
+    [(or `(inl ,v) `(inr ,v))
+      (stlc-dll/value? v)]
+    [(or `(pair ,v1 ,v2) `(,v1 ,v2))
+      (and (stlc-dll/value? v1) (stlc-dll/value? v2))]
+    [`(λ (,x : ,t) ,e ,env)
+      (and (symbol? x) (stlc-dll/type? t) (stlc-dll/expr? e) (dict? env))]
+    [_ #f]))
+
+
 (define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash() (make-hash)))
+  (interpret/core (desugar expr) #hash() (make-hash)))
 ;; Γ: a Table[Symbol, Expr] representing the context:
 ;;   the current bindings in scope introduced by λx.[]
 ;; Σ: a Table[Symbol, Expr] representing the heap:
 ;;   the current references on the heap generated by (gensym). mutable
 ;; Interprets a *desugared* expression *stripped* of type annotations.
-(define (interpret-core expr Γ Σ)
+(define/contract (interpret/core expr Γ Σ)
+  (-> stlc-dll/expr? dict? dict? stlc-dll/value?)
   (match expr
     ['sole 'sole]
     [n #:when (natural? n) n]
     [b #:when (boolean? b) b]
     [r #:when (dict-has-key? Σ r) r]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [f #:when (symbol? f) f]
 
     [`(inc ,e)
-      (match (interpret-core e Γ Σ)
+      (match (interpret/core e Γ Σ)
         [n #:when (natural? n) (+ n 1)]
         [e (format "incrementing an unknown value ~a" e)])]
     [`(if ,c ,e1 ,e2)
-      (match (interpret-core c Γ Σ)
-        ['#t (interpret-core e1 Γ Σ)]
-        ['#f (interpret-core e2 Γ Σ)]
+      (match (interpret/core c Γ Σ)
+        ['#t (interpret/core e1 Γ Σ)]
+        ['#f (interpret/core e2 Γ Σ)]
         [e (err (format "calling if on unknown expression ~a" e))])]
 
     [`(pair ,e1 ,e2)
-      `(pair ,(interpret-core e1 Γ Σ) ,(interpret-core e2 Γ Σ))]
+      `(pair ,(interpret/core e1 Γ Σ) ,(interpret/core e2 Γ Σ))]
     [`(car ,e)
-      (match (interpret-core e Γ Σ)
+      (match (interpret/core e Γ Σ)
         [`(pair ,e1 ,e2) e1]
         [e (err (format "calling car on unknown expression ~a" e))])]
     [`(cdr ,e)
-      (match (interpret-core e Γ Σ)
+      (match (interpret/core e Γ Σ)
         [`(pair ,e1 ,e2) e2]
         [e (err (format "calling cdr on unknown expression ~a" e))])]
 
-    [`(inl ,e) `(inl ,(interpret-core e Γ Σ))]
-    [`(inr ,e) `(inr ,(interpret-core e Γ Σ))]
+    [`(inl ,e) `(inl ,(interpret/core e Γ Σ))]
+    [`(inr ,e) `(inr ,(interpret/core e Γ Σ))]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (interpret-core e Γ Σ)
-        [`(inl ,e) (interpret-core e1 (dict-set Γ x1 e) Σ)]
-        [`(inr ,e) (interpret-core e2 (dict-set Γ x2 e) Σ)]
+      (match (interpret/core e Γ Σ)
+        [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e) Σ)]
+        [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e) Σ)]
         [e (err (format "calling case on unknown expression ~a" e))])]
 
     [`(new ,e)
       (let ([r (gensym)])
       (dict-set! Σ r e) r)]
     [`(! ,e)
-      (let ([r (interpret-core e Γ Σ)])
+      (let ([r (interpret/core e Γ Σ)])
       (if (dict-has-key? Σ r)
-        (interpret-core (dict-ref Σ r) Γ Σ)
+        (interpret/core (dict-ref Σ r) Γ Σ)
         (err (format "attempting to deref unknown reference ~a" r))))]
     [`(set ,e1 ,e2)
-      (let ([r (interpret-core e1 Γ Σ)])
-      (if (dict-has-key? Σ r) (dict-set! Σ r (interpret-core e2 Γ Σ))
+      (let ([r (interpret/core e1 Γ Σ)])
+      (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ))
         (err (format "attempting to update unknown reference ~a" r))))
       'sole]
 
-    [`(fold ,e) `(fold ,(interpret-core e Γ Σ))]
+    [`(fold ,e) `(fold ,(interpret/core e Γ Σ))]
     [`(unfold ,e)
-      (match (interpret-core e Γ Σ)
+      (match (interpret/core e Γ Σ)
         [`(fold ,e) e]
         [e (err (format "attempting to unfold unknown expression ~a" e))])]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
+    [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret-core e1 Γ Σ)
+      (match (interpret/core e1 Γ Σ)
         [`(λ ,x ,e1 ,env)
-          (interpret-core e1 (dict-set env x (interpret-core e2 Γ Σ)) Σ)]
-        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]
-
-    [e (err (format "attempting to interpret unknown expression ~a" e))]))
+          (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)]
+        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]))
 
 ;; Checks that an expression is of a type, and returns #t or #f (or a bubbled-up error)
 ;; with: a type in weak-head normal form (!!)
 ;; Γ: a Table[Symbol, Expr ⊕ Type] representing the context:
 ;;   the current bindings in scope introduced by λx.[] and μx.[] and τx.[]
-;;      (check Expr Type Table[Sym, Type]): Bool
 (define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ)
+  (-> stlc-dll/expr? stlc-dll/type? dict? boolean?)
   (match expr
     [`(type ,t1 ,t2 ,in)
-      (check-core in with (dict-set Γ `(type ,t1) t2))]
+      (check/core in with (dict-set Γ `(type ,t1) t2))]
 
     [`(if ,c ,e1 ,e2)
-      (and (check-core c 'Bool Γ)
-        (check-core e1 with Γ) (check-core e2 with Γ))]
+      (and (check/core c 'Bool Γ)
+        (check/core e1 with Γ) (check/core e2 with Γ))]
 
     [`(pair ,e1 ,e2)
       (match with
-        [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
+        [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))]
         [_ #f])]
 
     [`(inl ,e)
       (match with
-        [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
+        [`(,t1 ⊕ ,t2) (check/core e t1 Γ)]
         [_ #f])]
     [`(inr ,e)
       (match with
-        [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
+        [`(,t1 ⊕ ,t2) (check/core e t2 Γ)]
         [_ #f])]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (infer-core e Γ) ; avoid needing type annotation on e
+      (match (infer/core e Γ) ; avoid needing type annotation on e
         [`(,a1 ⊕ ,a2)
-          (and (check-core e1 with (dict-set Γ x1 a1))
-            (check-core e2 with (dict-set Γ x2 a2)))]
+          (and (check/core e1 with (dict-set Γ x1 a1))
+            (check/core e2 with (dict-set Γ x2 a2)))]
         [_ #f])]
 
     [`(new ,e)
       (match with
-        [`(Ref ,t) (check-core e t Γ)]
+        [`(Ref ,t) (check/core e t Γ)]
         [_ #f])]
     [`(! ,e)
-      (check-core e `(Ref ,with) Γ)]
+      (check/core e `(Ref ,with) Γ)]
 
     [`(fold ,e)
       (match with
-        [`(μ ,x ,t) (check-core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))]
+        [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))]
         [_ #f])]
 
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,k ,t2)
-          (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t))
+          (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t))
             (> k (level-body e (dict-set Γ x t1))))] ; KNOB
         [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
         [_ #f])]
 
-    [_ (equiv-type (infer-core expr Γ) with Γ)]))
+    [_ (equiv-type (infer/core expr Γ) with Γ)]))
 
 ;; Checks if two types are equivalent up to α-conversion in context
-;;      (equiv-type Type Type Table[Sym Type]): Bool
 (define (equiv-type e1 e2 Γ)
-  (equiv-type-core e1 e2 Γ Γ))
-(define (equiv-type-core e1 e2 Γ1 Γ2)
+  (equiv-type/core e1 e2 Γ Γ))
+(define/contract (equiv-type/core e1 e2 Γ1 Γ2)
+  (-> stlc-dll/type? stlc-dll/type? dict? dict? boolean?)
   (match* (e1 e2)
     ; bound identifiers: if a key exists in the context, look it up
     [(x1 x2) #:when (dict-has-key? Γ1 x1)
-      (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+      (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
-      (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+      (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
 
     ; recursive types: self-referential names can be arbitrary
     [(`(μ ,x1 ,t1) `(μ ,x2 ,t2))
       (let ([name gensym])
-      (equiv-type-core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+      (equiv-type/core t1 t2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
 
     ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
-      (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+      (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
 
 ;; Infers a type from a given expression, if possible, or errors out.
 ;; Returns a type in weak-head normal form for structural matching.
-;;      (infer Expr Table[Sym, Type]): Type
 (define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
+  (infer/core (desugar expr) #hash()))
+(define/contract (infer/core expr Γ)
+  (-> stlc-dll/expr? dict? stlc-dll/type?)
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
     [b #:when (boolean? b) 'Bool]
     [x #:when (dict-has-key? Γ x)
-      (expand (dict-ref Γ x) Γ)]
+      (type->whnf (dict-ref Γ x) Γ)]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
 
     [`(type ,t1 ,t2 ,in)
-      (infer-core in (dict-set Γ `(type ,t1) t2))]
+      (infer/core in (dict-set Γ `(type ,t1) t2))]
     [`(,e : ,t) ; we have a manual type annotation, so we must expand to weak-head normal form
-      (if (check-core e (expand t Γ) Γ) (expand t Γ)
+      (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ)
         (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
 
     [`(inc ,e)
-      (if (check-core e 'Nat Γ) 'Nat
-        (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))]
+      (if (check/core e 'Nat Γ) 'Nat
+        (err (format "calling inc on incorrect type ~a" (infer/core e Γ))))]
     [`(if ,c ,e1 ,e2)
-      (if (check-core c 'Bool Γ)
-        (let ([t (infer-core e1 Γ)])
-        (if (check-core e2 t Γ) t
+      (if (check/core c 'Bool Γ)
+        (let ([t (infer/core e1 Γ)])
+        (if (check/core e2 t Γ) t
           (err (format "condition has branches of differing types ~a and ~a"
-            t (infer-core e2 Γ)))))
-        (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))]
+            t (infer/core e2 Γ)))))
+        (err (format "condition ~a has incorrect type ~a" c (infer/core c Γ))))]
 
     [`(pair ,e1 ,e2)
-      `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))]
+      `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))]
     [`(car ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(,t1 × ,t2) t1]
         [t (err (format "calling car on incorrect type ~a" t))])]
     [`(cdr ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(,t1 × ,t2) t2]
         [t (err (format "calling cdr on incorrect type ~a" t))])]
 
@@ -207,53 +269,51 @@
     [`(inr ,e)
       (err (format "unable to infer the type of a raw inr"))]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(,a1 ⊕ ,a2)
-          (let ([b1 (infer-core e1 (dict-set Γ x1 a1))]
-                [b2 (infer-core e2 (dict-set Γ x2 a2))])
+          (let ([b1 (infer/core e1 (dict-set Γ x1 a1))]
+                [b2 (infer/core e2 (dict-set Γ x2 a2))])
             (if (equiv-type b1 b2 Γ) b1
               (err (format "case ~a is not of consistent type!"
                 `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
         [t (err (format "calling case on incorrect type ~a" t))])]
 
     [`(new ,e)
-      `(Ref ,(infer-core e Γ))]
+      `(Ref ,(infer/core e Γ))]
     [`(! ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(Ref ,t) t]
         [t (err (format "attempting to deref term ~a of type ~a" e t))])]
     [`(set ,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(Ref ,t)
-          (if (check-core e2 t Γ) 'Unit
+          (if (check/core e2 t Γ) 'Unit
             (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
-              e1 t e2 (infer-core e2 Γ))))]
+              e1 t e2 (infer/core e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
     [`(unfold ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(μ ,x ,t) (replace t x `(μ ,x ,t))]
         [t (err (format "expected ~a to be recursive, got ~a" e t))])]
 
     [`(λ (,x : ,t1) ,e)
-      (let* ([t2 (infer-core e (dict-set Γ x t1))]
-        [t1 (expand t1 Γ)] ; type annotation, must expand
+      (let* ([t2 (infer/core e (dict-set Γ x t1))]
+        [t1 (type->whnf t1 Γ)] ; type annotation, must expand
         [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB
         `(,t1 → ,k ,t2))]
     [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(,t1 → ,k ,t2)
-          (if (check-core e2 t1 Γ) t2
-            (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))]
+          (if (check/core e2 t1 Γ) t2
+            (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer/core e2 Γ))))]
         [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
+        [t (err (format "expected → type on application body, got ~a" t))])]))
 
 ;; Checks if a type is well-formed in the current context.
 ;; BIG ASSUMPTION: types in the current context are well-formed
-;;      (well-formed Type Context): Bool
-(define (well-formed t Γ)
+(define/contract (well-formed t Γ)
+  (-> stlc-dll/type? dict? boolean?)
   (match t
     [x #:when (dict-has-key? Γ x) #t]
     [(or 'Unit 'Nat 'Bool) #t]
@@ -266,8 +326,8 @@
 
 ;; Checks if a type is well-kinded with respect to a level in the current context
 ;; BIG ASSUMPTION: types in the current context are well-formed
-;;      (well-kinded Type Level Context): Bool
-(define (well-kinded t l Γ)
+(define/contract (well-kinded t l Γ)
+  (-> stlc-dll/type? natural? dict? boolean?)
   (match t
     [x #:when (dict-has-key? Γ x) #t]
     [(or 'Unit 'Nat 'Bool) (>= l 0)]
@@ -284,8 +344,8 @@
     [_ #f]))
 
 ;; Infers the level of a (well-formed) type.
-;;      (level-type Type): Natural
-(define (level-type t Γ)
+(define/contract (level-type t Γ)
+  (-> stlc-dll/type? dict? natural?)
   (match t
     [x #:when (dict-has-key? Γ x)
       (level-type (dict-ref Γ x) Γ)]
@@ -303,13 +363,13 @@
     [t #:when (symbol? t) 0])) ; μ-type variables, not in Γ
 
 ;; Infers the level of a (well-formed) expression.
-;;      (level-body Expr Context): Natural
-(define (level-body e Γ)
+(define/contract (level-body e Γ)
+  (-> stlc-dll/expr? dict? natural?)
   (match e
     ['sole 0]
     [n #:when (natural? n) 0]
     [x #:when (dict-has-key? Γ x) ; free variables, get their level
-      (level-type (expand (dict-ref Γ x) Γ) Γ)]
+      (level-type (type->whnf (dict-ref Γ x) Γ) Γ)]
     [(or `(,e : ,_) `(λ (,_ : ,_) ,e)
       `(inc ,e) `(new ,e) `(! ,e) `(car ,e) `(cdr ,e) `(inl ,e) `(inr ,e)
       `(fold ,e) `(unfold ,e) `(fold (μ ,_ ,_) ,e) `(unfold (μ ,_ ,_) ,e))
diff --git a/stlc-ext.rkt b/stlc-ext.rkt
index 2662135..c76db93 100644
--- a/stlc-ext.rkt
+++ b/stlc-ext.rkt
@@ -1,107 +1,172 @@
 #lang racket
 (require "lib.rkt")
 (require "base.rkt")
-(provide interpret check infer expand equiv-type equiv-term)
+(provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus, with simple extensions
 ;; Unit/String/Natural/Boolean, pairs, sums, lists, ascryption
 
-;;      (interpret Expr Table[Sym, Expr]): Value
+;; Checks an expression for syntactic well-formedness.
+(define (stlc-ext/expr? expr)
+  (match expr
+    [(or 'sole 'nil) #t]
+    [s #:when (string? s) #t]
+    [n #:when (natural? n) #t]
+    [b #:when (boolean? b) #t]
+    [x #:when (symbol? x) #t]
+
+    [(or
+      `(inc ,e)
+      `(car ,e) `(cdr ,e)
+      `(inl ,e) `(inr ,e)
+      `(head ,e) `(tail ,e) `(nil? ,e))
+      (stlc-ext/expr? e)]
+    [(or
+      `(pair ,e1 ,e2)
+      `(cons ,e1 ,e2)
+      `(,e1 ,e2))
+      (and (stlc-ext/expr? e1) (stlc-ext/expr? e2))]
+
+    [`(if ,c ,e1 ,e2)
+      (and (stlc-ext/expr? c) (stlc-ext/expr? e1) (stlc-ext/expr? e2))]
+    [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
+      (and (stlc-ext/expr? e) (stlc-ext/expr? e1) (stlc-ext/expr? e2)
+        (symbol? x1) (symbol? x2))]
+    [`(type ,t1 ,t2 ,e)
+      (and (stlc-ext/type? t1) (stlc-ext/type? t2) (stlc-ext/expr? e))]
+    [`(λ (,x : ,t) ,e)
+      (and (symbol? x) (stlc-ext/type? t) (stlc-ext/expr? e))]
+    [_ #f]))
+
+;; Checks a type for syntactic well-formedness.
+(define (stlc-ext/type? type)
+  (match type
+    [t #:when (symbol? t) #t]
+    [`(List ,t) (stlc-ext/type? t)]
+    [(or
+      `(,t1 → ,t2)
+      `(,t1 × ,t2)
+      `(,t1 ⊕ ,t2))
+      (and (stlc-ext/type? t1) (stlc-ext/type? t2))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc-ext/value? value)
+  (match value
+    [(or 'sole 'nil) #t]
+    [s #:when (string? s) #t]
+    [n #:when (natural? n) #t]
+    [b #:when (boolean? b) #t]
+    [x #:when (symbol? x) #t]
+    [(or
+      `(pair ,v1 ,v2)
+      `(cons ,v1 ,v2)
+      `(,v1 ,v2))
+      (and (stlc-ext/value? v1) (stlc-ext/value? v2))]
+    [`(λ ,x ,e ,env)
+      (and (symbol? x) (stlc-ext/expr? e) (dict? env))]
+    [_ #f]))
+
+;; Interprets an expression down to a value, in a given context.
 (define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash()))
-(define (interpret-core expr Γ)
+  (interpret/core (desugar expr) #hash()))
+(define/contract (interpret/core expr Γ)
+  (-> stlc-ext/expr? dict? stlc-ext/value?)
   (match expr
     ['sole 'sole]
     [s #:when (string? s) s]
     [n #:when (natural? n) n]
     [b #:when (boolean? b) b]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [f #:when (symbol? f) f]
+
+    [`(,e : ,t) (interpret/core e Γ)]
+    [`(type ,t1 ,t2 ,e) (interpret/core e Γ)]
 
     [`(inc ,e)
-      (match (interpret-core e Γ)
+      (match (interpret/core e Γ)
         [n #:when (natural? n) (+ n 1)]
         [e (format "incrementing an unknown value ~a" e)])]
     [`(if ,c ,e1 ,e2)
-      (match (interpret-core c Γ)
-        ['#t (interpret-core e1 Γ)]
-        ['#f (interpret-core e2 Γ)]
+      (match (interpret/core c Γ)
+        ['#t (interpret/core e1 Γ)]
+        ['#f (interpret/core e2 Γ)]
         [e (err (format "calling if on unknown expression ~a" e))])]
 
     [`(pair ,e1 ,e2)
-      `(pair ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))]
+      `(pair ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))]
     [`(car ,e)
-      (match (interpret-core e Γ)
+      (match (interpret/core e Γ)
         [`(pair ,e1 ,e2) e1]
         [e (err (format "calling car on unknown expression ~a" e))])]
     [`(cdr ,e)
-      (match (interpret-core e Γ)
+      (match (interpret/core e Γ)
         [`(pair ,e1 ,e2) e2]
         [e (err (format "calling cdr on unknown expression ~a" e))])]
 
-    [`(inl ,e) `(inl ,(interpret-core e Γ))]
-    [`(inr ,e) `(inr ,(interpret-core e Γ))]
+    [`(inl ,e) `(inl ,(interpret/core e Γ))]
+    [`(inr ,e) `(inr ,(interpret/core e Γ))]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (interpret-core e Γ)
-        [`(inl ,e) (interpret-core e1 (dict-set Γ x1 e))]
-        [`(inr ,e) (interpret-core e2 (dict-set Γ x2 e))]
+      (match (interpret/core e Γ)
+        [`(inl ,e) (interpret/core e1 (dict-set Γ x1 e))]
+        [`(inr ,e) (interpret/core e2 (dict-set Γ x2 e))]
         [e (err (format "calling case on unknown expression ~a" e))])]
 
     ['nil 'nil]
     [`(nil? ,e)
-      (match (interpret-core e Γ)
+      (match (interpret/core e Γ)
         ['nil '#t]
         [`(cons ,e1 ,e2) '#f]
         [e (err (format "calling isnil on unknown expression ~a" e))])]
     [`(cons ,e1 ,e2)
-     `(cons ,(interpret-core e1 Γ) ,(interpret-core e2 Γ))]
+     `(cons ,(interpret/core e1 Γ) ,(interpret/core e2 Γ))]
     [`(head ,e)
-      (match (interpret-core e Γ)
-        [`(cons ,e1 ,e2) (interpret-core e1 Γ)]
+      (match (interpret/core e Γ)
+        [`(cons ,e1 ,e2) (interpret/core e1 Γ)]
         [e (err (format "calling head on unknown expression ~a" e))])]
     [`(tail ,e)
-      (match (interpret-core e Γ)
-        [`(cons ,e1 ,e2) (interpret-core e2 Γ)]
+      (match (interpret/core e Γ)
+        [`(cons ,e1 ,e2) (interpret/core e2 Γ)]
         [e (err (format "calling tail on unknown expression ~a" e))])]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
+    [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret-core e1 Γ)
+      (match (interpret/core e1 Γ)
         [`(λ ,x ,e ,env)
-          (interpret-core e (dict-set env x (interpret-core e2 Γ)))]
-        [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
-
-    [e (err (format "interpreting an unknown expression ~a" e))]))
+          (interpret/core e (dict-set env x (interpret/core e2 Γ)))]
+        [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]))
 
-;;      (check Expr Type Table[Sym, Type]): Bool
+;; Checks an expression against some type, in a given context.
 (define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ)
+  (-> stlc-ext/expr? stlc-ext/type? dict? boolean?)
   (match expr
     [`(type ,t1 ,t2 ,in)
-      (check-core in with (dict-set Γ t1 t2))]
+      (check/core in with (dict-set Γ t1 t2))]
 
     [`(if ,c ,e1 ,e2)
-      (and (check-core c 'Bool Γ)
-        (check-core e1 with Γ) (check-core e2 with Γ))]
+      (and (check/core c 'Bool Γ)
+        (check/core e1 with Γ) (check/core e2 with Γ))]
 
     [`(pair ,e1 ,e2)
       (match with
-        [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
+        [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))]
         [_ #f])]
 
     [`(inl ,e)
       (match with
-        [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
+        [`(,t1 ⊕ ,t2) (check/core e t1 Γ)]
         [_ #f])]
     [`(inr ,e)
       (match with
-        [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
+        [`(,t1 ⊕ ,t2) (check/core e t2 Γ)]
         [_ #f])]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
       (match (infer-core e Γ)
         [`(,a1 ⊕ ,a2)
-          (and (check-core e1 with (dict-set Γ x1 a1))
-            (check-core e2 with (dict-set Γ x2 a2)))]
+          (and (check/core e1 with (dict-set Γ x1 a1))
+            (check/core e2 with (dict-set Γ x2 a2)))]
         [_ #f])]
 
     ['nil
@@ -111,43 +176,46 @@
     [`(cons ,f1 ,f2)
       (match with
         [`(List ,t)
-          (and (check-core f1 t Γ)
-            (check-core f2 `(List ,t) Γ))]
+          (and (check/core f1 t Γ)
+            (check/core f2 `(List ,t) Γ))]
         [_ #f])]
 
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,t2)
-          (and (equiv-type t1 t Γ) (check-core e t2 (dict-set Γ x t1)))]
+          (and (equiv-type t1 t Γ) (check/core e t2 (dict-set Γ x t1)))]
         [_ #f])]
 
     [_ (equiv-type (infer-core expr Γ) with Γ)]))
 
-;;      (infer Expr Table[Sym, Type]): Type
+;; Infers a type from some expression, in a given context.
 (define (infer expr)
   (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
+(define/contract (infer-core expr Γ)
+  (-> stlc-ext/expr? dict? stlc-ext/type?)
   (match expr
     ['sole 'Unit]
     [s #:when (string? s) 'Str]
     [n #:when (natural? n) 'Nat]
     [b #:when (boolean? b) 'Bool]
     [x #:when (dict-has-key? Γ x)
-      (expand (dict-ref Γ x) Γ)]
+      (type->whnf (dict-ref Γ x) Γ)]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
 
     [`(type ,t1 ,t2 ,in)
       (infer-core in (dict-set Γ t1 t2))]
     [`(,e : ,t)
-      (if (check-core e (expand t Γ) Γ) (expand t Γ)
+      (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ)
         (err (format "annotated expression ~a is not of annotated type ~a" e t)))]
 
     [`(inc ,e)
-      (if (check-core e 'Nat Γ) 'Nat
+      (if (check/core e 'Nat Γ) 'Nat
         (err (format "calling inc on incorrect type ~a" (infer-core e Γ))))]
     [`(if ,c ,e1 ,e2)
-      (if (check-core c 'Bool Γ)
+      (if (check/core c 'Bool Γ)
         (let ([t (infer-core e1 Γ)])
-        (if (check-core e2 t Γ) t
+        (if (check/core e2 t Γ) t
           (err (format "condition has branches of differing types ~a and ~a"
             t (infer-core e2 Γ)))))
         (err (format "condition ~a has incorrect type ~a" c (infer-core c Γ))))]
@@ -174,8 +242,8 @@
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
       (match (infer-core e Γ)
         [`(,a1 ⊕ ,a2)
-          (let ([b1 (infer-core e1 (dict-set Γ x1 (expand a1 Γ)))]
-            [b2 (infer-core e2 (dict-set Γ x2 (expand a2 Γ)))])
+          (let ([b1 (infer-core e1 (dict-set Γ x1 (type->whnf a1 Γ)))]
+            [b2 (infer-core e2 (dict-set Γ x2 (type->whnf a2 Γ)))])
           (if (equiv-type b1 b2 Γ) b1
             (err (format "case ~a is not of consistent type!" `(case (,a1 ⊕ ,a2) b1 b2)))))]
         [t (err (format "calling case on incorrect type ~a" t))])]
@@ -183,7 +251,7 @@
     ['nil (err (format "unable to infer type of empty list!"))]
     [`(cons ,e1 ,e2)
       (let ([t (infer-core e1 Γ)])
-      (if (check-core e2 `(List ,t) Γ) `(List ,t)
+      (if (check/core e2 `(List ,t) Γ) `(List ,t)
         (err (format "list ~a is not of consistent type!" `(cons ,e1 ,e2)))))]
     [`(head ,e)
       (match (infer-core e Γ)
@@ -195,61 +263,58 @@
         [t (err (format "calling tail on incorrect type ~a" t))])]
 
     [`(λ (,x : ,t) ,e)
-      `(,(expand t Γ) → ,(infer-core e (dict-set Γ x t)))]
+      `(,(type->whnf t Γ) → ,(infer-core e (dict-set Γ x t)))]
     [`(,e1 ,e2)
       (match (infer-core e1 Γ)
         [`(,t1 → ,t2)
-          (if (check-core e2 t1 Γ) t2
+          (if (check/core e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "inferring an unknown expression ~a" e))]))
+        [t (err (format "expected → type on application body, got ~a" t))])]))
 
 ;; Expands a type alias into weak-head normal form, for literal matching.
-;;      (expand Type Table[Id, Expr ⊕ Type]): Type
-(define (expand t Γ)
+(define (type->whnf t Γ)
   (if (dict-has-key? Γ `(type ,t))
-    (expand (dict-ref Γ `(type ,t)) Γ) t))
+    (type->whnf (dict-ref Γ `(type ,t)) Γ) t))
 
 ;; Checks if two types are equivalent up to α-conversion in context
 ;;      (equiv-type Expr Expr Table[Sym Expr]): Bool
 (define (equiv-type e1 e2 Γ)
-  (equiv-type-core e1 e2 Γ Γ))
-(define (equiv-type-core e1 e2 Γ1 Γ2)
+  (equiv-type/core e1 e2 Γ Γ))
+(define (equiv-type/core e1 e2 Γ1 Γ2)
   (match* (e1 e2)
     ; bound identifiers: if a key exists in the context, look it up
     [(x1 x2) #:when (dict-has-key? Γ1 x1)
-      (equiv-type-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+      (equiv-type/core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
-      (equiv-type-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+      (equiv-type/core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
 
     ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
-      (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+      (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
 
 ;; Checks if two terms are equivalent up to α-conversion in context
 ;;      (equiv-term Expr Expr Table[Sym Expr]): Bool
 (define (equiv-term e1 e2 Γ)
-  (equiv-term-core e1 e2 Γ Γ))
-(define (equiv-term-core e1 e2 Γ1 Γ2)
+  (equiv-term/core e1 e2 Γ Γ))
+(define (equiv-term/core e1 e2 Γ1 Γ2)
   (match* (e1 e2)
     ; bound identifiers: if a key exists in the context, look it up
     [(x1 x2) #:when (dict-has-key? Γ1 x1)
-      (equiv-term-core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
+      (equiv-term/core (dict-ref Γ1 x1) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 x2)
-      (equiv-term-core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
+      (equiv-term/core x1 (dict-ref Γ2 x2) Γ1 Γ2)]
 
     ; function expressions: parameter names can be arbitrary
     [(`(λ (,x1 : ,t1) ,e1) `(λ (,x2 : ,t2) ,e2))
       (let ([name gensym])
-      (and (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
-        (equiv-term-core t1 t2 Γ1 Γ2)))]
+      (and (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name))
+        (equiv-term/core t1 t2 Γ1 Γ2)))]
     [(`(λ ,x1 ,e1) `(λ ,x2 ,e2))
       (let ([name gensym])
-      (equiv-term-core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
+      (equiv-term/core e1 e2 (dict-set Γ1 x1 name) (dict-set Γ2 x2 name)))]
 
     ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
-      (foldl (λ (x1 x2 acc) (if (equiv-term-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+      (foldl (λ (x1 x2 acc) (if (equiv-term/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
diff --git a/stlc-fix.rkt b/stlc-fix.rkt
index 420aa15..06d0369 100644
--- a/stlc-fix.rkt
+++ b/stlc-fix.rkt
@@ -1,74 +1,87 @@
 #lang racket
 (require "lib.rkt")
 (require "base.rkt")
+(require (only-in "stlc.rkt" stlc/type?))
 
 ;; The Simply-Typed Lambda Calculus, with general recursion
 
-;;      (interpret Expr Context): Value
+;; Checks an expression for syntactic well-formedness.
+(define/contract (stlc-fix/expr? expr)
+  (-> any/c boolean?)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [`(fix ,e) (stlc-fix/expr? e)]
+    [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc-fix/expr? e))]
+    [`(,e1 ,e2) (and (stlc-fix/expr? e1) (stlc-fix/expr? e2))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc-fix/value? value)
+  (match value
+    [x #:when (symbol? x) #t]
+    [`(,v1 ,v2) (and (stlc-fix/value? v1) (stlc-fix/value? v2))]
+    [`(λ ,x ,e ,env) (and (symbol? x) (stlc-fix/expr? e) (dict? env))]
+    [_ #f]))
+
+;; Interprets an expression down to a value, in a given context.
 (define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash()))
-(define (interpret-core expr Γ)
+  (interpret/core (desugar expr) #hash()))
+(define/contract (interpret/core expr Γ)
+  (-> stlc-fix/expr? dict? stlc-fix/value?)
   (match expr
     ['sole 'sole]
-    [n #:when (natural? n) n]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [x #:when (symbol? x) x]
 
     [`(fix ,e)
-      (match (interpret-core e Γ)
+      (match (interpret/core e Γ)
         [`(λ ,x ,e ,env)
           ; FIXME: unsure what should be Γ and what should be env
-          (interpret-core e (dict-set env x `(fix (λ ,x ,e ,Γ))))]
+          (interpret/core e (dict-set env x `(fix (λ ,x ,e ,Γ))))]
         [e (err (format "applying fix to unknown expression ~a" e))])]
 
-    [`(λ ,id ,body) `(λ ,id ,body ,Γ)]
-    [`(λ ,id ,body ,env) `(λ ,id ,body ,env)]
+    [`(λ (,id : ,t) ,body) `(λ ,id ,body ,Γ)]
     [`(,body ,arg)
-      (match (interpret-core body Γ)
+      (match (interpret/core body Γ)
         [`(λ ,id ,body ,env)
-          (interpret-core body (dict-set env id (interpret-core arg Γ)))]
-        [e (err (format "applying arg ~a to unknown expression ~a" arg e))])]
+          (interpret/core body (dict-set env id (interpret/core arg Γ)))]
+        [e (err (format "applying arg ~a to unknown expression ~a" arg e))])]))
 
-    [e (err (format "interpreting an unknown expression ~a" e))]))
-
-;;      (check Expr Type Context): Bool
+;; Checks an expression against some type, in a given context.
 (define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ) ; FIXME
+  (-> stlc-fix/expr? stlc/type? dict? boolean?)
   (let ([with (if (dict-has-key? Γ with) (dict-ref Γ with) with)])
   (match expr
     [`(fix ,e)
-      (check-core (infer-core e) `(,with → ,with) Γ)]
-
+      (check/core (infer/core e) `(,with → ,with) Γ)]
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,t2)
           (and (equal? t1 t)
-            (check-core e t2 (dict-set Γ x t1)))]
+            (check/core e t2 (dict-set Γ x t1)))]
         [_ #f])]
+    [_ (equal? (infer/core expr Γ) with)])))
 
-    [_ (equal? (infer-core expr Γ) with)])))
-
-;;      (infer Expr Context): Type
+;; Infers a type from some expression, in a given context.
 (define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
+  (infer/core (desugar expr) #hash()))
+(define/contract (infer/core expr Γ)
+  (-> stlc-fix/expr? dict? stlc/type?)
   (match expr
-    ['sole 'Unit]
-    [n #:when (natural? n) 'Nat]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
-
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
     [`(fix ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(,t → ,t) t]
         [t (err (format "fix expects a term of type t → t, got ~a" t))])]
-
     [`(λ (,x : ,t) ,e)
-      `(,t → ,(infer-core e (dict-set Γ x t)))]
+      `(,t → ,(infer/core e (dict-set Γ x t)))]
     [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(,t1 → ,t2)
-          (if (check-core e2 t1 Γ) t2
+          (if (check/core e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "inferring an unknown expression ~a" e))]))
+        [t (err (format "expected → type on application body, got ~a" t))])]))
diff --git a/stlc-full.rkt b/stlc-full.rkt
index b25b56c..0ea8637 100644
--- a/stlc-full.rkt
+++ b/stlc-full.rkt
@@ -9,9 +9,12 @@
 ;; - impredicative references built on a levels system
 ;; - explicit level stratification syntax
 ;; - automatic level collection
-;;
-;; This system is impredicative. It can be made predicative by tweaking
-;; the sections of the code labeled with "KNOB".
+;; - [todo] implicit level stratification
+
+;; Whether the system is *predicative* or *impredicative*.
+;; The predicative system disallows quantification over references.
+;; The impredicative system allows so by tweaking level rules.
+(define impredicative? #f)
 
 (define-syntax-rule (print msg)
   (eprintf "~a~%" msg))
@@ -42,116 +45,101 @@
 (define (all? proc lst)
   (foldl (λ (x acc) (if (proc x) acc #f)) #t lst))
 
-;; Whether a given level is a syntactically valid level.
-;; This does not account for context, and so all symbols are valid levels.
-(define (level? level)
-  (match level
-    [n #:when (natural? n) #t]
-    ; Symbols are only valid if previously bound (by `level`).
-    ; We can't check that here, however.
-    [s #:when (symbol? s) #t]
-    ; Levels may be a list of symbols, or a list of symbols followed by a natural.
-    [`(+ ,l ... ,n) #:when (natural? n)
-      (all? (λ (s) (symbol? s)) l)]
-    [`(+ ,l ...)
-      (all? (λ (s) (symbol? s)) l)]
-    [_ #f]))
-
-;; Whether a given type is a syntactically valid type.
-;; This does not account for context, and so all symbols are valid types.
-(define (type? type)
-  (match type
-    [(or 'Unit 'Bool 'Nat) #t]
-    ; Symbols are only valid if previously bound (by `type` or `μ`).
-    ; We can't check that here, however.
-    [s #:when (symbol? s) #t]
-    [`(Ref ,t) (type? t)]
-    [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2)) (and (type? t1) (type? t2))]
-    [`(,t1 → ,l ,t2) (and (type? t1) (level? l) (type? t2))]
-    [`(μ ,x ,t) (and (symbol? x) (type? t))]
-    [_ #f]))
-
-;; Whether a given expression is a syntactically valid expression.
+;; Checks an expression for syntactic well-formedness.
 ;; This does not account for context, and so all symbols are valid exprs.
-(define (expr? expr)
+(define (stlc-full/expr? expr)
   (match expr
-    ['sole #t]
+    ; Symbols are only valid if previously bound by `λ` or `case` (or if `'sole`).
+    ; We can't check that here, however.
+    [x #:when (symbol? x) #t]
     [n #:when (natural? n) #t]
     [b #:when (boolean? b) #t]
-    ; Symbols are only valid if previously bound by `λ` or `case`.
-    ; We can't check that here, however.
-    [s #:when (symbol? s) #t]
-
-    [`(,e : ,t) (and (expr? e) (type? t))]
+    [`(,e : ,t)
+      (and (stlc-full/expr? e) (stlc-full/type? t))]
     [`(type ,t1 ,t2 ,e)
-      (and (type? t1) (type? t2) (expr? e))]
-
-    ; Note that level must only introduce new variables as levels.
-    [`(level ,l ,e)
-      (and (symbol? l) (expr? e))]
-    ; Kind of want to call ⇑ :: on analogy with :
-    [`(,e ⇑ ,l)
-      (and (expr? e) (level? l))]
-
-    [(or `(new ,e) `(! ,e)) (expr? e)]
-    ; [`(ptr ,a) (symbol? a)]
-    [`(set ,e1 ,e2) (and (expr? e1) (expr? e2))]
-
-    [`(inc ,e) (expr? e)]
+      (and (stlc-full/type? t1) (stlc-full/type? t2) (stlc-full/expr? e))]
+    [`(,e :: ,l)
+      (and (stlc-full/expr? e) (stlc-full/level? l))]
+    [`(level ,l ,e) ; note that level must only introduce new variables as levels
+      (and (symbol? l) (stlc-full/expr? e))]
+    [(or
+      `(inc ,e)
+      `(car ,e) `(cdr ,e)
+      `(inl ,e) `(inr ,e)
+      `(new ,e)  `(! ,e)
+      `(fold ,e) `(unfold ,e))
+      (stlc-full/expr? e)]
+    [(or
+      `(pair ,e1 ,e2)
+      `(set ,e1 ,e2)
+      `(,e1 ,e2))
+      (and (stlc-full/expr? e1) (stlc-full/expr? e2))]
     [`(if ,c ,e1 ,e2)
-      (and (expr? c) (expr? e1) (expr? e2))]
-
-    [`(pair ,e1 ,e2)
-      (and (expr? e1) (expr? e2))]
-    [(or `(car ,e) `(cdr ,e)) (expr? e)]
-
-    [(or `(inl ,e) `(inr ,e)) (expr? e)]
+      (and (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))]
     [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
       (and (symbol? x1) (symbol? x2)
-        (expr? c) (expr? e1) (expr? e2))]
-
-    [(or `(fold ,e) `(unfold ,e)) (expr? e)]
-
+        (stlc-full/expr? c) (stlc-full/expr? e1) (stlc-full/expr? e2))]
     [`(λ (,x : ,t) ,e)
-      (and (symbol? x) (type? t) (expr? e))]
-    [`(,e1 ,e2) (and (expr? e1) (expr? e2))]
+      (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e))]
     [_ #f]))
 
-;; Whether a term is a value or a computation. What's that little rhyme about this again?
-;; A value is, a computation/expr/term does?
-(define (value? expr)
+;; Checks a value for syntactic well-formedness.
+;; This does not account for context, and so all symbols are valid values.
+;; A value is, a computation/expr/term does...
+(define (stlc-full/value? expr)
   (match expr
-    ['sole #t]
+    [x #:when (symbol? x) #t]
     [n #:when (natural? n) #t]
     [b #:when (boolean? b) #t]
+    [`(ptr ,l ,a)
+      (and (stlc-full/level? l) (symbol? a))]
+    [(or `(inl ,v) `(inr ,v))
+      (stlc-full/value? v)]
+    [(or `(pair ,v1 ,v2) `(,v1 ,v2))
+      (and (stlc-full/value? v1) (stlc-full/value? v2))]
+    [`(λ (,x : ,t) ,e ,env)
+      (and (symbol? x) (stlc-full/type? t) (stlc-full/expr? e) (dict? env))]
+    [_ #f]))
 
-    ; [`(,v : ,t) (and (expr? v) (type? t))]
-    ; [`(type ,t1 ,t2 ,b)
-    ;   (and (type? t1) (type? t2) (value? v))]
-
-    ; [(or `(level ,l ,v) `(,v ⇑ ,l))
-    ;   (and (level? l) (value? v))]
-
-    [`(ptr ,l ,a) (and (level? l) (symbol? a))]
-
-    [`(pair ,v1 ,v2)
-      (and (value? v1) (value? v2))]
-
-    [(or `(inl ,v) `(inr ,v)) (value? v)]
-
-    ; [(or `(fold ,v) `(unfold ,v)) (value? v)]
+;; Checks a level for syntactic well-formedness.
+;; This does not account for context, and so all symbols are valid levels.
+(define (stlc-full/level? level)
+  (match level
+    ; Symbols are only valid if previously bound (by `level`).
+    ; We can't check that here, however.
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    ; Levels may be a list of symbols, or a list of symbols followed by a natural.
+    [`(+ ,l ... ,n) #:when (natural? n)
+      (all? (λ (s) (symbol? s)) l)]
+    [`(+ ,l ...)
+      (all? (λ (s) (symbol? s)) l)]
+    [_ #f]))
 
-    [`(λ (,x : ,t) ,e ,env)
-      (and (symbol? x) (type? t) (expr? e) (dict? env))]
+;; Checks a type for syntactic well-formedness.
+;; This does not account for context, and so all symbols are valid types.
+(define (stlc-full/type? type)
+  (match type
+    ; Symbols are only valid if previously bound (by `type` or `μ`).
+    ; We can't check that here, however.
+    [x #:when (symbol? x) #t]
+    [`(Ref ,t) (stlc-full/type? t)]
+    [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
+      (and (stlc-full/type? t1) (stlc-full/type? t2))]
+    [`(,t1 → ,l ,t2)
+      (and (stlc-full/type? t1) (stlc-full/level? l) (stlc-full/type? t2))]
+    [`(μ ,x ,t)
+      (and (symbol? x) (stlc-full/type? t))]
     [_ #f]))
 
-(define (ptr? expr)
+(define (stlc-full/ptr? expr)
   (match expr
-    [`(ptr ,l ,a) (and (level? l) (symbol? a))]
+    [`(ptr ,l ,a) (and (stlc-full/level? l) (symbol? a))]
     [_ #f]))
 
 ;; Creates a new multiset from a list.
-(define/contract (list->multiset l) (-> list? dict?)
+(define/contract (list->multiset l)
+  (-> list? dict?)
   (foldl
     (λ (x acc)
       (if (dict-has-key? acc x)
@@ -160,20 +148,23 @@
     #hash() l))
 
 ;; Creates a new list from a multiset.
-(define/contract (multiset->list m) (-> dict? list?)
+(define/contract (multiset->list m)
+  (-> dict? list?)
   (foldl
     (λ (x acc)
       (append acc (build-list (dict-ref m x) (λ (_) x))))
     '() (dict-keys m)))
 
 ;; Adds a symbol to a multiset.
-(define/contract (multiset-add m1 s) (-> dict? symbol? dict?)
+(define/contract (multiset-add m1 s)
+  (-> dict? symbol? dict?)
   (if (dict-has-key? m1 s)
     (dict-set m1 s (+ (dict-ref m1 s) 1))
     (dict-set m1 s 1)))
 
 ;; Queries two multisets for equality.
-(define/contract (multiset-eq m1 m2) (-> dict? dict? boolean?)
+(define/contract (multiset-eq m1 m2)
+  (-> dict? dict? boolean?)
   (if (equal? (length m1) (length m2)) #f
     (foldl
       (λ (x acc)
@@ -183,7 +174,8 @@
       #t (dict-keys m2))))
 
 ;; Unions two multisets. Shared members take the maximum count of each other.
-(define/contract (multiset-union m1 m2) (-> dict? dict? dict?)
+(define/contract (multiset-union m1 m2)
+  (-> dict? dict? dict?)
   (foldl
     (λ (x acc)
       (if (dict-has-key? acc x)
@@ -192,7 +184,8 @@
     m1 (dict-keys m2)))
 
 ;; Intersects two multisets. Shared members take the minimum count of each other.
-(define/contract (multiset-intersect m1 m2) (-> dict? dict? dict?)
+(define/contract (multiset-intersect m1 m2)
+  (-> dict? dict? dict?)
   (foldl
     (λ (x acc)
       (if (dict-has-key? m1 x)
@@ -201,16 +194,18 @@
     #hash() (dict-keys m2)))
 
 ;; Checks if a level is at its "base" form.
-(define/contract (level-base? l) (-> level? boolean?)
+(define/contract (level-base? l)
+  (-> stlc-full/level? boolean?)
   (match l
-    [n #:when (natural? n) (zero? n)]
     [s #:when (symbol? s) #t]
+    [n #:when (natural? n) (zero? n)]
     [`(+ ,s ... ,n) #:when (natural? n) (zero? n)] ; should be avoided
     [`(+ ,s ...) #t]))
 
 ;; Syntactic equality between levels is not trivial.
 ;; This helper function defines it.
-(define/contract (level-eq? l1 l2) (-> level? level? boolean?)
+(define/contract (level-eq? l1 l2)
+  (-> stlc-full/level? stlc-full/level? boolean?)
   (match* (l1 l2)
     [(n1 n2) #:when (and (natural? n1) (natural? n2))
       (equal? n1 n2)]
@@ -222,12 +217,13 @@
 
 ;; Levels can carry natural numbers, and so we define a stratification between them.
 ;; Note: this returns FALSE if the levels are incomparable (i.e. (level-geq 'a 'b))
-(define/contract (level-geq? l1 l2) (-> level? level? boolean?)
+(define/contract (level-geq? l1 l2)
+  (-> stlc-full/level? stlc-full/level? boolean?)
   (match* (l1 l2)
-    [(n1 n2) #:when (and (natural? n1) (natural? n2))
-      (>= n1 n2)]
     [(s1 s2) #:when (and (symbol? s1) (symbol? s2))
       (equal? s1 s2)]
+    [(n1 n2) #:when (and (natural? n1) (natural? n2))
+      (>= n1 n2)]
     [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
       (and (level-eq? `(+ ,@s1) `(+ ,@s2)) (level-geq? n1 n2))]
     [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n)
@@ -239,12 +235,13 @@
 
 ;; We define a maximum of two levels.
 ;; This can return one of the two levels or an entirely new level.
-(define/contract (level-max l1 l2) (-> level? level? level?)
+(define/contract (level-max l1 l2)
+  (-> stlc-full/level? stlc-full/level? stlc-full/level?)
   (match* (l1 l2)
-    [(n1 n2) #:when (and (natural? n1) (natural? n2))
-      (max n1 n2)]
     [(s1 s2) #:when (and (symbol? s1) (symbol? s2))
       (if (equal? s1 s2) s1 `(+ ,s1 ,s2))]
+    [(n1 n2) #:when (and (natural? n1) (natural? n2))
+      (max n1 n2)]
     [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
       (if (equal? s1 s2)
         `(+ ,@s1 ,(max n1 n2))
@@ -269,7 +266,8 @@
       (level-union `(+ ,@s1) `(+ ,@s2))]))
 
 ;; A helper function to perform the union of levels.
-(define/contract (level-union l1 l2) (-> level-base? level-base? level-base?)
+(define/contract (level-union l1 l2)
+  (-> level-base? level-base? level-base?)
   (match* (l1 l2)
     [(0 l) l]
     [(l 0) l]
@@ -277,12 +275,13 @@
       `(+ ,@(multiset->list (multiset-union (list->multiset s1) (list->multiset s2))))]))
 
 ;; We define addition in terms of our syntactic constructs.
-(define/contract (level-add l1 l2) (-> level? level? level?)
+(define/contract (level-add l1 l2)
+  (-> stlc-full/level? stlc-full/level? stlc-full/level?)
   (match* (l1 l2)
-    [(n1 n2) #:when (and (natural? n1) (natural? n2))
-      (+ n1 n2)]
     [(s1 s2) #:when (and (symbol? s1) (symbol? s2))
       `(+ ,s1 ,s2)]
+    [(n1 n2) #:when (and (natural? n1) (natural? n2))
+      (+ n1 n2)]
     [(`(+ ,s1 ... ,n1) `(+ ,s2 ... ,n2)) #:when (and (natural? n1) (natural? n2))
       (level-add (level-add `(+ ,@s1) `(+ ,@s2)) (+ n1 n2))]
     [(`(+ ,s1 ... ,n) `(+ ,s2 ...)) #:when (natural? n)
@@ -302,7 +301,8 @@
 
 ;; Decrements a level by 1.
 ;; ASSUMPTION: the level is not a base level (i.e. there is some n to dec)
-(define/contract (level-dec l) (-> level? level?)
+(define/contract (level-dec l)
+  (-> stlc-full/level? stlc-full/level?)
   (match l
     [n #:when (and (natural? n) (not (zero? n))) (- n 1)]
     [`(+ ,s ... 1) `(+ ,@s)]
@@ -310,18 +310,20 @@
     [_ (err (format "attempting to decrement base level ~a" l))]))
 
 ;; Returns the "base" form of a level.
-(define/contract (level-base l) (-> level? level?)
+(define/contract (level-base l)
+  (-> stlc-full/level? stlc-full/level?)
   (match l
-    [n #:when (natural? n) 0]
     [s #:when (symbol? s) s]
+    [n #:when (natural? n) 0]
     [`(+ ,s ... ,n) #:when (natural? n) `(+ ,@s)]
     [`(+ ,s ...) `(+ ,@s)]))
 
 ;; Returns the "offset" portion of a level.
-(define/contract (level-offset l) (-> level? level?)
+(define/contract (level-offset l)
+  (-> stlc-full/level? stlc-full/level?)
   (match l
-    [n #:when (natural? n) n]
     [s #:when (symbol? s) 0]
+    [n #:when (natural? n) n]
     [`(+ ,s ... ,n) #:when (natural? n) n]
     [`(+ ,s ...) 0]))
 
@@ -330,30 +332,32 @@
 ;; Otherwise, levels are syntactically inferred.
 ;; ASSUMPTION: the type is well-formed in the given context (i.e. all symbols bound).
 ;; This is not checked via contracts due to (presumably) massive performance overhead.
-(define/contract (level-type t Γ) (-> type? dict? level?)
+(define/contract (level-type t Γ)
+  (-> stlc-full/type? dict? stlc-full/level?)
   (match t
     [(or 'Unit 'Bool 'Nat) 0]
     [s #:when (symbol? s) 0] ; HACK: μ-type variables, not in Γ
-    [`(Ref ,t) ; KNOB
+    [`(Ref ,t)
       (let ([l (level-type t Γ)])
-        (if (level-base? l) l
-          (level-add l 1)))]
+      (if (and impredicative? (level-base? l))
+        l (level-add l 1)))]
     [(or `(,t1 × ,t2) `(,t1 ⊕ ,t2))
       (level-max (level-type t1 Γ) (level-type t2 Γ))]
-    [`(,t1 → ,l ,t2) ; KNOB
+    [`(,t1 → ,l ,t2) ; FIXME: knob??
       (if (and (level-geq? l (level-type t1 Γ)) (level-geq? l (level-type t2 Γ))) l
         (err (format "annotated level ~a is less than inferred levels ~a and ~a!")))]
     [`(μ ,x ,t)
       (level-type t (dict-set Γ x `(μ ,x ,t)))]))
 
 ;; Infers the level of a (well-formed) expression.
-(define/contract (level-expr e Γ) (-> expr? dict? level?)
+(define/contract (level-expr e Γ)
+  (-> stlc-full/expr? dict? stlc-full/level?)
   (match e
     ['sole 0]
     [n #:when (natural? n) 0]
     [b #:when (boolean? b) 0]
     [x #:when (dict-has-key? Γ x) ; free variables
-      (level-type (expand-whnf (dict-ref Γ x) Γ) Γ)]
+      (level-type (type->whnf (dict-ref Γ x) Γ) Γ)]
     [s #:when (symbol? s) 0] ; local variables
 
     [`(,e : ,t)
@@ -365,12 +369,12 @@
 
     [`(level ,l ,e) ; NOTE: is this correct?
       (level-expr e Γ)]
-    [`(,e ⇑ ,l)
+    [`(,e :: ,l)
       (level-add l (level-expr e Γ))]
 
-    [`(new ,e) ; KNOB
+    [`(new ,e) ; FIXME; knob??
       (let ([l (level-expr e Γ)])
-        (if (level-base? l) l (level-add l 1)))]
+      (if (level-base? l) l (level-add l 1)))]
 
     [`(if ,c ,e1 ,e2)
       (level-max (level-expr c Γ)
@@ -393,7 +397,8 @@
 ;; Whether a given type is a semantically valid type.
 ;; We assume any type in Γ is semantically valid.
 ;; Otherwise, we would infinitely recurse re: μ.
-(define/contract (well-formed? t Γ) (-> type? dict? boolean?)
+(define/contract (well-formed? t Γ)
+  (-> stlc-full/type? dict? boolean?)
   (match t
     [(or 'Unit 'Bool 'Nat) #t]
     [s #:when (symbol? s) (dict-has-key? Γ `(type s))]
@@ -406,7 +411,8 @@
       (well-formed? t (dict-set Γ `(type ,x) `(μ ,x ,t)))]))
 
 ;; Whether a given type at a given level is semantically valid.
-(define/contract (well-kinded? t l Γ) (-> type? level? dict? boolean?)
+(define/contract (well-kinded? t l Γ)
+  (-> stlc-full/type? stlc-full/level? dict? boolean?)
   (match t
     [(or 'Unit 'Bool 'Nat) (level-geq? l 0)]
     [s #:when (symbol? s)
@@ -428,16 +434,17 @@
 ;; Our heap is a Dict[Level, List[Dict[Addr, Expr]]]. In other words:
 ;; - the heap is first stratified by algebraic levels, i.e. α, β, α+β, etc
 ;; - those heaps are then stratified by n: the level as a natural number.
-;; - this is
-(define (heap? heap)
+#;
+(define (stlc-full/heap? heap)
   (match heap
     [`((,level-var . (,subheap ...)) ...)
-      (and (all? (λ (l) (level? l)) level-var)
+      (and (all? (λ (l) (stlc-full/level? l)) level-var)
         (all? (λ (n) (dict? n)) subheap))]
     [_ #f]))
 
 ;; Extends a list to have at least n+1 elements. Takes a default-generating procedure.
-(define/contract (list-extend l n default) (-> list? natural? procedure? list?)
+(define/contract (list-extend l n default)
+  (-> list? natural? procedure? list?)
   (if (>= n (length l))
     (build-list (+ n 1)
       (λ (k)
@@ -447,91 +454,101 @@
     l))
 
 ;; Models the allocation of an (unsized) memory pointer at an arbitrary heap level.
-(define/contract (alloc! Σ l) (-> dict? level? ptr?)
+(define/contract (alloc! Σ l)
+  (-> dict? stlc-full/level? stlc-full/ptr?)
   (let ([addr (gensym)] [base (level-base l)] [offset (level-offset l)])
-    (if (dict-has-key? Σ base)
-      (let ([base-heap (dict-ref Σ base)])
-        (if (>= offset (length base-heap))
-          (dict-set! Σ base ; FIXME: we probably should error if location is occupied
-            (let ([offset-heap (make-hash)])
-              (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null
-              (list-set (list-extend base-heap offset make-hash) offset offset-heap)))
-          (let ([offset-heap (list-ref base-heap offset)])
-            (dict-set! offset-heap addr 'null))))
-      (dict-set! Σ base
+  (if (dict-has-key? Σ base)
+    (let ([base-heap (dict-ref Σ base)])
+    (if (>= offset (length base-heap))
+      (dict-set! Σ base ; FIXME: we probably should error if location is occupied
         (let ([offset-heap (make-hash)])
-          (dict-set! offset-heap addr 'null)
-          (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap))))
-    `(ptr ,l ,addr)))
+        (dict-set! offset-heap addr 'null) ; FIXME: probably should not be null
+        (list-set (list-extend base-heap offset make-hash) offset offset-heap)))
+      (let ([offset-heap (list-ref base-heap offset)])
+      (dict-set! offset-heap addr 'null))))
+    (dict-set! Σ base
+      (let ([offset-heap (make-hash)])
+      (dict-set! offset-heap addr 'null)
+      (list-set (build-list (+ offset 1) (λ (_) (make-hash))) offset offset-heap))))
+  `(ptr ,l ,addr)))
 
 ;; Updates the heap given a pointer to a memory location and a value.
-(define/contract (write! Σ p v) (-> dict? ptr? value? ptr?)
+(define/contract (write! Σ p v)
+  (-> dict? stlc-full/ptr? stlc-full/value? stlc-full/ptr?)
   (match p
     [`(ptr ,l ,a)
       (let ([base (level-base l)] [offset (level-offset l)])
-        (if (dict-has-key? Σ base)
-          (let ([base-heap (dict-ref Σ base)])
-            (if (< offset (length base-heap))
-              (dict-set! (list-ref base-heap offset) a v)
-              (err (format "writing to invalid memory location ~a!" p))))
-          (err (format "writing to invalid memory location ~a!" p))))])
+      (if (dict-has-key? Σ base)
+        (let ([base-heap (dict-ref Σ base)])
+        (if (< offset (length base-heap))
+          (dict-set! (list-ref base-heap offset) a v)
+          (err (format "writing to invalid memory location ~a!" p))))
+        (err (format "writing to invalid memory location ~a!" p))))])
   p)
 
 ;; Returns the corresponding value of a pointer to a memory location on the heap.
-(define/contract (read! Σ p) (-> dict? ptr? value?)
+(define/contract (read! Σ p)
+  (-> dict? stlc-full/ptr? stlc-full/value?)
   (match p
     [`(ptr ,l ,a)
       (let ([base (level-base l)] [offset (level-offset l)])
-        (if (dict-has-key? Σ base)
-          (let ([base-heap (dict-ref Σ base)])
-            (if (< offset (length base-heap))
-              (dict-ref (list-ref base-heap offset) a)
-              (err (format "reading from invalid memory location ~a!" p))))
-          (err (format "reading from invalid memory location ~a!" p))))]))
+      (if (dict-has-key? Σ base)
+        (let ([base-heap (dict-ref Σ base)])
+        (if (< offset (length base-heap))
+          (dict-ref (list-ref base-heap offset) a)
+          (err (format "reading from invalid memory location ~a!" p))))
+        (err (format "reading from invalid memory location ~a!" p))))]))
 
 ;; Models the deallocation of all memory locations of level `l` or higher.
 ;; For complexity and performance purposes, we only support deallocating base levels.
-(define/contract (dealloc! Σ l) (-> dict? level-base? void?)
+(define/contract (dealloc! Σ l)
+  (-> dict? level-base? void?)
   (for-each
-    (λ (key) (if (level-geq? key l) (dict-remove! Σ key) (void)))
+    (λ (key)
+      (if (level-geq? key l)
+        (dict-remove! Σ key) (void)))
     (dict-keys Σ)))
 
 ;; Whether two types are equivalent in a context.
 ;; We define equivalence as equivalence up to α-renaming.
-(define/contract (equiv-type t1 t2 Γ) (-> type? type? dict? boolean?)
-  (equiv-type-core t1 t2 Γ Γ))
-(define (equiv-type-core t1 t2 Γ1 Γ2)
+(define/contract (equiv-type t1 t2 Γ)
+  (-> stlc-full/type? stlc-full/type? dict? boolean?)
+  (equiv-type/core t1 t2 Γ Γ))
+(define (equiv-type/core t1 t2 Γ1 Γ2)
   (match* (t1 t2)
     ; bound identifiers: if a key exists in the context, look it up
     [(x1 x2) #:when (dict-has-key? Γ1 `(type ,x1))
-      (equiv-type-core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)]
+      (equiv-type/core (dict-ref Γ1 `(type ,x1)) x2 Γ1 Γ2)]
     [(x1 x2) #:when (dict-has-key? Γ2 `(type ,x2))
-      (equiv-type-core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)]
+      (equiv-type/core x1 (dict-ref Γ2 `(type ,x2)) Γ1 Γ2)]
 
     ; recursive types: self-referential names can be arbitrary
     [(`(μ ,x1 ,t1) `(μ ,x2 ,t2))
       (let ([name gensym])
-        (equiv-type-core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))]
+      (equiv-type/core t1 t2 (dict-set Γ1 `(type ,x1) name) (dict-set Γ2 `(type ,x2) name)))]
 
     ; check for syntactic equivalence on remaining forms
     [(`(,l1 ...) `(,l2 ...))
-      (foldl (λ (x1 x2 acc) (if (equiv-type-core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
+      (foldl (λ (x1 x2 acc) (if (equiv-type/core x1 x2 Γ1 Γ2) acc #f)) #t l1 l2)]
     [(v1 v2) (equal? v1 v2)]))
 
 ;; Whether two expressions are equivalent in a context.
 ;; We define equivalence as equivalence up to α-renaming.
-; (define/contract (equiv-expr e1 e2 Γ) (-> expr? expr? dict? boolean?)
+; (define/contract (equiv-expr e1 e2 Γ)
+;   (-> stlc-full/expr? stlc-full/expr? dict? boolean?)
 ;   (equiv-expr-core e1 e2 Γ Γ))
 ; (define (equiv-expr-core e1 e2 Γ1 Γ2)
 ;   (match* (e1 e2)))
 
 ;; Expands a type alias into weak-head normal form, for literal matching.
-(define/contract (expand-whnf t Γ) (-> type? dict? type?)
+(define/contract (type->whnf t Γ)
+  (-> stlc-full/type? dict? stlc-full/type?)
   (if (dict-has-key? Γ `(type ,t))
-    (expand-whnf (dict-ref Γ `(type ,t)) Γ) t))
+    (type->whnf (dict-ref Γ `(type ,t)) Γ) t))
 
 ;; Replaces all references to a type alias with another alias.
-(define/contract (replace-type type key value) (-> type? type? type? type?)
+(define/contract (replace-type type key value)
+  (-> stlc-full/type? stlc-full/type? stlc-full/type? stlc-full/type?)
   (match type
     ; Do not accidentally replace shadowed bindings
     [`(μ ,x _) #:when (equal? x key) type]
@@ -541,218 +558,216 @@
 
 ;; Evaluates an expression to a value.
 ;; Follows the call-by-value evaluation strategy.
-(define/contract (call-by-value expr) (-> expr? value?)
-  (cbv-core expr #hash() (make-hash)))
-(define (cbv-core expr Γ Σ) ; ℓ
+(define (call-by-value expr)
+  (cbv/core (desugar expr) #hash() (make-hash)))
+(define/contract (cbv/core expr Γ Σ) ; ℓ
+  (-> stlc-full/expr? dict? dict? stlc-full/value?)
   (match expr
     ['sole 'sole]
     [n #:when (natural? n) n]
     [b #:when (boolean? b) b]
     [p #:when (dict-has-key? Σ p) p]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [f #:when (symbol? f) f]
 
     [`(,e : ,t)
-      (cbv-core e Γ Σ)]
+      (cbv/core e Γ Σ)]
     [`(type ,t1 ,t2 ,e)
-      (cbv-core e (dict-set Γ `(type ,t1) t2) Σ)]
+      (cbv/core e (dict-set Γ `(type ,t1) t2) Σ)]
 
     ; The (level ...) syntax introduces new level *variables*.
     [`(level ,l ,e)
-      (let ([v (cbv-core e (dict-set Γ `(level ,l) 'level) Σ)])
-        (dealloc! Σ l) v)] ; they are then freed at the end of scope
-    [`(,e ⇑ ,l)
-      (cbv-core e Γ Σ)]
+      (let ([v (cbv/core e (dict-set Γ `(level ,l) 'level) Σ)])
+      (dealloc! Σ l) v)] ; they are then freed at the end of scope
+    [`(,e :: ,l)
+      (cbv/core e Γ Σ)]
 
     [`(new ,e)
       (let ([p (alloc! Σ (level-expr e Γ))])
-        (write! Σ p (cbv-core e Γ Σ)))]
+      (write! Σ p (cbv/core e Γ Σ)))]
     [`(! ,e)
-      (match (cbv-core e Γ Σ)
+      (match (cbv/core e Γ Σ)
         [`(ptr ,l ,a) (read! Σ `(ptr ,l ,a))]
         [e (err (format "attempting to deref unknown expression ~a, expected ptr" e))])]
     [`(set ,e1 ,e2) ; FIXME: we do NOT check levels before writing here
-      (match (cbv-core e1 Γ Σ)
-        [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv-core e2 Γ Σ))]
+      (match (cbv/core e1 Γ Σ)
+        [`(ptr ,l ,a) (write! Σ `(ptr ,l ,a) (cbv/core e2 Γ Σ))]
         [e (err (format "attempting to write to unknown expression ~a, expected ptr" e))])]
 
     [`(inc ,e)
-      (match (cbv-core e Γ Σ)
+      (match (cbv/core e Γ Σ)
         [n #:when (natural? n) (+ n 1)]
         [e (err (format "incrementing an unknown value ~a" e))])]
     [`(if ,c ,e1 ,e2)
-      (match (cbv-core c Γ Σ)
-        ['#t (cbv-core e1 Γ Σ)]
-        ['#f (cbv-core e2 Γ Σ)]
+      (match (cbv/core c Γ Σ)
+        ['#t (cbv/core e1 Γ Σ)]
+        ['#f (cbv/core e2 Γ Σ)]
         [e (err (format "calling if on unknown expression ~a" e))])]
 
     [`(pair ,e1 ,e2)
-      `(pair ,(cbv-core e1 Γ Σ) ,(cbv-core e2 Γ Σ))]
+      `(pair ,(cbv/core e1 Γ Σ) ,(cbv/core e2 Γ Σ))]
     [`(car ,e)
-      (match (cbv-core e Γ Σ)
+      (match (cbv/core e Γ Σ)
         [`(pair ,e1 ,e2) e1]
         [e (err (format "calling car on unknown expression ~a" e))])]
     [`(cdr ,e)
-      (match (cbv-core e Γ Σ)
+      (match (cbv/core e Γ Σ)
         [`(pair ,e1 ,e2) e2]
         [e (err (format "calling cdr on unknown expression ~a" e))])]
 
     [`(inl ,e)
-      `(inl ,(cbv-core e Γ Σ))]
+      `(inl ,(cbv/core e Γ Σ))]
     [`(inr ,e)
-      `(inr ,(cbv-core e Γ Σ))]
+      `(inr ,(cbv/core e Γ Σ))]
     [`(case ,e (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (cbv-core e Γ Σ)
-        [`(inl ,e) (cbv-core e1 (dict-set Γ x1 e) Σ)]
-        [`(inr ,e) (cbv-core e2 (dict-set Γ x2 e) Σ)]
+      (match (cbv/core e Γ Σ)
+        [`(inl ,e) (cbv/core e1 (dict-set Γ x1 e) Σ)]
+        [`(inr ,e) (cbv/core e2 (dict-set Γ x2 e) Σ)]
         [e (err (format "calling case on unknown expression ~a" e))])]
 
-    [`(fold ,e) `(fold ,(cbv-core e Γ Σ))]
+    [`(fold ,e) `(fold ,(cbv/core e Γ Σ))]
     [`(unfold ,e)
-      (match (cbv-core e Γ Σ)
+      (match (cbv/core e Γ Σ)
         [`(fold ,e) e]
         [e (err (format "attempting to unfold unknown expression ~a" e))])]
 
     [`(λ (,x : ,t) ,e)
       `(λ (,x : ,t) ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (cbv-core e1 Γ Σ)
+      (match (cbv/core e1 Γ Σ)
         [`(λ (,x : ,t) ,e1 ,env)
-          (cbv-core e1 (dict-set env x (cbv-core e2 Γ Σ)) Σ)]
-        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]
-
-    [e (err (format "attempting to interpret unknown expression ~a" e))]))
+          (cbv/core e1 (dict-set env x (cbv/core e2 Γ Σ)) Σ)]
+        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]))
 
 ;; Checks that an expression is of a type, and returns #t or #f, or a bubbled-up error.
 ;; `with` must be a type in weak-head normal form for structural matching.
-(define/contract (check expr with) (-> expr? type? boolean?)
-  (check-core expr with #hash()))
-(define (check-core expr with Γ)
+(define (check expr with)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ)
+  (-> stlc-full/expr? stlc-full/type? dict? boolean?)
   (match expr
-    ['sole 'Unit]
-    [n #:when (natural? n) 'Nat]
-    [b #:when (boolean? b) 'Bool]
-    ; We expand into weak-head normal form as the binding may be whatever.
-    [x #:when (dict-has-key? Γ x)
-      (expand-whnf (dict-ref Γ x) Γ)]
-
     [`(type ,t1 ,t2 ,e)
-      (check-core e with (dict-set Γ `(type ,t1) t2))]
+      (check/core e with (dict-set Γ `(type ,t1) t2))]
 
     [`(level ,l ,e) ; We add the level to the context just to note it is valid.
-      (check-core e with (dict-set Γ `(level ,l) 'level))]
+      (check/core e with (dict-set Γ `(level ,l) 'level))]
 
     [`(new ,e)
       (match with
-        [`(Ref ,t) (check-core e t Γ)]
+        [`(Ref ,t) (check/core e t Γ)]
         [_ #f])]
     [`(! ,e)
-      (check-core e `(Ref ,with) Γ)]
+      (check/core e `(Ref ,with) Γ)]
 
     [`(if ,c ,e1 ,e2)
-      (and (check-core c 'Bool Γ)
-        (check-core e1 with Γ) (check-core e2 with Γ))]
+      (and (check/core c 'Bool Γ)
+        (check/core e1 with Γ) (check/core e2 with Γ))]
 
     [`(pair ,e1 ,e2)
       (match with
-        [`(,t1 × ,t2) (and (check-core e1 t1 Γ) (check-core e2 t2 Γ))]
+        [`(,t1 × ,t2) (and (check/core e1 t1 Γ) (check/core e2 t2 Γ))]
         [_ #f])]
 
     [`(inl ,e)
       (match with
-        [`(,t1 ⊕ ,t2) (check-core e t1 Γ)]
+        [`(,t1 ⊕ ,t2) (check/core e t1 Γ)]
         [_ #f])]
     [`(inr ,e)
       (match with
-        [`(,t1 ⊕ ,t2) (check-core e t2 Γ)]
+        [`(,t1 ⊕ ,t2) (check/core e t2 Γ)]
         [_ #f])]
     ; We do not technically need case in check form.
     ; We keep it here to avoid needing type annotations on `c`.
     [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (infer-core c Γ)
+      (match (infer/core c Γ)
         [`(,a1 ⊕ ,a2)
-          (and (check-core e1 with (dict-set Γ x1 a1))
-               (check-core e2 with (dict-set Γ x2 a2)))]
+          (and (check/core e1 with (dict-set Γ x1 a1))
+               (check/core e2 with (dict-set Γ x2 a2)))]
         [_ #f])]
 
     [`(fold ,e)
       (match with
-        [`(μ ,x ,t) (check-core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))]
+        [`(μ ,x ,t) (check/core e t (dict-set Γ `(type ,x) `(μ ,x ,t)))]
         [_ #f])]
 
     [`(λ (,x : ,t) ,e)
       (match with
-        [`(,t1 → ,l ,t2) ; KNOB
-          (and (equiv-type t t1 Γ) (check-core e t2 (dict-set Γ x t))
-            (> l (level-expr e (dict-set Γ x t1))))]
-        [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
+        [`(,t1 → ,l ,t2)
+          (and (equiv-type t t1 Γ) (check/core e t2 (dict-set Γ x t))
+            (if impredicative?
+              (> l (level-expr e (dict-set Γ x t1)))
+              (>= l (level-expr e (dict-set Γ x t1)))))]
         [_ #f])]
 
-    [_ (equiv-type (infer-core expr Γ) with Γ)]))
+    [_ (equiv-type (infer/core expr Γ) with Γ)]))
 
 ;; Infers a type from a given expression, if possible. Errors out otherwise.
 ;; Returns a type in weak-head normal form for structural matching.
-(define/contract (infer expr) (-> expr? type?)
-  (infer-core expr #hash()))
+(define (infer expr)
+  (infer/core (desugar expr) #hash()))
 ;; Γ is our context: a dictionary from symbols to types??? i forget actually
 ;; note: our context plays many roles.
-(define (infer-core expr Γ)
+(define/contract (infer/core expr Γ)
+  (-> stlc-full/expr? dict? stlc-full/type?)
   (match expr
     ['sole 'Unit]
     [n #:when (natural? n) 'Nat]
     [b #:when (boolean? b) 'Bool]
     ; We expand into weak-head normal form as the binding may be to another binding.
     [x #:when (dict-has-key? Γ x)
-      (expand-whnf (dict-ref Γ x) Γ)]
+      (type->whnf (dict-ref Γ x) Γ)]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
 
     [`(type ,t1 ,t2 ,e)
-      (infer-core e (dict-set Γ `(type ,t1) t2))]
+      (infer/core e (dict-set Γ `(type ,t1) t2))]
     [`(,e : ,t)
-      (if (check-core e (expand-whnf t Γ) Γ) (expand-whnf t Γ)
+      (if (check/core e (type->whnf t Γ) Γ) (type->whnf t Γ)
         (err (format "expression ~a is not of annotated type ~a" e t)))]
 
     [`(level ,l ,e) ; We add the level to the context just to note it is valid.
-      (infer-core e (dict-set Γ `(level ,l) 'level))]
-    [`(,e ⇑ ,l) ; We retrieve the level from the context to check it is valid.
+      (infer/core e (dict-set Γ `(level ,l) 'level))]
+    [`(,e :: ,l) ; We retrieve the level from the context to check it is valid.
       (if (dict-has-key? Γ `(level ,(level-base l)))
-        (infer-core e Γ)
+        (infer/core e Γ)
         (err (format "level ~a not found in context, was it introduced?")))]
 
     [`(new ,e)
-      `(Ref ,(infer-core e Γ))]
+      `(Ref ,(infer/core e Γ))]
     [`(ptr ,a)
       (err (format "cannot infer type from raw pointer ~a" `(ptr ,a)))]
     [`(! ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(Ref ,t) t]
         [t (err (format "attempting to deref term ~a of type ~a" e t))])]
     [`(set ,e1 ,e2) ; FIXME: this does not account for explicit allocation syntax!
-      (match (infer-core e1 Γ) ; should we check levels?
+      (match (infer/core e1 Γ) ; should we check levels?
         [`(Ref ,t)
-          (if (check-core e2 t Γ) 'Unit
+          (if (check/core e2 t Γ) 'Unit
             (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
-              e1 t e2 (infer-core e2 Γ))))]
+              e1 t e2 (infer/core e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
     [`(inc ,e)
-      (if (check-core e 'Nat Γ) 'Nat
-        (err (format "calling inc on incorrect type ~a, expected Nat" (infer-core e Γ))))]
+      (if (check/core e 'Nat Γ) 'Nat
+        (err (format "calling inc on incorrect type ~a, expected Nat" (infer/core e Γ))))]
     [`(if ,c ,e1 ,e2)
-      (if (check-core c 'Bool Γ)
-        (let ([t (infer-core e1 Γ)])
-          (if (check-core e2 t Γ) t
-            (err (format "if ~a is not of consistent type!"
-              `(if Bool ,t ,(infer-core e2 Γ))))))
+      (if (check/core c 'Bool Γ)
+        (let ([t (infer/core e1 Γ)])
+        (if (check/core e2 t Γ) t
+          (err (format "if ~a is not of consistent type!"
+            `(if Bool ,t ,(infer/core e2 Γ))))))
         (err (format "if ~a has incorrect type ~a on condition, expected Bool"
-          c (infer-core c Γ))))]
+          c (infer/core c Γ))))]
 
     [`(pair ,e1 ,e2)
-      `(,(infer-core e1 Γ) × ,(infer-core e2 Γ))]
+      `(,(infer/core e1 Γ) × ,(infer/core e2 Γ))]
     [`(car ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(,t1 × ,t2) t1]
         [t (err (format "calling car on incorrect type ~a, expected a product" t))])]
     [`(cdr ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(,t1 × ,t2) t2]
         [t (err (format "calling cdr on incorrect type ~a, expected a product" t))])]
 
@@ -761,34 +776,32 @@
     [`(inr ,e)
       (err (format "unable to infer the type of a raw inr"))]
     [`(case ,c (,x1 ⇒ ,e1) (,x2 ⇒ ,e2))
-      (match (infer-core c Γ)
+      (match (infer/core c Γ)
         [`(,a1 ⊕ ,a2)
-          (let ([b1 (infer-core e1 (dict-set Γ x1 a1))]
-                [b2 (infer-core e2 (dict-set Γ x2 a2))])
-            (if (equiv-type b1 b2 Γ) b1
-              (err (format "case ~a is not of consistent type!"
-                `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
+          (let ([b1 (infer/core e1 (dict-set Γ x1 a1))]
+                [b2 (infer/core e2 (dict-set Γ x2 a2))])
+          (if (equiv-type b1 b2 Γ) b1
+            (err (format "case ~a is not of consistent type!"
+              `(case (,a1 ⊕ ,a2) (,x1 ⇒ ,b1) (,x2 ⇒ ,b2))))))]
         [t (err (format "case has incorrect type ~a on condition, expected a sum" t))])]
 
     [`(unfold ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(μ ,x ,t) (replace-type t x `(μ ,x ,t))]
         [t (err (format "expected ~a to be of recursive type, got ~a" e t))])]
 
-    [`(λ (,x : ,t1) ,e) ; KNOB
-      (let* ([t2 (infer-core e (dict-set Γ x t1))]
-        [t1 (expand-whnf t1 Γ)] [l (+ 1 (level-expr e (dict-set Γ x t1)))])
-        `(,t1 → ,l ,t2))]
+    [`(λ (,x : ,t1) ,e)
+      (let* ([t2 (infer/core e (dict-set Γ x t1))]
+             [t1 (type->whnf t1 Γ)]
+             [l (level-expr e (dict-set Γ x t1))])
+      `(,t1 → ,(if impredicative? (+ l 1) l) ,t2))]
     [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(,t1 → ,l ,t2) ; should we check levels here? probably redundant
-          (if (check-core e2 t1 Γ) t2
+          (if (check/core e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a of type ~a"
-              t1 e2 (infer-core e2 Γ))))]
-        [`(,t1 → ,t2) (err (format "missing level annotation on function type"))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [_ (err (format "attempting to infer an unknown expression ~a" expr))]))
+              t1 e2 (infer/core e2 Γ))))]
+        [t (err (format "expected → type on application body, got ~a" t))])]))
 
 
 ;; Define aliases from higher-level constructs to lower-level core forms.
@@ -798,7 +811,7 @@
     ['⟨⟩ 'sole]
     [`(ref ,e) (desugar `(new ,e))]
     [`(deref ,e) (desugar `(! ,e))]
-    [`(,e :: ,k) (desugar `(,e ⇑ ,k))]
+    [`(,e ⇑ ,k) (desugar `(,e :: ,k))]
 
     ; set-with-continuation
     [`(set ,e1 ,e2 ,in)
@@ -826,7 +839,7 @@
 
 ;; (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))
 (check-equal?
-  (call-by-value (desugar '
+  (call-by-value '
     (let (next : ((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1
                   (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
       (λ (self : (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)))
@@ -839,31 +852,31 @@
           (pair 413
           (pair (new (inr sole))
                 (new (inr sole))))))
-    (next my_list)))))
+    (next my_list))))
   '(inr sole))
 
 (check-equal?
-  (infer (desugar '
+  (infer '
     (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
     (λ (self : DoublyLinkedList)
        (case (unfold self)
         (some ⇒ ((! (cdr (cdr some))) : DoublyLinkedList))
-        (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))))
+        (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
   '((μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit)) → 1 (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))
 
 (check-true
   (equiv-type
-    (infer (desugar '
+    (infer '
       (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
       (λ (self : DoublyLinkedList)
          (case (unfold self)
           (some ⇒ (! (cdr (cdr some))))
-          (none ⇒ ((fold (inr sole)) : DoublyLinkedList)))))))
+          (none ⇒ ((fold (inr sole)) : DoublyLinkedList))))))
   '(DoublyLinkedList → 1 DoublyLinkedList)
     #hash(((type DoublyLinkedList) . (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))))))
 
 (check-true
-  (check (desugar '
+  (check '
     (type DoublyLinkedList (μ Self ((Nat × ((Ref Self) × (Ref Self))) ⊕ Unit))
     (let (get : (DoublyLinkedList → 1 (Nat ⊕ Unit)))
       (λ self
@@ -885,5 +898,5 @@
         (pair 413
         (pair (new ((fold (inr sole)) : DoublyLinkedList))
               (new ((fold (inr sole)) : DoublyLinkedList))))))
-    (prev my_list)))))))
+    (prev my_list))))))
     'DoublyLinkedList))
diff --git a/stlc-hor.rkt b/stlc-hor.rkt
new file mode 100644
index 0000000..ad568c9
--- /dev/null
+++ b/stlc-hor.rkt
@@ -0,0 +1,154 @@
+#lang racket
+(require "lib.rkt")
+(require "base.rkt")
+(provide (all-defined-out))
+
+;; The Simply-Typed Lambda Calculus with higher-order references
+
+;; Whether the system is *predicative* or *impredicative*.
+;; The predicative system disallows quantification over references.
+;; The impredicative system allows so by tweaking level rules.
+(define impredicative? #f)
+
+;; Checks an expression for syntactic well-formedness.
+(define (stlc-hor/expr? expr)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    [(or `(new ,e) `(! ,e)) (stlc-hor/expr? e)]
+    [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-hor/expr? e1) (stlc-hor/expr? e2))]
+    [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-hor/type? t) (stlc-hor/expr? e))]
+    [_ #f]))
+
+;; Checks a type for syntactic well-formedness.
+(define (stlc-hor/type? type)
+  (match type
+    [t #:when (symbol? t) #t]
+    [`(,t1 → ,k ,t2) (and (natural? k) (stlc-hor/type? t1) (stlc-hor/type? t2))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc-hor/value? value)
+  (match value
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    [`(,v1 ,v2) (and (stlc-hor/value? v1) (stlc-hor/value? v2))]
+    [`(λ ,x ,e ,env) (and (symbol? x) (stlc-hor/expr? e) (dict? env))]
+    [_ #f]))
+
+;; Interprets an expression down to a value, in a given context.
+(define (interpret expr)
+  (interpret/core (desugar expr) #hash() (make-hash)))
+(define/contract (interpret/core expr Γ Σ)
+  (-> stlc-hor/expr? dict? dict? stlc-hor/value?)
+  (match expr
+    [r #:when (dict-has-key? Σ r) r]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [f #:when (symbol? f) f]
+
+    [`(new ,e)
+      (let ([r (gensym)])
+      (dict-set! Σ r e) r)]
+    [`(! ,e)
+      (let ([r (interpret/core e Γ Σ)])
+      (if (dict-has-key? Σ r)
+        (interpret/core (dict-ref Σ r) Γ Σ)
+        (err (format "attempting to deref unknown reference ~a" r))))]
+    [`(set ,e1 ,e2)
+      (let ([r (interpret/core e1 Γ Σ)])
+      (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ))
+        (err (format "attempting to update unknown reference ~a" r))))
+      'sole]
+
+    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
+    [`(,e1 ,e2)
+      (match (interpret/core e1 Γ Σ)
+        [`(λ ,x ,e1 ,env)
+          (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)]
+        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]))
+
+;; Checks an expression against some type, in a given context.
+(define (check expr with)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ)
+  (-> stlc-hor/expr? stlc-hor/type? dict? boolean?)
+  (match expr
+    [`(new ,e)
+      (match with
+        [`(Ref ,t) (check/core e t Γ)]
+        [_ #f])]
+    [`(! ,e)
+      (check/core e `(Ref ,with) Γ)]
+
+    [`(λ (,x : ,t) ,e)
+      (match with
+        [`(,t1 → ,k ,t2)
+          (and (equal? t t1) (check/core e t2 (dict-set Γ x t))
+            (if impredicative?
+              (> k (level-expr e (dict-set Γ x t1)))
+              (>= k (level-expr e (dict-set Γ x t1)))))]
+        [_ #f])]
+
+    [_ (equal? (infer/core expr Γ) with)]))
+
+;; Infers a type from some expression, in a given context.
+(define (infer expr)
+  (infer/core (desugar expr) #hash()))
+(define/contract (infer/core expr Γ)
+  (-> stlc-hor/expr? dict? stlc-hor/type?)
+  (match expr
+    ['sole 'Unit]
+    [n #:when (natural? n) 'Nat]
+    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
+
+    [`(new ,e) `(Ref ,(infer/core e Γ))]
+    [`(! ,e)
+      (match (infer/core e Γ)
+        [`(Ref ,t) t]
+        [t (err "attempting to deref term not of Ref type!")])]
+    [`(set ,e1 ,e2)
+      (match (infer/core e1 Γ)
+        [`(Ref ,t)
+          (if (check/core e2 t Γ) 'Unit
+            (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
+              e1 t e2 (infer/core e2 Γ))))]
+        [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
+
+    [`(λ (,x : ,t1) ,e)
+      (let ([t2 (infer/core e (dict-set Γ x t1))]
+            [k (level-expr e (dict-set Γ x t1))])
+      `(,t1 → ,(if impredicative? (+ k 1) k) ,t2))]
+    [`(,e1 ,e2)
+      (match (infer/core e1 Γ)
+        [`(,t1 → ,k ,t2)
+          (if (check/core e2 t1 Γ) t2
+            (err (format "inferred argument type ~a does not match arg ~a of type ~a"
+              t1 e2 (infer/core e2 Γ))))]
+        [t (err (format "expected → type on application body, got ~a" t))])]))
+
+;; Get the level associated with a type. This is known at compile time.
+(define/contract (level-type type)
+  (-> stlc-hor/type? natural?)
+  (match type
+    [(or 'Unit 'Nat) 0]
+    [`(Ref ,t)
+      (let ([k (level-type t)])
+      (if (and impredicative? (zero? k)) 0 (+ 1 k)))]
+    [`(,t1 → ,k ,t2)
+      (if (and (>= k (level-type t1)) (>= k (level-type t2))) k
+        (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
+          k t1 t2)))]
+    [t (err (format "attempting to infer the level of unknown type ~a" t))]))
+
+;; Get the level of an arbitrary expression. This is not known until runtime.
+(define/contract (level-expr expr Γ)
+  (-> stlc-hor/expr? dict? natural?)
+  (match expr
+    ['sole 0]
+    [n #:when (natural? n) 0]
+    [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))]
+    [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-expr e Γ)]
+    [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-expr e1 Γ) (level-expr e2 Γ))]
+    [x #:when (symbol? x) 0])) ; local variables, not in Γ
diff --git a/stlc-imp.rkt b/stlc-imp.rkt
deleted file mode 100644
index c550359..0000000
--- a/stlc-imp.rkt
+++ /dev/null
@@ -1,112 +0,0 @@
-#lang racket
-(require "lib.rkt")
-(require "base.rkt")
-(require (only-in "stlc-ref.rkt" interpret))
-(provide check infer level-type level-body)
-
-;; The Simply-Typed Lambda Calculus with higher-order *impredicative* references
-
-; Γ, x: τ₁ ⊢ e: τ₂    k > max-level(Γ, τ₁, τ₂)
-; ---------------------------------------------
-; Γ ⊢ λx:τ₁.e : τ₁ →ᵏ τ₂
-
-; Γ ⊢ e₁: τ₁ →ᵏ τ₂    Γ ⊢ e₂: τ₁
-; --------------------------------
-; Γ ⊢ (e₁ e₂): τ₂
-
-; --------------------------
-; Nat::Type₀, Unit::Type₀
-
-; τ::Type₀
-; ---------------
-; Ref τ :: Type₀
-
-; τ::Typeᵢ, i ≥ 0
-; ---------------
-; Ref τ :: Typeᵢ₊₁
-
-; τ₁::Typeᵢ, τ₂::Typeⱼ, k > max-level(τ₁, τ₂)
-; -----------------------------------------
-; τ₁ →ᵏ τ₂ :: Typeₖ
-(require (only-in "stlc-ref.rkt" interpret))
-
-;;      (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
-  (match expr
-    [`(new ,e)
-      (match with
-        [`(Ref ,t) (check-core e t Γ)]
-        [_ #f])]
-    [`(! ,e)
-      (check-core e `(Ref ,with) Γ)]
-
-    [`(λ (,x : ,t) ,e)
-      (match with
-        [`(,t1 → ,k ,t2)
-          (and (equal? t t1) (check-core e t2 (dict-set Γ x t))
-            (> k (level-body e (dict-set Γ x t1))))] ; KNOB
-        [_ #f])]
-
-    [_ (equal? (infer-core expr Γ) with)]))
-
-;;      (infer Expr Table[Sym, Type]): Type
-(define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
-  (match expr
-    ['sole 'Unit]
-    [n #:when (natural? n) 'Nat]
-    [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
-
-    [`(new ,e) `(Ref ,(infer-core e Γ))]
-    [`(! ,e)
-      (match (infer-core e Γ)
-        [`(Ref ,t) t]
-        [t (err "attempting to deref term not of Ref type!")])]
-    [`(set ,e1 ,e2)
-      (match (infer-core e1 Γ)
-        [`(Ref ,t)
-          (if (check-core e2 t Γ) 'Unit
-            (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
-              e1 t e2 (infer-core e2 Γ))))]
-        [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
-
-    [`(λ (,x : ,t1) ,e)
-      (let* ([t2 (infer-core e (dict-set Γ x t1))]
-        [k (+ 1 (level-body e (dict-set Γ x t1)))]) ; KNOB
-      `(,t1 → ,k ,t2))]
-    [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
-        [`(,t1 → ,k ,t2)
-          (if (check-core e2 t1 Γ) t2
-            (err (format "inferred argument type ~a does not match arg ~a of type ~a"
-              t1 e2 (infer-core e2 Γ))))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
-
-;;      (level-type Type): Natural
-(define (level-type t)
-  (match t
-    ['Unit 0]
-    ['Nat 0]
-    [`(,t1 → ,k ,t2)
-      (if (and (>= k (level-type t1)) (>= k (level-type t2))) k
-        (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
-          k t1 t2)))]
-    [`(Ref ,t)
-      (let ([k (level-type t)])
-      (if (zero? k) 0 (+ 1 k)))] ; KNOB
-    [t (err (format "attempting to infer the level of unknown type ~a" t))]))
-
-;;      (level-body Expr Table[Sym, Type]): Natural
-(define (level-body e Γ)
-  (match e
-    ['sole 0]
-    [n #:when (natural? n) 0]
-    [x #:when (dict-has-key? Γ x) (level-type (dict-ref Γ x))]
-    [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)]
-    [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))]
-    [x #:when (symbol? x) 0])) ; local variables, not in Γ
diff --git a/stlc-pred.rkt b/stlc-pred.rkt
deleted file mode 100644
index 197ad74..0000000
--- a/stlc-pred.rkt
+++ /dev/null
@@ -1,84 +0,0 @@
-#lang racket
-(require "lib.rkt")
-(require "base.rkt")
-(require (only-in "stlc-ref.rkt" interpret))
-(provide check infer level-type level-body)
-
-;; The Simply-Typed Lambda Calculus with higher-order *predicative* references
-
-;;      (check Expr Type Table[Sym, Type]): Bool
-(define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
-  (match expr
-    [`(new ,e)
-      (match with
-        [`(Ref ,t) (check-core e t Γ)]
-        [_ #f])]
-
-    [`(λ (,x : ,t) ,e)
-      (match with
-        [`(,t1 → ,k ,t2)
-          (and (equal? t t1) (check-core e t2 (dict-set Γ x t1))
-            (>= k (level-body e (dict-set Γ x t1))))] ; KNOB
-        [_ #f])]
-
-    [_ (equal? (infer-core expr Γ) with)]))
-
-;;      (infer Expr Table[Sym, Type]): Type
-(define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
-  (match expr
-    ['sole 'Unit]
-    [n #:when (natural? n) 'Nat]
-    [x #:when (dict-has-key? Γ x)
-      (dict-ref Γ x)]
-
-    [`(new ,e) `(Ref ,(infer-core e Γ))]
-    [`(! ,e)
-      (match (infer-core e Γ)
-        [`(Ref ,t) t]
-        [t (err "attempting to deref term not of Ref type!")])]
-    [`(set ,e1 ,e2)
-      (match (infer-core e1 Γ)
-        [`(Ref ,t)
-          (if (check-core e2 t Γ) 'Unit
-            (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
-              e1 t e2 (infer-core e2 Γ))))]
-        [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
-
-    [`(λ (,x : ,t1) ,e)
-      (let* ([t2 (infer-core e (dict-set Γ x t1))]
-        [k (level-body e (dict-set Γ x t1))]) ; KNOB
-      `(,t1 → ,k ,t2))]
-    [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
-        [`(,t1 → ,k ,t2)
-          (if (check-core e2 t1 Γ) t2
-            (err (format "inferred argument type ~a does not match arg ~a of type ~a" t1 e2 (infer-core e2 Γ))))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
-
-;;      (level-type Type): Natural
-(define (level-type t)
-  (match t
-    [(or 'Unit 'Nat) 0]
-    [`(,t1 → ,k ,t2)
-      (if (and (>= k (level-type t1)) (>= k (level-type t2))) k
-        (err (format "annotated level ~a is less than inferred levels of ~a and ~a!"
-          k t1 t2)))]
-    [`(Ref ,t) (+ 1 (level-type t))] ; (KNOB)
-    [t (err (format "attempting to infer the level of unknown type ~a" t))]))
-
-;;      (level-body Expr Table[Sym, Type]): Natural
-(define (level-body e Γ)
-  (match e
-    ['sole 0]
-    [n #:when (natural? n) 0]
-    [x #:when (dict-has-key? Γ x)
-      (level-type (dict-ref Γ x))]
-    [(or `(new ,e) `(! ,e) `(λ (,_ : ,_) ,e)) (level-body e Γ)]
-    [(or `(set ,e1 ,e2) `(,e1 ,e2)) (max (level-body e1 Γ) (level-body e2 Γ))]
-    [x #:when (symbol? x) 0]))
diff --git a/stlc-rec.rkt b/stlc-rec.rkt
index 84103bb..3266150 100644
--- a/stlc-rec.rkt
+++ b/stlc-rec.rkt
@@ -5,87 +5,104 @@
 
 ;; The Simply-Typed Lambda Calculus with iso-recursive types
 
-; Γ ⊢ e: [x ↦ μx.t] t
-; ------------------------
-; Γ ⊢ fold [μx.t] e: μx.t
-
-; Γ ⊢ e: μx.t
-; -----------------------------------
-; Γ ⊢ unfold [μx.t] e: [x ↦ μx.t] t
-
-;;      (interpret Expr Table[Sym, Expr]): Value
+;; Checks an expression for syntactic well-formedness.
+(define (stlc-rec/expr? expr)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [(or `(fold ,e) `(unfold ,e)) (stlc-rec/expr? e)]
+    [`(,e1 ,e2) (and (stlc-rec/expr? e1) (stlc-rec/expr? e2))]
+    [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-rec/type? t) (stlc-rec/expr? e))]
+    [_ #f]))
+
+;; Checks a type for syntactic well-formedness.
+(define (stlc-rec/type? type)
+  (match type
+    [t #:when (symbol? t) #t]
+    [`(,t1 → ,t2) (and (stlc-rec/type? t1) (stlc-rec/type? t2))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc-rec/value? value)
+  (match value
+    [x #:when (symbol? x) #t]
+    [`(,v1 ,v2) (and (stlc-rec/value? v1) (stlc-rec/value? v2))]
+    [`(λ ,x ,e ,env) (and (symbol? x) (stlc-rec/expr? e) (dict? env))]
+    [_ #f]))
+
+;; Interprets an expression down to a value, in a given context.
 (define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash()))
-(define (interpret-core expr Γ)
+  (interpret/core (desugar expr) #hash()))
+(define/contract (interpret/core expr Γ)
+  (-> stlc-rec/expr? dict? stlc-rec/value?)
   (match expr
     ['sole 'sole]
-    [n #:when (natural? n) n]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [n #:when (natural? n) n]
+    [f #:when (symbol? f) f]
 
-    [`(fold ,e) `(fold ,(interpret-core e Γ))]
+    [`(fold ,e) `(fold ,(interpret/core e Γ))]
     [`(unfold ,e)
-      (match (interpret-core e Γ)
+      (match (interpret/core e Γ)
         [`(fold ,e) e]
         [e `(unfold e)])]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
+    [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret-core e1 Γ)
+      (match (interpret/core e1 Γ)
         [`(λ ,x ,e ,env)
-          (interpret-core e (dict-set env x (interpret-core e2 Γ)))]
-        [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]
-
-    [e (err (format "interpreting an unknown expression ~a" e))]))
+          (interpret/core e (dict-set env x (interpret/core e2 Γ)))]
+        [e (err (format "applying arg ~a to unknown expression ~a" e2 e))])]))
 
-;;      (check Expr Type Table[Sym, Type]): Bool
+;; Checks an expression against some type, in a given context.
 (define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ)
+  (-> stlc-rec/expr? stlc-rec/type? dict? boolean?)
   (match expr
     [`(fold (μ ,x ,t) ,e)
       (match with
-        [`(μ ,x ,t) (check-core e t (dict-set Γ x `(μ ,x ,t)))]
+        [`(μ ,x ,t) (check/core e t (dict-set Γ x `(μ ,x ,t)))]
         [_ #f])]
 
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,t2)
-          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
+          (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))]
         [_ #f])]
 
-    [_ (equal? (infer-core expr Γ) with)]))
+    [_ (equal? (infer/core expr Γ) with)]))
 
-;;      (infer Expr Table[Sym, Type]): Type
+;; Infers a type from some expression, in a given context.
 (define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
+  (infer/core (desugar expr) #hash()))
+(define/contract (infer/core expr Γ)
+  (-> stlc-rec/expr? dict? stlc-rec/type?)
   (match expr
     ['sole 'Unit]
-    [n #:when (natural? n) 'Nat]
-    [b #:when (boolean? b) 'Bool]
     [x #:when (dict-has-key? Γ x)
       (dict-ref Γ x)]
+    [b #:when (boolean? b) 'Bool]
+    [n #:when (natural? n) 'Nat]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
 
     [`(fold (μ ,x ,t) ,e)
-      (if (check-core e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t)
+      (if (check/core e t (dict-set Γ x `(μ ,x ,t))) `(μ ,x ,t)
         (err (format "expected ~a to be of type ~a, got ~a"
           e t (infer e (dict-set Γ x `(μ ,x ,t))))))]
     [`(unfold (μ ,x ,t) ,e)
-      (if (check-core e `(μ ,x ,t)) (replace t x `(μ ,x ,t))
+      (if (check/core e `(μ ,x ,t)) (replace t x `(μ ,x ,t))
         (err (format "expected ~a to be of type ~a, got ~a"
-          e `(μ ,x ,t) (infer-core e Γ))))]
+          e `(μ ,x ,t) (infer/core e Γ))))]
 
     [`(λ (,x : ,t) ,e)
-      `(,t → ,(infer-core e (dict-set Γ x t)))]
-
+      `(,t → ,(infer/core e (dict-set Γ x t)))]
     [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(,t1 → ,t2)
-          (if (check-core e2 t1 Γ) t2
+          (if (check/core e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
+        [t (err (format "expected → type on application body, got ~a" t))])]))
 
 ;; Replace all references to an expression with a value.
 (define (replace expr key value)
diff --git a/stlc-ref.rkt b/stlc-ref.rkt
index d0afec0..4f5ac91 100644
--- a/stlc-ref.rkt
+++ b/stlc-ref.rkt
@@ -1,92 +1,120 @@
 #lang racket
 (require "lib.rkt")
 (require "base.rkt")
-(provide interpret check infer)
+(provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus with references
 
-;;      (interpret Expr Table[Sym, Expr] Table[Sym, Expr]): Value
+; todo: rewrite to use call-by-reference or call-by-value or call-by-name explicitly
+
+;; Checks an expression for syntactic well-formedness.
+(define (stlc-ref/expr? expr)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    [(or `(new ,e) `(! ,e)) (stlc-ref/expr? e)]
+    [(or `(set ,e1 ,e2) `(,e1 ,e2)) (and (stlc-ref/expr? e1) (stlc-ref/expr? e2))]
+    [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc-ref/type? t) (stlc-ref/expr? e))]
+    [_ #f]))
+
+;; Checks a type for syntactic well-formedness.
+(define (stlc-ref/type? type)
+  (match type
+    [t #:when (symbol? t) #t]
+    [`(Ref ,t) (stlc-ref/type? t)]
+    [`(,t1 → ,t2) (and (stlc-ref/type? t1) (stlc-ref/type? t2))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc-ref/value? value)
+  (match value
+    [x #:when (symbol? x) #t]
+    [n #:when (natural? n) #t]
+    [`(,v1 ,v2) (and (stlc-ref/value? v1) (stlc-ref/value? v2))]
+    [`(λ ,x ,e ,env) (and (symbol? x) (stlc-ref/expr? e) (dict? env))]
+    [_ #f]))
+
+;; Interprets an expression down to a value, in a given context.
 (define (interpret expr)
-  (interpret-core (strip (desugar expr)) #hash() (make-hash)))
-(define (interpret-core expr Γ Σ)
+  (interpret/core (desugar expr) #hash() (make-hash)))
+(define/contract (interpret/core expr Γ Σ)
+  (-> stlc-ref/expr? dict? dict? stlc-ref/value?)
   (match expr
-    ['sole 'sole]
-    [n #:when (natural? n) n]
     [r #:when (dict-has-key? Σ r) r]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [f #:when (symbol? f) f]
 
     [`(new ,e)
       (let ([r (gensym)])
       (dict-set! Σ r e) r)]
     [`(! ,e)
-      (let ([r (interpret-core e Γ Σ)])
+      (let ([r (interpret/core e Γ Σ)])
       (if (dict-has-key? Σ r)
-        (interpret-core (dict-ref Σ r) Γ Σ)
+        (interpret/core (dict-ref Σ r) Γ Σ)
         (err (format "attempting to deref unknown reference ~a" r))))]
     [`(set ,e1 ,e2)
-      (let ([r (interpret-core e1 Γ Σ)])
-      (if (dict-has-key? Σ r) (dict-set! Σ r (interpret-core e2 Γ Σ))
+      (let ([r (interpret/core e1 Γ Σ)])
+      (if (dict-has-key? Σ r) (dict-set! Σ r (interpret/core e2 Γ Σ))
         (err (format "attempting to update unknown reference ~a" r))))
       'sole]
 
-    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
-    [`(λ ,x ,e ,env) `(λ ,x ,e ,env)] ; ???
+    [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
-      (match (interpret-core e1 Γ Σ)
+      (match (interpret/core e1 Γ Σ)
         [`(λ ,x ,e1 ,env)
-          (interpret-core e1 (dict-set env x (interpret-core e2 Γ Σ)) Σ)]
-        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]
-
-    [e (err (format "attempting to interpret unknown expression ~a" e))]))
+          (interpret/core e1 (dict-set env x (interpret/core e2 Γ Σ)) Σ)]
+        [e1 (err (format "attempting to interpret arg ~a applied to unknown expression ~a" e2 e1))])]))
 
-;;      (check Expr Type Table[Sym, Type]): Bool
+;; Checks an expression against some type, in a given context.
 (define (check expr with)
-  (check-core (desugar expr) with #hash()))
-(define (check-core expr with Γ)
+  (check/core (desugar expr) with #hash()))
+(define/contract (check/core expr with Γ)
+  (-> stlc-ref/expr? stlc-ref/type? dict? boolean?)
   (match expr
     [`(new ,e)
       (match with
-        [`(Ref ,t) (check-core e t Γ)]
+        [`(Ref ,t) (check/core e t Γ)]
         [_ #f])]
-    [`(! ,e) (check-core e `(Ref ,with) Γ)]
+    [`(! ,e) (check/core e `(Ref ,with) Γ)]
 
     [`(λ (,x : ,t) ,e)
       (match with
         [`(,t1 → ,t2)
-          (and (equal? t1 t) (check-core e t2 (dict-set Γ x t1)))]
+          (and (equal? t1 t) (check/core e t2 (dict-set Γ x t1)))]
         [_ #f])]
 
-    [_ (equal? (infer-core expr Γ) with)]))
+    [_ (equal? (infer/core expr Γ) with)]))
 
-;;      (infer Expr Table[Sym, Type]): Type
+;; Infers a type from some expression, in a given context.
 (define (infer expr)
-  (infer-core (desugar expr) #hash()))
-(define (infer-core expr Γ)
+  (infer/core (desugar expr) #hash()))
+(define/contract (infer/core expr Γ)
+  (-> stlc-ref/expr? dict? stlc-ref/type?)
   (match expr
     ['sole 'Unit]
-    [n #:when (natural? n) 'Nat]
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
+    [n #:when (natural? n) n]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
 
-    [`(new ,e) `(Ref ,(infer-core e Γ))]
+    [`(new ,e) `(Ref ,(infer/core e Γ))]
     [`(! ,e)
-      (match (infer-core e Γ)
+      (match (infer/core e Γ)
         [`(Ref ,t) t]
         [t (err "attempting to deref term not of Ref type!")])]
     [`(set ,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(Ref ,t)
-          (if (check-core e2 t Γ) 'Unit
+          (if (check/core e2 t Γ) 'Unit
             (err (format "attempting to update ~a: ~a with term ~a: ~a of differing type"
-              e1 t e2 (infer-core e2 Γ))))]
+              e1 t e2 (infer/core e2 Γ))))]
         [t (err (format "attempting to update non-reference ~a: ~a" e1 t))])]
 
     [`(λ (,x : ,t) ,e)
-      `(,t → ,(infer-core e (dict-set Γ x t)))]
+      `(,t → ,(infer/core e (dict-set Γ x t)))]
     [`(,e1 ,e2)
-      (match (infer-core e1 Γ)
+      (match (infer/core e1 Γ)
         [`(,t1 → ,t2)
-          (if (check-core e2 t1 Γ) t2
+          (if (check/core e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
-        [t (err (format "expected → type on application body, got ~a" t))])]
-
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
+        [t (err (format "expected → type on application body, got ~a" t))])]))
diff --git a/stlc.rkt b/stlc.rkt
index 2ed7d90..3058bf2 100644
--- a/stlc.rkt
+++ b/stlc.rkt
@@ -1,23 +1,48 @@
 #lang racket
 (require "lib.rkt")
 (require "base.rkt")
-(provide interpret check infer)
+(provide (all-defined-out))
 
 ;; The Simply-Typed Lambda Calculus
 
-;;      (interpret Expr Context): Value
-(define (interpret expr [Γ #hash()])
-  (match (strip expr)
+;; Checks an expression for syntactic well-formedness.
+(define (stlc/expr? expr)
+  (match expr
+    [x #:when (symbol? x) #t]
+    [`(,e1 ,e2) (and (stlc/expr? e1) (stlc/expr? e2))]
+    [`(λ (,x : ,t) ,e) (and (symbol? x) (stlc/type? t) (stlc/expr? e))]
+    [_ #f]))
+
+;; Checks a type for syntactic well-formedness.
+(define (stlc/type? type)
+  (match type
+    [t #:when (symbol? t) #t]
+    [`(,t1 → ,t2) (and (stlc/type? t1) (stlc/type? t2))]
+    [_ #f]))
+
+;; Checks a value for syntactic well-formedness.
+(define (stlc/value? value)
+  (match value
+    [x #:when (symbol? x) #t]
+    [`(,v1 ,v2) (and (stlc/value? v1) (stlc/value? v2))]
+    [`(λ ,x ,e ,env) (and (symbol? x) (stlc/expr? e) (dict? env))]
+    [_ #f]))
+
+;; Interprets an expression down to a value, in a given context.
+(define/contract (interpret expr [Γ #hash()])
+  (->* (stlc/expr?) (dict?) stlc/value?)
+  (match expr
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
-    [`(λ ,x ,e) `(λ ,x ,e ,Γ)]
+    [f #:when (symbol? f) f]
+    [`(λ (,x : ,t) ,e) `(λ ,x ,e ,Γ)]
     [`(,e1 ,e2)
       (match (interpret e1 Γ)
         [`(λ ,x ,e ,env) (interpret e (dict-set env x (interpret e2 Γ)))]
-        [e `(,e ,(interpret e2 Γ))])]
-    [e e]))
+        [e `(,e ,(interpret e2 Γ))])]))
 
-;;      (check Expr Type Context): Bool
-(define (check expr with [Γ #hash()])
+;; Checks an expression against some type, in a given context.
+(define/contract (check expr with [Γ #hash()])
+  (->* (stlc/expr? stlc/type?) (dict?) boolean?)
   (match expr
     [`(λ (,x : ,t) ,e)
       (match with
@@ -26,16 +51,19 @@
         [_ #f])]
     [_ (equal? with (infer with Γ))]))
 
-;;      (infer Expr Context): Type
-(define (infer expr [Γ #hash()])
+;; Infers a type from some expression, in a given context.
+(define/contract (infer expr [Γ #hash()])
+  (->* (stlc/expr?) (dict?) stlc/type?)
   (match expr
     [x #:when (dict-has-key? Γ x) (dict-ref Γ x)]
-    [`(λ (,x : ,t) ,e)
-      `(,t → ,(infer e (dict-set Γ x t)))]
+    [f #:when (symbol? f)
+      (err (format "attempting to infer type of free variable ~a" f))]
     [`(,e1 ,e2)
       (match (infer e1 Γ)
         [`(,t1 → ,t2)
           (if (check e2 t1 Γ) t2
             (err (format "inferred argument type ~a does not match arg ~a" t1 e2)))]
         [t (err (format "expected → type on application body, got ~a" t))])]
-    [e (err (format "attempting to infer an unknown expression ~a" e))]))
+    [`(λ (,x : ,t) ,e)
+      `(,t → ,(infer e (dict-set Γ x t)))]))
+
diff --git a/tests/stlc-imp.rkt b/tests/stlc-imp.rkt
deleted file mode 100644
index 44e0c17..0000000
--- a/tests/stlc-imp.rkt
+++ /dev/null
@@ -1,29 +0,0 @@
-#lang racket
-(require (except-in rackunit check))
-(require "../stlc-imp.rkt")
-
-(define-test-suite landins-knot
-  (check-exn
-    exn:fail?
-    (λ () (infer '
-      (let (id : (Nat → 1 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-      (set r f
-      (f 0))))))))
-
-  (check-eq? ; fixme: this should fail
-    (infer '
-      (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-      (f 0)))))
-    'Nat)
-
-  (check-true
-    (check '
-      (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-      (f 0))))
-      'Nat)))
diff --git a/tests/stlc-pred.rkt b/tests/stlc-pred.rkt
deleted file mode 100644
index f7afc43..0000000
--- a/tests/stlc-pred.rkt
+++ /dev/null
@@ -1,29 +0,0 @@
-#lang racket
-(require (except-in rackunit check))
-(require "../stlc-pred.rkt")
-
-(define-test-suite landins-knot
-  (check-exn
-    exn:fail?
-    (λ () (infer '
-      (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-      (set r f
-      (f 0))))))))
-
-  (check-eq?
-    (infer '
-      (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-      (f 0)))))
-    'Nat)
-
-  (check-true
-    (check '
-      (let (id : (Nat → 0 Nat)) (λ x x)
-      (let (r : (Ref (Nat → 0 Nat))) (new id)
-      (let (f : (Nat → 1 Nat)) (λ x ((! r) x))
-      (f 0))))
-      'Nat)))
diff --git a/tests/stlc.rkt b/tests/stlc.rkt
index 154e77d..cfec36f 100644
--- a/tests/stlc.rkt
+++ b/tests/stlc.rkt
@@ -2,7 +2,7 @@
 (require (except-in rackunit check))
 (require "../stlc.rkt")
 
-(check-equal? (interpret '(λ x x)) '(λ x x #hash()))
-(check-equal? (interpret '((λ a a) (x y))) '(x y))
-(check-equal? (interpret '((λ a (x y)) (λ z z))) '(x y))
-(check-equal? (interpret '((λ a (a y)) x)) '(x y))
+(check-equal? (interpret '(λ (x : Foo) x)) '(λ x x #hash()))
+(check-equal? (interpret '((λ (a : Bar) a) (x y))) '(x y))
+(check-equal? (interpret '((λ (a : Bat) (x y)) (λ (z : Bingus) z))) '(x y))
+(check-equal? (interpret '((λ (a : Baz) (a y)) x)) '(x y))