Qualified types that mostly work.

1 files changed, 693 insertions, 632 deletions

diff --git a/chickadee/graphics/seagull.scm b/chickadee/graphics/seagull.scm
index 078e4aa..1ae82bb 100644
--- a/chickadee/graphics/seagull.scm
+++ b/chickadee/graphics/seagull.scm
@@ -18,18 +18,25 @@
 ;;; Commentary:
 ;;
 ;; The Seagull shading language is a purely functional, statically
-;; typed, Scheme-like language that can be compiled to GLSL code.
+;; typed, Scheme-like language that can be compiled to GLSL code.  The
+;; reality of how GPUs work imposes some significant language
+;; restrictions, but they are restrictions anyone who writes shader
+;; code is already used to.
 ;;
-;; Notable features and restrictions:
+;; Features:
 ;; - Purely functional
 ;; - Vertex and fragment shader output
 ;; - Targets multiple GLSL versions
 ;; - Type inference
 ;; - Lexical scoping
-;; - First-order functions
-;; - Nested functions (but no closures!)
+;; - Nested functions
 ;; - Multiple return values
 ;;
+;; Limitations:
+;; - No first-class functions
+;; - No closures
+;; - No recursion
+;;
 ;;; Code:
 (define-module (chickadee graphics seagull)
   #:use-module (ice-9 exceptions)
@@ -47,6 +54,8 @@
 ;; TODO:
 ;; - Loops
 ;; - Shader stage linking
+;; - Transform for-all functions into overloads
+;; - User functions that use overloaded functions need to be overloaded themselves
 
 
 ;;;
@@ -763,14 +772,14 @@
 
 
 ;;;
-;;; Typed expressions
+;;; Type inference
 ;;;
 
-;; Typed expressions combine a Seagull expression with the data types
-;; that expression returns.  This section includes all the kinds of
-;; types an expression may have and various transformation procedures
-;; to manipulate them.  This will be used below to convert the mostly
-;; untyped Seagull program into a fully typed one.
+;; Walk the expression tree of a type annotated program and solve for
+;; all of the type variables using a variant of the Hindley-Milner
+;; type inference algorithm.  GLSL is a statically typed language, but
+;; thanks to type inference the user doesn't have to specify any types
+;; expect for shader inputs, outputs, and uniforms.
 
 ;; Primitive types:
 (define (primitive-type name)
@@ -825,6 +834,9 @@
 (define (fresh-type-variable)
   (type-variable (unique-type-variable-name)))
 
+(define (fresh-type-variables-for-list lst)
+  (map (lambda (_x) (fresh-type-variable)) lst))
+
 (define (type-variable? obj)
   (match obj
     (('tvar _) #t)
@@ -847,37 +859,43 @@
   (match type
     (('-> _ returns) returns)))
 
+;; Qualified types:
+;; (define (qualified-type type predicate)
+;;   `(qualified ,type ,predicate))
+
+;; (define (qualified-type? type)
+;;   (match type
+;;     (('qualified _ _) #t)
+;;     (_ #f)))
+
+;; (define (qualified-type-ref type)
+;;   (match type
+;;     (('qualified type* _) type*)))
+
+;; (define (qualified-type-predicate type)
+;;   (match type
+;;     (('qualified _ predicate) predicate)))
+
 ;; For all types:
-(define (for-all-type quantifiers type)
-  `(for-all ,quantifiers ,type))
+(define (for-all-type quantifiers type predicate)
+  `(for-all ,quantifiers ,type ,predicate))
 
 (define (for-all-type? obj)
   (match obj
-    (('for-all _ _) #t)
+    (('for-all _ _ _) #t)
     (_ #f)))
 
 (define (for-all-type-quantifiers type)
   (match type
-    (('for-all q _) q)))
+    (('for-all q _ _) q)))
 
 (define (for-all-type-ref type)
   (match type
-    (('for-all _ t) t)))
-
-;; Overload types:
-(define (overload-type . types)
-  (match types
-    (((? function-type?) ...)
-     `(overload ,types))))
-
-(define (overload-type? obj)
-  (match obj
-    (('overload _) #t)
-    (_ #f)))
+    (('for-all _ t _) t)))
 
-(define (overload-type-ref type)
+(define (for-all-type-predicate type)
   (match type
-    (('overload types) types)))
+    (('for-all _ _ p) p)))
 
 ;; Outputs type:
 (define outputs-type '(outputs))
@@ -891,7 +909,8 @@
   (or (primitive-type? obj)
       (type-variable? obj)
       (function-type? obj)
-      (overload-type? obj)))
+      ;; (qualified-type? obj)
+      (outputs-type? obj)))
 
 (define (apply-substitution-to-type type from to)
   (cond
@@ -908,11 +927,13 @@
      (map (lambda (return-type)
             (apply-substitution-to-type return-type from to))
           (function-type-returns type))))
-   ((overload-type? type)
-    (apply overload-type
-           (map (lambda (type)
-                  (apply-substitution-to-type type from to))
-                (overload-type-ref type))))
+   ;; ((qualified-type? type)
+   ;;  (qualified-type (apply-substitution-to-type
+   ;;                   (qualified-type-ref type) from to)
+   ;;                  (apply-substitution-to-predicate
+   ;;                   (qualified-type-predicate type) from to)))
+   ((for-all-type? type)
+    type)
    (else (error "invalid type" type))))
 
 (define (apply-substitutions-to-type type subs)
@@ -926,6 +947,53 @@
          (apply-substitutions-to-type type subs))
        types))
 
+(define (apply-substitution-to-env env from to)
+  (env-fold (lambda (name types env*)
+              (extend-env name
+                          (map (lambda (type)
+                                 (apply-substitution-to-type type from to))
+                               types)
+                          env*))
+            (empty-env)
+            env))
+
+(define (apply-substitutions-to-env env subs)
+  (env-fold (lambda (from to env*)
+              (apply-substitution-to-env env* from to))
+            env
+            subs))
+
+(define (apply-substitutions-to-texp t subs)
+  (texp (apply-substitutions-to-types (texp-types t) subs)
+        (texp-exp t)))
+
+(define (apply-substitution-to-predicate pred from to)
+  (match pred
+    (#t #t)
+    (('= a b)
+     `(= ,(apply-substitution-to-type a from to)
+         ,(apply-substitution-to-type b from to)))
+    (('and preds ...)
+     `(and ,@(map (lambda (pred)
+                    (apply-substitution-to-predicate pred from to))
+                  preds)))
+    (('or preds ...)
+     `(or ,@(map (lambda (pred)
+                    (apply-substitution-to-predicate pred from to))
+                 preds)))
+    (('when test consequent)
+     `(when ,(apply-substitution-to-predicate test from to)
+        ,(apply-substitution-to-predicate consequent from to)))
+    (('substitute a b)
+     `(substitute ,(apply-substitution-to-type a from to)
+                  ,(apply-substitution-to-type b from to)))))
+
+(define (apply-substitutions-to-predicate pred subs)
+  (env-fold (lambda (from to pred*)
+              (apply-substitution-to-predicate pred* from to))
+            pred
+            subs))
+
 ;; Typed expressions:
 (define (texp types exp)
   `(t ,types ,exp))
@@ -948,184 +1016,217 @@
     ((type) type)
     (_ (error "expected only 1 type" texp))))
 
-
-;;;
-;;; Type annotation
-;;;
+(define &seagull-type-error
+  (make-exception-type '&seagull-type-error &error '()))
+
+(define make-seagull-type-error
+  (record-constructor &seagull-type-error))
+
+(define (seagull-type-error msg args origin)
+  (raise-exception
+   (make-exception
+    (make-seagull-type-error)
+    (make-exception-with-origin origin)
+    (make-exception-with-message
+     (format #f "seagull type error: ~a" msg))
+    (make-exception-with-irritants args))))
+
+(define (occurs? a b)
+  (cond
+   ((and (type-variable? a) (type-variable? b))
+    (eq? a b))
+   ((and (type-variable? a) (function-type? b))
+    (or (occurs? a (function-type-parameters b))
+        (occurs? a (function-type-returns b))))
+   ((and (type? a) (list? b))
+    (any (lambda (b*) (occurs? a b*)) b))
+   (else #f)))
+
+(define (compose-substitutions a b)
+  (define b*
+    (map (match-lambda
+           ((from . to)
+            (cons from (apply-substitutions-to-type to a))))
+         b))
+  (define a*
+    (filter-map (match-lambda
+                  ((from . to)
+                   (if (assq-ref b* from)
+                       #f
+                       (cons from to))))
+                a))
+  (append a* b*))
 
-;; Convert untyped Seagull expressions into typed expressions with
-;; type variables representing all unknown types.  This annotated
-;; version of a Seagull program can then be passed to the type
-;; inference algorithm to solve for all of the variables.
-
-(define add/sub-type
-  (list (overload-type
-         (function-type (list int-type int-type)
-                        (list int-type))
-         (function-type (list float-type float-type)
-                        (list float-type))
-         (function-type (list vec2-type vec2-type)
-                        (list vec2-type))
-         (function-type (list vec3-type vec3-type)
-                        (list vec3-type))
-         (function-type (list vec4-type vec4-type)
-                        (list vec4-type))
-         (function-type (list mat3-type mat3-type)
-                        (list mat3-type))
-         (function-type (list mat4-type mat4-type)
-                        (list mat4-type)))))
-
-(define mul-type
-  (list (overload-type
-         (function-type (list int-type int-type)
-                        (list int-type))
-         (function-type (list float-type float-type)
-                        (list float-type))
-         (function-type (list vec2-type vec2-type)
-                        (list vec2-type))
-         (function-type (list vec2-type float-type)
-                        (list vec2-type))
-         (function-type (list float-type vec2-type)
-                        (list vec2-type))
-         (function-type (list vec3-type vec3-type)
-                        (list vec3-type))
-         (function-type (list vec3-type float-type)
-                        (list vec3-type))
-         (function-type (list float-type vec3-type)
-                        (list vec3-type))
-         (function-type (list vec4-type vec4-type)
-                        (list vec4-type))
-         (function-type (list vec4-type float-type)
-                        (list vec4-type))
-         (function-type (list float-type vec4-type)
-                        (list vec4-type))
-         (function-type (list mat3-type mat3-type)
-                        (list mat3-type))
-         (function-type (list mat3-type vec3-type)
-                        (list mat3-type))
-         (function-type (list vec3-type mat3-type)
-                        (list mat3-type))
-         (function-type (list mat4-type mat4-type)
-                        (list mat4-type))
-         (function-type (list mat4-type vec4-type)
-                        (list vec4-type))
-         (function-type (list vec4-type mat4-type)
-                        (list vec4-type)))))
-
-(define div-type
-  (list (overload-type
-         (function-type (list int-type int-type)
-                        (list int-type))
-         (function-type (list float-type float-type)
-                        (list float-type))
-         (function-type (list vec2-type vec2-type)
-                        (list vec2-type))
-         (function-type (list vec2-type float-type)
-                        (list vec2-type))
-         (function-type (list vec3-type vec3-type)
-                        (list vec3-type))
-         (function-type (list vec3-type float-type)
-                        (list vec3-type))
-         (function-type (list vec4-type vec4-type)
-                        (list vec4-type))
-         (function-type (list vec4-type float-type)
-                        (list vec4-type))
-         (function-type (list mat3-type float-type)
-                        (list mat3-type))
-         (function-type (list mat4-type float-type)
-                        (list mat4-type)))))
-
-(define comparison-type
-  (list (overload-type
-         (function-type (list int-type int-type)
-                        (list bool-type))
-         (function-type (list float-type float-type)
-                        (list bool-type)))))
-
-(define make-vec2-type
-  (list (function-type (list float-type float-type)
-                       (list vec2-type))))
-
-(define make-vec3-type
-  (list (overload-type
-         (function-type (list float-type float-type float-type)
-                        (list vec3-type))
-         (function-type (list vec2-type float-type)
-                        (list vec3-type))
-         (function-type (list float-type vec2-type)
-                        (list vec3-type)))))
-
-(define make-vec4-type
-  (list (overload-type
-         (function-type (list float-type float-type float-type float-type)
-                        (list vec4-type))
-         (function-type (list vec2-type float-type float-type)
-                        (list vec4-type))
-         (function-type (list float-type vec2-type float-type)
-                        (list vec4-type))
-         (function-type (list float-type float-type vec2-type)
-                        (list vec4-type))
-         (function-type (list vec3-type float-type)
-                        (list vec4-type))
-         (function-type (list float-type vec3-type)
-                        (list vec4-type)))))
-
-(define abs-type
-  (list (overload-type
-         (function-type (list int-type) (list int-type))
-         (function-type (list float-type) (list float-type)))))
-
-(define sqrt-type
-  (list (overload-type
-         (function-type (list int-type) (list int-type))
-         (function-type (list float-type) (list float-type)))))
-
-(define min/max-type
-  (list (overload-type
-         (function-type (list int-type int-type) (list int-type))
-         (function-type (list float-type float-type) (list float-type)))))
-
-(define trigonometry-type
-  (list (function-type (list float-type) (list float-type))))
-
-(define clamp/mix-type
-  (list (overload-type
-         (function-type (list int-type int-type int-type)
-                        (list int-type))
-         (function-type (list float-type float-type float-type)
-                        (list float-type)))))
+;; (define add/sub-type
+;;   (list (overload-type
+;;          (function-type (list int-type int-type)
+;;                         (list int-type))
+;;          (function-type (list float-type float-type)
+;;                         (list float-type))
+;;          (function-type (list vec2-type vec2-type)
+;;                         (list vec2-type))
+;;          (function-type (list vec3-type vec3-type)
+;;                         (list vec3-type))
+;;          (function-type (list vec4-type vec4-type)
+;;                         (list vec4-type))
+;;          (function-type (list mat3-type mat3-type)
+;;                         (list mat3-type))
+;;          (function-type (list mat4-type mat4-type)
+;;                         (list mat4-type)))))
+
+;; (define mul-type
+;;   (list (overload-type
+;;          (function-type (list int-type int-type)
+;;                         (list int-type))
+;;          (function-type (list float-type float-type)
+;;                         (list float-type))
+;;          (function-type (list vec2-type vec2-type)
+;;                         (list vec2-type))
+;;          (function-type (list vec2-type float-type)
+;;                         (list vec2-type))
+;;          (function-type (list float-type vec2-type)
+;;                         (list vec2-type))
+;;          (function-type (list vec3-type vec3-type)
+;;                         (list vec3-type))
+;;          (function-type (list vec3-type float-type)
+;;                         (list vec3-type))
+;;          (function-type (list float-type vec3-type)
+;;                         (list vec3-type))
+;;          (function-type (list vec4-type vec4-type)
+;;                         (list vec4-type))
+;;          (function-type (list vec4-type float-type)
+;;                         (list vec4-type))
+;;          (function-type (list float-type vec4-type)
+;;                         (list vec4-type))
+;;          (function-type (list mat3-type mat3-type)
+;;                         (list mat3-type))
+;;          (function-type (list mat3-type vec3-type)
+;;                         (list mat3-type))
+;;          (function-type (list vec3-type mat3-type)
+;;                         (list mat3-type))
+;;          (function-type (list mat4-type mat4-type)
+;;                         (list mat4-type))
+;;          (function-type (list mat4-type vec4-type)
+;;                         (list vec4-type))
+;;          (function-type (list vec4-type mat4-type)
+;;                         (list vec4-type)))))
+
+;; (define div-type
+;;   (list (overload-type
+;;          (function-type (list int-type int-type)
+;;                         (list int-type))
+;;          (function-type (list float-type float-type)
+;;                         (list float-type))
+;;          (function-type (list vec2-type vec2-type)
+;;                         (list vec2-type))
+;;          (function-type (list vec2-type float-type)
+;;                         (list vec2-type))
+;;          (function-type (list vec3-type vec3-type)
+;;                         (list vec3-type))
+;;          (function-type (list vec3-type float-type)
+;;                         (list vec3-type))
+;;          (function-type (list vec4-type vec4-type)
+;;                         (list vec4-type))
+;;          (function-type (list vec4-type float-type)
+;;                         (list vec4-type))
+;;          (function-type (list mat3-type float-type)
+;;                         (list mat3-type))
+;;          (function-type (list mat4-type float-type)
+;;                         (list mat4-type)))))
+
+;; (define comparison-type
+;;   (list (overload-type
+;;          (function-type (list int-type int-type)
+;;                         (list bool-type))
+;;          (function-type (list float-type float-type)
+;;                         (list bool-type)))))
+
+;; (define make-vec2-type
+;;   (list (function-type (list float-type float-type)
+;;                        (list vec2-type))))
+
+;; (define make-vec3-type
+;;   (list (overload-type
+;;          (function-type (list float-type float-type float-type)
+;;                         (list vec3-type))
+;;          (function-type (list vec2-type float-type)
+;;                         (list vec3-type))
+;;          (function-type (list float-type vec2-type)
+;;                         (list vec3-type)))))
+
+;; (define make-vec4-type
+;;   (list (overload-type
+;;          (function-type (list float-type float-type float-type float-type)
+;;                         (list vec4-type))
+;;          (function-type (list vec2-type float-type float-type)
+;;                         (list vec4-type))
+;;          (function-type (list float-type vec2-type float-type)
+;;                         (list vec4-type))
+;;          (function-type (list float-type float-type vec2-type)
+;;                         (list vec4-type))
+;;          (function-type (list vec3-type float-type)
+;;                         (list vec4-type))
+;;          (function-type (list float-type vec3-type)
+;;                         (list vec4-type)))))
+
+;; (define abs-type
+;;   (list (overload-type
+;;          (function-type (list int-type) (list int-type))
+;;          (function-type (list float-type) (list float-type)))))
+
+;; (define sqrt-type
+;;   (list (overload-type
+;;          (function-type (list int-type) (list int-type))
+;;          (function-type (list float-type) (list float-type)))))
+
+;; (define min/max-type
+;;   (list (overload-type
+;;          (function-type (list int-type int-type) (list int-type))
+;;          (function-type (list float-type float-type) (list float-type)))))
+
+;; (define trigonometry-type
+;;   (list (function-type (list float-type) (list float-type))))
+
+;; (define clamp/mix-type
+;;   (list (overload-type
+;;          (function-type (list int-type int-type int-type)
+;;                         (list int-type))
+;;          (function-type (list float-type float-type float-type)
+;;                         (list float-type)))))
 
 (define (top-level-type-env stage)
-  `((+ . ,add/sub-type)
-    (- . ,add/sub-type)
-    (* . ,mul-type)
-    (/ . ,div-type)
-    (= . ,comparison-type)
-    (< . ,comparison-type)
-    (<= . ,comparison-type)
-    (> . ,comparison-type)
-    (>= . ,comparison-type)
-    (vec2 . ,make-vec2-type)
-    (vec3 . ,make-vec3-type)
-    (vec4 . ,make-vec4-type)
-    (not ,(function-type (list bool-type) (list bool-type)))
-    (int->float ,(function-type (list int-type) (list float-type)))
-    (float->int ,(function-type (list float-type) (list int-type)))
-    (abs . ,abs-type)
-    (sqrt . ,sqrt-type)
-    (min . ,min/max-type)
-    (max . ,min/max-type)
-    (sin . ,trigonometry-type)
-    (cos . ,trigonometry-type)
-    (tan . ,trigonometry-type)
-    (clamp . ,clamp/mix-type)
-    (mix . ,clamp/mix-type)
-    ,@(case stage
-        ((vertex)
-         `((gl-position ,vec4-type)))
-        ((fragment)
-         `((texture-2d ,(function-type (list sampler-2d-type vec2-type)
-                                       (list vec4-type))))))))
+  '()
+  ;; `((+ . ,add/sub-type)
+  ;;   (- . ,add/sub-type)
+  ;;   (* . ,mul-type)
+  ;;   (/ . ,div-type)
+  ;;   (= . ,comparison-type)
+  ;;   (< . ,comparison-type)
+  ;;   (<= . ,comparison-type)
+  ;;   (> . ,comparison-type)
+  ;;   (>= . ,comparison-type)
+  ;;   (vec2 . ,make-vec2-type)
+  ;;   (vec3 . ,make-vec3-type)
+  ;;   (vec4 . ,make-vec4-type)
+  ;;   (not ,(function-type (list bool-type) (list bool-type)))
+  ;;   (int->float ,(function-type (list int-type) (list float-type)))
+  ;;   (float->int ,(function-type (list float-type) (list int-type)))
+  ;;   (abs . ,abs-type)
+  ;;   (sqrt . ,sqrt-type)
+  ;;   (min . ,min/max-type)
+  ;;   (max . ,min/max-type)
+  ;;   (sin . ,trigonometry-type)
+  ;;   (cos . ,trigonometry-type)
+  ;;   (tan . ,trigonometry-type)
+  ;;   (clamp . ,clamp/mix-type)
+  ;;   (mix . ,clamp/mix-type)
+  ;;   ,@(case stage
+  ;;       ((vertex)
+  ;;        `((gl-position ,vec4-type)))
+  ;;       ((fragment)
+  ;;        `((texture-2d ,(function-type (list sampler-2d-type vec2-type)
+  ;;                                      (list vec4-type)))))))
+  )
 
 (define (lookup-type name env)
   (let ((type (lookup name env)))
@@ -1175,13 +1276,40 @@
              '()
              env)))
 
-(define (generalize type env)
+(define (free-variables-in-predicate pred)
+  (match pred
+    (#t '())
+    (('= a b)
+     (append (free-variables-in-type a)
+             (free-variables-in-type b)))
+    (('and preds ...)
+     (append-map (lambda (pred)
+                   (free-variables-in-predicate pred))
+                 preds))
+    (('or preds ...)
+     (append-map (lambda (pred)
+                   (free-variables-in-predicate pred))
+                 preds))
+    (('when test consequent)
+     (append (free-variables-in-predicate test)
+             (free-variables-in-predicate consequent)))
+    (('substitute a b)
+     (append (free-variables-in-type a)
+             (free-variables-in-type b)))))
+
+;; Quantified variables:
+;; - Unused parameters
+;; - Parameters that appear free in the return type
+;; - Parameters that are used in overloaded primcalls
+(define (generalize type pred env)
   (if (function-type? type)
-      (match (difference (free-variables-in-type type)
+      (match (difference (delete-duplicates
+                          (append (free-variables-in-type type)
+                                  (free-variables-in-predicate pred)))
                          (free-variables-in-env env))
         (() type)
         ((quantifiers ...)
-         (for-all-type quantifiers type)))
+         (for-all-type quantifiers type pred)))
       type))
 
 (define (instantiate for-all)
@@ -1190,451 +1318,384 @@
             (extend-env var (fresh-type-variable) env))
           (empty-env)
           (for-all-type-quantifiers for-all)))
-  (apply-substitutions-to-type (for-all-type-ref for-all) subs))
-
-(define (fresh-type-variables-for-list lst)
-  (map (lambda (_x) (fresh-type-variable)) lst))
-
-(define (annotate:list exps env)
-  (map (lambda (exp) (annotate-exp exp env)) exps))
-
-(define (annotate:if predicate consequent alternate env)
-  (define consequent* (annotate-exp consequent env))
-  (texp (texp-types consequent*)
-        `(if ,(annotate-exp predicate env)
-             ,consequent*
-             ,(annotate-exp alternate env))))
-
-(define (annotate:let names exps body env)
-  (define exps* (annotate:list exps env))
-  (define exp-types (map texp-types exps*))
-  (define env* (fold extend-env env names exp-types))
-  (define body* (annotate-exp body env*))
-  (texp (texp-types body*)
-        `(let ,(map list names exps*) ,body*)))
-
-(define (annotate:lambda params body env)
-  ;; Each function parameter gets a fresh type variable.
-  (define param-types (fresh-type-variables-for-list params))
-  ;; The type environment is extended with the function parameters.
-  (define env*
-    (fold (lambda (param type env*)
-            (extend-env param (list type) env*))
-          env params param-types))
-  ;; The body is annotated in the new environment.
-  (define body* (annotate-exp body env*))
-  (texp (list (function-type param-types (texp-types body*)))
-        `(lambda ,params ,body*)))
-
-(define (annotate:values exps env)
-  (define exps* (annotate:list exps env))
-  (texp (map single-type exps*)
-        `(values ,@exps*)))
-
-(define (annotate:primitive-call operator args env)
-  ;; The type signature of primitive functions can be looked up
-  ;; directly in the environment.
-  (define operator-types (lookup-type operator env))
-  (define operator* (texp operator-types operator))
-  (define args* (annotate:list args env))
-  (texp (fresh-type-variables-for-list (list operator*))
-        `(primcall ,operator* ,@args*)))
-
-(define (annotate:call operator args env)
-  (define operator* (annotate-exp operator env))
-  (define args* (annotate:list args env))
-  (texp (fresh-type-variables-for-list
-         (function-type-returns
-          (single-type operator*)))
-        `(call ,operator* ,@args*)))
-
-(define* (annotate:top-level bindings body env #:optional (result '()))
-  (match bindings
-    (()
-     (let ((body* (annotate-exp body env)))
-       (texp (texp-types body*) `(top-level ,(reverse result) ,body*))))
-    ((('function name exp) . rest)
-     (define exp*
-       (let ((x (annotate-exp exp env)))
-         ;; Function types must be generalized so that functions like
-         ;; (lambda (x) x) can truly be applied to any type.
-         (texp (list (generalize (single-type x) env))
-               (texp-exp x))))
-     (define env* (extend-env name (texp-types exp*) env))
-     (define result* (cons `(function ,name ,exp*) result))
-     (annotate:top-level rest body env* result*))
-    ((((? top-level-qualifier? qualifier) type-name name) . rest)
-     (define env* (extend-env name (list (type-name->type type-name)) env))
-     (define result* (cons (list qualifier type-name name) result))
-     (annotate:top-level rest body env* result*))))
-
-(define (annotate:outputs names exps env)
-  (texp (list outputs-type)
-        `(outputs
-          ,@(map (lambda (name exp)
-                   (list (texp (lookup name env) name)
-                         (annotate-exp exp env)))
-                 names exps))))
-
-(define (annotate-exp exp env)
-  (match exp
-    ((? exact-integer?)
-     (texp (list int-type) exp))
-    ((? float?)
-     (texp (list float-type) exp))
-    ((? boolean?)
-     (texp (list bool-type) exp))
-    (('var var _)
-     (texp (lookup-type var env) exp))
-    (('if predicate consequent alternate)
-     (annotate:if predicate consequent alternate env))
-    (('let ((names exps) ...) body)
-     (annotate:let names exps body env))
-    (('lambda (params ...) body)
-     (annotate:lambda params body env))
-    (('values exps ...)
-     (annotate:values exps env))
-    (('primcall operator args ...)
-     (annotate:primitive-call operator args env))
-    (('call operator args ...)
-     (annotate:call operator args env))
-    (('outputs (names exps) ...)
-     (annotate:outputs names exps env))
-    (('top-level bindings body)
-     (annotate:top-level bindings body env))))
-
-(define (annotate-exp* exp stage)
-  (annotate-exp exp (top-level-type-env stage)))
-
-
-;;;
-;;; Type inference
-;;;
-
-;; Walk the expression tree of a type annotated program and solve for
-;; all of the type variables using a variant of the Hindley-Milner
-;; type inference algorithm.  GLSL is a statically typed language, but
-;; thanks to type inference the user doesn't have to specify any types
-;; expect for shader inputs, outputs, and uniforms.
-
-(define &seagull-type-error
-  (make-exception-type '&seagull-type-error &error '()))
-
-(define make-seagull-type-error
-  (record-constructor &seagull-type-error))
-
-(define (seagull-type-error msg args origin)
-  (raise-exception
-   (make-exception
-    (make-seagull-type-error)
-    (make-exception-with-origin origin)
-    (make-exception-with-message
-     (format #f "seagull type error: ~a" msg))
-    (make-exception-with-irritants args))))
-
-(define (occurs? a b)
+  (values
+   (apply-substitutions-to-type (for-all-type-ref for-all) subs)
+   (apply-substitutions-to-predicate (for-all-type-predicate for-all) subs)))
+
+(define (maybe-instantiate types)
+  (define types+preds
+    (map (lambda (type)
+           (if (for-all-type? type)
+               (call-with-values (lambda () (instantiate type)) list)
+               (list type #t)))
+         types))
+  (values (map first types+preds)
+          (reduce compose-predicates #t (map second types+preds))))
+
+;; (define (strip-qualifier type)
+;;   (if (qualified-type? type)
+;;       (qualified-type-ref type)
+;;       type))
+
+;; (define (strip-qualifiers types)
+;;   (map strip-qualifier types))
+
+;; (define (predicate-for-type type)
+;;   (if (qualified-type? type)
+;;       (qualified-type-predicate type)
+;;       #t))
+
+(define (compose-predicates a b)
   (cond
-   ((and (type-variable? a) (type-variable? b))
-    (eq? a b))
-   ((and (type-variable? a) (function-type? b))
-    (or (occurs? a (function-type-parameters b))
-        (occurs? a (function-type-returns b))))
-   ((and (type? a) (list? b))
-    (any (lambda (b*) (occurs? a b*)) b))
-   (else #f)))
-
-(define (compose-substitutions a b)
-  (define b*
-    (map (match-lambda
-           ((from . to)
-            (cons from (apply-substitutions-to-type to a))))
-         b))
-  (define a*
-    (filter-map (match-lambda
-                  ((from . to)
-                   (if (assq-ref b* from)
-                       #f
-                       (cons from to))))
-                a))
-  (append a* b*))
-
-(define unify-prompt-tag (make-prompt-tag 'unify))
-
-(define (call-with-unify-rollback thunk handler)
-  (call-with-prompt unify-prompt-tag
-    thunk
-    (lambda (k args)
-      (apply handler args))))
-
-(define (unify:fail . args)
-  (abort-to-prompt unify-prompt-tag args))
-
-(define (unify:primitives a b success)
+   ((and (eq? a #t) (eq? b #t))
+    #t)
+   ((eq? a #t)
+    b)
+   ((eq? b #t)
+    a)
+   (else
+    `(and ,a ,b))))
+
+(define (compose-predicates* preds)
+  (reduce (lambda (pred memo)
+            (compose-predicates pred memo))
+          #t
+          preds))
+
+(define (compose-predicates-for-types types)
+  (compose-predicates* (map predicate-for-type types)))
+
+;; Produces a simplified predicate and a new set of substitutions for
+;; predicates that have been satisfied and simplified to #t.
+(define (eval-predicate pred)
+  (match pred
+    (#t (values #t '()))
+    ((or ('= (? type-variable?) _)
+         ('= _ (? type-variable?)))
+     (values pred '()))
+    (('= a b)
+     (values (equal? a b) '()))
+    (('or preds ...)
+     (let loop ((preds preds))
+       (match preds
+         (() (values #f '()))
+         ((pred* . rest)
+          (define-values (new-pred subs)
+            (eval-predicate pred*))
+          (match new-pred
+            (#t (values #t subs))
+            (#f (eval-predicate `(or ,@rest)))
+            (_ (values `(or ,new-pred ,@rest) '())))))))
+    (('and preds ...)
+     (let loop ((preds preds))
+       (match preds
+         (() (values #t '()))
+         ((pred* . rest)
+          (define-values (new-pred subs)
+            (eval-predicate pred*))
+          (match new-pred
+            (#t
+             (let ()
+               (define-values (new-pred* subs*)
+                 (eval-predicate `(and ,@rest)))
+               (values new-pred* (compose-substitutions subs subs*))))
+            (#f (values #f '()))
+            (_ (values `(and ,new-pred ,@rest) '())))))))
+    (('when test consequent)
+     (define-values (new-test subs)
+       (eval-predicate test))
+     (match new-test
+       (#t
+        (let ()
+          (define-values (new-consequent subs*)
+            (eval-predicate consequent))
+          (values new-consequent (compose-substitutions subs subs*))))
+       (#f (values #f '()))
+       (_ (values `(when ,new-test ,consequent) '()))))
+    (('substitute a b)
+     (values #t (list (cons a b))))))
+
+(define (eval-predicate* pred subs)
+  (define-values (new-pred pred-subs)
+    (eval-predicate
+     (apply-substitutions-to-predicate pred subs)))
+  ;; TODO: Get information about *why* the predicate failed.
+  (unless new-pred
+    (error "predicate failure"))
+  (values new-pred (compose-substitutions subs pred-subs)))
+
+(define (unify:primitives a b)
   (if (equal? a b)
-      (success '())
-      (unify:fail "primitive type mismatch" a b)))
+      '()
+      (error "primitive type mismatch" a b)))
 
-(define (unify:variable a b success)
+(define (unify:variable a b)
   (cond
    ((eq? a b)
-    (success '()))
+    '())
    ((occurs? a b)
-    (unify:fail "type contains reference to itself" a b))
+    (error "type contains reference to itself" a b))
    (else
-    (success (list (cons a b))))))
-
-(define (unify:functions a b success)
-  (unify (function-type-parameters a)
-         (function-type-parameters b)
-         (lambda (sub0)
-           (unify (apply-substitutions-to-types (function-type-returns a)
-                                                sub0)
-                  (apply-substitutions-to-types (function-type-returns b)
-                                                sub0)
-                  (lambda (sub1)
-                    (success (compose-substitutions sub0 sub1)))))))
-
-(define (unify:overload a b success)
-  (define (try-unify functions)
-    (match functions
-      (()
-       (unify:fail "no matching overload" a b))
-      ((function . rest)
-       (call-with-unify-rollback
-        (lambda ()
-          (unify function b success))
-        (lambda _
-          (try-unify rest))))))
-  (try-unify (overload-type-ref a)))
-
-(define (unify:lists a rest-a b rest-b success)
-  (unify a b
-         (lambda (sub0)
-           (unify (apply-substitutions-to-types rest-a sub0)
-                  (apply-substitutions-to-types rest-b sub0)
-                  (lambda (sub1)
-                    (success (compose-substitutions sub0 sub1)))))))
-
-(define (unify a b success)
+    (list (cons a b)))))
+
+(define (unify:functions a b)
+  (define param-subs
+    (unify (function-type-parameters a)
+           (function-type-parameters b)))
+  (define return-subs
+    (unify (apply-substitutions-to-types (function-type-returns a)
+                                         param-subs)
+           (apply-substitutions-to-types (function-type-returns b)
+                                         param-subs)))
+  (compose-substitutions param-subs return-subs))
+
+(define (unify:lists a rest-a b rest-b)
+  (define sub-first (unify a b))
+  (define sub-rest
+    (unify (apply-substitutions-to-types rest-a sub-first)
+           (apply-substitutions-to-types rest-b sub-first)))
+  (compose-substitutions sub-first sub-rest))
+
+(define (unify a b)
   (match (list a b)
     (((? primitive-type? a) (? primitive-type? b))
-     (unify:primitives a b success))
+     (unify:primitives a b))
     ((or ((? type-variable? a) b)
          (b (? type-variable? a)))
-     (unify:variable a b success))
+     (unify:variable a b))
     (((? function-type? a) (? function-type? b))
-     (unify:functions a b success))
-    ((a (? overload-type? b))
-     (unify:overload b a success))
+     (unify:functions a b))
     (((? outputs-type?) (? outputs-type?))
-     (success '()))
+     '())
     ((() ())
-     (success '()))
+     '())
     (((a rest-a ...) (b rest-b ...))
-     (unify:lists a rest-a b rest-b success))
+     (unify:lists a rest-a b rest-b))
     (_
-     (unify:fail "type mismatch" a b))))
-
-(define (infer:list exps subs success)
-  (match exps
-    (() (success subs))
-    ((exp . rest)
-     (infer exp
-            subs
-            (lambda (sub0)
-              (infer:list rest
-                          sub0
-                          (lambda (sub1)
-                            (success
-                             (compose-substitutions sub0 sub1)))))))))
-
-(define (infer:if types predicate consequent alternate subs success)
-  (infer predicate
-         subs
-         (lambda (sub0)
-           (unify (single-type predicate)
-                  bool-type
-                  (lambda (sub1)
-                    (define sub2 (compose-substitutions sub0 sub1))
-                    (infer consequent
-                           sub2
-                           (lambda (sub3)
-                             (infer alternate
-                                    sub3
-                                    (lambda (sub4)
-                                      (unify (apply-substitutions-to-types
-                                              (texp-types consequent)
-                                              sub4)
-                                             (apply-substitutions-to-types
-                                              (texp-types alternate)
-                                              sub4)
-                                             (lambda (sub5)
-                                               (success
-                                                (compose-substitutions
-                                                 sub4 sub5)))))))))))))
-
-(define (infer:lambda type body subs success)
-  (define type*
-    (if (for-all-type? type)
-        (for-all-type-ref type)
-        type))
-  (infer body
-         subs
-         (lambda (sub0)
-           (unify (apply-substitutions-to-types (texp-types body) sub0)
-                  (function-type-returns type*)
-                  (lambda (sub1)
-                    (success
-                     (compose-substitutions sub0 sub1)))))))
-
-(define (infer:values types exps subs success)
-  (infer:list exps subs success))
-
-(define (infer:call types operator args subs success)
-  (infer operator
-         subs
-         (lambda (sub0)
-           (infer:list
-            args
-            sub0
-            (lambda (sub1)
-              ;; Check if function call has the proper number of
-              ;; arguments.
-              (let* ((k (length args))
-                     (l (length (function-type-parameters
-                                 (single-type operator)))))
-                (unless (= k l)
-                  (seagull-type-error
-                   (format #f "expected ~a arguments, got ~a" l k)
-                   '()
-                   infer:call)))
-              (unify (apply-substitutions-to-type
-                      (function-type (map single-type args)
-                                     types)
-                      sub1)
-                     (apply-substitutions-to-type
-                      (single-type operator)
-                      sub1)
-                     (lambda (sub2)
-                       (success (compose-substitutions sub1 sub2)))))))))
-
-(define (infer:primcall types operator args subs success)
-  (infer:list
-   args
-   subs
-   (lambda (sub0)
-     (unify (apply-substitutions-to-type
-             (function-type (map single-type args)
-                            types)
-             sub0)
-            (apply-substitutions-to-type
-             (single-type operator)
-             sub0)
-            (lambda (sub1)
-              (success
-               (compose-substitutions sub0 sub1)))))))
-
-(define (infer:let types names exps body subs success)
-  (infer:list
-   exps
-   subs
-   (lambda (sub0)
-     (infer body
-            sub0
-            (lambda (sub1)
-              (unify (apply-substitutions-to-types types sub1)
-                     (apply-substitutions-to-types (texp-types body) sub1)
-                     (lambda (sub2)
-                       (success
-                        (compose-substitutions sub1 sub2)))))))))
-
-(define (infer:top-level types bindings body subs success)
-  (define exps
-    (filter-map (match-lambda
-                  (('function _ exp) exp)
-                  (_ #f))
-                bindings))
-  (infer:list
-   exps
-   subs
-   (lambda (sub0)
-     (infer body
-            sub0
-            (lambda (sub1)
-              (unify (apply-substitutions-to-types types sub1)
-                     (apply-substitutions-to-types (texp-types body) sub1)
-                     (lambda (sub2)
-                       (success
-                        (compose-substitutions sub1 sub2)))))))))
-
-(define (infer:outputs names exps subs success)
-  (define output-types (map single-type names))
-  (infer:list
-   exps
-   subs
-   (lambda (sub0)
-     (unify output-types
-            (apply-substitutions-to-types (map single-type exps) sub0)
-            (lambda (sub1)
-              (success
-               (compose-substitutions sub0 sub1)))))))
-
-(define (infer exp subs success)
+     (error "type mismatch" a b))))
+
+(define (infer:immediate x)
+  (values (texp (list (cond
+                       ((exact-integer? x)
+                        int-type)
+                       ((float? x)
+                        float-type)
+                       ((boolean? x)
+                        bool-type)))
+                x)
+          '()
+          #t))
+
+(define (infer:variable name env)
+  (define-values (types pred)
+    (maybe-instantiate (lookup-type name env)))
+  (values (texp types name)
+          '()
+          pred))
+
+(define (infer:list exps env)
+  (let loop ((exps exps)
+             (texps '())
+             (subs '())
+             (pred #t))
+    (match exps
+      (()
+       (values (reverse texps) subs pred))
+      ((exp . rest)
+       (define-values (texp subs* pred*)
+         (infer-exp exp env))
+       (define-values (new-pred combined-subs)
+         (eval-predicate* (compose-predicates pred pred*)
+                          (compose-substitutions subs subs*)))
+       (loop rest
+             (cons texp texps)
+             combined-subs
+             new-pred)))))
+
+(define (infer:if predicate consequent alternate env)
+  ;; Infer predicate types and unify it with the boolean type.
+  (define-values (predicate-texp predicate-subs predicate-pred)
+    (infer-exp predicate env))
+  (define predicate-unify-subs
+    (unify (texp-types predicate-texp) (list bool-type)))
+  ;; Combine the substitutions and apply them to the environment.
+  (define combined-subs-0
+    (compose-substitutions predicate-subs predicate-unify-subs))
+  (define env0
+    (apply-substitutions-to-env env combined-subs-0))
+  ;; Infer consequent and alternate types and unify them against each
+  ;; other.  Each branch of an 'if' should have the same type.
+  (define-values (consequent-texp consequent-subs consequent-pred)
+    (infer-exp consequent env0))
+  (define combined-subs-1
+    (compose-substitutions combined-subs-0 consequent-subs))
+  (define env1
+    (apply-substitutions-to-env env0 consequent-subs))
+  (define-values (alternate-texp alternate-subs alternate-pred)
+    (infer-exp alternate env1))
+  (define combined-subs-2
+    (compose-substitutions combined-subs-1 alternate-subs))
+  ;; Eval combined predicate.
+  (define-values (pred combined-subs-3)
+    (eval-predicate* (compose-predicates predicate-pred
+                                         (compose-predicates consequent-pred
+                                                             alternate-pred))
+                     combined-subs-2))
+  ;; ;; Apply final set of substitutions to the types of both branches.
+  (define consequent-texp*
+    (apply-substitutions-to-texp consequent-texp combined-subs-3))
+  (define alternate-texp*
+    (apply-substitutions-to-texp alternate-texp combined-subs-3))
+  (values (texp (texp-types consequent-texp)
+                `(if ,predicate-texp ,consequent-texp ,alternate-texp))
+          combined-subs-3
+          pred))
+
+(define (infer:lambda params body env)
+  ;; Each function parameter gets a fresh type variable.
+  (define param-types (fresh-type-variables-for-list params))
+  ;; The type environment is extended with the function parameters.
+  (define env*
+    (fold (lambda (param type env*)
+            (extend-env param (list type) env*))
+          env params param-types))
+  (define-values (body* body-subs body-pred)
+    (infer-exp body env*))
+  (define-values (pred subs)
+    (eval-predicate* body-pred body-subs))
+  (values (texp (list (generalize
+                       (function-type (apply-substitutions-to-types param-types
+                                                                    body-subs)
+                                      (texp-types body*))
+                       pred env))
+                `(lambda ,params ,body*))
+          subs #t))
+
+(define (infer:primitive-call operator args env)
+  ;; The type signature of primitive functions can be looked up
+  ;; directly in the environment.  Primitive functions may be
+  ;; overloaded and need to be instantiated with fresh type variables.
+  (define-values (types operator-pred)
+    (maybe-instantiate (lookup-type operator env)))
+  (define operator-type
+    (match types
+      ((type) type)))
+  ;; Infer the arguments.
+  (define-values (args* arg-subs arg-pred)
+    (infer:list args env))
+  ;; Generate fresh type variables to unify against the return types
+  ;; of the operator.
+  (define return-vars
+    (fresh-type-variables-for-list (function-type-returns operator-type)))
+  (define call-subs
+    (unify operator-type
+           (function-type (map single-type args*)
+                          return-vars)))
+  ;; Apply substitutions to the predicate and then eval it, producing
+  ;; a simplified predicate and a set of substitutions.
+  (define-values (pred combined-subs)
+    (eval-predicate* (compose-predicates operator-pred arg-pred)
+                     (compose-substitutions arg-subs call-subs)))
+  (values (texp (apply-substitutions-to-types return-vars combined-subs)
+                `(primcall ,operator
+                           ,@(map (lambda (arg)
+                                    (apply-substitutions-to-texp arg
+                                                                 combined-subs))
+                                  args*)))
+          combined-subs
+          pred))
+
+(define (infer:call operator args env)
+  ;; The type signature of primitive functions can be looked up
+  ;; directly in the environment.
+  (define-values (operator* operator-subs operator-pred)
+    (infer-exp operator env))
+  (define env*
+    (apply-substitutions-to-env env operator-subs))
+  ;; Infer the arguments.
+  (define-values (args* arg-subs arg-pred)
+    (infer:list args env*))
+  (define combined-subs-0
+    (compose-substitutions operator-subs arg-subs))
+  ;; Generate fresh type variables to unify against the return types
+  ;; of the operator.
+  (define operator-type (single-type operator*))
+  (define return-vars
+    (fresh-type-variables-for-list
+     (function-type-returns operator-type)))
+  (define call-subs
+    (unify (apply-substitutions-to-type operator-type combined-subs-0)
+           (function-type (apply-substitutions-to-types (map single-type args*)
+                                                        combined-subs-0)
+                          return-vars)))
+  ;; Eval predicate.
+  (define-values (pred combined-subs)
+    (eval-predicate* (compose-predicates operator-pred
+                                         arg-pred)
+                     (compose-substitutions combined-subs-0 call-subs)))
+  (values (texp (apply-substitutions-to-types return-vars combined-subs)
+                `(call ,(apply-substitutions-to-texp operator* combined-subs)
+                       ,@(map (lambda (arg)
+                                (apply-substitutions-to-texp arg
+                                                             combined-subs))
+                              args*)))
+          combined-subs
+          pred))
+
+(define (infer:let names exps body env)
+  (define-values (exps* exp-subs exp-pred)
+    (infer:list exps env))
+  (define exp-types (map texp-types exps*))
+  (define env*
+    (fold extend-env
+          (apply-substitutions-to-env env exp-subs)
+          names
+          exp-types))
+  (define-values (body* body-subs body-pred)
+    (infer-exp body env*))
+  (define-values (pred combined-subs)
+    (eval-predicate* (compose-predicates exp-pred body-pred)
+                     (compose-substitutions exp-subs body-subs)))
+  (values (texp (texp-types body*)
+                `(let ,(map list names exps*) ,body*))
+          combined-subs
+          pred))
+
+;; Inference returns 3 values:
+;; - a typed expression
+;; - a list of substitutions
+;; - a type predicate
+(define (infer-exp exp env)
   (match exp
-    (('t types (or (? immediate?) ('var _ _)))
-     (success subs))
-    (('t types ('if predicate consequent alternate))
-     (infer:if types predicate consequent alternate subs success))
-    (('t types ('let ((names exps) ...) body))
-     (infer:let types names exps body subs success))
-    (('t (type) ('lambda (params ...) body))
-     (infer:lambda type body subs success))
-    (('t types ('values exps ...))
-     (infer:values types exps subs success))
-    (('t types ('primcall operator args ...))
-     (infer:primcall types operator args subs success))
-    (('t types ('call operator args ...))
-     (infer:call types operator args subs success))
-    (('t _ ('outputs (names exps) ...))
-     (infer:outputs names exps subs success))
-    (('t types ('top-level bindings body))
-     (infer:top-level types bindings body subs success))
+    ((? immediate?)
+     (infer:immediate exp))
+    ((? symbol?)
+     (infer:variable exp env))
+    (('if predicate consequent alternate)
+     (infer:if predicate consequent alternate env))
+    (('let ((names exps) ...) body)
+     (infer:let names exps body env))
+    (('lambda (params ...) body)
+     (infer:lambda params body env))
+    ;; (('values exps ...)
+    ;;  (infer:values exps env))
+    (('primcall operator args ...)
+     (infer:primitive-call operator args env))
+    (('call operator args ...)
+     (infer:call operator args env))
+    ;; (('outputs (names exps) ...)
+    ;;  (infer:outputs names exps env))
+    ;; (('top-level bindings body)
+    ;;  (infer:top-level bindings body env))
     (_ (error "unknown form" exp))))
 
-(define (resolve:type-variable var env)
-  (let ((type (assq-ref env var)))
-    (if type
-        (resolve type env)
-        var)))
-
-;; TODO: If there are still quantified type variables, scan the entire
-;; program for calls to the function and build an intersection type.
-(define (resolve:for-all type env)
-  (let ((quantifiers (filter type-variable?
-                             (resolve (for-all-type-quantifiers type) env)))
-        (ref (resolve (for-all-type-ref type) env)))
-    (if (null? quantifiers) ref (for-all-type quantifiers ref))))
-
-(define (resolve:list exps env)
-  (map (lambda (exp) (resolve exp env)) exps))
-
-(define (resolve exp env)
-  (match exp
-    ((? type-variable?)
-     (resolve:type-variable exp env))
-    ((? for-all-type?)
-     (resolve:for-all exp env))
-    ((exps ...)
-     (resolve:list exps env))
-    (_ exp)))
-
 ;; TODO: Add some kind of context object that is threaded through the
 ;; inference process so that when a type error occurs we can show the
 ;; expression that caused it.
 (define (infer-types exp stage)
   (call-with-unify-rollback
    (lambda ()
-     (let ((annotated (annotate-exp* exp stage)))
+     (let ((annotated (pk 'annotated (annotate-exp* exp stage))))
        (infer annotated
               '()
               (lambda (subs)