Rewrite type predicates.

1 files changed, 304 insertions, 335 deletions

diff --git a/chickadee/graphics/seagull.scm b/chickadee/graphics/seagull.scm
index 4f88973..fd5be5b 100644
--- a/chickadee/graphics/seagull.scm
+++ b/chickadee/graphics/seagull.scm
@@ -57,6 +57,7 @@
   #:use-module ((rnrs base) #:select (mod))
   #:use-module (srfi srfi-1)
   #:use-module (srfi srfi-9)
+  #:use-module (srfi srfi-9 gnu)
   #:use-module (srfi srfi-11)
   #:use-module (system repl command)
   #:use-module (system repl common)
@@ -333,30 +334,248 @@
   (match type
     (('qualified _ pred) pred)))
 
-(define (predicate:and . preds)
-  ;; Combine inner 'and' predicates and remove #t predicates.
-  (define preds*
-    (let loop ((preds preds))
-      (match preds
-        (() '())
-        ((('and sub-preds ...) . rest)
-         (append sub-preds (loop rest)))
-        ((#t . rest)
-         (loop rest))
-        ((pred . rest)
-         (cons pred (loop rest))))))
-  (match preds*
-    (() #t)
-    ((pred) pred)
-    (_ `(and ,@preds*))))
+(define (type? obj)
+  (or (primitive-type? obj)
+      (variable-type? obj)
+      (function-type? obj)
+      (struct-type? obj)
+      (outputs-type? obj)))
 
+;; Type predicates represent additional constraints associated with a
+;; typed expression.  They are used to implement ad-hoc polymorphism.
+;; For example, a function with signature (-> (a a) (a)) could specify
+;; the following predicate to allow either ints or floats as arguments:
+;;
+;;   (let ((a (variable-type 'T0)))
+;;     (predicate:or (predicate:= a type:int)
+;;                   (predicate:= a type:float)
+(define-record-type <type-predicate>
+  (make-type-predicate exp evaluator substituter)
+  type-predicate?
+  (exp type-predicate-exp) ; symbolic representation
+  (evaluator type-predicate-evaluator) ; eval procedure
+  (substituter type-predicate-substituter)) ; substitute procedure
+
+(define (print-type-predicate pred port)
+  (format port "#<type-predicate ~a>" (type-predicate-exp pred)))
+
+(set-record-type-printer! <type-predicate> print-type-predicate)
+
+(define predicate:succeed
+  (make-type-predicate
+   #t
+   (lambda () (values predicate:succeed '()))
+   (lambda (from to) predicate:succeed)))
+
+(define (predicate:succeed? pred)
+  (eq? pred predicate:succeed))
+
+(define predicate:fail
+  (make-type-predicate
+   #f
+   (lambda () (values predicate:fail '()))
+   (lambda (from to) predicate:fail)))
+
+(define (predicate:fail? pred)
+  (eq? pred predicate:fail))
+
+(define (predicate:= a b)
+  (cond
+   ((or (variable-type? a)
+        (variable-type? b))
+    (make-type-predicate
+     `(= ,a ,b)
+     (lambda ()
+       (values (predicate:= a b) '()))
+     (lambda (from to)
+       (predicate:= (apply-substitution-to-type a from to)
+                    (apply-substitution-to-type b from to)))))
+   ((equal? a b)
+    predicate:succeed)
+   (else
+    predicate:fail)))
+
+(define (predicate:substitute a b)
+  (make-type-predicate
+   `(substitute ,a ,b)
+   (lambda ()
+     (values predicate:succeed (list (cons a b))))
+   (lambda (from to)
+     (predicate:substitute (apply-substitution-to-type a from to)
+                           (apply-substitution-to-type b from to)))))
+
+(define (predicate:struct-field struct field field-var)
+  (cond
+   ((struct-type? struct)
+    (let ((field-type (struct-type-ref struct field)))
+      (if field-type
+          (predicate:substitute field-var field-type)
+          predicate:fail)))
+   ((variable-type? struct)
+    (make-type-predicate
+     `(struct-field ,struct ,field ,field-var)
+     (lambda ()
+       (values (predicate:struct-field struct field field-var) '()))
+     (lambda (from to)
+       (predicate:struct-field
+        (apply-substitution-to-type struct from to)
+        field
+        (apply-substitution-to-type field-var from to)))))
+   (else predicate:fail)))
+
+(define (predicate:array-element array element-var)
+  (cond
+   ((array-type? array)
+    (predicate:substitute element-var (array-type-ref array)))
+   ((variable-type? array)
+    (make-type-predicate
+     `(array-element ,array ,element-var)
+     (lambda ()
+       (values (predicate:array-element array element-var) '()))
+     (lambda (from to)
+       (predicate:array-element
+        (apply-substitution-to-type array from to)
+        (apply-substitution-to-type element-var from to)))))
+   (else predicate:fail)))
+
+;; All the predicates must succeed, but unlike 'predicate:and', they
+;; can succeed independently of one another.
+(define (predicate:compose pred . rest)
+  (if (null? rest)
+      pred
+      (let ((other (apply predicate:compose rest)))
+        (cond
+         ((and (predicate:succeed? pred) (predicate:succeed? other))
+          predicate:succeed)
+         ((predicate:succeed? pred)
+          other)
+         ((predicate:succeed? other)
+          pred)
+         (else
+          (make-type-predicate
+           `(compose ,(type-predicate-exp pred)
+                     ,(type-predicate-exp other))
+           (lambda ()
+             (let-values (((pred* pred-subs) (eval-predicate pred)))
+               (cond
+                ;; Left succeeds, now check the right.
+                ((predicate:succeed? pred*)
+                 (let-values (((other* other-subs) (eval-predicate other)))
+                   (cond
+                    ;; Right succeeds, the composition is a success.
+                    ((predicate:succeed? other*)
+                     (values predicate:succeed
+                             (compose-substitutions pred-subs other-subs)))
+                    ;; Right fails, so the composition fails.
+                    ((predicate:fail? other*)
+                     (values predicate:fail '()))
+                    ;; Also inconclusive, return the same composition.
+                    (else
+                     (values other pred-subs)))))
+                ;; Left fails, so the composition fails.
+                ((predicate:fail? pred*)
+                 (values predicate:fail '()))
+                ;; Left predicate is inconclusive, try the right.
+                (else
+                 (let-values (((other* other-subs) (eval-predicate other)))
+                   (cond
+                    ;; Right succeeds, return the left.
+                    ((predicate:succeed? other*)
+                     (values pred other-subs))
+                    ;; Right fails, so the composition fails.
+                    ((predicate:fail? other*)
+                     (values predicate:fail '()))
+                    ;; Also inconclusive, return the same composition.
+                    (else
+                     (values (predicate:compose pred other) '()))))))))
+           (lambda (from to)
+             (predicate:compose
+              (apply-substitution-to-predicate pred from to)
+              (apply-substitution-to-predicate other from to)))))))))
+
+;; The 'and' predicate succeeds if and when all the given predicates
+;; succeed.
+(define (predicate:and . preds)
+  (match (remove predicate:succeed? preds)
+    (()
+     predicate:succeed)
+    ((pred)
+     pred)
+    ((or ((? predicate:fail?) _)
+         (_ (? predicate:fail?)))
+     predicate:fail)
+    ((a b)
+     (make-type-predicate
+      `(and ,(type-predicate-exp a) ,(type-predicate-exp b))
+      (lambda ()
+        (let-values (((a* a-subs) (eval-predicate a)))
+          (cond
+           ;; Left succeeds, now try the right.
+           ((predicate:succeed? a*)
+            (let-values (((b* b-subs) (eval-predicate b)))
+              (cond
+               ;; Right succeeds, so the 'and' succeeds.
+               ((predicate:succeed? b*)
+                (values predicate:succeed
+                        (compose-substitutions a-subs b-subs)))
+               ;; Right fails, so the 'and' fails.
+               ((predicate:fail? b*)
+                (values predicate:fail '()))
+               ;; Right is inconclusive, so return the same 'and'.
+               (else
+                (predicate:and a b)))))
+           ;; Left fails, so the 'and' fails.
+           ((predicate:fail? a*)
+            (values predicate:fail '()))
+           ;; Left is inconclusive, so return the same 'and'.
+           (else
+            (values (predicate:and a b) '())))))
+      (lambda (from to)
+        (predicate:and (apply-substitution-to-predicate a from to)
+                       (apply-substitution-to-predicate b from to)))))
+    ((a . rest)
+     (predicate:and a (apply predicate:and rest)))))
+
+;; The 'or' predicate succeeds if and when any given predicate
+;; succeeds.
 (define (predicate:or . preds)
-  (match preds
-    (() #f)
-    ((pred) pred)
-    ((pred ('or sub-preds ...))
-     `(or ,pred ,@sub-preds))
-    (_ `(or ,@preds))))
+  (match (remove predicate:fail? preds)
+    (()
+     predicate:fail)
+    ((pred)
+     pred)
+    ((or ((? predicate:succeed?) _)
+         (_ (? predicate:succeed?)))
+     predicate:succeed)
+    ((a b)
+     (make-type-predicate
+      `(or ,(type-predicate-exp a) ,(type-predicate-exp b))
+      (lambda ()
+        (let-values (((a* a-subs) (eval-predicate a)))
+          (cond
+           ;; Left succeeds, so the 'or' succeeds.
+           ((predicate:succeed? a*)
+            (values predicate:succeed a-subs))
+           ;; Left fails, so remove the 'or' and eval the right.
+           ((predicate:fail? a*)
+            (eval-predicate b))
+           ;; Left is inconclusive, check the right.
+           (else
+            (let-values (((b* b-subs) (eval-predicate b)))
+              (cond
+               ;; Right succeeds, so the 'or' succeeds.
+               ((predicate:succeed? b*)
+                (values predicate:succeed b-subs))
+               ;; Right fails, so remove the 'or' and return the left.
+               ((predicate:fail? b*)
+                (values a '()))
+               (else
+                (values (predicate:or a b) '()))))))))
+      (lambda (from to)
+        (predicate:or (apply-substitution-to-predicate a from to)
+                      (apply-substitution-to-predicate b from to)))))
+    ((a . rest)
+     (predicate:or a (apply predicate:or rest)))))
 
 (define (predicate:any var . types)
   (apply predicate:or
@@ -364,44 +583,31 @@
                 (predicate:= var type))
               types)))
 
-(define (predicate:list . preds)
-  (define preds*
-    (let loop ((preds preds))
-      (match preds
-        (() '())
-        ((('list sub-preds ...) . rest)
-         (append sub-preds (loop rest)))
-        ((pred . rest)
-         (cons pred (loop rest))))))
-  (match preds*
-    ((pred) pred)
-    (_ `(list ,@preds*))))
-
-(define (predicate:= a b)
-  `(= ,a ,b))
-
-(define (predicate:substitute from to)
-  `(substitute ,from ,to))
-
-(define (predicate:substitutes subs)
-  (apply predicate:and
-         (map (match-lambda
-                ((from . to)
-                 (predicate:substitute from to)))
-              subs)))
+(define (apply-substitution-to-predicate pred from to)
+  ((type-predicate-substituter pred) from to))
 
-(define (predicate:struct-field struct field var)
-  `(struct-field ,struct ,field ,var))
+(define (apply-substitutions-to-predicate pred subs)
+  (env-fold (lambda (from to pred*)
+              (apply-substitution-to-predicate pred* from to))
+            pred
+            subs))
 
-(define (predicate:array-element array var)
-  `(array-element ,array ,var))
+(define (eval-predicate pred)
+  ((type-predicate-evaluator pred)))
 
-(define (type? obj)
-  (or (primitive-type? obj)
-      (variable-type? obj)
-      (function-type? obj)
-      (struct-type? obj)
-      (outputs-type? obj)))
+(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
+    (seagull-type-error "type predicate failed" (list pred) eval-predicate*))
+  ;; Recursively evaluate the predicate, applying the substitutions
+  ;; generated by the last evaluation, until it cannot be simplified
+  ;; any further.
+  (if (null? pred-subs)
+      (values new-pred subs)
+      (eval-predicate* new-pred (compose-substitutions subs pred-subs))))
 
 ;; Built-in types:
 (define type:int (primitive-type 'int))
@@ -591,7 +797,7 @@
           (list var ...)
           (qualified-type
            (function-type (list args ...) (list returns ...))
-           (predicate:list
+           (predicate:compose
             (predicate:any var types ...) ...))))))))
 
 (define-syntax-rule (a+b->c (ta tb tc) ...)
@@ -1940,243 +2146,6 @@
                 a))
   (append a* b*))
 
-(define (compose-predicates a b)
-  (cond
-   ((and (eq? a #t) (eq? b #t))
-    #t)
-   ((eq? a #t)
-    b)
-   ((eq? b #t)
-    a)
-   (else
-    (predicate:list a b))))
-
-(define (compose-predicates* preds)
-  (reduce (lambda (pred memo)
-            (compose-predicates pred memo))
-          #t
-          preds))
-
-(define (apply-substitution-to-predicate pred from to)
-  (match pred
-    (#t #t)
-    (#f #f)
-    (('= 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)))
-    (('list preds ...)
-     `(list ,@(map (lambda (pred)
-                     (apply-substitution-to-predicate pred from to))
-                   preds)))
-    (('substitute a b)
-     `(substitute ,(apply-substitution-to-type a from to)
-                  ,(apply-substitution-to-type b from to)))
-    (('struct-field struct field var)
-     `(struct-field ,(apply-substitution-to-type struct from to)
-                    ,field
-                    ,(apply-substitution-to-type var from to)))
-    (('array-element array var)
-     `(array-element ,(apply-substitution-to-type array from to)
-                     ,(apply-substitution-to-type var from to)))))
-
-(define (apply-substitutions-to-predicate pred subs)
-  (env-fold (lambda (from to pred*)
-              (apply-substitution-to-predicate pred* from to))
-            pred
-            subs))
-
-;; Produces a simplified predicate and a new set of substitutions for
-;; predicates that have been satisfied and simplified to #t.  It's a
-;; bit of a weird process since we're dealing with partial evaluation,
-;; simplification, and constraint generation at the same time, so
-;; there are lots of comments explaining what the heck is going on.
-(define (eval-predicate pred)
-  (match pred
-    ;; #t is the simplest predicate.  It's always successful and
-    ;; results in no substitutions.
-    (#t (values #t '()))
-    (#f (values #f '()))
-    ;; '=' asserts that 'a' must equal 'b'.  If either is a type
-    ;; variable, then we don't have enough information to determine
-    ;; success or failure.
-    ((or ('= (? variable-type?) _)
-         ('= _ (? variable-type?)))
-     (values pred '()))
-    ;; Neither argument is a type variable, so we can get an answer.
-    (('= a b)
-     (values (equal? a b) '()))
-    ;; An 'or' succeeds if any of the predicates within succeed.
-    (('or preds ...)
-     (match preds
-       ;; No clause succeeded or the 'or' had no clauses to begin
-       ;; with.  Either way, the 'or' fails.
-       (() (values #f '()))
-       ((pred* . rest)
-        (define-values (new-pred subs)
-          (eval-predicate pred*))
-        (match new-pred
-          ;; This clause succeeded, so the entire 'or' can be
-          ;; reduced to #t.
-          (#t (values #t subs))
-          ;; This clause failed, so simplify the 'or' to just the
-          ;; rest of the clauses.
-          (#f (eval-predicate (apply predicate:or rest)))
-          ;; There isn't enough information to determine if this
-          ;; clause will succeed or fail.  So, we evaluate the rest
-          ;; of the 'or' clauses and compose the result with this
-          ;; undetermined clause.
-          (_
-           (define-values (rest-pred subs*)
-             (eval-predicate (apply predicate:or rest)))
-           (match rest-pred
-             ;; All of the other 'or' clauses have failed, so the
-             ;; 'or' can be removed entirely and reduced to the
-             ;; undetermined predicate.
-             (#f (values new-pred '()))
-             ;; The rest of the 'or' succeeded, so we can form a
-             ;; series of 'substitute' forms so that if this
-             ;; undetermined clause fails the substitutions from the
-             ;; rest of 'or' will still be respected.
-             (#t
-              (values (predicate:or new-pred (predicate:substitutes subs*))
-                      '()))
-             ;; The rest of the 'or' clauses have an undetermined
-             ;; answer, so the result is an 'or'.
-             (_
-              (values (predicate:or new-pred rest-pred) '()))))))))
-    ;; An 'and' succeeds if *all* of the predicates within succeed.
-    (('and preds ...)
-     (match preds
-       ;; All of the 'and' clauses succeed, so the 'and' succeeds.
-       (()
-        (values #t '()))
-       ((pred* . rest)
-        (define-values (new-pred subs)
-          (eval-predicate pred*))
-        (match new-pred
-          ;; The first 'and' clause is successful, so test the rest of
-          ;; the clauses and compose the substitutes.
-          (#t
-           (let ()
-             (define-values (rest-pred subs*)
-               (eval-predicate (apply predicate:and rest)))
-             (match rest-pred
-               ;; The rest of the 'and' clauses are successful, so the
-               ;; entire 'and' is successful and we can return the
-               ;; substitutions.
-               (#t
-                (values #t (compose-substitutions subs subs*)))
-               ;; At least one of the remaining clauses has failed, so
-               ;; the 'and' fails.
-               (#f
-                (values #f '()))
-               ;; The rest of the 'and' is undetermined, so form a new
-               ;; and that will perform the substitutions generated by
-               ;; this clause if the rest of the 'and' eventually
-               ;; succeeds.
-               (_
-                (values (predicate:and rest-pred (predicate:substitutes subs))
-                        '())
-                ;; (values (predicate:and rest-pred)
-                ;;         subs*)
-                ))))
-          ;; The clause failed, so the 'and' fails.
-          (#f (values #f '()))
-          ;; The clause is undetermined, so evaluate the rest of the
-          ;; clauses and attempt to simply the resulting 'and'
-          ;; expression.
-          (_
-           (define-values (rest-pred subs*)
-             (eval-predicate (apply predicate:and rest)))
-           (match rest-pred
-             ;; One of the remaining clauses fails, so even if the
-             ;; undetermined clause were to succeed later, the 'and'
-             ;; is going to fail so just fail now.
-             (#f (values #f '()))
-             ;; The remaining clauses pass, so we replace them with
-             ;; substitutions that will occur should this
-             ;; undertermined clause eventually succeed.
-             (#t
-              (values (predicate:and new-pred (predicate:substitutes subs*))
-                      '()))
-             ;; The remaining clauses have an undetermined result, so
-             ;; construct a new 'and'.
-             (_
-              (values (predicate:and new-pred rest-pred) '()))))))))
-    ;; A 'list' predicate is like an 'or' except if any clause
-    ;; succeeds the substitutions are propagated to the caller along
-    ;; with a new list withou the successful clause.  This is how
-    ;; multiple independent predicates are composed.
-    (('list preds ...)
-     (match preds
-       ;; No predicates, no failure.
-       (() (values #t '()))
-       ((pred* . rest)
-        (define-values (new-pred subs)
-          (eval-predicate pred*))
-        (match new-pred
-          ;; This clause succeeded, so remove it from the result, eval
-          ;; the rest of the clauses, and pass along the substitutions.
-          (#t
-           (let ()
-             (define-values (rest-pred subs*)
-               (eval-predicate (apply predicate:list rest)))
-             (values rest-pred (compose-substitutions subs subs*))))
-          ;; This clause failed, so the whole predicate fails.
-          (#f (values #f '()))
-          ;; There isn't enough information to determine if this
-          ;; clause will succeed or fail.  So, we evaluate the rest of
-          ;; the clauses and compose the result with this undetermined
-          ;; clause.
-          (_
-           (define-values (rest-pred subs*)
-             (eval-predicate (apply predicate:list rest)))
-           (match rest-pred
-             (#f (values #f '()))
-             (#t (values new-pred subs*))
-             (_ (values (predicate:list pred* rest-pred) subs*))))))))
-    ;; Substitution always succeeds and returns a substitution to be
-    ;; carried forward in the inference process.
-    (('substitute a b)
-     (values #t (list (cons a b))))
-    ;; Substitute the field var when struct has been resolved to a
-    ;; struct type.
-    (('struct-field struct field field-var)
-     (if (struct-type? struct)
-         (let ((field-type (struct-type-ref struct field)))
-           (if field-type
-               (values #t (list (cons field-var field-type)))
-               (values #f '())))
-         (values pred '())))
-    ;; Substitute the element var when array has been resolved to an
-    ;; array type.
-    (('array-element array element-var)
-     (if (array-type? array)
-         (values #t (list (cons element-var (array-type-ref array))))
-         (values pred '())))))
-
-(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
-    (seagull-type-error "type predicate failed" (list pred) eval-predicate*))
-  ;; Recursively evaluate the predicate, applying the substitutions
-  ;; generated by the last evaluation, until it cannot be simplified
-  ;; any further.
-  (if (null? pred-subs)
-      (values new-pred subs)
-      (eval-predicate* new-pred (compose-substitutions subs pred-subs))))
-
 (define* (free-variables-in-type type)
   (cond
    ((or (primitive-type? type)
@@ -2228,25 +2197,13 @@
 
 (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))
-    (('list preds ...)
-     (append-map (lambda (pred)
-                   (free-variables-in-predicate pred))
-                 preds))
-    (('substitute a b)
+    ((or #t #f) '())
+    (((or '= 'substitute) a b)
      (append (free-variables-in-type a)
              (free-variables-in-type b)))
+    (((or 'and 'or 'compose) a b)
+     (append (free-variables-in-predicate a)
+             (free-variables-in-predicate b)))
     (('struct-field struct field var)
      (append (free-variables-in-type struct)
              (free-variables-in-type var)))
@@ -2260,7 +2217,8 @@
   (if (function-type? type)
       (match (difference (delete-duplicates
                           (append (free-variables-in-type type)
-                                  (free-variables-in-predicate pred)))
+                                  (free-variables-in-predicate
+                                   (type-predicate-exp pred))))
                          (free-variables-in-env env))
         (() type)
         ((quantifiers ...)
@@ -2282,12 +2240,12 @@
    (if (qualified-type? type)
        (apply-substitutions-to-predicate (qualified-type-predicate type)
                                          subs)
-       #t)))
+       predicate:succeed)))
 
 (define (maybe-instantiate type)
   (if (type-scheme? type)
       (instantiate type)
-      (values type #t)))
+      (values type predicate:succeed)))
 
 (define (unify:primitives a b)
   (if (equal? a b)
@@ -2358,7 +2316,7 @@
                         type:bool)))
                 x)
           '()
-          #t))
+          predicate:succeed))
 
 (define (infer:variable name env)
   (define-values (type pred)
@@ -2371,7 +2329,7 @@
   (let loop ((exps exps)
              (texps '())
              (subs '())
-             (pred #t))
+             (pred predicate:succeed))
     (match exps
       (()
        (values (reverse texps) subs pred))
@@ -2379,7 +2337,7 @@
        (define-values (texp subs* pred*)
          (infer-exp exp env))
        (define-values (new-pred combined-subs)
-         (eval-predicate* (compose-predicates pred pred*)
+         (eval-predicate* (predicate:compose pred pred*)
                           (compose-substitutions subs subs*)))
        (loop rest
              (cons texp texps)
@@ -2411,9 +2369,9 @@
     (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))
+    (eval-predicate* (predicate:compose predicate-pred
+                                        consequent-pred
+                                        alternate-pred)
                      combined-subs-2))
   ;; ;; Apply final set of substitutions to the types of both branches.
   (define consequent-texp*
@@ -2443,7 +2401,7 @@
                                       (texp-types body*))
                        pred env))
                 `(lambda ,params ,body*))
-          subs #t))
+          subs predicate:succeed))
 
 (define (infer:primitive-call operator args env)
   (define primitive (lookup-seagull-primitive operator))
@@ -2465,7 +2423,7 @@
   ;; 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)
+    (eval-predicate* (predicate:compose operator-pred arg-pred)
                      (compose-substitutions arg-subs call-subs)))
   (values (texp (apply-substitutions-to-types return-vars combined-subs)
                 `(primcall ,operator
@@ -2501,8 +2459,8 @@
                           return-vars)))
   ;; Eval predicate.
   (define-values (pred combined-subs)
-    (eval-predicate* (compose-predicates operator-pred
-                                         arg-pred)
+    (eval-predicate* (predicate:compose 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)
@@ -2519,8 +2477,8 @@
   (define exp-type (single-type exp*))
   (define tvar (fresh-variable-type))
   (define-values (pred combined-subs)
-    (eval-predicate* (compose-predicates (predicate:struct-field exp-type field tvar)
-                                         exp-pred)
+    (eval-predicate* (predicate:compose (predicate:struct-field exp-type field tvar)
+                                        exp-pred)
                      exp-subs))
   (values (texp (list (apply-substitutions-to-type tvar combined-subs))
                 `(struct-ref ,(apply-substitutions-to-texp exp* combined-subs)
@@ -2543,9 +2501,9 @@
     (unify (apply-substitutions-to-type index-type combined-subs) type:int))
   (define tvar (fresh-variable-type))
   (define-values (pred subs)
-    (eval-predicate* (compose-predicates (predicate:array-element array-type tvar)
-                                         (compose-predicates array-exp-pred
-                                                             index-exp-pred))
+    (eval-predicate* (predicate:compose (predicate:array-element array-type tvar)
+                                         array-exp-pred
+                                         index-exp-pred)
                      (compose-substitutions combined-subs unify-subs)))
   (define array-exp**
     (apply-substitutions-to-texp array-exp* subs))
@@ -2568,7 +2526,7 @@
   (define-values (body* body-subs body-pred)
     (infer-exp body env*))
   (define-values (pred combined-subs)
-    (eval-predicate* (compose-predicates exp-pred body-pred)
+    (eval-predicate* (predicate:compose exp-pred body-pred)
                      (compose-substitutions exp-subs body-subs)))
   (define bindings
     (map (lambda (name exp)
@@ -2599,7 +2557,7 @@
   (define-values (body* body-subs body-pred)
     (infer-exp body env*))
   (define-values (pred combined-subs)
-    (eval-predicate* (compose-predicates exp-pred body-pred)
+    (eval-predicate* (predicate:compose exp-pred body-pred)
                      (compose-substitutions exp-subs body-subs)))
   (define bindings
     (map (lambda (names exp)
@@ -2658,7 +2616,7 @@
        (define-values (texp subs* pred*)
          (infer-exp exp env))
        (define-values (new-pred combined-subs)
-         (eval-predicate* (compose-predicates pred pred*)
+         (eval-predicate* (predicate:compose pred pred*)
                           (compose-substitutions subs subs*)))
        (define env*
          (apply-substitutions-to-env (extend-env name (single-type texp) env)
@@ -2687,11 +2645,11 @@
            (_ #f))
          bindings))
   (define-values (exps exp-subs exp-pred env*)
-    (infer-bindings bindings '() '() #t env))
+    (infer-bindings bindings '() '() predicate:succeed env))
   (define-values (body* body-subs body-pred)
     (infer-exp body env*))
   (define-values (pred combined-subs)
-    (eval-predicate* (compose-predicates exp-pred body-pred)
+    (eval-predicate* (predicate:compose exp-pred body-pred)
                      (compose-substitutions exp-subs body-subs)))
   (define bindings*
     (map (match-lambda*
@@ -3549,6 +3507,17 @@ Run the partial evaluator on EXP for shader STAGE."
   (parameterize ((unique-identifier-counter 0))
     (pretty-print (simplify* (expand* exp stage)))))
 
+(define-meta-command ((seagull-infer chickadee) repl stage exp)
+  "seagull-infer STAGE EXP
+Run type inference on EXP for shader STAGE."
+  (parameterize ((unique-identifier-counter 0))
+    (pretty-print
+     (infer-types (hoist-functions*
+                   (prune
+                    (simplify*
+                     (expand* exp stage))))
+                  stage))))
+
 (define-meta-command ((seagull-inspect chickadee) repl module)
   "seagull-inspect MODULE
 Show the intermediate compiled form of MODULE."